From 60da48e952c31c1d0a24790652414c619400da58 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Tue, 9 Jan 2024 19:36:26 +0100
Subject: [PATCH] update to Coq 8.18 and new version of deps

---
 .github/workflows/ci.yml  |   2 +-
 .gitlab-ci.yml            |  10 +--
 deps/Makefile             |   6 +-
 islaris.opam              |   6 +-
 sail-riscv/RV64.v         | 135 +++++++++++++++++++++++++++++++-------
 sail-riscv/memcpy.v       |  24 +++----
 sail-riscv/riscv64_test.v |  22 +++----
 sail-riscv/sail_opsem.v   |  61 ++++++++++-------
 sail-riscv/tactics.v      |  33 ++++++++--
 theories/automation.v     |   6 +-
 theories/ghost_state.v    |   6 +-
 theories/opsem.v          |  16 ++---
 12 files changed, 226 insertions(+), 101 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b671c00..efb1e95 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -22,7 +22,7 @@ jobs:
 
     env:
       OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
-      OPAM_PINS: "coq version 8.17.0   isla-lang git git+https://github.com/rems-project/isla-lang.git"
+      OPAM_PINS: "coq version 8.18.0   isla-lang git git+https://github.com/rems-project/isla-lang.git"
       CPU_CORES: "1"
       DENY_WARNINGS: "1"
       CI_RUNNER: "dummy"
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 66cac97..3e0ccc8 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -30,10 +30,10 @@ variables:
   - api
 
 ## Build jobs
-build-coq.8.17.0-timing:
+build-coq.8.18.0-timing:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.17.0   isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779"
+    OPAM_PINS: "coq version 8.18.0   isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779"
     DENY_WARNINGS: "1"
     # OPAM_PKG: "1"
   only:
@@ -43,10 +43,10 @@ build-coq.8.17.0-timing:
   tags:
   - fp-timing
 
-build-coq.8.17.0:
+build-coq.8.18.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.17.0   isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779"
+    OPAM_PINS: "coq version 8.18.0   isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779"
     DENY_WARNINGS: "1"
   only:
   - /^ci/@iris/isla-coq
@@ -54,7 +54,7 @@ build-coq.8.17.0:
 trigger-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.17.0   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV  isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779"
+    OPAM_PINS: "coq version 8.18.0   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV  isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779"
   except:
   only:
   - triggers
diff --git a/deps/Makefile b/deps/Makefile
index b4176cb..d5be9d0 100644
--- a/deps/Makefile
+++ b/deps/Makefile
@@ -16,8 +16,10 @@ sail: sail-$(SAIL_COMMIT).tar.gz
 	opam pin add coq-sail ./sail/lib/coq -n
 .PHONY: sail
 
-sail-riscv-coq: sail
-	opam pin add coq-sail-riscv 'git+https://github.com/riscv/sail-riscv#17a9929821470e119a6d5b4359d0a51d6dae6679' -n
+sail-riscv-coq:
+	opam pin add 'git+https://github.com/rems-project/sail#b14f649845db850b3673696e2aa90565fa2a60ef' -n
+	opam pin add coq-sail 'git+https://github.com/rems-project/coq-sail#169934e27ceafe393ed4d365985f7b12d974d56e' -n
+	opam pin add coq-sail-riscv 'git+https://github.com/riscv/sail-riscv#837ede9b39fae2aa97849da89c4b3b5a93344890' -n
 	opam install coq-sail-riscv
 .PHONY: sail-riscv-coq
 
