finish frame rule proof

bedrock2/src/bedrock2/FrameRule.v

@@ -1,12 +1,15 @@
+Require Import Coq.ZArith.ZArith.
 Require Import coqutil.sanity coqutil.Macros.subst coqutil.Macros.unique coqutil.Byte.
 Require Import coqutil.Datatypes.PrimitivePair coqutil.Datatypes.HList.
 Require Import coqutil.Decidable.
 Require Import coqutil.Tactics.fwd coqutil.Tactics.Tactics.
-Require Import bedrock2.Notations bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord.
-Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth.
+Require Import bedrock2.Notations bedrock2.Syntax.
+Require Import coqutil.Map.Interface coqutil.Map.Properties coqutil.Map.OfListWord.
+Require Import coqutil.Word.Interface coqutil.Word.Bitwidth.
 Require Import bedrock2.MetricLogging.
-Require Import bedrock2.Memory.
+Require Import bedrock2.Memory bedrock2.ptsto_bytes bedrock2.Map.Separation.
 Require Import bedrock2.Semantics.
+Require Import bedrock2.Map.DisjointUnion bedrock2.Map.split_alt.
 
 Require Import Coq.Lists.List.
 
@@ -15,23 +18,96 @@ Section semantics.
   Context {locals: map.map String.string word}.
   Context {env: map.map String.string (list String.string * list String.string * cmd)}.
   Context {ext_spec: ExtSpec}.
+  Context {mem_ok: map.ok mem} {word_ok: word.ok word}.
 
   Lemma frame_load: forall mSmall mBig mAdd a r (v: word),
-      map.split mBig mSmall mAdd ->
+      mmap.split mBig mSmall mAdd ->
       load a mSmall r = Some v ->
       load a mBig r = Some v.
   Proof.
