diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-20 18:04:36 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-20 18:04:36 -0400 |
| commit | cc8ddf38d88bac78a50f8e27966d331f444df549 (patch) | |
| tree | 46f1ea906c863f8cd9efa57c72feac2f482192dd /src/Assembly | |
| parent | 14daf64fc42608af1c626f2076444706b6299cef (diff) | |
Plug bounded into assembly stuff
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/GF25519BoundedInstantiation.v | 34 |
1 files changed, 12 insertions, 22 deletions
diff --git a/src/Assembly/GF25519BoundedInstantiation.v b/src/Assembly/GF25519BoundedInstantiation.v index 2661e07ae..e17e20386 100644 --- a/src/Assembly/GF25519BoundedInstantiation.v +++ b/src/Assembly/GF25519BoundedInstantiation.v @@ -6,36 +6,26 @@ Require Import Crypto.Util.Tuple. (* Totally fine to edit these definitions; DO NOT change the type signatures at all *) Definition ExprBinOp : Type - := @PhoasCommon.interp_type Z GF25519.FE -> @PhoasCommon.interp_type Z GF25519.FE -> @HL.HL.expr Z (@PhoasCommon.interp_type Z) GF25519.FE. + := @PhoasCommon.interp_type word64 GF25519.FE -> @PhoasCommon.interp_type word64 GF25519.FE -> @HL.HL.expr word64 (@PhoasCommon.interp_type word64) GF25519.FE. Definition ExprUnOp : Type - := @PhoasCommon.interp_type Z GF25519.FE -> @HL.HL.expr Z (@PhoasCommon.interp_type Z) GF25519.FE. -Definition interp_bexpr : ExprBinOp -> Specific.GF25519.fe25519 -> Specific.GF25519.fe25519 -> Specific.GF25519.fe25519 - := fun f x y => HL.HL.interp (E := Evaluables.ZEvaluable) (t := GF25519.FE) (f x y). -Definition interp_uexpr : ExprUnOp -> Specific.GF25519.fe25519 -> Specific.GF25519.fe25519 - := fun f x => HL.HL.interp (E := Evaluables.ZEvaluable) (t := GF25519.FE) (f x). -Definition radd : ExprBinOp := GF25519.AddExpr.ge25519_add. -Definition rsub : ExprBinOp := GF25519.SubExpr.ge25519_sub. -Definition rmul : ExprBinOp := GF25519.MulExpr.ge25519_mul. -Definition ropp : ExprUnOp := GF25519.OppExpr.ge25519_opp. + := @PhoasCommon.interp_type word64 GF25519.FE -> @HL.HL.expr word64 (@PhoasCommon.interp_type word64) GF25519.FE. +Definition interp_bexpr : ExprBinOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W + := fun f x y => HL.HL.interp (E := Evaluables.WordEvaluable) (t := GF25519.FE) (f x y). +Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W + := fun f x => HL.HL.interp (E := Evaluables.WordEvaluable) (t := GF25519.FE) (f x). +Axiom radd : ExprBinOp. (* := GF25519.AddExpr.ge25519_add. *) +Axiom rsub : ExprBinOp. (* := GF25519.SubExpr.ge25519_sub. *) +Axiom rmul : ExprBinOp. (* := GF25519.MulExpr.ge25519_mul. *) +Axiom ropp : ExprUnOp. (* := GF25519.OppExpr.ge25519_opp. *) Axiom rfreeze : ExprUnOp. -(*Local Notation ibinop_correct_and_bounded irop op - := (forall x y, - is_bounded (fe25519WToZ x) = true - -> is_bounded (fe25519WToZ y) = true - -> fe25519WToZ (irop x y) = op (fe25519WToZ x) (fe25519WToZ y) - /\ is_bounded (fe25519WToZ (irop x y)) = true) (only parsing). Local Notation binop_correct_and_bounded rop op := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing). -Local Notation iunop_correct_and_bounded irop op - := (forall x, - is_bounded (fe25519WToZ x) = true - -> fe25519WToZ (irop x) = op (fe25519WToZ x) - /\ is_bounded (fe25519WToZ (irop x)) = true) (only parsing). Local Notation unop_correct_and_bounded rop op := (iunop_correct_and_bounded (interp_uexpr rop) op) (only parsing). + Axiom radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. Axiom rsub_correct_and_bounded : binop_correct_and_bounded rsub carry_sub. Axiom rmul_correct_and_bounded : binop_correct_and_bounded rmul mul. Axiom ropp_correct_and_bounded : unop_correct_and_bounded ropp carry_opp. -Axiom rfreeze_correct_and_bounded : unop_correct_and_bounded rfreeze freeze.*) +Axiom rfreeze_correct_and_bounded : unop_correct_and_bounded rfreeze freeze. |