diff --git a/islaris.opam b/islaris.opam
index 295c805..76c7af8 100644
--- a/islaris.opam
+++ b/islaris.opam
@@ -10,10 +10,10 @@ dev-repo: "git+https://github.com/rems-project/islaris.git"
 synopsis: "Islaris assembly verification tool"
 
 depends: [
-  "coq" { (= "8.17.0") | (= "dev") }
-  "coq-lithium" { (= "dev.2023-08-14.1.766a0051") | (= "dev") }
+  "coq" { (= "8.18.0") | (= "dev") }
+  "coq-lithium" { (= "dev.2023-11-30.0.65d25ad4") | (= "dev") }
   "coq-stdpp-unstable"
-  "coq-record-update" { (= "0.3.0") | (= "dev") }
+  "coq-record-update" { (= "0.3.3") | (= "dev") }
   "cmdliner" {>= "1.1.0"}
   "pprint"
   "integers"
diff --git a/sail-riscv/RV64.v b/sail-riscv/RV64.v
index ec6c5a8..b6cbd14 100644
--- a/sail-riscv/RV64.v
+++ b/sail-riscv/RV64.v
@@ -114,6 +114,39 @@ Lemma regstate_eta (regs : regstate) :
     uepc := uepc regs;
     uscratch := uscratch regs;
     utvec := utvec regs;
+    vcsr := vcsr regs;
+    vr31 := vr31 regs;
+    vr30 := vr30 regs;
+    vr29 := vr29 regs;
+    vr28 := vr28 regs;
+    vr27 := vr27 regs;
+    vr26 := vr26 regs;
+    vr25 := vr25 regs;
+    vr24 := vr24 regs;
+    vr23 := vr23 regs;
+    vr22 := vr22 regs;
+    vr21 := vr21 regs;
+    vr20 := vr20 regs;
+    vr19 := vr19 regs;
+    vr18 := vr18 regs;
+    vr17 := vr17 regs;
+    vr16 := vr16 regs;
+    vr15 := vr15 regs;
+    vr14 := vr14 regs;
+    vr13 := vr13 regs;
+    vr12 := vr12 regs;
+    vr11 := vr11 regs;
+    vr10 := vr10 regs;
+    vr9 := vr9 regs;
+    vr8 := vr8 regs;
+    vr7 := vr7 regs;
+    vr6 := vr6 regs;
+    vr5 := vr5 regs;
+    vr4 := vr4 regs;
+    vr3 := vr3 regs;
+    vr2 := vr2 regs;
+    vr1 := vr1 regs;
+    vr0 := vr0 regs;
     pmpaddr15 := pmpaddr15 regs;
     pmpaddr14 := pmpaddr14 regs;
     pmpaddr13 := pmpaddr13 regs;
@@ -146,6 +179,14 @@ Lemma regstate_eta (regs : regstate) :
     pmp2cfg := pmp2cfg regs;
     pmp1cfg := pmp1cfg regs;
     pmp0cfg := pmp0cfg regs;
+    vtype := vtype regs;
+    vlenb := vlenb regs;
+    vl := vl regs;
+    vxrm := vxrm regs;
+    vxsat := vxsat regs;
+    vstart := vstart regs;
+    senvcfg := senvcfg regs;
+    menvcfg := menvcfg regs;
     tselect := tselect regs;
     stval := stval regs;
     scause := scause regs;
@@ -213,6 +254,8 @@ Lemma regstate_eta (regs : regstate) :
     instbits := instbits regs;
     nextPC := nextPC regs;
     PC := PC regs;
+    vlen := vlen regs;
+    elen := elen regs;
   |}.
 Proof. now destruct regs. Qed.
 
