Add BLS Elliptic Curve support in Cryptol

spec/Spec/BlsHelpers.cry

@@ -0,0 +1,72 @@
+/**
+ * The module contains functions that perform BLS operations.
+ * @see https://github.com/ethereum/consensus-specs/blob/dev/specs/deneb/polynomial-commitments.md#bls12-381-helpers
+ */
+module Spec::BlsHelpers where
+
+import Common::Utils
+
+/**
+ * BLS field elements are 256-bits long.
+ * @see https://github.com/ethereum/consensus-specs/blob/dev/specs/deneb/polynomial-commitments.md#custom-types
+ */
+type BlsFieldSize = 256
+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
+
+NEGATIVE_ONE : BlsFieldElement
+NEGATIVE_ONE = -1
+
+/**
+ * Compute the modular inverse of x
+ *  i.e. return y such that x * y % BLS_MODULUS == 1
+ * Precondition: x != 0
+ * @see https://github.com/ethereum/consensus-specs/blob/dev/specs/deneb/polynomial-commitments.md#bls_modular_inverse
+ */
+bls_modular_inverse : BlsFieldElement -> BlsFieldElement
+bls_modular_inverse x = pow`{BlsFieldSize} x NEGATIVE_ONE BLS_MODULUS
+
+/**
+ * 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 = (x * (bls_modular_inverse y)) % BLS_MODULUS
+
+/*
+ * ===============
+ * Unit test suite
+ * ===============
+ */
+
+/**
+ * Unit tests for `bls_modular_inverse`.
+ * ```repl
+ * :prove test_bls_modular_inverse 1 1
+ * :prove test_bls_modular_inverse 2 0
+ * :prove test_bls_modular_inverse 3 0x36bd0357810d2d627770d2a2a108d2a556ed06a7aaac4eabaaaaaaabaaaaaaaa
+ * ```
+ * NOTE: we just chose the last value at "random"
+ */
+test_bls_modular_inverse : BlsFieldElement -> BlsFieldElement -> Bit
+property test_bls_modular_inverse x expectedY =
+    bls_modular_inverse x == expectedY
+
+/**
+ * Unit tests for `bls_modular_inverse`.
+ * ```repl
+ * :prove test_bls_div 1 2 0
+ * :prove test_bls_div 13 1 13
+ * :prove test_bls_div 57 13 0x15eaf636af000c906a5000958036c58484dfe5d59d8b7c9e89d89d8ad89d89dc
+ * ```
+ * NOTE: we just chose the last value at "random"
+ */
+test_bls_div : BlsFieldElement -> BlsFieldElement -> BlsFieldElement -> Bit
+property test_bls_div x y expected =
+    bls_div x y == expected