Fix overflow concerns and add Serde functions

spec/Common/Utils.cry

@@ -29,6 +29,44 @@ bit_to_bool b = if b then 1 else 0
 bool_to_bit : [1] -> Bit
 bool_to_bit b = if b == 1 then True else False
 
+/**
+ * Convert an Integral value of 'n' bits to a `Bit`.
+ * ```repl
+ * :prove int_to_bit`{8} 1 == True
+ * :prove int_to_bit`{8} 0 == False
+ * ```
+ */
+int_to_bit : {n} (fin n, n >= 1) => [n] -> Bit
+int_to_bit b = if b == 1 then True else False
+
+/**
+ * Convert an Integral value of 'n' bits to a `Bit`.
+ * ```repl
+ * :prove bit_to_integer True == 1
+ * :prove bit_to_integer False == 0
+ * ```
+ */
+bit_to_integer : Bit -> Integer
+bit_to_integer b = if b then 1 else 0
+
+/**
+ * Convert from a `Z` type tp a fixed size bit type.
+ * ```repl
+ * :prove (fromIntegral`{13} (3:[384])) == (3 : Z 13)
+ * :prove (fromIntegral`{13} (14:[384])) == (1 : Z 13)
+ * :prove (fromIntegral`{13} (13:[384])) == (0 : Z 13)
+ */
+fromIntegral : {n, m} (fin n, n >= 1, fin m, m >= 1) => [m] -> Z n
+fromIntegral value = fromInteger (toInteger value)
+
+/**
+ * Convert from a fixed size bit type to a `Z` type.
+ * ```repl
+ * :prove (toIntegral`{m=384} (3 : Z 13) == (3:[384]))
+ */
+toIntegral : {n, m} (fin n, n >= 1, fin m, m >= 1) => Z n -> [m]
+toIntegral value = fromInteger (fromZ value)
+
 /**
  * Calculates the gcd and Bezout coefficients,
  *   using the Extended Euclidean Algorithm (recursive).
@@ -76,25 +114,34 @@ multinv x m =
 
 /**
  * Compute the modular inverse of x
- *  i.e. return y such that x * y % modulus == 1
- * Precondition: x != 0
+ *  i.e. return y such that x * y % n == 1
+ * Precondition: x != 0 mod n
  * ```repl
- * :prove modular_inverse 7492 319 == 177
- * :prove modular_inverse (-3) 319 == 106
+ * :prove modular_inverse`{319} (fromInteger 7492) == 177
+ * :prove modular_inverse`{319} (fromInteger (-3)) == 106
  * ```
  * NOTE: we just chose the values at "random." Checked against: https://planetcalc.com/3298/.
  */
