diff options
29 files changed, 627 insertions, 307 deletions
diff --git a/_CoqProject b/_CoqProject index 5b4c06f9c..cf46abd60 100644 --- a/_CoqProject +++ b/_CoqProject @@ -147,6 +147,11 @@ src/Specific/FancyMachine256/Barrett.v src/Specific/FancyMachine256/Core.v src/Specific/FancyMachine256/Montgomery.v src/Specific/GF25519Reflective/Common.v +src/Specific/GF25519Reflective/CommonBinOp.v +src/Specific/GF25519Reflective/CommonUnOp.v +src/Specific/GF25519Reflective/CommonUnOpFEToWire.v +src/Specific/GF25519Reflective/CommonUnOpFEToZ.v +src/Specific/GF25519Reflective/CommonUnOpWireToFE.v src/Specific/GF25519Reflective/Reified.v src/Specific/GF25519Reflective/Reified/Add.v src/Specific/GF25519Reflective/Reified/CarryAdd.v diff --git a/src/Experiments/Ed25519Extraction.v b/src/Experiments/Ed25519Extraction.v index 20a76f17f..eaa00bea4 100644 --- a/src/Experiments/Ed25519Extraction.v +++ b/src/Experiments/Ed25519Extraction.v @@ -233,7 +233,7 @@ Extraction Implicit Word.split1 [ 2 ]. Extraction Implicit Word.split2 [ 2 ]. Extraction Implicit WordUtil.cast_word [1 2 3]. Extraction Implicit WordUtil.wfirstn [ 2 4 ]. -Extract Inlined Constant WordUtil.cast_word => "". +Extraction Inline WordUtil.cast_word. Extract Inductive Word.word => "[Prelude.Bool]" [ "[]" "(:)" ] "(\fWO fWS w -> {- match_on_word -} case w of {[] -> fWO (); (b:w') -> fWS b w' } )". @@ -296,4 +296,4 @@ True Import Crypto.Spec.MxDH. Extraction Inline MxDH.ladderstep MxDH.montladder. -Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519.
\ No newline at end of file +Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519. diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v index bb833507f..5d9e64901 100644 --- a/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v @@ -5,9 +5,14 @@ Require Import Crypto.Util.ZUtil. Local Open Scope Z_scope. -Lemma neg_nonneg : forall x y, 0 <= ModularBaseSystemListZOperations.neg x y. -Proof. Admitted. +Lemma neg_nonneg : forall x y, 0 <= x -> 0 <= ModularBaseSystemListZOperations.neg x y. +Proof. + unfold neg; intros; break_match; auto with zarith. +Qed. Hint Resolve neg_nonneg : zarith. -Lemma neg_upperbound : forall x y, ModularBaseSystemListZOperations.neg x y <= Z.ones x. -Proof. Admitted. + +Lemma neg_upperbound : forall x y, 0 <= x -> ModularBaseSystemListZOperations.neg x y <= Z.ones x. +Proof. + unfold neg; intros; break_match; auto with zarith. +Qed. Hint Resolve neg_upperbound : zarith. diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 155698e56..7480db3b0 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -1071,7 +1071,7 @@ Section SquareRoots. by (rewrite carry_mul_opt_correct by auto; cbv [eq]; rewrite carry_mul_rep, mul_rep; reflexivity) end. - let RHS := match goal with |- {vs | eq ?vs ?RHS} => RHS end in + let RHS := match goal with |- {vs | eq vs ?RHS} => RHS end in let RHSf := match (eval pattern powx in RHS) with ?RHSf _ => RHSf end in change ({vs | eq vs (Let_In powx RHSf)}). match goal with diff --git a/src/MxDHRepChange.v b/src/MxDHRepChange.v index c99635baf..4596ad188 100644 --- a/src/MxDHRepChange.v +++ b/src/MxDHRepChange.v @@ -23,13 +23,15 @@ Section MxDHRepChange. Qed. Ltac t := + let hom := match goal with H : is_homomorphism |- _ => H end in + let mhom := constr:(@homomorphism_is_homomorphism _ _ _ _ _ _ _ _ _ _ _ hom) in repeat ( - rewrite homomorphism_id || - rewrite homomorphism_one || + rewrite (@homomorphism_id _ _ _ _ _ _ _ _ _ _ _ _ _ mhom) || + rewrite (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ hom) || + rewrite (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ hom) || + rewrite (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ hom) || + rewrite (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ hom) || rewrite homomorphism_a24 || - rewrite homomorphism_sub || - rewrite homomorphism_add || - rewrite homomorphism_mul || rewrite homomorphism_multiplicative_inverse_complete' || reflexivity ). @@ -75,7 +77,7 @@ Section MxDHRepChange. Lemma MxLoopIterRepChange b Fu s i Ku (HKu:Keq (FtoK Fu) Ku) : loopiter_eq (loopiter_phi (loopiter F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb1 Fu s i)) - (loopiter K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap b tb2 Ku (loopiter_phi s) i). + (loopiter K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap b tb2 Ku (loopiter_phi s) i). Proof. destruct_head' prod; break_match. simpl. @@ -98,7 +100,9 @@ Section MxDHRepChange. generalize dependent init; generalize dependent init'. induction xs; [solve [eauto]|]. repeat intro; simpl; rewrite IHxs by eauto. - f_equiv; eapply Proper_step'; eauto. + apply (_ : Proper ((R ==> eq ==> R) ==> SetoidList.eqlistA eq ==> R ==> R) (@fold_left _ _)); + try reflexivity; + eapply Proper_step'; eauto. Qed. Global Instance Proper_downto {T R} {Equivalence_R:@Equivalence T R} : @@ -154,4 +158,4 @@ Section MxDHRepChange. exact 0. exact 0. Qed. -End MxDHRepChange.
\ No newline at end of file +End MxDHRepChange. diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v index 9b58b5f5c..a3b51f28f 100644 --- a/src/Reflection/Z/Interpretations.v +++ b/src/Reflection/Z/Interpretations.v @@ -1,7 +1,5 @@ (** * Interpretation of PHOAS syntax for expression trees on ℤ *) -Require Import Bedrock.Nomega. Require Import Coq.ZArith.ZArith. -Require Import Coq.NArith.NArith. Require Import Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Application. @@ -16,9 +14,6 @@ Require Import Crypto.Util.Prod. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.WordUtil. Require Import Bedrock.Word. -Require Import Crypto.Assembly.WordizeUtil. -Require Import Crypto.Assembly.Evaluables. -Require Import Crypto.Assembly.QhasmUtil. Export Reflection.Syntax.Notations. Local Notation eta x := (fst x, snd x). @@ -215,16 +210,13 @@ Module Word64. := (forall x y z w, bounds_statement (wop x y z w) (Zop (word64ToZ x) (word64ToZ y) (word64ToZ z) (word64ToZ w))). - Require Import Crypto.Assembly.WordizeUtil. - Lemma word64ToZ_add : bounds_2statement add Z.add. Proof. w64ToZ_t. Qed. Lemma word64ToZ_sub : bounds_2statement sub Z.sub. Proof. w64ToZ_t. Qed. Lemma word64ToZ_mul : bounds_2statement mul Z.mul. Proof. w64ToZ_t. Qed. - Lemma word64ToZ_shl : bounds_2statement shl Z.shiftl. Proof. w64ToZ_t; w64ToZ_extra_t; unfold word64ToZ, wordBin. - rewrite wordToN_NToWord; [rewrite <- Z_inj_shiftl; reflexivity|]. + rewrite wordToN_NToWord_idempotent; [rewrite <- Z_inj_shiftl; reflexivity|]. apply N2Z.inj_lt. rewrite Z_inj_shiftl. destruct (Z.lt_ge_cases 0 ((word64ToZ x) << (word64ToZ y)))%Z; @@ -236,7 +228,7 @@ Module Word64. Lemma word64ToZ_shr : bounds_2statement shr Z.shiftr. Proof. w64ToZ_t; w64ToZ_extra_t; unfold word64ToZ, wordBin. - rewrite wordToN_NToWord; [rewrite <- Z_inj_shiftr; reflexivity|]. + rewrite wordToN_NToWord_idempotent; [rewrite <- Z_inj_shiftr; reflexivity|]. apply N2Z.inj_lt. rewrite Z_inj_shiftr. destruct (Z.lt_ge_cases 0 ((word64ToZ x) >> (word64ToZ y)))%Z; @@ -434,9 +426,9 @@ Module ZBounds. : Tuple.tuple t (S pred_n) := Tuple.push_option match int_width, Tuple.lift_option modulus, Tuple.lift_option value with - | Some int_width, Some modulus, Some value - => if check_conditional_subtract_bounds pred_n int_width modulus value - then Some (conditional_subtract' pred_n int_width modulus value) + | Some int_width, Some modulus, Some value' + => if check_conditional_subtract_bounds pred_n int_width modulus value' + then Some (conditional_subtract' pred_n int_width modulus value') else None | _, _, _ => None end. @@ -684,6 +676,10 @@ Module BoundedWord64. Ltac ktrans k := do k (etransitivity; [|eassumption]); assumption. Ltac trans' := first [ assumption | ktrans ltac:1 | ktrans ltac:2 ]. + Local Hint Resolve Word64.bit_width_pos : zarith. + Local Hint Extern 1 (Z.log2 _ < _)%Z => eapply Z.le_lt_trans; [ eapply Z.log2_le_mono; eassumption | eassumption ] : zarith. + (* Local *) Hint Resolve <- Z.log2_lt_pow2_alt : zarith. + (** TODO(jadep): Use the bounds lemma here to prove that if each component of [ret_val] is [Some (l, v, u)], then we can fill in @@ -696,6 +692,28 @@ Module BoundedWord64. pred_n (BoundedWordToBounds x) (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z) = true) : HList.hlist + (fun vlu : Z * ZBounds.bounds => + (0 <= ZBounds.lower (snd vlu))%Z /\ + (ZBounds.lower (snd vlu) <= fst vlu <= ZBounds.upper (snd vlu))%Z /\ + (Z.log2 (ZBounds.upper (snd vlu)) < Word64.bit_width)%Z) + (Tuple.map2 (fun v lu => (v, lu)) + (ModularBaseSystemListZOperations.conditional_subtract_modulus + (S pred_n) + (Word64.word64ToZ (value x)) + (Tuple.map Word64.word64ToZ (Tuple.map value y)) + (Tuple.map Word64.word64ToZ (Tuple.map value z))) + (ZBounds.conditional_subtract' + pred_n (BoundedWordToBounds x) + (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z))). + Proof. Admitted. + + Lemma conditional_subtract_bounded_word + (pred_n : nat) (x : BoundedWord) + (y z : Tuple.tuple BoundedWord (S pred_n)) + (H : ZBounds.check_conditional_subtract_bounds + pred_n (BoundedWordToBounds x) + (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z) = true) + : HList.hlist (fun vlu : Word64.word64 * ZBounds.bounds => (0 <= ZBounds.lower (snd vlu))%Z /\ (ZBounds.lower (snd vlu) <= Word64.word64ToZ (fst vlu) <= ZBounds.upper (snd vlu))%Z /\ @@ -706,12 +724,73 @@ Module BoundedWord64. (ZBounds.conditional_subtract' pred_n (BoundedWordToBounds x) (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z))). - Proof. Admitted. + Proof. + generalize (conditional_subtract_bounded pred_n x y z H). + unfold Word64.conditional_subtract; rewrite Tuple.map2_map_fst. + rewrite <- (Tuple.map_map2 (fun a b => (a, b)) (fun ab => (Word64.ZToWord64 (fst ab), snd ab))). + rewrite HList.hlist_map; simpl @fst; simpl @snd. + apply HList.hlist_impl, HList.const. + intros; destruct_head' and; repeat split; + autorewrite with push_word64ToZ; omega. + Qed. + Lemma conditional_subtract_bounded_lite_helper + (pred_n : nat) (x : BoundedWord) + (y z : Tuple.tuple BoundedWord (S pred_n)) + (H : ZBounds.check_conditional_subtract_bounds + pred_n (BoundedWordToBounds x) + (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z) = true) + : HList.hlist + (fun v : Z => + (0 <= v)%Z /\ + (Z.log2 v < Word64.bit_width)%Z) + (Tuple.map + (@fst _ _) + (Tuple.map2 (fun v lu => (v, lu)) + (ModularBaseSystemListZOperations.conditional_subtract_modulus + (S pred_n) + (Word64.word64ToZ (value x)) + (Tuple.map Word64.word64ToZ (Tuple.map value y)) + (Tuple.map Word64.word64ToZ (Tuple.map value z))) + (ZBounds.conditional_subtract' + pred_n (BoundedWordToBounds x) + (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z)))). + Proof. + generalize (conditional_subtract_bounded pred_n x y z H). + rewrite HList.hlist_map. + apply HList.hlist_impl, HList.const; intros. + destruct_head' and. + split; try omega; []. + eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eassumption ]; omega. + Qed. + + Lemma conditional_subtract_bounded_lite + (pred_n : nat) + (xbw : BoundedWord) (ybw zbw : Tuple.tuple BoundedWord (S pred_n)) + (x : Word64.word64) (y z : Tuple.tuple Word64.word64 (S pred_n)) + (xb : ZBounds.bounds) (yb zb : Tuple.tuple ZBounds.bounds (S pred_n)) + (Hx : value xbw = x) (Hy : Tuple.map value ybw = y) (Hz : Tuple.map value zbw = z) + (Hxb : BoundedWordToBounds xbw = xb) + (Hyb : Tuple.map BoundedWordToBounds ybw = yb) (Hzb : Tuple.map BoundedWordToBounds zbw = zb) + (Hc : ZBounds.check_conditional_subtract_bounds pred_n xb yb zb = true) + : HList.hlist (fun v : Z => (0 <= v)%Z /\ (Z.log2 v < Z.of_nat Word64.bit_width)%Z) + (ModularBaseSystemListZOperations.conditional_subtract_modulus + (S pred_n) + (Word64.word64ToZ x) + (Tuple.map Word64.word64ToZ y) + (Tuple.map Word64.word64ToZ z)). + Proof. + subst. + generalize (conditional_subtract_bounded_lite_helper pred_n xbw ybw zbw Hc). + rewrite Tuple.map_map2; simpl @fst. + rewrite Tuple.map2_fst, Tuple.map_id. + trivial. + Qed. + + (* TODO (rsloan): not entirely sure what's the best way to match on these... *) Local Ltac kill_assumptions := repeat split; abstract (cbn; assumption). - (* TODO (rsloan): not entirely sure what's the best way to match on these... *) Local Ltac apply_update lem lower0 value0 upper0 lower1 value1 upper1 := first [ apply (lem 64 lower1 value1 upper1 lower0 value0 upper0); kill_assumptions | apply (lem 64 lower0 value0 upper0 lower1 value1 upper1); kill_assumptions]. @@ -780,7 +859,7 @@ Module BoundedWord64. | progress subst | progress inversion_option | intro - | solve [ auto using conditional_subtract_bounded ] ] + | solve [ auto using conditional_subtract_bounded_word ] ] ). Defined. @@ -851,18 +930,18 @@ Module BoundedWord64. eauto. Qed. - Local Notation binop_correct_None op opW opB := + Local Notation binop_correct_None op opB := (forall x y, op (Some x) (Some y) = None -> opB (Some (BoundedWordToBounds x)) (Some (BoundedWordToBounds y)) = None) (only parsing). - Local Notation op4_correct_None op opW opB := + Local Notation op4_correct_None op opB := (forall x y z w, op (Some x) (Some y) (Some z) (Some w) = None -> opB (Some (BoundedWordToBounds x)) (Some (BoundedWordToBounds y)) (Some (BoundedWordToBounds z)) (Some (BoundedWordToBounds w)) = None) (only parsing). - Local Notation op1_tuple2_correct_None op opW opB := + Local Notation op1_tuple2_correct_None op opB := (forall x y z, Tuple.lift_option (op (Some x) (Tuple.push_option (Some y)) (Tuple.push_option (Some z))) = None -> Tuple.lift_option @@ -873,7 +952,7 @@ Module BoundedWord64. (only parsing). Lemma t_map2_correct_None opW opB pf - : binop_correct_None (t_map2 opW opB pf) opW opB. + : binop_correct_None (t_map2 opW opB pf) opB. Proof. intros ?? H. unfold t_map2 in H; convoy_destruct_in H; destruct_head' ZBounds.bounds; @@ -883,7 +962,7 @@ Module BoundedWord64. Qed. Lemma t_map4_correct_None opW opB pf - : op4_correct_None (t_map4 opW opB pf) opW opB. + : op4_correct_None (t_map4 opW opB pf) opB. Proof. intros ???? H. unfold t_map4 in H; convoy_destruct_in H; destruct_head' ZBounds.bounds; @@ -893,7 +972,7 @@ Module BoundedWord64. Qed. Lemma t_map1_tuple2_correct_None {n} opW opB pf - : op1_tuple2_correct_None (t_map1_tuple2 (n:=n) opW opB pf) opW opB. + : op1_tuple2_correct_None (t_map1_tuple2 (n:=n) opW opB pf) opB. Proof. intros ??? H. unfold t_map1_tuple2 in H; unfold BoundedWordToBounds in *. diff --git a/src/Reflection/Z/Interpretations/Relations.v b/src/Reflection/Z/Interpretations/Relations.v index 457d0d5ad..71d25fa3f 100644 --- a/src/Reflection/Z/Interpretations/Relations.v +++ b/src/Reflection/Z/Interpretations/Relations.v @@ -231,8 +231,8 @@ Lemma related_tuples_lift_relation2_untuple' <-> LiftOption.lift_relation2 (interp_flat_type_rel_pointwise2 (fun _ => R)) TZ - (option_map (flat_interp_untuple' (T:=Tbase TZ)) t) - (option_map (flat_interp_untuple' (T:=Tbase TZ)) u). + (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) t) + (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) u). Proof. induction n. { destruct_head' option; reflexivity. } @@ -257,8 +257,8 @@ Lemma related_tuples_lift_relation2_untuple'_ext <-> LiftOption.lift_relation2 (interp_flat_type_rel_pointwise2 (fun _ => R)) TZ - (option_map (flat_interp_untuple' (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t))) - (option_map (flat_interp_untuple' (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))). + (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t))) + (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))). Proof. induction n. { destruct_head_hnf' option; reflexivity. } @@ -270,7 +270,7 @@ Proof. (etransitivity; [ | first [ refine (f_equal (option_map (@fst _ _)) (_ : _ = Some (_, _))); eassumption | refine (f_equal (option_map (@snd _ _)) (_ : _ = Some (_, _))); eassumption ] ]); - simpl in *; break_match; simpl in *; congruence. } + instantiate; simpl in *; break_match; simpl in *; congruence. } destruct_head_hnf' prod; destruct_head_hnf' option; simpl @fst in *; simpl @snd in *; @@ -319,6 +319,7 @@ Local Arguments LiftOption.of' _ _ !_ / . Local Arguments BoundedWord64.BoundedWordToBounds !_ / . Local Ltac t_map1_tuple2_t_step := + instantiate; first [ exact I | reflexivity | progress destruct_head_hnf' False @@ -330,7 +331,7 @@ Local Ltac t_map1_tuple2_t_step := | intro | apply @related_tuples_None_left; constructor | apply -> @related_tuples_Some_left - | apply <- @related_tuples_proj_eq_rel_untuple + | refine (proj2 (@related_tuples_proj_eq_rel_untuple _ _ _ _ _ _) _) | apply <- @related_tuples_lift_relation2_untuple' | match goal with | [ H : appcontext[LiftOption.lift_relation] |- _ ] @@ -491,7 +492,7 @@ Local Ltac Word64.Rewrites.word64_util_arith ::= auto with zarith ] | apply Z.land_nonneg; Word64.Rewrites.word64_util_arith | eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eassumption ]; - apply Z.min_case_strong; intros; + instantiate; apply Z.min_case_strong; intros; first [ etransitivity; [ apply Z.land_upper_bound_l | ]; omega | etransitivity; [ apply Z.land_upper_bound_r | ]; omega ] | rewrite Z.log2_lor by omega; @@ -556,10 +557,15 @@ Tactic Notation "admit" := abstract case proof_admitted. Local Arguments related'_Z _ _ _ / . Lemma related_Z_t_map1_tuple2 n opZ opW opB pf (H : forall x y z bxs bys bzs brs, - Tuple.push_option (Some brs) = opB (Some bxs) (Tuple.push_option (Some bys)) (Tuple.push_option (Some bzs)) + Some brs = Tuple.lift_option (opB (Some bxs) (Tuple.push_option (Some bys)) (Tuple.push_option (Some bzs))) -> is_in_bounds x bxs - (*-> is_in_bounds y bys - -> is_in_bounds z bzs + -> { ybw : Tuple.tuple BoundedWord64.BoundedWord _ + | Tuple.map BoundedWord64.value ybw = y + /\ Tuple.map BoundedWord64.BoundedWordToBounds ybw = bys } + -> { zbw : Tuple.tuple BoundedWord64.BoundedWord _ + | Tuple.map BoundedWord64.value zbw = z + /\ Tuple.map BoundedWord64.BoundedWordToBounds zbw = bzs } + (* -> is_in_bounds (opW x y z) brs*) -> Tuple.map Word64.word64ToZ (opW x y z) = (opZ (Word64.word64ToZ x) (Tuple.map Word64.word64ToZ y) (Tuple.map Word64.word64ToZ z))) sv1 sv2 @@ -594,8 +600,13 @@ Local Ltac related_Z_op_fin_t_step := | progress inversion_option | intro | progress autorewrite with push_word64ToZ - | match goal with H : andb _ _ = true |- _ => rewrite Bool.andb_true_iff in H end - | progress Z.ltb_to_lt ]. + | match goal with + | [ H : andb _ _ = true |- _ ] => rewrite Bool.andb_true_iff in H + | [ H : context[Tuple.lift_option (Tuple.push_option _)] |- _ ] + => rewrite Tuple.lift_push_option in H + end + | progress Z.ltb_to_lt + | (progress unfold ZBounds.conditional_subtract in * ); break_match_hyps ]. Local Ltac related_Z_op_fin_t := repeat related_Z_op_fin_t_step. Local Opaque Word64.bit_width. @@ -614,9 +625,13 @@ Proof. { apply related_Z_t_map4; related_Z_op_fin_t. } { apply related_Z_t_map4; related_Z_op_fin_t. } { apply related_Z_t_map1_tuple2; related_Z_op_fin_t; - rewrite Word64.word64ToZ_conditional_subtract; try Word64.Rewrites.word64_util_arith. - pose proof BoundedWord64.conditional_subtract_bounded. - admit. (** TODO(jadep or jgross): Fill me in *) } + rewrite Word64.word64ToZ_conditional_subtract; try Word64.Rewrites.word64_util_arith; []. + destruct_head' sig; destruct_head' and; subst. + eapply BoundedWord64.conditional_subtract_bounded_lite + with (xbw := {| BoundedWord64.value := _ |}); + [ .. | eassumption ]; reflexivity. + Grab Existential Variables. + omega. } Qed. Create HintDb interp_related discriminated. diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index 80932d4df..3d448f97c 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -126,48 +126,7 @@ Notation correct_and_bounded_genT ropW'v ropZ_sigv /\ interp_type_rel_pointwise2 Relations.related_word64 (Interp (@BoundedWord64.interp_op) ropBoundedWord64) (Interp (@Word64.interp_op) ropW)) (only parsing). -Local Ltac args_to_bounded_helper v := - lazymatch v with - | (?x, ?xs) - => args_to_bounded_helper x; [ .. | args_to_bounded_helper xs ] - | ?w - => try refine (_, _); [ refine {| BoundedWord64.value := w |} | .. ] - end. - -Local Ltac make_args x := - let x' := fresh "x'" in - pose (x : id _) as x'; - cbv [fe25519W wire_digitsW] in x; destruct_head' prod; - cbv [fst snd] in *; - simpl @fe25519WToZ in *; - simpl @wire_digitsWToZ in *; - let T := fresh in - evar (T : Type); - cut T; subst T; - [ let H := fresh in - intro H; - let xv := (eval hnf in x') in - args_to_bounded_helper xv; - [ instantiate; - destruct_head' and; - match goal with - | [ H : ?T |- _ ] - => is_evar T; - refine (let c := proj1 H in _); (* work around broken evars in Coq 8.4 *) - lazymatch goal with H := proj1 _ |- _ => refine H end - end.. ] - | instantiate; - repeat match goal with H : is_bounded _ = true |- _ => unfold_is_bounded_in H end; - repeat match goal with H : wire_digits_is_bounded _ = true |- _ => unfold_is_bounded_in H end; - destruct_head' and; - Z.ltb_to_lt; - repeat first [ eexact I - | apply conj; - [ repeat apply conj; [ | eassumption | eassumption | ]; - instantiate; vm_compute; [ refine (fun x => match x with eq_refl => I end) | reflexivity ] - | ] ] ]. - -Local Ltac app_tuples x y := +Ltac app_tuples x y := let tx := type of x in lazymatch (eval hnf in tx) with | prod _ _ => let xs := app_tuples (snd x) y in @@ -175,15 +134,120 @@ Local Ltac app_tuples x y := | _ => constr:((x, y)) end. -Class is_evar {T} (x : T) := make_is_evar : True. -Hint Extern 0 (is_evar ?e) => is_evar e; exact I : typeclass_instances. +Local Arguments Tuple.map2 : simpl never. +Local Arguments Tuple.map : simpl never. + +Fixpoint args_to_bounded_helperT {n} + (v : Tuple.tuple' Word64.word64 n) + (bounds : Tuple.tuple' (Z * Z) n) + (pf : List.fold_right + andb true + (Tuple.to_list + _ + (Tuple.map2 + (n:=S n) + (fun bounds v => + let '(lower, upper) := bounds in ((lower <=? v)%Z && (v <=? upper)%Z)%bool) + bounds + (Tuple.map (n:=S n) Word64.word64ToZ v))) = true) + (res : Type) + {struct n} + : Type. +Proof. + refine (match n return (forall (v : Tuple.tuple' _ n) (bounds : Tuple.tuple' _ n), + List.fold_right + _ _ (Tuple.to_list + _ + (Tuple.map2 (n:=S n) _ bounds (Tuple.map (n:=S n) _ v))) = true + -> Type) + with + | 0 => fun v' bounds' pf0 => forall pf1 : (0 <= fst bounds' /\ Z.log2 (snd bounds') < Z.of_nat Word64.bit_width)%Z, res + | S n' => fun v' bounds' pf0 => let t := _ in + forall pf1 : (0 <= fst (snd bounds') /\ Z.log2 (snd (snd bounds')) < Z.of_nat Word64.bit_width)%Z, @args_to_bounded_helperT n' (fst v') (fst bounds') t res + end v bounds pf). + { clear -pf0. + abstract ( + destruct v', bounds'; simpl @fst; + rewrite Tuple.map_S in pf0; + simpl in pf0; + rewrite Tuple.map2_S in pf0; + simpl @List.fold_right in *; + rewrite Bool.andb_true_iff in pf0; tauto + ). } +Defined. + +Fixpoint args_to_bounded_helper {n} res + {struct n} + : forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res. +Proof. + refine match n return (forall v bounds pf, (Tuple.tuple' BoundedWord64.BoundedWord n -> res) -> @args_to_bounded_helperT n v bounds pf res) with + | 0 => fun v bounds pf f pf' => f {| BoundedWord64.lower := fst bounds ; BoundedWord64.value := v ; BoundedWord64.upper := snd bounds |} + | S n' + => fun v bounds pf f pf' + => @args_to_bounded_helper + n' res (fst v) (fst bounds) _ + (fun ts => f (ts, {| BoundedWord64.lower := fst (snd bounds) ; BoundedWord64.value := snd v ; BoundedWord64.upper := snd (snd bounds) |})) + end. + { clear -pf pf'. + unfold Tuple.map2, Tuple.map in pf; simpl in *. + abstract ( + destruct bounds; + simpl in *; + rewrite !Bool.andb_true_iff in pf; + destruct_head' and; + Z.ltb_to_lt; auto + ). } + { simpl in *. + clear -pf pf'. + abstract ( + destruct bounds as [? [? ?] ], v; simpl in *; + rewrite Tuple.map_S in pf; simpl in pf; rewrite Tuple.map2_S in pf; + simpl in pf; + rewrite !Bool.andb_true_iff in pf; + destruct_head' and; + Z.ltb_to_lt; auto + ). } +Defined. + +Definition assoc_right'' + := Eval cbv [Tuple.assoc_right' Tuple.rsnoc' fst snd] in @Tuple.assoc_right'. + +Definition args_to_bounded {n} v bounds pf + := Eval cbv [args_to_bounded_helper assoc_right''] in + @args_to_bounded_helper n _ v bounds pf (@assoc_right'' _ _). + +Local Ltac get_len T := + match (eval hnf in T) with + | prod ?A ?B + => let a := get_len A in + let b := get_len B in + (eval compute in (a + b)%nat) + | _ => constr:(1%nat) + end. + +Local Ltac args_to_bounded x H := + let x' := fresh in + set (x' := x); + compute in x; + let len := (let T := type of x in get_len T) in + destruct_head' prod; + let c := constr:(args_to_bounded (n:=pred len) x' _ H) in + let bounds := lazymatch c with args_to_bounded _ ?bounds _ => bounds end in + let c := (eval cbv [all_binders_for ExprUnOpT interp_flat_type args_to_bounded bounds pred fst snd] in c) in + apply c; compute; clear; + try abstract ( + repeat split; + solve [ reflexivity + | refine (fun v => match v with eq_refl => I end) ] + ). Definition unop_args_to_bounded (x : fe25519W) (H : is_bounded (fe25519WToZ x) = true) : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpT). -Proof. make_args x. Defined. +Proof. args_to_bounded x H. Defined. + Definition unopWireToFE_args_to_bounded (x : wire_digitsW) (H : wire_digits_is_bounded (wire_digitsWToZ x) = true) : interp_flat_type (fun _ => BoundedWord64.BoundedWord) (all_binders_for ExprUnOpWireToFET). -Proof. make_args x. Defined. +Proof. args_to_bounded x H. Defined. Definition binop_args_to_bounded (x : fe25519W * fe25519W) (H : is_bounded (fe25519WToZ (fst x)) = true) (H' : is_bounded (fe25519WToZ (snd x)) = true) @@ -225,7 +289,6 @@ Local Ltac make_bounds_prop bounds orig_bounds := | None => false end). - Definition unop_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders ExprUnOpT)) : bool. Proof. make_bounds_prop bounds ExprUnOp_bounds. Defined. Definition binop_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders ExprBinOpT)) : bool. @@ -244,7 +307,7 @@ Defined. various kinds of correct and boundedness, and abstract in Gallina rather than Ltac *) -Local Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := +Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := let Heq := fresh "Heq" in let Hbounds0 := fresh "Hbounds0" in let Hbounds1 := fresh "Hbounds1" in @@ -311,192 +374,6 @@ Local Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := change Word64.word64ToZ with word64ToZ in *; repeat apply conj; Z.ltb_to_lt; try omega; try reflexivity. -Local Opaque Interp. -Lemma ExprBinOp_correct_and_bounded - ropW op (ropZ_sig : rexpr_binop_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall xy - (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy))) - (Hxy : is_bounded (fe25519WToZ (fst xy)) = true - /\ is_bounded (fe25519WToZ (snd xy)) = true), - let Hx := let (Hx, Hy) := Hxy in Hx in - let Hy := let (Hx, Hy) := Hxy in Hy in - let args := binop_args_to_bounded xy Hx Hy in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall xy - (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy))) - (Hxy : is_bounded (fe25519WToZ (fst xy)) = true - /\ is_bounded (fe25519WToZ (snd xy)) = true), - let Hx := let (Hx, Hy) := Hxy in Hx in - let Hy := let (Hx, Hy) := Hxy in Hy in - let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in - let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in - match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) - with - | Some bounds => binop_bounds_good bounds = true - | None => False - end) - : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x y Hx Hy. - pose x as x'; pose y as y'. - hnf in x, y; destruct_head' prod. - specialize (H0 (x', y') (conj Hx Hy)). - specialize (H1 (x', y') (conj Hx Hy)). - let args := constr:(binop_args_to_bounded (x', y') Hx Hy) in - t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. -Qed. - -Lemma ExprUnOp_correct_and_bounded - ropW op (ropZ_sig : rexpr_unop_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x - (x := eta_fe25519W x) - (Hx : is_bounded (fe25519WToZ x) = true), - let args := unop_args_to_bounded x Hx in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x - (x := eta_fe25519W x) - (Hx : is_bounded (fe25519WToZ x) = true), - let args := unop_args_to_bounded x Hx in - let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in - match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) - with - | Some bounds => unop_bounds_good bounds = true - | None => False - end) - : unop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x Hx. - pose x as x'. - hnf in x; destruct_head' prod. - specialize (H0 x' Hx). - specialize (H1 x' Hx). - let args := constr:(unop_args_to_bounded x' Hx) in - t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. -Qed. - -Lemma ExprUnOpFEToWire_correct_and_bounded - ropW op (ropZ_sig : rexpr_unop_FEToWire_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x - (x := eta_fe25519W x) - (Hx : is_bounded (fe25519WToZ x) = true), - let args := unop_args_to_bounded x Hx in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x - (x := eta_fe25519W x) - (Hx : is_bounded (fe25519WToZ x) = true), - let args := unop_args_to_bounded x Hx in - let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in - match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) - with - | Some bounds => unopFEToWire_bounds_good bounds = true - | None => False - end) - : unop_FEToWire_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x Hx. - pose x as x'. - hnf in x; destruct_head' prod. - specialize (H0 x' Hx). - specialize (H1 x' Hx). - let args := constr:(unop_args_to_bounded x' Hx) in - t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. -Qed. - -Lemma ExprUnOpWireToFE_correct_and_bounded - ropW op (ropZ_sig : rexpr_unop_WireToFE_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x - (x := eta_wire_digitsW x) - (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), - let args := unopWireToFE_args_to_bounded x Hx in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x - (x := eta_wire_digitsW x) - (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), - let args := unopWireToFE_args_to_bounded x Hx in - let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in - match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) - with - | Some bounds => unopWireToFE_bounds_good bounds = true - | None => False - end) - : unop_WireToFE_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x Hx. - pose x as x'. - hnf in x; destruct_head' prod. - specialize (H0 x' Hx). - specialize (H1 x' Hx). - let args := constr:(unopWireToFE_args_to_bounded x' Hx) in - t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. -Qed. - -Lemma ExprUnOpFEToZ_correct_and_bounded - ropW op (ropZ_sig : rexpr_unop_FEToZ_sig op) - (Hbounds : correct_and_bounded_genT ropW ropZ_sig) - (H0 : forall x - (x := eta_fe25519W x) - (Hx : is_bounded (fe25519WToZ x) = true), - let args := unop_args_to_bounded x Hx in - match LiftOption.of' - (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) - (LiftOption.to' (Some args))) - with - | Some _ => True - | None => False - end) - (H1 : forall x - (x := eta_fe25519W x) - (Hx : is_bounded (fe25519WToZ x) = true), - let args := unop_args_to_bounded x Hx in - let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in - match LiftOption.of' - (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) - with - | Some bounds => unopFEToZ_bounds_good bounds = true - | None => False - end) - : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op. -Proof. - intros x Hx. - pose x as x'. - hnf in x; destruct_head' prod. - specialize (H0 x' Hx). - specialize (H1 x' Hx). - let args := constr:(unop_args_to_bounded x' Hx) in - t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. -Qed. Ltac rexpr_correct := let ropW' := fresh in diff --git a/src/Specific/GF25519Reflective/CommonBinOp.v b/src/Specific/GF25519Reflective/CommonBinOp.v new file mode 100644 index 000000000..32dae16e6 --- /dev/null +++ b/src/Specific/GF25519Reflective/CommonBinOp.v @@ -0,0 +1,50 @@ +Require Export Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519BoundedCommon. +Require Import Crypto.Reflection.Z.Interpretations. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Util.Tactics. + +Local Opaque Interp. +Lemma ExprBinOp_correct_and_bounded + ropW op (ropZ_sig : rexpr_binop_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall xy + (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy))) + (Hxy : is_bounded (fe25519WToZ (fst xy)) = true + /\ is_bounded (fe25519WToZ (snd xy)) = true), + let Hx := let (Hx, Hy) := Hxy in Hx in + let Hy := let (Hx, Hy) := Hxy in Hy in + let args := binop_args_to_bounded xy Hx Hy in + match LiftOption.of' + (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) + (LiftOption.to' (Some args))) + with + | Some _ => True + | None => False + end) + (H1 : forall xy + (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy))) + (Hxy : is_bounded (fe25519WToZ (fst xy)) = true + /\ is_bounded (fe25519WToZ (snd xy)) = true), + let Hx := let (Hx, Hy) := Hxy in Hx in + let Hy := let (Hx, Hy) := Hxy in Hy in + let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in + let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in + match LiftOption.of' + (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) + with + | Some bounds => binop_bounds_good bounds = true + | None => False + end) + : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. +Proof. + intros x y Hx Hy. + pose x as x'; pose y as y'. + hnf in x, y; destruct_head' prod. + specialize (H0 (x', y') (conj Hx Hy)). + specialize (H1 (x', y') (conj Hx Hy)). + let args := constr:(binop_args_to_bounded (x', y') Hx Hy) in + t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. +Qed. diff --git a/src/Specific/GF25519Reflective/CommonUnOp.v b/src/Specific/GF25519Reflective/CommonUnOp.v new file mode 100644 index 000000000..eac381b50 --- /dev/null +++ b/src/Specific/GF25519Reflective/CommonUnOp.v @@ -0,0 +1,44 @@ +Require Export Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519BoundedCommon. +Require Import Crypto.Reflection.Z.Interpretations. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Util.Tactics. + +Local Opaque Interp. +Lemma ExprUnOp_correct_and_bounded + ropW op (ropZ_sig : rexpr_unop_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall x + (x := eta_fe25519W x) + (Hx : is_bounded (fe25519WToZ x) = true), + let args := unop_args_to_bounded x Hx in + match LiftOption.of' + (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) + (LiftOption.to' (Some args))) + with + | Some _ => True + | None => False + end) + (H1 : forall x + (x := eta_fe25519W x) + (Hx : is_bounded (fe25519WToZ x) = true), + let args := unop_args_to_bounded x Hx in + let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in + match LiftOption.of' + (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) + with + | Some bounds => unop_bounds_good bounds = true + | None => False + end) + : unop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. +Proof. + intros x Hx. + pose x as x'. + hnf in x; destruct_head' prod. + specialize (H0 x' Hx). + specialize (H1 x' Hx). + let args := constr:(unop_args_to_bounded x' Hx) in + t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. +Qed. diff --git a/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v b/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v new file mode 100644 index 000000000..2fa1d2ee3 --- /dev/null +++ b/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v @@ -0,0 +1,44 @@ +Require Export Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519BoundedCommon. +Require Import Crypto.Reflection.Z.Interpretations. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Util.Tactics. + +Local Opaque Interp. +Lemma ExprUnOpFEToWire_correct_and_bounded + ropW op (ropZ_sig : rexpr_unop_FEToWire_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall x + (x := eta_fe25519W x) + (Hx : is_bounded (fe25519WToZ x) = true), + let args := unop_args_to_bounded x Hx in + match LiftOption.of' + (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) + (LiftOption.to' (Some args))) + with + | Some _ => True + | None => False + end) + (H1 : forall x + (x := eta_fe25519W x) + (Hx : is_bounded (fe25519WToZ x) = true), + let args := unop_args_to_bounded x Hx in + let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in + match LiftOption.of' + (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) + with + | Some bounds => unopFEToWire_bounds_good bounds = true + | None => False + end) + : unop_FEToWire_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. +Proof. + intros x Hx. + pose x as x'. + hnf in x; destruct_head' prod. + specialize (H0 x' Hx). + specialize (H1 x' Hx). + let args := constr:(unop_args_to_bounded x' Hx) in + t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. +Qed. diff --git a/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v b/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v new file mode 100644 index 000000000..7528cfc2d --- /dev/null +++ b/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v @@ -0,0 +1,44 @@ +Require Export Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519BoundedCommon. +Require Import Crypto.Reflection.Z.Interpretations. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Util.Tactics. + +Local Opaque Interp. +Lemma ExprUnOpFEToZ_correct_and_bounded + ropW op (ropZ_sig : rexpr_unop_FEToZ_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall x + (x := eta_fe25519W x) + (Hx : is_bounded (fe25519WToZ x) = true), + let args := unop_args_to_bounded x Hx in + match LiftOption.of' + (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) + (LiftOption.to' (Some args))) + with + | Some _ => True + | None => False + end) + (H1 : forall x + (x := eta_fe25519W x) + (Hx : is_bounded (fe25519WToZ x) = true), + let args := unop_args_to_bounded x Hx in + let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in + match LiftOption.of' + (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) + with + | Some bounds => unopFEToZ_bounds_good bounds = true + | None => False + end) + : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op. +Proof. + intros x Hx. + pose x as x'. + hnf in x; destruct_head' prod. + specialize (H0 x' Hx). + specialize (H1 x' Hx). + let args := constr:(unop_args_to_bounded x' Hx) in + t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. +Qed. diff --git a/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v b/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v new file mode 100644 index 000000000..d61807413 --- /dev/null +++ b/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v @@ -0,0 +1,44 @@ +Require Export Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519BoundedCommon. +Require Import Crypto.Reflection.Z.Interpretations. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Util.Tactics. + +Local Opaque Interp. +Lemma ExprUnOpWireToFE_correct_and_bounded + ropW op (ropZ_sig : rexpr_unop_WireToFE_sig op) + (Hbounds : correct_and_bounded_genT ropW ropZ_sig) + (H0 : forall x + (x := eta_wire_digitsW x) + (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), + let args := unopWireToFE_args_to_bounded x Hx in + match LiftOption.of' + (ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW)) + (LiftOption.to' (Some args))) + with + | Some _ => True + | None => False + end) + (H1 : forall x + (x := eta_wire_digitsW x) + (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true), + let args := unopWireToFE_args_to_bounded x Hx in + let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.BoundedWordToBounds) args in + match LiftOption.of' + (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x'))) + with + | Some bounds => unopWireToFE_bounds_good bounds = true + | None => False + end) + : unop_WireToFE_correct_and_bounded (MapInterp (fun _ x => x) ropW) op. +Proof. + intros x Hx. + pose x as x'. + hnf in x; destruct_head' prod. + specialize (H0 x' Hx). + specialize (H1 x' Hx). + let args := constr:(unopWireToFE_args_to_bounded x' Hx) in + t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. +Qed. diff --git a/src/Specific/GF25519Reflective/Reified/Add.v b/src/Specific/GF25519Reflective/Reified/Add.v index 36357fcb7..ae3a6a4c6 100644 --- a/src/Specific/GF25519Reflective/Reified/Add.v +++ b/src/Specific/GF25519Reflective/Reified/Add.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonBinOp. Definition raddZ_sig : rexpr_binop_sig add. Proof. reify_sig. Defined. Definition raddW := Eval vm_compute in rword_of_Z raddZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/CarryAdd.v b/src/Specific/GF25519Reflective/Reified/CarryAdd.v index 0ff563a8c..3051121c0 100644 --- a/src/Specific/GF25519Reflective/Reified/CarryAdd.v +++ b/src/Specific/GF25519Reflective/Reified/CarryAdd.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonBinOp. Definition rcarry_addZ_sig : rexpr_binop_sig carry_add. Proof. reify_sig. Defined. Definition rcarry_addW := Eval vm_compute in rword_of_Z rcarry_addZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/CarryOpp.v b/src/Specific/GF25519Reflective/Reified/CarryOpp.v index 4c21fbeb8..571b9db97 100644 --- a/src/Specific/GF25519Reflective/Reified/CarryOpp.v +++ b/src/Specific/GF25519Reflective/Reified/CarryOpp.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonUnOp. Definition rcarry_oppZ_sig : rexpr_unop_sig carry_opp. Proof. reify_sig. Defined. Definition rcarry_oppW := Eval vm_compute in rword_of_Z rcarry_oppZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/CarrySub.v b/src/Specific/GF25519Reflective/Reified/CarrySub.v index 3acfb1f45..fda466861 100644 --- a/src/Specific/GF25519Reflective/Reified/CarrySub.v +++ b/src/Specific/GF25519Reflective/Reified/CarrySub.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonBinOp. Definition rcarry_subZ_sig : rexpr_binop_sig carry_sub. Proof. reify_sig. Defined. Definition rcarry_subW := Eval vm_compute in rword_of_Z rcarry_subZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/Freeze.v b/src/Specific/GF25519Reflective/Reified/Freeze.v index e3ecc62c8..0dcea29e4 100644 --- a/src/Specific/GF25519Reflective/Reified/Freeze.v +++ b/src/Specific/GF25519Reflective/Reified/Freeze.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonUnOp. Definition rfreezeZ_sig : rexpr_unop_sig freeze. Proof. reify_sig. Defined. Definition rfreezeW := Eval vm_compute in rword_of_Z rfreezeZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/GeModulus.v b/src/Specific/GF25519Reflective/Reified/GeModulus.v index 73ee6904a..69eb3ba41 100644 --- a/src/Specific/GF25519Reflective/Reified/GeModulus.v +++ b/src/Specific/GF25519Reflective/Reified/GeModulus.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonUnOpFEToZ. Definition rge_modulusZ_sig : rexpr_unop_FEToZ_sig ge_modulus. Proof. reify_sig. Defined. Definition rge_modulusW := Eval vm_compute in rword_of_Z rge_modulusZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/Mul.v b/src/Specific/GF25519Reflective/Reified/Mul.v index a206f02a1..0c298134d 100644 --- a/src/Specific/GF25519Reflective/Reified/Mul.v +++ b/src/Specific/GF25519Reflective/Reified/Mul.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonBinOp. Definition rmulZ_sig : rexpr_binop_sig mul. Proof. reify_sig. Defined. Definition rmulW := Eval vm_compute in rword_of_Z rmulZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/Opp.v b/src/Specific/GF25519Reflective/Reified/Opp.v index 907771b14..58f2a6fbb 100644 --- a/src/Specific/GF25519Reflective/Reified/Opp.v +++ b/src/Specific/GF25519Reflective/Reified/Opp.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonUnOp. Definition roppZ_sig : rexpr_unop_sig opp. Proof. reify_sig. Defined. Definition roppW := Eval vm_compute in rword_of_Z roppZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/Pack.v b/src/Specific/GF25519Reflective/Reified/Pack.v index a7cf4fc13..cd85d0cd7 100644 --- a/src/Specific/GF25519Reflective/Reified/Pack.v +++ b/src/Specific/GF25519Reflective/Reified/Pack.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonUnOpFEToWire. Definition rpackZ_sig : rexpr_unop_FEToWire_sig pack. Proof. reify_sig. Defined. Definition rpackW := Eval vm_compute in rword_of_Z rpackZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/Sub.v b/src/Specific/GF25519Reflective/Reified/Sub.v index 9b684248d..03356cd50 100644 --- a/src/Specific/GF25519Reflective/Reified/Sub.v +++ b/src/Specific/GF25519Reflective/Reified/Sub.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonBinOp. Definition rsubZ_sig : rexpr_binop_sig sub. Proof. reify_sig. Defined. Definition rsubW := Eval vm_compute in rword_of_Z rsubZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/Unpack.v b/src/Specific/GF25519Reflective/Reified/Unpack.v index 027eedf39..a96f87d96 100644 --- a/src/Specific/GF25519Reflective/Reified/Unpack.v +++ b/src/Specific/GF25519Reflective/Reified/Unpack.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.GF25519Reflective.Common. +Require Import Crypto.Specific.GF25519Reflective.CommonUnOpWireToFE. Definition runpackZ_sig : rexpr_unop_WireToFE_sig unpack. Proof. reify_sig. Defined. Definition runpackW := Eval vm_compute in rword_of_Z runpackZ_sig. diff --git a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py index 76ac2c91b..404afc1ea 100755 --- a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py +++ b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py @@ -25,7 +25,7 @@ Definition r%(lname)sW_correct_and_bounded match proof_admitted with end match proof_admitted with end. """ % locals() with open(name.replace('_', '') + '.v', 'w') as f: - f.write(r"""Require Import Crypto.Specific.GF25519Reflective.Common. + f.write(r"""Require Import Crypto.Specific.GF25519Reflective.Common%(uopkind)s. Definition r%(lname)sZ_sig : rexpr_%(lopkind)s_sig %(lname)s. Proof. reify_sig. Defined. Definition r%(lname)sW := Eval vm_compute in rword_of_Z r%(lname)sZ_sig. diff --git a/src/Util/HList.v b/src/Util/HList.v index aacefe8f3..ec9dcdd7b 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -88,6 +88,18 @@ Proof. destruct n; [ constructor | apply hlist'_impl ]. Defined. +Local Arguments Tuple.map : simpl never. +Lemma hlist_map {n A B F} {f:A -> B} (xs:tuple A n) + : hlist F (Tuple.map f xs) = hlist (fun x => F (f x)) xs. +Proof. + destruct n as [|n]; [ reflexivity | ]. + induction n; [ reflexivity | ]. + specialize (IHn (fst xs)). + destruct xs; rewrite Tuple.map_S. + simpl @hlist in *; rewrite <- IHn. + reflexivity. +Qed. + Module Tuple. Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n) : hlist (fun x => f x = x) xs -> Tuple.map f xs = xs. diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 4d97c7857..79747ec2d 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -20,6 +20,42 @@ Definition tuple T n : Type := | S n' => tuple' T n' end. +(** right-associated tuples *) +Fixpoint rtuple' T n : Type := + match n with + | O => T + | S n' => (T * rtuple' T n')%type + end. + +Definition rtuple T n : Type := + match n with + | O => unit + | S n' => rtuple' T n' + end. + +Fixpoint rsnoc' T n {struct n} : forall (x : rtuple' T n) (y : T), rtuple' T (S n) + := match n return forall (x : rtuple' T n) (y : T), rtuple' T (S n) with + | O => fun x y => (x, y) + | S n' => fun x y => (fst x, @rsnoc' T n' (snd x) y) + end. +Global Arguments rsnoc' {T n} _ _. + +Fixpoint assoc_right' {n T} {struct n} + : tuple' T n -> rtuple' T n + := match n return tuple' T n -> rtuple' T n with + | 0 => fun x => x + | S n' => fun ts => let xs := @assoc_right' n' T (fst ts) in + let x := snd ts in + rsnoc' xs x + end. + +Definition assoc_right {n T} + : tuple T n -> rtuple T n + := match n with + | 0 => fun x => x + | S n' => @assoc_right' n' T + end. + Definition tl' {T n} : tuple' T (S n) -> tuple' T n := @fst _ _. Definition tl {T n} : tuple T (S n) -> tuple T n := match n with @@ -168,6 +204,11 @@ Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat} Definition map2 {n A B C} (f:A -> B -> C) (xs:tuple A n) (ys:tuple B n) : tuple C n := on_tuple2 (map2 f) (fun la lb pfa pfb => eq_trans (@map2_length _ _ _ _ la lb) (eq_trans (f_equal2 _ pfa pfb) (Min.min_idempotent _))) xs ys. +Lemma map2_S {n A B C} (f:A -> B -> C) (xs:tuple' A n) (ys:tuple' B n) (x:A) (y:B) + : map2 (n:=S (S n)) f (xs, x) (ys, y) = (map2 (n:=S n) f xs ys, f x y). +Proof. +Admitted. + Lemma map_map2 {n A B C D} (f:A -> B -> C) (g:C -> D) (xs:tuple A n) (ys:tuple B n) : map g (map2 f xs ys) = map2 (fun a b => g (f a b)) xs ys. Proof. @@ -193,6 +234,23 @@ Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n) Proof. Admitted. +Lemma map2_map {n A B C A' B'} (f:A -> B -> C) (g:A' -> A) (h:B' -> B) (xs:tuple A' n) (ys:tuple B' n) + : map2 f (map g xs) (map h ys) = map2 (fun a b => f (g a) (h b)) xs ys. +Proof. +Admitted. + +Lemma map2_map_fst {n A B C A'} (f:A -> B -> C) (g:A' -> A) (xs:tuple A' n) (ys:tuple B n) + : map2 f (map g xs) ys = map2 (fun a b => f (g a) b) xs ys. +Proof. + rewrite <- (map2_map f g (fun x => x)), map_id; reflexivity. +Qed. + +Lemma map2_map_snd {n A B C B'} (f:A -> B -> C) (g:B' -> B) (xs:tuple A n) (ys:tuple B' n) + : map2 f xs (map g ys) = map2 (fun a b => f a (g b)) xs ys. +Proof. + rewrite <- (map2_map f (fun x => x) g), map_id; reflexivity. +Qed. + Lemma map_map {n A B C} (g : B -> C) (f : A -> B) (xs:tuple A n) : map g (map f xs) = map (fun x => g (f x)) xs. Proof. diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 4c74fe9b4..f0e6ef335 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -1,5 +1,6 @@ Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Coq.ZArith.ZArith. +Require Import Coq.NArith.NArith. Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.Tactics. Require Import Bedrock.Word. @@ -51,6 +52,32 @@ Proof. auto. Qed. +Lemma Npow2_gt0 : forall x, (0 < Npow2 x)%N. +Proof. + intros; induction x. + + - simpl; apply N.lt_1_r; intuition. + + - replace (Npow2 (S x)) with (2 * (Npow2 x))%N by intuition. + apply (N.lt_0_mul 2 (Npow2 x)); left; split; apply N.neq_0_lt_0. + + + intuition; inversion H. + + + apply N.neq_0_lt_0 in IHx; intuition. +Qed. + +Lemma Npow2_N: forall n, Npow2 n = (2 ^ N.of_nat n)%N. +Proof. + induction n. + + - simpl; intuition. + + - rewrite Nat2N.inj_succ. + rewrite N.pow_succ_r; try apply N_ge_0. + rewrite <- IHn. + simpl; intuition. +Qed. + Lemma Npow2_Zlog2 : forall x n, (Z.log2 (Z.of_N x) < Z.of_nat n)%Z -> (x < Npow2 n)%N. @@ -243,16 +270,26 @@ Ltac wordsize_eq_tac := cbv beta delta [wordsize_eq] in *; omega*. Ltac gt84_abstract t := t. (* TODO: when we drop Coq 8.4, use [abstract] here *) Hint Extern 100 (wordsize_eq _ _) => gt84_abstract wordsize_eq_tac : typeclass_instances. -Program Fixpoint cast_word {n m} : forall {pf:wordsize_eq n m}, word n -> word m := - match n, m return wordsize_eq n m -> word n -> word m with - | O, O => fun _ _ => WO - | S n', S m' => fun _ w => WS (whd w) (@cast_word _ _ _ (wtl w)) - | _, _ => fun _ _ => ! +Fixpoint correct_wordsize_eq (x y : nat) : wordsize_eq x y -> x = y + := match x, y with + | O, O => fun _ => eq_refl + | S x', S y' => fun pf => f_equal S (correct_wordsize_eq x' y' (f_equal pred pf)) + | _, _ => fun x => x + end. + +Lemma correct_wordsize_eq_refl n pf : correct_wordsize_eq n n pf = eq_refl. +Proof. + induction n; [ reflexivity | simpl ]. + rewrite IHn; reflexivity. +Qed. + +Definition cast_word {n m} {pf:wordsize_eq n m} : word n -> word m := + match correct_wordsize_eq n m pf in _ = y return word n -> word y with + | eq_refl => fun w => w end. -Global Arguments cast_word {_ _ _} _. (* 8.4 does not pick up the forall braces *) Lemma cast_word_refl {n} pf (w:word n) : @cast_word n n pf w = w. -Proof. induction w; simpl; auto using f_equal. Qed. +Proof. unfold cast_word; rewrite correct_wordsize_eq_refl; reflexivity. Qed. Lemma wordToNat_cast_word {n} (w:word n) m pf : wordToNat (@cast_word n m pf w) = wordToNat w. @@ -721,4 +758,4 @@ Axiom winit : forall sz, word (sz+1) -> word sz. Arguments winit {_} _. Axiom combine_winit_wlast : forall {sz} a b (c:word (sz+1)), @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO). Axiom winit_combine : forall sz a b, @winit sz (combine a b) = a. -Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
\ No newline at end of file +Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 17e8d62bf..42e88e8c4 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -944,6 +944,7 @@ Module Z. rewrite Z.ones_succ by assumption. zero_bounds. Qed. + Hint Resolve ones_nonneg : zarith. Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. Proof. @@ -953,6 +954,7 @@ Module Z. apply Z.lt_succ_lt_pred. apply Z.pow_gt_1; omega. Qed. + Hint Resolve ones_pos_pos : zarith. Lemma pow2_mod_id_iff : forall a n, 0 <= n -> (Z.pow2_mod a n = a <-> 0 <= a < 2 ^ n). @@ -2128,7 +2130,7 @@ Module Z. Qed. Hint Resolve log2_ones_lt_nonneg : zarith. - Lemma log2_lt_pow2_alt a b : 0 < b -> a < 2^b <-> Z.log2 a < b. + Lemma log2_lt_pow2_alt a b : 0 < b -> (a < 2^b <-> Z.log2 a < b). Proof. destruct (Z_lt_le_dec 0 a); auto using Z.log2_lt_pow2; []. rewrite Z.log2_nonpos by omega. |