| Building abstractions that depend on a fixed code segment |
Require Import Arith List TheoryList.
Require Import Asm.Util.Specif.
Require Import Asm.Util.Tactics.
Require Import Asm.Util.ListUtil.
Require Import Asm.Util.ArithUtil.
Require Import Asm.Util.Monad.
Require Import Asm.Bitvector.Bitvector.
Require Import Asm.X86.X86.
Require Import ProofOS.Trusted.Safety.
Require Import ProofOS.Trusted.Machine.
Require Import ProofOS.Trusted.Arches.
Require Import ProofOS.AbsInt.Bounded.
Require Import ProofOS.AbsInt.Sal.
Lemma apart_or : forall a a',
bvec_to_nat a' + 4 <= bvec_to_nat a
\/ bvec_to_nat a' >= bvec_to_nat a + 4
-> apart a a'.
Module Type M86_PARAM_FIXED_CODE.
Parameter minitState : state -> Prop.
Parameter minitMem : mem.
Parameter codeStart : int32.
Parameter codeLength : nat.
Axiom codeHigh : bvec_to_nat codeStart >= 4.
Axiom codeFits : bvec_to_nat codeStart + codeLength < pow2 32 - 3.
Axiom pcInRange : forall st, minitState st
-> bvec_to_nat codeStart
<= bvec_to_nat (stPc st)
< bvec_to_nat codeStart + codeLength - longestInstr.
Axiom codeUniform : forall st, minitState st
-> agree_range (stMem st) minitMem codeStart codeLength.
End M86_PARAM_FIXED_CODE.
Module Make (Param : M86_PARAM_FIXED_CODE).
Import Param.
Module MySal := Sal.Make(Param).
Import MySal.
Definition validPc (pc : int32) :=
bvec_to_nat codeStart
<= bvec_to_nat pc
< bvec_to_nat codeStart + codeLength - longestInstr.
Definition apartFromCode (pc : int32) :=
(bvec_to_nat pc <= bvec_to_nat codeStart - 4
\/ bvec_to_nat pc >= bvec_to_nat codeStart + codeLength + 4).
Does an instruction avoid writing over code memory? |
Definition cmdOk st cmd :=
match cmd with
| SStore dst src => apartFromCode (evalExp st dst)
/\ not_too_high (evalExp st dst)
| _ => True
end.
Fixpoint cmdsOk (st : salState) (cmds : list salCmd) {struct cmds} : Prop :=
match cmds with
| nil => True
| cons cmd cmds => cmdOk st cmd /\ cmdsOk (salExecCmd st cmd) cmds
end.
Definition instrOk st (ins : salInstr) := cmdsOk st (fst ins).
Definition instructionOk st (ins : salInstruction) := instrOk st (snd ins).
Lemma agree_range_refl : forall a low lim,
agree_range a a low lim.
Hint Resolve agree_range_refl.
Lemma agree_range_trans : forall a1 a2 a3 low lim,
agree_range a1 a2 low lim
-> agree_range a2 a3 low lim
-> agree_range a1 a3 low lim.
Lemma cmdOk_sound : forall st cmd,
cmdOk st cmd
-> agree_range (SstMem (salExecCmd st cmd)) (SstMem st) codeStart codeLength.
Lemma jmpMem : forall jmp pc st st',
salExecJmp jmp pc st = Some st'
-> SstMem st = SstMem st'.
Lemma cmdsOk_sound : forall cmds st st',
cmdsOk st' cmds ->
agree_range (SstMem st')
(SstMem st) codeStart codeLength
-> agree_range (SstMem (fold_left salExecCmd cmds st'))
(SstMem st) codeStart codeLength.
Theorem instructionsOk_sound : forall st insPc st',
instructionOk st (fst insPc)
-> M.mexec insPc st st'
-> agree_range (SstMem st') (SstMem st) codeStart codeLength.
An abstraction of a concrete machine whose code segment is never touched |
Module Type FIXED_CODE_ABSTRACTION.
Declare Module Mac := M.
Parameter mastate : Set.
Parameter print_mastate : mastate -> unit.
Parameter mcontext : Set.
Parameter mconc : mcontext -> Mac.mstate -> mastate -> Prop.
Parameter maPc : forall (abs : mastate), sig_option (fun pc =>
forall ctx st, mconc ctx st abs -> SstPc st = pc).
Definition absValidPc abs :=
match maPc abs with
| SNone => True
| SSome pc _ => validPc pc
end.
Parameter minit : {init : list (list mastate * mastate)
| (forall abs hyps, In (hyps, abs) init -> absValidPc abs)
/\ 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) :=
instructionOk st (fst insPc)
/\ 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'.
Parameter 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 FIXED_CODE_ABSTRACTION.
Module Fix (Abs : FIXED_CODE_ABSTRACTION) : ABSTRACTION with Module Mac := M.
Module Mac := M.
Import Abs.
Definition mastate := mastate.
Definition print_mastate := print_mastate.
Definition mcontext := mcontext.
Definition absValidPc abs :=
match maPc abs with
| SNone => True
| SSome pc _ => validPc pc
end.
Record _mconc (ctx : mcontext) (st : Mac.mstate) (abs : mastate) : Prop := {
mcPc : absValidPc abs;
mcCode : agree_range (SstMem st) minitMem codeStart codeLength;
mcCust : mconc ctx st abs
}.
Definition get_instr pc :=
let (ins, pc) := decode_instr minitMem pc in
((ins, salCompile (ins, pc)), pc).
Definition maget_instr : forall (abs : mastate),
sig_option (fun insPc : Mac.minstr * int32 =>
forall st ctx, _mconc ctx st abs
-> insPc = Mac.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}.
On to the home stretch |
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 absValidPc_dec : forall (abs : mastate), pred_option (absValidPc abs).
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).
Definition mconc := _mconc.
End Fix.
End Make.