Library PIF_aux

Require Import lemmasfortoptheo.
Require Import ucert.
Require Import auxdef.
Require Import etraceref.
Require Import PIF_def.

Definition WEAK_PIF (O:osabst) :=
  forall els tls ct p_ct,
    OSAbstMod.get O absecblsid = Some (absecblist els) ->
    OSAbstMod.get O abtcblsid = Some (abstcblist tls) ->
    OSAbstMod.get O curtid = Some (oscurt ct) ->
    GET_OP ct tls els p_ct ->
    NO_NEST_PENDING tls els ->
    HighestRdy tls ct ->
    ~ (exists eid, IS_OWNER ct eid els) ->
    forall t p_t,
      t <> ct ->
      TcbMod.get tls t <> None ->
      GET_OP t tls els p_t ->
      IS_WAITING t els ->
      Int.ltu p_ct p_t = true.

Definition O_PI tls els :=
  exists t t_owner p p_owner st st_owner msg msg_owner,
    WAIT_OWNER t t_owner tls els /\
    TcbMod.get tls t = Some (p,st,msg) /\
    TcbMod.get tls t_owner = Some (p_owner,st_owner,msg_owner) /\
    Int.ltu p p_owner = true.

Definition O_PIF tls els := ~ O_PI tls els.

Definition OLD_PIF O:=
  forall els tls,
    OSAbstMod.get O absecblsid = Some (absecblist els) ->
    OSAbstMod.get O abtcblsid = Some (abstcblist tls) ->
    O_PIF tls els.

Definition PIF_aux (O:osabst) :=
  forall els tls ct p_ct,
    OSAbstMod.get O absecblsid = Some (absecblist els) ->
    OSAbstMod.get O abtcblsid = Some (abstcblist tls) ->
    OSAbstMod.get O curtid = Some (oscurt ct) ->
    GET_OP ct tls els p_ct ->
    HighestRdy tls ct ->
    ~ (exists eid, IS_OWNER ct eid els) ->
    forall t p_t,
      t <> ct ->
      TcbMod.get tls t <> None ->
      GET_OP t tls els p_t ->
      IS_WAITING t els ->
      Int.ltu p_ct p_t = true.

Definition O_PI_CHAIN tls els :=
  exists t t_owner p p_owner st st_owner msg msg_owner,
    WAIT_CHAIN t t_owner tls els /\
    TcbMod.get tls t = Some (p,st,msg) /\
    TcbMod.get tls t_owner = Some (p_owner,st_owner,msg_owner) /\
    Int.ltu p p_owner = true.

Definition O_PIF_CHAIN tls els := ~ O_PI_CHAIN tls els.

Definition OLD_PIF_CHAIN O:=
  forall els tls,
    OSAbstMod.get O absecblsid = Some (absecblist els) ->
    OSAbstMod.get O abtcblsid = Some (abstcblist tls) ->
    O_PIF_CHAIN tls els.

Definition rdy_notin_wl tls els :=
  (forall t p m, TcbMod.get tls t = Some (p,rdy,m) -> ~ IS_WAITING t els) /\
  (forall t p m eid tm,TcbMod.get tls t = Some (p,wait (os_stat_mutexsem eid) tm,m) -> IS_WAITING_E t eid els)/\
  (forall t eid, IS_WAITING_E t eid els -> exists p tm m, TcbMod.get tls t = Some (p,wait (os_stat_mutexsem eid) tm,m)) .

Definition not_in_two_wl els:= forall t,
                                 ~ exists eid eid´, eid <> eid´ /\ IS_WAITING_E t eid els /\ IS_WAITING_E t eid´ els.

Definition owner_prio_prop tls els:=
  forall t p st m eid pe po l,
    TcbMod.get tls t = Some (p,st,m) ->
    EcbMod.get els eid = Some (absmutexsem pe (Some (t,po)), l) ->
    (p = pe \/ p = po) /\ Int.ltu pe po =true.

Definition task_stat_prop tls:=
  forall t p st m,
    TcbMod.get tls t = Some (p,st,m) ->
    st = rdy \/ (exists eid tm, st = wait (os_stat_mutexsem eid) tm).

Definition op_p_prop tls els :=
  forall t st p m op,
    TcbMod.get tls t = Some (p,st,m) ->
    GET_OP t tls els op ->
    Int.ltu p op = true \/ Int.eq p op = true.

Definition wait_prop tls els:=
  forall t p m eid tm,
    TcbMod.get tls t = Some (p,wait (os_stat_mutexsem eid) tm,m) ->
    exists t´ po m, IS_OWNER t´ eid els /\ TcbMod.get tls t´ = Some (po,rdy,m) /\ Int.ltu po p = true /\
                    (forall op, GET_OP t tls els op -> op = p).

Definition no_owner_prio_prop tls els:=
  forall t p st m op,
    TcbMod.get tls t = Some (p,st,m) ->
    (~exists eid, IS_OWNER t eid els) ->
    GET_OP t tls els op ->
    op = p.


Definition GOOD_ST O :=
  forall tls els,
    OSAbstMod.get O absecblsid = Some (absecblist els) ->
    OSAbstMod.get O abtcblsid = Some (abstcblist tls) ->
    rdy_notin_wl tls els /\
    owner_prio_prop tls els /\
    task_stat_prop tls/\
    op_p_prop tls els/\
    wait_prop tls els/\
    no_owner_prio_prop tls els.

Definition api_spec_list´ :=
  (OSMutexAccept, mutexaccapi)
    :: (OSMutexCreate, mutexcreapi)
    :: (OSMutexDel, mutexdelapi)
    :: (OSMutexPend, mutexpendapi)
    :: (OSMutexPost, mutexpostapi)
    :: nil.

Definition api_spec´:= convert_api_spec api_spec_list´.

Definition os_spec´ := (api_spec´,int_spec,GetHPrio).

Definition GOOD_API_CODE O T :=
  exists C t,
    OSAbstMod.get O curtid = Some (oscurt t) /\
    TasksMod.get T t = Some C /\
    (
      (exists ke ks vl, C = (curs (hapi_code (spec_prim vl mutexacc_succ)), (ke,ks))) \/
      (exists ke ks vl, C = (curs (hapi_code (spec_prim vl mutexcre_succ)), (ke,ks))) \/
      (exists ke ks vl, C = (curs (hapi_code (spec_prim vl mutexdel_succ)), (ke,ks))) \/
      (exists ke ks vl, C = (curs (hapi_code (spec_prim vl mutexpend_get_succ)), (ke,ks))) \/
      (exists ke ks vl s, C = (curs (hapi_code (mutexpend_block_no_lift (|vl|);;s)), (ke,ks))) \/
      (exists ke ks vl s, C = (curs (hapi_code (mutexpend_block_lift (|vl|);;s)), (ke,ks))) \/
      (exists ke ks vl, C = (curs (hapi_code (mutexpost_nowt_return_prio_succ (|vl|))), (ke,ks))) \/
      (exists ke ks vl, C = (curs (hapi_code (mutexpost_nowt_no_return_prio_succ (|vl|))), (ke,ks))) \/
      (exists ke ks vl s, C = (curs (hapi_code (mutexpost_exwt_return_prio_succ (|vl|);;s)), (ke,ks))) \/
      (exists ke ks vl s, C = (curs (hapi_code (mutexpost_exwt_no_return_prio_succ (|vl|);;s)), (ke,ks)))\/
      (exists ke ks s, C = (curs (hapi_code (timetick_spec (|nil|);;s)), (ke,ks)))\/
      (exists ke ks s, C = (curs (hapi_code (sched;;s)), (ke,ks)))
    ).

Lemma joinsig_joinsig_eq:
  forall tls tls´ a b x y,
    TcbMod.join tls (TcbMod.sig a b ) tls´ ->
    TcbMod.join tls (TcbMod.sig x y) tls´ ->
    a = x /\ b = y.

Lemma osabst_get_get_disj_eq :
  forall O x y Of z,
    OSAbstMod.get O x = Some y ->
    OSAbstMod.get (OSAbstMod.merge O Of) x =
    Some z ->
    OSAbstMod.disj O Of -> y = z.

Lemma osabst_get_get_disj_get :
  forall O x y Of ,
    OSAbstMod.get O x = Some y ->
    
    OSAbstMod.disj O Of ->
    OSAbstMod.get (OSAbstMod.merge O Of) x =
    Some y.

Lemma abst_disj_merge_eq_eq:
  forall O Of O´,OSAbstMod.disj O Of -> OSAbstMod.merge O Of = OSAbstMod.merge O´ Of -> eqdomO O O´ -> O = O´.

