Library ProofOS.Trusted.Safety
Require Import List.
Require Import Asm.Bitvector.Bitvector.
Set Implicit Arguments.
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.
Definition cstep (mstate minstr : Set)
(mexec : (minstr * int32) -> mstate -> mstate -> Prop)
mget_instr st := mexec (mget_instr st) st.
CoInductive safe (mstate : Set) (cstep : mstate -> mstate -> Prop) : mstate -> Prop :=
| safe_rule : forall st st',
cstep st st'
-> (forall st'' : mstate, cstep st st'' -> safe cstep st'')
-> safe cstep st.
Module Safety (Mac : MACHINE).
Import Mac.
Definition cstep := cstep mexec mget_instr.
Definition safe := safe cstep.
End Safety.
Index
This page has been generated by coqdoc