1open HolKernel Parse boolLib bossLib
2open tripleTheory m0_decompTheory
3
4val () = new_theory "m0_core_decomp"
5
6val _ = Parse.hide "mem"
7
8(* definition of M0_ASSERT *)
9
10val _ = Hol_datatype`
11   m0_assertion =
12   M0_ASSERTION of bool => bool => bool => bool =>    (* n z c v      *)
13                   num =>                             (* count        *)
14                   RName set => (RName -> word32) =>  (* gp registers *)
15                   word32 set => (word32 -> word8) => (* memory       *)
16                   word32                             (* pc           *)`
17
18val M0_ASSERT_def = Define`
19   M0_ASSERT (M0_ASSERTION n z c v count dreg reg dmem mem pc) =
20     m0_PSR_N n *
21     m0_PSR_Z z *
22     m0_PSR_C c *
23     m0_PSR_V v *
24     m0_COUNT count *
25     m0_REGISTERS dreg reg *
26     m0_MEMORY dmem mem *
27     m0_PC pc`
28
29val L3_M0_def = Define `L3_M0 = (M0_ASSERT, M0_MODEL)`
30
31val () = export_theory()
32