diff options
Diffstat (limited to 'src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs')
21 files changed, 0 insertions, 243 deletions
diff --git a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/CurveParameters.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/CurveParameters.v deleted file mode 100644 index 36bcac59d..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/CurveParameters.v +++ /dev/null @@ -1,39 +0,0 @@ -Require Import Crypto.Specific.Framework.RawCurveParameters. -Require Import Crypto.Util.LetIn. - -(*** -Modulus : 2^256 - 2^224 + 2^192 + 2^96 - 1 -Base: 51.2 -***) - -Definition curve : CurveParameters := - {| - sz := 5%nat; - base := 51 + 1/5; - bitwidth := 64; - s := 2^256; - c := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)]; - carry_chains := Some [[3; 2; 0; 4]; [4; 3; 1; 0; 2]; [4; 3; 1; 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_2e256m2e224p2e192p2e96m1_5limbs/Synthesis.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/Synthesis.v deleted file mode 100644 index deb5c225d..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/Synthesis.v +++ /dev/null @@ -1,9 +0,0 @@ -Require Import Crypto.Specific.Framework.SynthesisFramework. -Require Import Crypto.Specific.solinas64_2e256m2e224p2e192p2e96m1_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_2e256m2e224p2e192p2e96m1_5limbs/compiler.sh b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/compiler.sh deleted file mode 100755 index bba022f1e..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_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,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{52,51,51,51,51}' -Dmodulus_array='{0xff,0xff,0xff,0xff,0x00,0x00,0x00,0x01,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff}' -Dmodulus_bytes_val='32' -Dmodulus_limbs='5' -Dq_mpz='(1_mpz<<256) - (1_mpz<<224) + (1_mpz<<192) + (1_mpz<<96) - 1' "$@" diff --git a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/compilerxx.sh b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/compilerxx.sh deleted file mode 100755 index 25318ed30..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_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,0x00,0x00,0x00,0x00,0x30,0x39}' -Dbitwidth='64' -Dlimb_weight_gaps_array='{52,51,51,51,51}' -Dmodulus_array='{0xff,0xff,0xff,0xff,0x00,0x00,0x00,0x01,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0x00,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff}' -Dmodulus_bytes_val='32' -Dmodulus_limbs='5' -Dq_mpz='(1_mpz<<256) - (1_mpz<<224) + (1_mpz<<192) + (1_mpz<<96) - 1' "$@" diff --git a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/feadd.c b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/feadd.c deleted file mode 100644 index a05766e0b..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_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_2e256m2e224p2e192p2e96m1_5limbs/feadd.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/feadd.v deleted file mode 100644 index 4e0dbfc51..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/feadd.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.solinas64_2e256m2e224p2e192p2e96m1_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_2e256m2e224p2e192p2e96m1_5limbs/feaddDisplay.log b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/feaddDisplay.log deleted file mode 100644 index bce3421b2..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_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_2e256m2e224p2e192p2e96m1_5limbs/feaddDisplay.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/feaddDisplay.v deleted file mode 100644 index c16c930d6..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/feaddDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.solinas64_2e256m2e224p2e192p2e96m1_5limbs.feadd. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display add. diff --git a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fecarry.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fecarry.v deleted file mode 100644 index 6af9c210b..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fecarry.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.solinas64_2e256m2e224p2e192p2e96m1_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_2e256m2e224p2e192p2e96m1_5limbs/fecarryDisplay.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fecarryDisplay.v deleted file mode 100644 index 69390f956..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fecarryDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.solinas64_2e256m2e224p2e192p2e96m1_5limbs.fecarry. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display carry. diff --git a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/femul.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/femul.v deleted file mode 100644 index 65a39b396..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/femul.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.solinas64_2e256m2e224p2e192p2e96m1_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_2e256m2e224p2e192p2e96m1_5limbs/femulDisplay.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/femulDisplay.v deleted file mode 100644 index bd3aad397..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/femulDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.solinas64_2e256m2e224p2e192p2e96m1_5limbs.femul. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display mul. diff --git a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fesquare.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fesquare.v deleted file mode 100644 index 48887f8fd..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fesquare.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.solinas64_2e256m2e224p2e192p2e96m1_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_2e256m2e224p2e192p2e96m1_5limbs/fesquareDisplay.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fesquareDisplay.v deleted file mode 100644 index 9e68ebde4..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fesquareDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.solinas64_2e256m2e224p2e192p2e96m1_5limbs.fesquare. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display square. diff --git a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fesub.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fesub.v deleted file mode 100644 index db1988e53..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fesub.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.solinas64_2e256m2e224p2e192p2e96m1_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_2e256m2e224p2e192p2e96m1_5limbs/fesubDisplay.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fesubDisplay.v deleted file mode 100644 index 571983faa..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/fesubDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.solinas64_2e256m2e224p2e192p2e96m1_5limbs.fesub. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display sub. diff --git a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/freeze.c b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/freeze.c deleted file mode 100644 index b5d95bd90..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_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, uint8_t x11 = Op (Syntax.SubWithGetBorrow 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x2, 0xfffffffffffff); - { uint64_t x13; ℤ x14 = _subborrow_u51ℤ(x11, x4, 0xfffffffffff, &x13); - { uint64_t x16; ℤ x17 = _subborrow_u51ℤ(x14, x6, 0x0, &x16); - { uint64_t x19; ℤ x20 = _subborrow_u51ℤ(x17, x8, 0x4000000000, &x19); - { uint64_t x22, uint8_t x23 = Op (Syntax.SubWithGetBorrow 51 Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x20, Return x7, 0x7fffffff80000); - { uint64_t x24 = cmovznz64(x23, 0x0, 0xffffffffffffffffL); - { uint64_t x25 = (x24 & 0xfffffffffffff); - { uint64_t x27, uint8_t x28 = Op (Syntax.AddWithGetCarry 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x10, Return x25); - { uint64_t x29 = (x24 & 0xfffffffffff); - { uint64_t x31; uint8_t x32 = _addcarryx_u51(x28, x13, x29, &x31); - { uint64_t x34; uint8_t x35 = _addcarryx_u51(x32, x16, 0x0, &x34); - { uint64_t x36 = (x24 & 0x4000000000); - { uint64_t x38; uint8_t x39 = _addcarryx_u51(x35, x19, x36, &x38); - { uint64_t x40 = (x24 & 0x7fffffff80000); - { uint64_t x42; uint8_t _ = _addcarryx_u51(x39, x22, x40, &x42); - out[0] = x27; - out[1] = x31; - out[2] = x34; - out[3] = x38; - out[4] = x42; - }}}}}}}}}}}}}}}}}}}} -} diff --git a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/freeze.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/freeze.v deleted file mode 100644 index e6fadc212..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/freeze.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.solinas64_2e256m2e224p2e192p2e96m1_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_2e256m2e224p2e192p2e96m1_5limbs/freezeDisplay.log b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/freezeDisplay.log deleted file mode 100644 index f5f1f30bc..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_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, uint8_t x11 = Op (Syntax.SubWithGetBorrow 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x2, 0xfffffffffffff); - uint64_t x13, ℤ x14 = subborrow_u51ℤ(x11, x4, 0xfffffffffff); - uint64_t x16, ℤ x17 = subborrow_u51ℤ(x14, x6, 0x0); - uint64_t x19, ℤ x20 = subborrow_u51ℤ(x17, x8, 0x4000000000); - uint64_t x22, uint8_t x23 = Op (Syntax.SubWithGetBorrow 51 Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x20, Return x7, 0x7fffffff80000); - uint64_t x24 = cmovznz64(x23, 0x0, 0xffffffffffffffffL); - uint64_t x25 = (x24 & 0xfffffffffffff); - uint64_t x27, uint8_t x28 = Op (Syntax.AddWithGetCarry 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x10, Return x25); - uint64_t x29 = (x24 & 0xfffffffffff); - uint64_t x31, uint8_t x32 = addcarryx_u51(x28, x13, x29); - uint64_t x34, uint8_t x35 = addcarryx_u51(x32, x16, 0x0); - uint64_t x36 = (x24 & 0x4000000000); - uint64_t x38, uint8_t x39 = addcarryx_u51(x35, x19, x36); - uint64_t x40 = (x24 & 0x7fffffff80000); - uint64_t x42, uint8_t _ = addcarryx_u51(x39, x22, x40); - (Return x42, Return x38, Return x34, Return x31, 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_2e256m2e224p2e192p2e96m1_5limbs/freezeDisplay.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/freezeDisplay.v deleted file mode 100644 index 316129c19..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/freezeDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.solinas64_2e256m2e224p2e192p2e96m1_5limbs.freeze. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display freeze. diff --git a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/py_interpreter.sh b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/py_interpreter.sh deleted file mode 100755 index 4d329b161..000000000 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1_5limbs/py_interpreter.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/sh -set -eu - -/usr/bin/env python3 "$@" -Dq='2**256 - 2**224 + 2**192 + 2**96 - 1' -Dmodulus_bytes='51.2' -Da24='121665' |