diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-20 00:13:43 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-20 00:13:43 -0400 |
| commit | a2f81a1a2a82be7c445748cfca375bd5f74688d2 (patch) | |
| tree | 7c22ab68b1db58556c941db2a03544d0ed107b43 /src/Assembly | |
| parent | 6b0876b5625cc9982bde1f4f24851c99a245d480 (diff) | |
Use carry versions of operations
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/GF25519.v | 10 | ||||
| -rw-r--r-- | src/Assembly/GF25519BoundedInstantiation.v | 16 |
2 files changed, 16 insertions, 10 deletions
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index 80d9044c4..50a886305 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -42,7 +42,7 @@ Module GF25519. Definition inputBounds := feBound ++ feBound. Definition ge25519_add_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In] in add. + Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in carry_add. Definition ge25519_add' (P Q: @interp_type Z FE) : { r: @HL.expr Z (@interp_type Z) FE @@ -95,7 +95,7 @@ Module GF25519. Definition inputBounds := feBound ++ feBound. Definition ge25519_sub_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In] in sub. + Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in carry_sub. Definition ge25519_sub' (P Q: @interp_type Z FE) : { r: @HL.expr Z (@interp_type Z) FE @@ -148,7 +148,7 @@ Module GF25519. Definition inputBounds := feBound ++ feBound. Definition ge25519_mul_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In] in mul. + Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in mul. Definition ge25519_mul' (P Q: @interp_type Z FE) : { r: @HL.expr Z (@interp_type Z) FE @@ -201,7 +201,7 @@ Module GF25519. Definition inputBounds := feBound. Definition ge25519_opp_expr := - Eval cbv beta delta [fe25519 add mul sub opp Let_In] in opp. + Eval cbv beta delta [fe25519 carry_add mul carry_sub carry_opp Let_In] in carry_opp. Definition ge25519_opp' (P: @interp_type Z FE) : { r: @HL.expr Z (@interp_type Z) FE @@ -255,4 +255,4 @@ End GF25519. Extraction "GF25519Add" GF25519.Add. Extraction "GF25519Sub" GF25519.Sub. Extraction "GF25519Mul" GF25519.Mul. -Extraction "GF25519Opp" GF25519.Opp.
\ No newline at end of file +Extraction "GF25519Opp" GF25519.Opp. diff --git a/src/Assembly/GF25519BoundedInstantiation.v b/src/Assembly/GF25519BoundedInstantiation.v index 0cbe305b7..511ff9a2e 100644 --- a/src/Assembly/GF25519BoundedInstantiation.v +++ b/src/Assembly/GF25519BoundedInstantiation.v @@ -1,11 +1,9 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.Assembly.GF25519. +Require Import Crypto.Specific.GF25519Bounded. Require Import Crypto.Specific.GF25519. Require Import Crypto.Util.Tuple. -Axiom is_bounded : forall (x : Specific.GF25519.fe25519), bool. (* Pull from Specific.GF25519Bounded when the latest changes to master are merged into this branch *) - - (* 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. @@ -20,8 +18,16 @@ Definition rsub : ExprBinOp := GF25519.SubExpr.ge25519_sub. Definition rmul : ExprBinOp := GF25519.MulExpr.ge25519_mul. Definition ropp : ExprUnOp := GF25519.OppExpr.ge25519_opp. Axiom rfreeze : ExprUnOp. -(*Axiom radd_correct : forall x y, interp_bexpr radd x y = carry_add x y. -Axiom rsub_correct : forall x y, interp_bexpr rsub x y = carry_sub x y.*) +Lemma radd_correct : forall x y, interp_bexpr radd x y = carry_add x y. +Proof. + cbv [interp_bexpr radd GF25519.AddExpr.ge25519_add]; intros. + apply proj2_sig. +Qed. +Lemma rsub_correct : forall x y, interp_bexpr rsub x y = carry_sub x y. +Proof. + cbv [interp_bexpr rsub GF25519.SubExpr.ge25519_sub]; intros. + apply proj2_sig. +Qed. Lemma rmul_correct : forall x y, interp_bexpr rmul x y = mul x y. Proof. cbv [interp_bexpr rmul GF25519.MulExpr.ge25519_mul]; intros. |