Library oscore_common
Require Import ucert.
Require Import OSTimeDlyPure.
Require Import OSQPostPure.
Require Import laby.
Require Import mathlib.
Open Scope code_scope.
Definition highest_rdy prio rtbl :=
(Int.unsigned prio < 64) /\
prio_in_tbl prio rtbl /\
forall prio´, 0 <= Int.unsigned prio´ < 64-> Int.eq prio prio´ = false -> prio_in_tbl prio´ rtbl -> Int.ltu prio prio´ = true.
Lemma get_highest_rdy:
forall rgrp rtbl x i0 y,
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE->
RL_Tbl_Grp_P rtbl (Vint32 rgrp) ->
(Int.unsigned rgrp <= 255) ->
nth_val´ (Z.to_nat (Int.unsigned rgrp)) OSUnMapVallist = Vint32 x ->
nth_val´ (Z.to_nat (Int.unsigned x)) rtbl = Vint32 i0 ->
nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 y ->
highest_rdy ((x<<$ 3) +ᵢ y) rtbl.
Lemma highest_rdy_eq´:
forall prio rtbl ptbl tcbls ct l1 l2 p1 hcurt P s t vhold,
t <> vhold ->
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE->
highest_rdy prio rtbl ->
nth_val´ (Z.to_nat (Int.unsigned prio)) ptbl = Vptr t ->
R_PrioTbl_P ptbl tcbls vhold ->
s |= AOSTCBList p1 (Vptr ct) l1 l2 rtbl hcurt tcbls ** HTCBList tcbls **P ->
s |= GV OSTCBCur @ OS_TCB ∗ |-> Vptr ct ** AHprio GetHPrio t ** Atrue.
Lemma nth_val´2nth_val´:
forall (rtbl : list val) (n : nat) x,
nth_val´ n rtbl = Vptr x -> nth_val n rtbl = Some (Vptr x).
Qed.
Lemma highest_rdy_eq:
forall p1 l1 l2 rtbl hcurt tcbls P i x i0 y ptbl s t ct vhold,
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE->
RL_Tbl_Grp_P rtbl (Vint32 i) ->
RL_RTbl_PrioTbl_P rtbl ptbl vhold->
(Int.unsigned i <= 255) ->
nth_val´ (Z.to_nat (Int.unsigned i)) OSUnMapVallist = Vint32 x ->
nth_val´ (Z.to_nat (Int.unsigned x)) rtbl = Vint32 i0 ->
nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 y ->
nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3) +ᵢ y))) ptbl = Vptr t ->
R_PrioTbl_P ptbl tcbls vhold ->
s |= AOSTCBList p1 (Vptr ct) l1 l2 rtbl hcurt tcbls ** HTCBList tcbls **P ->
s |= GV OSTCBCur @ OS_TCB ∗ |-> Vptr ct ** AHprio GetHPrio t ** Atrue.
Lemma hoare_pure_gen : forall P1 P2 (p:Prop) S Q a b c d e,
(forall s, s |= P1 -> p) ->
{|a,b,c,d,e|}|-{{P1 ** P2 ** [|p|]}} S {{Q}} ->
{|a,b,c,d,e|} |- {{P1 ** P2}} S {{Q}}.
Lemma hoare_pure_gen´ : forall P (p:Prop) S Q a b c d e,
(forall s, s |= P -> p) ->
{|a,b,c,d,e|}|-{{P ** [|p|]}} S {{Q}} ->
{|a,b,c,d,e|} |- {{P}} S {{Q}}.
Lemma sc_isched_step:
forall P v´0 t ct,
can_change_aop P ->
P ==> GV OSTCBCur @ OS_TCB ∗ |-> Vptr ct ** AHprio GetHPrio t ** Atrue //\\ HCurTCB ct ** [| ct <> t |] ** Atrue ->
⊢ <|| (ASSUME sc;;sched);; v´0 ||> ** P ⇒
<|| (spec_done None;;sched);; v´0 ||> ** P.
Lemma nsc_isched_step:
forall P v´0 t ct,
can_change_aop P ->
P ==> GV OSTCBCur @ OS_TCB ∗ |-> Vptr ct ** AHprio GetHPrio t ** Atrue //\\ HCurTCB ct ** [| ct =t |] ** Atrue ->
⊢ <|| ASSUME nsc;; v´0 ||> ** P ⇒
<|| spec_done None;;v´0 ||> ** P.
Lemma tcbjoinsig_set_sub_sub:
forall t x tcbls tcbls´ tls y tls´,
TcbMod.joinsig t x tcbls tcbls´ ->
TcbMod.set tls t y = tls´ ->
TcbMod.sub tcbls´ tls ->
TcbMod.sub tcbls tls´.
Lemma tickstep_eqdomtls:
forall tls qls tls´ qls´ tls_sub,
TcbMod.sub tls_sub tls ->
tickstep´ tls qls tls´ qls´ tls_sub->
eqdomtls tls tls´.
Lemma absimp_timetick:
forall P tls qls tls´ qls´ curtid tm s,
can_change_aop P ->
tickstep tls qls tls´ qls´ ->
absinfer ( <|| timetick_spec (|nil|);;s ||>
** HECBList qls ** HTCBList tls ** HTime tm ** HCurTCB curtid ** P)
( <|| END None;;s ||> **
HECBList qls´** HTCBList tls´ ** HTime (Int.add tm Int.one) **
HCurTCB curtid **P).
Lemma absimp_toy:
forall P tls qls curtid tm s,
can_change_aop P ->
absinfer ( <||toyint_spec (|nil|) ;; s||>
** HECBList qls ** HTCBList tls ** HTime tm ** HCurTCB curtid ** P)
( <||END None;;s ||> **
HECBList qls** HTCBList tls ** HTime tm **
HCurTCB curtid **P).
Lemma prio_neq_tid_neq:
forall p1 l1 l2 rtbl hcurt tcbls P i x i0 y ptbl s t ct vhold
next pre eptr msg dly st p_ct tcbx tcby tcbbitx tcbbity,
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE->
RL_Tbl_Grp_P rtbl (Vint32 i) ->
RL_RTbl_PrioTbl_P rtbl ptbl vhold->
(Int.unsigned i <= 255) ->
nth_val´ (Z.to_nat (Int.unsigned i)) OSUnMapVallist = Vint32 x ->
nth_val´ (Z.to_nat (Int.unsigned x)) rtbl = Vint32 i0 ->
nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 y ->
nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3) +ᵢ y))) ptbl = Vptr t ->
R_PrioTbl_P ptbl tcbls vhold ->
Int.eq ((x<<$ 3)+ᵢy) p_ct = false ->
s |= AOSTCBList p1 (Vptr ct) l1
((next
:: pre
:: eptr
:: msg
:: Vint32 dly
:: Vint32 st
:: Vint32 p_ct
:: Vint32 tcbx
:: Vint32 tcby
:: Vint32 tcbbitx :: Vint32 tcbbity :: nil)::l2) rtbl hcurt tcbls ** HTCBList tcbls ** P ->
ct <> t.
Lemma prio_eq_tid_eq:
forall p1 l1 l2 rtbl hcurt tcbls P i x i0 y ptbl s t ct vhold
next pre eptr msg dly st p_ct tcbx tcby tcbbitx tcbbity,
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE->
RL_Tbl_Grp_P rtbl (Vint32 i) ->
RL_RTbl_PrioTbl_P rtbl ptbl vhold->
(Int.unsigned i <= 255) ->
nth_val´ (Z.to_nat (Int.unsigned i)) OSUnMapVallist = Vint32 x ->
nth_val´ (Z.to_nat (Int.unsigned x)) rtbl = Vint32 i0 ->
nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 y ->
nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3) +ᵢ y))) ptbl = Vptr t ->
R_PrioTbl_P ptbl tcbls vhold ->
Int.eq ((x<<$ 3)+ᵢy) p_ct = true ->
s |= AOSTCBList p1 (Vptr ct) l1
((next
:: pre
:: eptr
:: msg
:: Vint32 dly
:: Vint32 st
:: Vint32 p_ct
:: Vint32 tcbx
:: Vint32 tcby
:: Vint32 tcbbitx :: Vint32 tcbbity :: nil)::l2) rtbl hcurt tcbls ** HTCBList tcbls ** P ->
ct = t.
Lemma backward_1 :
forall P P´ Q S Spec I r ri s,
P ==> P´ ->
{|Spec , GetHPrio, I, r, ri|}|- {{P´**Q}}s {{S}} ->
{|Spec , GetHPrio, I, r, ri|}|- {{P**Q}}s {{S}}.
Lemma gvar_off_zero:
forall s P l x t,
s |= G&x @ t == l ** P ->
exists b, l = (b,Int.zero).
Lemma dllseg_head_null_elim:
forall s v´8 v´11 v´13 x y z P,
s |= dllseg Vnull v´8 v´11 Vnull v´13 x y z ** P -> v´13= nil /\ v´8 = v´11.
Lemma dllseg_head_isptr´ :
forall l v1 v2 v3 v4 t n p P s, s |= dllseg v1 v2 v3 (Vptr v4) l t n p ** P -> isptr v1.
Lemma xx:
forall a b c a´ b´ c´ l l´,(logic_isr a
:: logic_is b
:: logic_val c::l) = ( logic_isr a´
:: logic_is b´
:: logic_val c´ :: l´)-> c=c´.
Lemma xxx:forall P s v´9 v´10,getisr (gettaskst s) = isrupd v´9 0%nat false -> getis (gettaskst s) = 0%nat :: v´10 -> getie (gettaskst s) = false -> ( forall j : nat,
(0 <= j < gettopis (OSTickISR :: v´10))%nat ->
isrupd v´9 OSTickISR true j = false) -> s|=P ->s|= (isr_inv //\\ Aie false) ** P.
Lemma xxxx: forall s P v´10, getis (gettaskst s) = 0%nat :: v´10->
s |= P ->
s |= [|hd_error (0%nat :: v´10) = Some 0%nat|] **
Ais (0%nat :: v´10) ** P.
Lemma xxxxx: forall s v´9 P, getisr (gettaskst s) = isrupd v´9 0%nat false -> s|=P ->s
|= ([|isrupd v´9 0%nat false 0%nat = false|] //\\
Aisr (isrupd v´9 0%nat false)) ** P.
Close Scope code_scope.
Require Import OSTimeDlyPure.
Require Import OSQPostPure.
Require Import laby.
Require Import mathlib.
Open Scope code_scope.
Definition highest_rdy prio rtbl :=
(Int.unsigned prio < 64) /\
prio_in_tbl prio rtbl /\
forall prio´, 0 <= Int.unsigned prio´ < 64-> Int.eq prio prio´ = false -> prio_in_tbl prio´ rtbl -> Int.ltu prio prio´ = true.
Lemma get_highest_rdy:
forall rgrp rtbl x i0 y,
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE->
RL_Tbl_Grp_P rtbl (Vint32 rgrp) ->
(Int.unsigned rgrp <= 255) ->
nth_val´ (Z.to_nat (Int.unsigned rgrp)) OSUnMapVallist = Vint32 x ->
nth_val´ (Z.to_nat (Int.unsigned x)) rtbl = Vint32 i0 ->
nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 y ->
highest_rdy ((x<<$ 3) +ᵢ y) rtbl.
Lemma highest_rdy_eq´:
forall prio rtbl ptbl tcbls ct l1 l2 p1 hcurt P s t vhold,
t <> vhold ->
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE->
highest_rdy prio rtbl ->
nth_val´ (Z.to_nat (Int.unsigned prio)) ptbl = Vptr t ->
R_PrioTbl_P ptbl tcbls vhold ->
s |= AOSTCBList p1 (Vptr ct) l1 l2 rtbl hcurt tcbls ** HTCBList tcbls **P ->
s |= GV OSTCBCur @ OS_TCB ∗ |-> Vptr ct ** AHprio GetHPrio t ** Atrue.
Lemma nth_val´2nth_val´:
forall (rtbl : list val) (n : nat) x,
nth_val´ n rtbl = Vptr x -> nth_val n rtbl = Some (Vptr x).
Qed.
Lemma highest_rdy_eq:
forall p1 l1 l2 rtbl hcurt tcbls P i x i0 y ptbl s t ct vhold,
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE->
RL_Tbl_Grp_P rtbl (Vint32 i) ->
RL_RTbl_PrioTbl_P rtbl ptbl vhold->
(Int.unsigned i <= 255) ->
nth_val´ (Z.to_nat (Int.unsigned i)) OSUnMapVallist = Vint32 x ->
nth_val´ (Z.to_nat (Int.unsigned x)) rtbl = Vint32 i0 ->
nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 y ->
nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3) +ᵢ y))) ptbl = Vptr t ->
R_PrioTbl_P ptbl tcbls vhold ->
s |= AOSTCBList p1 (Vptr ct) l1 l2 rtbl hcurt tcbls ** HTCBList tcbls **P ->
s |= GV OSTCBCur @ OS_TCB ∗ |-> Vptr ct ** AHprio GetHPrio t ** Atrue.
Lemma hoare_pure_gen : forall P1 P2 (p:Prop) S Q a b c d e,
(forall s, s |= P1 -> p) ->
{|a,b,c,d,e|}|-{{P1 ** P2 ** [|p|]}} S {{Q}} ->
{|a,b,c,d,e|} |- {{P1 ** P2}} S {{Q}}.
Lemma hoare_pure_gen´ : forall P (p:Prop) S Q a b c d e,
(forall s, s |= P -> p) ->
{|a,b,c,d,e|}|-{{P ** [|p|]}} S {{Q}} ->
{|a,b,c,d,e|} |- {{P}} S {{Q}}.
Lemma sc_isched_step:
forall P v´0 t ct,
can_change_aop P ->
P ==> GV OSTCBCur @ OS_TCB ∗ |-> Vptr ct ** AHprio GetHPrio t ** Atrue //\\ HCurTCB ct ** [| ct <> t |] ** Atrue ->
⊢ <|| (ASSUME sc;;sched);; v´0 ||> ** P ⇒
<|| (spec_done None;;sched);; v´0 ||> ** P.
Lemma nsc_isched_step:
forall P v´0 t ct,
can_change_aop P ->
P ==> GV OSTCBCur @ OS_TCB ∗ |-> Vptr ct ** AHprio GetHPrio t ** Atrue //\\ HCurTCB ct ** [| ct =t |] ** Atrue ->
⊢ <|| ASSUME nsc;; v´0 ||> ** P ⇒
<|| spec_done None;;v´0 ||> ** P.
Lemma tcbjoinsig_set_sub_sub:
forall t x tcbls tcbls´ tls y tls´,
TcbMod.joinsig t x tcbls tcbls´ ->
TcbMod.set tls t y = tls´ ->
TcbMod.sub tcbls´ tls ->
TcbMod.sub tcbls tls´.
Lemma tickstep_eqdomtls:
forall tls qls tls´ qls´ tls_sub,
TcbMod.sub tls_sub tls ->
tickstep´ tls qls tls´ qls´ tls_sub->
eqdomtls tls tls´.
Lemma absimp_timetick:
forall P tls qls tls´ qls´ curtid tm s,
can_change_aop P ->
tickstep tls qls tls´ qls´ ->
absinfer ( <|| timetick_spec (|nil|);;s ||>
** HECBList qls ** HTCBList tls ** HTime tm ** HCurTCB curtid ** P)
( <|| END None;;s ||> **
HECBList qls´** HTCBList tls´ ** HTime (Int.add tm Int.one) **
HCurTCB curtid **P).
Lemma absimp_toy:
forall P tls qls curtid tm s,
can_change_aop P ->
absinfer ( <||toyint_spec (|nil|) ;; s||>
** HECBList qls ** HTCBList tls ** HTime tm ** HCurTCB curtid ** P)
( <||END None;;s ||> **
HECBList qls** HTCBList tls ** HTime tm **
HCurTCB curtid **P).
Lemma prio_neq_tid_neq:
forall p1 l1 l2 rtbl hcurt tcbls P i x i0 y ptbl s t ct vhold
next pre eptr msg dly st p_ct tcbx tcby tcbbitx tcbbity,
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE->
RL_Tbl_Grp_P rtbl (Vint32 i) ->
RL_RTbl_PrioTbl_P rtbl ptbl vhold->
(Int.unsigned i <= 255) ->
nth_val´ (Z.to_nat (Int.unsigned i)) OSUnMapVallist = Vint32 x ->
nth_val´ (Z.to_nat (Int.unsigned x)) rtbl = Vint32 i0 ->
nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 y ->
nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3) +ᵢ y))) ptbl = Vptr t ->
R_PrioTbl_P ptbl tcbls vhold ->
Int.eq ((x<<$ 3)+ᵢy) p_ct = false ->
s |= AOSTCBList p1 (Vptr ct) l1
((next
:: pre
:: eptr
:: msg
:: Vint32 dly
:: Vint32 st
:: Vint32 p_ct
:: Vint32 tcbx
:: Vint32 tcby
:: Vint32 tcbbitx :: Vint32 tcbbity :: nil)::l2) rtbl hcurt tcbls ** HTCBList tcbls ** P ->
ct <> t.
Lemma prio_eq_tid_eq:
forall p1 l1 l2 rtbl hcurt tcbls P i x i0 y ptbl s t ct vhold
next pre eptr msg dly st p_ct tcbx tcby tcbbitx tcbbity,
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE->
RL_Tbl_Grp_P rtbl (Vint32 i) ->
RL_RTbl_PrioTbl_P rtbl ptbl vhold->
(Int.unsigned i <= 255) ->
nth_val´ (Z.to_nat (Int.unsigned i)) OSUnMapVallist = Vint32 x ->
nth_val´ (Z.to_nat (Int.unsigned x)) rtbl = Vint32 i0 ->
nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 y ->
nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3) +ᵢ y))) ptbl = Vptr t ->
R_PrioTbl_P ptbl tcbls vhold ->
Int.eq ((x<<$ 3)+ᵢy) p_ct = true ->
s |= AOSTCBList p1 (Vptr ct) l1
((next
:: pre
:: eptr
:: msg
:: Vint32 dly
:: Vint32 st
:: Vint32 p_ct
:: Vint32 tcbx
:: Vint32 tcby
:: Vint32 tcbbitx :: Vint32 tcbbity :: nil)::l2) rtbl hcurt tcbls ** HTCBList tcbls ** P ->
ct = t.
Lemma backward_1 :
forall P P´ Q S Spec I r ri s,
P ==> P´ ->
{|Spec , GetHPrio, I, r, ri|}|- {{P´**Q}}s {{S}} ->
{|Spec , GetHPrio, I, r, ri|}|- {{P**Q}}s {{S}}.
Lemma gvar_off_zero:
forall s P l x t,
s |= G&x @ t == l ** P ->
exists b, l = (b,Int.zero).
Lemma dllseg_head_null_elim:
forall s v´8 v´11 v´13 x y z P,
s |= dllseg Vnull v´8 v´11 Vnull v´13 x y z ** P -> v´13= nil /\ v´8 = v´11.
Lemma dllseg_head_isptr´ :
forall l v1 v2 v3 v4 t n p P s, s |= dllseg v1 v2 v3 (Vptr v4) l t n p ** P -> isptr v1.
Lemma xx:
forall a b c a´ b´ c´ l l´,(logic_isr a
:: logic_is b
:: logic_val c::l) = ( logic_isr a´
:: logic_is b´
:: logic_val c´ :: l´)-> c=c´.
Lemma xxx:forall P s v´9 v´10,getisr (gettaskst s) = isrupd v´9 0%nat false -> getis (gettaskst s) = 0%nat :: v´10 -> getie (gettaskst s) = false -> ( forall j : nat,
(0 <= j < gettopis (OSTickISR :: v´10))%nat ->
isrupd v´9 OSTickISR true j = false) -> s|=P ->s|= (isr_inv //\\ Aie false) ** P.
Lemma xxxx: forall s P v´10, getis (gettaskst s) = 0%nat :: v´10->
s |= P ->
s |= [|hd_error (0%nat :: v´10) = Some 0%nat|] **
Ais (0%nat :: v´10) ** P.
Lemma xxxxx: forall s v´9 P, getisr (gettaskst s) = isrupd v´9 0%nat false -> s|=P ->s
|= ([|isrupd v´9 0%nat false 0%nat = false|] //\\
Aisr (isrupd v´9 0%nat false)) ** P.
Close Scope code_scope.