Library OSMutex_common

Require Import ucert.
Require Export lab.
Require Import OSQPendPure.
Require Import OSQPostPure.
Require Import mathlib.
Open Scope code_scope.

Definition ProtectWrapper (a:Type) : Type :=a.
Lemma MakeProtectWrapper : forall H, H -> ProtectWrapper H.
Ltac protect H := let H´ := fresh in rename H into H´; lets H : MakeProtectWrapper H´; clear H´.
Ltac unprotect H := unfold ProtectWrapper in H.

      Lemma Zland_le_l: forall a b, 0<=a -> Z.land a b <= a.

      Lemma Zland_le_r: forall a b, 0<=b -> Z.land a b <= b.

      Lemma tblemma1 : forall i, 0<=i<8 -> Z.testbit 255 i = true.

      Lemma tblemma2 : forall i, 0<=i<8 -> Z.testbit 65280 i = false.

      Lemma tblemma4 : forall i x, 0<=x -> Z.testbit x i = true -> 2^i <= x.

      Lemma tblemma3 : forall i x, 0<=x<=255 -> i>=8 -> Z.testbit x i = false.

Lemma int_auxxx:
  forall x0,
    Int.unsigned x0 <= 65535 ->
    Int.unsigned (Int.or x0 ($ OS_MUTEX_AVAILABLE)) <= 65535.

      Lemma acpt_intlemma8: forall x, Int.or x ($ 0) = x.

Lemma int_aux´:
  forall x0,
    Int.unsigned x0 <= 65535 ->
    x0>>ᵢ$ 8 = (Int.or x0 ($ OS_MUTEX_AVAILABLE))>>ᵢ$ 8.

Lemma intandcomm : forall x y, Int.and x y = Int.and y x.

Lemma intorcomm : forall x y, Int.or x y = Int.or y x.

Lemma int_aux´´:
  forall x0,
    Int.unsigned x0 <= 65535 ->
    Int.or x0 ($ OS_MUTEX_AVAILABLE)&$ OS_MUTEX_KEEP_LOWER_8 =
    $ OS_MUTEX_AVAILABLE.

Lemma RLH_ECBData_P_or_available :
  forall x,
    Int.unsigned x <= 65535 ->
    Int.unsigned (x>>ᵢ$ 8) < 64 ->
    RLH_ECBData_P (DMutex (Vint32 (Int.or x ($ OS_MUTEX_AVAILABLE))) Vnull)
                  (absmutexsem (x>>ᵢ$ 8) None, nil).

Lemma del_intlemma1 :forall x, Int.unsigned (Int.shru x ($ 8)) < 64-> (if Int.unsigned (Int.modu (Int.shru x ($ 8)) ($ Byte.modulus)) <=?
                                                                           Byte.max_unsigned
                                                                        then true
                                                                        else false) = true.

Lemma del_intlemma2: forall x, Int.unsigned (Int.shru x ($ 8)) < 64 -> Int.unsigned (Int.modu (Int.shru x ($ 8)) ($ Byte.modulus)) < Z.of_nat 64.
  Require Import mathlib.

Lemma mutexdel_intlemma1: forall x, Int.unsigned (Int.shru x ($ 8)) < 64 -> (Int.modu (Int.shru x ($ 8)) ($ Byte.modulus)) = Int.shru x ($ 8).
  Require Import mathlib.


Lemma ecbmod_get_or : forall ma a, EcbMod.get ma a = None \/ exists b, EcbMod.get ma a = Some b.

