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

1 files changed, 431 insertions, 0 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 :=