18 files changed, 243 insertions, 0 deletions
diff --git a/src/Specific/NISTP256/AMD128/CurveParameters.v b/src/Specific/NISTP256/AMD128/CurveParameters.v
new file mode 100644
index 000000000..ea4865b08
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/CurveParameters.v
@@ -0,0 +1,34 @@
+Require Import Crypto.Specific.Framework.CurveParameters.
+Require Import Crypto.Util.LetIn.
+
+(***
+Modulus : 2^256-2^224+2^192+2^96-1
+Base: 128
+***)
+
+Module Curve <: CurveParameters.
+  Definition sz : nat := 2%nat.
+  Definition bitwidth : Z := 128.
+  Definition s : Z := 2^256.
+  Definition c : list limb := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)].
+  Definition carry_chains : option (list (list nat)) := Eval vm_compute in None.
+
+  Definition a24 : option Z := None.
+  Definition coef_div_modulus : option nat := None. (* add 0*modulus before subtracting *)
+
+  Definition goldilocks : bool := false.
+  Definition montgomery : bool := true.
+
+  Definition mul_code : option (Z^sz -> Z^sz -> Z^sz)
+    := None.
+
+  Definition square_code : option (Z^sz -> Z^sz)
+    := None.
+
+  Definition upper_bound_of_exponent : option (Z -> Z) := None.
+  Definition allowable_bit_widths : option (list nat) := None.
+  Definition freeze_extra_allowable_bit_widths : option (list nat) := None.
+  Definition modinv_fuel : option nat := None.
+  Ltac extra_prove_mul_eq := idtac.
+  Ltac extra_prove_square_eq := idtac.
+End Curve.
diff --git a/src/Specific/NISTP256/AMD128/Synthesis.v b/src/Specific/NISTP256/AMD128/Synthesis.v
new file mode 100644
index 000000000..3871666e1
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/Synthesis.v
@@ -0,0 +1,11 @@
+Require Import Crypto.Specific.Framework.SynthesisFramework.
+Require Import Crypto.Specific.NISTP256.AMD128.CurveParameters.
+
+Module Import T := MakeSynthesisTactics Curve.
+
+Module P <: PrePackage.
+  Definition package : Tag.Context.
+  Proof. make_Synthesis_package (). Defined.
+End P.
+
+Module Export S := PackageSynthesis Curve P.
diff --git a/src/Specific/NISTP256/AMD128/compiler.sh b/src/Specific/NISTP256/AMD128/compiler.sh
new file mode 100644
index 000000000..518f95765
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/compiler.sh
@@ -0,0 +1,4 @@
+#!/bin/sh
+set -eu
+
+gcc -fno-peephole2 `#GCC BUG 81300` -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes -Wno-incompatible-pointer-types -fno-strict-aliasing "$@"
diff --git a/src/Specific/NISTP256/AMD128/feadd.v b/src/Specific/NISTP256/AMD128/feadd.v
new file mode 100644
index 000000000..5ee329e4e
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/feadd.v
@@ -0,0 +1,14 @@
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.NISTP256.AMD128.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition add :
+  { add : feBW_small -> feBW_small -> feBW_small
+  | forall a b, phiM_small (add a b) = F.add (phiM_small a) (phiM_small b) }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_add ().
+  Show Ltac Profile.
+Time Defined.
+
+Print Assumptions add.
diff --git a/src/Specific/NISTP256/AMD128/feaddDisplay.log b/src/Specific/NISTP256/AMD128/feaddDisplay.log
new file mode 100644
index 000000000..ea6db527b
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/feaddDisplay.log
@@ -0,0 +1,14 @@
+λ x x0 : word128 * word128,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x4, x5, (x6, x7))%core,
+ uint128_t x9, uint8_t x10 = addcarryx_u128(0x0, x5, x7);
+ uint128_t x12, uint8_t x13 = addcarryx_u128(x10, x4, x6);
+ uint128_t x15, uint8_t x16 = subborrow_u128(0x0, x9, 0xffffffffffffffffffffffffL);
+ uint128_t x18, uint8_t x19 = subborrow_u128(x16, x12, 0xffffffff000000010000000000000000L);
+ uint128_t _, uint8_t x22 = subborrow_u128(x19, x13, 0x0);
+ uint128_t x23 = cmovznz(x22, x18, x12);
+ uint128_t x24 = cmovznz(x22, x15, x9);
+ return (x23, x24))
+(x, x0)%core
+     : word128 * word128 → word128 * word128 → ReturnType (uint128_t * uint128_t)
diff --git a/src/Specific/NISTP256/AMD128/feaddDisplay.v b/src/Specific/NISTP256/AMD128/feaddDisplay.v
new file mode 100644
index 000000000..cde97baed
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/feaddDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.NISTP256.AMD128.feadd.
+Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
+
+Check display add.
diff --git a/src/Specific/NISTP256/AMD128/femul.v b/src/Specific/NISTP256/AMD128/femul.v
new file mode 100644
index 000000000..7c2ecbec1
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/femul.v
@@ -0,0 +1,14 @@
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.NISTP256.AMD128.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition mul :
+  { mul : feBW_small -> feBW_small -> feBW_small
+  | forall a b, phiM_small (mul a b) = F.mul (phiM_small a) (phiM_small b) }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_mul ().
+  Show Ltac Profile.
+Time Defined.
+
+Print Assumptions mul.
diff --git a/src/Specific/NISTP256/AMD128/femulDisplay.log b/src/Specific/NISTP256/AMD128/femulDisplay.log
new file mode 100644
index 000000000..3edcd5cba
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/femulDisplay.log
@@ -0,0 +1,40 @@
+λ x x0 : word128 * word128,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x4, x5, (x6, x7))%core,
+ uint128_t x9, uint128_t x10 = mulx_u128(x5, x7);
+ uint128_t x12, uint128_t x13 = mulx_u128(x5, x6);
+ uint128_t x15, uint8_t x16 = addcarryx_u128(0x0, x10, x12);
+ uint128_t x18, uint8_t _ = addcarryx_u128(0x0, x16, x13);
+ uint128_t x21, uint128_t _ = mulx_u128(x9, 0x1000000000000000000000001L);
+ uint128_t x24, uint128_t x25 = mulx_u128(x21, 0xffffffffffffffffffffffffL);
+ uint128_t x27, uint128_t x28 = mulx_u128(x21, 0xffffffff000000010000000000000000L);
+ uint128_t x30, uint8_t x31 = addcarryx_u128(0x0, x25, x27);
+ uint128_t x33, uint8_t _ = addcarryx_u128(0x0, x31, x28);
+ uint128_t _, uint8_t x37 = addcarryx_u128(0x0, x9, x24);
+ uint128_t x39, uint8_t x40 = addcarryx_u128(x37, x15, x30);
+ uint128_t x42, uint8_t x43 = addcarryx_u128(x40, x18, x33);
+ uint128_t x45, uint128_t x46 = mulx_u128(x4, x7);
+ uint128_t x48, uint128_t x49 = mulx_u128(x4, x6);
+ uint128_t x51, uint8_t x52 = addcarryx_u128(0x0, x46, x48);
+ uint128_t x54, uint8_t _ = addcarryx_u128(0x0, x52, x49);
+ uint128_t x57, uint8_t x58 = addcarryx_u128(0x0, x39, x45);
+ uint128_t x60, uint8_t x61 = addcarryx_u128(x58, x42, x51);
+ uint128_t x63, uint8_t x64 = addcarryx_u128(x61, x43, x54);
+ uint128_t x66, uint128_t _ = mulx_u128(x57, 0x1000000000000000000000001L);
+ uint128_t x69, uint128_t x70 = mulx_u128(x66, 0xffffffffffffffffffffffffL);
+ uint128_t x72, uint128_t x73 = mulx_u128(x66, 0xffffffff000000010000000000000000L);
+ uint128_t x75, uint8_t x76 = addcarryx_u128(0x0, x70, x72);
+ uint128_t x78, uint8_t _ = addcarryx_u128(0x0, x76, x73);
+ uint128_t _, uint8_t x82 = addcarryx_u128(0x0, x57, x69);
+ uint128_t x84, uint8_t x85 = addcarryx_u128(x82, x60, x75);
+ uint128_t x87, uint8_t x88 = addcarryx_u128(x85, x63, x78);
+ uint8_t x89 = (x88 + x64);
+ uint128_t x91, uint8_t x92 = subborrow_u128(0x0, x84, 0xffffffffffffffffffffffffL);
+ uint128_t x94, uint8_t x95 = subborrow_u128(x92, x87, 0xffffffff000000010000000000000000L);
+ uint128_t _, uint8_t x98 = subborrow_u128(x95, x89, 0x0);
+ uint128_t x99 = cmovznz(x98, x94, x87);
+ uint128_t x100 = cmovznz(x98, x91, x84);
+ return (x99, x100))
+(x, x0)%core
+     : word128 * word128 → word128 * word128 → ReturnType (uint128_t * uint128_t)
diff --git a/src/Specific/NISTP256/AMD128/femulDisplay.v b/src/Specific/NISTP256/AMD128/femulDisplay.v
new file mode 100644
index 000000000..86a058019
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/femulDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.NISTP256.AMD128.femul.
+Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
+
+Check display mul.
diff --git a/src/Specific/NISTP256/AMD128/fenz.v b/src/Specific/NISTP256/AMD128/fenz.v
new file mode 100644
index 000000000..c1a91fa38
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/fenz.v
@@ -0,0 +1,16 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.NISTP256.AMD128.Synthesis.
+Local Open Scope Z_scope.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition nonzero :
+  { nonzero : feBW_small -> BoundedWord.BoundedWord 1 adjusted_bitwidth bound1
+  | forall a, (BoundedWord.BoundedWordToZ _ _ _ (nonzero a) =? 0) = (if Decidable.dec (phiM_small a = F.of_Z m 0) then true else false) }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_nonzero ().
+  Show Ltac Profile.
+Time Defined.
+
+Print Assumptions nonzero.
diff --git a/src/Specific/NISTP256/AMD128/fenzDisplay.log b/src/Specific/NISTP256/AMD128/fenzDisplay.log
new file mode 100644
index 000000000..58f9ac4f9
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/fenzDisplay.log
@@ -0,0 +1,20 @@
+λ x : word128 * word128,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x1, x2)%core,
+ uint128_t x3 = x2 | x1;
+ return x3)
+x
+     : word128 * word128 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in
+                                                                    lower) with
+                                                             | 0%Z => Eq
+                                                             | Z.pos _ => Lt
+                                                             | Z.neg _ => Gt
+                                                             end with
+                                                       | Eq => true
+                                                       | Lt => true
+                                                       | Gt => false
+                                                       end then Some 7 else None) with
+                                             | Some lgsz => Syntax.TWord lgsz
+                                             | None => Syntax.TZ
+                                             end)
diff --git a/src/Specific/NISTP256/AMD128/fenzDisplay.v b/src/Specific/NISTP256/AMD128/fenzDisplay.v
new file mode 100644
index 000000000..18ff51330
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/fenzDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.NISTP256.AMD128.fenz.
+Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
+
+Check display nonzero.
diff --git a/src/Specific/NISTP256/AMD128/feopp.v b/src/Specific/NISTP256/AMD128/feopp.v
new file mode 100644
index 000000000..682541e8c
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/feopp.v
@@ -0,0 +1,14 @@
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.NISTP256.AMD128.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition opp :
+  { opp : feBW_small -> feBW_small
+  | forall a, phiM_small (opp a) = F.opp (phiM_small a) }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_opp ().
+  Show Ltac Profile.
+Time Defined.
+
+Print Assumptions opp.
diff --git a/src/Specific/NISTP256/AMD128/feoppDisplay.log b/src/Specific/NISTP256/AMD128/feoppDisplay.log
new file mode 100644
index 000000000..ea60d9f66
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/feoppDisplay.log
@@ -0,0 +1,14 @@
+λ x : word128 * word128,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x1, x2)%core,
+ uint128_t x4, uint8_t x5 = subborrow_u128(0x0, 0x0, x2);
+ uint128_t x7, uint8_t x8 = subborrow_u128(x5, 0x0, x1);
+ uint128_t x9 = (uint128_t)cmovznz(x8, 0x0, 0xffffffffffffffffffffffffffffffffL);
+ uint128_t x10 = (x9 & 0xffffffffffffffffffffffffL);
+ uint128_t x12, uint8_t x13 = addcarryx_u128(0x0, x4, x10);
+ uint128_t x14 = (x9 & 0xffffffff000000010000000000000000L);
+ uint128_t x16, uint8_t _ = addcarryx_u128(x13, x7, x14);
+ (Return x16, Return x12))
+x
+     : word128 * word128 → ReturnType (uint128_t * uint128_t)
diff --git a/src/Specific/NISTP256/AMD128/feoppDisplay.v b/src/Specific/NISTP256/AMD128/feoppDisplay.v
new file mode 100644
index 000000000..8c84f30d2
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/feoppDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.NISTP256.AMD128.feopp.
+Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
+
+Check display opp.
diff --git a/src/Specific/NISTP256/AMD128/fesub.v b/src/Specific/NISTP256/AMD128/fesub.v
new file mode 100644
index 000000000..f8a59ec86
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/fesub.v
@@ -0,0 +1,14 @@
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.NISTP256.AMD128.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition sub :
+  { sub : feBW_small -> feBW_small -> feBW_small
+  | forall a b, phiM_small (sub a b) = F.sub (phiM_small a) (phiM_small b) }.
+Proof.
+  Set Ltac Profiling.
+  Time synthesize_sub ().
+  Show Ltac Profile.
+Time Defined.
+
+Print Assumptions sub.
diff --git a/src/Specific/NISTP256/AMD128/fesubDisplay.log b/src/Specific/NISTP256/AMD128/fesubDisplay.log
new file mode 100644
index 000000000..70f224d33
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/fesubDisplay.log
@@ -0,0 +1,14 @@
+λ x x0 : word128 * word128,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x4, x5, (x6, x7))%core,
+ uint128_t x9, uint8_t x10 = subborrow_u128(0x0, x5, x7);
+ uint128_t x12, uint8_t x13 = subborrow_u128(x10, x4, x6);
+ uint128_t x14 = (uint128_t)cmovznz(x13, 0x0, 0xffffffffffffffffffffffffffffffffL);
+ uint128_t x15 = (x14 & 0xffffffffffffffffffffffffL);
+ uint128_t x17, uint8_t x18 = addcarryx_u128(0x0, x9, x15);
+ uint128_t x19 = (x14 & 0xffffffff000000010000000000000000L);
+ uint128_t x21, uint8_t _ = addcarryx_u128(x18, x12, x19);
+ (Return x21, Return x17))
+(x, x0)%core
+     : word128 * word128 → word128 * word128 → ReturnType (uint128_t * uint128_t)
diff --git a/src/Specific/NISTP256/AMD128/fesubDisplay.v b/src/Specific/NISTP256/AMD128/fesubDisplay.v
new file mode 100644
index 000000000..4e46b2272
--- /dev/null
+++ b/src/Specific/NISTP256/AMD128/fesubDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.NISTP256.AMD128.fesub.
+Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
+
+Check display sub.