Library toptheorem

This file contains the side conditions used in the top rule. The key lemma "verified_os'" is used for proving the soundness of the top rule.

Require Import inferules.
Require Import language.
Require Import opsem.
Require Import etraceref.
Require Import assertion.
Require Import simulation.
Require Import memory.
Require Export MapLib.
Require Import lemmasfortoptheo.
Require Import LibTactics.
Require Import soundness.
Require Import auxdef.
Require Import tst_prop.
Require Import baseTac.
Require Import seplog_tactics.

the initial task pool is well-formed, which requires that the task pool and high-level abstract TCB list have the same domain.

Definition TaskOK :=
  fun (T : tasks) (p : progunit) (O : osabst) =>
    eqdomTO T O /\
    (forall (t : tidspec.A) (C : CodeSpec.B),
       TasksMod.get T t = Some C ->
       exists s f d1 d2 t0, C = nilcont s /\ p f = Some (t0, d1, d2, s)).

the client code is only allowed to call kernel APIs, while the kernel APIs and interrupts are only allowed to call internal functions

Definition good_call :=
fun (pc po pi : progunit) (ip : intunit) =>
no_call_api_pu po po /\ no_call_api_pu pi po /\ no_call_api_ipu ip po /\ no_call_api_pu pc pi.

the kernel APIs and internal functions are well-formed, which do not contain dynamic statements and specification code.

Definition good_os_pu (pu:progunit) :=
  (forall f t d1 d2 s, pu f = Some (t ,d1 ,d2 ,s ) -> good_decllist (revlcons d1 d2) = true /\ GoodStmt´ s).

Fixpoint Good_Clt_Stmt (s : stmts) {struct s} : Prop :=
  match s with
    | sskip _ => True
    | sassign _ _ => True
    | sif _ s1 s2 => Good_Clt_Stmt s1 /\ Good_Clt_Stmt s2
    | sifthen _ s0 => Good_Clt_Stmt s0
    | swhile _ s´ => Good_Clt_Stmt s´
    | sret => True
    | srete _ => True
    | scall f _ => True
    | scalle _ f _ => True
    | sseq s1 s2 => Good_Clt_Stmt s1 /\ Good_Clt_Stmt s2
    | sprint _ => True
    | sfexec _ _ _ => False
    | sfree _ _ => False
    | salloc _ _ => False
    | sprim _ => False
    | hapi_code _ => False
  end.

the constraint over the client code, which requires that the client code should not contain dynamic statements, assembly primitives (sprim) and specification code(hapi_code).

Definition good_cli_pu (pu:progunit):=
(forall f t d1 d2 s, pu f = Some (t ,d1 ,d2 ,s ) -> good_decllist (revlcons d1 d2) = true /\ Good_Clt_Stmt s).

the low-level program is well-formed

Definition ProgOK Pl :=
  exists pc po pi ip,
    Pl = (pc,(po,pi,ip)) /\
    no_fun_same pc po /\ no_fun_same pc pi /\ no_fun_same po pi /\
    good_call pc po pi ip /\
    good_os_pu po /\ good_os_pu pi /\ good_cli_pu pc.

the OS correctness is defined as contextual refinement. It says, if the initial tasks are well-formed, the low-level program is well-formed, the low level and high level have the same initial tasks, and the initial related states satisfy the initial assertion 'init', then the event trace set generated at the low level is the subset of that generated at the high level.

Definition OS_Correctness :=
fun (Os : oscode) (A : osspec) (init : InitAsrt) =>
  forall (t : tid) (pc : progunit)
         (Wl : progunit * oscode * tasks * clientst * osstate * tid)
         (Wh : progunit * osspec * tasks * clientst * OSAbstMod.map)
         (T : tasks) (S : osstate) (cst : clientst) (O : OSAbstMod.map),
    OSAbstMod.get O curtid = Some (oscurt t) ->
    TaskOK T pc O ->
    ProgOK (pc ,Os ) ->
    init S O ->
    Wl = (pc , Os , T , cst , S , t ) ->
    Wh = (pc , A , T , cst , O ) ->
    TasksMod.indom T t ->
    etrace_subset Wl Wh.

Definition WFIFun :=
  fun (P : progunit) (FSpec : funspec) (sd : ossched) (I : Inv) =>
    EqDom P FSpec /\
    (forall (f : fid) (pre : fpre) (post : fpost) (t : type) (tl : typelist),
       FSpec f = Some (pre , post , (t , tl )) ->
       exists d1 d2 s,
         P f = Some (t , d1, d2, s) /\
         tlmatch tl d1 /\
         (forall (vl : vallist) (p : asrt) (r : retasrt) (logicl : list logicvar),
            Some p = BuildPreI P f vl logicl pre ->
            Some r = BuildRetI P f vl logicl post ->
            {|FSpec , sd , I , r , Afalse |}|- {{p }}s {{Afalse }})).

Definition EqDomAPI (api:progunit) (aspec:osapispec) :=
   (forall f,
                (exists fdef, api f = Some fdef) <-> (exists fspec,aspec f =Some fspec))/\
             (forall f fdef fspec, api f = Some fdef -> aspec f = Some fspec ->
             tlmatch (snd (snd fspec)) (snd (fst (fst fdef))) /\ fst (fst (fst fdef)) = (fst (snd fspec)) ).

Definition EqDomInt (P:intunit) (intspec:osintspec) :=
   (forall i,
      (exists idef, P i = Some idef) <-> (exists absi,intspec i =Some absi)).

Definition WFAPI :=
  fun (P:progunit) (apispec:osapispec) (Spec:funspec) (sd : ossched) (I : Inv) =>
    EqDomAPI P apispec /\
    (
      forall (f:fid) ab vl p r ft,
        apispec f = Some (ab ,ft ) ->
        Some p = BuildPreA´ P f (ab ,ft ) vl ->
        Some r = BuildRetA´ P f (ab ,ft ) vl ->
        (
          exists t d1 d2 s,
            P f = Some (t, d1, d2, s) /\
            InfRules Spec sd I r Afalse p s Afalse
        )
    ).

Definition WFInt :=
  fun (P:intunit) (intspec:osintspec) (Spec:funspec) (sd : ossched) (I : Inv) =>
    EqDomInt P intspec /\
    (
      forall i isrreg si p r,
        Some p = BuildintPre i intspec isrreg si I ->
        Some r = BuildintRet i intspec isrreg si I ->
        exists s,
          P i = Some s /\
          {|Spec , sd , I , retfalse , r |}|- {{p }}s {{Afalse }}

    ).

Definition init_asrt I:= (INV I ) ** OS [empisr , true , nil , nil ] ** A_dom_lenv nil.

side-conditions for the invariants, the scheduler and the initial assertion

Definition side_condition I schedmethod init:=
  (
    GoodI I schedmethod /\
    (forall tid S O, init S O ->
                      (forall o, (projS S tid ) = Some o ->
                         forall ab, sat ((pair o O ),ab ) (init_asrt I)) /\ eqdomSO S O )
  ).

the main theorem for proving the soundness of the framework.

Theorem verified_os´:
  forall osc A (init:InitAsrt) (I:Inv) (Spec:funspec) pa pi ip apispec intspec schedmethod,
    osc = (pa ,pi ,ip ) ->
    A = (apispec ,intspec ,schedmethod ) ->

    WFAPI pa apispec Spec schedmethod I ->
    WFInt ip intspec Spec schedmethod I ->
    WFIFun pi Spec schedmethod I ->
    side_condition I schedmethod init ->

    OS_Correctness osc A init.