RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2024-02-27T14:25:19Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/175better implementation of trigger_foralls2024-02-27T14:25:19ZMichael Sammlerbetter implementation of trigger_forallshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/174port to Coq 8.19.02024-02-26T11:18:25ZMichael Sammlerport to Coq 8.19.0https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/173create evars for Type in liExist2024-02-16T11:27:39ZMichael Sammlercreate evars for Type in liExisthttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/172add ci to all branches except noci branches2024-02-06T08:22:06ZMichael Sammleradd ci to all branches except noci brancheshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/171Verification of receive messages and check channels2024-03-28T11:37:55ZKimaya BedarkarVerification of receive messages and check channelsThis MR adds the specs for `receive_messages` and `receive_one_message`. Some of the previous specs for `receive_one_message` and `read` have also been changed following a change in the underlying ground truth.This MR adds the specs for `receive_messages` and `receive_one_message`. Some of the previous specs for `receive_one_message` and `read` have also been changed following a change in the underlying ground truth.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/170Draft: Add specs for some more functions2024-02-02T15:10:45ZKimaya BedarkarDraft: Add specs for some more functionshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/169update to Coq 8.18.02023-11-30T09:49:33ZMichael Sammlerupdate to Coq 8.18.0https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/168Add prosa progress2023-09-26T14:56:24ZKimaya BedarkarAdd prosa progresshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/167change the return value of read2023-09-26T14:14:28ZKimaya Bedarkarchange the return value of readhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/166Add specs for malloc and free2023-08-25T13:32:20ZMichael SammlerAdd specs for malloc and freehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/165Add a stronger function subtyping rule2023-08-29T12:16:06ZLaila ElbeheiryAdd a stronger function subtyping ruleAdd a stronger rule for subsumption between function pointer typesAdd a stronger rule for subsumption between function pointer typeshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/164add annotation support for evar instantiation2023-08-25T13:44:13ZLaila Elbeheiryadd annotation support for evar instantiationUsing `lvar` and `set_lvar`, users can now control how lithium instantiates an existential variable in the proof search procedure.Using `lvar` and `set_lvar`, users can now control how lithium instantiates an existential variable in the proof search procedure.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/163Draft: Ci/pkvm hof2023-08-23T10:41:37ZLaila ElbeheiryDraft: Ci/pkvm hofhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/162verify receive one message function2023-08-29T14:04:32ZKimaya Bedarkarverify receive one message function- Add/Modify some typing rules
- Modify the type for `message` struct to use an `array_p`
- Add one assumption to the specs for `read`- Add/Modify some typing rules
- Modify the type for `message` struct to use an `array_p`
- Add one assumption to the specs for `read`https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/161Use more Hint Extern instead of IsEx2023-07-31T15:14:50ZMichael SammlerUse more Hint Extern instead of IsExNot a big win, but probably still worth it: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=3ba9876efb0884f13fd3a01abb54cffbefa78cbb&var-config1=build-coq.8.17.0-timing&va...Not a big win, but probably still worth it: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=3ba9876efb0884f13fd3a01abb54cffbefa78cbb&var-config1=build-coq.8.17.0-timing&var-branch2=time%2Fmore_hint_extern&var-commit2=0960c81d01f651d1df4c18358bfd56a5351758f5&var-config2=build-coq.8.17.0-timing&var-metric=instructions&var-group=%28%29.%2Ahttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/160Make existentials more lazy2023-07-31T14:24:38ZMichael SammlerMake existentials more lazyTiming gets worse, but it is not bad: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=4f0ad0efffb973e77de370367d0785027e5ed6cc&var-config1=build-coq.8.17.0-timing&var-bran...Timing gets worse, but it is not bad: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=4f0ad0efffb973e77de370367d0785027e5ed6cc&var-config1=build-coq.8.17.0-timing&var-branch2=time%2Flazy_ex&var-commit2=3ba9876efb0884f13fd3a01abb54cffbefa78cbb&var-config2=build-coq.8.17.0-timing&var-metric=instructions&var-group=%28%29.%2A
For Islaris, this MR even improves performance: https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?from=1690301582547&to=1690813398415&var-metric=instructions&var-project=isla-coq&var-branch=All&var-config=All&var-group=%28%29.%2Ahttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/159Keep sideconditions inside the iris ctx2023-07-25T15:50:10ZMichael SammlerKeep sideconditions inside the iris ctxThis is in preparation to keep existential quantifiers in the goal. It has even a small benefit for performance: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=f3820ba52a...This is in preparation to keep existential quantifiers in the goal. It has even a small benefit for performance: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=f3820ba52a435b7f9afea16180514dde65b639f4&var-config1=build-coq.8.17.0-timing&var-branch2=time%2Fkeep_sidecond_in_goal&var-commit2=6946308078465f20d49245f3eb486eb60217afcd&var-config2=build-coq.8.17.0-timing&var-metric=instructions&var-group=%28.%2A%29https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/158Remove continuation from SimplAnd and SimplImpl2023-07-25T14:32:26ZMichael SammlerRemove continuation from SimplAnd and SimplImplhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/157Verify fds data structure functions2023-07-19T06:24:25ZKimaya BedarkarVerify fds data structure functionshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/156add scheduler data structure2023-06-27T11:35:40ZKimaya Bedarkaradd scheduler data structure- Changes to the message queue library to make verification of scheduler data structure possible
- Verifying the enqueue and dequeu operations of the scheduler data structure- Changes to the message queue library to make verification of scheduler data structure possible
- Verifying the enqueue and dequeu operations of the scheduler data structureKimaya BedarkarKimaya Bedarkar