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