Coq: update RISC-V patch

1 files changed, 20 insertions, 23 deletions

diff --git a/riscv/coq.patch b/riscv/coq.patch
index 9ee0fc71..149c60ff 100644
--- a/riscv/coq.patch
+++ b/riscv/coq.patch
@@ -1,14 +1,11 @@
---- riscv.v.plain	2018-09-06 11:57:47.900156894 +0100
-+++ riscv.v	2018-09-06 11:57:50.244172679 +0100
-@@ -8383,14 +8383,16 @@
+--- riscv.v.plain	2018-09-12 17:53:51.151611265 +0100
++++ riscv.v	2018-09-12 17:57:47.097406204 +0100
+@@ -8336,14 +8336,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) 
-+Hint Unfold PAGESIZE_BITS : sail.
-+Hint Unfold SV39_LEVEL_BITS : sail.
-+
 +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
@@ -19,8 +16,8 @@
 +          (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 (8 * 8)) =>
-@@ -8403,27 +8405,27 @@
+    (phys_mem_read Data (EXTZ 64 pte_addr) 8 false false false) >>= fun w__0 : MemoryOpResult (mword (8 * 8)) =>
+@@ -8356,27 +8355,27 @@
         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
@@ -39,7 +36,7 @@
 +              : M (PTW_Result) end)
             : M (PTW_Result)
          else
-           checkPTEPermission ac priv mxr do_sum pattr >>= fun w__3 : bool =>
+           (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
@@ -54,7 +51,7 @@
                        if ((neq_vec (and_vec (_get_SV39_PTE_PPNi pte) mask)
                               (EXTZ 44 (vec_of_bits [B0]  : mword 1)))) then
                          PTW_Failure
-@@ -8433,12 +8435,12 @@
+@@ -8386,12 +8385,12 @@
                            or_vec (_get_SV39_PTE_PPNi pte)
                              (and_vec (EXTZ 44 (_get_SV39_Vaddr_VPNi va)) mask) in
                          PTW_Success
@@ -69,16 +66,16 @@
             : PTW_Result))
          : M (PTW_Result)
      end)
-@@ -8564,7 +8566,7 @@
+@@ -8517,7 +8516,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 =>
+        (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) =>
-@@ -12339,138 +12341,144 @@
+@@ -12279,138 +12278,144 @@
     returnm (true
      : bool).
  
@@ -282,7 +279,7 @@
     | 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)
-@@ -12510,6 +12518,7 @@
+@@ -12450,6 +12455,7 @@
     | THREAD_START (arg0) => returnm ((execute_THREAD_START arg0)  : bool)
     | ILLEGAL (s) => (execute_ILLEGAL s)  : M (bool)
     | C_ILLEGAL (arg0) => (execute_C_ILLEGAL arg0)  : M (bool)
@@ -290,7 +287,7 @@
     end.
  
  Definition assembly_forwards (arg_ : ast) 
-@@ -12772,7 +12781,7 @@
+@@ -12712,7 +12718,7 @@
      | _ => exit tt  : M (string)
      end)
      : M (string).
@@ -299,7 +296,7 @@
  Definition assembly_backwards (arg_ : string) 
  : M (ast) :=
     let _stringappend_756_ := arg_ in
-@@ -27038,7 +27047,7 @@
+@@ -27199,7 +27205,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)}))).
@@ -308,16 +305,16 @@
  Definition encdec_forwards (arg_ : ast) 
  : M (mword 32) :=
     (match arg_ with
-@@ -29126,7 +29135,7 @@
-         : M ((bool * bool))
-     end)
-     : M ((bool * bool)).
+@@ -29293,7 +29299,7 @@
+     else returnm (tt  : unit)) >>
+    returnm (stepped
+     : bool).
 -
 +(*
  Definition loop '(tt : unit) 
  : M (unit) :=
     let insns_per_tick := plat_insns_per_tick tt in
-@@ -29173,7 +29182,7 @@
+@@ -29335,7 +29341,7 @@
         returnm (i, step_no))) >>= fun '(i, step_no) =>
     returnm (tt
      : unit).