diff options
author | Jason Gross <jagro@google.com> | 2016-09-07 14:36:14 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-09-07 14:57:44 -0700 |
commit | 7e28bdd3ec3b2c715b9e9987c4668d1ec016671a (patch) | |
tree | 6b5991ecd0d407dccf4dc4674b0fa4a695df13b0 /src | |
parent | 054752ccf0b80bc413e70202a823fd034db6ea6b (diff) |
Add Barrett and Montgomery for the 256-bit machine
After | File Name | Before || Change
------------------------------------------------------------------------
0m12.69s | Total | 0m00.00s || +0m12.69s
------------------------------------------------------------------------
0m06.96s | Experiments/FancyMachineMontgomery256 | N/A || +0m06.96s
0m03.07s | Experiments/FancyMachineBarrett256 | N/A || +0m03.06s
0m02.67s | Experiments/FancyMachine256 | N/A || +0m02.67s
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/FancyMachine256.v | 359 | ||||
-rw-r--r-- | src/Experiments/FancyMachineBarrett256.v | 129 | ||||
-rw-r--r-- | src/Experiments/FancyMachineMontgomery256.v | 118 |
3 files changed, 606 insertions, 0 deletions
diff --git a/src/Experiments/FancyMachine256.v b/src/Experiments/FancyMachine256.v new file mode 100644 index 000000000..4fc6e3d1e --- /dev/null +++ b/src/Experiments/FancyMachine256.v @@ -0,0 +1,359 @@ +Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms. +Require Export Coq.ZArith.ZArith. +Require Export Crypto.BoundedArithmetic.Interface. +Require Export Crypto.BoundedArithmetic.ArchitectureToZLike. +Require Export Crypto.BoundedArithmetic.ArchitectureToZLikeProofs. +Require Export Crypto.Util.Tuple. +Require Import Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod. +Require Export Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Linearize. +Require Import Crypto.Reflection.CommonSubexpressionElimination. +Require Export Crypto.Reflection.Reify. +Require Export Crypto.Util.ZUtil. +Require Export Crypto.Util.Notations. + +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)). + +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. + 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 := + | OPldi : op tZ tW + | OPshrd : op (tW * tW * tZ) tW + | OPshl : op (tW * tZ) tW + | OPshr : op (tW * tZ) tW + | OPmkl : 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 interp_op src dst (f : op src dst) + : interp_flat_type_gen interp_base_type src -> interp_flat_type_gen interp_base_type dst + := match f in op s d return interp_flat_type_gen _ s -> interp_flat_type_gen _ d with + | 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 + | OPmkl => fun xy => let '(x, y) := eta xy in mkl 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 SConstT := ZConst (_ : Z) | BoolConst (_ : bool) | INVALID_CONST. + Inductive op_code : Set := + | SOPldi | SOPshrd | SOPshl | SOPshr | SOPmkl | SOPadc | SOPsubc + | SOPmulhwll | SOPmulhwhl | SOPmulhwhh | SOPselc | SOPaddm. + + Definition symbolicify_const (t : base_type) : interp_base_type t -> SConstT + := match t with + | TZ => fun x => ZConst x + | Tbool => fun x => BoolConst x + | TW => fun x => INVALID_CONST + end. + Definition symbolicify_op s d (v : op s d) : op_code + := match v with + | OPldi => SOPldi + | OPshrd => SOPshrd + | OPshl => SOPshl + | OPshr => SOPshr + | OPmkl => SOPmkl + | OPadc => SOPadc + | OPsubc => SOPsubc + | OPmulhwll => SOPmulhwll + | OPmulhwhl => SOPmulhwhl + | OPmulhwhh => SOPmulhwhh + | OPselc => SOPselc + | OPaddm => SOPaddm + end. + + Definition CSE {t} e := @CSE base_type SConstT op_code base_type_beq SConstT_beq op_code_beq internal_base_type_dec_bl interp_base_type op symbolicify_const symbolicify_op t e (fun _ => nil). +End reflection. +Section instances. + Context {ops : fancy_machine.instructions (2 * 128)}. + Global Instance: reify_op op (@Interface.ldi) 1 OPldi := I. + Global Instance: reify_op op (@Interface.shrd) 3 OPshrd := I. + Global Instance: reify_op op (@Interface.shl) 2 OPshl := I. + Global Instance: reify_op op (@Interface.shr) 2 OPshr := I. + Global Instance: reify_op op (@Interface.mkl) 2 OPmkl := I. + Global Instance: reify_op op (@Interface.adc) 3 OPadc := I. + Global Instance: reify_op op (@Interface.subc) 3 OPsubc := I. + Global Instance: reify_op op (@Interface.mulhwll) 2 OPmulhwll := I. + Global Instance: reify_op op (@Interface.mulhwhl) 2 OPmulhwhl := I. + Global Instance: reify_op op (@Interface.mulhwhh) 2 OPmulhwhh := I. + Global Instance: reify_op op (@Interface.selc) 3 OPselc := I. + Global Instance: reify_op op (@Interface.addm) 3 OPaddm := I. + Global Instance: reify type Z := TZ. + Global Instance: reify type bool := Tbool. + Global Instance: reify type fancy_machine.W := TW. +End instances. + +Ltac base_reify_op op op_head ::= + 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.mkl => constr:(reify_op op op_head 2 OPmkl) + | @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 e in + constr:(CSE _ (InlineConst (Linearize v))). +(*Ltac Reify_rhs := Reify.Reify_rhs base_type (interp_base_type _) op (interp_op _).*) + +Section syn. + Context {var : base_type -> Type}. + Inductive syntax := + | RegPInv + | RegMod + | RegMuLow + | RegZero + | cConstZ : Z -> syntax + | cConstBool : bool -> syntax + | cLowerHalf : syntax -> syntax + | cUpperHalf : syntax -> syntax + | cLeftShifted : syntax -> Z -> syntax + | cRightShifted : syntax -> Z -> syntax + | cVar : var TW -> syntax + | cVarC : var Tbool -> syntax + | cBind : syntax -> (var TW -> syntax) -> syntax + | cBindCarry : syntax -> (var Tbool -> var TW -> syntax) -> syntax + | cMul128 : syntax -> syntax -> syntax + | cRshi : syntax -> syntax -> Z -> syntax + | cSelc : var Tbool -> syntax -> syntax -> syntax + | cAddc : var Tbool -> syntax -> syntax -> syntax + | cAddm : syntax -> syntax -> syntax + | cAdd : syntax -> syntax -> syntax + | cSub : syntax -> syntax -> syntax + | cPair : syntax -> syntax -> syntax + | cAbs {t} : (var t -> syntax) -> syntax + | cINVALID {T} (_ : T). +End syn. + +Notation "'Return' x" := (cVar x) (at level 200). +Notation "'c.Mul128' ( x , A , B ) , b" := + (cBind (cMul128 A B) (fun x => b)) + (at level 200, b at level 200, format "'c.Mul128' ( x , A , B ) , '//' b"). +Notation "'c.Add' ( x , A , B ) , b" := + (cBindCarry (cAdd A B) (fun _ x => b)) + (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' b"). +Notation "'c.Add' ( x , A , B ) , b" := + (cBindCarry (cAdd (cVar A) B) (fun _ x => b)) + (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' b"). +Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , b" := + (cBindCarry (cAdd A B) (fun c x => cBindCarry (cAddc c A1 B1) (fun _ x1 => b))) + (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' 'c.Addc' ( x1 , A1 , B1 ) , '//' b"). +Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , b" := + (cBindCarry (cAdd A B) (fun c x => cBindCarry (cAddc c (cVar A1) B1) (fun _ x1 => b))) + (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' 'c.Addc' ( x1 , A1 , B1 ) , '//' b"). +Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , b" := + (cBindCarry (cAdd (cVar A) B) (fun c x => cBindCarry (cAddc c A1 B1) (fun _ x1 => b))) + (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' 'c.Addc' ( x1 , A1 , B1 ) , '//' b"). +Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , b" := + (cBindCarry (cAdd (cVar A) B) (fun c x => cBindCarry (cAddc c (cVar A1) B1) (fun _ x1 => b))) + (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' 'c.Addc' ( x1 , A1 , B1 ) , '//' b"). +Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , 'c.Selc' ( x2 , A2 , B2 ) , b" := + (cBindCarry (cAdd A B) (fun c x => cBindCarry (cAddc c A1 B1) (fun c1 x1 => cBind (cSelc c1 A2 B2) (fun x2 => b)))) + (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' 'c.Addc' ( x1 , A1 , B1 ) , '//' 'c.Selc' ( x2 , A2 , B2 ) , '//' b"). +Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , 'c.Selc' ( x2 , A2 , B2 ) , b" := + (cBindCarry (cAdd (cVar A) B) (fun c x => cBindCarry (cAddc c A1 B1) (fun c1 x1 => cBind (cSelc c1 A2 B2) (fun x2 => b)))) + (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' 'c.Addc' ( x1 , A1 , B1 ) , '//' 'c.Selc' ( x2 , A2 , B2 ) , '//' b"). +Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , 'c.Selc' ( x2 , A2 , B2 ) , b" := + (cBindCarry (cAdd A B) (fun c x => cBindCarry (cAddc c (cVar A1) B1) (fun c1 x1 => cBind (cSelc c1 A2 B2) (fun x2 => b)))) + (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' 'c.Addc' ( x1 , A1 , B1 ) , '//' 'c.Selc' ( x2 , A2 , B2 ) , '//' b"). +Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , 'c.Selc' ( x2 , A2 , B2 ) , b" := + (cBindCarry (cAdd (cVar A) B) (fun c x => cBindCarry (cAddc c (cVar A1) B1) (fun c1 x1 => cBind (cSelc c1 A2 B2) (fun x2 => b)))) + (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' 'c.Addc' ( x1 , A1 , B1 ) , '//' 'c.Selc' ( x2 , A2 , B2 ) , '//' b"). +Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , 'c.Selc' ( x2 , A2 , B2 ) , b" := + (cBindCarry (cAdd (cVar A) (cVar B)) (fun c x => cBindCarry (cAddc c (cVar A1) (cVar B1)) (fun c1 x1 => cBind (cSelc c1 A2 B2) (fun x2 => b)))) + (at level 200, b at level 200, format "'c.Add' ( x , A , B ) , '//' 'c.Addc' ( x1 , A1 , B1 ) , '//' 'c.Selc' ( x2 , A2 , B2 ) , '//' b"). + +Notation "'c.Sub' ( x , A , B ) , b" := + (cBindCarry (cSub A B) (fun _ x => b)) + (at level 200, b at level 200, format "'c.Sub' ( x , A , B ) , '//' b"). +Notation "'c.Sub' ( x , A , B ) , b" := + (cBindCarry (cSub (cVar A) B) (fun _ x => b)) + (at level 200, b at level 200, format "'c.Sub' ( x , A , B ) , '//' b"). +Notation "'c.Sub' ( x , A , B ) , b" := + (cBindCarry (cSub A (cVar B)) (fun _ x => b)) + (at level 200, b at level 200, format "'c.Sub' ( x , A , B ) , '//' b"). +Notation "'c.Sub' ( x , A , B ) , b" := + (cBindCarry (cSub (cVar A) (cVar B)) (fun _ x => b)) + (at level 200, b at level 200, format "'c.Sub' ( x , A , B ) , '//' b"). + +Notation "'c.Addm' ( x , A , B ) , b" := + (cBind (cAddm A B) (fun x => b)) + (at level 200, b at level 200, format "'c.Addm' ( x , A , B ) , '//' b"). +Notation "'c.Addm' ( x , A , B ) , b" := + (cBind (cAddm A (cVar B)) (fun x => b)) + (at level 200, b at level 200, format "'c.Addm' ( x , A , B ) , '//' b"). +Notation "'c.Addm' ( x , A , B ) , b" := + (cBind (cAddm (cVar A) B) (fun x => b)) + (at level 200, b at level 200, format "'c.Addm' ( x , A , B ) , '//' b"). +Notation "'c.Addm' ( x , A , B ) , b" := + (cBind (cAddm (cVar A) (cVar B)) (fun x => b)) + (at level 200, b at level 200, format "'c.Addm' ( x , A , B ) , '//' b"). + +Notation "'c.Rshi' ( x , A , B , C ) , b" := + (cBind (cRshi (cVar A) (cVar B) C) (fun x => b)) + (at level 200, b at level 200, format "'c.Rshi' ( x , A , B , C ) , '//' b"). + +Notation "'c.LowerHalf' ( x )" := + (cLowerHalf x) + (at level 200, format "'c.LowerHalf' ( x )"). +Notation "'c.LowerHalf' ( x )" := + (cLowerHalf (cVar x)) + (at level 200, format "'c.LowerHalf' ( x )"). +Notation "'c.UpperHalf' ( x )" := + (cUpperHalf x) + (at level 200, format "'c.UpperHalf' ( x )"). +Notation "'c.UpperHalf' ( x )" := + (cUpperHalf (cVar x)) + (at level 200, format "'c.UpperHalf' ( x )"). +Notation "'c.LeftShifted' { x , v }" := + (cLeftShifted x v) + (at level 200, format "'c.LeftShifted' { x , v }"). +Notation "'c.LeftShifted' { x , v }" := + (cLeftShifted (cVar x) v) + (at level 200, format "'c.LeftShifted' { x , v }"). +Notation "'c.RightShifted' { x , v }" := + (cRightShifted x v) + (at level 200, format "'c.RightShifted' { x , v }"). +Notation "'c.RightShifted' { x , v }" := + (cRightShifted (cVar x) v) + (at level 200, format "'c.RightShifted' { x , v }"). +Notation "'λ' x .. y , t" := (cAbs (fun x => .. (cAbs (fun y => t)) ..)) + (at level 200, x binder, y binder, right associativity). + +Definition Syntax := forall var, @syntax var. + +Section assemble. + Context (ops : fancy_machine.instructions (2 * 128)). + + Section with_var. + Context {var : base_type -> Type}. + + Fixpoint assemble_syntax_const + {t} + : interp_flat_type_gen (interp_base_type _) t -> @syntax var + := match t return interp_flat_type_gen (interp_base_type _) t -> @syntax var with + | Tbase TZ => cConstZ + | Tbase Tbool => cConstBool + | Tbase t => fun _ => cINVALID t + | Prod A B => fun xy => cPair (@assemble_syntax_const A (fst xy)) + (@assemble_syntax_const B (snd xy)) + end. + + Definition assemble_syntaxf_step + (assemble_syntaxf : forall {t} (v : @Syntax.exprf base_type (interp_base_type _) op (fun _ => @syntax var) t), @syntax var) + {t} (v : @Syntax.exprf base_type (interp_base_type _) op (fun _ => @syntax var) t) : @syntax var. + Proof. + refine match v return @syntax var with + | Syntax.Const t x => assemble_syntax_const x + | Syntax.Var _ x => x + | Syntax.Op t1 tR op args + => let v := @assemble_syntaxf t1 args in + match op, v with + | OPldi , cConstZ 0 => RegZero + | OPldi , cConstZ v => cINVALID v + | OPldi , RegZero => RegZero + | OPldi , RegMod => RegMod + | OPldi , RegMuLow => RegMuLow + | OPldi , RegPInv => RegPInv + | OPshrd , cPair x (cPair y (cConstZ n)) => cRshi x y n + | OPshrd , cPair (cPair x y) (cConstZ n) => cRshi x y n + | OPshl , cPair w (cConstZ n) => cLeftShifted w n + | OPshr , cPair w (cConstZ n) => cRightShifted w n + | OPmkl , _ => cINVALID op + | OPadc , cPair (cPair x y) (cVarC c) => cAddc c x y + | OPadc , cPair x (cPair y (cVarC c)) => cAddc c x y + | OPadc , cPair (cPair x y) (cConstBool false) => cAdd x y + | OPadc , cPair x (cPair y (cConstBool false)) => cAdd x y + | OPsubc , cPair (cPair x y) (cConstBool false) => cSub x y + | OPsubc , cPair x (cPair y (cConstBool false)) => cSub x y + | OPmulhwll, cPair x y => cMul128 (cLowerHalf x) (cLowerHalf y) + | OPmulhwhl, cPair x y => cMul128 (cUpperHalf x) (cLowerHalf y) + | OPmulhwhh, cPair x y => cMul128 (cUpperHalf x) (cUpperHalf y) + | OPselc , cPair (cVarC c) (cPair x y) => cSelc c x y + | OPselc , cPair (cPair (cVarC c) x) y => cSelc c x y + | OPaddm , cPair x (cPair y RegMod) => cAddm x y + | OPaddm , cPair (cPair x y) RegMod => cAddm x y + | _, _ => cINVALID op + end + | Syntax.Let tx ex _ eC + => let ex' := @assemble_syntaxf _ ex in + let eC' := fun x => @assemble_syntaxf _ (eC x) in + let special := match ex' with + | RegZero as ex'' | RegMuLow as ex'' | RegMod as ex'' | RegPInv as ex'' + | cUpperHalf _ as ex'' | cLowerHalf _ as ex'' + | cLeftShifted _ _ as ex'' + | cRightShifted _ _ as ex'' + => Some ex'' + | _ => None + end in + match special, tx return (interp_flat_type_gen _ tx -> _) -> _ with + | Some x, Tbase _ => fun eC' => eC' x + | _, Tbase TW + => fun eC' => cBind ex' (fun x => eC' (cVar x)) + | _, Prod (Tbase Tbool) (Tbase TW) + => fun eC' => cBindCarry ex' (fun c x => eC' (cVarC c, cVar x)) + | _, _ + => fun _ => cINVALID (fun x : Prop => x) + end eC' + | Syntax.Pair _ ex _ ey + => cPair (@assemble_syntaxf _ ex) (@assemble_syntaxf _ ey) + end. + Defined. + + Fixpoint assemble_syntaxf {t} v {struct v} : @syntax var + := @assemble_syntaxf_step (@assemble_syntaxf) t v. + Fixpoint assemble_syntax {t} (v : @Syntax.expr base_type (interp_base_type _) op (fun _ => @syntax var) t) (args : list (@syntax var)) {struct v} + : @syntax var + := match v, args return @syntax var with + | Syntax.Return _ x, _ => assemble_syntaxf x + | Syntax.Abs _ _ f, nil => cAbs (fun x => @assemble_syntax _ (f (cVar x)) args) + | Syntax.Abs _ _ f, cons v vs => @assemble_syntax _ (f v) vs + end. + End with_var. + + Definition AssembleSyntax {t} (v : Syntax.Expr _ _ _ t) (args : list Syntax) : Syntax + := fun var => @assemble_syntax var t (v _) (List.map (fun f => f var) args). +End assemble. diff --git a/src/Experiments/FancyMachineBarrett256.v b/src/Experiments/FancyMachineBarrett256.v new file mode 100644 index 000000000..5ca25fdb4 --- /dev/null +++ b/src/Experiments/FancyMachineBarrett256.v @@ -0,0 +1,129 @@ +Require Import Crypto.Experiments.FancyMachine256. +Require Import Crypto.ModularArithmetic.BarrettReduction.ZBounded. +Require Import Crypto.ModularArithmetic.BarrettReduction.ZHandbook. + +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). + (** 25519 dsa *) + 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. + Let props' := ZLikeProperties_of_ArchitectureBoundedOps ops m H 250 H' H''. + Let ops' := (ZLikeOps_of_ArchitectureBoundedOps ops m 250). + Local Existing Instances props' ops'. + Local Notation fst' := (@fst fancy_machine.W fancy_machine.W). + Local Notation snd' := (@snd fancy_machine.W fancy_machine.W). + 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' := _. + Axiom (μ_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. + + Definition pre_f v + := (@barrett_reduce m b k μ offset m_pos base_pos μ_good offset_nonneg k_big_enough m_small m_large ops' props' μ' I μ'_eq (fst' v, snd' v)). + + Local Arguments μ' / . + Local Arguments ldi' / . + + Definition expression' + := Eval simpl in + (fun v => proj1_sig (pre_f v)). + Definition expression + := Eval cbv beta iota delta [expression' fst snd] in + fun v => let RegMod := fancy_machine.ldi m in + let RegMu := fancy_machine.ldi μ in + let RegZero := fancy_machine.ldi 0 in + expression' v. + + Definition expression_eq v H : fancy_machine.decode (expression v) = _ + := proj1 (proj2_sig (pre_f v) H). +End expression. + +Section reflected. + Context (ops : fancy_machine.instructions (2 * 128)). + Definition rexpression : Syntax.Expr base_type (interp_base_type _) op (Arrow TZ (Arrow TZ (Arrow TW (Arrow TW (Tbase TW))))). + Proof. + let v := (eval cbv beta delta [expression] in (fun m μ x y => expression ops m μ (x, y))) in + let v := Reify v in + exact v. + Defined. + + Definition rexpression_simple := Eval vm_compute in rexpression. + + Context (m μ : Z) + (props : fancy_machine.arithmetic ops). + + Let result (v : tuple fancy_machine.W 2) := Syntax.Interp (interp_op _) rexpression_simple m μ (fst v) (snd v). + + Theorem sanity : result = expression ops m μ. + Proof. + reflexivity. + Qed. + + Theorem correctness + (b : Z := 2) + (k : Z := 253) + (offset : Z := 3) + (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)) + (v : tuple fancy_machine.W 2) + (H5 : 0 <= decode v < b^(2 * k)) + : fancy_machine.decode (result v) = decode v mod m. + Proof. + rewrite sanity; destruct v. + eapply expression_eq; assumption. + Grab Existential Variables. + assumption. + Qed. +End reflected. + +Definition compiled_syntax + := Eval vm_compute in + (fun ops => AssembleSyntax ops (rexpression_simple _) (@RegMod :: @RegMuLow :: nil)%list). + +Print compiled_syntax. +(* compiled_syntax = +fun (_ : fancy_machine.instructions (2 * 128)) (var : base_type -> Type) => +λ x x0 : var TW, +c.Rshi(x1, x0, x, 250), +c.Mul128(x2, c.UpperHalf(x1), c.UpperHalf(RegMuLow)), +c.Mul128(x3, c.UpperHalf(x1), c.LowerHalf(RegMuLow)), +c.Mul128(x4, c.LowerHalf(x1), c.LowerHalf(RegMuLow)), +c.Add(x6, x4, c.LeftShifted{x3, 128}), +c.Addc(x8, x2, c.RightShifted{x3, 128}), +c.Mul128(x9, c.UpperHalf(RegMuLow), c.LowerHalf(x1)), +c.Add(_, x6, c.LeftShifted{x9, 128}), +c.Addc(x13, x8, c.RightShifted{x9, 128}), +c.Mul128(x14, c.LowerHalf(x13), c.LowerHalf(RegMod)), +c.Mul128(x15, c.UpperHalf(x13), c.LowerHalf(RegMod)), +c.Add(x17, x14, c.LeftShifted{x15, 128}), +c.Mul128(x18, c.UpperHalf(RegMod), c.LowerHalf(x13)), +c.Add(x20, x17, c.LeftShifted{x18, 128}), +c.Sub(x22, x, x20), +c.Addm(x23, x22, RegZero), +c.Addm(x24, x23, RegZero), +Return x24 + : fancy_machine.instructions (2 * 128) -> forall var : base_type -> Type, syntax +*) diff --git a/src/Experiments/FancyMachineMontgomery256.v b/src/Experiments/FancyMachineMontgomery256.v new file mode 100644 index 000000000..0f8d8bd59 --- /dev/null +++ b/src/Experiments/FancyMachineMontgomery256.v @@ -0,0 +1,118 @@ +Require Import Crypto.Experiments.FancyMachine256. +Require Import Crypto.ModularArithmetic.Montgomery.ZBounded. +Require Import Crypto.ModularArithmetic.Montgomery.ZProofs. + +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. + Let props' := ZLikeProperties_of_ArchitectureBoundedOps ops modulus H 256 H' H''. + Let ops' := (ZLikeOps_of_ArchitectureBoundedOps ops modulus 256). + Local Notation fst' := (@fst fancy_machine.W fancy_machine.W). + Local Notation snd' := (@snd fancy_machine.W fancy_machine.W). + Definition ldi' : load_immediate + (@ZBounded.SmallT (2 ^ 256) (2 ^ 256) modulus + (@ZLikeOps_of_ArchitectureBoundedOps 128 ops modulus 256)) := _. + Let isldi : is_load_immediate ldi' := _. + Definition pre_f := (fun v => (reduce_via_partial (2^256) modulus (props := props') (ldi' m') I Hm (fst' v, snd' v))). + Definition f := (fun v => proj1_sig (pre_f 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 / . + + Definition expression' + := Eval simpl in f. + Definition expression + := Eval cbv beta delta [expression' fst snd] in + fun v => let RegMod := fancy_machine.ldi modulus in + let RegPInv := fancy_machine.ldi m' in + let RegZero := fancy_machine.ldi 0 in + expression' v. + 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) = _ + := @ZBounded.reduce_via_partial_correct (2^256) modulus _ props' (ldi' m') I Hm R' HR0 HR1 v I Hv. +End expression. + +Section reflected. + Context (ops : fancy_machine.instructions (2 * 128)). + Definition rexpression : Syntax.Expr base_type (interp_base_type _) op (Arrow TZ (Arrow TZ (Arrow TW (Arrow TW (Tbase TW))))). + Proof. + let v := (eval cbv beta delta [expression] in (fun modulus m' x y => expression ops modulus m' (x, y))) in + let v := Reify v in + exact v. + Defined. + + Definition rexpression_simple := Eval vm_compute in rexpression. + + Context (modulus m' : Z) + (props : fancy_machine.arithmetic ops). + + Let result (v : tuple fancy_machine.W 2) := Syntax.Interp (interp_op _) rexpression_simple modulus m' (fst v) (snd v). + + Theorem sanity : result = expression ops modulus m'. + Proof. + reflexivity. + Qed. + + Local Infix "≡₂₅₆" := (Z.equiv_modulo (2^256)). + Local Infix "≡" := (Z.equiv_modulo modulus). + + Theorem correctness + 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 fancy_machine.W 2) + (H5 : 0 <= decode v <= 2^256 * modulus) + : fancy_machine.decode (result v) = (decode v * R') mod modulus. + Proof. + 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. +End reflected. + +Definition compiled_syntax + := Eval vm_compute in + (fun ops => AssembleSyntax ops (rexpression_simple _) (@RegMod :: @RegPInv :: nil)%list). + +Print compiled_syntax. +(* compiled_syntax = +fun (_ : fancy_machine.instructions (2 * 128)) (var : base_type -> Type) => +λ x x0 : var TW, +c.Mul128(x1, c.LowerHalf(x), c.LowerHalf(RegPInv)), +c.Mul128(x2, c.UpperHalf(x), c.LowerHalf(RegPInv)), +c.Add(x4, x1, c.LeftShifted{x2, 128}), +c.Mul128(x5, c.UpperHalf(RegPInv), c.LowerHalf(x)), +c.Add(x7, x4, c.LeftShifted{x5, 128}), +c.Mul128(x8, c.UpperHalf(x7), c.UpperHalf(RegMod)), +c.Mul128(x9, c.UpperHalf(x7), c.LowerHalf(RegMod)), +c.Mul128(x10, c.LowerHalf(x7), c.LowerHalf(RegMod)), +c.Add(x12, x10, c.LeftShifted{x9, 128}), +c.Addc(x14, x8, c.RightShifted{x9, 128}), +c.Mul128(x15, c.UpperHalf(RegMod), c.LowerHalf(x7)), +c.Add(x17, x12, c.LeftShifted{x15, 128}), +c.Addc(x19, x14, c.RightShifted{x15, 128}), +c.Add(_, x, x17), +c.Addc(x23, x0, x19), +c.Selc(x24, RegMod, RegZero), +c.Sub(x26, x23, x24), +c.Addm(x27, x26, RegZero), +Return x27 + : fancy_machine.instructions (2 * 128) -> forall var : base_type -> Type, syntax +*) |