Lemma ecbmod_indom_eq_join_eq: forall ma mb ma´ mb´ mab, (forall a, EcbMod.indom ma a <-> EcbMod.indom ma´ a) -> EcbMod.join ma mb mab -> EcbMod.join ma´ mb´ mab -> ma = ma´.
    Lemma indom_join_a2b: forall ma ma´ mb mb´ mc, EcbMod.join ma mb mc -> EcbMod.join ma´ mb´ mc -> (forall a, EcbMod.indom mb a <-> EcbMod.indom mb´ a) -> (forall a, EcbMod.indom ma a <-> EcbMod.indom ma´ a).

    Lemma sig_indom_eq´: forall key val val´ a, EcbMod.indom (EcbMod.sig key val) a -> EcbMod.indom (EcbMod.sig key val´) a.

    Lemma sig_indom_eq: forall key val val´ a, EcbMod.indom (EcbMod.sig key val) a <-> EcbMod.indom (EcbMod.sig key val´) a.

  Lemma ecb_join_sig_eq: forall x x´ key val val´ y, EcbMod.join x (EcbMod.sig key val) y -> EcbMod.join x´ (EcbMod.sig key val´) y -> x´ = x.

  Lemma del_ecbmod_join_lemma0 : forall ma mb mc md me key val val´, EcbMod.join ma (EcbMod.sig key val) me -> EcbMod.join mb (EcbMod.sig key val´) mc -> EcbMod.join mc md me -> EcbMod.join mb md ma.

  Lemma mutex_no_owner_nil_wls : forall x e w0, RLH_ECBData_P (DMutex (Vint32 x) Vnull) (e, w0) -> w0=nil.

  Lemma mutex_no_owner_nil_wls´: forall x w, RH_ECB_P (absmutexsem x None, w) -> w=nil.

  Lemma R_ECB_ETbl_P_high_ecb_mutex_acpt_hold :
    forall x9 i x x3 v´44 v´42 v´37 i6 v´50,
      R_ECB_ETbl_P x9
                   (V$OS_EVENT_TYPE_MUTEX
                     :: Vint32 i :: Vint32 x :: Vnull :: x3 :: v´44 :: nil, v´42) v´37 ->
      R_ECB_ETbl_P x9
                   (V$OS_EVENT_TYPE_MUTEX
                     :: Vint32 i
                     :: Vint32 (Int.or (x&$ OS_MUTEX_KEEP_UPPER_8) i6)
                     :: Vptr (v´50, Int.zero) :: x3 :: v´44 :: nil, v´42) v´37.

  Lemma ecb_sig_join_sig´_set : forall a b c d b´, EcbMod.joinsig a b c d -> EcbMod.joinsig a b´ c (EcbMod.set d a b´).
  Lemma val_inj_eq
  : forall i0 a: int32,
      val_inj
        (notint
           (val_inj
              (if Int.eq i0 a
               then Some (Vint32 Int.one)
               else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
      val_inj
        (notint
           (val_inj
              (if Int.eq i0 a
               then Some (Vint32 Int.one)
               else Some (Vint32 Int.zero)))) = Vnull ->
      i0 = a.

  Lemma or_true_ltrue_rtrue: forall x y, val_inj (bool_or (val_inj (Some x)) (val_inj (Some y))) <> Vint32 Int.zero -> x <> Vint32 Int.zero \/ y <> Vint32 Int.zero.

  Lemma val_inj_or : forall (a b: bool),
                       val_inj
                         (if b
                          then Some (Vint32 Int.one)
                          else Some (Vint32 Int.zero)) <> Vint32 Int.zero \/
                       val_inj
                         (if a
                          then Some (Vint32 Int.one)
                          else Some (Vint32 Int.zero)) <> Vint32 Int.zero ->
                       a = true \/ b= true.

  Lemma le65535shr8mod255self:forall i1, Int.unsigned i1 <= 65535 -> (Int.modu (Int.shru i1 ($ 8)) ($ Byte.modulus)) = (Int.shru i1 ($ 8)).

  Lemma acpt_int_lemma00 : forall i1, Int.unsigned (i1 & $ OS_MUTEX_KEEP_UPPER_8) <= 65535.

  Lemma acpt_int_lemma0 : forall i1, Int.unsigned i1 <= 65535 -> Int.unsigned (i1 & $ OS_MUTEX_KEEP_UPPER_8) <= 65535.

  Lemma acpt_intlemma1 : forall i1, Int.unsigned i1 <= 65535 -> Int.unsigned (Int.modu (Int.shru i1 ($ 8)) ($ Byte.modulus)) <= Byte.max_unsigned.

  Lemma acpt_intlemma2: forall i1, val_inj
                                      (if Int.eq (i1&$ OS_MUTEX_KEEP_LOWER_8) ($ OS_MUTEX_AVAILABLE)
                                       then Some (Vint32 Int.one)
                                       else Some (Vint32 Int.zero)) <> Vint32 Int.zero -> i1 &$ OS_MUTEX_KEEP_LOWER_8 = $ OS_MUTEX_AVAILABLE.

    Lemma acpt_intlemma3: forall x y,Int.unsigned x<64 -> Int.or (y&$ OS_MUTEX_KEEP_UPPER_8) x&$ OS_MUTEX_KEEP_LOWER_8 = x.

    Lemma acpt_intlemma7: forall y, Int.unsigned y < 64 -> Int.shru y ($ 8) = $0.

  Lemma acpt_intlemma9: forall i6 x, Int.unsigned i6 < 64-> Int.ltu (Int.shru x ($ 8)) i6 = true-> Int.unsigned x <= 65535.

  Lemma acpt_intlemma10: forall x ,Int.unsigned x <= 65535 -> Int.unsigned (Int.shru x ($ 8)) <= 255.

    Lemma acpt_intlemma4: forall x y,Int.unsigned x <= 65535 -> Int.unsigned y <64 ->(Int.shru (Int.or (x&$ OS_MUTEX_KEEP_UPPER_8) y) ($ 8)) = Int.shru x ($ 8).

    Lemma acpt_intlemma5 : forall x i6, Int.unsigned i6 <64 -> Int.or (x&$ OS_MUTEX_KEEP_UPPER_8) i6&$ OS_MUTEX_KEEP_LOWER_8 = $ 255 -> False.

        Lemma acpt_intlemma15: forall n, Z.log2 (two_power_nat n) = Z_of_nat n.
      Lemma acpt_intlemma14: forall a n,a>0 ->( a< two_power_nat n <-> (forall x, x >= Z_of_nat n -> Z.testbit a x = false)).

    Lemma acpt_intlemma12 : forall a b n, a < two_power_nat n -> b < two_power_nat n -> Z.lor a b < two_power_nat n.
  Lemma acpt_intlemma6: forall x p, Int.unsigned p<=65535 -> Int.unsigned (Int.or (x&$ OS_MUTEX_KEEP_UPPER_8) p) <= 65535.

  Lemma intlemma13 : forall x y, Int.unsigned x < Int.unsigned y -> Int.modu x y = x.

  Lemma intlemma11:forall x x0, val_inj
                                  (bool_or
                                     (val_inj
                                        (if Int.ltu x0 x
                                         then Some (Vint32 Int.one)
                                         else Some (Vint32 Int.zero)))
                                     (val_inj
                                        (if Int.eq x0 x
                                         then Some (Vint32 Int.one)
                                         else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
                                val_inj
                                  (bool_or
                                     (val_inj
                                        (if Int.ltu x0 x
                                         then Some (Vint32 Int.one)
                                         else Some (Vint32 Int.zero)))
                                     (val_inj
                                        (if Int.eq x0 x
                                         then Some (Vint32 Int.one)
                                         else Some (Vint32 Int.zero)))) = Vnull -> Int.ltu (x) x0 = true.

Lemma eventtype_neq_mutex:
  forall v´38 v´21 i1 i0 i2 x2 x3 v´42 v´40 v´22 v´23 v´41 v´24 v´34 v´35 v´49 s P v´43 v´45 v´44 v´46,
    length v´21 = length v´23->
    ECBList_P v´38 Vnull
              (v´21 ++
                    ((Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil,
                      v´40) :: nil) ++ v´22) (v´23 ++ (v´41 :: nil) ++ v´24) v´34 v´35 ->
    ECBList_P v´38 (Vptr (v´49, Int.zero)) v´21 v´23 v´43 v´35 ->
    EcbMod.join v´43 v´45 v´34 ->
    EcbMod.joinsig (v´49, Int.zero) v´46 v´44 v´45 ->
    false = Int.eq i1 ($ OS_EVENT_TYPE_MUTEX) ->
    s|= AEventData
     (Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 ** P ->
    s |= AEventData
      (Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 **
      [|~ exists x y z, EcbMod.get v´34 (v´49,Int.zero) = Some (absmutexsem x y, z) |] ** P.
  Lemma Mutex_owner_set´ : forall x y z w u ,
                              RH_TCBList_ECBList_MUTEX_OWNER x y ->
                              RH_TCBList_ECBList_MUTEX_OWNER (EcbMod.set x z (absmutexsem w None, u)) y.

  Lemma mutex_ex_wt_ex_owner :forall i0 o x4 x5, RH_ECB_P (absmutexsem i0 o, x4 :: x5) -> exists yy, o= Some yy.
Goal forall x, val_inj
     (if Int.ltu ($ 8) Int.iwordsize then Some (Vint32 x) else None) =
   Vint32 x.
    Goal forall x, Int.ltu Int.zero x = false -> x= Int.zero.
  Goal forall x y , val_inj (bool_or x y ) =Vint32 Int.zero \/ val_inj (bool_or x y) = Vnull ->
x = Vint32 Int.zero /\ y = Vint32 Int.zero.
  Goal forall x y,
         val_inj
           (notint
              (val_inj
                 (if Int.eq x y
                  then Some (Vint32 Int.one)
                  else Some (Vint32 Int.zero)))) = Vint32 Int.zero -> x= y.
    Goal forall ls x, (x< length ls)%nat -> exists t, nth_val x ls = Some t.

        Lemma post_intlemma3 : forall x1, Int.unsigned x1 < 64 -> Int.unsigned (Int.shru x1 ($ 3)) < 8.
    Lemma post_intlemma4 : forall x1, Int.unsigned x1 < 64 -> Int.unsigned (Int.and x1 ($ 7)) < 8.

    Lemma postintlemma1 : forall x, (if Int.unsigned (Int.modu x ($ Byte.modulus)) <=?
                                         Byte.max_unsigned
                                      then true
                                      else false) = true.

    Lemma postintlemma2 : forall x, Int.unsigned (Int.modu x ($ Byte.modulus)) <=?
                                         Byte.max_unsigned =true.

    Lemma postintlemma3 : forall x, Int.unsigned (x&$ OS_MUTEX_KEEP_LOWER_8) <= 255.

    Lemma postintlemma4 : Int.ltu ($ 3) Int.iwordsize = true.

    Lemma osmapvallist_int8u : (array_type_vallist_match Int8u OSMapVallist).
    Lemma osmapvallist_length8 : length OSMapVallist = 8%nat.

    Lemma intlt2nat: forall x y, Int.unsigned x < y -> (Z.to_nat (Int.unsigned x) < Z.to_nat y)%nat.

    Lemma intlt2intlt: forall x y, Int.unsigned x < y -> Int.unsigned x < Z.of_nat (Z.to_nat y).

    Lemma ruletypevalmatch8u : forall x, rule_type_val_match Int8u x = true ->exists tt, x = Vint32 tt /\ Int.unsigned tt <= 255.

    Lemma mutexpost_intlemma1: forall x, Int.unsigned x < 64 -> (Int.modu x ($ Byte.modulus)) = x.

    Lemma int8ule255: forall x2, true = rule_type_val_match Int8u (Vint32 x2) -> Int.unsigned x2 <=255.

    Lemma postintlemma2´ : forall x, Int.unsigned (Int.modu x ($ Byte.modulus)) <=255.
    Lemma ifE : forall e:bool, (if e then true else false) = true <-> e = true.

    Lemma seporI : forall P Q, P ==> P\\//Q.

    Lemma seporI´ : forall P Q, Q ==> P\\//Q.

    Lemma RH_TL_EL_MUTEX_OWNER_hold: forall tls tid els eid prio st msg o1 pp w1 w2 pr, TcbMod.get tls tid = Some (prio, st, msg) -> EcbMod.get els eid = Some (absmutexsem pr o1, w1) -> RH_TCBList_ECBList_MUTEX_OWNER els tls -> RH_TCBList_ECBList_MUTEX_OWNER (EcbMod.set els eid (absmutexsem pr (Some (tid, pp)), w2)) tls.


Lemma post_exwt_succ_pre_mutex
     : forall (v´36 v´13 : vallist) (v´12 : int32)
         (v´32 : block) (v´15 : int32) (v´24 : block)
         (v´35 v´0 : val) (v´8 : tid) (v´9 v´11 : EcbMod.map)
         (x : val) (x0 : maxlen) (x1 : waitset)
         (v´6 v´10 : EcbMod.map) (v´38 v´69 v´39 : int32)
         (v´58 : block) (b : taskstatus)
         (c :msg) (v´62 v´7 : TcbMod.map)
         (vhold : addrval) pr o a,
       v´12 <> Int.zero ->
       R_PrioTbl_P v´36 v´7 vhold ->
       RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
       R_ECB_ETbl_P (v´32, Int.zero)
         (V$OS_EVENT_TYPE_MUTEX
          :: Vint32 v´12
             :: Vint32 v´15 :: Vptr (v´24, Int.zero) :: v´35 :: v´0 :: nil,
         v´13) v´7 ->
       RH_TCBList_ECBList_P v´11 v´7 v´8 ->
       EcbMod.join v´9 v´10 v´11 ->
       EcbMod.joinsig (v´32, Int.zero) (absmutexsem pr o , x1) v´6 v´10 ->
       Int.unsigned v´12 <= 255 ->
       array_type_vallist_match Int8u v´13 ->
       length v´13 = ∘OS_EVENT_TBL_SIZE ->
       nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
       Int.unsigned v´38 <= 7 ->
       nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
       Int.unsigned v´69 <= 255 ->
       nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
       Int.unsigned v´39 <= 7 ->
       nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 =
       Vptr (v´58, Int.zero) ->
       TcbJoin (v´58, Int.zero) (a, b, c) v´62 v´7 ->
       a = (v´38<<$ 3)+ᵢv´39/\ x1 <> nil /\
       GetHWait v´7 x1 (v´58, Int.zero) /\
       TcbMod.get v´7 (v´58, Int.zero) = Some (a, b, c)
.

Ltac hoare_assign_struct´ :=
  let s := fresh in
  let H := fresh in
  match goal with
  | |- {|_ , _, _, _, _|}|- {{?P}}?x ′ → _ =ₑ _ {{_}} =>
        match find_lvarmapsto P x with
        | some ?m =>
            match find_aop P with
            | none _ => fail 1
            | some ?n =>
                hoare lifts (n :: m :: nil) pre;
                 match goal with
                 | |-
                   {|_ , _, _, _, _|}|-
                   {{ <|| _ ||> ** LV x @ _ ∗ |-> Vptr ?l ** ?P´}}_ {{_}} =>
                       match find_ptrstruct P´ l with
                       | none _ => fail 2
                       | some ?o =>
                           hoare lifts (1%nat :: 2%nat :: S (S o) :: nil)
                            pre; eapply assign_rule_struct_aop;
                            [ intro s; split; intro H; exact H
                            | match goal with
                              | |- ?tp = STRUCT _ ­{ _ }­ => try unfold tp
                              end; auto
                            | simpl; auto
                            | unfold id_nth; simpl; auto
                            | simpl; auto
                            | intros; auto
                            | intros; auto
                            | symbolic
                            execution
                            | apply
                               aux_for_hoare_lemmas.assign_type_match_true;
                               simpl; auto
                            | simpl
                            | simpl; auto ]
                       end
                 end
            end
        | none _ =>
            match find_dom_lenv P with
            | (none _, _) => fail 3
            | (some ?m, Some ?ls) =>
                let ret1 := constr:(var_notin_dom x ls) in
                let ret2 := eval compute in ret1 in
                match ret2 with
                | true =>
                    match find_aop P with
                    | none _ => fail 1
                    | some ?n =>
                        match find_gvarmapsto P x with
                        | none _ => fail 4
                        | some ?o =>
                            hoare lifts (n :: m :: o :: nil) pre;
                             match goal with
                             | |-
                               {|_ , _, _, _, _|}|-
                               {{ <|| _ ||> **
                                 A_dom_lenv _ **
                                 GV x @ _ ∗ |-> Vptr ?l ** ?P´}}_ {{_}} =>
                                   match find_ptrstruct P´ l with
                                   | none _ => fail 5
                                   | some ?p =>
                                       hoare lifts
                                        (1%nat
                                         :: 2%nat
                                            :: 3%nat :: S (S (S p)) :: nil)
                                        pre; eapply assign_rule_struct_g_aop;
                                        [ intro s; split; intro H; exact H
                                        | simpl; auto
                                        | match goal with
                                          | |- ?tp = STRUCT _ ­{ _ }­ =>
                                                try unfold tp
                                          end; auto
                                        | simpl; auto
                                        | unfold id_nth; simpl; auto
                                        | simpl; auto
                                        | intros; auto
                                        | intros; auto
                                        | symbolic
                                        execution
                                        | apply
                                           aux_for_hoare_lemmas.assign_type_match_true;
                                           simpl; auto
                                        | simpl
                                        | simpl; auto ]
                                   end
                             end
                        end
                    end
                | false => fail 6
                end
            end
        end
  end.
    Ltac meew := eapply seq_rule;[ let s:= fresh in let H:= fresh in eapply forward_rule2; [hoare_assign_struct´ | intros s H; exact H]| idtac].

        Lemma val_injsimpl :forall i x2 x5 x, val_inj
          (bool_and
             (val_inj
                (notint
                   (val_inj
                      (if Int.eq i ($ 0)
                       then Some (Vint32 Int.one)
                       else Some (Vint32 Int.zero)))))
             (val_inj
                (bool_or
                   (val_inj
                      (if Int.ltu ((x2<<$ 3)+ᵢx5) (x>>ᵢ$ 8)
                       then Some (Vint32 Int.one)
                       else Some (Vint32 Int.zero)))
                   (val_inj
                      (if Int.eq ((x2<<$ 3)+ᵢx5) (x>>ᵢ$ 8)
                       then Some (Vint32 Int.one)
                       else Some (Vint32 Int.zero)))))) =
        Vint32 Int.zero \/
        val_inj
          (bool_and
             (val_inj
                (notint
                   (val_inj
                      (if Int.eq i ($ 0)
                       then Some (Vint32 Int.one)
                       else Some (Vint32 Int.zero)))))
             (val_inj
                (bool_or
                   (val_inj
                      (if Int.ltu ((x2<<$ 3)+ᵢx5) (x>>ᵢ$ 8)
                       then Some (Vint32 Int.one)
                       else Some (Vint32 Int.zero)))
                   (val_inj
                      (if Int.eq ((x2<<$ 3)+ᵢx5) (x>>ᵢ$ 8)
                       then Some (Vint32 Int.one)
                       else Some (Vint32 Int.zero)))))) = Vnull ->
           i = $0 \/ (Int.ltu ((x2<<$ 3)+ᵢx5) (x>>ᵢ$ 8) = false /\ ((x2<<$ 3)+ᵢx5) <> (x>>ᵢ$ 8)).

Lemma neq_imp_neqq :
  forall x y,
    x <> y ->
    Z.to_nat (Int.unsigned x) <> (Z.to_nat (Int.unsigned y)).

Lemma tcbjoin_mod:
  forall x y ma mb mc m,
    TcbJoin x y ma mb ->
    TcbMod.join mc mb m ->
    TcbMod.get m x = Some y.


Lemma return_r_pt_p :forall v´52 x t m x10 v´45 v´43 v´39 v´30 v´51,
                       array_type_vallist_match OS_TCB ∗ v´30 ->
                       length v´30 = 64%nat ->
                       Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3) < 8 ->
                       Int.unsigned ((x>>ᵢ$ 8)&$ 7) < 8 ->
                       Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)&$ 7) < 8 ->
                       Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3) < 8 ->
                       Int.unsigned (x>>ᵢ$ 8) < 64 ->
                       Int.unsigned (x&$ OS_MUTEX_KEEP_LOWER_8) < 64 ->
                       TcbJoin (v´52, Int.zero) ((x>>ᵢ$ 8), t, m) x10 v´45 ->
                       TcbMod.join v´43 v´45 v´39 ->
                       Int.ltu (x>>ᵢ$ 8) (x&$ OS_MUTEX_KEEP_LOWER_8) = true ->
                       nth_val((Z.to_nat (Int.unsigned (x&$ OS_MUTEX_KEEP_LOWER_8)))) v´30 = Some (Vptr v´51) ->
                       R_PrioTbl_P v´30 v´39 v´51 ->
                       R_PrioTbl_P
                         (update_nth_val (Z.to_nat (Int.unsigned (x>>ᵢ$ 8)))
                                         (update_nth_val (Z.to_nat (Int.unsigned (x&$ OS_MUTEX_KEEP_LOWER_8)))
                                                         v´30 (Vptr (v´52, Int.zero))) (Vptr v´51))
                         (TcbMod.set v´39 (v´52, Int.zero) (x&$ OS_MUTEX_KEEP_LOWER_8, t, m))
                         v´51.

Lemma rtbl_remove_RL_RTbl_PrioTbl_P_hold´:
  forall (prio : Z) (y bitx : int32) (rtbl : vallist)
         (ry : int32) (ptbl : vallist) (av : addrval),
    0 <= prio < 64 ->
    y = $ prio>>ᵢ$ 3 ->
    bitx = $ 1<<($ prio&$ 7) ->
    nth_val ∘(Int.unsigned y) rtbl = Some (Vint32 ry) ->
    RL_RTbl_PrioTbl_P rtbl ptbl av ->
    RL_RTbl_PrioTbl_P
      (update_nth_val ∘(Int.unsigned y) rtbl (Vint32 (ry&Int.not bitx)))
      (update_nth_val (∘prio) ptbl (Vptr av))
      av.

Lemma nth_val_upd_ex :
  forall x y vl v,
    (x < length vl)%nat ->
    exists t, nth_val x (update_nth_val y vl v) = Some t.

Lemma nth_val_exx:
  forall x vl,
  (x < length vl)%nat ->
  exists v, nth_val x vl = Some v.

Lemma RL_RTbl_PrioTbl_P_set:
  forall x vhold rtbl ptbl x4 x5 ptcb_addr,
    Int.unsigned x < 64 ->
    (length rtbl = 8)%nat ->
    (length ptbl = 64)%nat ->
    (ptcb_addr, Int.zero) <> vhold ->
    nth_val´ (Z.to_nat (Int.unsigned (x&$ 7))) OSMapVallist =
    Vint32 x4 ->
    nth_val´ (Z.to_nat (Int.unsigned (x>>ᵢ$ 3)))
             rtbl = Vint32 x5 ->
    RL_RTbl_PrioTbl_P rtbl ptbl vhold ->
    RL_RTbl_PrioTbl_P
      (update_nth_val (Z.to_nat (Int.unsigned (x>>ᵢ$ 3)))
                      rtbl (Vint32 (Int.or x5 x4)))
      (update_nth_val (Z.to_nat (Int.unsigned x))
                      ptbl
                      (Vptr (ptcb_addr, Int.zero))) vhold.

    Lemma nth_val_le_len_is_none: forall x ls, (x >= length ls)%nat -> nth_val x ls = None.

  Lemma double_update_exchange :forall a b c d ls, a<>b -> (a<length ls)%nat -> (b<length ls)%nat ->(forall x, nth_val x (update_nth_val a (update_nth_val b ls d) c) =nth_val x ( update_nth_val b (update_nth_val a ls c) d)).

  Lemma double_update_exchangable4rlrt_pt_p : forall a b c d l1 l2 vh, a<>b -> (a<length l2)%nat -> (b<length l2)%nat -> RL_RTbl_PrioTbl_P l1 (update_nth_val a (update_nth_val b l2 c) d) vh -> RL_RTbl_PrioTbl_P l1 (update_nth_val b (update_nth_val a l2 d) c) vh .

Lemma return_rl_rt_pt_p : forall x v´52 v´39 v´36 v´30 v´51 x11 x12 t1,
 (v´52, Int.zero) <> v´51 ->
Int.ltu (x>>ᵢ$ 8) (x&$ OS_MUTEX_KEEP_LOWER_8) = true ->
 array_type_vallist_match OS_TCB ∗ v´30 ->
 length v´30 = 64%nat ->
 array_type_vallist_match Int8u v´36 ->
 length v´36 = ∘OS_RDY_TBL_SIZE ->
 Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3) < 8 ->
 Int.unsigned ((x>>ᵢ$ 8)&$ 7) < 8 ->
 Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)&$ 7) < 8 ->
 Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3) < 8 ->
 Int.unsigned (x>>ᵢ$ 8) < 64 ->
 Int.unsigned (x&$ OS_MUTEX_KEEP_LOWER_8) < 64 ->
 nth_val´ (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)&$ 7)))
          OSMapVallist = Vint32 x11 ->
 true = rule_type_val_match Int8u (Vint32 x11) ->
 Int.unsigned x12 <= 255 ->
 nth_val´ (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36 =
        Vint32 x12 ->
 nth_val´ (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
         (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
            (val_inj
               (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7))))))) =
       Vint32 t1 ->
 Int.unsigned t1 <= 255 ->
 RL_RTbl_PrioTbl_P v´36 v´30 v´51 -> RH_CurTCB (v´52, Int.zero) v´39 ->
 RL_RTbl_PrioTbl_P
     (update_nth_val
        (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
        (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
           (val_inj
              (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7)))))))
        (val_inj
           (or
              (Vint32 t1)
              (Vint32 x11))))
     (update_nth_val (Z.to_nat (Int.unsigned (x>>ᵢ$ 8)))
        (update_nth_val (Z.to_nat (Int.unsigned (x&$ OS_MUTEX_KEEP_LOWER_8)))
           v´30 (Vptr (v´52, Int.zero))) (Vptr v´51)) v´51.
