diff options
author | jadep <jade.philipoom@gmail.com> | 2017-11-12 15:20:31 -0500 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2017-11-12 15:20:31 -0500 |
commit | 1c6950e607fb2ca13a773f96ba20366a886360fc (patch) | |
tree | 96cf2330ce5032f6f971d0b256d455372d6f3cad /src | |
parent | 8c296e81231b8e1fa66d1cba2426ab1f891b7593 (diff) |
add back incorrectly deleted files
Diffstat (limited to 'src')
-rw-r--r-- | src/Specific/CurveParameters/x2555_130.json | 10 | ||||
-rw-r--r-- | src/Specific/X2555/C128/CurveParameters.v | 39 | ||||
-rw-r--r-- | src/Specific/X2555/C128/Synthesis.v | 9 | ||||
-rw-r--r-- | src/Specific/X2555/C128/ladderstep.v | 24 | ||||
-rwxr-xr-x | src/Specific/X2555/C128/py_interpreter.sh | 4 |
5 files changed, 86 insertions, 0 deletions
diff --git a/src/Specific/CurveParameters/x2555_130.json b/src/Specific/CurveParameters/x2555_130.json new file mode 100644 index 000000000..130a87d38 --- /dev/null +++ b/src/Specific/CurveParameters/x2555_130.json @@ -0,0 +1,10 @@ +{ + "modulus" : "2^255-5", + "base" : "130", + "a24" : "121665 (* XXX TODO(andreser) FIXME? Is this right for this curve? *)", + "sz" : "3", + "bitwidth" : "128", + "carry_chains" : "default", + "coef_div_modulus" : "2", + "operations" : ["ladderstep"] +} diff --git a/src/Specific/X2555/C128/CurveParameters.v b/src/Specific/X2555/C128/CurveParameters.v new file mode 100644 index 000000000..1171f7583 --- /dev/null +++ b/src/Specific/X2555/C128/CurveParameters.v @@ -0,0 +1,39 @@ +Require Import Crypto.Specific.Framework.RawCurveParameters. +Require Import Crypto.Util.LetIn. + +(*** +Modulus : 2^255-5 +Base: 130 +***) + +Definition curve : CurveParameters := + {| + sz := 3%nat; + base := 130; + bitwidth := 128; + s := 2^255; + c := [(1, 5)]; + carry_chains := Some [seq 0 (pred 3); [0; 1]]%nat; + + a24 := Some (121665 (* XXX TODO(andreser) FIXME? Is this right for this curve? *)); + coef_div_modulus := Some 2%nat; + + goldilocks := None; + karatsuba := None; + montgomery := false; + freeze := Some false; + ladderstep := true; + + mul_code := None; + + square_code := None; + + upper_bound_of_exponent_loose := None; + upper_bound_of_exponent_tight := None; + allowable_bit_widths := None; + freeze_extra_allowable_bit_widths := None; + modinv_fuel := None + |}. + +Ltac extra_prove_mul_eq _ := idtac. +Ltac extra_prove_square_eq _ := idtac. diff --git a/src/Specific/X2555/C128/Synthesis.v b/src/Specific/X2555/C128/Synthesis.v new file mode 100644 index 000000000..af7b8ae33 --- /dev/null +++ b/src/Specific/X2555/C128/Synthesis.v @@ -0,0 +1,9 @@ +Require Import Crypto.Specific.Framework.SynthesisFramework. +Require Import Crypto.Specific.X2555.C128.CurveParameters. + +Module P <: PrePackage. + Definition package : Tag.Context. + Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined. +End P. + +Module Export S := PackageSynthesis P. diff --git a/src/Specific/X2555/C128/ladderstep.v b/src/Specific/X2555/C128/ladderstep.v new file mode 100644 index 000000000..16984403b --- /dev/null +++ b/src/Specific/X2555/C128/ladderstep.v @@ -0,0 +1,24 @@ +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.Ladderstep. +Require Import Crypto.Specific.X2555.C128.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition xzladderstep : + { xzladderstep : feW -> feW * feW -> feW * feW -> feW * feW * (feW * feW) + | forall x1 Q Q', + let xz := xzladderstep x1 Q Q' in + let eval := B.Positional.Fdecode wt in + feW_tight_bounded x1 + -> feW_tight_bounded (fst Q) /\ feW_tight_bounded (snd Q) + -> feW_tight_bounded (fst Q') /\ feW_tight_bounded (snd Q') + -> ((feW_tight_bounded (fst (fst xz)) /\ feW_tight_bounded (snd (fst xz))) + /\ (feW_tight_bounded (fst (snd xz)) /\ feW_tight_bounded (snd (snd xz)))) + /\ Tuple.map (n:=2) (Tuple.map (n:=2) phiW) xz = FMxzladderstep (m:=m) (eval (proj1_sig a24_sig)) (phiW x1) (Tuple.map (n:=2) phiW Q) (Tuple.map (n:=2) phiW Q') }. +Proof. + Set Ltac Profiling. + synthesize_xzladderstep (). + Show Ltac Profile. +Time Defined. + +Print Assumptions xzladderstep. diff --git a/src/Specific/X2555/C128/py_interpreter.sh b/src/Specific/X2555/C128/py_interpreter.sh new file mode 100755 index 000000000..7ec3fa6ab --- /dev/null +++ b/src/Specific/X2555/C128/py_interpreter.sh @@ -0,0 +1,4 @@ +#!/bin/sh +set -eu + +/usr/bin/env python3 "$@" -Dq='2**255-5' -Dmodulus_bytes='130' -Da24='121665 (* XXX TODO(andreser) FIXME? Is this right for this curve? *)' |