refactoring

_CoqProject

@@ -77,7 +77,8 @@ theories/stacked_borrows/steps_inv.v
 theories/stacked_borrows/tactics.v 
 theories/stacked_borrows/class_instances.v
 theories/stacked_borrows/tkmap_view.v
-theories/stacked_borrows/heap.v
+theories/stacked_borrows/logical_state.v
+theories/stacked_borrows/inv_accessors.v
 theories/stacked_borrows/steps_refl.v
 theories/stacked_borrows/steps_opt.v
 theories/stacked_borrows/primitive_laws.v

theories/stacked_borrows/examples/opt1.v

 From simuliris.simulation Require Import lifting.
-From simuliris.stacked_borrows Require Import proofmode defs lang heap.
+From simuliris.stacked_borrows Require Import primitive_laws proofmode.
 Set Default Proof Using "Type".
 
 (** Moving read of mutable reference up across code not using that ref. *)
@@ -47,7 +47,7 @@ Definition ex1_opt : ectx :=
     Free "x" ;;
     "v".
 
-Lemma sim_new_place_local `{sborG Σ} T v_t v_s π Φ :
+Lemma sim_new_place_local `{sborGS Σ} T v_t v_s π Φ :
   ⌜length v_t = length v_s⌝ -∗
   (∀ t l,
     ⌜length v_s = tsize T⌝ -∗
@@ -88,7 +88,7 @@ Qed.
   then we could use the above generic lemma for [new_place].
    currently we don't use it since, in order to apply it, we'd need to use UB that happens during its execution...
 *)
-Lemma sim_opt1 `{sborG Σ} π :
+Lemma sim_opt1 `{sborGS Σ} π :
   ⊢ sim_ectx rrel π ex1_opt ex1_unopt rrel.
 Proof.
   iIntros (r_t r_s) "Hrel".
@@ -162,7 +162,7 @@ Definition ex1_opt' : ectx :=
     Free "x" ;;
     "v".
 
-Lemma sim_opt1' `{sborG Σ} π :
+Lemma sim_opt1' `{sborGS Σ} π :
   ⊢ sim_ectx rrel π ex1_opt' ex1_unopt rrel.
 Proof.
   iIntros (r_t r_s) "Hrel".

theories/stacked_borrows/examples/opt1_down.v

 From simuliris.simulation Require Import lifting.
-From simuliris.stacked_borrows Require Import proofmode defs lang heap.
+From simuliris.stacked_borrows Require Import primitive_laws proofmode.
 Set Default Proof Using "Type".
 
 (** Moving a read of a mutable reference down across code that *may* use that ref. *)
@@ -46,7 +46,7 @@ Definition ex1_down_opt : ectx :=
 
 (*Lemma value_rel_poison *)
 
-Lemma sim_opt1_down `{sborG Σ} π :
+Lemma sim_opt1_down `{sborGS Σ} π :
   ⊢ sim_ectx rrel π ex1_down_opt ex1_down_unopt rrel.
 Proof.
   iIntros (r_t r_s) "Hrel".

theories/stacked_borrows/examples/opt2.v

@@ -50,7 +50,7 @@ Definition ex2_opt : ectx :=
     "v"
   .
 
-Lemma sim_opt2 `{sborG Σ} π :
+Lemma sim_opt2 `{sborGS Σ} π :
   ⊢ sim_ectx rrel π ex2_opt ex2_unopt rrel.
 Proof.
   iIntros (r_t r_s) "Hrel".
@@ -161,7 +161,7 @@ Definition ex2_opt' : ectx :=
   .
 
 
-Lemma sim_opt2' `{sborG Σ} π :
+Lemma sim_opt2' `{sborGS Σ} π :
   ⊢ sim_ectx rrel π ex2_opt' ex2_unopt' rrel.
 Proof.
   iIntros (r_t r_s) "Hrel".

theories/stacked_borrows/examples/pure.v

@@ -2,7 +2,7 @@ From simuliris.stacked_borrows Require Import proofmode.
 
 (** * Some trivial tests to check that the proofmode works *)
 Section boring_lang.
-Context `{sborG Σ}.
+Context `{sborGS Σ}.
 
 Definition val_rel (r1 r2 : result) : iProp Σ := ⌜r1 = r2⌝.
 (*Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.*)

theories/stacked_borrows/primitive_laws.v

-(** This file proves the basic laws of the BorIngLang program logic by applying
-the Simuliris lifting lemmas. *)
-
+(* Re-export steps *)
 From iris.proofmode Require Export tactics.
-From iris.bi.lib Require Import fractional.
-From iris.base_logic.lib Require Import ghost_map.
 From simuliris.base_logic Require Export gen_sim_heap gen_sim_prog.
 From simuliris.simulation Require Export slsls.
