RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2023-06-05T13:53:48Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/152remove specialized typeclasses2023-06-05T13:53:48ZMichael Sammlerremove specialized typeclasseshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/150Refactor Lithium2023-06-01T16:36:45ZMichael SammlerRefactor Lithiumhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/149Refactor the Lithium files2023-05-31T09:41:17ZMichael SammlerRefactor the Lithium fileshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/148Unbundle rtype to make more things typeclasses opaque2023-05-30T14:56:53ZMichael SammlerUnbundle rtype to make more things typeclasses opaqueGives a around 5% performance win: https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=refinedc&var-branch=All&var-config=All&var-group=%28%29.%2A&from=1684544604618&to=1685458516969Gives a around 5% performance win: https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=refinedc&var-branch=All&var-config=All&var-group=%28%29.%2A&from=1684544604618&to=1685458516969https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/147use primitive projections for iProp_to_Prop2023-05-14T09:15:35ZMichael Sammleruse primitive projections for iProp_to_PropSmall performance win: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=a09a919f04f114de27a324641b36edbdd5242ed0&var-config1=build-coq.8.17.0-timing&var-branch2=time%2FiPro...Small performance win: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=a09a919f04f114de27a324641b36edbdd5242ed0&var-config1=build-coq.8.17.0-timing&var-branch2=time%2FiProp_to_Prop_primitive_proj&var-commit2=f43db09c385c0212f59c894e694ae730dea86ac3&var-config2=build-coq.8.17.0-timing&var-metric=instructions&var-group=(.*)https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/145add bitmap with 256 priorities2023-06-16T16:47:48ZKimaya Bedarkaradd bitmap with 256 priorities- Fix small errors in Coqproject and Makefile for scheduler
- Delete bitmap with 64 priorities
- Add bitmap with 256 priorities- Fix small errors in Coqproject and Makefile for scheduler
- Delete bitmap with 64 priorities
- Add bitmap with 256 prioritieshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/143add note in developers.md for mlgmpidl library and small corrections in the a...2023-04-04T09:06:37ZKimaya Bedarkaradd note in developers.md for mlgmpidl library and small corrections in the annotations docshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/142Fix W.subst_l slowdown2023-03-07T11:38:55ZLennard Gähergaeher@mpi-sws.orgFix W.subst_l slowdownThis fixes a slowdown where the time `simpl` takes to simplify `W.subst_l` blows up exponentially with the number of local variables.
(In RefinedRust, the current definition therefore makes it intractable to verify functions with 30+ loc...This fixes a slowdown where the time `simpl` takes to simplify `W.subst_l` blows up exponentially with the number of local variables.
(In RefinedRust, the current definition therefore makes it intractable to verify functions with 30+ local variables).
In my tests, the new definition has performed measurably better once more than 19-20 variables are involved, while performing similarly on fewer variables.
Thus, there is no measurable advantage for the current RefinedC case studies, but in case someone ever verifies a function with lots of local variables, this might still be useful.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/141Port to 8.16.02022-09-13T15:24:26ZMichael SammlerPort to 8.16.0https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/140Change implementation of the --no-mem-cast flag2022-09-12T12:18:49ZMichael SammlerChange implementation of the --no-mem-cast flaghttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/138update Iris for later credits2022-07-07T20:33:09ZRalf Jungjung@mpi-sws.orgupdate Iris for later creditsLike https://gitlab.mpi-sws.org/iris/refinedc/-/merge_requests/137 but hopefully with CI. :)Like https://gitlab.mpi-sws.org/iris/refinedc/-/merge_requests/137 but hopefully with CI. :)https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/136update Iris2022-05-13T16:15:28ZMichael Sammlerupdate Irishttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/135add and verify simpler bitmap implementation2022-05-03T12:02:49ZKimaya Bedarkaradd and verify simpler bitmap implementationThis MR introduces the file `priority_modified.h`. This file contains an alternate implementation of the bitmap that only supports 64 priorities and is, therefore, easier to verify. This alternate implementation of the bitmap is fully ve...This MR introduces the file `priority_modified.h`. This file contains an alternate implementation of the bitmap that only supports 64 priorities and is, therefore, easier to verify. This alternate implementation of the bitmap is fully verified.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/133example scheduler2022-05-11T21:10:25ZMichael Sammlerexample schedulerhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/131Fix res_ty for rc_annot2022-02-23T16:02:16ZMichael SammlerFix res_ty for rc_annotWithout this MR code like
```
u16 rateval = rc_bitfield_init(u16, "rate_sig");
```
generates
```
f_code := (
<[ "#0" :=
"rateval" <-{ IntOp u16 }
LocInfoE loc_708 (UnOp (CastOp $ IntOp u16) (IntOp i32) (LocInfoE l...Without this MR code like
```
u16 rateval = rc_bitfield_init(u16, "rate_sig");
```
generates
```
f_code := (
<[ "#0" :=
"rateval" <-{ IntOp u16 }
LocInfoE loc_708 (UnOp (CastOp $ IntOp u16) (IntOp i32) (LocInfoE loc_708 (AnnotExpr 1%nat (BitfieldInitAnnot (rate_sig)) (LocInfoE loc_709 (UnOp (CastOp $ IntOp u16) (IntOp i32) (LocInfoE loc_710 (i2v 0 i32))))))) ;
```
Note that this contains a cast too much.
This MR fixes this issue and a similar issue for the ternary operator.
@lepigre Does this fix make sense?https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/130fix some typos in the tutorial2022-02-17T13:33:21ZKimaya Bedarkarfix some typos in the tutorialFixed some typos I found in t00 and t01.Fixed some typos I found in t00 and t01.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/129Create a separate coq-lithium package2022-02-28T08:45:47ZMichael SammlerCreate a separate coq-lithium packageThis MR creates a separate coq-lithium packages such that one can install Lithium without needing to pull in the full RefinedC (especially without needing to compile cerberus). Sadly, we need a hack to remove `lithium` from the refinedc ...This MR creates a separate coq-lithium packages such that one can install Lithium without needing to pull in the full RefinedC (especially without needing to compile cerberus). Sadly, we need a hack to remove `lithium` from the refinedc `dune` files before installing, since otherwise `dune` gets confused.
@lepigre any thoughts on this?https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/128Add VerifyThis2021 solutions2021-12-09T13:31:50ZMichael SammlerAdd VerifyThis2021 solutionshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/127Add notation for tyexists2021-12-06T15:17:10ZMichael SammlerAdd notation for tyexistshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/126Remove Movable typeclass2021-12-03T15:31:54ZMichael SammlerRemove Movable typeclass