diff options
| author |  Robert Sloan <varomodt@google.com> | 2016-10-24 11:41:47 -0700 |
|---|---|---|
| committer | Robert Sloan <varomodt@google.com> | 2016-10-24 11:41:47 -0700 |
| commit | 6c29b39c2c0eafdd6f92e7b3d67c451b3c769af5 (patch) | |
| tree | 532ed133b3e9a2517aaedb95b7b0a910e25b9049 | |
| parent | b31a3355d3e134e346d77d2a3715a334d7633c01 (diff) | |
| parent | ea3bf2b136dd9f439f6c568f899c15aff2b8b6cb (diff) | |
Merge branch 'rsloan-phoas' of github.com:mit-plv/fiat-crypto into rsloan-phoas
| -rw-r--r-- | _CoqProject | 89 | ||||
| -rw-r--r-- | src/Assembly/Compile.v | 7 | ||||
| -rw-r--r-- | src/Assembly/Conversions.v | 6 | ||||
| -rw-r--r-- | src/Assembly/Evaluables.v | 12 | ||||
| -rw-r--r-- | src/Assembly/GF25519BoundedInstantiation.v | 34 | ||||
| -rw-r--r-- | src/Assembly/HL.v | 3 | ||||
| -rw-r--r-- | src/Assembly/LL.v | 9 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 13 | ||||
| -rw-r--r-- | src/Experiments/Ed25519.v | 347 | ||||
| -rw-r--r-- | src/Experiments/ExtrHaskellNats.v | 94 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 14 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemList.v | 36 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListProofs.v | 148 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 43 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 28 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 59 | ||||
| -rw-r--r-- | src/Specific/GF25519Bounded.v | 212 | ||||
| -rw-r--r-- | src/Specific/GF25519BoundedCommon.v | 81 | ||||
| -rw-r--r-- | src/Util/Bool.v | 10 | ||||
| -rw-r--r-- | src/Util/LetIn.v | 4 | ||||
| -rw-r--r-- | src/Util/WordUtil.v | 19 |
21 files changed, 899 insertions, 369 deletions
diff --git a/_CoqProject b/_CoqProject index 757d85fe7..17a326a12 100644 --- a/_CoqProject +++ b/_CoqProject @@ -3,27 +3,35 @@ Bedrock/Nomega.v Bedrock/Word.v src/Algebra.v +src/BaseSystem.v +src/BaseSystemProofs.v +src/EdDSARepChange.v +src/Testbit.v src/Assembly/Bounds.v src/Assembly/Compile.v src/Assembly/Conversions.v src/Assembly/Evaluables.v -src/Assembly/GF25519BoundedInstantiation.v src/Assembly/GF25519.v +src/Assembly/GF25519BoundedInstantiation.v src/Assembly/HL.v src/Assembly/LL.v src/Assembly/PhoasCommon.v src/Assembly/Pipeline.v +src/Assembly/Qhasm.v src/Assembly/QhasmCommon.v src/Assembly/QhasmEvalCommon.v src/Assembly/QhasmUtil.v -src/Assembly/Qhasm.v src/Assembly/State.v src/Assembly/StringConversion.v src/Assembly/WordizeUtil.v -src/BaseSystemProofs.v -src/BaseSystem.v -src/BoundedArithmetic/ArchitectureToZLikeProofs.v src/BoundedArithmetic/ArchitectureToZLike.v +src/BoundedArithmetic/ArchitectureToZLikeProofs.v +src/BoundedArithmetic/Eta.v +src/BoundedArithmetic/Interface.v +src/BoundedArithmetic/InterfaceProofs.v +src/BoundedArithmetic/StripCF.v +src/BoundedArithmetic/X86ToZLike.v +src/BoundedArithmetic/X86ToZLikeProofs.v src/BoundedArithmetic/Double/Core.v src/BoundedArithmetic/Double/Proofs/BitwiseOr.v src/BoundedArithmetic/Double/Proofs/Decode.v @@ -31,10 +39,10 @@ src/BoundedArithmetic/Double/Proofs/LoadImmediate.v src/BoundedArithmetic/Double/Proofs/Multiply.v src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v src/BoundedArithmetic/Double/Proofs/SelectConditional.v -src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v src/BoundedArithmetic/Double/Proofs/ShiftLeft.v -src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v +src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v src/BoundedArithmetic/Double/Proofs/ShiftRight.v +src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v src/BoundedArithmetic/Double/Proofs/SpreadLeftImmediate.v src/BoundedArithmetic/Double/Repeated/Core.v src/BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr.v @@ -45,42 +53,29 @@ src/BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub.v src/BoundedArithmetic/Double/Repeated/Proofs/SelectConditional.v src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v src/BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate.v -src/BoundedArithmetic/Eta.v -src/BoundedArithmetic/InterfaceProofs.v -src/BoundedArithmetic/Interface.v -src/BoundedArithmetic/StripCF.v -src/BoundedArithmetic/X86ToZLikeProofs.v -src/BoundedArithmetic/X86ToZLike.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/ExtendedCoordinates.v src/CompleteEdwardsCurve/Pre.v -src/EdDSARepChange.v src/Encoding/EncodingTheorems.v src/Encoding/ModularWordEncodingPre.v src/Encoding/ModularWordEncodingTheorems.v -src/Encoding/PointEncodingPre.v src/Encoding/PointEncoding.v +src/Encoding/PointEncodingPre.v src/Experiments/Ed25519.v +src/Experiments/ExtrHaskellNats.v src/Experiments/GenericFieldPow.v src/Experiments/MontgomeryCurve.v -src/ModularArithmetic/BarrettReduction/ZBounded.v -src/ModularArithmetic/BarrettReduction/ZGeneralized.v -src/ModularArithmetic/BarrettReduction/ZHandbook.v -src/ModularArithmetic/BarrettReduction/Z.v src/ModularArithmetic/Conversion.v -src/ModularArithmetic/ExtendedBaseVector.v src/ModularArithmetic/ExtPow2BaseMulProofs.v +src/ModularArithmetic/ExtendedBaseVector.v src/ModularArithmetic/ModularArithmeticTheorems.v -src/ModularArithmetic/ModularBaseSystemListProofs.v +src/ModularArithmetic/ModularBaseSystem.v src/ModularArithmetic/ModularBaseSystemList.v +src/ModularArithmetic/ModularBaseSystemListProofs.v src/ModularArithmetic/ModularBaseSystemOpt.v src/ModularArithmetic/ModularBaseSystemProofs.v -src/ModularArithmetic/ModularBaseSystem.v -src/ModularArithmetic/Montgomery/ZBounded.v -src/ModularArithmetic/Montgomery/ZProofs.v -src/ModularArithmetic/Montgomery/Z.v -src/ModularArithmetic/Pow2BaseProofs.v src/ModularArithmetic/Pow2Base.v +src/ModularArithmetic/Pow2BaseProofs.v src/ModularArithmetic/Pre.v src/ModularArithmetic/PrimeFieldTheorems.v src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -88,19 +83,32 @@ src/ModularArithmetic/PseudoMersenneBaseParams.v src/ModularArithmetic/Tutorial.v src/ModularArithmetic/ZBounded.v src/ModularArithmetic/ZBoundedZ.v +src/ModularArithmetic/BarrettReduction/Z.v +src/ModularArithmetic/BarrettReduction/ZBounded.v +src/ModularArithmetic/BarrettReduction/ZGeneralized.v +src/ModularArithmetic/BarrettReduction/ZHandbook.v +src/ModularArithmetic/Montgomery/Z.v +src/ModularArithmetic/Montgomery/ZBounded.v +src/ModularArithmetic/Montgomery/ZProofs.v src/Reflection/CommonSubexpressionElimination.v src/Reflection/Conversion.v src/Reflection/CountLets.v src/Reflection/FilterLive.v -src/Reflection/InlineInterp.v src/Reflection/Inline.v +src/Reflection/InlineInterp.v src/Reflection/InlineWf.v src/Reflection/InputSyntax.v src/Reflection/InterpProofs.v -src/Reflection/LinearizeInterp.v src/Reflection/Linearize.v +src/Reflection/LinearizeInterp.v src/Reflection/LinearizeWf.v src/Reflection/MapInterp.v +src/Reflection/Reify.v +src/Reflection/Syntax.v +src/Reflection/TestCase.v +src/Reflection/WfProofs.v +src/Reflection/WfReflective.v +src/Reflection/WfRel.v src/Reflection/Named/Compile.v src/Reflection/Named/ContextOn.v src/Reflection/Named/DeadCodeElimination.v @@ -108,31 +116,24 @@ src/Reflection/Named/EstablishLiveness.v src/Reflection/Named/NameUtil.v src/Reflection/Named/RegisterAssign.v src/Reflection/Named/Syntax.v -src/Reflection/Reify.v -src/Reflection/Syntax.v -src/Reflection/TestCase.v -src/Reflection/WfProofs.v -src/Reflection/WfReflective.v -src/Reflection/WfRel.v src/Spec/CompleteEdwardsCurve.v src/Spec/Ed25519.v src/Spec/EdDSA.v src/Spec/Encoding.v -src/Specific/FancyMachine256/Barrett.v -src/Specific/FancyMachine256/Core.v -src/Specific/FancyMachine256/Montgomery.v -src/Specific/GF1305.v -src/Specific/GF25519BoundedCommon.v -src/Specific/GF25519Bounded.v -src/Specific/GF25519.v -src/Specific/SC25519.v src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v src/Spec/MxDH.v src/Spec/WeierstrassCurve.v -src/Tactics/Algebra_syntax/Nsatz.v +src/Specific/GF1305.v +src/Specific/GF25519.v +src/Specific/GF25519Bounded.v +src/Specific/GF25519BoundedCommon.v +src/Specific/SC25519.v +src/Specific/FancyMachine256/Barrett.v +src/Specific/FancyMachine256/Core.v +src/Specific/FancyMachine256/Montgomery.v src/Tactics/VerdiTactics.v -src/Testbit.v +src/Tactics/Algebra_syntax/Nsatz.v src/Test/Curve25519SpecTestVectors.v src/Util/AdditionChainExponentiation.v src/Util/AutoRewrite.v diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v index 91eb37a16..e072342a5 100644 --- a/src/Assembly/Compile.v +++ b/src/Assembly/Compile.v @@ -9,6 +9,8 @@ Require Import Crypto.Assembly.QhasmEvalCommon. Require Import Crypto.Assembly.QhasmCommon. Require Import Crypto.Assembly.Qhasm. +Local Arguments LetIn.Let_In _ _ _ _ / . + Module CompileHL. Section Compilation. Context {T: Type}. @@ -281,11 +283,12 @@ Module CompileLL. (fun rt var op x y out => Some out) (fun t' a => Some (vars a)). - Fixpoint fillInputs {t inputs} (prog: NAry inputs Z (WExpr t)) {struct inputs}: WExpr t := + Fixpoint fillInputs t inputs (prog: NAry inputs Z (WExpr t)) {struct inputs}: WExpr t := match inputs as inputs' return NAry inputs' Z (WExpr t) -> NAry O Z (WExpr t) with | O => fun p => p - | S inputs'' => fun p => fillInputs (p (Z.of_nat inputs)) + | S inputs'' => fun p => @fillInputs _ _ (p (Z.of_nat inputs)) end prog. + Global Arguments fillInputs {t inputs} _. Definition compile {t inputs} (p: NAry inputs Z (WExpr t)): option (Program * list nat) := let p' := fillInputs p in diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v index e4ea4b5d1..c24cf618f 100644 --- a/src/Assembly/Conversions.v +++ b/src/Assembly/Conversions.v @@ -18,6 +18,8 @@ Require Import Coq.NArith.Nnat Coq.NArith.Ndigits. Require Import Coq.Bool.Sumbool. +Local Arguments LetIn.Let_In _ _ _ _ / . + Definition typeMap {A B t} (f: A -> B) (x: @interp_type A t): @interp_type B t. Proof. induction t; [refine (f x)|]. @@ -282,7 +284,7 @@ Module LLConversions. Lemma roundTrip_0 : @toT Correctness.B BE (@fromT Z ZE 0%Z) <> None. Proof. intros; unfold toT, fromT, BE, ZE, BoundedEvaluable, ZEvaluable, bwFromRWV; - kill_dec; simpl; kill_dec; simpl; try abstract (intro Z; inversion Z); + break_match; simpl; try break_match; simpl; try abstract (intro Z; inversion Z); pose proof (Npow2_gt0 n); simpl in *; nomega. Qed. @@ -361,7 +363,7 @@ Module LLConversions. kill_dec; simpl in *; kill_dec; first [reflexivity|nomega]. *) + unfold bcheck, getBounds in *. - replace (interp_binop op _ _) + replace (interp_binop op (interp_arg x) (interp_arg y)) with (varBoundedToZ (n := n) (opBounded op (interp_arg' boundVarInterp (convertArg _ x)) (interp_arg' boundVarInterp (convertArg _ y)))). diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v index 8d68ac696..c4aa56175 100644 --- a/src/Assembly/Evaluables.v +++ b/src/Assembly/Evaluables.v @@ -13,7 +13,7 @@ Section BaseTypes. Record RangeWithValue := rwv { rwv_low: N; rwv_value: N; - rwv_high: N; + rwv_high: N }. Record BoundedWord {n} := bounded { @@ -23,7 +23,7 @@ Section BaseTypes. ge_low: (bw_low <= wordToN bw_value)%N; le_high: (wordToN bw_value <= bw_high)%N; - high_bound: (bw_high < Npow2 n)%N; + high_bound: (bw_high < Npow2 n)%N }. End BaseTypes. @@ -652,11 +652,11 @@ Section BoundedWord. eand := fun x y => omap x (fun X => omap y (fun Y => bapp range_and_valid X Y)); eltb := fun x y => - orElse false (omap x (fun X => omap y (fun Y => + orElse false (omap x (fun X => omap y (fun Y => Some (N.ltb (wordToN (bw_value X)) (wordToN (bw_value Y)))))); eeqb := fun x y => - orElse false (omap x (fun X => omap y (fun Y => + orElse false (omap x (fun X => omap y (fun Y => Some (N.eqb (wordToN (bw_value X)) (wordToN (bw_value Y)))))) }. End BoundedWord. @@ -729,7 +729,7 @@ Section RangeWithValue. | (Some (rwv xlow xv xhigh), Some (rwv ylow yv yhigh)) => N.ltb xv yv - | _ => false + | _ => false end; eeqb := fun x y => @@ -738,6 +738,6 @@ Section RangeWithValue. andb (andb (N.eqb xlow ylow) (N.eqb xhigh yhigh)) (N.eqb xv yv) | _ => false - end; + end }. End RangeWithValue. diff --git a/src/Assembly/GF25519BoundedInstantiation.v b/src/Assembly/GF25519BoundedInstantiation.v index 83b0dd4bf..07c074f5e 100644 --- a/src/Assembly/GF25519BoundedInstantiation.v +++ b/src/Assembly/GF25519BoundedInstantiation.v @@ -7,6 +7,7 @@ Require Import Crypto.Assembly.GF25519. Require Import Crypto.Specific.GF25519. Require Import Crypto.Specific.GF25519BoundedCommon. Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Tuple. (* Totally fine to edit these definitions; DO NOT change the type signatures at all *) @@ -43,6 +44,39 @@ Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommon.fe25519W -> := interp_uexpr'. Axiom rfreeze : ExprUnOp. +Declare Reduction asm_interp + := cbv [id + interp_bexpr interp_uexpr interp_bexpr' interp_uexpr' + radd rsub rmul ropp (*rfreeze*) + GF25519.GF25519.Add.wordProg GF25519.GF25519.AddExpr.bits GF25519.GF25519.Add.llProg GF25519.GF25519.AddExpr.hlProg GF25519.GF25519.AddExpr.inputs + GF25519.GF25519.Sub.wordProg GF25519.GF25519.SubExpr.bits GF25519.GF25519.Sub.llProg GF25519.GF25519.SubExpr.hlProg GF25519.GF25519.SubExpr.inputs + GF25519.GF25519.Mul.wordProg GF25519.GF25519.MulExpr.bits GF25519.GF25519.Mul.llProg GF25519.GF25519.MulExpr.hlProg GF25519.GF25519.MulExpr.inputs + GF25519.GF25519.Opp.wordProg GF25519.GF25519.OppExpr.bits GF25519.GF25519.Opp.llProg GF25519.GF25519.OppExpr.hlProg GF25519.GF25519.OppExpr.inputs + (*GF25519.GF25519.Freeze.wordProg GF25519.GF25519.FreezeExpr.bits GF25519.GF25519.Freeze.llProg GF25519.GF25519.FreezeExpr.hlProg GF25519.GF25519.FreezeExpr.inputs *) + GF25519.GF25519.bits GF25519.GF25519.FE + QhasmCommon.liftN QhasmCommon.NArgMap Compile.CompileHL.compile LL.LL.under_lets LL.LL.interp LL.LL.interp_arg LL.LL.match_arg_Prod Conversions.LLConversions.convertZToWord Conversions.LLConversions.convertExpr Conversions.LLConversions.convertArg Conversions.LLConversions.convertVar PhoasCommon.type_rect PhoasCommon.type_rec PhoasCommon.type_ind PhoasCommon.interp_binop LL.LL.uninterp_arg + Evaluables.ezero Evaluables.toT Evaluables.fromT Evaluables.eadd Evaluables.esub Evaluables.emul Evaluables.eshiftr Evaluables.eand Evaluables.eltb Evaluables.eeqb + Evaluables.WordEvaluable Evaluables.ZEvaluable]. + +Definition interp_radd : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W + := Eval asm_interp in interp_bexpr radd. +Print interp_radd. +Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl. +Definition interp_rsub : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W + := Eval asm_interp in interp_bexpr rsub. +(*Print interp_rsub.*) +Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl. +Definition interp_rmul : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W + := Eval asm_interp in interp_bexpr rmul. +(*Print interp_rmul.*) +Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl. +Definition interp_ropp : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W + := Eval asm_interp in interp_uexpr ropp. +Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. +Definition interp_rfreeze : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W + := Eval asm_interp in interp_uexpr rfreeze. +Definition interp_rfreeze_correct : interp_rfreeze = interp_uexpr rfreeze := eq_refl. + Local Notation binop_correct_and_bounded rop op := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing). Local Notation unop_correct_and_bounded rop op diff --git a/src/Assembly/HL.v b/src/Assembly/HL.v index 14ca2edca..2107b7f0a 100644 --- a/src/Assembly/HL.v +++ b/src/Assembly/HL.v @@ -1,5 +1,6 @@ Require Import Crypto.Assembly.PhoasCommon. Require Import Coq.setoid_ring.InitialRing. +Require Import Crypto.Util.LetIn. Module HL. Section Language. @@ -27,7 +28,7 @@ Module HL. | Const n => n | Var _ n => n | Binop _ _ _ op e1 e2 => interp_binop op (interp e1) (interp e2) - | Let _ ex _ eC => let x := interp ex in interp (eC x) + | Let _ ex _ eC => dlet x := interp ex in interp (eC x) | Pair _ e1 _ e2 => (interp e1, interp e2) | MatchPair _ _ ep _ eC => let (v1, v2) := interp ep in interp (eC v1 v2) end. diff --git a/src/Assembly/LL.v b/src/Assembly/LL.v index fd0a92f96..e0588214c 100644 --- a/src/Assembly/LL.v +++ b/src/Assembly/LL.v @@ -1,4 +1,7 @@ Require Import Crypto.Assembly.PhoasCommon. +Require Import Crypto.Util.LetIn. + +Local Arguments Let_In / _ _ _ _. Module LL. Section Language. @@ -61,7 +64,7 @@ Module LL. match x' with | (x0, x1) => Pair (uninterp_arg_as_var x0) (uninterp_arg_as_var x1) end - | TT => Var + | TT => Var end x. Fixpoint interp' {V t} (f: V -> T) (e:expr t) : interp_type t := @@ -74,7 +77,7 @@ Module LL. Fixpoint interp {t} (e:expr t) : interp_type t := match e with | LetBinop _ _ _ op a b _ eC => - let x := interp_binop op (interp_arg a) (interp_arg b) in interp (eC (uninterp_arg x)) + dlet x := interp_binop op (interp_arg a) (interp_arg b) in interp (eC (uninterp_arg x)) | Return _ a => interp_arg a end. @@ -153,7 +156,7 @@ Module LL. induction t as [|i0 v0 i1 v1]; simpl; intros; try reflexivity. break_match; subst; simpl. unfold interp_arg in *. - cbn; rewrite v0, v1; reflexivity. + simpl; rewrite v0, v1; reflexivity. Qed. Lemma interp_under_lets {T} {_: Evaluable T} {t: type} {tC: type} diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 3e447cb04..5a6f7588a 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -47,6 +47,7 @@ Module Extended. | _ => solve [eauto] | _ => solve [intuition eauto] | _ => solve [etransitivity; eauto] + | |- _ => rewrite <-!(field_div_definition(field:=field)) in * | |- _*_ <> 0 => apply Ring.zero_product_iff_zero_factor | [H: _ |- _ ] => solve [intro; apply H; super_nsatz] | |- Feq _ _ => super_nsatz @@ -62,7 +63,7 @@ Module Extended. (let (x,y) := E.coordinates P in (x, y, 1, x*y)) _. Program Definition to_twisted (P:point) : Epoint := exist _ - (let '(X,Y,Z,T) := coordinates P in ((X/Z), (Y/Z))) _. + (let '(X,Y,Z,T) := coordinates P in let iZ := Finv Z in ((X*iZ), (Y*iZ))) _. Definition eq (P Q:point) := E.eq (to_twisted P) (to_twisted Q). Global Instance DecidableRel_eq : Decidable.DecidableRel eq := _. @@ -128,7 +129,12 @@ Module Extended. pose proof (add_coordinates_correct P Q) as Hrep. destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ]. autounfold with bash in *; simpl in *. - destruct Hrep as [HA HB]. rewrite <-!HA, <-!HB; clear HA HB. + destruct Hrep as [HA HB]. + pose proof (field_div_definition(field:=field)) as Hdiv; symmetry in Hdiv; + (rewrite_strat bottomup Hdiv); + (rewrite_strat bottomup Hdiv in HA); + (rewrite_strat bottomup Hdiv in HB). + rewrite <-!HA, <-!HB; clear HA HB. split; reflexivity. Qed. @@ -255,7 +261,8 @@ Module Extended. | [p: point |- _ ] => destruct p as [ [ [ [ ] ? ] ? ] [ ? [ ? ? ] ] ] | |- context[point_phi] => setoid_rewrite point_phi_correct | |- _ => progress cbv [fst snd coordinates proj1_sig eq to_twisted E.eq E.coordinates fieldwise fieldwise' add add_coordinates ref_phi] in * - | |- Keq ?x ?x => reflexivity + | |- _ => rewrite <-!(field_div_definition(field:=fieldF)) in * + | |- _ => rewrite <-!(field_div_definition(field:=fieldK)) in * | |- Keq ?x ?y => rewrite_strat bottomup hints field_homomorphism | [ H : Feq _ _ |- Keq (phi _) (phi _)] => solve [f_equiv; intuition] end. diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 39de39262..0961aa77d 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -61,7 +61,7 @@ Definition coord_to_extended (xy : GF25519.fe25519 * GF25519.fe25519) pf := (exist Pre.onCurve xy pf). Definition extended_to_coord (P : Erep) : (GF25519.fe25519 * GF25519.fe25519) := - CompleteEdwardsCurve.E.coordinates (ExtendedCoordinates.Extended.to_twisted P). + CompleteEdwardsCurve.E.coordinates (ExtendedCoordinates.Extended.to_twisted P (field:=GF25519.field25519)). Lemma encode_eq_iff : forall x y : ModularArithmetic.F.F GF25519.modulus, ModularBaseSystem.eq @@ -103,7 +103,7 @@ Definition feEnc (x : GF25519.fe25519) : Word.word 255 := (Word.combine (ZNWord 32 x4) (Word.combine (ZNWord 32 x5) (Word.combine (ZNWord 32 x6) (ZNWord 31 x7))))))). - +Check GF25519.ge_modulus. Definition feDec (w : Word.word 255) : option GF25519.fe25519 := let w0 := Word.split1 32 _ w in let a0 := Word.split2 32 _ w in @@ -120,7 +120,7 @@ Definition feDec (w : Word.word 255) : option GF25519.fe25519 := let w6 := Word.split1 32 _ a5 in let w7 := Word.split2 32 _ a5 in let result := (GF25519.unpack (WordNZ w0, WordNZ w1, WordNZ w2, WordNZ w3, WordNZ w4, WordNZ w5, WordNZ w6, WordNZ w7)) in - if GF25519.ge_modulus result + if Z.eqb (GF25519.ge_modulus result) 1 then None else (Some result). Let ERepEnc := @@ -129,7 +129,7 @@ Let ERepEnc := (Kenc := feEnc) (Kpoint := Erep) (Kpoint_to_coord := fun P => CompleteEdwardsCurve.E.coordinates - (ExtendedCoordinates.Extended.to_twisted P)) + (ExtendedCoordinates.Extended.to_twisted P (field:=GF25519.field25519))) ). Let SRep := SC25519.SRep. @@ -175,7 +175,7 @@ Let SRepERepMul : SRep -> Erep -> Erep := . Lemma SRepERepMul_correct n P : - ExtendedCoordinates.Extended.eq + ExtendedCoordinates.Extended.eq (field:=GF25519.field25519) (EToRep (CompleteEdwardsCurve.E.mul n P)) (SRepERepMul (S2Rep (ModularArithmetic.F.of_nat l n)) (EToRep P)). Proof. @@ -225,7 +225,7 @@ Proof. Qed. Lemma ext_eq_correct : forall p q : Erep, - ExtendedCoordinates.Extended.eq p q <-> + ExtendedCoordinates.Extended.eq (field:=GF25519.field25519) p q <-> Tuple.fieldwise (n := 2) ModularBaseSystem.eq (extended_to_coord p) (extended_to_coord q). Proof. cbv [extended_to_coord]; intros. @@ -243,10 +243,10 @@ Let SRepEnc : SRep -> Word.word b := (fun x => Word.NToWord _ (Z.to_N x)). Axiom SRepERepMul_correct: forall (n : nat) (P : E), - ExtendedCoordinates.Extended.eq (EToRep (CompleteEdwardsCurve.E.mul n P)) + ExtendedCoordinates.Extended.eq (field:=GF25519.field25519) (EToRep (CompleteEdwardsCurve.E.mul n P)) (SRepERepMul (S2Rep (ModularArithmetic.F.of_nat l n)) (EToRep P)). -Axiom Proper_SRepERepMul : Proper (SC25519.SRepEq ==> ExtendedCoordinates.Extended.eq ==> ExtendedCoordinates.Extended.eq) SRepERepMul. +Axiom Proper_SRepERepMul : Proper (SC25519.SRepEq ==> ExtendedCoordinates.Extended.eq (field:=GF25519.field25519) ==> ExtendedCoordinates.Extended.eq (field:=GF25519.field25519)) SRepERepMul. Axiom SRepEnc_correct : forall x : ModularArithmetic.F.F l, Senc x = SRepEnc (S2Rep x). @@ -277,23 +277,28 @@ Let ERepB : Erep. exists rB. exact onCurve_ERepB. Defined. -Let ERepB_correct : ExtendedCoordinates.Extended.eq ERepB (EToRep B). vm_decide_no_check. Qed. - -Axiom ERep_group : - @Algebra.group Erep - (@ExtendedCoordinates.Extended.eq GF25519.fe25519 - (@ModularBaseSystem.eq GF25519.modulus GF25519.params25519) GF25519.zero_ GF25519.one_ GF25519.add - GF25519.mul (@ModularBaseSystem.div GF25519.modulus GF25519.params25519) a d) ErepAdd - (@ExtendedCoordinates.Extended.zero GF25519.fe25519 - (@ModularBaseSystem.eq GF25519.modulus GF25519.params25519) GF25519.zero_ GF25519.one_ - GF25519.opp GF25519.add GF25519.sub GF25519.mul GF25519.inv - (@ModularBaseSystem.div GF25519.modulus GF25519.params25519) a d GF25519.field25519 - twedprm_ERep _) - (@ExtendedCoordinates.Extended.opp GF25519.fe25519 - (@ModularBaseSystem.eq GF25519.modulus GF25519.params25519) GF25519.zero_ GF25519.one_ - GF25519.opp GF25519.add GF25519.sub GF25519.mul GF25519.inv - (@ModularBaseSystem.div GF25519.modulus GF25519.params25519) a d GF25519.field25519 - twedprm_ERep _). +Let ERepB_correct : ExtendedCoordinates.Extended.eq (field:=GF25519.field25519) ERepB (EToRep B). vm_decide_no_check. Qed. + +Axiom ERepGroup : + @Algebra.group Erep + (@ExtendedCoordinates.Extended.eq GF25519.fe25519 + (@ModularBaseSystem.eq GF25519.modulus GF25519.params25519) GF25519.zero_ GF25519.one_ GF25519.opp + GF25519.add GF25519.sub GF25519.mul GF25519.inv + (@ModularBaseSystem.div GF25519.modulus GF25519.params25519) a d GF25519.field25519 + (fun x y : GF25519.fe25519 => + @ModularArithmeticTheorems.F.eq_dec GF25519.modulus + (@ModularBaseSystem.decode GF25519.modulus GF25519.params25519 x) + (@ModularBaseSystem.decode GF25519.modulus GF25519.params25519 y))) ErepAdd + (@ExtendedCoordinates.Extended.zero GF25519.fe25519 + (@ModularBaseSystem.eq GF25519.modulus GF25519.params25519) GF25519.zero_ GF25519.one_ + _ GF25519.add _ GF25519.mul _ + (@ModularBaseSystem.div GF25519.modulus GF25519.params25519) a d GF25519.field25519 + twedprm_ERep _) + (@ExtendedCoordinates.Extended.opp GF25519.fe25519 + (@ModularBaseSystem.eq GF25519.modulus GF25519.params25519) GF25519.zero_ GF25519.one_ + _ GF25519.add _ GF25519.mul _ + (@ModularBaseSystem.div GF25519.modulus GF25519.params25519) a d GF25519.field25519 + twedprm_ERep _). Let sign := @EdDSARepChange.sign E (@CompleteEdwardsCurveTheorems.E.eq Fq (@eq Fq) (@ModularArithmetic.F.one q) @@ -342,7 +347,7 @@ Let sign_correct : forall pk sk {mlen} (msg:Word.word mlen), sign pk sk _ msg = (* ErepAdd := *) ErepAdd (* ErepId := *) ExtendedCoordinates.Extended.zero (* ErepOpp := *) ExtendedCoordinates.Extended.opp - (* Agroup := *) ERep_group + (* Agroup := *) ERepGroup (* EToRep := *) EToRep (* ERepEnc := *) ERepEnc (* ERepEnc_correct := *) ERepEnc_correct @@ -512,10 +517,13 @@ Extract Inlined Constant eq_rec_r => "". Extract Inductive comparison => "Prelude.Ordering" ["Prelude.EQ" "Prelude.LT" "Prelude.GT"]. -(** Bool *) +(** Bool, sumbool, Decidable *) Extract Inductive bool => "Prelude.Bool" ["Prelude.True" "Prelude.False"]. Extract Inductive sumbool => "Prelude.Bool" ["Prelude.True" "Prelude.False"]. +Extract Inductive Bool.reflect => "Prelude.Bool" ["Prelude.True" "Prelude.False"]. +Extract Inlined Constant Bool.iff_reflect => "". +Extraction Inline Crypto.Util.Decidable.Decidable Crypto.Util.Decidable.dec. (* Extract Inlined Constant Equality.bool_beq => *) (* "((Prelude.==) :: Prelude.Bool -> Prelude.Bool -> Prelude.Bool)". *) @@ -529,6 +537,11 @@ Extract Inlined Constant orb => "(Prelude.||)". Extract Inlined Constant andb => "(Prelude.&&)". Extract Inlined Constant xorb => "Data.Bits.xor". +(** Comparisons *) + +Extract Inductive comparison => "Prelude.Ordering" [ "Prelude.EQ" "Prelude.LT" "Prelude.GT" ]. +Extract Inductive CompareSpecT => "Prelude.Ordering" [ "Prelude.EQ" "Prelude.LT" "Prelude.GT" ]. + (** Maybe *) Extract Inductive option => "Prelude.Maybe" ["Prelude.Just" "Prelude.Nothing"]. @@ -567,53 +580,103 @@ Extract Inductive unit => "()" ["()"]. (** nat *) -Extract Inlined Constant Nat.add => "(Prelude.+)". -Extract Inlined Constant Nat.mul => "(Prelude.*)". -Extract Inlined Constant Nat.max => "Prelude.max". -Extract Inlined Constant Nat.min => "Prelude.min". -Extract Inlined Constant Init.Nat.add => "(Prelude.+)". -Extract Inlined Constant Init.Nat.mul => "(Prelude.*)". -Extract Inlined Constant Init.Nat.max => "Prelude.max". -Extract Inlined Constant Init.Nat.min => "Prelude.min". -Extract Inlined Constant PeanoNat.Nat.add => "(Prelude.+)". -Extract Inlined Constant PeanoNat.Nat.mul => "(Prelude.*)". -Extract Inlined Constant PeanoNat.Nat.max => "Prelude.max". -Extract Inlined Constant PeanoNat.Nat.min => "Prelude.min". -Extract Inlined Constant Compare_dec.lt_dec => "(Prelude.<)". -Extract Inlined Constant Compare_dec.leb => "(Prelude.<=)". -Extract Inlined Constant Compare_dec.le_lt_dec => "(Prelude.<=)". -Extract Inlined Constant EqNat.beq_nat => "(Prelude.==)". -Extract Inlined Constant EqNat.eq_nat_decide => "(Prelude.==)". -Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)". - -Extract Constant Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))". -Extract Constant Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))". -Extract Constant Init.Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))". -Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))". - -Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". -Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". -Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". -Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". - -Extract Inductive nat => "Prelude.Integer" [ "0" "Prelude.succ" ] - "(\fO fS n -> {- match_on_nat -} if n Prelude.== 0 then fO () else fS (n Prelude.- 1))". +Require Import Crypto.Experiments.ExtrHaskellNats. + +(** positive *) +Require Import BinPos. + +Extract Inductive positive => "Prelude.Integer" [ + "(\x -> 2 Prelude.* x Prelude.+ 1)" + "(\x -> 2 Prelude.* x)" + "1" ] + "(\fI fO fH n -> {- match_on_positive -} + if n Prelude.== 1 then fH () else + if Prelude.odd n + then fI (n `Prelude.div` 2) + else fO (n `Prelude.div` 2))". + +Extract Inlined Constant Pos.succ => "(1 Prelude.+)". +Extract Inlined Constant Pos.add => "(Prelude.+)". +Extract Inlined Constant Pos.mul => "(Prelude.*)". +Extract Inlined Constant Pos.pow => "(Prelude.^)". +Extract Inlined Constant Pos.max => "Prelude.max". +Extract Inlined Constant Pos.min => "Prelude.min". +Extract Inlined Constant Pos.gcd => "Prelude.gcd". +Extract Inlined Constant Pos.land => "(Data.Bits..&.)". +Extract Inlined Constant Pos.lor => "(Data.Bits..|.)". +Extract Inlined Constant Pos.compare => "Prelude.compare". +Extract Inlined Constant Pos.ltb => "(Prelude.<)". +Extract Inlined Constant Pos.leb => "(Prelude.<=)". +Extract Inlined Constant Pos.eq_dec => "(Prelude.==)". +Extract Inlined Constant Pos.eqb => "(Prelude.==)". + +(* XXX: unsound -- overflow in fromIntegral *) +Extract Constant Pos.shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))". +Extract Constant Pos.shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))". +Extract Constant Pos.testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))". + +Extract Constant Pos.pred => "(\n -> Prelude.max 1 (Prelude.pred n))". +Extract Constant Pos.sub => "(\n m -> Prelude.max 1 (n Prelude.- m))". + +(** N *) + +Extract Inlined Constant N.succ => "(1 Prelude.+)". +Extract Inlined Constant N.add => "(Prelude.+)". +Extract Inlined Constant N.mul => "(Prelude.*)". +Extract Inlined Constant N.pow => "(Prelude.^)". +Extract Inlined Constant N.max => "Prelude.max". +Extract Inlined Constant N.min => "Prelude.min". +Extract Inlined Constant N.gcd => "Prelude.gcd". +Extract Inlined Constant N.lcm => "Prelude.lcm". +Extract Inlined Constant N.land => "(Data.Bits..&.)". +Extract Inlined Constant N.lor => "(Data.Bits..|.)". +Extract Inlined Constant N.lxor => "Data.Bits.xor". +Extract Inlined Constant N.compare => "Prelude.compare". +Extract Inlined Constant N.eq_dec => "(Prelude.==)". +Extract Inlined Constant N.ltb => "(Prelude.<)". +Extract Inlined Constant N.leb => "(Prelude.<=)". +Extract Inlined Constant N.eq_dec => "(Prelude.==)". +Extract Inlined Constant N.odd => "Prelude.odd". +Extract Inlined Constant N.even => "Prelude.even". + +(* XXX: unsound -- overflow in fromIntegral *) +Extract Constant N.shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))". +Extract Constant N.shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))". +Extract Constant N.testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))". + +Extract Constant N.pred => "(\n -> Prelude.max 0 (Prelude.pred n))". +Extract Constant N.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))". +Extract Constant N.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". +Extract Constant N.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". + +Extract Inductive N => "Prelude.Integer" [ "0" "(\x -> x)" ] + "(\fO fS n -> {- match_on_N -} if n Prelude.== 0 then fO () else fS (n Prelude.- 1))". (** Z *) +Require Import ZArith.BinInt. -Require Import ZArith. -Require Import EqNat. +Extract Inductive Z => "Prelude.Integer" [ "0" "(\x -> x)" "Prelude.negate" ] + "(\fO fP fN n -> {- match_on_Z -} + if n Prelude.== 0 then fO () else + if n Prelude.> 0 then fP n else + fN (Prelude.negate n))". +Extract Inlined Constant Z.succ => "(1 Prelude.+)". Extract Inlined Constant Z.add => "(Prelude.+)". Extract Inlined Constant Z.sub => "(Prelude.-)". +Extract Inlined Constant Z.opp => "Prelude.negate". Extract Inlined Constant Z.mul => "(Prelude.*)". +Extract Inlined Constant Z.pow => "(Prelude.^)". +Extract Inlined Constant Z.pow_pos => "(Prelude.^)". Extract Inlined Constant Z.max => "Prelude.max". Extract Inlined Constant Z.min => "Prelude.min". +Extract Inlined Constant Z.lcm => "Prelude.lcm". +Extract Inlined Constant Z.land => "(Data.Bits..&.)". +Extract Inlined Constant Z.pred => "Prelude.pred". Extract Inlined Constant Z.land => "(Data.Bits..&.)". Extract Inlined Constant Z.lor => "(Data.Bits..|.)". -Extract Inlined Constant Z.shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))". -Extract Inlined Constant Z.shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))". -Extract Inlined Constant Z.testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))". +Extract Inlined Constant Z.lxor => "Data.Bits.xor". +Extract Inlined Constant Z.compare => "Prelude.compare". Extract Inlined Constant Z.eq_dec => "(Prelude.==)". Extract Inlined Constant Z_ge_lt_dec => "(Prelude.>=)". Extract Inlined Constant Z_gt_le_dec => "(Prelude.>)". @@ -621,59 +684,127 @@ Extract Inlined Constant Z.ltb => "(Prelude.<)". Extract Inlined Constant Z.leb => "(Prelude.<=)". Extract Inlined Constant Z.gtb => "(Prelude.>)". Extract Inlined Constant Z.geb => "(Prelude.>=)". +Extract Inlined Constant Z.odd => "Prelude.odd". +Extract Inlined Constant Z.even => "Prelude.even". + +(* XXX: unsound -- overflow in fromIntegral *) +Extract Constant Z.shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))". +Extract Constant Z.shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))". +Extract Constant Z.testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))". Extract Constant Z.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". Extract Constant Z.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". -Extract Inlined Constant BinIntDef.Z.compare => "Prelude.compare". -Extract Inductive comparison => "Prelude.Ordering" [ "Prelude.EQ" "Prelude.LT" "Prelude.GT" ]. -Extract Inductive CompareSpecT => "Prelude.Ordering" [ "Prelude.EQ" "Prelude.LT" "Prelude.GT" ]. - -Extract Inductive positive => "Prelude.Integer" [ - "(\x -> 2 Prelude.* x Prelude.+ 1)" - "(\x -> 2 Prelude.* x)" - "1" ] - "(\fI fO fH n -> {- match_on_positive -} - if n Prelude.== 1 then fH () else - if Prelude.odd n - then fI (n `Prelude.div` 2) - else fO (n `Prelude.div` 2))". - -Extract Inductive Z => "Prelude.Integer" [ "0" "(\x -> x)" "Prelude.negate" ] - "(\fO fP fN n -> {- match_on_Z -} - if n Prelude.== 0 then fO () else - if n Prelude.> 0 then fP n else - fN (Prelude.negate n))". +(** Conversions *) + +Extract Inlined Constant Z.of_N => "". +Extract Inlined Constant Z.to_N => "". +Extract Inlined Constant N.to_nat => "". +Extract Inlined Constant N.of_nat => "". +Extract Inlined Constant Z.to_nat => "". +Extract Inlined Constant Z.of_nat => "". +Extract Inlined Constant Z.abs_N => "Prelude.abs". +Extract Inlined Constant Z.abs_nat => "Prelude.abs". +Extract Inlined Constant Pos.pred_N => "Prelude.pred". +Extract Inlined Constant Pos.lxor => "Data.Bits.xor". + +(** Word *) +(* do not annotate every bit of a word with the number of bits after it *) +Extraction Implicit Word.WS [ 2 ]. +Extraction Implicit Word.whd [ 1 ]. +Extraction Implicit Word.wtl [ 1 ]. +Extraction Implicit Word.bitwp [ 2 ]. +Extraction Implicit Word.wand [ 1 ]. +Extraction Implicit Word.wor [ 1 ]. +Extraction Implicit Word.wxor [ 1 ]. +Extraction Implicit Word.wordToN [ 1 ]. +Extraction Implicit Word.wordToNat [ 1 ]. +Extraction Implicit Word.combine [ 1 3 ]. +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 => "". (** Let_In *) Extraction Inline LetIn.Let_In. + +(* inlining, primarily to reduce polymorphism *) +Extraction Inline dec_eq_Z dec_eq_N dec_eq_sig_hprop. +Extraction Inline Erep SRep ZNWord WordNZ. +Extraction Inline GF25519.fe25519. Extraction Inline EdDSARepChange.sign EdDSARepChange.splitSecretPrngCurve. Extraction Inline SRep_testbit. +Extraction Inline Crypto.Util.IterAssocOp.iter_op Crypto.Util.IterAssocOp.test_and_op. Extraction Inline PointEncoding.Kencode_point. -Extraction Inline ExtendedCoordinates.Extended.coordinates ExtendedCoordinates.Extended.to_twisted ExtendedCoordinates.Extended.from_twisted. -Extraction Inline CompleteEdwardsCurve.E.coordinates. - -(* unused functions *) -Extraction Inline False_rect False_rec and_rect and_rec. -Extraction Inline Z.div_eucl. -Extraction Inline Tuple.from_list'_obligation_1 Tuple.from_list_obligation_1. -Extraction Inline Tuple.from_list'_obligation_2 Tuple.from_list_obligation_2. -Extract Inlined Constant Coq.Numbers.Natural.Peano.NPeano.Nat.max_case_strong => "#error unused". -Extract Inlined Constant Coq.Numbers.Natural.Peano.NPeano.Nat.max_case => "#error unused". -Extract Inlined Constant Coq.Arith.Max.max_dec => "#error unused". -Extract Inlined Constant Coq.NArith.BinNat.N.max_dec => "#error unused". -Extract Inlined Constant Coq.Numbers.Natural.Peano.NPeano.Nat.max_dec => "#error unused". -Extract Inlined Constant Coq.Arith.PeanoNat.Nat.max_dec => "#error unused". -Extract Inlined Constant Coq.PArith.BinPos.Pos.max_dec => "#error unused". -Extract Inlined Constant Coq.NArith.BinNat.N.Private_Dec.max_dec => "#error unused". -Extract Inlined Constant Coq.Numbers.Natural.Peano.NPeano.Nat.Private_Dec.max_dec => "#error unused". -Extract Inlined Constant Coq.Arith.PeanoNat.Nat.Private_Dec.max_dec => "#error unused". -Extract Inlined Constant Coq.PArith.BinPos.Pos.Private_Dec.max_dec => "#error unused". -Extract Inlined Constant Coq.ZArith.BinInt.Z.Private_Dec.max_dec => "#error unused". -Extract Inlined Constant Coq.ZArith.BinInt.Z.max_dec => "#error unused". -Extract Inlined Constant Nat.divmod => "#error unused". -Extract Inlined Constant Coq.NArith.BinNat.N.sqrt_up => "#error unused". -Extract Inlined Constant Coq.Numbers.Natural.Peano.NPeano.Nat.sqrt_up => "#error unused". -Extract Inlined Constant Coq.Arith.PeanoNat.Nat.sqrt_up => "#error unused". -Extract Inlined Constant Coq.ZArith.BinInt.Z.sqrt_up => "#error unused". +Extraction Inline ExtendedCoordinates.Extended.point ExtendedCoordinates.Extended.coordinates ExtendedCoordinates.Extended.to_twisted ExtendedCoordinates.Extended.from_twisted ExtendedCoordinates.Extended.add_coordinates ExtendedCoordinates.Extended.add ExtendedCoordinates.Extended.opp ExtendedCoordinates.Extended.zero. (* ExtendedCoordinates.Extended.zero could be precomputed *) +Extraction Inline CompleteEdwardsCurve.E.coordinates CompleteEdwardsCurve.E.zero. + (* Recursive Extraction sign. *) + (* most of the code we want seems to be below [eq_dec1] and there is other stuff above that *) + (* TODO: remove branching from [sRep] functions *) + +(* fragment of output: + +sign :: Word -> Word -> Prelude.Integer -> Word -> Word +sign pk sk mlen msg = + let { + sp = let {hsk = h b sk} in + (,) + (sRepDecModLShort + (combine n (clearlow n c (wfirstn n ((Prelude.+) b b) hsk)) (Prelude.succ 0) + (wones (Prelude.succ 0)))) (split2 b b hsk)} + in + let {r = sRepDecModL (h ((Prelude.+) b mlen) (combine b (Prelude.snd sp) mlen msg))} in + let {r0 = sRepERepMul r eRepB} in + combine b (eRepEnc r0) b + (sRepEnc + (sRepAdd r + (sRepMul + (sRepDecModL + (h ((Prelude.+) b ((Prelude.+) b mlen)) + (combine b (eRepEnc r0) ((Prelude.+) b mlen) (combine b pk mlen msg)))) (Prelude.fst sp)))) + +sRepERepMul :: SRep0 -> Erep -> Erep +sRepERepMul sc a = + Prelude.snd + (funexp (\state -> + case state of { + (,) i acc -> + let {acc2 = erepAdd acc acc} in + let {acc2a = erepAdd a acc2} in + (\fO fS n -> {- match_on_nat -} if n Prelude.== 0 then fO () else fS (n Prelude.- 1)) + (\_ -> (,) 0 + acc) + (\i' -> (,) i' + (eRepSel ((\w n -> Data.Bits.testBit w (Prelude.fromIntegral n)) sc (of_nat i')) acc2 acc2a)) + i}) ((,) ll + (case ((,) zero_ one_) of { + (,) x y -> (,) ((,) ((,) x y) one_) (mul3 x y)})) ll) + +erepAdd :: (Point0 Fe25519) -> (Point0 Fe25519) -> Point0 Fe25519 +erepAdd p q = + case p of { + (,) y t1 -> + case y of { + (,) y0 z1 -> + case y0 of { + (,) x1 y1 -> + case q of { + (,) y2 t2 -> + case y2 of { + (,) y3 z2 -> + case y3 of { + (,) x2 y4 -> + let {a = mul3 (sub2 y1 x1) (sub2 y4 x2)} in + let {b0 = mul3 (add2 y1 x1) (add2 y4 x2)} in + let {c0 = mul3 (mul3 t1 twice_d) t2} in + let {d = mul3 z1 (add2 z2 z2)} in + let {e = sub2 b0 a} in + let {f = sub2 d c0} in + let {g = add2 d c0} in + let {h0 = add2 b0 a} in + let {x3 = mul3 e f} in + let {y5 = mul3 g h0} in + let {t3 = mul3 e h0} in let {z3 = mul3 f g} in (,) ((,) ((,) x3 y5) z3) t3}}}}}} +*) diff --git a/src/Experiments/ExtrHaskellNats.v b/src/Experiments/ExtrHaskellNats.v new file mode 100644 index 000000000..ef9fd06d9 --- /dev/null +++ b/src/Experiments/ExtrHaskellNats.v @@ -0,0 +1,94 @@ +(** * Extraction Directives for [nat] in Haskell *) +(** [nat] is really complicated, so we jump through many hoops to get + code that compiles in 8.4 and 8.5 at the same time. *) +Require Coq.Numbers.Natural.Peano.NPeano. +Require Coq.Arith.Compare_dec Coq.Arith.EqNat Coq.Arith.Peano_dec. + +Extract Inductive nat => "Prelude.Integer" [ "0" "Prelude.succ" ] + "(\fO fS n -> {- match_on_nat -} if n Prelude.== 0 then fO () else fS (n Prelude.- 1))". + + +(** We rely on the fact that Coq forbids masking absolute names. Hopefully we can drop support for 8.4 before this is changed. *) +Module Coq. + Module M. Export NPeano.Nat. End M. + Module Init. + Module Nat. + Export M. + End Nat. + End Init. + Module Numbers. + Module Natural. + Module Peano. + Module NPeano. + Module Nat. + Export M. + End Nat. + End NPeano. + End Peano. + End Natural. + End Numbers. + Module Arith. + Module PeanoNat. + Module Nat. + Export M. + End Nat. + End PeanoNat. + End Arith. +End Coq. + +Module Export Import_NPeano_Nat. + Import Coq.Numbers.Natural.Peano.NPeano.Nat. + + Extract Inlined Constant add => "(Prelude.+)". + Extract Inlined Constant mul => "(Prelude.*)". + Extract Inlined Constant pow => "(Prelude.^)". + Extract Inlined Constant max => "Prelude.max". + Extract Inlined Constant min => "Prelude.min". + Extract Inlined Constant gcd => "Prelude.gcd". + Extract Inlined Constant lcm => "Prelude.lcm". + Extract Inlined Constant land => "(Data.Bits..&.)". + Extract Inlined Constant compare => "Prelude.compare". + Extract Inlined Constant ltb => "(Prelude.<)". + Extract Inlined Constant leb => "(Prelude.<=)". + Extract Inlined Constant eqb => "(Prelude.==)". + Extract Inlined Constant odd => "Prelude.odd". + Extract Inlined Constant even => "Prelude.even". + Extract Constant pred => "(\n -> Prelude.max 0 (Prelude.pred n))". + Extract Constant sub => "(\n m -> Prelude.max 0 (n Prelude.- m))". + Extract Constant div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". + Extract Constant modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". +End Import_NPeano_Nat. + + +Module Export Import_Init_Nat. + Import Coq.Init.Nat. + + Extract Inlined Constant add => "(Prelude.+)". + Extract Inlined Constant mul => "(Prelude.*)". + Extract Inlined Constant max => "Prelude.max". + Extract Inlined Constant min => "Prelude.min". + Extract Constant pred => "(\n -> Prelude.max 0 (Prelude.pred n))". + Extract Constant sub => "(\n m -> Prelude.max 0 (n Prelude.- m))". + + Extract Constant div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". + Extract Constant modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". +End Import_Init_Nat. + + +Module Export Import_PeanoNat_Nat. + Import Coq.Arith.PeanoNat.Nat. + + Extract Inlined Constant add => "(Prelude.+)". + Extract Inlined Constant mul => "(Prelude.*)". + Extract Inlined Constant max => "Prelude.max". + Extract Inlined Constant min => "Prelude.min". + Extract Inlined Constant compare => "Prelude.compare". +End Import_PeanoNat_Nat. + +Extract Inlined Constant Compare_dec.nat_compare_alt => "Prelude.compare". +Extract Inlined Constant Compare_dec.lt_dec => "(Prelude.<)". +Extract Inlined Constant Compare_dec.leb => "(Prelude.<=)". +Extract Inlined Constant Compare_dec.le_lt_dec => "(Prelude.<=)". +Extract Inlined Constant EqNat.beq_nat => "(Prelude.==)". +Extract Inlined Constant EqNat.eq_nat_decide => "(Prelude.==)". +Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)". diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 5c0d143c2..615bd832b 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -82,10 +82,10 @@ Section ModularBaseSystem. Definition eq (x y : digits) : Prop := decode x = decode y. - Definition freeze (x : digits) : digits := - from_list (freeze [[x]]) (length_freeze length_to_list). + Definition freeze B (x : digits) : digits := + from_list (freeze B [[x]]) (length_freeze length_to_list). - Definition eqb (x y : digits) : bool := fieldwiseb Z.eqb (freeze x) (freeze y). + Definition eqb B (x y : digits) : bool := fieldwiseb Z.eqb (freeze B x) (freeze B y). (* Note : both of the following square root definitions will produce garbage output if the input is not square mod [modulus]. The caller should either provably only call them with square input, @@ -97,10 +97,10 @@ Section ModularBaseSystem. (* sqrt_5mod8 is parameterized over implementation of [mul] and [pow] because it relies on bounds-checking for these two functions, which is much easier for simplified implementations than the more generalized ones defined here. *) - Definition sqrt_5mod8 mul_ pow_ (chain : list (nat * nat)) + Definition sqrt_5mod8 B mul_ pow_ (chain : list (nat * nat)) (chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (modulus / 8 + 1)) (sqrt_minus1 x : digits) : digits := - let b := pow_ x chain in if eqb (mul_ b b) x then b else mul_ sqrt_minus1 b. + let b := pow_ x chain in if eqb B (mul_ b b) x then b else mul_ sqrt_minus1 b. Import Morphisms. Global Instance eq_Equivalence : Equivalence eq. @@ -108,6 +108,10 @@ Section ModularBaseSystem. split; cbv [eq]; repeat intro; congruence. Qed. + Definition select B (b : Z) (x y : digits) := + add (map (Z.land (neg B b)) x) + (map (Z.land (neg B (Z.lxor b 1))) x). + Context {target_widths} (target_widths_nonneg : forall x, In x target_widths -> 0 <= x) (bits_eq : sum_firstn limb_widths (length limb_widths) = sum_firstn target_widths (length target_widths)). diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v index 6d0848151..e64ed5d0f 100644 --- a/src/ModularArithmetic/ModularBaseSystemList.v +++ b/src/ModularArithmetic/ModularBaseSystemList.v @@ -8,6 +8,7 @@ Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. Require Import Crypto.ModularArithmetic.ExtendedBaseVector. Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. Require Import Crypto.ModularArithmetic.Pow2Base. Require Import Crypto.ModularArithmetic.Conversion. @@ -51,28 +52,35 @@ Section Defs. Definition modulus_digits := encodeZ limb_widths modulus. - (* compute at compile time *) - Definition max_ones := Z.ones (fold_right Z.max 0 limb_widths). - (* Constant-time comparison with modulus; only works if all digits of [us] are less than 2 ^ their respective limb width. *) - Fixpoint ge_modulus' us acc i := - match i with - | O => andb (Z.leb (modulus_digits [0]) (us [0])) acc - | S i' => ge_modulus' us (andb (Z.eqb (modulus_digits [i]) (us [i])) acc) i' + Fixpoint ge_modulus' {A} (f : Z -> A) us (result : Z) i := + dlet r := result in + match i return A with + | O => dlet x := if Z.leb (modulus_digits [0]) (us [0]) + then r + else 0 in f x + | S i' => ge_modulus' f us + (if Z.eqb (modulus_digits [i]) (us [i]) + then r + else 0) i' end. - Definition ge_modulus us := ge_modulus' us true (length limb_widths - 1)%nat. + Definition ge_modulus us := ge_modulus' id us 1 (length limb_widths - 1)%nat. + + (* analagous to NEG assembly instruction on an integer that is 0 or 1: + neg 1 = 2^64 - 1 (on 64-bit; 2^32-1 on 32-bit, etc.) + neg 0 = 0 *) + Definition neg (int_width : Z) (b : Z) := if b =? 1 then Z.ones int_width else 0. - Definition conditional_subtract_modulus (us : digits) (cond : bool) := - let and_term := if cond then max_ones else 0 in + Definition conditional_subtract_modulus int_width (us : digits) (cond : Z) := (* [and_term] is all ones if us' is full, so the subtractions subtract q overall. Otherwise, it's all zeroes, and the subtractions do nothing. *) - map2 (fun x y => x - y) us (map (Z.land and_term) modulus_digits). + map2 (fun x y => x - y) us (map (Z.land (neg int_width cond)) modulus_digits). - Definition freeze (us : digits) : digits := + Definition freeze int_width (us : digits) : digits := let us' := carry_full (carry_full (carry_full us)) in - conditional_subtract_modulus us' (ge_modulus us'). + conditional_subtract_modulus int_width us' (ge_modulus us'). Context {target_widths} (target_widths_nonneg : forall x, In x target_widths -> 0 <= x) (bits_eq : sum_firstn limb_widths (length limb_widths) = @@ -86,4 +94,4 @@ Section Defs. limb_widths limb_widths_nonneg (Z.eq_le_incl _ _ (Z.eq_sym bits_eq)). -End Defs. +End Defs.
\ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v index 93b39e89a..23ec30cf7 100644 --- a/src/ModularArithmetic/ModularBaseSystemListProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v @@ -110,10 +110,11 @@ Section LengthProofs. rewrite encode'_spec, encode'_length; auto using encode'_length, limb_widths_nonneg, Nat.eq_le_incl, base_from_limb_widths_length. Qed. + Hint Rewrite @length_modulus_digits : distr_length. - Lemma length_conditional_subtract_modulus {u cond} : + Lemma length_conditional_subtract_modulus {int_width u cond} : length u = length limb_widths - -> length (conditional_subtract_modulus u cond) = length limb_widths. + -> length (conditional_subtract_modulus int_width u cond) = length limb_widths. Proof. intros; unfold conditional_subtract_modulus. rewrite map2_length, map_length, length_modulus_digits. @@ -121,9 +122,9 @@ Section LengthProofs. Qed. Hint Rewrite @length_conditional_subtract_modulus : distr_length. - Lemma length_freeze {u} : + Lemma length_freeze {int_width u} : length u = length limb_widths - -> length (freeze u) = length limb_widths. + -> length (freeze int_width u) = length limb_widths. Proof. intros; unfold freeze; repeat autorewrite with distr_length; congruence. Qed. @@ -285,27 +286,41 @@ Section ModulusComparisonProofs. reflexivity. Qed. - Lemma ge_modulus'_false : forall us i, - ge_modulus' us false i = false. + Lemma ge_modulus'_0 : forall {A} f us i, + ge_modulus' (A := A) f us 0 i = f 0. Proof. - induction i; intros; simpl; rewrite Bool.andb_false_r; auto. + induction i; intros; simpl; break_if; auto. + Qed. + + Lemma ge_modulus'_01 : forall {A} f us i b, + (b = 0 \/ b = 1) -> + (ge_modulus' (A := A) f us b i = f 0 \/ ge_modulus' (A := A) f us b i = f 1). + Proof. + induction i; intros; + try intuition (subst; cbv [ge_modulus' LetIn.Let_In]; break_if; tauto). + simpl; cbv [LetIn.Let_In]. + break_if; apply IHi; tauto. + Qed. + + Lemma ge_modulus_01 : forall us, + (ge_modulus us = 0 \/ ge_modulus us = 1). + Proof. + cbv [ge_modulus]; intros; apply ge_modulus'_01; tauto. Qed. Lemma ge_modulus'_true_digitwise : forall us, length us = length limb_widths -> - forall i, (i < length us)%nat -> ge_modulus' us true i = true -> + forall i, (i < length us)%nat -> ge_modulus' id us 1 i = 1 -> forall j, (j <= i)%nat -> nth_default 0 modulus_digits j <= nth_default 0 us j. Proof. induction i; repeat match goal with | |- _ => progress intros; simpl in * - | |- _ => rewrite ge_modulus'_false in * + | |- _ => progress cbv [LetIn.Let_In] in * + | |- _ =>erewrite (ge_modulus'_0 (@id Z)) in * | H : (?x <= 0)%nat |- _ => progress replace x with 0%nat in * by omega - | H : (?b && true)%bool = true |- _ => let A:= fresh "H" in - rewrite Bool.andb_true_r in H; case_eq b; intro A; rewrite A in H - | H : ge_modulus' _ (?b && true)%bool _ = true |- _ => let A:= fresh "H" in - rewrite Bool.andb_true_r in H; case_eq b; intro A; rewrite A in H + | |- _ => break_if | |- _ => discriminate | |- _ => solve [rewrite ?Z.leb_le, ?Z.eqb_eq in *; omega] end. @@ -316,35 +331,39 @@ Section ModulusComparisonProofs. Lemma ge_modulus'_compare' : forall us, length us = length limb_widths -> bounded limb_widths us -> forall i, (i < length limb_widths)%nat -> - (ge_modulus' us true i = false <-> compare' us modulus_digits (S i) = Lt). + (ge_modulus' id us 1 i = 0 <-> compare' us modulus_digits (S i) = Lt). Proof. induction i; repeat match goal with - | |- _ => progress intros - | |- _ => progress (simpl compare' in *) + | |- _ => progress (intros; cbv [LetIn.Let_In id]) + | |- _ => progress (simpl compare' in * ) | |- _ => progress specialize_by omega - | |- _ => progress rewrite ?Z.compare_eq_iff, - ?Z.compare_gt_iff, ?Z.compare_lt_iff in * - | |- appcontext[ge_modulus' _ _ 0] => + | |- _ => (progress rewrite ?Z.compare_eq_iff, + ?Z.compare_gt_iff, ?Z.compare_lt_iff in * ) + | |- appcontext[ge_modulus' _ _ _ 0] => cbv [ge_modulus'] - | |- appcontext[ge_modulus' _ _ (S _)] => - unfold ge_modulus'; fold ge_modulus' + | |- appcontext[ge_modulus' _ _ _ (S _)] => + unfold ge_modulus'; fold (ge_modulus' (@id Z)) | |- _ => break_if | |- _ => rewrite Nat.sub_0_r - | |- _ => rewrite ge_modulus'_false + | |- _ => rewrite (ge_modulus'_0 (@id Z)) | |- _ => rewrite Bool.andb_true_r | |- _ => rewrite Z.leb_compare; break_match | |- _ => rewrite Z.eqb_compare; break_match + | |- _ => (rewrite Z.leb_le in * ) + | |- _ => (rewrite Z.leb_gt in * ) + | |- _ => (rewrite Z.eqb_eq in * ) + | |- _ => (rewrite Z.eqb_neq in * ) | |- _ => split; (congruence || omega) | |- _ => assumption - end; - pose proof (bounded_le_modulus_digits c_upper_bound us (S i)); - specialize_by (auto || omega); omega. + end; + pose proof (bounded_le_modulus_digits c_upper_bound us (S i)); + specialize_by (auto || omega); split; (congruence || omega). Qed. Lemma ge_modulus_spec : forall u, length u = length limb_widths -> bounded limb_widths u -> - (ge_modulus u = false <-> 0 <= BaseSystem.decode base u < modulus). + (ge_modulus u = 0 <-> 0 <= BaseSystem.decode base u < modulus). Proof. cbv [ge_modulus]; intros. assert (0 < length limb_widths)%nat @@ -365,6 +384,8 @@ End ModulusComparisonProofs. Section ConditionalSubtractModulusProofs. Context `{prm :PseudoMersenneBaseParams} + (* B is machine integer width (e.g. 32, 64) *) + {B} (B_pos : 0 < B) (B_compat : forall w, In w limb_widths -> w <= B) (c_upper_bound : c - 1 < 2 ^ nth_default 0 limb_widths 0) (lt_1_length_limb_widths : (1 < length limb_widths)%nat). Local Notation base := (base_from_limb_widths limb_widths). @@ -386,24 +407,33 @@ Section ConditionalSubtractModulusProofs. simpl; f_equal; auto using in_eq, in_cons. Qed. - Lemma map_land_max_ones : forall us, length us = length limb_widths -> - bounded limb_widths us -> map (Z.land max_ones) us = us. + Lemma bounded_digit_fits : forall us, + length us = length limb_widths -> bounded limb_widths us -> + forall x, In x us -> 0 <= x < 2 ^ B. Proof. - intros; apply map_id_strong; intros ? HIn. - rewrite Z.land_comm. - cbv [max_ones]. - rewrite Z.land_ones by apply Z.le_fold_right_max_initial. - apply Z.mod_small. - apply In_nth with (d := 0) in HIn. - destruct HIn as [i HIn]; destruct HIn; subst. - rewrite bounded_iff in H0. - specialize (H0 i). + intros. + let i := fresh "i" in + match goal with H : In ?x ?us, Hb : bounded _ _ |- _ => + apply In_nth with (d := 0) in H; destruct H as [i [? ?] ]; + rewrite bounded_iff in Hb; specialize (Hb i); + assert (2 ^ nth i limb_widths 0 <= 2 ^ B) by + (apply Z.pow_le_mono_r; try apply B_compat, nth_In; omega) end. rewrite !nth_default_eq in *. - split; try omega. - eapply Z.lt_le_trans; try intuition eassumption. - apply Z.pow_le_mono_r; try omega. - apply Z.le_fold_right_max; eauto. - apply nth_In. omega. + omega. + Qed. + + Lemma map_land_max_ones : forall us, + length us = length limb_widths -> + bounded limb_widths us -> map (Z.land (Z.ones B)) us = us. + Proof. + repeat match goal with + | |- _ => progress intros + | |- _ => apply map_id_strong + | |- appcontext[Z.ones ?n &' ?x] => rewrite (Z.land_comm _ x); + rewrite Z.land_ones by omega + | |- _ => apply Z.mod_small + | |- _ => solve [eauto using bounded_digit_fits] + end. Qed. Lemma map_land_zero : forall us, map (Z.land 0) us = zeros (length us). @@ -411,32 +441,35 @@ Section ConditionalSubtractModulusProofs. induction us; boring. Qed. - Lemma conditional_subtract_modulus_spec : forall u cond, + Hint Rewrite @length_modulus_digits @length_zeros : distr_length. + Lemma conditional_subtract_modulus_spec : forall u cond + (cond_01 : cond = 0 \/ cond = 1), length u = length limb_widths -> - BaseSystem.decode base (conditional_subtract_modulus u cond) = - BaseSystem.decode base u - (if cond then 1 else 0) * modulus. + BaseSystem.decode base (conditional_subtract_modulus B u cond) = + BaseSystem.decode base u - cond * modulus. Proof. repeat match goal with - | |- _ => progress (cbv [conditional_subtract_modulus]; intros) + | |- _ => progress (cbv [conditional_subtract_modulus neg]; intros) + | |- _ => destruct cond_01; subst | |- _ => break_if | |- _ => rewrite map_land_max_ones by auto using bounded_modulus_digits | |- _ => rewrite map_land_zero - | |- _ => rewrite map2_sub_eq - by (rewrite ?length_modulus_digits, ?length_zeros; congruence) + | |- _ => rewrite map2_sub_eq by distr_length | |- _ => rewrite sub_rep by auto | |- _ => rewrite zeros_rep | |- _ => rewrite decode_modulus_digits by auto | |- _ => f_equal; ring + | |- _ => discriminate end. Qed. Lemma conditional_subtract_modulus_preserves_bounded : forall u, length u = length limb_widths -> bounded limb_widths u -> - bounded limb_widths (conditional_subtract_modulus u (ge_modulus u)). + bounded limb_widths (conditional_subtract_modulus B u (ge_modulus u)). Proof. repeat match goal with - | |- _ => progress (cbv [conditional_subtract_modulus]; intros) + | |- _ => progress (cbv [conditional_subtract_modulus neg]; intros) | |- _ => unique pose proof bounded_modulus_digits | |- _ => rewrite map_land_max_ones by auto using bounded_modulus_digits | |- _ => rewrite map_land_zero @@ -455,11 +488,12 @@ Section ConditionalSubtractModulusProofs. | |- _ => omega end. cbv [ge_modulus] in Heqb. + rewrite Z.eqb_eq in *. apply ge_modulus'_true_digitwise with (j := i) in Heqb; auto; omega. Qed. Lemma bounded_mul2_modulus : forall u, length u = length limb_widths -> - bounded limb_widths u -> ge_modulus u = true -> + bounded limb_widths u -> ge_modulus u = 1 -> modulus <= BaseSystem.decode base u < 2 * modulus. Proof. intros. @@ -494,16 +528,16 @@ Section ConditionalSubtractModulusProofs. Lemma conditional_subtract_lt_modulus : forall u, length u = length limb_widths -> bounded limb_widths u -> - ge_modulus (conditional_subtract_modulus u (ge_modulus u)) = false. + ge_modulus (conditional_subtract_modulus B u (ge_modulus u)) = 0. Proof. intros. - rewrite ge_modulus_spec by auto using length_conditional_subtract_modulus, - conditional_subtract_modulus_preserves_bounded. + rewrite ge_modulus_spec by auto using length_conditional_subtract_modulus, conditional_subtract_modulus_preserves_bounded. + pose proof (ge_modulus_01 u) as Hgm01. rewrite conditional_subtract_modulus_spec by auto. - break_if. - + pose proof (bounded_mul2_modulus u); specialize_by auto. + destruct Hgm01 as [Hgm0 | Hgm1]; rewrite ?Hgm0, ?Hgm1. + + apply ge_modulus_spec in Hgm0; auto. omega. - + apply ge_modulus_spec in Heqb; auto. + + pose proof (bounded_mul2_modulus u); specialize_by auto. omega. Qed. End ConditionalSubtractModulusProofs.
\ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index ff1dd87dd..1117229d1 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -49,7 +49,6 @@ Definition full_carry_chain_opt := Eval compute in @Pow2Base.full_carry_chain. Definition length_opt := Eval compute in length. Definition base_from_limb_widths_opt := Eval compute in @Pow2Base.base_from_limb_widths. Definition minus_opt := Eval compute in minus. -Definition max_ones_opt := Eval compute in @max_ones. Definition from_list_default_opt {A} := Eval compute in (@from_list_default A). Definition sum_firstn_opt {A} := Eval compute in (@sum_firstn A). Definition zeros_opt := Eval compute in (@zeros). @@ -954,18 +953,16 @@ Section Canonicalization. -> carry_full_3_opt_cps f us = f (carry_full (carry_full (carry_full us))) := proj2_sig (carry_full_3_opt_cps_sig f us). - Definition conditional_subtract_modulus_opt_sig (f : list Z) (cond : bool) : - { g | g = conditional_subtract_modulus f cond}. + Definition conditional_subtract_modulus_opt_sig (f : list Z) (cond : Z) : + { g | g = conditional_subtract_modulus int_width f cond}. Proof. eexists. cbv [conditional_subtract_modulus]. - match goal with |- appcontext[if cond then ?a else ?b] => let LHS := match goal with |- ?LHS = ?RHS => LHS end in let RHS := match goal with |- ?LHS = ?RHS => RHS end in - let RHSf := match (eval pattern (if cond then a else b) in RHS) with ?RHSf _ => RHSf end in - change (LHS = Let_In (if cond then a else b) RHSf) end. + let RHSf := match (eval pattern (neg int_width cond) in RHS) with ?RHSf _ => RHSf end in + change (LHS = Let_In (neg int_width cond) RHSf). cbv [map2 map]. - change @max_ones with max_ones_opt. reflexivity. Defined. @@ -973,39 +970,50 @@ Section Canonicalization. := Eval cbv [proj1_sig conditional_subtract_modulus_opt_sig] in proj1_sig (conditional_subtract_modulus_opt_sig f cond). Definition conditional_subtract_modulus_opt_correct f cond - : conditional_subtract_modulus_opt f cond = conditional_subtract_modulus f cond + : conditional_subtract_modulus_opt f cond = conditional_subtract_modulus int_width f cond := Eval cbv [proj2_sig conditional_subtract_modulus_opt_sig] in proj2_sig (conditional_subtract_modulus_opt_sig f cond). + Lemma ge_modulus'_cps : forall {A} (f : Z -> A) (us : list Z) i b, + f (ge_modulus' id us b i) = ge_modulus' f us b i. + Proof. + induction i; intros; simpl; cbv [Let_In]; break_if; try reflexivity; + apply IHi. + Qed. + Definition ge_modulus_opt_sig (us : list Z) : - { b : bool | b = ModularBaseSystemList.ge_modulus us }. + { a : Z | a = ge_modulus us}. Proof. eexists. - cbv beta iota delta [ge_modulus ge_modulus']. + cbv [ge_modulus ge_modulus']. change length with length_opt. change nth_default with @nth_default_opt. change minus with minus_opt. reflexivity. Defined. - Definition ge_modulus_opt us : bool + Definition ge_modulus_opt us : Z := Eval cbv [proj1_sig ge_modulus_opt_sig] in proj1_sig (ge_modulus_opt_sig us). Definition ge_modulus_opt_correct us : - ge_modulus_opt us = ge_modulus us + ge_modulus_opt us= ge_modulus us := Eval cbv [proj2_sig ge_modulus_opt_sig] in proj2_sig (ge_modulus_opt_sig us). Definition freeze_opt_sig (us : list Z) : { b : list Z | length us = length limb_widths - -> b = ModularBaseSystemList.freeze us }. + -> b = ModularBaseSystemList.freeze int_width us }. Proof. eexists. cbv [ModularBaseSystemList.freeze]. rewrite <-conditional_subtract_modulus_opt_correct. intros. + cbv [ge_modulus]. + rewrite ge_modulus'_cps. let LHS := match goal with |- ?LHS = ?RHS => LHS end in let RHS := match goal with |- ?LHS = ?RHS => RHS end in let RHSf := match (eval pattern (carry_full (carry_full (carry_full us))) in RHS) with ?RHSf _ => RHSf end in rewrite <-carry_full_3_opt_cps_correct with (f := RHSf) by auto. + cbv [carry_full_3_opt_cps carry_full_opt_cps carry_sequence_opt_cps]. + cbv [ge_modulus']. cbv beta iota delta [ge_modulus ge_modulus']. change length with length_opt. change nth_default with @nth_default_opt. @@ -1019,7 +1027,7 @@ Section Canonicalization. Definition freeze_opt_correct us : length us = length limb_widths - -> freeze_opt us = ModularBaseSystemList.freeze us + -> freeze_opt us = ModularBaseSystemList.freeze int_width us := proj2_sig (freeze_opt_sig us). End Canonicalization. @@ -1061,15 +1069,16 @@ Section SquareRoots. End SquareRoot3mod4. Import Morphisms. - Global Instance eqb_Proper : Proper (eq ==> eq ==> Logic.eq) ModularBaseSystem.eqb. Admitted. + Global Instance eqb_Proper : Proper (Logic.eq ==> eq ==> eq ==> Logic.eq) ModularBaseSystem.eqb. Admitted. Section SquareRoot5mod8. Context {ec : ExponentiationChain (modulus / 8 + 1)}. Context (sqrt_m1 : digits) (sqrt_m1_correct : rep (mul sqrt_m1 sqrt_m1) (F.opp 1%F)). + Context {int_width} (preconditions : freezePreconditions prm int_width). Definition sqrt_5mod8_opt_sig (us : digits) : { vs : digits | - eq vs (sqrt_5mod8 (carry_mul_opt k_ c_) (pow_opt k_ c_ one_) chain chain_correct sqrt_m1 us)}. + eq vs (sqrt_5mod8 int_width (carry_mul_opt k_ c_) (pow_opt k_ c_ one_) chain chain_correct sqrt_m1 us)}. Proof. eexists; cbv [sqrt_5mod8]. let LHS := match goal with |- eq ?LHS ?RHS => LHS end in @@ -1083,7 +1092,7 @@ Section SquareRoots. proj1_sig (sqrt_5mod8_opt_sig us). Definition sqrt_5mod8_opt_correct us - : eq (sqrt_5mod8_opt us) (ModularBaseSystem.sqrt_5mod8 _ _ chain chain_correct sqrt_m1 us) + : eq (sqrt_5mod8_opt us) (ModularBaseSystem.sqrt_5mod8 int_width _ _ chain chain_correct sqrt_m1 us) := Eval cbv [proj2_sig sqrt_5mod8_opt_sig] in proj2_sig (sqrt_5mod8_opt_sig us). End SquareRoot5mod8. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index f8ad0969d..9a07e8ec0 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -833,7 +833,7 @@ Section CanonicalizationProofs. then 0 else (2 ^ B) >> (limb_widths [pred n]))). Local Notation minimal_rep u := ((bounded limb_widths (to_list (length limb_widths) u)) - /\ (ge_modulus (to_list _ u) = false)). + /\ (ge_modulus (to_list _ u) = 0)). Lemma decode_bitwise_eq_iff : forall u v, minimal_rep u -> minimal_rep v -> (fieldwise Logic.eq u v <-> @@ -896,7 +896,7 @@ Section CanonicalizationProofs. Qed. Lemma minimal_rep_freeze : forall u, initial_bounds u -> - minimal_rep (freeze u). + minimal_rep (freeze B u). Proof. repeat match goal with | |- _ => progress (cbv [freeze ModularBaseSystemList.freeze]) @@ -907,12 +907,12 @@ Section CanonicalizationProofs. | |- _ => apply conditional_subtract_lt_modulus | |- _ => apply conditional_subtract_modulus_preserves_bounded | |- bounded _ (carry_full _) => apply bounded_iff - | |- _ => solve [auto using lt_1_length_limb_widths, length_carry_full, length_to_list] + | |- _ => solve [auto using B_pos, B_compat, lt_1_length_limb_widths, length_carry_full, length_to_list] end. Qed. Lemma freeze_decode : forall u, - BaseSystem.decode base (to_list _ (freeze u)) mod modulus = + BaseSystem.decode base (to_list _ (freeze B u)) mod modulus = BaseSystem.decode base (to_list _ u) mod modulus. Proof. repeat match goal with @@ -922,7 +922,7 @@ Section CanonicalizationProofs. | |- _ => rewrite Z.mod_add by (pose proof prime_modulus; prime_bound) | |- _ => rewrite to_list_from_list | |- _ => rewrite conditional_subtract_modulus_spec by - auto using lt_1_length_limb_widths, length_carry_full, length_to_list + auto using B_pos, B_compat, lt_1_length_limb_widths, length_carry_full, length_to_list, ge_modulus_01 end. rewrite !decode_mod_Fdecode by auto using length_carry_full, length_to_list. cbv [carry_full]. @@ -941,7 +941,7 @@ Section CanonicalizationProofs. rewrite from_list_to_list; reflexivity. Qed. - Lemma freeze_rep : forall u x, rep u x -> rep (freeze u) x. + Lemma freeze_rep : forall u x, rep u x -> rep (freeze B u) x. Proof. cbv [rep]; intros. apply F.eq_to_Z_iff. @@ -952,7 +952,7 @@ Section CanonicalizationProofs. Lemma freeze_canonical : forall u v x y, rep u x -> rep v y -> initial_bounds u -> initial_bounds v -> - (x = y <-> fieldwise Logic.eq (freeze u) (freeze v)). + (x = y <-> fieldwise Logic.eq (freeze B u) (freeze B v)). Proof. intros; apply bounded_canonical; auto using freeze_rep, minimal_rep_freeze. Qed. @@ -977,7 +977,7 @@ Section SquareRootProofs. Lemma eqb_true_iff : forall u v x y, bounded_by u freeze_input_bounds -> bounded_by v freeze_input_bounds -> - u ~= x -> v ~= y -> (x = y <-> eqb u v = true). + u ~= x -> v ~= y -> (x = y <-> eqb B u v = true). Proof. cbv [eqb freeze_input_bounds]. intros. rewrite fieldwiseb_fieldwise by (apply Z.eqb_eq). @@ -986,10 +986,10 @@ Section SquareRootProofs. Lemma eqb_false_iff : forall u v x y, bounded_by u freeze_input_bounds -> bounded_by v freeze_input_bounds -> - u ~= x -> v ~= y -> (x <> y <-> eqb u v = false). + u ~= x -> v ~= y -> (x <> y <-> eqb B u v = false). Proof. intros. - case_eq (eqb u v). + case_eq (eqb B u v). + rewrite <-eqb_true_iff by eassumption; split; intros; congruence || contradiction. + split; intros; auto. @@ -1032,24 +1032,24 @@ Section SquareRootProofs. Lemma sqrt_5mod8_correct : forall u x, u ~= x -> bounded_by u pow_input_bounds -> bounded_by u freeze_input_bounds -> - (sqrt_5mod8 mul_ pow_ chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x. + (sqrt_5mod8 B mul_ pow_ chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x. Proof. repeat match goal with | |- _ => progress (cbv [sqrt_5mod8 F.sqrt_5mod8]; intros) | |- _ => rewrite @F.pow_2_r in * | |- _ => rewrite eqb_correct in * by eassumption - | |- (if eqb ?a ?b then _ else _) ~= + | |- (if eqb _ ?a ?b then _ else _) ~= (if dec (?c = _) then _ else _) => assert (a ~= c); rewrite !mul_equiv, pow_equiv in *; repeat break_if | |- _ => apply mul_rep; try reflexivity; rewrite <-chain_correct; apply pow_rep; eassumption | |- _ => rewrite <-chain_correct; apply pow_rep; eassumption - | H : eqb ?a ?b = true |- _ => + | H : eqb _ ?a ?b = true |- _ => rewrite <-(eqb_true_iff a b) in H by (eassumption || rewrite <-mul_equiv, <-pow_equiv; apply mul_bounded, pow_bounded; auto) - | H : eqb ?a ?b = false |- _ => + | H : eqb _ ?a ?b = false |- _ => rewrite <-(eqb_false_iff a b) in H by (eassumption || rewrite <-mul_equiv, <-pow_equiv; apply mul_bounded, pow_bounded; auto) diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 36feb2f4c..e89615dde 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -129,7 +129,7 @@ Definition zero_subst : zero = zero_ := eq_refl zero_. Definition modulus_digits_ := Eval compute in ModularBaseSystemList.modulus_digits. Definition modulus_digits_subst : ModularBaseSystemList.modulus_digits = modulus_digits_ := eq_refl modulus_digits_. -Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb Z.leb andb. +Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb Z.leb ModularBaseSystemList.neg. Definition app_7 {T} (f : wire_digits) (P : wire_digits -> T) : T. Proof. @@ -461,7 +461,7 @@ Proof. Qed. Definition ge_modulus_sig (f : fe25519) : - { b : bool | b = ge_modulus_opt (to_list 10 f) }. + { b : Z | b = ge_modulus_opt (to_list 10 f) }. Proof. cbv [fe25519] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -471,7 +471,7 @@ Proof. reflexivity. Defined. -Definition ge_modulus (f : fe25519) : bool := +Definition ge_modulus (f : fe25519) : Z := Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in proj1_sig (ge_modulus_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). @@ -486,11 +486,11 @@ Proof. Defined. Definition freeze_sig (f : fe25519) : - { f' : fe25519 | f' = from_list_default 0 10 (freeze_opt c_ (to_list 10 f)) }. + { f' : fe25519 | f' = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)) }. Proof. cbv [fe25519] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - eexists; cbv [freeze_opt]. + eexists; cbv [freeze_opt int_width]. cbv [to_list to_list']. cbv [conditional_subtract_modulus_opt]. rewrite !modulus_digits_subst. @@ -509,7 +509,7 @@ Definition freeze (f : fe25519) : fe25519 := proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). Definition freeze_correct (f : fe25519) - : freeze f = from_list_default 0 10 (freeze_opt c_ (to_list 10 f)). + : freeze f = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)). Proof. pose proof (proj2_sig (freeze_sig f)). cbv [fe25519] in *. @@ -528,20 +528,28 @@ Proof. Defined. Definition fieldwiseb (f g : fe25519) : bool - := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in proj1_sig (fieldwiseb_sig f g). - -Definition fieldwiseb_correct (f g : fe25519) - : fieldwiseb f g = @Tuple.fieldwiseb Z Z 10 Z.eqb f g - := Eval cbv beta iota delta [proj2_sig fieldwiseb_sig] in proj2_sig (fieldwiseb_sig f g). + := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in + let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in + let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9) := g in + proj1_sig (fieldwiseb_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) + (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9)). + +Lemma fieldwiseb_correct (f g : fe25519) + : fieldwiseb f g = @Tuple.fieldwiseb Z Z 10 Z.eqb f g. +Proof. + set (f' := f); set (g' := g). + hnf in f, g; destruct_head' prod. + exact (proj2_sig (fieldwiseb_sig f' g')). +Qed. Definition eqb_sig (f g : fe25519) : - { b | b = eqb f g }. + { b | b = eqb int_width f g }. Proof. cbv [eqb]. cbv [fe25519] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. - cbv [ModularBaseSystem.freeze]. + cbv [ModularBaseSystem.freeze int_width]. rewrite <-!from_list_default_eq with (d := 0). rewrite <-!(freeze_opt_correct c_) by auto using length_to_list. rewrite <-!freeze_correct. @@ -550,17 +558,26 @@ Proof. Defined. Definition eqb (f g : fe25519) : bool - := Eval cbv beta iota delta [proj1_sig eqb_sig] in proj1_sig (eqb_sig f g). - -Definition eqb_correct (f g : fe25519) - : eqb f g = ModularBaseSystem.eqb f g - := Eval cbv beta iota delta [proj2_sig eqb_sig] in proj2_sig (eqb_sig f g). + := Eval cbv beta iota delta [proj1_sig eqb_sig] in + let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in + let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9) := g in + proj1_sig (eqb_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) + (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9)). + +Lemma eqb_correct (f g : fe25519) + : eqb f g = ModularBaseSystem.eqb int_width f g. +Proof. + set (f' := f); set (g' := g). + hnf in f, g; destruct_head' prod. + exact (proj2_sig (eqb_sig f' g')). +Qed. Definition sqrt_sig (f : fe25519) : - { f' : fe25519 | f' = sqrt_5mod8_opt k_ c_ one_ sqrt_m1 f}. + { f' : fe25519 | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ one_ sqrt_m1 f}. Proof. eexists. - cbv [sqrt_5mod8_opt]. + cbv [sqrt_5mod8_opt int_width]. + rewrite <- pow_correct. apply Proper_Let_In_nd_changebody; [reflexivity|intro]. set_evars. rewrite <-!mul_correct, <-eqb_correct. subst_evars. reflexivity. @@ -662,4 +679,4 @@ Definition unpack (f : wire_digits) : fe25519 := Definition unpack_correct (f : wire_digits) : unpack f = unpack_opt params25519 wire_widths_nonneg bits_eq f - := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). + := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f).
\ No newline at end of file diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v index e133e62ad..5d29d4cd5 100644 --- a/src/Specific/GF25519Bounded.v +++ b/src/Specific/GF25519Bounded.v @@ -16,6 +16,7 @@ Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Bool. Require Import Crypto.Util.Decidable. Require Import Crypto.Algebra. Import ListNotations. @@ -33,25 +34,37 @@ Local Ltac define_unop f opW blem := refine (exist_fe25519W (opW (proj1_fe25519W f)) _); abstract bounded_t opW blem. -Definition addW (f g : fe25519W) : fe25519W := interp_bexpr radd f g. -Definition subW (f g : fe25519W) : fe25519W := interp_bexpr rsub f g. -Definition mulW (f g : fe25519W) : fe25519W := interp_bexpr rmul f g. -Definition oppW (f : fe25519W) : fe25519W := interp_uexpr ropp f. -Definition freezeW (f : fe25519W) : fe25519W := interp_uexpr rfreeze f. +Local Opaque Let_In. +Local Arguments interp_radd / _ _. +Local Arguments interp_rsub / _ _. +Local Arguments interp_rmul / _ _. +Local Arguments interp_ropp / _. +Local Arguments interp_rfreeze / _. +Definition addW (f g : fe25519W) : fe25519W := Eval simpl in interp_radd f g. +Definition subW (f g : fe25519W) : fe25519W := Eval simpl in interp_rsub f g. +Definition mulW (f g : fe25519W) : fe25519W := Eval simpl in interp_rmul f g. +Definition oppW (f : fe25519W) : fe25519W := Eval simpl in interp_ropp f. +Definition freezeW (f : fe25519W) : fe25519W := Eval simpl in interp_rfreeze f. +Local Transparent Let_In. Definition powW (f : fe25519W) chain := fold_chain_opt (proj1_fe25519W one) mulW chain [f]. Definition invW (f : fe25519W) : fe25519W := Eval cbv -[Let_In fe25519W mulW] in powW f (chain inv_ec). -Definition add (f g : fe25519) : fe25519. -Proof. define_binop f g addW radd_correct_and_bounded. Defined. -Definition sub (f g : fe25519) : fe25519. -Proof. define_binop f g subW rsub_correct_and_bounded. Defined. -Definition mul (f g : fe25519) : fe25519. -Proof. define_binop f g mulW rmul_correct_and_bounded. Defined. -Definition opp (f : fe25519) : fe25519. -Proof. define_unop f oppW ropp_correct_and_bounded. Defined. -Definition freeze (f : fe25519) : fe25519. -Proof. define_unop f freezeW rfreeze_correct_and_bounded. Defined. +Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb := + change opW with (interp_rop); + rewrite pre_rewrite; + intros; apply rop_cb; assumption. + +Lemma addW_correct_and_bounded : ibinop_correct_and_bounded addW carry_add. +Proof. port_correct_and_bounded interp_radd_correct addW interp_radd radd_correct_and_bounded. Qed. +Lemma subW_correct_and_bounded : ibinop_correct_and_bounded subW carry_sub. +Proof. port_correct_and_bounded interp_rsub_correct subW interp_rsub rsub_correct_and_bounded. Qed. +Lemma mulW_correct_and_bounded : ibinop_correct_and_bounded mulW mul. +Proof. port_correct_and_bounded interp_rmul_correct mulW interp_rmul rmul_correct_and_bounded. Qed. +Lemma oppW_correct_and_bounded : iunop_correct_and_bounded oppW carry_opp. +Proof. port_correct_and_bounded interp_ropp_correct oppW interp_ropp ropp_correct_and_bounded. Qed. +Lemma freezeW_correct_and_bounded : iunop_correct_and_bounded freezeW freeze. +Proof. port_correct_and_bounded interp_rfreeze_correct freezeW interp_rfreeze rfreeze_correct_and_bounded. Qed. Lemma powW_correct_and_bounded chain : iunop_correct_and_bounded (fun x => powW x chain) (fun x => pow x chain). Proof. @@ -62,7 +75,7 @@ Proof. { intros; progress rewrite <- ?mul_correct, <- ?(fun X Y => proj1 (rmul_correct_and_bounded _ _ X Y)) by assumption. apply rmul_correct_and_bounded; assumption. } - { intros; symmetry; apply rmul_correct_and_bounded; assumption. } + { intros; change mulW with interp_rmul; rewrite interp_rmul_correct; symmetry; apply rmul_correct_and_bounded; assumption. } { intros [|?]; autorewrite with simpl_nth_default; (assumption || reflexivity). } Qed. @@ -79,34 +92,169 @@ Proof. apply powW_correct_and_bounded. Qed. +Definition fieldwisebW_sig (f g : fe25519W) + : { b | b = GF25519.fieldwiseb (fe25519WToZ f) (fe25519WToZ g) }. +Proof. + hnf in f, g; destruct_head' prod. + eexists. + cbv [GF25519.fieldwiseb fe25519WToZ]. + rewrite !word64eqb_Zeqb. + reflexivity. +Defined. + +Definition fieldwisebW (f g : fe25519W) : bool := + Eval cbv beta iota delta [proj1_sig fieldwisebW_sig] in + let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in + let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9) := g in + proj1_sig (fieldwisebW_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) + (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9)). + +Lemma fieldwisebW_correct f g + : fieldwisebW f g = GF25519.fieldwiseb (fe25519WToZ f) (fe25519WToZ g). +Proof. + set (f' := f); set (g' := g). + hnf in f, g; destruct_head' prod. + exact (proj2_sig (fieldwisebW_sig f' g')). +Qed. + +Local Arguments freezeW : simpl never. + +Definition eqbW_sig (f g : fe25519W) + : { b | is_bounded (fe25519WToZ f) = true + -> is_bounded (fe25519WToZ g) = true + -> b = GF25519.eqb (fe25519WToZ f) (fe25519WToZ g) }. +Proof. + pose proof (fun pf => proj1 (freezeW_correct_and_bounded f pf)) as frf. + pose proof (fun pf => proj1 (freezeW_correct_and_bounded g pf)) as frg. + hnf in f, g; destruct_head' prod. + eexists. + unfold GF25519.eqb. + simpl @fe25519WToZ in *; cbv beta iota. + intros. + rewrite <- frf, <- frg by assumption. + rewrite <- fieldwisebW_correct. + reflexivity. +Defined. + +Definition eqbW (f g : fe25519W) : bool := + Eval cbv beta iota delta [proj1_sig eqbW_sig] in + let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in + let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9) := g in + proj1_sig (eqbW_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) + (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9)). + +Lemma eqbW_correct f g + : is_bounded (fe25519WToZ f) = true + -> is_bounded (fe25519WToZ g) = true + -> eqbW f g = GF25519.eqb (fe25519WToZ f) (fe25519WToZ g). +Proof. + set (f' := f); set (g' := g). + hnf in f, g; destruct_head' prod. + exact (proj2_sig (eqbW_sig f' g')). +Qed. + +Definition sqrt_m1W : fe25519W := + Eval vm_compute in fe25519ZToW sqrt_m1. + +Definition sqrtW_sig + : { sqrtW | iunop_correct_and_bounded sqrtW GF25519.sqrt }. +Proof. + eexists. + unfold GF25519.sqrt. + intros; rewrite <- (fun pf => proj1 (powW_correct_and_bounded _ _ pf)) by assumption. + match goal with + | [ |- context G[dlet x := fe25519WToZ ?v in @?f x] ] + => let G' := context G[dlet x := v in f (fe25519WToZ x)] in + cut G'; cbv beta; + [ cbv [Let_In]; exact (fun x => x) | ] + end. + split. + { etransitivity. + Focus 2. { + apply Proper_Let_In_nd_changebody_eq; intros. + set_evars. + change sqrt_m1 with (fe25519WToZ sqrt_m1W). + rewrite <- !(fun X Y => proj1 (mulW_correct_and_bounded _ _ X Y)), <- eqbW_correct, (pull_bool_if fe25519WToZ) + by repeat match goal with + | _ => progress subst + | [ |- is_bounded (fe25519WToZ ?op) = true ] + => lazymatch op with + | mulW _ _ => apply mulW_correct_and_bounded + | powW _ _ => apply powW_correct_and_bounded + | sqrt_m1W => vm_compute; reflexivity + | _ => assumption + end + end. + subst_evars; reflexivity. + } Unfocus. + lazymatch goal with + | [ |- context G[dlet x := ?v in fe25519WToZ (@?f x)] ] + => let G' := context G[fe25519WToZ (dlet x := v in f x)] in + cut G'; cbv beta; + [ cbv [Let_In]; exact (fun x => x) | apply f_equal ] + end. + reflexivity. } + { cbv [Let_In]. + break_if. + { apply powW_correct_and_bounded; assumption. } + { apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ]. + apply powW_correct_and_bounded; assumption. } } +Defined. + +Definition sqrtW (f : fe25519W) : fe25519W := + Eval cbv beta iota delta [proj1_sig sqrtW_sig] in + let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in + proj1_sig sqrtW_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9). + +Lemma sqrtW_correct_and_bounded : iunop_correct_and_bounded sqrtW GF25519.sqrt. +Proof. + intro f. + set (f' := f). + hnf in f; destruct_head' prod. + assert (H : sqrtW f' = proj1_sig sqrtW_sig f') + by (subst f'; cbv beta iota delta [proj1_sig sqrtW_sig sqrtW]; reflexivity). + rewrite H. + exact (proj2_sig sqrtW_sig f'). +Qed. + +Definition add (f g : fe25519) : fe25519. +Proof. define_binop f g addW addW_correct_and_bounded. Defined. +Definition sub (f g : fe25519) : fe25519. +Proof. define_binop f g subW subW_correct_and_bounded. Defined. +Definition mul (f g : fe25519) : fe25519. +Proof. define_binop f g mulW mulW_correct_and_bounded. Defined. +Definition opp (f : fe25519) : fe25519. +Proof. define_unop f oppW oppW_correct_and_bounded. Defined. +Definition freeze (f : fe25519) : fe25519. +Proof. define_unop f freezeW freezeW_correct_and_bounded. Defined. + Definition pow (f : fe25519) (chain : list (nat * nat)) : fe25519. Proof. define_unop f (fun x => powW x chain) powW_correct_and_bounded. Defined. Definition inv (f : fe25519) : fe25519. Proof. define_unop f invW invW_correct_and_bounded. Defined. +Definition sqrt (f : fe25519) : fe25519. +Proof. define_unop f sqrtW sqrtW_correct_and_bounded. Defined. -Local Ltac unop_correct_t op opW rop_correct_and_bounded := - cbv [op opW]; rewrite proj1_fe25519_exist_fe25519W; - rewrite (fun X => proj1 (rop_correct_and_bounded _ X)) by apply is_bounded_proj1_fe25519; - try reflexivity. -Local Ltac binop_correct_t op opW rop_correct_and_bounded := - cbv [op opW]; rewrite proj1_fe25519_exist_fe25519W; - rewrite (fun X Y => proj1 (rop_correct_and_bounded _ _ X Y)) by apply is_bounded_proj1_fe25519; - try reflexivity. +Local Ltac op_correct_t op opW_correct_and_bounded := + cbv [op]; rewrite proj1_fe25519_exist_fe25519W; + apply opW_correct_and_bounded; apply is_bounded_proj1_fe25519. Lemma add_correct (f g : fe25519) : proj1_fe25519 (add f g) = carry_add (proj1_fe25519 f) (proj1_fe25519 g). -Proof. binop_correct_t add addW radd_correct_and_bounded. Qed. +Proof. op_correct_t add addW_correct_and_bounded. Qed. Lemma sub_correct (f g : fe25519) : proj1_fe25519 (sub f g) = carry_sub (proj1_fe25519 f) (proj1_fe25519 g). -Proof. binop_correct_t sub subW rsub_correct_and_bounded. Qed. +Proof. op_correct_t sub subW_correct_and_bounded. Qed. Lemma mul_correct (f g : fe25519) : proj1_fe25519 (mul f g) = GF25519.mul (proj1_fe25519 f) (proj1_fe25519 g). -Proof. binop_correct_t mul mulW rmul_correct_and_bounded. Qed. +Proof. op_correct_t mul mulW_correct_and_bounded. Qed. Lemma opp_correct (f : fe25519) : proj1_fe25519 (opp f) = carry_opp (proj1_fe25519 f). -Proof. unop_correct_t opp oppW ropp_correct_and_bounded. Qed. +Proof. op_correct_t opp oppW_correct_and_bounded. Qed. Lemma freeze_correct (f : fe25519) : proj1_fe25519 (freeze f) = GF25519.freeze (proj1_fe25519 f). -Proof. unop_correct_t freeze freezeW rfreeze_correct_and_bounded. Qed. +Proof. op_correct_t freeze freezeW_correct_and_bounded. Qed. Lemma pow_correct (f : fe25519) chain : proj1_fe25519 (pow f chain) = GF25519.pow (proj1_fe25519 f) chain. -Proof. unop_correct_t pow pow (powW_correct_and_bounded chain). Qed. +Proof. op_correct_t pow (powW_correct_and_bounded chain). Qed. Lemma inv_correct (f : fe25519) : proj1_fe25519 (inv f) = GF25519.inv (proj1_fe25519 f). -Proof. unop_correct_t inv inv invW_correct_and_bounded. Qed. +Proof. op_correct_t inv invW_correct_and_bounded. Qed. +Lemma sqrt_correct (f : fe25519) : proj1_fe25519 (sqrt f) = GF25519.sqrt (proj1_fe25519 f). +Proof. op_correct_t sqrt sqrtW_correct_and_bounded. Qed. Import Morphisms. @@ -144,4 +292,4 @@ Proof. { reflexivity. } Qed. -(** TODO: pack, unpack, sqrt *) +(** TODO: pack, unpack *) diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v index 6e2213ee7..e044aa170 100644 --- a/src/Specific/GF25519BoundedCommon.v +++ b/src/Specific/GF25519BoundedCommon.v @@ -25,6 +25,10 @@ Definition word64 := Word.word 64. Coercion word64ToZ (x : word64) : Z := Z.of_N (wordToN x). Coercion ZToWord64 (x : Z) : word64 := NToWord _ (Z.to_N x). +Definition w64eqb (x y : word64) := weqb x y. + +Lemma word64eqb_Zeqb x y : (word64ToZ x =? word64ToZ y)%Z = w64eqb x y. +Proof. apply wordeqb_Zeqb. Qed. (* END aliases for word extraction *) @@ -39,8 +43,22 @@ Qed. (* BEGIN precomputation. *) Local Notation b_of exp := (0, 2^exp + 2^(exp-3))%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *) -Local Notation Z_of exp := { v : Z | fst (b_of exp) <= v <= snd (b_of exp) }. -Local Notation word_of exp := { v : word64 | fst (b_of exp) <= v <= snd (b_of exp) }. +Record bounded_word (lower upper : Z) := + Build_bounded_word' + { proj_word :> word64; + word_bounded : andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true }. +Arguments proj_word {_ _} _. +Arguments word_bounded {_ _} _. +Arguments Build_bounded_word' {_ _} _ _. +Definition Build_bounded_word {lower upper} (proj_word : word64) (word_bounded : andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true) + : bounded_word lower upper + := Build_bounded_word' + proj_word + (match andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z as b return b = true -> b = true with + | true => fun _ => eq_refl + | false => fun x => x + end word_bounded). +Local Notation word_of exp := (bounded_word (fst (b_of exp)) (snd (b_of exp))). Definition bounds : list (Z * Z) := Eval compute in [b_of 25; b_of 26; b_of 25; b_of 26; b_of 25; b_of 26; b_of 25; b_of 26; b_of 25; b_of 26]. @@ -58,8 +76,8 @@ Definition fe25519 := (word_of 25 * word_of 26 * word_of 25 * word_of 26 * word_of 25 * word_of 26 * word_of 25 * word_of 26 * word_of 25 * word_of 26)%type. Definition proj1_fe25519W (x : fe25519) : fe25519W := let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in - (proj1_sig x0, proj1_sig x1, proj1_sig x2, proj1_sig x3, proj1_sig x4, - proj1_sig x5, proj1_sig x6, proj1_sig x7, proj1_sig x8, proj1_sig x9). + (proj_word x0, proj_word x1, proj_word x2, proj_word x3, proj_word x4, + proj_word x5, proj_word x6, proj_word x7, proj_word x8, proj_word x9). Coercion proj1_fe25519 (x : fe25519) : Specific.GF25519.fe25519 := fe25519WToZ (proj1_fe25519W x). Definition is_bounded (x : Specific.GF25519.fe25519) : bool @@ -72,40 +90,22 @@ Definition is_bounded (x : Specific.GF25519.fe25519) : bool Lemma is_bounded_proj1_fe25519 (x : fe25519) : is_bounded (proj1_fe25519 x) = true. Proof. - refine (let '(exist x0 p0, exist x1 p1, exist x2 p2, exist x3 p3, exist x4 p4, - exist x5 p5, exist x6 p6, exist x7 p7, exist x8 p8, exist x9 p9) + refine (let '(Build_bounded_word' x0 p0, Build_bounded_word' x1 p1, Build_bounded_word' x2 p2, Build_bounded_word' x3 p3, Build_bounded_word' x4 p4, + Build_bounded_word' x5 p5, Build_bounded_word' x6 p6, Build_bounded_word' x7 p7, Build_bounded_word' x8 p8, Build_bounded_word' x9 p9) as x := x return is_bounded (proj1_fe25519 x) = true in _). - cbv [is_bounded proj1_fe25519 proj1_fe25519W fe25519WToZ to_list length bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map List.rev List.app proj1_sig]. + cbv [is_bounded proj1_fe25519 proj1_fe25519W fe25519WToZ to_list length bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map List.rev List.app proj_word]. apply fold_right_andb_true_iff_fold_right_and_True. cbv [fold_right List.map]. cbv beta in *. - repeat split; rewrite !Bool.andb_true_iff, !Z.leb_le; - assumption. + repeat split; assumption. Qed. -(* Make small [vm_computable] versions of proofs *) -Definition correct_le_le {l v u} : l <= v <= u -> l <= v <= u. -Proof. - intro pf; pose proof (proj1 pf) as pf1; pose proof (proj2 pf) as pf2; clear pf; - split; hnf in *; - lazymatch goal with - | [ H : ?x = Gt -> False |- ?x = Gt -> False ] - => revert H; - refine match x as y return (y = Gt -> False) -> y = Gt -> False with - | Gt => fun f => f - | _ => fun _ pf => match pf with - | eq_refl => I - end - end - end. -Defined. - (** TODO: Turn this into a lemma to speed up proofs *) Ltac unfold_is_bounded_in H := unfold is_bounded, fe25519WToZ in H; cbv [to_list length bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app] in H; - rewrite !Bool.andb_true_iff, !Z.leb_le in H. + rewrite !Bool.andb_true_iff in H. Definition Pow2_64 := Eval compute in 2^64. Definition unfold_Pow2_64 : 2^64 = Pow2_64 := eq_refl. @@ -113,8 +113,8 @@ Definition unfold_Pow2_64 : 2^64 = Pow2_64 := eq_refl. Definition exist_fe25519W (x : fe25519W) : is_bounded (fe25519WToZ x) = true -> fe25519. Proof. refine (let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) as x := x return is_bounded (fe25519WToZ x) = true -> fe25519 in - fun H => (fun H' => (exist _ x0 _, exist _ x1 _, exist _ x2 _, exist _ x3 _, exist _ x4 _, - exist _ x5 _, exist _ x6 _, exist _ x7 _, exist _ x8 _, exist _ x9 _)) + fun H => (fun H' => (Build_bounded_word x0 _, Build_bounded_word x1 _, Build_bounded_word x2 _, Build_bounded_word x3 _, Build_bounded_word x4 _, + Build_bounded_word x5 _, Build_bounded_word x6 _, Build_bounded_word x7 _, Build_bounded_word x8 _, Build_bounded_word x9 _)) (let H' := proj1 (@fold_right_andb_true_iff_fold_right_and_True _) H in _)); [ @@ -122,7 +122,8 @@ Proof. | clearbody H'; clear H x; unfold_is_bounded_in H'; exact H' ]; - destruct_head and; auto. + destruct_head and; auto; + rewrite_hyp !*; reflexivity. Defined. Definition exist_fe25519' (x : Specific.GF25519.fe25519) : is_bounded x = true -> fe25519. @@ -133,6 +134,7 @@ Proof. pose proof H as H'; unfold_is_bounded_in H; destruct_head and; + Z.ltb_to_lt; rewrite !ZToWord64ToZ by (simpl; omega); assumption ). @@ -144,11 +146,11 @@ Proof. fun H => _). let v := constr:(exist_fe25519' (x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) H) in let rec do_refine v := - first [ let v' := (eval cbv [exist_fe25519W fe25519ZToW exist_fe25519' proj1_sig snd fst] in (proj1_sig v)) in - refine (exist _ v' (correct_le_le _)); abstract exact (proj2_sig v) - | let v' := (eval cbv [exist_fe25519W fe25519ZToW exist_fe25519' proj1_sig snd fst] in (proj1_sig (snd v))) in - refine (_, exist _ v' (correct_le_le _)); - [ do_refine (fst v) | abstract exact (proj2_sig (snd v)) ] ] in + first [ let v' := (eval cbv [exist_fe25519W fe25519ZToW exist_fe25519' proj_word Build_bounded_word snd fst] in (proj_word v)) in + refine (Build_bounded_word v' _); abstract exact (word_bounded v) + | let v' := (eval cbv [exist_fe25519W fe25519ZToW exist_fe25519' proj_word Build_bounded_word snd fst] in (proj_word (snd v))) in + refine (_, Build_bounded_word v' _); + [ do_refine (fst v) | abstract exact (word_bounded (snd v)) ] ] in do_refine v. Defined. @@ -171,9 +173,10 @@ Proof. revert pf. refine (let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) as x := x return forall pf : is_bounded x = true, proj1_fe25519 (exist_fe25519 x pf) = x in fun pf => _). - cbv [proj1_fe25519 exist_fe25519 proj1_fe25519W fe25519WToZ proj1_sig]. + cbv [proj1_fe25519 exist_fe25519 proj1_fe25519W fe25519WToZ proj_word Build_bounded_word]. unfold_is_bounded_in pf. destruct_head and. + Z.ltb_to_lt. rewrite !ZToWord64ToZ by (rewrite unfold_Pow2_64; cbv [Pow2_64]; omega). reflexivity. Qed. @@ -182,9 +185,9 @@ Qed. (* Precompute constants *) -Definition one := Eval cbv -[Z.le] in exist_fe25519 Specific.GF25519.one_ eq_refl. +Definition one := Eval vm_compute in exist_fe25519 Specific.GF25519.one_ eq_refl. -Definition zero := Eval cbv -[Z.le] in exist_fe25519 Specific.GF25519.zero_ eq_refl. +Definition zero := Eval vm_compute in exist_fe25519 Specific.GF25519.zero_ eq_refl. Lemma fold_chain_opt_gen {A B} (F : A -> B) is_bounded ls id' op' id op chain (Hid_bounded : is_bounded (F id') = true) @@ -233,7 +236,7 @@ Proof. cbv [Z.pow_pos Z.mul Pos.mul Pos.iter nth_default nth_error value] in *. unfold is_bounded. apply fold_right_andb_true_iff_fold_right_and_True. - cbv [is_bounded proj1_fe25519 to_list length bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map List.rev List.app proj1_sig fold_right]. + cbv [is_bounded proj1_fe25519 to_list length bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map List.rev List.app proj_word fold_right]. repeat split; rewrite !Bool.andb_true_iff, !Z.leb_le; omega. Qed. diff --git a/src/Util/Bool.v b/src/Util/Bool.v index 5293268df..7b94c503e 100644 --- a/src/Util/Bool.v +++ b/src/Util/Bool.v @@ -41,3 +41,13 @@ Hint Rewrite Bool.orb_andb_distrib_r Bool.orb_andb_distrib_l : push_orb. Hint Rewrite <- Bool.andb_orb_distrib_r Bool.andb_orb_distrib_l : push_orb. Hint Rewrite <- Bool.orb_andb_distrib_r Bool.orb_andb_distrib_l : pull_orb. Hint Rewrite Bool.andb_orb_distrib_r Bool.andb_orb_distrib_l : pull_orb. + +Definition pull_bool_if_dep {A B} (f : forall b : bool, A b -> B b) (b : bool) (x : A true) (y : A false) + : (if b return B b then f _ x else f _ y) = f b (if b return A b then x else y) + := if b return ((if b return B b then f _ x else f _ y) = f b (if b return A b then x else y)) + then eq_refl + else eq_refl. + +Definition pull_bool_if {A B} (f : A -> B) (b : bool) (x : A) (y : A) + : (if b then f x else f y) = f (if b then x else y) + := @pull_bool_if_dep (fun _ => A) (fun _ => B) (fun _ => f) b x y. diff --git a/src/Util/LetIn.v b/src/Util/LetIn.v index db09baf9c..12e1e6d43 100644 --- a/src/Util/LetIn.v +++ b/src/Util/LetIn.v @@ -20,6 +20,10 @@ Global Instance Proper_Let_In_nd_changevalue {A B} (RA:relation A) {RB:relation : Proper (RA ==> (RA ==> RB) ==> RB) (Let_In (P:=fun _=>B)). Proof. cbv; intuition. Qed. +Lemma Proper_Let_In_nd_changebody_eq {A P R} {Reflexive_R:@Reflexive P R} {x} + : Proper ((fun f g => forall a, x = a -> R (f a) (g a)) ==> R) (@Let_In A (fun _ => P) x). +Proof. lazy; intros; subst; auto; congruence. Qed. + Definition app_Let_In_nd {A B T} (f:B->T) (e:A) (C:A->B) : f (Let_In e C) = Let_In e (fun v => f (C v)) := eq_refl. diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index a89d02364..f2ceb047f 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -140,4 +140,21 @@ Lemma wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w) Admitted. Lemma wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordToNat w) mod (2^a). -Admitted.
\ No newline at end of file +Admitted. + +Lemma wordeqb_Zeqb {sz} (x y : word sz) : (Z.of_N (wordToN x) =? Z.of_N (wordToN y))%Z = weqb x y. +Proof. + match goal with |- ?LHS = ?RHS => destruct LHS eqn:HL, RHS eqn:HR end; + repeat match goal with + | _ => reflexivity + | _ => progress unfold not in * + | [ H : Z.eqb _ _ = true |- _ ] => apply Z.eqb_eq in H + | [ |- Z.eqb _ _ = true ] => apply Z.eqb_eq + | [ H : context[Z.of_N _ = Z.of_N _] |- _ ] => rewrite N2Z.inj_iff in H + | [ H : wordToN _ = wordToN _ |- _ ] => apply wordToN_inj in H + | [ H : x = y :> word _ |- _ ] => apply weqb_true_iff in H + | [ H : ?x = false |- _ ] => progress rewrite <- H; clear H + | _ => congruence + | [ H : weqb _ _ = true |- _ ] => apply weqb_true_iff in H; subst + end. +Qed. |