Contextual refinement for Stacked Borrows
Merge request reports
Activity
added 14 commits
-
d100f24c...154b4d29 - 4 commits from branch
master - 6e6e9739 - Rename Ctx to Ectx
- 03aaaea3 - Add general contexts for stacked borrows
- 610b062e - Add Wf for stacked borrows
- 84da68f0 - Add parallel subst
- dd1c3748 - Fix stacked borrows' parallel subst to use result
- 3e70b1e2 - Add open logical relations for stacked borrows
- e55a542d - Fix with lint
- 1129c9f4 - Make tactics and proofmode more aware of results
- b662bf46 - Add more properties for proofmode/tactics concerning SB results
- 9b429499 - Add initial work on SB's compatibility lemmas
Toggle commit list-
d100f24c...154b4d29 - 4 commits from branch
added 2 commits
added 21 commits
-
9e9e2cad...e3cf8dac - 4 commits from branch
master - f3355954 - Rename Ctx to Ectx
- e4e7d0b1 - Add general contexts for stacked borrows
- c96b5837 - Add Wf for stacked borrows
- ff50c3f8 - Add parallel subst
- 3c6a60d1 - Fix stacked borrows' parallel subst to use result
- 217d5516 - Add open logical relations for stacked borrows
- 79fbbd92 - Fix with lint
- 01ac7ebe - Make tactics and proofmode more aware of results
- 692acf9d - Add more properties for proofmode/tactics concerning SB results
- a90b91e7 - Add initial work on SB's compatibility lemmas
- ce10293a - Avoid generated names in SB parallel subst
- ebd26555 - Add stub reflexivity for log_rel
- de22da1e - Add TODO for std++
- 49681918 - Add missing EndCallCtx
- 1e9c91f7 - Remove admits for some SB pure cases
- 8df4ae92 - Fix SB instances to deal with of_result
- 2edbe465 - More compatibility lemmas proven
Toggle commit list-
9e9e2cad...e3cf8dac - 4 commits from branch
@haidang please let me know once you want another round of feedback. :)
added 20 commits
-
2edbe465...0a89934a - 2 commits from branch
master - 1dcf4d48 - Rename Ctx to Ectx
- 727419e2 - Add general contexts for stacked borrows
- 1bd5f3a5 - Add Wf for stacked borrows
- 162635e0 - Add parallel subst
- dbdee243 - Fix stacked borrows' parallel subst to use result
- ed1c5850 - Add open logical relations for stacked borrows
- 66ef4003 - Fix with lint
- 316e05a4 - Make tactics and proofmode more aware of results
- ba3d6164 - Add more properties for proofmode/tactics concerning SB results
- c2579ca9 - Add initial work on SB's compatibility lemmas
- 42aa690a - Avoid generated names in SB parallel subst
- ea0baabe - Add stub reflexivity for log_rel
- 274fe211 - Add TODO for std++
- 33730f5a - Add missing EndCallCtx
- f5efd737 - Remove admits for some SB pure cases
- 46975f82 - Fix SB instances to deal with of_result
- 9f125b42 - More compatibility lemmas proven
- 9c73a780 - Prove more compatibility lemmas for SB
Toggle commit list-
2edbe465...0a89934a - 2 commits from branch
added 2 commits
- theories/stacked_borrows/refl.v 0 → 100644
288 solve_rrel_refl. 289 Qed. 290 291 Lemma log_rel_result v_t v_s : 292 rrel v_t v_s ⊢ log_rel (of_result v_t) (of_result v_s). 293 Proof. 294 iIntros "#Hv" (? xs) "!# #Hs"; simpl. rewrite !subst_map_of_result. 295 sim_val ; by iFrame. 296 Qed. 297 End log_rel. 298 299 Definition expr_head_wf (e : expr_head) : Prop := 300 match e with 301 | ValHead v => value_wf v 302 | InitCallHead => False (* administrative *) 303 | EndCallHead => False (* administrative *) changed this line in version 12 of the diff
I looked at the original semantics and this seems to be a problem. In the original semantics
InitCallandEndCallare generated and cannot be used by the client/context. This is becauseEndCalldoesn't have a trivial precondition. Indeed I cannot prove reflexivity ofEndCall, because ofsim_endcall:Lemma sim_endcall c π Φ : c @@ ∅ -∗ (* needs to be empty so we don't trip private locations *) #[☠] ⪯{π} #[☠] [{ Φ }] -∗ EndCall #[ScCallId c] ⪯{π} EndCall #[ScCallId c] [{ Φ }].-
Yes, we changed the semantics for Simuliris.
Edited by Ralf Jung -
So, the "value relation" for Call IDs (we should have something like that) should say the call IDs are "public" and thus ending them works any time.
@lgaeher how much of that is implemented?
I see. Right now
sc_rel (ScCallId c) (ScCallId c') := ⌜c = c'⌝. Isc @@ ∅the "public" condition you were talking about?Edited by Hai DangWe do not have a notion of public callids, but I now see that we are going to need it. I will need to add ghost state that owns the
c @@ \emptysetpersistently in the state interpretation and then that needs to be added to the screl. That should not be too hard, I think.(previously I was thinking that we'd just want to exclude
EndCallandInitCallinexpr_wfjust as in the original code, but that would be too restrictive since the original semantics could still insert it for calls).I'm working on it now.
Edited by Lennard Gäher
added 23 commits
-
40a24f96...3a255a85 - 2 commits from branch
master - afa61763 - Rename Ctx to Ectx
- 61e2f24d - Add general contexts for stacked borrows
- 1871763d - Add Wf for stacked borrows
- b28bfc22 - Add parallel subst
- 387604ac - Fix stacked borrows' parallel subst to use result
- d33bb4d8 - Add open logical relations for stacked borrows
- e1405881 - Fix with lint
- ca050fee - Make tactics and proofmode more aware of results
- a5d6f587 - Add more properties for proofmode/tactics concerning SB results
- d50bdc16 - Add initial work on SB's compatibility lemmas
- f4b00f46 - Avoid generated names in SB parallel subst
- cc6c4dbb - Add stub reflexivity for log_rel
- 67aaf536 - Add TODO for std++
- 2081390f - Add missing EndCallCtx
- d0baed70 - Remove admits for some SB pure cases
- bb5b0b40 - Fix SB instances to deal with of_result
- bec4aef2 - More compatibility lemmas proven
- 1d4d3934 - Prove more compatibility lemmas for SB
- a7110cc1 - Move some sim lemmas out of SB proofmode
- 8a6ae196 - Proven more SB compatibility lemmas
- cfb3c745 - Remove upstreamed lemmas
Toggle commit list-
40a24f96...3a255a85 - 2 commits from branch
