diff options
Diffstat (limited to 'src/Specific/montgomery32_2e510m290x2e496m1_16limbs')
20 files changed, 0 insertions, 370 deletions
diff --git a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/CurveParameters.v b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/CurveParameters.v deleted file mode 100644 index 8dd31f795..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/CurveParameters.v +++ /dev/null @@ -1,39 +0,0 @@ -Require Import Crypto.Specific.Framework.RawCurveParameters. -Require Import Crypto.Util.LetIn. - -(*** -Modulus : 2^510 - 290*2^496 - 1 -Base: 32 -***) - -Definition curve : CurveParameters := - {| - sz := 16%nat; - base := 32; - bitwidth := 32; - s := 2^510; - c := [(1, 1); (290, 2^496)]; - carry_chains := None; - - a24 := None; - coef_div_modulus := None; - - goldilocks := None; - karatsuba := None; - montgomery := true; - freeze := Some false; - 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/montgomery32_2e510m290x2e496m1_16limbs/Synthesis.v b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/Synthesis.v deleted file mode 100644 index a51058007..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/Synthesis.v +++ /dev/null @@ -1,9 +0,0 @@ -Require Import Crypto.Specific.Framework.SynthesisFramework. -Require Import Crypto.Specific.montgomery32_2e510m290x2e496m1_16limbs.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/montgomery32_2e510m290x2e496m1_16limbs/compiler.sh b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/compiler.sh deleted file mode 100755 index b6155d473..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/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,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,0x00,0x00,0x30,0x39}' -Dbitwidth='32' -Dlimb_weight_gaps_array='{32,32,32,32,32,32,32,32,32,32,32,32,32,32,32,32}' -Dmodulus_array='{0x3e,0xdd,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff}' -Dmodulus_bytes_val='64' -Dmodulus_limbs='16' -Dq_mpz='(1_mpz<<510) - 290*(1_mpz<<496) - 1' "$@" diff --git a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/compilerxx.sh b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/compilerxx.sh deleted file mode 100755 index dc962804e..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/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,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,0x00,0x00,0x30,0x39}' -Dbitwidth='32' -Dlimb_weight_gaps_array='{32,32,32,32,32,32,32,32,32,32,32,32,32,32,32,32}' -Dmodulus_array='{0x3e,0xdd,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff,0xff}' -Dmodulus_bytes_val='64' -Dmodulus_limbs='16' -Dq_mpz='(1_mpz<<510) - 290*(1_mpz<<496) - 1' "$@" diff --git a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feadd.c b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feadd.c deleted file mode 100644 index 9ad623033..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feadd.c +++ /dev/null @@ -1,100 +0,0 @@ -static void feadd(uint32_t out[16], const uint32_t in1[16], const uint32_t in2[16]) { - { const uint32_t x32 = in1[15]; - { const uint32_t x33 = in1[14]; - { const uint32_t x31 = in1[13]; - { const uint32_t x29 = in1[12]; - { const uint32_t x27 = in1[11]; - { const uint32_t x25 = in1[10]; - { const uint32_t x23 = in1[9]; - { const uint32_t x21 = in1[8]; - { const uint32_t x19 = in1[7]; - { const uint32_t x17 = in1[6]; - { const uint32_t x15 = in1[5]; - { const uint32_t x13 = in1[4]; - { const uint32_t x11 = in1[3]; - { const uint32_t x9 = in1[2]; - { const uint32_t x7 = in1[1]; - { const uint32_t x5 = in1[0]; - { const uint32_t x62 = in2[15]; - { const uint32_t x63 = in2[14]; - { const uint32_t x61 = in2[13]; - { const uint32_t x59 = in2[12]; - { const uint32_t x57 = in2[11]; - { const uint32_t x55 = in2[10]; - { const uint32_t x53 = in2[9]; - { const uint32_t x51 = in2[8]; - { const uint32_t x49 = in2[7]; - { const uint32_t x47 = in2[6]; - { const uint32_t x45 = in2[5]; - { const uint32_t x43 = in2[4]; - { const uint32_t x41 = in2[3]; - { const uint32_t x39 = in2[2]; - { const uint32_t x37 = in2[1]; - { const uint32_t x35 = in2[0]; - { uint32_t x65; uint8_t x66 = _addcarryx_u32(0x0, x5, x35, &x65); - { uint32_t x68; uint8_t x69 = _addcarryx_u32(x66, x7, x37, &x68); - { uint32_t x71; uint8_t x72 = _addcarryx_u32(x69, x9, x39, &x71); - { uint32_t x74; uint8_t x75 = _addcarryx_u32(x72, x11, x41, &x74); - { uint32_t x77; uint8_t x78 = _addcarryx_u32(x75, x13, x43, &x77); - { uint32_t x80; uint8_t x81 = _addcarryx_u32(x78, x15, x45, &x80); - { uint32_t x83; uint8_t x84 = _addcarryx_u32(x81, x17, x47, &x83); - { uint32_t x86; uint8_t x87 = _addcarryx_u32(x84, x19, x49, &x86); - { uint32_t x89; uint8_t x90 = _addcarryx_u32(x87, x21, x51, &x89); - { uint32_t x92; uint8_t x93 = _addcarryx_u32(x90, x23, x53, &x92); - { uint32_t x95; uint8_t x96 = _addcarryx_u32(x93, x25, x55, &x95); - { uint32_t x98; uint8_t x99 = _addcarryx_u32(x96, x27, x57, &x98); - { uint32_t x101; uint8_t x102 = _addcarryx_u32(x99, x29, x59, &x101); - { uint32_t x104; uint8_t x105 = _addcarryx_u32(x102, x31, x61, &x104); - { uint32_t x107; uint8_t x108 = _addcarryx_u32(x105, x33, x63, &x107); - { uint32_t x110; uint8_t x111 = _addcarryx_u32(x108, x32, x62, &x110); - { uint32_t x113; uint8_t x114 = _subborrow_u32(0x0, x65, 0xffffffff, &x113); - { uint32_t x116; uint8_t x117 = _subborrow_u32(x114, x68, 0xffffffff, &x116); - { uint32_t x119; uint8_t x120 = _subborrow_u32(x117, x71, 0xffffffff, &x119); - { uint32_t x122; uint8_t x123 = _subborrow_u32(x120, x74, 0xffffffff, &x122); - { uint32_t x125; uint8_t x126 = _subborrow_u32(x123, x77, 0xffffffff, &x125); - { uint32_t x128; uint8_t x129 = _subborrow_u32(x126, x80, 0xffffffff, &x128); - { uint32_t x131; uint8_t x132 = _subborrow_u32(x129, x83, 0xffffffff, &x131); - { uint32_t x134; uint8_t x135 = _subborrow_u32(x132, x86, 0xffffffff, &x134); - { uint32_t x137; uint8_t x138 = _subborrow_u32(x135, x89, 0xffffffff, &x137); - { uint32_t x140; uint8_t x141 = _subborrow_u32(x138, x92, 0xffffffff, &x140); - { uint32_t x143; uint8_t x144 = _subborrow_u32(x141, x95, 0xffffffff, &x143); - { uint32_t x146; uint8_t x147 = _subborrow_u32(x144, x98, 0xffffffff, &x146); - { uint32_t x149; uint8_t x150 = _subborrow_u32(x147, x101, 0xffffffff, &x149); - { uint32_t x152; uint8_t x153 = _subborrow_u32(x150, x104, 0xffffffff, &x152); - { uint32_t x155; uint8_t x156 = _subborrow_u32(x153, x107, 0xffffffff, &x155); - { uint32_t x158; uint8_t x159 = _subborrow_u32(x156, x110, 0x3eddffff, &x158); - { uint32_t _; uint8_t x162 = _subborrow_u32(x159, x111, 0x0, &_); - { uint32_t x163 = cmovznz32(x162, x158, x110); - { uint32_t x164 = cmovznz32(x162, x155, x107); - { uint32_t x165 = cmovznz32(x162, x152, x104); - { uint32_t x166 = cmovznz32(x162, x149, x101); - { uint32_t x167 = cmovznz32(x162, x146, x98); - { uint32_t x168 = cmovznz32(x162, x143, x95); - { uint32_t x169 = cmovznz32(x162, x140, x92); - { uint32_t x170 = cmovznz32(x162, x137, x89); - { uint32_t x171 = cmovznz32(x162, x134, x86); - { uint32_t x172 = cmovznz32(x162, x131, x83); - { uint32_t x173 = cmovznz32(x162, x128, x80); - { uint32_t x174 = cmovznz32(x162, x125, x77); - { uint32_t x175 = cmovznz32(x162, x122, x74); - { uint32_t x176 = cmovznz32(x162, x119, x71); - { uint32_t x177 = cmovznz32(x162, x116, x68); - { uint32_t x178 = cmovznz32(x162, x113, x65); - out[0] = x178; - out[1] = x177; - out[2] = x176; - out[3] = x175; - out[4] = x174; - out[5] = x173; - out[6] = x172; - out[7] = x171; - out[8] = x170; - out[9] = x169; - out[10] = x168; - out[11] = x167; - out[12] = x166; - out[13] = x165; - out[14] = x164; - out[15] = x163; - }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} -} diff --git a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feadd.v b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feadd.v deleted file mode 100644 index e66a17d0a..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feadd.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.montgomery32_2e510m290x2e496m1_16limbs.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/montgomery32_2e510m290x2e496m1_16limbs/feaddDisplay.log b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feaddDisplay.log deleted file mode 100644 index 36c81d199..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feaddDisplay.log +++ /dev/null @@ -1,56 +0,0 @@ -λ x x0 : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, -Interp-η -(λ var : Syntax.base_type → Type, - λ '(x32, x33, x31, x29, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x62, x63, x61, x59, x57, x55, x53, x51, x49, x47, x45, x43, x41, x39, x37, x35))%core, - uint32_t x65, uint8_t x66 = addcarryx_u32(0x0, x5, x35); - uint32_t x68, uint8_t x69 = addcarryx_u32(x66, x7, x37); - uint32_t x71, uint8_t x72 = addcarryx_u32(x69, x9, x39); - uint32_t x74, uint8_t x75 = addcarryx_u32(x72, x11, x41); - uint32_t x77, uint8_t x78 = addcarryx_u32(x75, x13, x43); - uint32_t x80, uint8_t x81 = addcarryx_u32(x78, x15, x45); - uint32_t x83, uint8_t x84 = addcarryx_u32(x81, x17, x47); - uint32_t x86, uint8_t x87 = addcarryx_u32(x84, x19, x49); - uint32_t x89, uint8_t x90 = addcarryx_u32(x87, x21, x51); - uint32_t x92, uint8_t x93 = addcarryx_u32(x90, x23, x53); - uint32_t x95, uint8_t x96 = addcarryx_u32(x93, x25, x55); - uint32_t x98, uint8_t x99 = addcarryx_u32(x96, x27, x57); - uint32_t x101, uint8_t x102 = addcarryx_u32(x99, x29, x59); - uint32_t x104, uint8_t x105 = addcarryx_u32(x102, x31, x61); - uint32_t x107, uint8_t x108 = addcarryx_u32(x105, x33, x63); - uint32_t x110, uint8_t x111 = addcarryx_u32(x108, x32, x62); - uint32_t x113, uint8_t x114 = subborrow_u32(0x0, x65, 0xffffffff); - uint32_t x116, uint8_t x117 = subborrow_u32(x114, x68, 0xffffffff); - uint32_t x119, uint8_t x120 = subborrow_u32(x117, x71, 0xffffffff); - uint32_t x122, uint8_t x123 = subborrow_u32(x120, x74, 0xffffffff); - uint32_t x125, uint8_t x126 = subborrow_u32(x123, x77, 0xffffffff); - uint32_t x128, uint8_t x129 = subborrow_u32(x126, x80, 0xffffffff); - uint32_t x131, uint8_t x132 = subborrow_u32(x129, x83, 0xffffffff); - uint32_t x134, uint8_t x135 = subborrow_u32(x132, x86, 0xffffffff); - uint32_t x137, uint8_t x138 = subborrow_u32(x135, x89, 0xffffffff); - uint32_t x140, uint8_t x141 = subborrow_u32(x138, x92, 0xffffffff); - uint32_t x143, uint8_t x144 = subborrow_u32(x141, x95, 0xffffffff); - uint32_t x146, uint8_t x147 = subborrow_u32(x144, x98, 0xffffffff); - uint32_t x149, uint8_t x150 = subborrow_u32(x147, x101, 0xffffffff); - uint32_t x152, uint8_t x153 = subborrow_u32(x150, x104, 0xffffffff); - uint32_t x155, uint8_t x156 = subborrow_u32(x153, x107, 0xffffffff); - uint32_t x158, uint8_t x159 = subborrow_u32(x156, x110, 0x3eddffff); - uint32_t _, uint8_t x162 = subborrow_u32(x159, x111, 0x0); - uint32_t x163 = cmovznz32(x162, x158, x110); - uint32_t x164 = cmovznz32(x162, x155, x107); - uint32_t x165 = cmovznz32(x162, x152, x104); - uint32_t x166 = cmovznz32(x162, x149, x101); - uint32_t x167 = cmovznz32(x162, x146, x98); - uint32_t x168 = cmovznz32(x162, x143, x95); - uint32_t x169 = cmovznz32(x162, x140, x92); - uint32_t x170 = cmovznz32(x162, x137, x89); - uint32_t x171 = cmovznz32(x162, x134, x86); - uint32_t x172 = cmovznz32(x162, x131, x83); - uint32_t x173 = cmovznz32(x162, x128, x80); - uint32_t x174 = cmovznz32(x162, x125, x77); - uint32_t x175 = cmovznz32(x162, x122, x74); - uint32_t x176 = cmovznz32(x162, x119, x71); - uint32_t x177 = cmovznz32(x162, x116, x68); - uint32_t x178 = cmovznz32(x162, x113, x65); - return (x163, x164, x165, x166, x167, x168, x169, x170, x171, x172, x173, x174, x175, x176, x177, x178)) -(x, x0)%core - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) diff --git a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feaddDisplay.v b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feaddDisplay.v deleted file mode 100644 index f5411c7b9..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feaddDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.montgomery32_2e510m290x2e496m1_16limbs.feadd. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display add. diff --git a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/femul.v b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/femul.v deleted file mode 100644 index 2d0530515..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/femul.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.montgomery32_2e510m290x2e496m1_16limbs.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/montgomery32_2e510m290x2e496m1_16limbs/femulDisplay.v b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/femulDisplay.v deleted file mode 100644 index 6908019e6..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/femulDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.montgomery32_2e510m290x2e496m1_16limbs.femul. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display mul. diff --git a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fenz.c b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fenz.c deleted file mode 100644 index 5c5d21b0e..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fenz.c +++ /dev/null @@ -1,35 +0,0 @@ -static void fenz(ReturnType uint32_t out[1], const uint32_t in1[16]) { - { const uint32_t x29 = in1[15]; - { const uint32_t x30 = in1[14]; - { const uint32_t x28 = in1[13]; - { const uint32_t x26 = in1[12]; - { const uint32_t x24 = in1[11]; - { const uint32_t x22 = in1[10]; - { const uint32_t x20 = in1[9]; - { const uint32_t x18 = in1[8]; - { const uint32_t x16 = in1[7]; - { const uint32_t x14 = in1[6]; - { const uint32_t x12 = in1[5]; - { const uint32_t x10 = in1[4]; - { const uint32_t x8 = in1[3]; - { const uint32_t x6 = in1[2]; - { const uint32_t x4 = in1[1]; - { const uint32_t x2 = in1[0]; - { uint32_t x31 = (x30 | x29); - { uint32_t x32 = (x28 | x31); - { uint32_t x33 = (x26 | x32); - { uint32_t x34 = (x24 | x33); - { uint32_t x35 = (x22 | x34); - { uint32_t x36 = (x20 | x35); - { uint32_t x37 = (x18 | x36); - { uint32_t x38 = (x16 | x37); - { uint32_t x39 = (x14 | x38); - { uint32_t x40 = (x12 | x39); - { uint32_t x41 = (x10 | x40); - { uint32_t x42 = (x8 | x41); - { uint32_t x43 = (x6 | x42); - { uint32_t x44 = (x4 | x43); - { uint32_t x45 = (x2 | x44); - out[0] = x45; - }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} -} diff --git a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fenz.v b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fenz.v deleted file mode 100644 index f28b6235b..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fenz.v +++ /dev/null @@ -1,16 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.montgomery32_2e510m290x2e496m1_16limbs.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/montgomery32_2e510m290x2e496m1_16limbs/fenzDisplay.log b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fenzDisplay.log deleted file mode 100644 index eb0b6ea33..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fenzDisplay.log +++ /dev/null @@ -1,22 +0,0 @@ -λ x : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, -Interp-η -(λ var : Syntax.base_type → Type, - λ '(x29, x30, x28, x26, x24, x22, x20, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core, - uint32_t x31 = (x30 | x29); - uint32_t x32 = (x28 | x31); - uint32_t x33 = (x26 | x32); - uint32_t x34 = (x24 | x33); - uint32_t x35 = (x22 | x34); - uint32_t x36 = (x20 | x35); - uint32_t x37 = (x18 | x36); - uint32_t x38 = (x16 | x37); - uint32_t x39 = (x14 | x38); - uint32_t x40 = (x12 | x39); - uint32_t x41 = (x10 | x40); - uint32_t x42 = (x8 | x41); - uint32_t x43 = (x6 | x42); - uint32_t x44 = (x4 | x43); - uint32_t x45 = (x2 | x44); - return x45) -x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fenzDisplay.v b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fenzDisplay.v deleted file mode 100644 index beb477c79..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fenzDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.montgomery32_2e510m290x2e496m1_16limbs.fenz. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display nonzero. diff --git a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feopp.v b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feopp.v deleted file mode 100644 index ad725872f..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feopp.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.montgomery32_2e510m290x2e496m1_16limbs.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/montgomery32_2e510m290x2e496m1_16limbs/feoppDisplay.v b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feoppDisplay.v deleted file mode 100644 index 6ee281365..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/feoppDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.montgomery32_2e510m290x2e496m1_16limbs.feopp. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display opp. diff --git a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fesquare.c b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fesquare.c deleted file mode 100644 index e3345edfe..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fesquare.c +++ /dev/null @@ -1,5 +0,0 @@ -/* WARNING: This file was copied from Specific/CurveParameters/montgomery32/fesquare.c. - If you edit it here, changes will be erased the next time remake_curves.sh is run. */ -static void fesquare(uint32_t *out, const uint32_t *in) { - femul(out, in, in); -} diff --git a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fesub.v b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fesub.v deleted file mode 100644 index dffd1a5e9..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fesub.v +++ /dev/null @@ -1,14 +0,0 @@ -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.montgomery32_2e510m290x2e496m1_16limbs.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/montgomery32_2e510m290x2e496m1_16limbs/fesubDisplay.v b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fesubDisplay.v deleted file mode 100644 index 5819c30a6..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/fesubDisplay.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Crypto.Specific.montgomery32_2e510m290x2e496m1_16limbs.fesub. -Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. - -Check display sub. diff --git a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/py_interpreter.sh b/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/py_interpreter.sh deleted file mode 100755 index c7e51b970..000000000 --- a/src/Specific/montgomery32_2e510m290x2e496m1_16limbs/py_interpreter.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/sh -set -eu - -/usr/bin/env python3 "$@" -Dq='2**510 - 290*2**496 - 1' -Dmodulus_bytes='32' -Da24='121665' |