diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Hoare.v | 50 | ||||
| -rw-r--r-- | lib/coq/Sail2_state.v | 30 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_lemmas.v | 101 |
3 files changed, 180 insertions, 1 deletions
diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v index 400630af..c91814b0 100644 --- a/lib/coq/Hoare.v +++ b/lib/coq/Hoare.v @@ -530,6 +530,16 @@ destruct b as [H | H]. * apply (HY H). reflexivity. Qed. +Lemma PrePostE_match_sum_branch (*[PrePostE_compositeI]:*) Regs A Ety X Y (b : sumbool X Y) (f : X -> monadS Regs A Ety) (g : Y -> monadS Regs A Ety) Pf Pg Q E : + (forall H : X, b = left H -> PrePostE (Pf H) (f H) Q E) -> + (forall H : Y, b = right H -> PrePostE (Pg H) (g H) Q E) -> + PrePostE (fun s => match b with left H => Pf H s | right H => Pg H s end) (match b with left H => f H | right H => g H end) Q E. +intros HX HY. +destruct b as [H | H]. +* apply (HX H). reflexivity. +* apply (HY H). reflexivity. +Qed. + Lemma PrePostE_if Regs A Ety (b : bool) (f g : monadS Regs A Ety) P Q E : (b = true -> PrePostE P f Q E) -> (b = false -> PrePostE P g Q E) -> @@ -764,6 +774,43 @@ apply PrePost_foreachS_invariant with (Q := fun v => match v with Value a => Q a auto. Qed. +Lemma PrePostE_foreach_ZS_up_invariant Regs Vars Ety from to step (H : Sail2_values.ArithFact (0 < step)%Z) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) : + (forall i range vars, PrePostE (Q vars) (body i range vars) Q E) -> + PrePostE (Q vars) (foreach_ZS_up from to step vars body) Q E. +intro INV. +unfold foreach_ZS_up. +match goal with +| |- context[@foreach_ZS_up' _ _ _ _ _ _ _ _ _ ?pf _ _] => generalize pf +end. +generalize 0%Z at 2 3 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros. +* simpl. destruct (Sumbool.sumbool_of_bool (from + off <=? to)%Z); apply PrePostE_returnS. +* simpl. destruct (Sumbool.sumbool_of_bool (from + off <=? to)%Z). + + eapply PrePostE_bindS. + - intro. apply IHn. + - apply INV. + + apply PrePostE_returnS. +Qed. + +Lemma PrePostE_foreach_ZS_down_invariant Regs Vars Ety from to step (H : Sail2_values.ArithFact (0 < step)%Z) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) : + (forall i range vars, PrePostE (Q vars) (body i range vars) Q E) -> + PrePostE (Q vars) (foreach_ZS_down from to step vars body) Q E. +intro INV. +unfold foreach_ZS_down. +match goal with +| |- context[@foreach_ZS_down' _ _ _ _ _ _ _ _ _ ?pf _ _] => generalize pf +end. +generalize 0%Z at 1 3 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros. +* simpl. destruct (Sumbool.sumbool_of_bool (to <=? from + off)%Z); apply PrePostE_returnS. +* simpl. destruct (Sumbool.sumbool_of_bool (to <=? from + off)%Z). + + eapply PrePostE_bindS. + - intro. apply IHn. + - apply INV. + + apply PrePostE_returnS. +Qed. Lemma PrePostE_use_pre Regs A Ety m (P : predS Regs) (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : (forall s, P s -> PrePostE P m Q E) -> @@ -1077,9 +1124,12 @@ Ltac PrePostE_step := [ eapply PrePostE_if_branch; intros | eapply PrePostE_if_sum_branch; intros ] + | |- PrePostE _ (match _ with left _ => _ | right _ => _ end) _ _ => + eapply PrePostE_match_sum_branch; intros | |- PrePostE _ (readS _) ?ppeQ ?ppeE => apply PrePostE_readS with (Q := ppeQ) (E := ppeE) | |- PrePostE _ (assert_expS _ _) _ _ => apply PrePostE_assert_expS | |- PrePostE _ (assert_expS' _ _) _ _ => apply PrePostE_assert_expS' + | |- PrePostE _ (maybe_failS _ _) _ _ => apply PrePostE_maybe_failS | |- PrePostE _ (exitS _) _ ?E => apply (PrePostE_exitS _ _ _ _ _ E) | |- PrePostE _ (and_boolS _ _) _ _ => eapply PrePostE_and_boolS | |- PrePostE _ (or_boolS _ _) _ _ => eapply PrePostE_or_boolS diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v index 618ca3a5..0cfc9f17 100644 --- a/lib/coq/Sail2_state.v +++ b/lib/coq/Sail2_state.v @@ -30,6 +30,36 @@ Fixpoint foreachS {A RV Vars E} (xs : list A) (vars : Vars) (body : A -> Vars -> foreachS xs vars body end. +(* This uses the same subproof as the prompt version to get around proof relevance issues + in Sail2_state_lemmas. TODO: if we switch to boolean properties this shouldn't be + necessary. *) +Fixpoint foreach_ZS_up' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> monadS rv Vars e) {struct n} : monadS rv Vars e. +exact ( + match sumbool_of_bool (from + off <=? to) with left LE => + match n with + | O => returnS vars + | S n => body (from + off) (foreach_ZM_up'_subproof _ _ _ _ _ _ LE) vars >>$= fun vars => foreach_ZS_up' rv e Vars from to step (off + step) n _ (foreach_ZM_up'_subproof0 _ _ _ _) vars body + end + | right _ => returnS vars + end). +Defined. + +Fixpoint foreach_ZS_down' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> monadS rv Vars e) {struct n} : monadS rv Vars e. +exact ( + match sumbool_of_bool (to <=? from + off) with left LE => + match n with + | O => returnS vars + | S n => body (from + off) (foreach_ZM_down'_subproof _ _ _ _ _ _ LE) vars >>$= fun vars => foreach_ZS_down' _ _ _ from to step (off - step) n _ (foreach_ZM_down'_subproof0 _ _ _ _) vars body + end + | right _ => returnS vars + end). +Defined. + +Definition foreach_ZS_up {rv e Vars} from to step vars body `{ArithFact (0 < step)} := + foreach_ZS_up' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. +Definition foreach_ZS_down {rv e Vars} from to step vars body `{ArithFact (0 < step)} := + foreach_ZS_down' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. + (*val genlistS : forall 'a 'rv 'e. (nat -> monadS 'rv 'a 'e) -> nat -> monadS 'rv (list 'a) 'e*) Definition genlistS {A RV E} (f : nat -> monadS RV A E) n : monadS RV (list A) E := let indices := List.seq 0 n in diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v index dd83f239..e5394f32 100644 --- a/lib/coq/Sail2_state_lemmas.v +++ b/lib/coq/Sail2_state_lemmas.v @@ -28,6 +28,42 @@ Add Parametric Morphism {Regs A Vars E : Type} : (@foreachS A Regs Vars E) apply foreachS_cong. Qed. +Lemma foreach_ZS_up_cong rv e Vars from to step vars body body' H : + (forall a pf vars, body a pf vars === body' a pf vars) -> + @foreach_ZS_up rv e Vars from to step vars body H === foreach_ZS_up from to step vars body'. +intro EQ. +unfold foreach_ZS_up. +match goal with +| |- @foreach_ZS_up' _ _ _ _ _ _ _ _ _ ?pf _ _ === _ => generalize pf +end. +generalize 0 at 2 3 4 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros; simpl. +* reflexivity. +* destruct (sumbool_of_bool (from + off <=? to)); auto. + rewrite EQ. + setoid_rewrite IHn. + reflexivity. +Qed. + +Lemma foreach_ZS_down_cong rv e Vars from to step vars body body' H : + (forall a pf vars, body a pf vars === body' a pf vars) -> + @foreach_ZS_down rv e Vars from to step vars body H === foreach_ZS_down from to step vars body'. +intro EQ. +unfold foreach_ZS_down. +match goal with +| |- @foreach_ZS_down' _ _ _ _ _ _ _ _ _ ?pf _ _ === _ => generalize pf +end. +generalize 0 at 1 3 4 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros; simpl. +* reflexivity. +* destruct (sumbool_of_bool (to <=? from + off)); auto. + rewrite EQ. + setoid_rewrite IHn. + reflexivity. +Qed. + Local Opaque _limit_reduces. Ltac gen_reduces := match goal with |- context[@_limit_reduces ?a ?b ?c] => generalize (@_limit_reduces a b c) end. @@ -227,11 +263,15 @@ Ltac statecong db := let ty := type of x in match ty with | bool => eapply if_bool_cong; statecong db - | sumbool _ _ => eapply if_sumbool_cong; statecong db + | sumbool _ _ => eapply if_sumbool_cong; statecong db (* There's also a dependent case below *) | _ => apply equiv_reflexive end | |- (foreachS _ _ _) === _ => solve [ eapply foreachS_cong; intros; statecong db ] + | |- (foreach_ZS_up _ _ _ _ _) === _ => + solve [ eapply foreach_ZS_up_cong; intros; statecong db ] + | |- (foreach_ZS_down _ _ _ _ _) === _ => + solve [ eapply foreach_ZS_down_cong; intros; statecong db ] | |- (genlistS _ _) === _ => solve [ eapply genlistS_cong; intros; statecong db ] | |- (whileST _ _ _ _) === _ => @@ -260,6 +300,10 @@ Ltac statecong db := eapply (@equiv_transitive _ _ _ _ (match e1 with None => _ | Some _ => _ end) _); [ destruct e1; [> etransitivity; [> statecong db | apply equiv_reflexive ] ..] | apply equiv_reflexive ] + | |- (match ?e1 with left _ => _ | right _ => _ end) === _ => + eapply (@equiv_transitive _ _ _ _ (match e1 with left _ => _ | right _ => _ end) _); + [ destruct e1; [> etransitivity; [> statecong db | apply equiv_reflexive ] ..] + | apply equiv_reflexive ] | |- ?X => solve [ apply equiv_reflexive @@ -316,6 +360,19 @@ Hint Extern 0 (liftState _ ?t = _) => end end : liftState. +Lemma liftState_match_distrib_sumbool {Regs Regval A E P Q r x y} {c : sumbool P Q} : + @liftState Regs Regval A E r (match c with left H => x H | right H => y H end) = match c with left H => liftState r (x H) | right H => liftState r (y H) end. +destruct c; reflexivity. +Qed. +(* As above, but also need to beta reduce H into x and y. *) +Hint Extern 0 (liftState _ ?t = _) => + match t with + | match ?x with _ => _ end => + match type of x with + | sumbool _ _ => etransitivity; [apply liftState_match_distrib_sumbool | cbv beta; reflexivity ] + end + end : liftState. + Lemma liftState_let_pair Regs RegVal A B C E r (x : B * C) M : @liftState Regs RegVal A E r (let '(y, z) := x in M y z) = let '(y, z) := x in liftState r (M y z). @@ -656,6 +713,48 @@ Qed. Hint Rewrite liftState_foreachM : liftState. Hint Resolve liftState_foreachM : liftState. +Lemma liftState_foreach_ZM_up Regs Regval Vars E from to step vars body H r : + liftState (Regs := Regs) r + (@foreach_ZM_up Regval E Vars from to step vars body H) === + foreach_ZS_up from to step vars (fun z H' a => liftState r (body z H' a)). +unfold foreach_ZM_up, foreach_ZS_up. +match goal with +| |- liftState _ (@foreach_ZM_up' _ _ _ _ _ _ _ _ _ ?pf _ _) === _ => generalize pf +end. +generalize 0 at 2 3 4 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros. +* simpl. + rewrite_liftState. + reflexivity. +* simpl. + rewrite_liftState. + reflexivity. +Qed. +Hint Rewrite liftState_foreach_ZM_up : liftState. +Hint Resolve liftState_foreach_ZM_up : liftState. + +Lemma liftState_foreach_ZM_down Regs Regval Vars E from to step vars body H r : + liftState (Regs := Regs) r + (@foreach_ZM_down Regval E Vars from to step vars body H) === + foreach_ZS_down from to step vars (fun z H' a => liftState r (body z H' a)). +unfold foreach_ZM_down, foreach_ZS_down. +match goal with +| |- liftState _ (@foreach_ZM_down' _ _ _ _ _ _ _ _ _ ?pf _ _) === _ => generalize pf +end. +generalize 0 at 1 3 4 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros. +* simpl. + rewrite_liftState. + reflexivity. +* simpl. + rewrite_liftState. + reflexivity. +Qed. +Hint Rewrite liftState_foreach_ZM_down : liftState. +Hint Resolve liftState_foreach_ZM_down : liftState. + Lemma liftState_genlistM Regs Regval A E r f n : liftState (Regs := Regs) r (@genlistM A Regval E f n) === genlistS (fun x => liftState r (f x)) n. unfold genlistM, genlistS. |