diff options
Diffstat (limited to 'lib')
29 files changed, 1030 insertions, 168 deletions
diff --git a/lib/coq/Makefile b/lib/coq/Makefile index 816a6c3d..97869e3c 100644 --- a/lib/coq/Makefile +++ b/lib/coq/Makefile @@ -1,4 +1,4 @@ -BBV_DIR=../../../bbv +BBV_DIR=../../../bbv/theories SRC=Sail2_prompt_monad.v Sail2_prompt.v Sail2_impl_base.v Sail2_instr_kinds.v Sail2_operators_bitlists.v Sail2_operators_mwords.v Sail2_operators.v Sail2_values.v Sail2_state_monad.v Sail2_state.v diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index ee98c94e..bb4bf053 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -3,6 +3,7 @@ Require Import Sail2_operators. Require Import Sail2_prompt_monad. Require Import Sail2_prompt. Require Import bbv.Word. +Require bbv.BinNotation. Require Import Arith. Require Import ZArith. Require Import Omega. @@ -267,8 +268,8 @@ Definition msb := most_significant val int_of_vec : forall 'a. Size 'a => bool -> mword 'a -> integer Definition int_of_vec := int_of_bv -val string_of_vec : forall 'a. Size 'a => mword 'a -> string -Definition string_of_vec := string_of_bv*) +val string_of_vec : forall 'a. Size 'a => mword 'a -> string*) +Definition string_of_bits {n} (w : mword n) : string := string_of_bv w. Definition with_word' {n} (P : Type -> Type) : (forall n, Word.word n -> P (Word.word n)) -> mword n -> P (mword n) := fun f w => @with_word n _ (f (Z.to_nat n)) w. Definition word_binop {n} (f : forall n, Word.word n -> Word.word n -> Word.word n) : mword n -> mword n -> mword n := with_word' (fun x => x -> x) f. Definition word_unop {n} (f : forall n, Word.word n -> Word.word n) : mword n -> mword n := with_word' (fun x => x) f. diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 336ca8de..c98e2926 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -30,6 +30,27 @@ match l with foreachM xs vars body end. +Fixpoint foreach_ZM_up' {rv e Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e := + if sumbool_of_bool (from + off <=? to) then + match n with + | O => returnm vars + | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_up' from to step (off + step) n vars body + end + else returnm vars. + +Fixpoint foreach_ZM_down' {rv e Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e := + if sumbool_of_bool (to <=? from + off) then + match n with + | O => returnm vars + | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_down' from to step (off - step) n vars body + end + else returnm vars. + +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)} := + 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*) (*val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e*) diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 137be85c..0ce6134f 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -2,6 +2,7 @@ (*Require Import Sail_impl_base*) Require Export ZArith. +Require Import Ascii. Require Export String. Require Import bbv.Word. Require Export List. @@ -72,7 +73,13 @@ Definition nn := nat. (*val pow : Z -> Z -> Z*) Definition pow m n := m ^ n. -Definition pow2 n := 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. +Qed. + (* Definition inline lt := (<) Definition inline gt := (>) @@ -105,7 +112,15 @@ Definition negate_real r := realNegate r Definition abs_real r := realAbs r Definition power_real b e := realPowInteger b e*) +Definition print_endline (_ : string) : unit := tt. +Definition prerr_endline (_ : string) : unit := tt. +Definition prerr (_ : string) : unit := tt. Definition print_int (_ : string) (_ : Z) : unit := tt. +Definition prerr_int (_ : string) (_ : Z) : unit := tt. +Definition putchar (_ : Z) : unit := tt. + +Definition shl_int := Z.shiftl. +Definition shr_int := Z.shiftr. (* Definition or_bool l r := (l || r) @@ -123,9 +138,29 @@ Fixpoint repeat' {a} (xs : list a) n := | O => [] | S n => xs ++ repeat' xs n end. +Lemma repeat'_length {a} {xs : list a} {n : nat} : List.length (repeat' xs n) = (n * List.length xs)%nat. +induction n. +* reflexivity. +* simpl. + rewrite app_length. + auto with arith. +Qed. Definition repeat {a} (xs : list a) (n : Z) := if n <=? 0 then [] else repeat' xs (Z.to_nat n). +Lemma repeat_length {a} {xs : list a} {n : Z} (H : n >= 0) : length_list (repeat xs n) = n * length_list xs. +unfold length_list, repeat. +destruct n. ++ reflexivity. ++ simpl (List.length _). + rewrite repeat'_length. + rewrite Nat2Z.inj_mul. + rewrite positive_nat_Z. + reflexivity. ++ exfalso. + auto with zarith. +Qed. + (*declare {isabelle} termination_argument repeat = automatic Definition duplicate_to_list bit length := repeat [bit] length @@ -186,6 +221,48 @@ lemma just_list_spec: ((forall xs. (just_list xs = None) <-> List.elem None xs) && (forall xs es. (just_list xs = Some es) <-> (xs = List.map Some es)))*) +Lemma just_list_length {A} : forall (l : list (option A)) (l' : list A), + Some l' = just_list l -> List.length l = List.length l'. +induction l. +* intros. + simpl in H. + inversion H. + reflexivity. +* intros. + destruct a; simplify_eq H. + simpl in *. + destruct (just_list l); simplify_eq H. + intros. + subst. + simpl. + f_equal. + apply IHl. + reflexivity. +Qed. + +Lemma just_list_length_Z {A} : forall (l : list (option A)) l', Some l' = just_list l -> length_list l = length_list l'. +unfold length_list. +intros. +f_equal. +auto using just_list_length. +Qed. + +Fixpoint member_Z_list (x : Z) (l : list Z) : bool := +match l with +| [] => false +| h::t => if x =? h then true else member_Z_list x t +end. + +Lemma member_Z_list_In {x l} : member_Z_list x l = true <-> In x l. +induction l. +* simpl. split. congruence. tauto. +* simpl. destruct (x =? a) eqn:H. + + rewrite Z.eqb_eq in H. subst. tauto. + + rewrite Z.eqb_neq in H. split. + - intro Heq. right. apply IHl. assumption. + - intros [bad | good]. congruence. apply IHl. assumption. +Qed. + (*** Bits *) Inductive bitU := B0 | B1 | BU. @@ -196,6 +273,13 @@ match b with | BU => "U" end%string. +Definition bitU_char b := +match b with +| B0 => "0" +| B1 => "1" +| BU => "?" +end%char. + (*instance (Show bitU) let show := showBitU end*) @@ -463,47 +547,52 @@ Definition arith_op_bits (op : Z -> Z -> Z) (sign : bool) l r := end. -(* -Definition char_of_nibble := function - | (B0, B0, B0, B0) => Some #'0' - | (B0, B0, B0, B1) => Some #'1' - | (B0, B0, B1, B0) => Some #'2' - | (B0, B0, B1, B1) => Some #'3' - | (B0, B1, B0, B0) => Some #'4' - | (B0, B1, B0, B1) => Some #'5' - | (B0, B1, B1, B0) => Some #'6' - | (B0, B1, B1, B1) => Some #'7' - | (B1, B0, B0, B0) => Some #'8' - | (B1, B0, B0, B1) => Some #'9' - | (B1, B0, B1, B0) => Some #'A' - | (B1, B0, B1, B1) => Some #'B' - | (B1, B1, B0, B0) => Some #'C' - | (B1, B1, B0, B1) => Some #'D' - | (B1, B1, B1, B0) => Some #'E' - | (B1, B1, B1, B1) => Some #'F' +Definition char_of_nibble x := + match x with + | (B0, B0, B0, B0) => Some "0"%char + | (B0, B0, B0, B1) => Some "1"%char + | (B0, B0, B1, B0) => Some "2"%char + | (B0, B0, B1, B1) => Some "3"%char + | (B0, B1, B0, B0) => Some "4"%char + | (B0, B1, B0, B1) => Some "5"%char + | (B0, B1, B1, B0) => Some "6"%char + | (B0, B1, B1, B1) => Some "7"%char + | (B1, B0, B0, B0) => Some "8"%char + | (B1, B0, B0, B1) => Some "9"%char + | (B1, B0, B1, B0) => Some "A"%char + | (B1, B0, B1, B1) => Some "B"%char + | (B1, B1, B0, B0) => Some "C"%char + | (B1, B1, B0, B1) => Some "D"%char + | (B1, B1, B1, B0) => Some "E"%char + | (B1, B1, B1, B1) => Some "F"%char | _ => None - end + end. Fixpoint hexstring_of_bits bs := match bs with | b1 :: b2 :: b3 :: b4 :: bs => let n := char_of_nibble (b1, b2, b3, b4) in let s := hexstring_of_bits bs in match (n, s) with - | (Some n, Some s) => Some (n :: s) + | (Some n, Some s) => Some (String n s) | _ => None end + | [] => Some EmptyString | _ => None - end -declare {isabelle} termination_argument hexstring_of_bits = automatic + end%string. + +Fixpoint binstring_of_bits bs := match bs with + | b :: bs => String (bitU_char b) (binstring_of_bits bs) + | [] => EmptyString + end. Definition show_bitlist bs := match hexstring_of_bits bs with - | Some s => toString (#'0' :: #x' :: s) - | None => show bs - end + | Some s => String "0" (String "x" s) + | None => String "0" (String "b" (binstring_of_bits bs)) + end. (*** List operations *) - +(* Definition inline (^^) := append_list val subrange_list_inc : forall a. list a -> Z -> Z -> list a*) @@ -628,10 +717,10 @@ Definition update_list {A} (is_inc : bool) (xs : list A) n x := | [] => failwith "extract_only_element called for empty list" | [e] => e | _ => failwith "extract_only_element called for list with more elements" -end +end*) (*** Machine words *) -*) + Definition mword (n : Z) := match n with | Zneg _ => False @@ -832,8 +921,20 @@ Class ReasonableSize (a : Z) : Prop := { isPositive : a >= 0 }. -Hint Resolve -> Z.gtb_lt Z.geb_le Z.ltb_lt Z.leb_le : zbool. -Hint Resolve <- Z.ge_le_iff Z.gt_lt_iff : zbool. +(* 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 +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. *) +Ltac not_Z ty := match ty with Z => fail 1 | _ => idtac end. +Ltac clear_non_Z_defns := + repeat match goal with H := _ : ?X |- _ => not_Z X; clearbody H end. Lemma ArithFact_mword (a : Z) (w : mword a) : ArithFact (a >= 0). constructor. @@ -843,7 +944,7 @@ auto using Z.le_ge, Zle_0_pos. destruct w. Qed. Ltac unwrap_ArithFacts := - repeat match goal with H:(ArithFact _) |- _ => apply use_ArithFact in H end. + repeat match goal with H:(ArithFact _) |- _ => let H' := fresh H in case H as [H'] end. Ltac unbool_comparisons := repeat match goal with | H:context [Z.geb _ _] |- _ => rewrite Z.geb_leb in H @@ -855,16 +956,29 @@ Ltac unbool_comparisons := | H:context [Z.ltb _ _ = false] |- _ => rewrite Z.ltb_ge in H | H:context [Z.eqb _ _ = false] |- _ => rewrite Z.eqb_neq in H | H:context [orb _ _ = true] |- _ => rewrite Bool.orb_true_iff in H + | H:context [orb _ _ = false] |- _ => rewrite Bool.orb_false_iff in H + | H:context [andb _ _ = true] |- _ => rewrite Bool.andb_true_iff in H + | 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 [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 end. + (* Split up dependent pairs to get at proofs of properties *) -(* TODO: simpl is probably too strong here *) Ltac extract_properties := - repeat match goal with H := (projT1 ?X) |- _ => destruct X in *; simpl in H; unfold H in * end; - repeat match goal with |- context [projT1 ?X] => destruct X in *; simpl end. + repeat match goal with H := (projT1 ?X) |- _ => + let x := fresh "x" in + let Hx := fresh "Hx" in + destruct X as [x Hx] in *; + change (projT1 (existT _ x Hx)) with x in *; unfold H in * end; + repeat match goal with |- context [projT1 ?X] => + let x := fresh "x" in + let Hx := fresh "Hx" in + destruct X as [x Hx] in *; + change (projT1 (existT _ x Hx)) with x in * end. (* TODO: hyps, too? *) Ltac reduce_list_lengths := repeat match goal with |- context [length_list ?X] => @@ -881,22 +995,37 @@ Ltac reduce_pow := let r := (eval cbn in (Z.pow X Y)) in change (Z.pow X Y) with r end. -Ltac solve_arithfact := +Ltac dump_context := + repeat match goal with + | H:=?X |- _ => idtac H ":=" X; fail + | H:?X |- _ => idtac H ":" X; fail end; + match goal with |- ?X => idtac "Goal:" X end. +Ltac prepare_for_solver := +(*dump_context;*) + clear_non_Z_defns; extract_properties; repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end; unwrap_ArithFacts; + unfold_In; autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *) unbool_comparisons; reduce_list_lengths; - reduce_pow; + reduce_pow. +Ltac solve_arithfact := +prepare_for_solver; +(*dump_context;*) solve [apply ArithFact_mword; assumption | constructor; omega with Z (* The datatypes hints give us some list handling, esp In *) - | constructor; auto with datatypes zbool zarith sail]. + | constructor; eauto with datatypes zarith sail + | constructor; idtac "Unable to solve constraint"; dump_context; fail]. Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances. Hint Unfold length_mword : sail. +Definition neq_atom (x : Z) (y : Z) : bool := negb (Z.eqb x y). +Hint Unfold neq_atom : sail. + Lemma ReasonableSize_witness (a : Z) (w : mword a) : ReasonableSize a. constructor. destruct a. @@ -946,9 +1075,9 @@ Definition extz_bv n (v : a) : option b := of_bits (extz_bits n (bits_of v)). (*val exts_bv : forall a b. Bitvector a, Bitvector b => Z -> a -> b*) Definition exts_bv n (v : a) : option b := of_bits (exts_bits n (bits_of v)). -(*val string_of_bv : forall a. Bitvector a => a -> string -Definition string_of_bv v := show_bitlist (bits_of v) -*) +(*val string_of_bv : forall a. Bitvector a => a -> string *) +Definition string_of_bv v := show_bitlist (bits_of v). + End Bitvector_defs. (*** Bytes and addresses *) @@ -1216,17 +1345,51 @@ end. (*declare {isabelle} termination_argument foreach = automatic val index_list : Z -> Z -> Z -> list Z*) -Fixpoint index_list' from step n := - match n with - | O => [] - | S n => from :: index_list' (from + step) step n - end. +Fixpoint index_list' from to step n := + if orb (andb (step >? 0) (from <=? to)) (andb (step <? 0) (to <=? from)) then + match n with + | O => [] + | S n => from :: index_list' (from + step) to step n + end + else []. Definition index_list from to step := if orb (andb (step >? 0) (from <=? to)) (andb (step <? 0) (to <=? from)) then - index_list' from step (S (Z.abs_nat (from - to))) + index_list' from to step (S (Z.abs_nat (from - to))) else []. +Fixpoint foreach_Z' {Vars} from to step n (vars : Vars) (body : Z -> Vars -> Vars) : Vars := + if orb (andb (step >? 0) (from <=? to)) (andb (step <? 0) (to <=? from)) then + match n with + | O => vars + | S n => let vars := body from vars in foreach_Z' (from + step) to step n vars body + end + else vars. + +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 := + if sumbool_of_bool (from + off <=? to) then + match n with + | O => vars + | S n => let vars := body (from + off) _ vars in foreach_Z_up' from to step (off + step) n vars body + 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 := + if sumbool_of_bool (to <=? from + off) then + match n with + | O => vars + | S n => let vars := body (from + off) _ vars in foreach_Z_down' from to step (off - step) n vars body + end + else vars. + +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)} := + 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 Fixpoint while vars cond body := if cond vars then while (body vars) cond body else vars @@ -1323,6 +1486,8 @@ Definition abs_with_eq n : {o : Z & ArithFact (o = Z.abs n)} := build_ex (Z.ab (* 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 := + (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)} := build_ex ((projT1 l) + (projT1 r)). @@ -1338,3 +1503,108 @@ Definition min_atom (a : Z) (b : Z) : {c : Z & ArithFact (c = a \/ c = b /\ c <= Definition max_atom (a : Z) (b : Z) : {c : Z & ArithFact (c = a \/ c = b /\ c >= a /\ c >= b)} := build_ex (Z.max a b). + +(*** Generic vectors *) + +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 := + access_list_dec (projT1 v) m. +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 := + existT _ (repeat [t] n) _. +Next Obligation. +rewrite repeat_length; auto using fact. +unfold length_list. +simpl. +auto with zarith. +Qed. + +Lemma skipn_length {A n} {l: list A} : (n <= List.length l -> List.length (skipn n l) = List.length l - n)%nat. +revert l. +induction n. +* simpl. auto with arith. +* intros l H. + destruct l. + + inversion H. + + simpl in H. + simpl. + rewrite IHn; auto with arith. +Qed. +Lemma update_list_inc_length {T} {l:list T} {m x} : 0 <= m < length_list l -> length_list (update_list_inc l m x) = length_list l. +unfold update_list_inc, list_update, length_list. +intro H. +f_equal. +assert ((0 <= Z.to_nat m < Datatypes.length l)%nat). +{ destruct H as [H1 H2]. + split. + + change 0%nat with (Z.to_nat 0). + apply Z2Nat.inj_le; auto with zarith. + + rewrite <- Nat2Z.id. + apply Z2Nat.inj_lt; auto with zarith. +} +rewrite app_length. +rewrite firstn_length_le; only 2:omega. +cbn -[skipn]. +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) _. +Next Obligation. +unfold update_list_dec. +rewrite update_list_inc_length. ++ destruct v. apply e. ++ destruct H. + 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) _. +Next Obligation. +rewrite update_list_inc_length. ++ destruct v. apply e. ++ destruct H. + destruct v. simpl (projT1 _). rewrite e. + omega. +Qed. + +Program Definition vec_map {S T} (f : S -> T) {n} (v : vec S n) : vec T n := existT _ (List.map f (projT1 v)) _. +Next Obligation. +destruct v as [l H]. +cbn. +unfold length_list. +rewrite map_length. +apply H. +Qed. + +Program Definition just_vec {A n} (v : vec (option A) n) : option (vec A n) := + match just_list (projT1 v) with + | None => None + | Some v' => Some (existT _ v' _) + end. +Next Obligation. +rewrite <- (just_list_length_Z _ _ Heq_anonymous). +destruct v. +assumption. +Qed. + +Definition list_of_vec {A n} (v : vec A n) : list A := projT1 v. + +Program Definition vec_of_list {A} n (l : list A) : option (vec A n) := + if sumbool_of_bool (n =? length_list l) then Some (existT _ l _) else None. +Next Obligation. +symmetry. +apply Z.eqb_eq. +assumption. +Qed. + +Definition vec_of_list_len {A} (l : list A) : vec A (length_list l) := existT _ l (eq_refl _). + +Definition map_bind {A B} (f : A -> option B) (a : option A) : option B := +match a with +| Some a' => f a' +| None => None +end.
\ No newline at end of file diff --git a/lib/coq/_CoqProject b/lib/coq/_CoqProject new file mode 100644 index 00000000..9f5d26b8 --- /dev/null +++ b/lib/coq/_CoqProject @@ -0,0 +1,2 @@ +-R . Sail +-R ../../../bbv/theories bbv diff --git a/lib/flow.sail b/lib/flow.sail index c4ffd75a..b4440eaa 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -9,7 +9,7 @@ val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool -val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val neq_atom = {lem: "neq", coq: "neq_atom"} : forall 'n 'm. (atom('n), atom('m)) -> bool function neq_atom (x, y) = not_bool(eq_atom(x, y)) @@ -27,7 +27,7 @@ val lteq_atom_range = {coq: "leb_range_r", _: "lteq"} : forall 'n 'm 'o. (atom(' val gt_atom_range = {coq: "gtb_range_r", _: "gt"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool val gteq_atom_range = {coq: "geb_range_r", _: "gteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool -val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool +val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "eq_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : (int, int) -> bool val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool diff --git a/lib/hol/Holmakefile b/lib/hol/Holmakefile index eac4fec8..8e8403f3 100644 --- a/lib/hol/Holmakefile +++ b/lib/hol/Holmakefile @@ -1,11 +1,12 @@ -LEM_SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript.sml \ - sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \ - state_monadScript.sml stateScript.sml promptScript.sml prompt_monadScript.sml +LEM_SCRIPTS = sail2_instr_kindsScript.sml sail2_valuesScript.sml sail2_operatorsScript.sml \ + sail2_operators_mwordsScript.sml sail2_operators_bitlistsScript.sml \ + sail2_state_monadScript.sml sail2_stateScript.sml sail2_promptScript.sml sail2_prompt_monadScript.sml \ + sail2_stringScript.sml LEM_CLEANS = $(LEM_SCRIPTS) SCRIPTS = $(LEM_SCRIPTS) \ - sail_valuesAuxiliaryScript.sml stateAuxiliaryScript.sml + sail2_valuesAuxiliaryScript.sml sail2_stateAuxiliaryScript.sml THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS)) diff --git a/lib/hol/Makefile b/lib/hol/Makefile index 065f887a..783ef23d 100644 --- a/lib/hol/Makefile +++ b/lib/hol/Makefile @@ -1,22 +1,25 @@ LEMSRC = \ - ../../src/lem_interp/sail_instr_kinds.lem \ - ../../src/gen_lib/sail_values.lem \ - ../../src/gen_lib/sail_operators.lem \ - ../../src/gen_lib/sail_operators_mwords.lem \ - ../../src/gen_lib/sail_operators_bitlists.lem \ - ../../src/gen_lib/state_monad.lem \ - ../../src/gen_lib/state.lem \ - prompt_monad.lem \ - prompt.lem + ../../src/lem_interp/sail2_instr_kinds.lem \ + ../../src/gen_lib/sail2_values.lem \ + ../../src/gen_lib/sail2_operators.lem \ + ../../src/gen_lib/sail2_operators_mwords.lem \ + ../../src/gen_lib/sail2_operators_bitlists.lem \ + ../../src/gen_lib/sail2_state_monad.lem \ + ../../src/gen_lib/sail2_state.lem \ + ../../src/gen_lib/sail2_string.lem \ + sail2_prompt_monad.lem \ + sail2_prompt.lem -SCRIPTS = sail_instr_kindsScript.sml sail_valuesScript.sml sail_operatorsScript.sml \ - sail_operators_mwordsScript.sml sail_operators_bitlistsScript.sml \ - state_monadScript.sml stateScript.sml \ - prompt_monadScript.sml promptScript.sml +SCRIPTS = sail2_instr_kindsScript.sml sail2_valuesScript.sml sail2_operatorsScript.sml \ + sail2_operators_mwordsScript.sml sail2_operators_bitlistsScript.sml \ + sail2_state_monadScript.sml sail2_stateScript.sml \ + sail2_prompt_monadScript.sml sail2_promptScript.sml \ + sail2_stringScript.sml THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS)) all: sail-heap $(THYS) +all-scripts: $(SCRIPTS) $(SCRIPTS): $(LEMSRC) lem -hol -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $(LEMSRC) @@ -28,4 +31,4 @@ $(THYS) sail-heap: $(SCRIPTS) clean: Holmake cleanAll -.PHONY: all clean +.PHONY: all all-scripts clean diff --git a/lib/hol/prompt.lem b/lib/hol/prompt.lem deleted file mode 100644 index edbd3752..00000000 --- a/lib/hol/prompt.lem +++ /dev/null @@ -1,18 +0,0 @@ -open import Prompt_monad -open import State_monad -open import State - -let inline undefined_bool = undefined_boolS -let inline bool_of_bitU_oracle = bool_of_bitU_oracleS -let inline bool_of_bitU_fail = bool_of_bitU_fail -let inline bools_of_bits_oracle = bools_of_bits_oracleS -let inline of_bits_oracle = of_bits_oracleS -let inline of_bits_fail = of_bits_failS -let inline mword_oracle = mword_oracleS -let inline reg_deref = read_regS - -let inline foreachM = foreachS -let inline whileM = whileS -let inline untilM = untilS -let inline and_boolM = and_boolS -let inline or_boolM = or_boolS diff --git a/lib/hol/sail2_prompt.lem b/lib/hol/sail2_prompt.lem new file mode 100644 index 00000000..674d4e34 --- /dev/null +++ b/lib/hol/sail2_prompt.lem @@ -0,0 +1,19 @@ +open import Sail2_prompt_monad +open import Sail2_state_monad +open import Sail2_state + +let inline undefined_bool = undefined_boolS +let inline bool_of_bitU_nondet = bool_of_bitU_nondetS +let inline bool_of_bitU_fail = bool_of_bitU_fail +let inline bools_of_bits_nondet = bools_of_bits_nondetS +let inline of_bits_nondet = of_bits_nondetS +let inline of_bits_fail = of_bits_failS +let inline mword_nondet = mword_nondetS +let inline reg_deref = read_regS +let inline internal_pick = internal_pickS + +let inline foreachM = foreachS +let inline whileM = whileS +let inline untilM = untilS +let inline and_boolM = and_boolS +let inline or_boolM = or_boolS diff --git a/lib/hol/prompt_monad.lem b/lib/hol/sail2_prompt_monad.lem index 8fcd645a..3af931a5 100644 --- a/lib/hol/prompt_monad.lem +++ b/lib/hol/sail2_prompt_monad.lem @@ -1,7 +1,7 @@ open import Pervasives_extra -open import Sail_instr_kinds -open import Sail_values -open import State_monad +open import Sail2_instr_kinds +open import Sail2_values +open import Sail2_state_monad (* Fake interface of the prompt monad by redirecting to the state monad, since the former is not currently supported by HOL4 *) diff --git a/lib/hol/stateAuxiliaryScript.sml b/lib/hol/sail2_stateAuxiliaryScript.sml index c8269750..4d70b033 100644 --- a/lib/hol/stateAuxiliaryScript.sml +++ b/lib/hol/sail2_stateAuxiliaryScript.sml @@ -1,6 +1,6 @@ (*Generated by Lem from ../../src/gen_lib/state.lem.*) open HolKernel Parse boolLib bossLib; -open lem_pervasives_extraTheory sail_valuesTheory state_monadTheory stateTheory; +open lem_pervasives_extraTheory sail2_valuesTheory sail2_state_monadTheory sail2_stateTheory; val _ = numLib.prefer_num(); @@ -8,7 +8,7 @@ val _ = numLib.prefer_num(); open lemLib; (* val _ = lemLib.run_interactive := true; *) -val _ = new_theory "stateAuxiliary" +val _ = new_theory "sail2_stateAuxiliary" (****************************************************) diff --git a/lib/hol/sail_valuesAuxiliaryScript.sml b/lib/hol/sail2_valuesAuxiliaryScript.sml index aa169979..b475c5ea 100644 --- a/lib/hol/sail_valuesAuxiliaryScript.sml +++ b/lib/hol/sail2_valuesAuxiliaryScript.sml @@ -1,6 +1,6 @@ (*Generated by Lem from ../../src/gen_lib/sail_values.lem.*) open HolKernel Parse boolLib bossLib; -open lem_pervasives_extraTheory lem_machine_wordTheory sail_valuesTheory; +open lem_pervasives_extraTheory lem_machine_wordTheory sail2_valuesTheory; open intLib; val _ = numLib.prefer_num(); @@ -9,7 +9,7 @@ val _ = numLib.prefer_num(); open lemLib; (* val _ = lemLib.run_interactive := true; *) -val _ = new_theory "sail_valuesAuxiliary" +val _ = new_theory "sail2_valuesAuxiliary" (****************************************************) diff --git a/lib/isabelle/.gitignore b/lib/isabelle/.gitignore index 0d595f3c..ed83cdc1 100644 --- a/lib/isabelle/.gitignore +++ b/lib/isabelle/.gitignore @@ -1,13 +1,13 @@ -PromptAuxiliary.thy -Prompt_monadAuxiliary.thy -Prompt_monad.thy -Prompt.thy -Sail_instr_kinds.thy -Sail_operators_bitlists.thy -Sail_operators_mwords.thy -Sail_operators.thy -Sail_valuesAuxiliary.thy -Sail_values.thy -StateAuxiliary.thy -State_monad.thy -State.thy +Sail2_promptAuxiliary.thy +Sail2_prompt_monadAuxiliary.thy +Sail2_prompt_monad.thy +Sail2_prompt.thy +Sail2_instr_kinds.thy +Sail2_operators_bitlists.thy +Sail2_operators_mwords.thy +Sail2_operators.thy +Sail2_valuesAuxiliary.thy +Sail2_values.thy +Sail2_stateAuxiliary.thy +Sail2_state_monad.thy +Sail2_state.thy diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy index 5c77c5e7..76750117 100644 --- a/lib/isabelle/Hoare.thy +++ b/lib/isabelle/Hoare.thy @@ -13,7 +13,7 @@ subsection \<open>Hoare triples\<close> type_synonym 'regs predS = "'regs sequential_state \<Rightarrow> bool" -definition PrePost :: "'regs predS \<Rightarrow> ('regs, 'a, 'e) monadS \<Rightarrow> (('a, 'e) result \<Rightarrow> 'regs predS) \<Rightarrow> bool" +definition PrePost :: "'regs predS \<Rightarrow> ('regs, 'a, 'e) monadS \<Rightarrow> (('a, 'e) result \<Rightarrow> 'regs predS) \<Rightarrow> bool" ("\<lbrace>_\<rbrace> _ \<lbrace>_\<rbrace>") where "PrePost P f Q \<equiv> (\<forall>s. P s \<longrightarrow> (\<forall>(r, s') \<in> f s. Q r s'))" lemma PrePostI: @@ -211,7 +211,7 @@ there is an exception. [1] D. Cock, G. Klein, and T. Sewell, ‘Secure Microkernels, State Monads and Scalable Refinement’, in Theorem Proving in Higher Order Logics, 2008, pp. 167–182.\<close> -definition PrePostE :: "'regs predS \<Rightarrow> ('regs, 'a, 'e) monadS \<Rightarrow> ('a \<Rightarrow> 'regs predS) \<Rightarrow> ('e ex \<Rightarrow> 'regs predS) \<Rightarrow> bool" +definition PrePostE :: "'regs predS \<Rightarrow> ('regs, 'a, 'e) monadS \<Rightarrow> ('a \<Rightarrow> 'regs predS) \<Rightarrow> ('e ex \<Rightarrow> 'regs predS) \<Rightarrow> bool" ("\<lbrace>_\<rbrace> _ \<lbrace>_ \<bar> _\<rbrace>") where "PrePostE P f Q E \<equiv> PrePost P f (\<lambda>v. case v of Value a \<Rightarrow> Q a | Ex e \<Rightarrow> E e)" lemmas PrePost_defs = PrePost_def PrePostE_def @@ -253,6 +253,27 @@ lemma PrePostE_weaken_post: named_theorems PrePostE_compositeI named_theorems PrePostE_atomI +lemma PrePostE_conj_conds: + assumes "PrePostE P1 m Q1 E1" + and "PrePostE P2 m Q2 E2" + shows "PrePostE (\<lambda>s. P1 s \<and> P2 s) m (\<lambda>r s. Q1 r s \<and> Q2 r s) (\<lambda>e s. E1 e s \<and> E2 e s)" + using assms by (auto intro: PrePostE_I elim: PrePostE_elim) + +lemmas PrePostE_conj_conds_consequence = PrePostE_conj_conds[THEN PrePostE_consequence] + +lemma PrePostE_post_mp: + assumes "PrePostE P m Q' E" + and "PrePostE P m (\<lambda>r s. Q' r s \<longrightarrow> Q r s) E" + shows "PrePostE P m Q E" + using PrePostE_conj_conds[OF assms] by (auto intro: PrePostE_weaken_post) + +lemma PrePostE_cong: + assumes "\<And>s. P1 s \<longleftrightarrow> P2 s" and "\<And>s. P1 s \<Longrightarrow> m1 s = m2 s" and "\<And>r s. Q1 r s \<longleftrightarrow> Q2 r s" + and "\<And>e s. E1 e s \<longleftrightarrow> E2 e s" + shows "PrePostE P1 m1 Q1 E1 \<longleftrightarrow> PrePostE P2 m2 Q2 E2" + using assms unfolding PrePostE_def PrePost_def + by (auto split: result.splits) + lemma PrePostE_True_post[PrePostE_atomI, intro, simp]: "PrePostE P m (\<lambda>_ _. True) (\<lambda>_ _. True)" unfolding PrePost_defs by (auto split: result.splits) @@ -320,6 +341,11 @@ lemma PrePostE_option_cases[PrePostE_compositeI]: shows "PrePostE (case x of Some a \<Rightarrow> PS a | None \<Rightarrow> PN) (case x of Some a \<Rightarrow> s a | None \<Rightarrow> n) Q E" using assms by (auto split: option.splits) +lemma PrePostE_sum_cases[PrePostE_compositeI]: + assumes "\<And>a. PrePostE (Pl a) (l a) Q E" and "\<And>b. PrePostE (Pr b) (r b) Q E" + shows "PrePostE (case x of Inl a \<Rightarrow> Pl a | Inr b \<Rightarrow> Pr b) (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b) Q E" + using assms by (auto split: sum.splits) + lemma PrePostE_let[PrePostE_compositeI]: assumes "PrePostE P (m y) Q E" shows "PrePostE P (let x = y in m x) Q E" @@ -347,10 +373,51 @@ lemma PrePostE_failS[PrePostE_atomI, intro]: "PrePostE (E (Failure msg)) (failS msg) Q E" unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre) +lemma PrePostE_maybe_failS[PrePostE_atomI]: + "PrePostE (\<lambda>s. case v of Some v \<Rightarrow> Q v s | None \<Rightarrow> E (Failure msg) s) (maybe_failS msg v) Q E" + by (auto simp: maybe_failS_def split: option.splits) + +lemma PrePostE_exitS[PrePostE_atomI, intro]: "PrePostE (E (Failure ''exit'')) (exitS msg) Q E" + unfolding exitS_def PrePostE_def PrePost_def failS_def by auto + lemma PrePostE_chooseS[intro, PrePostE_atomI]: "PrePostE (\<lambda>s. \<forall>x \<in> xs. Q x s) (chooseS xs) Q E" unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre) +lemma PrePostE_throwS[PrePostE_atomI]: "PrePostE (E (Throw e)) (throwS e) Q E" + by (intro PrePostE_I) (auto simp: throwS_def) + +lemma PrePostE_try_catchS[PrePostE_compositeI]: + assumes Ph: "\<And>s e s'. (Ex (Throw e), s') \<in> m s \<Longrightarrow> PrePostE (Ph e) (h e) Q E" + and m: "PrePostE P m Q (\<lambda>ex. case ex of Throw e \<Rightarrow> Ph e | Failure msg \<Rightarrow> E (Failure msg))" + shows "PrePostE P (try_catchS m h) Q E" + unfolding PrePostE_def +proof (intro PrePostI) + fix s r s' + assume "(r, s') \<in> try_catchS m h s" and P: "P s" + then show "(case r of Value a \<Rightarrow> Q a | result.Ex e \<Rightarrow> E e) s'" using m + proof (cases rule: try_catchS_cases) + case (h e s'') + then have "Ph e s''" using P m by (auto elim!: PrePostE_elim) + then show ?thesis using Ph[OF h(1)] h(2) by (auto elim!: PrePostE_elim) + qed (auto elim!: PrePostE_elim) +qed + +lemma PrePostE_catch_early_returnS[PrePostE_compositeI]: + assumes "PrePostE P m Q (\<lambda>ex. case ex of Throw (Inl a) \<Rightarrow> Q a | Throw (Inr e) \<Rightarrow> E (Throw e) | Failure msg \<Rightarrow> E (Failure msg))" + shows "PrePostE P (catch_early_returnS m) Q E" + unfolding catch_early_returnS_def + by (rule PrePostE_try_catchS, rule PrePostE_sum_cases[OF PrePostE_returnS PrePostE_throwS]) + (auto intro: assms) + +lemma PrePostE_early_returnS[PrePostE_atomI]: "PrePostE (E (Throw (Inl r))) (early_returnS r) Q E" + by (auto simp: early_returnS_def intro: PrePostE_throwS) + +lemma PrePostE_liftRS[PrePostE_compositeI]: + assumes "PrePostE P m Q (\<lambda>ex. case ex of Throw e \<Rightarrow> E (Throw (Inr e)) | Failure msg \<Rightarrow> E (Failure msg))" + shows "PrePostE P (liftRS m) Q E" + using assms unfolding liftRS_def by (intro PrePostE_try_catchS[OF PrePostE_throwS]) + lemma PrePostE_foreachS_Cons: assumes "\<And>s vars' s'. (Value vars', s') \<in> body x vars s \<Longrightarrow> PrePostE (Q vars') (foreachS xs vars' body) Q E" and "PrePostE (Q vars) (body x vars) Q E" @@ -363,4 +430,88 @@ lemma PrePostE_foreachS_invariant: using assms unfolding PrePostE_def by (intro PrePost_foreachS_invariant[THEN PrePost_strengthen_pre]) auto +lemma PrePostE_untilS: + assumes dom: "\<And>s. Inv Q vars s \<Longrightarrow> untilS_dom (vars, cond, body, s)" + and cond: "\<And>vars. PrePostE (Inv' Q vars) (cond vars) (\<lambda>c s'. Inv Q vars s' \<and> (c \<longrightarrow> Q vars s')) E" + and body: "\<And>vars. PrePostE (Inv Q vars) (body vars) (Inv' Q) E" + shows "PrePostE (Inv Q vars) (untilS vars cond body) Q E" +proof (unfold PrePostE_def, rule PrePostI) + fix s r s' + assume Inv_s: "Inv Q vars s" and r: "(r, s') \<in> untilS vars cond body s" + with dom[OF Inv_s] cond body + show "(case r of Value a \<Rightarrow> Q a | result.Ex e \<Rightarrow> E e) s'" + proof (induction vars cond body s rule: untilS.pinduct[case_names Step]) + case (Step vars cond body s) + consider + (Value) vars' c sb sc where "(Value vars', sb) \<in> body vars s" and "(Value c, sc) \<in> cond vars' sb" + and "if c then r = Value vars' \<and> s' = sc else (r, s') \<in> untilS vars' cond body sc" + | (Ex) e where "(Ex e, s') \<in> bindS (body vars) cond s" and "r = Ex e" + using Step(1,6) + by (auto simp: untilS.psimps returnS_def Ex_bindS_iff elim!: bindS_cases split: if_splits; fastforce) + then show ?case + proof cases + case Value + then show ?thesis using Step.IH[OF Value(1,2) _ Step(3,4)] Step(3,4,5) + by (auto split: if_splits elim: PrePostE_elim) + next + case Ex + then show ?thesis using Step(3,4,5) by (auto elim!: bindS_cases PrePostE_elim) + qed + qed +qed + +lemma PrePostE_untilS_pure_cond: + assumes dom: "\<And>s. Inv Q vars s \<Longrightarrow> untilS_dom (vars, returnS \<circ> cond, body, s)" + and body: "\<And>vars. PrePostE (Inv Q vars) (body vars) (\<lambda>vars' s'. Inv Q vars' s' \<and> (cond vars' \<longrightarrow> Q vars' s')) E" + shows "PrePostE (Inv Q vars) (untilS vars (returnS \<circ> cond) body) Q E" + using assms by (intro PrePostE_untilS) (auto simp: comp_def) + +lemma PrePostE_liftState_untilM: + assumes dom: "\<And>s. Inv Q vars s \<Longrightarrow> untilM_dom (vars, cond, body)" + and cond: "\<And>vars. PrePostE (Inv' Q vars) (liftState r (cond vars)) (\<lambda>c s'. Inv Q vars s' \<and> (c \<longrightarrow> Q vars s')) E" + and body: "\<And>vars. PrePostE (Inv Q vars) (liftState r (body vars)) (Inv' Q) E" + shows "PrePostE (Inv Q vars) (liftState r (untilM vars cond body)) Q E" +proof - + have domS: "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" if "Inv Q vars s" for s + using dom that by (intro untilM_dom_untilS_dom) + then have "PrePostE (Inv Q vars) (untilS vars (liftState r \<circ> cond) (liftState r \<circ> body)) Q E" + using cond body by (auto intro: PrePostE_untilS simp: comp_def) + moreover have "liftState r (untilM vars cond body) s = untilS vars (liftState r \<circ> cond) (liftState r \<circ> body) s" + if "Inv Q vars s" for s + unfolding liftState_untilM[OF domS[OF that] dom[OF that]] .. + ultimately show ?thesis by (auto cong: PrePostE_cong) +qed + +lemma PrePostE_liftState_untilM_pure_cond: + assumes dom: "\<And>s. Inv Q vars s \<Longrightarrow> untilM_dom (vars, return \<circ> cond, body)" + and body: "\<And>vars. PrePostE (Inv Q vars) (liftState r (body vars)) (\<lambda>vars' s'. Inv Q vars' s' \<and> (cond vars' \<longrightarrow> Q vars' s')) E" + shows "PrePostE (Inv Q vars) (liftState r (untilM vars (return \<circ> cond) body)) Q E" + using assms by (intro PrePostE_liftState_untilM) (auto simp: comp_def liftState_simp) + +lemma PrePostE_undefined_boolS[PrePostE_atomI]: + "PrePostE (\<lambda>s. \<forall>b. Q b s) + (undefined_boolS unit) Q E" + unfolding undefined_boolS_def seqS_def + by (auto intro: PrePostE_strengthen_pre PrePostE_chooseS) + +lemma PrePostE_bool_of_bitU_nondetS_any: + "PrePostE (\<lambda>s. \<forall>b. Q b s) (bool_of_bitU_nondetS b) Q E" + unfolding bool_of_bitU_nondetS_def undefined_boolS_def + by (cases b; simp; rule PrePostE_strengthen_pre, rule PrePostE_atomI) auto + +lemma PrePostE_bools_of_bits_nondetS_any: + "PrePostE (\<lambda>s. \<forall>bs. Q bs s) (bools_of_bits_nondetS bs) Q E" + unfolding bools_of_bits_nondetS_def + by (rule PrePostE_weaken_post[where B = "\<lambda>_ s. \<forall>bs. Q bs s"], rule PrePostE_strengthen_pre, + (rule PrePostE_foreachS_invariant[OF PrePostE_strengthen_pre] PrePostE_bindS PrePostE_returnS + PrePostE_bool_of_bitU_nondetS_any)+) + auto + +lemma PrePostE_internal_pick: + "xs \<noteq> [] \<Longrightarrow> PrePostE (\<lambda>s. \<forall>x \<in> set xs. Q x s) (internal_pickS xs) Q E" + unfolding internal_pickS_def Let_def + by (rule PrePostE_strengthen_pre, + (rule PrePostE_compositeI PrePostE_atomI PrePostE_bools_of_bits_nondetS_any)+) + (auto split: option.splits) + end diff --git a/lib/isabelle/Sail2_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy index ae8802f2..fd54c93a 100644 --- a/lib/isabelle/Sail2_operators_mwords_lemmas.thy +++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy @@ -2,14 +2,14 @@ theory Sail2_operators_mwords_lemmas imports Sail2_operators_mwords begin -lemmas uint_simps[simp] = uint_maybe_def uint_fail_def uint_oracle_def -lemmas sint_simps[simp] = sint_maybe_def sint_fail_def sint_oracle_def +lemmas uint_simps[simp] = uint_maybe_def uint_fail_def uint_nondet_def +lemmas sint_simps[simp] = sint_maybe_def sint_fail_def sint_nondet_def -lemma bools_of_bits_oracle_just_list[simp]: +lemma bools_of_bits_nondet_just_list[simp]: assumes "just_list (map bool_of_bitU bus) = Some bs" - shows "bools_of_bits_oracle bus = return bs" + shows "bools_of_bits_nondet bus = return bs" proof - - have f: "foreachM bus bools (\<lambda>b bools. bool_of_bitU_oracle b \<bind> (\<lambda>b. return (bools @ [b]))) = return (bools @ bs)" + have f: "foreachM bus bools (\<lambda>b bools. bool_of_bitU_nondet b \<bind> (\<lambda>b. return (bools @ [b]))) = return (bools @ bs)" if "just_list (map bool_of_bitU bus) = Some bs" for bus bs bools proof (use that in \<open>induction bus arbitrary: bs bools\<close>) case (Cons bu bus bs) @@ -17,26 +17,26 @@ proof - using Cons.prems by (cases bu) (auto split: option.splits) then show ?case using Cons.prems Cons.IH[where bs = bs' and bools = "bools @ [b]"] - by (cases bu) (auto simp: bool_of_bitU_oracle_def split: option.splits) + by (cases bu) (auto simp: bool_of_bitU_nondet_def split: option.splits) qed auto - then show ?thesis using f[OF assms, of "[]"] unfolding bools_of_bits_oracle_def + then show ?thesis using f[OF assms, of "[]"] unfolding bools_of_bits_nondet_def by auto qed lemma of_bits_mword_return_of_bl[simp]: assumes "just_list (map bool_of_bitU bus) = Some bs" - shows "of_bits_oracle BC_mword bus = return (of_bl bs)" + shows "of_bits_nondet BC_mword bus = return (of_bl bs)" and "of_bits_fail BC_mword bus = return (of_bl bs)" - by (auto simp: of_bits_oracle_def of_bits_fail_def maybe_fail_def assms BC_mword_defs) + by (auto simp: of_bits_nondet_def of_bits_fail_def maybe_fail_def assms BC_mword_defs) lemma vec_of_bits_of_bl[simp]: assumes "just_list (map bool_of_bitU bus) = Some bs" shows "vec_of_bits_maybe bus = Some (of_bl bs)" and "vec_of_bits_fail bus = return (of_bl bs)" - and "vec_of_bits_oracle bus = return (of_bl bs)" + and "vec_of_bits_nondet bus = return (of_bl bs)" and "vec_of_bits_failwith bus = of_bl bs" and "vec_of_bits bus = of_bl bs" - unfolding vec_of_bits_maybe_def vec_of_bits_fail_def vec_of_bits_oracle_def + unfolding vec_of_bits_maybe_def vec_of_bits_fail_def vec_of_bits_nondet_def vec_of_bits_failwith_def vec_of_bits_def by (auto simp: assms) @@ -53,10 +53,10 @@ lemma bool_of_bitU_monadic_simps[simp]: "bool_of_bitU_fail B0 = return False" "bool_of_bitU_fail B1 = return True" "bool_of_bitU_fail BU = Fail ''bool_of_bitU''" - "bool_of_bitU_oracle B0 = return False" - "bool_of_bitU_oracle B1 = return True" - "bool_of_bitU_oracle BU = undefined_bool ()" - unfolding bool_of_bitU_fail_def bool_of_bitU_oracle_def + "bool_of_bitU_nondet B0 = return False" + "bool_of_bitU_nondet B1 = return True" + "bool_of_bitU_nondet BU = undefined_bool ()" + unfolding bool_of_bitU_fail_def bool_of_bitU_nondet_def by auto lemma update_vec_dec_simps[simp]: @@ -66,18 +66,69 @@ lemma update_vec_dec_simps[simp]: "update_vec_dec_fail w i B0 = return (set_bit w (nat i) False)" "update_vec_dec_fail w i B1 = return (set_bit w (nat i) True)" "update_vec_dec_fail w i BU = Fail ''bool_of_bitU''" - "update_vec_dec_oracle w i B0 = return (set_bit w (nat i) False)" - "update_vec_dec_oracle w i B1 = return (set_bit w (nat i) True)" - "update_vec_dec_oracle w i BU = undefined_bool () \<bind> (\<lambda>b. return (set_bit w (nat i) b))" + "update_vec_dec_nondet w i B0 = return (set_bit w (nat i) False)" + "update_vec_dec_nondet w i B1 = return (set_bit w (nat i) True)" + "update_vec_dec_nondet w i BU = undefined_bool () \<bind> (\<lambda>b. return (set_bit w (nat i) b))" "update_vec_dec w i B0 = set_bit w (nat i) False" "update_vec_dec w i B1 = set_bit w (nat i) True" - unfolding update_vec_dec_maybe_def update_vec_dec_fail_def update_vec_dec_oracle_def update_vec_dec_def + unfolding update_vec_dec_maybe_def update_vec_dec_fail_def update_vec_dec_nondet_def update_vec_dec_def by (auto simp: update_mword_dec_def update_mword_bool_dec_def maybe_failwith_def) lemma len_of_minus_One_minus_nonneg_lt_len_of[simp]: "n \<ge> 0 \<Longrightarrow> nat (int LENGTH('a::len) - 1 - n) < LENGTH('a)" by (metis diff_mono diff_zero len_gt_0 nat_eq_iff2 nat_less_iff order_refl zle_diff1_eq) +declare subrange_vec_dec_def[simp] + +lemma update_subrange_vec_dec_update_subrange_list_dec: + assumes "0 \<le> j" and "j \<le> i" and "i < int LENGTH('a)" + shows "update_subrange_vec_dec (w :: 'a::len word) i j w' = + of_bl (update_subrange_list_dec (to_bl w) i j (to_bl w'))" + using assms + unfolding update_subrange_vec_dec_def update_subrange_list_dec_def update_subrange_list_inc_def + by (auto simp: word_update_def split_at_def Let_def nat_diff_distrib min_def) + +lemma subrange_vec_dec_subrange_list_dec: + assumes "0 \<le> j" and "j \<le> i" and "i < int LENGTH('a)" and "int LENGTH('b) = i - j + 1" + shows "subrange_vec_dec (w :: 'a::len word) i j = (of_bl (subrange_list_dec (to_bl w) i j) :: 'b::len word)" + using assms unfolding subrange_vec_dec_def + by (auto simp: subrange_list_dec_drop_take slice_take of_bl_drop') + +lemma slice_simp[simp]: "slice w lo len = Word.slice (nat lo) w" + by (auto simp: slice_def) + +declare slice_id[simp] + +lemma of_bools_of_bl[simp]: "of_bools_method BC_mword = of_bl" + by (auto simp: BC_mword_defs) + +lemma of_bl_bin_word_of_int: + "len = LENGTH('a) \<Longrightarrow> of_bl (bin_to_bl_aux len n []) = (word_of_int n :: ('a::len) word)" + by (auto simp: of_bl_def bin_bl_bin') + +lemma get_slice_int_0_bin_to_bl[simp]: + "len > 0 \<Longrightarrow> get_slice_int len n 0 = of_bl (bin_to_bl (nat len) n)" + unfolding get_slice_int_def get_slice_int_bv_def subrange_list_def + by (auto simp: subrange_list_dec_drop_take len_bin_to_bl_aux) + +lemma to_bl_of_bl[simp]: + fixes bl :: "bool list" + defines w: "w \<equiv> of_bl bl :: 'a::len word" + assumes len: "length bl = LENGTH('a)" + shows "to_bl w = bl" + using len unfolding w by (intro word_bl.Abs_inverse) auto + +lemma reverse_endianness_byte[simp]: + "LENGTH('a) = 8 \<Longrightarrow> reverse_endianness (w :: 'a::len word) = w" + unfolding reverse_endianness_def by (auto simp: reverse_endianness_list_simps) + +lemma reverse_reverse_endianness[simp]: + "8 dvd LENGTH('a) \<Longrightarrow> reverse_endianness (reverse_endianness w) = (w :: 'a::len word)" + unfolding reverse_endianness_def by (simp) + +lemma replicate_bits_zero[simp]: "replicate_bits 0 n = 0" + by (intro word_eqI) (auto simp: replicate_bits_def test_bit_of_bl rev_nth nth_repeat simp del: repeat.simps) + declare extz_vec_def[simp] declare exts_vec_def[simp] declare concat_vec_def[simp] @@ -109,4 +160,10 @@ lemma arith_vec_int_simps[simp]: unfolding add_vec_int_def sub_vec_int_def mult_vec_int_def by (auto simp: arith_op_bv_int_def BC_mword_defs word_add_def word_sub_wi word_mult_def) +lemma shiftl_simp[simp]: "shiftl w l = w << (nat l)" + by (auto simp: shiftl_def shiftl_mword_def) + +lemma shiftr_simp[simp]: "shiftr w l = w >> (nat l)" + by (auto simp: shiftr_def shiftr_mword_def) + end diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy index 08c9b33c..25eb9f52 100644 --- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy +++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy @@ -64,7 +64,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, ' | Barrier: "((Barrier bk k), e_barrier bk, k) \<in> T" | Read_reg: "((Read_reg r k), e_read_reg r v, k v) \<in> T" | Write_reg: "((Write_reg r v k), e_write_reg r v, k) \<in> T" -| Undefined : "((Undefined k), e_undefined v, k v) \<in> T" +| Undefined: "((Undefined k), e_undefined v, k v) \<in> T" | Print: "((Print msg k), e_print msg, k) \<in> T" inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where @@ -95,7 +95,7 @@ lemma Traces_cases: | (Write_ea) wk addr s k t' where "m = Write_ea wk addr s k" and "t = e_write_ea wk addr s # t'" and "(k, t', m') \<in> Traces" | (Footprint) k t' where "m = Footprint k" and "t = e_footprint # t'" and "(k, t', m') \<in> Traces" | (Write_reg) reg v k t' where "m = Write_reg reg v k" and "t = e_write_reg reg v # t'" and "(k, t', m') \<in> Traces" - | (Undefined) v k t' where "m = Undefined k" and "t = e_undefined v # t'" and "(k v, t', m') \<in> Traces" + | (Undefined) xs v k t' where "m = Undefined k" and "t = e_undefined v # t'" and "(k v, t', m') \<in> Traces" | (Print) msg k t' where "m = Print msg k" and "t = e_print msg # t'" and "(k, t', m') \<in> Traces" proof (use Run in \<open>cases m t m' set: Traces\<close>) case Nil @@ -129,6 +129,16 @@ lemma bind_T_cases: | (Bind) m' where "s' = bind m' f" and "(m, e, m') \<in> T" using assms by (cases; blast elim: bind.elims) +lemma Run_bindI: + fixes m :: "('r, 'a, 'e) monad" + assumes "Run m t1 a1" + and "Run (f a1) t2 a2" + shows "Run (m \<bind> f) (t1 @ t2) a2" +proof (use assms in \<open>induction m t1 "Done a1 :: ('r, 'a, 'e) monad" rule: Traces.induct\<close>) + case (Step s e s'' t) + then show ?case by (elim T.cases) auto +qed auto + lemma Run_bindE: fixes m :: "('rv, 'b, 'e) monad" and a :: 'a assumes "Run (bind m f) t a" @@ -161,6 +171,31 @@ lemma Run_DoneE: lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a" by (auto elim: Run_DoneE) +lemma Run_bindE_ignore_trace: + assumes "Run (m \<bind> f) t a" + obtains tm tf am where "Run m tm am" and "Run (f am) tf a" + using assms by (elim Run_bindE) + +lemma Run_letE: + assumes "Run (let x = y in f x) t a" + obtains "Run (f y) t a" + using assms by auto + +lemma Run_ifE: + assumes "Run (if b then f else g) t a" + obtains "b" and "Run f t a" | "\<not>b" and "Run g t a" + using assms by (auto split: if_splits) + +lemma Run_returnE: + assumes "Run (return x) t a" + obtains "t = []" and "a = x" + using assms by (auto simp: return_def) + +lemma Run_early_returnE: + assumes "Run (early_return x) t a" + shows P + using assms by (auto simp: early_return_def throw_def elim: Traces_cases) + lemma bind_cong[fundef_cong]: assumes m: "m1 = m2" and f: "\<And>t a. Run m2 t a \<Longrightarrow> f1 a = f2 a" @@ -168,4 +203,10 @@ lemma bind_cong[fundef_cong]: unfolding m using f by (induction m2 f1 arbitrary: f2 rule: bind.induct; unfold bind.simps; blast) +lemma liftR_read_reg[simp]: "liftR (read_reg reg) = read_reg reg" by (auto simp: read_reg_def liftR_def split: option.splits) +lemma try_catch_return[simp]: "try_catch (return x) h = return x" by (auto simp: return_def) +lemma liftR_return[simp]: "liftR (return x) = return x" by (auto simp: liftR_def) +lemma liftR_undefined_bool[simp]: "liftR (undefined_bool ()) = undefined_bool ()" by (auto simp: undefined_bool_def liftR_def) +lemma assert_exp_True_return[simp]: "assert_exp True msg = return ()" by (auto simp: assert_exp_def return_def) + end diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy index 124722ab..ba69d0d8 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -23,6 +23,14 @@ lemma Value_liftState_Run: lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra] +lemma Value_bindS_iff: + "(Value b, s'') \<in> bindS m f s \<longleftrightarrow> (\<exists>a s'. (Value a, s') \<in> m s \<and> (Value b, s'') \<in> f a s')" + by (auto elim!: bindS_cases intro: bindS_intros) + +lemma Ex_bindS_iff: + "(Ex e, s'') \<in> bindS m f s \<longleftrightarrow> (Ex e, s'') \<in> m s \<or> (\<exists>a s'. (Value a, s') \<in> m s \<and> (Ex e, s'') \<in> f a s')" + by (auto elim!: bindS_cases intro: bindS_intros) + lemma liftState_throw[liftState_simp]: "liftState r (throw e) = throwS e" by (auto simp: throw_def) lemma liftState_assert[liftState_simp]: "liftState r (assert_exp c msg) = assert_expS c msg" @@ -51,7 +59,7 @@ lemma liftState_try_catch[liftState_simp]: by (induction m h rule: try_catch_induct) (auto simp: try_catchS_bindS_no_throw) lemma liftState_early_return[liftState_simp]: - "liftState r (early_return r) = early_returnS r" + "liftState r (early_return x) = early_returnS x" by (auto simp: early_return_def early_returnS_def liftState_simp) lemma liftState_catch_early_return[liftState_simp]: @@ -66,6 +74,10 @@ lemma liftState_try_catchR[liftState_simp]: "liftState r (try_catchR m h) = try_catchRS (liftState r m) (liftState r \<circ> h)" by (auto simp: try_catchR_def try_catchRS_def sum.case_distrib liftState_simp cong: sum.case_cong) +lemma liftState_bool_of_bitU_nondet[liftState_simp]: + "liftState r (bool_of_bitU_nondet b) = bool_of_bitU_nondetS b" + by (cases b; auto simp: bool_of_bitU_nondet_def bool_of_bitU_nondetS_def liftState_simp) + lemma liftState_read_mem_BC: assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a" shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz" @@ -87,7 +99,7 @@ lemma liftState_write_mem_ea[liftState_simp]: "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = write_mem_eaS BC_bitU_list rk a (nat sz)" by (auto simp: liftState_write_mem_ea_BC) -lemma liftState_write_mem_val: +lemma liftState_write_mem_val[liftState_simp]: "liftState r (write_mem_val BC v) = write_mem_valS BC v" by (auto simp: write_mem_val_def write_mem_valS_def liftState_simp split: option.splits) @@ -126,6 +138,80 @@ lemma liftState_foreachM[liftState_simp]: by (induction xs vars "\<lambda>x vars. liftState r (body x vars)" rule: foreachS.induct) (auto simp: liftState_simp cong: bindS_cong) +lemma liftState_bools_of_bits_nondet[liftState_simp]: + "liftState r (bools_of_bits_nondet bs) = bools_of_bits_nondetS bs" + unfolding bools_of_bits_nondet_def bools_of_bits_nondetS_def + by (auto simp: liftState_simp comp_def) + +lemma liftState_internal_pick[liftState_simp]: + "liftState r (internal_pick xs) = internal_pickS xs" + by (auto simp: internal_pick_def internal_pickS_def liftState_simp comp_def + option.case_distrib[where h = "liftState r"] + simp del: repeat.simps + cong: option.case_cong) + +lemma liftRS_returnS[simp]: "liftRS (returnS x) = returnS x" + by (auto simp: liftRS_def) + +lemma liftRS_bindS: + fixes m :: "('regs, 'a, 'e) monadS" and f :: "'a \<Rightarrow> ('regs, 'b, 'e) monadS" + shows "(liftRS (bindS m f) :: ('regs, 'b, 'r, 'e) monadRS) = bindS (liftRS m) (liftRS \<circ> f)" +proof (intro ext set_eqI iffI) + fix s and rs' :: "('b, 'r + 'e) result \<times> 'regs sequential_state" + assume lhs: "rs' \<in> liftRS (bindS m f) s" + then show "rs' \<in> bindS (liftRS m) (liftRS \<circ> f) s" + by (cases rs') + (fastforce simp: liftRS_def throwS_def elim!: bindS_cases try_catchS_cases + intro: bindS_intros try_catchS_intros) +next + fix s and rs' :: "('b, 'r + 'e) result \<times> 'regs sequential_state" + assume "rs' \<in> bindS (liftRS m) (liftRS \<circ> f) s" + then show "rs' \<in> liftRS (bindS m f) s" + by (cases rs') + (fastforce simp: liftRS_def throwS_def elim!: bindS_cases try_catchS_cases + intro: bindS_intros try_catchS_intros) +qed + +lemma liftRS_assert_expS_True[simp]: "liftRS (assert_expS True msg) = returnS ()" + by (auto simp: liftRS_def assert_expS_def) + +lemma untilM_domI: + fixes V :: "'vars \<Rightarrow> nat" + assumes "Inv vars" + and "\<And>vars t vars' t'. \<lbrakk>Inv vars; Run (body vars) t vars'; Run (cond vars') t' False\<rbrakk> \<Longrightarrow> V vars' < V vars \<and> Inv vars'" + shows "untilM_dom (vars, cond, body)" + using assms + by (induction vars rule: measure_induct_rule[where f = V]) + (auto intro: untilM.domintros) + +lemma untilM_dom_untilS_dom: + assumes "untilM_dom (vars, cond, body)" + shows "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" + using assms + by (induction vars cond body arbitrary: s rule: untilM.pinduct) + (rule untilS.domintros, auto elim!: Value_liftState_Run) + +lemma measure2_induct: + fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> nat" + assumes "\<And>x1 y1. (\<And>x2 y2. f x2 y2 < f x1 y1 \<Longrightarrow> P x2 y2) \<Longrightarrow> P x1 y1" + shows "P x y" +proof - + have "P (fst x) (snd x)" for x + by (induction x rule: measure_induct_rule[where f = "\<lambda>x. f (fst x) (snd x)"]) (auto intro: assms) + then show ?thesis by auto +qed + +lemma untilS_domI: + fixes V :: "'vars \<Rightarrow> 'regs sequential_state \<Rightarrow> nat" + assumes "Inv vars s" + and "\<And>vars s vars' s' s''. + \<lbrakk>Inv vars s; (Value vars', s') \<in> body vars s; (Value False, s'') \<in> cond vars' s'\<rbrakk> + \<Longrightarrow> V vars' s'' < V vars s \<and> Inv vars' s''" + shows "untilS_dom (vars, cond, body, s)" + using assms + by (induction vars s rule: measure2_induct[where f = V]) + (auto intro: untilS.domintros) + lemma whileS_dom_step: assumes "whileS_dom (vars, cond, body, s)" and "(Value True, s') \<in> cond vars s" @@ -230,6 +316,9 @@ lemma and_boolM_return_if: "and_boolM (return b) y = (if b then y else return False)" by (auto simp: and_boolM_def) +lemma and_boolM_return_return_and[simp]: "and_boolM (return l) (return r) = return (l \<and> r)" + by (auto simp: and_boolM_def) + lemmas and_boolM_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolM x y" for y] lemma or_boolM_simps[simp]: @@ -243,6 +332,9 @@ lemma or_boolM_return_if: "or_boolM (return b) y = (if b then return True else y)" by (auto simp: or_boolM_def) +lemma or_boolM_return_return_or[simp]: "or_boolM (return l) (return r) = return (l \<or> r)" + by (auto simp: or_boolM_def) + lemmas or_boolM_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolM x y" for y] lemma if_returnS_returnS[simp]: "(if a then returnS True else returnS False) = returnS a" by auto @@ -260,8 +352,12 @@ lemma and_boolS_returnS_if: lemmas and_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolS x y" for y] +lemma and_boolS_returnS_True[simp]: "and_boolS (returnS True) c = c" + by (auto simp: and_boolS_def) + lemma or_boolS_simps[simp]: "or_boolS (returnS b) (returnS c) = returnS (b \<or> c)" + "or_boolS (returnS False) m = m" "or_boolS x (returnS True) = bindS x (\<lambda>_. returnS True)" "or_boolS x (returnS False) = x" "\<And>x y z. or_boolS (bindS x y) z = (bindS x (\<lambda>r. or_boolS (y r) z))" @@ -273,4 +369,19 @@ lemma or_boolS_returnS_if: lemmas or_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolS x y" for y] +lemma Run_or_boolM_E: + assumes "Run (or_boolM l r) t a" + obtains "Run l t True" and "a" + | tl tr where "Run l tl False" and "Run r tr a" and "t = tl @ tr" + using assms by (auto simp: or_boolM_def elim!: Run_bindE Run_ifE Run_returnE) + +lemma Run_and_boolM_E: + assumes "Run (and_boolM l r) t a" + obtains "Run l t False" and "\<not>a" + | tl tr where "Run l tl True" and "Run r tr a" and "t = tl @ tr" + using assms by (auto simp: and_boolM_def elim!: Run_bindE Run_ifE Run_returnE) + +lemma maybe_failS_Some[simp]: "maybe_failS msg (Some v) = returnS v" + by (auto simp: maybe_failS_def) + end diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy index b705de4c..3a286c10 100644 --- a/lib/isabelle/Sail2_state_monad_lemmas.thy +++ b/lib/isabelle/Sail2_state_monad_lemmas.thy @@ -8,6 +8,9 @@ begin notes returnS_def[simp] and failS_def[simp] and throwS_def[simp] and readS_def[simp] and updateS_def[simp] begin*) +notation bindS (infixr "\<bind>\<^sub>S" 54) +notation seqS (infixr "\<then>\<^sub>S" 54) + lemma bindS_ext_cong[fundef_cong]: assumes m: "m1 s = m2 s" and f: "\<And>a s'. (Value a, s') \<in> (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" @@ -35,6 +38,9 @@ lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))" lemma bindS_assertS_True[simp]: "bindS (assert_expS True msg) f = f ()" by (auto simp: assert_expS_def) +lemma bindS_chooseS_returnS[simp]: "bindS (chooseS xs) (\<lambda>x. returnS (f x)) = chooseS (f ` xs)" + by (intro ext) (auto simp: bindS_def chooseS_def returnS_def) + lemma result_cases: fixes r :: "('a, 'e) result" diff --git a/lib/isabelle/Sail2_values_lemmas.thy b/lib/isabelle/Sail2_values_lemmas.thy index b50d8942..576cd8ea 100644 --- a/lib/isabelle/Sail2_values_lemmas.thy +++ b/lib/isabelle/Sail2_values_lemmas.thy @@ -2,18 +2,135 @@ theory Sail2_values_lemmas imports Sail2_values begin +lemma while_domI: + fixes V :: "'vars \<Rightarrow> nat" + assumes "\<And>vars. cond vars \<Longrightarrow> V (body vars) < V vars" + shows "while_dom (vars, cond, body)" + by (induction vars rule: measure_induct_rule[where f = V]) + (use assms in \<open>auto intro: while.domintros\<close>) + lemma nat_of_int_nat_simps[simp]: "nat_of_int = nat" by (auto simp: nat_of_int_def) termination reverse_endianness_list by (lexicographic_order simp add: drop_list_def) +declare reverse_endianness_list.simps[simp del] +declare take_list_def[simp] +declare drop_list_def[simp] + +function take_chunks :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where + "take_chunks n [] = []" +| "take_chunks 0 xs = []" +| "take_chunks n xs = take n xs # take_chunks n (drop n xs)" if "n > 0" and "xs \<noteq> []" + by auto blast +termination by lexicographic_order + +lemma take_chunks_length_leq_n: "length xs \<le> n \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> take_chunks n xs = [xs]" + by (cases n) auto + +lemma take_chunks_append: "n dvd length a \<Longrightarrow> take_chunks n (a @ b) = take_chunks n a @ take_chunks n b" + by (induction n a rule: take_chunks.induct) (auto simp: dvd_imp_le) + +lemma Suc8_plus8: "Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc x))))))) = 8 + x" + by auto + +lemma byte_chunks_take_chunks_8: + assumes "8 dvd length xs" + shows "byte_chunks xs = Some (take_chunks 8 xs)" +proof - + have Suc8_plus8: "Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc x))))))) = 8 + x" for x + by auto + from assms show ?thesis + by (induction xs rule: byte_chunks.induct) (auto simp: Suc8_plus8 nat_dvd_not_less) +qed + +lemma reverse_endianness_list_rev_take_chunks: + "reverse_endianness_list bits = List.concat (rev (take_chunks 8 bits))" + by (induction "8 :: nat" bits rule: take_chunks.induct) + (auto simp: reverse_endianness_list.simps) + +lemma reverse_endianness_list_simps: + "length bits \<le> 8 \<Longrightarrow> reverse_endianness_list bits = bits" + "length bits > 8 \<Longrightarrow> reverse_endianness_list bits = reverse_endianness_list (drop 8 bits) @ take 8 bits" + by (cases bits; auto simp: reverse_endianness_list_rev_take_chunks)+ + +lemma reverse_endianness_list_append: + assumes "8 dvd length a" + shows "reverse_endianness_list (a @ b) = reverse_endianness_list b @ reverse_endianness_list a" + using assms by (auto simp: reverse_endianness_list_rev_take_chunks take_chunks_append) + +lemma length_reverse_endianness_list[simp]: + "length (reverse_endianness_list l) = length l" + by (induction l rule: reverse_endianness_list.induct) (auto simp: reverse_endianness_list.simps) + +lemma reverse_endianness_list_take_8[simp]: + "reverse_endianness_list (take 8 bits) = take 8 bits" + by (auto simp: reverse_endianness_list_simps) + +lemma reverse_reverse_endianness_list[simp]: + assumes "8 dvd length l" + shows "reverse_endianness_list (reverse_endianness_list l) = l" +proof (use assms in \<open>induction l rule: reverse_endianness_list.induct[case_names Step]\<close>) + case (Step bits) + then show ?case + by (auto simp: reverse_endianness_list.simps[of bits] reverse_endianness_list_append) +qed + +declare repeat.simps[simp del] + +lemma length_repeat[simp]: "length (repeat xs n) = nat n * length xs" +proof (induction xs n rule: repeat.induct[case_names Step]) + case (Step xs n) + then show ?case unfolding repeat.simps[of xs n] + by (auto simp del: mult_Suc simp: mult_Suc[symmetric]) +qed + +lemma nth_repeat: + assumes "i < nat n * length xs" + shows "repeat xs n ! i = xs ! (i mod length xs)" +proof (use assms in \<open>induction xs n arbitrary: i rule: repeat.induct[case_names Step]\<close>) + case (Step xs n i) + show ?case + using Step.prems Step.IH[of "i - length xs"] + unfolding repeat.simps[of xs n] + by (auto simp: nth_append mod_geq[symmetric] nat_diff_distrib diff_mult_distrib) +qed termination index_list by (relation "measure (\<lambda>(i, j, step). nat ((j - i + step) * sgn step))") auto +lemma index_list_Zero[simp]: "index_list i j 0 = []" + by auto + +lemma index_list_singleton[simp]: "n \<noteq> 0 \<Longrightarrow> index_list i i n = [i]" + by auto + +lemma index_list_simps: + "0 < step \<Longrightarrow> from \<le> to \<Longrightarrow> index_list from to step = from # index_list (from + step) to step" + "0 < step \<Longrightarrow> from > to \<Longrightarrow> index_list from to step = []" + "0 > step \<Longrightarrow> from \<ge> to \<Longrightarrow> index_list from to step = from # index_list (from + step) to step" + "0 > step \<Longrightarrow> from < to \<Longrightarrow> index_list from to step = []" + by auto + +lemma index_list_step1_upto[simp]: "index_list i j 1 = [i..j]" + by (induction i j "1 :: int" rule: index_list.induct) + (auto simp: index_list_simps upto.simps) + +lemma length_upto[simp]: "i \<le> j \<Longrightarrow> length [i..j] = nat (j - i + 1)" + by (induction i j rule: upto.induct) (auto simp: upto.simps) + +lemma nth_upto[simp]: "i + int n \<le> j \<Longrightarrow> [i..j] ! n = i + int n" + by (induction i j arbitrary: n rule: upto.induct) + (auto simp: upto.simps nth_Cons split: nat.splits) + +declare index_list.simps[simp del] + lemma just_list_map_Some[simp]: "just_list (map Some v) = Some v" by (induction v) auto lemma just_list_None_iff[simp]: "just_list xs = None \<longleftrightarrow> None \<in> set xs" by (induction xs) (auto split: option.splits) +lemma just_list_None_member_None: "None \<in> set xs \<Longrightarrow> just_list xs = None" + by auto + lemma just_list_Some_iff[simp]: "just_list xs = Some ys \<longleftrightarrow> xs = map Some ys" by (induction xs arbitrary: ys) (auto split: option.splits) @@ -28,10 +145,10 @@ lemma repeat_singleton_replicate[simp]: proof (induction n) case (nonneg n) have "nat (1 + int m) = Suc m" for m by auto - then show ?case by (induction n) auto + then show ?case by (induction n) (auto simp: repeat.simps) next case (neg n) - then show ?case by auto + then show ?case by (auto simp: repeat.simps) qed lemma bool_of_bitU_simps[simp]: @@ -102,6 +219,15 @@ lemma unsigned_bits_of_mword[simp]: "unsigned_method BC_bitU_list (bits_of_method BC_mword a) = Some (uint a)" by (auto simp: BC_bitU_list_def BC_mword_defs unsigned_of_bits_def unsigned_of_bools_def) +definition mem_bytes_of_word :: "'a::len word \<Rightarrow> bitU list list" where + "mem_bytes_of_word w = rev (take_chunks 8 (map bitU_of_bool (to_bl w)))" + +lemma mem_bytes_of_bits_mem_bytes_of_word[simp]: + assumes "8 dvd LENGTH('a)" + shows "mem_bytes_of_bits BC_mword (w :: 'a::len word) = Some (mem_bytes_of_word w)" + using assms + by (auto simp: mem_bytes_of_bits_def bytes_of_bits_def BC_mword_defs byte_chunks_take_chunks_8 mem_bytes_of_word_def) + lemma bits_of_bitU_list[simp]: "bits_of_method BC_bitU_list v = v" "of_bits_method BC_bitU_list v = Some v" @@ -158,6 +284,14 @@ lemma update_list_dec_update[simp]: "update_list_dec xs n x = xs[length xs - nat (n + 1) := x]" by (auto simp: update_list_dec_def add.commute diff_diff_add nat_minus_as_int) +lemma update_list_dec_update_rev: + "0 \<le> n \<Longrightarrow> nat n < length xs \<Longrightarrow> update_list_dec xs n x = rev ((rev xs)[nat n := x])" + by (auto simp: update_list_dec_def add.commute diff_diff_add nat_minus_as_int rev_update) + +lemma access_list_dec_update_list_dec[simp]: + "0 \<le> n \<Longrightarrow> nat n < length xs \<Longrightarrow> access_list_dec (update_list_dec xs n x) n = x" + by (auto simp: access_list_dec_rev_nth update_list_dec_update_rev) + lemma bools_of_nat_aux_simps[simp]: "\<And>len. len \<le> 0 \<Longrightarrow> bools_of_nat_aux len x acc = acc" "\<And>len. bools_of_nat_aux (int (Suc len)) x acc = @@ -200,7 +334,7 @@ proof (induction len arbitrary: n acc) qed auto lemma bools_of_int_bin_to_bl[simp]: - "bools_of_int (int len) n = bin_to_bl len n" + "bools_of_int len n = bin_to_bl (nat len) n" by (auto simp: bools_of_int_def Let_def map_Not_bin_to_bl rbl_succ[unfolded bin_to_bl_def]) end diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy index 6cd90a9a..0d67f6c5 100644 --- a/lib/isabelle/manual/Manual.thy +++ b/lib/isabelle/manual/Manual.thy @@ -168,8 +168,8 @@ following variants: \<^item> @{term quot_vec_maybe} returns an option type, with @{lemma "quot_vec_maybe w 0 = None" by (auto simp: quot_vec_maybe_def quot_bv_def arith_op_bv_no0_def)}. \<^item> @{term quot_vec_fail} is monadic and either returns the result or raises an exception. - \<^item> @{term quot_vec_oracle} is monadic and uses the @{term Undefined} effect in the exception case - to fill the result with bits drawn from a bitstream oracle. + \<^item> @{term quot_vec_nondet} is monadic and uses the @{term Undefined} effect in the exception case + to fill the result with bits chosen nondeterministically. \<^item> @{term quot_vec} is pure and returns an arbitrary (but fixed) value in the exception case, currently defined as follows: For the bitlist representation of bitvectors, @{term "quot_vec w 0"} returns a list filled with @{term BU}, while for the machine word @@ -263,9 +263,6 @@ The @{type sequential_state} record has the following fields: of the last announced memory write, if any. \<^item> The @{term last_exclusive_operation_was_load} flag is used to determine whether exclusive operations can succeed. - \<^item> The function stored in the @{term next_bool} field together with the seed in the @{term seed} - field are used as a random bit generator for undefined values. The @{term next_bool} - function takes the current seed as an argument and returns a @{type bool} and the next seed. The library defines several combinators and wrappers in addition to the standard monadic bind and return (called @{term bindS} and @{term returnS} here, where the suffix @{term S} differentiates them diff --git a/lib/main.ml b/lib/main.ml index e9dcb4e0..c1b6fcae 100644 --- a/lib/main.ml +++ b/lib/main.ml @@ -1,4 +1,3 @@ - (**************************************************************************) (* Sail *) (* *) diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index c9164b6c..aa8d05cd 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -42,14 +42,14 @@ val is_zero_subrange : forall 'n, 'n >= 0. (bits('n), int, int) -> bool effect pure function is_zero_subrange (xs, i, j) = { - (xs & slice_mask(j, i-j)) == extzv(0b0) + (xs & slice_mask(j, i-j+1)) == extzv(0b0) } val is_ones_subrange : forall 'n, 'n >= 0. (bits('n), int, int) -> bool effect pure function is_ones_subrange (xs, i, j) = { - let m : bits('n) = slice_mask(j,j-i) in + let m : bits('n) = slice_mask(j,j-i+1) in (xs & m) == m } @@ -76,8 +76,8 @@ val subrange_subrange_eq : forall 'n, 'n >= 0. (bits('n), int, int, bits('n), int, int) -> bool effect pure function subrange_subrange_eq (xs, i, j, ys, i', j') = { - let xs = (xs & slice_mask(j,i-j)) >> j in - let ys = (ys & slice_mask(j',i'-j')) >> j' in + let xs = (xs & slice_mask(j,i-j+1)) >> j in + let ys = (ys & slice_mask(j',i'-j'+1)) >> j' in xs == ys } @@ -85,16 +85,16 @@ val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's = 'o - ('p - 1) + (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure function subrange_subrange_concat (xs, i, j, ys, i', j') = { - let xs = (xs & slice_mask(j,i-j)) >> j in - let ys = (ys & slice_mask(j',i'-j')) >> j' in - extzv(xs) << i' - (j' - 1) | extzv(ys) + let xs = (xs & slice_mask(j,i-j+1)) >> j in + let ys = (ys & slice_mask(j',i'-j'+1)) >> j' in + extzv(xs) << (i' - j' + 1) | extzv(ys) } val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0. (bits('n), int, int, int) -> bits('m) effect pure function place_subrange(xs,i,j,shift) = { - let xs = (xs & slice_mask(j,i-j)) >> j in + let xs = (xs & slice_mask(j,i-j+1)) >> j in extzv(xs) << shift } @@ -144,7 +144,7 @@ val unsigned_subrange : forall 'n, 'n >= 0. (bits('n), int, int) -> int effect pure function unsigned_subrange(xs,i,j) = { - let xs = (xs & slice_mask(j,i-j)) >> i in + let xs = (xs & slice_mask(j,i-j+1)) >> i in _builtin_unsigned(xs) } diff --git a/lib/regfp.sail b/lib/regfp.sail index b8cffb98..fcf10850 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -75,6 +75,10 @@ enum barrier_kind = { Barrier_RISCV_r_r, Barrier_RISCV_rw_w, Barrier_RISCV_w_w, + Barrier_RISCV_w_rw, + Barrier_RISCV_rw_r, + Barrier_RISCV_r_w, + Barrier_RISCV_w_r, Barrier_RISCV_i, Barrier_x86_MFENCE } @@ -7,7 +7,7 @@ #include"elf.h" static uint64_t g_elf_entry; -static uint64_t g_cycle_count = 0; +uint64_t g_cycle_count = 0; static uint64_t g_cycle_limit; void sail_match_failure(sail_string msg) @@ -208,7 +208,7 @@ void kill_mem() // ***** Memory builtins ***** -unit write_ram(const mpz_t addr_size, // Either 32 or 64 +bool write_ram(const mpz_t addr_size, // Either 32 or 64 const mpz_t data_size_mpz, // Number of bytes const sail_bits hex_ram, // Currently unused const sail_bits addr_bv, @@ -231,7 +231,7 @@ unit write_ram(const mpz_t addr_size, // Either 32 or 64 } mpz_clear(buf); - return UNIT; + return true; } void read_ram(sail_bits *data, @@ -427,7 +427,7 @@ bool cycle_limit_reached(const unit u) unit cycle_count(const unit u) { if (cycle_limit_reached(UNIT)) { - printf("\n[Sail] cycle limit %" PRId64 " reached\n", g_cycle_limit); + printf("\n[Sail] TIMEOUT: exceeded %" PRId64 " cycles\n", g_cycle_limit); exit(EXIT_SUCCESS); } return UNIT; @@ -53,7 +53,7 @@ uint64_t read_mem(uint64_t); // These memory builtins are intended to match the semantics for the // __ReadRAM and __WriteRAM functions in ASL. -unit write_ram(const mpz_t addr_size, // Either 32 or 64 +bool write_ram(const mpz_t addr_size, // Either 32 or 64 const mpz_t data_size_mpz, // Number of bytes const sail_bits hex_ram, // Currently unused const sail_bits addr_bv, @@ -1,3 +1,4 @@ +#include<assert.h> #include<inttypes.h> #include<stdbool.h> #include<stdio.h> @@ -34,7 +35,7 @@ void cleanup_library(void) mpq_clear(sail_lib_tmp_real); } -bool eq_unit(const unit a, const unit b) +bool EQUAL(unit)(const unit a, const unit b) { return true; } @@ -62,7 +63,7 @@ bool not(const bool b) { return !b; } -bool eq_bool(const bool a, const bool b) { +bool EQUAL(bool)(const bool a, const bool b) { return a == b; } @@ -116,6 +117,11 @@ bool eq_string(const sail_string str1, const sail_string str2) return strcmp(str1, str2) == 0; } +bool EQUAL(sail_string)(const sail_string str1, const sail_string str2) +{ + return strcmp(str1, str2) == 0; +} + void undefined_string(sail_string *str, const unit u) {} void concat_str(sail_string *stro, const sail_string str1, const sail_string str2) @@ -128,6 +134,12 @@ void concat_str(sail_string *stro, const sail_string str1, const sail_string str /* ***** Sail integers ***** */ +inline +bool EQUAL(mach_int)(const mach_int op1, const mach_int op2) +{ + return op1 == op2; +} + #ifndef USE_INT128 inline @@ -197,6 +209,12 @@ bool eq_int(const sail_int op1, const sail_int op2) } inline +bool EQUAL(sail_int)(const sail_int op1, const sail_int op2) +{ + return !abs(mpz_cmp(op1, op2)); +} + +inline bool lt(const sail_int op1, const sail_int op2) { return mpz_cmp(op1, op2) < 0; @@ -329,6 +347,11 @@ void pow2(sail_int *rop, const sail_int exp) { /* ***** Sail bitvectors ***** */ +bool EQUAL(mach_bits)(const mach_bits op1, const mach_bits op2) +{ + return op1 == op2; +} + void CREATE(sail_bits)(sail_bits *rop) { rop->bits = malloc(sizeof(mpz_t)); @@ -419,6 +442,7 @@ void add_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2) void sub_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2) { + assert(op1.len == op2.len); rop->len = op1.len; mpz_sub(*rop->bits, *op1.bits, *op2.bits); normalize_sail_bits(rop); @@ -440,18 +464,21 @@ void sub_bits_int(sail_bits *rop, const sail_bits op1, const mpz_t op2) void and_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2) { + assert(op1.len == op2.len); rop->len = op1.len; mpz_and(*rop->bits, *op1.bits, *op2.bits); } void or_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2) { + assert(op1.len == op2.len); rop->len = op1.len; mpz_ior(*rop->bits, *op1.bits, *op2.bits); } void xor_bits(sail_bits *rop, const sail_bits op1, const sail_bits op2) { + assert(op1.len == op2.len); rop->len = op1.len; mpz_xor(*rop->bits, *op1.bits, *op2.bits); } @@ -495,12 +522,14 @@ void zeros(sail_bits *rop, const sail_int op) void zero_extend(sail_bits *rop, const sail_bits op, const sail_int len) { + assert(op.len <= mpz_get_ui(len)); rop->len = mpz_get_ui(len); mpz_set(*rop->bits, *op.bits); } void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len) { + assert(op.len <= mpz_get_ui(len)); rop->len = mpz_get_ui(len); if(mpz_tstbit(*op.bits, op.len - 1)) { mpz_set(*rop->bits, *op.bits); @@ -519,14 +548,21 @@ void length_sail_bits(sail_int *rop, const sail_bits op) bool eq_bits(const sail_bits op1, const sail_bits op2) { + assert(op1.len == op2.len); for (mp_bitcnt_t i = 0; i < op1.len; i++) { if (mpz_tstbit(*op1.bits, i) != mpz_tstbit(*op2.bits, i)) return false; } return true; } +bool EQUAL(sail_bits)(const sail_bits op1, const sail_bits op2) +{ + return eq_bits(op1, op2); +} + bool neq_bits(const sail_bits op1, const sail_bits op2) { + assert(op1.len == op2.len); for (mp_bitcnt_t i = 0; i < op1.len; i++) { if (mpz_tstbit(*op1.bits, i) != mpz_tstbit(*op2.bits, i)) return true; } @@ -548,6 +584,7 @@ void vector_subrange_sail_bits(sail_bits *rop, void sail_truncate(sail_bits *rop, const sail_bits op, const sail_int len) { + assert(op.len >= mpz_get_ui(len)); rop->len = mpz_get_ui(len); mpz_set(*rop->bits, *op.bits); normalize_sail_bits(rop); @@ -594,8 +631,8 @@ void replicate_bits(sail_bits *rop, const sail_bits op1, const mpz_t op2) { uint64_t op2_ui = mpz_get_ui(op2); rop->len = op1.len * op2_ui; - mpz_set(*rop->bits, *op1.bits); - for (int i = 1; i < op2_ui; i++) { + mpz_set_ui(*rop->bits, 0); + for (int i = 0; i < op2_ui; i++) { mpz_mul_2exp(*rop->bits, *rop->bits, op1.len); mpz_ior(*rop->bits, *rop->bits, *op1.bits); } @@ -670,6 +707,7 @@ void vector_update_subrange_sail_bits(sail_bits *rop, uint64_t m = mpz_get_ui(m_mpz); mpz_set(*rop->bits, *op.bits); + rop->len = op.len; for (uint64_t i = 0; i < n - (m - 1ul); i++) { if (mpz_tstbit(*slice.bits, i)) { @@ -682,10 +720,11 @@ void vector_update_subrange_sail_bits(sail_bits *rop, void slice(sail_bits *rop, const sail_bits op, const sail_int start_mpz, const sail_int len_mpz) { + assert(mpz_get_ui(start_mpz) + mpz_get_ui(len_mpz) <= op.len); uint64_t start = mpz_get_ui(start_mpz); uint64_t len = mpz_get_ui(len_mpz); - mpz_set_ui(*rop->bits, 0ul); + mpz_set_ui(*rop->bits, 0); rop->len = len; for (uint64_t i = 0; i < len; i++) { @@ -742,6 +781,19 @@ void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits } } +void shiftl(sail_bits *rop, const sail_bits op1, const sail_int op2) +{ + rop->len = op1.len; + mpz_mul_2exp(*rop->bits, *op1.bits, mpz_get_ui(op2)); + normalize_sail_bits(rop); +} + +void shiftr(sail_bits *rop, const sail_bits op1, const sail_int op2) +{ + rop->len = op1.len; + mpz_tdiv_q_2exp(*rop->bits, *op1.bits, mpz_get_ui(op2)); +} + void reverse_endianness(sail_bits *rop, const sail_bits op) { rop->len = op.len; @@ -916,7 +968,7 @@ void to_real(real *rop, const sail_int op) mpq_canonicalize(*rop); } -bool eq_real(const real op1, const real op2) +bool EQUAL(real)(const real op1, const real op2) { return mpq_cmp(op1, op2) == 0; } @@ -30,6 +30,7 @@ void cleanup_library(void); #define COPY(type) copy_ ## type #define KILL(type) kill_ ## type #define UNDEFINED(type) undefined_ ## type +#define EQUAL(type) eq_ ## type #define SAIL_BUILTIN_TYPE(type)\ void create_ ## type(type *);\ @@ -44,7 +45,7 @@ typedef int unit; #define UNIT 0 unit UNDEFINED(unit)(const unit); -bool eq_unit(const unit, const unit); +bool EQUAL(unit)(const unit, const unit); unit skip(const unit); @@ -55,7 +56,7 @@ unit skip(const unit); * short-circuiting evaluation. */ bool not(const bool); -bool eq_bool(const bool, const bool); +bool EQUAL(bool)(const bool, const bool); bool UNDEFINED(bool)(const unit); /* ***** Sail strings ***** */ @@ -73,6 +74,7 @@ void hex_str(sail_string *str, const mpz_t n); void undefined_string(sail_string *str, const unit u); bool eq_string(const sail_string, const sail_string); +bool EQUAL(sail_string)(const sail_string, const sail_string); void concat_str(sail_string *stro, const sail_string str1, const sail_string str2); @@ -80,6 +82,8 @@ void concat_str(sail_string *stro, const sail_string str1, const sail_string str typedef int64_t mach_int; +bool EQUAL(mach_int)(const mach_int, const mach_int); + /* * Integers can be either stack-allocated as 128-bit integers if * __int128 is available, or use GMP arbitrary precision @@ -114,6 +118,7 @@ typedef __int128 sail_int; * Comparison operators for integers */ bool eq_int(const sail_int, const sail_int); +bool EQUAL(sail_int)(const sail_int, const sail_int); bool lt(const sail_int, const sail_int); bool gt(const sail_int, const sail_int); @@ -162,6 +167,8 @@ typedef uint64_t mach_bits; bool eq_bit(const mach_bits a, const mach_bits b); +bool EQUAL(mach_bits)(const mach_bits, const mach_bits); + typedef struct { mp_bitcnt_t len; mpz_t *bits; @@ -218,6 +225,7 @@ void sign_extend(sail_bits *rop, const sail_bits op, const sail_int len); void length_sail_bits(sail_int *rop, const sail_bits op); bool eq_bits(const sail_bits op1, const sail_bits op2); +bool EQUAL(sail_bits)(const sail_bits op1, const sail_bits op2); bool neq_bits(const sail_bits op1, const sail_bits op2); void vector_subrange_sail_bits(sail_bits *rop, @@ -265,6 +273,9 @@ void shift_bits_left(sail_bits *rop, const sail_bits op1, const sail_bits op2); void shift_bits_right(sail_bits *rop, const sail_bits op1, const sail_bits op2); void shift_bits_right_arith(sail_bits *rop, const sail_bits op1, const sail_bits op2); +void shiftl(sail_bits *rop, const sail_bits op1, const sail_int op2); +void shiftr(sail_bits *rop, const sail_bits op1, const sail_int op2); + void reverse_endianness(sail_bits*, sail_bits); /* ***** Sail reals ***** */ @@ -292,7 +303,7 @@ void round_down(sail_int *rop, const real op); void to_real(real *rop, const sail_int op); -bool eq_real(const real op1, const real op2); +bool EQUAL(real)(const real op1, const real op2); bool lt_real(const real op1, const real op2); bool gt_real(const real op1, const real op2); diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 86bbe601..8abcd218 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -22,7 +22,7 @@ val vector_length = { ocaml: "length", lem: "length_list", c: "length", - coq: "length_list" + coq: "vec_length" } : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) overload length = {bitvector_length, vector_length} @@ -68,7 +68,7 @@ val bitvector_access = { val plain_vector_access = { ocaml: "access", lem: "access_list_dec", - coq: "access_list_dec", + coq: "vec_access_dec", c: "vector_access" } : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a @@ -84,7 +84,7 @@ val bitvector_update = { val plain_vector_update = { ocaml: "update", lem: "update_list_dec", - coq: "update_list_dec", + coq: "vec_update_dec", c: "vector_update" } : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) |