Bedrock2 End2End field and co-Z operations for secp256k1

[atrieu]

This PR contains verified Bedrock2 code for

• secp256k1 field operations (using Montgomery representation? Not sure about the terminology, is there any literature about saturated/unsaturated Solinas representation ? A quick research hasn't found anything).
  This includes field inversion using the addition chain provided by addchain. I suspect it may be easier to automate using Rupicola, but I spent a couple hours trying to prove zdau thay way and couldn't make sense of the errors I got, so I didn't even try using it for inversion. Though I guess that could make a good candidate for comparison if someone wants to try doing it.
• secp256k1 co-Z point operations.

I also added unverified code for the Joye ladder, I can remove it from this PR if you prefer only proved code.
This PR is maybe of interest for #1444 ?

Current code output available here https://gist.github.com/atrieu/b32fcc79c87efc72cefe8c354ce6e587

[atrieu]

FWIW I finished proving the scalar multiplication Joye ladder implementation.
I seem to be getting around 200us per scalar multiplication with the below code using gcc -O3.
For comparison, I think the equivalent in bitcoin-core/secp256k1 is secp256k1_ecmult_const which runs at 40us per multiplication on my laptop.

#include "stdio.h"
#include "stdint.h"
#include <inttypes.h>
#include <sys/time.h>
#include <sys/random.h>
#include "secp256k1_64.c"

static int64_t gettime_i64(void) {
  struct timeval tv;
  gettimeofday(&tv, NULL);
  return (int64_t)tv.tv_usec + (int64_t)tv.tv_sec * 1000000LL;
}

int main(void) {
  // https://neuromancer.sk/std/secg/secp256k1
  // G = (0x79be667ef9dcbbac55a06295ce870b07029bfcdb2dce28d959f2815b16f81798, 0x483ada7726a3c4655da4fbfc0e1108a8fd17b448a68554199c47d08ffb10d4b8)
  // G x-coordinate
  uint8_t g_x[32] = {
    0x98, 0x17, 0xf8, 0x16,
    0x5b, 0x81, 0xf2, 0x59,
    0xd9, 0x28, 0xce, 0x2d,
    0xdb, 0xfc, 0x9b, 0x02,
    0x07, 0x0b, 0x87, 0xce,
    0x95, 0x62, 0xa0, 0x55,
    0xac, 0xbb, 0xdc, 0xf9,
    0x7e, 0x66, 0xbe, 0x79
  };
  // G y-coordinate
  uint8_t g_y[32] = {
    0xb8, 0xd4, 0x10, 0xfb,
    0x8f, 0xd0, 0x47, 0x9c,
    0x19, 0x54, 0x85, 0xa6,
    0x48, 0xb4, 0x17, 0xfd,
    0xa8, 0x08, 0x11, 0x0e,
    0xfc, 0xfb, 0xa4, 0x5d,
    0x65, 0xc4, 0xa3, 0x26,
    0x77, 0xda, 0x3a, 0x48
  };

  uint8_t n[32] = {0};

  uint8_t tempx[32] = {0};
  uint8_t tempy[32] = {0};
  uint8_t res_x[32] = {0};
  uint8_t res_y[32] = {0};
  int64_t sum = 0;

  secp256k1_to_mont((uintptr_t)&tempy, (uintptr_t)&g_y);
  secp256k1_square((uintptr_t)&res_y, (uintptr_t)&tempy);
  secp256k1_from_mont((uintptr_t)&res_y, (uintptr_t)&res_y); // y^2 = x^3 + 7

  secp256k1_to_mont((uintptr_t)&tempx, (uintptr_t)&g_x);
  secp256k1_square((uintptr_t)&res_x, (uintptr_t)&tempx);
  secp256k1_mul((uintptr_t)&res_x, (uintptr_t)&res_x, (uintptr_t)&tempx);
  secp256k1_from_mont((uintptr_t)&res_x, (uintptr_t)&res_x); // x^3

  printf("Should be 7: 0x");
  for (uint8_t i = 0; i < 32; i++) {
    printf("%02x ", res_y[31 - i] - res_x[31 - i]);
  };
  printf("\n");

  for (uint64_t i = 0; i < 8192; i++) {
    int64_t begin, total;
    getrandom(n, sizeof n, 0);
    begin = gettime_i64();
    secp256k1_to_mont((uintptr_t)&tempx, (uintptr_t)&g_x);
    secp256k1_to_mont((uintptr_t)&tempy, (uintptr_t)&g_y);
    secp256k1_laddermul((uintptr_t)&res_x, (uintptr_t)&res_y, (uintptr_t)&n, (uintptr_t)&tempx, (uintptr_t)&tempy);
    secp256k1_from_mont((uintptr_t)&res_x, (uintptr_t)&res_x);
    secp256k1_from_mont((uintptr_t)&res_y, (uintptr_t)&res_y);
    total = gettime_i64() - begin;
    sum = sum + total;
  };

  printf("average: %" PRId64" us\n", (sum>>13));
  return 0;
}

[andres-erbsen]

This is a cool contribution -- please don't take my tardiness in tending to it as a negative judgement. I flipped through the code, found it reasonable, and prepared a catch-up patch here.

I don't know any writeups about the solinas-style representation used for secpk256k1. I believe the tricks in question were novel in libsecp256k1 and were added to fiat-crypot as a part of #1954. generated code. benchmarks.

[atrieu]

No worries and thanks for looking through the code!
Do you need any additional action on my side?

[andres-erbsen]

Merged as ee1e322. Thank you!