RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2023-06-13T11:00:05Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/155Cleanup new Lithium Syntax2023-06-13T11:00:05ZMichael SammlerCleanup new Lithium Syntaxhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/154simpler definition of simplify_goal2023-06-07T10:21:16ZMichael Sammlersimpler definition of simplify_goalhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/153Automatically generate typeclass instances2023-06-06T13:06:44ZMichael SammlerAutomatically generate typeclass instanceshttps://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/151Verify scheduler data structure2023-06-21T01:04:45ZKimaya BedarkarVerify scheduler data structure- The refinement type for message is also changed to use the ID which is generated from the arrival sequence.
- Verify two functions in the scheduler.h file that enqueue and dequeue messages.- The refinement type for message is also changed to use the ID which is generated from the arrival sequence.
- Verify two functions in the scheduler.h file that enqueue and dequeue messages.https://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/146Draft: Verification of enqueue and dequeue functions2023-04-21T09:34:32ZKimaya BedarkarDraft: Verification of enqueue and dequeue functionshttps://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/144Verification of bitmap with 256 priorities2023-04-20T13:05:12ZKimaya BedarkarVerification of bitmap with 256 priorities- Delete the old bitmap library supporting 64 priorities.
- Add and use new bitmap library supporting 256 priorities.- Delete the old bitmap library supporting 64 priorities.
- Add and use new bitmap library supporting 256 priorities.https://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/139WIP: Update to new Iris language interface2022-08-10T07:32:39ZMichael SammlerWIP: Update to new Iris language interfaceUpdate to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/825/Update to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/825/Michael SammlerMichael Sammlerhttps://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/137update Iris for later credits2022-07-08T21:43:16ZRalf Jungjung@mpi-sws.orgupdate Iris for later creditsShould help with the nightly build failures. Unfortunately I cannot easily test this locally since the project does not seem to work with ProofGeneral out-of-the-box
```
Error: Cannot find a physical path bound to logical path type with ...Should help with the nightly build failures. Unfortunately I cannot easily test this locally since the project does not seem to work with ProofGeneral out-of-the-box
```
Error: Cannot find a physical path bound to logical path type with prefix refinedc.typing.
```
Note sure what that is about. I see some `_build` things in `_CoqProject`. Maybe dune stuff? Anyway something that breaks the workflow I have been using for 10 years... so let's just see what CI says. ;)
(`make builddep` insists on installing cerberus which I don't want to do since I just want to change some Coq files.)Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/136update Iris2022-05-13T16:15:28ZMichael Sammlerupdate Iris