From f1ec636b83611f9d69e2a4d6ce34413399b73823 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 1 Aug 2018 14:26:12 +0100
Subject: Coq: implicit range conversions for function arguments, debug tracing
 The new option -dcoq_debug_on takes a list of functions to output tracing on.

---
 lib/coq/Sail2_values.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 0ce6134f..5752e6c0 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1036,6 +1036,10 @@ Qed.
 
 Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply ReasonableSize_witness; assumption | constructor; omega]) : typeclass_instances.
 
+Definition to_range (x : Z) : {y : Z & ArithFact (x <= y <= x)} := build_ex x.
+
+
+
 Instance mword_Bitvector {a : Z} `{ArithFact (a >= 0)} : (Bitvector (mword a)) := {
   bits_of v := List.map bitU_of_bool (bitlistFromWord (get_word v));
   of_bits v := option_map (fun bl => to_word isPositive (fit_bbv_word (wordFromBitlist bl))) (just_list (List.map bool_of_bitU v));
-- 
cgit v1.2.3


From 5980711d118ad6d0c28644be605447c3dc82be64 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 2 Aug 2018 11:52:04 +0100
Subject: Update a few prover gitignores

---
 lib/hol/.gitignore      | 19 ++++++++++---------
 lib/isabelle/.gitignore |  2 ++
 2 files changed, 12 insertions(+), 9 deletions(-)

(limited to 'lib')

diff --git a/lib/hol/.gitignore b/lib/hol/.gitignore
index fe652801..73d33f88 100644
--- a/lib/hol/.gitignore
+++ b/lib/hol/.gitignore
@@ -1,9 +1,10 @@
-prompt_monadScript.sml
-promptScript.sml
-sail_instr_kindsScript.sml
-sail_operators_bitlistsScript.sml
-sail_operators_mwordsScript.sml
-sail_operatorsScript.sml
-sail_valuesScript.sml
-state_monadScript.sml
-stateScript.sml
+sail2_prompt_monadScript.sml
+sail2_promptScript.sml
+sail2_instr_kindsScript.sml
+sail2_operators_bitlistsScript.sml
+sail2_operators_mwordsScript.sml
+sail2_operatorsScript.sml
+sail2_valuesScript.sml
+sail2_state_monadScript.sml
+sail2_stateScript.sml
+sail2_stringScript.sml
diff --git a/lib/isabelle/.gitignore b/lib/isabelle/.gitignore
index ed83cdc1..fad6adbd 100644
--- a/lib/isabelle/.gitignore
+++ b/lib/isabelle/.gitignore
@@ -10,4 +10,6 @@ Sail2_valuesAuxiliary.thy
 Sail2_values.thy
 Sail2_stateAuxiliary.thy
 Sail2_state_monad.thy
+Sail2_state_lifting.thy
 Sail2_state.thy
+Sail2_string.thy
\ No newline at end of file
-- 
cgit v1.2.3


From 8a06df3ad1b90a355d3e5adb694002f00e67823e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 2 Aug 2018 15:58:45 +0100
Subject: Fill in more Coq builtins for aarch64

---
 lib/coq/Sail2_values.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 5752e6c0..6fcbbb52 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -54,7 +54,10 @@ Instance Decidable_eq_from_dec {T:Type} (eqdec: forall x y : T, {x = y} + {x <>
   Decidable_witness := proj1_sig (bool_of_sumbool (eqdec x y))
 }.
 destruct (eqdec x y); simpl; split; congruence.
-Qed.
+Defined.
+
+Instance Decidable_eq_string : forall (x y : string), Decidable (x = y) :=
+  Decidable_eq_from_dec String.string_dec.
 
 
 (* Project away range constraints in comparisons *)
-- 
cgit v1.2.3


From 03dcb84bb8330cfa7b947ff4ecc0c5c9efca8ab0 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 2 Aug 2018 16:35:47 +0100
Subject: Coq: limit eauto to ensure termination in reasonable time

---
 lib/coq/Sail2_values.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 6fcbbb52..41414c96 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1020,7 +1020,7 @@ prepare_for_solver;
  solve [apply ArithFact_mword; assumption
        | constructor; omega with Z
          (* The datatypes hints give us some list handling, esp In *)
-       | constructor; eauto with datatypes zarith sail
+       | constructor; eauto 3 with datatypes zarith sail
        | constructor; idtac "Unable to solve constraint"; dump_context; fail].
 Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances.
 
-- 
cgit v1.2.3


From 2cb15665392d0b87da9e0c1f43e19267f28c3a82 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 3 Aug 2018 14:52:44 +0100
Subject: Coq: generalise dependent pair handling a little 1. for monadic
 values (not in a terribly useful way, though) 2. for more types

---
 lib/coq/Sail2_prompt.v | 10 ++++++++++
 lib/coq/Sail2_values.v |  2 +-
 2 files changed, 11 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index c98e2926..0b3a2cd8 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -115,3 +115,13 @@ let rec untilM vars cond body =
   write_reg r1 r1_v >> write_reg r2 r2_v*)
 
 *)
+
+(* If we need to build an existential after a monadic operation, assume that
+   we can do it entirely from the type. *)
+
+Definition build_ex_m {rv e} {T:Type} (x:monad rv T e) {P:T -> Prop} `{H:forall x, ArithFact (P x)} : monad rv {x : T & ArithFact (P x)} e :=
+  x >>= fun y => returnm (existT _ y (H y)).
+
+Definition projT1_m {rv e} {P:Z -> Prop} (x: monad rv {x : Z & P x} e) : monad rv Z e :=
+  x >>= fun y => returnm (projT1 y).
+
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 41414c96..acd11b45 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -21,7 +21,7 @@ Lemma use_ArithFact {P} `(ArithFact P) : P.
 apply fact.
 Defined.
 
-Definition build_ex (n:Z) {P:Z -> Prop} `{H:ArithFact (P n)} : {x : Z & ArithFact (P x)} :=
+Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} :=
   existT _ n H.
 
 Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness.
