Library ProofOS.Trusted.Safety

Abstract machine 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