diff options
| -rw-r--r-- | lib/coq/Hoare.v | 54 | ||||
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 140 | ||||
| -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 | 41 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_lemmas.v | 21 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_monad.v | 4 | ||||
| -rw-r--r-- | lib/coq/Sail2_string.v | 34 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 665 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 181 | ||||
| -rw-r--r-- | test/coq/pass/booltyparam.sail | 11 |
12 files changed, 888 insertions, 403 deletions
diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v index c91814b0..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 => @@ -608,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 @@ -645,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 @@ -774,7 +774,7 @@ 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) : +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. @@ -793,7 +793,7 @@ induction (S (Z.abs_nat (from - to))); intros. + 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) : +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. @@ -1038,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. @@ -1049,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. @@ -1111,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 @@ -1152,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 @@ -1164,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/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index 698ca51b..9970dcd5 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -43,11 +43,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 +100,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 +114,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 +125,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 +135,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 +149,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 +164,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 +182,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 +191,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 +203,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 +214,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 +239,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 +288,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 +326,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 +355,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 +398,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 +485,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 +520,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 +571,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 +586,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 +596,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 +608,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 0cfc9f17..7c751bc7 100644 --- a/lib/coq/Sail2_state.v +++ b/lib/coq/Sail2_state.v @@ -30,34 +30,31 @@ Fixpoint foreachS {A RV Vars E} (xs : list A) (vars : Vars) (body : A -> Vars -> foreachS xs vars body end. -(* This uses the same subproof as the prompt version to get around proof relevance issues - in Sail2_state_lemmas. TODO: if we switch to boolean properties this shouldn't be - necessary. *) -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. +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) (foreach_ZM_up'_subproof _ _ _ _ _ _ LE) vars >>$= fun vars => foreach_ZS_up' rv e Vars from to step (off + step) n _ (foreach_ZM_up'_subproof0 _ _ _ _) vars body + | 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. +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) (foreach_ZM_down'_subproof _ _ _ _ _ _ LE) vars >>$= fun vars => foreach_ZS_down' _ _ _ from to step (off - step) n _ (foreach_ZM_down'_subproof0 _ _ _ _) vars body + | 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)} := +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)} := +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*) @@ -73,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 := @@ -114,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 @@ -199,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 e5394f32..ef82084f 100644 --- a/lib/coq/Sail2_state_lemmas.v +++ b/lib/coq/Sail2_state_lemmas.v @@ -196,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 *) @@ -288,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 ] @@ -513,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. @@ -729,6 +740,8 @@ induction (S (Z.abs_nat (from - to))); intros. 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. @@ -750,6 +763,8 @@ induction (S (Z.abs_nat (from - to))); intros. 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. @@ -805,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_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 404d585d..48920a59 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -14,6 +14,7 @@ Require Import Lia. Import ListNotations. Open Scope Z. +Open Scope bool. Module Z_eq_dec. Definition U := Z. @@ -26,27 +27,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. @@ -132,16 +180,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. @@ -149,23 +201,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); @@ -206,6 +258,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 := (<) @@ -817,19 +876,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). @@ -886,15 +951,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. @@ -970,7 +1035,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)). @@ -979,16 +1044,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 *) @@ -1057,20 +1124,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. *) @@ -1083,17 +1139,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 @@ -1108,15 +1201,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 @@ -1131,12 +1238,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 *) @@ -1361,10 +1476,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. @@ -1418,7 +1535,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; @@ -1427,9 +1543,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)). @@ -1437,14 +1553,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 @@ -1479,6 +1600,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. *) @@ -1497,8 +1683,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 @@ -1529,6 +1715,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] @@ -1627,7 +1814,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. @@ -1656,41 +1843,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 *) @@ -1758,7 +1977,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. @@ -1766,6 +1984,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 ]. @@ -1779,21 +2000,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. @@ -1815,18 +2149,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 ]. @@ -1836,6 +2183,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. @@ -1855,13 +2203,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. - -Definition to_range (x : Z) : {y : Z & ArithFact (x <= y <= x)} := build_ex x. - +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. -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)); @@ -2194,7 +2540,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 @@ -2202,7 +2548,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 @@ -2210,9 +2556,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 @@ -2305,27 +2651,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). @@ -2333,15 +2679,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. @@ -2389,21 +2738,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. @@ -2423,6 +2776,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. @@ -2461,51 +2815,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/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 3a37d9ff..867a1c84 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -93,7 +93,7 @@ type context = { kid_renames : kid KBindings.t; (* Plain tyvar -> tyvar renames, used to avoid variable/type variable name clashes *) (* Note that as well as these kid renames, we also attempt to replace entire - n_constraints with equivalent variables in doc_nc_prop and doc_nc_exp. *) + n_constraints with equivalent variables in doc_nc_exp. *) kid_id_renames : (id option) KBindings.t; (* tyvar -> argument renames *) kid_id_renames_rev : kid Bindings.t; (* reverse of kid_id_renames *) bound_nvars : KidSet.t; @@ -388,16 +388,12 @@ match nc1, nc2 with | _,_ -> mk_nc (NC_app (mk_id "iff",[arg_bool nc1; arg_bool nc2])) (* n_constraint functions are currently just Z3 functions *) -let doc_nc_fn_prop id = - match string_of_id id with - | "not" -> string "not" - | _ -> doc_id_type id - -(* n_constraint functions are currently just Z3 functions *) -let doc_nc_fn id = - match string_of_id id with - | "not" -> string "negb" - | s -> string s +let doc_nc_fn (Id_aux (id,_) as full_id) = + match id with + | Id "not" -> string "negb" + | Operator "-->" -> string "implb" + | Id "iff" -> string "Bool.eqb" + | _ -> doc_id full_id let merge_kid_count = KBindings.union (fun _ m n -> Some (m+n)) @@ -622,7 +618,7 @@ let rec doc_typ_fns ctx env = | Bool_boring -> string "bool" | Bool_complex (_,_,atom_nc) -> (* simplify won't introduce new kopts *) let var = mk_kid "_bool" in (* TODO collision avoid *) - let nc = nice_iff (nc_var var) atom_nc in + let nc = nice_iff atom_nc (nc_var var) in braces (separate space [doc_var ctx var; colon; string "bool"; ampersand; @@ -676,7 +672,7 @@ let rec doc_typ_fns ctx env = let length_constraint_pp = if KidSet.is_empty (KidSet.inter kid_set (nexp_frees m)) then None - else Some (separate space [len_pp; doc_var ctx var; equals; doc_nexp ctx m]) + else Some (separate space [len_pp; doc_var ctx var; string "=?"; doc_nexp ctx m]) in braces (separate space [doc_var ctx var; colon; tpp; @@ -694,7 +690,7 @@ let rec doc_typ_fns ctx env = let length_constraint_pp = if KidSet.is_empty (KidSet.inter kid_set (nexp_frees m)) then None - else Some (separate space [len_pp; doc_var ctx var; equals; doc_nexp ctx m]) + else Some (separate space [len_pp; doc_var ctx var; string "=?"; doc_nexp ctx m]) in braces (separate space [doc_var ctx var; colon; tpp; @@ -705,7 +701,7 @@ let rec doc_typ_fns ctx env = | Bool_boring -> string "bool" | Bool_complex (kopts,nc,atom_nc) -> let var = mk_kid "_bool" in (* TODO collision avoid *) - let nc = nice_and (nice_iff (nc_var var) atom_nc) nc in + let nc = nice_and (nice_iff atom_nc (nc_var var)) nc in braces (separate space [doc_var ctx var; colon; string "bool"; ampersand; @@ -773,94 +769,26 @@ let rec doc_typ_fns ctx env = | A_typ t -> app_typ true t | A_nexp n -> doc_nexp ctx n | A_order o -> empty - | A_bool nc -> doc_nc_prop ~prop_vars ~top:false ctx env nc + | A_bool nc -> parens (doc_nc_exp ctx env nc) in typ', atomic_typ, doc_typ_arg and doc_typ ctx env = let f,_,_ = doc_typ_fns ctx env in f and doc_atomic_typ ctx env = let _,f,_ = doc_typ_fns ctx env in f and doc_typ_arg ctx env = let _,_,f = doc_typ_fns ctx env in f -and doc_arithfact ?(prop_vars=false) ctxt env ?(exists = []) ?extra nc = - let prop = doc_nc_prop ~prop_vars ctxt env nc in +and doc_arithfact ctxt env ?(exists = []) ?extra nc = + let prop = doc_nc_exp ctxt env nc in let prop = match extra with | None -> prop - | Some pp -> separate space [pp; string "/\\"; parens prop] - in - let prop = - match exists with - | [] -> prop - | _ -> separate space ([string "exists"]@(List.map (doc_var ctxt) exists)@[comma; prop]) + | Some pp -> separate space [parens pp; string "&&"; parens prop] in - string "ArithFact" ^^ space ^^ parens prop + let prop = prop in + match exists with + | [] -> string "ArithFact" ^^ space ^^ parens prop + | _ -> string "ArithFactP" ^^ space ^^ + parens (separate space ([string "exists"]@(List.map (doc_var ctxt) exists)@[comma; prop; equals; string "true"])) (* Follows Coq precedence levels *) -and doc_nc_prop ?(top = true) ?(prop_vars = false) ctx env nc = - let locals = Env.get_locals env |> Bindings.bindings in - let nc = Env.expand_constraint_synonyms env nc in - let doc_nc_var varpp = - if prop_vars then varpp else doc_op equals varpp (string "true") - in - let nc_id_map = - List.fold_left - (fun m (v,(_,Typ_aux (typ,_))) -> - match typ with - | Typ_app (id, [A_aux (A_bool nc,_)]) when string_of_id id = "atom_bool" -> - (flatten_nc nc, v)::m - | _ -> m) [] locals - in - let rec newnc f nc = - let ncs = flatten_nc nc in - let candidates = - Util.map_filter (fun (ncs',id) -> Util.option_map (fun x -> x,id) (list_contains NC.compare ncs ncs')) nc_id_map - in - match List.sort (fun (l,_) (l',_) -> compare l l') candidates with - | ([],id)::_ -> parens (doc_nc_var (doc_id id)) - | ((h::t),id)::_ -> parens (doc_op (string "/\\") (parens (doc_nc_var (doc_id id))) (l80 (List.fold_left nc_and h t))) - | [] -> f nc - and l85 (NC_aux (nc,_) as nc_full) = - match nc with - | NC_or (nc1, nc2) -> doc_op (string "\\/") (newnc l80 nc1) (newnc l85 nc2) - | _ -> l80 nc_full - and l80 (NC_aux (nc,_) as nc_full) = - match nc with - | NC_and (nc1, nc2) -> doc_op (string "/\\") (newnc l70 nc1) (newnc l80 nc2) - | _ -> l70 nc_full - and l70 (NC_aux (nc,_) as nc_full) = - match nc with - | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_var kid -> doc_nc_var (doc_nexp ctx (nvar kid)) - | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_bounded_gt (ne1, ne2) -> doc_op (string ">") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_bounded_le (ne1, ne2) -> doc_op (string "<=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_bounded_lt (ne1, ne2) -> doc_op (string "<") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_not_equal (ne1, ne2) -> doc_op (string "<>") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | _ -> l10 nc_full - and l10 (NC_aux (nc,_) as nc_full) = - match nc with - | NC_set (kid, is) -> - separate space [string "In"; doc_var ctx kid; - brackets (separate (string "; ") - (List.map (fun i -> string (Nat_big_num.to_string i)) is))] - | NC_app (f,args) -> separate space (doc_nc_fn_prop f::List.map (doc_typ_arg ~prop_vars ctx env) args) - | _ -> l0 nc_full - and l0 (NC_aux (nc,_) as nc_full) = - match nc with - | NC_true -> string "True" - | NC_false -> string "False" - | NC_set _ - | NC_app _ - | NC_var _ - | NC_or _ - | NC_and _ - | NC_equal _ - | NC_bounded_ge _ - | NC_bounded_gt _ - | NC_bounded_le _ - | NC_bounded_lt _ - | NC_not_equal _ -> parens (l85 nc_full) - in if top then newnc l85 nc else newnc l0 nc - -(* Follows Coq precedence levels *) -let rec doc_nc_exp ctx env nc = +and doc_nc_exp ctx env nc = let locals = Env.get_locals env |> Bindings.bindings in let nc = Env.expand_constraint_synonyms env nc in let nc_id_map = @@ -871,6 +799,9 @@ let rec doc_nc_exp ctx env nc = (flatten_nc nc, v)::m | _ -> m) [] locals in + (* Look for variables in the environment which exactly express the nc, and use + them instead. As well as often being shorter, this avoids unbound type + variables added by Sail's type checker. *) let rec newnc f nc = let ncs = flatten_nc nc in let candidates = @@ -903,10 +834,16 @@ let rec doc_nc_exp ctx env nc = separate space [string "member_Z_list"; doc_var ctx kid; brackets (separate (string "; ") (List.map (fun i -> string (Nat_big_num.to_string i)) is))] + | NC_app (f,args) -> separate space (doc_nc_fn f::List.map doc_typ_arg_exp args) + | _ -> l0 nc_full + and l0 (NC_aux (nc,_) as nc_full) = + match nc with | NC_true -> string "true" | NC_false -> string "false" - | NC_app (f,args) -> separate space (doc_nc_fn f::List.map (doc_typ_arg_exp ctx env) args) | NC_var kid -> doc_nexp ctx (nvar kid) + | NC_not_equal _ + | NC_set _ + | NC_app _ | NC_equal _ | NC_bounded_ge _ | NC_bounded_gt _ @@ -914,13 +851,13 @@ let rec doc_nc_exp ctx env nc = | NC_bounded_lt _ | NC_or _ | NC_and _ -> parens (l70 nc_full) - in newnc l70 nc -and doc_typ_arg_exp ctx env (A_aux (arg,l)) = - match arg with - | A_nexp nexp -> doc_nexp ctx nexp - | A_bool nc -> doc_nc_exp ctx env nc - | A_order _ | A_typ _ -> + and doc_typ_arg_exp (A_aux (arg,l)) = + match arg with + | A_nexp nexp -> doc_nexp ctx nexp + | A_bool nc -> newnc l0 nc + | A_order _ | A_typ _ -> raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function") + in newnc l70 nc (* Check for variables in types that would be pretty-printed and are not bound in the val spec of the function. *) @@ -1024,7 +961,7 @@ let doc_quant_item_constr ?(prop_vars=false) ctx env delimit (QI_aux (qi,_)) = match qi with | QI_id _ -> None | QI_constant _ -> None - | QI_constraint nc -> Some (bquote ^^ braces (doc_arithfact ~prop_vars ctx env nc)) + | QI_constraint nc -> Some (bquote ^^ braces (doc_arithfact ctx env nc)) (* At the moment these are all anonymous - when used we rely on Coq to fill them in. *) @@ -2515,9 +2452,9 @@ let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = let idpp = doc_id_type id in doc_op coloneq (separate space [string "Definition"; idpp; - doc_typquant_items ~prop_vars:true empty_ctxt Env.empty parens typq; - colon; string "Prop"]) - (doc_nc_prop ~prop_vars:true empty_ctxt Env.empty nc) ^^ dot ^^ hardline ^^ + doc_typquant_items empty_ctxt Env.empty parens typq; + colon; string "bool"]) + (doc_nc_exp empty_ctxt Env.empty nc) ^^ dot ^^ hardline ^^ separate space [string "Hint Unfold"; idpp; colon; string "sail."] ^^ twice hardline | TD_abbrev _ -> empty (* TODO? *) @@ -2538,24 +2475,31 @@ let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = mk_typ (Typ_app (id, targs)) | TypQ_aux (TypQ_no_forall, _) -> mk_id_typ id in let fs_doc = group (separate_map (break 1) f_pp fs) in + let type_id_pp = doc_id_type id in + let match_parameters = + let (kopts,_) = quant_split typq in + match kopts with + | [] -> empty + | _ -> space ^^ separate_map space (fun _ -> underscore) kopts + in let doc_update_field (_,fid) = let idpp = fname fid in - let otherfield (_,fid') = - if Id.compare fid fid' == 0 then None else - let idpp = fname fid' in - Some (separate space [idpp; string ":="; idpp; string "r"]) + let pp_field alt i (_,fid') = + if Id.compare fid fid' == 0 then string alt else + let id = "f" ^ string_of_int i in + string id in match fs with | [_] -> string "Notation \"{[ r 'with' '" ^^ idpp ^^ string "' := e ]}\" :=" ^//^ string "{| " ^^ idpp ^^ string " := e |} (only parsing)." | _ -> - string "Notation \"{[ r 'with' '" ^^ idpp ^^ string "' := e ]}\" := {|" ^//^ - idpp ^^ string " := e;" ^/^ separate (semi ^^ break 1) (Util.map_filter otherfield fs) ^/^ - string "|}" ^^ dot + string "Notation \"{[ r 'with' '" ^^ idpp ^^ string "' := e ]}\" :=" ^//^ + string "match r with Build_" ^^ type_id_pp ^^ match_parameters ^^ space ^^ separate space (List.mapi (pp_field "_") fs) ^^ string " =>" ^//^ + string "Build_" ^^ type_id_pp ^^ match_parameters ^^ space ^^ separate space (List.mapi (pp_field "e") fs) ^//^ + string "end" ^^ dot in let updates_pp = separate hardline (List.map doc_update_field fs) in - let id_pp = doc_id_type id in let numfields = List.length fs in let intros_pp s = string " intros [" ^^ @@ -2564,8 +2508,8 @@ let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = in let eq_pp = if IdSet.mem id generic_eq_types then - string "Instance Decidable_eq_" ^^ id_pp ^^ space ^^ colon ^/^ - string "forall (x y : " ^^ id_pp ^^ string "), Decidable (x = y)." ^^ + string "Instance Decidable_eq_" ^^ type_id_pp ^^ space ^^ colon ^/^ + string "forall (x y : " ^^ type_id_pp ^^ string "), Decidable (x = y)." ^^ hardline ^^ intros_pp "x" ^^ intros_pp "y" ^^ separate hardline (list_init numfields (fun n -> @@ -2576,9 +2520,9 @@ let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = string "Defined." ^^ twice hardline else empty in - let reset_implicits_pp = doc_reset_implicits id_pp typq in + let reset_implicits_pp = doc_reset_implicits type_id_pp typq in doc_op coloneq - (separate space [string "Record"; id_pp; doc_typquant_items empty_ctxt Env.empty braces typq]) + (separate space [string "Record"; type_id_pp; doc_typquant_items empty_ctxt Env.empty braces typq]) ((*doc_typquant typq*) (braces (space ^^ align fs_doc ^^ space))) ^^ dot ^^ hardline ^^ reset_implicits_pp ^^ hardline ^^ eq_pp ^^ updates_pp ^^ twice hardline @@ -2743,7 +2687,7 @@ let rec atom_constraint ctxt (pat, typ) = None | _ -> Some (bquote ^^ braces (string "ArithFact" ^^ space ^^ - parens (doc_op equals (doc_id id) (doc_nexp ctxt nexp))))) + parens (doc_op (string "=?") (doc_id id) (doc_nexp ctxt nexp))))) | P_aux (P_typ (_,p),_), _ -> atom_constraint ctxt (p, typ) | _ -> None @@ -3205,7 +3149,7 @@ let doc_axiom_typschm typ_env l (tqs,typ) = let v = fresh_var () in parens (v ^^ string " : Z") ^/^ bquote ^^ braces (string "ArithFact " ^^ - parens (v ^^ string " = " ^^ string (Big_int.to_string n))) + parens (v ^^ string " =? " ^^ string (Big_int.to_string n))) | _ -> match Type_check.destruct_atom_bool typ_env typ with | Some (NC_aux (NC_var kid,_)) when KidSet.mem kid args -> @@ -3377,6 +3321,7 @@ try hardline; string "Open Scope string."; hardline; string "Open Scope bool."; hardline; + string "Open Scope Z."; hardline; hardline; hardline; separate empty (List.map doc_def defs); diff --git a/test/coq/pass/booltyparam.sail b/test/coq/pass/booltyparam.sail new file mode 100644 index 00000000..423c2720 --- /dev/null +++ b/test/coq/pass/booltyparam.sail @@ -0,0 +1,11 @@ +/* Test a boolean type parameter. Not sure that this is terribly useful, + but it fills a gap in coverage... */ + +$include <prelude.sail> + +union perhaps('b : Bool) = {No : unit, Yes : {'n, 'b. atom('n)}} + +val foo : forall 'n. atom('n) -> perhaps('n >= 0) + +function foo(n) = + if n >= 0 then Yes(n) else No() |