aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/X25519
diff options
context:
space:
mode:
Diffstat (limited to 'src/Specific/X25519')
-rw-r--r--src/Specific/X25519/C32/CurveParameters.v436
-rwxr-xr-xsrc/Specific/X25519/C32/compiler.sh2
-rw-r--r--src/Specific/X25519/C32/freeze.v12
-rw-r--r--src/Specific/X25519/C32/freezeDisplay.log38
-rw-r--r--src/Specific/X25519/C32/freezeDisplay.v4
-rwxr-xr-xsrc/Specific/X25519/C64/compiler.sh2
-rw-r--r--src/Specific/X25519/C64/freeze.v12
-rw-r--r--src/Specific/X25519/C64/freezeDisplay.log23
-rw-r--r--src/Specific/X25519/C64/freezeDisplay.v4
-rw-r--r--src/Specific/X25519/C64/parameters.json75
10 files changed, 313 insertions, 295 deletions
diff --git a/src/Specific/X25519/C32/CurveParameters.v b/src/Specific/X25519/C32/CurveParameters.v
index 5040bf182..c8c7cb04f 100644
--- a/src/Specific/X25519/C32/CurveParameters.v
+++ b/src/Specific/X25519/C32/CurveParameters.v
@@ -11,234 +11,234 @@ Module Curve <: CurveParameters.
Definition bitwidth : Z := 32.
Definition s : Z := 2^255.
Definition c : list limb := [(1, 19)].
- Definition carry_chain1 := Eval vm_compute in Some (seq 0 (pred sz)).
- Definition carry_chain2 := Some [0;1]%nat.
+ Definition carry_chain1 : option (list nat) := Eval vm_compute in Some (seq 0 (pred sz)).
+ Definition carry_chain2 : option (list nat) := Eval vm_compute in Some [0; 1]%nat.
- Definition a24 := 121665%Z.
- Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *)
+ Definition a24 : Z := 121665.
+ Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *)
Definition mul_code : option (Z^sz -> Z^sz -> Z^sz)
:= Some (fun a b =>
(* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
- let '(in_9, in_8, in_7, in_6, in_5, in_4, in_3, in_2, in_1, in_0) := a in
- let '(in2_9, in2_8, in2_7, in2_6, in2_5, in2_4, in2_3, in2_2, in2_1, in2_0) := b in
- dlet output_0 := in2_0 * in_0 in
-dlet output_1 := in2_0 * in_1 +
- in2_1 * in_0 in
-dlet output_2 := 2 * in2_1 * in_1 +
- in2_0 * in_2 +
- in2_2 * in_0 in
-dlet output_3 := in2_1 * in_2 +
- in2_2 * in_1 +
- in2_0 * in_3 +
- in2_3 * in_0 in
-dlet output_4 := in2_2 * in_2 +
- 2 * (in2_1 * in_3 +
- in2_3 * in_1) +
- in2_0 * in_4 +
- in2_4 * in_0 in
-dlet output_5 := in2_2 * in_3 +
- in2_3 * in_2 +
- in2_1 * in_4 +
- in2_4 * in_1 +
- in2_0 * in_5 +
- in2_5 * in_0 in
-dlet output_6 := 2 * (in2_3 * in_3 +
- in2_1 * in_5 +
- in2_5 * in_1) +
- in2_2 * in_4 +
- in2_4 * in_2 +
- in2_0 * in_6 +
- in2_6 * in_0 in
-dlet output_7 := in2_3 * in_4 +
- in2_4 * in_3 +
- in2_2 * in_5 +
- in2_5 * in_2 +
- in2_1 * in_6 +
- in2_6 * in_1 +
- in2_0 * in_7 +
- in2_7 * in_0 in
-dlet output_8 := in2_4 * in_4 +
- 2 * (in2_3 * in_5 +
- in2_5 * in_3 +
- in2_1 * in_7 +
- in2_7 * in_1) +
- in2_2 * in_6 +
- in2_6 * in_2 +
- in2_0 * in_8 +
- in2_8 * in_0 in
-dlet output_9 := in2_4 * in_5 +
- in2_5 * in_4 +
- in2_3 * in_6 +
- in2_6 * in_3 +
- in2_2 * in_7 +
- in2_7 * in_2 +
- in2_1 * in_8 +
- in2_8 * in_1 +
- in2_0 * in_9 +
- in2_9 * in_0 in
-dlet output_10 := 2 * (in2_5 * in_5 +
- in2_3 * in_7 +
- in2_7 * in_3 +
- in2_1 * in_9 +
- in2_9 * in_1) +
- in2_4 * in_6 +
- in2_6 * in_4 +
- in2_2 * in_8 +
- in2_8 * in_2 in
-dlet output_11 := in2_5 * in_6 +
- in2_6 * in_5 +
- in2_4 * in_7 +
- in2_7 * in_4 +
- in2_3 * in_8 +
- in2_8 * in_3 +
- in2_2 * in_9 +
- in2_9 * in_2 in
-dlet output_12 := in2_6 * in_6 +
- 2 * (in2_5 * in_7 +
- in2_7 * in_5 +
- in2_3 * in_9 +
- in2_9 * in_3) +
- in2_4 * in_8 +
- in2_8 * in_4 in
-dlet output_13 := in2_6 * in_7 +
- in2_7 * in_6 +
- in2_5 * in_8 +
- in2_8 * in_5 +
- in2_4 * in_9 +
- in2_9 * in_4 in
-dlet output_14 := 2 * (in2_7 * in_7 +
- in2_5 * in_9 +
- in2_9 * in_5) +
- in2_6 * in_8 +
- in2_8 * in_6 in
-dlet output_15 := in2_7 * in_8 +
- in2_8 * in_7 +
- in2_6 * in_9 +
- in2_9 * in_6 in
-dlet output_16 := in2_8 * in_8 +
- 2 * (in2_7 * in_9 +
- in2_9 * in_7) in
-dlet output_17 := in2_8 * in_9 +
- in2_9 * in_8 in
-dlet output_18 := 2 * in2_9 * in_9 in
-dlet output_8 := output_8 + output_18 << 4 in
-dlet output_8 := output_8 + output_18 << 1 in
-dlet output_8 := output_8 + output_18 in
-dlet output_7 := output_7 + output_17 << 4 in
-dlet output_7 := output_7 + output_17 << 1 in
-dlet output_7 := output_7 + output_17 in
-dlet output_6 := output_6 + output_16 << 4 in
-dlet output_6 := output_6 + output_16 << 1 in
-dlet output_6 := output_6 + output_16 in
-dlet output_5 := output_5 + output_15 << 4 in
-dlet output_5 := output_5 + output_15 << 1 in
-dlet output_5 := output_5 + output_15 in
-dlet output_4 := output_4 + output_14 << 4 in
-dlet output_4 := output_4 + output_14 << 1 in
-dlet output_4 := output_4 + output_14 in
-dlet output_3 := output_3 + output_13 << 4 in
-dlet output_3 := output_3 + output_13 << 1 in
-dlet output_3 := output_3 + output_13 in
-dlet output_2 := output_2 + output_12 << 4 in
-dlet output_2 := output_2 + output_12 << 1 in
-dlet output_2 := output_2 + output_12 in
-dlet output_1 := output_1 + output_11 << 4 in
-dlet output_1 := output_1 + output_11 << 1 in
-dlet output_1 := output_1 + output_11 in
-dlet output_0 := output_0 + output_10 << 4 in
-dlet output_0 := output_0 + output_10 << 1 in
-dlet output_0 := output_0 + output_10 in
-(output_9, output_8, output_7, output_6, output_5, output_4, output_3, output_2, output_1, output_0)
+ let '(in9, in8, in7, in6, in5, in4, in3, in2, in1, in0) := a in
+ let '(in29, in28, in27, in26, in25, in24, in23, in22, in21, in20) := b in
+ dlet output0 := in20 * in0 in
+ dlet output1 := in20 * in1 +
+ in21 * in0 in
+ dlet output2 := 2 * in21 * in1 +
+ in20 * in2 +
+ in22 * in0 in
+ dlet output3 := in21 * in2 +
+ in22 * in1 +
+ in20 * in3 +
+ in23 * in0 in
+ dlet output4 := in22 * in2 +
+ 2 * (in21 * in3 +
+ in23 * in1) +
+ in20 * in4 +
+ in24 * in0 in
+ dlet output5 := in22 * in3 +
+ in23 * in2 +
+ in21 * in4 +
+ in24 * in1 +
+ in20 * in5 +
+ in25 * in0 in
+ dlet output6 := 2 * (in23 * in3 +
+ in21 * in5 +
+ in25 * in1) +
+ in22 * in4 +
+ in24 * in2 +
+ in20 * in6 +
+ in26 * in0 in
+ dlet output7 := in23 * in4 +
+ in24 * in3 +
+ in22 * in5 +
+ in25 * in2 +
+ in21 * in6 +
+ in26 * in1 +
+ in20 * in7 +
+ in27 * in0 in
+ dlet output8 := in24 * in4 +
+ 2 * (in23 * in5 +
+ in25 * in3 +
+ in21 * in7 +
+ in27 * in1) +
+ in22 * in6 +
+ in26 * in2 +
+ in20 * in8 +
+ in28 * in0 in
+ dlet output9 := in24 * in5 +
+ in25 * in4 +
+ in23 * in6 +
+ in26 * in3 +
+ in22 * in7 +
+ in27 * in2 +
+ in21 * in8 +
+ in28 * in1 +
+ in20 * in9 +
+ in29 * in0 in
+ dlet output10 := 2 * (in25 * in5 +
+ in23 * in7 +
+ in27 * in3 +
+ in21 * in9 +
+ in29 * in1) +
+ in24 * in6 +
+ in26 * in4 +
+ in22 * in8 +
+ in28 * in2 in
+ dlet output11 := in25 * in6 +
+ in26 * in5 +
+ in24 * in7 +
+ in27 * in4 +
+ in23 * in8 +
+ in28 * in3 +
+ in22 * in9 +
+ in29 * in2 in
+ dlet output12 := in26 * in6 +
+ 2 * (in25 * in7 +
+ in27 * in5 +
+ in23 * in9 +
+ in29 * in3) +
+ in24 * in8 +
+ in28 * in4 in
+ dlet output13 := in26 * in7 +
+ in27 * in6 +
+ in25 * in8 +
+ in28 * in5 +
+ in24 * in9 +
+ in29 * in4 in
+ dlet output14 := 2 * (in27 * in7 +
+ in25 * in9 +
+ in29 * in5) +
+ in26 * in8 +
+ in28 * in6 in
+ dlet output15 := in27 * in8 +
+ in28 * in7 +
+ in26 * in9 +
+ in29 * in6 in
+ dlet output16 := in28 * in8 +
+ 2 * (in27 * in9 +
+ in29 * in7) in
+ dlet output17 := in28 * in9 +
+ in29 * in8 in
+ dlet output18 := 2 * in29 * in9 in
+ dlet output8 := output8 + output18 << 4 in
+ dlet output8 := output8 + output18 << 1 in
+ dlet output8 := output8 + output18 in
+ dlet output7 := output7 + output17 << 4 in
+ dlet output7 := output7 + output17 << 1 in
+ dlet output7 := output7 + output17 in
+ dlet output6 := output6 + output16 << 4 in
+ dlet output6 := output6 + output16 << 1 in
+ dlet output6 := output6 + output16 in
+ dlet output5 := output5 + output15 << 4 in
+ dlet output5 := output5 + output15 << 1 in
+ dlet output5 := output5 + output15 in
+ dlet output4 := output4 + output14 << 4 in
+ dlet output4 := output4 + output14 << 1 in
+ dlet output4 := output4 + output14 in
+ dlet output3 := output3 + output13 << 4 in
+ dlet output3 := output3 + output13 << 1 in
+ dlet output3 := output3 + output13 in
+ dlet output2 := output2 + output12 << 4 in
+ dlet output2 := output2 + output12 << 1 in
+ dlet output2 := output2 + output12 in
+ dlet output1 := output1 + output11 << 4 in
+ dlet output1 := output1 + output11 << 1 in
+ dlet output1 := output1 + output11 in
+ dlet output0 := output0 + output10 << 4 in
+ dlet output0 := output0 + output10 << 1 in
+ dlet output0 := output0 + output10 in
+ (output9, output8, output7, output6, output5, output4, output3, output2, output1, output0)
).
Definition square_code : option (Z^sz -> Z^sz)
:= Some (fun a =>
(* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)
- let '(in_9, in_8, in_7, in_6, in_5, in_4, in_3, in_2, in_1, in_0) := a in
-dlet output_0 := in_0 * in_0 in
-dlet output_1 := 2 * in_0 * in_1 in
-dlet output_2 := 2 * (in_1 * in_1 +
- in_0 * in_2) in
-dlet output_3 := 2 * (in_1 * in_2 +
- in_0 * in_3) in
-dlet output_4 := in_2 * in_2 +
- 4 * in_1 * in_3 +
- 2 * in_0 * in_4 in
-dlet output_5 := 2 * (in_2 * in_3 +
- in_1 * in_4 +
- in_0 * in_5) in
-dlet output_6 := 2 * (in_3 * in_3 +
- in_2 * in_4 +
- in_0 * in_6 +
- 2 * in_1 * in_5) in
-dlet output_7 := 2 * (in_3 * in_4 +
- in_2 * in_5 +
- in_1 * in_6 +
- in_0 * in_7) in
-dlet output_8 := in_4 * in_4 +
- 2 * (in_2 * in_6 +
- in_0 * in_8 +
- 2 * (in_1 * in_7 +
- in_3 * in_5)) in
-dlet output_9 := 2 * (in_4 * in_5 +
- in_3 * in_6 +
- in_2 * in_7 +
- in_1 * in_8 +
- in_0 * in_9) in
-dlet output_10 := 2 * (in_5 * in_5 +
- in_4 * in_6 +
- in_2 * in_8 +
- 2 * (in_3 * in_7 +
- in_1 * in_9)) in
-dlet output_11 := 2 * (in_5 * in_6 +
- in_4 * in_7 +
- in_3 * in_8 +
- in_2 * in_9) in
-dlet output_12 := in_6 * in_6 +
- 2 * (in_4 * in_8 +
- 2 * (in_5 * in_7 +
- in_3 * in_9)) in
-dlet output_13 := 2 * (in_6 * in_7 +
- in_5 * in_8 +
- in_4 * in_9) in
-dlet output_14 := 2 * (in_7 * in_7 +
- in_6 * in_8 +
- 2 * in_5 * in_9) in
-dlet output_15 := 2 * (in_7 * in_8 +
- in_6 * in_9) in
-dlet output_16 := in_8 * in_8 +
- 4 * in_7 * in_9 in
-dlet output_17 := 2 * in_8 * in_9 in
-dlet output_18 := 2 * in_9 * in_9 in
-dlet output_8 := output_8 + output_18 << 4 in
-dlet output_8 := output_8 + output_18 << 1 in
-dlet output_8 := output_8 + output_18 in
-dlet output_7 := output_7 + output_17 << 4 in
-dlet output_7 := output_7 + output_17 << 1 in
-dlet output_7 := output_7 + output_17 in
-dlet output_6 := output_6 + output_16 << 4 in
-dlet output_6 := output_6 + output_16 << 1 in
-dlet output_6 := output_6 + output_16 in
-dlet output_5 := output_5 + output_15 << 4 in
-dlet output_5 := output_5 + output_15 << 1 in
-dlet output_5 := output_5 + output_15 in
-dlet output_4 := output_4 + output_14 << 4 in
-dlet output_4 := output_4 + output_14 << 1 in
-dlet output_4 := output_4 + output_14 in
-dlet output_3 := output_3 + output_13 << 4 in
-dlet output_3 := output_3 + output_13 << 1 in
-dlet output_3 := output_3 + output_13 in
-dlet output_2 := output_2 + output_12 << 4 in
-dlet output_2 := output_2 + output_12 << 1 in
-dlet output_2 := output_2 + output_12 in
-dlet output_1 := output_1 + output_11 << 4 in
-dlet output_1 := output_1 + output_11 << 1 in
-dlet output_1 := output_1 + output_11 in
-dlet output_0 := output_0 + output_10 << 4 in
-dlet output_0 := output_0 + output_10 << 1 in
-dlet output_0 := output_0 + output_10 in
-(output_9, output_8, output_7, output_6, output_5, output_4, output_3, output_2, output_1, output_0)
+ let '(in9, in8, in7, in6, in5, in4, in3, in2, in1, in0) := a in
+ dlet output0 := in0 * in0 in
+ dlet output1 := 2 * in0 * in1 in
+ dlet output2 := 2 * (in1 * in1 +
+ in0 * in2) in
+ dlet output3 := 2 * (in1 * in2 +
+ in0 * in3) in
+ dlet output4 := in2 * in2 +
+ 4 * in1 * in3 +
+ 2 * in0 * in4 in
+ dlet output5 := 2 * (in2 * in3 +
+ in1 * in4 +
+ in0 * in5) in
+ dlet output6 := 2 * (in3 * in3 +
+ in2 * in4 +
+ in0 * in6 +
+ 2 * in1 * in5) in
+ dlet output7 := 2 * (in3 * in4 +
+ in2 * in5 +
+ in1 * in6 +
+ in0 * in7) in
+ dlet output8 := in4 * in4 +
+ 2 * (in2 * in6 +
+ in0 * in8 +
+ 2 * (in1 * in7 +
+ in3 * in5)) in
+ dlet output9 := 2 * (in4 * in5 +
+ in3 * in6 +
+ in2 * in7 +
+ in1 * in8 +
+ in0 * in9) in
+ dlet output10 := 2 * (in5 * in5 +
+ in4 * in6 +
+ in2 * in8 +
+ 2 * (in3 * in7 +
+ in1 * in9)) in
+ dlet output11 := 2 * (in5 * in6 +
+ in4 * in7 +
+ in3 * in8 +
+ in2 * in9) in
+ dlet output12 := in6 * in6 +
+ 2 * (in4 * in8 +
+ 2 * (in5 * in7 +
+ in3 * in9)) in
+ dlet output13 := 2 * (in6 * in7 +
+ in5 * in8 +
+ in4 * in9) in
+ dlet output14 := 2 * (in7 * in7 +
+ in6 * in8 +
+ 2 * in5 * in9) in
+ dlet output15 := 2 * (in7 * in8 +
+ in6 * in9) in
+ dlet output16 := in8 * in8 +
+ 4 * in7 * in9 in
+ dlet output17 := 2 * in8 * in9 in
+ dlet output18 := 2 * in9 * in9 in
+ dlet output8 := output8 + output18 << 4 in
+ dlet output8 := output8 + output18 << 1 in
+ dlet output8 := output8 + output18 in
+ dlet output7 := output7 + output17 << 4 in
+ dlet output7 := output7 + output17 << 1 in
+ dlet output7 := output7 + output17 in
+ dlet output6 := output6 + output16 << 4 in
+ dlet output6 := output6 + output16 << 1 in
+ dlet output6 := output6 + output16 in
+ dlet output5 := output5 + output15 << 4 in
+ dlet output5 := output5 + output15 << 1 in
+ dlet output5 := output5 + output15 in
+ dlet output4 := output4 + output14 << 4 in
+ dlet output4 := output4 + output14 << 1 in
+ dlet output4 := output4 + output14 in
+ dlet output3 := output3 + output13 << 4 in
+ dlet output3 := output3 + output13 << 1 in
+ dlet output3 := output3 + output13 in
+ dlet output2 := output2 + output12 << 4 in
+ dlet output2 := output2 + output12 << 1 in
+ dlet output2 := output2 + output12 in
+ dlet output1 := output1 + output11 << 4 in
+ dlet output1 := output1 + output11 << 1 in
+ dlet output1 := output1 + output11 in
+ dlet output0 := output0 + output10 << 4 in
+ dlet output0 := output0 + output10 << 1 in
+ dlet output0 := output0 + output10 in
+ (output9, output8, output7, output6, output5, output4, output3, output2, output1, output0)
).
Definition upper_bound_of_exponent : option (Z -> Z) := None.
diff --git a/src/Specific/X25519/C32/compiler.sh b/src/Specific/X25519/C32/compiler.sh
index e64df574a..401968c8b 100755
--- a/src/Specific/X25519/C32/compiler.sh
+++ b/src/Specific/X25519/C32/compiler.sh
@@ -1,4 +1,4 @@
#!/bin/sh
set -eu
-gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes $@
+gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes "$@"
diff --git a/src/Specific/X25519/C32/freeze.v b/src/Specific/X25519/C32/freeze.v
new file mode 100644
index 000000000..9af1e8e0f
--- /dev/null
+++ b/src/Specific/X25519/C32/freeze.v
@@ -0,0 +1,12 @@
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.X25519.C32.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition freeze :
+ { freeze : feBW -> feBW
+ | forall a, phiBW (freeze a) = phiBW a }.
+Proof.
+ Set Ltac Profiling.
+ Time synthesize_freeze ().
+ Show Ltac Profile.
+Time Defined.
diff --git a/src/Specific/X25519/C32/freezeDisplay.log b/src/Specific/X25519/C32/freezeDisplay.log
new file mode 100644
index 000000000..b2582c34a
--- /dev/null
+++ b/src/Specific/X25519/C32/freezeDisplay.log
@@ -0,0 +1,38 @@
+λ x : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x17, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core,
+ uint32_t x20, uint8_t x21 = Op (Syntax.SubWithGetBorrow 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x2, Const 67108845);
+ uint32_t x23, uint8_t x24 = Op (Syntax.SubWithGetBorrow 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x21, Return x4, 0x1ffffff);
+ uint32_t x26, uint8_t x27 = Op (Syntax.SubWithGetBorrow 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x24, Return x6, 0x3ffffff);
+ uint32_t x29, uint8_t x30 = Op (Syntax.SubWithGetBorrow 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x27, Return x8, 0x1ffffff);
+ uint32_t x32, uint8_t x33 = Op (Syntax.SubWithGetBorrow 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x30, Return x10, 0x3ffffff);
+ uint32_t x35, uint8_t x36 = Op (Syntax.SubWithGetBorrow 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x33, Return x12, 0x1ffffff);
+ uint32_t x38, uint8_t x39 = Op (Syntax.SubWithGetBorrow 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x36, Return x14, 0x3ffffff);
+ uint32_t x41, uint8_t x42 = Op (Syntax.SubWithGetBorrow 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x39, Return x16, 0x1ffffff);
+ uint32_t x44, uint8_t x45 = Op (Syntax.SubWithGetBorrow 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x42, Return x18, 0x3ffffff);
+ uint32_t x47, uint8_t x48 = Op (Syntax.SubWithGetBorrow 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x45, Return x17, 0x1ffffff);
+ uint32_t x49 = (uint32_t)cmovznz(x48, 0x0, 0xffffffff);
+ uint32_t x50 = x49 & Const 67108845;
+ uint32_t x52, uint8_t x53 = Op (Syntax.AddWithGetCarry 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x20, Return x50);
+ uint32_t x54 = x49 & 0x1ffffff;
+ uint32_t x56, uint8_t x57 = Op (Syntax.AddWithGetCarry 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x53, Return x23, Return x54);
+ uint32_t x58 = x49 & 0x3ffffff;
+ uint32_t x60, uint8_t x61 = Op (Syntax.AddWithGetCarry 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x57, Return x26, Return x58);
+ uint32_t x62 = x49 & 0x1ffffff;
+ uint32_t x64, uint8_t x65 = Op (Syntax.AddWithGetCarry 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x61, Return x29, Return x62);
+ uint32_t x66 = x49 & 0x3ffffff;
+ uint32_t x68, uint8_t x69 = Op (Syntax.AddWithGetCarry 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x65, Return x32, Return x66);
+ uint32_t x70 = x49 & 0x1ffffff;
+ uint32_t x72, uint8_t x73 = Op (Syntax.AddWithGetCarry 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x69, Return x35, Return x70);
+ uint32_t x74 = x49 & 0x3ffffff;
+ uint32_t x76, uint8_t x77 = Op (Syntax.AddWithGetCarry 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x73, Return x38, Return x74);
+ uint32_t x78 = x49 & 0x1ffffff;
+ uint32_t x80, uint8_t x81 = Op (Syntax.AddWithGetCarry 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x77, Return x41, Return x78);
+ uint32_t x82 = x49 & 0x3ffffff;
+ uint32_t x84, uint8_t x85 = Op (Syntax.AddWithGetCarry 26 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x81, Return x44, Return x82);
+ uint32_t x86 = x49 & 0x1ffffff;
+ uint32_t x88, uint8_t _ = Op (Syntax.AddWithGetCarry 25 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x85, Return x47, Return x86);
+ (Return x88, Return x84, Return x80, Return x76, Return x72, Return x68, Return x64, Return x60, Return x56, Return x52))
+x
+ : 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)
diff --git a/src/Specific/X25519/C32/freezeDisplay.v b/src/Specific/X25519/C32/freezeDisplay.v
new file mode 100644
index 000000000..dc0defdc8
--- /dev/null
+++ b/src/Specific/X25519/C32/freezeDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.X25519.C32.freeze.
+Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
+
+Check display freeze.
diff --git a/src/Specific/X25519/C64/compiler.sh b/src/Specific/X25519/C64/compiler.sh
index e64df574a..401968c8b 100755
--- a/src/Specific/X25519/C64/compiler.sh
+++ b/src/Specific/X25519/C64/compiler.sh
@@ -1,4 +1,4 @@
#!/bin/sh
set -eu
-gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes $@
+gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes "$@"
diff --git a/src/Specific/X25519/C64/freeze.v b/src/Specific/X25519/C64/freeze.v
new file mode 100644
index 000000000..ef826dba5
--- /dev/null
+++ b/src/Specific/X25519/C64/freeze.v
@@ -0,0 +1,12 @@
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.X25519.C64.Synthesis.
+
+(* TODO : change this to field once field isomorphism happens *)
+Definition freeze :
+ { freeze : feBW -> feBW
+ | forall a, phiBW (freeze a) = phiBW a }.
+Proof.
+ Set Ltac Profiling.
+ Time synthesize_freeze ().
+ Show Ltac Profile.
+Time Defined.
diff --git a/src/Specific/X25519/C64/freezeDisplay.log b/src/Specific/X25519/C64/freezeDisplay.log
new file mode 100644
index 000000000..e25c7e397
--- /dev/null
+++ b/src/Specific/X25519/C64/freezeDisplay.log
@@ -0,0 +1,23 @@
+λ x : word64 * word64 * word64 * word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x7, x8, x6, x4, x2)%core,
+ uint64_t x10, uint8_t x11 = subborrow_u51(0x0, x2, 0x7ffffffffffed);
+ uint64_t x13, uint8_t x14 = subborrow_u51(x11, x4, 0x7ffffffffffff);
+ uint64_t x16, uint8_t x17 = subborrow_u51(x14, x6, 0x7ffffffffffff);
+ uint64_t x19, uint8_t x20 = subborrow_u51(x17, x8, 0x7ffffffffffff);
+ uint64_t x22, uint8_t x23 = subborrow_u51(x20, x7, 0x7ffffffffffff);
+ uint64_t x24 = (uint64_t)cmovznz(x23, 0x0, 0xffffffffffffffffL);
+ uint64_t x25 = (x24 & 0x7ffffffffffed);
+ uint64_t x27, uint8_t x28 = addcarryx_u51(0x0, x10, x25);
+ uint64_t x29 = (x24 & 0x7ffffffffffff);
+ uint64_t x31, uint8_t x32 = addcarryx_u51(x28, x13, x29);
+ uint64_t x33 = (x24 & 0x7ffffffffffff);
+ uint64_t x35, uint8_t x36 = addcarryx_u51(x32, x16, x33);
+ uint64_t x37 = (x24 & 0x7ffffffffffff);
+ uint64_t x39, uint8_t x40 = addcarryx_u51(x36, x19, x37);
+ uint64_t x41 = (x24 & 0x7ffffffffffff);
+ uint64_t x43, uint8_t _ = addcarryx_u51(x40, x22, x41);
+ (Return x43, Return x39, Return x35, 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/X25519/C64/freezeDisplay.v b/src/Specific/X25519/C64/freezeDisplay.v
new file mode 100644
index 000000000..d3f1a5499
--- /dev/null
+++ b/src/Specific/X25519/C64/freezeDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.X25519.C64.freeze.
+Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon.
+
+Check display freeze.
diff --git a/src/Specific/X25519/C64/parameters.json b/src/Specific/X25519/C64/parameters.json
deleted file mode 100644
index b03a8cee5..000000000
--- a/src/Specific/X25519/C64/parameters.json
+++ /dev/null
@@ -1,75 +0,0 @@
-{
- "modulus" : "2^255-19",
- "base" : "51",
- "operations" : ["femul", "fesquare", "ladderstep", "freeze"],
- "sz" : "5",
- "bitwidth" : "64",
- "s" : "2^255",
- "c" : [["1", "19"]],
- "carry_chain1" : "default",
- "carry_chain2" : ["0", "1"],
- "a24" : "121665",
- "coef_div_modulus" : "2",
- "mul_header" : "(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)",
- "mul_code"
- :
- "
- uint128_t t[5];
- limb r0,r1,r2,r3,r4,s0,s1,s2,s3,s4,c;
-
- r0 = in[0];
- r1 = in[1];
- r2 = in[2];
- r3 = in[3];
- r4 = in[4];
-
- s0 = in2[0];
- s1 = in2[1];
- s2 = in2[2];
- s3 = in2[3];
- s4 = in2[4];
-
- t[0] = ((uint128_t) r0) * s0;
- t[1] = ((uint128_t) r0) * s1 + ((uint128_t) r1) * s0;
- t[2] = ((uint128_t) r0) * s2 + ((uint128_t) r2) * s0 + ((uint128_t) r1) * s1;
- t[3] = ((uint128_t) r0) * s3 + ((uint128_t) r3) * s0 + ((uint128_t) r1) * s2 + ((uint128_t) r2) * s1;
- t[4] = ((uint128_t) r0) * s4 + ((uint128_t) r4) * s0 + ((uint128_t) r3) * s1 + ((uint128_t) r1) * s3 + ((uint128_t) r2) * s2;
-
- r4 *= 19;
- r1 *= 19;
- r2 *= 19;
- r3 *= 19;
-
- t[0] += ((uint128_t) r4) * s1 + ((uint128_t) r1) * s4 + ((uint128_t) r2) * s3 + ((uint128_t) r3) * s2;
- t[1] += ((uint128_t) r4) * s2 + ((uint128_t) r2) * s4 + ((uint128_t) r3) * s3;
- t[2] += ((uint128_t) r4) * s3 + ((uint128_t) r3) * s4;
- t[3] += ((uint128_t) r4) * s4;
-",
- "square_header" : "(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)",
- "square_code"
- :
- "
- uint128_t t[5];
- limb r0,r1,r2,r3,r4,c;
- limb d0,d1,d2,d4,d419;
-
- r0 = in[0];
- r1 = in[1];
- r2 = in[2];
- r3 = in[3];
- r4 = in[4];
-
- do {
- d0 = r0 * 2;
- d1 = r1 * 2;
- d2 = r2 * 2 * 19;
- d419 = r4 * 19;
- d4 = d419 * 2;
-
- t[0] = ((uint128_t) r0) * r0 + ((uint128_t) d4) * r1 + (((uint128_t) d2) * (r3 ));
- t[1] = ((uint128_t) d0) * r1 + ((uint128_t) d4) * r2 + (((uint128_t) r3) * (r3 * 19));
- t[2] = ((uint128_t) d0) * r2 + ((uint128_t) r1) * r1 + (((uint128_t) d4) * (r3 ));
- t[3] = ((uint128_t) d0) * r3 + ((uint128_t) d1) * r2 + (((uint128_t) r4) * (d419 ));
- t[4] = ((uint128_t) d0) * r4 + ((uint128_t) d1) * r3 + (((uint128_t) r2) * (r2 ));
-"
-}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 14:45:46 +0000