| Verifying a machine language by compiling it to another (probably simpler) language |
Require Import List TheoryList ZArith.
Require Import Asm.Util.Specif.
Require Import Asm.Util.Tactics.
Require Import Asm.Util.ListUtil.
Require Import Asm.Util.Monad.
Require Import Asm.Bitvector.Bitvector.
Require Import ProofOS.Trusted.Safety.
Require Import ProofOS.Trusted.Machine.
Require Import ProofOS.AbsInt.Bounded.
Set Implicit Arguments.
A reduction from one machine to another |
Module Type REDUCTION.
Declare Module Conc : MACHINE.
| Concrete machine whose programs we want to verify |
Declare Module Abs : ABSTRACTION.
| An abstraction, probably over a _different_ machine |
Parameter R : Conc.mstate -> Abs.Mac.mstate -> Prop.
| Concretization relation |
Parameter cameFrom : forall (ins : Abs.Mac.minstr),
{ins' : Conc.minstr
| forall abs nextPc, Abs.Mac.mget_instr abs = (ins, nextPc)
-> forall st, R st abs -> Conc.mget_instr st = (ins', nextPc)}.
| For simplicity in verification, we want to know which instruction each abstract instruction was compiled from. |
Axiom init : forall conc, Conc.minitState conc
-> exists abs, R conc abs /\ Abs.Mac.minitState abs.
| Every concrete start state is covered by an abstract start state. |
Parameter compile : forall (insPc : Conc.minstr * int32),
{ins' : Abs.Mac.minstr
| forall conc abs,
R conc abs
-> (forall abs', Abs.Mac.mexec (ins', snd insPc) abs abs'
-> exists conc', Conc.mexec insPc conc conc')
/\ (forall conc', Conc.mexec insPc conc conc'
-> exists abs', Abs.Mac.mexec (ins', snd insPc) abs abs'
/\ R conc' abs')}.
| Translate concrete into abstract instructions that are safe in the usual progress and preservation sense. |
End REDUCTION.
Functor to build a verifier based on a reduction |
Module Make(Red : REDUCTION) : CHECKER with Module Mac := Red.Conc.
Import Red.
Module ReduceAbs <: ABSTRACTION.
Module Mac := Conc.
Definition mastate := Abs.mastate.
Definition print_mastate := Abs.print_mastate.
Definition mcontext := Abs.mcontext.
Definition mconc (ctx : mcontext) (st : Mac.mstate) (abs : mastate) :=
exists ab, Abs.mconc ctx ab abs /\ R st ab.
Definition maget_instr : forall (abs : mastate),
sig_option (fun insPc : Conc.minstr * int32 =>
forall st ctx, mconc ctx st abs
-> insPc = Conc.mget_instr st).
Definition minit : {init : list (list mastate * mastate)
| forall st, Mac.minitState st -> exists ctx, exists abs,
In (nil, abs) init /\ mconc ctx st abs}.
Definition progress (insPc : Mac.minstr * int32) (st : Mac.mstate) :=
exists st' : Mac.mstate,
Mac.mexec insPc st st'.
Definition localStep (hyps abss : list mastate)
(ctx : mcontext) (st' : Mac.mstate) (abs' : mastate) :=
((In abs' abss \/ In abs' hyps) /\ mconc ctx st' abs').
Definition callStep (hyps abss : list mastate) (ctx : mcontext)
(st' : Mac.mstate)
(abs' : mastate) (ctx' : mcontext) (hyps' : list mastate) :=
In (hyps', abs') (proj1_sig minit)
/\ AllS (fun need => exists have,
(In have abss \/ In have hyps)
/\ subsumes mconc ctx' need ctx have) hyps'
/\ mconc ctx' st' abs'.
Definition preservation (hyps : list mastate) (abs : mastate)
(insPc : Mac.minstr * int32) (abss : list mastate)
(st : Mac.mstate) (ctx : mcontext) :=
forall (st' : Mac.mstate) (Hexec : Mac.mexec insPc st st'),
exists abs', localStep hyps abss ctx st' abs'
\/ exists ctx', exists hyps', callStep hyps abss ctx st' abs' ctx' hyps'.
Definition mstep : forall hyps abs insPc, sig_option (fun abss : list mastate =>
forall st ctx, mconc ctx st abs
-> progress insPc st
/\ preservation hyps abs insPc abss st ctx).
End ReduceAbs.
Module Ch := Checker(ReduceAbs).
Definition verify := Ch.verify.
Module Mac := Red.Conc.
End Make.