Get Aarch64 exported to HOL4

Worked around problem with the model where it tries to use bound variables
in patterns

4 files changed, 71 insertions, 51 deletions

diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem
index 03a3b390..f9027593 100644
--- a/aarch64/mono/aarch64_extras.lem
+++ b/aarch64/mono/aarch64_extras.lem
@@ -8,12 +8,15 @@ open import Prompt
 type ty512
 instance (Size ty512) let size = 512 end
 declare isabelle target_rep type ty512 = `512`
+declare hol target_rep type ty512 = `512`
 type ty1024
 instance (Size ty1024) let size = 1024 end
 declare isabelle target_rep type ty1024 = `1024`
+declare hol target_rep type ty1024 = `1024`
 type ty2048
 instance (Size ty2048) let size = 2048 end
 declare isabelle target_rep type ty2048 = `2048`
+declare hol target_rep type ty2048 = `2048`
 
 let hexchar_to_bool_list c =
   if c = #'0' then      Just ([false;false;false;false])
@@ -50,13 +53,10 @@ let hexstring_to_bools s =
 
 val hex_slice : forall 'rv 'n 'e. Size 'n => string -> integer -> integer -> monad 'rv (mword 'n) 'e
 let hex_slice v len lo =
-  match hexstring_to_bools v with
-    | Just bs ->
-       let hi = len + lo - 1 in
-       let bs = ext_list false (len + lo) bs in
-       return (of_bools (subrange_list false bs hi lo))
-    | Nothing -> Fail "hex_slice"
-  end
+  maybe_fail "hex_slice" (hexstring_to_bools v) >>= fun bs ->
+   let hi = len + lo - 1 in
+   let bs = ext_list false (len + lo) bs in
+   return (of_bools (subrange_list false bs hi lo))
 
 let internal_pick vs = return (head vs)
 
