diff options
| -rw-r--r-- | _CoqProject | 6 | ||||
| -rw-r--r-- | src/Util/ForLoop.v | 89 | ||||
| -rw-r--r-- | src/Util/ForLoop/Instances.v | 67 | ||||
| -rw-r--r-- | src/Util/ForLoop/InvariantFramework.v | 369 | ||||
| -rw-r--r-- | src/Util/ForLoop/Tests.v | 55 | ||||
| -rw-r--r-- | src/Util/ForLoop/Unrolling.v | 314 | ||||
| -rw-r--r-- | src/Util/Loop.v | 480 |
7 files changed, 0 insertions, 1380 deletions
diff --git a/_CoqProject b/_CoqProject index 31249c067..8c376eb88 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6454,7 +6454,6 @@ src/Util/Factorize.v src/Util/FixCoqMistakes.v src/Util/FixedWordSizes.v src/Util/FixedWordSizesEquality.v -src/Util/ForLoop.v src/Util/FsatzAutoLemmas.v src/Util/GlobalSettings.v src/Util/HList.v @@ -6466,7 +6465,6 @@ src/Util/LetIn.v src/Util/LetInMonad.v src/Util/ListUtil.v src/Util/Logic.v -src/Util/Loop.v src/Util/NUtil.v src/Util/NatUtil.v src/Util/Notations.v @@ -6496,10 +6494,6 @@ src/Util/Bool/Equality.v src/Util/Bool/IsTrue.v src/Util/Decidable/Bool2Prop.v src/Util/Decidable/Decidable2Bool.v -src/Util/ForLoop/Instances.v -src/Util/ForLoop/InvariantFramework.v -src/Util/ForLoop/Tests.v -src/Util/ForLoop/Unrolling.v src/Util/ListUtil/FoldBool.v src/Util/ListUtil/Forall.v src/Util/Logic/ImplAnd.v diff --git a/src/Util/ForLoop.v b/src/Util/ForLoop.v deleted file mode 100644 index db12608e2..000000000 --- a/src/Util/ForLoop.v +++ /dev/null @@ -1,89 +0,0 @@ -(** * Definition and Notations for [for (int i = i₀; i < i∞; i += Δi)] *) -Require Import Coq.ZArith.BinInt. -Require Import Crypto.Util.Notations. -(** Note: These definitions are fairly tricky. See - https://github.com/mit-plv/fiat-crypto/issues/164 and - https://github.com/mit-plv/fiat-crypto/pull/163 for more - discussion. - - TODO: Fix the definitions to make them more obviously right. *) - -Section with_body. - Context {stateT : Type} - (body : nat -> stateT -> stateT). - - Fixpoint repeat_function (count : nat) (st : stateT) : stateT - := match count with - | O => st - | S count' => repeat_function count' (body count st) - end. -End with_body. - -Local Open Scope bool_scope. -Local Open Scope Z_scope. - -Definition for_loop {stateT} (i0 finish : Z) (step : Z) (initial : stateT) (body : Z -> stateT -> stateT) - : stateT - := let count := Z.to_nat (Z.quot (finish - i0 + step - Z.sgn step) step) in - repeat_function (fun c => body (i0 + step * Z.of_nat (count - c))) count initial. - - -Notation "'for' i (:= i0 ; += step ; < finish ) 'updating' ( state := initial ) {{ body }}" - := (for_loop i0 finish step initial (fun i state => body)) - : core_scope. - -Module Import ForNotationConstants. - Definition eq := @eq Z. - Module Z. - Definition ltb := Z.ltb. - Definition ltb' := Z.ltb. - Definition gtb := Z.gtb. - Definition gtb' := Z.gtb. - End Z. -End ForNotationConstants. - -Delimit Scope for_notation_scope with for_notation. -Notation "x += y" := (eq x (Z.pos y)) : for_notation_scope. -Notation "x -= y" := (eq x (Z.neg y)) : for_notation_scope. -Notation "++ x" := (x += 1)%for_notation : for_notation_scope. -Notation "-- x" := (x -= 1)%for_notation : for_notation_scope. -Notation "x ++" := (x += 1)%for_notation : for_notation_scope. -Notation "x --" := (x -= 1)%for_notation : for_notation_scope. -Infix "<" := Z.ltb : for_notation_scope. -Infix ">" := Z.gtb : for_notation_scope. -Notation "x <= y" := (Z.ltb' x (y + 1)) : for_notation_scope. -Notation "x >= y" := (Z.gtb' x (y - 1)) : for_notation_scope. - -Class class_eq {A} (x y : A) := make_class_eq : x = y. -Global Instance class_eq_refl {A x} : @class_eq A x x := eq_refl. - -Class for_loop_is_good (i0 : Z) (step : Z) (finish : Z) (cmp : Z -> Z -> bool) - := make_good : - ((Z.sgn step =? Z.sgn (finish - i0)) - && (cmp i0 finish)) - = true. -Hint Extern 0 (for_loop_is_good _ _ _ _) => vm_compute; reflexivity : typeclass_instances. - -Definition for_loop_notation {i0 : Z} {step : Z} {finish : Z} {stateT} {initial : stateT} - {cmp : Z -> Z -> bool} - step_expr finish_expr (body : Z -> stateT -> stateT) - {Hstep : class_eq (fun i => i = step) step_expr} - {Hfinish : class_eq (fun i => cmp i finish) finish_expr} - {Hgood : for_loop_is_good i0 step finish cmp} - : stateT - := for_loop i0 finish step initial body. - -Notation "'for' ( 'int' i = i0 ; finish_expr ; step_expr ) 'updating' ( state1 .. staten = initial ) {{ body }}" - := (@for_loop_notation - i0%Z _ _ _ initial%Z _ - (fun i : Z => step_expr%for_notation) - (fun i : Z => finish_expr%for_notation) - (fun (i : Z) => (fun state1 => .. (fun staten => body) .. )) - _ _ _). -Notation "'for' ( 'int' i = i0 ; finish_expr ; step_expr ) 'updating' ( state1 .. staten = initial ) {{ body }}" - := (@for_loop_notation - i0%Z _ _ _ initial%Z _ - (fun i : Z => step_expr%for_notation) - (fun i : Z => finish_expr%for_notation) - (fun (i : Z) => (fun state1 => .. (fun staten => body) .. )) - eq_refl eq_refl _). diff --git a/src/Util/ForLoop/Instances.v b/src/Util/ForLoop/Instances.v deleted file mode 100644 index 0a1f65e29..000000000 --- a/src/Util/ForLoop/Instances.v +++ /dev/null @@ -1,67 +0,0 @@ -Require Import Coq.omega.Omega. -Require Import Coq.Classes.Morphisms. -Require Import Crypto.Util.ForLoop. -Require Import Crypto.Util.Notations. - -Lemma repeat_function_Proper_rel_le {stateT} R f g n - (Hfg : forall c, 0 < c <= n -> forall s1 s2, R s1 s2 -> R (f c s1) (g c s2)) - s1 s2 (Hs : R s1 s2) - : R (@repeat_function stateT f n s1) (@repeat_function stateT g n s2). -Proof. - revert s1 s2 Hs. - induction n; simpl; auto. - intros; apply IHn; auto; - intros; apply Hfg; auto; - omega. -Qed. - -Global Instance repeat_function_Proper_rel {stateT} R - : Proper (pointwise_relation _ (R ==> R) ==> eq ==> R ==> R) (@repeat_function stateT) | 10. -Proof. - unfold pointwise_relation, respectful. - intros body1 body2 Hbody c y ?; subst y. - induction c; simpl; auto. -Qed. - -Lemma repeat_function_Proper_le {stateT} f g n - (Hfg : forall c, 0 < c <= n -> forall st, f c st = g c st) - st - : @repeat_function stateT f n st = @repeat_function stateT g n st. -Proof. - apply repeat_function_Proper_rel_le; try reflexivity; intros; subst; auto. -Qed. - -Global Instance repeat_function_Proper {stateT} - : Proper (pointwise_relation _ (pointwise_relation _ eq) ==> eq ==> eq ==> eq) (@repeat_function stateT). -Proof. - intros ???; eapply repeat_function_Proper_rel; repeat intro; subst. - unfold pointwise_relation, respectful in *; auto. -Qed. -About for_loop. - -Global Instance for_loop_Proper_rel {stateT} R i0 final step - : Proper (R ==> pointwise_relation _ (R ==> R) ==> R) (@for_loop stateT i0 final step) | 10. -Proof. - intros ?? Hinitial ?? Hbody; revert Hinitial. - unfold for_loop; eapply repeat_function_Proper_rel; - unfold pointwise_relation, respectful in *; auto. -Qed. - -Global Instance for_loop_Proper_rel_full {stateT} R - : Proper (eq ==> eq ==> eq ==> R ==> pointwise_relation _ (R ==> R) ==> R) (@for_loop stateT) | 20. -Proof. - intros ?????????; subst; apply for_loop_Proper_rel. -Qed. - -Global Instance for_loop_Proper {stateT} i0 final step initial - : Proper (pointwise_relation _ (pointwise_relation _ eq) ==> eq) (@for_loop stateT i0 final step initial). -Proof. - unfold pointwise_relation. - intros ???; eapply for_loop_Proper_rel; try reflexivity; repeat intro; subst; auto. -Qed. - -Global Instance for_loop_Proper_full {stateT} - : Proper (eq ==> eq ==> eq ==> eq ==> pointwise_relation _ (pointwise_relation _ eq) ==> eq) (@for_loop stateT) | 5. -Proof. - intros ????????????; subst; apply for_loop_Proper. -Qed. diff --git a/src/Util/ForLoop/InvariantFramework.v b/src/Util/ForLoop/InvariantFramework.v deleted file mode 100644 index 2bff6bef9..000000000 --- a/src/Util/ForLoop/InvariantFramework.v +++ /dev/null @@ -1,369 +0,0 @@ -(** * Proving properties of for-loops via loop-invariants *) -Require Import Coq.micromega.Psatz. -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Util.ForLoop. -Require Import Crypto.Util.ForLoop.Unrolling. -Require Import Crypto.Util.ZUtil. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.Tactics.UniquePose. -Require Import Crypto.Util.Notations. - -Lemma repeat_function_ind {stateT} (P : nat -> stateT -> Prop) - (body : nat -> stateT -> stateT) - (count : nat) (st : stateT) - (Pbefore : P count st) - (Pbody : forall c st, c < count -> P (S c) st -> P c (body (S c) st)) - : P 0 (repeat_function body count st). -Proof. - revert dependent st; revert dependent body; revert dependent P. - induction count as [|? IHcount]; intros P body Pbody st Pbefore; [ exact Pbefore | ]. - { rewrite repeat_function_unroll1_end; apply Pbody; [ omega | ]. - apply (IHcount (fun c => P (S c))); auto with omega. } -Qed. - -Local Open Scope bool_scope. -Local Open Scope Z_scope. - -Section for_loop. - Context (i0 finish : Z) (step : Z) {stateT} (initial : stateT) (body : Z -> stateT -> stateT) - (P : Z -> stateT -> Prop) - (Pbefore : P i0 initial) - (Pbody : forall c st n, c = i0 + n * step -> i0 <= c < finish \/ finish < c <= i0 -> P c st -> P (c + step) (body c st)) - (Hgood : Z.sgn step = Z.sgn (finish - i0)). - - Let countZ := (Z.quot (finish - i0 + step - Z.sgn step) step). - Let count := Z.to_nat countZ. - Let of_nat_count c := (i0 + step * Z.of_nat (count - c)). - Let nat_body := (fun c => body (of_nat_count c)). - - Local Arguments Z.mul !_ !_. - Local Arguments Z.add !_ !_. - Local Arguments Z.sub !_ !_. - - Local Lemma Hgood_complex : Z.sgn step = Z.sgn (finish - i0 + step - Z.sgn step). - Proof using Hgood. - clear -Hgood. - revert Hgood. - generalize dependent (finish - i0); intro z; intros. - destruct step, z; simpl in * |- ; try (simpl; omega); - repeat change (Z.sgn (Z.pos _)) with 1; - repeat change (Z.sgn (Z.neg _)) with (-1); - symmetry; - [ apply Z.sgn_pos_iff | apply Z.sgn_neg_iff ]; - lia. - Qed. - - Local Lemma Hcount_nonneg : 0 <= countZ. - Proof using Hgood. - apply Z.quot_nonneg_same_sgn. - symmetry; apply Hgood_complex. - Qed. - - Lemma for_loop_ind - : P (finish - Z.sgn (finish - i0 + step - Z.sgn step) * (Z.abs (finish - i0 + step - Z.sgn step) mod Z.abs step) + step - Z.sgn step) - (for_loop i0 finish step initial body). - Proof using Pbody Pbefore Hgood. - destruct (Z_zerop step). - { subst; unfold for_loop; simpl in *. - rewrite Z.quot_div_full; simpl. - symmetry in Hgood; rewrite Z.sgn_null_iff in Hgood. - assert (finish = i0) by omega; subst. - simpl; autorewrite with zsimplify_const; simpl; auto. } - assert (Hsgn_step : Z.sgn step <> 0) by (rewrite Z.sgn_null_iff; auto). - assert (Hsgn : Z.sgn ((finish - i0 + step - Z.sgn step) / step) = Z.sgn ((finish - i0 + step - Z.sgn step) / step) * Z.sgn (finish - i0 + step - Z.sgn step) * Z.sgn step) - by (rewrite <- Hgood_complex, <- Z.mul_assoc, <- Z.sgn_mul, (Z.sgn_pos (_ * _)) by nia; omega). - assert (Hfis_div : 0 <= (finish - i0 + step - Z.sgn step) / step) - by (apply Z.sgn_nonneg; rewrite Hsgn; apply Zdiv_sgn). - clear Hsgn. - let rhs := match goal with |- ?P ?rhs _ => rhs end in - assert (Heq : i0 + step * Z.of_nat count = rhs). - { unfold count, countZ. - rewrite Z.mod_eq by (rewrite Z.abs_0_iff; assumption). - rewrite Z.quot_div_full, <- !Z.sgn_abs, <- !Hgood_complex, !Zdiv_mult_cancel_r, !Z.mul_sub_distr_l by auto. - rewrite <- !Z.sgn_mul, !(Z.mul_comm _ (Z.sgn _)), !(Z.mul_assoc (Z.sgn _) _), <- Z.sgn_mul, Z.sgn_pos, !Z.mul_1_l by nia. - repeat rewrite ?Z.sub_add_distr, ?Z.sub_sub_distr; rewrite Z.sub_diag. - autorewrite with zsimplify_const. - rewrite Z2Nat.id by omega. - omega. } - rewrite <- Heq; clear Heq. - unfold for_loop. - generalize (@repeat_function_ind stateT (fun c => P (of_nat_count c)) nat_body count initial); - cbv beta in *. - unfold of_nat_count in *; cbv beta in *. - rewrite Nat.sub_diag, !Nat.sub_0_r. - autorewrite with zsimplify_const. - intro H; specialize (H Pbefore). - destruct (Z_dec' i0 finish) as [ Hs | Hs]. - { apply H; clear H Pbefore. - { intros c st Hc. - assert (Hclt : 0 < Z.of_nat (count - c)) by (apply (inj_lt 0); omega). - intro H'; specialize (fun pf' n pf => Pbody _ _ n pf pf' H'). - move Pbody at bottom. - { let T := match type of Pbody with ?T -> _ => T end in - let H := fresh in - cut T; [ intro H; specialize (Pbody H) | ]. - { revert Pbody. - subst nat_body; cbv beta. - rewrite Nat.sub_succ_r, Nat2Z.inj_pred by omega. - rewrite <- Z.sub_1_r, Z.mul_sub_distr_l, Z.mul_1_r. - rewrite <- !Z.add_assoc, !Z.sub_add in *. - refine (fun p => p (Z.of_nat (count - c) - 1) _). - lia. } - { destruct Hs; [ left | right ]. - { assert (Hstep : 0 < step) - by (rewrite <- Z.sgn_pos_iff, Hgood, Z.sgn_pos_iff; omega). - assert (0 < Z.of_nat (S c)) by (apply (inj_lt 0); omega). - assert (0 <= (finish - i0 + step - Z.sgn step) mod step) by auto with zarith. - assert (0 < step <= step * Z.of_nat (S c)) by nia. - split; [ nia | ]. - rewrite Nat2Z.inj_sub, Z.mul_sub_distr_l by omega. - unfold count. - rewrite Z2Nat.id by auto using Hcount_nonneg. - unfold countZ. - rewrite Z.mul_quot_eq_full by auto. - rewrite <- !Hgood_complex, Z.abs_sgn. - rewrite !Z.add_sub_assoc, !Z.add_assoc, Zplus_minus. - rewrite Z.sgn_pos in * by omega. - omega. } - { assert (Hstep : step < 0) - by (rewrite <- Z.sgn_neg_iff, Hgood, Z.sgn_neg_iff; omega). - assert (Hcsc0 : 0 <= Z.of_nat (count - S c)) by auto with zarith. - assert (Hsc0 : 0 < Z.of_nat (S c)) by lia. - assert (step * Z.of_nat (count - S c) <= 0) by (clear -Hcsc0 Hstep; nia). - assert (step * Z.of_nat (S c) <= step < 0) by (clear -Hsc0 Hstep; nia). - assert (finish - i0 < 0) - by (rewrite <- Z.sgn_neg_iff, <- Hgood, Z.sgn_neg_iff; omega). - assert (finish - i0 + step - Z.sgn step < 0) - by (rewrite <- Z.sgn_neg_iff, <- Hgood_complex, Z.sgn_neg_iff; omega). - assert ((finish - i0 + step - Z.sgn step) mod step <= 0) by (apply Z_mod_neg; auto with zarith). - split; [ | nia ]. - rewrite Nat2Z.inj_sub, Z.mul_sub_distr_l by omega. - unfold count. - rewrite Z2Nat.id by auto using Hcount_nonneg. - unfold countZ. - rewrite Z.mul_quot_eq_full by auto. - rewrite <- !Hgood_complex, Z.abs_sgn. - rewrite Z.sgn_neg in * by omega. - omega. } } } } } - { subst. - subst count nat_body countZ. - repeat first [ assumption - | rewrite Z.sub_diag - | progress autorewrite with zsimplify_const in * - | rewrite Z.quot_sub_sgn ]. } - Qed. -End for_loop. - -Lemma for_loop_notation_ind {stateT} (P : Z -> stateT -> Prop) - {i0 : Z} {step : Z} {finish : Z} {initial : stateT} - {cmp : Z -> Z -> bool} - {step_expr finish_expr} (body : Z -> stateT -> stateT) - {Hstep : class_eq (fun i => i = step) step_expr} - {Hfinish : class_eq (fun i => cmp i finish) finish_expr} - {Hgood : for_loop_is_good i0 step finish cmp} - (Pbefore : P i0 initial) - (Pbody : forall c st n, c = i0 + n * step -> i0 <= c < finish \/ finish < c <= i0 -> P c st -> P (c + step) (body c st)) - : P (finish - Z.sgn (finish - i0 + step - Z.sgn step) * (Z.abs (finish - i0 + step - Z.sgn step) mod Z.abs step) + step - Z.sgn step) - (@for_loop_notation i0 step finish _ initial cmp step_expr finish_expr body Hstep Hfinish Hgood). -Proof. - unfold for_loop_notation, for_loop_is_good in *; split_andb; Z.ltb_to_lt. - apply for_loop_ind; auto. -Qed. - -Local Ltac pre_t := - lazymatch goal with - | [ Pbefore : ?P ?i0 ?initial - |- ?P _ (@for_loop_notation ?i0 ?step ?finish _ ?initial _ ?step_expr ?finish_expr ?body ?Hstep ?Hfinish ?Hgood) ] - => generalize (@for_loop_notation_ind - _ P i0 step finish initial _ step_expr finish_expr body Hstep Hfinish Hgood Pbefore) - end. -Local Ltac t_step := - first [ progress unfold for_loop_is_good, for_loop_notation in * - | progress split_andb - | progress Z.ltb_to_lt - | rewrite Z.sgn_pos by lia - | rewrite Z.abs_eq by lia - | rewrite Z.sgn_neg by lia - | rewrite Z.abs_neq by lia - | progress autorewrite with zsimplify_const - | match goal with - | [ Hsgn : Z.sgn ?step = Z.sgn _ |- _ ] - => unique assert (0 < step) by (rewrite <- Z.sgn_pos_iff, Hsgn, Z.sgn_pos_iff; omega); clear Hsgn - | [ Hsgn : Z.sgn ?step = Z.sgn _ |- _ ] - => unique assert (step < 0) by (rewrite <- Z.sgn_neg_iff, Hsgn, Z.sgn_neg_iff; omega); clear Hsgn - | [ |- (_ -> ?P ?x ?y) -> ?P ?x' ?y' ] - => replace x with x' by lia; let H' := fresh in intro H'; apply H'; clear H' - | [ |- (_ -> _) -> _ ] - => let H := fresh "Hbody" in intro H; progress Z.replace_all_neg_with_pos; revert H - end - | rewrite !Z.opp_sub_distr - | rewrite !Z.opp_add_distr - | rewrite !Z.opp_involutive - | rewrite !Z.sub_opp_r - | rewrite (Z.add_opp_r _ 1) - | progress (push_Zmod; pull_Zmod) - | progress Z.replace_all_neg_with_pos - | solve [ eauto with omega ] ]. -Local Ltac t := pre_t; repeat t_step. - -Lemma for_loop_ind_lt {stateT} (P : Z -> stateT -> Prop) - {i0 : Z} {step : Z} {finish : Z} {initial : stateT} - {step_expr finish_expr} (body : Z -> stateT -> stateT) - {Hstep : class_eq (fun i => i = step) step_expr} - {Hfinish : class_eq (fun i => Z.ltb i finish) finish_expr} - {Hgood : for_loop_is_good i0 step finish Z.ltb} - (Pbefore : P i0 initial) - (Pbody : forall c st n, c = i0 + n * step -> i0 <= c < finish -> P c st -> P (c + step) (body c st)) - : P (finish + step - 1 - ((finish - i0 - 1) mod step)) - (@for_loop_notation i0 step finish _ initial Z.ltb (fun i => step_expr i) (fun i => finish_expr i) (fun i st => body i st) Hstep Hfinish Hgood). -Proof. t. Qed. - -Lemma for_loop_ind_gt {stateT} (P : Z -> stateT -> Prop) - {i0 : Z} {step : Z} {finish : Z} {initial : stateT} - {step_expr finish_expr} (body : Z -> stateT -> stateT) - {Hstep : class_eq (fun i => i = step) step_expr} - {Hfinish : class_eq (fun i => Z.gtb i finish) finish_expr} - {Hgood : for_loop_is_good i0 step finish Z.gtb} - (Pbefore : P i0 initial) - (Pbody : forall c st n, c = i0 + n * step -> finish < c <= i0 -> P c st -> P (c + step) (body c st)) - : P (finish + step + 1 + (i0 - finish - step - 1) mod (-step)) - (@for_loop_notation i0 step finish _ initial Z.gtb (fun i => step_expr i) (fun i => finish_expr i) (fun i st => body i st) Hstep Hfinish Hgood). -Proof. - replace (i0 - finish) with (-(finish - i0)) by omega. - t. -Qed. - -Lemma for_loop_ind_lt1 {stateT} (P : Z -> stateT -> Prop) - {i0 : Z} {finish : Z} {initial : stateT} - (body : Z -> stateT -> stateT) - {Hgood : for_loop_is_good i0 1 finish _} - (Pbefore : P i0 initial) - (Pbody : forall c st, i0 <= c < finish -> P c st -> P (c + 1) (body c st)) - : P finish - (for (int i = i0; i < finish; i++) updating (st = initial) {{ - body i st - }}). -Proof. - generalize (@for_loop_ind_lt - stateT P i0 1 finish initial _ _ body eq_refl eq_refl Hgood Pbefore). - rewrite Z.mod_1_r, Z.sub_0_r, Z.add_simpl_r. - auto. -Qed. - -Lemma for_loop_ind_gt1 {stateT} (P : Z -> stateT -> Prop) - {i0 : Z} {finish : Z} {initial : stateT} - (body : Z -> stateT -> stateT) - {Hgood : for_loop_is_good i0 (-1) finish _} - (Pbefore : P i0 initial) - (Pbody : forall c st, finish < c <= i0 -> P c st -> P (c - 1) (body c st)) - : P finish - (for (int i = i0; i > finish; i--) updating (st = initial) {{ - body i st - }}). -Proof. - generalize (@for_loop_ind_gt - stateT P i0 (-1) finish initial _ _ body eq_refl eq_refl Hgood Pbefore). - simpl; rewrite Z.mod_1_r, Z.add_0_r, (Z.add_opp_r _ 1), Z.sub_simpl_r. - intro H; apply H; intros *. - rewrite (Z.add_opp_r _ 1); auto. -Qed. - -Local Hint Extern 1 (for_loop_is_good (?i0 + ?step) ?step ?finish _) -=> refine (for_loop_is_good_step_lt _); try assumption : typeclass_instances. -Local Hint Extern 1 (for_loop_is_good (?i0 + ?step) ?step ?finish _) -=> refine (for_loop_is_good_step_gt _); try assumption : typeclass_instances. -Local Hint Extern 1 (for_loop_is_good (?i0 - ?step') _ ?finish _) -=> refine (for_loop_is_good_step_gt (step:=-step') _); try assumption : typeclass_instances. -Local Hint Extern 1 (for_loop_is_good (?i0 + 1) 1 ?finish _) -=> refine (for_loop_is_good_step_lt' _); try assumption : typeclass_instances. -Local Hint Extern 1 (for_loop_is_good (?i0 - 1) (-1) ?finish _) -=> refine (for_loop_is_good_step_gt' _); try assumption : typeclass_instances. - -(** The Hoare-logic-like conditions for ≤ and ≥ loops seem slightly - unnatural; you have to choose either to state your correctness - property in terms of [i + 1], or talk about the correctness - condition when the loop counter is [i₀ - 1] (which is strange; - it's like saying the loop has run -1 times), or give the - correctness condition after the first run of the loop body, rather - than before it. We give lemmas for the second two options; if - you're using the first one, Coq probably won't be able to infer - the motive ([P], below) automatically, and you might as well use - the vastly more general version [for_loop_ind_lt] / - [for_loop_ind_gt]. *) -Lemma for_loop_ind_le1 {stateT} (P : Z -> stateT -> Prop) - {i0 : Z} {finish : Z} {initial : stateT} - (body : Z -> stateT -> stateT) - {Hgood : for_loop_is_good i0 1 (finish+1) _} - (Pbefore : P i0 (body i0 initial)) - (Pbody : forall c st, i0 <= c <= finish -> P (c-1) st -> P c (body c st)) - : P finish - (for (int i = i0; i <= finish; i++) updating (st = initial) {{ - body i st - }}). -Proof. - rewrite for_loop_le1_unroll1. - edestruct Sumbool.sumbool_of_bool; Z.ltb_to_lt; cbv zeta. - { generalize (@for_loop_ind_lt - stateT (fun n => P (n - 1)) (i0+1) 1 (finish+1) (body i0 initial) _ _ body eq_refl eq_refl _). - rewrite Z.mod_1_r, Z.sub_0_r, !Z.add_simpl_r. - intro H; apply H; auto with omega; intros *. - rewrite !Z.add_simpl_r; auto with omega. } - { unfold for_loop_is_good, ForNotationConstants.Z.ltb', ForNotationConstants.Z.ltb in *; split_andb; Z.ltb_to_lt. - assert (i0 = finish) by omega; subst. - assumption. } -Qed. - -Lemma for_loop_ind_le1_offset {stateT} (P : Z -> stateT -> Prop) - {i0 : Z} {finish : Z} {initial : stateT} - (body : Z -> stateT -> stateT) - {Hgood : for_loop_is_good i0 1 (finish+1) _} - (Pbefore : P (i0-1) initial) - (Pbody : forall c st, i0 <= c <= finish -> P (c-1) st -> P c (body c st)) - : P finish - (for (int i = i0; i <= finish; i++) updating (st = initial) {{ - body i st - }}). -Proof. - apply for_loop_ind_le1; auto with omega. - unfold for_loop_is_good, ForNotationConstants.Z.ltb', ForNotationConstants.Z.ltb in *; split_andb; Z.ltb_to_lt. - auto with omega. -Qed. - -Lemma for_loop_ind_ge1 {stateT} (P : Z -> stateT -> Prop) - {i0 : Z} {finish : Z} {initial : stateT} - (body : Z -> stateT -> stateT) - {Hgood : for_loop_is_good i0 (-1) (finish-1) _} - (Pbefore : P i0 (body i0 initial)) - (Pbody : forall c st, finish <= c <= i0 -> P (c+1) st -> P c (body c st)) - : P finish - (for (int i = i0; i >= finish; i--) updating (st = initial) {{ - body i st - }}). -Proof. - rewrite for_loop_ge1_unroll1. - edestruct Sumbool.sumbool_of_bool; Z.ltb_to_lt; cbv zeta. - { generalize (@for_loop_ind_gt - stateT (fun n => P (n + 1)) (i0-1) (-1) (finish-1) (body i0 initial) _ _ body eq_refl eq_refl _). - simpl; rewrite Z.mod_1_r, Z.add_0_r, (Z.add_opp_r _ 1), !Z.sub_simpl_r. - intro H; apply H; intros *; auto with omega. - rewrite (Z.add_opp_r _ 1), !Z.sub_simpl_r; auto with omega. } - { unfold for_loop_is_good, ForNotationConstants.Z.gtb', ForNotationConstants.Z.gtb in *; split_andb; Z.ltb_to_lt. - assert (i0 = finish) by omega; subst. - assumption. } -Qed. - -Lemma for_loop_ind_ge1_offset {stateT} (P : Z -> stateT -> Prop) - {i0 : Z} {finish : Z} {initial : stateT} - (body : Z -> stateT -> stateT) - {Hgood : for_loop_is_good i0 (-1) (finish-1) _} - (Pbefore : P (i0+1) initial) - (Pbody : forall c st, finish <= c <= i0 -> P (c+1) st -> P c (body c st)) - : P finish - (for (int i = i0; i >= finish; i--) updating (st = initial) {{ - body i st - }}). -Proof. - apply for_loop_ind_ge1; auto with omega. - unfold for_loop_is_good, ForNotationConstants.Z.gtb', ForNotationConstants.Z.gtb in *; split_andb; Z.ltb_to_lt. - auto with omega. -Qed. diff --git a/src/Util/ForLoop/Tests.v b/src/Util/ForLoop/Tests.v deleted file mode 100644 index 1061f1958..000000000 --- a/src/Util/ForLoop/Tests.v +++ /dev/null @@ -1,55 +0,0 @@ -Require Import Coq.ZArith.BinInt. -Require Import Coq.micromega.Psatz. -Require Import Crypto.Util.ForLoop. -Require Import Crypto.Util.ForLoop.InvariantFramework. -Require Import Crypto.Util.ZUtil. - -Local Open Scope Z_scope. - -Check (for i (:= 0; += 1; < 10) updating (v := 5) {{ v + i }}). -Check (for (int i = 0; i < 5; i++) updating ( '(v1, v2) = (0, 0) ) {{ (v1 + i, v2 + i) }}). - -Compute for (int i = 0; i < 5; i++) updating (v = 0) {{ v + i }}. -Compute for (int i = 0; i <= 5; i++) updating (v = 0) {{ v + i }}. -Compute for (int i = 5; i > -1; i--) updating (v = 0) {{ v + i }}. -Compute for (int i = 5; i >= 0; i--) updating (v = 0) {{ v + i }}. -Compute for (int i = 0; i < 5; i += 2) updating (v = 0) {{ v + i }}. -Compute for (int i = 0; i <= 5; i += 2) updating (v = 0) {{ v + i }}. -Compute for (int i = 5; i > -1; i -= 2) updating (v = 0) {{ v + i }}. -Compute for (int i = 5; i >= 0; i -= 2) updating (v = 0) {{ v + i }}. -Compute for (int i = 0; i < 6; i += 2) updating (v = 0) {{ v + i }}. -Compute for (int i = 0; i <= 6; i += 2) updating (v = 0) {{ v + i }}. -Compute for (int i = 6; i > -1; i -= 2) updating (v = 0) {{ v + i }}. -Compute for (int i = 6; i >= 0; i -= 2) updating (v = 0) {{ v + i }}. -Check eq_refl : for (int i = 0; i <= 5; i++) updating (v = 0) {{ v + i }} = 15. -Check eq_refl : for (int i = 0; i < 5; i++) updating (v = 0) {{ v + i }} = 10. -Check eq_refl : for (int i = 5; i >= 0; i--) updating (v = 0) {{ v + i }} = 15. -Check eq_refl : for (int i = 5; i > -1; i--) updating (v = 0) {{ v + i }} = 15. -Check eq_refl : for (int i = 0; i <= 5; i += 2) updating (v = 0) {{ v + i }} = 6. -Check eq_refl : for (int i = 0; i < 5; i += 2) updating (v = 0) {{ v + i }} = 6. -Check eq_refl : for (int i = 5; i > -1; i -= 2) updating (v = 0) {{ v + i }} = 9. -Check eq_refl : for (int i = 5; i >= 0; i -= 2) updating (v = 0) {{ v + i }} = 9. -Check eq_refl : for (int i = 0; i <= 6; i += 2) updating (v = 0) {{ v + i }} = 12. -Check eq_refl : for (int i = 0; i < 6; i += 2) updating (v = 0) {{ v + i }} = 6. -Check eq_refl : for (int i = 6; i > -1; i -= 2) updating (v = 0) {{ v + i }} = 12. -Check eq_refl : for (int i = 6; i >= 0; i -= 2) updating (v = 0) {{ v + i }} = 12. - -Local Notation for_sumT n' - := (let n := Z.pos n' in - (2 * - for (int i = 0; i <= n; i++) updating (v = 0) {{ - v + i - }})%Z - = n * (n + 1)) - (only parsing). - -Check eq_refl : for_sumT 5. - -(** Here we show that if we add the numbers from 0 to n, we get [n * (n + 1) / 2] *) -Example for_sum n' : for_sumT n'. -Proof. - intro n. - apply for_loop_ind_le1. - { compute; reflexivity. } - { intros; nia. } -Qed. diff --git a/src/Util/ForLoop/Unrolling.v b/src/Util/ForLoop/Unrolling.v deleted file mode 100644 index 95b46e711..000000000 --- a/src/Util/ForLoop/Unrolling.v +++ /dev/null @@ -1,314 +0,0 @@ -(** * Proving properties of for-loops via loop-unrolling *) -Require Import Coq.micromega.Psatz. -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Util.ForLoop. -Require Import Crypto.Util.ForLoop.Instances. -Require Import Crypto.Util.ZUtil. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.Tactics.RewriteHyp. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Notations. - -Section with_body. - Context {stateT : Type} - (body : nat -> stateT -> stateT). - - Lemma unfold_repeat_function (count : nat) (st : stateT) - : repeat_function body count st - = match count with - | O => st - | S count' => repeat_function body count' (body count st) - end. - Proof using Type. destruct count; reflexivity. Qed. - - Lemma repeat_function_unroll1_start (count : nat) (st : stateT) - : repeat_function body (S count) st - = repeat_function body count (body (S count) st). - Proof using Type. rewrite unfold_repeat_function; reflexivity. Qed. - - Lemma repeat_function_unroll1_end (count : nat) (st : stateT) - : repeat_function body (S count) st - = body 1 (repeat_function (fun count => body (S count)) count st). - Proof using Type. - revert st; induction count as [|? IHcount]; [ reflexivity | ]. - intros; simpl in *; rewrite <- IHcount; reflexivity. - Qed. - - Lemma repeat_function_unroll1_start_match (count : nat) (st : stateT) - : repeat_function body count st - = match count with - | 0 => st - | S count' => repeat_function body count' (body count st) - end. - Proof using Type. destruct count; [ reflexivity | apply repeat_function_unroll1_start ]. Qed. - - Lemma repeat_function_unroll1_end_match (count : nat) (st : stateT) - : repeat_function body count st - = match count with - | 0 => st - | S count' => body 1 (repeat_function (fun count => body (S count)) count' st) - end. - Proof using Type. destruct count; [ reflexivity | apply repeat_function_unroll1_end ]. Qed. -End with_body. - -Local Open Scope bool_scope. -Local Open Scope Z_scope. - -Section for_loop. - Context (i0 finish : Z) (step : Z) {stateT} (initial : stateT) (body : Z -> stateT -> stateT) - (Hgood : Z.sgn step = Z.sgn (finish - i0)). - - Let countZ := (Z.quot (finish - i0 + step - Z.sgn step) step). - Let count := Z.to_nat countZ. - Let of_nat_count c := (i0 + step * Z.of_nat (count - c)). - Let nat_body := (fun c => body (of_nat_count c)). - - Lemma for_loop_empty - (Heq : finish = i0) - : for_loop i0 finish step initial body = initial. - Proof. - subst; unfold for_loop. - rewrite Z.sub_diag, Z.quot_sub_sgn; autorewrite with zsimplify_const. - reflexivity. - Qed. - - Lemma for_loop_unroll1 - : for_loop i0 finish step initial body - = if finish =? i0 - then initial - else let initial' := body i0 initial in - if Z.abs (finish - i0) <=? Z.abs step - then initial' - else for_loop (i0 + step) finish step initial' body. - Proof. - break_innermost_match_step; Z.ltb_to_lt. - { apply for_loop_empty; assumption. } - { unfold for_loop. - rewrite repeat_function_unroll1_start_match. - destruct (Z_zerop step); - repeat first [ progress break_innermost_match - | congruence - | lia - | progress Z.ltb_to_lt - | progress subst - | progress rewrite Nat.sub_diag - | progress autorewrite with zsimplify_const in * - | progress rewrite Z.quot_small_iff in * by omega - | progress rewrite Z.quot_small_abs in * by lia - | rewrite Nat.sub_succ_l by omega - | progress destruct_head' and - | rewrite !Z.sub_add_distr - | match goal with - | [ H : ?x = Z.of_nat _ |- context[?x] ] => rewrite H - | [ H : Z.abs ?x <= 0 |- _ ] => assert (x = 0) by lia; clear H - | [ H : 0 = Z.sgn ?x |- _ ] => assert (x = 0) by lia; clear H - | [ H : ?x - ?y = 0 |- _ ] => is_var x; assert (x = y) by omega; subst x - | [ H : Z.to_nat _ = _ |- _ ] => apply Nat2Z.inj_iff in H - | [ H : context[Z.abs ?x] |- _ ] => rewrite (Z.abs_eq x) in H by omega - | [ H : context[Z.abs ?x] |- _ ] => rewrite (Z.abs_neq x) in H by omega - | [ H : Z.of_nat (Z.to_nat _) = _ |- _ ] - => rewrite Z2Nat.id in H by (apply Z.quot_nonneg_same_sgn; lia) - | [ H : _ = Z.of_nat (S ?x) |- _ ] - => is_var x; destruct x; [ reflexivity | ] - | [ H : ?x + 1 = Z.of_nat (S ?y) |- _ ] - => assert (x = Z.of_nat y) by lia; clear H - | [ |- repeat_function _ ?x ?y = repeat_function _ ?x ?y ] - => apply repeat_function_Proper_le; intros - | [ |- ?f _ ?x = ?f _ ?x ] - => is_var f; apply f_equal2; [ | reflexivity ] - end - | progress rewrite Z.quot_add_sub_sgn_small in * |- by lia - | progress autorewrite with zsimplify ]. } - Qed. -End for_loop. - -Lemma for_loop_notation_empty {stateT} - {i0 : Z} {step : Z} {finish : Z} {initial : stateT} - {cmp : Z -> Z -> bool} - {step_expr finish_expr} (body : Z -> stateT -> stateT) - {Hstep : class_eq (fun i => i = step) step_expr} - {Hfinish : class_eq (fun i => cmp i finish) finish_expr} - {Hgood : for_loop_is_good i0 step finish cmp} - (Heq : i0 = finish) - : @for_loop_notation i0 step finish _ initial cmp step_expr finish_expr body Hstep Hfinish Hgood = initial. -Proof. - unfold for_loop_notation, for_loop_is_good in *; split_andb; Z.ltb_to_lt. - apply for_loop_empty; auto. -Qed. - -Local Notation adjust_bool b p - := (match b as b' return b' = true -> b' = true with - | true => fun _ => eq_refl - | false => fun x => x - end p). - -Lemma for_loop_is_good_step_gen - cmp - (Hcmp : cmp = Z.ltb \/ cmp = Z.gtb) - {i0 step finish} - {H : for_loop_is_good i0 step finish cmp} - (H' : cmp (i0 + step) finish = true) - : for_loop_is_good (i0 + step) step finish cmp. -Proof. - unfold for_loop_is_good in *. - rewrite H', Bool.andb_true_r. - destruct Hcmp; subst; - split_andb; Z.ltb_to_lt; - [ rewrite (Z.sgn_pos (finish - i0)) in * by omega - | rewrite (Z.sgn_neg (finish - i0)) in * by omega ]; - destruct step; simpl in *; try congruence; - symmetry; - [ apply Z.sgn_pos_iff | apply Z.sgn_neg_iff ] - ; omega. -Qed. - -Definition for_loop_is_good_step_lt - {i0 step finish} - {H : for_loop_is_good i0 step finish Z.ltb} - (H' : Z.ltb (i0 + step) finish = true) - : for_loop_is_good (i0 + step) step finish Z.ltb - := for_loop_is_good_step_gen Z.ltb (or_introl eq_refl) (H:=H) H'. -Definition for_loop_is_good_step_gt - {i0 step finish} - {H : for_loop_is_good i0 step finish Z.gtb} - (H' : Z.gtb (i0 + step) finish = true) - : for_loop_is_good (i0 + step) step finish Z.gtb - := for_loop_is_good_step_gen Z.gtb (or_intror eq_refl) (H:=H) H'. -Definition for_loop_is_good_step_lt' - {i0 finish} - {H : for_loop_is_good i0 1 (finish + 1) Z.ltb} - (H' : Z.ltb i0 finish = true) - : for_loop_is_good (i0 + 1) 1 (finish + 1) Z.ltb. -Proof. - apply for_loop_is_good_step_lt; Z.ltb_to_lt; omega. -Qed. -Definition for_loop_is_good_step_gt' - {i0 finish} - {H : for_loop_is_good i0 (-1) (finish - 1) Z.gtb} - (H' : Z.gtb i0 finish = true) - : for_loop_is_good (i0 - 1) (-1) (finish - 1) Z.gtb. -Proof. - apply for_loop_is_good_step_gt; Z.ltb_to_lt; omega. -Qed. - -Local Hint Extern 1 (for_loop_is_good (?i0 + ?step) ?step ?finish _) -=> refine (adjust_bool _ (for_loop_is_good_step_lt _)); try assumption : typeclass_instances. -Local Hint Extern 1 (for_loop_is_good (?i0 + ?step) ?step ?finish _) -=> refine (adjust_bool _ (for_loop_is_good_step_gt _)); try assumption : typeclass_instances. -Local Hint Extern 1 (for_loop_is_good (?i0 - ?step') _ ?finish _) -=> refine (adjust_bool _ (for_loop_is_good_step_gt (step:=-step') _)); try assumption : typeclass_instances. -Local Hint Extern 1 (for_loop_is_good (?i0 + 1) 1 ?finish _) -=> refine (adjust_bool _ (for_loop_is_good_step_lt' _)); try assumption : typeclass_instances. -Local Hint Extern 1 (for_loop_is_good (?i0 - 1) (-1) ?finish _) -=> refine (adjust_bool _ (for_loop_is_good_step_gt' _)); try assumption : typeclass_instances. - -Local Ltac t := - repeat match goal with - | _ => progress unfold for_loop_is_good, for_loop_notation in * - | _ => progress rewrite for_loop_unroll1 by auto - | _ => omega - | _ => progress subst - | _ => reflexivity - | _ => progress split_andb - | _ => progress Z.ltb_to_lt - | _ => progress break_innermost_match_step - | [ H : context[Z.abs ?x] |- _ ] => rewrite (Z.abs_eq x) in H by omega - | [ H : context[Z.abs ?x] |- _ ] => rewrite (Z.abs_neq x) in H by omega - | [ H : context[Z.sgn ?x] |- _ ] => rewrite (Z.sgn_pos x) in H by omega - | [ H : context[Z.sgn ?x] |- _ ] => rewrite (Z.sgn_neg x) in H by omega - | [ H : Z.sgn _ = 1 |- _ ] => apply Z.sgn_pos_iff in H - | [ H : Z.sgn _ = -1 |- _ ] => apply Z.sgn_neg_iff in H - end. - -Lemma for_loop_lt_unroll1 {stateT} - {i0 : Z} {step : Z} {finish : Z} {initial : stateT} - {step_expr finish_expr} (body : Z -> stateT -> stateT) - {Hstep : class_eq (fun i => i = step) step_expr} - {Hfinish : class_eq (fun i => Z.ltb i finish) finish_expr} - {Hgood : for_loop_is_good i0 step finish Z.ltb} - : (@for_loop_notation i0 step finish _ initial Z.ltb (fun i => step_expr i) (fun i => finish_expr i) (fun i st => body i st) Hstep Hfinish Hgood) - = let initial' := body i0 initial in - if Sumbool.sumbool_of_bool (Z.ltb (i0 + step) finish) - then @for_loop_notation (i0 + step) step finish _ initial' Z.ltb (fun i => step_expr i) (fun i => finish_expr i) (fun i st => body i st) Hstep Hfinish _ - else initial'. -Proof. t. Qed. - -Lemma for_loop_gt_unroll1 {stateT} - {i0 : Z} {step : Z} {finish : Z} {initial : stateT} - {step_expr finish_expr} (body : Z -> stateT -> stateT) - {Hstep : class_eq (fun i => i = step) step_expr} - {Hfinish : class_eq (fun i => Z.gtb i finish) finish_expr} - {Hgood : for_loop_is_good i0 step finish Z.gtb} - : (@for_loop_notation i0 step finish _ initial Z.gtb (fun i => step_expr i) (fun i => finish_expr i) (fun i st => body i st) Hstep Hfinish Hgood) - = let initial' := body i0 initial in - if Sumbool.sumbool_of_bool (Z.gtb (i0 + step) finish) - then @for_loop_notation (i0 + step) step finish _ initial' Z.gtb (fun i => step_expr i) (fun i => finish_expr i) (fun i st => body i st) Hstep Hfinish _ - else initial'. -Proof. t. Qed. - -Lemma for_loop_lt1_unroll1 {stateT} - {i0 : Z} {finish : Z} {initial : stateT} - {body : Z -> stateT -> stateT} - {Hgood : for_loop_is_good i0 1 finish _} - : for (int i = i0; i < finish; i++) updating (st = initial) {{ - body i st - }} - = let initial' := body i0 initial in - if Sumbool.sumbool_of_bool (Z.ltb (i0 + 1) finish) - then for (int i = i0+1; i < finish; i++) updating (st = initial') {{ - body i st - }} - else initial'. -Proof. apply for_loop_lt_unroll1. Qed. - -Lemma for_loop_gt1_unroll1 {stateT} - {i0 : Z} {finish : Z} {initial : stateT} - {body : Z -> stateT -> stateT} - {Hgood : for_loop_is_good i0 (-1) finish _} - : for (int i = i0; i > finish; i--) updating (st = initial) {{ - body i st - }} - = let initial' := body i0 initial in - if Sumbool.sumbool_of_bool (Z.gtb (i0 - 1) finish) - then for (int i = i0-1; i > finish; i--) updating (st = initial') {{ - body i st - }} - else initial'. -Proof. apply for_loop_gt_unroll1. Qed. - -Lemma for_loop_le1_unroll1 {stateT} - {i0 : Z} {finish : Z} {initial : stateT} - {body : Z -> stateT -> stateT} - {Hgood : for_loop_is_good i0 1 (finish+1) _} - : for (int i = i0; i <= finish; i++) updating (st = initial) {{ - body i st - }} - = let initial' := body i0 initial in - if Sumbool.sumbool_of_bool (Z.ltb i0 finish) - then for (int i = i0+1; i <= finish; i++) updating (st = initial') {{ - body i st - }} - else initial'. -Proof. - rewrite for_loop_lt_unroll1; unfold for_loop_notation. - break_innermost_match; Z.ltb_to_lt; try omega; try reflexivity. -Qed. - -Lemma for_loop_ge1_unroll1 {stateT} - {i0 : Z} {finish : Z} {initial : stateT} - {body : Z -> stateT -> stateT} - {Hgood : for_loop_is_good i0 (-1) (finish-1) _} - : for (int i = i0; i >= finish; i--) updating (st = initial) {{ - body i st - }} - = let initial' := body i0 initial in - if Sumbool.sumbool_of_bool (Z.gtb i0 finish) - then for (int i = i0-1; i >= finish; i--) updating (st = initial') {{ - body i st - }} - else initial'. -Proof. - rewrite for_loop_gt_unroll1; unfold for_loop_notation. - break_innermost_match; Z.ltb_to_lt; try omega; try reflexivity. -Qed. diff --git a/src/Util/Loop.v b/src/Util/Loop.v deleted file mode 100644 index 2ee90d11f..000000000 --- a/src/Util/Loop.v +++ /dev/null @@ -1,480 +0,0 @@ -(** * Definition and Notations for [do { body }] *) -Require Import Coq.ZArith.BinInt. -Require Import Coq.Classes.Morphisms. -Require Import Coq.micromega.Lia. -Require Import Coq.omega.Omega. -Require Import Crypto.Util.ZUtil. -Require Import Crypto.Util.ZUtil.Z2Nat. -Require Import Crypto.Util.Notations Crypto.Util.CPSNotations. -Require Import Crypto.Util.LetIn. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.UniquePose. - -Section with_state. - Import CPSNotations. - Context {state : Type}. - - Definition loop_cps_step - (loop_cps - : forall (max_iter : nat) - (initial : state) - (body : state -> forall {T} (continue : state -> T) (break : state -> T), T), - ~> state) - (max_iter : nat) - : forall (initial : state) - (body : state -> forall {T} (continue : state -> T) (break : state -> T), T), - ~> state - := fun st body - => match max_iter with - | 0 - => (return st) - | S max_iter' - => fun T ret - => body st T (fun st' => @loop_cps max_iter' st' body _ ret) ret - end. - - Fixpoint loop_cps (max_iter : nat) - : forall (initial : state) - (body : state -> forall {T} (continue : state -> T) (break : state -> T), T), - ~> state - := loop_cps_step loop_cps max_iter. - - Lemma unfold_loop_cps - (max_iter : nat) - : loop_cps max_iter - = loop_cps_step loop_cps max_iter. - Proof. - destruct max_iter; reflexivity. - Qed. - - Theorem loop_cps_def (max_iter : nat) - (initial : state) - (body : state -> forall {T} (continue : state -> T) (break : state -> T), T) - T ret - : loop_cps (S max_iter) initial body T ret = - body initial (fun st' => @loop_cps max_iter st' body _ ret) ret. - Proof. - reflexivity. - Qed. - - Theorem loop_cps_ind - (invariant : state -> Prop) - T (P : T -> Prop) n v0 body rest - : invariant v0 - -> (forall v continue break, - (forall v, invariant v -> P (continue v)) - -> (forall v, invariant v -> P (break v)) - -> invariant v - -> P (body v T continue break)) - -> (forall v, invariant v -> P (rest v)) - -> P (loop_cps n v0 body T rest). - Proof. - revert v0 rest. - induction n as [|n IHn]; intros v0 rest Hinv Hbody HP; simpl; cbv [cpsreturn]; auto. - Qed. - - Local Hint Extern 2 => omega. - - (** TODO(andreser): Remove this if we don't need it *) - Theorem loop_cps_wf_ind_break - (measure : state -> nat) - (invariant : state -> Prop) - T (P : T -> Prop) n v0 body rest - : invariant v0 - -> (forall v continue, - invariant v - -> (forall break, - (forall v', measure v' < measure v -> invariant v' -> P (continue v')) - -> P (body v T continue break)) - \/ P (body v T continue rest)) - -> measure v0 < n - -> P (loop_cps n v0 body T rest). - Proof. - revert v0 rest. - induction n as [|n IHn]; intros v0 rest Hinv Hbody Hmeasure; simpl; try omega. - edestruct Hbody as [Hbody'|Hbody']; eauto. - Qed. - - Theorem loop_cps_wf_ind - (measure : state -> nat) - (invariant : state -> Prop) - T (P : T -> Prop) n v0 body rest - : invariant v0 - -> (forall v continue, - invariant v - -> ((forall v', measure v' < measure v -> invariant v' -> P (continue v')) - -> P (body v T continue rest))) - -> measure v0 < n - -> P (loop_cps n v0 body T rest). - Proof. - revert v0. - induction n as [|n IHn]; intros v0 Hinv Hbody Hmeasure; simpl; try omega. - eauto. - Qed. - - Theorem eq_loop_cps_large_n - (measure : state -> nat) - n n' v0 body T rest - : measure v0 < n - -> measure v0 < n' - -> (forall v continue continue', - (forall v', measure v' < measure v -> continue v' = continue' v') - -> measure v <= measure v0 - -> body v T continue rest = body v T continue' rest) - -> loop_cps n v0 body T rest = loop_cps n' v0 body T rest. - Proof. - revert n n'. - match goal with - | [ |- forall n n', ?P ] => cut (forall n n', n <= n' -> P) - end. - { intros H n n' ???. - destruct (le_lt_dec n n'); [ | symmetry ]; auto. } - { intros n n' Hle Hn _. - revert n' Hle v0 Hn. - induction n as [|n IHn], n' as [|n']; simpl; - auto with omega. } - Qed. -End with_state. - -(** N.B. If the body is polymorphic (that is, if the type argument - shows up in the body), then we need to bind the name of the type - parameter somewhere in the notation for it to show up; we have a - separate notation for this case. *) -(** TODO: When these notations are finalized, reserve them in Notations.v and moving the level and formatting rules there *) -Notation "'loop' _{ fuel } ( state1 .. staten = initial ) 'labels' ( continue , break , @ T ) {{ body }} ; rest" - := (@loop_cps _ fuel initial - (fun state1 => .. (fun staten => id (fun T continue break => body)) .. ) - _ (fun state1 => .. (fun staten => rest) .. )) - (at level 200, state1 binder, staten binder, - format "'[v ' 'loop' _{ fuel } ( state1 .. staten = initial ) 'labels' ( continue , break , @ T ) {{ '//' body ']' '//' }} ; '//' rest"). -Notation "'loop' _{ fuel } ( state1 .. staten = initial ) 'labels' ( continue , break ) {{ body }} ; rest" - := (@loop_cps _ fuel initial - (fun state1 => .. (fun staten => id (fun T continue break => body)) .. ) - _ (fun state1 => .. (fun staten => rest) .. )) - (at level 200, state1 binder, staten binder, - format "'[v ' 'loop' _{ fuel } ( state1 .. staten = initial ) 'labels' ( continue , break ) {{ '//' body ']' '//' }} ; '//' rest"). -Notation "'loop' _{ fuel } ( state1 .. staten = initial ) 'labels' ( continue ) {{ body }} ; rest" - := (@loop_cps _ fuel initial - (fun state1 => .. (fun staten => id (fun T continue _ => body)) .. ) - _ (fun state1 => .. (fun staten => rest) .. )) - (at level 200, state1 binder, staten binder, - format "'[v ' 'loop' _{ fuel } ( state1 .. staten = initial ) 'labels' ( continue ) {{ '//' body ']' '//' }} ; '//' rest"). - -Section with_for_state. - Import CPSNotations. - Section with_loop_params. - Context {state : Type}. - Context (test : Z -> Z -> bool) (i_final : Z) (upd_i : Z -> Z) - (body : state -> Z -> forall {T} (continue : state -> T) (break : state -> T), T). - - (* we assume that [upd_i] is linear to compute the fuel *) - Definition for_cps (i0 : Z) (initial : state) - : ~> state - := fun T ret - => @loop_cps - (Z * state) - (S (S (Z.to_nat ((i_final - i0) / (upd_i 0%Z))))) - (i0, initial) - (fun '(i, st) T continue break - => if test i i_final - then @body st i T - (fun st' => continue (upd_i i, st')%Z) - (fun st' => break (i, st')) - else break (i, st)) - T (fun '(i, st) => ret st). - - Section lemmas. - Local Open Scope Z_scope. - Context (upd_linear : forall x, upd_i x = upd_i 0 + x) - (upd_nonzero : upd_i 0 <> 0) - (upd_signed : forall i0, test i0 i_final = true -> 0 <= (i_final - i0) / (upd_i 0)). - - (** TODO: Strengthen this to take into account the value of - the loop counter at the end of the loop; based on - [ForLoop.v], it should be something like [(finish - - Z.sgn (finish - i0 + step - Z.sgn step) * (Z.abs - (finish - i0 + step - Z.sgn step) mod Z.abs step) + - step - Z.sgn step)] *) - Theorem for_cps_ind - (invariant : Z -> state -> Prop) - T (P : (*Z ->*) T -> Prop) i0 v0 rest - : invariant i0 v0 - -> (forall i v continue, - test i i_final = true - -> (forall v, invariant (upd_i i) v -> P (continue v)) - -> invariant i v - -> P (@body v i T continue rest)) - -> (forall i v, test i i_final = false -> invariant i v -> P (rest v)) - -> P (for_cps i0 v0 T rest). - Proof. - unfold for_cps, cpscall, cpsreturn. - intros Hinv IH Hrest. - eapply @loop_cps_wf_ind with (T:=T) - (invariant := fun '(i, s) => invariant i s) - (measure := fun '(i, s) => Z.to_nat (1 + (i_final - i) / upd_i 0)); - [ assumption - | - | solve [ destruct (Z_le_gt_dec 0 ((i_final - i0) / upd_i 0)); - [ rewrite Z2Nat.inj_add by omega; simpl; omega - | rewrite Z2Nat.inj_nonpos by omega; omega ] ] ]. - intros [i st] continue Hinv' IH'. - destruct (test i i_final) eqn:Hi; [ | solve [ eauto ] ]. - pose proof (upd_signed _ Hi) as upd_signed'. - assert (upd_i 0 <> 0) - by (intro H'; rewrite H' in upd_signed'; autorewrite with zsimplify in upd_signed'; - omega). - specialize (IH i st (fun st' => continue (upd_i i, st')) Hi). - specialize (fun v pf => IH' (upd_i i, v) pf). - cbv beta iota in *. - specialize (fun pf v => IH' v pf). - rewrite upd_linear in IH'. - replace ((i_final - (upd_i 0 + i)) / upd_i 0) - with ((i_final - i) / upd_i 0 - 1) - in IH' - by (Z.div_mod_to_quot_rem; nia). - rewrite <- upd_linear, Zplus_minus, Z2Nat.inj_add in IH' by omega. - auto with omega. - Qed. - - Theorem for_cps_unroll1 - T i0 v0 rest - (body_Proper : Proper (eq ==> eq ==> forall_relation (fun T => (pointwise_relation _ eq) ==> eq ==> eq)) body) - : for_cps i0 v0 T rest - = if test i0 i_final - then @body v0 i0 T - (fun v => for_cps (upd_i i0) v T rest) - rest - else rest v0. - Proof. - unfold for_cps at 1. - rewrite loop_cps_def. - destruct (test i0 i_final) eqn:Hi; [ | reflexivity ]. - apply body_Proper; [ reflexivity | reflexivity | intro st | reflexivity ]. - assert (Hto0 : forall x, x <= 0 -> Z.to_nat x = 0%nat) - by (intros []; intros; simpl; lia). - apply eq_loop_cps_large_n with (measure := fun '(i, st) => Z.to_nat (1 + (i_final - i) / upd_i 0)); - repeat first [ progress intros - | reflexivity - | progress destruct_head'_prod - | progress unfold pointwise_relation - | break_innermost_match_step - | apply body_Proper - | omega - | rewrite Zdiv.Zdiv_0_r in * - | rewrite ?(Z.add_opp_r _ 1), Zplus_minus, <- ?(Z.add_opp_r _ 1) in * - | match goal with - | [ H : forall v, _ -> ?continue _ = ?continue' _ |- ?continue _ = ?continue' _ ] => apply H - | [ |- context[upd_i ?x] ] - => lazymatch x with - | 0 => fail - | _ => rewrite (upd_linear x) - end - | [ H : ?x = 0 |- context[?x] ] => rewrite H - | [ H : ?x = 0, H' : context[?x] |- _ ] => rewrite H in H' - | [ H : forall i, ?f i ?y = true -> ?R (_ / 0), H' : ?f _ ?y = true |- _ ] - => specialize (H _ H') - | [ |- context[?i_final - (upd_i 0 + ?i0)] ] - => replace (i_final - (upd_i 0 + i0)) with ((i_final - i0) + (-1) * upd_i 0) by omega; - rewrite Zdiv.Z_div_plus_full by assumption - end - | lazymatch goal with - | [ H : upd_i 0 = 0 |- _ ] => fail - | [ H : upd_i 0 <> 0 |- _ ] => fail - | _ => destruct (Z_zerop (upd_i 0)) - end - | match goal with - | [ |- context[S (Z.to_nat ?x)] ] - => destruct (Z_lt_le_dec 0 x); - [ rewrite <- (Z2Nat.inj_succ x) by omega - | rewrite !(Hto0 x) by omega ] - | [ |- (Z.to_nat _ < Z.to_nat _)%nat ] - => apply Z2Nat.inj_lt - | [ |- (Z.to_nat ?x < ?n)%nat ] - => apply (Z2Nat.inj_lt x (Z.of_nat n)); simpl - | [ H : forall i, ?f i ?y = true -> 0 <= _ / _, H' : ?f _ ?y = true |- _ ] - => specialize (H _ H') - end ]. - Qed. - End lemmas. - End with_loop_params. -End with_for_state. - -Delimit Scope for_upd_scope with for_upd. -Delimit Scope for_test_scope with for_test. -Notation "i += k" := (Z.add i k) : for_upd_scope. -Notation "i -= k" := (Z.sub i k) : for_upd_scope. -Notation "i ++" := (i += 1)%for_upd : for_upd_scope. -Notation "i --" := (i -= 1)%for_upd : for_upd_scope. -Notation "<" := Z.ltb (at level 71) : for_test_scope. -Notation ">" := Z.gtb (at level 71) : for_test_scope. -Notation "<=" := Z.leb (at level 71) : for_test_scope. -Notation ">=" := Z.geb (at level 71) : for_test_scope. -Notation "≤" := Z.leb (at level 71) : for_test_scope. -Notation "≥" := Z.geb (at level 71) : for_test_scope. -Global Close Scope for_test_scope. (* TODO: make these notations not print all over the place *) - -Definition force_idZ (f : Z -> Z) (pf : f = id) {T} (v : T) := v. -(** [lhs] and [cmp_expr] go at level 9 so that they bind more tightly - than application (so that [i (<)] sticks [i] in [lhs] and [(<)] in - [cmp_expr], rather than sticking [i (<)] in [lhs] and then - complaining about a missing value for [cmp_expr]. Unfortunately, - because the comparison operators need to be at level > 70 to not - conflict with their infix versions, putting [cmp_expr] at level 9 - forces us to wrap parentheses around the comparison operator. *) -(** TODO(andreser): If it's worth it, duplicate these notations for - each value of [cmp_expr] so that we don't need to wrap the - comparison operator in parentheses. *) -(** TODO: When these notations are finalized, reserve them in Notations.v and moving the level and formatting rules there *) -Notation "'for' ( i1 .. i2 = i0 ; lhs cmp_expr final ; upd_expr ) 'updating' ( state1 .. staten = initial ) 'labels' ( continue , break , @ T ) {{ body }} ; rest" - := (force_idZ - (fun i1 => .. (fun i2 => lhs) ..) - eq_refl - (@for_cps _ cmp_expr%for_test - final - (fun i1 => .. (fun i2 => upd_expr%for_upd) .. ) - (fun state1 => .. (fun staten => id (fun i1 => .. (fun i2 => id (fun T continue break => body)) .. )) .. ) - i0 - initial - _ (fun state1 => .. (fun staten => rest) .. ))) - (at level 200, state1 binder, staten binder, i1 binder, i2 binder, lhs at level 9, cmp_expr at level 9, - format "'[v ' 'for' ( i1 .. i2 = i0 ; lhs cmp_expr final ; upd_expr ) 'updating' ( state1 .. staten = initial ) 'labels' ( continue , break , @ T ) {{ '//' body ']' '//' }} ; '//' rest"). -Notation "'for' ( i1 .. i2 = i0 ; lhs cmp_expr final ; upd_expr ) 'updating' ( state1 .. staten = initial ) 'labels' ( continue , break ) {{ body }} ; rest" - := (force_idZ - (fun i1 => .. (fun i2 => lhs) ..) - eq_refl - (@for_cps _ cmp_expr%for_test - final - (fun i1 => .. (fun i2 => upd_expr%for_upd) .. ) - (fun state1 => .. (fun staten => id (fun i1 => .. (fun i2 => id (fun T continue break => body)) .. )) .. ) - i0 - initial - _ (fun state1 => .. (fun staten => rest) .. ))) - (at level 200, state1 binder, staten binder, i1 binder, i2 binder, lhs at level 9, cmp_expr at level 9, - format "'[v ' 'for' ( i1 .. i2 = i0 ; lhs cmp_expr final ; upd_expr ) 'updating' ( state1 .. staten = initial ) 'labels' ( continue , break ) {{ '//' body ']' '//' }} ; '//' rest"). -Notation "'for' ( i1 .. i2 = i0 ; lhs cmp_expr final ; upd_expr ) 'updating' ( state1 .. staten = initial ) 'labels' ( continue ) {{ body }} ; rest" - := (force_idZ - (fun i1 => .. (fun i2 => lhs) ..) - eq_refl - (@for_cps _ cmp_expr%for_test - final - (fun i1 => .. (fun i2 => upd_expr%for_upd) .. ) - (fun state1 => .. (fun staten => id (fun i1 => .. (fun i2 => id (fun T continue break => body)) .. )) .. ) - i0 - initial - _ (fun state1 => .. (fun staten => rest) .. ))) - (at level 200, state1 binder, staten binder, i1 binder, i2 binder, lhs at level 9, cmp_expr at level 9, - format "'[v ' 'for' ( i1 .. i2 = i0 ; lhs cmp_expr final ; upd_expr ) 'updating' ( state1 .. staten = initial ) 'labels' ( continue ) {{ '//' body ']' '//' }} ; '//' rest"). - -Section LoopTest. - Import CPSNotations. - Check loop _{ 10 } (x = 0) labels (continue, break) {{ continue (x + 1) }} ; x. - - Check - loop _{ 1234 } ('(i, a) = (0, 0)) labels (continue, break) - {{ - if i <? 10 - then - continue (i + 1, a+1) - else - break (0, a) - }}; - a. - - Context (f:nat~>nat). - - Check x <- f 0 ; return x + x. - Check x <- f 0 ; y <- f x; z <- f y; return (x,y,z). - - Check loop _{ 10 } (x = 0) labels (continue, break) {{ continue (x + 1) }} ; - return x. - - Check loop _{ 10 } (x = 0) labels (continue, break) {{ continue (x + 1) }} ; - x <- f x; - return x. - - Check loop _{ 10 } (x = 0) labels (continue, break) {{ x <- f x ; continue (x) }} ; x. - - - Context (s F : Z) (zero : nat). - Check for ( i = s; i (<) F; i++) updating (P = zero) labels (continue, break) - {{ - continue (P+P) - }}; - P. - - Check for ( i = s; i (<) F; i++) updating (P = zero) labels (continue) - {{ - P <- f P; - continue (P+P) - }}; - P. -End LoopTest. - -Module CPSBoilerplate. - Import CPSNotations. - Definition valid {R} (f:~>R) := - forall {T} (continuation:R->T), - (x <- f; continuation x) = (continuation (f _ id)). - Existing Class valid. -End CPSBoilerplate. - -Require Import Coq.Classes.Morphisms. -Require Import Crypto.Algebra.ScalarMult. -Section ScalarMult. - Import CPSNotations. - - Context {G} (zero:G) (k w : Z) (add_tbl : G -> Z -> Z ~> G) (nth_limb : Z ~> Z). (* k w-bit limbs *) - - Definition ScalarMultBase := - for ( i = 0; i (<) k; i++) updating (P = zero) labels (continue, break) - {{ - x <- nth_limb i; - P <- add_tbl P i x; - continue P - }}; - P. - - Context {Geq add opp} {Hmonoid:@Algebra.Hierarchy.group G Geq add zero opp}. - Local Notation smul := (@scalarmult_ref G add zero opp). - Context {nth_limb_valid : forall a, CPSBoilerplate.valid (nth_limb a)}. - Context {add_tbl_valid : forall a b c, CPSBoilerplate.valid (add_tbl a b c)}. - Context {Proper_add_tbl : Proper (Geq ==> eq ==> eq ==> Geq) (fun a b c => add_tbl a b c _ id)}. - Context (B:G). - Context {limb_good} - {nth_limb_good: forall i, (0 <= i < k)%Z -> limb_good i (nth_limb i _ id)} - {add_tbl_correct : forall P i limb, - limb_good i limb -> Geq (add_tbl P i limb G id) (add P (smul (2 ^ i * limb) B))}. - - Definition n_upto t : Z := - for ( i = 0; i (<) t; i++) updating (n = 0%Z) labels (continue) - {{ - x <- nth_limb i; - continue (n + (2^i)*x)%Z - }}; - n. - - - Lemma ScalarMultBase_correct : Geq ScalarMultBase (smul (n_upto k) B). - cbv [ScalarMultBase]. - eapply for_cps_ind with (invariant := fun i P => Geq P (smul (n_upto i) B )%Z). - - intros; omega. - - omega. - - intros; rewrite Z.ltb_lt in H; autorewrite with zsimplify; omega. - - autorewrite with zsimplify. symmetry; eapply (scalarmult_0_l(add:=add)). - - cbv [force_idZ id]; intros. clear H. - setoid_rewrite nth_limb_valid; setoid_rewrite add_tbl_valid. - setoid_rewrite <-H0; [reflexivity|]; clear H0. - - etransitivity. - eapply Proper_add_tbl; [eapply H1|reflexivity|reflexivity]. - clear H1. - replace (n_upto (i+1))%Z with (n_upto i + (2^i)*(nth_limb i _ id))%Z by admit. - rewrite scalarmult_add_l. - rewrite add_tbl_correct; [reflexivity|]. - apply nth_limb_good. - admit. - Admitted. -End ScalarMult. |