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/Specific/X2555/C128/ladderstep.v | |
parent | 8c296e81231b8e1fa66d1cba2426ab1f891b7593 (diff) |
add back incorrectly deleted files
Diffstat (limited to 'src/Specific/X2555/C128/ladderstep.v')
-rw-r--r-- | src/Specific/X2555/C128/ladderstep.v | 24 |
1 files changed, 24 insertions, 0 deletions
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. |