summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/isabelle/Hoare.thy22
-rw-r--r--lib/isabelle/ROOT2
-rw-r--r--lib/isabelle/Sail2_operators_mwords_lemmas.thy4
-rw-r--r--lib/isabelle/Sail2_prompt_monad_lemmas.thy304
-rw-r--r--lib/isabelle/Sail2_state_lemmas.thy189
-rw-r--r--lib/isabelle/Sail2_state_monad_lemmas.thy37
-rw-r--r--lib/isabelle/Sail2_values_lemmas.thy28
-rw-r--r--src/gen_lib/sail2_prompt.lem26
-rw-r--r--src/gen_lib/sail2_prompt_monad.lem230
-rw-r--r--src/gen_lib/sail2_state.lem16
-rw-r--r--src/gen_lib/sail2_state_lifting.lem66
-rw-r--r--src/gen_lib/sail2_state_monad.lem138
-rw-r--r--src/gen_lib/sail2_values.lem3
13 files changed, 802 insertions, 263 deletions
diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy
index 76750117..98b7d077 100644
--- a/lib/isabelle/Hoare.thy
+++ b/lib/isabelle/Hoare.thy
@@ -164,7 +164,7 @@ qed
lemma PrePost_assert_expS[intro, PrePost_atomI]: "PrePost (if c then P (Value ()) else P (Ex (Failure m))) (assert_expS c m) P"
unfolding PrePost_def assert_expS_def by (auto simp: returnS_def failS_def)
-lemma PrePost_chooseS[intro, PrePost_atomI]: "PrePost (\<lambda>s. \<forall>x \<in> xs. Q (Value x) s) (chooseS xs) Q"
+lemma PrePost_chooseS[intro, PrePost_atomI]: "PrePost (\<lambda>s. \<forall>x \<in> set xs. Q (Value x) s) (chooseS xs) Q"
by (auto simp: PrePost_def chooseS_def)
lemma PrePost_failS[intro, PrePost_atomI]: "PrePost (Q (Ex (Failure msg))) (failS msg) Q"
@@ -381,7 +381,7 @@ lemma PrePostE_exitS[PrePostE_atomI, intro]: "PrePostE (E (Failure ''exit'')) (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"
+ "PrePostE (\<lambda>s. \<forall>x \<in> set 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"
@@ -488,11 +488,11 @@ lemma PrePostE_liftState_untilM_pure_cond:
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]:
+lemma PrePostE_choose_boolS_any[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)
+ (choose_boolS unit) Q E"
+ unfolding choose_boolS_def seqS_def
+ by (auto intro: PrePostE_strengthen_pre)
lemma PrePostE_bool_of_bitU_nondetS_any:
"PrePostE (\<lambda>s. \<forall>b. Q b s) (bool_of_bitU_nondetS b) Q E"
@@ -507,11 +507,19 @@ lemma PrePostE_bools_of_bits_nondetS_any:
PrePostE_bool_of_bitU_nondetS_any)+)
auto
+lemma PrePostE_choose_boolsS_any:
+ "PrePostE (\<lambda>s. \<forall>bs. Q bs s) (choose_boolsS n) Q E"
+ unfolding choose_boolsS_def genlistS_def Let_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_choose_boolS_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)+)
+ (rule PrePostE_compositeI PrePostE_atomI PrePostE_choose_boolsS_any)+)
(auto split: option.splits)
end
diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT
index 545e47c4..fb73a673 100644
--- a/lib/isabelle/ROOT
+++ b/lib/isabelle/ROOT
@@ -2,7 +2,7 @@ session "Sail" = "LEM" +
options [browser_info, document = pdf, document_output = "output"]
sessions
"HOL-Eisbach"
- theories [document = false]
+ theories
Sail2_values_lemmas
Sail2_prompt
Sail2_state_lemmas
diff --git a/lib/isabelle/Sail2_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy
index fd54c93a..3e8dcb2f 100644
--- a/lib/isabelle/Sail2_operators_mwords_lemmas.thy
+++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy
@@ -55,7 +55,7 @@ lemma bool_of_bitU_monadic_simps[simp]:
"bool_of_bitU_fail BU = Fail ''bool_of_bitU''"
"bool_of_bitU_nondet B0 = return False"
"bool_of_bitU_nondet B1 = return True"
- "bool_of_bitU_nondet BU = undefined_bool ()"
+ "bool_of_bitU_nondet BU = choose_bool ''bool_of_bitU''"
unfolding bool_of_bitU_fail_def bool_of_bitU_nondet_def
by auto
@@ -68,7 +68,7 @@ lemma update_vec_dec_simps[simp]:
"update_vec_dec_fail w i BU = Fail ''bool_of_bitU''"
"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_nondet w i BU = choose_bool ''bool_of_bitU'' \<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_nondet_def update_vec_dec_def
diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 25eb9f52..1fde3287 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -30,42 +30,22 @@ lemma All_try_catch_dom: "try_catch_dom (m, h)"
termination try_catch using All_try_catch_dom by auto
lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Exception] = try_catch.induct
-datatype 'regval event =
- (* Request to read memory *)
- e_read_mem read_kind "bitU list" nat "memory_byte list"
- | e_read_tag "bitU list" bitU
- (* Write is imminent, at address lifted, of size nat *)
- | e_write_ea write_kind "bitU list" nat
- (* Request the result of store-exclusive *)
- | e_excl_res bool
- (* Request to write memory at last signalled address. Memory value should be 8
- times the size given in ea signal *)
- | e_write_memv "memory_byte list" bool
- | e_write_tag "bitU list" bitU bool
- (* Tell the system to dynamically recalculate dependency footprint *)
- | e_footprint
- (* Request a memory barrier *)
- | e_barrier " barrier_kind "
- (* Request to read register *)
- | e_read_reg string 'regval
- (* Request to write register *)
- | e_write_reg string 'regval
- | e_undefined bool
- | e_print string
-
inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, 'e) monad) set" where
- Read_mem: "((Read_mem rk addr sz k), e_read_mem rk addr sz v, k v) \<in> T"
-| Read_tag: "((Read_tag addr k), e_read_tag addr v, k v) \<in> T"
-| Write_ea: "((Write_ea wk addr sz k), e_write_ea wk addr sz, k) \<in> T"
-| Excl_res: "((Excl_res k), e_excl_res r, k r) \<in> T"
-| Write_memv: "((Write_memv v k), e_write_memv v r, k r) \<in> T"
-| Write_tag: "((Write_tag a v k), e_write_tag a v r, k r) \<in> T"
-| Footprint: "((Footprint k), e_footprint, k) \<in> T"
-| 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"
-| Print: "((Print msg k), e_print msg, k) \<in> T"
+ Read_mem: "((Read_mem rk addr sz k), E_read_mem rk addr sz v, k v) \<in> T"
+| Read_memt: "((Read_memt rk addr sz k), E_read_memt rk addr sz v, k v) \<in> T"
+| Write_ea: "((Write_ea wk addr sz k), E_write_ea wk addr sz, k) \<in> T"
+| Excl_res: "((Excl_res k), E_excl_res r, k r) \<in> T"
+| Write_mem: "((Write_mem wk addr sz v k), E_write_mem wk addr sz v r, k r) \<in> T"
+| Write_memt: "((Write_memt wk addr sz v t k), E_write_memt wk addr sz v t r, k r) \<in> T"
+| Footprint: "((Footprint k), E_footprint, k) \<in> T"
+| 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"
+| Choose: "((Choose descr k), E_choose descr v, k v) \<in> T"
+| Print: "((Print msg k), E_print msg, k) \<in> T"
+
+lemma emitEvent_iff_T: "emitEvent m e = Some m' \<longleftrightarrow> (m, e, m') \<in> T"
+ by (cases e) (auto simp: emitEvent_def elim: T.cases intro: T.intros split: monad.splits)
inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where
Nil: "(s, [], s) \<in> Traces"
@@ -81,38 +61,68 @@ lemmas Traces_ConsI = T.intros[THEN Step, rotated]
inductive_cases Traces_NilE[elim]: "(s, [], s') \<in> Traces"
inductive_cases Traces_ConsE[elim]: "(s, e # t, s') \<in> Traces"
+lemma runTrace_iff_Traces: "runTrace t m = Some m' \<longleftrightarrow> (m, t, m') \<in> Traces"
+ by (induction t m rule: runTrace.induct; fastforce simp: bind_eq_Some_conv emitEvent_iff_T)
+
+lemma hasTrace_iff_Traces_final: "hasTrace t m \<longleftrightarrow> (\<exists>m'. (m, t, m') \<in> Traces \<and> final m')"
+ by (auto simp: hasTrace_def runTrace_iff_Traces[symmetric] split: option.splits)
+
lemma Traces_cases:
fixes m :: "('rv, 'a, 'e) monad"
assumes Run: "(m, t, m') \<in> Traces"
obtains (Nil) a where "m = m'" and "t = []"
- | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = e_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces"
- | (Read_tag) addr k t' v where "m = Read_tag addr k" and "t = e_read_tag addr v # t'" and "(k v, t', m') \<in> Traces"
- | (Write_memv) val k t' v where "m = Write_memv val k" and "t = e_write_memv val v # t'" and "(k v, t', m') \<in> Traces"
- | (Write_tag) a val k t' v where "m = Write_tag a val k" and "t = e_write_tag a val v # t'" and "(k v, t', m') \<in> Traces"
- | (Barrier) bk k t' v where "m = Barrier bk k" and "t = e_barrier bk # t'" and "(k, t', m') \<in> Traces"
- | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = e_read_reg reg v # t'" and "(k v, t', m') \<in> Traces"
- | (Excl_res) k t' v where "m = Excl_res k" and "t = e_excl_res v # t'" and "(k v, t', m') \<in> Traces"
- | (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) 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"
+ | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = E_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces"
+ | (Read_memt) rk addr s k t' v tag where "m = Read_memt rk addr s k" and "t = E_read_memt rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces"
+ | (Write_mem) wk addr sz val k v t' where "m = Write_mem wk addr sz val k" and "t = E_write_mem wk addr sz val v # t'" and "(k v, t', m') \<in> Traces"
+ | (Write_memt) wk addr sz val tag k t' v where "m = Write_memt wk addr sz val tag k" and "t = E_write_memt wk addr sz val tag v # t'" and "(k v, t', m') \<in> Traces"
+ | (Barrier) bk k t' v where "m = Barrier bk k" and "t = E_barrier bk # t'" and "(k, t', m') \<in> Traces"
+ | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = E_read_reg reg v # t'" and "(k v, t', m') \<in> Traces"
+ | (Excl_res) k t' v where "m = Excl_res k" and "t = E_excl_res v # t'" and "(k v, t', m') \<in> Traces"
+ | (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"
+ | (Choose) descr v k t' where "m = Choose descr k" and "t = E_choose descr 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
then show ?thesis by (auto intro: that(1))
next
case (Step e m'' t')
- from \<open>(m, e, m'') \<in> T\<close> and \<open>t = e # t'\<close> and \<open>(m'', t', m') \<in> Traces\<close>
- show ?thesis by (cases m e m'' rule: T.cases; elim that; blast)
+ note t = \<open>t = e # t'\<close>
+ note m' = \<open>(m'', t', m') \<in> Traces\<close>
+ from \<open>(m, e, m'') \<in> T\<close> and t and m'
+ show ?thesis proof (cases m e m'' rule: T.cases)
+ case (Read_memt rk addr sz k v)
+ then show ?thesis using t m' by (cases v; elim that; blast)
+ qed (elim that; blast)+
qed
abbreviation Run :: "('rv, 'a, 'e) monad \<Rightarrow> 'rv event list \<Rightarrow> 'a \<Rightarrow> bool"
where "Run s t a \<equiv> (s, t, Done a) \<in> Traces"
-lemma Run_appendI:
+lemma final_cases:
+ assumes "final m"
+ obtains (Done) a where "m = Done a" | (Fail) f where "m = Fail f" | (Ex) e where "m = Exception e"
+ using assms by (cases m) (auto simp: final_def)
+
+lemma hasTraces_elim:
+ assumes "hasTrace t m"
+ obtains m' where "(m, t, m') \<in> Traces" and "final m'"
+ using assms
+ unfolding hasTrace_iff_Traces_final
+ by blast
+
+lemma hasTrace_cases:
+ assumes "hasTrace t m"
+ obtains (Run) a where "Run m t a"
+ | (Fail) f where "(m, t, Fail f) \<in> Traces"
+ | (Ex) e where "(m, t, Exception e) \<in> Traces"
+ using assms by (elim hasTraces_elim final_cases) auto
+
+lemma Traces_appendI:
assumes "(s, t1, s') \<in> Traces"
- and "Run s' t2 a"
- shows "Run s (t1 @ t2) a"
+ and "(s', t2, s'') \<in> Traces"
+ shows "(s, t1 @ t2, s'') \<in> Traces"
proof (use assms in \<open>induction t1 arbitrary: s\<close>)
case (Cons e t1)
then show ?case by (elim Traces_ConsE) auto
@@ -125,20 +135,188 @@ lemma bind_DoneE:
lemma bind_T_cases:
assumes "(bind m f, e, s') \<in> T"
- obtains (Done) a where "m = Done a"
+ obtains (Done) a where "m = Done a" and "(f a, e, s') \<in> T"
| (Bind) m' where "s' = bind m' f" and "(m, e, m') \<in> T"
- using assms by (cases; blast elim: bind.elims)
+ using assms by (cases; fastforce elim: bind.elims)
-lemma Run_bindI:
+lemma Traces_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"
+ and "(f a1, t2, m') \<in> Traces"
+ shows "(m \<bind> f, t1 @ t2, m') \<in> Traces"
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_DoneE:
+ assumes "Run (Done a) t a'"
+ obtains "t = []" and "a' = a"
+ using assms by (auto elim: Traces.cases T.cases)
+
+lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a"
+ by (auto elim: Run_DoneE)
+
+lemma Run_Nil_iff_Done: "Run m [] a \<longleftrightarrow> m = Done a"
+ by auto
+
+lemma Traces_Nil_iff: "(m, [], m') \<in> Traces \<longleftrightarrow> m' = m"
+ by auto
+
+lemma bind_Traces_cases:
+ assumes "(m \<bind> f, t, m') \<in> Traces"
+ obtains (Left) m'' where "(m, t, m'') \<in> Traces" and "m' = m'' \<bind> f"
+ | (Bind) tm am tf where "t = tm @ tf" and "Run m tm am" and "(f am, tf, m') \<in> Traces"
+proof (use assms in \<open>induction "bind m f" t m' arbitrary: m rule: Traces.induct\<close>)
+ case Nil
+ then show ?case by (auto simp: Traces_Nil_iff)
+next
+ case (Step e s'' t s')
+ note IH = Step(3)
+ note Left' = Step(4)
+ note Bind' = Step(5)
+ show thesis
+ proof (use \<open>(m \<bind> f, e, s'') \<in> T\<close> in \<open>cases rule: bind_T_cases\<close>)
+ case (Done a)
+ then show ?thesis using \<open>(s'', t, s') \<in> Traces\<close> Step(5)[of "[]" "e # t" a] by auto
+ next
+ case (Bind m')
+ show ?thesis
+ proof (rule IH)
+ show "s'' = m' \<bind> f" using Bind by blast
+ next
+ fix m''
+ assume "(m', t, m'') \<in> Traces" and "s' = m'' \<bind> f"
+ then show thesis using \<open>(m, e, m') \<in> T\<close> Left'[of m''] by auto
+ next
+ fix tm tf am
+ assume "t = tm @ tf" and "Run m' tm am" and "(f am, tf, s') \<in> Traces"
+ then show thesis using \<open>(m, e, m') \<in> T\<close> Bind'[of "e # tm" tf am] by auto
+ qed
+ qed
+qed
+
+lemma final_bind_cases:
+ assumes "final (m \<bind> f)"
+ obtains (Done) a where "m = Done a" and "final (f a)"
+ | (Fail) msg where "m = Fail msg"
+ | (Ex) e where "m = Exception e"
+ using assms by (cases m) (auto simp: final_def)
+
+lemma hasFailure_iff_Traces_Fail: "hasFailure t m \<longleftrightarrow> (\<exists>msg. (m, t, Fail msg) \<in> Traces)"
+ by (auto simp: hasFailure_def runTrace_iff_Traces[symmetric] split: option.splits monad.splits)
+
+lemma hasException_iff_Traces_Exception: "hasException t m \<longleftrightarrow> (\<exists>e. (m, t, Exception e) \<in> Traces)"
+ by (auto simp: hasException_def runTrace_iff_Traces[symmetric] split: option.splits monad.splits)
+
+lemma hasTrace_bind_cases:
+ assumes "hasTrace t (m \<bind> f)"
+ obtains (Bind) tm am tf where "t = tm @ tf" and "Run m tm am" and "hasTrace tf (f am)"
+ | (Fail) "hasFailure t m"
+ | (Ex) "hasException t m"
+proof -
+ from assms obtain m' where t: "(m \<bind> f, t, m') \<in> Traces" and m': "final m'"
+ by (auto simp: hasTrace_iff_Traces_final)
+ note [simp] = hasTrace_iff_Traces_final hasFailure_iff_Traces_Fail hasException_iff_Traces_Exception
+ from t show thesis
+ proof (cases rule: bind_Traces_cases)
+ case (Left m'')
+ then show ?thesis
+ using m' Fail Ex Bind[of t "[]"]
+ by (fastforce elim!: final_bind_cases)
+ next
+ case (Bind tm am tf)
+ then show ?thesis
+ using m' that
+ by fastforce
+ qed
+qed
+
+lemma try_catch_T_cases:
+ assumes "(try_catch m h, e, m') \<in> T"
+ obtains (NoEx) m'' where "(m, e, m'') \<in> T" and "m' = try_catch m'' h"
+ | (Ex) ex where "m = Exception ex" and "(h ex, e, m') \<in> T"
+ using assms
+ by (cases m) (auto elim!: T.cases)
+
+lemma try_catch_Traces_cases:
+ assumes "(try_catch m h, t, mtc) \<in> Traces"
+ obtains (NoEx) m' where "(m, t, m') \<in> Traces" and "mtc = try_catch m' h"
+ | (Ex) tm ex th where "(m, tm, Exception ex) \<in> Traces" and "(h ex, th, mtc) \<in> Traces" and "t = tm @ th"
+proof (use assms in \<open>induction "try_catch m h" t mtc arbitrary: m rule: Traces.induct\<close>)
+ case Nil
+ then show ?case by auto
+next
+ case (Step e mtc' t mtc)
+ note e = \<open>(try_catch m h, e, mtc') \<in> T\<close>
+ note t = \<open>(mtc', t, mtc) \<in> Traces\<close>
+ note IH = Step(3)
+ note NoEx_ConsE = Step(4)
+ note Ex_ConsE = Step(5)
+ show ?case
+ proof (use e in \<open>cases rule: try_catch_T_cases\<close>)
+ case (NoEx m1)
+ show ?thesis
+ proof (rule IH)
+ show "mtc' = try_catch m1 h" using NoEx by auto
+ next
+ fix m'
+ assume "(m1, t, m') \<in> Traces" and "mtc = try_catch m' h"
+ then show ?thesis
+ using NoEx NoEx_ConsE[of m']
+ by auto
+ next
+ fix tm ex th
+ assume "(m1, tm, Exception ex) \<in> Traces" and "(h ex, th, mtc) \<in> Traces" and "t = tm @ th"
+ then show ?thesis
+ using NoEx Ex_ConsE[of "e # tm" ex th]
+ by auto
+ qed
+ next
+ case (Ex ex)
+ then show ?thesis
+ using t Ex_ConsE[of "[]" ex "e # t"]
+ by auto
+ qed
+qed
+
+lemma Done_Traces_iff[simp]: "(Done a, t, m') \<in> Traces \<longleftrightarrow> t = [] \<and> m' = Done a"
+ by (auto elim: Traces_cases)
+
+lemma Fail_Traces_iff[simp]: "(Fail msg, t, m') \<in> Traces \<longleftrightarrow> t = [] \<and> m' = Fail msg"
+ by (auto elim: Traces_cases)
+
+lemma Exception_Traces_iff[simp]: "(Exception e, t, m') \<in> Traces \<longleftrightarrow> t = [] \<and> m' = Exception e"
+ by (auto elim: Traces_cases)
+
+lemma Read_reg_TracesE:
+ assumes "(Read_reg r k, t, m') \<in> Traces"
+ obtains (Nil) "t = []" and "m' = Read_reg r k"
+ | (Cons) v t' where "t = E_read_reg r v # t'" and "(k v, t', m') \<in> Traces"
+ using assms
+ by (auto elim: Traces_cases)
+
+lemma Write_reg_TracesE:
+ assumes "(Write_reg r v k, t, m') \<in> Traces"
+ obtains (Nil) "t = []" and "m' = Write_reg r v k"
+ | (Cons) t' where "t = E_write_reg r v # t'" and "(k, t', m') \<in> Traces"
+ using assms
+ by (auto elim: Traces_cases)
+
+lemma Write_ea_TracesE:
+ assumes "(Write_ea wk addr sz k, t, m') \<in> Traces"
+ obtains (Nil) "t = []" and "m' = Write_ea wk addr sz k"
+ | (Cons) t' where "t = E_write_ea wk addr sz # t'" and "(k, t', m') \<in> Traces"
+ using assms
+ by (auto elim: Traces_cases)
+
+lemma Write_memt_TracesE:
+ assumes "(Write_memt wk addr sz v tag k, t, m') \<in> Traces"
+ obtains (Nil) "t = []" and "m' = Write_memt wk addr sz v tag k"
+ | (Cons) t' r where "t = E_write_memt wk addr sz v tag r # t'" and "(k r, t', m') \<in> Traces"
+ using assms
+ by (auto elim: Traces_cases)
+
lemma Run_bindE:
fixes m :: "('rv, 'b, 'e) monad" and a :: 'a
assumes "Run (bind m f) t a"
@@ -163,14 +341,6 @@ next
qed
qed
-lemma Run_DoneE:
- assumes "Run (Done a) t a'"
- obtains "t = []" and "a' = a"
- using assms by (auto elim: Traces.cases T.cases)
-
-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"
@@ -205,8 +375,10 @@ lemma bind_cong[fundef_cong]:
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 try_catch_choose_bool[simp]: "try_catch (choose_bool descr) h = choose_bool descr" by (auto simp: choose_bool_def)
+lemma liftR_choose_bool[simp]: "liftR (choose_bool descr) = choose_bool descr" by (auto simp: choose_bool_def liftR_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 liftR_undefined_bool[simp]: "liftR (undefined_bool ()) = undefined_bool ()" by (auto simp: undefined_bool_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 ba69d0d8..8b189f7a 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -2,6 +2,8 @@ theory Sail2_state_lemmas
imports Sail2_state Sail2_state_lifting
begin
+text \<open>Monad lifting\<close>
+
lemma All_liftState_dom: "liftState_dom (r, m)"
by (induction m) (auto intro: liftState.domintros)
termination liftState using All_liftState_dom by auto
@@ -18,7 +20,7 @@ lemma Value_liftState_Run:
assumes "(Value a, s') \<in> liftState r m s"
obtains t where "Run m t a"
by (use assms in \<open>induction r m arbitrary: s s' rule: liftState.induct\<close>;
- auto simp add: failS_def throwS_def returnS_def simp del: read_regvalS.simps;
+ simp add: failS_def throwS_def returnS_def del: read_regvalS.simps;
blast elim: Value_bindS_elim)
lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra]
@@ -43,6 +45,9 @@ lemma liftState_barrier[liftState_simp]: "liftState r (barrier bk) = returnS ()"
by (auto simp: barrier_def)
lemma liftState_footprint[liftState_simp]: "liftState r (footprint ()) = returnS ()"
by (auto simp: footprint_def)
+lemma liftState_choose_bool[liftState_simp]: "liftState r (choose_bool descr) = choose_boolS ()"
+ by (auto simp: choose_bool_def liftState_simp)
+declare undefined_boolS_def[simp]
lemma liftState_undefined[liftState_simp]: "liftState r (undefined_bool ()) = undefined_boolS ()"
by (auto simp: undefined_bool_def liftState_simp)
lemma liftState_maybe_fail[liftState_simp]: "liftState r (maybe_fail msg x) = maybe_failS msg x"
@@ -78,30 +83,44 @@ 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"
- using assms
- by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def liftState_simp split: option.splits)
+lemma liftState_read_memt[liftState_simp]:
+ shows "liftState r (read_memt BCa BCb rk a sz) = read_memtS BCa BCb rk a sz"
+ by (auto simp: read_memt_def read_memt_bytes_def maybe_failS_def read_memtS_def
+ prod.case_distrib option.case_distrib[where h = "liftState r"]
+ option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp
+ split: option.splits intro: bindS_cong)
lemma liftState_read_mem[liftState_simp]:
- "\<And>a. liftState r (read_mem BC_mword BC_mword rk a sz) = read_memS BC_mword BC_mword rk a sz"
- "\<And>a. liftState r (read_mem BC_bitU_list BC_bitU_list rk a sz) = read_memS BC_bitU_list BC_bitU_list rk a sz"
- by (auto simp: liftState_read_mem_BC)
+ shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz"
+ by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def
+ read_memtS_def
+ prod.case_distrib option.case_distrib[where h = "liftState r"]
+ option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp
+ split: option.splits intro: bindS_cong)
lemma liftState_write_mem_ea_BC:
- assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
- shows "liftState r (write_mem_ea BCa rk a sz) = write_mem_eaS BCa rk a (nat sz)"
- using assms by (auto simp: write_mem_ea_def write_mem_eaS_def)
+ assumes "unsigned_method BCa a = Some a'"
+ shows "liftState r (write_mem_ea BCa rk a sz) = returnS ()"
+ using assms by (auto simp: write_mem_ea_def nat_of_bv_def maybe_fail_def)
-lemma liftState_write_mem_ea[liftState_simp]:
- "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = write_mem_eaS BC_mword rk a (nat sz)"
- "\<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_ea[liftState_simp]:
+ "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = returnS ()"
+ "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = returnS ()"
+ by (auto simp: liftState_write_mem_ea_BC)*)
-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)
+(*lemma write_mem_bytesS_def_BC_bitU_list_BC_mword[simp]:
+ "write_mem_bytesS BC_bitU_list wk (bits_of_method BC_mword addr) sz v t =
+ write_mem_bytesS BC_mword wk addr sz v t"
+ by (auto simp: write_mem_bytesS_def)*)
+
+lemma liftState_write_memt[liftState_simp]:
+ "liftState r (write_memt BCa BCv wk addr sz v t) = write_memtS BCa BCv wk addr sz v t"
+ by (auto simp: write_memt_def write_memtS_def liftState_simp split: option.splits)
+
+lemma liftState_write_mem[liftState_simp]:
+ "liftState r (write_mem BCa BCv wk addr sz v) = write_memS BCa BCv wk addr sz v"
+ by (auto simp: write_mem_def write_memS_def write_memtS_def write_mem_bytesS_def liftState_simp
+ split: option.splits)
lemma liftState_read_reg_readS:
assumes "\<And>s. Option.bind (get_regval' (name reg) s) (of_regval reg) = Some (read_from reg s)"
@@ -138,6 +157,14 @@ 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_genlistM[liftState_simp]:
+ "liftState r (genlistM f n) = genlistS (liftState r \<circ> f) n"
+ by (auto simp: genlistM_def genlistS_def liftState_simp cong: bindS_cong)
+
+lemma liftState_choose_bools[liftState_simp]:
+ "liftState r (choose_bools descr n) = choose_boolsS n"
+ by (auto simp: choose_bools_def choose_boolsS_def liftState_simp comp_def)
+
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
@@ -146,6 +173,7 @@ lemma liftState_bools_of_bits_nondet[liftState_simp]:
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
+ chooseM_def
option.case_distrib[where h = "liftState r"]
simp del: repeat.simps
cong: option.case_cong)
@@ -301,7 +329,7 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState
qed auto
qed
-(* Simplification rules for monadic Boolean connectives *)
+text \<open>Simplification rules for monadic Boolean connectives\<close>
lemma if_return_return[simp]: "(if a then return True else return False) = return a" by auto
@@ -384,4 +412,125 @@ lemma Run_and_boolM_E:
lemma maybe_failS_Some[simp]: "maybe_failS msg (Some v) = returnS v"
by (auto simp: maybe_failS_def)
+text \<open>Event traces\<close>
+
+lemma Some_eq_bind_conv: "Some x = Option.bind f g \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)"
+ unfolding bind_eq_Some_conv[symmetric] by auto
+
+lemma if_then_Some_eq_Some_iff: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)"
+ by auto
+
+lemma Some_eq_if_then_Some_iff: "(Some y = (if b then Some x else None)) \<longleftrightarrow> (b \<and> y = x)"
+ by auto
+
+lemma emitEventS_update_cases:
+ assumes "emitEventS ra e s = Some s'"
+ obtains
+ (Write_mem) wk addr sz v tag r
+ where "e = E_write_memt wk addr sz v tag r \<or> (e = E_write_mem wk addr sz v r \<and> tag = B0)"
+ and "s' = put_mem_bytes addr sz v tag s"
+ | (Write_reg) r v rs'
+ where "e = E_write_reg r v" and "(snd ra) r v (regstate s) = Some rs'"
+ and "s' = s\<lparr>regstate := rs'\<rparr>"
+ | (Read) "s' = s"
+ using assms
+ by (elim emitEventS.elims)
+ (auto simp: Some_eq_bind_conv bind_eq_Some_conv if_then_Some_eq_Some_iff Some_eq_if_then_Some_iff)
+
+lemma runTraceS_singleton[simp]: "runTraceS ra [e] s = emitEventS ra e s"
+ by (cases "emitEventS ra e s"; auto)
+
+lemma runTraceS_ConsE:
+ assumes "runTraceS ra (e # t) s = Some s'"
+ obtains s'' where "emitEventS ra e s = Some s''" and "runTraceS ra t s'' = Some s'"
+ using assms by (auto simp: bind_eq_Some_conv)
+
+lemma runTraceS_ConsI:
+ assumes "emitEventS ra e s = Some s'" and "runTraceS ra t s' = Some s''"
+ shows "runTraceS ra (e # t) s = Some s''"
+ using assms by auto
+
+lemma runTraceS_Cons_tl:
+ assumes "emitEventS ra e s = Some s'"
+ shows "runTraceS ra (e # t) s = runTraceS ra t s'"
+ using assms by (elim emitEventS.elims) (auto simp: Some_eq_bind_conv bind_eq_Some_conv)
+
+lemma runTraceS_appendE:
+ assumes "runTraceS ra (t @ t') s = Some s'"
+ obtains s'' where "runTraceS ra t s = Some s''" and "runTraceS ra t' s'' = Some s'"
+proof -
+ have "\<exists>s''. runTraceS ra t s = Some s'' \<and> runTraceS ra t' s'' = Some s'"
+ proof (use assms in \<open>induction t arbitrary: s\<close>)
+ case (Cons e t)
+ from Cons.prems
+ obtain s_e where "emitEventS ra e s = Some s_e" and "runTraceS ra (t @ t') s_e = Some s'"
+ by (auto elim: runTraceS_ConsE simp: bind_eq_Some_conv)
+ with Cons.IH[of s_e] show ?case by (auto intro: runTraceS_ConsI)
+ qed auto
+ then show ?thesis using that by blast
+qed
+
+lemma runTraceS_nth_split:
+ assumes "runTraceS ra t s = Some s'" and n: "n < length t"
+ obtains s1 s2 where "runTraceS ra (take n t) s = Some s1"
+ and "emitEventS ra (t ! n) s1 = Some s2"
+ and "runTraceS ra (drop (Suc n) t) s2 = Some s'"
+proof -
+ have "runTraceS ra (take n t @ t ! n # drop (Suc n) t) s = Some s'"
+ using assms
+ by (auto simp: id_take_nth_drop[OF n, symmetric])
+ then show thesis by (blast elim: runTraceS_appendE runTraceS_ConsE intro: that)
+qed
+
+text \<open>Memory accesses\<close>
+
+lemma get_mem_bytes_put_mem_bytes_same_addr:
+ assumes "length v = sz"
+ shows "get_mem_bytes addr sz (put_mem_bytes addr sz v tag s) = Some (v, if sz > 0 then tag else B1)"
+proof (unfold assms[symmetric], induction v rule: rev_induct)
+ case Nil
+ then show ?case by (auto simp: get_mem_bytes_def)
+next
+ case (snoc x xs)
+ then show ?case
+ by (cases tag)
+ (auto simp: get_mem_bytes_def put_mem_bytes_def Let_def and_bit_eq_iff foldl_and_bit_eq_iff
+ cong: option.case_cong split: if_splits option.splits)
+qed
+
+lemma memstate_put_mem_bytes:
+ assumes "length v = sz"
+ shows "memstate (put_mem_bytes addr sz v tag s) addr' =
+ (if addr' \<in> {addr..<addr+sz} then Some (v ! (addr' - addr)) else memstate s addr')"
+ unfolding assms[symmetric]
+ by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def)
+
+lemma tagstate_put_mem_bytes:
+ assumes "length v = sz"
+ shows "tagstate (put_mem_bytes addr sz v tag s) addr' =
+ (if addr' \<in> {addr..<addr+sz} then Some tag else tagstate s addr')"
+ unfolding assms[symmetric]
+ by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def)
+
+lemma get_mem_bytes_cong:
+ assumes "\<forall>addr'. addr \<le> addr' \<and> addr' < addr + sz \<longrightarrow>
+ (memstate s' addr' = memstate s addr' \<and> tagstate s' addr' = tagstate s addr')"
+ shows "get_mem_bytes addr sz s' = get_mem_bytes addr sz s"
+proof (use assms in \<open>induction sz\<close>)
+ case 0
+ then show ?case by (auto simp: get_mem_bytes_def)
+next
+ case (Suc sz)
+ then show ?case
+ by (auto simp: get_mem_bytes_def Let_def
+ intro!: map_option_cong map_cong foldl_cong
+ arg_cong[where f = just_list] arg_cong2[where f = and_bit])
+qed
+
+lemma get_mem_bytes_tagged_tagstate:
+ assumes "get_mem_bytes addr sz s = Some (v, B1)"
+ shows "\<forall>addr' \<in> {addr..<addr + sz}. tagstate s addr' = Some B1"
+ using assms
+ by (auto simp: get_mem_bytes_def foldl_and_bit_eq_iff Let_def split: option.splits)
+
end
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index 3a286c10..1e9f50cc 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -38,10 +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)"
+lemma bindS_chooseS_returnS[simp]: "bindS (chooseS xs) (\<lambda>x. returnS (f x)) = chooseS (map f xs)"
by (intro ext) (auto simp: bindS_def chooseS_def returnS_def)
-
lemma result_cases:
fixes r :: "('a, 'e) result"
obtains (Value) a where "r = Value a"
@@ -198,31 +197,37 @@ lemma no_throw_basic_builtins[simp]:
"\<And>f. ignore_throw (readS f) = readS f"
"\<And>f. ignore_throw (updateS f) = updateS f"
"ignore_throw (chooseS xs) = chooseS xs"
+ "ignore_throw (choose_boolS ()) = choose_boolS ()"
"ignore_throw (failS msg) = failS msg"
"ignore_throw (maybe_failS msg x) = maybe_failS msg x"
- unfolding ignore_throw_def returnS_def chooseS_def maybe_failS_def failS_def readS_def updateS_def
+ unfolding ignore_throw_def returnS_def chooseS_def maybe_failS_def failS_def readS_def updateS_def choose_boolS_def
by (intro ext; auto split: option.splits)+
lemmas ignore_throw_option_case_distrib =
option.case_distrib[where h = "\<lambda>c. ignore_throw c s" and option = "c s" for c s]
+ option.case_distrib[where h = "\<lambda>c. ignore_throw c" and option = "c" for c]
+
+lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in ignore_throw (f x))"
+ by auto
lemma no_throw_mem_builtins:
- "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s"
+ "\<And>rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s"
+ "\<And>rk a sz s. ignore_throw (read_memt_bytesS rk a sz) s = read_memt_bytesS rk a sz s"
"\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s"
- "\<And>BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s"
- "\<And>v s. ignore_throw (write_mem_bytesS v) s = write_mem_bytesS v s"
- "\<And>BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s"
- "\<And>BC a t s. ignore_throw (write_tagS BC a t) s = write_tagS BC a t s"
+ "\<And>BCa BCv rk a sz s. ignore_throw (read_memS BCa BCv rk a sz) s = read_memS BCa BCv rk a sz s"
+ "\<And>BCa BCv rk a sz s. ignore_throw (read_memtS BCa BCv rk a sz) s = read_memtS BCa BCv rk a sz s"
+ "\<And>BC wk addr sz v s. ignore_throw (write_mem_bytesS wk addr sz v) s = write_mem_bytesS wk addr sz v s"
+ "\<And>BC wk addr sz v t s. ignore_throw (write_memt_bytesS wk addr sz v t) s = write_memt_bytesS wk addr sz v t s"
+ "\<And>BCa BCv wk addr sz v s. ignore_throw (write_memS BCa BCv wk addr sz v) s = write_memS BCa BCv wk addr sz v s"
+ "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memtS BCa BCv wk addr sz v t) s = write_memtS BCa BCv wk addr sz v t s"
"\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s"
"\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s"
- unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def
- unfolding write_mem_valS_def write_mem_bytesS_def write_tagS_def
- unfolding excl_resultS_def undefined_boolS_def
+ unfolding read_mem_bytesS_def read_memt_bytesS_def read_memtS_def read_memS_def read_tagS_def
+ unfolding write_memS_def write_memtS_def write_mem_bytesS_def write_memt_bytesS_def
+ unfolding excl_resultS_def undefined_boolS_def maybe_failS_def
+ unfolding ignore_throw_bindS
by (auto cong: bindS_cong bindS_ext_cong ignore_throw_cong option.case_cong
- simp: option.case_distrib prod.case_distrib ignore_throw_option_case_distrib comp_def)
-
-lemma no_throw_read_memS: "ignore_throw (read_memS BCa BCb rk a sz) s = read_memS BCa BCb rk a sz s"
- by (auto simp: read_memS_def no_throw_mem_builtins cong: bindS_ext_cong)
+ simp: prod.case_distrib ignore_throw_option_case_distrib ignore_throw_let_distrib comp_def)
lemma no_throw_read_regvalS: "ignore_throw (read_regvalS r reg_name) s = read_regvalS r reg_name s"
by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong)
@@ -231,7 +236,7 @@ lemma no_throw_write_regvalS: "ignore_throw (write_regvalS r reg_name v) s = wri
by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong)
lemmas no_throw_builtins[simp] =
- no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS
+ no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS
(* end *)
diff --git a/lib/isabelle/Sail2_values_lemmas.thy b/lib/isabelle/Sail2_values_lemmas.thy
index 576cd8ea..27a6952f 100644
--- a/lib/isabelle/Sail2_values_lemmas.thy
+++ b/lib/isabelle/Sail2_values_lemmas.thy
@@ -123,6 +123,9 @@ lemma nth_upto[simp]: "i + int n \<le> j \<Longrightarrow> [i..j] ! n = i + int
declare index_list.simps[simp del]
+lemma genlist_add_upt[simp]: "genlist ((+) start) len = [start..<start + len]"
+ by (auto simp: genlist_def map_add_upt add.commute cong: map_cong)
+
lemma just_list_map_Some[simp]: "just_list (map Some v) = Some v" by (induction v) auto
lemma just_list_None_iff[simp]: "just_list xs = None \<longleftrightarrow> None \<in> set xs"
@@ -151,6 +154,31 @@ next
then show ?case by (auto simp: repeat.simps)
qed
+lemma and_bit_B1[simp]: "and_bit B1 b = b"
+ by (cases b) auto
+
+lemma and_bit_idem[simp]: "and_bit b b = b"
+ by (cases b) auto
+
+lemma and_bit_eq_iff:
+ "and_bit b b' = B0 \<longleftrightarrow> (b = B0 \<or> b' = B0)"
+ "and_bit b b' = BU \<longleftrightarrow> (b = BU \<or> b' = BU) \<and> b \<noteq> B0 \<and> b' \<noteq> B0"
+ "and_bit b b' = B1 \<longleftrightarrow> (b = B1 \<and> b' = B1)"
+ by (cases b; cases b'; auto)+
+
+lemma foldl_and_bit_eq_iff:
+ shows "foldl and_bit b bs = B0 \<longleftrightarrow> (b = B0 \<or> B0 \<in> set bs)" (is ?B0)
+ and "foldl and_bit b bs = B1 \<longleftrightarrow> (b = B1 \<and> set bs \<subseteq> {B1})" (is ?B1)
+ and "foldl and_bit b bs = BU \<longleftrightarrow> (b = BU \<or> BU \<in> set bs) \<and> b \<noteq> B0 \<and> B0 \<notin> set bs" (is ?BU)
+proof -
+ have "?B0 \<and> ?B1 \<and> ?BU"
+ proof (induction bs arbitrary: b)
+ case (Cons b' bs)
+ show ?case using Cons.IH by (cases b; cases b') auto
+ qed auto
+ then show ?B0 and ?B1 and ?BU by auto
+qed
+
lemma bool_of_bitU_simps[simp]:
"bool_of_bitU B0 = Some False"
"bool_of_bitU B1 = Some True"
diff --git a/src/gen_lib/sail2_prompt.lem b/src/gen_lib/sail2_prompt.lem
index e01cc051..3cde7ade 100644
--- a/src/gen_lib/sail2_prompt.lem
+++ b/src/gen_lib/sail2_prompt.lem
@@ -38,6 +38,11 @@ end
declare {isabelle} termination_argument foreachM = automatic
+val genlistM : forall 'a 'rv 'e. (nat -> monad 'rv 'a 'e) -> nat -> monad 'rv (list 'a) 'e
+let genlistM f n =
+ let indices = genlist (fun n -> n) n in
+ foreachM indices [] (fun n xs -> (f n >>= (fun x -> return (xs ++ [x]))))
+
val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
let and_boolM l r = l >>= (fun l -> if l then r else return false)
@@ -55,7 +60,7 @@ val bool_of_bitU_nondet : forall 'rv 'e. bitU -> monad 'rv bool 'e
let bool_of_bitU_nondet = function
| B0 -> return false
| B1 -> return true
- | BU -> undefined_bool ()
+ | BU -> choose_bool "bool_of_bitU"
end
val bools_of_bits_nondet : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
@@ -93,16 +98,25 @@ let rec untilM vars cond body =
cond vars >>= fun cond_val ->
if cond_val then return vars else untilM vars cond body
-val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
-let internal_pick xs =
- (* Use sufficiently many undefined bits and convert into an index into the list *)
- bools_of_bits_nondet (repeat [BU] (length_list xs)) >>= fun bs ->
+val choose_bools : forall 'rv 'e. string -> nat -> monad 'rv (list bool) 'e
+let choose_bools descr n = genlistM (fun _ -> choose_bool descr) n
+
+val choose : forall 'rv 'a 'e. string -> list 'a -> monad 'rv 'a 'e
+let choose descr xs =
+ (* Use sufficiently many nondeterministically chosen bits and convert into an
+ index into the list *)
+ choose_bools descr (List.length xs) >>= fun bs ->
let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
match index xs idx with
| Just x -> return x
- | Nothing -> Fail "internal_pick"
+ | Nothing -> Fail ("choose " ^ descr)
end
+declare {isabelle} rename function choose = chooseM
+
+val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
+let internal_pick xs = choose "internal_pick" xs
+
(*let write_two_regs r1 r2 vec =
let is_inc =
let is_inc_r1 = is_inc_of_reg r1 in
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 78b1615e..e0ac09f6 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -8,19 +8,20 @@ type address = list bitU
type monad 'regval 'a 'e =
| Done of 'a
- (* Read a number of bytes from memory, returned in little endian order *)
- | Read_mem of read_kind * address * nat * (list memory_byte -> monad 'regval 'a 'e)
- (* Read the tag of a memory address *)
- | Read_tag of address * (bitU -> monad 'regval 'a 'e)
- (* Tell the system a write is imminent, at address lifted, of size nat *)
- | Write_ea of write_kind * address * nat * monad 'regval 'a 'e
+ (* Read a number of bytes from memory, returned in little endian order,
+ with or without a tag. The first nat specifies the address, the second
+ the number of bytes. *)
+ | Read_mem of read_kind * nat * nat * (list memory_byte -> monad 'regval 'a 'e)
+ | Read_memt of read_kind * nat * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e)
+ (* Tell the system a write is imminent, at the given address and with the
+ given size. *)
+ | Write_ea of write_kind * nat * nat * monad 'regval 'a 'e
(* Request the result of store-exclusive *)
| Excl_res of (bool -> monad 'regval 'a 'e)
- (* Request to write memory at last signalled address. Memory value should be 8
- times the size given in ea signal, given in little endian order *)
- | Write_memv of list memory_byte * (bool -> monad 'regval 'a 'e)
- (* Request to write the tag at given address. *)
- | Write_tag of address * bitU * (bool -> monad 'regval 'a 'e)
+ (* Request to write a memory value of the given size at the given address,
+ with or without a tag. *)
+ | Write_mem of write_kind * nat * nat * list memory_byte * (bool -> monad 'regval 'a 'e)
+ | Write_memt of write_kind * nat * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e)
(* Tell the system to dynamically recalculate dependency footprint *)
| Footprint of monad 'regval 'a 'e
(* Request a memory barrier *)
@@ -29,8 +30,10 @@ type monad 'regval 'a 'e =
| Read_reg of register_name * ('regval -> monad 'regval 'a 'e)
(* Request to write register *)
| Write_reg of register_name * 'regval * monad 'regval 'a 'e
- (* Request to choose a Boolean, e.g. to resolve an undefined bit *)
- | Undefined of (bool -> monad 'regval 'a 'e)
+ (* Request to choose a Boolean, e.g. to resolve an undefined bit. The string
+ argument may be used to provide information to the system about what the
+ Boolean is going to be used for. *)
+ | Choose of string * (bool -> monad 'regval 'a 'e)
(* Print debugging or tracing information *)
| Print of string * monad 'regval 'a 'e
(*Result of a failed assert with possible error message to report*)
@@ -38,33 +41,52 @@ type monad 'regval 'a 'e =
(* Exception of type 'e *)
| Exception of 'e
+type event 'regval =
+ | E_read_mem of read_kind * nat * nat * list memory_byte
+ | E_read_memt of read_kind * nat * nat * (list memory_byte * bitU)
+ | E_write_mem of write_kind * nat * nat * list memory_byte * bool
+ | E_write_memt of write_kind * nat * nat * list memory_byte * bitU * bool
+ | E_write_ea of write_kind * nat * nat
+ | E_excl_res of bool
+ | E_barrier of barrier_kind
+ | E_footprint
+ | E_read_reg of register_name * 'regval
+ | E_write_reg of register_name * 'regval
+ | E_choose of string * bool
+ | E_print of string
+
+type trace 'regval = list (event 'regval)
+
val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e
let return a = Done a
val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
let rec bind m f = match m with
| Done a -> f a
- | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> bind (k v) f)
- | Read_tag a k -> Read_tag a (fun v -> bind (k v) f)
- | Write_memv descr k -> Write_memv descr (fun v -> bind (k v) f)
- | Write_tag a t k -> Write_tag a t (fun v -> bind (k v) f)
- | Read_reg descr k -> Read_reg descr (fun v -> bind (k v) f)
- | Excl_res k -> Excl_res (fun v -> bind (k v) f)
- | Undefined k -> Undefined (fun v -> bind (k v) f)
- | Write_ea wk a sz k -> Write_ea wk a sz (bind k f)
- | Footprint k -> Footprint (bind k f)
- | Barrier bk k -> Barrier bk (bind k f)
- | Write_reg r v k -> Write_reg r v (bind k f)
- | Print msg k -> Print msg (bind k f)
- | Fail descr -> Fail descr
- | Exception e -> Exception e
+ | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> bind (k v) f)
+ | Read_memt rk a sz k -> Read_memt rk a sz (fun v -> bind (k v) f)
+ | Write_mem wk a sz v k -> Write_mem wk a sz v (fun v -> bind (k v) f)
+ | Write_memt wk a sz v t k -> Write_memt wk a sz v t (fun v -> bind (k v) f)
+ | Read_reg descr k -> Read_reg descr (fun v -> bind (k v) f)
+ | Excl_res k -> Excl_res (fun v -> bind (k v) f)
+ | Choose descr k -> Choose descr (fun v -> bind (k v) f)
+ | Write_ea wk a sz k -> Write_ea wk a sz (bind k f)
+ | Footprint k -> Footprint (bind k f)
+ | Barrier bk k -> Barrier bk (bind k f)
+ | Write_reg r v k -> Write_reg r v (bind k f)
+ | Print msg k -> Print msg (bind k f)
+ | Fail descr -> Fail descr
+ | Exception e -> Exception e
end
val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e
let exit () = Fail "exit"
+val choose_bool : forall 'rv 'e. string -> monad 'rv bool 'e
+let choose_bool descr = Choose descr return
+
val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e
-let undefined_bool () = Undefined return
+let undefined_bool () = choose_bool "undefined_bool"
val assert_exp : forall 'rv 'e. bool -> string -> monad 'rv unit 'e
let assert_exp exp msg = if exp then Done () else Fail msg
@@ -74,21 +96,21 @@ let throw e = Exception e
val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv 'a 'e2
let rec try_catch m h = match m with
- | Done a -> Done a
- | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> try_catch (k v) h)
- | Read_tag a k -> Read_tag a (fun v -> try_catch (k v) h)
- | Write_memv descr k -> Write_memv descr (fun v -> try_catch (k v) h)
- | Write_tag a t k -> Write_tag a t (fun v -> try_catch (k v) h)
- | Read_reg descr k -> Read_reg descr (fun v -> try_catch (k v) h)
- | Excl_res k -> Excl_res (fun v -> try_catch (k v) h)
- | Undefined k -> Undefined (fun v -> try_catch (k v) h)
- | Write_ea wk a sz k -> Write_ea wk a sz (try_catch k h)
- | Footprint k -> Footprint (try_catch k h)
- | Barrier bk k -> Barrier bk (try_catch k h)
- | Write_reg r v k -> Write_reg r v (try_catch k h)
- | Print msg k -> Print msg (try_catch k h)
- | Fail descr -> Fail descr
- | Exception e -> h e
+ | Done a -> Done a
+ | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> try_catch (k v) h)
+ | Read_memt rk a sz k -> Read_memt rk a sz (fun v -> try_catch (k v) h)
+ | Write_mem wk a sz v k -> Write_mem wk a sz v (fun v -> try_catch (k v) h)
+ | Write_memt wk a sz v t k -> Write_memt wk a sz v t (fun v -> try_catch (k v) h)
+ | Read_reg descr k -> Read_reg descr (fun v -> try_catch (k v) h)
+ | Excl_res k -> Excl_res (fun v -> try_catch (k v) h)
+ | Choose descr k -> Choose descr (fun v -> try_catch (k v) h)
+ | Write_ea wk a sz k -> Write_ea wk a sz (try_catch k h)
+ | Footprint k -> Footprint (try_catch k h)
+ | Barrier bk k -> Barrier bk (try_catch k h)
+ | Write_reg r v k -> Write_reg r v (try_catch k h)
+ | Print msg k -> Print msg (try_catch k h)
+ | Fail descr -> Fail descr
+ | Exception e -> h e
end
(* For early return, we abuse exceptions by throwing and catching
@@ -126,19 +148,37 @@ let maybe_fail msg = function
| Nothing -> Fail msg
end
+val read_memt_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e
+let read_memt_bytes rk addr sz =
+ bind
+ (maybe_fail "nat_of_bv" (nat_of_bv addr))
+ (fun addr -> Read_memt rk addr (nat_of_int sz) return)
+
+val read_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e
+let read_memt rk addr sz =
+ bind
+ (read_memt_bytes rk addr sz)
+ (fun (bytes, tag) ->
+ match of_bits (bits_of_mem_bytes bytes) with
+ | Just v -> return (v, tag)
+ | Nothing -> Fail "bits_of_mem_bytes"
+ end)
+
val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e
let read_mem_bytes rk addr sz =
- Read_mem rk (bits_of addr) (nat_of_int sz) return
+ bind
+ (maybe_fail "nat_of_bv" (nat_of_bv addr))
+ (fun addr -> Read_mem rk addr (nat_of_int sz) return)
val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e
let read_mem rk addr sz =
bind
(read_mem_bytes rk addr sz)
(fun bytes ->
- maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)))
-
-val read_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bitU 'e
-let read_tag addr = Read_tag (bits_of addr) return
+ match of_bits (bits_of_mem_bytes bytes) with
+ | Just v -> return v
+ | Nothing -> Fail "bits_of_mem_bytes"
+ end)
val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e
let excl_result () =
@@ -146,16 +186,28 @@ let excl_result () =
Excl_res k
val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e
-let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (nat_of_int sz) (Done ())
-
-val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e
-let write_mem_val v = match mem_bytes_of_bits v with
- | Just v -> Write_memv v return
- | Nothing -> Fail "write_mem_val"
-end
-
-val write_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> bitU -> monad 'rv bool 'e
-let write_tag addr b = Write_tag (bits_of addr) b return
+let write_mem_ea wk addr sz =
+ bind
+ (maybe_fail "nat_of_bv" (nat_of_bv addr))
+ (fun addr -> Write_ea wk addr (nat_of_int sz) (Done ()))
+
+val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
+ write_kind -> 'a -> integer -> 'b -> monad 'rv bool 'e
+let write_mem wk addr sz v =
+ match (mem_bytes_of_bits v, nat_of_bv addr) with
+ | (Just v, Just addr) ->
+ Write_mem wk addr (nat_of_int sz) v return
+ | _ -> Fail "write_mem"
+ end
+
+val write_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
+ write_kind -> 'a -> integer -> 'b -> bitU -> monad 'rv bool 'e
+let write_memt wk addr sz v tag =
+ match (mem_bytes_of_bits v, nat_of_bv addr) with
+ | (Just v, Just addr) ->
+ Write_memt wk addr (nat_of_int sz) v tag return
+ | _ -> Fail "write_mem"
+ end
val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
let read_reg reg =
@@ -214,6 +266,68 @@ let barrier bk = Barrier bk (Done ())
val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e
let footprint _ = Footprint (Done ())
+(* Event traces *)
+
+val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event 'regval -> maybe (monad 'regval 'a 'e)
+let emitEvent m e = match (e, m) with
+ | (E_read_mem rk a sz v, Read_mem rk' a' sz' k) ->
+ if rk' = rk && a' = a && sz' = sz then Just (k v) else Nothing
+ | (E_read_memt rk a sz vt, Read_memt rk' a' sz' k) ->
+ if rk' = rk && a' = a && sz' = sz then Just (k vt) else Nothing
+ | (E_write_mem wk a sz v r, Write_mem wk' a' sz' v' k) ->
+ if wk' = wk && a' = a && sz' = sz && v' = v then Just (k r) else Nothing
+ | (E_write_memt wk a sz v tag r, Write_memt wk' a' sz' v' tag' k) ->
+ if wk' = wk && a' = a && sz' = sz && v' = v && tag' = tag then Just (k r) else Nothing
+ | (E_read_reg r v, Read_reg r' k) ->
+ if r' = r then Just (k v) else Nothing
+ | (E_write_reg r v, Write_reg r' v' k) ->
+ if r' = r && v' = v then Just k else Nothing
+ | (E_write_ea wk a sz, Write_ea wk' a' sz' k) ->
+ if wk' = wk && a' = a && sz' = sz then Just k else Nothing
+ | (E_barrier bk, Barrier bk' k) ->
+ if bk' = bk then Just k else Nothing
+ | (E_print m, Print m' k) ->
+ if m' = m then Just k else Nothing
+ | (E_excl_res v, Excl_res k) -> Just (k v)
+ | (E_choose descr v, Choose descr' k) -> if descr' = descr then Just (k v) else Nothing
+ | (E_footprint, Footprint k) -> Just k
+ | _ -> Nothing
+end
+
+val runTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> maybe (monad 'regval 'a 'e)
+let rec runTrace t m = match t with
+ | [] -> Just m
+ | e :: t' -> Maybe.bind (emitEvent m e) (runTrace t')
+end
+
+declare {isabelle} termination_argument runTrace = automatic
+
+val final : forall 'regval 'a 'e. monad 'regval 'a 'e -> bool
+let final = function
+ | Done _ -> true
+ | Fail _ -> true
+ | Exception _ -> true
+ | _ -> false
+end
+
+val hasTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
+let hasTrace t m = match runTrace t m with
+ | Just m -> final m
+ | Nothing -> false
+end
+
+val hasException : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
+let hasException t m = match runTrace t m with
+ | Just (Exception _) -> true
+ | _ -> false
+end
+
+val hasFailure : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
+let hasFailure t m = match runTrace t m with
+ | Just (Fail _) -> true
+ | _ -> false
+end
+
(* Define a type synonym that also takes the register state as a type parameter,
in order to make switching to the state monad without changing generated
definitions easier, see also lib/hol/prompt_monad.lem. *)
diff --git a/src/gen_lib/sail2_state.lem b/src/gen_lib/sail2_state.lem
index f703dead..ec787764 100644
--- a/src/gen_lib/sail2_state.lem
+++ b/src/gen_lib/sail2_state.lem
@@ -28,6 +28,11 @@ end
declare {isabelle} termination_argument foreachS = automatic
+val genlistS : forall 'a 'rv 'e. (nat -> monadS 'rv 'a 'e) -> nat -> monadS 'rv (list 'a) 'e
+let genlistS f n =
+ let indices = genlist (fun n -> n) n in
+ foreachS indices [] (fun n xs -> (f n >>$= (fun x -> returnS (xs ++ [x]))))
+
val and_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e
let and_boolS l r = l >>$= (fun l -> if l then r else returnS false)
@@ -84,12 +89,17 @@ let rec untilS vars cond body s =
(cond vars >>$= (fun cond_val s'' ->
if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s
+val choose_boolsS : forall 'rv 'e. nat -> monadS 'rv (list bool) 'e
+let choose_boolsS n = genlistS (fun _ -> choose_boolS ()) n
+
+(* TODO: Replace by chooseS and prove equivalence to prompt monad version *)
val internal_pickS : forall 'rv 'a 'e. list 'a -> monadS 'rv 'a 'e
let internal_pickS xs =
- (* Use sufficiently many undefined bits and convert into an index into the list *)
- bools_of_bits_nondetS (repeat [BU] (length_list xs)) >>$= fun bs ->
+ (* Use sufficiently many nondeterministically chosen bits and convert into an
+ index into the list *)
+ choose_boolsS (List.length xs) >>$= fun bs ->
let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
match index xs idx with
| Just x -> returnS x
- | Nothing -> failS "internal_pick"
+ | Nothing -> failS "choose internal_pick"
end
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index 039343e2..98a5390d 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -5,23 +5,53 @@ open import Sail2_prompt
open import Sail2_state_monad
open import {isabelle} `Sail2_state_monad_lemmas`
-(* State monad wrapper around prompt monad *)
-
+(* Lifting from prompt monad to state monad *)
val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
-let rec liftState ra s = match s with
- | (Done a) -> returnS a
- | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
- | (Read_tag t k) -> bindS (read_tagS t) (fun v -> liftState ra (k v))
- | (Write_memv a k) -> bindS (write_mem_bytesS a) (fun v -> liftState ra (k v))
- | (Write_tag a t k) -> bindS (write_tagS a t) (fun v -> liftState ra (k v))
- | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v))
- | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v))
- | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v))
- | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k)
- | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k)
- | (Footprint k) -> liftState ra k
- | (Barrier _ k) -> liftState ra k
- | (Print _ k) -> liftState ra k (* TODO *)
- | (Fail descr) -> failS descr
- | (Exception e) -> throwS e
+let rec liftState ra m = match m with
+ | (Done a) -> returnS a
+ | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
+ | (Read_memt rk a sz k) -> bindS (read_memt_bytesS rk a sz) (fun v -> liftState ra (k v))
+ | (Write_mem wk a sz v k) -> bindS (write_mem_bytesS wk a sz v) (fun v -> liftState ra (k v))
+ | (Write_memt wk a sz v t k) -> bindS (write_memt_bytesS wk a sz v t) (fun v -> liftState ra (k v))
+ | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v))
+ | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v))
+ | (Choose _ k) -> bindS (choose_boolS ()) (fun v -> liftState ra (k v))
+ | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k)
+ | (Write_ea _ _ _ k) -> liftState ra k
+ | (Footprint k) -> liftState ra k
+ | (Barrier _ k) -> liftState ra k
+ | (Print _ k) -> liftState ra k (* TODO *)
+ | (Fail descr) -> failS descr
+ | (Exception e) -> throwS e
+end
+
+val emitEventS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> event 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
+let emitEventS ra e s = match e with
+ | E_read_mem _ addr sz v ->
+ Maybe.bind (get_mem_bytes addr sz s) (fun (v', _) ->
+ if v' = v then Just s else Nothing)
+ | E_read_memt _ addr sz (v, tag) ->
+ Maybe.bind (get_mem_bytes addr sz s) (fun (v', tag') ->
+ if v' = v && tag' = tag then Just s else Nothing)
+ | E_write_mem _ addr sz v success ->
+ if success then Just (put_mem_bytes addr sz v B0 s) else Nothing
+ | E_write_memt _ addr sz v tag success ->
+ if success then Just (put_mem_bytes addr sz v tag s) else Nothing
+ | E_read_reg r v ->
+ let (read_reg, _) = ra in
+ Maybe.bind (read_reg r s.regstate) (fun v' ->
+ if v' = v then Just s else Nothing)
+ | E_write_reg r v ->
+ let (_, write_reg) = ra in
+ Maybe.bind (write_reg r v s.regstate) (fun rs' ->
+ Just <| s with regstate = rs' |>)
+ | _ -> Just s
end
+
+val runTraceS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> trace 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
+let rec runTraceS ra t s = match t with
+ | [] -> Just s
+ | e :: t' -> Maybe.bind (emitEventS ra e s) (runTraceS ra t')
+end
+
+declare {isabelle} termination_argument runTraceS = automatic
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 30b296cc..3042700c 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -4,24 +4,20 @@ open import Sail2_values
(* 'a is result type *)
-type memstate = map integer memory_byte
-type tagstate = map integer bitU
+type memstate = map nat memory_byte
+type tagstate = map nat bitU
(* type regstate = map string (vector bitU) *)
type sequential_state 'regs =
<| regstate : 'regs;
memstate : memstate;
- tagstate : tagstate;
- write_ea : maybe (write_kind * integer * integer);
- last_exclusive_operation_was_load : bool |>
+ tagstate : tagstate |>
val init_state : forall 'regs. 'regs -> sequential_state 'regs
let init_state regs =
<| regstate = regs;
memstate = Map.empty;
- tagstate = Map.empty;
- write_ea = Nothing;
- last_exclusive_operation_was_load = false |>
+ tagstate = Map.empty |>
type ex 'e =
| Failure of string
@@ -51,8 +47,8 @@ let seqS m n = bindS m (fun (_ : unit) -> n)
let inline (>>$=) = bindS
let inline (>>$) = seqS
-val chooseS : forall 'regs 'a 'e. SetType 'a => set 'a -> monadS 'regs 'a 'e
-let chooseS xs s = Set.map (fun x -> (Value x, s)) xs
+val chooseS : forall 'regs 'a 'e. SetType 'a => list 'a -> monadS 'regs 'a 'e
+let chooseS xs s = Set.fromList (List.map (fun x -> (Value x, s)) xs)
val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e
let readS f = (fun s -> returnS (f s) s)
@@ -63,8 +59,9 @@ let updateS f = (fun s -> returnS () (f s))
val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e
let failS msg s = {(Ex (Failure msg), s)}
-val undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
-let undefined_boolS () = chooseS {false; true}
+val choose_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
+let choose_boolS () = chooseS [false; true]
+let undefined_boolS = choose_boolS
val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
let exitS () = failS "exit"
@@ -120,69 +117,78 @@ end
val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e
let read_tagS addr =
- maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
+ maybe_failS "nat_of_bv" (nat_of_bv addr) >>$= (fun addr ->
readS (fun s -> fromMaybe B0 (Map.lookup addr s.tagstate)))
(* Read bytes from memory and return in little endian order *)
-val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte) 'e
-let read_mem_bytesS read_kind addr sz =
- maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
- let sz = integerFromNat sz in
- let addrs = index_list addr (addr+sz-1) 1 in
+val get_mem_bytes : forall 'regs. nat -> nat -> sequential_state 'regs -> maybe (list memory_byte * bitU)
+let get_mem_bytes addr sz s =
+ let addrs = genlist (fun n -> addr + n) sz in
let read_byte s addr = Map.lookup addr s.memstate in
- readS (fun s -> just_list (List.map (read_byte s) addrs)) >>$= (function
- | Just mem_val ->
- updateS (fun s ->
- if read_is_exclusive read_kind
- then <| s with last_exclusive_operation_was_load = true |>
- else s) >>$
- returnS mem_val
- | Nothing -> failS "read_memS"
- end))
+ let read_tag s addr = Map.findWithDefault addr B0 s.tagstate in
+ Maybe.map
+ (fun mem_val -> (mem_val, List.foldl and_bit B1 (List.map (read_tag s) addrs)))
+ (just_list (List.map (read_byte s) addrs))
+
+val read_memt_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e
+let read_memt_bytesS _ addr sz =
+ readS (get_mem_bytes addr sz) >>$=
+ maybe_failS "read_memS"
+
+val read_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte) 'e
+let read_mem_bytesS rk addr sz =
+ read_memt_bytesS rk addr sz >>$= (fun (bytes, _) ->
+ returnS bytes)
+
+val read_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e
+let read_memtS rk a sz =
+ maybe_failS "nat_of_bv" (nat_of_bv a) >>$= (fun a ->
+ read_memt_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) ->
+ maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val ->
+ returnS (mem_val, tag))))
val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e
let read_memS rk a sz =
- read_mem_bytesS rk a (nat_of_int sz) >>$= (fun bytes ->
- maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)))
+ read_memtS rk a sz >>$= (fun (bytes, _) ->
+ returnS bytes)
val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
-let excl_resultS () =
- readS (fun s -> s.last_exclusive_operation_was_load) >>$= (fun excl_load ->
- updateS (fun s -> <| s with last_exclusive_operation_was_load = false |>) >>$
- chooseS (if excl_load then {false; true} else {false}))
-
-val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> monadS 'regs unit 'e
-let write_mem_eaS write_kind addr sz =
- maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
- let sz = integerFromNat sz in
- updateS (fun s -> <| s with write_ea = Just (write_kind, addr, sz) |>))
-
-(* Write little-endian list of bytes to previously announced address *)
-val write_mem_bytesS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e
-let write_mem_bytesS v =
- readS (fun s -> s.write_ea) >>$= (function
- | Nothing -> failS "write ea has not been announced yet"
- | Just (_, addr, sz) ->
- let addrs = index_list addr (addr+sz-1) 1 in
- (*let v = external_mem_value (bits_of v) in*)
- let a_v = List.zip addrs v in
- let write_byte mem (addr, v) = Map.insert addr v mem in
- updateS (fun s ->
- <| s with memstate = List.foldl write_byte s.memstate a_v |>) >>$
- returnS true
- end)
-
-val write_mem_valS : forall 'regs 'e 'a. Bitvector 'a => 'a -> monadS 'regs bool 'e
-let write_mem_valS v = match mem_bytes_of_bits v with
- | Just v -> write_mem_bytesS v
- | Nothing -> failS "write_mem_val"
-end
-
-val write_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> bitU -> monadS 'regs bool 'e
-let write_tagS addr t =
- maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
- updateS (fun s -> <| s with tagstate = Map.insert addr t s.tagstate |>) >>$
- returnS true)
+let excl_resultS =
+ (* TODO: This used to be more deterministic, checking a flag in the state
+ whether an exclusive load has occurred before. However, this does not
+ seem very precise; it might be safer to overapproximate the possible
+ behaviours by always making a nondeterministic choice. *)
+ undefined_boolS
+
+(* Write little-endian list of bytes to given address *)
+val put_mem_bytes : forall 'regs. nat -> nat -> list memory_byte -> bitU -> sequential_state 'regs -> sequential_state 'regs
+let put_mem_bytes addr sz v tag s =
+ let addrs = genlist (fun n -> addr + n) sz in
+ let a_v = List.zip addrs v in
+ let write_byte mem (addr, v) = Map.insert addr v mem in
+ let write_tag mem addr = Map.insert addr tag mem in
+ <| s with memstate = List.foldl write_byte s.memstate a_v;
+ tagstate = List.foldl write_tag s.tagstate addrs |>
+
+val write_memt_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
+let write_memt_bytesS _ addr sz v t =
+ updateS (put_mem_bytes addr sz v t) >>$
+ returnS true
+
+val write_mem_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> monadS 'regs bool 'e
+let write_mem_bytesS wk addr sz v = write_memt_bytesS wk addr sz v B0
+
+val write_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
+ write_kind -> 'a -> integer -> 'b -> bitU -> monadS 'regs bool 'e
+let write_memtS wk addr sz v t =
+ match (nat_of_bv addr, mem_bytes_of_bits v) with
+ | (Just addr, Just v) -> write_memt_bytesS wk addr (nat_of_int sz) v t
+ | _ -> failS "write_mem"
+ end
+
+val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
+ write_kind -> 'a -> integer -> 'b -> monadS 'regs bool 'e
+let write_memS wk addr sz v = write_memtS wk addr sz v B0
val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e
let read_regS reg = readS (fun s -> reg.read_from s.regstate)
diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index 8957f0dd..fa1e8426 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -625,6 +625,9 @@ let extz_bv n v = extz_bits n (bits_of v)
val exts_bv : forall 'a. Bitvector 'a => integer -> 'a -> list bitU
let exts_bv n v = exts_bits n (bits_of v)
+val nat_of_bv : forall 'a. Bitvector 'a => 'a -> maybe nat
+let nat_of_bv v = Maybe.map nat_of_int (unsigned v)
+
val string_of_bv : forall 'a. Bitvector 'a => 'a -> string
let string_of_bv v = show_bitlist (bits_of v)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 17:54:20 +0000