-From simuliris.simulation Require Import lifting.
-From simuliris.stacked_borrows Require Export class_instances tactics notation heap steps_refl steps_opt.
-From iris.prelude Require Import options.
-
-
-
-(** Program assertions *)
-Notation "f '@t' Kt" := (hasfun (hG:=gen_prog_inG_target) f Kt)
-  (at level 20, format "f  @t  Kt") : bi_scope.
-Notation "f '@s' Ks" := (hasfun (hG:=gen_prog_inG_source) f Ks)
-  (at level 20, format "f  @s  Ks") : bi_scope.
-
-
-Section lifting.
-Context `{!sborG Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : result → result → iProp Σ.
-Implicit Types σ σ_s σ_t : state.
-Implicit Types r r_s r_t : result.
-Implicit Types l : loc.
-Implicit Types f : fname.
-
-Context (Ω : result → result → iProp Σ).
-
-
-(** Program for target *)
-Lemma hasfun_target_agree f K_t1 K_t2 : f @t K_t1 -∗ f @t K_t2 -∗ ⌜K_t1 = K_t2⌝.
-Proof. apply hasfun_agree. Qed.
-
-(** Program for source *)
-Lemma hasfun_source_agree f K_s1 K_s2 : f @s K_s1 -∗ f @s K_s2 -∗ ⌜K_s1 = K_s2⌝.
-Proof. apply hasfun_agree. Qed.
-
-End lifting.
+From simuliris.stacked_borrows Require Export class_instances tactics notation defs logical_state steps_refl steps_opt.

theories/stacked_borrows/proofmode.v

@@ -11,7 +11,7 @@ From simuliris.stacked_borrows Require Export primitive_laws notation.
 
 
 Section sim.
-Context `{!sborG Σ}.
+Context `{!sborGS Σ}.
 Context (Ω : result → result → iProp Σ).
 (*Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{Ω} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.*)
 (*Local Notation "et '⪯' es [{ Φ }]" := (et ⪯{Ω} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.*)
@@ -133,9 +133,6 @@ Proof.
   iIntros "H". iApply source_red_bind. by iApply Hs.
 Qed.
 
-(* TODO: heap tactics *)
-
-
 
 (** Switching between judgments *)
 Lemma tac_to_target Δ e_t e_s Φ π :

theories/stacked_borrows/steps_refl.v

 From iris.proofmode Require Export tactics.
-From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
 From simuliris.base_logic Require Export gen_sim_prog.
 From simuliris.simulation Require Export slsls.
 From simuliris.simulation Require Import lifting.
-From iris.prelude Require Import options.
 From simuliris.stacked_borrows Require Import tkmap_view.
 From simuliris.stacked_borrows Require Export defs.
 From simuliris.stacked_borrows Require Import steps_progress steps_retag steps_inv.
-From simuliris.stacked_borrows Require Import heap.
+From simuliris.stacked_borrows Require Import logical_state inv_accessors.
+From iris.prelude Require Import options.
 
 Section lifting.
-Context `{!sborG Σ}.
+Context `{!sborGS Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : expr → expr → iProp Σ.
 Implicit Types σ σ_s σ_t : state.
@@ -67,10 +66,10 @@ Proof.
   - (* state rel *)
     rewrite -{2}(map_empty_union M_t).
     subst σ_s' α' nt. rewrite -{2}Hsst_eq.
-    iApply sim_alloc_state_rel_update; last done.
+    iApply state_rel_alloc_update; last done.
     intros t (s & Hs) ->. congruence.
   - (* call interp *)
-    iPureIntro. apply sim_alloc_call_set_interp_update; done.
+    iPureIntro. apply call_set_interp_alloc_update; done.
   - (* tag interp *)
     iPureIntro. destruct Htag_interp as (Htag_interp & Hdom_t & Hdom_s). split_and!.
     { simpl. intros t tk. rewrite lookup_insert_Some. intros [[<- [= <-]] | [Hneq Hsome]].
@@ -199,6 +198,7 @@ Proof.
   - iPureIntro. by eapply head_step_wf.
 Qed.
 
+(** TODO: generalize, move, and use it for the opt lemmas too *)
 Lemma sim_copy_public_controlled_update σ l l' (bor : tag) (T : type) (α' : stacks) (t : ptr_id) (tk : tag_kind) sc :
   memory_read σ.(sst) σ.(scs) l bor (tsize T) = Some α' →
   state_wf σ →
@@ -392,6 +392,7 @@ Proof.
 Qed.
 
 (** Write *)
+(* TODO: generalize, move, and use for opt steps too *)
 Lemma loc_controlled_write_public σ bor tk l l' T α' sc v t :
   state_wf σ →
   (bor = Tagged t → tk = tk_pub) →
@@ -647,9 +648,9 @@ Proof.
       - (* old tags are preserved *)
         simpl. specialize (Htag_interp _ _ Hsome') as (? & ? & Hcontrolled_t & Hcontrolled_s & Hdom).
         split_and!; [lia | lia | | | ].
-        + intros. eapply retag_loc_controlled_preserved; [ done | done | | done | by apply Hcontrolled_t].
+        + intros. eapply loc_controlled_retag_update; [ done | done | | done | by apply Hcontrolled_t].
           intros <-. move : Hpub. rewrite /untagged_or_public. congruence.
-        + intros. eapply retag_loc_controlled_preserved; [ done | done | | done | by apply Hcontrolled_s].
+        + intros. eapply loc_controlled_retag_update; [ done | done | | done | by apply Hcontrolled_s].
           intros <-. move : Hpub. rewrite /untagged_or_public. congruence.
         + done.
     }