Get RISC-V on Coq into reasonable state to show

- Fill in Coq builtins for more of the RISC-V prelude
- Update Barriers
- More general autocast
- Temporary sub_nat definition (until the backend handles nat better)
- Patch to bring results into a reasonable state
- Use Let rather than Definition for non-dependent top-level values

2 files changed, 459 insertions, 28 deletions

diff --git a/riscv/coq.patch b/riscv/coq.patch
new file mode 100644
index 00000000..cd7ad6b3
--- /dev/null
+++ b/riscv/coq.patch
@@ -0,0 +1,431 @@
+--- riscv.v.orig	2018-08-15 11:35:48.766557392 +0100
++++ riscv.v	2018-08-15 11:36:59.395492502 +0100
+@@ -7712,14 +7712,13 @@
+    returnm ((EXTZ 56 (shiftl (_get_Satp64_PPN satp64) PAGESIZE_BITS))
+     : mword 56).
+ 
+-Fixpoint walk39 (vaddr : mword 39) (ac : AccessType) (priv : Privilege) (mxr : bool) (do_sum : bool) (ptb : mword 56) '((existT _ level _) : {n : Z & ArithFact (n >=
+-  0)}) (global : bool) 
++Fixpoint walk39 (vaddr : mword 39) (ac : AccessType) (priv : Privilege) (mxr : bool) (do_sum : bool) (ptb : mword 56) (level : nat) (global : bool) 
+ : M (PTW_Result) :=
+    let va := Mk_SV39_Vaddr vaddr in
+    let pt_ofs : paddr39 :=
+      shiftl
+        (EXTZ 56
+-          (subrange_vec_dec (shiftr (_get_SV39_Vaddr_VPNi va) (Z.mul level SV39_LEVEL_BITS))
++          (subrange_vec_dec (shiftr (_get_SV39_Vaddr_VPNi va) (Z.mul (Z.of_nat level) SV39_LEVEL_BITS))
+              (projT1 (sub_range (build_ex SV39_LEVEL_BITS) (build_ex 1))) 0)) PTE39_LOG_SIZE in
+    let pte_addr := add_vec ptb pt_ofs in
+    phys_mem_read Data (EXTZ 64 pte_addr) 8 false false false >>= fun w__0 : MemoryOpResult (mword 64) =>
+@@ -7732,26 +7731,26 @@
+        let is_global := orb global (eq_vec (_get_PTE_Bits_G pattr) ((bool_to_bits true)  : mword 1)) in
+        (if ((isInvalidPTE pbits)) then returnm ((PTW_Failure PTW_Invalid_PTE)  : PTW_Result)
+         else if ((isPTEPtr pbits)) then
+-          (if sumbool_of_bool ((Z.eqb level 0)) then
++          (match level with | O =>
+              returnm ((PTW_Failure PTW_Invalid_PTE)
+               : PTW_Result)
+-           else
++           | S level' =>
+              (walk39 vaddr ac priv mxr do_sum
+                 (EXTZ 56 (shiftl (_get_SV39_PTE_PPNi pte) PAGESIZE_BITS))
+-                (build_ex (projT1 (sub_range (build_ex level) (build_ex 1)))) is_global)
+-              : M (PTW_Result))
++                level' is_global)
++              : M (PTW_Result) end)
+            : M (PTW_Result)
+         else
+           checkPTEPermission ac priv mxr do_sum pattr >>= fun w__3 : bool =>
+           returnm ((if ((negb w__3)) then PTW_Failure PTW_No_Permission
+-                    else if sumbool_of_bool ((Z.gtb level 0)) then
++                    else if sumbool_of_bool (Nat.ltb O level) then
+                       let mask :=
+                         sub_vec_int
+                           (shiftl
+                              (xor_vec (_get_SV39_PTE_PPNi pte)
+                                 (xor_vec (_get_SV39_PTE_PPNi pte)
+                                    (EXTZ 44 (vec_of_bits [B1]  : mword 1))))
+-                             (Z.mul level SV39_LEVEL_BITS)) 1 in
++                             (Z.mul (Z.of_nat level) SV39_LEVEL_BITS)) 1 in
+                       if ((neq_vec (and_vec (_get_SV39_PTE_PPNi pte) mask)
+                              (EXTZ 44 (vec_of_bits [B0]  : mword 1)))) then
+                         PTW_Failure PTW_Misaligned
+@@ -7760,15 +7759,18 @@
+                           or_vec (_get_SV39_PTE_PPNi pte)
+                             (and_vec (EXTZ 44 (_get_SV39_Vaddr_VPNi va)) mask) in
+                         PTW_Success (concat_vec ppn (_get_SV39_Vaddr_PgOfs va),pte,pte_addr,build_ex
+-                        level,is_global)
++                        (Z.of_nat level),is_global)
+                     else
+                       PTW_Success (concat_vec (_get_SV39_PTE_PPNi pte) (_get_SV39_Vaddr_PgOfs va),pte,pte_addr,build_ex
+-                      level,is_global))
++                      (Z.of_nat level),is_global))
+            : PTW_Result))
+         : M (PTW_Result)
+     end)
+     : M (PTW_Result).
+ 
++Hint Unfold PAGESIZE_BITS : sail.
++Hint Unfold SV39_LEVEL_BITS : sail.
++
+ Definition make_TLB39_Entry (asid : mword 16) (global : bool) (vAddr : mword 39) (pAddr : mword 56) (pte : SV39_PTE) '((existT _ level _) : {n : Z & ArithFact (n >=
+   0)}) (pteAddr : mword 56) 
+ : M (TLB39_Entry) :=
+@@ -7884,7 +7886,7 @@
+         : M (TR39_Result)
+     | None =>
+        curPTB39 tt >>= fun w__6 : mword 56 =>
+-       walk39 vAddr ac priv mxr do_sum w__6 (build_ex level) false >>= fun w__7 : PTW_Result =>
++       walk39 vAddr ac priv mxr do_sum w__6 (Z.to_nat level) false >>= fun w__7 : PTW_Result =>
+        (match w__7 with
+         | PTW_Failure (f) => returnm ((TR39_Failure f)  : TR39_Result)
+         | PTW_Success (pAddr,pte,pteAddr,(existT _ level _),global) =>
+@@ -7961,7 +7963,7 @@
+     | Sbare => returnm ((TR_Address vAddr)  : TR_Result)
+     | SV39 =>
+        translate39 (subrange_vec_dec vAddr 38 0) ac effPriv mxr do_sum
+-         (build_ex (projT1 (sub_range (build_ex SV39_LEVELS) (build_ex 1)))) >>= fun w__7 : TR39_Result =>
++         (build_ex ( (Z.sub ( SV39_LEVELS) ( 1)))) >>= fun w__7 : TR39_Result =>
+        returnm ((match w__7 with
+                  | TR39_Address (pa) => TR_Address (EXTZ 64 pa)
+                  | TR39_Failure (f) => TR_Failure (translationException ac f)
+@@ -10867,11 +10869,11 @@
+           (match width with
+            | WORD =>
+               mem_read addr 4 aq rl true >>= fun w__2 : MemoryOpResult (mword 32) =>
+-              (process_loadres rd vaddr w__2 false)
++              (process_loadres (n := 4) rd vaddr w__2 false)
+                : M (bool)
+            | DOUBLE =>
+               mem_read addr 8 aq rl true >>= fun w__4 : MemoryOpResult (mword 64) =>
+-              (process_loadres rd vaddr w__4 false)
++              (process_loadres (n := 8) rd vaddr w__4 false)
+                : M (bool)
+            | _ => (internal_error "LOADRES expected WORD or DOUBLE")  : M (bool)
+            end)
+@@ -10894,19 +10896,19 @@
+           (match width with
+            | BYTE =>
+               mem_read addr 1 aq rl false >>= fun w__3 : MemoryOpResult (mword 8) =>
+-              (process_load rd vaddr w__3 is_unsigned)
++              (process_load (n := 1) rd vaddr w__3 is_unsigned)
+                : M (bool)
+            | HALF =>
+               mem_read addr 2 aq rl false >>= fun w__5 : MemoryOpResult (mword 16) =>
+-              (process_load rd vaddr w__5 is_unsigned)
++              (process_load (n := 2) rd vaddr w__5 is_unsigned)
+                : M (bool)
+            | WORD =>
+               mem_read addr 4 aq rl false >>= fun w__7 : MemoryOpResult (mword 32) =>
+-              (process_load rd vaddr w__7 is_unsigned)
++              (process_load (n := 4) rd vaddr w__7 is_unsigned)
+                : M (bool)
+            | DOUBLE =>
+               mem_read addr 8 aq rl false >>= fun w__9 : MemoryOpResult (mword 64) =>
+-              (process_load rd vaddr w__9 is_unsigned)
++              (process_load (n := 8) rd vaddr w__9 is_unsigned)
+                : M (bool)
+            end)
+            : M (bool)
+@@ -11023,7 +11025,7 @@
+      if sumbool_of_bool ((andb s
+                             (Z.gtb q (projT1 (sub_range (build_ex (projT1 (pow2 31))) (build_ex 1))))))
+      then
+-       projT1 (sub_range (build_ex 0) ((ex_int (pow 2 31))  : {n : Z & ArithFact (True)}))
++        (Z.sub ( 0) ((pow 2 31)))
+      else q in
+    wX (projT1 ((regbits_to_regno rd)  : {n : Z & ArithFact (0 <= n /\ (n + 1) <= 32)}))
+      (EXTS 64 (to_bits 32 q')) >>
+@@ -11127,11 +11129,11 @@
+            match width with
+            | WORD =>
+               mem_read addr 4 aq (andb aq rl) true >>= fun w__4 : MemoryOpResult (mword 32) =>
+-              returnm ((extend_value false w__4)
++              returnm ((extend_value (n := 4) false w__4)
+                : MemoryOpResult xlenbits)
+            | DOUBLE =>
+               mem_read addr 8 aq (andb aq rl) true >>= fun w__5 : MemoryOpResult (mword 64) =>
+-              returnm ((extend_value false w__5)
++              returnm ((extend_value (n := 8) false w__5)
+                : MemoryOpResult xlenbits)
+            | _ => (internal_error "AMO expected WORD or DOUBLE")  : M (MemoryOpResult xlenbits)
+            end >>= fun rval : MemoryOpResult xlenbits =>
+@@ -11193,134 +11195,140 @@
+    returnm (true
+     : bool).
+ 
+-Fixpoint execute (merge_var : ast) 
+-: M (bool) :=
+-   match merge_var with
++Definition expand_ast (i : ast) : ast :=
++match i with
+    | C_ADDI4SPN (rdc,nzimm) =>
+       let imm : bits 12 :=
+         concat_vec (vec_of_bits [B0;B0]  : mword 2)
+           (concat_vec nzimm (vec_of_bits [B0;B0]  : mword 2)) in
+       let rd := creg2reg_bits rdc in
+-      (execute (ITYPE (imm,sp,rd,RISCV_ADDI)))
+-       : M (bool)
++      ( (ITYPE (imm,sp,rd,RISCV_ADDI)))
++       
+    | C_LW (uimm,rsc,rdc) =>
+       let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0]  : mword 2)) in
+       let rd := creg2reg_bits rdc in
+       let rs := creg2reg_bits rsc in
+-      (execute (LOAD (imm,rs,rd,false,WORD,false,false)))
+-       : M (bool)
++      ( (LOAD (imm,rs,rd,false,WORD,false,false)))
++       
+    | C_LD (uimm,rsc,rdc) =>
+       let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0;B0]  : mword 3)) in
+       let rd := creg2reg_bits rdc in
+       let rs := creg2reg_bits rsc in
+-      (execute (LOAD (imm,rs,rd,false,DOUBLE,false,false)))
+-       : M (bool)
++      ( (LOAD (imm,rs,rd,false,DOUBLE,false,false)))
++       
+    | C_SW (uimm,rsc1,rsc2) =>
+       let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0]  : mword 2)) in
+       let rs1 := creg2reg_bits rsc1 in
+       let rs2 := creg2reg_bits rsc2 in
+-      (execute (STORE (imm,rs2,rs1,WORD,false,false)))
+-       : M (bool)
++      ( (STORE (imm,rs2,rs1,WORD,false,false)))
++       
+    | C_SD (uimm,rsc1,rsc2) =>
+       let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0;B0]  : mword 3)) in
+       let rs1 := creg2reg_bits rsc1 in
+       let rs2 := creg2reg_bits rsc2 in
+-      (execute (STORE (imm,rs2,rs1,DOUBLE,false,false)))
+-       : M (bool)
++      ( (STORE (imm,rs2,rs1,DOUBLE,false,false)))
++       
+    | C_ADDI (nzi,rsd) =>
+       let imm : bits 12 := EXTS 12 nzi in
+-      (execute (ITYPE (imm,rsd,rsd,RISCV_ADDI)))
+-       : M (bool)
++      ( (ITYPE (imm,rsd,rsd,RISCV_ADDI)))
++       
+    | C_JAL (imm) =>
+-      (execute (RISCV_JAL (EXTS 21 (concat_vec imm (vec_of_bits [B0]  : mword 1)),ra)))  : M (bool)
++      ( (RISCV_JAL (EXTS 21 (concat_vec imm (vec_of_bits [B0]  : mword 1)),ra)))  
+    | C_LI (imm,rd) =>
+       let imm : bits 12 := EXTS 12 imm in
+-      (execute (ITYPE (imm,zreg,rd,RISCV_ADDI)))
+-       : M (bool)
++      ( (ITYPE (imm,zreg,rd,RISCV_ADDI)))
++       
+    | C_ADDI16SP (imm) =>
+       let imm : bits 12 := EXTS 12 (concat_vec imm (vec_of_bits [B0;B0;B0;B0]  : mword 4)) in
+-      (execute (ITYPE (imm,sp,sp,RISCV_ADDI)))
+-       : M (bool)
++      ( (ITYPE (imm,sp,sp,RISCV_ADDI)))
++       
+    | C_LUI (imm,rd) =>
+       let res : bits 20 := EXTS 20 imm in
+-      (execute (UTYPE (res,rd,RISCV_LUI)))
+-       : M (bool)
++      ( (UTYPE (res,rd,RISCV_LUI)))
++       
+    | C_SRLI (shamt,rsd) =>
+       let rsd := creg2reg_bits rsd in
+-      (execute (SHIFTIOP (shamt,rsd,rsd,RISCV_SRLI)))
+-       : M (bool)
++      ( (SHIFTIOP (shamt,rsd,rsd,RISCV_SRLI)))
++       
+    | C_SRAI (shamt,rsd) =>
+       let rsd := creg2reg_bits rsd in
+-      (execute (SHIFTIOP (shamt,rsd,rsd,RISCV_SRAI)))
+-       : M (bool)
++      ( (SHIFTIOP (shamt,rsd,rsd,RISCV_SRAI)))
++       
+    | C_ANDI (imm,rsd) =>
+       let rsd := creg2reg_bits rsd in
+-      (execute (ITYPE (EXTS 12 imm,rsd,rsd,RISCV_ANDI)))
+-       : M (bool)
++      ( (ITYPE (EXTS 12 imm,rsd,rsd,RISCV_ANDI)))
++       
+    | C_SUB (rsd,rs2) =>
+       let rsd := creg2reg_bits rsd in
+       let rs2 := creg2reg_bits rs2 in
+-      (execute (RTYPE (rs2,rsd,rsd,RISCV_SUB)))
+-       : M (bool)
++      ( (RTYPE (rs2,rsd,rsd,RISCV_SUB)))
++       
+    | C_XOR (rsd,rs2) =>
+       let rsd := creg2reg_bits rsd in
+       let rs2 := creg2reg_bits rs2 in
+-      (execute (RTYPE (rs2,rsd,rsd,RISCV_XOR)))
+-       : M (bool)
++      ( (RTYPE (rs2,rsd,rsd,RISCV_XOR)))
++       
+    | C_OR (rsd,rs2) =>
+       let rsd := creg2reg_bits rsd in
+       let rs2 := creg2reg_bits rs2 in
+-      (execute (RTYPE (rs2,rsd,rsd,RISCV_OR)))
+-       : M (bool)
++      ( (RTYPE (rs2,rsd,rsd,RISCV_OR)))
++       
+    | C_AND (rsd,rs2) =>
+       let rsd := creg2reg_bits rsd in
+       let rs2 := creg2reg_bits rs2 in
+-      (execute (RTYPE (rs2,rsd,rsd,RISCV_AND)))
+-       : M (bool)
++      ( (RTYPE (rs2,rsd,rsd,RISCV_AND)))
++       
+    | C_SUBW (rsd,rs2) =>
+       let rsd := creg2reg_bits rsd in
+       let rs2 := creg2reg_bits rs2 in
+-      (execute (RTYPEW (rs2,rsd,rsd,RISCV_SUBW)))
+-       : M (bool)
++      ( (RTYPEW (rs2,rsd,rsd,RISCV_SUBW)))
++       
+    | C_ADDW (rsd,rs2) =>
+       let rsd := creg2reg_bits rsd in
+       let rs2 := creg2reg_bits rs2 in
+-      (execute (RTYPEW (rs2,rsd,rsd,RISCV_ADDW)))
+-       : M (bool)
++      ( (RTYPEW (rs2,rsd,rsd,RISCV_ADDW)))
++       
+    | C_J (imm) =>
+-      (execute (RISCV_JAL (EXTS 21 (concat_vec imm (vec_of_bits [B0]  : mword 1)),zreg)))
+-       : M (bool)
++      ( (RISCV_JAL (EXTS 21 (concat_vec imm (vec_of_bits [B0]  : mword 1)),zreg)))
++       
+    | C_BEQZ (imm,rs) =>
+-      (execute
++      (
+          (BTYPE (EXTS 13 (concat_vec imm (vec_of_bits [B0]  : mword 1)),zreg,creg2reg_bits rs,RISCV_BEQ)))
+-       : M (bool)
++       
+    | C_BNEZ (imm,rs) =>
+-      (execute
++      (
+          (BTYPE (EXTS 13 (concat_vec imm (vec_of_bits [B0]  : mword 1)),zreg,creg2reg_bits rs,RISCV_BNE)))
+-       : M (bool)
+-   | C_SLLI (shamt,rsd) => (execute (SHIFTIOP (shamt,rsd,rsd,RISCV_SLLI)))  : M (bool)
++       
++   | C_SLLI (shamt,rsd) => ( (SHIFTIOP (shamt,rsd,rsd,RISCV_SLLI)))  
+    | C_LWSP (uimm,rd) =>
+       let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0]  : mword 2)) in
+-      (execute (LOAD (imm,sp,rd,false,WORD,false,false)))
+-       : M (bool)
++      ( (LOAD (imm,sp,rd,false,WORD,false,false)))
++       
+    | C_LDSP (uimm,rd) =>
+       let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0;B0]  : mword 3)) in
+-      (execute (LOAD (imm,sp,rd,false,DOUBLE,false,false)))
+-       : M (bool)
++      ( (LOAD (imm,sp,rd,false,DOUBLE,false,false)))
++       
+    | C_SWSP (uimm,rs2) =>
+       let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0]  : mword 2)) in
+-      (execute (STORE (imm,rs2,sp,WORD,false,false)))
+-       : M (bool)
++      ( (STORE (imm,rs2,sp,WORD,false,false)))
++       
+    | C_SDSP (uimm,rs2) =>
+       let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0;B0]  : mword 3)) in
+-      (execute (STORE (imm,rs2,sp,DOUBLE,false,false)))
+-       : M (bool)
++      ( (STORE (imm,rs2,sp,DOUBLE,false,false)))
++       
+    | C_JR (rs1) =>
+-      (execute (RISCV_JALR (EXTZ 12 (vec_of_bits [B0]  : mword 1),rs1,zreg)))  : M (bool)
++      ( (RISCV_JALR (EXTZ 12 (vec_of_bits [B0]  : mword 1),rs1,zreg)))  
+    | C_JALR (rs1) =>
+-      (execute (RISCV_JALR (EXTZ 12 (vec_of_bits [B0]  : mword 1),rs1,ra)))  : M (bool)
+-   | C_MV (rd,rs2) => (execute (RTYPE (rs2,zreg,rd,RISCV_ADD)))  : M (bool)
+-   | C_ADD (rsd,rs2) => (execute (RTYPE (rs2,rsd,rsd,RISCV_ADD)))  : M (bool)
++      ( (RISCV_JALR (EXTZ 12 (vec_of_bits [B0]  : mword 1),rs1,ra)))  
++   | C_MV (rd,rs2) => ( (RTYPE (rs2,zreg,rd,RISCV_ADD)))  
++   | C_ADD (rsd,rs2) => ( (RTYPE (rs2,rsd,rsd,RISCV_ADD)))  
++| _ => i
++end.
++
++Fixpoint execute (merge_var : ast) 
++: M (bool) :=
++let merge_var := expand_ast merge_var in
++   match merge_var with
+    | UTYPE (imm,rd,op) => (execute_UTYPE imm rd op)  : M (bool)
+    | RISCV_JAL (imm,rd) => (execute_RISCV_JAL imm rd)  : M (bool)
+    | RISCV_JALR (imm,rs1,rd) => (execute_RISCV_JALR imm rs1 rd)  : M (bool)
+@@ -11360,6 +11368,7 @@
+    | THREAD_START (g__29) => returnm ((execute_THREAD_START g__29)  : bool)
+    | ILLEGAL (s) => (execute_ILLEGAL s)  : M (bool)
+    | C_ILLEGAL (g__30) => (execute_C_ILLEGAL g__30)  : M (bool)
++| _ => Fail "Unexpanded instruction"
+    end.
+ 
+ Definition assembly_forwards (arg_ : ast) 
+@@ -11622,7 +11631,7 @@
+     | _ => exit tt  : M (string)
+     end)
+     : M (string).
+-
++(*
+ Definition assembly_backwards (arg_ : string) 
+ : M (ast) :=
+    let _stringappend_1112_ := arg_ in
+@@ -29689,7 +29698,7 @@
+           : M (option ((ast * {n : Z & ArithFact (n >= 0)}))))
+        : M (option ((ast * {n : Z & ArithFact (n >= 0)}))))
+     : M (option ((ast * {n : Z & ArithFact (n >= 0)}))).
+-
++*)
+ Definition encdec_forwards (arg_ : ast) 
+ : M (mword 32) :=
+    (match arg_ with
+@@ -31899,7 +31908,7 @@
+         : M ((bool * bool))
+     end)
+     : M ((bool * bool)).
+-
++(*
+ Definition loop '(tt : unit) 
+ : M (unit) :=
+    let insns_per_tick := plat_insns_per_tick tt in
+@@ -31938,7 +31947,7 @@
+        returnm (i, step_no))) >>= fun '(i, step_no) =>
+    returnm (tt
+     : unit).
+-
++*)
+ Definition read_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 11)} 
+ : read_kind :=
+    let p0_ := arg_ in
+@@ -32029,7 +32038,7 @@
+    else if sumbool_of_bool ((Z.eqb p0_ 20)) then Barrier_RISCV_w_r
+    else if sumbool_of_bool ((Z.eqb p0_ 21)) then Barrier_RISCV_i
+    else Barrier_x86_MFENCE.
+-
++(*
+ Definition num_of_barrier_kind (arg_ : barrier_kind) 
+ : {e : Z & ArithFact (0 <= e /\ e <= 22)} :=
+    match arg_ with
+@@ -32057,7 +32066,7 @@
+    | Barrier_RISCV_i => build_ex 21
+    | Barrier_x86_MFENCE => build_ex 22
+    end.
+-
++*)
+ Definition trans_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 2)} 
+ : trans_kind :=
+    let p0_ := arg_ in
+@@ -32078,6 +32087,7 @@
+                  "x10";"x9";"x8";"x7";"x6";"x5";"x4";"x3";"x2";"x1";"x0"].
+ Let CIA_fp := RFull "CIA".
+ Let NIA_fp := RFull "NIA".
++(*
+ Definition initial_analysis (instr : ast) 
+ : M ((list regfp * list regfp * list regfp * list niafp * diafp * instruction_kind)) :=
+    let iR := []  : regfps in
+@@ -32602,7 +32612,7 @@
+    end >>= fun '(Nias, aR, iR, ik, oR) =>
+    returnm ((iR, oR, aR, Nias, Dia, ik)
+     : (list regfp * list regfp * list regfp * list niafp * diafp * instruction_kind)).
+-
++*)
+ Let initial_regstate : regstate :=
+ {| tlb39 := None; 
+    htif_exit_code :=
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 8636bda6..d5c133fc 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -70,12 +70,12 @@ val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -
 val lt_atom = {coq: "Z.ltb", _: "lt"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 val gt_atom = {coq: "Z.gtb", _: "gt"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 
-val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
-val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit"} : (bit, bit) -> bool
+val eq_int = {ocaml: "eq_int", lem: "eq", coq: "Z.eqb"} : (int, int) -> bool
+val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit", coq: "eq_bit"} : (bit, bit) -> bool
 
-val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec", coq: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
 
-val eq_string = {ocaml: "eq_string", lem: "eq"} : (string, string) -> bool
+val eq_string = {ocaml: "eq_string", lem: "eq", coq: "generic_eq"} : (string, string) -> bool
 val string_startswith = "string_startswith" : (string, string) -> bool
 val string_drop = "string_drop" : (string, nat) -> string
 val string_length = "string_length" : string -> nat
@@ -87,11 +87,11 @@ val maybe_int_of_string = "maybe_int_of_string" : string -> option(int)
 
 val eq_real = {ocaml: "eq_real", lem: "eq"} : (real, real) -> bool
 
-val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq"} : forall ('a : Type). ('a, 'a) -> bool
+val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", coq: "generic_eq"} : forall ('a : Type). ('a, 'a) -> bool
 
-val bitvector_length = {ocaml: "length", lem: "length"} : forall 'n. bits('n) -> atom('n)
-val vector_length = {ocaml: "length", lem: "length_list"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
-val list_length = {ocaml: "length", lem: "length_list"} : forall ('a : Type). list('a) -> int
+val bitvector_length = {ocaml: "length", lem: "length", coq: "length_mword"} : forall 'n. bits('n) -> atom('n)
+val vector_length = {ocaml: "length", lem: "length_list", coq: "vec_length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
+val list_length = {ocaml: "length", lem: "length_list", coq: "length_list"} : forall ('a : Type). list('a) -> int
 
 overload length = {bitvector_length, vector_length, list_length}
 
@@ -101,32 +101,32 @@ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
 
 overload operator == = {eq_atom, eq_int, eq_bit, eq_vec, eq_string, eq_real, eq_anything}
 
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
   (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
 
-val bitvector_access = {ocaml: "access", lem: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n.
+val bitvector_access = {ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n.
   (bits('n), atom('m)) -> bit
 
-val any_vector_access = {ocaml: "access", lem: "access_list_dec"} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n.
+val any_vector_access = {ocaml: "access", lem: "access_list_dec", coq: "vec_access_dec"} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n.
   (vector('n, dec, 'a), atom('m)) -> 'a
 
 overload vector_access = {bitvector_access, any_vector_access}
 
-val bitvector_update = {ocaml: "update", lem: "update_vec_dec"} : forall 'n.
+val bitvector_update = {ocaml: "update", lem: "update_vec_dec", coq: "update_vec_dec"} : forall 'n.
   (bits('n), int, bit) -> bits('n)
 
-val any_vector_update = {ocaml: "update", lem: "update_list_dec"} : forall 'n ('a : Type).
+val any_vector_update = {ocaml: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type).
   (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
 
 overload vector_update = {bitvector_update, any_vector_update}
 
-val update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+val update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
   (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
 val vcons = {lem: "cons_vec"} : forall ('n : Int) ('a : Type).
   ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a)
 
-val bitvector_concat = {ocaml: "append", lem: "concat_vec"} : forall ('n : Int) ('m : Int).
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 
 val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type).
@@ -152,7 +152,7 @@ val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
 
 function neq_vec (x, y) = not_bool(eq_vec(x, y))
 
-val neq_anything = {lem: "neq"} : forall ('a : Type). ('a, 'a) -> bool
+val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
 
 function neq_anything (x, y) = not_bool(x == y)
 
@@ -162,7 +162,7 @@ val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
 
 val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val and_vec = {lem: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val and_vec = {lem: "and_vec", coq: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 function and_vec (xs, ys) = builtin_and_vec(xs, ys)
 
@@ -172,15 +172,15 @@ val or_bool = {coq: "orb", _:"or_bool"} : (bool, bool) -> bool
 
 val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val or_vec = {lem: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val or_vec = {lem: "or_vec", coq: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 function or_vec (xs, ys) = builtin_or_vec(xs, ys)
 
 overload operator | = {or_bool, or_vec}
 
-val unsigned = {ocaml: "uint", lem: "uint"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
+val unsigned = {ocaml: "uint", lem: "uint", coq: "uint"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
 
-val signed = {ocaml: "sint", lem: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
+val signed = {ocaml: "sint", lem: "sint", coq: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
 val hex_slice = "hex_slice" : forall 'n 'm, 'n >= 'm. (string, atom('n), atom('m)) -> bits('n - 'm)
 
@@ -221,7 +221,7 @@ val print = "print_endline" : string -> unit
 
 val putchar = "putchar" : forall ('a : Type). 'a -> unit
 
-val concat_str = {ocaml: "concat_str", lem: "stringAppend"} : (string, string) -> string
+val concat_str = {ocaml: "concat_str", lem: "stringAppend", coq: "String.append"} : (string, string) -> string
 
 val string_of_int = {ocaml: "string_of_int", lem: "stringFromInteger"} : int -> string
 
@@ -233,7 +233,7 @@ val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
 
 val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val int_power = {ocaml: "int_power", lem: "pow"} : (int, int) -> int
+val int_power = {ocaml: "int_power", lem: "pow", coq: "pow"} : (int, int) -> int
 
 val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> real
 
@@ -257,7 +257,7 @@ val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : fora
 
 val sub_int = {ocaml: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int
 val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)",
-               lem: "integerMinus"}
+               lem: "integerMinus", coq: "sub_nat"}
             : (nat, nat) -> nat
 
 val "sub_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -344,11 +344,11 @@ val shr_int = "shr_int" : (int, int) -> int
 
 val min_nat = {ocaml: "min_int", lem: "min"} : (nat, nat) -> nat
 
-val min_int = {ocaml: "min_int", lem: "min"} : (int, int) -> int
+val min_int = {ocaml: "min_int", lem: "min", coq: "Z.min"} : (int, int) -> int
 
 val max_nat = {ocaml: "max_int", lem: "max"} : (nat, nat) -> nat
 
-val max_int = {ocaml: "max_int", lem: "max"} : (int, int) -> int
+val max_int = {ocaml: "max_int", lem: "max", coq: "Z.max"} : (int, int) -> int
 
 overload min = {min_nat, min_int}
 
@@ -445,8 +445,8 @@ infix 4 <_u
 infix 4 >=_u
 infix 4 <=_u
 
-val operator <_s  : forall 'n. (bits('n), bits('n)) -> bool
-val operator >=_s : forall 'n. (bits('n), bits('n)) -> bool
+val operator <_s  : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
+val operator >=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
 val operator <_u  : forall 'n. (bits('n), bits('n)) -> bool
 val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool
 val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool
@@ -479,7 +479,7 @@ function vector64 n = __raw_GetSlice_int(64, n, 0)
 val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l)
 function to_bits (l, n) = __raw_GetSlice_int(l, n, 0)
 
-val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o.
+val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
   (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
 val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o.