diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Hoare.v | 100 | ||||
| -rw-r--r-- | lib/coq/Makefile | 2 | ||||
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 141 | ||||
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 65 | ||||
| -rw-r--r-- | lib/coq/Sail2_prompt_monad.v | 4 | ||||
| -rw-r--r-- | lib/coq/Sail2_real.v | 71 | ||||
| -rw-r--r-- | lib/coq/Sail2_state.v | 53 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_lemmas.v | 122 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_monad.v | 4 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_monad_lemmas.v | 4 | ||||
| -rw-r--r-- | lib/coq/Sail2_string.v | 34 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 687 | ||||
| -rw-r--r-- | lib/coq/Sail2_values_lemmas.v | 392 | ||||
| -rw-r--r-- | lib/hol/Makefile | 2 | ||||
| -rw-r--r-- | lib/isabelle/Makefile | 10 | ||||
| -rw-r--r-- | lib/main.ml | 3 | ||||
| -rw-r--r-- | lib/regfp.sail | 32 | ||||
| -rw-r--r-- | lib/sail.c | 9 | ||||
| -rw-r--r-- | lib/sail.h | 2 |
19 files changed, 1443 insertions, 294 deletions
diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v index 400630af..f5d764b2 100644 --- a/lib/coq/Hoare.v +++ b/lib/coq/Hoare.v @@ -193,9 +193,9 @@ eapply PrePost_bindS. Qed. Lemma PrePost_and_boolSP (*[PrePost_compositeI]:*) Regs E PP QQ RR H - (l : monadS Regs {b : bool & Sail2_values.ArithFact (PP b)} E) - (r : monadS Regs {b : bool & Sail2_values.ArithFact (QQ b)} E) - P (Q : result {b : bool & Sail2_values.ArithFact (RR b)} E -> predS Regs) R : + (l : monadS Regs {b : bool & Sail2_values.ArithFactP (PP b)} E) + (r : monadS Regs {b : bool & Sail2_values.ArithFactP (QQ b)} E) + P (Q : result {b : bool & Sail2_values.ArithFactP (RR b)} E -> predS Regs) R : (forall p, PrePost R r (fun r => @@ -237,9 +237,9 @@ eapply PrePost_bindS. Qed. Lemma PrePost_or_boolSP (*[PrePost_compositeI]:*) Regs E PP QQ RR H - (l : monadS Regs {b : bool & Sail2_values.ArithFact (PP b)} E) - (r : monadS Regs {b : bool & Sail2_values.ArithFact (QQ b)} E) - P (Q : result {b : bool & Sail2_values.ArithFact (RR b)} E -> predS Regs) R : + (l : monadS Regs {b : bool & Sail2_values.ArithFactP (PP b)} E) + (r : monadS Regs {b : bool & Sail2_values.ArithFactP (QQ b)} E) + P (Q : result {b : bool & Sail2_values.ArithFactP (RR b)} E -> predS Regs) R : (forall p, PrePost R r (fun r => @@ -530,6 +530,16 @@ destruct b as [H | H]. * apply (HY H). reflexivity. Qed. +Lemma PrePostE_match_sum_branch (*[PrePostE_compositeI]:*) Regs A Ety X Y (b : sumbool X Y) (f : X -> monadS Regs A Ety) (g : Y -> monadS Regs A Ety) Pf Pg Q E : + (forall H : X, b = left H -> PrePostE (Pf H) (f H) Q E) -> + (forall H : Y, b = right H -> PrePostE (Pg H) (g H) Q E) -> + PrePostE (fun s => match b with left H => Pf H s | right H => Pg H s end) (match b with left H => f H | right H => g H end) Q E. +intros HX HY. +destruct b as [H | H]. +* apply (HX H). reflexivity. +* apply (HY H). reflexivity. +Qed. + Lemma PrePostE_if Regs A Ety (b : bool) (f g : monadS Regs A Ety) P Q E : (b = true -> PrePostE P f Q E) -> (b = false -> PrePostE P g Q E) -> @@ -598,9 +608,9 @@ Qed. and prevents the reduction of the function application. *) Lemma PrePostE_and_boolSP (*[PrePost_compositeI]:*) Regs Ety PP QQ RR H - (l : monadS Regs {b : bool & Sail2_values.ArithFact (PP b)} Ety) - (r : monadS Regs {b : bool & Sail2_values.ArithFact (QQ b)} Ety) - P (Q : {b : bool & Sail2_values.ArithFact (RR b)} -> predS Regs) E R : + (l : monadS Regs {b : bool & Sail2_values.ArithFactP (PP b)} Ety) + (r : monadS Regs {b : bool & Sail2_values.ArithFactP (QQ b)} Ety) + P (Q : {b : bool & Sail2_values.ArithFactP (RR b)} -> predS Regs) E R : PrePostE R r (fun r s => forall pf, Q (existT _ (projT1 r) pf) s) E -> PrePostE P l (fun r s => match r with @@ -635,9 +645,9 @@ eapply PrePostE_bindS. Qed. Lemma PrePostE_or_boolSP (*[PrePost_compositeI]:*) Regs Ety PP QQ RR H - (l : monadS Regs {b : bool & Sail2_values.ArithFact (PP b)} Ety) - (r : monadS Regs {b : bool & Sail2_values.ArithFact (QQ b)} Ety) - P (Q : {b : bool & Sail2_values.ArithFact (RR b)} -> predS Regs) E R : + (l : monadS Regs {b : bool & Sail2_values.ArithFactP (PP b)} Ety) + (r : monadS Regs {b : bool & Sail2_values.ArithFactP (QQ b)} Ety) + P (Q : {b : bool & Sail2_values.ArithFactP (RR b)} -> predS Regs) E R : PrePostE R r (fun r s => forall pf, Q (existT _ (projT1 r) pf) s) E -> PrePostE P l (fun r s => match r with @@ -764,6 +774,43 @@ apply PrePost_foreachS_invariant with (Q := fun v => match v with Value a => Q a auto. Qed. +Lemma PrePostE_foreach_ZS_up_invariant Regs Vars Ety from to step (H : Sail2_values.ArithFact (0 <? step)%Z) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) : + (forall i range vars, PrePostE (Q vars) (body i range vars) Q E) -> + PrePostE (Q vars) (foreach_ZS_up from to step vars body) Q E. +intro INV. +unfold foreach_ZS_up. +match goal with +| |- context[@foreach_ZS_up' _ _ _ _ _ _ _ _ _ ?pf _ _] => generalize pf +end. +generalize 0%Z at 2 3 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros. +* simpl. destruct (Sumbool.sumbool_of_bool (from + off <=? to)%Z); apply PrePostE_returnS. +* simpl. destruct (Sumbool.sumbool_of_bool (from + off <=? to)%Z). + + eapply PrePostE_bindS. + - intro. apply IHn. + - apply INV. + + apply PrePostE_returnS. +Qed. + +Lemma PrePostE_foreach_ZS_down_invariant Regs Vars Ety from to step (H : Sail2_values.ArithFact (0 <? step)%Z) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) : + (forall i range vars, PrePostE (Q vars) (body i range vars) Q E) -> + PrePostE (Q vars) (foreach_ZS_down from to step vars body) Q E. +intro INV. +unfold foreach_ZS_down. +match goal with +| |- context[@foreach_ZS_down' _ _ _ _ _ _ _ _ _ ?pf _ _] => generalize pf +end. +generalize 0%Z at 1 3 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros. +* simpl. destruct (Sumbool.sumbool_of_bool (to <=? from + off)%Z); apply PrePostE_returnS. +* simpl. destruct (Sumbool.sumbool_of_bool (to <=? from + off)%Z). + + eapply PrePostE_bindS. + - intro. apply IHn. + - apply INV. + + apply PrePostE_returnS. +Qed. Lemma PrePostE_use_pre Regs A Ety m (P : predS Regs) (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : (forall s, P s -> PrePostE P m Q E) -> @@ -991,7 +1038,7 @@ Qed. Local Open Scope Z. -Lemma PrePostE_undefined_bitvectorS_any Regs Ety n `{Sail2_values.ArithFact (n >= 0)} (Q : Sail2_values.mword n -> predS Regs) (E : ex Ety -> predS Regs) : +Lemma PrePostE_undefined_bitvectorS_any Regs Ety n `{Sail2_values.ArithFact (n >=? 0)} (Q : Sail2_values.mword n -> predS Regs) (E : ex Ety -> predS Regs) : PrePostE (fun s => forall w, Q w s) (undefined_bitvectorS n) Q E. unfold undefined_bitvectorS. eapply PrePostE_strengthen_pre. @@ -1002,15 +1049,15 @@ simpl. auto. Qed. -Lemma PrePostE_undefined_bitvectorS_ignore Regs Ety n `{Sail2_values.ArithFact (n >= 0)} (Q : predS Regs) (E : ex Ety -> predS Regs) : +Lemma PrePostE_undefined_bitvectorS_ignore Regs Ety n `{Sail2_values.ArithFact (n >=? 0)} (Q : predS Regs) (E : ex Ety -> predS Regs) : PrePostE Q (undefined_bitvectorS n) (fun _ => Q) E. eapply PrePostE_strengthen_pre. apply PrePostE_undefined_bitvectorS_any; auto. simpl; auto. Qed. -Lemma PrePostE_build_trivial_exS Regs (T:Type) Ety (m : monadS Regs T Ety) P (Q : {T & Sail2_values.ArithFact True} -> predS Regs) E : - PrePostE P m (fun v => Q (existT _ v (Sail2_values.Build_ArithFact _ I))) E -> +Lemma PrePostE_build_trivial_exS Regs (T:Type) Ety (m : monadS Regs T Ety) P (Q : {T & Sail2_values.ArithFact true} -> predS Regs) E : + PrePostE P m (fun v => Q (existT _ v (Sail2_values.Build_ArithFactP _ eq_refl))) E -> PrePostE P (build_trivial_exS m) Q E. intro H. unfold build_trivial_exS. @@ -1064,7 +1111,6 @@ Create HintDb PrePostE_specs. Ltac PrePostE_step := match goal with - | |- _ => solve [ clear; eauto with nocore PrePostE_specs ] | |- PrePostE _ (bindS _ (fun _ => ?f)) _ _ => eapply PrePostE_bindS_ignore | |- PrePostE _ (bindS _ _) _ _ => eapply PrePostE_bindS; intros | |- PrePostE _ (seqS _ _) _ _ => eapply PrePostE_seqS; intros @@ -1077,9 +1123,12 @@ Ltac PrePostE_step := [ eapply PrePostE_if_branch; intros | eapply PrePostE_if_sum_branch; intros ] + | |- PrePostE _ (match _ with left _ => _ | right _ => _ end) _ _ => + eapply PrePostE_match_sum_branch; intros | |- PrePostE _ (readS _) ?ppeQ ?ppeE => apply PrePostE_readS with (Q := ppeQ) (E := ppeE) | |- PrePostE _ (assert_expS _ _) _ _ => apply PrePostE_assert_expS | |- PrePostE _ (assert_expS' _ _) _ _ => apply PrePostE_assert_expS' + | |- PrePostE _ (maybe_failS _ _) _ _ => apply PrePostE_maybe_failS | |- PrePostE _ (exitS _) _ ?E => apply (PrePostE_exitS _ _ _ _ _ E) | |- PrePostE _ (and_boolS _ _) _ _ => eapply PrePostE_and_boolS | |- PrePostE _ (or_boolS _ _) _ _ => eapply PrePostE_or_boolS @@ -1102,6 +1151,8 @@ Ltac PrePostE_step := | |- PrePostE _ (undefined_bitvectorS _) ?ppeQ ?ppeE => apply PrePostE_undefined_bitvectorS_any with (Q := ppeQ) (E := ppeE) | |- PrePostE _ (build_trivial_exS _) _ _ => eapply PrePostE_build_trivial_exS; intros + | |- PrePostE _ (liftRS _) ?ppeQ ?ppeE => + apply PrePostE_liftRS with (Q := ppeQ) (E := ppeE); intros | |- PrePostE _ (let '(_,_) := ?x in _) _ _ => is_var x; let PAIR := fresh "PAIR" in @@ -1114,4 +1165,19 @@ Ltac PrePostE_step := assert (PAIR : x = existT _ (projT1 x) (projT2 x)) by (destruct x; reflexivity); rewrite PAIR at - 1; clear PAIR + (* Applying specifications from the hintdb. For performance, + * don't use hypotheses from the context (if we need to and it's + not good enough, consider using a separate hintdb) + + * use auto rather than eauto - when eauto is applied to a goal + with an evar Coq falls back to trying all of the specs rather + than picking out one which matches (at least, with 8.9). + *) + | |- PrePostE ?pre _ _ _ => + clear; + solve [ tryif is_evar pre then auto with nocore PrePostE_specs + else (eapply PrePostE_strengthen_pre; + [ auto with nocore PrePostE_specs + | exact (fun s p => p) ]) + ] end. diff --git a/lib/coq/Makefile b/lib/coq/Makefile index fa453d90..d16191cb 100644 --- a/lib/coq/Makefile +++ b/lib/coq/Makefile @@ -1,7 +1,7 @@ BBV_DIR?=../../../bbv CORESRC=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_state_lifting.v Sail2_string.v Sail2_real.v -PROOFSRC=Sail2_state_monad_lemmas.v Sail2_state_lemmas.v Hoare.v +PROOFSRC=Sail2_values_lemmas.v Sail2_state_monad_lemmas.v Sail2_state_lemmas.v Hoare.v SRC=$(CORESRC) $(PROOFSRC) COQ_LIBS = -R . Sail -R "$(BBV_DIR)/theories" bbv diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index 698ca51b..1f176ad9 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -8,6 +8,7 @@ Require Import Arith. Require Import ZArith. Require Import Omega. Require Import Eqdep_dec. +Open Scope Z. Fixpoint cast_positive (T : positive -> Type) (p q : positive) : T p -> p = q -> T q. refine ( @@ -43,11 +44,17 @@ destruct m. * simpl. rewrite cast_positive_refl. reflexivity. Qed. -Definition autocast {T : Z -> Type} {m n} (x : T m) `{H:ArithFact (m = n)} : T n := - cast_T x (use_ArithFact H). +Definition autocast {T : Z -> Type} {m n} (x : T m) `{H:ArithFact (m =? n)} : T n. +refine (cast_T x _). +apply Z.eqb_eq. +apply (use_ArithFact H). +Defined. -Definition autocast_m {rv e m n} (x : monad rv (mword m) e) `{H:ArithFact (m = n)} : monad rv (mword n) e := - x >>= fun x => returnm (cast_T x (use_ArithFact H)). +Definition autocast_m {rv e m n} (x : monad rv (mword m) e) `{H:ArithFact (m =? n)} : monad rv (mword n) e. +refine (x >>= fun x => returnm (cast_T x _)). +apply Z.eqb_eq. +apply (use_ArithFact H). +Defined. Definition cast_word {m n} (x : Word.word m) (eq : m = n) : Word.word n := DepEqNat.nat_cast _ eq x. @@ -94,9 +101,10 @@ Definition update_vec_inc {a} (w : mword a) i b : mword a := (*val update_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a*) Definition update_vec_dec {a} (w : mword a) i b : mword a := opt_def w (update_mword_dec w i b). -Lemma subrange_lemma0 {n m o} `{ArithFact (0 <= o)} `{ArithFact (o <= m < n)} : (Z.to_nat o <= Z.to_nat m < Z.to_nat n)%nat. +Lemma subrange_lemma0 {n m o} `{ArithFact (0 <=? o)} `{ArithFact (o <=? m <? n)} : (Z.to_nat o <= Z.to_nat m < Z.to_nat n)%nat. intros. unwrap_ArithFacts. +unbool_comparisons. split. + apply Z2Nat.inj_le; omega. + apply Z2Nat.inj_lt; omega. @@ -107,9 +115,10 @@ Qed. Lemma subrange_lemma2 {n m o} : (o <= m < n -> m+1 = o+(m-o+1))%nat. omega. Qed. -Lemma subrange_lemma3 {m o} `{ArithFact (0 <= o)} `{ArithFact (o <= m)} : +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. +unbool_comparisons. rewrite Nat2Z.inj_add. rewrite Nat2Z.inj_sub. repeat rewrite Z2Nat.id; try omega. @@ -117,7 +126,7 @@ reflexivity. apply Z2Nat.inj_le; omega. Qed. -Definition subrange_vec_dec {n} (v : mword n) m o `{ArithFact (0 <= o)} `{ArithFact (o <= m < n)} : mword (m - o + 1) := +Definition subrange_vec_dec {n} (v : mword n) m o `{ArithFact (0 <=? o)} `{ArithFact (o <=? m <? n)} : mword (m - o + 1) := let n := Z.to_nat n in let m := Z.to_nat m in let o := Z.to_nat o in @@ -127,10 +136,10 @@ Definition subrange_vec_dec {n} (v : mword n) m o `{ArithFact (0 <= o)} `{ArithF (cast_word (split1 (m+1) (n-(m+1)) (cast_word w (subrange_lemma1 prf))) (subrange_lemma2 prf))) subrange_lemma3. -Definition subrange_vec_inc {n} (v : mword n) m o `{ArithFact (0 <= m)} `{ArithFact (m <= o < n)} : mword (o - m + 1) := autocast (subrange_vec_dec v (n-1-m) (n-1-o)). +Definition subrange_vec_inc {n} (v : mword n) m o `{ArithFact (0 <=? m)} `{ArithFact (m <=? o <? n)} : mword (o - m + 1) := autocast (subrange_vec_dec v (n-1-m) (n-1-o)). (* TODO: get rid of bogus default *) -Parameter dummy_vector : forall {n} `{ArithFact (n >= 0)}, mword n. +Parameter dummy_vector : forall {n} `{ArithFact (n >=? 0)}, mword n. (*val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a*) Definition update_subrange_vec_inc_unchecked {a b} (v : mword a) i j (w : mword b) : mword a := @@ -141,10 +150,11 @@ Definition update_subrange_vec_dec_unchecked {a b} (v : mword a) i j (w : mword opt_def dummy_vector (of_bits (update_subrange_bv_dec v i j w)). Lemma update_subrange_vec_dec_pf {o m n} : -ArithFact (0 <= o) -> -ArithFact (o <= m < n) -> +ArithFact (0 <=? o) -> +ArithFact (o <=? m <? n) -> Z.of_nat (Z.to_nat o + (Z.to_nat (m - o + 1) + (Z.to_nat n - (Z.to_nat m + 1)))) = n. intros [H1] [H2]. +unbool_comparisons. rewrite <- subrange_lemma3. rewrite !Nat2Z.inj_add. rewrite !Nat2Z.inj_sub. @@ -155,7 +165,7 @@ apply Z2Nat.inj_lt; omega. apply Z2Nat.inj_le; omega. Qed. -Definition update_subrange_vec_dec {n} (v : mword n) m o `{ArithFact (0 <= o)} `{ArithFact (o <= m < n)} (w : mword (m - o + 1)) : mword n. +Definition update_subrange_vec_dec {n} (v : mword n) m o `{ArithFact (0 <=? o)} `{ArithFact (o <=? m <? n)} (w : mword (m - o + 1)) : mword n. refine ( let n := Z.to_nat n in let m := Z.to_nat m in @@ -173,7 +183,7 @@ refine ( cast_to_mword z (update_subrange_vec_dec_pf _ _)). Defined. -Definition update_subrange_vec_inc {n} (v : mword n) m o `{ArithFact (0 <= m)} `{ArithFact (m <= o < n)} (w : mword (o - m + 1)) : mword n := update_subrange_vec_dec v (n-1-m) (n-1-o) (autocast w). +Definition update_subrange_vec_inc {n} (v : mword n) m o `{ArithFact (0 <=? m)} `{ArithFact (m <=? o <? n)} (w : mword (o - m + 1)) : mword n := update_subrange_vec_dec v (n-1-m) (n-1-o) (autocast w). Lemma mword_nonneg {a} : mword a -> a >= 0. destruct a; @@ -182,9 +192,10 @@ destruct 1. Qed. (*val extz_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*) -Definition extz_vec {a b} `{ArithFact (b >= a)} (n : Z) (v : mword a) : mword b. +Definition extz_vec {a b} `{ArithFact (b >=? a)} (n : Z) (v : mword a) : mword b. refine (cast_to_mword (Word.zext (get_word v) (Z.to_nat (b - a))) _). unwrap_ArithFacts. +unbool_comparisons. assert (a >= 0). { apply mword_nonneg. assumption. } rewrite <- Z2Nat.inj_add; try omega. rewrite Zplus_minus. @@ -193,9 +204,10 @@ auto with zarith. Defined. (*val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b*) -Definition exts_vec {a b} `{ArithFact (b >= a)} (n : Z) (v : mword a) : mword b. +Definition exts_vec {a b} `{ArithFact (b >=? a)} (n : Z) (v : mword a) : mword b. refine (cast_to_mword (Word.sext (get_word v) (Z.to_nat (b - a))) _). unwrap_ArithFacts. +unbool_comparisons. assert (a >= 0). { apply mword_nonneg. assumption. } rewrite <- Z2Nat.inj_add; try omega. rewrite Zplus_minus. @@ -203,13 +215,14 @@ apply Z2Nat.id. auto with zarith. Defined. -Definition zero_extend {a} (v : mword a) (n : Z) `{ArithFact (n >= a)} : mword n := extz_vec n v. +Definition zero_extend {a} (v : mword a) (n : Z) `{ArithFact (n >=? a)} : mword n := extz_vec n v. -Definition sign_extend {a} (v : mword a) (n : Z) `{ArithFact (n >= a)} : mword n := exts_vec n v. +Definition sign_extend {a} (v : mword a) (n : Z) `{ArithFact (n >=? a)} : mword n := exts_vec n v. -Definition zeros (n : Z) `{ArithFact (n >= 0)} : mword n. +Definition zeros (n : Z) `{ArithFact (n >=? 0)} : mword n. refine (cast_to_mword (Word.wzero (Z.to_nat n)) _). unwrap_ArithFacts. +unbool_comparisons. apply Z2Nat.id. auto with zarith. Defined. @@ -227,11 +240,17 @@ assert ((Z.to_nat m <= Z.to_nat n)%nat). omega. Qed. -Definition vector_truncate {n} (v : mword n) (m : Z) `{ArithFact (m >= 0)} `{ArithFact (m <= n)} : mword m := - cast_to_mword (Word.split1 _ _ (cast_word (get_word v) (ltac:(unwrap_ArithFacts; apply truncate_eq; auto) : Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat)) (ltac:(unwrap_ArithFacts; apply Z2Nat.id; omega) : Z.of_nat (Z.to_nat m) = m). +Definition vector_truncate {n} (v : mword n) (m : Z) `{ArithFact (m >=? 0)} `{ArithFact (m <=? n)} : mword m. +refine (cast_to_mword (Word.split1 _ _ (cast_word (get_word v) (_ : Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat)) (_ : Z.of_nat (Z.to_nat m) = m)). +abstract (unwrap_ArithFacts; unbool_comparisons; apply truncate_eq; auto with zarith). +abstract (unwrap_ArithFacts; unbool_comparisons; apply Z2Nat.id; omega). +Defined. -Definition vector_truncateLSB {n} (v : mword n) (m : Z) `{ArithFact (m >= 0)} `{ArithFact (m <= n)} : mword m := - cast_to_mword (Word.split2 _ _ (cast_word (get_word v) (ltac:(unwrap_ArithFacts; apply truncateLSB_eq; auto) : Z.to_nat n = (Z.to_nat n - Z.to_nat m) + Z.to_nat m)%nat)) (ltac:(unwrap_ArithFacts; apply Z2Nat.id; omega) : Z.of_nat (Z.to_nat m) = m). +Definition vector_truncateLSB {n} (v : mword n) (m : Z) `{ArithFact (m >=? 0)} `{ArithFact (m <=? n)} : mword m. +refine (cast_to_mword (Word.split2 _ _ (cast_word (get_word v) (_ : Z.to_nat n = (Z.to_nat n - Z.to_nat m) + Z.to_nat m)%nat)) (_ : Z.of_nat (Z.to_nat m) = m)). +abstract (unwrap_ArithFacts; unbool_comparisons; apply truncateLSB_eq; auto with zarith). +abstract (unwrap_ArithFacts; unbool_comparisons; apply Z2Nat.id; omega). +Defined. Lemma concat_eq {a b} : a >= 0 -> b >= 0 -> Z.of_nat (Z.to_nat b + Z.to_nat a)%nat = a + b. intros. @@ -270,13 +289,18 @@ induction n. reflexivity. Qed. -Program Definition uint {a} (x : mword a) : {z : Z & ArithFact (0 <= z /\ z <= 2 ^ a - 1)} := - existT _ (Z.of_N (Word.wordToN (get_word x))) _. +Definition uint_plain {a} (x : mword a) : Z := + Z.of_N (Word.wordToN (get_word x)). + +Program Definition uint {a} (x : mword a) : {z : Z & ArithFact (0 <=? z <=? 2 ^ a - 1)} := + existT _ (uint_plain x) _. Next Obligation. constructor. +apply Bool.andb_true_iff. constructor. -* apply N2Z.is_nonneg. -* assert (2 ^ a - 1 = Z.of_N (2 ^ (Z.to_N a) - 1)). { +* apply Z.leb_le. apply N2Z.is_nonneg. +* apply Z.leb_le. + assert (2 ^ a - 1 = Z.of_N (2 ^ (Z.to_N a) - 1)). { rewrite N2Z.inj_sub. * rewrite N2Z.inj_pow. rewrite Z2N.id; auto. @@ -303,12 +327,18 @@ induction n. rewrite Z.pow_succ_r; auto with zarith. Qed. -Program Definition sint {a} `{ArithFact (a > 0)} (x : mword a) : {z : Z & ArithFact (-(2^(a-1)) <= z /\ z <= 2 ^ (a-1) - 1)} := - existT _ (Word.wordToZ (get_word x)) _. +Definition sint_plain {a} (x : mword a) : Z := + Word.wordToZ (get_word x). + +Program Definition sint {a} `{ArithFact (a >? 0)} (x : mword a) : {z : Z & ArithFact (-(2^(a-1)) <=? z <=? 2 ^ (a-1) - 1)} := + existT _ (sint_plain x) _. Next Obligation. +unfold sint_plain. destruct H. +unbool_comparisons. destruct a; try inversion fact. constructor. +unbool_comparisons_goal. generalize (get_word x). rewrite <- positive_nat_Z. destruct (Pos2Nat.is_succ p) as [n eq]. @@ -326,10 +356,10 @@ rewrite <- Z.lt_le_pred. auto. Defined. -Definition sint0 {a} `{ArithFact (a >= 0)} (x : mword a) : Z := +Definition sint0 {a} `{ArithFact (a >=? 0)} (x : mword a) : Z := if sumbool_of_bool (Z.eqb a 0) then 0 else projT1 (sint x). -Lemma length_list_pos : forall {A} {l:list A}, length_list l >= 0. +Lemma length_list_pos : forall {A} {l:list A}, 0 <= Z.of_nat (List.length l). unfold length_list. auto with zarith. Qed. @@ -369,9 +399,9 @@ val smult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword Definition add_vec {n} : mword n -> mword n -> mword n := word_binop Word.wplus. (*Definition sadd_vec {n} : mword n -> mword n -> mword n := sadd_bv w.*) Definition sub_vec {n} : mword n -> mword n -> mword n := word_binop Word.wminus. -Definition mult_vec {n m} `{ArithFact (m >= n)} (l : mword n) (r : mword n) : mword m := +Definition mult_vec {n m} `{ArithFact (m >=? n)} (l : mword n) (r : mword n) : mword m := word_binop Word.wmult (zero_extend l _) (zero_extend r _). -Definition mults_vec {n m} `{ArithFact (m >= n)} (l : mword n) (r : mword n) : mword m := +Definition mults_vec {n m} `{ArithFact (m >=? n)} (l : mword n) (r : mword n) : mword m := word_binop Word.wmult (sign_extend l _) (sign_extend r _). (*val add_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a @@ -456,14 +486,14 @@ match n with | O => Word.WO | S m => Word.combine w (replicate_bits_aux w m) end. -Lemma replicate_ok {n a} `{ArithFact (n >= 0)} `{ArithFact (a >= 0)} : +Lemma replicate_ok {n a} `{ArithFact (n >=? 0)} `{ArithFact (a >=? 0)} : Z.of_nat (Z.to_nat n * Z.to_nat a) = a * n. -destruct H. destruct H0. +destruct H. destruct H0. unbool_comparisons. rewrite <- Z2Nat.id; auto with zarith. rewrite Z2Nat.inj_mul; auto with zarith. rewrite Nat.mul_comm. reflexivity. Qed. -Definition replicate_bits {a} (w : mword a) (n : Z) `{ArithFact (n >= 0)} : mword (a * n) := +Definition replicate_bits {a} (w : mword a) (n : Z) `{ArithFact (n >=? 0)} : mword (a * n) := cast_to_mword (replicate_bits_aux (get_word w) (Z.to_nat n)) replicate_ok. (*val duplicate : forall 'a. Size 'a => bitU -> integer -> mword 'a @@ -491,6 +521,28 @@ Definition ugteq_vec := ugteq_bv. Definition sgteq_vec := sgteq_bv. *) +Lemma eq_vec_true_iff {n} (v w : mword n) : + eq_vec v w = true <-> v = w. +unfold eq_vec. +destruct n. +* simpl in v,w. shatter_word v. shatter_word w. + compute. intuition. +* simpl in *. destruct (weq v w). + + subst. rewrite weqb_eq; tauto. + + rewrite weqb_ne; auto. intuition. +* destruct v. +Qed. + +Lemma eq_vec_false_iff {n} (v w : mword n) : + eq_vec v w = false <-> v <> w. +specialize (eq_vec_true_iff v w). +destruct (eq_vec v w). +intuition. +intros [H1 H2]. +split. +* intros _ EQ. intuition. +* auto. +Qed. Definition eq_vec_dec {n} : forall (x y : mword n), {x = y} + {x <> y}. refine (match n with @@ -520,7 +572,7 @@ Qed. Definition reverse_endianness {n} (bits : mword n) := with_word (P := id) reverse_endianness_word bits. -Definition get_slice_int {a} `{ArithFact (a >= 0)} : Z -> Z -> Z -> mword a := get_slice_int_bv. +Definition get_slice_int {a} `{ArithFact (a >=? 0)} : Z -> Z -> Z -> mword a := get_slice_int_bv. Definition set_slice n m (v : mword n) x (w : mword m) : mword n := update_subrange_vec_dec_unchecked v (x + m - 1) x w. @@ -535,7 +587,7 @@ Definition set_slice_int len n lo (v : mword len) : Z := else n. (* Variant of bitvector slicing for the ARM model with few constraints *) -Definition slice {m} (v : mword m) lo len `{ArithFact (0 <= len)} : mword len := +Definition slice {m} (v : mword m) lo len `{ArithFact (0 <=? len)} : mword len := if sumbool_of_bool (orb (len =? 0) (lo <? 0)) then zeros len else @@ -545,7 +597,6 @@ Definition slice {m} (v : mword m) lo len `{ArithFact (0 <= len)} : mword len := else zeros len else autocast (subrange_vec_dec v (lo + len - 1) lo). -(* Lemma slice_is_ok m (v : mword m) lo len (H1 : 0 <= lo) (H2 : 0 < len) (H3: lo + len < m) : slice v lo len = autocast (subrange_vec_dec v (lo + len - 1) lo). @@ -558,20 +609,20 @@ destruct (sumbool_of_bool _). + exfalso. unbool_comparisons. omega. - + f_equal. - f_equal. -*) + + repeat replace_ArithFact_proof. + reflexivity. +Qed. Import ListNotations. -Definition count_leading_zeros {N : Z} (x : mword N) `{ArithFact (N >= 1)} -: {n : Z & ArithFact (0 <= n /\ n <= N)} := - let r : {n : Z & ArithFact (0 <= n /\ n <= N)} := build_ex N in +Definition count_leading_zeros {N : Z} (x : mword N) `{ArithFact (N >=? 1)} +: {n : Z & ArithFact (0 <=? n <=? N)} := + let r : {n : Z & ArithFact (0 <=? n <=? N)} := build_ex N in foreach_Z_up 0 (N - 1) 1 r (fun i _ r => (if ((eq_vec (vec_of_bits [access_vec_dec x i] : mword 1) (vec_of_bits [B1] : mword 1))) then build_ex (Z.sub (Z.sub (length_mword x) i) 1) - : {n : Z & ArithFact (0 <= n /\ n <= N)} + : {n : Z & ArithFact (0 <=? n <=? N)} else r)) . diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index fbc0f5b1..aeca1248 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -30,7 +30,7 @@ match l with foreachM xs vars body end. -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. +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 @@ -40,7 +40,7 @@ exact ( else returnm vars). Defined. -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. +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 @@ -50,9 +50,9 @@ exact ( else returnm vars). Defined. -Definition foreach_ZM_up {rv e Vars} from to step vars body `{ArithFact (0 < step)} := +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. -Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (0 < step)} := +Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (0 <? step)} := foreach_ZM_down' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. (*declare {isabelle} termination_argument foreachM = automatic*) @@ -69,9 +69,9 @@ Definition and_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad the state monad and program logic rules. They are not currently used in the proof rules because it was more convenient to quantify over them instead. *) Definition and_bool_left_proof {P Q R:bool -> Prop} : - ArithFact (P false) -> - ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r)) -> - ArithFact (R false). + ArithFactP (P false) -> + (forall l r, ArithFactP (P l -> ((l = true -> (Q r)) -> (R (andb l r))))) -> + ArithFactP (R false). intros [p] [h]. constructor. change false with (andb false false). @@ -80,20 +80,20 @@ congruence. Qed. Definition and_bool_full_proof {P Q R:bool -> Prop} {r} : - ArithFact (P true) -> - ArithFact (Q r) -> - ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r)) -> - ArithFact (R r). + ArithFactP (P true) -> + ArithFactP (Q r) -> + (forall l r, ArithFactP ((P l) -> ((l = true -> (Q r)) -> (R (andb l r))))) -> + ArithFactP (R r). intros [p] [q] [h]. constructor. change r with (andb true r). apply h; auto. Qed. -Definition and_boolMP {rv E} {P Q R:bool->Prop} (x : monad rv {b:bool & ArithFact (P b)} E) (y : monad rv {b:bool & ArithFact (Q b)} E) - `{H:ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r))} - : monad rv {b:bool & ArithFact (R b)} E := - x >>= fun '(existT _ x p) => (if x return ArithFact (P x) -> _ then +Definition and_boolMP {rv E} {P Q R:bool->Prop} (x : monad rv {b:bool & ArithFactP (P b)} E) (y : monad rv {b:bool & ArithFactP (Q b)} E) + `{H:forall l r, ArithFactP ((P l) -> ((l = true -> (Q r)) -> (R (andb l r))))} + : monad rv {b:bool & ArithFactP (R b)} E := + x >>= fun '(existT _ x p) => (if x return ArithFactP (P x) -> _ then fun p => y >>= fun '(existT _ y q) => returnm (existT _ y (and_bool_full_proof p q H)) else fun p => returnm (existT _ false (and_bool_left_proof p H))) p. @@ -103,9 +103,9 @@ Definition or_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad r Definition or_bool_left_proof {P Q R:bool -> Prop} : - ArithFact (P true) -> - ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r)) -> - ArithFact (R true). + ArithFactP (P true) -> + (forall l r, ArithFactP ((P l) -> (((l = false) -> (Q r)) -> (R (orb l r))))) -> + ArithFactP (R true). intros [p] [h]. constructor. change true with (orb true false). @@ -114,25 +114,25 @@ congruence. Qed. Definition or_bool_full_proof {P Q R:bool -> Prop} {r} : - ArithFact (P false) -> - ArithFact (Q r) -> - ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r)) -> - ArithFact (R r). + ArithFactP (P false) -> + ArithFactP (Q r) -> + (forall l r, ArithFactP ((P l) -> (((l = false) -> (Q r)) -> (R (orb l r))))) -> + ArithFactP (R r). intros [p] [q] [h]. constructor. change r with (orb false r). apply h; auto. Qed. -Definition or_boolMP {rv E} {P Q R:bool -> Prop} (l : monad rv {b : bool & ArithFact (P b)} E) (r : monad rv {b : bool & ArithFact (Q b)} E) - `{ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r))} - : monad rv {b : bool & ArithFact (R b)} E := +Definition or_boolMP {rv E} {P Q R:bool -> Prop} (l : monad rv {b : bool & ArithFactP (P b)} E) (r : monad rv {b : bool & ArithFactP (Q b)} E) + `{forall l r, ArithFactP ((P l) -> (((l = false) -> (Q r)) -> (R (orb l r))))} + : monad rv {b : bool & ArithFactP (R b)} E := l >>= fun '(existT _ l p) => - (if l return ArithFact (P l) -> _ then fun p => returnm (existT _ true (or_bool_left_proof p H)) + (if l return ArithFactP (P l) -> _ then fun p => returnm (existT _ true (or_bool_left_proof p H)) else fun p => r >>= fun '(existT _ r q) => returnm (existT _ r (or_bool_full_proof p q H))) p. -Definition build_trivial_ex {rv E} {T:Type} (x:monad rv T E) : monad rv {x : T & ArithFact True} E := - x >>= fun x => returnm (existT _ x (Build_ArithFact _ I)). +Definition build_trivial_ex {rv E} {T:Type} (x:monad rv T E) : monad rv {x : T & ArithFact true} E := + x >>= fun x => returnm (existT _ x (Build_ArithFactP _ eq_refl)). (*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e*) Definition bool_of_bitU_fail {rv E} (b : bitU) : monad rv bool E := @@ -164,9 +164,10 @@ Definition of_bits_fail {rv A E} `{Bitvector A} (bits : list bitU) : monad rv A (* For termination of recursive functions. We don't name assertions, so use the type class mechanism to find it. *) -Definition _limit_reduces {_limit} (_acc:Acc (Zwf 0) _limit) `{ArithFact (_limit >= 0)} : Acc (Zwf 0) (_limit - 1). +Definition _limit_reduces {_limit} (_acc:Acc (Zwf 0) _limit) `{ArithFact (_limit >=? 0)} : Acc (Zwf 0) (_limit - 1). refine (Acc_inv _acc _). destruct H. +unbool_comparisons. red. omega. Defined. @@ -269,18 +270,18 @@ Fixpoint undefined_word_nat {rv e} n : monad rv (Word.word n) e := returnm (Word.WS b t) end. -Definition undefined_bitvector {rv e} n `{ArithFact (n >= 0)} : monad rv (mword n) e := +Definition undefined_bitvector {rv e} n `{ArithFact (n >=? 0)} : monad rv (mword n) e := undefined_word_nat (Z.to_nat n) >>= fun w => returnm (word_to_mword w). (* 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 := +Definition build_ex_m {rv e} {T:Type} (x:monad rv T e) {P:T -> Prop} `{H:forall x, ArithFactP (P x)} : monad rv {x : T & ArithFactP (P x)} e := x >>= fun y => returnm (existT _ y (H y)). Definition projT1_m {rv e} {T:Type} {P:T -> Prop} (x: monad rv {x : T & P x} e) : monad rv T e := x >>= fun y => returnm (projT1 y). -Definition derive_m {rv e} {T:Type} {P Q:T -> Prop} (x : monad rv {x : T & P x} e) `{forall x, ArithFact (P x) -> ArithFact (Q x)} : monad rv {x : T & (ArithFact (Q x))} e := +Definition derive_m {rv e} {T:Type} {P Q:T -> Prop} (x : monad rv {x : T & ArithFactP (P x)} e) `{forall x, ArithFactP (P x) -> ArithFactP (Q x)} : monad rv {x : T & (ArithFactP (Q x))} e := x >>= fun y => returnm (build_ex (projT1 y)). diff --git a/lib/coq/Sail2_prompt_monad.v b/lib/coq/Sail2_prompt_monad.v index b26a2ff3..0ff65d28 100644 --- a/lib/coq/Sail2_prompt_monad.v +++ b/lib/coq/Sail2_prompt_monad.v @@ -189,7 +189,7 @@ Definition read_memt_bytes {rv A E} rk (addr : mword A) sz : monad rv (list memo Read_memt rk (Word.wordToNat (get_word addr)) (Z.to_nat sz) returnm. (*val read_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e*) -Definition read_memt {rv A B E} `{ArithFact (B >= 0)} rk (addr : mword A) sz : monad rv (mword B * bitU) E := +Definition read_memt {rv A B E} `{ArithFact (B >=? 0)} rk (addr : mword A) sz : monad rv (mword B * bitU) E := bind (read_memt_bytes rk addr sz) (fun '(bytes, tag) => @@ -203,7 +203,7 @@ Definition read_mem_bytes {rv A E} rk (addr : mword A) sz : monad rv (list memor Read_mem rk (Word.wordToNat (get_word addr)) (Z.to_nat sz) returnm. (*val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e*) -Definition read_mem {rv A B E} `{ArithFact (B >= 0)} rk (addrsz : Z) (addr : mword A) sz : monad rv (mword B) E := +Definition read_mem {rv A B E} `{ArithFact (B >=? 0)} rk (addrsz : Z) (addr : mword A) sz : monad rv (mword B) E := bind (read_mem_bytes rk addr sz) (fun bytes => diff --git a/lib/coq/Sail2_real.v b/lib/coq/Sail2_real.v index 494e36d4..4800f18b 100644 --- a/lib/coq/Sail2_real.v +++ b/lib/coq/Sail2_real.v @@ -34,3 +34,74 @@ Definition pow_real := powerRZ. Definition print_real (_ : string) (_ : R) : unit := tt. Definition prerr_real (_ : string) (_ : R) : unit := tt. + + + + +Lemma IZRdiv m n : + 0 < m -> 0 < n -> + (IZR (m / n) <= IZR m / IZR n)%R. +intros. +apply Rmult_le_reg_l with (r := IZR n). +auto using IZR_lt. +unfold Rdiv. +rewrite <- Rmult_assoc. +rewrite Rinv_r_simpl_m. +rewrite <- mult_IZR. +apply IZR_le. +apply Z.mul_div_le. +assumption. +discrR. +omega. +Qed. + +(* One annoying use of reals in the ARM spec I've been looking at. *) +Lemma round_up_div m n : + 0 < m -> 0 < n -> + round_up (div_real (to_real m) (to_real n)) = (m + n - 1) / n. +intros. +unfold round_up, round_down, div_real, to_real. +apply Z.eq_opp_l. +apply Z.sub_move_r. +symmetry. +apply up_tech. + +rewrite Ropp_Ropp_IZR. +apply Ropp_le_contravar. +apply Rmult_le_reg_l with (r := IZR n). +auto using IZR_lt. +unfold Rdiv. +rewrite <- Rmult_assoc. +rewrite Rinv_r_simpl_m. +rewrite <- mult_IZR. +apply IZR_le. +assert (diveq : n*((m+n-1)/n) = (m+n-1) - (m+n-1) mod n). +apply Zplus_minus_eq. +rewrite (Z.add_comm ((m+n-1) mod n)). +apply Z.div_mod. +omega. +rewrite diveq. +assert (modmax : (m+n-1) mod n < n). +specialize (Z.mod_pos_bound (m+n-1) n). intuition. +omega. + +discrR; omega. + +rewrite <- Z.opp_sub_distr. +rewrite Ropp_Ropp_IZR. +apply Ropp_lt_contravar. +apply Rmult_lt_reg_l with (r := IZR n). +auto using IZR_lt. +unfold Rdiv. +rewrite <- Rmult_assoc. +rewrite Rinv_r_simpl_m. +2: { discrR. omega. } +rewrite <- mult_IZR. +apply IZR_lt. +rewrite Z.mul_sub_distr_l. +apply Z.le_lt_trans with (m := m+n-1-n*1). +apply Z.sub_le_mono_r. +apply Z.mul_div_le. +assumption. +omega. +Qed. diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v index 618ca3a5..7c751bc7 100644 --- a/lib/coq/Sail2_state.v +++ b/lib/coq/Sail2_state.v @@ -30,6 +30,33 @@ Fixpoint foreachS {A RV Vars E} (xs : list A) (vars : Vars) (body : A -> Vars -> foreachS xs vars body end. +Fixpoint foreach_ZS_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 -> monadS rv Vars e) {struct n} : monadS rv Vars e. +exact ( + match sumbool_of_bool (from + off <=? to) with left LE => + match n with + | O => returnS vars + | S n => body (from + off) _ vars >>$= fun vars => foreach_ZS_up' rv e Vars from to step (off + step) n _ _ vars body + end + | right _ => returnS vars + end). +Defined. + +Fixpoint foreach_ZS_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 -> monadS rv Vars e) {struct n} : monadS rv Vars e. +exact ( + match sumbool_of_bool (to <=? from + off) with left LE => + match n with + | O => returnS vars + | S n => body (from + off) _ vars >>$= fun vars => foreach_ZS_down' _ _ _ from to step (off - step) n _ _ vars body + end + | right _ => returnS vars + end). +Defined. + +Definition foreach_ZS_up {rv e Vars} from to step vars body `{ArithFact (0 <? step)} := + foreach_ZS_up' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. +Definition foreach_ZS_down {rv e Vars} from to step vars body `{ArithFact (0 <? step)} := + foreach_ZS_down' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. + (*val genlistS : forall 'a 'rv 'e. (nat -> monadS 'rv 'a 'e) -> nat -> monadS 'rv (list 'a) 'e*) Definition genlistS {A RV E} (f : nat -> monadS RV A E) n : monadS RV (list A) E := let indices := List.seq 0 n in @@ -43,22 +70,22 @@ Definition and_boolS {RV E} (l r : monadS RV bool E) : monadS RV bool E := Definition or_boolS {RV E} (l r : monadS RV bool E) : monadS RV bool E := l >>$= (fun l => if l then returnS true else r). -Definition and_boolSP {rv E} {P Q R:bool->Prop} (x : monadS rv {b:bool & ArithFact (P b)} E) (y : monadS rv {b:bool & ArithFact (Q b)} E) - `{H:ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r))} - : monadS rv {b:bool & ArithFact (R b)} E := - x >>$= fun '(existT _ x p) => (if x return ArithFact (P x) -> _ then +Definition and_boolSP {rv E} {P Q R:bool->Prop} (x : monadS rv {b:bool & ArithFactP (P b)} E) (y : monadS rv {b:bool & ArithFactP (Q b)} E) + `{H:forall l r, ArithFactP ((P l) -> ((l = true -> (Q r)) -> (R (andb l r))))} + : monadS rv {b:bool & ArithFactP (R b)} E := + x >>$= fun '(existT _ x p) => (if x return ArithFactP (P x) -> _ then fun p => y >>$= fun '(existT _ y q) => returnS (existT _ y (and_bool_full_proof p q H)) else fun p => returnS (existT _ false (and_bool_left_proof p H))) p. -Definition or_boolSP {rv E} {P Q R:bool -> Prop} (l : monadS rv {b : bool & ArithFact (P b)} E) (r : monadS rv {b : bool & ArithFact (Q b)} E) - `{ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r))} - : monadS rv {b : bool & ArithFact (R b)} E := +Definition or_boolSP {rv E} {P Q R:bool -> Prop} (l : monadS rv {b : bool & ArithFactP (P b)} E) (r : monadS rv {b : bool & ArithFactP (Q b)} E) + `{forall l r, ArithFactP ((P l) -> (((l = false) -> (Q r)) -> (R (orb l r))))} + : monadS rv {b : bool & ArithFactP (R b)} E := l >>$= fun '(existT _ l p) => - (if l return ArithFact (P l) -> _ then fun p => returnS (existT _ true (or_bool_left_proof p H)) + (if l return ArithFactP (P l) -> _ then fun p => returnS (existT _ true (or_bool_left_proof p H)) else fun p => r >>$= fun '(existT _ r q) => returnS (existT _ r (or_bool_full_proof p q H))) p. -Definition build_trivial_exS {rv E} {T:Type} (x : monadS rv T E) : monadS rv {x : T & ArithFact True} E := - x >>$= fun x => returnS (existT _ x (Build_ArithFact _ I)). +Definition build_trivial_exS {rv E} {T:Type} (x : monadS rv T E) : monadS rv {x : T & ArithFact true} E := + x >>$= fun x => returnS (existT _ x (Build_ArithFactP _ eq_refl)). (*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e*) Definition bool_of_bitU_fail {RV E} (b : bitU) : monadS RV bool E := @@ -84,12 +111,12 @@ Definition bools_of_bits_nondetS {RV E} bits : monadS RV (list bool) E := returnS (bools ++ [b]))). (*val of_bits_nondetS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e*) -Definition of_bits_nondetS {RV A E} bits `{ArithFact (A >= 0)} : monadS RV (mword A) E := +Definition of_bits_nondetS {RV A E} bits `{ArithFact (A >=? 0)} : monadS RV (mword A) E := bools_of_bits_nondetS bits >>$= (fun bs => returnS (of_bools bs)). (*val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e*) -Definition of_bits_failS {RV A E} bits `{ArithFact (A >= 0)} : monadS RV (mword A) E := +Definition of_bits_failS {RV A E} bits `{ArithFact (A >=? 0)} : monadS RV (mword A) E := maybe_failS "of_bits" (of_bits bits). (*val mword_nondetS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e @@ -169,7 +196,7 @@ Fixpoint undefined_word_natS {rv e} n : monadS rv (Word.word n) e := returnS (Word.WS b t) end. -Definition undefined_bitvectorS {rv e} n `{ArithFact (n >= 0)} : monadS rv (mword n) e := +Definition undefined_bitvectorS {rv e} n `{ArithFact (n >=? 0)} : monadS rv (mword n) e := undefined_word_natS (Z.to_nat n) >>$= fun w => returnS (word_to_mword w). diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v index dd83f239..ef82084f 100644 --- a/lib/coq/Sail2_state_lemmas.v +++ b/lib/coq/Sail2_state_lemmas.v @@ -28,6 +28,42 @@ Add Parametric Morphism {Regs A Vars E : Type} : (@foreachS A Regs Vars E) apply foreachS_cong. Qed. +Lemma foreach_ZS_up_cong rv e Vars from to step vars body body' H : + (forall a pf vars, body a pf vars === body' a pf vars) -> + @foreach_ZS_up rv e Vars from to step vars body H === foreach_ZS_up from to step vars body'. +intro EQ. +unfold foreach_ZS_up. +match goal with +| |- @foreach_ZS_up' _ _ _ _ _ _ _ _ _ ?pf _ _ === _ => generalize pf +end. +generalize 0 at 2 3 4 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros; simpl. +* reflexivity. +* destruct (sumbool_of_bool (from + off <=? to)); auto. + rewrite EQ. + setoid_rewrite IHn. + reflexivity. +Qed. + +Lemma foreach_ZS_down_cong rv e Vars from to step vars body body' H : + (forall a pf vars, body a pf vars === body' a pf vars) -> + @foreach_ZS_down rv e Vars from to step vars body H === foreach_ZS_down from to step vars body'. +intro EQ. +unfold foreach_ZS_down. +match goal with +| |- @foreach_ZS_down' _ _ _ _ _ _ _ _ _ ?pf _ _ === _ => generalize pf +end. +generalize 0 at 1 3 4 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros; simpl. +* reflexivity. +* destruct (sumbool_of_bool (to <=? from + off)); auto. + rewrite EQ. + setoid_rewrite IHn. + reflexivity. +Qed. + Local Opaque _limit_reduces. Ltac gen_reduces := match goal with |- context[@_limit_reduces ?a ?b ?c] => generalize (@_limit_reduces a b c) end. @@ -160,8 +196,15 @@ Lemma build_trivial_exS_cong {RV T E} x x' : @build_trivial_exS RV T E x === build_trivial_exS x'. intros E1. unfold build_trivial_exS. -rewrite E1. -reflexivity. +apply bindS_cong; auto. +Qed. + +Lemma liftRS_cong {A R Regs E} m m' : + m === m' -> + @liftRS A R Regs E m === liftRS m'. +intros E1. +unfold liftRS. +apply try_catchS_cong; auto. Qed. (* Monad lifting *) @@ -227,11 +270,15 @@ Ltac statecong db := let ty := type of x in match ty with | bool => eapply if_bool_cong; statecong db - | sumbool _ _ => eapply if_sumbool_cong; statecong db + | sumbool _ _ => eapply if_sumbool_cong; statecong db (* There's also a dependent case below *) | _ => apply equiv_reflexive end | |- (foreachS _ _ _) === _ => solve [ eapply foreachS_cong; intros; statecong db ] + | |- (foreach_ZS_up _ _ _ _ _) === _ => + solve [ eapply foreach_ZS_up_cong; intros; statecong db ] + | |- (foreach_ZS_down _ _ _ _ _) === _ => + solve [ eapply foreach_ZS_down_cong; intros; statecong db ] | |- (genlistS _ _) === _ => solve [ eapply genlistS_cong; intros; statecong db ] | |- (whileST _ _ _ _) === _ => @@ -248,6 +295,8 @@ Ltac statecong db := solve [ eapply or_boolSP_cong; intros; statecong db ] | |- (build_trivial_exS _) === _ => solve [ eapply build_trivial_exS_cong; intros; statecong db ] + | |- (liftRS _) === _ => + solve [ eapply liftRS_cong; intros; statecong db ] | |- (let '(matchvar1, matchvar2) := ?e1 in _) === _ => eapply (@equiv_transitive _ _ _ _ (let '(matchvar1,matchvar2) := e1 in _) _); [ destruct e1; etransitivity; [ statecong db | apply equiv_reflexive ] @@ -260,6 +309,10 @@ Ltac statecong db := eapply (@equiv_transitive _ _ _ _ (match e1 with None => _ | Some _ => _ end) _); [ destruct e1; [> etransitivity; [> statecong db | apply equiv_reflexive ] ..] | apply equiv_reflexive ] + | |- (match ?e1 with left _ => _ | right _ => _ end) === _ => + eapply (@equiv_transitive _ _ _ _ (match e1 with left _ => _ | right _ => _ end) _); + [ destruct e1; [> etransitivity; [> statecong db | apply equiv_reflexive ] ..] + | apply equiv_reflexive ] | |- ?X => solve [ apply equiv_reflexive @@ -316,6 +369,19 @@ Hint Extern 0 (liftState _ ?t = _) => end end : liftState. +Lemma liftState_match_distrib_sumbool {Regs Regval A E P Q r x y} {c : sumbool P Q} : + @liftState Regs Regval A E r (match c with left H => x H | right H => y H end) = match c with left H => liftState r (x H) | right H => liftState r (y H) end. +destruct c; reflexivity. +Qed. +(* As above, but also need to beta reduce H into x and y. *) +Hint Extern 0 (liftState _ ?t = _) => + match t with + | match ?x with _ => _ end => + match type of x with + | sumbool _ _ => etransitivity; [apply liftState_match_distrib_sumbool | cbv beta; reflexivity ] + end + end : liftState. + Lemma liftState_let_pair Regs RegVal A B C E r (x : B * C) M : @liftState Regs RegVal A E r (let '(y, z) := x in M y z) = let '(y, z) := x in liftState r (M y z). @@ -456,6 +522,8 @@ Lemma liftState_build_trivial_ex Regs Regval E T r m : @liftState Regs Regval _ E r (@build_trivial_ex _ _ T m) === build_trivial_exS (liftState r m). unfold build_trivial_ex, build_trivial_exS. +unfold ArithFact. +intro. rewrite liftState_bind. reflexivity. Qed. @@ -656,6 +724,52 @@ Qed. Hint Rewrite liftState_foreachM : liftState. Hint Resolve liftState_foreachM : liftState. +Lemma liftState_foreach_ZM_up Regs Regval Vars E from to step vars body H r : + liftState (Regs := Regs) r + (@foreach_ZM_up Regval E Vars from to step vars body H) === + foreach_ZS_up from to step vars (fun z H' a => liftState r (body z H' a)). +unfold foreach_ZM_up, foreach_ZS_up. +match goal with +| |- liftState _ (@foreach_ZM_up' _ _ _ _ _ _ _ _ _ ?pf _ _) === _ => generalize pf +end. +generalize 0 at 2 3 4 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros. +* simpl. + rewrite_liftState. + reflexivity. +* simpl. + rewrite_liftState. + destruct (sumbool_of_bool (from + off <=? to)); auto. + repeat replace_ArithFact_proof. + reflexivity. +Qed. +Hint Rewrite liftState_foreach_ZM_up : liftState. +Hint Resolve liftState_foreach_ZM_up : liftState. + +Lemma liftState_foreach_ZM_down Regs Regval Vars E from to step vars body H r : + liftState (Regs := Regs) r + (@foreach_ZM_down Regval E Vars from to step vars body H) === + foreach_ZS_down from to step vars (fun z H' a => liftState r (body z H' a)). +unfold foreach_ZM_down, foreach_ZS_down. +match goal with +| |- liftState _ (@foreach_ZM_down' _ _ _ _ _ _ _ _ _ ?pf _ _) === _ => generalize pf +end. +generalize 0 at 1 3 4 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros. +* simpl. + rewrite_liftState. + reflexivity. +* simpl. + rewrite_liftState. + destruct (sumbool_of_bool (to <=? from + off)); auto. + repeat replace_ArithFact_proof. + reflexivity. +Qed. +Hint Rewrite liftState_foreach_ZM_down : liftState. +Hint Resolve liftState_foreach_ZM_down : liftState. + Lemma liftState_genlistM Regs Regval A E r f n : liftState (Regs := Regs) r (@genlistM A Regval E f n) === genlistS (fun x => liftState r (f x)) n. unfold genlistM, genlistS. @@ -706,7 +820,7 @@ Qed. Hint Rewrite liftState_undefined_word_nat : liftState. Hint Resolve liftState_undefined_word_nat : liftState. -Lemma liftState_undefined_bitvector Regs Regval E r n `{ArithFact (n >= 0)} : +Lemma liftState_undefined_bitvector Regs Regval E r n `{ArithFact (n >=? 0)} : liftState (Regs := Regs) (Regval := Regval) (E := E) r (undefined_bitvector n) === undefined_bitvectorS n. unfold undefined_bitvector, undefined_bitvectorS. rewrite_liftState. 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). diff --git a/lib/coq/Sail2_state_monad_lemmas.v b/lib/coq/Sail2_state_monad_lemmas.v index e9ab36c1..c834a0cb 100644 --- a/lib/coq/Sail2_state_monad_lemmas.v +++ b/lib/coq/Sail2_state_monad_lemmas.v @@ -22,8 +22,8 @@ Global Instance refl_eq_subrelation {A : Type} {R : A -> A -> Prop} `{Reflexive intros x y EQ. subst. reflexivity. Qed. -Hint Extern 4 (_ === _) => reflexivity. -Hint Extern 4 (_ === _) => symmetry. +Hint Extern 4 (_ === _) => reflexivity : core. +Hint Extern 4 (_ === _) => symmetry : core. diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v index a0a23933..1e1b445b 100644 --- a/lib/coq/Sail2_string.v +++ b/lib/coq/Sail2_string.v @@ -8,15 +8,15 @@ Definition string_startswith s expected := let prefix := String.substring 0 (String.length expected) s in generic_eq prefix expected. -Definition string_drop s (n : Z) `{ArithFact (n >= 0)} := +Definition string_drop s (n : Z) `{ArithFact (n >=? 0)} := let n := Z.to_nat n in String.substring n (String.length s - n) s. -Definition string_take s (n : Z) `{ArithFact (n >= 0)} := +Definition string_take s (n : Z) `{ArithFact (n >=? 0)} := let n := Z.to_nat n in String.substring 0 n s. -Definition string_length s : {n : Z & ArithFact (n >= 0)} := +Definition string_length s : {n : Z & ArithFact (n >=? 0)} := build_ex (Z.of_nat (String.length s)). Definition string_append := String.append. @@ -56,7 +56,7 @@ match s with else (acc, len) end end. -Local Definition int_of (s : string) (base : Z) (len : nat) : option (Z * {n : Z & ArithFact (n >= 0)}) := +Local Definition int_of (s : string) (base : Z) (len : nat) : option (Z * {n : Z & ArithFact (n >=? 0)}) := match s with | EmptyString => None | String h t => @@ -74,7 +74,7 @@ end. (* I've stuck closely to OCaml's int_of_string, because that's what's currently used elsewhere. *) -Definition maybe_int_of_prefix (s : string) : option (Z * {n : Z & ArithFact (n >= 0)}) := +Definition maybe_int_of_prefix (s : string) : option (Z * {n : Z & ArithFact (n >=? 0)}) := match s with | EmptyString => None | String "0" (String ("x"|"X") t) => int_of t 16 2 @@ -105,16 +105,16 @@ Fixpoint n_leading_spaces (s:string) : nat := | _ => 0 end. -Definition opt_spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >= 0)}) := +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)}) := +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. -Definition hex_bits_n_matches_prefix sz `{ArithFact (sz >= 0)} s : option (mword sz * {n : Z & ArithFact (n >= 0)}) := +Definition hex_bits_n_matches_prefix sz `{ArithFact (sz >=? 0)} s : option (mword sz * {n : Z & ArithFact (n >=? 0)}) := match maybe_int_of_prefix s with | None => None | Some (n, len) => @@ -180,6 +180,23 @@ match z with | Zneg p => String "-" (string_of_N (pos_limit p) (Npos p) "") end. +Local Definition asciiA : N := Ascii.N_of_ascii "A". +Local Fixpoint hex_string_of_N (limit : nat) (n : N) (acc : string) : string := +match limit with +| O => acc +| S limit' => + let (d,m) := N.div_eucl n 16 in + let digit := if 10 <=? m then m - 10 + asciiA else m + zero in + let acc := String (Ascii.ascii_of_N digit) acc in + if N.ltb 0 d then hex_string_of_N limit' d acc else acc +end%N. +Definition hex_string_of_int (z : Z) : string := +match z with +| Z0 => "0" +| Zpos p => hex_string_of_N (pos_limit p) (Npos p) "" +| Zneg p => String "-" (hex_string_of_N (pos_limit p) (Npos p) "") +end. + Definition decimal_string_of_bv {a} `{Bitvector a} (bv : a) : string := match unsigned bv with | None => "?" @@ -191,4 +208,5 @@ Definition decimal_string_of_bits {n} (bv : mword n) : string := decimal_string_ (* Some aliases for compatibility. *) Definition dec_str := string_of_int. +Definition hex_str := hex_string_of_int. Definition concat_str := String.append. diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index b29963b6..9b76ce62 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -5,6 +5,7 @@ Require Export ZArith. Require Import Ascii. Require Export String. Require Import bbv.Word. +Require Export bbv.HexNotationWord. Require Export List. Require Export Sumbool. Require Export DecidableClass. @@ -14,6 +15,7 @@ Require Import Lia. Import ListNotations. Open Scope Z. +Open Scope bool. Module Z_eq_dec. Definition U := Z. @@ -26,27 +28,74 @@ Module ZEqdep := DecidableEqDep (Z_eq_dec). can be added to, and a typeclass to wrap constraint arguments in to trigger automatic solving. *) Create HintDb sail. -Class ArithFact (P : Prop) := { fact : P }. -Lemma use_ArithFact {P} `(ArithFact P) : P. +(* Facts translated from Sail's type system are wrapped in ArithFactP or + ArithFact so that the solver can be invoked automatically by Coq's + typeclass mechanism. Most properties are boolean, which enjoys proof + irrelevance by UIP. *) +Class ArithFactP (P : Prop) := { fact : P }. +Class ArithFact (P : bool) := ArithFactClass : ArithFactP (P = true). +Lemma use_ArithFact {P} `(ArithFact P) : P = true. +unfold ArithFact in *. apply fact. Defined. +Lemma ArithFact_irrelevant (P : bool) (p q : ArithFact P) : p = q. +destruct p,q. +f_equal. +apply Eqdep_dec.UIP_dec. +apply Bool.bool_dec. +Qed. + +Ltac replace_ArithFact_proof := + match goal with |- context[?x] => + match tt with + | _ => is_var x; fail 1 + | _ => + match type of x with ArithFact ?P => + let pf := fresh "pf" in + generalize x as pf; intro pf; + repeat multimatch goal with |- context[?y] => + match type of y with ArithFact P => + match y with + | pf => idtac + | _ => rewrite <- (ArithFact_irrelevant P pf y) + end + end + end + end + end + end. + +Ltac generalize_ArithFact_proof_in H := + match type of H with context f [?x] => + match type of x with ArithFactP (?P = true) => + let pf := fresh "pf" in + cut (forall (pf : ArithFact P), ltac:(let t := context f[pf] in exact t)); + [ clear H; intro H + | intro pf; rewrite <- (ArithFact_irrelevant P x pf); apply H ] + | ArithFact ?P => + let pf := fresh "pf" in + cut (forall (pf : ArithFact P), ltac:(let t := context f[pf] in exact t)); + [ clear H; intro H + | intro pf; rewrite <- (ArithFact_irrelevant P x pf); apply H ] + end + end. + (* Allow setoid rewriting through ArithFact *) Require Import Coq.Classes.Morphisms. Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. + Section Morphism. Local Obligation Tactic := try solve [simpl_relation | firstorder auto]. - -Global Program Instance ArithFact_iff_morphism : - Proper (iff ==> iff) ArithFact. +Global Program Instance ArithFactP_iff_morphism : + Proper (iff ==> iff) ArithFactP. End Morphism. - -Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} := +Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFactP (P n)} : {x : T & ArithFactP (P x)} := existT _ n H. -Definition build_ex2 {T:Type} {T':T -> Type} (n:T) (m:T' n) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & T' x & ArithFact (P x)} := +Definition build_ex2 {T:Type} {T':T -> Type} (n:T) (m:T' n) {P:T -> Prop} `{H:ArithFactP (P n)} : {x : T & T' x & ArithFactP (P x)} := existT2 _ _ n m H. Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness. @@ -75,23 +124,25 @@ destruct Decidable_witness; simpl in *; congruence. Qed. Instance Decidable_eq_from_dec {T:Type} (eqdec: forall x y : T, {x = y} + {x <> y}) : - forall (x y : T), Decidable (eq x y) := { + forall (x y : T), Decidable (eq x y). +refine (fun x y => {| Decidable_witness := proj1_sig (bool_of_sumbool (eqdec x y)) -}. +|}). destruct (eqdec x y); simpl; split; congruence. Defined. -Instance Decidable_eq_unit : forall (x y : unit), Decidable (x = y) := - { Decidable_witness := true }. +Instance Decidable_eq_unit : forall (x y : unit), Decidable (x = y). +refine (fun x y => {| Decidable_witness := true |}). destruct x, y; split; auto. Defined. Instance Decidable_eq_string : forall (x y : string), Decidable (x = y) := Decidable_eq_from_dec String.string_dec. -Instance Decidable_eq_pair {A B : Type} `(DA : forall x y : A, Decidable (x = y), DB : forall x y : B, Decidable (x = y)) : forall x y : A*B, Decidable (x = y) := -{ Decidable_witness := andb (@Decidable_witness _ (DA (fst x) (fst y))) -(@Decidable_witness _ (DB (snd x) (snd y))) }. +Instance Decidable_eq_pair {A B : Type} `(DA : forall x y : A, Decidable (x = y), DB : forall x y : B, Decidable (x = y)) : forall x y : A*B, Decidable (x = y). +refine (fun x y => +{| Decidable_witness := andb (@Decidable_witness _ (DA (fst x) (fst y))) + (@Decidable_witness _ (DB (snd x) (snd y))) |}). destruct x as [x1 x2]. destruct y as [y1 y2]. simpl. @@ -130,16 +181,20 @@ Ltac cmp_record_field x y := ]. +Notation "x <=? y <=? z" := ((x <=? y) && (y <=? z)) (at level 70, y at next level) : Z_scope. +Notation "x <=? y <? z" := ((x <=? y) && (y <? z)) (at level 70, y at next level) : Z_scope. +Notation "x <? y <? z" := ((x <? y) && (y <? z)) (at level 70, y at next level) : Z_scope. +Notation "x <? y <=? z" := ((x <? y) && (y <=? z)) (at level 70, y at next level) : Z_scope. (* Project away range constraints in comparisons *) -Definition ltb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.ltb (projT1 l) r. -Definition leb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.leb (projT1 l) r. -Definition gtb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.gtb (projT1 l) r. -Definition geb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.geb (projT1 l) r. -Definition ltb_range_r {lo hi} l (r : {x & ArithFact (lo <= x /\ x <= hi)}) := Z.ltb l (projT1 r). -Definition leb_range_r {lo hi} l (r : {x & ArithFact (lo <= x /\ x <= hi)}) := Z.leb l (projT1 r). -Definition gtb_range_r {lo hi} l (r : {x & ArithFact (lo <= x /\ x <= hi)}) := Z.gtb l (projT1 r). -Definition geb_range_r {lo hi} l (r : {x & ArithFact (lo <= x /\ x <= hi)}) := Z.geb l (projT1 r). +Definition ltb_range_l {lo hi} (l : {x & ArithFact (lo <=? x <=? hi)}) r := Z.ltb (projT1 l) r. +Definition leb_range_l {lo hi} (l : {x & ArithFact (lo <=? x <=? hi)}) r := Z.leb (projT1 l) r. +Definition gtb_range_l {lo hi} (l : {x & ArithFact (lo <=? x <=? hi)}) r := Z.gtb (projT1 l) r. +Definition geb_range_l {lo hi} (l : {x & ArithFact (lo <=? x <=? hi)}) r := Z.geb (projT1 l) r. +Definition ltb_range_r {lo hi} l (r : {x & ArithFact (lo <=? x <=? hi)}) := Z.ltb l (projT1 r). +Definition leb_range_r {lo hi} l (r : {x & ArithFact (lo <=? x <=? hi)}) := Z.leb l (projT1 r). +Definition gtb_range_r {lo hi} l (r : {x & ArithFact (lo <=? x <=? hi)}) := Z.gtb l (projT1 r). +Definition geb_range_r {lo hi} l (r : {x & ArithFact (lo <=? x <=? hi)}) := Z.geb l (projT1 r). Definition ii := Z. Definition nn := nat. @@ -147,23 +202,23 @@ Definition nn := nat. (*val pow : Z -> Z -> Z*) Definition pow m n := m ^ n. -Program Definition pow2 n : {z : Z & ArithFact (2 ^ n <= z <= 2 ^ n)} := existT _ (pow 2 n) _. +Program Definition pow2 n : {z : Z & ArithFact (2 ^ n <=? z <=? 2 ^ n)} := existT _ (pow 2 n) _. Next Obligation. constructor. unfold pow. -auto using Z.le_refl. +auto using Z.leb_refl with bool. Qed. -Lemma ZEuclid_div_pos : forall x y, y > 0 -> x >= 0 -> ZEuclid.div x y >= 0. +Lemma ZEuclid_div_pos : forall x y, 0 < y -> 0 <= x -> 0 <= ZEuclid.div x y. intros. unfold ZEuclid.div. change 0 with (0 * 0). -apply Zmult_ge_compat; auto with zarith. -* apply Z.le_ge. apply Z.sgn_nonneg. apply Z.ge_le. auto with zarith. -* apply Z_div_ge0; auto. apply Z.lt_gt. apply Z.abs_pos. auto with zarith. +apply Zmult_le_compat; auto with zarith. +* apply Z.sgn_nonneg. auto with zarith. +* apply Z_div_pos; auto. apply Z.lt_gt. apply Z.abs_pos. auto with zarith. Qed. -Lemma ZEuclid_pos_div : forall x y, y > 0 -> ZEuclid.div x y >= 0 -> x >= 0. +Lemma ZEuclid_pos_div : forall x y, 0 < y -> 0 <= ZEuclid.div x y -> 0 <= x. intros x y GT. specialize (ZEuclid.div_mod x y); specialize (ZEuclid.mod_always_pos x y); @@ -204,6 +259,13 @@ Qed. Hint Resolve ZEuclid_div_pos ZEuclid_pos_div ZEuclid_div_ge ZEuclid_div_mod0 : sail. +Lemma Z_geb_ge n m : (n >=? m) = true <-> n >= m. +rewrite Z.geb_leb. +split. +* intro. apply Z.le_ge, Z.leb_le. assumption. +* intro. apply Z.ge_le in H. apply Z.leb_le. assumption. +Qed. + (* Definition inline lt := (<) @@ -815,19 +877,25 @@ apply Z2Nat.inj_lt. Close Scope nat. (*val access_list_inc : forall a. list a -> Z -> a*) -Definition access_list_inc {A} (xs : list A) n `{ArithFact (0 <= n)} `{ArithFact (n < length_list xs)} := nth_in_range (Z.to_nat n) xs (nth_Z_nat (use_ArithFact _) (use_ArithFact _)). +Definition access_list_inc {A} (xs : list A) n `{ArithFact (0 <=? n)} `{ArithFact (n <? length_list xs)} : A. +refine (nth_in_range (Z.to_nat n) xs (nth_Z_nat _ _)). +* apply Z.leb_le. + auto using use_ArithFact. +* apply Z.ltb_lt. + auto using use_ArithFact. +Defined. (*val access_list_dec : forall a. list a -> Z -> a*) -Definition access_list_dec {A} (xs : list A) n `{ArithFact (0 <= n)} `{ArithFact (n < length_list xs)} : A. +Definition access_list_dec {A} (xs : list A) n `{H1:ArithFact (0 <=? n)} `{H2:ArithFact (n <? length_list xs)} : A. refine ( let top := (length_list xs) - 1 in @access_list_inc A xs (top - n) _ _). -constructor. apply use_ArithFact in H. apply use_ArithFact in H0. omega. -constructor. apply use_ArithFact in H. apply use_ArithFact in H0. omega. +abstract (constructor; apply use_ArithFact, Z.leb_le in H1; apply use_ArithFact, Z.ltb_lt in H2; apply Z.leb_le; omega). +abstract (constructor; apply use_ArithFact, Z.leb_le in H1; apply use_ArithFact, Z.ltb_lt in H2; apply Z.ltb_lt; omega). Defined. (*val access_list : forall a. bool -> list a -> Z -> a*) -Definition access_list {A} (is_inc : bool) (xs : list A) n `{ArithFact (0 <= n)} `{ArithFact (n < length_list xs)} := +Definition access_list {A} (is_inc : bool) (xs : list A) n `{ArithFact (0 <=? n)} `{ArithFact (n <? length_list xs)} := if is_inc then access_list_inc xs n else access_list_dec xs n. Definition access_list_opt_inc {A} (xs : list A) n := nth_error xs (Z.to_nat n). @@ -884,15 +952,15 @@ match n with | Zpos _ => fun f w => f w end. -Program Definition to_word {n} : n >= 0 -> word (Z.to_nat n) -> mword n := +Program Definition to_word {n} : n >=? 0 = true -> word (Z.to_nat n) -> mword n := match n with | Zneg _ => fun H _ => _ | Z0 => fun _ w => w | Zpos _ => fun _ w => w end. -Definition word_to_mword {n} (w : word (Z.to_nat n)) `{H:ArithFact (n >= 0)} : mword n := - to_word (match H with Build_ArithFact _ H' => H' end) w. +Definition word_to_mword {n} (w : word (Z.to_nat n)) `{H:ArithFact (n >=? 0)} : mword n := + to_word (use_ArithFact H) w. (*val length_mword : forall a. mword a -> Z*) Definition length_mword {n} (w : mword n) := n. @@ -968,7 +1036,7 @@ Definition update_mword {a} (is_inc : bool) (w : mword a) n b := if is_inc then update_mword_inc w n b else update_mword_dec w n b. (*val int_of_mword : forall 'a. bool -> mword 'a -> integer*) -Definition int_of_mword {a} `{ArithFact (a >= 0)} (sign : bool) (w : mword a) := +Definition int_of_mword {a} `{ArithFact (a >=? 0)} (sign : bool) (w : mword a) := if sign then wordToZ (get_word w) else Z.of_N (wordToN (get_word w)). @@ -977,16 +1045,18 @@ Definition mword_of_int len n := let w := wordFromInteger n in if (length_mword w = len) then w else failwith "unexpected word length" *) -Program Definition mword_of_int {len} `{H:ArithFact (len >= 0)} n : mword len := +Program Definition mword_of_int {len} `{H:ArithFact (len >=? 0)} n : mword len := match len with | Zneg _ => _ | Z0 => ZToWord 0 n | Zpos p => ZToWord (Pos.to_nat p) n end. Next Obligation. -destruct H. -auto. +destruct H as [H]. +unfold Z.geb, Z.compare in H. +discriminate. Defined. + (* (* Translating between a type level number (itself n) and an integer *) @@ -1055,20 +1125,9 @@ Instance bitlist_Bitvector {a : Type} `{BitU a} : (Bitvector (list a)) := { }. Class ReasonableSize (a : Z) : Prop := { - isPositive : a >= 0 + isPositive : a >=? 0 = true }. -(* Omega doesn't know about In, but can handle disjunctions. *) -Ltac unfold_In := -repeat match goal with -| H:context [member_Z_list _ _ = true] |- _ => rewrite member_Z_list_In in H -| H:context [In ?x (?y :: ?t)] |- _ => change (In x (y :: t)) with (y = x \/ In x t) in H -| H:context [In ?x []] |- _ => change (In x []) with False in H -| |- context [member_Z_list _ _ = true] => rewrite member_Z_list_In -| |- context [In ?x (?y :: ?t)] => change (In x (y :: t)) with (y = x \/ In x t) -| |- context [In ?x []] => change (In x []) with False -end. - (* Definitions in the context that involve proof for other constraints can break some of the constraint solving tactics, so prune definition bodies down to integer types. *) @@ -1081,17 +1140,54 @@ repeat match goal with X := _ |- _ => match goal with _ : context[X] |- _ => idtac end || clear X end. -Lemma ArithFact_mword (a : Z) (w : mword a) : ArithFact (a >= 0). +Lemma lift_bool_exists (l r : bool) (P : bool -> Prop) : + (l = r -> exists x, P x) -> + (exists x, l = r -> P x). +intro H. +destruct (Bool.bool_dec l r) as [e | ne]. +* destruct (H e) as [x H']; eauto. +* exists true; tauto. +Qed. + +Lemma ArithFact_mword (a : Z) (w : mword a) : ArithFact (a >=? 0). constructor. destruct a. auto with zarith. auto using Z.le_ge, Zle_0_pos. destruct w. Qed. +(* Remove constructor from ArithFact(P)s and if they're used elsewhere + in the context create a copy that rewrites will work on. *) Ltac unwrap_ArithFacts := - repeat match goal with H:(ArithFact _) |- _ => let H' := fresh H in case H as [H']; clear H end. + let gen X := + let Y := fresh "Y" in pose X as Y; generalize Y + in + let unwrap H := + let H' := fresh H in case H as [H']; clear H; + match goal with + | _ : context[H'] |- _ => gen H' + | _ := context[H'] |- _ => gen H' + | |- context[H'] => gen H' + | _ => idtac + end + in + repeat match goal with + | H:(ArithFact _) |- _ => unwrap H + | H:(ArithFactP _) |- _ => unwrap H + end. Ltac unbool_comparisons := repeat match goal with + | H:@eq bool _ _ -> @ex bool _ |- _ => apply lift_bool_exists in H; destruct H + | H:@ex Z _ |- _ => destruct H + (* Omega doesn't know about In, but can handle disjunctions. *) + | H:context [member_Z_list _ _ = true] |- _ => rewrite member_Z_list_In in H + | H:context [In ?x (?y :: ?t)] |- _ => change (In x (y :: t)) with (y = x \/ In x t) in H + | H:context [In ?x []] |- _ => change (In x []) with False in H + | H:?v = true |- _ => is_var v; subst v + | H:?v = false |- _ => is_var v; subst v + | H:true = ?v |- _ => is_var v; subst v + | H:false = ?v |- _ => is_var v; subst v + | H:_ /\ _ |- _ => destruct H | H:context [Z.geb _ _] |- _ => rewrite Z.geb_leb in H | H:context [Z.gtb _ _] |- _ => rewrite Z.gtb_ltb in H | H:context [Z.leb _ _ = true] |- _ => rewrite Z.leb_le in H @@ -1106,15 +1202,29 @@ Ltac unbool_comparisons := | H:context [andb _ _ = false] |- _ => rewrite Bool.andb_false_iff in H | H:context [negb _ = true] |- _ => rewrite Bool.negb_true_iff in H | H:context [negb _ = false] |- _ => rewrite Bool.negb_false_iff in H + | H:context [Bool.eqb _ ?r = true] |- _ => rewrite Bool.eqb_true_iff in H; + try (is_var r; subst r) + | H:context [Bool.eqb _ _ = false] |- _ => rewrite Bool.eqb_false_iff in H | H:context [generic_eq _ _ = true] |- _ => apply generic_eq_true in H | H:context [generic_eq _ _ = false] |- _ => apply generic_eq_false in H | H:context [generic_neq _ _ = true] |- _ => apply generic_neq_true in H | H:context [generic_neq _ _ = false] |- _ => apply generic_neq_false in H | H:context [_ <> true] |- _ => rewrite Bool.not_true_iff_false in H | H:context [_ <> false] |- _ => rewrite Bool.not_false_iff_true in H + | H:context [@eq bool ?l ?r] |- _ => + lazymatch r with + | true => fail + | false => fail + | _ => rewrite (Bool.eq_iff_eq_true l r) in H + end end. Ltac unbool_comparisons_goal := repeat match goal with + (* Important to have these early in the list - setoid_rewrite can + unfold member_Z_list. *) + | |- context [member_Z_list _ _ = true] => rewrite member_Z_list_In + | |- context [In ?x (?y :: ?t)] => change (In x (y :: t)) with (y = x \/ In x t) + | |- context [In ?x []] => change (In x []) with False | |- context [Z.geb _ _] => setoid_rewrite Z.geb_leb | |- context [Z.gtb _ _] => setoid_rewrite Z.gtb_ltb | |- context [Z.leb _ _ = true] => setoid_rewrite Z.leb_le @@ -1129,12 +1239,20 @@ Ltac unbool_comparisons_goal := | |- context [andb _ _ = false] => setoid_rewrite Bool.andb_false_iff | |- context [negb _ = true] => setoid_rewrite Bool.negb_true_iff | |- context [negb _ = false] => setoid_rewrite Bool.negb_false_iff + | |- context [Bool.eqb _ _ = true] => setoid_rewrite Bool.eqb_true_iff + | |- context [Bool.eqb _ _ = false] => setoid_rewrite Bool.eqb_false_iff | |- context [generic_eq _ _ = true] => apply generic_eq_true | |- context [generic_eq _ _ = false] => apply generic_eq_false | |- context [generic_neq _ _ = true] => apply generic_neq_true | |- context [generic_neq _ _ = false] => apply generic_neq_false | |- context [_ <> true] => setoid_rewrite Bool.not_true_iff_false | |- context [_ <> false] => setoid_rewrite Bool.not_false_iff_true + | |- context [@eq bool _ ?r] => + lazymatch r with + | true => fail + | false => fail + | _ => setoid_rewrite Bool.eq_iff_eq_true + end end. (* Split up dependent pairs to get at proofs of properties *) @@ -1359,10 +1477,12 @@ end; (* We may have uncovered more conjunctions *) repeat match goal with H:and _ _ |- _ => destruct H end. +(* Remove details of embedded proofs. *) Ltac generalize_embedded_proofs := repeat match goal with H:context [?X] |- _ => - match type of X with ArithFact _ => - generalize dependent X + match type of X with + | ArithFact _ => generalize dependent X + | ArithFactP _ => generalize dependent X end end; intros. @@ -1416,7 +1536,6 @@ Ltac prepare_for_solver := unbool_comparisons_goal; repeat match goal with H:and _ _ |- _ => destruct H end; remove_unnecessary_casesplit; - unfold_In; (* after unbool_comparisons to deal with && and || *) reduce_list_lengths; reduce_pow; filter_disjunctions; @@ -1425,9 +1544,9 @@ Ltac prepare_for_solver := subst; clean_up_props. -Lemma trivial_range {x : Z} : ArithFact (x <= x /\ x <= x). +Lemma trivial_range {x : Z} : ArithFact ((x <=? x <=? x)). constructor. -auto with zarith. +auto using Z.leb_refl with bool. Qed. Lemma ArithFact_self_proof {P} : forall x : {y : Z & ArithFact (P y)}, ArithFact (P (projT1 x)). @@ -1435,14 +1554,19 @@ intros [x H]. exact H. Qed. +Lemma ArithFactP_self_proof {P} : forall x : {y : Z & ArithFactP (P y)}, ArithFactP (P (projT1 x)). +intros [x H]. +exact H. +Qed. + Ltac fill_in_evar_eq := - match goal with |- ArithFact (?x = ?y) => + 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 *) (* Disabled because cbn may reduce definitions, even after clearbody 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. + idtac "Warning: unknown equality constraint"; constructor; exact (Z.eqb_refl _ : x =? y = true) end. Ltac bruteforce_bool_exists := match goal with @@ -1477,6 +1601,71 @@ repeat match goal with intros end; nia. +(* Try to get the linear arithmetic solver to do booleans. *) + +Lemma b2z_true x : x = true <-> Z.b2z x = 1. +destruct x; compute; split; congruence. +Qed. + +Lemma b2z_false x : x = false <-> Z.b2z x = 0. +destruct x; compute; split; congruence. +Qed. + +Lemma b2z_tf x : 0 <= Z.b2z x <= 1. +destruct x; simpl; omega. +Qed. + +Lemma b2z_andb a b : + Z.b2z (a && b) = Z.min (Z.b2z a) (Z.b2z b). +destruct a,b; reflexivity. +Qed. +Lemma b2z_orb a b : + Z.b2z (a || b) = Z.max (Z.b2z a) (Z.b2z b). +destruct a,b; reflexivity. +Qed. + +Lemma b2z_eq : forall a b, Z.b2z a = Z.b2z b <-> a = b. +intros [|] [|]; +simpl; +intuition try congruence. +Qed. + +Lemma b2z_negb x : Z.b2z (negb x) = 1 - Z.b2z x. + destruct x ; reflexivity. +Qed. + +Ltac bool_to_Z := + subst; + rewrite ?truefalse, ?falsetrue, ?or_False_l, ?or_False_r in *; + (* I did try phrasing these as rewrites, but Coq was oddly reluctant to use them *) + repeat match goal with + | H:?x = ?x <-> _ |- _ => apply iff_equal_l in H + | H:_ <-> ?x = ?x |- _ => apply iff_equal_r in H + end; + repeat match goal with + | H:context [negb ?v] |- _ => rewrite b2z_negb in H + | |- context [negb ?v] => rewrite b2z_negb + | H:context [?v = true] |- _ => is_var v; rewrite (b2z_true v) in * + | |- context [?v = true] => is_var v; rewrite (b2z_true v) in * + | H:context [?v = false] |- _ => is_var v; rewrite (b2z_false v) in * + | |- context [?v = false] => is_var v; rewrite (b2z_false v) in * + | H:context [?v = ?w] |- _ => rewrite <- (b2z_eq v w) in H + | |- context [?v = ?w] => rewrite <- (b2z_eq v w) + | H:context [Z.b2z (?v && ?w)] |- _ => rewrite (b2z_andb v w) in H + | |- context [Z.b2z (?v && ?w)] => rewrite (b2z_andb v w) + | H:context [Z.b2z (?v || ?w)] |- _ => rewrite (b2z_orb v w) in H + | |- context [Z.b2z (?v || ?w)] => rewrite (b2z_orb v w) + end; + change (Z.b2z true) with 1 in *; + change (Z.b2z false) with 0 in *; + repeat match goal with + | _:context [Z.b2z ?v] |- _ => generalize (b2z_tf v); generalize dependent (Z.b2z v) + | |- context [Z.b2z ?v] => generalize (b2z_tf v); generalize dependent (Z.b2z v) + end. +Ltac solve_bool_with_Z := + bool_to_Z; + intros; + lia. (* A more ambitious brute force existential solver. *) @@ -1495,8 +1684,8 @@ Ltac guess_ex_solver := guess_ex_solver*) | |- @ex bool _ => exists true; guess_ex_solver | |- @ex bool _ => exists false; guess_ex_solver - | x : Z |- @ex Z _ => exists x; guess_ex_solver - | _ => solve [tauto | eauto 3 with zarith sail | omega | intuition] + | x : ?ty |- @ex ?ty _ => exists x; guess_ex_solver + | _ => solve [tauto | eauto 3 with zarith sail | solve_bool_with_Z | omega] end. (* A straightforward solver for simple problems like @@ -1527,6 +1716,7 @@ Ltac simple_ex_iff := match goal with | |- @ex _ _ => eexists; simple_ex_iff | |- _ <-> _ => + symmetry; simple_split_iff; form_iff_true; solve [apply iff_refl | eassumption] @@ -1625,7 +1815,7 @@ Ltac ex_iff_solve := | |- @ex _ _ => eexists; ex_iff_solve (* Range constraints are attached to the right *) | |- _ /\ _ => split; [ex_iff_solve | omega] - | |- _ <-> _ => conjuncts_iff_solve + | |- _ <-> _ => conjuncts_iff_solve || (symmetry; conjuncts_iff_solve) end. @@ -1654,41 +1844,73 @@ Ltac z_comparisons := | exact Z_compare_gt_lt | exact Z_compare_gt_eq ]. + +Ltac bool_ex_solve := +match goal with H : ?l = ?v -> @ex _ _ |- @ex _ _ => + match v with true => idtac | false => idtac end; + destruct l; + repeat match goal with H:?X = ?X -> _ |- _ => specialize (H eq_refl) end; + repeat match goal with H:@ex _ _ |- _ => destruct H end; + unbool_comparisons; + guess_ex_solver +end. -(* Try to get the linear arithmetic solver to do booleans. *) - -Lemma b2z_true x : x = true <-> Z.b2z x = 1. -destruct x; compute; split; congruence. -Qed. - -Lemma b2z_false x : x = false <-> Z.b2z x = 0. -destruct x; compute; split; congruence. -Qed. +(* Solve a boolean equality goal which is just rearranged clauses (e.g, at the + end of the clause_matching_bool_solver, below. *) +Ltac bruteforce_bool_eq := + lazymatch goal with + | |- _ && ?l1 = _ => idtac l1; destruct l1; rewrite ?Bool.andb_true_l, ?Bool.andb_true_r, ?Bool.andb_false_l, ?Bool.andb_false_r; bruteforce_bool_eq + | |- ?l = _ => reflexivity + end. -Lemma b2z_tf x : 0 <= Z.b2z x <= 1. -destruct x; simpl; omega. -Qed. +Ltac clause_matching_bool_solver := +(* Do the left hand and right hand clauses have the same shape? *) +let rec check l r := + lazymatch l with + | ?l1 || ?l2 => + lazymatch r with ?r1 || ?r2 => check l1 r1; check l2 r2 end + | ?l1 =? ?l2 => + lazymatch r with ?r1 =? ?r2 => check l1 r1; check l2 r2 end + | _ => is_evar l + constr_eq l r + end +in +(* Rebuild remaining rhs, dropping extra "true"s. *) +let rec add_clause l r := + match l with + | true => r + | _ => match r with true => l | _ => constr:(l && r) end + end +in +(* Find a clause in r matching l, use unify to instantiate evars, return rest of r *) +let rec find l r := + lazymatch r with + | ?r1 && ?r2 => + match l with + | _ => let r1' := find l r1 in add_clause r1' r2 + | _ => let r2' := find l r2 in add_clause r1 r2' + end + | _ => constr:(ltac:(check l r; unify l r; exact true)) + end +in +(* For each clause in the lhs, find a matching clause in rhs, fill in + remaining evar with left over. TODO: apply to goals without an evar clause *) +match goal with + | |- @ex _ _ => eexists; clause_matching_bool_solver + | |- _ = _ /\ _ <= _ <= _ => split; [clause_matching_bool_solver | omega] + | |- ?l = ?r => + let rec clause l r := + match l with + | ?l1 && ?l2 => + let r2 := clause l1 r in clause l2 r2 + | _ => constr:(ltac:(is_evar l; exact r)) + | _ => find l r + end + in let r' := clause l r in + instantiate (1 := r'); + rewrite ?Bool.andb_true_l, ?Bool.andb_assoc; + bruteforce_bool_eq +end. -Ltac solve_bool_with_Z := - subst; - rewrite ?truefalse, ?falsetrue, ?or_False_l, ?or_False_r in *; - (* I did try phrasing these as rewrites, but Coq was oddly reluctant to use them *) - repeat match goal with - | H:?x = ?x <-> _ |- _ => apply iff_equal_l in H - | H:_ <-> ?x = ?x |- _ => apply iff_equal_r in H - end; - repeat match goal with - | H:context [?v = true] |- _ => is_var v; rewrite (b2z_true v) in * - | |- context [?v = true] => is_var v; rewrite (b2z_true v) in * - | H:context [?v = false] |- _ => is_var v; rewrite (b2z_false v) in * - | |- context [?v = false] => is_var v; rewrite (b2z_false v) in * - end; - repeat match goal with - | _:context [Z.b2z ?v] |- _ => generalize (b2z_tf v); generalize dependent (Z.b2z v) - | |- context [Z.b2z ?v] => generalize (b2z_tf v); generalize dependent (Z.b2z v) - end; - intros; - lia. (* Redefine this to add extra solver tactics *) @@ -1756,7 +1978,6 @@ Ltac main_solver := repeat match goal with H:@ex _ _ |- _ => destruct H end; guess_ex_solver end - | match goal with |- @ex _ _ => guess_ex_solver end (* While firstorder was quite effective at dealing with existentially quantified goals from boolean expressions, it attempts lazy normalization of terms, which blows up on integer comparisons with large constants. @@ -1764,6 +1985,9 @@ Ltac main_solver := (* Don't use auto for the fallback to keep runtime down *) firstorder fail end*) + | bool_ex_solve + | clause_matching_bool_solver + | match goal with |- @ex _ _ => guess_ex_solver end | sail_extra_tactic | idtac "Unable to solve constraint"; dump_context; fail ]. @@ -1777,21 +2001,134 @@ Ltac simple_omega := end; omega. Ltac solve_unknown := - match goal with |- (ArithFact (?x ?y)) => + match goal with + | |- (ArithFact (?x ?y)) => + is_evar x; + idtac "Warning: unknown constraint"; + let t := type of y in + unify x (fun (_ : t) => true); + exact (Build_ArithFactP _ eq_refl : ArithFact true) + | |- (ArithFactP (?x ?y)) => is_evar x; idtac "Warning: unknown constraint"; let t := type of y in unify x (fun (_ : t) => True); - exact (Build_ArithFact _ I) + exact (Build_ArithFactP _ I : ArithFactP True) end. +(* Solving straightforward and_boolMP / or_boolMP goals *) + +Lemma default_and_proof l r r' : + (l = true -> r' = r) -> + l && r' = l && r. + intro H. +destruct l; [specialize (H eq_refl) | clear H ]; auto. +Qed. + +Lemma default_and_proof2 l l' r r' : + l' = l -> + (l = true -> r' = r) -> + l' && r' = l && r. +intros; subst. +auto using default_and_proof. +Qed. + +Lemma default_or_proof l r r' : + (l = false -> r' = r) -> + l || r' = l || r. + intro H. +destruct l; [clear H | specialize (H eq_refl) ]; auto. +Qed. + +Lemma default_or_proof2 l l' r r' : + l' = l -> + (l = false -> r' = r) -> + l' || r' = l || r. +intros; subst. +auto using default_or_proof. +Qed. + +Ltac default_andor := + intros; constructor; intros; + repeat match goal with + | H:@ex _ _ |- _ => destruct H + | H:@eq bool _ _ -> @ex bool _ |- _ => apply lift_bool_exists in H + end; + repeat match goal with |- @ex _ _ => eexists end; + rewrite ?Bool.eqb_true_iff, ?Bool.eqb_false_iff in *; + match goal with + | H:?v = true -> _ |- _ = ?v && _ => eapply default_and_proof; eauto + | H:?v = true -> _ |- _ = ?v && _ => eapply default_and_proof2; eauto + | H:?v = false -> _ |- _ = ?v || _ => eapply default_or_proof; eauto + | H:?v = false -> _ |- _ = ?v || _ => eapply default_or_proof2; eauto + end. + +(* Solving simple and_boolMP / or_boolMP goals where unknown booleans + have been merged together. *) + +Ltac squashed_andor_solver := + clear; + match goal with |- forall l r : bool, ArithFactP (_ -> _ -> _) => idtac end; + intros l r; constructor; intros; + let func := match goal with |- context[?f l r] => f end in + match goal with + | H1 : @ex _ _, H2 : l = _ -> @ex _ _ |- _ => + let x1 := fresh "x1" in + let x2 := fresh "x2" in + let H1' := fresh "H1" in + let H2' := fresh "H2" in + apply lift_bool_exists in H2; + destruct H1 as [x1 H1']; destruct H2 as [x2 H2']; + exists x1, x2 + | H : l = _ -> @ex _ _ |- _ => + let x := fresh "x" in + let H' := fresh "H" in + apply lift_bool_exists in H; + destruct H as [x H']; + exists (func x l) + | H : @ex _ _ |- _ => + let x := fresh "x" in + let H' := fresh "H" in + destruct H as [x H']; + exists (func x r) + end; + repeat match goal with + | H : l = _ -> @ex _ _ |- _ => + let x := fresh "x" in + let H' := fresh "H" in + apply lift_bool_exists in H; + destruct H as [x H']; + exists x + | H : @ex _ _ |- _ => + let x := fresh "x" in + let H' := fresh "H" in + destruct H as [x H']; + exists x + end; + (* Attempt to shrink size of problem *) + try match goal with + | _ : l = _ -> ?v = r |- context[?v] => generalize dependent v; intros + | _ : l = _ -> Bool.eqb ?v r = true |- context[?v] => generalize dependent v; intros + end; + unbool_comparisons; unbool_comparisons_goal; + repeat match goal with + | _ : context[?li =? ?ri] |- _ => + specialize (Z.eqb_eq li ri); generalize dependent (li =? ri); intros + | |- context[?li =? ?ri] => + specialize (Z.eqb_eq li ri); generalize (li =? ri); intros + end; + rewrite <- ?Z.eqb_eq in *; + solve_bool_with_Z. + 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). *) -try (constructor; simple_omega); +try solve [default_andor]; +constructor; +try simple_omega; prepare_for_solver; (*dump_context;*) -constructor; +unbool_comparisons_goal; (* Applying the ArithFact constructor will reveal an = true, so this might do more than it did in prepare_for_solver *) repeat match goal with |- and _ _ => split end; main_solver. @@ -1813,18 +2150,31 @@ Ltac clear_fixpoints := match goal with | H:_ -> ?res |- _ => is_fixpoint res; clear H end. +Ltac clear_proof_bodies := + repeat match goal with + | H := _ : ?ty |- _ => + match type of ty with + | Prop => clearbody H + end + end. Ltac solve_arithfact := + clear_proof_bodies; + try solve [squashed_andor_solver]; (* Do this first so that it can name the intros *) intros; (* To solve implications for derive_m *) clear_fixpoints; (* Avoid using recursive calls *) + cbv beta; (* Goal might be eta-expanded *) solve [ solve_unknown - | match goal with |- ArithFact (?x <= ?x <= ?x) => exact trivial_range end + | assumption + | match goal with |- ArithFact ((?x <=? ?x <=? ?x)) => exact trivial_range end + | eauto 2 with sail (* the low search bound might not be necessary *) | fill_in_evar_eq | match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end + | match goal with |- context [projT1 ?X] => apply (ArithFactP_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 + fill_in_evar_eq above, e.g., 8 * n =? 8 * ?Goal3 *) + | constructor; apply Z.eqb_eq; reflexivity | constructor; repeat match goal with |- and _ _ => split end; z_comparisons | run_main_solver ]. @@ -1834,6 +2184,7 @@ Ltac solve_arithfact := Ltac run_solver := solve_arithfact. Hint Extern 0 (ArithFact _) => run_solver : typeclass_instances. +Hint Extern 0 (ArithFactP _) => run_solver : typeclass_instances. Hint Unfold length_mword : sail. @@ -1853,13 +2204,11 @@ auto using Z.le_ge, Zle_0_pos. destruct w. Qed. -Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply ReasonableSize_witness; assumption | constructor; omega]) : typeclass_instances. +Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply ReasonableSize_witness; assumption | constructor; auto with zarith]) : typeclass_instances. -Definition to_range (x : Z) : {y : Z & ArithFact (x <= y <= x)} := build_ex x. +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)) := { +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)); of_bools v := to_word isPositive (fit_bbv_word (wordFromBitlist v)); @@ -2192,7 +2541,7 @@ Fixpoint foreach_Z' {Vars} from to step n (vars : Vars) (body : Z -> Vars -> Var Definition foreach_Z {Vars} from to step vars body := foreach_Z' (Vars := Vars) from to step (S (Z.abs_nat (from - to))) vars body. -Fixpoint foreach_Z_up' {Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> Vars) {struct n} : Vars := +Fixpoint foreach_Z_up' {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 -> Vars) {struct n} : Vars := if sumbool_of_bool (from + off <=? to) then match n with | O => vars @@ -2200,7 +2549,7 @@ Fixpoint foreach_Z_up' {Vars} from to step off n `{ArithFact (0 < step)} `{Arith end else vars. -Fixpoint foreach_Z_down' {Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> Vars) {struct n} : Vars := +Fixpoint foreach_Z_down' {Vars} from to step off n `{ArithFact (0 <? step)} `{ArithFact (off <=? 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact ((to <=? z <=? from))), Vars -> Vars) {struct n} : Vars := if sumbool_of_bool (to <=? from + off) then match n with | O => vars @@ -2208,9 +2557,9 @@ Fixpoint foreach_Z_down' {Vars} from to step off n `{ArithFact (0 < step)} `{Ari end else vars. -Definition foreach_Z_up {Vars} from to step vars body `{ArithFact (0 < step)} := +Definition foreach_Z_up {Vars} from to step vars body `{ArithFact (0 <? step)} := foreach_Z_up' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. -Definition foreach_Z_down {Vars} from to step vars body `{ArithFact (0 < step)} := +Definition foreach_Z_down {Vars} from to step vars body `{ArithFact (0 <? step)} := foreach_Z_down' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. (*val while : forall vars. vars -> (vars -> bool) -> (vars -> vars) -> vars @@ -2303,27 +2652,27 @@ end (* Arithmetic functions which return proofs that match the expected Sail types in smt.sail. *) -Definition ediv_with_eq n m : {o : Z & ArithFact (o = ZEuclid.div n m)} := build_ex (ZEuclid.div n m). -Definition emod_with_eq n m : {o : Z & ArithFact (o = ZEuclid.modulo n m)} := build_ex (ZEuclid.modulo n m). -Definition abs_with_eq n : {o : Z & ArithFact (o = Z.abs n)} := build_ex (Z.abs n). +Definition ediv_with_eq n m : {o : Z & ArithFact (o =? ZEuclid.div n m)} := build_ex (ZEuclid.div n m). +Definition emod_with_eq n m : {o : Z & ArithFact (o =? ZEuclid.modulo n m)} := build_ex (ZEuclid.modulo n m). +Definition abs_with_eq n : {o : Z & ArithFact (o =? Z.abs n)} := build_ex (Z.abs n). (* Similarly, for ranges (currently in MIPS) *) -Definition eq_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)}) : bool := +Definition eq_range {n m o p} (l : {l & ArithFact (n <=? l <=? m)}) (r : {r & ArithFact (o <=? r <=? p)}) : bool := (projT1 l) =? (projT1 r). -Definition add_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)}) - : {x & ArithFact (n+o <= x <= m+p)} := +Definition add_range {n m o p} (l : {l & ArithFact (n <=? l <=? m)}) (r : {r & ArithFact (o <=? r <=? p)}) + : {x & ArithFact (n+o <=? x <=? m+p)} := build_ex ((projT1 l) + (projT1 r)). -Definition sub_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)}) - : {x & ArithFact (n-p <= x <= m-o)} := +Definition sub_range {n m o p} (l : {l & ArithFact (n <=? l <=? m)}) (r : {r & ArithFact (o <=? r <=? p)}) + : {x & ArithFact (n-p <=? x <=? m-o)} := build_ex ((projT1 l) - (projT1 r)). -Definition negate_range {n m} (l : {l : Z & ArithFact (n <= l <= m)}) - : {x : Z & ArithFact ((- m) <= x <= (- n))} := +Definition negate_range {n m} (l : {l : Z & ArithFact (n <=? l <=? m)}) + : {x : Z & ArithFact ((- m) <=? x <=? (- n))} := build_ex (- (projT1 l)). -Definition min_atom (a : Z) (b : Z) : {c : Z & ArithFact ((c = a \/ c = b) /\ c <= a /\ c <= b)} := +Definition min_atom (a : Z) (b : Z) : {c : Z & ArithFact (((c =? a) || (c =? b)) && (c <=? a) && (c <=? b))} := build_ex (Z.min a b). -Definition max_atom (a : Z) (b : Z) : {c : Z & ArithFact ((c = a \/ c = b) /\ c >= a /\ c >= b)} := +Definition max_atom (a : Z) (b : Z) : {c : Z & ArithFact (((c =? a) || (c =? b)) && (c >=? a) && (c >=? b))} := build_ex (Z.max a b). @@ -2331,15 +2680,18 @@ Definition max_atom (a : Z) (b : Z) : {c : Z & ArithFact ((c = a \/ c = b) /\ c Definition vec (T:Type) (n:Z) := { l : list T & length_list l = n }. Definition vec_length {T n} (v : vec T n) := n. -Definition vec_access_dec {T n} (v : vec T n) m `{ArithFact (0 <= m < n)} : T := +Definition vec_access_dec {T n} (v : vec T n) m `{ArithFact ((0 <=? m <? n))} : T := access_list_dec (projT1 v) m. -Definition vec_access_inc {T n} (v : vec T n) m `{ArithFact (0 <= m < n)} : T := + +Definition vec_access_inc {T n} (v : vec T n) m `{ArithFact (0 <=? m <? n)} : T := access_list_inc (projT1 v) m. -Program Definition vec_init {T} (t : T) (n : Z) `{ArithFact (n >= 0)} : vec T n := +Program Definition vec_init {T} (t : T) (n : Z) `{ArithFact (n >=? 0)} : vec T n := existT _ (repeat [t] n) _. Next Obligation. -rewrite repeat_length; auto using fact. +intros. +cbv beta. +rewrite repeat_length. 2: apply Z_geb_ge, fact. unfold length_list. simpl. auto with zarith. @@ -2387,21 +2739,25 @@ rewrite skipn_length; omega. Qed. -Program Definition vec_update_dec {T n} (v : vec T n) m t `{ArithFact (0 <= m < n)} : vec T n := existT _ (update_list_dec (projT1 v) m t) _. +Program Definition vec_update_dec {T n} (v : vec T n) m t `{ArithFact (0 <=? m <? n)} : vec T n := existT _ (update_list_dec (projT1 v) m t) _. Next Obligation. +intros; cbv beta. unfold update_list_dec. rewrite update_list_inc_length. + destruct v. apply e. -+ destruct H. ++ destruct H as [H]. + unbool_comparisons. destruct v. simpl (projT1 _). rewrite e. omega. Qed. -Program Definition vec_update_inc {T n} (v : vec T n) m t `{ArithFact (0 <= m < n)} : vec T n := existT _ (update_list_inc (projT1 v) m t) _. +Program Definition vec_update_inc {T n} (v : vec T n) m t `{ArithFact (0 <=? m <? n)} : vec T n := existT _ (update_list_inc (projT1 v) m t) _. Next Obligation. +intros; cbv beta. rewrite update_list_inc_length. + destruct v. apply e. + destruct H. + unbool_comparisons. destruct v. simpl (projT1 _). rewrite e. omega. Qed. @@ -2421,6 +2777,7 @@ Program Definition just_vec {A n} (v : vec (option A) n) : option (vec A n) := | Some v' => Some (existT _ v' _) end. Next Obligation. +intros; cbv beta. rewrite <- (just_list_length_Z _ _ Heq_anonymous). destruct v. assumption. @@ -2436,9 +2793,10 @@ refine (if List.list_eq_dec D (projT1 x) (projT1 y) then left _ else right _). Defined. Instance Decidable_eq_vec {T : Type} {n} `(DT : forall x y : T, Decidable (x = y)) : - forall x y : vec T n, Decidable (x = y) := { + forall x y : vec T n, Decidable (x = y). +refine (fun x y => {| Decidable_witness := proj1_sig (bool_of_sumbool (vec_eq_dec (fun x y => generic_dec x y) x y)) -}. +|}). destruct (vec_eq_dec _ x y); simpl; split; congruence. Defined. @@ -2458,51 +2816,58 @@ match a with | None => None end. -Definition sub_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} : - {z : Z & ArithFact (z >= 0)} := +Definition sub_nat (x : Z) `{ArithFact (x >=? 0)} (y : Z) `{ArithFact (y >=? 0)} : + {z : Z & ArithFact (z >=? 0)} := let z := x - y in if sumbool_of_bool (z >=? 0) then build_ex z else build_ex 0. -Definition min_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} : - {z : Z & ArithFact (z >= 0)} := +Definition min_nat (x : Z) `{ArithFact (x >=? 0)} (y : Z) `{ArithFact (y >=? 0)} : + {z : Z & ArithFact (z >=? 0)} := build_ex (Z.min x y). -Definition max_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} : - {z : Z & ArithFact (z >= 0)} := +Definition max_nat (x : Z) `{ArithFact (x >=? 0)} (y : Z) `{ArithFact (y >=? 0)} : + {z : Z & ArithFact (z >=? 0)} := build_ex (Z.max x y). -Definition shl_int_8 (x y : Z) `{HE:ArithFact (x = 8)} `{HR:ArithFact (0 <= y <= 3)}: {z : Z & ArithFact (In z [8;16;32;64])}. +Definition shl_int_8 (x y : Z) `{HE:ArithFact (x =? 8)} `{HR:ArithFact (0 <=? y <=? 3)}: {z : Z & ArithFact (member_Z_list z [8;16;32;64])}. refine (existT _ (shl_int x y) _). destruct HE as [HE]. destruct HR as [HR]. -assert (H : y = 0 \/ y = 1 \/ y = 2 \/ y = 3) by omega. +unbool_comparisons. +assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3) by omega. constructor. intuition (subst; compute; auto). Defined. -Definition shl_int_32 (x y : Z) `{HE:ArithFact (x = 32)} `{HR:ArithFact (In y [0;1])}: {z : Z & ArithFact (In z [32;64])}. +Definition shl_int_32 (x y : Z) `{HE:ArithFact (x =? 32)} `{HR:ArithFact (member_Z_list y [0;1])}: {z : Z & ArithFact (member_Z_list z [32;64])}. refine (existT _ (shl_int x y) _). destruct HE as [HE]. -destruct HR as [[HR1 | [HR2 | []]]]; +destruct HR as [HR]. +constructor. +unbool_comparisons. +destruct HR as [HR | [HR | []]]; subst; compute; -auto using Build_ArithFact. +auto. Defined. -Definition shr_int_32 (x y : Z) `{HE:ArithFact (0 <= x <= 31)} `{HR:ArithFact (y = 1)}: {z : Z & ArithFact (0 <= z <= 15)}. +Definition shr_int_32 (x y : Z) `{HE:ArithFact (0 <=? x <=? 31)} `{HR:ArithFact (y =? 1)}: {z : Z & ArithFact (0 <=? z <=? 15)}. refine (existT _ (shr_int x y) _). -destruct HE as [HE]. -destruct HR as [HR]; -subst. -unfold shr_int. -rewrite <- Z.div2_spec. -constructor. -rewrite Z.div2_div. -specialize (Z.div_mod x 2). -specialize (Z.mod_pos_bound x 2). -generalize (Z.div x 2). -generalize (x mod 2). -intros. -nia. +abstract ( + destruct HE as [HE]; + destruct HR as [HR]; + unbool_comparisons; + subst; + constructor; + unbool_comparisons_goal; + unfold shr_int; + rewrite <- Z.div2_spec; + rewrite Z.div2_div; + specialize (Z.div_mod x 2); + specialize (Z.mod_pos_bound x 2); + generalize (Z.div x 2); + generalize (x mod 2); + intros; + nia). Defined. Lemma shl_8_ge_0 {n} : shl_int 8 n >= 0. diff --git a/lib/coq/Sail2_values_lemmas.v b/lib/coq/Sail2_values_lemmas.v new file mode 100644 index 00000000..ed8b6af0 --- /dev/null +++ b/lib/coq/Sail2_values_lemmas.v @@ -0,0 +1,392 @@ +Require Import Sail2_values. + +(* + +lemma while_domI: + fixes V :: "'vars \<Rightarrow> nat" + assumes "\<And>vars. cond vars \<Longrightarrow> V (body vars) < V vars" + shows "while_dom (vars, cond, body)" + by (induction vars rule: measure_induct_rule[where f = V]) + (use assms in \<open>auto intro: while.domintros\<close>) + +lemma nat_of_int_nat_simps[simp]: "nat_of_int = nat" by (auto simp: nat_of_int_def) + +termination reverse_endianness_list by (lexicographic_order simp add: drop_list_def) +declare reverse_endianness_list.simps[simp del] +declare take_list_def[simp] +declare drop_list_def[simp] +*) +Import ListNotations. +Require Program.Wf. + +Lemma skipn_length T n (xs : list T) : + n <> 0%nat -> + xs <> [] -> + (List.length (skipn n xs) < List.length xs)%nat. +revert n. +induction xs. +* congruence. +* destruct n. + + congruence. + + intros _ _. simpl. + destruct xs. + - destruct n; simpl; auto. + - destruct n; auto. + apply Nat.lt_lt_succ_r. + apply IHxs; congruence. +Qed. + +Program Fixpoint take_chunks {a} (n : nat) (xs : list a) {measure (List.length xs)} : list (list a) := + match xs with + | [] => [] + | _ => match n with O => [] | _ => (firstn n xs)::take_chunks n (skipn n xs) end + end. +Next Obligation. +apply skipn_length; auto. +Qed. + +(* +lemma take_chunks_length_leq_n: "length xs \<le> n \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> take_chunks n xs = [xs]" + by (cases n) auto + +lemma take_chunks_append: "n dvd length a \<Longrightarrow> take_chunks n (a @ b) = take_chunks n a @ take_chunks n b" + by (induction n a rule: take_chunks.induct) (auto simp: dvd_imp_le) + +lemma Suc8_plus8: "Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc x))))))) = 8 + x" + by auto + +lemma byte_chunks_take_chunks_8: + assumes "8 dvd length xs" + shows "byte_chunks xs = Some (take_chunks 8 xs)" +proof - + have Suc8_plus8: "Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc x))))))) = 8 + x" for x + by auto + from assms show ?thesis + by (induction xs rule: byte_chunks.induct) (auto simp: Suc8_plus8 nat_dvd_not_less) +qed + +lemma reverse_endianness_list_rev_take_chunks: + "reverse_endianness_list bits = List.concat (rev (take_chunks 8 bits))" + by (induction "8 :: nat" bits rule: take_chunks.induct) + (auto simp: reverse_endianness_list.simps) + +lemma reverse_endianness_list_simps: + "length bits \<le> 8 \<Longrightarrow> reverse_endianness_list bits = bits" + "length bits > 8 \<Longrightarrow> reverse_endianness_list bits = reverse_endianness_list (drop 8 bits) @ take 8 bits" + by (cases bits; auto simp: reverse_endianness_list_rev_take_chunks)+ + +lemma reverse_endianness_list_append: + assumes "8 dvd length a" + shows "reverse_endianness_list (a @ b) = reverse_endianness_list b @ reverse_endianness_list a" + using assms by (auto simp: reverse_endianness_list_rev_take_chunks take_chunks_append) + +lemma length_reverse_endianness_list[simp]: + "length (reverse_endianness_list l) = length l" + by (induction l rule: reverse_endianness_list.induct) (auto simp: reverse_endianness_list.simps) + +lemma reverse_endianness_list_take_8[simp]: + "reverse_endianness_list (take 8 bits) = take 8 bits" + by (auto simp: reverse_endianness_list_simps) + +lemma reverse_reverse_endianness_list[simp]: + assumes "8 dvd length l" + shows "reverse_endianness_list (reverse_endianness_list l) = l" +proof (use assms in \<open>induction l rule: reverse_endianness_list.induct[case_names Step]\<close>) + case (Step bits) + then show ?case + by (auto simp: reverse_endianness_list.simps[of bits] reverse_endianness_list_append) +qed + +declare repeat.simps[simp del] + +lemma length_repeat[simp]: "length (repeat xs n) = nat n * length xs" +proof (induction xs n rule: repeat.induct[case_names Step]) + case (Step xs n) + then show ?case unfolding repeat.simps[of xs n] + by (auto simp del: mult_Suc simp: mult_Suc[symmetric]) +qed + +lemma nth_repeat: + assumes "i < nat n * length xs" + shows "repeat xs n ! i = xs ! (i mod length xs)" +proof (use assms in \<open>induction xs n arbitrary: i rule: repeat.induct[case_names Step]\<close>) + case (Step xs n i) + show ?case + using Step.prems Step.IH[of "i - length xs"] + unfolding repeat.simps[of xs n] + by (auto simp: nth_append mod_geq[symmetric] nat_diff_distrib diff_mult_distrib) +qed + +termination index_list + by (relation "measure (\<lambda>(i, j, step). nat ((j - i + step) * sgn step))") auto + +lemma index_list_Zero[simp]: "index_list i j 0 = []" + by auto + +lemma index_list_singleton[simp]: "n \<noteq> 0 \<Longrightarrow> index_list i i n = [i]" + by auto + +lemma index_list_simps: + "0 < step \<Longrightarrow> from \<le> to \<Longrightarrow> index_list from to step = from # index_list (from + step) to step" + "0 < step \<Longrightarrow> from > to \<Longrightarrow> index_list from to step = []" + "0 > step \<Longrightarrow> from \<ge> to \<Longrightarrow> index_list from to step = from # index_list (from + step) to step" + "0 > step \<Longrightarrow> from < to \<Longrightarrow> index_list from to step = []" + by auto + +lemma index_list_step1_upto[simp]: "index_list i j 1 = [i..j]" + by (induction i j "1 :: int" rule: index_list.induct) + (auto simp: index_list_simps upto.simps) + +lemma length_upto[simp]: "i \<le> j \<Longrightarrow> length [i..j] = nat (j - i + 1)" + by (induction i j rule: upto.induct) (auto simp: upto.simps) + +lemma nth_upto[simp]: "i + int n \<le> j \<Longrightarrow> [i..j] ! n = i + int n" + by (induction i j arbitrary: n rule: upto.induct) + (auto simp: upto.simps nth_Cons split: nat.splits) + +declare index_list.simps[simp del] + +lemma genlist_add_upt[simp]: "genlist ((+) start) len = [start..<start + len]" + by (auto simp: genlist_def map_add_upt add.commute cong: map_cong) + +lemma just_list_map_Some[simp]: "just_list (map Some v) = Some v" by (induction v) auto + +lemma just_list_None_iff[simp]: "just_list xs = None \<longleftrightarrow> None \<in> set xs" + by (induction xs) (auto split: option.splits) + +lemma just_list_None_member_None: "None \<in> set xs \<Longrightarrow> just_list xs = None" + by auto + +lemma just_list_Some_iff[simp]: "just_list xs = Some ys \<longleftrightarrow> xs = map Some ys" + by (induction xs arbitrary: ys) (auto split: option.splits) + +lemma just_list_cases: + assumes "just_list xs = y" + obtains (None) "None \<in> set xs" and "y = None" + | (Some) ys where "xs = map Some ys" and "y = Some ys" + using assms by (cases y) auto + +lemma repeat_singleton_replicate[simp]: + "repeat [x] n = replicate (nat n) x" +proof (induction n) + case (nonneg n) + have "nat (1 + int m) = Suc m" for m by auto + then show ?case by (induction n) (auto simp: repeat.simps) +next + case (neg n) + then show ?case by (auto simp: repeat.simps) +qed + +lemma and_bit_B1[simp]: "and_bit B1 b = b" + by (cases b) auto + +lemma and_bit_idem[simp]: "and_bit b b = b" + by (cases b) auto + +lemma and_bit_eq_iff: + "and_bit b b' = B0 \<longleftrightarrow> (b = B0 \<or> b' = B0)" + "and_bit b b' = BU \<longleftrightarrow> (b = BU \<or> b' = BU) \<and> b \<noteq> B0 \<and> b' \<noteq> B0" + "and_bit b b' = B1 \<longleftrightarrow> (b = B1 \<and> b' = B1)" + by (cases b; cases b'; auto)+ + +lemma foldl_and_bit_eq_iff: + shows "foldl and_bit b bs = B0 \<longleftrightarrow> (b = B0 \<or> B0 \<in> set bs)" (is ?B0) + and "foldl and_bit b bs = B1 \<longleftrightarrow> (b = B1 \<and> set bs \<subseteq> {B1})" (is ?B1) + and "foldl and_bit b bs = BU \<longleftrightarrow> (b = BU \<or> BU \<in> set bs) \<and> b \<noteq> B0 \<and> B0 \<notin> set bs" (is ?BU) +proof - + have "?B0 \<and> ?B1 \<and> ?BU" + proof (induction bs arbitrary: b) + case (Cons b' bs) + show ?case using Cons.IH by (cases b; cases b') auto + qed auto + then show ?B0 and ?B1 and ?BU by auto +qed + +lemma bool_of_bitU_simps[simp]: + "bool_of_bitU B0 = Some False" + "bool_of_bitU B1 = Some True" + "bool_of_bitU BU = None" + by (auto simp: bool_of_bitU_def) + +lemma bitops_bitU_of_bool[simp]: + "and_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool (x \<and> y)" + "or_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool (x \<or> y)" + "xor_bit (bitU_of_bool x) (bitU_of_bool y) = bitU_of_bool ((x \<or> y) \<and> \<not>(x \<and> y))" + "not_bit (bitU_of_bool x) = bitU_of_bool (\<not>x)" + "not_bit \<circ> bitU_of_bool = bitU_of_bool \<circ> Not" + by (auto simp: bitU_of_bool_def not_bit_def) + +lemma image_bitU_of_bool_B0_B1: "bitU_of_bool ` bs \<subseteq> {B0, B1}" + by (auto simp: bitU_of_bool_def split: if_splits) + +lemma bool_of_bitU_bitU_of_bool[simp]: + "bool_of_bitU \<circ> bitU_of_bool = Some" + "bool_of_bitU \<circ> (bitU_of_bool \<circ> f) = Some \<circ> f" + "bool_of_bitU (bitU_of_bool x) = Some x" + by (intro ext, auto simp: bool_of_bitU_def bitU_of_bool_def)+ + +abbreviation "BC_bitU_list \<equiv> instance_Sail2_values_Bitvector_list_dict instance_Sail2_values_BitU_Sail2_values_bitU_dict" +lemmas BC_bitU_list_def = instance_Sail2_values_Bitvector_list_dict_def instance_Sail2_values_BitU_Sail2_values_bitU_dict_def +abbreviation "BC_mword \<equiv> instance_Sail2_values_Bitvector_Machine_word_mword_dict" +lemmas BC_mword_defs = instance_Sail2_values_Bitvector_Machine_word_mword_dict_def + access_mword_def access_mword_inc_def access_mword_dec_def + (*update_mword_def update_mword_inc_def update_mword_dec_def*) + subrange_list_def subrange_list_inc_def subrange_list_dec_def + update_subrange_list_def update_subrange_list_inc_def update_subrange_list_dec_def + +declare size_itself_int_def[simp] +declare size_itself_def[simp] +declare word_size[simp] + +lemma int_of_mword_simps[simp]: + "int_of_mword False w = uint w" + "int_of_mword True w = sint w" + "int_of_bv BC_mword False w = Some (uint w)" + "int_of_bv BC_mword True w = Some (sint w)" + by (auto simp: int_of_mword_def int_of_bv_def BC_mword_defs) + +lemma BC_mword_simps[simp]: + "unsigned_method BC_mword a = Some (uint a)" + "signed_method BC_mword a = Some (sint a)" + "length_method BC_mword (a :: ('a :: len) word) = int (LENGTH('a))" + by (auto simp: BC_mword_defs) + +lemma of_bits_mword_of_bl[simp]: + assumes "just_list (map bool_of_bitU bus) = Some bs" + shows "of_bits_method BC_mword bus = Some (of_bl bs)" + and "of_bits_failwith BC_mword bus = of_bl bs" + using assms by (auto simp: BC_mword_defs of_bits_failwith_def maybe_failwith_def) + +lemma nat_of_bits_aux_bl_to_bin_aux: + "nat_of_bools_aux acc bs = nat (bl_to_bin_aux bs (int acc))" + by (induction acc bs rule: nat_of_bools_aux.induct) + (auto simp: Bit_def intro!: arg_cong[where f = nat] arg_cong2[where f = bl_to_bin_aux] split: if_splits) + +lemma nat_of_bits_bl_to_bin[simp]: + "nat_of_bools bs = nat (bl_to_bin bs)" + by (auto simp: nat_of_bools_def bl_to_bin_def nat_of_bits_aux_bl_to_bin_aux) + +lemma unsigned_bits_of_mword[simp]: + "unsigned_method BC_bitU_list (bits_of_method BC_mword a) = Some (uint a)" + by (auto simp: BC_bitU_list_def BC_mword_defs unsigned_of_bits_def unsigned_of_bools_def) +*) +Definition mem_bytes_of_word {a} (w : mword a) : list (list bitU) := + List.rev (take_chunks 8 (bits_of w)). +(* +lemma mem_bytes_of_bits_mem_bytes_of_word[simp]: + assumes "8 dvd LENGTH('a)" + shows "mem_bytes_of_bits BC_mword (w :: 'a::len word) = Some (mem_bytes_of_word w)" + using assms + by (auto simp: mem_bytes_of_bits_def bytes_of_bits_def BC_mword_defs byte_chunks_take_chunks_8 mem_bytes_of_word_def) + +lemma bits_of_bitU_list[simp]: + "bits_of_method BC_bitU_list v = v" + "of_bits_method BC_bitU_list v = Some v" + by (auto simp: BC_bitU_list_def) + +lemma subrange_list_inc_drop_take: + "subrange_list_inc xs i j = drop (nat i) (take (nat (j + 1)) xs)" + by (auto simp: subrange_list_inc_def split_at_def) + +lemma subrange_list_dec_drop_take: + assumes "i \<ge> 0" and "j \<ge> 0" + shows "subrange_list_dec xs i j = drop (length xs - nat (i + 1)) (take (length xs - nat j) xs)" + using assms unfolding subrange_list_dec_def + by (auto simp: subrange_list_inc_drop_take add.commute diff_diff_add nat_minus_as_int) + +lemma update_subrange_list_inc_drop_take: + assumes "i \<ge> 0" and "j \<ge> i" + shows "update_subrange_list_inc xs i j xs' = take (nat i) xs @ xs' @ drop (nat (j + 1)) xs" + using assms unfolding update_subrange_list_inc_def + by (auto simp: split_at_def min_def) + +lemma update_subrange_list_dec_drop_take: + assumes "j \<ge> 0" and "i \<ge> j" + shows "update_subrange_list_dec xs i j xs' = take (length xs - nat (i + 1)) xs @ xs' @ drop (length xs - nat j) xs" + using assms unfolding update_subrange_list_dec_def update_subrange_list_inc_def + by (auto simp: split_at_def min_def Let_def add.commute diff_diff_add nat_minus_as_int) + +declare access_list_inc_def[simp] + +lemma access_list_dec_rev_nth: + assumes "0 \<le> i" and "nat i < length xs" + shows "access_list_dec xs i = rev xs ! (nat i)" + using assms + by (auto simp: access_list_dec_def rev_nth intro!: arg_cong2[where f = List.nth]) + +lemma access_bv_dec_mword[simp]: + fixes w :: "('a::len) word" + assumes "0 \<le> n" and "nat n < LENGTH('a)" + shows "access_bv_dec BC_mword w n = bitU_of_bool (w !! (nat n))" + using assms unfolding access_bv_dec_def access_list_def + by (auto simp: access_list_dec_rev_nth BC_mword_defs rev_map test_bit_bl) + +lemma access_list_dec_nth[simp]: + assumes "0 \<le> i" + shows "access_list_dec xs i = xs ! (length xs - nat (i + 1))" + using assms + by (auto simp: access_list_dec_def add.commute diff_diff_add nat_minus_as_int) + +lemma update_list_inc_update[simp]: + "update_list_inc xs n x = xs[nat n := x]" + by (auto simp: update_list_inc_def) + +lemma update_list_dec_update[simp]: + "update_list_dec xs n x = xs[length xs - nat (n + 1) := x]" + by (auto simp: update_list_dec_def add.commute diff_diff_add nat_minus_as_int) + +lemma update_list_dec_update_rev: + "0 \<le> n \<Longrightarrow> nat n < length xs \<Longrightarrow> update_list_dec xs n x = rev ((rev xs)[nat n := x])" + by (auto simp: update_list_dec_def add.commute diff_diff_add nat_minus_as_int rev_update) + +lemma access_list_dec_update_list_dec[simp]: + "0 \<le> n \<Longrightarrow> nat n < length xs \<Longrightarrow> access_list_dec (update_list_dec xs n x) n = x" + by (auto simp: access_list_dec_rev_nth update_list_dec_update_rev) + +lemma bools_of_nat_aux_simps[simp]: + "\<And>len. len \<le> 0 \<Longrightarrow> bools_of_nat_aux len x acc = acc" + "\<And>len. bools_of_nat_aux (int (Suc len)) x acc = + bools_of_nat_aux (int len) (x div 2) ((if x mod 2 = 1 then True else False) # acc)" + by auto +declare bools_of_nat_aux.simps[simp del] + +lemma bools_of_nat_aux_bin_to_bl_aux: + "bools_of_nat_aux len n acc = bin_to_bl_aux (nat len) (int n) acc" +proof (cases len) + case (nonneg len') + show ?thesis unfolding nonneg + proof (induction len' arbitrary: n acc) + case (Suc len'' n acc) + then show ?case + using zmod_int[of n 2] + by (auto simp del: of_nat_simps simp add: bin_rest_def bin_last_def zdiv_int) + qed auto +qed auto + +lemma bools_of_nat_bin_to_bl[simp]: + "bools_of_nat len n = bin_to_bl (nat len) (int n)" + by (auto simp: bools_of_nat_def bools_of_nat_aux_bin_to_bl_aux) + +lemma add_one_bool_ignore_overflow_aux_rbl_succ[simp]: + "add_one_bool_ignore_overflow_aux xs = rbl_succ xs" + by (induction xs) auto + +lemma add_one_bool_ignore_overflow_rbl_succ[simp]: + "add_one_bool_ignore_overflow xs = rev (rbl_succ (rev xs))" + unfolding add_one_bool_ignore_overflow_def by auto + +lemma map_Not_bin_to_bl: + "map Not (bin_to_bl_aux len n acc) = bin_to_bl_aux len (-n - 1) (map Not acc)" +proof (induction len arbitrary: n acc) + case (Suc len n acc) + moreover have "(- (n div 2) - 1) = ((-n - 1) div 2)" by auto + moreover have "(n mod 2 = 0) = ((- n - 1) mod 2 = 1)" by presburger + ultimately show ?case by (auto simp: bin_rest_def bin_last_def) +qed auto + +lemma bools_of_int_bin_to_bl[simp]: + "bools_of_int len n = bin_to_bl (nat len) n" + by (auto simp: bools_of_int_def Let_def map_Not_bin_to_bl rbl_succ[unfolded bin_to_bl_def]) + +end +*)
\ No newline at end of file diff --git a/lib/hol/Makefile b/lib/hol/Makefile index c863a05b..ccd871dc 100644 --- a/lib/hol/Makefile +++ b/lib/hol/Makefile @@ -1,7 +1,7 @@ LEM_DIR?=$(shell opam config var lem:share) LEMSRC = \ - ../../src/lem_interp/sail2_instr_kinds.lem \ + ../../src/gen_lib/sail2_instr_kinds.lem \ ../../src/gen_lib/sail2_values.lem \ ../../src/gen_lib/sail2_operators.lem \ ../../src/gen_lib/sail2_operators_mwords.lem \ diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 465b4c36..42071a8c 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -18,17 +18,17 @@ all: thys thys: $(THYS) heap-img: thys $(EXTRA_THYS) ROOT -ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),) - $(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable) -endif - isabelle build -b -d $(LEM_ISA_LIB) -D . + if [ -z "$(wildcard $(LEM_ISA_LIB)/ROOT)" ]; \ + then echo isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable; false; \ + else isabelle build -b -d $(LEM_ISA_LIB) -D . ; \ + fi manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex cp output/document/session_graph.pdf manual/document/Sail_session_graph.pdf make -C $(SAIL_RISCV) riscv_duopod isabelle build -d $(LEM_ISA_LIB) -d . -d $(SAIL_RISCV)/generated_definitions/isabelle -D manual -Sail2_instr_kinds.thy: ../../src/lem_interp/sail2_instr_kinds.lem +Sail2_instr_kinds.thy: ../../src/gen_lib/sail2_instr_kinds.lem lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< Sail2_values.thy: ../../src/gen_lib/sail2_values.lem Sail2_instr_kinds.thy diff --git a/lib/main.ml b/lib/main.ml index c1b6fcae..a3541c69 100644 --- a/lib/main.ml +++ b/lib/main.ml @@ -60,7 +60,8 @@ let options = Arg.align [ | [fname;addr] -> (fname, Nat_big_num.of_string addr) | _ -> raise (Arg.Bad (s ^ " not of form <filename>@<addr>")) in opt_raw_files := (file, addr) :: !opt_raw_files), - "<file@0xADDR> load a raw binary in memory at given address.")] + "<file@0xADDR> load a raw binary in memory at given address."); + ("-cycle-limit", Arg.Set_int (Sail_lib.opt_cycle_limit), "<int> exit after given number of instructions executed.")] let usage_msg = "Sail OCaml RTS options:" diff --git a/lib/regfp.sail b/lib/regfp.sail index 070ff524..86b3cf17 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -31,6 +31,7 @@ union diafp = { DIAFP_reg : regfp } +$ifdef ARM_SPEC enum read_kind = { Read_plain, Read_reserve, @@ -38,6 +39,7 @@ enum read_kind = { Read_exclusive, Read_exclusive_acquire, Read_stream, + Read_ifetch, Read_RISCV_acquire, Read_RISCV_strong_acquire, Read_RISCV_reserved, @@ -45,6 +47,22 @@ enum read_kind = { Read_RISCV_reserved_strong_acquire, Read_X86_locked } +$else +enum read_kind = { + Read_plain, + Read_reserve, + Read_acquire, + Read_exclusive, + Read_exclusive_acquire, + Read_stream, + Read_RISCV_acquire, + Read_RISCV_strong_acquire, + Read_RISCV_reserved, + Read_RISCV_reserved_acquire, + Read_RISCV_reserved_strong_acquire, + Read_X86_locked +} +$endif enum write_kind = { Write_plain, @@ -142,6 +160,20 @@ val __barrier = { ocaml: "Platform.barrier", c: "platform_barrier", _: "barrier" } : barrier_kind -> unit effect {barr} +val __branch_announce + = { ocaml: "Platform.branch_announce", c: "platform_branch_announce", _ : "branch_announce" } + : forall (constant 'addrsize : Int), 'addrsize in {32, 64}. + (int('addrsize), bits('addrsize)) -> unit + +val __cache_maintenance + = { ocaml: "Platform.cache_maintenance", c: "platform_cache_maintenance", _ : "cache_maintenance" } + : forall (constant 'addrsize : Int), 'addrsize in {32, 64}. + (cache_op_kind, int('addrsize), bits('addrsize)) -> unit + +val __instr_announce + = { ocaml: "Platform.instr_announce", c: "platform_instr_announce", _: "instr_announce" } + : forall 'n, 'n > 0. + bits('n) -> unit /* val __write : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {eamem,wmv} @@ -837,6 +837,15 @@ fbits bitvector_access(const lbits op, const sail_int n_mpz) return (fbits) mpz_tstbit(*op.bits, n); } +fbits update_fbits(const fbits op, const uint64_t n, const fbits bit) +{ + if ((bit & 1) == 1) { + return op | (bit << n); + } else { + return op & ~(bit << n); + } +} + void sail_unsigned(sail_int *rop, const lbits op) { /* Normal form of bv_t is always positive so just return the bits. */ @@ -288,6 +288,8 @@ void sail_truncateLSB(lbits *rop, const lbits op, const sail_int len); fbits bitvector_access(const lbits op, const sail_int n_mpz); +fbits update_fbits(const fbits op, const uint64_t n, const fbits bit); + void sail_unsigned(sail_int *rop, const lbits op); void sail_signed(sail_int *rop, const lbits op); |