Merge branch 'master' of gitlab.mpi-sws.org:FP/stacked-borrows

theories/opt/ex1.v

@@ -28,7 +28,7 @@ Definition ex1_opt : function :=
 
 Lemma ex1_sim_body fs ft : ⊨{fs,ft} ex1 ≥ᶠ ex1_opt.
 Proof.
-  intros r es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
+  intros rf es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
   destruct els as [|efs []]; [done| |done].  simpl in SUBSTs.
   destruct elt as [|eft []]; [done| |done].  simpl in SUBSTt. simplify_eq.
 

theories/sim/cmra.v

@@ -293,3 +293,8 @@ Lemma tmap_lookup_core_pub (pm: tmapUR) t h:
   pm !! t ≡ Some (to_tagKindR tkPub, h) →
   core pm !! t ≡ Some (to_tagKindR tkPub, h).
 Proof. intros Eq. rewrite lookup_core Eq /core /= core_id //. Qed.
+
+(** Resources that we own. *)
+
+Definition res_callState (c: call_id) (cs: call_state) : resUR :=
+  ((ε, {[c := to_callStateR cs]}), ε).

theories/sim/instance.v

@@ -3,7 +3,7 @@ From stbor.sim Require Export local invariant.
 
 Notation "r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ" :=
   (sim_local_body wsat vrel_expr fs ft r n%nat es%E σs et%E σt Φ)
-  (at level 70, format "r  ⊨{ n , fs , ft }  ( es ,  σs )  ≥  ( et ,  σt )  :  Φ").
+  (at level 70, format "'[hv' r  ⊨{ n , fs , ft } '/  ' '[  ' ( es ,  σs ) ']' '/' ≥  '/  ' '[  ' ( et ,  σt ) ']'  '/' :  Φ ']'").
 
 Notation "⊨{ fs , ft } f1 ≥ᶠ f2" :=
   (sim_local_fun wsat vrel_expr fs ft end_call_sat f1 f2)

theories/sim/refl_step.v

@@ -850,7 +850,7 @@ Abort.
 Lemma sim_body_init_call fs ft r n es et σs σt Φ :
   let σs' := mkState σs.(shp) σs.(sst) (σs.(snc) :: σs.(scs)) σs.(snp) (S σs.(snc)) in
   let σt' := mkState σt.(shp) σt.(sst) (σt.(snc) :: σt.(scs)) σt.(snp) (S σt.(snc)) in
-  let r'  : resUR := ((ε, {[σt.(snc) := to_callStateR (csOwned ∅)]}), ε) in
+  let r'  : resUR := res_callState σt.(snc) (csOwned ∅) in
   r ⋅ r' ⊨{n,fs,ft} (es, σs') ≥ (et, σt') : Φ →
   r ⊨{n,fs,ft} (InitCall es, σs) ≥ (InitCall et, σt) : Φ.
 Proof.