summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/coq/Sail2_operators_mwords.v2
-rw-r--r--lib/coq/Sail2_prompt.v32
-rw-r--r--lib/coq/Sail2_state.v16
-rw-r--r--lib/coq/Sail2_state_lemmas.v27
-rw-r--r--lib/coq/Sail2_values.v33
5 files changed, 68 insertions, 42 deletions
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 1aaa3298..698ca51b 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -107,7 +107,7 @@ Qed.
Lemma subrange_lemma2 {n m o} : (o <= m < n -> m+1 = o+(m-o+1))%nat.
omega.
Qed.
-Lemma subrange_lemma3 {n m o} `{ArithFact (0 <= o)} `{ArithFact (o <= m < n)} :
+Lemma subrange_lemma3 {m o} `{ArithFact (0 <= o)} `{ArithFact (o <= m)} :
Z.of_nat (Z.to_nat m - Z.to_nat o + 1)%nat = m - o + 1.
unwrap_ArithFacts.
rewrite Nat2Z.inj_add.
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index d2a8c805..fbc0f5b1 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -30,21 +30,25 @@ match l with
foreachM xs vars body
end.
-Fixpoint foreach_ZM_up' {rv e Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e :=
+Fixpoint foreach_ZM_up' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e.
+exact (
if sumbool_of_bool (from + off <=? to) then
match n with
| O => returnm vars
- | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_up' from to step (off + step) n vars body
+ | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_up' rv e Vars from to step (off + step) n _ _ vars body
end
- else returnm vars.
+ else returnm vars).
+Defined.
-Fixpoint foreach_ZM_down' {rv e Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e :=
+Fixpoint foreach_ZM_down' {rv e Vars} (from to step off : Z) (n : nat) `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e.
+exact (
if sumbool_of_bool (to <=? from + off) then
match n with
| O => returnm vars
- | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_down' from to step (off - step) n vars body
+ | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_down' _ _ _ from to step (off - step) n _ _ vars body
end
- else returnm vars.
+ else returnm vars).
+Defined.
Definition foreach_ZM_up {rv e Vars} from to step vars body `{ArithFact (0 < step)} :=
foreach_ZM_up' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body.
@@ -190,13 +194,15 @@ Definition Zwf_guarded (z:Z) : Acc (Zwf 0) z :=
(*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*)
-Fixpoint whileMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) (acc : Acc (Zwf 0) limit) : monad RV Vars E :=
+Fixpoint whileMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) (acc : Acc (Zwf 0) limit) : monad RV Vars E.
+exact (
if Z_ge_dec limit 0 then
cond vars >>= fun cond_val =>
if cond_val then
- body vars >>= fun vars => whileMT' (limit - 1) vars cond body (_limit_reduces acc)
+ body vars >>= fun vars => whileMT' _ _ _ (limit - 1) vars cond body (_limit_reduces acc)
else returnm vars
- else Fail "Termination limit reached".
+ else Fail "Termination limit reached").
+Defined.
Definition whileMT {RV Vars E} (vars : Vars) (measure : Vars -> Z) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E :=
let limit := measure vars in
@@ -204,12 +210,14 @@ Definition whileMT {RV Vars E} (vars : Vars) (measure : Vars -> Z) (cond : Vars
(*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*)
-Fixpoint untilMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) (acc : Acc (Zwf 0) limit) : monad RV Vars E :=
+Fixpoint untilMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) (acc : Acc (Zwf 0) limit) : monad RV Vars E.
+exact (
if Z_ge_dec limit 0 then
body vars >>= fun vars =>
cond vars >>= fun cond_val =>
- if cond_val then returnm vars else untilMT' (limit - 1) vars cond body (_limit_reduces acc)
- else Fail "Termination limit reached".
+ if cond_val then returnm vars else untilMT' _ _ _ (limit - 1) vars cond body (_limit_reduces acc)
+ else Fail "Termination limit reached").
+Defined.
Definition untilMT {RV Vars E} (vars : Vars) (measure : Vars -> Z) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E :=
let limit := measure vars in
diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v
index 7a25cbe9..618ca3a5 100644
--- a/lib/coq/Sail2_state.v
+++ b/lib/coq/Sail2_state.v
@@ -114,13 +114,15 @@ let rec untilS vars cond body s =
if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s
*)
-Fixpoint whileST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E :=
+Fixpoint whileST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E.
+exact (
if Z_ge_dec limit 0 then
cond vars >>$= fun cond_val =>
if cond_val then
- body vars >>$= fun vars => whileST' (limit - 1) vars cond body (_limit_reduces acc)
+ body vars >>$= fun vars => whileST' _ _ _ (limit - 1) vars cond body (_limit_reduces acc)
else returnS vars
- else failS "Termination limit reached".
+ else failS "Termination limit reached").
+Defined.
Definition whileST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E :=
let limit := measure vars in
@@ -128,12 +130,14 @@ Definition whileST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV b
(*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*)
-Fixpoint untilST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E :=
+Fixpoint untilST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E.
+exact (
if Z_ge_dec limit 0 then
body vars >>$= fun vars =>
cond vars >>$= fun cond_val =>
- if cond_val then returnS vars else untilST' (limit - 1) vars cond body (_limit_reduces acc)
- else failS "Termination limit reached".
+ if cond_val then returnS vars else untilST' _ _ _ (limit - 1) vars cond body (_limit_reduces acc)
+ else failS "Termination limit reached").
+Defined.
Definition untilST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E :=
let limit := measure vars in
diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v
index 90ae6840..dd83f239 100644
--- a/lib/coq/Sail2_state_lemmas.v
+++ b/lib/coq/Sail2_state_lemmas.v
@@ -839,26 +839,26 @@ unfold whileMT, whileST.
generalize (measure vars) as limit. intro.
revert vars.
destruct (Z.le_decidable 0 limit).
-* generalize (Zwf_guarded limit) as acc.
+* generalize (Zwf_guarded limit) at 1 as acc1.
+ generalize (Zwf_guarded limit) at 1 as acc2.
apply Wf_Z.natlike_ind with (x := limit).
- + intros [acc] *; simpl.
- match goal with |- context [Build_ArithFact _ ?prf] => generalize prf; intros ?Proof end.
+ + intros [acc1] [acc2] *; simpl.
rewrite_liftState.
apply bindS_cong; auto.
intros [|]; auto.
apply bindS_cong; auto.
- intros. destruct (_limit_reduces _). simpl.
+ intros. repeat destruct (_limit_reduces _). simpl.
reflexivity.
+ clear limit H.
- intros limit H IH [acc] vars s. simpl.
+ intros limit H IH [acc1] [acc2] vars s. simpl.
destruct (Z_ge_dec _ _); try omega.
rewrite_liftState.
apply bindS_cong; auto.
intros [|]; auto.
apply bindS_cong; auto.
intros.
- gen_reduces.
- replace (Z.succ limit - 1) with limit; try omega. intro acc'.
+ repeat gen_reduces.
+ replace (Z.succ limit - 1) with limit; try omega. intros acc1' acc2'.
apply IH.
+ assumption.
* intros. simpl.
@@ -912,24 +912,25 @@ unfold untilMT, untilST.
generalize (measure vars) as limit. intro.
revert vars.
destruct (Z.le_decidable 0 limit).
-* generalize (Zwf_guarded limit) as acc.
+* generalize (Zwf_guarded limit) at 1 as acc1.
+ generalize (Zwf_guarded limit) at 1 as acc2.
apply Wf_Z.natlike_ind with (x := limit).
- + intros [acc] * s; simpl.
+ + intros [acc1] [acc2] * s; simpl.
rewrite_liftState.
apply bindS_cong; auto.
intros. apply bindS_cong; auto.
intros [|]; auto.
- destruct (_limit_reduces _). simpl.
+ repeat destruct (_limit_reduces _). simpl.
reflexivity.
+ clear limit H.
- intros limit H IH [acc] vars s. simpl.
+ intros limit H IH [acc1] [acc2] vars s. simpl.
destruct (Z_ge_dec _ _); try omega.
rewrite_liftState.
apply bindS_cong; auto.
intros. apply bindS_cong; auto.
intros [|]; auto.
- gen_reduces.
- replace (Z.succ limit - 1) with limit; try omega. intro acc'.
+ repeat gen_reduces.
+ replace (Z.succ limit - 1) with limit; try omega. intros acc1' acc2'.
apply IH.
+ assumption.
* intros. simpl.
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index afa22856..47fa2fda 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1785,18 +1785,9 @@ Ltac solve_unknown :=
exact (Build_ArithFact _ I)
end.
-Ltac solve_arithfact :=
+Ltac run_main_solver_impl :=
(* Attempt a simple proof first to avoid lengthy preparation steps (especially
as the large proof terms can upset subsequent proofs). *)
-intros; (* To solve implications for derive_m *)
-try solve_unknown;
-match goal with |- ArithFact (?x <= ?x <= ?x) => try (exact trivial_range) | _ => idtac end;
-try fill_in_evar_eq;
-try match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end;
-(* Trying reflexivity will fill in more complex metavariable examples than
- fill_in_evar_eq above, e.g., 8 * n = 8 * ?Goal3 *)
-try (constructor; reflexivity);
-try (constructor; repeat match goal with |- and _ _ => split end; z_comparisons);
try (constructor; simple_omega);
prepare_for_solver;
(*dump_context;*)
@@ -1804,9 +1795,31 @@ constructor;
repeat match goal with |- and _ _ => split end;
main_solver.
+(* This can be redefined to remove the abstract. *)
+Ltac run_main_solver :=
+ solve
+ [ abstract run_main_solver_impl
+ | run_main_solver_impl (* for cases where there's an evar in the goal *)
+ ].
+
+Ltac solve_arithfact :=
+ intros; (* To solve implications for derive_m *)
+ solve
+ [ solve_unknown
+ | match goal with |- ArithFact (?x <= ?x <= ?x) => exact trivial_range end
+ | fill_in_evar_eq
+ | match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end
+ (* Trying reflexivity will fill in more complex metavariable examples than
+ fill_in_evar_eq above, e.g., 8 * n = 8 * ?Goal3 *)
+ | constructor; reflexivity
+ | constructor; repeat match goal with |- and _ _ => split end; z_comparisons
+ | run_main_solver
+ ].
+
(* Add an indirection so that you can redefine run_solver to fail to get
slow running constraints into proof mode. *)
Ltac run_solver := solve_arithfact.
+
Hint Extern 0 (ArithFact _) => run_solver : typeclass_instances.
Hint Unfold length_mword : sail.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 22:56:08 +0000