From c9ed329bc24d1796cbb5e4e14b1b4ec742575dee Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Fri, 30 Sep 2022 19:13:03 -0400 Subject: [PATCH] finish frame rule proof --- bedrock2/src/bedrock2/FrameRule.v | 182 ++++++++++++++++++---- bedrock2/src/bedrock2/Map/DisjointUnion.v | 2 + bedrock2/src/bedrock2/Map/split_alt.v | 17 ++ 3 files changed, 168 insertions(+), 33 deletions(-) create mode 100644 bedrock2/src/bedrock2/Map/split_alt.v diff --git a/bedrock2/src/bedrock2/FrameRule.v b/bedrock2/src/bedrock2/FrameRule.v index 2e53b68c6..4e1f56b26 100644 --- a/bedrock2/src/bedrock2/FrameRule.v +++ b/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. diff --git a/bedrock2/src/bedrock2/Map/DisjointUnion.v b/bedrock2/src/bedrock2/Map/DisjointUnion.v index 941f15593..9f2d6957d 100644 --- a/bedrock2/src/bedrock2/Map/DisjointUnion.v +++ b/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). diff --git a/bedrock2/src/bedrock2/Map/split_alt.v b/bedrock2/src/bedrock2/Map/split_alt.v new file mode 100644 index 000000000..041054c6a --- /dev/null +++ b/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.