Library derivedrules
Require Import include.
Require Import memdata.
Require Import memory.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import simulation.
Require Import inferules.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Require Import baseTac.
Lemma Aop_Aop´_eq :
forall p aop,
p //\\ <| aop |> <==> p ** <|| aop ||>.
Lemma Aop_Aop´_eq´ :
forall p aop,
p //\\ <| aop |> <==> <|| aop ||> ** p.
Theorem ret_rule´ :
forall (Spec : funspec) (I : Inv) (r : option val -> asrt)
(p : asrt) sc,
p ==> r None ->
{|Spec , sc , I, r, Afalse|}|- {{p}}sret {{Afalse}}.
Theorem iret_rule´ :
forall (Spec : funspec) (I : Inv) (ri : asrt)
(p : asrt) sc,
p ==> ri ->
{|Spec , sc , I, arfalse, ri|}|- {{p}}sprim exint {{Afalse}}.
Theorem rete_rule´ :
forall (Spec : funspec) (I : Inv) (r : option val -> asrt)
(p : asrt) (v : val) (e : expr)
(t: type) sc,
p ==> Rv e @ t == v ->
p ==> r (Some v) ->
{|Spec , sc, I, r, Afalse|}|- {{p}}srete e {{Afalse}}.
Theorem call_rule´ :
forall (f : fid)
Spec
(I : Inv) (r : retasrt) (ri : asrt)
(pre : fpre)
(post : fpost) (p P: asrt) (el : exprlist)
(vl : vallist) (tp : type)
(tl : typelist) (logicl:list logicvar) sc,
Spec f = Some (pre, post, (tp, tl)) ->
P ==> Rvl el @ tl == vl ->
P ==> PRE [pre, vl,logicl] ** p ->
GoodFrm p ->
tl_vl_match tl vl =true ->
{|Spec , sc , I, r, ri|}|-
{{ P}}
scall f el
{{ EX v, POST [post, vl, v,logicl] ** p}}.
Theorem calle_rule´ :
forall (f : fid) (e : expr) (l : addrval)
Spec (I : Inv)
(r : retasrt) (ri : asrt)
(pre : fpre) (post : fpost)
(p P : asrt) (el : exprlist) (v´ : val)
(vl : vallist) (tp : type)
(tl : typelist) logicl sc,
Spec f = Some (pre, post, (tp, tl)) ->
P ==> PRE [pre, vl,logicl] ** PV l @ tp |-> v´ ** p ->
GoodFrm p ->
retpost post ->
P ==> Rvl el @ tl == vl ->
PV l @ tp |-> v´ ** p ==> Lv e @ tp == l ->
tl_vl_match tl vl =true ->
{|Spec , sc , I , r, ri|}|-
{{ P }}
scalle e f el
{{EX v, POST [post, vl, Some v,logicl] ** PV l @ tp |-> v ** p}}.
Theorem calle_rule_lvar´ :
forall (f : fid) (x : var)
Spec (I : Inv)
(r : retasrt) (ri : asrt)
(pre : fpre) (post : fpost)
(p P : asrt) (el : exprlist) (v´ : val)
(vl : vallist) (tp : type)
(tl : typelist) logicl sc,
Spec f = Some (pre, post, (tp, tl)) ->
P ==> Rvl el @ tl == vl ->
P ==> PRE [pre, vl, logicl] ** LV x @ tp |-> v´ ** p ->
GoodFrm p ->
retpost post ->
tl_vl_match tl vl =true ->
{|Spec , sc, I, r, ri|}|-
{{ P }}
scalle (evar x) f el
{{EX v, POST [post, vl, Some v,logicl] ** LV x @ tp |-> v ** p}}.
Theorem forward_rule1 :
forall Spec I r ri p q q´ s sc,
q ==> q´ ->
{|Spec , sc, I, r, ri|}|- {{p}}s {{q}} ->
{|Spec , sc, I, r, ri|}|- {{p}}s {{q´}}.
Theorem forward_rule2 :
forall Spec I r ri p q q´ s sc,
{|Spec , sc, I, r, ri|}|- {{p}}s {{q}} ->
q ==> q´ ->
{|Spec , sc, I, r, ri|}|- {{p}}s {{q´}}.
Theorem backward_rule1 :
forall Spec I r ri p p´ q s sc,
p´ ==> p ->
{|Spec, sc, I, r, ri|}|- {{p}}s {{q}} ->
{|Spec, sc, I, r, ri|}|- {{p´}}s {{q}}.
Theorem backward_rule2 :
forall Spec I r ri p p´ q s sc,
{|Spec , sc, I, r, ri|}|- {{p}}s {{q}} ->
p´ ==> p ->
{|Spec , sc, I, r, ri|}|- {{p´}}s {{q}}.
Theorem forward_rule3 :
forall Spec I r ri p q q´ R s sc,
q ==> q´ ->
{|Spec , sc, I, r, ri|}|- {{p }}s {{q //\\ R}} ->
{|Spec , sc, I, r, ri|}|- {{p }}s {{q´ //\\ R}}.
Theorem forward_rule4 :
forall Spec I r ri p q q´ R s sc,
{|Spec , sc, I, r, ri|}|- {{p}}s {{q //\\ R}} ->
q ==> q´ ->
{|Spec , sc, I, r, ri|}|- {{p}}s {{q´//\\R}}.
Theorem backward_rule3 :
forall Spec I r ri p p´ q R s sc,
p´ ==> p ->
{|Spec, sc, I, r, ri|}|- {{p //\\ R}}s {{q}} ->
{|Spec, sc, I, r, ri|}|- {{p´//\\R}}s {{q}}.
Theorem backward_rule4 :
forall Spec I r ri p p´ q R s sc,
{|Spec, sc, I, r, ri|}|- {{p //\\ R}}s {{q}} ->
p´ ==> p ->
{|Spec, sc, I, r, ri|}|- {{p´ //\\ R}}s {{q}}.
Theorem frame_rule´ :
forall (Spec : funspec) (I : Inv)
(p q frm : asrt) (s : stmts)
(aop aop´ : absop) r ri sc,
GoodI I sc->
GoodStmt´ s ->
GoodFrm frm ->
{|Spec, sc, I, arfalse, Afalse|}|- {{ <|| aop ||> ** p }}s {{ <|| aop´ ||> ** q }} ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** frm ** p }}s
{{ <|| aop´ ||> ** frm ** q }}.
Theorem frame_rule_all´ :
forall (Spec : funspec) (I : Inv)
(r : retasrt) (ri p q p´ frm : asrt)
(s : stmts) (aop : absop) sc,
GoodI I sc->
GoodStmt´ s ->
GoodFrm frm ->
p ==> <|| aop ||> ** p´ ->
{|Spec, sc, I, r, ri|}|- {{p}}s {{q}} ->
{|Spec, sc, I, fun v : option val => r v ** frm,
ri ** frm|}|- {{ frm ** p }}s {{ frm ** q }}.
Theorem assign_rule´ :
forall (Spec : funspec) (I : Inv)
(r : retasrt) (ri : asrt)
(p : asrt) (e1 e2 : expr) (l : addrval)
(v1 v2 : val) (tp1 tp2 : type)
(aop : absop) sc,
assign_type_match tp1 tp2 ->
PV l @ tp1 |-> v1 ** p ==> Lv e1 @ tp1 == l //\\ Rv e2 @ tp2 == v2 ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** PV l @ tp1 |-> v1 ** p }}
sassign e1 e2 {{ <|| aop ||> ** PV l @ tp1 |-> v2 ** p }}.
Theorem encrit1_rule´ :
forall Spec I r ri i isr is cs frm aop p sc,
p ==> Aisr isr ** Aie true ** Ais is ** Acs cs ** ATopis i ** [| i <= INUM |] ** frm ->
GoodI I sc->
GoodFrm frm ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** p }} sprim encrit
{{ <|| aop ||> ** Aisr isr ** Aie false ** Ais is ** Acs (true::cs) ** invlth_isr I 0 i ** frm }}.
Theorem encrit2_rule´ :
forall Spec I r ri isr is cs frm aop p sc,
p ==> Aisr isr ** Aie false ** Ais is ** Acs cs ** frm ->
GoodI I sc->
GoodFrm frm ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** p }} sprim encrit
{{ <|| aop ||> ** Aisr isr ** Aie false ** Ais is ** Acs (false::cs) ** frm }}.
Theorem excrit1_rule´ :
forall Spec I r ri i isr is cs frm aop p sc,
p ==> Aisr isr ** Aie false ** Ais is ** Acs (true::cs) ** ATopis i ** invlth_isr I 0 i ** frm ->
GoodI I sc->
GoodFrm frm ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** p }} sprim excrit
{{ <|| aop ||> ** Aisr isr ** Aie true ** Ais is ** Acs cs ** frm }}.
Theorem excrit2_rule´ :
forall Spec I r ri isr is cs frm aop p sc,
p ==> Aisr isr ** Aie false ** Ais is ** Acs (false::cs) ** frm ->
GoodI I sc->
GoodFrm frm ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** p }} sprim excrit
{{ <|| aop ||> ** Aisr isr ** Aie false ** Ais is ** Acs cs ** frm }}.
Theorem cli1_rule´ :
forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri : asrt) (isr : isr)
(is : is) (i : hid) (aop : absop) frm p sc,
p ==> Aisr isr ** Aie true ** Ais is ** Acs nil ** ATopis i ** [|i <= INUM|] ** frm ->
GoodI I sc->
GoodFrm frm ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** p }}sprim cli
{{ <|| aop ||> ** Aisr isr ** Aie false ** Ais is ** Acs nil ** invlth_isr I 0 i ** frm }}.
Theorem cli2_rule´ :
forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri : asrt) (isr : isr)
(is : is) (aop : absop) p frm sc,
p ==> Aisr isr ** Aie false ** Ais is ** Acs nil ** frm ->
GoodI I sc->
GoodFrm frm ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** p }}
sprim cli {{ <|| aop ||> ** Aisr isr ** Aie false ** Ais is ** Acs nil ** frm }}.
Theorem sti1_rule´ :
forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri : asrt) (isr : isr)
(i : hid) (is : is) (aop : absop) p frm sc,
p ==> Aisr isr ** Aie false ** Ais is ** Acs nil ** ATopis i ** invlth_isr I 0 i ** frm ->
GoodI I sc->
GoodFrm frm ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** p }}sprim sti
{{ <|| aop ||> ** Aisr isr ** Aie true ** Ais is ** Acs nil ** frm }}.
Theorem sti2_rule´ :
forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri : asrt) (isr : isr)
(is : is) (aop : absop) frm p sc,
p ==> Aisr isr ** Aie true ** Ais is ** Acs nil ** frm ->
GoodI I sc->
GoodFrm frm ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** p}}
sprim sti {{ <|| aop ||> ** Aisr isr ** Aie true ** Ais is ** Acs nil ** frm }}.
Lemma aop_intro:
forall P s aop, s|= <||aop||> ** P -> s|=<|aop|>.
Theorem switch_rule´ :
forall (Spec : funspec) (I : Inv)
(r : retasrt) (ri : asrt)
(x : var) (aop : absop) is cs P sc,
P ==> SWINV I ** Ais is ** Acs cs ** <||sched;; aop ||> ->
P ==> SWPRE sc x->
{|Spec, sc, I, r, ri|}|- {{ P }}
sprim (switch x) {{ <|| aop ||> ** SWINV I ** Ais is ** Acs cs}}.
Theorem eoi_ieon_rule´ :
forall (Spec : funspec) (I : Inv)
(r : retasrt) (ri : asrt)
(isr : isr) (is : list nat) (id : int32)
(cs : cs) (i : nat) (aop : absop) p frm sc,
(0 <= Int.unsigned id < Z.of_nat INUM)%Z ->
i = Z.to_nat (Int.unsigned id) ->
p ==> Aisr isr ** Aie true ** Ais (i::is) ** Acs cs ** getinv (I i) ** frm ->
GoodI I sc->
GoodFrm frm ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** p }}sprim (eoi id)
{{ <|| aop ||> ** Aisr (isrupd isr i false) ** Aie true ** Ais (i::is) ** Acs cs ** frm }}.
Theorem eoi_ieoff_rule´ :
forall (Spec : funspec) (I : Inv)
(r : retasrt) (ri : asrt)
(isr : isr) (is : list nat)
(id : int32) (i : nat) (cs : cs)
(aop : absop) p frm sc,
(0 <= Int.unsigned id < Z.of_nat INUM)%Z ->
i = Z.to_nat (Int.unsigned id) ->
p ==> Aisr isr ** Aie false ** Ais (i::is) ** Acs cs ** frm ->
GoodI I sc->
GoodFrm frm ->
{|Spec, sc, I, r, ri|}|- {{ <|| aop ||> ** p }}
sprim (eoi id)
{{ <|| aop ||> ** Aisr (isrupd isr i false) ** Aie false ** Ais (i::is) ** Acs cs ** frm }}.
Definition scheck e := sifthen e (sskip None).
Theorem ex_intro_rule´ :
forall Spec I r ri {tp:Type} (p q: tp -> asrt) s sc,
(forall v´ : tp, {| Spec, sc, I, r, ri|} |- {{ p v´ }} s {{ q v´ }}) ->
{| Spec, sc, I, r, ri |} |- {{ EX v, p v }} s {{ EX v, q v }}.
Theorem pure_intro_rule´: forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri : asrt) (p q : asrt)
(pu : Prop) (s : stmts) sc,
(pu -> {|Spec, sc, I, r, ri|}|- {{ [| pu |] ** p}}s {{q}}) ->
{|Spec, sc, I, r, ri|}|- {{ [|pu|]**p}}s {{q}}.
Theorem pure_split_rule´: forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri : asrt) (p q : asrt)
(pu : Prop) (s : stmts) sc,
(pu -> {|Spec, sc, I, r, ri|}|- {{ p}}s {{q}}) ->
{|Spec, sc, I, r, ri|}|- {{ [|pu|]**p}}s {{q}}.
Theorem prop_intro_rule :
forall Spec I r ri p s q (P:Prop) sc,
(P -> {| Spec, sc, I, r, ri |} |- {{ p }} s {{ q }}) ->
(forall s, s |= p -> P) ->
{| Spec, sc, I, r, ri |} |- {{ p }} s {{ q }}.
Lemma abscsq_rule´ :
forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri : asrt) (p´ p q : asrt) (s : stmts) sc,
absinfer p´ p ->
{|Spec, sc, I, r, ri|}|- {{p}}s {{q}} ->
{|Spec, sc, I, r, ri|}|- {{p´}}s {{q}}.
Lemma abscsq_rule´´ :
forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri : asrt) (q´ p q : asrt) (s : stmts) sc,
absinfer q q´ ->
{|Spec, sc, I, r, ri|}|- {{p}}s {{q}} ->
{|Spec, sc, I, r, ri|}|- {{p}}s {{q´}}.
Lemma disj_rule´ :
forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri p1 p2 : asrt) (s : stmts) (q1 q2 : asrt) sc,
{|Spec, sc, I, r, ri|}|- {{p1}}s {{q1 }} ->
{|Spec, sc, I, r, ri|}|- {{p2}}s {{q2 }} ->
{|Spec, sc, I, r, ri|}|- {{p1 \\// p2}}s {{q1 \\// q2}}.
Lemma checkis_rule´ :
forall Spec I r ri isr ie is cs frm aop p v x sc,
p ==> Aisr isr ** Aie ie ** Ais is ** Acs cs ** LV x @ Tint32 |-> v ** frm ->
GoodI I sc->
GoodFrm frm ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** p }} (sprim (checkis x))
{{ <|| aop ||> ** Aisr isr ** Aie ie ** Ais is ** Acs cs **
LV x @ Tint32 |-> is_length is ** frm }}.
Require Import tst_prop.
Definition invlth_noisr´ I high:=
match high with
| 0 => Aemp
| _ => starinv_noisr I 0 (high -1)
end.
Lemma isr_false_inv_eq:
forall (i : nat) (ge le : env) (M : mem) (ir : isr)
(ie0 : ie) (is0 : is) (cs0 : cs) (O0 : osabst)
(ab : absop) (I : Inv),
i <= INUM ->
(forall j : nat, 0 <= j < i -> ir j = false) ->
(ge, le, M, ir, (ie0, is0, cs0), O0, ab) |= invlth_isr I 0 i ->
(ge, le, M, ir, (ie0, is0, cs0), O0, ab)
|= invlth_noisr´ I i **
([|ir i = true|] \\//
[|ir i = false|] ** getinv (I i)).
Lemma starinv_prop1´: forall j i I,
(starinv_noisr I i (S j)) ==>
(starinv_noisr I i j) ** (starinv_noisr I (S (i+j)) 0)%nat.
Lemma starinv_prop1_rev: forall j i I,
(starinv_isr I i j) ** (starinv_isr I (S (i+j)) 0)%nat ==>
(starinv_isr I i (S j)).
Lemma invnoisr_imply_isr´ :
forall j ge le M ir aux O ab I , ( forall i : hid, i <= j -> ir i = false) ->
(ge, le, M, ir, aux, O, ab) |= starinv_noisr I 0 j ->
(ge, le, M, ir, aux, O, ab) |= starinv_isr I 0 j.
Lemma isr_false_inv_eq´:
forall (i : nat) (ge le : env) (M : mem) (ir : isr)
(ie0 : ie) (is0 : is) (cs0 : cs) (O0 : osabst)
(ab : absop) (I : Inv),
i <= INUM ->
(forall j : nat, 0 <= j < i -> ir j = false) ->
(ge, le, M, ir, (ie0, is0, cs0), O0, ab)
|= invlth_noisr´ I i **
([|ir i = true|] \\//
[|ir i = false|] ** getinv (I i)) ->
(ge, le, M, ir, (ie0, is0, cs0), O0, ab) |= invlth_isr I 0 i.
Lemma xxx:forall P, Aemp ** P ==> P.
Qed.
Theorem encrit_rule_pre:
forall Spec I r ri i isr is cs aop sc,
i <= INUM ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** Aisr isr ** Aie true ** Ais is ** Acs cs ** isr_inv ** ATopis i }} sprim encrit
{{ <|| aop ||> ** Aisr isr ** Aie false ** Ais is ** Acs (true::cs) ** isr_inv ** invlth_noisr´ I i ** ( ([|isr i = true|] ) \\// ([|isr i = false|]) ** getinv (I i))}}.
Lemma xx:
forall e e0 m isr is cs o aop P ,
(forall j : nat, 0 <= j < gettopis is -> isr j = false) ->
(e, e0, m, isr, (false, is, true :: cs), o, aop) |= P ->
(e, e0, m, isr, (false, is, true :: cs), o, aop) |= (Aisr isr //\\
ATopis (gettopis is) //\\
[|forall j : nat, 0 <= j < gettopis is -> isr j = false|]) ** P.
Qed.
Theorem excrit_rule_pre:
forall Spec I r ri i isr is cs aop sc,
i <= INUM ->
{|Spec, sc, I, r, ri|}|-
{{ <|| aop ||> ** Aisr isr ** Aie false ** Ais is ** Acs (true::cs) ** isr_inv ** ATopis i ** invlth_noisr´ I i ** ( ([|isr i = true|] ) \\// ([|isr i = false|]) ** getinv (I i)) }} sprim excrit
{{ <|| aop ||> ** Aisr isr ** Aie true ** Ais is ** Acs cs ** isr_inv}}.