Lemma spec_ext : forall f1 f2 : vallist -> osabst -> option val * osabst -> Prop,
                   f1 = f2 -> (forall vl O1 rst, f1 vl O1 rst = f2 vl O1 rst).

Lemma prop_eq_impl : forall P Q : Prop, P = Q -> (P -> Q).

Definition addrval_a := (xI xH, Int.one).
Definition tid_a := (xH, Int.zero).

Lemma no_nest_pending_set_none:
  forall tls p_ct st msg els eid ct p_e wl x6 x7,
    TcbMod.get tls ct = Some (p_ct, st, msg) ->
    EcbMod.get els eid = Some (absmutexsem x6 None, x7) ->
    NO_NEST_PENDING tls (EcbMod.set els eid (absmutexsem p_e (Some (ct, p_ct)), wl)) ->
    ~ (exists qid, IS_OWNER ct qid els).

Lemma no_nest_pending_set_prio_eq:
  forall tls x4 x3 x6 ct x8 x7 x9 x10 p_ct,
    NO_NEST_PENDING tls (EcbMod.set x4 x3 (absmutexsem x6 (Some (ct, x8)), x7)) ->
    GET_OP ct tls (EcbMod.set x4 x3 (absmutexsem x6 (Some (ct, x8)), x7)) p_ct ->
    TcbMod.get tls ct = Some (x8, x9, x10) ->
    p_ct = x8.

Lemma no_nest_pending_set_hold:
  forall tls x4 x3 x6 ct x8 x7,
    NO_NEST_PENDING tls
                    (EcbMod.set x4 x3 (absmutexsem x6 (Some (ct, x8)), x7)) ->
    EcbMod.get x4 x3 = Some (absmutexsem x6 None, x7) ->
    NO_NEST_PENDING tls x4.

Lemma set_neq_getop_eq:
  forall t ct tls x4 x3 x6 x7 x8 p_t,
    t <> ct ->
    TcbMod.get tls t <> None ->
    EcbMod.get x4 x3 = Some (absmutexsem x6 None, x7) ->
    GET_OP t tls (EcbMod.set x4 x3 (absmutexsem x6 (Some (ct, x8)), x7)) p_t ->
    GET_OP t tls x4 p_t.

Lemma iswaiting_set_ct_neq_hold:
  forall t ct tls x4 x3 x6 x7 xx yy,
    t <> ct ->
    TcbMod.get tls t <> None ->
    EcbMod.get x4 x3 = Some (absmutexsem x6 xx, x7) ->
    IS_WAITING t (EcbMod.set x4 x3 (absmutexsem x6 yy, x7)) ->
    IS_WAITING t x4.

Lemma ecb_joinsig_get_eq:
  forall x6 x3 x4 els x8 a0 x9 x,
    EcbMod.joinsig x6 (absmutexsem x3 None, nil) x4 els ->
    EcbMod.get x4 x = Some (absmutexsem x9 a0, x8) ->
    EcbMod.get els x = Some (absmutexsem x9 a0, x8).

Lemma getop_cre_hold:
  forall x6 x3 x4 els tls ct p_ct,
    GET_OP ct tls els p_ct ->
    EcbMod.joinsig x6 (absmutexsem x3 None, nil) x4 els ->
    GET_OP ct tls x4 p_ct.

Lemma no_nest_pending_cre_hold:
  forall tls els x6 x3 x4,
    NO_NEST_PENDING tls els ->
    EcbMod.joinsig x6 (absmutexsem x3 None, nil) x4 els ->
    NO_NEST_PENDING tls x4.

Lemma iswaiting_cre_hold:
  forall t x4 x3 x6 els,
    EcbMod.joinsig x6 (absmutexsem x3 None, nil) x4 els ->
    IS_WAITING t els ->
    IS_WAITING t x4.

Lemma ecb_join_get_eq´:
  forall x6 x3 x4 els x7 x8 a0 x9 x,
    EcbMod.join els (EcbMod.sig x3 (absmutexsem x6 None, nil)) x4 ->
    EcbMod.get x4 x = Some (absmutexsem x9 (Some (a0, x7)), x8) ->
    EcbMod.get els x = Some (absmutexsem x9 (Some (a0, x7)), x8).

Lemma getop_del_hold:
  forall ct tls els p_ct x3 x6 x4,
    GET_OP ct tls els p_ct ->
    EcbMod.join els (EcbMod.sig x3 (absmutexsem x6 None, nil)) x4 ->
    GET_OP ct tls x4 p_ct.

Lemma no_nest_pending_del:
  forall tls els x3 x6 x4,
    NO_NEST_PENDING tls els ->
    EcbMod.join els (EcbMod.sig x3 (absmutexsem x6 None, nil)) x4 ->
    NO_NEST_PENDING tls x4.

Lemma iswaiting_del_hold:
  forall t x4 x3 x6 els,
    EcbMod.join els (EcbMod.sig x3 (absmutexsem x6 None, nil)) x4 ->
    IS_WAITING t els ->
    IS_WAITING t x4.

Lemma pend_no_lift_getop:
  forall tls ct x12 x2 els x x8 x9 x10 x7 x0 t p_t,
    TcbMod.get tls ct = Some (x12, rdy, x2) ->
    EcbMod.get els x = Some (absmutexsem x8 (Some (x9, x10)), x7) ->
    GET_OP t (TcbMod.set tls ct (x12, wait (os_stat_mutexsem x) x0, Vnull))
           (EcbMod.set els x (absmutexsem x8 (Some (x9, x10)), ct :: x7)) p_t ->
    GET_OP t tls els p_t.

Lemma pend_no_lift_nnp:
  forall tls ct x12 x2 els x x8 x9 x10 x7 x0,
    TcbMod.get tls ct = Some (x12, rdy, x2) ->
    EcbMod.get els x = Some (absmutexsem x8 (Some (x9, x10)), x7) ->
    NO_NEST_PENDING (TcbMod.set tls ct (x12, wait (os_stat_mutexsem x) x0, Vnull))
                    (EcbMod.set els x (absmutexsem x8 (Some (x9, x10)), ct :: x7)) ->
    NO_NEST_PENDING tls els.

Lemma pend_no_lift_iswating:
  forall t ct els x x8 x9 x10 x7,
    t <> ct ->
    EcbMod.get els x = Some (absmutexsem x8 (Some (x9, x10)), x7) ->
    IS_WAITING t (EcbMod.set els x (absmutexsem x8 (Some (x9, x10)), ct :: x7)) ->
    IS_WAITING t els.

Lemma tcb_get_set_neq_none:
  forall t ct x tls,
    t <> ct ->
    TcbMod.get (TcbMod.set tls ct x) t <> None ->
    TcbMod.get tls t <> None.

Lemma pend_lift_nnp:
  forall tls ct x11 x12 x2 els x x8 x9 x10 x0 x13 x14 x15,
    TcbMod.get tls ct = Some (x13, rdy, x2) ->
    TcbMod.get tls x10 = Some (x12, x14, x15) ->
    EcbMod.get els x = Some (absmutexsem x9 (Some (x10, x11)), x8) ->
    NO_NEST_PENDING (TcbMod.set
                       (TcbMod.set tls ct (x13, wait (os_stat_mutexsem x) x0, x2)) x10
                       (x9, x14, x15))
                    (EcbMod.set els x (absmutexsem x9 (Some (x10, x11)), ct :: x8)) ->
    NO_NEST_PENDING tls els.

Lemma pend_lift_getop_t:
  forall tls ct x10 x13 x2 x12 x14 x15 x11 x x8 x9 t p_t els x0 st,
    t<> ct ->
    t<> x10 ->
    TcbMod.get tls ct = Some (x13, st, x2) ->
    TcbMod.get tls x10 = Some (x12, x14, x15) ->
    EcbMod.get els x = Some (absmutexsem x9 (Some (x10, x11)), x8) ->
    GET_OP t
           (TcbMod.set
              (TcbMod.set tls ct (x13, wait (os_stat_mutexsem x) x0, x2)) x10
              (x9, x14, x15))
           (EcbMod.set els x (absmutexsem x9 (Some (x10, x11)), ct :: x8)) p_t ->
    GET_OP t tls els p_t.

Lemma pend_lift_iswait:
  forall t ct els x x9 x10 x11 x8 ,
    t <> ct ->
    EcbMod.get els x = Some (absmutexsem x9 (Some (x10, x11)), x8) ->
    IS_WAITING t
               (EcbMod.set els x (absmutexsem x9 (Some (x10, x11)), ct :: x8)) ->
    IS_WAITING t els.

