extend partial wp_write_sc proof

theories/lang/lifting.v

@@ -13,7 +13,11 @@ Class lrustG Σ := LRustG {
 }.
 
 Definition heap_stbor_rel (m : mem) (st : stacks) : Prop :=
-  ∀ l : loc, is_Some (m !! l) → is_Some (st.(stks) !! l).
+  ∀ l : loc, is_Some (m !! l) ↔ is_Some (st.(stks) !! l).
+
+(* Section HeapRel *)
+(*   Lemma heap_stbor_rel_stable (m : mem) (st : stacks) : *)
+(* End HeapRel. *)
 
 Instance lrustG_irisG `{!lrustG Σ} : irisG lrust_lang Σ := {
   iris_invG := lrustG_invG;
@@ -138,6 +142,57 @@ Global Instance pure_if b e1 e2 :
 Proof. destruct b; solve_pure_exec. Qed.
 
 (** Heap *)
+Lemma wp_write_sc E l tg e v v' :
+  IntoVal e v →
+  {{{ ▷ l ↦ v' ∗ stbor_top l tg }}} Write ScOrd (Lit $ LitLoc l tg) e @ E
+  {{{ RET LitV LitPoison; l ↦ v ∗ stbor_top l tg }}}.
+Proof.
+  iIntros (<- Φ) "[>Hv Htop] HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 ???) "Hσ".
+  iDestruct "Hσ" as "(Hmem & Hstacks & #Hrel)". iDestruct "Hrel" as %Hrel.
+  iDestruct (heap_read_1 with "Hmem Hv") as %?.
+  iDestruct (stbor_pop_until_1 with "Hstacks Htop") as %[stk [Hlookup [stk' Hpop]]].
+  iMod (heap_write _ _ _  v with "Hmem Hv") as "[Hmem Hv]".
+  iMod (stbor_pop_until with "Hstacks Htop") as "[Hstacks Htop]".
+  { apply Hlookup. }
+  { apply Hpop. }
+  iModIntro; iSplit.
+  (* TODO: Umm... *)
+  { iPureIntro.
+    set (σ' := {| stks := <[l := stk']> (stks (ststks σ1)); sfreshtg := (sfreshtg (ststks σ1)); |}).
+    eexists. eexists. eexists. eexists. eapply WriteScS.
+    - apply to_of_val.
+    - econstructor. apply H.
+    - rewrite /stack_step.
+      instantiate (1 := σ'). simpl.
+      eapply StackWriteS.
+      + apply Hlookup.
+      + apply Hpop. }
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+  inversion H9; inversion H10. (* TODO: Don't refer to numerically named hypotheses *)
+  iModIntro; iSplit=> //. iFrame "Hmem".
+  iSplitL "Hstacks".
+  - rewrite H8 in Hlookup; inversion Hlookup; subst.
+    specialize (pop_until_deterministic _ _ _ _ Hpop H11) as Hdet.
+    rewrite -Hdet in H6. rewrite H6 H7.
+    iFrame "Hstacks".
+    iPureIntro.
+    rewrite /heap_stbor_rel.
+    admit.
+  - iApply "HΦ". iFrame.
+Admitted.
+
+(* Lemma wp_read_sc E l q v : *)
+(*   {{{ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E *)
+(*   {{{ RET v; l ↦{q} v }}}. *)
+(* Proof. *)
+(*   iIntros (?) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. *)
+(*   iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?]. *)
+(*   iModIntro; iSplit; first by eauto. *)
+(*   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. *)
+(*   iModIntro; iSplit=> //. iFrame. by iApply "HΦ". *)
+(* Qed. *)
+
 (* Lemma wp_alloc E (n : Z) : *)
 (*   0 < n → *)
 (*   {{{ True }}} Alloc (Lit $ LitInt n) @ E *)
@@ -165,17 +220,6 @@ Proof. destruct b; solve_pure_exec. Qed.
 (*   iModIntro; iSplit=> //. iFrame. iApply "HΦ"; auto. *)
 (* Qed. *)
 
-(* Lemma wp_read_sc E l q v : *)
-(*   {{{ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E *)
-(*   {{{ RET v; l ↦{q} v }}}. *)
-(* Proof. *)
-(*   iIntros (?) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. *)
-(*   iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?]. *)
-(*   iModIntro; iSplit; first by eauto. *)
-(*   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. *)
-(*   iModIntro; iSplit=> //. iFrame. by iApply "HΦ". *)
-(* Qed. *)
-
 (* Lemma wp_read_na E l q v : *)
 (*   {{{ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E *)
 (*   {{{ RET v; l ↦{q} v }}}. *)
@@ -194,18 +238,6 @@ Proof. destruct b; solve_pure_exec. Qed.
 (*   iFrame "Hσ". iSplit; [done|]. by iApply "HΦ". *)
 (* Qed. *)
 
-(* Lemma wp_write_sc E l e v v' : *)
-(*   IntoVal e v → *)
-(*   {{{ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E *)
-(*   {{{ RET LitV LitPoison; l ↦ v }}}. *)
-(* Proof. *)
-(*   iIntros (<- Φ) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. *)
-(*   iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?. *)
-(*   iMod (heap_write _ _ _  v with "Hσ Hv") as "[Hσ Hv]". *)
-(*   iModIntro; iSplit; first by eauto. *)
-(*   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. *)
-(*   iModIntro; iSplit=> //. iFrame. by iApply "HΦ". *)
-(* Qed. *)
 
 (* Lemma wp_write_na E l e v v' : *)
 (*   IntoVal e v → *)

theories/lang/stbor/ghost_stack.v

@@ -316,6 +316,15 @@ Section defs.
     iFrame "Htop Hheap Hstack Htopauth".
   Qed.
 
+  Lemma stack_pop_until_1 (γs : stack_names) (stk stk' : stack) (tg fresh : tag) :
+    stack_ctx γs stk fresh -∗
+    stack_top γs tg -∗ ⌜∃ stk', pop_until tg stk stk'⌝.
+  Proof.
+    iIntros "(Hbelow● & Hstack & Htop●) Htop".
+    iDestruct (stack_top_elem with "Htop● Htop") as %Helem.
+    iPureIntro. apply elem_pop_until; first assumption.
+  Qed.
+
   (* TODO: Might not need the view shift here *)
   Lemma stack_pop_until (γs : stack_names) (stk stk' : stack) (tg fresh : tag) :
     pop_until tg stk stk' →

theories/lang/stbor/ghost_stbor.v

@@ -122,6 +122,28 @@ Section defs.
     iFrame "Hstacks". iExists γs. iFrame "Hnames Hctx".
   Qed.
 
+  Lemma stbor_names_lookup (names : gmap loc stack_names) (l : loc) (γs : stack_names) :
+    stbor_names_auth names -∗
+    stbor_names l γs -∗
+    ⌜names !! l = Some γs⌝.
+  Proof.
+    iIntros "Hnames● Hγs".
+    iCombine "Hnames● Hγs" as "Hnames".
+    rewrite own_valid.
+    Set Printing All.
+    (* rewrite auth_both_valid. *)
+  Admitted.
+
+  Lemma stbor_pop_until_1 (l : loc) (stks : stacks_map) (tg fresh : tag) :
+    stbor_ctx' stks fresh -∗
+    stbor_top l tg -∗
+    ⌜∃ stk, stks !! l = Some stk ∧ ∃ stk', pop_until tg stk stk'⌝.
+  Proof.
+    iIntros "Hctx Htop". rewrite /stbor_ctx'.
+    iDestruct "Hctx" as (names) "(Hdom & Hnames● & Hstacks)".
+    iDestruct "Htop" as (γs) "[Hγs Htop]".
+  Admitted.
+
   Lemma stbor_pop_until (l : loc) (stks : stacks_map) (tg fresh : tag) (stk stk' : stack) :
     stks !! l = Some stk →
     pop_until tg stk stk' →

theories/lang/stbor/semantics.v

@@ -94,3 +94,20 @@ Proof.
   - exists stk. done.
   - assumption.
 Qed.
+
+Lemma elem_pop_until (tg : tag) (stk : stack) :
+  tg ∈ stk → ∃ stk', pop_until tg stk stk'.
+Proof.
+  intros Helem. induction Helem as [tg stk|tg tg' stk Helem IH].
+  - eexists. constructor.
+  - destruct IH as [stkout IH].
+    destruct (decide (tg = tg')) as [Heq|Hneq].
+    + rewrite Heq. eexists. constructor.
+    + eexists. constructor; done.
+Qed.
+
+Lemma pop_until_deterministic (tg : tag) (stk stk1 stk2 : stack) :
+  pop_until tg stk stk1 → pop_until tg stk stk2 → stk1 = stk2.
+Proof.
+  intros Hpop1 Hpop2. induction Hpop1; inversion Hpop2; try done; auto.
+Qed.