Lemma rl_rtbl_priotbl_p_hold´:
  forall (v´36 : vallist) (v´12 : int32) (v´13 : vallist)
    (v´38 v´69 v´39 : int32) (v´58 : block) (v´40 v´41 v´57 : int32)
    (v´37 : vallist) (vhold : block * int32),
  (v´58, Int.zero) <> vhold ->
  RL_RTbl_PrioTbl_P v´37 v´36 vhold ->
  True ->
  Int.unsigned v´12 <= 255 ->
  array_type_vallist_match Int8u v´13 ->
  length v´13 = ∘OS_EVENT_TBL_SIZE ->
  array_type_vallist_match Int8u v´37 ->
  length v´37 = ∘OS_EVENT_TBL_SIZE ->
  nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
  Int.unsigned v´38 <= 7 ->
  nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
  Int.unsigned v´69 <= 255 ->
  True ->
  Int.unsigned v´39 <= 7 ->
  
  length v´36 = 64%nat ->
  nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
  Int.unsigned v´40 <= 128 ->
  nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
  Int.unsigned v´41 <= 128 ->
  True ->
  True ->
  Int.unsigned v´57 <= 255 ->
  array_type_vallist_match Int8u v´37 ->
  length v´37 = ∘OS_RDY_TBL_SIZE ->
  RL_RTbl_PrioTbl_P
    (update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
       (val_inj
          (or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37) (Vint32 v´40))))
    (update_nth_val (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 (Vptr (v´58, Int.zero)) ) vhold.

Lemma unsignedsimpllemma : forall x y, y < 8 -> Int.unsigned x = y -> x = Int.repr y.

Lemma exists_some_unmap_is_x : forall x, Int.unsigned x < 8 -> nth_val´ (Z.to_nat (Int.unsigned ($ 1 << x))) OSUnMapVallist = Vint32 x /\ Int.unsigned ($ 1 << x) <= 128.








  Lemma xmapis1shlx : forall x, Int.unsigned x < 8 -> nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 ($ 1 << x).

Qed.

Lemma return_rl_t_g_p :
  forall v´36 i7 x v´52 w x8 x11 x12 t1 t11,
    array_type_vallist_match Int8u v´36 ->
    length v´36 = ∘OS_RDY_TBL_SIZE ->
    Int.unsigned i7 <= 255 ->
    Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3) < 8 ->
    Int.unsigned ((x>>ᵢ$ 8)&$ 7) < 8 ->
    Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)&$ 7) < 8 ->
    Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3) < 8 ->
    Int.unsigned (x>>ᵢ$ 8) < 64 ->
    Int.unsigned (x&$ OS_MUTEX_KEEP_LOWER_8) < 64 ->
    val_inj (val_eq (Vint32 t11) (V$0)) <> Vint32 Int.zero ->
    nth_val´ (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3)))
             (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
                             (val_inj
                                (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7))))))) =
    Vint32 t11 ->
    nth_val´
      (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
      OSMapVallist = Vint32 x8 ->
    true = rule_type_val_match Int8u (Vint32 x8) ->
    nth_val´ (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)&$ 7)))
             OSMapVallist = Vint32 x11 ->
    true = rule_type_val_match Int8u (Vint32 x11) ->
    Int.unsigned x12 <= 255 ->
    nth_val´ (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36 =
    Vint32 x12 ->
    nth_val´ (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
             (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
                             (val_inj
                                (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7))))))) =
    Vint32 t1 ->
    Int.unsigned t1 <= 255 ->
    RL_Tbl_Grp_P v´36 (Vint32 i7) ->
    prio_in_tbl ($ OS_IDLE_PRIO) v´36 ->
    RLH_ECBData_P (DMutex (Vint32 x) (Vptr (v´52, $ 0)))
                  (absmutexsem (x>>ᵢ$ 8)
                               (Some (v´52, $ 0, x&$ OS_MUTEX_KEEP_LOWER_8)), w) ->
    RL_Tbl_Grp_P
      (update_nth_val
         (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
         (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
                         (val_inj
                            (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7)))))))
         (val_inj
            (or
               (Vint32 t1)
               (Vint32 x11))))
      (Vint32 (Int.or (i7&Int.not ($ 1<<((x>>ᵢ$ 8)>>ᵢ$ 3))) x8)) /\
    prio_in_tbl ($ OS_IDLE_PRIO)
                (update_nth_val
                   (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
                   (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
                                   (val_inj
                                      (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7)))))))
                   (val_inj
                      (or
                         (Vint32 t1)
                         (Vint32 x11)))).

Lemma return_rl_t_g_p´ :
  forall v´36 i7 x v´52 w x8 x11 x12 t1 t11,
    array_type_vallist_match Int8u v´36 ->
    length v´36 = ∘OS_RDY_TBL_SIZE ->
    Int.unsigned i7 <= 255 ->
    Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3) < 8 ->
    Int.unsigned ((x>>ᵢ$ 8)&$ 7) < 8 ->
    Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)&$ 7) < 8 ->
    Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3) < 8 ->
    Int.unsigned (x>>ᵢ$ 8) < 64 ->
    Int.unsigned (x&$ OS_MUTEX_KEEP_LOWER_8) < 64 ->
    val_inj (val_eq (Vint32 t11) (V$0)) = Vint32 Int.zero \/
    val_inj (val_eq (Vint32 t11) (V$0)) = Vnull ->
    nth_val´ (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3)))
             (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
                             (val_inj
                                (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7))))))) =
    Vint32 t11 ->
    nth_val´
      (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
      OSMapVallist = Vint32 x8 ->
    true = rule_type_val_match Int8u (Vint32 x8) ->
    nth_val´ (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)&$ 7)))
             OSMapVallist = Vint32 x11 ->
    true = rule_type_val_match Int8u (Vint32 x11) ->
    Int.unsigned x12 <= 255 ->
    nth_val´ (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36 =
    Vint32 x12 ->
    nth_val´ (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
             (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
                             (val_inj
                                (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7))))))) =
    Vint32 t1 ->
    Int.unsigned t1 <= 255 ->
    RL_Tbl_Grp_P v´36 (Vint32 i7) ->
    prio_in_tbl ($ OS_IDLE_PRIO) v´36 ->
    RLH_ECBData_P (DMutex (Vint32 x) (Vptr (v´52, $ 0)))
                  (absmutexsem (x>>ᵢ$ 8)
                               (Some (v´52, $ 0, x&$ OS_MUTEX_KEEP_LOWER_8)), w) ->
    RL_Tbl_Grp_P
      (update_nth_val
         (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
         (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
                         (val_inj
                            (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7)))))))
         (val_inj (or (Vint32 t1) (Vint32 x11)))) (Vint32 (Int.or i7 x8)) /\
    prio_in_tbl ($ OS_IDLE_PRIO)
                (update_nth_val
                   (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
                   (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
                                   (val_inj
                                      (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7)))))))
                   (val_inj (or (Vint32 t1) (Vint32 x11)))).

Lemma return_gethwait :
  forall v´38 v´39 v´52 v´55 w prio m v´87 v´59,
  
 

 RH_TCBList_ECBList_P v´38 v´39 (v´52, Int.zero) ->
 EcbMod.get v´38 (v´59, Int.zero) = Some (absmutexsem (v´55>>ᵢ$ 8)
            (Some (v´52, $ 0, v´55&$ OS_MUTEX_KEEP_LOWER_8)), w) ->
 TcbMod.get v´39 (v´52, Int.zero) = Some (prio, rdy, m) ->
    GetHWait
      (TcbMod.set v´39 (v´52, Int.zero)
                  (v´55&$ OS_MUTEX_KEEP_LOWER_8, rdy, m)) w
      (v´87, Int.zero) ->
 (v´52, Int.zero) <> (v´87, Int.zero) ->
   GetHWait v´39 w (v´87, Int.zero).

Lemma vhold_not_get:
  forall tcbls_l tcbls_r tcbls ct cur_prio x2 v´32 v´53 phold,
    TcbMod.join tcbls_l tcbls_r tcbls ->
    TcbJoin ct (cur_prio, rdy, Vnull) x2 tcbls_r ->
    R_PrioTbl_P v´32 tcbls v´53 ->
    nth_val´ (Z.to_nat (Int.unsigned phold)) v´32 =
    Vptr v´53 ->
    forall (tid : tidspec.A) (p : priority) (s0 : taskstatus) (m : msg),
      TcbMod.get x2 tid = Some (p, s0, m) -> p <> phold.

Lemma vhold_not_get´
: forall (tcbls_l tcbls_r tcbls : TcbMod.map)
         (v´32 : vallist) (v´53 : addrval) (phold : int32),
    TcbMod.join tcbls_l tcbls_r tcbls ->
    R_PrioTbl_P v´32 tcbls v´53 ->
    nth_val´ (Z.to_nat (Int.unsigned phold)) v´32 = Vptr v´53 ->
    forall (tid : tidspec.A) (p : priority) (s0 : taskstatus) (m : msg),
      TcbMod.get tcbls_l tid = Some (p, s0, m) -> p <> phold.

Require Import sem_common.

Ltac simpl_vqm :=
  repeat
    match goal with
      | H: ?f _ = Some _ |- _ => simpl in H;inverts H
      | _ => idtac
    end.

Lemma tcbls_l_mutexpend:
  forall prio_lift ptcb_prio v´33 v´34 v´45 v´43 x11 xm i8 ptcb_tcby ptcb_bitx ptcb_bity v´36 os_rdy_tbl tcbls_l v´32 tcbls_r tcbls ptcb_addr v0 x5 vhold,
    
    get_last_tcb_ptr v´34 v´33 = Some (Vptr (ptcb_addr,Int.zero)) ->
    nth_val´ (Z.to_nat (Int.unsigned prio_lift)) v´32 =
                  Vptr vhold ->
    TcbMod.join tcbls_l tcbls_r tcbls ->
    R_PrioTbl_P v´32 tcbls vhold ->
    Int.unsigned prio_lift < 64 ->
    ptcb_prio <> prio_lift->
    TcbMod.get tcbls_l (ptcb_addr, Int.zero) =
    Some (ptcb_prio, rdy, xm) ->
    nth_val´ (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl =
    Vint32 v0 ->
    nth_val´ (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
             (update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl
                             (Vint32 (v0&Int.not ptcb_bitx))) = Vint32 x5 ->
    TCBList_P v´33
              (v´34 ++
                    (v´45
                       :: v´43
                       :: x11
                       :: xm
                       :: V$0
                       :: V$OS_STAT_RDY
                       :: Vint32 ptcb_prio
                       :: Vint32 i8
                       :: Vint32 ptcb_tcby
                       :: Vint32 ptcb_bitx
                       ::
                       Vint32 ptcb_bity :: nil)
                    :: v´36) os_rdy_tbl tcbls_l ->
    TCBList_P v´33
              (v´34 ++
                    (v´45
                       :: v´43
                       :: x11
                       :: xm
                       :: V$0
                       :: V$OS_STAT_RDY
                       :: Vint32 prio_lift
                       :: Vint32 (prio_lift&$ 7)
                       :: Vint32 (prio_lift>>ᵢ$ 3)
                       :: Vint32 ($ 1<<(prio_lift&$ 7)) :: Vint32 ($ 1<<(prio_lift>>ᵢ$ 3)) :: nil) :: v´36)
              (update_nth_val (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
                              (update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl
                                              (Vint32 (v0&Int.not ptcb_bitx)))
                              (Vint32 (Int.or x5 ($ 1<<(prio_lift&$ 7)))))
              (TcbMod.set tcbls_l (ptcb_addr, Int.zero) (prio_lift, rdy, xm)).

Lemma return_tcbl_p: forall m x x11 x8 v´35 v´36 x12 t1 v´52 v´45 v´24 x15 x7 v´51 v´39 v´30 x10 v´43,
                       nth_val´
                         (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
                         OSMapVallist = Vint32 x8 ->
                      
                       true = rule_type_val_match Int8u (Vint32 x8) ->
                       Int.ltu (x>>ᵢ$ 8) (x&$ OS_MUTEX_KEEP_LOWER_8) = true->
                       array_type_vallist_match Int8u v´36 ->
                       length v´36 = ∘OS_RDY_TBL_SIZE ->
                       Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3) < 8 ->
                       Int.unsigned ((x>>ᵢ$ 8)&$ 7) < 8 ->
                       Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)&$ 7) < 8 ->
                       Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3) < 8 ->
                       Int.unsigned (x>>ᵢ$ 8) < 64 ->
                       Int.unsigned (x&$ OS_MUTEX_KEEP_LOWER_8) < 64 ->
                       nth_val´ (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)&$ 7)))
                                OSMapVallist = Vint32 x11 ->
                       true = rule_type_val_match Int8u (Vint32 x11) ->
                       Int.unsigned x12 <= 255 ->
                       nth_val´ (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36 =
                       Vint32 x12 ->
                       nth_val´ (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
                                (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
                                                (val_inj
                                                   (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7))))))) =
                       Vint32 t1 ->
                       Int.unsigned t1 <= 255 ->
                       TcbMod.join v´43 v´45 v´39 ->
                       TcbJoin (v´52, Int.zero) (x>>ᵢ$ 8, rdy, m) x10 v´45 ->
                       nth_val (Z.to_nat (Int.unsigned (x&$ OS_MUTEX_KEEP_LOWER_8))) v´30 =
                       Some (Vptr v´51) ->
                       R_PrioTbl_P v´30 v´39 v´51 ->
                       TCBList_P (Vptr (v´52, Int.zero))
                                 ((x7
                                     :: v´24
                                     :: x15
                                     :: m
                                     :: V$0
                                     :: V$OS_STAT_RDY
                                     :: Vint32 (x>>ᵢ$ 8)
                                     :: Vint32 ((x>>ᵢ$ 8)&$ 7)
                                     :: Vint32 ((x>>ᵢ$ 8)>>ᵢ$ 3)
                                     :: Vint32 ($ 1<<((x>>ᵢ$ 8)&$ 7))
                                     :: Vint32 ($ 1<<((x>>ᵢ$ 8)>>ᵢ$ 3))
                                     :: nil) :: v´35) v´36 v´45 ->
                       TCBList_P (Vptr (v´52, Int.zero))
                                 ((x7
                                     :: v´24
                                     :: x15
                                     :: m
                                     :: V$0
                                     :: V$OS_STAT_RDY
                                     :: Vint32 (x&$ OS_MUTEX_KEEP_LOWER_8)
                                     :: Vint32 ((x&$ OS_MUTEX_KEEP_LOWER_8)&$ 7)
                                     :: Vint32 ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)
                                     :: Vint32 x11 :: Vint32 x8 :: nil) :: v´35)
                                 (update_nth_val
                                    (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
                                    (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
                                                    (val_inj
                                                       (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7)))))))
                                    (val_inj (or (Vint32 t1) (Vint32 x11))))
                                 (TcbMod.set v´45 (v´52, Int.zero) (x&$ OS_MUTEX_KEEP_LOWER_8, rdy, m)).

