| Basic definitions about machine semantics |
Require Import Asm.Bitvector.Bitvector.
| A concrete machine semantics |
Module Type MACHINE.
Parameter mstate : Set.
Parameter minitState : mstate -> Prop.
Parameter minstr : Set.
Parameter mget_instr : mstate -> minstr * int32.
Parameter mexec : (minstr * int32) -> mstate -> mstate -> Prop.
End MACHINE.