Lemma post_nowt_return_getop_ct:
  forall tls els x x5 ct x6 x7 x8 p_ct,
    NO_NEST_PENDING tls els ->
    EcbMod.get els x = Some (absmutexsem x5 (Some (ct, x6)), nil) ->
    TcbMod.get tls ct = Some (x5, x7, x8) ->
    GET_OP ct (TcbMod.set tls ct (x6, x7, x8))
           (EcbMod.set els x (absmutexsem x5 None, nil)) p_ct ->
    GET_OP ct tls els x6 /\ p_ct = x6.

Lemma post_nowt_return_getop_t:
  forall tls els x x5 t ct x6 x7 x8 p_t,
    t <> ct ->
    EcbMod.get els x = Some (absmutexsem x5 (Some (ct, x6)), nil) ->
    TcbMod.get tls ct = Some (x5, x7, x8) ->
    GET_OP t (TcbMod.set tls ct (x6, x7, x8))
           (EcbMod.set els x (absmutexsem x5 None, nil)) p_t ->
    GET_OP t tls els p_t.

Lemma no_owner_cre:
  forall ct els x6 x3 x4,
    ~ (exists eid, IS_OWNER ct eid els) ->
    EcbMod.joinsig x6 (absmutexsem x3 None, nil) x4 els ->
    ~ (exists eid, IS_OWNER ct eid x4).

Lemma no_owner_del:
  forall ct els x6 x3 x4,
    ~ (exists eid, IS_OWNER ct eid els) ->
    EcbMod.join els (EcbMod.sig x3 (absmutexsem x6 None, nil)) x4 ->
    ~ (exists eid, IS_OWNER ct eid x4).

Lemma post_lift_get_op_ct:
  forall Ox els tls x x5 ct x0 x1 p_ct,
    NO_NEST_PENDING_O Ox ->
    OSAbstMod.get Ox absecblsid = Some (absecblist els) ->
    OSAbstMod.get Ox abtcblsid = Some (abstcblist tls) ->
    EcbMod.get els x = Some (absmutexsem x5 (Some (ct, x0)), nil) ->
    TcbMod.get tls ct = Some (x5, rdy, x1) ->
    GET_OP ct (TcbMod.set tls ct (x0, rdy, x1))
           (EcbMod.set els x (absmutexsem x5 None, nil)) p_ct ->
    p_ct = x0.

Lemma post_lift_ct_nowner:
  forall Ox els tls x x5 ct x0 x1 p_ct x3,
    NO_NEST_PENDING_O Ox ->
    OSAbstMod.get Ox absecblsid = Some (absecblist els) ->
    OSAbstMod.get Ox abtcblsid = Some (abstcblist tls) ->
    EcbMod.get els x = Some (absmutexsem x5 (Some (ct, p_ct)), nil) ->
    TcbMod.get tls ct = Some (x5, rdy, x1) ->
    IS_OWNER x3 x0 (EcbMod.set els x (absmutexsem x5 None, nil)) ->
    x3 <> ct.

Lemma post_nolift_get_op_ct:
  forall Ox els tls x x5 x0 ct x1 p_ct,
    NO_NEST_PENDING_O Ox ->
    OSAbstMod.get Ox absecblsid = Some (absecblist els) ->
    OSAbstMod.get Ox abtcblsid = Some (abstcblist tls) ->
    EcbMod.get els x = Some (absmutexsem x5 (Some (ct, x0)), nil) ->
    TcbMod.get tls ct = Some (x0, rdy, x1) ->
    GET_OP ct tls
           (EcbMod.set els x (absmutexsem x5 None, nil)) p_ct ->
    p_ct = x0.

Lemma post_no_lift_ct_nowner:
  forall Ox els tls x x5 ct x0 x1 p_ct x3,
    NO_NEST_PENDING_O Ox ->
    OSAbstMod.get Ox absecblsid = Some (absecblist els) ->
    OSAbstMod.get Ox abtcblsid = Some (abstcblist tls) ->
    EcbMod.get els x = Some (absmutexsem x5 (Some (ct, p_ct)), nil) ->
    TcbMod.get tls ct = Some (p_ct, rdy, x1) ->
    IS_OWNER x3 x0 (EcbMod.set els x (absmutexsem x5 None, nil)) ->
    x3 <> ct.

Lemma post_ex_wait_ct_neq:
  forall Ox els tls x x6 ct x8 x11 x12,
    NO_NEST_PENDING_O Ox ->
    OSAbstMod.get Ox absecblsid = Some (absecblist els) ->
    OSAbstMod.get Ox abtcblsid = Some (abstcblist tls) ->
    EcbMod.get els x = Some (absmutexsem x6 (Some (ct, x8)), x11) ->
    GetHWait tls x11 x12 ->
    x12 <> ct.

Lemma post_lift_exwt_get_op_ct:
  forall (Ox : OSAbstMod.map) (els : EcbMod.map)
         (tls : TcbMod.map) (x : tidspec.A) (x6 : int32)
         (ct : tid) (x0 : int32) (x1 : msg) (p_ct : int32) x12 x7 x11 x5,
    x12 <> ct ->
    NO_NEST_PENDING_O Ox ->
    OSAbstMod.get Ox absecblsid = Some (absecblist els) ->
    OSAbstMod.get Ox abtcblsid = Some (abstcblist tls) ->
    EcbMod.get els x = Some (absmutexsem x6 (Some (ct, x0)), x11) ->
    TcbMod.get tls ct = Some (x5, rdy, x1) ->
    GET_OP ct
           (TcbMod.set (TcbMod.set tls ct (x0, rdy, x1)) x12 (x7, rdy, Vptr x))
           (EcbMod.set els x
                       (absmutexsem x6 (Some (x12, x7)), remove_tid x12 x11)) p_ct ->
    p_ct = x0.

Lemma post_lift_exwt_ct_nowner:
  forall Ox els tls x x5 ct x0 x1 p_ct x3 x12 x7 x11,
    NO_NEST_PENDING_O Ox ->
    OSAbstMod.get Ox absecblsid = Some (absecblist els) ->
    OSAbstMod.get Ox abtcblsid = Some (abstcblist tls) ->
    EcbMod.get els x = Some (absmutexsem x5 (Some (ct, p_ct)), x11) ->
    TcbMod.get tls ct = Some (x5, rdy, x1) ->
    IS_OWNER x3 x0 (EcbMod.set els x (absmutexsem x5 (Some (x12, x7)), remove_tid x12 x11)) -> x12 <> ct ->
    x3 <> ct.

Lemma post_nolift_exwt_get_op_ct:
  forall Ox els tls x ct p_ct x11 x12 x13 x6 x7 x8 x9,
    x13 <> ct ->
    NO_NEST_PENDING_O Ox ->
    OSAbstMod.get Ox absecblsid = Some (absecblist els) ->
    OSAbstMod.get Ox abtcblsid = Some (abstcblist tls) ->
    EcbMod.get els x = Some (absmutexsem x6 (Some (ct, x9)), x12) ->
    TcbMod.get tls ct = Some (x8, rdy, x11) ->
    GET_OP ct (TcbMod.set tls x13 (x7, rdy, Vptr x))
           (EcbMod.set els x
                       (absmutexsem x6 (Some (x13, x7)), remove_tid x13 x12)) p_ct ->
    p_ct = x8.

Lemma post_nolift_exwt_ct_nowner:
  forall Ox els tls x x3 ct x0 p_ct x13 x6 x7 x12 x11,
    NO_NEST_PENDING_O Ox ->
    OSAbstMod.get Ox absecblsid = Some (absecblist els) ->
    OSAbstMod.get Ox abtcblsid = Some (abstcblist tls) ->
    EcbMod.get els x = Some (absmutexsem x6 (Some (ct, p_ct)), x12) ->
    TcbMod.get tls ct = Some (p_ct, rdy, x11) ->
    IS_OWNER x3 x0 (EcbMod.set els x
                                (absmutexsem x6 (Some (x13, x7)), remove_tid x13 x12))-> x13 <> ct ->
    x3 <> ct.

Lemma tickchange_els :
  forall t st st´ els els´,
    tickchange t st els st´ els´ ->
    (els = els´ \/
     (exists eid m wl, EcbMod.get els eid = Some (m, wl) /\
        els´ = EcbMod.set els eid (m, remove_tid t wl))
    ).

Lemma GET_OP_st_irrel :
  forall tls els t ct p st st´ msg p_ct,
    TcbMod.get tls t = Some (p, st, msg) ->
    GET_OP ct (TcbMod.set tls t (p, st´, msg)) els p_ct ->
    GET_OP ct tls els p_ct.

Lemma IS_OWNER_remove_tid_irrel :
    forall els m wl x x0 t ct,
      EcbMod.get els x = Some (m, wl) ->
      IS_OWNER ct x0 (EcbMod.set els x (m, remove_tid t wl)) ->
      IS_OWNER ct x0 els.

