Finish rules_Store

theories/rules/rules_Store.v

@@ -172,15 +172,17 @@ Section cap_lang_rules.
     iModIntro.
     iIntros (wa) "(%Hppc & %Hpmema & %Hcorrpc & %Hdinstr) Hcred".
 
-    iApply (wp_wp2 (φ1 := exec_optL_Store lregs lmem r1 r2)).
+    iApply (wp_wp2 (φ1 := exec_optL_Store lregs lmem r1 r2) (φ2 := _)).
+    (* unsolved existential, see bottom of proof... :( *)
 
     iApply wp_opt2_bind. iApply wp_opt2_eqn_both.
     iMod (state_interp_transient_intro_nodfracs (lm := lmem) with "[$Hregs $Hσ Hmem Hpca]") as "Hσ".
     { iCombine "Hpca Hmem" as "Hmem".
-      rewrite -(big_sepM_insert (fun x y => mapsto x (DfracOwn (pos_to_Qp 1)) y)). Set Printing Notations. iFrame. rewrite insert_delete. iFrame. auto. Search (delete ?x ?y !! ?x = None). rewrite lookup_delete. done. }
-    iApply (wp2_word_of_argument with "[Hφ Hcred $Hσ]"). { set_solver. }
-    iIntros (r2v) "Hσ %Hlr2v %Hr2v".
+      rewrite -(big_sepM_insert (fun x y => mapsto x (DfracOwn (pos_to_Qp 1)) y)).
+      rewrite insert_delete. iFrame. auto. by rewrite lookup_delete. }
+    iApply (wp2_word_of_argument (lrt := lregs) (lw := lw) with "[Hφ Hcred $Hσ]"). { set_solver. }
 
+    iIntros (r2v) "Hσ %Hlr2v %Hr2v".
     iApply wp_opt2_bind. iApply wp_opt2_eqn_both.
     iApply (wp2_reg_lookup with "[$Hσ Hφ Hcred]") ; first by set_solver.
     iIntros (r1v) "Hσ %Hlr1v %Hr1v".
@@ -196,31 +198,31 @@ Section cap_lang_rules.
       constructor 2 with (lmem' := lmem); try easy. now constructor 1 with (lw := r1v). }
 
     iIntros (p b e a v) "%Heqlwr1v %Heqgwr1v".
+
+    destruct r1v; try destruct sb; unfold reg_allows_store;
+    auto; inversion Heqlwr1v; inversion Heqgwr1v; subst.
     destruct (writeAllowed p && withinBounds b e a)  eqn:?; cbn. all: revgoals.
     { (* failure case: no valid capability for writing to memory *)
       iDestruct (state_interp_transient_elim_abort with "Hσ") as "($ & Hregs & Hmem)".
       iModIntro. rewrite big_sepM_fmap. iApply ("Hφ" with "[$Hregs $Hmem]").
       iPureIntro. constructor 2 with (lmem' := lmem); try easy.
-      constructor 2 with (p := p) (b := b) (e := e) (a := a) (v := v).
-      - destruct r1v; cbn in *; try destruct sb; cbn; inversion Heqgwr1v; inversion Heqlwr1v; subst. apply Hlr1v.
-      - rewrite andb_false_iff in Heqb0. destruct Heqb0; auto. }
+      constructor 2 with (p := p) (b := b) (e := e) (a := a) (v := v); auto.
+      by rewrite andb_false_iff in Heqb0. }
 
     (* valid capability for writing to memory *)
 
     destruct HaStore as [p' [b' [e' [a' [v' [Hreadreg Hlmem]]]]]].
     rewrite decide_True in Hlmem. destruct Hlmem as [oldlw Hlmem].
     2: { unfold read_reg_inr in *. rewrite Hlr1v in Hreadreg.
-         destruct r1v; try destruct sb; unfold reg_allows_store;
-         auto; inversion Heqlwr1v; inversion Heqgwr1v; subst.
          rewrite andb_true_iff in Heqb0. destruct Heqb0 as [Hwrite Hinbounds].
-         inversion Hreadreg. subst. auto. }
+         inversion Hreadreg; subst. unfold reg_allows_store; auto. }
     rewrite updatePC_incrementPC. cbn.
 
     iApply wp_opt2_bind. iApply wp_opt2_eqn_both.
-
     unfold read_reg_inr in *. rewrite Hlr1v in Hreadreg.
-    destruct r1v; try destruct sb; inversion Heqlwr1v;
-    inversion Hreadreg; subst.
+    inversion Heqlwr1v; inversion Hreadreg; subst.
+
+    (* update the transient logical memory to have a' point to the value in r2 *)
     rewrite (update_state_interp_transient_from_mem_mod _ (a', v') r2v _).
     2: { intros cur_map Hcurr. apply (word_of_argumentL_cur Hlr2v Hcurr). }
     2: {  rewrite lookup_fmap. unfold LMem, LAddr in *. rewrite option_fmap_compose.
@@ -243,13 +245,14 @@ Section cap_lang_rules.
     rewrite -fmap_insert big_sepM_fmap; cbn.
     iApply ("Hφ" with "[$Hmem $Hregs]").
     iPureIntro.
-    rewrite andb_true_iff in Heqb0; destruct Heqb0 as [Hwrite Hinbounds].
 
     apply (Store_spec_success _ _ _ _ _ _ p' b' e' a' v' r2v oldlw); auto.
+    unfold reg_allows_store.
+    rewrite andb_true_iff in Heqb0; destruct Heqb0 as [Hwrite Hinbounds].
+    auto.
 
-    unfold reg_allows_store. auto.
-
-  Admitted.
+    Unshelve. exact lregs'. (* awkward... *)
+  Qed.
 
   Lemma wp_store_success_z_PC E pc_p pc_b pc_e pc_a pc_v pc_a' lw z :
      decodeInstrWL lw = Store PC (inl z) →
@@ -347,7 +350,7 @@ Section cap_lang_rules.
        Instr Executable @ E
        {{{ RET NextIV;
            PC ↦ᵣ LCap pc_p pc_b pc_e pc_a' pc_v
-        Alexandre Moine      ∗ (pc_a, pc_v) ↦ₐ LCap pc_p pc_b pc_e pc_a pc_v }}}.
+           ∗ (pc_a, pc_v) ↦ₐ LCap pc_p pc_b pc_e pc_a pc_v }}}.
    Proof.
   (*    iIntros (Hinstr Hvpc Hpca' Hwa φ) *)
   (*           "(>HPC & >Hi) Hφ". *)