temporarily replace DST_len by concrete value

I don't understand the error that arises otherwise.
GaloisInc · Aug 6, 2021 · 2a37a46 · 2a37a46
1 parent fdd517f
commit 2a37a46
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 6 deletions.
diff --git a/spec/BLSGeneric.cry b/spec/BLSGeneric.cry
@@ -43,7 +43,8 @@ parameter
     // H, a hash function, is always HKDF, so not listed here
 
     // hash_to_point
-    type DST_len: #
+    // TODO: why is this not working?
+    // type DST_len: #
 
     hash_to_point: {msg_len} (Hashable msg_len) =>
                [msg_len][8] -> EC::AffinePoint t_F
@@ -64,7 +65,8 @@ parameter
     pubkey_subgroup_check: EC::AffinePoint t_F' -> Bool
     signature_subgroup_check: EC::AffinePoint t_F -> Bool
 
-type constraint Hashable msg_len = (msg_len <= 255, 61 >= width (69 + msg_len + DST_len))
+//type constraint Hashable msg_len = (msg_len <= 255, 61 >= width (69 + msg_len + DST_len))
+type constraint Hashable msg_len = (msg_len <= 255, 61 >= width (69 + msg_len + 43))
 
 // TODO: Better name.  Maybe param should be _pubkey_subgroup_check and this
 // should be pubkey_subgroup_check

diff --git a/spec/BLSMinimalPublicKeySize.cry b/spec/BLSMinimalPublicKeySize.cry
@@ -26,9 +26,9 @@ main_curve = E'
 other_curve = E
 
 // hash_to_point  BLS12381G2_XMD:SHA-256_SSWU_RO_
-type DST_len = 43
+// type DST_len = 43
 
-DST: [DST_len][8]
+DST: [43][8]
 DST = "BLS_SIG_BLS12381G2_XMD:SHA-256_SSWU_RO_NUL_"
 
 hash_to_point hx = hash_to_curve (DST, hx)

diff --git a/spec/BLSMinimalSignatureSize.cry b/spec/BLSMinimalSignatureSize.cry
@@ -26,11 +26,11 @@ main_curve = E
 other_curve = E'
 
 // hash_to_point  BLS12381G1_XMD:SHA-256_SSWU_RO_
-type DST_len = 43
+// type DST_len = 43
 
 // TODO: Make this match whatever DST string we use (what about null
 // terminator?)
-DST: [DST_len][8]
+DST: [43][8]
 DST = "BLS_SIG_BLS12381G1_XMD:SHA-256_SSWU_RO_NUL_"
 
 hash_to_point hx = hash_to_curve (hx, DST)