Fixing a Cryptol->Coq extraction issue.

apetcher-amazon · Apr 9, 2024 · d9cb16d · d9cb16d
1 parent 691274b
commit d9cb16d
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 12 deletions.
diff --git a/SAW/spec/EC/EC_mul.cry b/SAW/spec/EC/EC_mul.cry
@@ -374,5 +374,16 @@ validate_one f = res
 validate_one_wrapper: () -> felem -> Bit
 validate_one_wrapper _ x = validate_one x
 
+jacobianToAffine : JacobianBVPoint -> AffineBVPoint
+jacobianToAffine p = {X = x, Y = y} where
+  px = felem_from_bytes (p.X)
+  py = felem_from_bytes (p.Y)
+  pz = felem_from_bytes (p.Z)
+  z2 = felem_inv_sqr pz
+  x_raw = felem_mul px z2
+  z4 = felem_sqr z2
+  y_raw = felem_mul (felem_mul py pz) z4
+  x = (felem_to_bytes x_raw)
+  y = (felem_to_bytes y_raw)
 
 
diff --git a/SAW/spec/EC/EC_primitives.cry b/SAW/spec/EC/EC_primitives.cry
@@ -210,18 +210,6 @@ felem_inv_sqr in = ret where
 
 type AffineBVPoint = { X : [bit_length], Y : [bit_length]}
 
-jacobianToAffine : JacobianBVPoint -> AffineBVPoint
-jacobianToAffine p = {X = x, Y = y} where
- px = felem_from_bytes (p.X)
- py = felem_from_bytes (p.Y)
- pz = felem_from_bytes (p.Z)
- z2 = felem_inv_sqr pz
- x_raw = felem_mul px z2
- z4 = felem_sqr z2
- y_raw = felem_mul (felem_mul py pz) z4
- x = (felem_to_bytes x_raw)
- y = (felem_to_bytes y_raw)
-