Lemma IS_OWNER_remove_tid_irrel´ :
    forall els m wl x x0 t ct,
      EcbMod.get els x = Some (m, wl) ->
      IS_OWNER ct x0 els ->
      IS_OWNER ct x0 (EcbMod.set els x (m, remove_tid t wl)).

Lemma IS_OWNER_P_remove_tid_irrel :
  forall els m wl x x0 t ct p_ct,
    EcbMod.get els x = Some (m, wl) ->
    IS_OWNER_P ct x0 (EcbMod.set els x (m, remove_tid t wl)) p_ct ->
    IS_OWNER_P ct x0 els p_ct.

Lemma GET_OP_remove_tid_irrel :
  forall tls els ct t x m wl p_ct,
    EcbMod.get els x = Some (m, wl) ->
    GET_OP ct tls (EcbMod.set els x (m, remove_tid t wl)) p_ct ->
    GET_OP ct tls els p_ct.


Lemma tickchange_getop_eq:
  forall ct tls tls´ t0 p st msg0 st´ els els´ p_ct´,
    TcbMod.get tls t0 = Some (p, st, msg0) ->
    TcbMod.set tls t0 (p, st´, msg0) = tls´ ->
    tickchange t0 st els st´ els´ ->
    GET_OP ct tls´ els´ p_ct´ ->
    GET_OP ct tls els p_ct´.

Lemma tickchange_highestrdy_rdy:
  forall ct tls tls´ t0 p st msg0 st´ els els´,
    TcbMod.get tls t0 = Some (p, st, msg0) ->
    TcbMod.set tls t0 (p, st´, msg0) = tls´ ->
    tickchange t0 st els st´ els´ ->
    HighestRdy tls´ ct ->
    (exists p msg, TcbMod.get tls ct = Some (p,rdy,msg)) ->
    HighestRdy tls ct.

Lemma tickchange_no_owner:
  forall ct tls tls´ t0 p st msg0 st´ els els´,
    TcbMod.get tls t0 = Some (p, st, msg0) ->
    TcbMod.set tls t0 (p, st´, msg0) = tls´ ->
    tickchange t0 st els st´ els´ ->
    ~ (exists eid, IS_OWNER ct eid els´) ->
    ~ (exists eid, IS_OWNER ct eid els).

Lemma tickchange_nonone:
  forall ct tls tls´ t0 p st msg0 st´ els els´,
    TcbMod.get tls t0 = Some (p, st, msg0) ->
    TcbMod.set tls t0 (p, st´, msg0) = tls´ ->
    tickchange t0 st els st´ els´ ->
    TcbMod.get tls´ ct <> None ->
    TcbMod.get tls ct <> None.

Lemma tickchange_iswait:
  forall ct tls tls´ t0 p st msg0 st´ els els´,
    TcbMod.get tls t0 = Some (p, st, msg0) ->
    TcbMod.set tls t0 (p, st´, msg0) = tls´ ->
    tickchange t0 st els st´ els´ ->
    IS_WAITING ct els´ ->
    IS_WAITING ct els.
  Lemma In_remove_tid : forall wl t ct, In ct (remove_tid t wl) -> In ct wl.

Qed.

Lemma tickchange_nonestpend:
  forall tls tls´ t0 p st msg0 st´ els els´,
    TcbMod.get tls t0 = Some (p, st, msg0) ->
    TcbMod.set tls t0 (p, st´, msg0) = tls´ ->
    tickchange t0 st els st´ els´ ->
    NO_NEST_PENDING tls els ->
    NO_NEST_PENDING tls´ els´.

Lemma tickchange_exct:
  forall tls els els´ tls´ t0 ct p st st´ msg0,
    tickchange t0 st els st´ els´ ->
    TcbMod.set tls t0 (p, st´, msg0) = tls´ ->
    TcbMod.get tls t0 = Some (p, st, msg0) ->
    HighestRdy tls´ ct ->
    exists pct stct mct,TcbMod.get tls ct = Some (pct,stct,mct).

Lemma tickchange_eq_prio:
  forall tls els els´ tls´ t0 ct p msg0 pct pct´ st st´ stx stx´ m m´,
    tickchange t0 st els st´ els´ ->
    TcbMod.set tls t0 (p, st´, msg0) = tls´ ->
    TcbMod.get tls t0 = Some (p, st, msg0) ->
    TcbMod.get tls ct = Some (pct,stx,m) ->
    TcbMod.get tls´ ct = Some (pct´,stx´,m´) ->
    pct = pct´.

Lemma tickchange_nonest_ct:
  forall tls els els´ tls´ t0 ct p msg0 pct´ st st´ tm m eid x2,
    rdy_notin_wl tls els ->
    tickchange t0 st els st´ els´ ->
    TcbMod.set tls t0 (p, st´, msg0) = tls´ ->
    TcbMod.get tls t0 = Some (p, st, msg0) ->
    IS_OWNER ct x2 els´ ->
    TcbMod.get tls ct = Some (pct´, wait (os_stat_mutexsem eid) tm, m) ->
    NO_NEST_PENDING tls els ->
    False.

Lemma joinsig_neq_get:
  forall x y els els0 s eid,
    eid <> x ->
    EcbMod.get els0 eid = s ->
    EcbMod.joinsig x y els els0 ->
    EcbMod.get els eid = s.

Lemma ecb_joinsig_get_eq´
: forall (x6 : tidspec.A) (x3 : int32) (x4 els : EcbMod.map)
         (x8 : waitset) a0 (x9 : int32) (x : tidspec.A),
    EcbMod.joinsig x6 (absmutexsem x3 None, nil) els x4->
    EcbMod.get x4 x = Some (absmutexsem x9 (Some a0), x8) ->
    EcbMod.get els x = Some (absmutexsem x9 (Some a0), x8).

Lemma is_owner_set_other:
  forall t eid els x x3 x4 x5 ct,
    t <> ct ->
    IS_OWNER t eid els ->
    EcbMod.get els x = Some (absmutexsem x3 None, x4) ->
    IS_OWNER t eid
             (EcbMod.set els x (absmutexsem x3 (Some (ct, x5)), x4)).

Lemma pend_lift_getop_ct:
  forall (tls : TcbMod.map) (ct x10 : tidspec.A)
         (x13 : priority) (x2 : msg) (x12 : priority)
         (x14 : taskstatus) (x15 : msg) (x11 : int32)
         (x : tidspec.A) (x8 : waitset) (x9 : int32)
         (p_t : int32) (els : EcbMod.map)
         (x0 : int32) (st : taskstatus),
    x10 <> ct ->
    TcbMod.get tls ct = Some (x13, st, x2) ->
    TcbMod.get tls x10 = Some (x12, x14, x15) ->
    EcbMod.get els x = Some (absmutexsem x9 (Some (x10, x11)), x8) ->
    GET_OP ct
           (TcbMod.set
              (TcbMod.set tls ct (x13, wait (os_stat_mutexsem x) x0, x2)) x10
              (x9, x14, x15))
           (EcbMod.set els x (absmutexsem x9 (Some (x10, x11)), ct :: x8)) p_t ->
    GET_OP ct tls els p_t.

Lemma post_iswait:
  forall t x11 x12 x x6 els owner owner´,
    t <> x12 ->
    EcbMod.get els x = Some (absmutexsem x6 owner, x11) ->
    (IS_WAITING t
               (EcbMod.set els x
                           (absmutexsem x6 owner´, remove_tid x12 x11)) <->
    IS_WAITING t els).
  Lemma In_remove_tid´ : forall wl t t´, t <> t´ -> In t wl -> In t (remove_tid t´ wl).
    Lemma beq_tid_true_eq: forall t1 t2, beq_tid t1 t2 = true -> t1 = t2.
  Qed.

Qed.

Lemma post_iswait´:
  forall t x11 x12 x x6 eid els owner owner´,
    t <> x12 ->
    EcbMod.get els x = Some (absmutexsem x6 owner, x11) ->
    (IS_WAITING_E t eid
                 (EcbMod.set els x
                             (absmutexsem x6 owner´, remove_tid x12 x11)) <->
    IS_WAITING_E t eid els).

Lemma In_remove_tid_false : forall wl t, In t (remove_tid t wl) -> False.
  Lemma beq_tid_true : forall t, beq_tid t t = true.
Qed.

