Add formally verified and prover generated BLS12_381 implementation

formal_verification/README.md

@@ -0,0 +1,14 @@
+# Formal verification
+
+This folder will hold code related to formal verification.
+
+## References
+
+- Fiat Crypto: Synthesizing Correct-by-Construction Code for Cryptographic Primitives
+  https://github.com/mit-plv/fiat-crypto
+
+- [Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala. Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises. To Appear in Proceedings of the IEEE Symposium on Security & Privacy 2019 (S&P'19). May 2019.](http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf). This paper describes multiple field arithmetic implementations, and an older version of the compilation pipeline (preserved [here](https://github.com/mit-plv/fiat-crypto/tree/sp2019latest)). It is somewhat space-constrained, so some details are best read about in theses below.
+- [Jade Philipoom. Correct-by-Construction Finite Field Arithmetic in Coq. MIT Master's Thesis. February 2018.](http://adam.chlipala.net/theses/jadep_meng.pdf) Chapters 3 and 4 contain a detailed walkthrough of the field arithmetic implementations (again, targeting the previous compilation pipeline).
+- [Andres Erbsen. Crafting Certified Elliptic CurveCryptography Implementations in Coq. MIT Master's Thesis. June 2017.](
+http://adam.chlipala.net/theses/andreser_meng.pdf) Section 3 contains a whirlwind introduction to synthesizing field arithmetic code using coq, without assuming Coq skills, but covering a tiny fraction of the overall library. Sections 5 and 6 contain the only write-up on the ellitpic-curve library in this repository.
+- The newest compilation pipeline does not have a separate document yet, but this README does go over it in some detail.

formal_verification/bls12_381_q_64.nim

@@ -0,0 +1,261 @@
+##  Autogenerated
+##  curve description: test
+##  requested operations: (all)
+##  m = 0x1a0111ea397fe69a4b1ba7b6434bacd764774b84f38512bf6730d2a0f6b0f6241eabfffeb153ffffb9feffffffffaaab (from "0x1a0111ea397fe69a4b1ba7b6434bacd764774b84f38512bf6730d2a0f6b0f6241eabfffeb153ffffb9feffffffffaaab")
+##  machine_wordsize = 64 (from "64")
+##
+##  NOTE: In addition to the bounds specified above each function, all
+##    functions synthesized for this Montgomery arithmetic require the
+##    input to be strictly less than the prime modulus (m), and also
+##    require the input to be in the unique saturated representation.
+##    All functions also ensure that these two properties are true of
+##    return values.
+
+{.compile: "bls12_381_q_64.c".}
+
+type
+  fiat_bls12_381_q_uint1*{.importc.} = cuchar
+  fiat_bls12_381_q_int1*{.importc.} = cchar
+  fiat_bls12_381_q_int128*{.importc.} = object
+  fiat_bls12_381_q_uint128*{.importc.} = object
+
+  BLSNumber = array[6, uint64]
+
+func fiat_bls12_381_q_mul*(r: var BLSNumber, a, b: BLSNumber) {.importc.}
+  ## Mongomery Mul
+func fiat_bls12_381_q_square*(r: var BLSNumber, a: BLSNumber) {.importc.}
+  ## Mongomery Square
+func fiat_bls12_381_q_add*(r: var BLSNumber, a, b: BLSNumber) {.importc.}
+  ## Modular Add
+func fiat_bls12_381_q_sub*(r: var BLSNumber, a, b: BLSNumber) {.importc.}
+  ## Modular Sub
+func fiat_bls12_381_q_opp*(r: var BLSNumber, a: BLSNumber) {.importc.}
+  ## Modular Negate
+func fiat_bls12_381_q_from_montgomery*(r: var BLSNumber, a: BLSNumber) {.importc.}
+  ## Montgomery to Canonical
+func fiat_bls12_381_q_to_bytes*(r: var array[48, byte], a: BLSNumber) {.importc.}
+  ## Montgomery to Little-Endian
+func fiat_bls12_381_q_from_bytes*(r: var BLSNumber, a: array[48, byte]) {.importc.}
+  ## Little-Endian to Montgomery
+
+# Hex conversion
+# -------------------------------------------------------------------------
+
+func readHexChar(c: char): uint8 {.inline.}=
+  ## Converts an hex char to an int
+  ## CT: leaks position of invalid input if any.
+  case c
+  of '0'..'9': result = uint8 ord(c) - ord('0')
+  of 'a'..'f': result = uint8 ord(c) - ord('a') + 10
+  of 'A'..'F': result = uint8 ord(c) - ord('A') + 10
+  else:
+    raise newException(ValueError, $c & "is not a hexadecimal character")
+
+func skipPrefixes(current_idx: var int, str: string, radix: static range[2..16]) {.inline.} =
+  ## Returns the index of the first meaningful char in `hexStr` by skipping
+  ## "0x" prefix
+  ## CT:
+  ##   - leaks if input length < 2
+  ##   - leaks if input start with 0x, 0o or 0b prefix
+
+  if str.len < 2:
+    return
+
+  assert current_idx == 0, "skipPrefixes only works for prefixes (position 0 and 1 of the string)"
+  if str[0] == '0':
+    case str[1]
+    of {'x', 'X'}:
+      assert radix == 16, "Parsing mismatch, 0x prefix is only valid for a hexadecimal number (base 16)"
+      current_idx = 2
+    of {'o', 'O'}:
+      assert radix == 8, "Parsing mismatch, 0o prefix is only valid for an octal number (base 8)"
+      current_idx = 2
+    of {'b', 'B'}:
+      assert radix == 2, "Parsing mismatch, 0b prefix is only valid for a binary number (base 2)"
+      current_idx = 2
+    else: discard
+
+func countNonBlanks(hexStr: string, startPos: int): int =
+  ## Count the number of non-blank characters
+  ## ' ' (space) and '_' (underscore) are considered blank
+  ##
+  ## CT:
+  ##   - Leaks white-spaces and non-white spaces position
+  const blanks = {' ', '_'}
+
+  for c in hexStr:
+    if c in blanks:
+      result += 1
+
+func fromHex(output: var openArray[byte], hexStr: string, order: static[Endianness]) =
+  ## Read a hex string and store it in a byte array `output`.
+  ## The string may be shorter than the byte array.
+  ##
+  ## The source string must be hex big-endian.
+  ## The destination array can be big or little endian
+  var
+    skip = 0
+    dstIdx: int
+    shift = 4
+  skipPrefixes(skip, hexStr, 16)
+
+  const blanks = {' ', '_'}
+  let nonBlanksCount = countNonBlanks(hexStr, skip)
+
+  let maxStrSize = output.len * 2
+  let size = hexStr.len - skip - nonBlanksCount
+
+  doAssert size <= maxStrSize, "size: " & $size & " (without blanks or prefix), maxSize: " & $maxStrSize
+
+  if size < maxStrSize:
+    # include extra byte if odd length
+    dstIdx = output.len - (size + 1) div 2
+    # start with shl of 4 if length is even
+    shift = 4 - size mod 2 * 4
+
+  for srcIdx in skip ..< hexStr.len:
+    if hexStr[srcIdx] in blanks:
+      continue
+
+    let nibble = hexStr[srcIdx].readHexChar shl shift
+    when order == bigEndian:
+      output[dstIdx] = output[dstIdx] or nibble
+    else:
+      output[output.high - dstIdx] = output[output.high - dstIdx] or nibble
+    shift = (shift + 4) and 4
+    dstIdx += shift shr 2
+
+# -------------------------------------------------------------------------
+
+when isMainModule:
+  import random, std/monotimes, times, strformat, ./timers
+
+  const Iters = 1_000_000
+  const InvIters = 1000
+
+  randomize(1234)
+
+  # warmup
+  proc warmup*() =
+    # Warmup - make sure cpu is on max perf
+    let start = cpuTime()
+    var foo = 123
+    for i in 0 ..< 300_000_000:
+      foo += i*i mod 456
+      foo = foo mod 789
+
+    # Compiler shouldn't optimize away the results as cpuTime rely on sideeffects
+    let stop = cpuTime()
+    echo &"\n\nWarmup: {stop - start:>4.4f} s, result {foo} (displayed to avoid compiler optimizing warmup away)\n"
+
+  warmup()
+
+  echo "\n⚠️ Measurements are approximate and use the CPU nominal clock: Turbo-Boost and overclocking will skew them."
+  echo "==========================================================================================================\n"
+
+  proc report(op, field: string, start, stop: MonoTime, startClk, stopClk: int64, iters: int) =
+    echo &"{op:<15} {field:<15} {inNanoseconds((stop-start) div iters):>9} ns {(stopClk - startClk) div iters:>9} cycles"
+
+  proc addBench() =
+    var aBytes, bBytes: array[48, byte]
+    # BN254 field modulus
+    aBytes.fromHex("0x30644e72e131a029b85045b68181585d97816a916871ca8d3c208c16d87cfd47", littleEndian)
+    # BLS12-381 prime - 2
+    bBytes.fromHex("0x1a0111ea397fe69a4b1ba7b6434bacd764774b84f38512bf6730d2a0f6b0f6241eabfffeb153ffffb9feffffffffaaa9", littleEndian)
+
+    var r, a, b: BLSNumber
+
+    a.fiat_bls12_381_q_from_bytes(aBytes)
+    b.fiat_bls12_381_q_from_bytes(bBytes)
+
+    let start = getMonotime()
+    let startClk = getTicks()
+    for _ in 0 ..< Iters:
+      r.fiat_bls12_381_q_add(a, b)
+    let stopClk = getTicks()
+    let stop = getMonotime()
+    report("Addition", "FiatCrypto[BLS12_381]", start, stop, startClk, stopClk, Iters)
+
+  addBench()
+
+  proc subBench() =
+    var aBytes, bBytes: array[48, byte]
+    # BN254 field modulus
+    aBytes.fromHex("0x30644e72e131a029b85045b68181585d97816a916871ca8d3c208c16d87cfd47", littleEndian)
+    # BLS12-381 prime - 2
+    bBytes.fromHex("0x1a0111ea397fe69a4b1ba7b6434bacd764774b84f38512bf6730d2a0f6b0f6241eabfffeb153ffffb9feffffffffaaa9", littleEndian)
+
+    var r, a, b: BLSNumber
+
+    a.fiat_bls12_381_q_from_bytes(aBytes)
+    b.fiat_bls12_381_q_from_bytes(bBytes)
+
+    let start = getMonotime()
+    let startClk = getTicks()
+    for _ in 0 ..< Iters:
+      r.fiat_bls12_381_q_add(a, b)
+    let stopClk = getTicks()
+    let stop = getMonotime()
+    report("Substraction", "FiatCrypto[BLS12_381]", start, stop, startClk, stopClk, Iters)
+
+  subBench()
+
+  proc negBench() =
+    var aBytes: array[48, byte]
+    # BN254 field modulus
+    aBytes.fromHex("0x30644e72e131a029b85045b68181585d97816a916871ca8d3c208c16d87cfd47", littleEndian)
+
+    var r, a: BLSNumber
+    a.fiat_bls12_381_q_from_bytes(aBytes)
+
+    let start = getMonotime()
+    let startClk = getTicks()
+    for _ in 0 ..< Iters:
+      r.fiat_bls12_381_q_opp(a)
+    let stopClk = getTicks()
+    let stop = getMonotime()
+    report("Negation", "FiatCrypto[BLS12_381]", start, stop, startClk, stopClk, Iters)
+
+  negBench()
+
+  proc mulBench() =
+    var aBytes, bBytes: array[48, byte]
+    # BN254 field modulus
+    aBytes.fromHex("0x30644e72e131a029b85045b68181585d97816a916871ca8d3c208c16d87cfd47", littleEndian)
+    # BLS12-381 prime - 2
+    bBytes.fromHex("0x1a0111ea397fe69a4b1ba7b6434bacd764774b84f38512bf6730d2a0f6b0f6241eabfffeb153ffffb9feffffffffaaa9", littleEndian)
+
+    var r, a, b: BLSNumber
+
+    a.fiat_bls12_381_q_from_bytes(aBytes)
+    b.fiat_bls12_381_q_from_bytes(bBytes)
+
+    let start = getMonotime()
+    let startClk = getTicks()
+    for _ in 0 ..< Iters:
+      r.fiat_bls12_381_q_mul(a, b)
+    let stopClk = getTicks()
+    let stop = getMonotime()
+    report("Multiplication", "FiatCrypto[BLS12_381]", start, stop, startClk, stopClk, Iters)
+
+  mulBench()
+
+  proc sqrBench() =
+    var aBytes: array[48, byte]
+    # BN254 field modulus
+    aBytes.fromHex("0x30644e72e131a029b85045b68181585d97816a916871ca8d3c208c16d87cfd47", littleEndian)
+
+    var r, a: BLSNumber
+    a.fiat_bls12_381_q_from_bytes(aBytes)
+
+    let start = getMonotime()
+    let startClk = getTicks()
+    for _ in 0 ..< Iters:
+      r.fiat_bls12_381_q_square(a)
+    let stopClk = getTicks()
+    let stop = getMonotime()
+    report("Squaring", "FiatCrypto[BLS12_381]", start, stop, startClk, stopClk, Iters)
+
+  sqrBench()
+
+  # TODO: No inversion bench