Lemma return_tcbl_p´ :forall v´31 v´33 v´36 v´43 x x11 t1 x12 v´51 v´39 v´30 v´45 x10 t m v´52,
                        array_type_vallist_match Int8u v´36 ->
                        length v´36 = ∘OS_RDY_TBL_SIZE ->
                        Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3) < 8 ->
                        Int.unsigned ((x>>ᵢ$ 8)&$ 7) < 8 ->
                        Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)&$ 7) < 8 ->
                        Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3) < 8 ->
                        Int.unsigned (x>>ᵢ$ 8) < 64 ->
                        Int.unsigned (x&$ OS_MUTEX_KEEP_LOWER_8) < 64 ->
                        nth_val´ (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)&$ 7)))
                                 OSMapVallist = Vint32 x11 ->
                        true = rule_type_val_match Int8u (Vint32 x11) ->
                        Int.unsigned x12 <= 255 ->
                        nth_val´ (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36 =
                        Vint32 x12 ->
                        nth_val´ (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
                                 (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
                                                 (val_inj
                                                    (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7))))))) =
                        Vint32 t1 ->
                        Int.unsigned t1 <= 255 ->
                        TcbMod.join v´43 v´45 v´39 ->
                        TcbJoin (v´52, Int.zero) (x>>ᵢ$ 8, t, m) x10 v´45 ->
                        nth_val (Z.to_nat (Int.unsigned (x&$ OS_MUTEX_KEEP_LOWER_8))) v´30 =
                        Some (Vptr v´51) ->
                        R_PrioTbl_P v´30 v´39 v´51 ->
                        TCBList_P v´31 v´33 v´36 v´43 ->
                        TCBList_P v´31 v´33
                                  (update_nth_val
                                     (Z.to_nat (Int.unsigned ((x&$ OS_MUTEX_KEEP_LOWER_8)>>ᵢ$ 3)))
                                     (update_nth_val (Z.to_nat (Int.unsigned ((x>>ᵢ$ 8)>>ᵢ$ 3))) v´36
                                                     (val_inj
                                                        (and (Vint32 x12) (Vint32 (Int.not ($ 1<<((x>>ᵢ$ 8)&$ 7)))))))
                                     (val_inj (or (Vint32 t1) (Vint32 x11)))) v´43
.

Lemma int_ltu_prop:
  forall x y, Int.ltu x y = false ->
                x <> y ->
                Int.ltu y x = true.

Lemma intlemmag :
  forall x2 x x5, Int.ltu ((x2<<$ 3)+ᵢx5) (x>>ᵢ$ 8) = false
                  /\ (x2<<$ 3)+ᵢx5 <> x>>ᵢ$ 8 ->
                  Int.ltu (x>>ᵢ$ 8) ((x2<<$ 3)+ᵢx5) = true.

 Lemma ltu_false_eq_false_ltu_true :
    forall i1 i2,
      Int.ltu i1 i2 = false ->
      Int.eq i1 i2 = false ->
      Int.ltu i2 i1 = true.
Lemma return_r_ecb_et_p :
  forall i v´52 x3 v´46 v´44 v´39 v´29 x p m,
    TcbMod.get v´39 (v´52, Int.zero) = Some (p,rdy,m) ->
    R_ECB_ETbl_P (v´29, Int.zero)
                 (V$OS_EVENT_TYPE_MUTEX
                   :: Vint32 i :: Vint32 x :: Vptr (v´52, $ 0) :: x3 :: v´46 :: nil,
                  v´44) v´39 ->
    R_ECB_ETbl_P (v´29, Int.zero)
                 (V$OS_EVENT_TYPE_MUTEX
                   :: Vint32 i :: Vint32 x :: Vptr (v´52, $ 0) :: x3 :: v´46 :: nil, v´44)
                 (TcbMod.set v´39 (v´52, Int.zero) (x&$ OS_MUTEX_KEEP_LOWER_8, rdy, m)).

Lemma ecblist_p_mutexpend_changeprio:
  forall ectl tcbls v´44 edatal ecbls ptcb_addr ptcb_prio xm prio_lift tl,
    TcbMod.get tcbls (ptcb_addr, Int.zero) = Some (ptcb_prio, rdy, xm) ->
    ECBList_P v´44 tl ectl edatal ecbls tcbls ->
    ECBList_P v´44 tl ectl edatal ecbls (TcbMod.set tcbls (ptcb_addr, Int.zero) (prio_lift, rdy, xm)).

Lemma RH_TCBList_ECBList_P_changeprio:
  forall ptcb_prio tid tcbls ecbls pcur xm p´,
    TcbMod.get tcbls tid = Some (ptcb_prio, rdy, xm)->
    RH_TCBList_ECBList_P ecbls tcbls pcur ->
    RH_TCBList_ECBList_P ecbls (TcbMod.set tcbls tid (p´,rdy,xm)) pcur.

Lemma return_ecbl_p : forall v´57 v´26 v´28 v´48 v´39 v´52 v´55 m x10 tl v´45 v´43,
                        TcbJoin (v´52, Int.zero) (v´55>>ᵢ$ 8, rdy, m) x10 v´45 ->
                        TcbMod.join v´43 v´45 v´39 ->
                        ECBList_P v´57 tl v´26 v´28 v´48 v´39 ->
                        ECBList_P v´57 tl v´26 v´28 v´48
                                  (TcbMod.set v´39 (v´52, Int.zero) (v´55&$ OS_MUTEX_KEEP_LOWER_8, rdy, m)).

Lemma return_rh_tcbl_ecbl_p : forall v´38 v´39 v´52 v´55 m x10 v´45 v´43,
                                TcbJoin (v´52, Int.zero) (v´55>>ᵢ$ 8, rdy, m) x10 v´45 ->
                                TcbMod.join v´43 v´45 v´39 ->
                                RH_TCBList_ECBList_P v´38 v´39 (v´52, Int.zero) ->
                                RH_TCBList_ECBList_P v´38
                                                     (TcbMod.set v´39 (v´52, Int.zero) (v´55&$ OS_MUTEX_KEEP_LOWER_8, rdy, m))
                                                     (v´52, Int.zero).

Lemma eq2inteq: forall x y, x=y -> Int.eq x y = true.

Lemma tcbset_indom_eq: forall tls a c ,TcbMod.indom tls a-> (forall tid, TcbMod.indom tls tid <-> TcbMod.indom (TcbMod.set tls a c) tid).

Lemma ecblistp_hold :
  forall v´42 v´25 i x v´52 x3 v´46 v´44 v´26 v´27 v´28 v´38 v´39 v´29 v´48 v´49 v´47,
    ((v´42 = Vptr (v´29, Int.zero) /\ v´25 = nil)\/ get_last_ptr v´25 = Some (Vptr (v´29, Int.zero))) /\ (length v´25 = length v´27)->
    EcbMod.joinsig (v´29, Int.zero)
                   (absmutexsem (x>>ᵢ$ 8) (Some (v´52, $ 0, x&$ OS_MUTEX_KEEP_LOWER_8)),
                    nil) v´48 v´49 ->
    EcbMod.join v´47 v´49 v´38 ->
    ECBList_P v´42 Vnull
              (v´25 ++
                    ((V$OS_EVENT_TYPE_MUTEX
                       :: Vint32 i :: Vint32 x :: Vptr (v´52, $ 0) :: x3 :: v´46 :: nil,
                                         v´44) :: nil) ++ v´26)
              (v´27 ++ (DMutex (Vint32 x) (Vptr (v´52, $ 0)) :: nil) ++ v´28) v´38 v´39 ->
    R_ECB_ETbl_P (v´29, Int.zero)
                 (V$OS_EVENT_TYPE_MUTEX
                   :: Vint32 i :: Vint32 x :: Vptr (v´52, $ 0) :: x3 :: v´46 :: nil,
                  v´44) v´39 ->
    ECBList_P v´42 Vnull
              (v´25 ++
                    ((V$OS_EVENT_TYPE_MUTEX
                       :: Vint32 i
                       :: Vint32 (Int.or x ($ OS_MUTEX_AVAILABLE))
                       :: Vnull :: x3 :: v´46 :: nil, v´44) :: nil) ++ v´26)
              (v´27 ++
                    (DMutex (Vint32 (Int.or x ($ OS_MUTEX_AVAILABLE))) Vnull :: nil) ++
                    v´28)
              (EcbMod.set v´38 (v´29, Int.zero) (absmutexsem (x>>ᵢ$ 8) None, nil))
              v´39.

Lemma retpost_eventrdy : retpost OS_EventTaskRdyPost.

Lemma Mutex_owner_set_true:
  forall tcbls tid p st msg t pr opr wls eid ecbls,
    TcbMod.get tcbls tid = Some (p, st, msg) ->
    t = (absmutexsem pr (Some (tid, opr)), wls) ->
    RH_TCBList_ECBList_MUTEX_OWNER ecbls tcbls ->
    RH_TCBList_ECBList_MUTEX_OWNER (EcbMod.set ecbls eid t) tcbls.

Lemma mutex_acpt_rh_tcblist_ecblist_p_hold:
  forall v v´37 v´50 x vv x0 x1 x2,
    TcbMod.get v´37 (v´50, Int.zero) = Some (x0, x1, x2) ->
    EcbMod.get vv v = Some (absmutexsem (Int.shru x ($ 8)) None, nil) ->
    RH_TCBList_ECBList_P vv v´37 (v´50, Int.zero) ->
    RH_TCBList_ECBList_P
      (EcbMod.set vv v
                  (absmutexsem (Int.shru x ($ 8)) (Some (v´50, Int.zero, x0)), nil)) v´37
      (v´50, Int.zero).

Lemma mund_int_c1:
  forall i x,
    Int.unsigned i < 64 ->
    Int.unsigned x <= 65535 ->
    Int.unsigned (Int.or (x&$ OS_MUTEX_KEEP_UPPER_8) i) <= 65535.

Lemma mutex_pend_inv_update1:
  forall i2 i6 s low med high P low´ med´ high´ i0 x3 v´48 x1 x2 x0 v´54 v´41,
    s |= AEventData low med ** P ->
    RLH_ECBData_P med high ->
    low = (V$OS_EVENT_TYPE_MUTEX
            :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´48 :: nil) ->
    med = DMutex (Vint32 i2) x2 ->
    high = (absmutexsem (Int.shru i2 ($ 8)) x0, x1) ->
    RH_CurTCB (v´54, Int.zero) v´41 ->
    Int.unsigned i6 < 64 ->
    Int.unsigned i2 <= 65535 ->
    Int.ltu (Int.shru i2 ($ 8)) i6 = true ->
    i2& ($ OS_MUTEX_KEEP_LOWER_8) = ($ OS_MUTEX_AVAILABLE) ->
    low´ = (V$OS_EVENT_TYPE_MUTEX
             :: Vint32 i0
             :: Vint32 (Int.or (i2&$ OS_MUTEX_KEEP_UPPER_8) i6)
             :: Vptr (v´54, Int.zero) :: x3 :: v´48 :: nil) ->
    med´ = DMutex (Vint32 (Int.or (i2&$ OS_MUTEX_KEEP_UPPER_8) i6))
                  (Vptr (v´54, Int.zero)) ->
    high´ = (absmutexsem (Int.shru i2 ($ 8)) (Some ((v´54, Int.zero), i6)), x1) ->
    s |= AEventData low´ med´ **
         [| RLH_ECBData_P med´ high´ |] ** P.

Lemma TCBList_P_split_by_tcbls_verbose :
  forall l tls tid htcb s head hprev tail tnext rtbl P,
    TcbMod.get tls tid = Some htcb ->
    TCBList_P head l rtbl tls ->
    s |= tcbdllseg head hprev tail tnext l ** P ->
    exists l1 tcbnode l2 tls1 tls2 tail1,
       s |= tcbdllseg head hprev tail1 (Vptr tid) l1 **
         tcbdllseg (Vptr tid) tail1 tail tnext (tcbnode :: l2) ** P /\
       TCBList_P head l1 rtbl tls1 /\
       TCBList_P (Vptr tid) (tcbnode :: l2) rtbl tls2 /\
       TcbMod.join tls1 tls2 tls /\
       l = l1 ++ (tcbnode :: l2) /\
       get_last_tcb_ptr l1 head = Some (Vptr tid).