Lemma nnp_remove_nwait:
  forall tls els x11 t x x6 ct x8 p x13 x14,
    NO_NEST_PENDING tls els ->
    rdy_notin_wl tls els ->
    GetHWait tls x11 t ->
    EcbMod.get els x = Some (absmutexsem x6 (Some (ct, x8)), x11) ->
    TcbMod.get tls t = Some (p, x13, x14) ->
    ~
      IS_WAITING t
      (EcbMod.set els x (absmutexsem x6 (Some (t, p)), remove_tid t x11)).

Lemma remove_is_wait_neq:
  forall x12 t x x6 x7 x11 els ct x8,
    t <> x12 ->
    EcbMod.get els x = Some (absmutexsem x6 (Some (ct, x8)), x11) ->
    IS_WAITING t
               (EcbMod.set els x
                           (absmutexsem x6 (Some (x12, x7)), remove_tid x12 x11)) ->
    IS_WAITING t els.

Lemma tickchange_not_waiting:
  forall tls t p0 eid m0 m wl els,
    EcbMod.get els eid = Some (m, wl) ->
    TcbMod.get tls t = Some (p0, wait (os_stat_mutexsem eid) Int.one, m0)->
    rdy_notin_wl tls els ->
    NO_NEST_PENDING tls els ->
    ~ IS_WAITING t (EcbMod.set els eid (m, remove_tid t wl)).

Lemma remove_tid_in_false:
  forall t wl,
    In t (remove_tid t wl) -> False.

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

Definition GoodAcc (s:spec_code) vl:=
  (s = mutexacc_null (|vl|)
                     ?? mutexacc_no_mutex_err (|vl|)
                     ?? mutexacc_no_available (|vl|)
                     ?? mutexacc_prio_err (|vl|) ?? mutexacc_succ (|vl|)) \/
  s = mutexacc_null (|vl|) \/
  (s = mutexacc_no_mutex_err (|vl|)
                             ?? mutexacc_no_available (|vl|)
                             ?? mutexacc_prio_err (|vl|) ?? mutexacc_succ (|vl|)) \/
  s = mutexacc_no_mutex_err (|vl|) \/
  (s = mutexacc_no_available (|vl|)
                             ?? mutexacc_prio_err (|vl|) ?? mutexacc_succ (|vl|))\/
  s = mutexacc_no_available (|vl|)\/
  (s = mutexacc_prio_err (|vl|) ?? mutexacc_succ (|vl|) ) \/
  s = mutexacc_prio_err (|vl|) \/
  s = mutexacc_succ (|vl|) \/
  exists v, s = spec_done v.

Definition GoodCre (s:spec_code) vl:=
  (s = mutexcre_error (|vl|) ?? mutexcre_succ (|vl|)) \/
  s = mutexcre_error (|vl|) \/
  s = mutexcre_succ (|vl|) \/
  exists v, s = spec_done v.

Definition GoodDel (s:spec_code) vl:=
  (s = mutexdel_null (|vl|)
                     ?? mutexdel_no_mutex_err (|vl|)
                     ?? mutexdel_type_err (|vl|)
                     ?? mutexdel_ex_wt_err (|vl|) ?? mutexdel_succ (|vl|) ?? mutexdel_pr_not_holder_err (|vl|)) \/
  (s = mutexdel_null (|vl|)) \/
  (s = mutexdel_no_mutex_err (|vl|)
                     ?? mutexdel_type_err (|vl|)
                     ?? mutexdel_ex_wt_err (|vl|) ?? mutexdel_succ (|vl|) ?? mutexdel_pr_not_holder_err (|vl|) ) \/
  (s = mutexdel_no_mutex_err (|vl|)) \/
  (s = mutexdel_type_err (|vl|)
                         ?? mutexdel_ex_wt_err (|vl|) ?? mutexdel_succ (|vl|)?? mutexdel_pr_not_holder_err (|vl|)) \/
  (s = mutexdel_type_err (|vl|)) \/
  (s = mutexdel_ex_wt_err (|vl|) ?? mutexdel_succ (|vl|)?? mutexdel_pr_not_holder_err (|vl|)) \/
  (s = mutexdel_ex_wt_err (|vl|)) \/
  (s = mutexdel_succ (|vl|)?? mutexdel_pr_not_holder_err (|vl|)) \/
  s = mutexdel_succ (|vl|) \/
  s = mutexdel_pr_not_holder_err (|vl|) \/
  exists v, s = spec_done v.

