diff options
Diffstat (limited to 'src/Specific/NISTP256/FancyMachine256')
| -rw-r--r-- | src/Specific/NISTP256/FancyMachine256/Barrett.v | 155 | ||||
| -rw-r--r-- | src/Specific/NISTP256/FancyMachine256/Core.v | 339 | ||||
| -rw-r--r-- | src/Specific/NISTP256/FancyMachine256/Montgomery.v | 157 |
3 files changed, 0 insertions, 651 deletions
diff --git a/src/Specific/NISTP256/FancyMachine256/Barrett.v b/src/Specific/NISTP256/FancyMachine256/Barrett.v deleted file mode 100644 index 9c3b55485..000000000 --- a/src/Specific/NISTP256/FancyMachine256/Barrett.v +++ /dev/null @@ -1,155 +0,0 @@ -Require Import Crypto.Specific.NISTP256.FancyMachine256.Core. -Require Import LegacyArithmetic.BarretReduction. -Require Import Crypto.Arithmetic.BarrettReduction.HAC. - -(** Useful for arithmetic in the field of integers modulo the order of the curve25519 base point *) -Section expression. - Let b : Z := 2. - Let k : Z := 253. - Let offset : Z := 3. - Context (ops : fancy_machine.instructions (2 * 128)) (props : fancy_machine.arithmetic ops). - Context (m μ : Z) - (m_pos : 0 < m). - Let base_pos : 0 < b. reflexivity. Qed. - Context (k_good : m < b^k) - (μ_good : μ = b^(2*k) / m) (* [/] is [Z.div], which is truncated *). - Let offset_nonneg : 0 <= offset. unfold offset; omega. Qed. - Let k_big_enough : offset <= k. unfold offset, k; omega. Qed. - Context (m_small : 3 * m <= b^(k+offset)) - (m_large : b^(k-offset) <= m + 1). - Context (H : 0 <= m < 2^256). - Let H' : 0 <= 250 <= 256. omega. Qed. - Let H'' : 0 < 250. omega. Qed. - Local Notation SmallT := (@ZBounded.SmallT (2 ^ 256) (2 ^ 250) m - (@ZLikeOps_of_ArchitectureBoundedOps 128 ops m _)). - Definition ldi' : load_immediate SmallT := _. - Let isldi : is_load_immediate ldi' := _. - Context (μ_range : 0 <= b ^ (2 * k) / m < b ^ (k + offset)). - Definition μ' : SmallT := ldi' μ. - Let μ'_eq : ZBounded.decode_small μ' = μ. - Proof. - unfold ZBounded.decode_small, ZLikeOps_of_ArchitectureBoundedOps, μ'. - apply (decode_load_immediate _ _). - rewrite μ_good; apply μ_range. - Qed. - - Let props' - ldi_modulus ldi_0 Hldi_modulus Hldi_0 - := ZLikeProperties_of_ArchitectureBoundedOps_Factored ops m ldi_modulus ldi_0 Hldi_modulus Hldi_0 H 250 H' H''. - - Definition pre_f' ldi_modulus ldi_0 ldi_μ Hldi_modulus Hldi_0 (Hldi_μ : ldi_μ = ldi' μ) - := (fun v => (@barrett_reduce m b k μ offset m_pos base_pos μ_good offset_nonneg k_big_enough m_small m_large _ (props' ldi_modulus ldi_0 Hldi_modulus Hldi_0) ldi_μ I (eq_trans (f_equal _ Hldi_μ) μ'_eq) (fst v, snd v))). - - Definition pre_f := pre_f' _ _ _ eq_refl eq_refl eq_refl. - - Local Arguments μ' / . - Local Arguments ldi' / . - Local Arguments Core.mul_double / _ _ _ _ _ _ _ _ _ _. - Local Opaque Let_In Let_In_pf. - - Definition expression' - := Eval simpl in - (fun v => pflet ldi_modulus, Hldi_modulus := fancy_machine.ldi m in - pflet ldi_μ, Hldi_μ := fancy_machine.ldi μ in - pflet ldi_0, Hldi_0 := fancy_machine.ldi 0 in - proj1_sig (pre_f' ldi_modulus ldi_0 ldi_μ Hldi_modulus Hldi_0 Hldi_μ v)). - Local Transparent Let_In Let_In_pf. - Definition expression - := Eval cbv beta iota delta [expression' fst snd Let_In Let_In_pf] in expression'. - - Definition expression_eq v (H : 0 <= _ < _) : fancy_machine.decode (expression v) = _ - := proj1 (proj2_sig (pre_f v) H). -End expression. - -Section reflected. - Context (ops : fancy_machine.instructions (2 * 128)). - Local Notation tZ := (Tbase TZ). - Local Notation tW := (Tbase TW). - Definition rexpression : Syntax.Expr base_type op (Arrow (tZ * tZ * tW * tW) tW). - Proof. - let v := (eval cbv beta delta [expression] in (fun mμxy => let '(mv, μv, xv, yv) := mμxy in expression ops mv μv (xv, yv))) in - let v := Reify v in - exact v. - Defined. - - Definition rexpression_simple := Eval vm_compute in rexpression. - - (*Compute DefaultRegisters rexpression_simple.*) - - Definition registers - := [RegMod; RegMuLow; x; xHigh; RegMod; RegMuLow; RegZero; tmp; q; qHigh; scratch+3; - SpecialCarryBit; q; SpecialCarryBit; qHigh; scratch+3; SpecialCarryBit; q; SpecialCarryBit; qHigh; tmp; - scratch+3; SpecialCarryBit; tmp; scratch+3; SpecialCarryBit; tmp; SpecialCarryBit; tmp; q; out]. - - Definition compiled_syntax - := Eval lazy in AssembleSyntax rexpression_simple registers. - - Context (m μ : Z) - (props : fancy_machine.arithmetic ops). - - Let result (v : Tuple.tuple fancy_machine.W 2) := Syntax.Interp (@interp_op _) rexpression_simple (m, μ, fst v, snd v). - Let assembled_result (v : Tuple.tuple fancy_machine.W 2) : fancy_machine.W := Core.Interp compiled_syntax (m, μ, fst v, snd v). - - Theorem sanity : result = expression ops m μ. - Proof using Type. - reflexivity. - Qed. - - Theorem assembled_sanity : assembled_result = expression ops m μ. - Proof using Type. - reflexivity. - Qed. - - Section correctness. - Let b : Z := 2. - Let k : Z := 253. - Let offset : Z := 3. - Context (H0 : 0 < m) - (H1 : μ = b^(2 * k) / m) - (H2 : 3 * m <= b^(k + offset)) - (H3 : b^(k - offset) <= m + 1) - (H4 : 0 <= m < 2^(k + offset)) - (H5 : 0 <= b^(2 * k) / m < b^(k + offset)) - (v : Tuple.tuple fancy_machine.W 2) - (H6 : 0 <= decode v < b^(2 * k)). - Theorem correctness : fancy_machine.decode (result v) = decode v mod m. - Proof using H0 H1 H2 H3 H4 H5 H6 props. - rewrite sanity; destruct v. - apply expression_eq; assumption. - Qed. - Theorem assembled_correctness : fancy_machine.decode (assembled_result v) = decode v mod m. - Proof using H0 H1 H2 H3 H4 H5 H6 props. - rewrite assembled_sanity; destruct v. - apply expression_eq; assumption. - Qed. - End correctness. -End reflected. - -Print compiled_syntax. -(* compiled_syntax = -fun ops : fancy_machine.instructions (2 * 128) => -λn (RegMod, RegMuLow, x, xHigh), -nlet RegMod := RegMod in -nlet RegMuLow := RegMuLow in -nlet RegZero := ldi 0 in -c.Rshi(tmp, xHigh, x, 250), -c.Mul128(q, c.LowerHalf(tmp), c.LowerHalf(RegMuLow)), -c.Mul128(qHigh, c.UpperHalf(tmp), c.UpperHalf(RegMuLow)), -c.Mul128(scratch+3, c.UpperHalf(tmp), c.LowerHalf(RegMuLow)), -c.Add(q, q, c.LeftShifted{scratch+3, 128}), -c.Addc(qHigh, qHigh, c.RightShifted{scratch+3, 128}), -c.Mul128(scratch+3, c.UpperHalf(RegMuLow), c.LowerHalf(tmp)), -c.Add(q, q, c.LeftShifted{scratch+3, 128}), -c.Addc(qHigh, qHigh, c.RightShifted{scratch+3, 128}), -c.Mul128(tmp, c.LowerHalf(qHigh), c.LowerHalf(RegMod)), -c.Mul128(scratch+3, c.UpperHalf(qHigh), c.LowerHalf(RegMod)), -c.Add(tmp, tmp, c.LeftShifted{scratch+3, 128}), -c.Mul128(scratch+3, c.UpperHalf(RegMod), c.LowerHalf(qHigh)), -c.Add(tmp, tmp, c.LeftShifted{scratch+3, 128}), -c.Sub(tmp, x, tmp), -c.Addm(q, tmp, RegZero), -c.Addm(out, q, RegZero), -Return out - : forall ops : fancy_machine.instructions (2 * 128), - expr base_type op Register (Tbase TZ * Tbase TZ * Tbase TW * Tbase TW -> Tbase TW) -*) diff --git a/src/Specific/NISTP256/FancyMachine256/Core.v b/src/Specific/NISTP256/FancyMachine256/Core.v deleted file mode 100644 index 881fa2e1e..000000000 --- a/src/Specific/NISTP256/FancyMachine256/Core.v +++ /dev/null @@ -1,339 +0,0 @@ -(** * A Fancy Machine with 256-bit registers *) -Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms. -Require Import Coq.PArith.BinPos Coq.micromega.Psatz. -Require Export Coq.ZArith.ZArith Coq.Lists.List. -Require Import Crypto.Util.Decidable. -Require Export Crypto.LegacyArithmetic.Interface. -Require Export Crypto.LegacyArithmetic.ArchitectureToZLike. -Require Export Crypto.LegacyArithmetic.ArchitectureToZLikeProofs. -Require Export Crypto.Util.Tuple. -Require Import Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod. -Require Import Crypto.Compilers.Named.Context. -Require Export Crypto.Compilers.Named.Syntax. -Require Export Crypto.Compilers.Named.PositiveContext. -Require Import Crypto.Compilers.Named.DeadCodeElimination. -Require Import Crypto.Compilers.CountLets. -Require Import Crypto.Compilers.Named.ContextOn. -Require Import Crypto.Compilers.Named.Wf. -Require Export Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Linearize. -Require Import Crypto.Compilers.Inline. -Require Import Crypto.Compilers.CommonSubexpressionElimination. -Require Export Crypto.Compilers.Reify. -Require Export Crypto.Util.Option. -Require Export Crypto.Util.Notations. -Require Import Crypto.Util.ListUtil. -Require Export Crypto.Util.LetIn. -Require Import Crypto.Util.Tactics.BreakMatch. -Export ListNotations. - -Open Scope Z_scope. -Local Notation eta x := (fst x, snd x). -Local Notation eta3 x := (eta (fst x), snd x). -Local Notation eta3' x := (fst x, eta (snd x)). - -(** ** Reflective Assembly Syntax *) -Section reflection. - Context {ops : fancy_machine.instructions (2 * 128)}. - Local Set Boolean Equality Schemes. - Local Set Decidable Equality Schemes. - Inductive base_type := TZ | Tbool | TW. - Global Instance dec_base_type : DecidableRel (@eq base_type) - := base_type_eq_dec. - Definition interp_base_type (v : base_type) : Type := - match v with - | TZ => Z - | Tbool => bool - | TW => fancy_machine.W - end. - Local Notation tZ := (Tbase TZ). - Local Notation tbool := (Tbase Tbool). - Local Notation tW := (Tbase TW). - Local Open Scope ctype_scope. - Inductive op : flat_type base_type -> flat_type base_type -> Type := - | OPconst t : interp_base_type t -> op Unit (Tbase t) - | OPldi : op tZ tW - | OPshrd : op (tW * tW * tZ) tW - | OPshl : op (tW * tZ) tW - | OPshr : op (tW * tZ) tW - | OPadc : op (tW * tW * tbool) (tbool * tW) - | OPsubc : op (tW * tW * tbool) (tbool * tW) - | OPmulhwll : op (tW * tW) tW - | OPmulhwhl : op (tW * tW) tW - | OPmulhwhh : op (tW * tW) tW - | OPselc : op (tbool * tW * tW) tW - | OPaddm : op (tW * tW * tW) tW. - - Definition is_const s d (v : op s d) : bool - := match v with OPconst _ _ => true | _ => false end. - - Definition interp_op src dst (f : op src dst) - : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst - := match f in op s d return interp_flat_type _ s -> interp_flat_type _ d with - | OPconst _ v => fun _ => v - | OPldi => ldi - | OPshrd => fun xyz => let '(x, y, z) := eta3 xyz in shrd x y z - | OPshl => fun xy => let '(x, y) := eta xy in shl x y - | OPshr => fun xy => let '(x, y) := eta xy in shr x y - | OPadc => fun xyz => let '(x, y, z) := eta3 xyz in adc x y z - | OPsubc => fun xyz => let '(x, y, z) := eta3 xyz in subc x y z - | OPmulhwll => fun xy => let '(x, y) := eta xy in mulhwll x y - | OPmulhwhl => fun xy => let '(x, y) := eta xy in mulhwhl x y - | OPmulhwhh => fun xy => let '(x, y) := eta xy in mulhwhh x y - | OPselc => fun xyz => let '(x, y, z) := eta3 xyz in selc x y z - | OPaddm => fun xyz => let '(x, y, z) := eta3 xyz in addm x y z - end. - - Inductive op_code : Type := - | SOPconstb (v : bool) | SOPconstZ (v : Z) | SOPconstW - | SOPldi | SOPshrd | SOPshl | SOPshr | SOPadc | SOPsubc - | SOPmulhwll | SOPmulhwhl | SOPmulhwhh | SOPselc | SOPaddm. - - Definition symbolicify_op s d (v : op s d) : op_code - := match v with - | OPconst TZ v => SOPconstZ v - | OPconst Tbool v => SOPconstb v - | OPconst TW v => SOPconstW - | OPldi => SOPldi - | OPshrd => SOPshrd - | OPshl => SOPshl - | OPshr => SOPshr - | OPadc => SOPadc - | OPsubc => SOPsubc - | OPmulhwll => SOPmulhwll - | OPmulhwhl => SOPmulhwhl - | OPmulhwhh => SOPmulhwhh - | OPselc => SOPselc - | OPaddm => SOPaddm - end. - - Definition CSE {t} e := @CSE base_type op_code base_type_beq op_code_beq internal_base_type_dec_bl op symbolicify_op (fun _ x => x) true t e (fun _ => nil). - - Inductive inline_option := opt_inline | opt_default | opt_noinline. - - Definition postprocess var t (e : @exprf base_type op var t) - : @inline_directive base_type op var t - := let opt : inline_option - := match e with - | Op _ _ OPshl _ => opt_inline - | Op _ _ OPshr _ => opt_inline - | Op _ _ (OPconst _ _) _ => opt_inline - | _ => opt_default - end in - match opt with - | opt_noinline => no_inline e - | opt_default => default_inline e - | opt_inline => match t as t' return exprf _ _ t' -> inline_directive t' with - | Tbase _ => fun e => @inline _ _ _ (Tbase _) e - | _ => fun e => default_inline e - end e - end. - - Definition Inline {t} e := @InlineConstGen base_type op postprocess t e. -End reflection. - -Ltac base_reify_op op op_head expr ::= - lazymatch op_head with - | @Interface.ldi => constr:(reify_op op op_head 1 OPldi) - | @Interface.shrd => constr:(reify_op op op_head 3 OPshrd) - | @Interface.shl => constr:(reify_op op op_head 2 OPshl) - | @Interface.shr => constr:(reify_op op op_head 2 OPshr) - | @Interface.adc => constr:(reify_op op op_head 3 OPadc) - | @Interface.subc => constr:(reify_op op op_head 3 OPsubc) - | @Interface.mulhwll => constr:(reify_op op op_head 2 OPmulhwll) - | @Interface.mulhwhl => constr:(reify_op op op_head 2 OPmulhwhl) - | @Interface.mulhwhh => constr:(reify_op op op_head 2 OPmulhwhh) - | @Interface.selc => constr:(reify_op op op_head 3 OPselc) - | @Interface.addm => constr:(reify_op op op_head 3 OPaddm) - end. -Ltac base_reify_type T ::= - match T with - | Z => TZ - | bool => Tbool - | fancy_machine.W => TW - end. - -Ltac Reify' e := Reify.Reify' base_type (@interp_base_type _) (@op _) e. -Ltac Reify e := - let v := Reify.Reify base_type (@interp_base_type _) (@op _) (@OPconst _) e in - constr:(Inline ((*CSE _*) (InlineConst (@is_const _) (ANormal v)))). -(*Ltac Reify_rhs := Reify.Reify_rhs base_type (interp_base_type _) op (interp_op _).*) - -(** ** Raw Syntax Trees *) -(** These are used solely for pretty-printing the expression tree in a - form that can be basically copy-pasted into other languages which - can be compiled for the Fancy Machine. Hypothetically, we could - add support for custom named identifiers, by carrying around - [string] identifiers and using them for pretty-printing... It - might also be possible to verify this layer, too, by adding a - partial interpretation function... *) - -Local Set Decidable Equality Schemes. -Local Set Boolean Equality Schemes. - -Inductive Register := -| RegPInv | RegMod | RegMuLow | RegZero -| y | t1 | t2 | lo | hi | out | src1 | src2 | tmp | q | qHigh | x | xHigh -| SpecialCarryBit -| scratch | scratchplus (n : nat). - -Notation "'scratch+' n" := (scratchplus n) (format "'scratch+' n", at level 10). - -Definition pos_of_Register (r : Register) := - match r with - | RegPInv => 1 - | RegMod => 2 - | RegMuLow => 3 - | RegZero => 4 - | y => 5 - | t1 => 6 - | t2 => 7 - | lo => 8 - | hi => 9 - | out => 10 - | src1 => 11 - | src2 => 12 - | tmp => 13 - | q => 14 - | qHigh => 15 - | x => 16 - | xHigh => 17 - | SpecialCarryBit => 18 - | scratch => 19 - | scratchplus n => 19 + Pos.of_nat (S n) - end%positive. - -Lemma pos_of_Register_inj x y : pos_of_Register x = pos_of_Register y -> x = y. -Proof. - unfold pos_of_Register; repeat break_match; subst; - try rewrite Pos.add_cancel_l; try rewrite Nat2Pos.inj_iff; - try solve [ simpl; congruence | intros; exfalso; lia ]. -Qed. - -Definition RegisterContext {var : base_type -> Type} : Context Register var - := ContextOn pos_of_Register (PositiveContext _ _ base_type_beq internal_base_type_dec_bl). - -Definition syntax {ops : fancy_machine.instructions (2 * 128)} - := Named.expr base_type op Register. - -Class wf_empty {ops} {var} {t} (e : Named.expr base_type (@op ops) Register t) - := mk_wf_empty : @Wf.Named.wf base_type Register _ var RegisterContext empty t e. -Global Hint Extern 0 (wf_empty _) => vm_compute; intros; constructor : typeclass_instances. - -(** Assemble a well-typed easily interpretable expression into a - syntax tree we can use for pretty-printing. *) -Section assemble. - Context {ops : fancy_machine.instructions (2 * 128)}. - - Definition AssembleSyntax' {t} (e : Expr base_type op t) (ls : list Register) - : option (syntax t) - := CompileAndEliminateDeadCode (base_type_code_bl:=internal_base_type_dec_bl) (Context:=RegisterContext) e ls. - Definition AssembleSyntax {t} e ls (res := @AssembleSyntax' t e ls) - := match res return match res with None => _ | _ => _ end with - | Some v => v - | None => I - end. - - Definition dummy_registers (n : nat) : list Register - := List.map scratchplus (seq 0 n). - Definition DefaultRegisters {t} (e : Expr base_type op t) : list Register - := dummy_registers (CountBinders e). - - Definition DefaultAssembleSyntax {t} e := @AssembleSyntax t e (DefaultRegisters e). - - Definition Interp {t} e v - := invert_Some (@Named.Interp base_type interp_base_type op Register RegisterContext interp_op t e v). -End assemble. - -Export Compilers.Named.Syntax. -Open Scope nexpr_scope. -Open Scope ctype_scope. -Open Scope type_scope. -Open Scope core_scope. - -Notation Return x := (Var x). -Notation Const z := (Op (@OPconst _ _ z) TT). -Notation ldi z := (Op OPldi (Const z%Z)). -Notation "'nlet' x := A 'in' b" := (LetIn _ x (Op OPldi (Var A%nexpr)) b%nexpr) : nexpr_scope. -Notation "'c.Rshi' ( x , A , B , C ) , b" := - (LetIn _ x (Op OPshrd (Pair (Pair (Var A) (Var B)) (Const C%Z))) b) - (at level 200, b at level 200, format "'c.Rshi' ( x , A , B , C ) , '//' b"). -Notation "'c.Mul128' ( x , 'c.UpperHalf' ( A ) , 'c.UpperHalf' ( B ) ) , b" := - (LetIn _ x (Op OPmulhwhh (Pair (Var A) (Var B))) b) - (at level 200, b at level 200, format "'c.Mul128' ( x , 'c.UpperHalf' ( A ) , 'c.UpperHalf' ( B ) ) , '//' b"). -Notation "'c.Mul128' ( x , 'c.UpperHalf' ( A ) , 'c.LowerHalf' ( B ) ) , b" := - (LetIn _ x (Op OPmulhwhl (Pair (Var A) (Var B))) b) - (at level 200, b at level 200, format "'c.Mul128' ( x , 'c.UpperHalf' ( A ) , 'c.LowerHalf' ( B ) ) , '//' b"). -Notation "'c.Mul128' ( x , 'c.LowerHalf' ( A ) , 'c.LowerHalf' ( B ) ) , b" := - (LetIn _ x (Op OPmulhwll (Pair (Var A) (Var B))) b) - (at level 200, b at level 200, format "'c.Mul128' ( x , 'c.LowerHalf' ( A ) , 'c.LowerHalf' ( B ) ) , '//' b"). -Notation "'c.LeftShifted' { x , v }" := - (Op OPshl (Pair (Var x) (Const v%Z))) - (at level 200, format "'c.LeftShifted' { x , v }"). -Notation "'c.RightShifted' { x , v }" := - (Op OPshr (Pair (Var x) (Const v%Z))) - (at level 200, format "'c.RightShifted' { x , v }"). - -Notation "'c.Add' ( x , A , B ) , b" := - (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair A B) (Const false))) b) - (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' b"). -Notation "'c.Add' ( x , A , B ) , b" := - (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair (Var A) B) (Const false))) b) - (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' b"). -Notation "'c.Add' ( x , A , B ) , b" := - (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair A (Var B)) (Const false))) b) - (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' b"). -Notation "'c.Add' ( x , A , B ) , b" := - (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair (Var A) (Var B)) (Const false))) b) - (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' b"). -Notation "'c.Addc' ( x , A , B ) , b" := - (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair A B) (Var SpecialCarryBit))) b) - (at level 200, b at level 200, format "'c.Addc' ( x , A , B ) , '//' b"). -Notation "'c.Addc' ( x , A , B ) , b" := - (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair (Var A) B) (Var SpecialCarryBit))) b) - (at level 200, b at level 200, format "'c.Addc' ( x , A , B ) , '//' b"). -Notation "'c.Addc' ( x , A , B ) , b" := - (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair A (Var B)) (Var SpecialCarryBit))) b) - (at level 200, b at level 200, format "'c.Addc' ( x , A , B ) , '//' b"). -Notation "'c.Addc' ( x , A , B ) , b" := - (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair (Var A) (Var B)) (Var SpecialCarryBit))) b) - (at level 200, b at level 200, format "'c.Addc' ( x , A , B ) , '//' b"). - -Notation "'c.Sub' ( x , A , B ) , b" := - (LetIn _ (pair SpecialCarryBit x) (Op OPsubc (Pair (Pair A B) (Const false))) b) - (at level 200, b at level 200, format "'c.Sub' ( x , A , B ) , '//' b"). -Notation "'c.Sub' ( x , A , B ) , b" := - (LetIn _ (pair SpecialCarryBit x) (Op OPsubc (Pair (Pair (Var A) B) (Const false))) b) - (at level 200, b at level 200, format "'c.Sub' ( x , A , B ) , '//' b"). -Notation "'c.Sub' ( x , A , B ) , b" := - (LetIn _ (pair SpecialCarryBit x) (Op OPsubc (Pair (Pair A (Var B)) (Const false))) b) - (at level 200, b at level 200, format "'c.Sub' ( x , A , B ) , '//' b"). -Notation "'c.Sub' ( x , A , B ) , b" := - (LetIn _ (pair SpecialCarryBit x) (Op OPsubc (Pair (Pair (Var A) (Var B)) (Const false))) b) - (at level 200, b at level 200, format "'c.Sub' ( x , A , B ) , '//' b"). - -Notation "'c.Addm' ( x , A , B ) , b" := - (LetIn _ x (Op OPaddm (Pair (Pair A B) (Var RegMod))) b) - (at level 200, b at level 200, format "'c.Addm' ( x , A , B ) , '//' b"). -Notation "'c.Addm' ( x , A , B ) , b" := - (LetIn _ x (Op OPaddm (Pair (Pair (Var A) B) (Var RegMod))) b) - (at level 200, b at level 200, format "'c.Addm' ( x , A , B ) , '//' b"). -Notation "'c.Addm' ( x , A , B ) , b" := - (LetIn _ x (Op OPaddm (Pair (Pair A (Var B)) (Var RegMod))) b) - (at level 200, b at level 200, format "'c.Addm' ( x , A , B ) , '//' b"). -Notation "'c.Addm' ( x , A , B ) , b" := - (LetIn _ x (Op OPaddm (Pair (Pair (Var A) (Var B)) (Var RegMod))) b) - (at level 200, b at level 200, format "'c.Addm' ( x , A , B ) , '//' b"). - -Notation "'c.Selc' ( x , A , B ) , b" := - (LetIn _ x (Op OPselc (Pair (Pair (Var SpecialCarryBit) A) B)) b) - (at level 200, b at level 200, format "'c.Selc' ( x , A , B ) , '//' b"). -Notation "'c.Selc' ( x , A , B ) , b" := - (LetIn _ x (Op OPselc (Pair (Pair (Var SpecialCarryBit) (Var A)) B)) b) - (at level 200, b at level 200, format "'c.Selc' ( x , A , B ) , '//' b"). -Notation "'c.Selc' ( x , A , B ) , b" := - (LetIn _ x (Op OPselc (Pair (Pair (Var SpecialCarryBit) A) (Var B))) b) - (at level 200, b at level 200, format "'c.Selc' ( x , A , B ) , '//' b"). -Notation "'c.Selc' ( x , A , B ) , b" := - (LetIn _ x (Op OPselc (Pair (Pair (Var SpecialCarryBit) (Var A)) (Var B))) b) - (at level 200, b at level 200, format "'c.Selc' ( x , A , B ) , '//' b"). diff --git a/src/Specific/NISTP256/FancyMachine256/Montgomery.v b/src/Specific/NISTP256/FancyMachine256/Montgomery.v deleted file mode 100644 index 4caecca6b..000000000 --- a/src/Specific/NISTP256/FancyMachine256/Montgomery.v +++ /dev/null @@ -1,157 +0,0 @@ -Require Import Crypto.Specific.NISTP256.FancyMachine256.Core. -Require Import Crypto.LegacyArithmetic.MontgomeryReduction. -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. -Require Import Crypto.Util.ZUtil.EquivModulo. - -Section expression. - Context (ops : fancy_machine.instructions (2 * 128)) (props : fancy_machine.arithmetic ops) (modulus : Z) (m' : Z) (Hm : modulus <> 0) (H : 0 <= modulus < 2^256) (Hm' : 0 <= m' < 2^256). - Let H' : 0 <= 256 <= 256. omega. Qed. - Let H'' : 0 < 256. omega. Qed. - Definition ldi' : load_immediate - (@ZBounded.SmallT (2 ^ 256) (2 ^ 256) modulus - (@ZLikeOps_of_ArchitectureBoundedOps 128 ops modulus 256)) := _. - Let isldi : is_load_immediate ldi' := _. - Let props' - ldi_modulus ldi_0 Hldi_modulus Hldi_0 - := ZLikeProperties_of_ArchitectureBoundedOps_Factored ops modulus ldi_modulus ldi_0 Hldi_modulus Hldi_0 H 256 H' H''. - Definition pre_f' ldi_modulus ldi_0 Hldi_modulus Hldi_0 lm' - := (fun v => (reduce_via_partial (2^256) modulus (props := props' ldi_modulus ldi_0 Hldi_modulus Hldi_0) lm' I Hm (fst v, snd v))). - Definition pre_f := pre_f' _ _ eq_refl eq_refl (ldi' m'). - - Definition f := (fun v => pflet ldi_modulus, Hldi_modulus := ldi' modulus in - dlet lm' := ldi' m' in - pflet ldi_0, Hldi_0 := ldi' 0 in - proj1_sig (pre_f' ldi_modulus ldi_0 Hldi_modulus Hldi_0 lm' v)). - - Local Arguments proj1_sig _ _ !_ / . - Local Arguments ZBounded.CarryAdd / _ _ _ _ _ _. - Local Arguments ZBounded.ConditionalSubtract / _ _ _ _ _ _. - Local Arguments ZBounded.ConditionalSubtractModulus / _ _ _ _ _. - Local Arguments ZLikeOps_of_ArchitectureBoundedOps / _ _ _ _. - Local Arguments ZBounded.DivBy_SmallBound / _ _ _ _ _. - Local Arguments f / _. - Local Arguments pre_f' / _ _ _ _ _ _. - Local Arguments ldi' / . - Local Arguments reduce_via_partial / _ _ _ _ _ _ _ _. - Local Arguments Core.mul_double / _ _ _ _ _ _ _ _ _ _. - Local Opaque Let_In Let_In_pf. - - Definition expression' - := Eval simpl in f. - Local Transparent Let_In Let_In_pf. - Definition expression - := Eval cbv beta delta [expression' fst snd Let_In Let_In_pf] in expression'. - - Definition expression_eq v : fancy_machine.decode (expression v) = _ - := proj1 (proj2_sig (pre_f v) I). - Definition expression_correct - R' HR0 HR1 - v - Hv - : fancy_machine.decode (expression v) = _ - := @Crypto.LegacyArithmetic.MontgomeryReduction.reduce_via_partial_correct (2^256) modulus _ (props' _ _ eq_refl eq_refl) (ldi' m') I Hm R' HR0 HR1 (fst v, snd v) I Hv. -End expression. - -Section reflected. - Context (ops : fancy_machine.instructions (2 * 128)). - Local Notation tZ := (Tbase TZ). - Local Notation tW := (Tbase TW). - Definition rexpression : Syntax.Expr base_type op (Arrow (tZ * tZ * tW * tW) tW). - Proof. - let v := (eval cbv beta delta [expression] in - (fun modulus_m'_x_y => let '(modulusv, m'v, xv, yv) := modulus_m'_x_y in - expression ops modulusv m'v (xv, yv))) in - let v := Reify v in - exact v. - Defined. - - Definition rexpression_simple := Eval vm_compute in rexpression. - - (*Compute DefaultRegisters rexpression_simple.*) - - Definition registers - := [RegMod; RegPInv; lo; hi; RegMod; RegPInv; RegZero; y; t1; SpecialCarryBit; y; - t1; SpecialCarryBit; y; t1; t2; scratch+3; SpecialCarryBit; t1; SpecialCarryBit; t2; - scratch+3; SpecialCarryBit; t1; SpecialCarryBit; t2; SpecialCarryBit; lo; SpecialCarryBit; hi; y; - SpecialCarryBit; lo; lo]. - - Definition compiled_syntax - := Eval lazy in AssembleSyntax rexpression_simple registers. - - Context (modulus m' : Z) - (props : fancy_machine.arithmetic ops). - - Let result (v : Tuple.tuple fancy_machine.W 2) := Syntax.Interp interp_op rexpression_simple (modulus, m', fst v, snd v). - - Let assembled_result (v : Tuple.tuple fancy_machine.W 2) : fancy_machine.W := Core.Interp compiled_syntax (modulus, m', fst v, snd v). - - Theorem sanity : result = expression ops modulus m'. - Proof using Type. - reflexivity. - Qed. - - Theorem assembled_sanity : assembled_result = expression ops modulus m'. - Proof using Type. - reflexivity. - Qed. - - Local Infix "≡₂₅₆" := (Z.equiv_modulo (2^256)). - Local Infix "≡" := (Z.equiv_modulo modulus). - - Section correctness. - Context R' (* modular inverse of 2^256 *) - (H0 : modulus <> 0) - (H1 : 0 <= modulus < 2^256) - (H2 : 0 <= m' < 2^256) - (H3 : 2^256 * R' ≡ 1) - (H4 : modulus * m' ≡₂₅₆ -1) - (v : Tuple.tuple fancy_machine.W 2) - (H5 : 0 <= decode v <= 2^256 * modulus). - Theorem correctness - : fancy_machine.decode (result v) = (decode v * R') mod modulus. - Proof using H0 H1 H2 H3 H4 H5 props. - replace m' with (fancy_machine.decode (fancy_machine.ldi m')) - in H4 - by (apply decode_load_immediate; trivial; exact _). - rewrite sanity; destruct v; apply expression_correct; assumption. - Qed. - Theorem assembled_correctness - : fancy_machine.decode (assembled_result v) = (decode v * R') mod modulus. - Proof using H0 H1 H2 H3 H4 H5 props. - replace m' with (fancy_machine.decode (fancy_machine.ldi m')) - in H4 - by (apply decode_load_immediate; trivial; exact _). - rewrite assembled_sanity; destruct v; apply expression_correct; assumption. - Qed. - End correctness. -End reflected. - -Print compiled_syntax. -(* compiled_syntax = -fun ops : fancy_machine.instructions (2 * 128) => -λn (RegMod, RegPInv, lo, hi), -nlet RegMod := RegMod in -nlet RegPInv := RegPInv in -nlet RegZero := ldi 0 in -c.Mul128(y, c.LowerHalf(lo), c.LowerHalf(RegPInv)), -c.Mul128(t1, c.UpperHalf(lo), c.LowerHalf(RegPInv)), -c.Add(y, y, c.LeftShifted{t1, 128}), -c.Mul128(t1, c.UpperHalf(RegPInv), c.LowerHalf(lo)), -c.Add(y, y, c.LeftShifted{t1, 128}), -c.Mul128(t1, c.LowerHalf(y), c.LowerHalf(RegMod)), -c.Mul128(t2, c.UpperHalf(y), c.UpperHalf(RegMod)), -c.Mul128(scratch+3, c.UpperHalf(y), c.LowerHalf(RegMod)), -c.Add(t1, t1, c.LeftShifted{scratch+3, 128}), -c.Addc(t2, t2, c.RightShifted{scratch+3, 128}), -c.Mul128(scratch+3, c.UpperHalf(RegMod), c.LowerHalf(y)), -c.Add(t1, t1, c.LeftShifted{scratch+3, 128}), -c.Addc(t2, t2, c.RightShifted{scratch+3, 128}), -c.Add(lo, lo, t1), -c.Addc(hi, hi, t2), -c.Selc(y, RegMod, RegZero), -c.Sub(lo, hi, y), -c.Addm(lo, lo, RegZero), -Return lo - : forall ops : fancy_machine.instructions (2 * 128), - expr base_type op Register (Tbase TZ * Tbase TZ * Tbase TW * Tbase TW -> Tbase TW) -*) |