-modular_inverse : Integer -> Integer -> Integer
-modular_inverse x modulus = multinv x' modulus where
-    x' = if x < 0 then x % modulus
-         else x
+modular_inverse : {n} (fin n, n >= 1) => Z n -> Z n
+modular_inverse x = fromInteger (multinv (fromZ x) `n)
 
 /**
  * Divide two field elements: x by y
  * ```repl
- * :prov div 3 7492 319 == 212
- * :prov div 3 (-7492) 319 == 107
+ * :prov div_mod (3 : Z 319) (fromInteger 7492) == 212
+ * :prov div_mod (3 : Z 319) (fromInteger (-7492))== 107
  * ```
  */
-div : Integer -> Integer -> Integer -> Integer
-div x y modulus = (x * (modular_inverse y modulus)) % modulus
+div_mod : {n} (fin n, n >= 1) => Z n -> Z n -> Z n
+div_mod x y = x * (modular_inverse y)
+
+/**
+ * Exponentiation in the specified modulo field `n`.
+ * @see https://github.com/ethereum/c-kzg-4844/blob/main/src/common/fr.c#L93
+ * ```repl
+ * :prove pow_mod (3 : Z 7) 2 == 2
+ * :prove pow_mod`{2} (fromInteger 1) 18 == 1
+ * :prove pow_mod`{3} (0 : Z 3) 5 == 0
+ */
+pow_mod : {n} (fin n, n >= 1) => Z n -> Integer -> Z n
+pow_mod base exp = base ^^ exp

spec/Spec/BlsEC.cry

@@ -10,22 +10,16 @@ module Spec::BlsEC where
 
 import Common::Utils
 
-/**
- * Size of a G1 point
- */
-type G1Bits = 384
-
-/**
- * Serialized G1 point
- */
-type Bytes48 = [G1Bits]
-
 /**
  * G1 elliptic curve point
+ *
+ * Note: by using the Z type, all modular arithmetic
+ *  is handled automatically and there is no potential
+ *  for any overflow errors.
  */
 type G1Point =
-    { xCoord : Bytes48
-    , yCoord : Bytes48
+    { xCoord : Z Fp
+    , yCoord : Z Fp
     }
 
 /**
@@ -56,8 +50,7 @@ G1 =
  *  finite field Fp, where p is the prime defined below.
  * @see https://hackmd.io/@Wimet/S1dvK2NBh#The-Curve
  */
-Fp : Bytes48
-Fp = 4002409555221667393417789825735904156556882819939007885332058136124031650490837864442687629129015664037894272559787
+type Fp = 4002409555221667393417789825735904156556882819939007885332058136124031650490837864442687629129015664037894272559787
 
 /**
  * Determines whether or not the given point is on the G1 curve.
@@ -73,27 +66,25 @@ Fp = 400240955522166739341778982573590415655688281993900788533205813612403165049
  */
 g1_is_valid_point : G1Point -> Bit
 g1_is_valid_point point =
-    (y^^2 - x^^3) % modulus == 4
+    y^^2 - x^^3 == 4
     where
-        x = toInteger point.xCoord
-        y = toInteger point.yCoord
-        modulus = toInteger Fp
+        x = point.xCoord
+        y = point.yCoord
 
 /**
  * Double a G1 point
  * @see https://github.com/ethereum/py_ecc/blob/main/py_ecc/bls12_381/bls12_381_curve.py#L84
  */
 g1_double : G1Point -> G1Point
 g1_double point = newPoint where
-    x = toInteger point.xCoord
-    y = toInteger point.yCoord
-    modulus = toInteger Fp
-    m = div (3 * x^^2) (2 * y) modulus
+    x = point.xCoord
+    y = point.yCoord
+    m = div_mod (3 * x^^2) (2 * y)
     newX = m^^2 - (2 * x)
     newY = m * (x - newX) - y
     newPoint =
-        { xCoord = fromInteger (newX % modulus)
-        , yCoord = fromInteger (newY % modulus)
+        { xCoord = newX
+        , yCoord = newY
         }
 
 /**
@@ -107,16 +98,15 @@ g1_add p1 p2 =
     else if (x2 == x1) && (y2 == y1) then
         g1_double p1
     else
-        { xCoord = fromInteger (newX % modulus)
-        , yCoord = fromInteger (newY % modulus)
+        { xCoord = newX
+        , yCoord = newY
         }
     where
-    x1 = toInteger p1.xCoord
-    y1 = toInteger p1.yCoord
-    x2 = toInteger p2.xCoord
-    y2 = toInteger p2.yCoord
-    modulus = toInteger Fp
-    m = div (y2 - y1) (x2 - x1) modulus
+    x1 = p1.xCoord
+    y1 = p1.yCoord
+    x2 = p2.xCoord
+    y2 = p2.yCoord
+    m = div_mod (y2 - y1) (x2 - x1)
     newX = m^^2 - x1 - x2
     newY = m * (x1 - newX) - y1
 
@@ -169,8 +159,14 @@ G1_5P =
 
 G1_6P : G1Point
 G1_6P =
-    { xCoord = 0x06e82f6da4520f85c5d27d8f329eccfa05944fd1096b20734c894966d12a9e2a9a9744529d7212d33883113a0cadb909
-    , yCoord = 0x17d81038f7d60bee9110d9c0d6d1102fe2d998c957f28e31ec284cc04134df8e47e8f82ff3af2e60a6d9688a4563477c
+    { xCoord = 1063080548659463434646774310890803636667161539235054707411467714858983518890075240133758563865893724012200489498889
+    , yCoord = 3669927104170827068533340245967707139563249539898402807511810342954528074138727808893798913182606104785795124774780
+    }
+
+G1_7P : G1Point
+G1_7P =
+    { xCoord = 3872473689207892378470335395114902631176541028916158626161662840934315241539439160301564344905260612642783644023991
+    , yCoord = 2547806390474846378491145127515427451279430889101277169890334737406180277792171092197824251632631671609860505999900
     }
 
 /**
@@ -187,6 +183,9 @@ g1_point_eq p1 p2 =
  * :prove test_g1_is_valid_point G1_2P
  * :prove test_g1_is_valid_point G1_3P
  * :prove test_g1_is_valid_point G1_4P
+ * :prove test_g1_is_valid_point G1_5P
+ * :prove test_g1_is_valid_point G1_6P
+ * :prove test_g1_is_valid_point G1_7P
  */
 test_g1_is_valid_point : G1Point -> Bit
 property test_g1_is_valid_point point = g1_is_valid_point point
@@ -213,15 +212,11 @@ property test_g1_double p1 p2 =
  * :prove test_g1_add G1 G1 G1_2P
  * :prove test_g1_add G1 G1_2P G1_3P
  * :prove test_g1_add G1_2P G1 G1_3P
- * :prove test_g1_add G1 G1_3P G1_4P
  * :prove test_g1_add G1_3P G1 G1_4P
  * :prove test_g1_add G1_2P G1_2P G1_4P
  * :prove test_g1_add G1 G1_4P G1_5P
- * :prove test_g1_add G1_4P G1 G1_5P
- * :prove test_g1_add G1_2P G1_3P G1_5P
  * :prove test_g1_add G1_3P G1_2P G1_5P
  * :prove test_g1_add G1_2P G1_4P G1_6P
- * :prove test_g1_add G1_4P G1_2P G1_6P
  * ```
  */
 test_g1_add : G1Point -> G1Point -> G1Point -> Bit

spec/Spec/BlsHelpers.cry

@@ -5,6 +5,8 @@
 module Spec::BlsHelpers where
 
 import Common::Utils
+import Spec::BlsEC
+import Spec::BlsSerde
 
 /**
  * BLS field elements are 256-bits long.
@@ -17,31 +19,28 @@ type BlsFieldElement = [BlsFieldSize]
  * Specified by the consensus-specs.
  * @see https://github.com/ethereum/consensus-specs/blob/dev/specs/deneb/polynomial-commitments.md#constants
  */
-BLS_MODULUS : BlsFieldElement
-BLS_MODULUS = 52435875175126190479447740508185965837690552500527637822603658699938581184513
+type BLS_MODULUS = 52435875175126190479447740508185965837690552500527637822603658699938581184513
 
 /**
  * Compute the modular inverse of x
  *  i.e. return y such that x * y % BLS_MODULUS == 1
- * Precondition: x != 0
+ * Precondition: x != 0 BLS_MODULUS
  * @see https://github.com/ethereum/consensus-specs/blob/dev/specs/deneb/polynomial-commitments.md#bls_modular_inverse
  * NOTE: Cryptol can not perform exponentiation with negative exponents,
  *  we cannot just execute `x^^(-1) % BLS_MODULUS` like the Python spec does.
  */
 bls_modular_inverse : BlsFieldElement -> BlsFieldElement
-bls_modular_inverse x = fromInteger (modular_inverse x' modulus) where
-    x' = toInteger x
-    modulus = toInteger BLS_MODULUS
+bls_modular_inverse x = toIntegral (modular_inverse x') where
+    x' = fromIntegral`{BLS_MODULUS} x
 
 /**
  * Divide two field elements: x by y
  * @see https://github.com/ethereum/consensus-specs/blob/dev/specs/deneb/polynomial-commitments.md#div
  */
 bls_div : BlsFieldElement -> BlsFieldElement -> BlsFieldElement
-bls_div x y = fromInteger (div x' y' modulus) where
-    x' = toInteger x
-    y' = toInteger y
-    modulus = toInteger BLS_MODULUS
+bls_div x y = toIntegral (div_mod x' y') where
+    x' = fromIntegral`{BLS_MODULUS} x
+    y' = fromIntegral`{BLS_MODULUS} y
 
 /**
  * Return x to power of [0, n-1].
@@ -51,7 +50,39 @@ bls_div x y = fromInteger (div x' y' modulus) where
  */
 compute_powers : {n} (fin n, width n <= 64, n >= 2) => BlsFieldElement -> [n]BlsFieldElement
 compute_powers x = powers where
-        powers = [x] # [(powers@(i-1) * x) % BLS_MODULUS | i <- [1 .. n-1]]
+        x' = fromIntegral`{BLS_MODULUS} x
+        powers' = [x'] # [powers'@(i-1) * x' | i <- [1 .. n-1]]
+        powers = [toIntegral xi' | xi' <- powers']
+
+/**
+ * Performs a multi-scalar multiplication between G1 `points` and `scalars`.
+ * @see https://github.com/ethereum/consensus-specs/blob/dev/specs/deneb/polynomial-commitments.md#multi_exp
+ */
+g1_multi_exp : {len} (fin len, len >= 1) => [len]G1Point -> [len]UInt64 -> G1Point
+g1_multi_exp points scalars = results!0 where
+    results = [G1_INFINITY] # [g1_add (results@i) (g1_multi (points@i) (scalars@i)) | i <- [0 .. len-1]]
+
+/**
+ * Deserialize the G1 bytes into a G1 point
+ * ```repl
+ * :prove bytes48_to_G1 G1_POINT_AT_INFINITY == G1_INFINITY
+ * :prove bytes48_to_G1 G1_2P_COMPRESSED == G1_2P
+ * :prove bytes48_to_G1 G1_7P_COMPRESSED == G1_7P
+ * ```
+ */
+bytes48_to_G1 : Bytes48 -> G1Point
+bytes48_to_G1 bytes = decompress_G1 bytes
+
+/**
+ * Serialize the G1 point into G1 bytes
+ * ```repl
+ * :prove g1_to_bytes48 G1_INFINITY == G1_POINT_AT_INFINITY
+ * :prove g1_to_bytes48 G1_2P == G1_2P_COMPRESSED
+ * :prove g1_to_bytes48 G1_7P == G1_7P_COMPRESSED
+ * ```
+ */
+g1_to_bytes48 : G1Point -> Bytes48
+g1_to_bytes48 point = compress_G1 point
 
 /*
  * ===============
@@ -96,3 +127,16 @@ property test_bls_div x y expected =
 test_compute_powers : {n} (fin n, width n <= 64, n >= 2) => BlsFieldElement -> [n]BlsFieldElement -> Bit
 property test_compute_powers x expected =
     join (compute_powers`{n} x) == join expected
+
+/**
+ * Unit tests for `g1_multi_exp`.
+ * ```repl
+ * :prove test_g1_multi_exp`{1} [G1] [1] G1
+ * :prove test_g1_multi_exp`{2} [G1, G1] [2, 3] G1_5P
+ * :prove test_g1_multi_exp`{2} [G1_3P, G1_2P] [1, 2] G1_7P
+ * :prove test_g1_multi_exp`{3} [G1_4P, G1_2P, G1_3P] [2, 3, 5] (g1_multi_exp`{2} [G1_5P, G1_7P] [3, 2])
+ * ```
+ */
+test_g1_multi_exp : {len} (fin len, len >= 1) => [len]G1Point -> [len]UInt64 -> G1Point -> Bit
+property test_g1_multi_exp points scalars expected =
+    g1_point_eq (g1_multi_exp points scalars) expected