Coq: solver should split earlier

otherwise some other parts don't work properly.
Also update RISC-V patch.

2 files changed, 28 insertions, 28 deletions

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 6b75bd47..7a9d16be 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1039,14 +1039,14 @@ Ltac prepare_for_solver :=
  clear_irrelevant_defns;
  clear_non_Z_defns;
  autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *)
+ split_cases;
  extract_properties;
  repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
  unwrap_ArithFacts;
  unfold_In;
  unbool_comparisons;
  reduce_list_lengths;
- reduce_pow;
- split_cases.
+ reduce_pow.
 
 Lemma trivial_range {x : Z} : ArithFact (x <= x /\ x <= x).
 constructor.
diff --git a/riscv/coq.patch b/riscv/coq.patch
index f6f2b9d3..6a90205e 100644
--- a/riscv/coq.patch
+++ b/riscv/coq.patch
@@ -1,6 +1,6 @@
---- riscv.v.orig	2018-09-03 12:15:42.629947208 +0100
-+++ riscv.v	2018-09-03 12:16:05.170089474 +0100
-@@ -8405,14 +8405,16 @@
+--- riscv.v.plain	2018-09-03 18:49:16.824340711 +0100
++++ riscv.v	2018-09-03 18:49:31.420452869 +0100
+@@ -8420,14 +8420,16 @@
     returnm ((EXTZ 56 (shiftl (_get_Satp64_PPN satp64) PAGESIZE_BITS))
      : mword 56).
  
@@ -20,7 +20,7 @@
               (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)) =>
-@@ -8425,27 +8427,27 @@
+@@ -8440,27 +8442,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
@@ -54,7 +54,7 @@
                        if ((neq_vec (and_vec (_get_SV39_PTE_PPNi pte) mask)
                               (EXTZ 44 (vec_of_bits [B0]  : mword 1)))) then
                          PTW_Failure
-@@ -8455,12 +8457,12 @@
+@@ -8470,12 +8472,12 @@
                            or_vec (_get_SV39_PTE_PPNi pte)
                              (and_vec (EXTZ 44 (_get_SV39_Vaddr_VPNi va)) mask) in
                          PTW_Success
@@ -69,7 +69,7 @@
             : PTW_Result))
          : M (PTW_Result)
      end)
-@@ -8586,7 +8588,7 @@
+@@ -8601,7 +8603,7 @@
          : M (TR39_Result)
      | None =>
         curPTB39 tt >>= fun w__6 : mword 56 =>
