Bls operations rebased

patches/blst_header.patch

@@ -0,0 +1,41 @@
+diff --git a/bindings/blst.h b/bindings/blst.h
+index 3a333b1..cbd3642 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);
+ bool blst_p1_is_inf(const blst_p1 *a);
+ const blst_p1 *blst_p1_generator();
+
+-bool blst_p1_affine_on_curve(const blst_p1_affine *p);
+-bool blst_p1_affine_in_g1(const blst_p1_affine *p);
++limb_t blst_p1_affine_on_curve(const blst_p1_affine *p);
++limb_t blst_p1_affine_in_g1(const blst_p1_affine *p);
+ bool blst_p1_affine_is_equal(const blst_p1_affine *a, const blst_p1_affine *b);
+-bool blst_p1_affine_is_inf(const blst_p1_affine *a);
++limb_t blst_p1_affine_is_inf(const blst_p1_affine *a);
+ const blst_p1_affine *blst_p1_affine_generator();
+
+ typedef struct { blst_fp2 x, y, z; } blst_p2;
+@@ -194,10 +194,10 @@ bool blst_p2_is_equal(const blst_p2 *a, const blst_p2 *b);
+ bool blst_p2_is_inf(const blst_p2 *a);
+ const blst_p2 *blst_p2_generator();
+
+-bool blst_p2_affine_on_curve(const blst_p2_affine *p);
+-bool blst_p2_affine_in_g2(const blst_p2_affine *p);
++limb_t blst_p2_affine_on_curve(const blst_p2_affine *p);
++limb_t blst_p2_affine_in_g2(const blst_p2_affine *p);
+ bool blst_p2_affine_is_equal(const blst_p2_affine *a, const blst_p2_affine *b);
+-bool blst_p2_affine_is_inf(const blst_p2_affine *a);
++limb_t blst_p2_affine_is_inf(const blst_p2_affine *a);
+ 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,
+                                      size_t aug_len DEFNULL);
+ BLST_ERROR blst_core_verify_pk_in_g2(const blst_p2_affine *pk,
+                                      const blst_p1_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,

proof/aggregate_in_g2.saw

@@ -5,7 +5,7 @@
 
 // NOTE: we only consider inputs that either have the infinity-bit set or compressed-bit set
 
-// aggregate_in_g2_error_precond describes the circumstances under which aggregate_in_g2 returns an error (assuming either the compressed bit is set of the infinity bit is set)
+// aggregate_in_g2_error_precond describes the circumstances under which aggregate_in_g2 returns an error (assuming either the compressed bit is set or the infinity bit is set)
 let {{
   aggregate_in_g2_error_precond : [96][8] -> Bool
   aggregate_in_g2_error_precond zwire =
@@ -95,7 +95,8 @@ let overrides = foldr concat [vec_overrides,curve_operations_e2_ovs] [POINTonE2_
 
 // Assumptions
 
-uncompress_not_point_O <- admit_cryptol {{ \x -> (is_point_O E' (uncompress_E2_OK x)) == if uncompress_E2_x_fp x != Fp_2.field_zero then False else apply is_point_O E' (uncompress_E2_OK x) }};
+// uncompressing a valid point that does not have the infinity bit set does not return point_O:
+uncompress_not_point_O <- admit_cryptol {{ \x -> (is_point_O E' (uncompress_E2_OK x)) == if (uncompress_E2_imp x != nothing) then False else apply is_point_O E' (uncompress_E2_OK x) }};
 
 uncompress_on_curve <- admit_cryptol {{ \x -> (is_point_affine E' (uncompress_E2_OK x)) == True }};
 

proof/api-extra-for-release-2.saw

@@ -1,6 +1,6 @@
 /*
-Copyright (c) 2020 Galois, Inc.
-SPDX-License-Identifier: Apache-2.0 OR MIT
+ * Copyright (c) 2020 Galois, Inc.
+ * SPDX-License-Identifier: Apache-2.0 OR MIT
 */
 
 blst_p1_affine_in_g1_ov <- verify_unint "blst_p1_affine_in_g1"

proof/bls_operations.c

@@ -0,0 +1,138 @@
+#include "blst.h"
+#include <stdio.h> // for NULL 
+
+// TODO: Move
+
+// 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)
+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_";
+
+// KeyGen maps directly to blst_keygen
+
+// SkToPk
+void demo_SkToPk_A(unsigned char out[96], const blst_scalar *SK) {
+  blst_p2 pk;
+  blst_sk_to_pk_in_g2(&pk, SK);
+  blst_p2_compress(out, &pk);
+  }
+
+void demo_SkToPk_B(unsigned char out[48], const blst_scalar *SK) {
+  blst_p1 pk;
+  blst_sk_to_pk_in_g1(&pk, SK);
+  blst_p1_compress(out, &pk);
+};
+
+// KeyValidate
+
+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;
+  if (! blst_p2_affine_in_g2(&pk)) return 0;
+  return 1;
+};
+
+limb_t demo_KeyValidate_B(const unsigned char in[48]) {
+  blst_p1_affine pk;
+  BLST_ERROR r;
+  r = blst_p1_uncompress(&pk, in);
+  if (r != 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;
+  return 1;
+};
+
+
+// BasicSign
+
+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);
+};
+
+void demo_BasicSign_B(byte out[96], const blst_scalar *SK,
+                     const byte *message, size_t message_len) {
+  blst_p2 Q1, Q2;
+  blst_hash_to_g2(&Q1, message, message_len, demo_DST_B, 43, NULL, 0); // no "aug" string
+  blst_sign_pk_in_g1(&Q2, &Q1, SK);
+  blst_p2_compress(out, &Q2);
+};
+
+// BasicVerify
+
+limb_t demo_BasicVerify_A(const byte sig[48], const byte pk[96], const byte *message, size_t message_len) {
+  blst_p1_affine R;
+  blst_p1 Q;
+  blst_p2_affine PK;
+  // uncompress and check the sig
+  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;
+
+  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) {
+  blst_p2_affine R;
+  blst_p2 Q;
+  blst_p1_affine PK;
+  // uncompress and check the sig
+  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;
+
+  // TODO: Maybe remove the above checks if the override handles error cases.
+  // Can't remove pubkey checks?  (Same goes for A variant)
+
+  // 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)
+    return 0;
+  return 1;
+};