Definition GoodPend (s:spec_code) vl :=
  s = mutexpend_null (|vl|)
                     ?? mutexpend_no_mutex_err (|vl|)
                     ?? mutexpend_type_err (|vl|)
                     ?? mutexpend_idle_err (|vl|)
                     ?? mutexpend_stat_err (|vl|)
                     ?? mutexpend_prio_err (|vl|)
                     ?? mutexpend_get_succ (|vl|)
                     ?? (mutexpend_block_lift (|vl|)
                                              ?? mutexpend_block_no_lift (|vl|));;
                     isched;;
                     (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) ?? mutexpend_pr_not_holder_err (|vl|) ??
                     mutexpend_nest_err (|vl|) ?? mutexpend_deadlock_err (|vl|)
                     ?? mutexpend_msg_not_null_err (|vl|) ?? mutexpend_cur_prio_eql_mprio_err
                                       (|vl|)
                                       ?? mutexpend_ptcb_prio_eql_idle_err
                                          (|vl|)
  \/
  s = mutexpend_null (|vl|) \/
  s = mutexpend_no_mutex_err (|vl|)
                             ?? mutexpend_type_err (|vl|)
                             ?? mutexpend_idle_err (|vl|)
                             ?? mutexpend_stat_err (|vl|)
                             ?? mutexpend_prio_err (|vl|)
                             ?? mutexpend_get_succ (|vl|)
                             ?? (mutexpend_block_lift (|vl|)
                                                      ?? mutexpend_block_no_lift (|vl|));;
                                                      isched;;
                                                      (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) ?? mutexpend_pr_not_holder_err (|vl|) ??
  mutexpend_nest_err (|vl|) ?? mutexpend_deadlock_err (|vl|)
                              ?? mutexpend_msg_not_null_err (|vl|) ?? mutexpend_cur_prio_eql_mprio_err
                                       (|vl|)
                                       ?? mutexpend_ptcb_prio_eql_idle_err
                                          (|vl|) \/
  s = mutexpend_no_mutex_err (|vl|) \/
  s = mutexpend_type_err (|vl|)
                         ?? mutexpend_idle_err (|vl|)
                         ?? mutexpend_stat_err (|vl|)
                         ?? mutexpend_prio_err (|vl|)
                         ?? mutexpend_get_succ (|vl|)
                         ?? (mutexpend_block_lift (|vl|)
                                                  ?? mutexpend_block_no_lift (|vl|));;
                                                  isched;;
                                                  (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) ?? mutexpend_pr_not_holder_err (|vl|)??
  mutexpend_nest_err (|vl|) ?? mutexpend_deadlock_err (|vl|)
                              ?? mutexpend_msg_not_null_err (|vl|) ?? mutexpend_cur_prio_eql_mprio_err
                                       (|vl|)
                                       ?? mutexpend_ptcb_prio_eql_idle_err
                                          (|vl|) \/
  s = mutexpend_type_err (|vl|) \/
  s = mutexpend_idle_err (|vl|)
                         ?? mutexpend_stat_err (|vl|)
                         ?? mutexpend_prio_err (|vl|)
                         ?? mutexpend_get_succ (|vl|)
                         ?? (mutexpend_block_lift (|vl|)
                                                  ?? mutexpend_block_no_lift (|vl|));;
                                                  isched;;
                                                  (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) ?? mutexpend_pr_not_holder_err (|vl|)??
  mutexpend_nest_err (|vl|) ?? mutexpend_deadlock_err (|vl|)
                              ?? mutexpend_msg_not_null_err (|vl|) ?? mutexpend_cur_prio_eql_mprio_err
                                       (|vl|)
                                       ?? mutexpend_ptcb_prio_eql_idle_err
                                          (|vl|) \/
  s = mutexpend_idle_err (|vl|) \/
  s = mutexpend_stat_err (|vl|)
                         ?? mutexpend_prio_err (|vl|)
                         ?? mutexpend_get_succ (|vl|)
                         ?? (mutexpend_block_lift (|vl|)
                                                  ?? mutexpend_block_no_lift (|vl|));;
                                                  isched;;
                                                  (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) ?? mutexpend_pr_not_holder_err (|vl|)??
  mutexpend_nest_err (|vl|) ?? mutexpend_deadlock_err (|vl|)
                              ?? mutexpend_msg_not_null_err (|vl|) ?? mutexpend_cur_prio_eql_mprio_err
                                       (|vl|)
                                       ?? mutexpend_ptcb_prio_eql_idle_err
                                          (|vl|)\/
  s = mutexpend_stat_err (|vl|) \/
  s = mutexpend_prio_err (|vl|)
                         ?? mutexpend_get_succ (|vl|)
                         ?? (mutexpend_block_lift (|vl|)
                                                  ?? mutexpend_block_no_lift (|vl|));;
                                                  isched;;
                                                  (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) ?? mutexpend_pr_not_holder_err (|vl|)??
  mutexpend_nest_err (|vl|) ?? mutexpend_deadlock_err (|vl|)
                              ?? mutexpend_msg_not_null_err (|vl|) ?? mutexpend_cur_prio_eql_mprio_err
                                       (|vl|)
                                       ?? mutexpend_ptcb_prio_eql_idle_err
                                          (|vl|) \/
  s = mutexpend_prio_err (|vl|)\/
  s = mutexpend_get_succ (|vl|)
                         ?? (mutexpend_block_lift (|vl|)
                                                  ?? mutexpend_block_no_lift (|vl|));;
                                                  isched;;
                                                  (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) ?? mutexpend_pr_not_holder_err (|vl|)??
  mutexpend_nest_err (|vl|) ?? mutexpend_deadlock_err (|vl|)
                              ?? mutexpend_msg_not_null_err (|vl|) ?? mutexpend_cur_prio_eql_mprio_err
                                       (|vl|)
                                       ?? mutexpend_ptcb_prio_eql_idle_err
                                          (|vl|) \/
  s = mutexpend_get_succ (|vl|) \/
  s = (mutexpend_block_lift (|vl|)
                            ?? mutexpend_block_no_lift (|vl|));;
                            isched;;
                            (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) ?? mutexpend_pr_not_holder_err (|vl|) ??
  mutexpend_nest_err (|vl|) ?? mutexpend_deadlock_err (|vl|)
                              ?? mutexpend_msg_not_null_err (|vl|) ?? mutexpend_cur_prio_eql_mprio_err
                                       (|vl|)
                                       ?? mutexpend_ptcb_prio_eql_idle_err
                                          (|vl|)\/

  s = (mutexpend_block_lift (|vl|)
                            ?? mutexpend_block_no_lift (|vl|));;
                                                              isched;;
                                                              (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) \/
  s = mutexpend_pr_not_holder_err (|vl|) ??
                                  mutexpend_nest_err (|vl|) ?? mutexpend_deadlock_err (|vl|)
                              ?? mutexpend_msg_not_null_err (|vl|) ?? mutexpend_cur_prio_eql_mprio_err
                                       (|vl|)
                                       ?? mutexpend_ptcb_prio_eql_idle_err
                                          (|vl|) \/
  s = mutexpend_pr_not_holder_err (|vl|) \/
  s = mutexpend_nest_err (|vl|) ?? mutexpend_deadlock_err (|vl|)
                         ?? mutexpend_msg_not_null_err (|vl|) ?? mutexpend_cur_prio_eql_mprio_err
                                       (|vl|)
                                       ?? mutexpend_ptcb_prio_eql_idle_err
                                          (|vl|) \/
  s = mutexpend_nest_err (|vl|) \/
  s = mutexpend_deadlock_err (|vl|)
                             ?? mutexpend_msg_not_null_err (|vl|) ?? mutexpend_cur_prio_eql_mprio_err
                                       (|vl|)
                                       ?? mutexpend_ptcb_prio_eql_idle_err
                                          (|vl|) \/
  s = mutexpend_deadlock_err (|vl|) \/
  s = mutexpend_msg_not_null_err (|vl|) ?? mutexpend_cur_prio_eql_mprio_err
                                       (|vl|)
                                       ?? mutexpend_ptcb_prio_eql_idle_err
                                       (|vl|) \/
  s = mutexpend_msg_not_null_err (|vl|) \/
  s = mutexpend_cur_prio_eql_mprio_err
                                       (|vl|)
                                       ?? mutexpend_ptcb_prio_eql_idle_err
                                       (|vl|) \/
  s = mutexpend_cur_prio_eql_mprio_err
        (|vl|) \/
  s = mutexpend_ptcb_prio_eql_idle_err
        (|vl|) \/
  s = mutexpend_block_lift (|vl|)
                            ;;
                            isched;;
                            (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) \/

  s = mutexpend_block_no_lift (|vl|)
                            ;;
                            isched;;
                            (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) \/
  s = spec_done None ;; isched ;;
                            (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) \/
  s = isched ;; (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) \/
  s = (ASSUME sc;; sched) ;;(mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) \/
  s = (spec_done None;;sched) ;; (mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) \/
  s = sched;;(mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) \/
  s = ASSUME nsc;;(mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) \/
  s = spec_done None;;(mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|)) \/
  s = mutexpend_to (|vl|) ?? mutexpend_block_get (|vl|) \/
  s = mutexpend_to (|vl|) \/
  s = mutexpend_block_get (|vl|) \/
  exists v, s = spec_done v.

Definition GoodPost (s:spec_code) vl:=
  s = mutexpost_null (|vl|)
                     ?? mutexpost_no_mutex_err (|vl|)
                     ?? mutexpost_type_err (|vl|)
                     ?? mutexpost_no_owner_err (|vl|)
                     ?? mutexpost_nowt_return_prio_succ (|vl|)
                                                         ?? mutexpost_nowt_no_return_prio_succ (|vl|)

                                                           ?? (mutexpost_exwt_return_prio_succ (|vl|)
                                                              ?? mutexpost_exwt_no_return_prio_succ (|vl|))
                                                         ;;isched;; END Some (V$NO_ERR)??
                     mutexpost_original_not_holder_err (|vl|) ??
                     mutexpost_prio_err (|vl|) ?? mutexpost_wl_highest_prio_err (|vl|) \/
  s = mutexpost_null (|vl|) \/
  s = mutexpost_no_mutex_err (|vl|)
                             ?? mutexpost_type_err (|vl|)
                             ?? mutexpost_no_owner_err (|vl|)
                             ?? mutexpost_nowt_return_prio_succ (|vl|)
                                                                  ?? mutexpost_nowt_no_return_prio_succ (|vl|)
                                                                  ?? (mutexpost_exwt_return_prio_succ (|vl|)
                                                                  ?? mutexpost_exwt_no_return_prio_succ (|vl|))
                                   ;;isched;; END Some (V$NO_ERR)??
                     mutexpost_original_not_holder_err (|vl|) ??
                     mutexpost_prio_err (|vl|) ?? mutexpost_wl_highest_prio_err (|vl|) \/
  s = mutexpost_no_mutex_err (|vl|) \/
  s = mutexpost_type_err (|vl|)
                         ?? mutexpost_no_owner_err (|vl|)
                         ?? mutexpost_nowt_return_prio_succ (|vl|)
                                                              ?? mutexpost_nowt_no_return_prio_succ (|vl|)
                                                              ?? (mutexpost_exwt_return_prio_succ (|vl|)
                                                              ?? mutexpost_exwt_no_return_prio_succ (|vl|))
                               ;;isched;; END Some (V$NO_ERR)??
                     mutexpost_original_not_holder_err (|vl|) ??
                     mutexpost_prio_err (|vl|) ?? mutexpost_wl_highest_prio_err (|vl|)\/
  s = mutexpost_type_err (|vl|) \/
  s = mutexpost_no_owner_err (|vl|)
                             ?? mutexpost_nowt_return_prio_succ (|vl|)
                                                                  ?? mutexpost_nowt_no_return_prio_succ (|vl|)
                                                                  ?? (mutexpost_exwt_return_prio_succ (|vl|)
                                                                  ?? mutexpost_exwt_no_return_prio_succ (|vl|))
                                   ;;isched;; END Some (V$NO_ERR)??
                     mutexpost_original_not_holder_err (|vl|) ??
                     mutexpost_prio_err (|vl|) ?? mutexpost_wl_highest_prio_err (|vl|) \/
  s = mutexpost_no_owner_err (|vl|) \/
  s = mutexpost_nowt_return_prio_succ (|vl|)
                                        ?? mutexpost_nowt_no_return_prio_succ (|vl|)
                                        ?? (mutexpost_exwt_return_prio_succ (|vl|)
                                        ?? mutexpost_exwt_no_return_prio_succ (|vl|))
         ;;isched;; END Some (V$NO_ERR)??
                     mutexpost_original_not_holder_err (|vl|) ??
                     mutexpost_prio_err (|vl|) ?? mutexpost_wl_highest_prio_err (|vl|) \/
  s = mutexpost_nowt_return_prio_succ (|vl|) \/
  s = mutexpost_nowt_no_return_prio_succ (|vl|)
                                        ?? (mutexpost_exwt_return_prio_succ (|vl|)
                                        ?? mutexpost_exwt_no_return_prio_succ (|vl|))
         ;;isched;; END Some (V$NO_ERR) ?? mutexpost_original_not_holder_err (|vl|) ??
                     mutexpost_prio_err (|vl|) ?? mutexpost_wl_highest_prio_err (|vl|) \/
  s = mutexpost_nowt_no_return_prio_succ (|vl|) \/
  s = (mutexpost_exwt_return_prio_succ (|vl|)
                                        ?? mutexpost_exwt_no_return_prio_succ (|vl|))
         ;;isched;; END Some (V$NO_ERR) ?? mutexpost_original_not_holder_err (|vl|) ??
                     mutexpost_prio_err (|vl|) ?? mutexpost_wl_highest_prio_err (|vl|)\/
  s = (mutexpost_exwt_return_prio_succ (|vl|)
                                        ?? mutexpost_exwt_no_return_prio_succ (|vl|))
       ;;isched;; END Some (V$NO_ERR) \/
  s = mutexpost_original_not_holder_err (|vl|) ??
                                        mutexpost_prio_err (|vl|) ?? mutexpost_wl_highest_prio_err (|vl|) \/
  s = mutexpost_exwt_return_prio_succ (|vl|);;isched;; END Some (V$NO_ERR) \/
  s = mutexpost_exwt_no_return_prio_succ (|vl|);;isched;; END Some (V$NO_ERR) \/
  s = spec_done None ;;isched;; END Some (V$NO_ERR) \/
  s = isched;; END Some (V$NO_ERR) \/
  s = (ASSUME sc;; sched) ;; END Some (V$NO_ERR) \/
  s = (spec_done None;;sched) ;;END Some (V$NO_ERR) \/
  s = sched;; END Some (V$NO_ERR) \/
  s = ASSUME nsc;;END Some (V$NO_ERR) \/
  s = END None;;END Some (V$NO_ERR) \/
  s = mutexpost_original_not_holder_err (|vl|) \/
  s = mutexpost_prio_err (|vl|) ?? mutexpost_wl_highest_prio_err (|vl|) \/
  s = mutexpost_prio_err (|vl|) \/
  s = mutexpost_wl_highest_prio_err (|vl|) \/
  exists v, s = spec_done v.

