cbmc: add fd_keyguard_ambiguity_proof

verification/proofs/keyguard/ambiguity/Makefile

@@ -0,0 +1,16 @@
+HARNESS_ENTRY = harness
+HARNESS_FILE = fd_keyguard_ambiguity_proof
+
+PROOF_UID = fd_keyguard_ambiguity
+
+DEFINES +=
+INCLUDES += -I$(SRCDIR)
+
+REMOVE_FUNCTION_BODY +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES = $(SRCDIR)/disco/keyguard/fd_keyguard_match.c
+
+UNWINDSET += memcmp.0:1024
+
+include ../../Makefile.common

verification/proofs/keyguard/ambiguity/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "fd_keyguard_ambiguity",
+  "proof-root": "verification/proofs"
+}

verification/proofs/keyguard/ambiguity/fd_keyguard_ambiguity_proof.c

@@ -0,0 +1,17 @@
+#include <disco/keyguard/fd_keyguard.h>
+#include <stdlib.h>
+#include <assert.h>
+
+/* fd_keyguard_ambiguity_proof proves that no message up to 2048 bytes
+   has an ambiguous type detection result. */
+
+void
+harness( void ) {
+  ulong size;
+  __CPROVER_assume( size<=FD_KEYGUARD_SIGN_REQ_MTU );
+
+  uchar * buf = malloc( size );
+  if( !buf ) return;
+
+  assert( fd_keyguard_payload_check_ambiguous( buf, size )==0 );
+}