From aeba539412d37f4e0f6b8e02bea7389b433fbb80 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 29 Nov 2019 15:09:17 +0000 Subject: Coq: switch to boolean predicates for Sail-type properties - ArithFact takes a boolean predicate - defined in terms of ArithFactP, which takes a Prop predicate, and is used directly for existentials - used abstract in more definitions with direct proofs - beef up solve_bool_with_Z to handle more equalities, andb and orb --- lib/coq/Hoare.v | 36 ++-- lib/coq/Sail2_operators_mwords.v | 100 ++++++----- lib/coq/Sail2_prompt.v | 65 +++---- lib/coq/Sail2_prompt_monad.v | 4 +- lib/coq/Sail2_state.v | 34 ++-- lib/coq/Sail2_state_lemmas.v | 7 +- lib/coq/Sail2_state_monad.v | 4 +- lib/coq/Sail2_string.v | 16 +- lib/coq/Sail2_values.v | 362 ++++++++++++++++++++++++--------------- src/pretty_print_coq.ml | 73 ++++---- 10 files changed, 415 insertions(+), 286 deletions(-) diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v index c91814b0..44a81971 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 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 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. diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index 698ca51b..dfc7fc46 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 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 = 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 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 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,15 @@ induction n. reflexivity. Qed. -Program Definition uint {a} (x : mword a) : {z : Z & ArithFact (0 <= z /\ z <= 2 ^ a - 1)} := +Program Definition uint {a} (x : mword a) : {z : Z & ArithFact (0 <=? z <=? 2 ^ a - 1)} := existT _ (Z.of_N (Word.wordToN (get_word 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 +323,14 @@ 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)} := +Program Definition sint {a} `{ArithFact (a >? 0)} (x : mword a) : {z : Z & ArithFact (-(2^(a-1)) <=? z <=? 2 ^ (a-1) - 1)} := existT _ (Word.wordToZ (get_word x)) _. Next Obligation. 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 +348,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 +391,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 +478,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 @@ -520,7 +542,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 +557,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 = 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 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 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 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_state.v b/lib/coq/Sail2_state.v index 0cfc9f17..51a8e5fd 100644 --- a/lib/coq/Sail2_state.v +++ b/lib/coq/Sail2_state.v @@ -33,7 +33,7 @@ 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 monadS rv Vars e) {struct n} : monadS rv Vars e. exact ( match sumbool_of_bool (from + off <=? to) with left LE => match n with @@ -44,7 +44,7 @@ exact ( 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 monadS rv Vars e) {struct n} : monadS rv Vars e. exact ( match sumbool_of_bool (to <=? from + off) with left LE => match n with @@ -55,9 +55,9 @@ exact ( 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 monadS 'rv 'a 'e) -> nat -> monadS 'rv (list 'a) 'e*) @@ -73,22 +73,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 +114,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 +199,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..39406208 100644 --- a/lib/coq/Sail2_state_lemmas.v +++ b/lib/coq/Sail2_state_lemmas.v @@ -196,8 +196,7 @@ 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. (* Monad lifting *) @@ -513,6 +512,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. @@ -805,7 +806,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..152c003a 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) => diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 404d585d..d25ab00b 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,8 +27,14 @@ 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. @@ -35,18 +42,17 @@ Defined. 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 +138,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 -> 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. @@ -206,6 +216,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 +834,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 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 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 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 +993,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 +1002,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,7 +1082,7 @@ 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. *) @@ -1083,7 +1108,7 @@ 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 ArithFact_mword (a : Z) (w : mword a) : ArithFact (a >=? 0). constructor. destruct a. auto with zarith. @@ -1091,9 +1116,16 @@ auto using Z.le_ge, Zle_0_pos. destruct w. Qed. Ltac unwrap_ArithFacts := - repeat match goal with H:(ArithFact _) |- _ => let H' := fresh H in case H as [H']; clear H end. + repeat match goal with + | H:(ArithFact _) |- _ => let H' := fresh H in case H as [H']; clear H + | H:(ArithFactP _) |- _ => let H' := fresh H in case H as [H']; clear H + end. Ltac unbool_comparisons := repeat match goal with + | 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: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,6 +1140,8 @@ 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 _ _ = true] |- _ => rewrite Bool.eqb_true_iff in H + | 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 @@ -1131,6 +1165,8 @@ 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 @@ -1361,10 +1397,16 @@ end; (* We may have uncovered more conjunctions *) repeat match goal with H:and _ _ |- _ => destruct H end. +(* Remove details of embedded proofs and provide a copy that nothing + depends upon so that rewrites on it will work. *) Ltac generalize_embedded_proofs := + let gen X := + let Y := fresh "Y" in pose X as Y; generalize Y; generalize dependent X + in repeat match goal with H:context [?X] |- _ => - match type of X with ArithFact _ => - generalize dependent X + match type of X with + | ArithFact _ => gen X + | ArithFactP _ => gen X end end; intros. @@ -1427,9 +1469,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 +1479,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 +1526,61 @@ 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. + +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 * + | 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; + 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. (* A more ambitious brute force existential solver. *) @@ -1497,8 +1599,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 | intuition] end. (* A straightforward solver for simple problems like @@ -1657,40 +1759,6 @@ Ltac z_comparisons := | exact Z_compare_gt_eq ]. -(* 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. - -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 *) @@ -1779,21 +1847,29 @@ 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. 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); +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. @@ -1819,14 +1895,17 @@ Ltac clear_fixpoints := Ltac solve_arithfact := 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 | 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; unbool_comparisons_goal; reflexivity | constructor; repeat match goal with |- and _ _ => split end; z_comparisons | run_main_solver ]. @@ -1836,6 +1915,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 +1935,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 +2272,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 Vars) {struct n} : Vars := if sumbool_of_bool (from + off <=? to) then match n with | O => vars @@ -2202,7 +2280,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 Vars) {struct n} : Vars := if sumbool_of_bool (to <=? from + off) then match n with | O => vars @@ -2210,9 +2288,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 (vars -> bool) -> (vars -> vars) -> vars @@ -2305,27 +2383,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 +2411,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 = 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 +2470,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 Some (existT _ v' _) end. Next Obligation. +intros; cbv beta. rewrite <- (just_list_length_Z _ _ Heq_anonymous). destruct v. assumption. @@ -2461,51 +2547,59 @@ 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]. +unbool_comparisons. assert (H : 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. +apply member_Z_list_In in HR. +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..8b147572 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -394,10 +394,12 @@ let doc_nc_fn_prop id = | _ -> 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 +624,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 +678,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 +696,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 +707,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; @@ -779,18 +781,17 @@ 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 = @@ -860,7 +861,7 @@ and doc_nc_prop ?(top = true) ?(prop_vars = false) ctx env nc = 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 +872,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 +907,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 +924,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 +1034,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 +2525,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? *) @@ -2743,7 +2753,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 +3215,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 +3387,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); -- cgit v1.2.3