Use lifted struct type instead of CN datatype

GaloisInc · Feb 12, 2025 · 53cb312 · 53cb312
1 parent 9217268
commit 53cb312
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 17 deletions.
diff --git a/components/platform_crypto/shave_trusted_boot/firmware.c b/components/platform_crypto/shave_trusted_boot/firmware.c
@@ -43,7 +43,7 @@ static bool xmss_verify_signature(XmssPublicKey *exported_public_key, uint8_t *m
     take epko = Owned<XmssPublicKey>(exported_public_key);
     take mo = Array_u8(msg, msg_size);
     take sbo = XmssSignatureBlobP(signature_blob);
-    data_size(sbi) == data_size(sbo);
+    sbi.data_size == sbo.data_size;
 $*/
 {
     bool success = true;

diff --git a/components/platform_crypto/shave_trusted_boot/xmss-library/include/structures.h b/components/platform_crypto/shave_trusted_boot/xmss-library/include/structures.h
@@ -212,24 +212,12 @@ typedef struct XmssSignatureBlob {
 } XmssSignatureBlob;
 
 /*$
-datatype XmssSignatureBlobT {
-  XmssSigBlobF {size_t data_size, map<u64,u8> data}
-}
-predicate (datatype XmssSignatureBlobT) XmssSignatureBlobP(pointer p)
+predicate (struct XmssSignatureBlob) XmssSignatureBlobP(pointer p)
 {
   take sz = Owned<size_t>(member_shift<XmssSignatureBlob>(p, data_size));
   assert(sz >= 0u64);
   take cont = Array_u8(member_shift<XmssSignatureBlob>(p, data), sz);
-  return XmssSigBlobF { data_size: sz, data: cont };
-}
-// No dot notation for datatype member access
-function (size_t) data_size(datatype XmssSignatureBlobT a)
-{
-  match a {
-    XmssSigBlobF {data_size: p, data: q} => {
-      p
-    }
-  }
+  return struct XmssSignatureBlob {data_size : sz, data : cont};
 }
 $*/
 
@@ -247,7 +235,7 @@ static inline XmssSignature *xmss_get_signature_struct(const XmssSignatureBlob *
   ensures
     take so = Owned<XmssSignature>(return);
     take sz = Owned<size_t>(member_shift<XmssSignatureBlob>(signature, data_size));
-    data_size(si) == sz;
+    si.data_size == sz;
 $*/
 {
     if (signature == NULL) {
@@ -263,7 +251,7 @@ lemma Unxmss_get_signature_struct(pointer blob, pointer sig)
     take sz = Owned<size_t>(member_shift<XmssSignatureBlob>(blob, data_size));
   ensures
     take si = XmssSignatureBlobP(blob);
-    sz == data_size(si);
+    sz == si.data_size;
 
 $*/