CakeML export README and useful scripts

hol/cake_export/README.md

@@ -0,0 +1,21 @@
+This directory contains facilities to compile P4 programs to binary using CakeML. Currently, this uses the unverified export mechanism.
+
+The translations from HOL4 uses the version of CakeML at commit [`d4f0662af`](https://github.com/CakeML/cakeml/tree/d4f0662af8596e6f964e54519b206be44e5b9f71), which for our use case appears to be compatible with the Trindemossen-1 release of HOL4 currently used for HOL4P4 (no CakeML release is compatible with Trindemossen-1).
+
+The compilation of the CakeML S-expression obtained from translation uses the release [v2702](https://github.com/CakeML/cakeml/releases/tag/v2702) of CakeML - note that this release is later than the commit used for obtaining the S-expression in the first place. You may want to consider using release [v2419](https://github.com/CakeML/cakeml/releases/tag/v2419) if any issue arises at this step, since this is closer to the commit being used for translation.
+
+To download this release, run in this directory e.g.:
+
+```bash
+wget https://github.com/CakeML/cakeml/releases/download/v2702/cake-x64-64.tar.gz
+tar -xvf cake-x64-64.tar.gz -C test/ --strip-components=1
+rm cake-x64-64.tar.gz
+```
+
+Two example programs are featured: a tiny program from the symbolic executor in `p4_conditional_cakeProgScript.sml` and the VSS example in `p4_vss_example_cakeProgScript.sml`. To compile your own programs to binary, use the HOL4P4 import tool to obtain the static environment `actx` and initial state `astate`, then supply a suitably large amount of maximum steps to `n_max`. Your programs may feature additional externs which have not been translated yet - in that case, you will have to add the translations in the corresponding `p4_exec_sem_ARCH_cakeProgScript.sml`, where "`ARCH`" is replaced by your architecture.
+
+To test the translation of the VSS example, after downloading the necessary CakeML release run:
+
+```bash
+./vss_test.sh
+```

hol/cake_export/test/compile_test_cake.sh

@@ -0,0 +1,13 @@
+#!/bin/bash
+
+progname=$1
+
+if [ -z $1 ]; then
+  echo "Usage: supply the name of the CakeML sexp file without the .sexp suffix as a command-line argument"
+  exit 0
+fi
+
+# NOTE: Always set skip_type_inference to false if you don't know what you're doing when in-lining CakeML code.
+CML_STACK_SIZE=1000 CML_HEAP_SIZE=6000 ./cake --sexp=true --exclude_prelude=true --skip_type_inference=true --emit_empty_ffi=true --reg_alg=0 < $progname.sexp > $progname.cake.S
+
+cc ${progname}.cake.S basis_ffi.c -o ${progname}.cake

hol/cake_export/vss_test.sh

@@ -0,0 +1,11 @@
+#!/bin/bash
+
+progname=vss_example
+
+Holmake p4_${progname}_cakeProgTheory
+cp ${progname}.sexp test/
+cd test
+./compile_test_cake.sh ${progname}
+# TODO: This packet is expected to be dropped. Hard-code some tables to obtain a better example.
+time ./${progname}.cake 0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000100000000000010001010000000000000000000101000000000101000000000010100000000000000001000000000101000000000010100000000101000000010000000010000000000000000000000000000000000000000000000000000000000000000000 1
+cd ..