Library inferules


This file defines the inference rules of the refinement program logic. Corresponding to Sec. 4

Require Import include.
Require Import memdata.
Require Import memory.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import simulation.

Import OSAbstMod.

the execution step of the high-level specification code
Definition primstep (p p´ : asrt) :=
forall (s : taskst) (O : osabst) (gamma : absop),
(s, O, gamma) |= p ->
exists O´ gamma´,
hmstep gamma O gamma´ O´ /\ (s, O´, gamma´) |= p´.

the inference rules for the high-level abstract step
Inductive absinfer : asrt -> asrt -> Prop :=
| absinfer_eq :
    forall p,
      absinfer p p
               
| absinfer_trans :
    forall p q r,
      absinfer p q -> absinfer q r -> absinfer p r
                                               
| absinfer_disj:
    forall p1 p2 q1 q2,
      absinfer p1 q1 ->
      absinfer p2 q2 ->
      absinfer (p1\\//p2) (q1\\// q2)

| absinfer_conseq :
    forall p q p´ q´,
      q ==> q´ ->
      absinfer p q ->
      p´==> p -> absinfer p´ q´

| absinfer_ex :
    forall (tp:Type) (p:tp->asrt) q,
      (forall x,absinfer (p x) q) -> absinfer (EX x:tp,p x) q
                                    
| absinfer_frm :
    forall p q r,
      can_change_aop r ->
      absinfer p q -> absinfer (p ** r) (q ** r)
                                               
| absinfer_prim:
    forall p q step vl v,
      can_change_aop p ->
      can_change_aop q ->
      primstep (<||step (|vl|)||> ** p) (<||END v||> ** q)
      -> absinfer (<||step (|vl|)||> ** p) (<||END v||> ** q)
                   
| absinfer_seq: forall p q s1 s2 s1´,
                  can_change_aop p ->
                  can_change_aop q ->
                  absinfer (<||s1||> ** p) (<||s1´||> ** q) ->
                  absinfer (<||s1 ;; s2 ||> **p ) (<||s1´;;s2||>**q)

                                              
| absinfer_seq_end: forall p q s v,
                  can_change_aop p ->
                  can_change_aop q ->
                  p ==> q ->
                  absinfer (<||END v ;; s ||> **p ) (<||s||> ** q)
                           
| absinfer_choice1 :
    forall p q s1 s2,
      can_change_aop p ->
      can_change_aop q ->
      p ==> q ->
      absinfer (<||s1 ?? s2 ||> ** p) (<||s1||> ** q)
               
| absinfer_choice2 :
     forall p q s1 s2 ,
       can_change_aop p ->
       can_change_aop q ->
       p ==> q ->
       absinfer (<||s1 ?? s2 ||> ** p ) (<||s2||> ** q)
                
|absinfer_assume :
   forall p (b:absexpr) q,
     can_change_aop p ->
     can_change_aop q ->
      p ==> q ->
      (forall s, (s |= p) -> b (getabst s)) ->
     absinfer (<||ASSUME b||> ** p) (<||END None||> ** q).

Notation " ´⊢´ p ´⇒´ q " := (absinfer p q) (at level 80).

Open Local Scope Z_scope.

Definition match_tid_prio (tls: TcbMod.map) (v v´ : val) :=
 (exists pr a tid msg, v = Vptr tid /\
 TcbMod.get tls tid = Some (pr, a, msg) /\ v´ = Vint32 pr).

Definition retpost (p : fpost) : Prop :=
          forall s vl v logicl,sat s (getasrt (p vl v logicl))-> v <> None.

the side-condition for the frame rule
Fixpoint GoodStmt´ s :=
    match s with
      | sskip _ => True
      | sassign _ _ => True
      | sif _ s1 s2 => GoodStmt´ s1 /\ GoodStmt´ s2
      | sifthen _ s => GoodStmt´ s
      | swhile _ s´ => GoodStmt´ s´
      | sret => True
      | srete _ => True
      | scall f _ => True
      | scalle _ f _ => True
      | sseq s1 s2 => GoodStmt´ s1 /\ GoodStmt´ s2
      | sprint _ => True
      | sfexec _ _ _ => False
      | sfree _ _ => False
      | salloc _ _ => False
      | sprim _ => True
      | hapi_code _ => False
  end.

Fixpoint GoodFrm (p : asrt){struct p}: Prop :=
           match p with
           | Aie _ => False
           | Ais _ => False
           | ATopis _ => False
           | Aisr _ => False
           | Acs _ => False
           | p´ //\\ q´ => GoodFrm p´ /\ GoodFrm q´
           | p´ \\// q´ => GoodFrm p´ /\ GoodFrm q´
           | p´ ** q´ => GoodFrm p´ /\ GoodFrm q´
           | Aexists t p´ => forall x, GoodFrm (p´ x)
           | Anot _ => False
           | Aop _ => False
           | _ => True
         end.

Definition GoodSched (sd : ossched) :=
  (forall x a y t, OSAbstMod.join x a y ->
                   sd x t -> sd y t) /\
  (forall x t, sd x t ->
                (exists tcbls tcb,OSAbstMod.get x abstcblsid =
                                  Some (abstcblist tcbls) /\ TcbMod.get tcbls t = Some tcb)) /\
  (forall O1 O2 O t t´,
    OSAbstMod.join O1 O2 O ->
    sd O1 t ->
    sd O t´ ->
    sd O1 t´).

Definition GoodI (I:Inv) (sd : ossched) :=
  (forall o O O´ ab, (o,O,ab) |= starinv_noisr I 0%nat (S INUM) -> OSAbstMod.disj O O´ -> O´ =empabst)
/\
(forall o O ab, (o,O,ab)|= SWINV I -> exists b tp v tid, EnvMod.get (get_genv (get_smem o)) OSTCBCur = Some (b,(Tptr tp)) /\
    load (Tptr tp) (get_mem (get_smem o)) (b,0%Z) = Some v /\ OSAbstMod.get O curtid = Some (oscurt tid))
 /\
 ( forall o O ab tid b tp M´, (o,O,ab)|= SWINV I -> (o,O,ab) |= AHprio sd tid ** Atrue -> EnvMod.get (get_genv (get_smem o)) OSTCBCur = Some (b,(Tptr tp)) -> store (Tptr tp) (get_mem (get_smem o)) (b,0%Z) (Vptr tid) = Some M´ -> (substaskst o M´, set O curtid (oscurt tid), ab) |= SWINV I) /\ GoodSched sd.

The inference rules.
The 'ret_rule' requires that the post-condition 'r None' holds when we reach the end of the non-handler function without return value.
The 'iret_rule' simply requires that the post-condition 'ri' holds when we reach the end of the interrupt handler.
The 'rete_rule' requires that the post-condition 'r (Some v)' holds when we reach the end of the non-handler function with return expression 'e' and 'v' is the value of 'e'.
The 'abscsq_rule' looks like a regular consequence rule but allows us to consume the abstract code. 'primstep' defines the step of high-level specification, That is, starting from related states satisfying pre-condition, the abstract code could execute one step so that the resulting related states satisfy post-condition. This rule allows us to establish simulation between the concrete and the abstract code, which then ensures refinement. And we provide some inference rules 'absinfer' for high-level steps.
The 'encrit1_rule' shows the ownership transfer when interrupts are disabled. Suppose we are at the level-k handler (k = N means we are executing the non- handler code). Disabling interrupts prevents interrupt requests from level 0 to k − 1, therefore the current task gains the ownership of I0, k − 1. If the bit isr(k) is 0 (or k = N ), the task also gains the ownership of I(k), otherwise it already has the ownership of the k-th block and there is no extra ownership transfer. Note that, if the top of 'is' is k, then for all n < k, isr(n)=0, this is a invariant of 'isr' and 'is', and its easy to understand because the interrupt will lower-priority can not break the execution of the interrupts with higher-priority.
The 'switch_rule' requires that the invariant SWINV(I) holds before switching away and it is preserved after switching back. SWINV(I) says that interrupts must be disabled, and all the bits of isr are 0 (i.e., either we are running non-handler code or we are in the outmost layer of nested invocation of interrupt handlers and have already executed eoi). Also if we are running level-k code (either handler or non-handler if k = N ), the resource blocks 0 to k acquired before should satisfy I0, k, so that the target task could access them. The rule also says that the task-local states is and cs are not changed by switch. To establish refinement, the precondition also requires that the high-level abstract scheduler χ picks the same task with the one in x, and switch x at the low level correspond to the sched step at the high level. Therefore in the post-condition sched is no longer in the remaining abstract operations.

Inductive InfRules: funspec -> ossched -> Inv -> retasrt -> asrt ->
                    asrt -> stmts -> asrt -> Prop:=
  
| pfalse_rule: forall Spec sd I r ri q s,
                              InfRules Spec sd I r ri Afalse s q
 
| pure_split_rule: forall Spec sd I r ri p q (pu:Prop) s,
                              (pu -> InfRules Spec sd I r ri
                                       p s q ) -> (InfRules Spec sd I r ri
                                       (p**[|pu|]) s q)

| genv_introret_rule : forall Spec sd I r ri p q s G,
                               InfRules Spec sd I r ri p s q ->
                              InfRules Spec sd I (fun v => (Agenv G //\\ r v)) ri
                        (Agenv G //\\ p) s q

| genv_introexint_rule : forall Spec sd I r ri p q s G,
                               InfRules Spec sd I r ri p s q ->
                              InfRules Spec sd I r (Agenv G //\\ ri)
                        (Agenv G //\\ p) s q



| ret_rule : forall Spec sd I r p,
                                (p ==> r None) ->
                                InfRules Spec sd I r Afalse p sret Afalse



| iret_rule : forall Spec sd I ri p, (p ==> ri ) ->
                                   InfRules Spec sd I arfalse ri p (sprim exint ) Afalse
                                            


| rete_rule : forall (Spec:funspec) sd I r p e v t,
                     (p ==> r (Some v) //\\ Rv e@t == v) ->
                     InfRules Spec sd I r Afalse p (srete e) Afalse
                                          

| call_rule :forall f Spec sd I r ri pre post p P el vl logicl tp tl,
         GoodFrm p ->
         Spec f = Some (pre, post, (tp, tl)) ->
         P ==> (PRE[pre, vl, logicl] ** p) ->
         P ==> Rvl el @ tl == vl ->
         tl_vl_match tl vl = true ->
         InfRules Spec sd I r ri (P) (scall f el)
                  (EX v,POST[post, vl,v,logicl] ** p )
                  
| calle_rule : forall f e l Spec sd I r ri pre post p P el v´ vl logicl tp tl,
             GoodFrm p ->
             retpost post ->
             Spec f = Some (pre, post, (tp ,tl))->
             P ==> (PRE[pre,vl,logicl]** ( PV l @ tp|-> v´) **p) ->
             P ==> Rvl el @ tl == vl ->
             ((PV l @ tp|-> v´) **p ==> Lv e @ tp == l) ->
             tl_vl_match tl vl =true ->
             InfRules Spec sd I r ri ( P)
                      (scalle e f el) (EX v, POST[post, vl, Some v,logicl] ** PV l @ tp|-> v ** p )

| calle_rule_lvar: forall f x Spec sd t I r ri pre post P p el v´ vl logicl tp tl,
             GoodFrm p ->
             retpost post ->
             Spec f = Some (pre, post, (tp ,tl))->
             P ==> (PRE[pre,vl,logicl] ** LV x @ t |-> v´ ** p) ->
             P ==> Rvl el @ tl == vl ->
             tl_vl_match tl vl = true ->
             InfRules Spec sd I r ri (P )
                     (scalle (evar x) f el) (EX v, POST[post, vl, Some v,logicl] ** LV x @ t |-> v ** p)

| conseq_rule : forall Spec sd I r ri p´ p q q´ s,
                               (p´ ==> p) -> (q ==> q´) ->
                              InfRules Spec sd I r ri p s q ->
                                  InfRules Spec sd I r ri p´ s q´
| r_conseq_rule : forall Spec sd I r ri r´ p q ri´ s,
                               (forall v,r v ==> r´ v) -> (ri ==> ri´) ->
                              InfRules Spec sd I r ri p s q ->
                                  InfRules Spec sd I r´ ri´ p s q



| abscsq_rule : forall Spec sd I r ri p´ p q q´ s,
                  ⊢ p´⇒p -> ⊢ q ⇒ q´ ->
                  InfRules Spec sd I r ri p s q ->
                  InfRules Spec sd I r ri p´ s q´

| seq_rule : forall Spec sd I r ri p p´ q s1 s2,
                              InfRules Spec sd I r ri p s1 p´ ->
                              InfRules Spec sd I r ri p´ s2 q ->
                                   InfRules Spec sd I r ri p (sseq s1 s2) q

| if_rule : forall Spec sd I r ri p q e tp s1 s2,
                                  (p ==> EX v , Rv e @ tp == v) ->
                         InfRules Spec sd I r ri (p//\\ Aistrue e) s1 q ->
                          InfRules Spec sd I r ri (p //\\ Aisfalse e) s2 q ->
                          InfRules Spec sd I r ri p (sif e s1 s2) q

| ift_rule : forall Spec sd I r ri p q e tp s,
                                  (p ==> EX v , Rv e @ tp == v) ->
                                  (p//\\ Aisfalse e ==> q) ->
                         InfRules Spec sd I r ri (p//\\ Aistrue e) s q ->
                          InfRules Spec sd I r ri p (sifthen e s) q


| while_rule : forall Spec sd I r ri p e s tp,
                           ( p ==> EX v , Rv e @ tp == v) ->
                  InfRules Spec sd I r ri ( p //\\ (Aistrue e)) s p ->
                   InfRules Spec sd I r ri p (swhile e s) (p //\\ (Aisfalse e))

| frame_rule : forall Spec sd I p q frm s aop aop´,
                  GoodI I sd->
                  GoodStmt´ s -> GoodFrm frm ->
                  InfRules Spec sd I arfalse Afalse (p //\\ <|aop|>) s (q //\\ <|aop´|>) ->
                  InfRules Spec sd I arfalse Afalse (p ** frm //\\ <|aop|>) s (q ** frm //\\ <|aop´|>)

| frame_rule_all: forall Spec sd I r ri p q frm s,
                     GoodI I sd ->
                     GoodStmt´ s -> GoodFrm frm ->
                     InfRules Spec sd I r ri p s q ->
                     InfRules Spec sd I (fun v =>(r v) ** frm)
                             (ri**frm) (p ** frm ) s (q ** frm )

| retspec_intro_rule : forall Spec sd I r ri p q s ,
                    InfRules Spec sd I arfalse Afalse p s q ->
                   InfRules Spec sd I r ri p s q

| assign_rule : forall Spec sd I r ri p e1 e2 l v1 v2 tp1 tp2 aop,
                    assign_type_match tp1 tp2 ->
                    ((p ** PV l @ tp1|-> v1) ==> Lv e1 @ tp1 == l //\\ Rv e2 @ tp2 == v2) ->
                    InfRules Spec sd I r ri ((p ** PV l @ tp1 |-> v1)
              //\\ <|aop|>) (sassign e1 e2) (p ** PV l @ tp1 |-> v2 //\\ <|aop|>)


| encrit1_rule : forall Spec sd I r ri isr is cs i aop,
                         InfRules Spec sd I r ri
                (OS[isr, true, is, cs] ** (ATopis i) ** (Apure (i <= INUM)%nat) //\\ <|aop|>)
                  (sprim encrit)
                (OS[isr, false, is, true::cs] ** (invlth_isr I O i)//\\ <|aop|>)


| encrit2_rule : forall Spec sd I r ri isr is cs aop,
                         InfRules Spec sd I r ri
             (OS[isr, false, is, cs] //\\ <|aop|>)
                  (sprim encrit)
             (OS[isr, false, is, false::cs] //\\ <|aop|>)

| excrit1_rule : forall Spec sd I r ri isr is cs i aop,
                         InfRules Spec sd I r ri
          (OS[isr, false, is, true::cs] ** (ATopis i) ** (invlth_isr I O i)//\\ <|aop|>)
                  (sprim excrit)
          (OS[isr, true, is, cs] //\\ <|aop|>)

| excrit2_rule : forall Spec sd I r ri isr is cs aop,
                         InfRules Spec sd I r ri
               (OS[isr, false, is, false::cs] //\\ <|aop|>)
                  (sprim excrit)
               (OS[isr, false, is, cs] //\\ <|aop|>)

| cli1_rule :forall Spec sd I r ri isr is i aop,
                         InfRules Spec sd I r ri
             (OS[isr, true, is, nil] ** (ATopis i) ** (Apure (i <= INUM)%nat)
                           //\\ <|aop|>)
                  (sprim cli)
             (OS[isr, false,is, nil] ** (invlth_isr I O i)//\\ <|aop|>)

| cli2_rule : forall Spec sd I r ri isr is aop,
                         InfRules Spec sd I r ri
               (OS[isr, false, is, nil] //\\ <|aop|>)
                  (sprim cli)
               (OS[isr, false, is, nil] //\\ <|aop|>)

| sti1_rule : forall Spec sd I r ri isr i is aop,
                         InfRules Spec sd I r ri
              (OS[isr, false, is, nil] ** (ATopis i) ** (invlth_isr I O i)//\\ <|aop|>)
                  (sprim sti)
              (OS[isr, true, is, nil] //\\ <|aop|>)

| sti2_rule : forall Spec sd I r ri isr is aop,
                         InfRules Spec sd I r ri
              (OS[isr, true, is, nil] //\\ <|aop|>)
                  (sprim sti)
              (OS[isr, true, is, nil] //\\ <|aop|>)


| switch_rule : forall Spec sd I r ri x is cs P aop,
                  P ==> (SWINV I ** Ais is ** Acs cs //\\ <|spec_seq sched aop|>) ->
                  P ==> (SWPRE sd x) ->
                  InfRules Spec sd I r ri (P)
                           (sprim (switch x)) ((SWINV I ** Ais is ** Acs cs) //\\ <|aop|>)

| checkis_rule : forall Spec sd I r ri x aop isr is ie cs v,
                   InfRules Spec sd I r ri
                            ((OS[isr, ie, is, cs] ** LV x @ Tint32 |-> v) //\\ <|aop|>)
                            (sprim (checkis x))
                            (OS[isr, ie, is, cs] ** LV x @ Tint32 |-> (is_length is) //\\ <|aop|>)

| eoi_ieon_rule : forall Spec sd I r ri isr is id cs i aop,
                          0 <= Int.unsigned id < Z_of_nat INUM ->
                          i = Z.to_nat (Int.unsigned id) ->
                         InfRules Spec sd I r ri
                        (OS[isr, true, i::is, cs] ** (getinv (I i)) //\\ <|aop|>)
                            (sprim (eoi id))
                        (OS[isrupd isr i false, true, i::is, cs] //\\ <|aop|>)
   
| eoi_ieoff_rule : forall Spec sd I r ri isr is id i cs aop,
                          0 <= Int.unsigned id < Z_of_nat INUM ->
                          i = Z.to_nat (Int.unsigned id) ->
                         InfRules Spec sd I r ri
              (OS[isr, false, i::is, cs] //\\ <|aop|>)
                  (sprim (eoi id))
               (OS[isrupd isr i false, false, i::is, cs] //\\ <|aop|>)

| ex_intro_rule : forall Spec sd I r ri q s {tp:Type} p,
                    (forall v´,InfRules Spec sd I r ri (p v´) s q) ->
                    InfRules Spec sd I r ri (EX v:tp,p v) s q

| disj_rule : forall Spec sd I r ri p1 p2 s q,
                InfRules Spec sd I r ri p1 s q ->
                InfRules Spec sd I r ri p2 s q ->
                InfRules Spec sd I r ri (p1\\//p2) s q.

Notation " ´{|´ F , sd , I , r , ri ´|}´ ´|-´ ´{{´ p ´}}´ s ´{{´ q ´}}´" :=
              (InfRules F sd I r ri p s q) (at level 50).

Definition WFFunEnv (P:progunit) (FSpec:funspec) (sd:ossched)(I:Inv) :Prop:=
                  EqDom P FSpec /\
                  forall f pre post t tl, FSpec f = Some (pre, post, (t, tl)) ->
                   exists d1 d2 s, P f = Some (t, d1, d2, s)/\
                   tlmatch tl d1 /\
                   good_decllist (revlcons d1 d2) = true /\
                   (
                        forall vl p r logicl,
                        Some p = BuildPreI P f vl logicl pre ->
                        Some r = BuildRetI P f vl logicl post ->
                        InfRules FSpec sd I r Afalse p s Afalse
                    ).

Definition WFFuncsSim´ (P:progunit) (FSpec:funspec) (sd:ossched)(I:Inv) :Prop:=
                    EqDom P FSpec /\
                  forall f pre post t tl, FSpec f = Some (pre, post, (t, tl)) ->
                   exists d1 d2 s, P f = Some (t, d1, d2, s)/\
                   tlmatch tl d1 /\
                   good_decllist (revlcons d1 d2) = true /\
                   (
                        forall vl p r logicl,
                        Some p = BuildPreI P f vl logicl pre ->
                        Some r = BuildRetI P f vl logicl post ->
                        (forall o O aop, (o, O, aop) |= p ->
                           MethSim P sd (nilcont s) o aop O I r Afalse (lift Afalse))
                    ).

Open Scope Z_scope.

Definition rule_type_val_match (t:type) (v:val) :=
  match t,v with
    | Tnull, Vnull => true
    | Tint8,Vint32 v =>
      match (Int.unsigned v) <=? Byte.max_unsigned with
        | true => true
        | false => false
      end
    | Tint16,Vint32 v =>
      match (Int.unsigned v) <=? Int16.max_unsigned with
        | true => true
        | false => false
      end
    | Tint32,Vint32 v =>true
    | Tptr t,Vptr l => true
    | Tcom_ptr i,Vptr l => true
    | Tptr t ,Vnull => true
    | Tcom_ptr i,Vnull => true
    | _,_=> false
  end.
Close Scope Z_scope.

Definition absimp´ (p p´ : asrt) :=
  forall (s : taskst) (O : osabst) (gamma : absop),
    (s, O, gamma) |= p ->
    forall (Of : OSAbstMod.map),
      OSAbstMod.disj O Of ->
      exists O´ gamma´,
        OSAbstMod.disj O´ Of /\
        hmstepstar gamma (OSAbstMod.merge O Of) gamma´
                   (OSAbstMod.merge O´ Of) /\ (s, O´, gamma´) |= p´.

Definition absimp (p p´ : asrt) :=
  forall (s : taskst) (O : osabst) (gamma : absop),
    (s, O, gamma) |= p ->
    exists O´ gamma´,
      hmstepstar gamma O gamma´ O´ /\ (s, O´, gamma´) |= p´.

Definition emposspec : osspec := ( fun (i : fid) => None, fun (i : hid) => None, fun _ _ => True ).