txn: add FD_TXN_MIN_SERIALIZED_SZ

Adds constant for minimum serialized txn size.

Adds CBMC proof for lower bound, i.e.:
"There is no byte array with sz <= FD_TXN_MIN_SERIALIZED_SZ that
is successfully parsed by fd_txn_parse()."

src/ballet/txn/fd_txn.h

@@ -98,6 +98,10 @@
    transaction. */
 #define FD_TXN_MTU                  (1232UL)
 
+/* FD_TXN_MIN_SERIALIZED_SZ: The minimum size (in bytes) of a serialized
+   transaction, using fd_txn_parse() verification rules. */
+#define FD_TXN_MIN_SERIALIZED_SZ     (134UL)
+
 
 /* A Solana transaction instruction, i.e. one command or step to execute in a
    transaction.

verification/proofs/txn/minsz/Makefile

@@ -0,0 +1,15 @@
+HARNESS_ENTRY = harness
+HARNESS_FILE = fd_txn_minsz_harness
+
+PROOF_UID = fd_txn_minsz
+
+DEFINES +=
+INCLUDES += -I$(SRCDIR)
+
+REMOVE_FUNCTION_BODY +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROOF_SOURCES += $(PROOF_STUB)/fd_log.c
+PROJECT_SOURCES = $(SRCDIR)/ballet/txn/fd_txn_parse.c
+
+include ../../Makefile.common

verification/proofs/txn/minsz/cbmc-viewer.json

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

verification/proofs/txn/minsz/fd_txn_minsz_harness.c

@@ -0,0 +1,26 @@
+#include <ballet/txn/fd_txn.h>
+
+#include <assert.h>
+#include <stdlib.h>
+
+/* Prove that there is no valid serialized txn with size less than
+   FD_TXN_MIN_SERIALIZED_SZ. */
+
+void
+harness( void ) {
+  /* Input */
+  ulong input_sz;
+  __CPROVER_assume( input_sz<FD_TXN_MIN_SERIALIZED_SZ );
+  uchar * input = malloc( input_sz );
+  if( !input ) return;
+
+  /* Parsing target buffers */
+  fd_txn_parse_counters_t counters = {0};
+  uchar __attribute__((aligned((alignof(fd_txn_t))))) txn_buf[ FD_TXN_MAX_SZ ];
+
+  /* Parse */
+  ulong res = fd_txn_parse( input, input_sz, txn_buf, &counters );
+
+  /* Parsing must have failed */
+  assert( res==0UL );
+}