Add Isabelle support for translation start/end outcomes

rems-project · Apr 25, 2024 · c565693 · c565693
1 parent 6a7bab4
commit c565693
Show file tree

Hide file tree

Showing 4 changed files with 187 additions and 159 deletions.
diff --git a/lib/isabelle/Sail2_concurrency_interface_lemmas.thy b/lib/isabelle/Sail2_concurrency_interface_lemmas.thy
@@ -40,6 +40,8 @@ inductive_set T (*:: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a,
 | Read_mem: "((Mem_read_request req k), E_mem_read_request req v, k v) \<in> T"
 | Write_mem: "((Mem_write_request req k), E_mem_write_request req r, k r) \<in> T"
 | Write_announce: "((Mem_write_announce_address a k), E_mem_write_announce_address a, k) \<in> T"
+| Translation_start: "((Translation_start ts k), E_translation_start ts, k) \<in> T"
+| Translation_end: "((Translation_end te k), E_translation_end te, k) \<in> T"
 | Branch_announce: "((Branch_announce_address a k), E_branch_announce_address a, k) \<in> T"
 | Barrier_request: "((Barrier_request r k), E_barrier_request r, k) \<in> T"
 | Cache_op_request: "((Cache_op_request r k), E_cache_op_request r, k) \<in> T"
@@ -62,6 +64,8 @@ lemma emitEvent_cases:
   | (Read_mem) req k v where "m = Mem_read_request req k" and "e = E_mem_read_request req v" and "m' = k v"
   | (Write_mem) req k r where "m = Mem_write_request req k" and "e = E_mem_write_request req r" and "m' = k r"
   | (Write_announce) a k where "m = Mem_write_announce_address a k" and "e = E_mem_write_announce_address a" and "m' = k"
+  | (Translation_start) ts k where "m = Translation_start ts k" and "e = E_translation_start ts" and "m' = k"
+  | (Translation_end) te k where "m = Translation_end te k" and "e = E_translation_end te" and "m' = k"
   | (Branch_announce) a k where "m = Branch_announce_address a k" and "e = E_branch_announce_address a" and "m' = k"
   | (Barrier_request) r k where "m = Barrier_request r k" and "e = E_barrier_request r" and "m' = k"
   | (Cache_op_request) r k where "m = Cache_op_request r k" and "e = E_cache_op_request r" and "m' = k"
@@ -109,6 +113,8 @@ lemma Traces_cases:
   | (Read_mem) req k t' v where "m = Mem_read_request req k" and "t = E_mem_read_request req v # t'" and "(k v, t', m') \<in> Traces"
   | (Write_mem) req k v t' where "m = Mem_write_request req k" and "t = E_mem_write_request req v # t'" and "(k v, t', m') \<in> Traces"
   | (Write_announce) a k t' where "m = Mem_write_announce_address a k" and "t = E_mem_write_announce_address a # t'" and "(k, t', m') \<in> Traces"
+  | (Translation_start) ts k t' where "m = Translation_start ts k" and "t = E_translation_start ts # t'" and "(k, t', m') \<in> Traces"
+  | (Translation_end) te k t' where "m = Translation_end te k" and "t = E_translation_end te # t'" and "(k, t', m') \<in> Traces"
   | (Branch_announce) a k t' where "m = Branch_announce_address a k" and "t = E_branch_announce_address a # t'" and "(k, t', m') \<in> Traces"
   | (Barrier) r k t' where "m = Barrier_request r k" and "t = E_barrier_request r # t'" and "(k, t', m') \<in> Traces"
   | (Cache_op) r k t' where "m = Cache_op_request r k" and "t = E_cache_op_request r # t'" and "(k, t', m') \<in> Traces"
@@ -134,6 +140,8 @@ lemma Traces_iffs:
   "\<And>req k t m'. (Mem_read_request req k, t, m') \<in> Traces \<longleftrightarrow> (t = [] \<and> m' = Mem_read_request req k \<or> (\<exists>a t'. t = E_mem_read_request req a # t' \<and> (k a, t', m') \<in> Traces))"
   "\<And>req k t m'. (Mem_write_request req k, t, m') \<in> Traces \<longleftrightarrow> (t = [] \<and> m' = Mem_write_request req k \<or> (\<exists>a t'. t = E_mem_write_request req a # t' \<and> (k a, t', m') \<in> Traces))"
   "\<And>a k t m'. (Mem_write_announce_address a k, t, m') \<in> Traces \<longleftrightarrow> (t = [] \<and> m' = Mem_write_announce_address a k \<or> (\<exists>t'. t = E_mem_write_announce_address a # t' \<and> (k, t', m') \<in> Traces))"
+  "\<And>ts k t m'. (Translation_start ts k, t, m') \<in> Traces \<longleftrightarrow> (t = [] \<and> m' = Translation_start ts k \<or> (\<exists>t'. t = E_translation_start ts # t' \<and> (k, t', m') \<in> Traces))"
+  "\<And>te k t m'. (Translation_end te k, t, m') \<in> Traces \<longleftrightarrow> (t = [] \<and> m' = Translation_end te k \<or> (\<exists>t'. t = E_translation_end te # t' \<and> (k, t', m') \<in> Traces))"
   "\<And>a k t m'. (Branch_announce_address a k, t, m') \<in> Traces \<longleftrightarrow> (t = [] \<and> m' = Branch_announce_address a k \<or> (\<exists>t'. t = E_branch_announce_address a # t' \<and> (k, t', m') \<in> Traces))"
   "\<And>req k t m'. (Barrier_request req k, t, m') \<in> Traces \<longleftrightarrow> (t = [] \<and> m' = Barrier_request req k \<or> (\<exists>t'. t = E_barrier_request req # t' \<and> (k, t', m') \<in> Traces))"
   "\<And>req k t m'. (Cache_op_request req k, t, m') \<in> Traces \<longleftrightarrow> (t = [] \<and> m' = Cache_op_request req k \<or> (\<exists>t'. t = E_cache_op_request req # t' \<and> (k, t', m') \<in> Traces))"