update to Coq 8.18 and new version of deps

.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"

.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,18 +43,18 @@ 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
 
 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

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
 

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"

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 →

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.

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.