diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-14 19:35:18 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-14 19:35:18 -0400 |
| commit | 1c8c702b7ee5b1f62496e6fdf9070332a344f4f7 (patch) | |
| tree | d884381cc4eb7085ac8c4ffa76088e6f21f6ee84 | |
| parent | e22a7e15a30c961a8afb7f8041dfdaf570225bae (diff) | |
Make proj1_sig square_sig take only one argument
| -rw-r--r-- | src/Specific/ArithmeticSynthesisTest.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v index d2d50fa2b..9ea1369dd 100644 --- a/src/Specific/ArithmeticSynthesisTest.v +++ b/src/Specific/ArithmeticSynthesisTest.v @@ -185,10 +185,10 @@ Section Ops51. Defined. Definition square_sig : - {mul : (Z^sz -> Z^sz -> Z^sz)%type | + {square : (Z^sz -> Z^sz)%type | forall a : Z^sz, let eval := Positional.Fdecode (m := m) wt in - eval (mul a a) = (eval a * eval a)%F}. + eval (square a) = (eval a * eval a)%F}. Proof. eexists; cbv beta zeta; intros. pose proof wt_nonzero. @@ -196,7 +196,7 @@ Section Ops51. Positional.mul_cps (n:=sz) (m:=sz2) wt a a (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)) in solve_op_F wt x. - instantiate (1 := fun a _ => + instantiate (1 := fun a => (* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *) let '(r4, r3, r2, r1, r0) := a in dlet d0 := r0 * 2 in |