-- 
cgit v1.2.3


From baabef2bc2d39fc47ba47cd2ac5305856dd212a2 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 3 Aug 2018 15:04:18 +0100
Subject: Coq: use a dummy constraint when the real one is unknown Not really
 what we want, but a useful placeholder because of the widespread use of
 ex_int.

---
 lib/coq/Sail2_values.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index acd11b45..e4fff741 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1017,7 +1017,8 @@ Ltac prepare_for_solver :=
 Ltac solve_arithfact :=
 prepare_for_solver;
 (*dump_context;*)
- solve [apply ArithFact_mword; assumption
+ solve [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; instantiate (1 := fun _ => True); constructor; constructor end
+       | apply ArithFact_mword; assumption
        | constructor; omega with Z
          (* The datatypes hints give us some list handling, esp In *)
        | constructor; eauto 3 with datatypes zarith sail
-- 
cgit v1.2.3


From f9282ab5dec29d7ec99d473d013d32b41a0b8dbc Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 7 Aug 2018 11:02:09 +0100
Subject: Improve cast introduction for Lem Handles mutable variables and
 conditionals (there are still some corner cases that don't appear in Aarch64
 to do). The pretty printer is now back to preferring to use concrete types,
 but has a special case for casts to print more general types.

---
 lib/mono_rewrites.sail | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index aa8d05cd..9e837e10 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -29,7 +29,8 @@ function extsv(v) = exts_vec(sizeof('m),v)
 
 /* This is generated internally to deal with case splits which reveal the size
    of a bitvector */
-val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
 
 /* Definitions for the rewrites */
 
-- 
cgit v1.2.3


From 991dd7696058770d384b2aee3be0097f9af8d35d Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 9 Aug 2018 11:16:41 +0100
Subject: Coq: a bit more handling of unknown constraints

---
 lib/coq/Sail2_values.v | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index e4fff741..14ed0459 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1017,12 +1017,20 @@ Ltac prepare_for_solver :=
 Ltac solve_arithfact :=
 prepare_for_solver;
 (*dump_context;*)
- solve [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; instantiate (1 := fun _ => True); constructor; constructor end
-       | apply ArithFact_mword; assumption
-       | constructor; omega with Z
-         (* The datatypes hints give us some list handling, esp In *)
-       | constructor; eauto 3 with datatypes zarith sail
-       | constructor; idtac "Unable to solve constraint"; dump_context; fail].
+ solve
+ [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; constructor; exact (I : (fun _ => True) _) end
+ | match goal with |- ArithFact (?x = ?y) =>
+   (is_evar x || is_evar y);
+   (* compute to allow projections to remove proofs that might not be allowed in the evar *)
+   let x := eval cbn in x in
+   let y := eval cbn in y in
+   idtac "Warning: unknown equality constraint"; constructor; exact (eq_refl _ : x = y) end
+ | apply ArithFact_mword; assumption
+ | constructor; omega with Z
+   (* The datatypes hints give us some list handling, esp In *)
+ | constructor; eauto 3 with datatypes zarith sail
+ | constructor; idtac "Unable to solve constraint"; dump_context; fail
+ ].
 Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances.
 
 Hint Unfold length_mword : sail.
-- 
cgit v1.2.3


From 3f2205e552d850c5eb128f4763ea0e4016e43ad2 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 10 Aug 2018 18:37:24 +0100
Subject: Coq: add some of string library

---
 lib/coq/Makefile       |  2 +-
 lib/coq/Sail2_string.v | 16 ++++++++++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 lib/coq/Sail2_string.v

(limited to 'lib')

diff --git a/lib/coq/Makefile b/lib/coq/Makefile
index 97869e3c..99321aae 100644
--- a/lib/coq/Makefile
+++ b/lib/coq/Makefile
@@ -1,6 +1,6 @@
 BBV_DIR=../../../bbv/theories
 
-SRC=Sail2_prompt_monad.v  Sail2_prompt.v  Sail2_impl_base.v  Sail2_instr_kinds.v  Sail2_operators_bitlists.v  Sail2_operators_mwords.v  Sail2_operators.v  Sail2_values.v  Sail2_state_monad.v  Sail2_state.v
+SRC=Sail2_prompt_monad.v  Sail2_prompt.v  Sail2_impl_base.v  Sail2_instr_kinds.v  Sail2_operators_bitlists.v  Sail2_operators_mwords.v  Sail2_operators.v  Sail2_values.v  Sail2_state_monad.v  Sail2_state.v  Sail2_string.v
 
 COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv
 
diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
new file mode 100644
index 00000000..8bd7f0a6
--- /dev/null
+++ b/lib/coq/Sail2_string.v
@@ -0,0 +1,16 @@
+Require Import Sail2_values.
+
+Definition string_sub (s : string) (start : Z) (len : Z) : string :=
+  String.substring (Z.to_nat start) (Z.to_nat len) s.
+
+Definition string_startswith s expected :=
+  let prefix := String.substring 0 (String.length expected) s in
+  generic_eq prefix expected.
+
+Definition string_drop s n :=
+  let n := Z.to_nat n in
+  String.substring n (String.length s - n) s.
+
+Definition string_length s := Z.of_nat (String.length s).
+
+Definition string_append := String.append.
\ No newline at end of file
-- 
cgit v1.2.3


From a8fc6f2480790149a689e58d55a9dd3d6818dd3c Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 13 Aug 2018 11:52:30 +0100
Subject: Coq: drop irrelevant definitions before constraint solving (which
 were slowing down RISCV unacceptably because dealing with the xlen max/min
 values is surprisingly expensive)

---
 lib/coq/Sail2_values.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 14ed0459..7766e6af 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -938,6 +938,11 @@ end.
 Ltac not_Z ty := match ty with Z => fail 1 | _ => idtac end.
 Ltac clear_non_Z_defns := 
   repeat match goal with H := _ : ?X |- _ => not_Z X; clearbody H end.
+Ltac clear_irrelevant_defns :=
+repeat match goal with X := _ |- _ =>
+  match goal with |- context[X] => idtac end ||
+  match goal with _ : context[X] |- _ => idtac end || clear X
+end.
 
 Lemma ArithFact_mword (a : Z) (w : mword a) : ArithFact (a >= 0).
 constructor.
@@ -1005,6 +1010,7 @@ Ltac dump_context :=
   match goal with |- ?X => idtac "Goal:" X end.
 Ltac prepare_for_solver :=
 (*dump_context;*)
+ clear_irrelevant_defns;
  clear_non_Z_defns;
  extract_properties;
  repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
-- 
cgit v1.2.3


From a3c66eb5bc5d98a8ce400e5c391e7d9db940c3a7 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 13 Aug 2018 17:24:54 +0100
Subject: Coq: more strings for RISC-V

---
 lib/coq/Sail2_string.v | 27 +++++++++++++++++++++++----
 1 file changed, 23 insertions(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
index 8bd7f0a6..9ca9cb67 100644
--- a/lib/coq/Sail2_string.v
+++ b/lib/coq/Sail2_string.v
@@ -7,10 +7,29 @@ Definition string_startswith s expected :=
   let prefix := String.substring 0 (String.length expected) s in
   generic_eq prefix expected.
 
-Definition string_drop s n :=
-  let n := Z.to_nat n in
+Definition string_drop s (n : {n : Z & ArithFact (n >= 0)}) :=
+  let n := Z.to_nat (projT1 n) in
   String.substring n (String.length s - n) s.
 
-Definition string_length s := Z.of_nat (String.length s).
+Definition string_length s : {n : Z & ArithFact (n >= 0)} :=
+ build_ex (Z.of_nat (String.length s)).
 
-Definition string_append := String.append.
\ No newline at end of file
+Definition string_append := String.append.
+
+(* TODO: maybe_int_of_prefix, maybe_int_of_string *)
+
+Fixpoint n_leading_spaces (s:string) : nat :=
+  match s with
+  | EmptyString => 0
+  | String " " t => S (n_leading_spaces t)
+  | _ => 0
+  end.
+
+Definition opt_spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >= 0)}) :=
+  Some (tt, build_ex (Z.of_nat (n_leading_spaces s))).
+
+Definition spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >= 0)}) :=
+  match n_leading_spaces s with
+  | O => None
+  | S n => Some (tt, build_ex (Z.of_nat (S n)))
+  end.
\ No newline at end of file
-- 
cgit v1.2.3