From 7fc5222ef8daa887eab8a7d178a459c0c84d45f6 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 25 Feb 2019 14:53:57 +0000 Subject: Fix some builtins, and make mod_int return natural --- lib/arith.sail | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/arith.sail b/lib/arith.sail index 8825ac2f..20231de1 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -94,7 +94,7 @@ val mod_int = { lem: "integerMod", c: "tmod_int", coq: "Z.rem" -} : (int, int) -> int +} : (int, int) -> nat overload operator % = {mod_int} @@ -104,6 +104,6 @@ val abs_int = { lem: "abs_int", c: "abs_int", coq: "Z.abs" -} : (int, int) -> int +} : int -> int $endif -- cgit v1.2.3 From 2fd45fa939ddae7cdb31ee0495e622e6e6a6235f Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 20 Feb 2019 09:55:19 +0000 Subject: Coq: some work on bool simplification This introduces some simplification of informative booleans, but tries too hard to eliminate all of the existentials resulting in difficulties in and/or trees. --- lib/coq/Sail2_prompt.v | 14 ++++++++++++++ lib/coq/Sail2_values.v | 10 ++++++++++ 2 files changed, 24 insertions(+) (limited to 'lib') diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index bd0d7750..dc00fdd3 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -61,6 +61,20 @@ Definition and_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad Definition or_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E := l >>= (fun l => if l then returnm true else r). +Definition and_boolBM {rv E P Q} (l : monad rv (Bool P) E) (r : monad rv (Bool Q) E) : monad rv (Bool (P /\ Q)) E. +refine ( + l >>= (fun l => if l then r >>= fun r => if r then returnm (left _) else returnm (right _) else returnm (right _)) +). +all: tauto. +Defined. + +Definition or_boolBM {rv E P Q} (l : monad rv (Bool P) E) (r : monad rv (Bool Q) E) : monad rv (Bool (P \/ Q)) E. +refine ( + l >>= (fun l => if l then returnm (left _) else r >>= fun r => if r then returnm (left _) else returnm (right _)) +). +all: tauto. +Defined. + (*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 := match b with diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 943d850a..bd2c0fdb 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -64,6 +64,16 @@ Lemma projBool_false {P:Prop} {b:Bool P} : projBool b = false <-> ~P. destruct b; simpl; intuition. Qed. +Definition and_boolB {P Q} (l : Bool P) (r : Bool Q) : Bool (P /\ Q). +refine (if l then if r then left _ else right _ else right _). +all: tauto. +Defined. + +Definition or_boolB {P Q} (l : Bool P) (r : Bool Q) : Bool (P \/ Q). +refine (if l then left _ else if r then left _ else right _). +all: tauto. +Defined. + Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness. Definition generic_neq {T:Type} (x y:T) `{Decidable (x = y)} := negb Decidable_witness. -- cgit v1.2.3 From 143ae2d39ede6bef3e39e2ec4d407ddfdd281a0c Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 22 Feb 2019 12:22:06 +0000 Subject: Coq: more for informative booleans Make internal_plet produce annotations (with code to replace unusable type variables) Add mappings for bool kids at bindings Add version of and_bool that proves a property --- lib/coq/Sail2_prompt.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'lib') diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index dc00fdd3..f5d277e1 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -57,9 +57,37 @@ Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (0 < s Definition and_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E := l >>= (fun l => if l then r else returnm false). +Definition and_boolMP {rv E} {P Q R:bool->Prop} (x : monad rv {b:bool & P b} E) (y : monad rv {b:bool & Q b} E) + `{H:ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r))} + : monad rv {b:bool & R b} E. +refine ( + x >>= fun '(existT _ x p) => (if x return P x -> _ then + fun p => y >>= fun '(existT _ y _) => returnm (existT _ y _) + else fun p => returnm (existT _ false _)) p +). +* destruct H. change y with (andb true y). auto. +* destruct H. change false with (andb false false). apply fact. + assumption. + congruence. +Defined. + (*val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e*) Definition or_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E := l >>= (fun l => if l then returnm true else r). +Definition or_boolMP {rv E} {P Q R:bool -> Prop} (l : monad rv {b : bool & P b} E) (r : monad rv {b : bool & Q b} E) + `{ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r))} + : monad rv {b : bool & R b} E. +refine ( + l >>= fun '(existT _ l p) => + (if l return P l -> _ then fun p => returnm (existT _ true _) + else fun p => r >>= fun '(existT _ r _) => returnm (existT _ r _)) p +). +* destruct H. change true with (orb true true). apply fact. assumption. congruence. +* destruct H. change r with (orb false r). auto. +Defined. + +Definition build_trivial_ex {rv E} {T:Type} (x:monad rv T E) : monad rv {x : T & True} E := + x >>= fun x => returnm (existT _ x I). Definition and_boolBM {rv E P Q} (l : monad rv (Bool P) E) (r : monad rv (Bool Q) E) : monad rv (Bool (P /\ Q)) E. refine ( -- cgit v1.2.3 From f86ce3508a9909032d1168091989b65a796314a6 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 28 Feb 2019 16:47:00 +0000 Subject: Coq: Clean up rich boolean handling in backend Now generates something vaguely sensible for RISC-V, although the solver needs a little work. Adds type annotations around effectful, rich and/or expressions. --- lib/coq/Sail2_prompt.v | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'lib') diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index f5d277e1..741fa921 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -57,16 +57,16 @@ Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (0 < s Definition and_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E := l >>= (fun l => if l then r else returnm false). -Definition and_boolMP {rv E} {P Q R:bool->Prop} (x : monad rv {b:bool & P b} E) (y : monad rv {b:bool & Q b} E) +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 & R b} E. + : monad rv {b:bool & ArithFact (R b)} E. refine ( - x >>= fun '(existT _ x p) => (if x return P x -> _ then + x >>= fun '(existT _ x (Build_ArithFact _ p)) => (if x return P x -> _ then fun p => y >>= fun '(existT _ y _) => returnm (existT _ y _) else fun p => returnm (existT _ false _)) p ). -* destruct H. change y with (andb true y). auto. -* destruct H. change false with (andb false false). apply fact. +* constructor. destruct H. destruct a0. change y with (andb true y). auto. +* constructor. destruct H. change false with (andb false false). apply fact. assumption. congruence. Defined. @@ -74,20 +74,20 @@ Defined. (*val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e*) Definition or_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E := l >>= (fun l => if l then returnm true else r). -Definition or_boolMP {rv E} {P Q R:bool -> Prop} (l : monad rv {b : bool & P b} E) (r : monad rv {b : bool & Q b} E) +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 & R b} E. + : monad rv {b : bool & ArithFact (R b)} E. refine ( - l >>= fun '(existT _ l p) => + l >>= fun '(existT _ l (Build_ArithFact _ p)) => (if l return P l -> _ then fun p => returnm (existT _ true _) else fun p => r >>= fun '(existT _ r _) => returnm (existT _ r _)) p ). -* destruct H. change true with (orb true true). apply fact. assumption. congruence. -* destruct H. change r with (orb false r). auto. +* constructor. destruct H. change true with (orb true true). apply fact. assumption. congruence. +* constructor. destruct H. destruct a0. change r with (orb false r). auto. Defined. -Definition build_trivial_ex {rv E} {T:Type} (x:monad rv T E) : monad rv {x : T & True} E := - x >>= fun x => returnm (existT _ x 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_ArithFact _ I)). Definition and_boolBM {rv E P Q} (l : monad rv (Bool P) E) (r : monad rv (Bool Q) E) : monad rv (Bool (P /\ Q)) E. refine ( -- cgit v1.2.3 From 3e59f95ce23e24c5ccfa9e0475f0a3d4a070e318 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 28 Feb 2019 17:04:31 +0000 Subject: Coq: remove unused library definitions --- lib/coq/Sail2_prompt.v | 14 -------------- lib/coq/Sail2_values.v | 35 ----------------------------------- 2 files changed, 49 deletions(-) (limited to 'lib') diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 741fa921..bae8381e 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -89,20 +89,6 @@ Defined. 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 and_boolBM {rv E P Q} (l : monad rv (Bool P) E) (r : monad rv (Bool Q) E) : monad rv (Bool (P /\ Q)) E. -refine ( - l >>= (fun l => if l then r >>= fun r => if r then returnm (left _) else returnm (right _) else returnm (right _)) -). -all: tauto. -Defined. - -Definition or_boolBM {rv E P Q} (l : monad rv (Bool P) E) (r : monad rv (Bool Q) E) : monad rv (Bool (P \/ Q)) E. -refine ( - l >>= (fun l => if l then returnm (left _) else r >>= fun r => if r then returnm (left _) else returnm (right _)) -). -all: tauto. -Defined. - (*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 := match b with diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index bd2c0fdb..1b5da853 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -45,35 +45,6 @@ End Morphism. Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} := existT _ n H. -(* The informative boolean type. *) - -Definition Bool (P : Prop) : Type := {P} + {~P}. - -Definition build_Bool {P:Prop} (b:bool) `{ArithFact (b = true <-> P)} : Bool P. -refine (if sumbool_of_bool b then left _ else right _); -destruct H; subst; -intuition. -Defined. - -Definition projBool {P:Prop} (b:Bool P) : bool := if b then true else false. - -Lemma projBool_true {P:Prop} {b:Bool P} : projBool b = true <-> P. -destruct b; simpl; intuition. -Qed. -Lemma projBool_false {P:Prop} {b:Bool P} : projBool b = false <-> ~P. -destruct b; simpl; intuition. -Qed. - -Definition and_boolB {P Q} (l : Bool P) (r : Bool Q) : Bool (P /\ Q). -refine (if l then if r then left _ else right _ else right _). -all: tauto. -Defined. - -Definition or_boolB {P Q} (l : Bool P) (r : Bool Q) : Bool (P \/ Q). -refine (if l then left _ else if r then left _ else right _). -all: tauto. -Defined. - Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness. Definition generic_neq {T:Type} (x y:T) `{Decidable (x = y)} := negb Decidable_witness. @@ -1123,11 +1094,6 @@ Ltac extract_properties := let Hx := fresh "Hx" in destruct X as [x Hx] in *; change (projT1 (existT _ x Hx)) with x in * end. -(* We could also destruct any remaining Bools, if necessary. *) -Ltac extract_Bool_props := - repeat match goal with - | H:projBool _ = true |- _ => rewrite projBool_true in H - | H:projBool _ = false |- _ => rewrite projBool_false in H end. (* TODO: hyps, too? *) Ltac reduce_list_lengths := repeat match goal with |- context [length_list ?X] => @@ -1193,7 +1159,6 @@ Ltac prepare_for_solver := autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *) split_cases; extract_properties; - extract_Bool_props; repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end; unwrap_ArithFacts; destruct_exists; -- cgit v1.2.3 From 576fb915bc281ea8e59eba896e3404d2f85e918c Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 1 Mar 2019 10:41:33 +0000 Subject: Coq: add a little bit of boolean solving Just enough for RISC-V to go through --- lib/coq/Sail2_values.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'lib') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 1b5da853..e6c5e786 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1208,6 +1208,14 @@ prepare_for_solver; | constructor; eauto 3 with zarith sail (* The datatypes hints give us some list handling, esp In *) | constructor; drop_exists; eauto 3 with datatypes zarith sail + (* Booleans - and_boolMP *) + | match goal with |- ArithFact (forall l r:bool, _ -> _ -> exists _, _) => + constructor; intros l r H1 H2; + solve [exists l; destruct l; intuition | exists r; destruct l; intuition] + end + | match goal with |- context [@eq _ _ _] => + constructor; intuition + end | constructor; idtac "Unable to solve constraint"; dump_context; fail ]. (* Add an indirection so that you can redefine run_solver to fail to get -- cgit v1.2.3 From a3558b92aa7395b2c841c737d867bbe02c848e03 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 1 Mar 2019 18:19:27 +0000 Subject: Coq: some library compatibility changes --- lib/coq/Sail2_string.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'lib') diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v index 0a00f8d7..543b0fad 100644 --- a/lib/coq/Sail2_string.v +++ b/lib/coq/Sail2_string.v @@ -188,3 +188,6 @@ Definition decimal_string_of_bv {a} `{Bitvector a} (bv : a) : string := Definition decimal_string_of_bits {n} (bv : mword n) : string := decimal_string_of_bv bv. +(* Some aliases for compatibility. *) +Definition dec_str := string_of_int. +Definition concat_str := String.append. -- cgit v1.2.3