From 102904674d12d1791f55a55cb66a334e5c21715a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 21 Oct 2017 23:43:59 -0400 Subject: Add tight and loose bounds, no carry in add, sub Following Andres' suggestions to allow making ladderstep from other synthesis things. It went though mostly without a hitch, though there were a number of boilerplate changes needed. --- src/Specific/X25519/C32/feadd.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 src/Specific/X25519/C32/feadd.v (limited to 'src/Specific/X25519/C32/feadd.v') diff --git a/src/Specific/X25519/C32/feadd.v b/src/Specific/X25519/C32/feadd.v new file mode 100644 index 000000000..f74cf9cef --- /dev/null +++ b/src/Specific/X25519/C32/feadd.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.X25519.C32.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition add : + { add : feBW_tight -> feBW_tight -> feBW_loose + | forall a b, phiBW_loose (add a b) = F.add (phiBW_tight a) (phiBW_tight b) }. +Proof. + Set Ltac Profiling. + Time synthesize_add (). + Show Ltac Profile. +Time Defined. + +Print Assumptions add. -- cgit v1.2.3