Definition GoodTick s:=
  s = timetick_spec (|nil|);;
                    ((isched;; END None)
                            ?? END None) \/
  s = spec_done None;;
                    ( (isched;; END None)
                            ?? END None) \/
  s = ( (isched;; END None)
                            ?? END None) \/
  s = (isched;; END None) \/
  s = (ASSUME sc;; sched) ;; END None \/
  s = (spec_done None;;sched) ;;END None \/
  s = sched;; END None \/
  s = ASSUME nsc;;END None \/
  s = spec_done None;;END None \/
  exists v, s = spec_done v.

Definition GoodToy s:=
  s = toyint_spec (|nil|);;
                    ((isched;; END None)
                            ?? END None) \/
  s = spec_done None;;
                    ( (isched;; END None)
                            ?? END None) \/
  s = ( (isched;; END None)
                            ?? END None) \/
  s = (isched;; END None) \/
  s = (ASSUME sc;; sched) ;; END None \/
  s = (spec_done None;;sched) ;;END None \/
  s = sched;; END None \/
  s = ASSUME nsc;;END None \/
  s = spec_done None;;END None \/
  exists v, s = spec_done v.

Definition good_api_stmt s:=
  (exists vl, GoodAcc s vl) \/
  (exists vl, GoodCre s vl) \/
  (exists vl, GoodDel s vl) \/
  (exists vl, GoodPend s vl) \/
  (exists vl, GoodPost s vl) \/
  ( GoodTick s ) \/
  ( GoodToy s ).

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

Definition goodeval_h (c:cureval):=
  match c with
    | cure _ => True
    | curs s => goodstmt_h s
  end.

Fixpoint goodks_h ks:=
  match ks with
    | kint _ _ _ _ => False
    | kevent c ke ks´ => goodeval_h c /\ goodks_h ks´
    | kstop => True
    | kcall _ s _ ks´ => goodks_h ks´ /\ goodstmt_h s
    | kseq s ks´ => goodks_h ks´ /\ goodstmt_h s
    | kassignr _ _ ks´ => goodks_h ks´
    | kassignl _ _ ks´ => goodks_h ks´
    | kfuneval _ _ _ _ ks´ => goodks_h ks´
    | kif s1 s2 ks´ => goodks_h ks´ /\ goodstmt_h s1 /\ goodstmt_h s2
    | kwhile _ s ks´ => goodks_h ks´ /\ goodstmt_h s
    | kret ks´ => goodks_h ks´
  end.

Definition goodcode_h (c:code):=
  match c with
    | (c,(ke,ks)) => goodeval_h c /\ goodks_h ks
  end.

Definition goodtasks_h T:=
  forall t c, TasksMod.get T t = Some c -> goodcode_h c.

Definition no_nest_client (client_code:progunit) O T cst:=
  forall T´ cst´ O´,
    hpstepstar (client_code, os_spec´) T cst O T´ cst´ O´ ->
    NO_NEST_PENDING_O O´.

Definition good_client_code client_code :=
      (forall (f : fid) (a : type) (b c : decllist) (s : stmts),
       client_code f = Some (a, b, c, s) -> GoodStmt_h s).

Definition INV_PROP (client_code:progunit) O T cst :=
  good_client_code client_code /\ no_nest_client client_code O T cst /\ GOOD_ST O.

Definition apibound (api: fid -> option osapi) T (O:osabst) : Prop :=
  exists t C ks cd f tl,
         exists (s:spec_code) tp vl,
     OSAbstMod.get O curtid = Some (oscurt t) /\
     TasksMod.get T t = Some C /\
     C = (curs (hapi_code (cd vl)), (kenil,ks))
     /\ api f = Some (cd, (tp,tl)) /\ s = cd vl.

Definition intbound (ints : hid -> option int_code)
           (T : TasksMod.map) (O:osabst) : Prop :=
  exists cd h t ke ks c s C,
      OSAbstMod.get O curtid = Some (oscurt t) /\
      TasksMod.get T t = Some C /\
      C = (curs (hapi_code s), (kenil, kevent c ke ks))
       /\ ints h = Some cd /\ s = cd.

Lemma good_clt_imp :
  forall C pc, good_clt C pc ->
      ~(exists s´ ke´ ks´, C = (curs (hapi_code s´), (ke´,ks´))).

Lemma cstep_good_clt_hold:
  forall pc C m C´ m´ ,
    good_clt C pc ->
    cstep pc C m C´ m´ ->
    good_clt C´ pc.

 Definition nhapi T pc :=
   forall t C, TasksMod.get T t = Some C -> good_clt C pc .

 Lemma nhapi_set_hold:
   forall T C t pc,
     nhapi T pc->
     good_clt C pc ->
     nhapi (TasksMod.set T t C) pc.

Lemma cstep_nhapi_hold:
  forall pc C m C´ m´ t T,
    nhapi T pc->
    cstep pc C m C´ m´ ->
    TasksMod.get T t = Some C ->
    nhapi (TasksMod.set T t C´) pc.

Ltac destruct_inverts1 H:=
  let Hx:= fresh in
  match type of H with
    | ?H1 \/ ?H2 => destruct H as [Hx | H]; [inverts Hx | destruct_inverts1 H]
    | exists _, _ = _ => let x:= fresh in (destruct H as (x&H);inverts H)
    | _ => idtac
  end.

Lemma callcont_goodks:
  forall ks f s le ks´,
    callcont ks = Some (kcall f s le ks´) ->
    goodks_h ks ->
    goodks_h ks´.

Lemma hapistep_goodcode:
  forall C O c O´,
    goodcode_h C->
    goodcode_h C ->
    goodcode_h C ->
    goodcode_h C ->
    goodcode_h C ->
    goodcode_h C ->
    goodcode_h C ->
    hapistep os_spec´ C O c O´ ->
    goodcode_h c.

Lemma htstep_goodcode_h:
  forall pc t C cst O c cst´ O´,
    good_client_code pc ->
    htstep (pc, os_spec´) t C cst O c cst´ O´ ->
    goodcode_h C ->
    goodcode_h c.

Lemma hpstep_goodcode_h:
  forall pc T cst O T´ cst´ O´,
    goodtasks_h T ->
    good_client_code pc ->
    hpstep (pc,os_spec´) T cst O T´ cst´ O´ ->
    goodtasks_h T´.

