Coq: switch to boolean predicates for Sail-type properties

- ArithFact takes a boolean predicate
- defined in terms of ArithFactP, which takes a Prop predicate,
  and is used directly for existentials
- used abstract in more definitions with direct proofs
- beef up solve_bool_with_Z to handle more equalities, andb and orb

1 files changed, 2 insertions, 2 deletions

diff --git a/lib/coq/Sail2_state_monad.v b/lib/coq/Sail2_state_monad.v
index bf5c5916..3fb1f8d9 100644
--- a/lib/coq/Sail2_state_monad.v
+++ b/lib/coq/Sail2_state_monad.v
@@ -182,14 +182,14 @@ Definition read_mem_bytesS {Regs E} (rk : read_kind) addr sz : monadS Regs (list
   returnS bytes).
 
 (*val read_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e*)
-Definition read_memtS {Regs E A B} (rk : read_kind) (a : mword A) sz `{ArithFact (B >= 0)} : monadS Regs (mword B * bitU) E :=
+Definition read_memtS {Regs E A B} (rk : read_kind) (a : mword A) sz `{ArithFact (B >=? 0)} : monadS Regs (mword B * bitU) E :=
   let a := Word.wordToNat (get_word a) in
   read_memt_bytesS rk a (Z.to_nat sz) >>$= (fun '(bytes, tag) =>
   maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val =>
   returnS (mem_val, tag))).
 
 (*val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e*)
-Definition read_memS {Regs E A B} rk (a : mword A) sz `{ArithFact (B >= 0)} : monadS Regs (mword B) E :=
+Definition read_memS {Regs E A B} rk (a : mword A) sz `{ArithFact (B >=? 0)} : monadS Regs (mword B) E :=
   read_memtS rk a sz >>$= (fun '(bytes, _) =>
   returnS bytes).