diff --git a/aarch64/mono/demo/Holmakefile b/aarch64/mono/demo/Holmakefile
new file mode 100644
index 00000000..47959f81
--- /dev/null
+++ b/aarch64/mono/demo/Holmakefile
@@ -0,0 +1,11 @@
+LEMDIR=../../../../lem/hol-lib
+
+INCLUDES = $(LEMDIR) ../../../lib/hol
+
+all: aarch64_monoTheory.uo
+.PHONY: all
+
+ifdef POLY
+HOLHEAP = ../../../lib/hol/sail-heap
+
+endif
diff --git a/aarch64/mono/demo/aarch64_no_vector/spec.sail b/aarch64/mono/demo/aarch64_no_vector/spec.sail
index 01b7660a..7f3fb09e 100644
--- a/aarch64/mono/demo/aarch64_no_vector/spec.sail
+++ b/aarch64/mono/demo/aarch64_no_vector/spec.sail
@@ -6760,10 +6760,10 @@ function AArch64_StateMatch (SSC__arg, HMC__arg, PxC__arg, linked__arg, LBN, isb
   priv_match : bool = undefined;
   if ~(ispriv) & ~(isbreakpnt) then priv_match = EL0_match
   else match PSTATE.EL {
-    EL3 => priv_match = EL3_match,
-    EL2 => priv_match = EL2_match,
-    EL1 => priv_match = EL1_match,
-    EL0 => priv_match = EL0_match
+    ? if ? == EL3 => priv_match = EL3_match,
+    ? if ? == EL2 => priv_match = EL2_match,
+    ? if ? == EL1 => priv_match = EL1_match,
+    ? if ? == EL0 => priv_match = EL0_match
   };
   security_state_match : bool = undefined;
   match SSC {
@@ -7067,20 +7067,20 @@ function Strip (A, data) = {
   else
     original_ptr = slice(extfield, 0, negate(bottom_PAC_bit) + 64) @ slice(A, 0, bottom_PAC_bit);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       TrapEL2 = false;
       TrapEL3 = false
     }
@@ -7115,23 +7115,23 @@ function AuthIB (X, Y) = {
   Enable : bits(1) = undefined;
   APIBKey_EL1 : bits(128) = slice(APIBKeyHi_EL1, 0, 64) @ slice(APIBKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[30]] else [SCTLR_EL2[30]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[30]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[30]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[30]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7189,23 +7189,23 @@ function AuthIA (X, Y) = {
   Enable : bits(1) = undefined;
   APIAKey_EL1 : bits(128) = slice(APIAKeyHi_EL1, 0, 64) @ slice(APIAKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[31]] else [SCTLR_EL2[31]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[31]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[31]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[31]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7276,23 +7276,23 @@ function AuthDB (X, Y) = {
   Enable : bits(1) = undefined;
   APDBKey_EL1 : bits(128) = slice(APDBKeyHi_EL1, 0, 64) @ slice(APDBKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[13]] else [SCTLR_EL2[13]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[13]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[13]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[13]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7319,23 +7319,23 @@ function AuthDA (X, Y) = {
   Enable : bits(1) = undefined;
   APDAKey_EL1 : bits(128) = slice(APDAKeyHi_EL1, 0, 64) @ slice(APDAKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[27]] else [SCTLR_EL2[27]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[27]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[27]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[27]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7362,23 +7362,23 @@ function AddPACIB (X, Y) = {
   Enable : bits(1) = undefined;
   APIBKey_EL1 : bits(128) = slice(APIBKeyHi_EL1, 0, 64) @ slice(APIBKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[30]] else [SCTLR_EL2[30]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[30]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[30]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[30]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7436,23 +7436,23 @@ function AddPACIA (X, Y) = {
   Enable : bits(1) = undefined;
   APIAKey_EL1 : bits(128) = slice(APIAKeyHi_EL1, 0, 64) @ slice(APIAKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[31]] else [SCTLR_EL2[31]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[31]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[31]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[31]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7509,20 +7509,20 @@ function AddPACGA (X, Y) = {
   TrapEL3 : bool = undefined;
   APGAKey_EL1 : bits(128) = slice(APGAKeyHi_EL1, 0, 64) @ slice(APGAKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       TrapEL2 = false;
       TrapEL3 = false
     }
@@ -7548,23 +7548,23 @@ function AddPACDB (X, Y) = {
   Enable : bits(1) = undefined;
   APDBKey_EL1 : bits(128) = slice(APDBKeyHi_EL1, 0, 64) @ slice(APDBKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[13]] else [SCTLR_EL2[13]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[13]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[13]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[13]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7591,23 +7591,23 @@ function AddPACDA (X, Y) = {
   Enable : bits(1) = undefined;
   APDAKey_EL1 : bits(128) = slice(APDAKeyHi_EL1, 0, 64) @ slice(APDAKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[27]] else [SCTLR_EL2[27]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[27]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[27]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[27]];
       TrapEL2 = false;
       TrapEL3 = false
diff --git a/aarch64/mono/demo/mk.hol b/aarch64/mono/demo/mk.hol
new file mode 100755
index 00000000..ac20717f
--- /dev/null
+++ b/aarch64/mono/demo/mk.hol
@@ -0,0 +1,9 @@
+#!/bin/bash
+set -ex
+../../../sail ../../prelude.sail ../mono_rewrites.sail \
+     aarch64_no_vector/spec.sail aarch64_no_vector/decode_start.sail aarch64_no_vector/decode.sail aarch64_no_vector/decode_end.sail \
+     -no_lexp_bounds_check -memo_z3 -undefined_gen \
+     -auto_mono -mono_rewrites -dall_split_errors -dmono_continue \
+     -lem -lem_mwords -lem_sequential -lem_lib Aarch64_extras -o aarch64_mono
+lem -hol -outdir . -lib ../../../lib/hol -lib ../../../src/gen_lib/ -lib ../../../src/lem_interp ../aarch64_extras.lem aarch64_mono_types.lem aarch64_mono.lem 
+Holmake