Lemma hpstepstar_goodcode_h:
  forall pc T cst O T´ cst´ O´,
    hpstepstar (pc,os_spec´) T cst O T´ cst´ O´ ->
    goodtasks_h T ->
    good_client_code pc ->
    goodtasks_h T´.

Lemma hpstep_goodcode_goodapi:
  forall pc T cst O T´ cst´ O´,
    goodtasks_h T ->
    good_client_code pc ->
    hpstep (pc,os_spec´) T cst O T´ cst´ O´ ->
    O = O´ \/ GOOD_API_CODE O T.

Lemma init_goodks_h:
  forall T client_code cst O,
    InitTasks T client_code cst O ->
    INV_PROP client_code O T cst ->
    goodtasks_h T .

Lemma code_exe_prop1:
  forall client_code T cst O T´ cst´ O´ T´´ O´´ cst´´,
    good_client_code client_code ->
    goodtasks_h T ->
    hpstepstar (client_code, os_spec´) T cst O T´ cst´ O´ ->
    hpstep (client_code, os_spec´) T´ cst´ O´ T´´ cst´´ O´´->
    O´ = O´´ \/ GOOD_API_CODE O´ T´.

Lemma tcbjoinsig_set_sub_sub:
  forall t x tcbls tcbls´ tls y tls´,
    TcbMod.joinsig t x tcbls tcbls´ ->
    TcbMod.set tls t y = tls´ ->
    TcbMod.sub tcbls´ tls ->
    TcbMod.sub tcbls tls´.

Lemma sub_joinsig_get:
  forall tls_used tls t x tls_used´,
    TcbMod.sub tls_used tls -> TcbMod.joinsig t x tls_used´ tls_used -> TcbMod.get tls t = Some x.

Lemma tickchange_goodst:
  forall tls els tls´ els´ st´ t0 p st msg0,
    NO_NEST_PENDING tls els ->
    TcbMod.get tls t0 = Some (p, st, msg0)->
    (rdy_notin_wl tls els /\

     owner_prio_prop tls els /\
     task_stat_prop tls /\
     op_p_prop tls els /\
     wait_prop tls els /\ no_owner_prio_prop tls els) ->
    tickchange t0 st els st´ els´ ->
    TcbMod.set tls t0 (p, st´, msg0) = tls´ ->
    (rdy_notin_wl tls´ els´ /\

     owner_prio_prop tls´ els´ /\
     task_stat_prop tls´ /\
     op_p_prop tls´ els´ /\ wait_prop tls´ els´ /\ no_owner_prio_prop tls´ els´
    ).

Lemma tickstep_goodst:
  forall tls els tls´ els´ tls_sub,
    TcbMod.sub tls_sub tls ->
    tickstep´ tls els tls´ els´ tls_sub ->
    NO_NEST_PENDING tls els ->
    NO_NEST_PENDING tls´ els´ ->
    (rdy_notin_wl tls els /\
     owner_prio_prop tls els /\
     task_stat_prop tls /\
     op_p_prop tls els /\
     wait_prop tls els /\ no_owner_prio_prop tls els) ->
    rdy_notin_wl tls´ els´ /\
    owner_prio_prop tls´ els´ /\
    task_stat_prop tls´ /\
    op_p_prop tls´ els´ /\
    wait_prop tls´ els´ /\
    no_owner_prio_prop tls´ els´.

Lemma code_exe_prop2:
  forall client_code T´ cst´ O´ T´´ O´´ cst´´,
    O´ = O´´ \/ GOOD_API_CODE O´ T´ ->
    NO_NEST_PENDING_O O´ ->
    GOOD_ST O´ ->
    hpstep (client_code, os_spec´) T´ cst´ O´ T´´ cst´´ O´´->
    NO_NEST_PENDING_O O´´ ->
    GOOD_ST O´´.


Lemma timetick_weakpif:
  forall tls tls0 els els0 tlsx ct t p_ct p_t,
    (rdy_notin_wl tls els /\

         owner_prio_prop tls els /\
         task_stat_prop tls /\
         op_p_prop tls els /\ wait_prop tls els /\ no_owner_prio_prop tls els) ->
    TcbMod.sub tlsx tls ->
    (forall p_ct´,
       GET_OP ct tls els p_ct´ ->
       NO_NEST_PENDING tls els ->
       HighestRdy tls ct ->
        ~ (exists eid, IS_OWNER ct eid els) ->
       forall (t0 : addrval) (p_t0 : int32),
         t0 <> ct ->
         TcbMod.get tls t0 <> None ->
         GET_OP t0 tls els p_t0 ->
         IS_WAITING t0 els -> Int.ltu p_ct´ p_t0 = true) ->
    t <> ct ->
    TcbMod.get tls0 t <> None ->
    GET_OP ct tls0 els0 p_ct ->
    GET_OP t tls0 els0 p_t ->
    NO_NEST_PENDING tls els ->
    NO_NEST_PENDING tls0 els0 ->
    HighestRdy tls0 ct ->
    ~ (exists eid, IS_OWNER ct eid els0) ->
    IS_WAITING t els0 ->
    tickstep´ tls els tls0 els0 tlsx ->
    Int.ltu p_ct p_t = true.

Theorem no_nest_pif:
  forall client_code T cst O T´ cst´ O´,
    NO_NEST_PENDING_O O ->
    NO_NEST_PENDING_O O´ ->
    (O = O´ \/ (GOOD_API_CODE O T)) ->
    GOOD_ST O ->
    WEAK_PIF O ->
    hpstep (client_code, os_spec´) T cst O T´ cst´ O´ ->
    WEAK_PIF O´.
        Lemma set_getop_eq:
          forall ct tls x4 x3 x6 x7 p_ct x0 x1,
            TcbMod.get tls ct = Some (p_ct, x0, x1) ->
            EcbMod.get x4 x3 = Some (absmutexsem x6 None, x7) ->
            GET_OP ct tls (EcbMod.set x4 x3 (absmutexsem x6 (Some (ct, p_ct)), x7)) p_ct ->
            NO_NEST_PENDING tls
                            (EcbMod.set x4 x3 (absmutexsem x6 (Some (ct, p_ct)), x7)) ->
            GET_OP ct tls x4 p_ct.















































































Qed.

Lemma no_nest_prop_step_hold:
  forall client_code T cst O T´ cst´ O´ ,
    no_nest_client client_code O T cst ->
    hpstep (client_code, os_spec´) T cst O T´ cst´ O´ ->
    no_nest_client client_code O´ T´ cst´.

Lemma hpstep_inv_prop_hold:
  forall client_code T cst O T´ cst´ O´ ,
    goodtasks_h T ->
    hpstep (client_code, os_spec´) T cst O T´ cst´ O´ ->
    INV_PROP client_code O T cst ->
    INV_PROP client_code O´ T´ cst´.

Lemma hpstep_wpif_hold:
  forall client_code T cst O T´ cst´ O´,
    goodtasks_h T ->
    INV_PROP client_code O T cst ->
    WEAK_PIF O ->
    hpstep (client_code, os_spec´) T cst O T´ cst´ O´ ->
    WEAK_PIF O´.

Lemma hpstep_pif_hold
: forall (client_code : progunit) (T : TasksMod.map)
         (cst : clientst) (O : osabst) (T´ : tasks)
         (cst´ : clientst) (O´ : osabst),
    goodtasks_h T ->
    INV_PROP client_code O T cst ->
    PIF_aux O ->
    hpstep (client_code, os_spec´) T cst O T´ cst´ O´ -> PIF_aux O´.

Theorem Priority_Inversion_Free_Prop:
  forall client_code T cst O T´ cst´ O´,
    InitTasks T client_code cst O ->
    INV_PROP client_code O T cst ->
    hpstepstar (client_code, os_spec´) T cst O T´ cst´ O´ ->
    PIF_aux O ->
    PIF_aux O´.

Theorem GOOD_ST_Prop´:
  forall client_code T cst O T´ cst´ O´,
    goodtasks_h T ->
    good_client_code client_code ->
    GOOD_ST O->
    good_client_code client_code ->
    no_nest_client client_code O T cst ->
    hpstepstar (client_code, os_spec´) T cst O T´ cst´ O´ ->
    GOOD_ST O´.

Lemma init_goodks_h´:
  forall T client_code cst O,
    InitTasks T client_code cst O ->
    good_client_code client_code ->
    goodtasks_h T .


Theorem GOOD_ST_Prop:
  forall client_code T cst O T´ cst´ O´,
    InitTasks T client_code cst O ->
    init_st O ->
    good_client_code client_code ->
    no_nest_client client_code O T cst ->
    hpstepstar (client_code, os_spec´) T cst O T´ cst´ O´ ->
    GOOD_ST O´.