-  Admitted.
+    unfold load, load_Z. intros. fwd. eapply sep_of_load_bytes in E0.
+    2: destruct a; simpl; destruct width_cases as [W | W]; rewrite W; cbv; discriminate.
+    fwd. unfold sep in E0. fwd.
+    eapply map.split_alt in E0p0.
+    unfold mmap.split in *.
+    rewrite E0p0 in H.
+    rewrite mmap.du_assoc in H. unfold mmap.du in H at 1. fwd.
+    erewrite load_bytes_of_sep. 1: reflexivity.
+    unfold sep. do 2 eexists.
+    rewrite map.split_alt.
+    unfold mmap.split.
+    ssplit. 2: eassumption. all: simpl; exact H.
+  Qed.
+
+  (* TODO share with FlatToRiscvCommon *)
+
+  Lemma store_bytes_preserves_footprint: forall n a v (m m': mem),
+      Memory.store_bytes n m a v = Some m' ->
+      map.same_domain m m'.
+  Proof using word_ok mem_ok.
+    intros. unfold store_bytes, load_bytes, unchecked_store_bytes in *. fwd.
+    eapply map.putmany_of_tuple_preserves_domain; eauto.
+  Qed.
+
+  Lemma disjoint_putmany_preserves_store_bytes: forall n a vs (m1 m1' mq: mem),
+      store_bytes n m1 a vs = Some m1' ->
+      map.disjoint m1 mq ->
+      store_bytes n (map.putmany m1 mq) a vs = Some (map.putmany m1' mq).
+  Proof using word_ok mem_ok.
+    intros.
+    unfold store_bytes, load_bytes, unchecked_store_bytes in *. fwd.
+    erewrite map.getmany_of_tuple_in_disjoint_putmany by eassumption.
+    f_equal.
+    set (ks := (footprint a n)) in *.
+    rename mq into m2.
+    rewrite map.putmany_of_tuple_to_putmany.
+    rewrite (map.putmany_of_tuple_to_putmany n m1 ks vs).
+    apply map.disjoint_putmany_commutes.
+    pose proof map.getmany_of_tuple_to_sub_domain _ _ _ _ E as P.
+    apply map.sub_domain_value_indep with (vs2 := vs) in P.
+    set (mp := (map.putmany_of_tuple ks vs map.empty)) in *.
+    apply map.disjoint_comm.
+    eapply map.sub_domain_disjoint; eassumption.
+  Qed.
+
+  Lemma store_bytes_frame: forall {n: nat} {m1 m1' m: mem} {a: word} {v: HList.tuple byte n} {F},
+      Memory.store_bytes n m1 a v = Some m1' ->
+      (eq m1 * F)%sep m ->
+      exists m', (eq m1' * F)%sep m' /\ Memory.store_bytes n m a v = Some m'.
+  Proof using word_ok mem_ok.
+    intros.
+    unfold sep in H0.
+    destruct H0 as (mp & mq & A & B & C).
+    subst mp.
+    unfold map.split in A. destruct A as [A1 A2].
+    eexists (map.putmany m1' mq).
+    split.
+    - unfold sep.
+      exists m1', mq. repeat split; trivial.
+      apply store_bytes_preserves_footprint in H.
+      clear -H A2.
+      unfold map.disjoint, map.same_domain, map.sub_domain in *. destruct H as [P Q].
+      intros.
+      edestruct Q; eauto.
+    - subst m.
+      eauto using disjoint_putmany_preserves_store_bytes.
+  Qed.
 
   Lemma frame_store: forall sz (mSmall mSmall' mBig mAdd: mem) a v,
-      map.split mBig mSmall mAdd ->
+      mmap.split mBig mSmall mAdd ->
       store sz mSmall a v = Some mSmall' ->
-      exists mBig', map.split mBig' mSmall' mAdd /\ store sz mBig a v = Some mBig'.
+      exists mBig', mmap.split mBig' mSmall' mAdd /\ store sz mBig a v = Some mBig'.
   Proof.
-  Admitted.
+    intros. eapply (store_bytes_frame (F := eq mAdd)) in H0.
+    2: {
+      unfold sep. do 2 eexists. ssplit. 2,3: reflexivity. eapply map.split_alt; exact H.
+    }
+    fwd. unfold store, store_Z. rewrite H0p1. eexists. split. 2: reflexivity.
+    unfold sep in H0p0. fwd. eapply map.split_alt. assumption.
+  Qed.
 
   Lemma frame_eval_expr: forall l e mSmall mBig mAdd mc (v: word) mc',
-      map.split mBig mSmall mAdd ->
+      mmap.split mBig mSmall mAdd ->
       eval_expr mSmall l e mc = Some (v, mc') ->
       eval_expr mBig l e mc = Some (v, mc').
   Proof.
@@ -50,7 +126,7 @@ Section semantics.
 
   Lemma frame_evaluate_call_args_log: forall l mSmall mBig mAdd arges
                                              mc (args: list word) mc',
-      map.split mBig mSmall mAdd ->
+      mmap.split mBig mSmall mAdd ->
       evaluate_call_args_log mSmall l arges mc = Some (args, mc') ->
       evaluate_call_args_log mBig   l arges mc = Some (args, mc').
   Proof.
@@ -60,14 +136,12 @@ Section semantics.
       1: reflexivity. all: assumption.
   Qed.
 
-  Axiom TODO: False.
-
   Lemma frame_exec: forall e c t mSmall l mc P,
       exec e c t mSmall l mc P ->
       forall mBig mAdd,
-        map.split mBig mSmall mAdd ->
+        mmap.split mBig mSmall mAdd ->
         exec e c t mBig l mc (fun t' mBig' l' mc' =>
-          exists mSmall', map.split mBig' mSmall' mAdd /\ P t' mSmall' l' mc').
+          exists mSmall', mmap.split mBig' mSmall' mAdd /\ P t' mSmall' l' mc').
   Proof.
     induction 1; intros;
       try match goal with
@@ -79,19 +153,36 @@ Section semantics.
       intros.
       rename mCombined into mCombinedBig.
       specialize H1 with (1 := H3).
-      assert (map.split (map.putmany mSmall mStack) mSmall mStack) as Sp by case TODO.
-      specialize H1 with (1 := Sp).
-      specialize (H1 mCombinedBig mAdd).
-      assert (map.split mCombinedBig (map.putmany mSmall mStack) mAdd) as Sp' by case TODO.
-      specialize (H1 Sp').
+      specialize (H1 (mmap.force (mmap.du (Some mSmall) (Some mStack)))).
+      eapply map.split_alt in H4. pose proof H4 as D0. unfold mmap.split in D0.
+      rewrite H2 in D0.
+      rewrite (mmap.du_comm (Some mSmall) (Some mAdd)) in D0.
+      rewrite mmap.du_assoc in D0. unfold mmap.du at 1 in D0. fwd.
+      change (Some mCombinedBig = mmap.du (Some mAdd) (Some r)) in D0.
       eapply exec.weaken. 1: eapply H1.
+      { simpl. eapply map.split_alt. unfold mmap.split. symmetry. assumption. }
+      { unfold mmap.split. simpl. rewrite map.du_comm. exact D0. }
       cbv beta. intros. fwd.
-      assert (map.split m' (map.putmany mSmall'0 mAdd) mStack') as Sp'' by case TODO.
-      eexists. exists mStack'. ssplit.
-      1,2: eassumption.
+      move D0 at bottom.
+      repeat match reverse goal with
+             | H: map.split _ _ _ |- _ => eapply map.split_alt in H
+             | H: mmap.split _ _ _ |- _ =>
+                 unfold mmap.split in H;
+                 let F := fresh "D0" in
+                 rename H into F;
+                 move F at bottom
+             end.
+      rewrite D1 in D2. clear D1 mBig. rewrite D4 in D3. clear D4 mSmall'.
+      rewrite mmap.du_assoc in D3. rewrite (mmap.du_comm (Some mStack')) in D3.
+      rewrite <- mmap.du_assoc in D3.
+      eexists (mmap.force (mmap.du (Some mSmall'0) (Some mAdd))). exists mStack'. ssplit.
+      1: eassumption.
+      { simpl. eapply map.split_alt. unfold mmap.split.
+        rewrite D3. f_equal. unfold mmap.du at 1 in D3. fwd. simpl in E0. rewrite E0.
+        reflexivity. }
       eexists; split. 2: eassumption.
-      assert (map.split (map.putmany mSmall'0 mAdd) mSmall'0 mAdd) by case TODO.
-      assumption. }
+      unfold mmap.split. simpl.
+      unfold mmap.du at 1 in D3. fwd. simpl in E0. rewrite E0. reflexivity. }
     { eapply exec.seq. 1: eapply IHexec; eassumption.
       cbv beta. intros. fwd. eapply H1. 1: eassumption. assumption. }
     { eapply exec.while_true.
@@ -100,22 +191,47 @@ Section semantics.
       { eapply IHexec. 1: eassumption. }
       cbv beta. intros. fwd. eauto. }
     { (* call *)
-      case TODO. }
+      econstructor. 1: eassumption.
+      { eauto using frame_evaluate_call_args_log. }
+      1: eassumption.
+      1: eapply IHexec. 1: eassumption.
+      cbv beta. intros. fwd.
+      specialize H3 with (1 := H5p1). fwd. eauto 10. }
     { (* interact *)
-      assert (map.split mBig (map.putmany mKeep mAdd) mGive) as Sp by case TODO.
-      econstructor. 1: exact Sp.
+      eapply map.split_alt in H. pose proof H3 as A.
+      unfold mmap.split in H3, H. rewrite H in H3.
+      rewrite mmap.du_assoc in H3. rewrite (mmap.du_comm (Some mGive)) in H3.
+      rewrite <- mmap.du_assoc in H3.
+      assert (exists mKeepBig, Some mKeepBig = mmap.du (Some mKeep) (Some mAdd)) as Sp0. {
+        exists (mmap.force (map.du mKeep mAdd)).
+        unfold mmap.du in H3 at 1. fwd. simpl in E. rewrite E. reflexivity.
+      }
+      destruct Sp0 as (mKeepBig & Sp0).
+      assert (mmap.split mBig mKeepBig mGive) as Sp.
+      { unfold mmap.split. rewrite Sp0. assumption. }
+      econstructor. 1: eapply map.split_alt; exact Sp.
       { eauto using frame_evaluate_call_args_log. }
       1: eassumption.
       intros.
       specialize H2 with (1 := H4). fwd.
       eexists. split. 1: eassumption.
       intros.
-      assert (exists mSmall', map.split mSmall' mKeep mReceive) by case TODO.
-      fwd. exists mSmall'.
-      assert (map.split m' mSmall' mAdd) by case TODO.
-      split.
-      1: assumption.
-      eapply H2p1. assumption.
+      eapply map.split_alt in H2. unfold mmap.split in *.
+      assert (exists mSmall', mmap.split mSmall' mKeep mReceive) as Sp1. {
+        exists (mmap.force (map.du mKeep mReceive)).
+        eapply map.split_alt. rewrite Sp0 in H2.
+        rewrite mmap.du_assoc in H2. rewrite (mmap.du_comm (Some mAdd)) in H2.
+        rewrite <- mmap.du_assoc in H2.
+        unfold mmap.du at 1 in H2. fwd.
+        eapply map.split_alt. unfold mmap.split. simpl in E. simpl. rewrite E. reflexivity.
+      }
+      destruct Sp1 as (mSmall' & Sp1).
+      exists mSmall'. split. 2: eapply H2p1.
+      2: { eapply map.split_alt. exact Sp1. }
+      rewrite Sp0 in H2.
+      unfold mmap.split in Sp1. rewrite Sp1. rewrite mmap.du_assoc in H2.
+      rewrite (mmap.du_comm (Some mAdd)) in H2. rewrite <- mmap.du_assoc in H2.
+      exact H2.
     }
   Qed.
 

bedrock2/src/bedrock2/Map/DisjointUnion.v

@@ -309,6 +309,8 @@ Module mmap. Section __.
     unfold du. intros. fwd. f_equal. eapply map.du_inj_r; eassumption.
   Qed.
 
+  Definition split(m m1 m2: map): Prop :=
+    Some m = du (Some m1) (Some m2).
 End __. End mmap.
 
 Notation "a \*/ b" := (mmap.du a b) (at level 34, left associativity).

bedrock2/src/bedrock2/Map/split_alt.v

@@ -0,0 +1,17 @@
+Require Import coqutil.Map.Interface coqutil.Map.Properties.
+Require Import coqutil.Tactics.Tactics.
+Require Import coqutil.Tactics.fwd.
+Require Import bedrock2.Map.Separation.
+Require Export bedrock2.Map.DisjointUnion.
+
+Module map. Section __.
+  Context {key value} {map : map.map key value} {ok: map.ok map}.
+  Context {key_eqb: key -> key -> bool} {key_eq_dec: EqDecider key_eqb}.
+
+  Lemma split_alt: forall {m m1 m2: map}, map.split m m1 m2 <-> mmap.split m m1 m2.
+  Proof.
+    unfold map.split, mmap.split, mmap.du, map.du. split; intros; fwd.
+    - eapply map.disjointb_spec in Hp1. rewrite Hp1. reflexivity.
+    - split. 1: reflexivity. eapply map.disjointb_spec. assumption.
+  Qed.
+End __. End map.