I plus this
Lemma lzh_tcb_list_split:
  forall s P head headpre tail tailnext l tid abstcb tcbls rtbl,
    s |= tcbdllseg head headpre tail tailnext l ** P ->
    TcbMod.get tcbls tid = Some abstcb ->
    TCBList_P head l rtbl tcbls ->
    s |= EX ltcb l1 l2 p p_pre p_next tcbls1 tcbls2´ tcbls2,
         [| p = Vptr tid |] **
         tcbdllseg head headpre p_pre p l1 **
         node p ltcb OS_TCB **
         [| V_OSTCBNext ltcb = Some p_next |] **
         [| get_last_tcb_ptr l1 head = Some p |] **
         [| V_OSTCBPrev ltcb = Some p_pre |] **
         tcbdllseg p_next p tail tailnext l2 **
         [| l = l1 ++ ltcb :: l2 |] **
         [| TcbMod.join tcbls1 tcbls2´ tcbls |] **
         [| TcbMod.joinsig tid abstcb tcbls2 tcbls2´ |] **
         [| TCBNode_P ltcb rtbl abstcb |] **
         [| TCBList_P head l1 rtbl tcbls1 |] **
         [| TCBList_P p_next l2 rtbl tcbls2 |] ** P.
Lemma mund_int_a1:
  forall i,
    Int.unsigned i <= 65535 ->
    Int.unsigned (i>>ᵢ$ 8) <= 255.

Lemma mund_int_a2:
  forall i,
    Int.unsigned i <= 255 ->
    (if Int.unsigned i <=? Byte.max_unsigned then true else false) = true.

Lemma mund_val_inj_a0:
  forall (b:bool),
    val_inj
     (if b
      then Some (Vint32 Int.one)
      else Some (Vint32 Int.zero)) <> Vundef.

Lemma mund_val_inj_a1:
  forall (b1 b2:bool),
   val_inj
     (bool_or
        (val_inj
           (if b1
            then Some (Vint32 Int.one)
            else Some (Vint32 Int.zero)))
        (val_inj
           (if b2
            then Some (Vint32 Int.one)
            else Some (Vint32 Int.zero)))) <> Vundef.

Lemma mund_int_ltu_revers:
  forall x y,
    Int.ltu x y = true \/ Int.eq x y = true ->
    Int.ltu y x = false.

Lemma absinfer_mutex_pend_cur_prio_higher:
  forall P ecbls tcbls t ct v prio st msg pr owner wls eid,
    Int.unsigned v <= 65535 ->
    TcbMod.get tcbls ct = Some (prio, st, msg) ->
    EcbMod.get ecbls eid = Some (absmutexsem pr owner, wls) ->
    Int.ltu pr prio = false ->
    can_change_aop P ->
    absinfer
      (<|| mutexpend (Vptr eid :: Vint32 v :: nil) ||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P)
      (<|| END (Some (Vint32 (Int.repr OS_ERR_MUTEX_PRIO)))||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P).

Lemma mund_int_a3:
  forall i,
    Int.unsigned i <= 65535 ->
    Int.unsigned (i&$ OS_MUTEX_KEEP_LOWER_8) <= 255.

Lemma mund_int_byte_modulus:
  Byte.modulus = 256.

Lemma mund_int_mod:
  forall i,
    Int.unsigned i <= 255 ->
    $ Int.unsigned i mod 256 = i.

Lemma absinfer_mutex_pend_available_return:
  forall P v sid prio m pr els tls t ct,
    can_change_aop P ->
    Int.unsigned v <= 65535 ->
    TcbMod.get tls ct = Some (prio, rdy, m) ->
    EcbMod.get els sid = Some (absmutexsem pr None, nil) ->
    Int.ltu pr prio = true ->
    absinfer
      ( <|| mutexpend (Vptr sid :: Vint32 v :: nil) ||> **
        HECBList els **
        HTCBList tls **
        HTime t **
        HCurTCB ct ** P)
      ( <|| END (Some (Vint32 (Int.repr NO_ERR))) ||> **
        HECBList (EcbMod.set els sid (absmutexsem pr (Some (ct, prio)), nil)) **
        HTCBList tls **
        HTime t **
        HCurTCB ct ** P).

Lemma lzh_ecb_join_set_one:
  forall ml a b ml1 ml2 ml1´ med b´,
    RLH_ECBData_P med b´ ->
    EcbMod.get ml a = Some b ->
    EcbMod.joinsig a
                   b ml1´ ml1 ->
    EcbMod.join ml2 ml1 ml ->
    exists ml1n, EcbMod.joinsig a b´ ml1´ ml1n /\ EcbMod.join ml2 ml1n (EcbMod.set ml a b´).

Lemma TCBList_get_head:
  forall tcbls tid abstcb vl l rtbl,
    TCBList_P (Vptr tid) (vl :: l) rtbl tcbls ->
    TcbMod.get tcbls tid = Some abstcb ->
    TCBNode_P vl rtbl abstcb.

Lemma mund_ltu_a1:
  Int.ltu Int.zero Int.zero = false.

Lemma mund_ltu_a2:
  Int.ltu Int.zero Int.one = true.

Lemma mund_int_byte_max_unsigned:
  Byte.max_unsigned = 255.

Lemma mund_to_nat_a1:
  forall i,
    Int.unsigned i < 64 ->
    (Z.to_nat (Int.unsigned i) < 64)%nat.

Lemma mund_nth_val_a1:
  forall i v´32,
    Int.unsigned i < 64 ->
    array_type_vallist_match OS_TCB ∗ v´32 ->
    length v´32 = 64%nat ->
    (exists v, (nth_val´ (Z.to_nat (Int.unsigned i)) v´32) = Vptr v) \/
    (nth_val´ (Z.to_nat (Int.unsigned i)) v´32) = Vnull.

Lemma absinfer_mutex_pend_null_return:
   forall P x,
    can_change_aop P ->
    tl_vl_match (Tint16 :: nil) x = true ->
    absinfer
      (<|| mutexpend (Vnull :: x) ||> ** P)
      (<|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> ** P).

Lemma absinfer_mbox_pend_p_not_legal_return :
  forall x a P b v´33 v´16 v´35,
    can_change_aop P ->
    Int.unsigned b<=65535 ->
    EcbMod.get x a = None ->
    absinfer
      (<|| mutexpend (Vptr a ::Vint32 b:: nil) ||> **
           HECBList x **
           HTCBList v´33 **
           HTime v´16 **
           HCurTCB v´35 ** P)
      (<|| END (Some (V$ OS_ERR_PEVENT_NO_EX)) ||> **
           HECBList x **
           HTCBList v´33 **
           HTime v´16 **
           HCurTCB v´35 ** P).

Lemma mutex_eventtype_neq_mutex:
   forall s P a msgq mq t,
    s |= AEventData a msgq ** P ->
    RLH_ECBData_P msgq mq ->
    V_OSEventType a = Some (Vint32 t) ->
    t <> ($ OS_EVENT_TYPE_MUTEX) ->
    s |= AEventData a msgq **
         [| (~ exists pr owner wls, mq = (absmutexsem pr owner, wls)) |] ** P.

Lemma absinfer_mutex_pend_wrong_type_return :
  forall x a b P v´33 v´16 v´35,
    can_change_aop P ->
    Int.unsigned b <= 65535 ->
    (exists d,
       EcbMod.get x a = Some d /\ ~ (exists x y wls, d = (absmutexsem x y, wls))) ->
    absinfer
      (<|| mutexpend (Vptr a :: Vint32 b :: nil) ||> **
           HECBList x **
           HTCBList v´33 **
           HTime v´16 **
           HCurTCB v´35 ** P)
      (<|| END (Some (V$ OS_ERR_EVENT_TYPE)) ||> **
           HECBList x **
           HTCBList v´33 **
           HTime v´16 **
           HCurTCB v´35 ** P).

Lemma mutex_triangle:
  
  forall s P a x y msgq mq,
    s |= AEventData a msgq ** P ->
    RLH_ECBData_P msgq mq ->
    V_OSEventType a = Some (V$OS_EVENT_TYPE_MUTEX) ->
    V_OSEventCnt a = Some x ->
    V_OSEventPtr a = Some y ->
    s |= AEventData a msgq **
         [| exists pr own wls, msgq = DMutex x y
                               /\ mq = (absmutexsem pr own, wls)
                               /\ MatchMutexSem x y pr own
                               /\ RH_ECB_P mq|] ** P.

Lemma TCBList_imp_TCBNode:
  forall v v´52 v´26 x12 x11 i8 i7 i6 i5 i4 i3 i1 v´37 v´38 v´47,
    TCBList_P (Vptr v)
              ((v´52
                  :: v´26
                  :: x12
                  :: x11
                  :: Vint32 i8
                  :: Vint32 i7
                  :: Vint32 i6
                  :: Vint32 i5
                  :: Vint32 i4
                  :: Vint32 i3 :: Vint32 i1 :: nil) :: v´37)
              v´38 v´47 ->
    exists abstcb,
      TCBNode_P
        (v´52
           :: v´26
           :: x12
           :: x11
           :: Vint32 i8
           :: Vint32 i7
           :: Vint32 i6
           :: Vint32 i5
           :: Vint32 i4 :: Vint32 i3 :: Vint32 i1 :: nil)
        v´38 abstcb /\
      TcbMod.get v´47 v = Some abstcb /\
      exists st, abstcb = (i6, st, x11).

Lemma absinfer_mutex_pend_from_idle_return :
  forall x a b P y t ct,
    can_change_aop P ->
    Int.unsigned b <= 65535 ->
    (exists st msg, TcbMod.get y ct = Some (Int.repr OS_IDLE_PRIO, st, msg)) ->
    absinfer
      (<|| mutexpend (Vptr a :: Vint32 b :: nil) ||> **
           HECBList x **
           HTCBList y **
           HTime t **
           HCurTCB ct ** P)
      ( <|| END (Some (V$ OS_ERR_IDLE)) ||> **
            HECBList x **
            HTCBList y **
            HTime t **
            HCurTCB ct ** P).

Lemma absinfer_mutex_pend_not_ready_return :
  forall P ecbls tcbls t ct st msg v x prio,
    Int.unsigned v <= 65535 ->
    TcbMod.get tcbls ct = Some (prio, st, msg) ->
    ~ st = rdy ->
    can_change_aop P ->
    absinfer
      (<|| mutexpend (Vptr x :: Vint32 v :: nil) ||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P)
      (<|| END (Some (Vint32 (Int.repr OS_ERR_STAT)))||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P).

Lemma absinfer_mutex_pend_msg_not_null_return :
  forall P ecbls tcbls t ct st msg v x prio,
    Int.unsigned v <= 65535 ->
    TcbMod.get tcbls ct = Some (prio, st, msg) ->
    ~ msg = Vnull ->
    can_change_aop P ->
    absinfer
      (<|| mutexpend (Vptr x :: Vint32 v :: nil) ||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P)
      (<|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL)))||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P).

Lemma absinfer_mutex_post_null_return : forall P,
                                          can_change_aop P ->
                                          absinfer (<|| mutexpost (Vnull :: nil) ||> ** P) ( <|| END (Some (Vint32 (Int.repr OS_ERR_PEVENT_NULL))) ||> ** P).

Lemma absinfer_mutex_post_p_not_legal_return : forall x a P tcbls t ct,
                                                 can_change_aop P ->
                                                 EcbMod.get x a = None ->
                                                 absinfer (<|| mutexpost (Vptr a :: nil) ||> ** HECBList x** HTCBList tcbls ** HTime t ** HCurTCB ct **
                                                               P) ( <|| END (Some (V$ OS_ERR_PEVENT_NO_EX)) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).