@@ -643,6 +686,39 @@ Definition riscv_regs := [
   ("uepc", RegRef uepc_ref);
   ("uscratch", RegRef uscratch_ref);
   ("utvec", RegRef utvec_ref);
+  ("vcsr", RegRef vcsr_ref);
+  ("vr31", RegRef vr31_ref);
+  ("vr30", RegRef vr30_ref);
+  ("vr29", RegRef vr29_ref);
+  ("vr28", RegRef vr28_ref);
+  ("vr27", RegRef vr27_ref);
+  ("vr26", RegRef vr26_ref);
+  ("vr25", RegRef vr25_ref);
+  ("vr24", RegRef vr24_ref);
+  ("vr23", RegRef vr23_ref);
+  ("vr22", RegRef vr22_ref);
+  ("vr21", RegRef vr21_ref);
+  ("vr20", RegRef vr20_ref);
+  ("vr19", RegRef vr19_ref);
+  ("vr18", RegRef vr18_ref);
+  ("vr17", RegRef vr17_ref);
+  ("vr16", RegRef vr16_ref);
+  ("vr15", RegRef vr15_ref);
+  ("vr14", RegRef vr14_ref);
+  ("vr13", RegRef vr13_ref);
+  ("vr12", RegRef vr12_ref);
+  ("vr11", RegRef vr11_ref);
+  ("vr10", RegRef vr10_ref);
+  ("vr9", RegRef vr9_ref);
+  ("vr8", RegRef vr8_ref);
+  ("vr7", RegRef vr7_ref);
+  ("vr6", RegRef vr6_ref);
+  ("vr5", RegRef vr5_ref);
+  ("vr4", RegRef vr4_ref);
+  ("vr3", RegRef vr3_ref);
+  ("vr2", RegRef vr2_ref);
+  ("vr1", RegRef vr1_ref);
+  ("vr0", RegRef vr0_ref);
   ("pmpaddr15", RegRef pmpaddr15_ref);
   ("pmpaddr14", RegRef pmpaddr14_ref);
   ("pmpaddr13", RegRef pmpaddr13_ref);
@@ -675,6 +751,14 @@ Definition riscv_regs := [
   ("pmp2cfg", RegRef pmp2cfg_ref);
   ("pmp1cfg", RegRef pmp1cfg_ref);
   ("pmp0cfg", RegRef pmp0cfg_ref);
+  ("vtype", RegRef vtype_ref);
+  ("vlenb", RegRef vlenb_ref);
+  ("vl", RegRef vl_ref);
+  ("vxrm", RegRef vxrm_ref);
+  ("vxsat", RegRef vxsat_ref);
+  ("vstart", RegRef vstart_ref);
+  ("senvcfg", RegRef senvcfg_ref);
+  ("menvcfg", RegRef menvcfg_ref);
   ("tselect", RegRef tselect_ref);
   ("stval", RegRef stval_ref);
   ("scause", RegRef scause_ref);
@@ -741,20 +825,22 @@ Definition riscv_regs := [
   ("x1", RegRef x1_ref);
   ("instbits", RegRef instbits_ref);
   ("nextPC", RegRef nextPC_ref);
-  ("PC", RegRef PC_ref)
+  ("PC", RegRef PC_ref);
+  ("vlen", RegRef vlen_ref);
+  ("elen", RegRef elen_ref)
 ].
 
 Lemma get_regval_refs_eq r regs regs':
-  (∀ rf, (r, rf) ∈ riscv_regs → rf.(reg_ref_ref).(read_from) regs' = rf.(reg_ref_ref).(read_from) regs) →
+  (Forall (λ '(r', rf), r = r' → rf.(reg_ref_ref).(read_from) regs' = rf.(reg_ref_ref).(read_from) regs) riscv_regs) →
   get_regval r regs' = get_regval r regs.
 Proof.
   unfold get_regval.
   have Hcase : ∀ s (e1 e2 e1' e2' : option register_value) rf' rfs,
       (read_from (reg_ref_ref rf') regs' = read_from (reg_ref_ref rf') regs → e1 = e1') →
-      ((∀ rf, (r, rf) ∈ rfs → read_from (reg_ref_ref rf) regs' = read_from (reg_ref_ref rf) regs) → e2 = e2') →
-      (∀ rf, (r, rf) ∈ (s, rf')::rfs → read_from (reg_ref_ref rf) regs' = read_from (reg_ref_ref rf) regs) →
+      ((Forall (λ '(r', rf), r = r' → read_from (reg_ref_ref rf) regs' = read_from (reg_ref_ref rf) regs) rfs) → e2 = e2') →
+      (Forall (λ '(r', rf), r = r' → read_from (reg_ref_ref rf) regs' = read_from (reg_ref_ref rf) regs) ((s, rf')::rfs)) →
       (if string_dec r s then e1 else e2) = (if string_dec r s then e1' else e2'). {
-    move => s ?????? He1 He2 Hf2. destruct (string_dec r s); set_solver.
+    move => s ?????? He1 He2 /(Forall_cons_1 _ _ _) [??]. destruct (string_dec r s); naive_solver.
   }
   repeat (apply Hcase; [ by destruct regs, regs' => -> |]). done.
 Qed.
@@ -781,7 +867,7 @@ Lemma get_set_regval_ne r r' regs regs' v:
   get_regval r regs' = get_regval r regs.
 Proof.
   move => /set_regval_refs_eq[rf1 [? [Hin1 ->]]] Hneq.
-  apply get_regval_refs_eq => rf2 Hin2.
+  apply get_regval_refs_eq.
   have Hcase : ∀ a b (P : Prop) r rf (rfs : list (string * register_ref_record)),
       (a = r → b = rf → P) →
       ((a, b) ∈ rfs → P) →
@@ -790,23 +876,28 @@ Proof.
   }
   destruct regs.
   revert Hin1.
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 10 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
-  do 8 (apply Hcase; [abstract (move => ? ?; subst; revert Hin2; repeat (apply Hcase; [move => ? ->; done|]); by move =>/elem_of_nil)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 10 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
+  do 1 (apply Hcase; [abstract (move => ??; subst; repeat constructor; done)|]).
   by move =>/elem_of_nil.
-Qed.
+Time Qed.
 
 Lemma get_regval_None_stable r regs regs':
   get_regval r regs = None →
diff --git a/sail-riscv/memcpy.v b/sail-riscv/memcpy.v
index 6609bb3..692ab57 100644
--- a/sail-riscv/memcpy.v
+++ b/sail-riscv/memcpy.v
@@ -93,14 +93,14 @@ Proof.
   unfold translateAddr. red_sim. rewrite mstatus_nextPC cur_privilege_nextPC.
   apply sim_effectivePrivilege; [done|]. red_sim.
   unfold translateAddr_priv. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim.
   unfold translationMode.
   have -> : (cur_privilege regs) = Machine by destruct (cur_privilege regs). red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim. rewrite x11_nextPC.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim. rewrite x11_nextPC.
   unfold mem_read. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim. rewrite mstatus_nextPC.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim. rewrite mstatus_nextPC.
   apply sim_effectivePrivilege; [done|]. red_sim.
   rewrite Hassume. red_sim.
   rewrite if_false; [|shelve]. rewrite if_true; [|shelve]. red_sim.
@@ -116,7 +116,7 @@ Proof.
     + rewrite ->Hassume1, Hassume2, !bv_add_unsigned, !bv_unsigned_BV in *.
       unfold bv_wrap, bv_modulus in *. lia.
   - by rewrite mword_to_bv_add_vec.
-  - rewrite mword_to_bv_EXTS // mword_to_bv_to_mword //.
+  - rewrite mword_to_bv_sign_extend' // mword_to_bv_to_mword //.
   - rewrite mword_to_bv_add_vec //.
     Unshelve. all: exact: inhabitant.
 Qed.
@@ -130,14 +130,14 @@ Proof.
   unfold translateAddr. red_sim. rewrite mstatus_nextPC cur_privilege_nextPC.
   apply sim_effectivePrivilege; [done|]. red_sim.
   unfold translateAddr_priv. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim.
   unfold translationMode.
   have -> : (cur_privilege regs) = Machine by destruct (cur_privilege regs). red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim. rewrite x10_nextPC.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim. rewrite x10_nextPC.
   unfold mem_write_value, mem_write_value_meta. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim. rewrite mstatus_nextPC cur_privilege_nextPC.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim. rewrite mstatus_nextPC cur_privilege_nextPC.
   apply sim_effectivePrivilege; [done|]. red_sim.
   rewrite Hassume. red_sim.
   rewrite if_false; [|shelve]. rewrite if_true; [|shelve]. red_sim.
@@ -195,7 +195,7 @@ Proof.
   move => regs. unfold step_cpu, a18.
   red_sim. unfold execute. red_sim. unfold execute_BTYPE.
   red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim. rewrite x12_nextPC.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim. rewrite x12_nextPC.
   destruct (neq_vec (x12 regs) zero_reg) eqn: Hx12; unfold neq_vec in Hx12; sim_simpl_hyp Hx12; red_sim.
   - apply: (sim_tcases 0); [done|]. red_sim.
     rewrite bit_to_bool_false; [|shelve]. red_sim.
diff --git a/sail-riscv/riscv64_test.v b/sail-riscv/riscv64_test.v
index 38f8654..fe3efe4 100644
--- a/sail-riscv/riscv64_test.v
+++ b/sail-riscv/riscv64_test.v
@@ -91,14 +91,14 @@ Proof.
   unfold translateAddr. red_sim. rewrite mstatus_nextPC.
   apply sim_effectivePrivilege; [done|]. red_sim.
   unfold translateAddr_priv. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim.
   unfold translationMode. rewrite cur_privilege_nextPC.
   have -> : (cur_privilege regs) = Machine by destruct (cur_privilege regs). red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim. rewrite x11_nextPC.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim. rewrite x11_nextPC.
   unfold mem_write_value, mem_write_value_meta. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim. rewrite mstatus_nextPC.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim. rewrite mstatus_nextPC.
   apply sim_effectivePrivilege; [done|]. red_sim.
   rewrite Hassume. red_sim.
   rewrite if_false; [|shelve]. rewrite if_true; [|shelve]. red_sim.
@@ -132,14 +132,14 @@ Proof.
   unfold translateAddr. red_sim. rewrite mstatus_nextPC.
   apply sim_effectivePrivilege; [done|]. red_sim.
   unfold translateAddr_priv. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim.
   unfold translationMode. rewrite cur_privilege_nextPC.
   have -> : (cur_privilege regs) = Machine by destruct (cur_privilege regs). red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim. rewrite x2_nextPC.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim. rewrite x2_nextPC.
   unfold mem_read. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim. rewrite mstatus_nextPC.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|]. red_sim. rewrite mstatus_nextPC.
   apply sim_effectivePrivilege; [done|]. red_sim.
   rewrite Hassume. red_sim.
   rewrite if_false; [|shelve]. rewrite if_true; [|shelve]. red_sim.
@@ -159,7 +159,7 @@ Proof.
       change (2 + 1 - 0)%N with (3%N).
       lia.
   - by rewrite mword_to_bv_add_vec.
-  - rewrite mword_to_bv_EXTS // mword_to_bv_to_mword //.
+  - rewrite mword_to_bv_sign_extend' // mword_to_bv_to_mword //.
   - by rewrite mword_to_bv_add_vec.
     Unshelve. all: exact: inhabitant.
 Qed.
diff --git a/sail-riscv/sail_opsem.v b/sail-riscv/sail_opsem.v
index ceb7c6a..1cbf9df 100644
--- a/sail-riscv/sail_opsem.v
+++ b/sail-riscv/sail_opsem.v
@@ -100,7 +100,7 @@ Lemma mword_to_bv_unsigned {n1 n2} (b : mword n1):
   n1 = Z.of_N n2 →
   bv_unsigned (mword_to_bv (n2:=n2) b) = Z.of_N (Word.wordToN (get_word b)).
 Proof.
-  move => Heq. rewrite /mword_to_bv/Z_to_bv_checked. case_option_guard as Hn => //=.
+  move => Heq. rewrite /mword_to_bv/Z_to_bv_checked. case_guard as Hn => //=.
   contradict Hn. apply/bv_wf_in_range. unfold bv_modulus.
   have /lt_Npow2:= Word.wordToN_bound (get_word b). subst. lia.
 Qed.
@@ -251,7 +251,7 @@ Qed.
 
 Lemma unfold_sign_extend m n (w: Word.word m) :
   forall H : (m <= n)%nat,
-  MachineWord.sign_extend n w = cast_nat (Word.sext w (n - m)) (le_plus_minus_r m n H).
+  MachineWord.sign_extend n w = cast_nat (Word.sext w (n - m)) (MachineWord.MachineWord.extend_ok H).
 Proof.
   intro.
   rewrite /MachineWord.sign_extend.
@@ -268,19 +268,19 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma mword_to_bv_EXTS n1 n2' n2 (b : mword n1):
+Lemma mword_to_bv_sign_extend' n1 n2' n2 (b : mword n1):
   0 ≤ n1 →
   n2' = Z.of_N n2 →
   n1 ≤ n2' →
-  mword_to_bv (n2:=n2) (@EXTS _ n2' b) = bv_sign_extend _ (mword_to_bv (n2:=(Z.to_N n1)) b).
+  mword_to_bv (n2:=n2) (sign_extend' n2' b) = bv_sign_extend _ (mword_to_bv (n2:=(Z.to_N n1)) b).
 Proof.
   move => ???.
-  apply bv_eq_signed. rewrite mword_to_bv_signed //. rewrite /EXTS/sign_extend/exts_vec/= get_word_to_word.
+  apply bv_eq_signed. rewrite mword_to_bv_signed //. rewrite /sign_extend'/sign_extend/exts_vec/= get_word_to_word.
   rewrite unfold_sign_extend. 1: lia. move => ?. rewrite wordToZ_cast_nat.
   rewrite Word.sext_wordToZ bv_sign_extend_signed ?mword_to_bv_signed //.
   all: lia.
 Qed.
-Arguments EXTS : simpl never.
+Global Arguments sign_extend' : simpl never.
 
 (* #[local] Hint Rewrite wordToN_spec_high Z_of_bool_spec_high using lia : rewrite_bits_db. *)
 Lemma mword_to_bv_update_vec_dec n1 n2 (b : mword n1) b1 z b2:
@@ -411,15 +411,28 @@ Proof.
   f_equal. lia.
 Qed.
 
-Definition register_value_to_valu (v : register_value) : valu :=
+Definition register_value_to_valu (r : register_name) (v : register_value) : valu :=
+  if bool_decide (r = "misa" ∨ r = "mstatus") then
+    if v is Regval_bitvector_64 m then
+      RegVal_Struct [("bits", RVal_Bits (mword_to_bv (n2:=64) m))]
+    else
+      RegVal_Poison
+  else
   match v with
-  | Regval_bitvector_64_dec m => RVal_Bits (mword_to_bv (n2:=64) m)
+  | Regval_bitvector_1 m => RVal_Bits (mword_to_bv (n2:=1) m)
+  | Regval_bitvector_2 m => RVal_Bits (mword_to_bv (n2:=2) m)
+  | Regval_bitvector_3 m => RVal_Bits (mword_to_bv (n2:=3) m)
+  | Regval_bitvector_4 m => RVal_Bits (mword_to_bv (n2:=4) m)
+  | Regval_bitvector_8 m => RVal_Bits (mword_to_bv (n2:=8) m)
+  | Regval_bitvector_16 m => RVal_Bits (mword_to_bv (n2:=16) m)
+  | Regval_bitvector_32 m => RVal_Bits (mword_to_bv (n2:=32) m)
+  | Regval_bitvector_64 m => RVal_Bits (mword_to_bv (n2:=64) m)
+  | Regval_bitvector_65536 m => RVal_Bits (mword_to_bv (n2:=65536) m)
   | Regval_bool b => RVal_Bool b
-  | Regval_Misa m => RegVal_Struct [("bits", RVal_Bits (mword_to_bv (n2:=64) m.(Misa_bits)))]
-  | Regval_Mstatus m => RegVal_Struct [("bits", RVal_Bits (mword_to_bv (n2:=64) m.(Mstatus_bits)))]
   | Regval_Privilege p => RVal_Enum (match p with | User => "User" | Supervisor => "Supervisor" | Machine => "Machine" end)
   | _ => RegVal_Poison
   end.
+Global Arguments register_value_to_valu !_ !_ /.
 
 Lemma iris_module_wf_isla_lang :
   iris_module_wf isla_lang.
@@ -544,13 +557,13 @@ Definition get_plat_config (reg_name : string) : option register_value :=
   match reg_name with
   | "rv_enable_pmp" => Some (Regval_bool (plat_enable_pmp ()))
   | "rv_enable_misaligned_access" => Some (Regval_bool (plat_enable_misaligned_access ()))
-  | "rv_ram_base" => Some (Regval_bitvector_64_dec (plat_ram_base ()))
-  | "rv_ram_size" => Some (Regval_bitvector_64_dec (plat_ram_size ()))
-  | "rv_rom_base" => Some (Regval_bitvector_64_dec (plat_rom_base ()))
-  | "rv_rom_size" => Some (Regval_bitvector_64_dec (plat_rom_size ()))
-  | "rv_clint_base" => Some (Regval_bitvector_64_dec (plat_clint_base ()))
-  | "rv_clint_size" => Some (Regval_bitvector_64_dec (plat_clint_size ()))
-  | "rv_htif_tohost" => Some (Regval_bitvector_64_dec (plat_htif_tohost ()))
+  | "rv_ram_base" => Some (Regval_bitvector_64 (plat_ram_base ()))
+  | "rv_ram_size" => Some (Regval_bitvector_64 (plat_ram_size ()))
+  | "rv_rom_base" => Some (Regval_bitvector_64 (plat_rom_base ()))
+  | "rv_rom_size" => Some (Regval_bitvector_64 (plat_rom_size ()))
+  | "rv_clint_base" => Some (Regval_bitvector_64 (plat_clint_base ()))
+  | "rv_clint_size" => Some (Regval_bitvector_64 (plat_clint_size ()))
+  | "rv_htif_tohost" => Some (Regval_bitvector_64 (plat_htif_tohost ()))
   | "Machine" => Some (Regval_Privilege (Machine))
   | _ => None
   end.
@@ -562,7 +575,7 @@ Definition get_regval_or_config (reg_name : string) (s : regstate) : option regi
   end.
 
 Definition isla_regs_wf (regs : regstate) (isla_regs : reg_map) : Prop :=
-  ∀ r vi, isla_regs !! r = Some vi → ∃ vs, get_regval_or_config r regs = Some vs ∧ vi = (register_value_to_valu vs).
+  ∀ r vi, isla_regs !! r = Some vi → ∃ vs, get_regval_or_config r regs = Some vs ∧ vi = (register_value_to_valu r vs).
 
 Definition private_regs_wf (isla_regs : reg_map) : Prop :=
   isla_regs !! "nextPC" = None.
@@ -723,7 +736,7 @@ Qed.
 Lemma sim_read_reg A E Σ K e2 ann r v v':
   get_regval (name r) Σ.(sim_regs) = Some v' →
   of_regval r v' = Some (read_from r Σ.(sim_regs)) →
-  v = register_value_to_valu v' →
+  v = register_value_to_valu (name r) v' →
   sim (A:=A) (E:=E) Σ (Done (read_from r Σ.(sim_regs))) K e2 →
   sim (A:=A) (E:=E) Σ (read_reg r) K (ReadReg (name r) [] v ann :t: e2).
 Proof.
@@ -743,7 +756,7 @@ Qed.
 
 Lemma sim_ReadReg_config A E Σ K e1 e2 ann r v v':
   get_plat_config r = Some v' →
-  v = register_value_to_valu v' →
+  v = register_value_to_valu r v' →
   sim (A:=A) (E:=E) Σ e1 K e2 →
   sim (A:=A) (E:=E) Σ e1 K (ReadReg r [] v ann :t: e2).
 Proof.
@@ -763,7 +776,7 @@ Qed.
 Lemma sim_write_reg {A E} Σ (r : register_ref _ _ A) e2 v K v' ann:
   name r ≠ "tlb48" ∧ name r ≠ "tlb39" →
   set_regval (name r) (regval_of r v) Σ.(sim_regs) = Some (write_to r v Σ.(sim_regs)) →
-  v' = register_value_to_valu (regval_of r v) →
+  v' = register_value_to_valu (name r) (regval_of r v) →
   sim (Σ <|sim_regs := write_to r v Σ.(sim_regs)|>) (Done tt) K e2 →
   sim (E:=E) Σ (write_reg r v) K (WriteReg (name r) [] v' ann :t: e2).
 Proof.
@@ -894,7 +907,7 @@ Proof.
     (read_mem_list mem (bv_unsigned a') len' = None ∧
        bv_unsigned a' + Z.of_N len' ≤ 2 ^ 64 ∧
        set_Forall (λ ad, ¬ (bv_unsigned a' ≤ bv_unsigned ad < bv_unsigned a' + Z.of_N len')) (dom mem))). {
-    efeed pose proof Hsafe as He.
+    opose proof* Hsafe as He.
     { apply: steps_l'; [|apply steps_refl|done].
       constructor. econstructor; [done|eapply (DeclareConstBitVecS' (bv_0 _))|] => /=. done. }
     move: He => [| {}Hsafe]. { unfold seq_to_val. by case. }
@@ -1027,7 +1040,7 @@ Qed.
 Definition eval_assume_val' (regs : regstate) (v : assume_val) : option base_val :=
   match v with
   | AVal_Var r l => v' ← get_regval_or_config r regs;
-                   v'' ← read_accessor l (register_value_to_valu v');
+                   v'' ← read_accessor l (register_value_to_valu r v');
                    if v'' is RegVal_Base b then Some b else None
   | AVal_Bool b => Some (Val_Bool b)
   | AVal_Bits b => Some (Val_Bits b)
@@ -1093,7 +1106,7 @@ Proof.
 Qed.
 
 Lemma sim_AssumeReg A E Σ K e1 e2 ann r v al:
-  ((v' ← get_regval_or_config r Σ.(sim_regs); read_accessor al (register_value_to_valu v')) = Some v
+  ((v' ← get_regval_or_config r Σ.(sim_regs); read_accessor al (register_value_to_valu r v')) = Some v
     → sim (A:=A) (E:=E) Σ e1 K e2) →
   sim (A:=A) (E:=E) Σ e1 K (AssumeReg r al v ann :t: e2).
 Proof.
diff --git a/sail-riscv/tactics.v b/sail-riscv/tactics.v
index 4b3b803..cd24c3e 100644
--- a/sail-riscv/tactics.v
+++ b/sail-riscv/tactics.v
@@ -183,6 +183,25 @@ Ltac sim_simpl_hyp H :=
   try apply bool_decide_eq_false_1 in H;
   try (apply Eqdep_dec.inj_pair2_eq_dec in H; [|by move => ??; apply decide; apply _]).
 
+
+Lemma of_regval_regval_of_mstatus a :
+ Mstatus_of_regval (regval_of_Mstatus a) = Some a.
+Proof. by destruct a. Qed.
+Lemma of_regval_regval_of_misa a :
+ Misa_of_regval (regval_of_Misa a) = Some a.
+Proof. by destruct a. Qed.
+
+Ltac solve_of_regval_regval_of :=
+  match goal with
+  (* some goals of this form contain eta expansions that done cannot
+  solve, so we have to manually apply a lemma *)
+  | _ =>
+      by apply of_regval_regval_of_mstatus
+  | _ =>
+      by apply of_regval_regval_of_misa
+  | _ => done
+  end.
+
 Ltac red_monad_sim :=
   repeat match goal with
          | |- sim _ (_ >>= _) _ _  => apply sim_bind
@@ -212,7 +231,7 @@ Ltac red_monad_sim :=
          | |- sim _ _ _ (AssumeReg _ _ _ _:t:_)  =>
              let H := fresh "Hassume" in apply: sim_AssumeReg => H; simpl in H; sim_simpl_hyp H
          | |- sim _ _ _ (ReadReg _ _ _ _:t:_)  => apply: sim_ReadReg_config; [reflexivity | try done; shelve|]
-         | |- sim _ (read_reg _) _ (ReadReg _ _ _ _:t:_)  => apply: sim_read_reg; [done | done | try done; shelve|]
+         | |- sim _ (read_reg _) _ (ReadReg _ _ _ _:t:_)  => apply: sim_read_reg; [done | solve_of_regval_regval_of | try done; shelve|]
          | |- sim _ (write_reg nextPC_ref _) _ _  => apply: sim_write_reg_private; [done..|]
          | |- sim _ (read_reg nextPC_ref) _ _  => apply: sim_read_reg_l; [done..|]
          | |- sim _ (get_next_pc ()) _ _  => apply: sim_read_reg_l; [done..|]
@@ -290,9 +309,9 @@ Lemma sim_haveFExt Σ K e2:
 Proof.
   move => Hsim.
   unfold haveFExt. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
-  case_match => //. red_sim.
-  apply: sim_read_reg_l; [done|].
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|].
+  red_sim. case_match => //. red_sim.
+  apply sim_read_reg_l; [solve_of_regval_regval_of|].
   by red_sim.
 Qed.
 
@@ -302,9 +321,9 @@ Lemma sim_haveDExt Σ K e2:
 Proof.
   move => Hsim.
   unfold haveDExt. red_sim.
-  apply: sim_read_reg_l; [done|]. red_sim.
-  case_match => //. red_sim.
-  apply: sim_read_reg_l; [done|].
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|].
+  red_sim. case_match => //. red_sim.
+  apply: sim_read_reg_l; [solve_of_regval_regval_of|].
   by red_sim.
 Qed.
 
diff --git a/theories/automation.v b/theories/automation.v
index 0c43fa7..227e4cd 100644
--- a/theories/automation.v
+++ b/theories/automation.v
@@ -371,7 +371,7 @@ this is useful (if one defines a function [Definition test_to_A {A} (x : A) (X :
 then vm_compute still reduces x). *)
 Ltac solve_compute_wp_exp :=
   let H := fresh in move => ? H;
-  lazy [eval_exp' mapM mbind option_bind eval_unop eval_manyop eval_binop option_fmap option_map fmap mret option_ret foldl bvn_to_bv decide decide_rel BinNat.N.eq_dec N.eq_dec N_rec N_rect bvn_n sumbool_rec sumbool_rect BinPos.Pos.eq_dec Pos.eq_dec positive_rect positive_rec eq_rect eq_ind_r eq_ind eq_sym bvn_val N.add N.sub Pos.add Pos.succ mguard option_guard Pos.sub_mask Pos.double_mask Pos.succ_double_mask Pos.pred_double Pos.double_pred_mask];
+  lazy [eval_exp' mapM mbind option_bind eval_unop eval_manyop eval_binop option_fmap option_map fmap mret option_ret guard_or mthrow option_mfail foldl bvn_to_bv decide decide_rel BinNat.N.eq_dec N.eq_dec N_rec N_rect bvn_n sumbool_rec sumbool_rect BinPos.Pos.eq_dec Pos.eq_dec positive_rect positive_rec eq_rect eq_ind_r eq_ind eq_sym bvn_val N.add N.sub Pos.add Pos.succ Pos.sub_mask Pos.double_mask Pos.succ_double_mask Pos.pred_double Pos.double_pred_mask];
   lazymatch goal with | |- Some _ = _ => idtac | |- ?G => idtac "solve_compute_wp_exp failed:" G; fail end;
   autorewrite with isla_coq_rewrite;
   apply H.
@@ -543,7 +543,7 @@ Proof.
         move: Hs => [Hlen Hall'']. move: (Hall'') => /Forall_fold_right/(Forall_lookup_1 _ _ _ _)Hall.
         have [|[??]?]:= lookup_lt_is_Some_2 rs i.
         { rewrite -Hlen. apply: lookup_lt_is_Some_1. naive_solver. }
-        efeed pose proof Hall as Hall'. { by rewrite ->lookup_zip_with; simplify_option_eq. }
+        opose proof* Hall as Hall'. { by rewrite ->lookup_zip_with; simplify_option_eq. }
         destruct Hall' as [??]; simplify_eq.
         iExists _, _. rewrite ->reg_col_cons. iSplit; [done|]. iFrame. iSplit. {
           iPureIntro. rewrite /read_accessor => /=. apply bind_Some. eexists _. split.
@@ -551,7 +551,7 @@ Proof.
           apply list_find_idx_Some. eexists (_, _). split_and! => //. move => j[??]?/=.
           have [|[??]?]:= lookup_lt_is_Some_2 ss j.
           { rewrite Hlen. apply: lookup_lt_is_Some_1. naive_solver. }
-          efeed pose proof Hall as Hall'. { by rewrite ->lookup_zip_with; simplify_option_eq. }
+          opose proof* Hall as Hall'. { by rewrite ->lookup_zip_with; simplify_option_eq. }
           eapply (Hnot _ (_, _)). naive_solver.
         }
         iIntros "[? %]". iExists _. by iFrame.
diff --git a/theories/ghost_state.v b/theories/ghost_state.v
index 24a8ac4..b3a966e 100644
--- a/theories/ghost_state.v
+++ b/theories/ghost_state.v
@@ -307,7 +307,7 @@ Section instr.
   Proof.
     rewrite instr_eq. iIntros (??) "?". iExists _, _. iFrame.
     iPureIntro. split; [|done].
-    unfold Z_to_bv_checked. case_option_guard => //.
+    unfold Z_to_bv_checked. case_guard => //=.
     f_equal. by apply bv_eq.
   Qed.
 
@@ -332,7 +332,7 @@ Section instr.
     instr_ctx instrs -∗ instr (bv_unsigned a) i -∗ ⌜instrs !! a = i⌝.
   Proof.
     iIntros "Hctx Hinstr". iDestruct (instr_lookup with "Hctx Hinstr") as %[b [Hb ?]].
-    iPureIntro. unfold Z_to_bv_checked in *. case_option_guard => //; by simplify_eq.
+    iPureIntro. unfold Z_to_bv_checked in *. case_guard => //=; by simplify_eq/=.
   Qed.
 
 End instr.
@@ -364,7 +364,7 @@ Section reg.
         move => [??] /=? /lookup_kmap_Some[?[? /elem_of_list_to_map/(elem_of_list_lookup_1 _ _)[//|i ?]]]; simplify_map_eq.
         eexists _, _. split_and! => //.
         apply list_find_idx_Some. eexists _. split_and!; [done..|] => j[??]/=???; simplify_eq.
-        efeed pose proof (NoDup_lookup l.*1 i j); [done| rewrite list_lookup_fmap fmap_Some.. | lia].
+        opose proof* (NoDup_lookup l.*1 i j); [done| rewrite list_lookup_fmap fmap_Some.. | lia].
         all: naive_solver.
       + move => ? [? /lookup_delete_Some[??]] [?[?/lookup_union_Some[| |]]]; [| |naive_solver].
         { apply map_disjoint_spec => -[??]?? /lookup_kmap_Some. naive_solver. }
diff --git a/theories/opsem.v b/theories/opsem.v
index 46c10a6..9dcbd12 100644
--- a/theories/opsem.v
+++ b/theories/opsem.v
@@ -281,28 +281,28 @@ Definition eval_binop (b : binop) (v1 v2 : base_val) : option base_val :=
     Some (Val_Bits (bv_ashiftr n1.(bvn_val) n2'))
 
   | Bvcomp Bvult, Val_Bits n1, Val_Bits n2 =>
-    guard (n1.(bvn_n) = n2.(bvn_n));
+    guard (n1.(bvn_n) = n2.(bvn_n));;
     Some (Val_Bool (bool_decide (bv_unsigned n1.(bvn_val) < bv_unsigned n2.(bvn_val))))
   | Bvcomp Bvslt, Val_Bits n1, Val_Bits n2 =>
-    guard (n1.(bvn_n) = n2.(bvn_n));
+    guard (n1.(bvn_n) = n2.(bvn_n));;
     Some (Val_Bool (bool_decide (bv_signed n1.(bvn_val) < bv_signed n2.(bvn_val))))
   | Bvcomp Bvule, Val_Bits n1, Val_Bits n2 =>
-    guard (n1.(bvn_n) = n2.(bvn_n));
+    guard (n1.(bvn_n) = n2.(bvn_n));;
     Some (Val_Bool (bool_decide (bv_unsigned n1.(bvn_val) ≤ bv_unsigned n2.(bvn_val))))
   | Bvcomp Bvsle, Val_Bits n1, Val_Bits n2 =>
-    guard (n1.(bvn_n) = n2.(bvn_n));
+    guard (n1.(bvn_n) = n2.(bvn_n));;
     Some (Val_Bool (bool_decide (bv_signed n1.(bvn_val) ≤ bv_signed n2.(bvn_val))))
   | Bvcomp Bvuge, Val_Bits n1, Val_Bits n2 =>
-    guard (n1.(bvn_n) = n2.(bvn_n));
+    guard (n1.(bvn_n) = n2.(bvn_n));;
     Some (Val_Bool (bool_decide (bv_unsigned n1.(bvn_val) >= bv_unsigned n2.(bvn_val))))
   | Bvcomp Bvsge, Val_Bits n1, Val_Bits n2 =>
-    guard (n1.(bvn_n) = n2.(bvn_n));
+    guard (n1.(bvn_n) = n2.(bvn_n));;
     Some (Val_Bool (bool_decide (bv_signed n1.(bvn_val) >= bv_signed n2.(bvn_val))))
   | Bvcomp Bvugt, Val_Bits n1, Val_Bits n2 =>
-    guard (n1.(bvn_n) = n2.(bvn_n));
+    guard (n1.(bvn_n) = n2.(bvn_n));;
     Some (Val_Bool (bool_decide (bv_unsigned n1.(bvn_val) > bv_unsigned n2.(bvn_val))))
   | Bvcomp Bvsgt, Val_Bits n1, Val_Bits n2 =>
-    guard (n1.(bvn_n) = n2.(bvn_n));
+    guard (n1.(bvn_n) = n2.(bvn_n));;
     Some (Val_Bool (bool_decide (bv_signed n1.(bvn_val) > bv_signed n2.(bvn_val))))
   | _, _, _ => None
   end.