@@ -78,7 +78,7 @@
         (match w__7 with
          | PTW_Failure (f) => returnm ((TR39_Failure (f))  : TR39_Result )
          | PTW_Success (pAddr,pte,pteAddr,(existT _ level _),global) =>
-@@ -8666,7 +8668,7 @@
+@@ -8681,7 +8683,7 @@
      | Sbare => returnm ((TR_Address (vAddr))  : TR_Result )
      | SV39 =>
         translate39 (subrange_vec_dec vAddr 38 0) ac effPriv mxr do_sum
@@ -87,7 +87,7 @@
         returnm ((match w__7 with
                   | TR39_Address (pa) => TR_Address (EXTZ 64 pa)
                   | TR39_Failure (f) => TR_Failure (translationException ac f)
-@@ -11507,7 +11509,7 @@
+@@ -11522,7 +11524,7 @@
            (tt))
     else None.
  
@@ -96,7 +96,7 @@
  : M (bool) :=
     read_reg cur_privilege_ref >>= fun w__0 : Privilege =>
     (match w__0 with
-@@ -11539,7 +11541,7 @@
+@@ -11554,7 +11556,7 @@
     returnm (true
      : bool).
  
@@ -105,7 +105,7 @@
  
  Fixpoint execute_STORECON (aq : bool) (rl : bool) (rs2 : mword 5) (rs1 : mword 5) (width : word_width) (rd : mword 5) 
  : M (bool) :=
-@@ -11668,9 +11670,9 @@
+@@ -11683,9 +11685,9 @@
         : M (bool))
      : M (bool).
  
@@ -117,7 +117,7 @@
  : M (bool) :=
     read_reg cur_privilege_ref >>= fun w__0 : Privilege =>
     match w__0 with
-@@ -11914,7 +11916,7 @@
+@@ -11929,7 +11931,7 @@
     returnm (true
      : bool).
  
@@ -126,7 +126,7 @@
  
  Fixpoint execute_MULW (rs2 : mword 5) (rs1 : mword 5) (rd : mword 5) 
  : M (bool) :=
-@@ -11956,7 +11958,7 @@
+@@ -11971,7 +11973,7 @@
     returnm (true
      : bool).
  
@@ -135,7 +135,7 @@
  : M (bool) :=
     read_reg cur_privilege_ref >>= fun w__0 : Privilege =>
     (if ((eq_vec ((privLevel_to_bits w__0)  : mword 2) ((privLevel_to_bits Machine)  : mword 2)))
-@@ -12067,7 +12069,7 @@
+@@ -12082,7 +12084,7 @@
  
  Fixpoint execute_ILLEGAL (s : mword 32)  : M (bool) := handle_illegal tt >> returnm (false  : bool).
  
@@ -144,7 +144,7 @@
  
  Fixpoint execute_FENCE (pred : mword 4) (succ : mword 4) 
  : M (bool) :=
-@@ -12123,7 +12125,7 @@
+@@ -12138,7 +12140,7 @@
     returnm (true
      : bool).
  
@@ -153,7 +153,7 @@
  : M (bool) :=
     read_reg cur_privilege_ref >>= fun w__0 : Privilege =>
     let t : sync_exception :=
-@@ -12139,7 +12141,7 @@
+@@ -12154,7 +12156,7 @@
     handle_exception w__1 (CTL_TRAP (t)) w__2 >>= fun w__3 : mword 64 =>
     write_reg nextPC_ref w__3 >> returnm (false  : bool).
  
@@ -162,7 +162,7 @@
  : M (bool) :=
     (read_reg PC_ref  : M (mword 64)) >>= fun w__0 : xlenbits =>
     handle_mem_exception w__0 E_Breakpoint >> returnm (false  : bool).
-@@ -12161,8 +12163,8 @@
+@@ -12176,8 +12178,8 @@
       if sumbool_of_bool ((andb s
                              (Z.gtb q (projT1 (sub_range (build_ex (projT1 (pow2 31))) (build_ex 1))))))
       then
@@ -173,7 +173,7 @@
                    : {n : Z & ArithFact (True)}))))
       else q in
     wX
-@@ -12189,7 +12191,7 @@
+@@ -12204,7 +12206,7 @@
     returnm (true
      : bool).
  
@@ -182,7 +182,7 @@
  
  Fixpoint execute_C_ADDIW (imm : mword 6) (rsd : mword 5) 
  : M (bool) :=
-@@ -12355,138 +12357,144 @@
+@@ -12370,138 +12372,144 @@
     returnm (true
      : bool).
  
@@ -386,7 +386,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)
-@@ -12526,6 +12534,7 @@
+@@ -12541,6 +12549,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)
@@ -394,7 +394,7 @@
     end.
  
  Definition assembly_forwards (arg_ : ast) 
-@@ -12788,7 +12797,7 @@
+@@ -12803,7 +12812,7 @@
      | _ => exit tt  : M (string)
      end)
      : M (string).
@@ -403,7 +403,7 @@
  Definition assembly_backwards (arg_ : string) 
  : M (ast) :=
     let _stringappend_756_ := arg_ in
-@@ -27054,7 +27063,7 @@
+@@ -27069,7 +27078,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)}))).
@@ -412,7 +412,7 @@
  Definition encdec_forwards (arg_ : ast) 
  : M (mword 32) :=
     (match arg_ with
-@@ -29142,7 +29151,7 @@
+@@ -29157,7 +29166,7 @@
          : M ((bool * bool))
      end)
      : M ((bool * bool)).
@@ -421,7 +421,7 @@
  Definition loop '(tt : unit) 
  : M (unit) :=
     let insns_per_tick := plat_insns_per_tick tt in
-@@ -29189,7 +29198,7 @@
+@@ -29204,7 +29213,7 @@
         returnm (i, step_no))) >>= fun '(i, step_no) =>
     returnm (tt
      : unit).
@@ -430,7 +430,7 @@
  Definition read_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 11)} 
  : read_kind :=
     let p0_ := arg_ in
-@@ -29280,7 +29289,7 @@
+@@ -29295,7 +29304,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.
@@ -439,10 +439,10 @@
  Definition num_of_barrier_kind (arg_ : barrier_kind) 
  : {e : Z & ArithFact (0 <= e /\ e <= 22)} :=
     build_ex(match arg_ with
-@@ -30454,5 +30463,5 @@
-                    B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
+@@ -30473,5 +30482,5 @@
                     B0]
         : mword 64) |}.
+ Hint Unfold initial_regstate : sail.
 -
 +*)
  End Content.