Lemma absinfer_mutex_post_wrong_type_return : forall x a P tcbls t ct,
                                                can_change_aop P ->
                                                (exists d,
                                                   EcbMod.get x a = Some d /\ ~ (exists x y wls, d = (absmutexsem x y, wls))) ->
                                                absinfer (<|| mutexpost (Vptr a :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct **
                                                              P) ( <|| END (Some (V$OS_ERR_EVENT_TYPE)) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).

Lemma absinfer_mutex_post_no_owner_return : forall x a P tcbls t ct y y0 wl,
                                              can_change_aop P ->
                                              EcbMod.get x a = Some (absmutexsem y0 y, wl) ->
                                              (~ exists p, y =Some (ct,p)) ->
                                              absinfer (<|| mutexpost (Vptr a :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct **
                                                            P) ( <|| END (Some (V$OS_ERR_NOT_MUTEX_OWNER)) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).

Lemma valinj_lemma1 : forall v0 v´52, isptr v0 ->val_inj
                                                    (notint
                                                       (val_inj
                                                          match v0 with
                                                            | Vundef => None
                                                            | Vnull => Some (Vint32 Int.zero)
                                                            | Vint32 _ => None
                                                            | Vptr (b2, ofs2) =>
                                                              if peq v´52 b2
                                                              then
                                                                if Int.eq Int.zero ofs2
                                                                then Some (Vint32 Int.one)
                                                                else Some (Vint32 Int.zero)
                                                              else Some (Vint32 Int.zero)
                                                          end)) <> Vint32 Int.zero -> v0 = Vnull \/( exists b2 ofs2, v0= Vptr (b2, ofs2) /\ (Int.eq Int.zero ofs2 = false \/ v´52 <> b2)).

Lemma valinj_lemma2:forall v0 v´52, val_inj
                                       (notint
                                          (val_inj
                                             match v0 with
                                               | Vundef => None
                                               | Vnull => Some (Vint32 Int.zero)
                                               | Vint32 _ => None
                                               | Vptr (b2, ofs2) =>
                                                 if peq v´52 b2
                                                 then
                                                   if Int.eq Int.zero ofs2
                                                   then Some (Vint32 Int.one)
                                                   else Some (Vint32 Int.zero)
                                                 else Some (Vint32 Int.zero)
                                             end)) = Vint32 Int.zero \/
                                     val_inj
                                       (notint
                                          (val_inj
                                             match v0 with
                                               | Vundef => None
                                               | Vnull => Some (Vint32 Int.zero)
                                               | Vint32 _ => None
                                               | Vptr (b2, ofs2) =>
                                                 if peq v´52 b2
                                                 then
                                                   if Int.eq Int.zero ofs2
                                                   then Some (Vint32 Int.one)
                                                   else Some (Vint32 Int.zero)
                                                 else Some (Vint32 Int.zero)
                                             end)) = Vnull -> v0=Vptr (v´52, $0).

Lemma post_intlemma1 : forall i4 x, Int.unsigned (Int.shru x ($ 8))<64 -> val_inj
                                                                            (if Int.ltu i4 (Int.modu (Int.shru x ($ 8)) ($ Byte.modulus))
                                                                             then Some (Vint32 Int.one)
                                                                             else Some (Vint32 Int.zero)) <> Vint32 Int.zero -> Int.ltu i4 (Int.shru x ($ 8)) = true.

Lemma unMapvallistint8u : array_type_vallist_match Int8u OSUnMapVallist.

Lemma absinfer_mutex_post_prio_err_return : forall x a P tcbls t ct p stp wl prio st msg,
                                              can_change_aop P ->
                                              EcbMod.get x a = Some (absmutexsem p stp,wl) ->
                                              TcbMod.get tcbls ct = Some (prio,st,msg) ->
                                              Int.ltu prio p = true ->
                                              absinfer (<|| mutexpost (Vptr a :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct **
                                                            P) ( <|| END (Some (V$OS_ERR_MUTEX_PRIO)) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).

Lemma post_intlemma2 :forall x i4 , Int.unsigned (Int.shru x ($ 8)) < 64 ->
                                    val_inj (if Int.ltu i4 (Int.modu (Int.shru x ($ 8)) ($ Byte.modulus))
                                             then Some (Vint32 Int.one)
                                             else Some (Vint32 Int.zero)) = Vint32 Int.zero \/
                                    val_inj
                                      (if Int.ltu i4 (Int.modu (Int.shru x ($ 8)) ($ Byte.modulus))
                                       then Some (Vint32 Int.one)
                                       else Some (Vint32 Int.zero)) = Vnull -> Int.ltu i4 (Int.shru x ($ 8)) = false.

Lemma Bmax_unsigned : Byte.max_unsigned = 255.

Lemma Bmodulus : Byte.modulus = 256.

Lemma absinfer_mutex_post_wl_highest_prio_err_return : forall x a P tcbls t ct pr opr wl sometid somepr somest somemsg,
                                                         can_change_aop P ->
                                                         EcbMod.get x a = Some (absmutexsem pr opr, wl) ->
                                                         In sometid wl ->
                                                         TcbMod.get tcbls sometid = Some (somepr, somest, somemsg) ->
                                                         Int.ltu pr somepr = false ->
                                                         absinfer (<|| mutexpost (Vptr a :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct **
                                                                       P) ( <|| END (Some (V$OS_ERR_MUTEX_WL_HIGHEST_PRIO)) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).

Lemma absinfer_mutex_post_original_not_holder_err_return : forall x a P tcbls t ct,
                                                             can_change_aop P ->
                                                             absinfer (<|| mutexpost (Vptr a :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct **
                                                                           P) ( <|| END (Some (V$OS_ERR_ORIGINAL_NOT_HOLDER)) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).

Lemma simpl_valinj : forall i5 i6 a b, val_inj
                                         (bool_or
                                            (val_inj
                                               (notint
                                                  (val_inj
                                                     (if Int.eq i5 a
                                                      then Some (Vint32 Int.one)
                                                      else Some (Vint32 Int.zero)))))
                                            (val_inj
                                               (notint
                                                  (val_inj
                                                     (if Int.eq i6 b
                                                      then Some (Vint32 Int.one)
                                                      else Some (Vint32 Int.zero)))))) =
                                       Vint32 Int.zero \/
                                       val_inj
                                         (bool_or
                                            (val_inj
                                               (notint
                                                  (val_inj
                                                     (if Int.eq i5 a
                                                      then Some (Vint32 Int.one)
                                                      else Some (Vint32 Int.zero)))))
                                            (val_inj
                                               (notint
                                                  (val_inj
                                                     (if Int.eq i6 b
                                                      then Some (Vint32 Int.one)
                                                      else Some (Vint32 Int.zero)))))) = Vnull -> i5 =a /\ i6 = b.
Lemma prio_from_grp_tbl_PrioWaitInQ :
  forall grp evnt_rdy_tbl x1 x2 x3,
    length evnt_rdy_tbl = ∘OS_EVENT_TBL_SIZE ->
    RL_Tbl_Grp_P evnt_rdy_tbl (Vint32 grp) ->
    Int.unsigned x2 <= 255 ->
    Int.unsigned grp <= 255 ->
    grp <> $ 0 ->
    nth_val´ (Z.to_nat (Int.unsigned grp)) OSUnMapVallist = Vint32 x1 ->
    nth_val´ (Z.to_nat (Int.unsigned x1)) evnt_rdy_tbl = Vint32 x2 ->
    nth_val´ (Z.to_nat (Int.unsigned x2)) OSUnMapVallist = Vint32 x3 ->
    PrioWaitInQ (Int.unsigned ((x1<<$ 3)+ᵢx3)) evnt_rdy_tbl.

Lemma int_ltu_zero_one_true : Int.ltu Int.zero Int.one = true.
Lemma int_ltu_zero_notbool_one_false : Int.ltu Int.zero (Int.notbool Int.one) = false.
Lemma int_ltu_zero_zero_false : Int.ltu Int.zero Int.zero = false.

Lemma int_ltu_zero_notbool_zero_true : Int.ltu Int.zero (Int.notbool Int.zero) = true.


Lemma mutexacc_null_absinfer:forall P, can_change_aop P -> absinfer
     ( <|| mutexacc (Vnull :: nil) ||> **
     P) (<|| END (Some (V$0)) ||> **
     P).

Lemma mutexacc_no_mutex_err_absinfer:
  forall P mqls x v1 v3 ct,
    can_change_aop P ->
    (~ exists a b wl,EcbMod.get mqls x = Some (absmutexsem a b,wl)) ->
    absinfer
      ( <|| mutexacc (Vptr x :: nil) ||> ** HECBList mqls ** HTCBList v1 **
      HTime v3 **
      HCurTCB ct **
            P)
      (<|| END (Some (V$0)) ||> ** HECBList mqls ** HTCBList v1 **
      HTime v3 **
      HCurTCB ct **
     P).

Lemma mutexacc_no_available_absinfer:
  forall P mqls x wl p o v1 v3 ct,
    can_change_aop P ->
    EcbMod.get mqls x = Some (absmutexsem p (Some o),wl)->
    absinfer
      ( <|| mutexacc (Vptr x :: nil) ||> **
            HECBList mqls ** HTCBList v1 **
      HTime v3 **
      HCurTCB ct ** P)
      (<|| END (Some (V$0)) ||> ** HECBList mqls ** HTCBList v1 **
      HTime v3 **
      HCurTCB ct **
                    P).

  Lemma mutexacc_prio_err_absinfer:
    forall P mqls x wl p v1 v3 ct pt st m owner,
      can_change_aop P ->
      EcbMod.get mqls x = Some (absmutexsem p owner,wl)-> TcbMod.get v1 ct = Some (pt,st,m) ->
      Int.ltu p pt = false ->
      absinfer
        ( <|| mutexacc (Vptr x :: nil) ||> **
              HECBList mqls ** HTCBList v1 **
              HTime v3 **
              HCurTCB ct ** P)
        (<|| END (Some (V$0)) ||> ** HECBList mqls ** HTCBList v1 **
             HTime v3 **
             HCurTCB ct **
             P).

Lemma mutexacc_succ_absinfer:
  forall P mqls x wl v1 v3 ct p pt st m,
    can_change_aop P ->
    EcbMod.get mqls x = Some (absmutexsem p None,wl) ->
    TcbMod.get v1 ct = Some (pt,st,m) ->
   Int.ltu p pt = true->
    absinfer
      ( <|| mutexacc (Vptr x :: nil) ||> **
            HECBList mqls ** HTCBList v1 **
      HTime v3 **
      HCurTCB ct **
       P)
      (<|| END (Some (V$1)) ||> ** HECBList (EcbMod.set mqls x (absmutexsem p (Some (ct,pt)),wl)) ** HTCBList v1 **
      HTime v3 **
      HCurTCB ct **
                    P).


  Lemma RLH_ECBData_p_high_mbox_acpt_hold:forall x e w0 i6 v´50, Int.unsigned i6 < 64-> Int.ltu (Int.shru x ($ 8)) i6 = true-> RLH_ECBData_P (DMutex (Vint32 x) Vnull) (e, w0) -> RLH_ECBData_P
                                                                                                                                                (DMutex (Vint32 (Int.or (x&$ OS_MUTEX_KEEP_UPPER_8) i6))
                                                                                                                                                        (Vptr (v´50, Int.zero))) (absmutexsem (Int.shru ( Int.or (x & $ OS_MUTEX_KEEP_UPPER_8) i6) ($ 8)) ( Some
                                                                                                                                                                                                                                                              (v´50, Int.zero, i6)), w0)
  .
  Lemma l2 : forall T b (a:T), (a::nil) ++ b = a :: b.


Lemma mutexcre_error_absinfer :
  forall P i,
    can_change_aop P ->
    (Int.unsigned i <=? 255 = true) ->
    absinfer ( <|| mutexcre (Vint32 i :: nil) ||> ** P)
           ( <|| END (Some Vnull) ||> ** P).

Lemma mutexcre_succ_absinfer :
  forall P i qid qls tcbls curtid tm,
    can_change_aop P ->
    (Int.unsigned i <=? 255 = true) ->
    prio_available i tcbls ->
    Int.ltu i (Int.repr OS_LOWEST_PRIO)= true ->
    EcbMod.get qls qid = None ->
    absinfer ( <|| mutexcre (Vint32 i :: nil) ||>
                 **HECBList qls ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
           ( <|| END (Some (Vptr qid)) ||> **
                 HECBList (EcbMod.set qls qid (absmutexsem i
                                                       None,
                                               nil:list tid)) **HTCBList tcbls ** HTime tm **
                 HCurTCB curtid **P).
Lemma intlemma1 :forall v´19 v´21, id_addrval´ (Vptr (v´21, Int.zero)) OSEventTbl OS_EVENT = Some v´19 -> (v´21, Int.zero+ᵢ($ 4+ᵢ($ 2+ᵢ($ 1+ᵢ($ 1+ᵢInt.zero))))) = v´19.

Lemma val_inj_eq´
     : forall a ,
       val_inj
         (notint
            (val_inj
               a)) = Vint32 Int.zero \/
       val_inj
         (notint
            (val_inj
               a)) = Vnull ->
       (exists v, a= Some (Vint32 v)) /\a <> Some (Vint32 Int.zero).
Lemma val_eq_some_not_zero : forall xx xxx x,
                               val_eq xx xxx = Some (Vint32 x) ->
                               val_eq xx xxx <> Some (Vint32 Int.zero) ->
                               xx= xxx.
 Lemma R_PrioTbl_P_update_vhold : forall i v´5 v´14 v´17, Int.unsigned i < 63->R_PrioTbl_P v´5 v´14 v´17 -> nth_val´ (Z.to_nat (Int.unsigned i)) v´5 = Vnull -> R_PrioTbl_P (update_nth_val (Z.to_nat (Int.unsigned i)) v´5 (Vptr v´17)) v´14 v´17.

 Lemma RL_RTbl_PrioTbl_P_update_vhold : forall i v´5 v´11 v´17, Int.unsigned i < 63-> RL_RTbl_PrioTbl_P v´11 v´5 v´17 -> nth_val´ (Z.to_nat (Int.unsigned i)) v´5 = Vnull -> RL_RTbl_PrioTbl_P v´11
     (update_nth_val (Z.to_nat (Int.unsigned i)) v´5 (Vptr v´17)) v´17.

Lemma ECBList_Mutex_Create_prop :
  forall v´41 v´50 v´22 v´28 v´40
          v´37 v´38 v´27 x i,

    Int.unsigned i < 63 ->
    RH_TCBList_ECBList_P v´37 v´38 v´40 ->
    EcbMod.get v´37 (v´41, Int.zero) = None ->
    ECBList_P v´22 Vnull v´28 v´27 v´37 v´38->
    ECBList_P (Vptr (v´41, Int.zero)) Vnull
              
              ((V$OS_EVENT_TYPE_MUTEX :: Vint32 Int.zero :: val_inj
               (or
                  (val_inj
                     (if Int.ltu ($ 8) Int.iwordsize
                      then Some (Vint32 (i<<$ 8))
                      else None)) (V$OS_MUTEX_AVAILABLE)) :: x :: v´50 :: v´22 :: nil, INIT_EVENT_TBL) :: v´28)
              (DMutex (val_inj
               (or
                  (val_inj
                     (if Int.ltu ($ 8) Int.iwordsize
                      then Some (Vint32 (i<<$ 8))
                      else None)) (V$OS_MUTEX_AVAILABLE))) Vnull :: v´27)
              (EcbMod.set v´37 (v´41, Int.zero) (absmutexsem i None, nil))
              v´38.

 Lemma create_val_inj_lemma0: forall i v´5, val_inj
         (notint
            (val_inj
               (val_eq (nth_val´ (Z.to_nat (Int.unsigned i)) v´5) Vnull))) =
       Vint32 Int.zero \/
       val_inj
         (notint
            (val_inj
               (val_eq (nth_val´ (Z.to_nat (Int.unsigned i)) v´5) Vnull))) =
       Vnull ->(nth_val´ (Z.to_nat (Int.unsigned i)) v´5) = Vnull.
   Lemma priotbl_null_no_tcb :forall v´5 v´14 v´17 i, R_PrioTbl_P v´5 v´14 v´17 -> nth_val (Z.to_nat (Int.unsigned i)) v´5 = Some Vnull -> (~ exists x st msg, TcbMod.get v´14 x = Some ( i, st, msg)).

Lemma Mutex_Create_TCB_prop :
  forall v´37 x i v´38 v´40,
    ~ (exists x st msg, TcbMod.get v´38 x = Some (i, st, msg)) ->
    EcbMod.get v´37 x = None ->
    RH_TCBList_ECBList_P v´37 v´38 v´40 ->
    RH_TCBList_ECBList_P
      (EcbMod.set v´37 x (absmutexsem i None, nil))
      v´38 v´40.

 Lemma mutex_createpure : forall v´5 v´14 v´17 i, R_PrioTbl_P v´5 v´14 v´17 -> nth_val´ (Z.to_nat (Int.unsigned i)) v´5 = Vnull -> prio_available i v´14.


Lemma mutexdel_null_absinfer:
  forall P ,
    can_change_aop P ->
    absinfer (<|| mutexdel (Vnull :: nil) ||> ** P)
           ( <|| END (Some (V$ OS_ERR_PEVENT_NULL)) ||> ** P).

Lemma mutexdel_no_mutex_err_absinfer:
  forall x a P tcbls tm curtid,
    can_change_aop P ->
    EcbMod.get x a = None ->
    absinfer (<|| mutexdel (Vptr a :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
           ( <|| END (Some (V$ OS_ERR_PEVENT_NO_EX)) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).

Lemma mutexdel_type_err_absinfer:
  forall ecbls a P X tcbls tm curtid,
    can_change_aop P ->
    EcbMod.get ecbls a = Some X ->
    (~ exists x y wl, X = (absmutexsem x y, wl))->
    absinfer (<|| mutexdel (Vptr a :: nil) ||> ** HECBList ecbls ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
           ( <|| END (Some (V$OS_ERR_EVENT_TYPE)) ||> ** HECBList ecbls ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).

Lemma mutexdel_ex_wt_err_absinfer:
  forall x a P p o tl tcbls tm curtid ,
    can_change_aop P ->
    EcbMod.get x a = Some (absmutexsem p (Some o), tl)->
    absinfer (<|| mutexdel (Vptr a :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P)
           ( <|| END (Some (V$ OS_ERR_TASK_WAITING)) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).

Lemma mutexdel_succ_absinfer:
  forall x a P z x´ tid t tcbls ,
    can_change_aop P ->
    EcbMod.get x a = Some (absmutexsem z None, nil) ->
    EcbMod.join x´ (EcbMod.sig a (absmutexsem z None, nil)) x ->
    absinfer (<|| mutexdel (Vptr a :: nil) ||> **
                HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB tid ** P)
           ( <|| END (Some (V$ NO_ERR)) ||> ** HECBList x´ ** HTCBList tcbls **
                 HTime t ** HCurTCB tid ** P).

Lemma mutexdel_pr_not_holder_err_absinfer:
  forall P tcbls x curtid tm a,
    can_change_aop P ->
    absinfer (<|| mutexdel (Vptr a ::nil)||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P) ( <|| END (Some (V$ OS_ERR_MUTEXPR_NOT_HOLDER))||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).

Lemma ecb_wt_ex_prop_mutex :
  forall
    v´43 v´34 v´38 x v´21 tid
    v´23 v´35 i i3 x2 x3 v´42 v´40,
    Int.eq i ($ 0) = false ->
    Int.unsigned i <= 255 ->
    array_type_vallist_match Int8u v´40 ->
    length v´40 = ∘OS_EVENT_TBL_SIZE ->
    RL_Tbl_Grp_P v´40 (Vint32 i) ->
    ECBList_P v´38 (Vptr x) v´21 v´23 v´43 v´35->
    R_ECB_ETbl_P x
                 (V$OS_EVENT_TYPE_MUTEX
                   :: Vint32 i
                   :: Vint32 i3 :: x2 :: x3 :: v´42 :: nil,
                  v´40) v´35 ->
    RH_TCBList_ECBList_P v´34 v´35 tid ->
    exists z zz t´ tl,
      EcbMod.get v´34 x = Some (absmutexsem z zz, t´ :: tl).

Lemma inteq_has_value: forall a b, (exists x, (notint
                   (val_inj
                      (if Int.eq a b
                       then Some (Vint32 Int.one)
                       else Some (Vint32 Int.zero))) = Some x)).

Lemma upd_last_prop:
  forall v g x vl z ,
    V_OSEventListPtr v = Some x ->
    vl = upd_last_ectrls ((v, g) :: nil) z ->
    exists v´, vl = ((v´, g) ::nil) /\ V_OSEventListPtr v´ = Some z.

Lemma nth_val_upd_prop:
  forall vl n m v x,
    (n<>m)%nat ->
    (nth_val n (update_nth val m vl v) = Some x <->
     nth_val n vl = Some x).

Lemma R_ECB_upd_hold :
  forall x1 v v0 v´36 x8,
    R_ECB_ETbl_P x1 (v, v0) v´36 ->
    R_ECB_ETbl_P x1 (update_nth val 5 v x8, v0) v´36.

Lemma ecb_list_join_join :
  forall v´40 v´52 v´61 v´21 x x2 v´36 x8 v´42 v´37 x0 v´51,
     v´40 <> nil ->
     ECBList_P v´52 (Vptr (v´61, Int.zero)) v´40 v´21 x v´36 ->
     ECBList_P x8 Vnull v´42 v´37 x0 v´36 ->
     v´51 = upd_last_ectrls v´40 x8 ->
     EcbMod.join x0 x x2 ->
     ECBList_P v´52 Vnull (v´51 ++ v´42) (v´21 ++ v´37) x2 v´36.

Lemma ecblist_ecbmod_get_aux_mutex :
  forall v´61 i6 x4 x8 v´58 v´42
         v´63 x20 v´37 v´35 v´36 v´38 x21,
    array_type_vallist_match Int8u v´58->
    RH_CurTCB v´38 v´36 ->
    length v´58 = ∘OS_EVENT_TBL_SIZE ->
    RH_TCBList_ECBList_P v´35 v´36 v´38 ->
    RL_Tbl_Grp_P v´58 (V$0) ->
    ECBList_P (Vptr (v´61, Int.zero)) Vnull
              (
                   ((V$OS_EVENT_TYPE_MUTEX
                      :: V$0 :: Vint32 i6 :: v´63 :: x4 :: x8 :: nil,
                     v´58) :: nil) ++ v´42)
                                       ((DMutex x20 x21 :: nil) ++ v´37) v´35 v´36 ->
    exists msgls xx,
      EcbMod.get v´35 (v´61, Int.zero) = Some (absmutexsem msgls xx, nil)
    /\ exists vv, EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmutexsem msgls xx, nil)) v´35 /\ECBList_P x8 Vnull v´42 v´37 vv v´36.

Lemma ecblist_ecbmod_get_mutex :
  forall v´61 i6 x4 x8 v´58 v´42 v´21 v´63 x20 v´37 v´35 v´36 v´38 x21,
    length v´21 = O ->
    array_type_vallist_match Int8u v´58->
    RH_CurTCB v´38 v´36 ->
    length v´58 = ∘OS_EVENT_TBL_SIZE ->
    RH_TCBList_ECBList_P v´35 v´36 v´38 ->
    RL_Tbl_Grp_P v´58 (V$0) ->
    ECBList_P (Vptr (v´61, Int.zero)) Vnull
              (nil ++
                   ((V$OS_EVENT_TYPE_MUTEX
                      :: V$0 :: Vint32 i6 :: v´63 :: x4 :: x8 :: nil,
                     v´58) :: nil) ++ v´42)
              (v´21 ++
                    (DMutex x20 x21 :: nil) ++ v´37) v´35 v´36 ->
    exists msgls xx,
      EcbMod.get v´35 (v´61, Int.zero) = Some (absmutexsem msgls xx, nil)
      /\ exists vv, EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmutexsem msgls xx, nil)) v´35 /\ECBList_P x8 Vnull v´42 v´37 vv v´36.
  Goal forall i0,val_inj
          (notint
             (val_inj
                (if Int.eq i0 ($ 0)
                 then Some (Vint32 Int.one)
                 else Some (Vint32 Int.zero)))) = Vint32 Int.zero -> i0 = $0.

Lemma get_last_prop:
  forall (l : list EventCtr) x v y,
    l <> nil ->
    (get_last_ptr ((x, v) :: l) = y <->
     get_last_ptr l = y).

Lemma ecblist_p_decompose :
  forall y1 z1 x y2 z2 t z ,
    length y1 = length y2 ->
    ECBList_P x Vnull (y1++z1) (y2++z2) t z ->
    exists x1 t1 t2,
      ECBList_P x x1 y1 y2 t1 z /\ ECBList_P x1 Vnull z1 z2 t2 z /\
      EcbMod.join t1 t2 t /\ (get_last_ptr y1 = None \/ get_last_ptr y1 = Some x1).

Lemma ecblist_ecbmod_get_mutex´ :
  forall v´40 v´52 v´61 i6 x4 x8 v´58 v´42 v´21 xx
         v´63 x20 i5 v´37 v´35 v´36 v´38 x21,
    Some (Vptr (v´61, Int.zero)) = get_last_ptr v´40 ->
    length v´40 = length v´21 ->
    Int.unsigned i5 <= 65535 ->
    array_type_vallist_match Int8u v´58->
    RH_CurTCB v´38 v´36 ->
    length v´58 = ∘OS_EVENT_TBL_SIZE ->
    RH_TCBList_ECBList_P v´35 v´36 v´38 ->
    RL_Tbl_Grp_P v´58 (V$0) ->
    ECBList_P v´52 Vnull
              (v´40 ++
                    ((V$OS_EVENT_TYPE_MUTEX
                       :: xx :: Vint32 i6 :: v´63 :: x4 :: x8 :: nil,
                      v´58) :: nil) ++ v´42)
              (v´21 ++
                                              (DMutex x20 x21 :: nil) ++ v´37) v´35 v´36 ->
 
     exists msgls xx,
      EcbMod.get v´35 (v´61, Int.zero) = Some (absmutexsem msgls xx, nil)
    /\ exists vg vv vx,
         ECBList_P v´52 (Vptr (v´61, Int.zero)) v´40 v´21 vg v´36 /\
         EcbMod.join vg vx v´35/\
         EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmutexsem msgls xx, nil)) vx/\
         ECBList_P x8 Vnull v´42 v´37 vv v´36.

  Lemma R_Prio_Tbl_P_hold_for_del :
    forall v´29 v´38 v´50 v´37 v´40 x x0 v´66,
      nth_val (Z.to_nat (Int.unsigned x)) v´29 =Some (Vptr v´50)->
      EcbMod.join x0 (EcbMod.sig (v´66, Int.zero) (absmutexsem x None, nil)) v´37 ->
      0<= Int.unsigned x <64 ->
      length v´29 = 64%nat ->
      R_PrioTbl_P v´29 v´38 v´50 ->
      RH_TCBList_ECBList_P v´37 v´38 v´40 ->
      R_PrioTbl_P (update_nth_val (Z.to_nat (Int.unsigned x)) v´29 Vnull) v´38 v´50.
  Lemma val_eq_lemma001 :forall x0 v´50, val_inj (notint (val_inj (val_eq x0 (Vptr v´50)))) = Vint32 Int.zero \/
        val_inj (notint (val_inj (val_eq x0 (Vptr v´50)))) = Vnull -> x0= Vptr v´50.

  Lemma RL_RTbl_PrioTbl_P_hold_for_del: forall v´29 v´38 v´50 v´37 v´40 x x0 v´66 v´35,
      nth_val (Z.to_nat (Int.unsigned x)) v´29 =Some (Vptr v´50)-> EcbMod.join x0
          (EcbMod.sig (v´66, Int.zero) (absmutexsem x None, nil)) v´37 -> 0<= Int.unsigned x <64 -> length v´29 = 64%nat -> R_PrioTbl_P v´29 v´38 v´50 -> RH_TCBList_ECBList_P v´37 v´38 v´40 -> RL_RTbl_PrioTbl_P v´35 v´29 v´50-> RL_RTbl_PrioTbl_P v´35
     (update_nth_val
        (Z.to_nat (Int.unsigned x )) v´29
        Vnull) v´50.
  Goal forall v´35 v´36 x y , RH_TCBList_ECBList_MUTEX_OWNER v´35 v´36 -> EcbMod.join x y v´35 -> RH_TCBList_ECBList_MUTEX_OWNER x v´36.
Lemma ecb_del_prop_RHhold:
  forall v´35 v´36 v´38 x y absmg,
    RH_TCBList_ECBList_P v´35 v´36 v´38 ->
    EcbMod.join x (EcbMod.sig y (absmg, nil))
                v´35 -> RH_TCBList_ECBList_P x v´36 v´38 .

  Lemma ltu_eq_false_ltu´:
    forall a b,
      Int.ltu a b = false ->
      Int.eq a b = false ->
      Int.ltu b a = true.


Lemma AOSRdyTblGrp_fold:
  forall s P v´38 v´39,
    s |= GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE) v´38 **
         AOSRdyGrp v´39 ** P ->
    array_type_vallist_match Int8u v´38 /\ length v´38 = ∘OS_RDY_TBL_SIZE ->
    RL_Tbl_Grp_P v´38 v´39 /\ prio_in_tbl ($ OS_IDLE_PRIO) v´38 ->
    s |= AOSRdyTblGrp v´38 v´39 ** P.

Lemma mutexpend_TCBNode_P_in_tcb_rdy:
  forall v´51 v´22 xs x9 x8 i9 i8 i6 i5 i4 i3 xx rtbl,
    array_type_vallist_match Int8u rtbl ->
    length rtbl = ∘OS_RDY_TBL_SIZE ->
    TCBNode_P (v´51
                  :: v´22
                  :: x9
                  :: x8
                  :: Vint32 i9
                  :: Vint32 i8
                  :: Vint32 xx
                  :: Vint32 i6
                  :: Vint32 i5
                  :: Vint32 i4 :: Vint32 i3 :: nil)
              rtbl (xx, xs, x8) ->
    i9 = $ 0 ->
    i8 = $ OS_STAT_RDY ->
    xs = rdy.

Lemma absinfer_mutex_pend_ptcb_is_cur:
  forall P ecbls tcbls t ct v pr wls eid p´ ptcb,
    Int.unsigned v <= 65535 ->
    EcbMod.get ecbls eid = Some (absmutexsem pr (Some (ptcb, p´)), wls) ->
    ptcb = ct ->
    can_change_aop P ->
    absinfer
      (<|| mutexpend (Vptr eid :: Vint32 v :: nil) ||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P)
      (<|| END (Some (Vint32 (Int.repr OS_ERR_MUTEX_DEADLOCK)))||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P).

Lemma absinfer_mutex_pend_ptcb_is_idle:
  forall P ecbls tcbls t ct v pr wls eid p´ ptcb st msg,
    Int.unsigned v <= 65535 ->
    EcbMod.get ecbls eid = Some (absmutexsem pr (Some (ptcb, p´)), wls) ->
    TcbMod.get tcbls ptcb = Some (Int.repr OS_IDLE_PRIO,st,msg) ->
    can_change_aop P ->
    absinfer
      (<|| mutexpend (Vptr eid :: Vint32 v :: nil) ||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P)
      (<|| END (Some (Vint32 (Int.repr OS_ERR_MUTEX_IDLE)))||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P).

Lemma absinfer_mutex_pend_ptcb_is_not_rdy:
  forall P ecbls tcbls t ct v pr wls eid p´ ptcb st msg ptcb_prio cur_prio m,
    Int.unsigned v <= 65535 ->
    EcbMod.get ecbls eid = Some (absmutexsem pr (Some (ptcb, p´)), wls) ->
    TcbMod.get tcbls ptcb = Some (ptcb_prio ,st,msg) ->
    TcbMod.get tcbls ct = Some (cur_prio,rdy,m) ->
    ~ st = rdy ->
    can_change_aop P ->
    absinfer
      (<|| mutexpend (Vptr eid :: Vint32 v :: nil) ||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P)
      (<|| END (Some (Vint32 (Int.repr OS_ERR_NEST)))||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P).

Lemma absinfer_mutex_pend_cur_prio_eql_mprio:
  forall P ecbls tcbls t ct v pr wls eid p´ ptcb st msg cur_prio,
    Int.unsigned v <= 65535 ->
    EcbMod.get ecbls eid = Some (absmutexsem pr (Some (ptcb, p´)), wls) ->
    TcbMod.get tcbls ct = Some (cur_prio ,st,msg) ->
    p´ = cur_prio ->
    can_change_aop P ->
    absinfer
      (<|| mutexpend (Vptr eid :: Vint32 v :: nil) ||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P)
      (<|| END (Some (Vint32 (Int.repr OS_ERR_MUTEX_DEADLOCK)))||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P).

Lemma absinfer_mutex_pend_pip_is_not_hold:
  forall P ecbls tcbls t ct v eid,
    Int.unsigned v <= 65535 ->
    can_change_aop P ->
    absinfer
      (<|| mutexpend (Vptr eid :: Vint32 v :: nil) ||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P)
      (<|| END (Some (Vint32 (Int.repr OS_ERR_MUTEXPR_NOT_HOLDER)))||> **
           HECBList ecbls **
           HTCBList tcbls **
           HTime t **
           HCurTCB ct ** P).

Lemma seporI2 : forall p q p´, (p´ ==> p) -> p´ ==> p \\// q.
Lemma seporI2´ : forall p q p´, (p´ ==> p) -> p´ ==> q \\// p.

Lemma post_valinjlemma1 : forall v0 v´51, val_inj (notint (val_inj (val_eq v0 (Vptr v´51)))) = Vint32 Int.zero \/
                                           val_inj (notint (val_inj (val_eq v0 (Vptr v´51)))) = Vnull -> v0 = (Vptr v´51).

Lemma absinfer_mutexpost_return_exwt_succ:
  forall P mqls x wl tls t ct st m m´ st´ t´ p´ pr op,
    can_change_aop P ->
    EcbMod.get mqls x = Some (absmutexsem pr (Some (ct, op)) ,wl) ->
    ~ wl=nil ->
    GetHWait tls wl t´ ->
    TcbMod.get tls ct= Some (pr, st, m) ->
    TcbMod.get tls t´ = Some (p´, st´, m´) ->
    absinfer
      ( <|| mutexpost (Vptr x :: nil) ||> **
            HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
      (<|| isched;;END (Some (Vint32 (Int.repr NO_ERR))) ||> ** HECBList (EcbMod.set mqls x (absmutexsem pr (Some (t´, p´)), (remove_tid t´ wl))) ** HTCBList (TcbMod.set (TcbMod.set tls ct (op, st, m)) t´ (p´, rdy, (Vptr x)) ) ** HTime t ** HCurTCB ct ** P).

Lemma absinfer_mutexpost_noreturn_exwt_succ:
  forall P mqls x wl tls t ct st m m´ st´ t´ p´ pr op p,
    can_change_aop P ->
    EcbMod.get mqls x = Some (absmutexsem pr (Some (ct, op)) ,wl) ->
    Int.eq p pr = false /\
    ~ wl=nil ->
    GetHWait tls wl t´ ->
    TcbMod.get tls ct= Some (p, st, m) ->
    TcbMod.get tls t´ = Some (p´, st´, m´) ->
    absinfer
      ( <|| mutexpost (Vptr x :: nil) ||> **
            HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
      (<|| isched;;END (Some (Vint32 (Int.repr NO_ERR))) ||> ** HECBList (EcbMod.set mqls x (absmutexsem pr (Some (t´, p´)), (remove_tid t´ wl))) ** HTCBList (TcbMod.set tls t´ (p´, rdy, (Vptr x)) ) ** HTime t ** HCurTCB ct ** P).
Goal forall x y, Int.eq x y = true -> x=y.

Lemma Astruct_PV_neq1 :
  forall s p1 p2 v2 h vl P,
    s |= Astruct p1 OS_TCB (h::vl) ** PV p2 @ Int8u |-> v2 ** P ->
    p1 <> p2.

Lemma absinfer_mutexpost_exwt_no_return_prio_succ :
  forall qls qls´ qid p p´ p´´ t t´ pt wl tls tls´ st st´ m m´ tm P,
    can_change_aop P ->
    EcbMod.get qls qid = Some (absmutexsem p (Some (t, pt)), wl) ->
    wl <> nil ->
    GetHWait tls wl t´ ->
    Int.eq p´´ p = false ->
    TcbMod.get tls t = Some (p´´, st, m) ->
    TcbMod.get tls t´ = Some (p´, st´, m´) ->
    tls´ = TcbMod.set tls t´ (p´, rdy, Vptr qid) ->
    qls´ = EcbMod.set qls qid (absmutexsem p (Some (t´, p´)), remove_tid t´ wl) ->
    absinfer
      (<|| mutexpost (Vptr qid :: nil) ||> **
           HECBList qls ** HTCBList tls ** HTime tm ** HCurTCB t ** P)
      (<|| isched;; END Some (V$NO_ERR) ||> **
           HECBList qls´ ** HTCBList tls´ ** HTime tm ** HCurTCB t ** P).

Lemma zh_asdf1 :
  forall
    (v´79 : int32)
    (H137 : Int.unsigned v´79 <= 255)
    (H125 : Int.eq (v´79&Int.not ($ OS_STAT_MUTEX)) ($ OS_STAT_RDY) = true),
    $ OS_STAT_RDY = v´79&Int.not ($ OS_STAT_MUTEX).

Lemma nth_val´_length :
  forall l n,
    nth_val´ n l <> Vundef ->
    (n < length l)%nat.

Lemma zh_asdf:
  forall (v´54 : int32)
         (v´62 : int32)
         (v´64 : int32),
    val_inj
      (bool_and (val_inj (notint (val_inj (Some (Vint32 Int.zero)))))
                (val_inj
                   (bool_or
                      (val_inj
                         (if Int.ltu ((v´62<<$ 3)+ᵢv´64) (v´54>>ᵢ$ 8)
                          then Some (Vint32 Int.one)
                          else Some (Vint32 Int.zero)))
                      (val_inj
                         (if Int.eq ((v´62<<$ 3)+ᵢv´64) (v´54>>ᵢ$ 8)
                          then Some (Vint32 Int.one)
                          else Some (Vint32 Int.zero)))))) =
    Vint32 Int.zero \/
    val_inj
      (bool_and (val_inj (notint (val_inj (Some (Vint32 Int.zero)))))
                (val_inj
                   (bool_or
                      (val_inj
                         (if Int.ltu ((v´62<<$ 3)+ᵢv´64) (v´54>>ᵢ$ 8)
                          then Some (Vint32 Int.one)
                          else Some (Vint32 Int.zero)))
                      (val_inj
                         (if Int.eq ((v´62<<$ 3)+ᵢv´64) (v´54>>ᵢ$ 8)
                          then Some (Vint32 Int.one)
                          else Some (Vint32 Int.zero)))))) = Vnull
    ->
    Int.ltu (v´54>>ᵢ$ 8) ((v´62<<$ 3)+ᵢv´64) = true.

Lemma GetHWait_In :
  forall w v´61 v´86,
    GetHWait v´61 w (v´86, Int.zero) -> In (v´86, Int.zero) w.

Lemma tcb_join_join_merge :
  forall m1 m2 m3 m4 m5,
    TcbMod.join m1 m2 m3 ->
    TcbMod.join m4 m5 m2 ->
    TcbMod.join m4 (TcbMod.merge m1 m5) m3.

Lemma or_OS_MUTEX_AVAILABLE_le_65535 :
  forall x, Int.unsigned x <= 65535 ->
            Int.unsigned (Int.or x ($ OS_MUTEX_AVAILABLE)) <= 65535.

Lemma absinfer_mutexpost_nowt_no_return_prio_succ :
  forall qls qls´ qid p p´ p´´ t tm tls st m P,
    can_change_aop P ->
    EcbMod.get qls qid = Some (absmutexsem p (Some (t, p´)), nil) ->
    TcbMod.get tls t = Some (p´´, st, m) ->
    Int.eq p´´ p = false ->
    qls´ = EcbMod.set qls qid (absmutexsem p None, nil) ->
    absinfer
      (<|| mutexpost (Vptr qid :: nil) ||> **
           HECBList qls ** HTCBList tls ** HTime tm ** HCurTCB t ** P)
      (<|| END Some (V$NO_ERR) ||> **
           HECBList qls´ ** HTCBList tls ** HTime tm ** HCurTCB t ** P).

Lemma isptr_zh :
  forall x, isptr x ->
            match x with
              | Vundef => false
              | Vnull => true
              | Vint32 _ => false
              | Vptr _ => true
            end = true.

Lemma evsllseg_aux:
  forall l1 s a b l2 P,
    s |= evsllseg a b l1 l2 ** P ->
    (a = b /\ l1 = nil \/ get_last_ptr l1 = Some b) /\ length l1 = length l2.
Lemma mutex_rh_tcblist_ecblist_p_hold: forall v´34 v´35 v´37 v w m y, EcbMod.get v´34 v = Some (absmutexsem m y, w) ->RH_TCBList_ECBList_P v´34 v´35 v´37 ->
                                                                      RH_TCBList_ECBList_P
                                                                        (EcbMod.set v´34 v (absmutexsem m None, w)) v´35 v´37.

Lemma intlemmaf: forall i, val_inj
                              (notint
                                 (val_inj
                                    (if Int.eq i ($ 0)
                                     then Some (Vint32 Int.one)
                                     else Some (Vint32 Int.zero)))) <>
                            Vint32 Int.zero -> i <> Int.zero.

Lemma return_rh_ctcb :forall v´52 v´39 a b c, RH_CurTCB (v´52, Int.zero) (TcbMod.set v´39 (v´52, Int.zero) (a, b, c)).

Lemma rg1 : forall x2 x6 , 0 <= Int.unsigned x2 < 64->
                             x6 = $ Int.unsigned x2&$ 7 ->
                             0<= Int.unsigned x6 < 8.

Lemma rg2 : forall x2 x7 , 0 <= Int.unsigned x2 < 64->
                             x7 = Int.shru ($ Int.unsigned x2) ($ 3) ->
                             0<= Int.unsigned x7 < 8.

Lemma something_in_not_nil : forall (T:Type) (y: @list T), y<>nil -> exists x, In x y.

Lemma post_exwt_succ_pre_mutex´
: forall (v´36 v´13 : vallist) (v´12 : int32)
         (v´32 : block) (v´15 : int32) (v´24 : val)
         (v´35 v´0 : val) (v´8 : tid) (v´9 v´11 : EcbMod.map)
         x (x1 : waitset)
         (v´6 v´10 : EcbMod.map) (v´38 v´69 v´39 : int32)
         (v´58 : block) (a : priority)
         (c : msg) (v´62 v´7 : TcbMod.map)
         (vhold : addrval) y,
    v´12 = Int.zero ->
    R_PrioTbl_P v´36 v´7 vhold ->
    RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
    R_ECB_ETbl_P (v´32, Int.zero)
                 (V$OS_EVENT_TYPE_MUTEX
                   :: Vint32 v´12
                   :: Vint32 v´15 :: v´24 :: v´35 :: v´0 :: nil,
                  v´13) v´7 ->
    RH_TCBList_ECBList_P v´11 v´7 v´8 ->
    EcbMod.join v´9 v´10 v´11 ->
    EcbMod.joinsig (v´32, Int.zero) (absmutexsem x y , x1) v´6 v´10 ->
    x1 = nil
.

Lemma absinfer_mutexpost_return_nowt_succ:
  forall P mqls x tls t ct st m pr op,
    can_change_aop P ->
    EcbMod.get mqls x = Some (absmutexsem pr (Some (ct, op)) ,nil) ->
    TcbMod.get tls ct= Some (pr, st, m) ->
    Int.eq pr op = false ->
    absinfer
      ( <|| mutexpost (Vptr x :: nil) ||> **
            HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
      (<|| END (Some (Vint32 (Int.repr NO_ERR))) ||> ** HECBList (EcbMod.set mqls x (absmutexsem pr None, nil)) ** HTCBList (TcbMod.set tls ct (op, st, m)) ** HTime t ** HCurTCB ct ** P).

Lemma intcbnotvhold :forall ptbl tcbls vhold tcbptr p s m, R_PrioTbl_P ptbl tcbls vhold -> TcbMod.get tcbls tcbptr = Some (p, s, m) -> tcbptr <> vhold.

Lemma valinjlemma1: forall a b, val_inj
                                   (if Int.eq a b
                                    then Some (Vint32 Int.one)
                                    else Some (Vint32 Int.zero)) <> Vint32 Int.zero -> a= b.
Lemma val_inj2 : forall x x6, val_inj
                                 (if Int.eq x6 x
                                  then Some (Vint32 Int.one)
                                  else Some (Vint32 Int.zero)) <> Vint32 Int.zero -> x6 = x.