Add remaining BLS wrapper proofs (#70)

This change adds the remaining BLS wrapper proofs and also cleans up the existing proofs. Specifically, it adds proofs for

* demo_BasicVerify_B
* demo_BasicAggregateVerify_A
* demo_BasicAggregateVerify_B

and moves the existing proofs out of bls_operations.saw and min_key.saw into individual SAW files in proof/bls_operations. It also:

* Cleans up the existing BLS wrapper proofs
* Removes some assumptions
* Proves some assumptions
* Adds documentation justifying all remaining assumptions introduced for the BLS wrapper proofs

patches/blst/aggregate.patch

@@ -0,0 +1,13 @@
+diff --git a/src/aggregate.c b/src/aggregate.c
+index 50f6557..b8b7bd4 100644
+--- a/src/aggregate.c
++++ b/src/aggregate.c
+@@ -37,7 +37,7 @@
+  */
+
+ #ifndef N_MAX
+-# define N_MAX 8
++# define N_MAX 2
+ #endif
+
+ typedef union { POINTonE1 e1; POINTonE2 e2; } AggregatedSignature;

patches/blst/blst_header.patch

@@ -1,5 +1,5 @@
 diff --git a/bindings/blst.h b/bindings/blst.h
-index 3a333b1..cbd3642 100644
+index 3a333b1..72b6c1c 100644
 --- a/bindings/blst.h
 +++ b/bindings/blst.h
 @@ -168,10 +168,10 @@ bool blst_p1_is_equal(const blst_p1 *a, const blst_p1 *b);
@@ -30,7 +30,53 @@ index 3a333b1..cbd3642 100644
  const blst_p2_affine *blst_p2_affine_generator();
 
  /*
-@@ -351,7 +351,7 @@ BLST_ERROR blst_core_verify_pk_in_g1(const blst_p1_affine *pk,
+@@ -279,11 +279,25 @@ void blst_miller_loop_lines(blst_fp12 *ret, const blst_fp6 Qlines[68],
+ #ifdef __BLST_CGO__
+ typedef limb_t blst_pairing;
+ #else
+-typedef struct {} blst_pairing;
++#ifndef N_MAX
++# define N_MAX 2
++#endif
++
++typedef union { blst_p1 e1; blst_p2 e2; } AggregatedSignature;
++typedef struct blst_pairing_st {
++    unsigned int ctrl;
++    unsigned int nelems;
++    const void *DST;
++    size_t DST_len;
++    blst_fp12 GT;
++    AggregatedSignature AggrSign;
++    blst_p2_affine Q[N_MAX];
++    blst_p1_affine P[N_MAX];
++} blst_pairing;
+ #endif
+
+ size_t blst_pairing_sizeof();
+-void blst_pairing_init(blst_pairing *new_ctx, bool hash_or_encode,
++void blst_pairing_init(blst_pairing *new_ctx, int hash_or_encode,
+                        const byte *DST DEFNULL, size_t DST_len DEFNULL);
+ const byte *blst_pairing_get_dst(const blst_pairing *ctx);
+ void blst_pairing_commit(blst_pairing *ctx);
+@@ -318,7 +332,7 @@ BLST_ERROR blst_pairing_mul_n_aggregate_pk_in_g1(blst_pairing *ctx,
+                                                  const byte *aug DEFNULL,
+                                                  size_t aug_len DEFNULL);
+ BLST_ERROR blst_pairing_merge(blst_pairing *ctx, const blst_pairing *ctx1);
+-bool blst_pairing_finalverify(const blst_pairing *ctx,
++limb_t blst_pairing_finalverify(const blst_pairing *ctx,
+                               const blst_fp12 *gtsig DEFNULL);
+
+
+@@ -343,7 +357,7 @@ void blst_aggregated_in_g2(blst_fp12 *out, const blst_p2_affine *signature);
+  */
+ BLST_ERROR blst_core_verify_pk_in_g1(const blst_p1_affine *pk,
+                                      const blst_p2_affine *signature,
+-                                     bool hash_or_encode,
++                                     int hash_or_encode,
+                                      const byte *msg, size_t msg_len,
+                                      const byte *DST DEFNULL,
+                                      size_t DST_len DEFNULL,
+@@ -351,7 +365,7 @@ BLST_ERROR blst_core_verify_pk_in_g1(const blst_p1_affine *pk,
                                       size_t aug_len DEFNULL);
  BLST_ERROR blst_core_verify_pk_in_g2(const blst_p2_affine *pk,
                                       const blst_p1_affine *signature,

proof/aggregate.saw

@@ -30,7 +30,7 @@ let AGGR_GT_SET = {{ 32:[32] }};
 let AGGR_HASH_OR_ENCODE = {{ 64:[32] }};
 let MIN_SIG_OR_PK = {{ AGGR_MIN_SIG || AGGR_MIN_PK }};
 
-let N_MAX = 8; // NOTE: must match N_MAX defined in C code
+let N_MAX = 2; // NOTE: must match N_MAX defined in C code
 
 let {{ is_in_G1 (p : ([6][64], [6][64])) = (undefined:[64]) }}; // NOTE: the goal is to leave it uninterpreted
 let POINTonE1_in_G1_spec = do {
@@ -296,7 +296,7 @@ let overrides = foldr concat [hash_to_field_ovs, ec_ops_overrides, assembly_over
 
 pairing_init_ov <- verify "blst_pairing_init" [] (blst_pairing_init_spec 8);
 
-let aggregate_ns = [0,1,7]; // aggregate_... calls miller_loop_n for nelems+1
+let aggregate_ns = [0,1]; // aggregate_... calls miller_loop_n for nelems+1
 
 let make_aggregate_pk_in_g1_ov null_sig nelems = verify_unint "blst_pairing_aggregate_pk_in_g1" overrides ["is_in_G2"] (blst_pairing_aggregate_pk_in_spec DST_len msg_len aug_len nelems null_sig false); // null_sig should be 0 or 1
 aggregate_pk_in_g1_null_sig_ovs <- for aggregate_ns (make_aggregate_pk_in_g1_ov 1);

proof/aggregate_in_g1.saw

@@ -98,11 +98,11 @@ let overrides = foldr concat [vec_overrides,curve_operations_e1_ovs] [POINTonE1_
 uncompress_not_point_O <- admit_cryptol {{ \x -> (is_point_O E (uncompress_E1_OK x)) == if uncompress_E1_x_fp x != Fp.field_zero then False else apply is_point_O E (uncompress_E1_OK x) }};
 
 // decompression yields a point on the curve
-uncompress_on_curve <- admit_cryptol {{ \x -> (is_point_affine E (uncompress_E1_OK x)) == True }};
+uncompress_E1_on_curve <- admit_cryptol {{ \x -> (is_point_affine E (uncompress_E1_OK x)) == True }};
 
 // Proofs
 
-let simpset = addsimps (concat_all [e1_curve_op_thms, POINTonE1_thms, [normalize_uncompress_OK_thm, uncompress_not_point_O, uncompress_on_curve]]) fp_simpset; // uncompress_not_point_O and uncompress_on_curve are there to satisfy the preconditions of the subgroup check
+let simpset = addsimps (concat_all [e1_curve_op_thms, POINTonE1_thms, [normalize_uncompress_OK_thm, uncompress_not_point_O, uncompress_E1_on_curve]]) fp_simpset; // uncompress_not_point_O and uncompress_E1_on_curve are there to satisfy the preconditions of the subgroup check
 
 let fp_unit_rep = run ( eval_term {{ (fp_rep Fp.field_unit):[6][64] }} ); // NOTE: this results in type `([6][64])` (a one-tuple?) instead of `[6][64]`, but not in newer versions of SAW.
 

proof/bls_operations.c

@@ -1,14 +1,13 @@
 #include "blst.h"
 #include <stdio.h> // for NULL 
-
-// TODO: Move
+#include <string.h> // for memcmp
 
 // Two variants:
 // _A: min signature size
 // _B: min pk size
 
-// Explicitly note that demo_DST_A is 43 bytes to avoid the null terminator
-// (needed for SAW to treat the allocation as 32 bytes)
+// demo_DST_A and demo_DST_B are 43 bytes to avoid the null terminator.  This
+// is needed for SAW to treat the allocations as 43 bytes.
 byte demo_DST_A[43] = "BLS_SIG_BLS12381G1_XMD:SHA-256_SSWU_RO_NUL_";
 byte demo_DST_B[43] = "BLS_SIG_BLS12381G2_XMD:SHA-256_SSWU_RO_NUL_";
 
@@ -33,12 +32,6 @@ limb_t demo_KeyValidate_A(const unsigned char in[96]) {
   blst_p2_affine pk;
   BLST_ERROR r;
   r = blst_p2_uncompress(&pk, in);
-  /*
-  return r == BLST_SUCCESS &&
-         blst_p2_affine_on_curve(&pk) &&
-         !blst_p2_affine_is_inf(&pk) &&
-         blst_p2_affine_in_g2(&pk);
-         */
   if (r != BLST_SUCCESS) return 0;
   if (! blst_p2_affine_on_curve(&pk)) return 0;
   if (blst_p2_affine_is_inf(&pk)) return 0;
@@ -62,15 +55,8 @@ limb_t demo_KeyValidate_B(const unsigned char in[48]) {
 
 void demo_BasicSign_A(byte out[48], const blst_scalar *SK,
                      const byte *message, size_t message_len) {
-  // TODO: Figure out how to use globals in SAW?
-  //const byte local_DST_A[] = "BLS_SIG_BLS12381G1_XMD:SHA-256_SSWU_RO_AUG_";
   blst_p1 Q1, Q2;
-  // TODO: Double check, but I think aug is supposed to be a public key?  That
-  // will determine the size it should be.
-  // TODO: Is DST_len supposted to include the null terminator?  It's 44 with
-  // the null terminator, and 43 without.
   blst_hash_to_g1(&Q1, message, message_len, demo_DST_A, 43, NULL, 0); // no "aug" string
-  // blst_p1_mult(&Q, &Q, SK, 256); // or 255?
   blst_sign_pk_in_g2(&Q2, &Q1, SK);
   blst_p1_compress(out, &Q2);
 };
@@ -97,21 +83,15 @@ limb_t demo_BasicVerify_A(const byte sig[48], const byte pk[96], const byte *mes
 
   if (!demo_KeyValidate_A(pk)) return 0;
 
-  // TODO: Use KeyValidate below instead to better match the spec?
   // uncompress and check the pub key
   if (blst_p2_uncompress(&PK, pk) != BLST_SUCCESS) return 0;
-  /*
-  if (! blst_p2_affine_on_curve(&PK)) return 0;
-  if (blst_p2_affine_is_inf(&PK)) return 0;
-  if (! blst_p2_affine_in_g2(&PK)) return 0;
-  */
 
   if (blst_core_verify_pk_in_g2(&PK, &R, 1, message, message_len, demo_DST_A, 43, NULL, 0) != BLST_SUCCESS)
     return 0;
   return 1;
 };
 
-bool demo_BasicVerify_B(const byte sig[96], const byte pk[48], const byte *message, size_t message_len) {
+limb_t demo_BasicVerify_B(const byte sig[96], const byte pk[48], const byte *message, size_t message_len) {
   blst_p2_affine R;
   blst_p2 Q;
   blst_p1_affine PK;
@@ -121,18 +101,101 @@ bool demo_BasicVerify_B(const byte sig[96], const byte pk[48], const byte *messa
   if (blst_p2_affine_is_inf(&R)) return 0;
   if (! blst_p2_affine_in_g2(&R)) return 0;
 
-  // TODO: Maybe remove the above checks if the override handles error cases.
-  // Can't remove pubkey checks?  (Same goes for A variant)
+  if (!demo_KeyValidate_B(pk)) return 0;
 
   // uncompress and check the pub key
   if (blst_p1_uncompress(&PK, pk) != BLST_SUCCESS) return 0;
-  if (! blst_p1_affine_on_curve(&PK)) return 0;
-  if (blst_p1_affine_is_inf(&PK)) return 0;
-  if (! blst_p1_affine_in_g1(&PK)) return 0;
-
 
-  // TODO: fix DST string
-  if (blst_core_verify_pk_in_g1(&PK, &R, 1, message, message_len, demo_DST_A, 43, NULL, 0) != BLST_SUCCESS)
+  if (blst_core_verify_pk_in_g1(&PK, &R, 1, message, message_len, demo_DST_B, 43, NULL, 0) != BLST_SUCCESS)
     return 0;
   return 1;
 };
+
+// Assert no two messages are equal
+limb_t all_distinct(size_t n, size_t message_len, const byte messages[n][message_len]) {
+  for (size_t i; i < n; ++i) {
+    for (size_t j = i+1; j < n; ++j) {
+      if (memcmp(messages[i], messages[j], message_len)) return 0;
+    }
+  }
+  return 1;
+}
+
+limb_t demo_BasicAggregateVerify_A(size_t n,
+                                   size_t message_len,
+                                   const byte pks[n][96],
+                                   const byte messages[n][message_len],
+                                   const byte sig[48]) {
+  if (!all_distinct(n, message_len, messages)) return 0;
+
+  // uncompress and check the sig
+  blst_p1_affine R;
+  if (blst_p1_uncompress(&R, sig) != BLST_SUCCESS) return 0;
+  if (! blst_p1_affine_on_curve(&R)) return 0;
+  if (blst_p1_affine_is_inf(&R)) return 0;
+  if (! blst_p1_affine_in_g1(&R)) return 0;
+
+  // Create aggregate verify context
+  blst_pairing ctx;
+  blst_pairing_init(&ctx, 1, demo_DST_A, 43);
+
+  for (size_t i = 0; i < n; ++i) {
+    const byte* pk = pks[i];
+    // Check and Uncompress PK
+    if (!demo_KeyValidate_A(pk)) return 0;
+
+    blst_p2_affine PK;
+    if (blst_p2_uncompress(&PK, pk) != BLST_SUCCESS) return 0;
+
+    // Aggregate
+    if (blst_pairing_aggregate_pk_in_g2(&ctx,
+                                        &PK,
+                                        i ? NULL : &R,
+                                        messages[i],
+                                        message_len,
+                                        NULL,
+                                        0) != BLST_SUCCESS) return 0;
+  }
+  blst_pairing_commit(&ctx);
+  if (!blst_pairing_finalverify(&ctx, NULL)) return 0;
+  return 1;
+}
+
+limb_t demo_BasicAggregateVerify_B(size_t n,
+                                   size_t message_len,
+                                   const byte pks[n][48],
+                                   const byte messages[n][message_len],
+                                   const byte sig[96]) {
+  if (!all_distinct(n, message_len, messages)) return 0;
+
+  // uncompress and check the sig
+  blst_p2_affine R;
+  if (blst_p2_uncompress(&R, sig) != BLST_SUCCESS) return 0;
+  if (! blst_p2_affine_on_curve(&R)) return 0;
+  if (blst_p2_affine_is_inf(&R)) return 0;
+  if (! blst_p2_affine_in_g2(&R)) return 0;
+
+  // Create aggregate verify context
+  blst_pairing ctx;
+  blst_pairing_init(&ctx, 1, demo_DST_B, 43);
+
+  for (size_t i = 0; i < n; ++i) {
+    const byte* pk = pks[i];
+    // Check and Uncompress PK
+    if (!demo_KeyValidate_B(pk)) return 0;
+    blst_p1_affine PK;
+    if (blst_p1_uncompress(&PK, pk) != BLST_SUCCESS) return 0;
+
+    // Aggregate
+    if (blst_pairing_aggregate_pk_in_g1(&ctx,
+                                        &PK,
+                                        i ? NULL : &R,
+                                        messages[i],
+                                        message_len,
+                                        NULL,
+                                        0) != BLST_SUCCESS) return 0;
+  }
+  blst_pairing_commit(&ctx);
+  if (!blst_pairing_finalverify(&ctx, NULL)) return 0;
+  return 1;
+}