| Concrete semantics for particular architectures |
Require Import Asm.X86.X86.
Require Import ProofOS.Trusted.Machine.
Module Type M86_PARAM.
Parameter minitState : state -> Prop.
End M86_PARAM.
Module M86 (Param : M86_PARAM) <: MACHINE.
Definition mstate := state.
Definition minitState := Param.minitState.
Definition minstr := instr.
Definition mget_instr := get_instr.
Definition mexec := exec.
End M86.