aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/solinas64_2e224m2e96p1_5limbs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Specific/solinas64_2e224m2e96p1_5limbs')
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/CurveParameters.v39
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/Synthesis.v9
-rwxr-xr-xsrc/Specific/solinas64_2e224m2e96p1_5limbs/compiler.sh4
-rwxr-xr-xsrc/Specific/solinas64_2e224m2e96p1_5limbs/compilerxx.sh4
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/feadd.c18
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/feadd.v14
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/feaddDisplay.log7
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/feaddDisplay.v4
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/fecarry.v14
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/fecarryDisplay.v4
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/femul.v14
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/femulDisplay.v4
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/fesquare.v14
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/fesquareDisplay.v4
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/fesub.v14
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/fesubDisplay.v4
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/freeze.c28
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/freeze.v14
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/freezeDisplay.log22
-rw-r--r--src/Specific/solinas64_2e224m2e96p1_5limbs/freezeDisplay.v4
-rwxr-xr-xsrc/Specific/solinas64_2e224m2e96p1_5limbs/py_interpreter.sh4
21 files changed, 0 insertions, 243 deletions
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/CurveParameters.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/CurveParameters.v
deleted file mode 100644
index 77da23e52..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/CurveParameters.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Require Import Crypto.Specific.Framework.RawCurveParameters.
-Require Import Crypto.Util.LetIn.
-
-(***
-Modulus : 2^224 - 2^96 + 1
-Base: 44.8
-***)
-
-Definition curve : CurveParameters :=
- {|
- sz := 5%nat;
- base := 44 + 4/5;
- bitwidth := 64;
- s := 2^224;
- c := [(1, -1); (2^96, 1)];
- carry_chains := Some [[1; 4]; [2; 0; 3; 1; 4]; [2; 0]]%nat;
-
- a24 := None;
- coef_div_modulus := Some 2%nat;
-
- goldilocks := None;
- karatsuba := None;
- montgomery := false;
- freeze := Some true;
- ladderstep := false;
-
- 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/solinas64_2e224m2e96p1_5limbs/Synthesis.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/Synthesis.v
deleted file mode 100644
index 898a8f2bb..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/Synthesis.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Require Import Crypto.Specific.Framework.SynthesisFramework.
-Require Import Crypto.Specific.solinas64_2e224m2e96p1_5limbs.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/solinas64_2e224m2e96p1_5limbs/compiler.sh b/src/Specific/solinas64_2e224m2e96p1_5limbs/compiler.sh
deleted file mode 100755
index a7e6c65ee..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/compiler.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-set -eu
-
-clang -fbracket-depth=999999 -march=native -mbmi2 -mtune=native -std=gnu11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{45,45,45,45,44}' -Dmodulus_array='{0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x01}' -Dmodulus_bytes_val='28' -Dmodulus_limbs='5' -Dq_mpz='(1_mpz<<224) - (1_mpz<<96) + 1' "$@"
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/compilerxx.sh b/src/Specific/solinas64_2e224m2e96p1_5limbs/compilerxx.sh
deleted file mode 100755
index 38dc9c684..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/compilerxx.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-set -eu
-
-clang++ -fbracket-depth=999999 -march=native -mbmi2 -mtune=native -std=gnu++11 -O3 -flto -fuse-ld=lld -fomit-frame-pointer -fwrapv -Wno-attributes -fno-strict-aliasing -Da24_hex='0x3039' -Da24_val='12345' -Da_minus_two_over_four_array='{0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{45,45,45,45,44}' -Dmodulus_array='{0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x01}' -Dmodulus_bytes_val='28' -Dmodulus_limbs='5' -Dq_mpz='(1_mpz<<224) - (1_mpz<<96) + 1' "$@"
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/feadd.c b/src/Specific/solinas64_2e224m2e96p1_5limbs/feadd.c
deleted file mode 100644
index a05766e0b..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/feadd.c
+++ /dev/null
@@ -1,18 +0,0 @@
-static void feadd(uint64_t out[5], const uint64_t in1[5], const uint64_t in2[5]) {
- { const uint64_t x10 = in1[4];
- { const uint64_t x11 = in1[3];
- { const uint64_t x9 = in1[2];
- { const uint64_t x7 = in1[1];
- { const uint64_t x5 = in1[0];
- { const uint64_t x18 = in2[4];
- { const uint64_t x19 = in2[3];
- { const uint64_t x17 = in2[2];
- { const uint64_t x15 = in2[1];
- { const uint64_t x13 = in2[0];
- out[0] = (x5 + x13);
- out[1] = (x7 + x15);
- out[2] = (x9 + x17);
- out[3] = (x11 + x19);
- out[4] = (x10 + x18);
- }}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/feadd.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/feadd.v
deleted file mode 100644
index 79416d067..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/feadd.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e224m2e96p1_5limbs.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.
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/feaddDisplay.log b/src/Specific/solinas64_2e224m2e96p1_5limbs/feaddDisplay.log
deleted file mode 100644
index bce3421b2..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/feaddDisplay.log
+++ /dev/null
@@ -1,7 +0,0 @@
-λ x x0 : word64 * word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core,
- ((x10 + x18), (x11 + x19), (x9 + x17), (x7 + x15), (x5 + x13)))
-(x, x0)%core
- : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/feaddDisplay.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/feaddDisplay.v
deleted file mode 100644
index 9b9de6003..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/feaddDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e224m2e96p1_5limbs.feadd.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display add.
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/fecarry.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/fecarry.v
deleted file mode 100644
index 054e09872..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/fecarry.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e224m2e96p1_5limbs.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition carry :
- { carry : feBW_loose -> feBW_tight
- | forall a, phiBW_tight (carry a) = (phiBW_loose a) }.
-Proof.
- Set Ltac Profiling.
- Time synthesize_carry ().
- Show Ltac Profile.
-Time Defined.
-
-Print Assumptions carry.
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/fecarryDisplay.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/fecarryDisplay.v
deleted file mode 100644
index 103629cd3..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/fecarryDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e224m2e96p1_5limbs.fecarry.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display carry.
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/femul.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/femul.v
deleted file mode 100644
index 24c302bc2..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/femul.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e224m2e96p1_5limbs.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition mul :
- { mul : feBW_loose -> feBW_loose -> feBW_tight
- | forall a b, phiBW_tight (mul a b) = F.mul (phiBW_loose a) (phiBW_loose b) }.
-Proof.
- Set Ltac Profiling.
- Time synthesize_mul ().
- Show Ltac Profile.
-Time Defined.
-
-Print Assumptions mul.
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/femulDisplay.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/femulDisplay.v
deleted file mode 100644
index 4ad58b459..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/femulDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e224m2e96p1_5limbs.femul.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display mul.
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/fesquare.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/fesquare.v
deleted file mode 100644
index fd71658c3..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/fesquare.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e224m2e96p1_5limbs.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition square :
- { square : feBW_loose -> feBW_tight
- | forall a, phiBW_tight (square a) = F.mul (phiBW_loose a) (phiBW_loose a) }.
-Proof.
- Set Ltac Profiling.
- Time synthesize_square ().
- Show Ltac Profile.
-Time Defined.
-
-Print Assumptions square.
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/fesquareDisplay.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/fesquareDisplay.v
deleted file mode 100644
index abbb96fd1..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/fesquareDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e224m2e96p1_5limbs.fesquare.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display square.
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/fesub.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/fesub.v
deleted file mode 100644
index c20396fbc..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/fesub.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e224m2e96p1_5limbs.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition sub :
- { sub : feBW_tight -> feBW_tight -> feBW_loose
- | forall a b, phiBW_loose (sub a b) = F.sub (phiBW_tight a) (phiBW_tight b) }.
-Proof.
- Set Ltac Profiling.
- Time synthesize_sub ().
- Show Ltac Profile.
-Time Defined.
-
-Print Assumptions sub.
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/fesubDisplay.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/fesubDisplay.v
deleted file mode 100644
index 0e61ade87..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/fesubDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e224m2e96p1_5limbs.fesub.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display sub.
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/freeze.c b/src/Specific/solinas64_2e224m2e96p1_5limbs/freeze.c
deleted file mode 100644
index 9bd4af647..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/freeze.c
+++ /dev/null
@@ -1,28 +0,0 @@
-static void freeze(uint64_t out[5], const uint64_t in1[5]) {
- { const uint64_t x7 = in1[4];
- { const uint64_t x8 = in1[3];
- { const uint64_t x6 = in1[2];
- { const uint64_t x4 = in1[1];
- { const uint64_t x2 = in1[0];
- { uint64_t x10, ℤ x11 = Op (Syntax.SubWithGetBorrow 45 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 3) (Syntax.TWord 6) Syntax.TZ) (0x0, Return x2, 0x1);
- { uint64_t x13, ℤ x14 = Op (Syntax.SubWithGetBorrow 45 Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 3) (Syntax.TWord 6) Syntax.TZ) (Return x11, Return x4, 0x0);
- { uint64_t x16, uint8_t x17 = Op (Syntax.SubWithGetBorrow 45 Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x14, Return x6, 0x1fffffffffc0);
- { uint64_t x19, uint8_t x20 = Op (Syntax.SubWithGetBorrow 45 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x17, Return x8, 0x1fffffffffff);
- { uint64_t x22, uint8_t x23 = Op (Syntax.SubWithGetBorrow 44 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x20, Return x7, 0xfffffffffff);
- { uint64_t x24 = cmovznz64(x23, 0x0, 0xffffffffffffffffL);
- { uint8_t x25 = ((uint8_t)x24 & 0x1);
- { uint64_t x27, uint8_t x28 = Op (Syntax.AddWithGetCarry 45 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x10, Return x25);
- { uint64_t x30, uint8_t x31 = Op (Syntax.AddWithGetCarry 45 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x28, Return x13, 0x0);
- { uint64_t x32 = (x24 & 0x1fffffffffc0);
- { uint64_t x34, uint8_t x35 = Op (Syntax.AddWithGetCarry 45 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x31, Return x16, Return x32);
- { uint64_t x36 = (x24 & 0x1fffffffffff);
- { uint64_t x38, uint8_t x39 = Op (Syntax.AddWithGetCarry 45 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x35, Return x19, Return x36);
- { uint64_t x40 = (x24 & 0xfffffffffff);
- { uint64_t x42, uint8_t _ = Op (Syntax.AddWithGetCarry 44 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x39, Return x22, Return x40);
- out[0] = x27;
- out[1] = x30;
- out[2] = x34;
- out[3] = x38;
- out[4] = x42;
- }}}}}}}}}}}}}}}}}}}}
-}
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/freeze.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/freeze.v
deleted file mode 100644
index b43ca8351..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/freeze.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.solinas64_2e224m2e96p1_5limbs.Synthesis.
-
-(* TODO : change this to field once field isomorphism happens *)
-Definition freeze :
- { freeze : feBW_tight -> feBW_limbwidths
- | forall a, phiBW_limbwidths (freeze a) = phiBW_tight a }.
-Proof.
- Set Ltac Profiling.
- Time synthesize_freeze ().
- Show Ltac Profile.
-Time Defined.
-
-Print Assumptions freeze.
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/freezeDisplay.log b/src/Specific/solinas64_2e224m2e96p1_5limbs/freezeDisplay.log
deleted file mode 100644
index 86c5ce8e8..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/freezeDisplay.log
+++ /dev/null
@@ -1,22 +0,0 @@
-λ x : word64 * word64 * word64 * word64 * word64,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x7, x8, x6, x4, x2)%core,
- uint64_t x10, ℤ x11 = Op (Syntax.SubWithGetBorrow 45 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 3) (Syntax.TWord 6) Syntax.TZ) (0x0, Return x2, 0x1);
- uint64_t x13, ℤ x14 = Op (Syntax.SubWithGetBorrow 45 Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 3) (Syntax.TWord 6) Syntax.TZ) (Return x11, Return x4, 0x0);
- uint64_t x16, uint8_t x17 = Op (Syntax.SubWithGetBorrow 45 Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x14, Return x6, 0x1fffffffffc0);
- uint64_t x19, uint8_t x20 = Op (Syntax.SubWithGetBorrow 45 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x17, Return x8, 0x1fffffffffff);
- uint64_t x22, uint8_t x23 = Op (Syntax.SubWithGetBorrow 44 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x20, Return x7, 0xfffffffffff);
- uint64_t x24 = cmovznz64(x23, 0x0, 0xffffffffffffffffL);
- uint8_t x25 = ((uint8_t)x24 & 0x1);
- uint64_t x27, uint8_t x28 = Op (Syntax.AddWithGetCarry 45 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x10, Return x25);
- uint64_t x30, uint8_t x31 = Op (Syntax.AddWithGetCarry 45 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x28, Return x13, 0x0);
- uint64_t x32 = (x24 & 0x1fffffffffc0);
- uint64_t x34, uint8_t x35 = Op (Syntax.AddWithGetCarry 45 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x31, Return x16, Return x32);
- uint64_t x36 = (x24 & 0x1fffffffffff);
- uint64_t x38, uint8_t x39 = Op (Syntax.AddWithGetCarry 45 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x35, Return x19, Return x36);
- uint64_t x40 = (x24 & 0xfffffffffff);
- uint64_t x42, uint8_t _ = Op (Syntax.AddWithGetCarry 44 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x39, Return x22, Return x40);
- (Return x42, Return x38, Return x34, Return x30, Return x27))
-x
- : word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/freezeDisplay.v b/src/Specific/solinas64_2e224m2e96p1_5limbs/freezeDisplay.v
deleted file mode 100644
index 46dc82d84..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/freezeDisplay.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Crypto.Specific.solinas64_2e224m2e96p1_5limbs.freeze.
-Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
-
-Check display freeze.
diff --git a/src/Specific/solinas64_2e224m2e96p1_5limbs/py_interpreter.sh b/src/Specific/solinas64_2e224m2e96p1_5limbs/py_interpreter.sh
deleted file mode 100755
index 81d1e73f5..000000000
--- a/src/Specific/solinas64_2e224m2e96p1_5limbs/py_interpreter.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/bin/sh
-set -eu
-
-/usr/bin/env python3 "$@" -Dq='2**224 - 2**96 + 1' -Dmodulus_bytes='44.8' -Da24='121665'