Library Scat.KernelVCG
Require Import Assertions.
Require Import Guassign.
Require Import Atoms.
Require Import BoundedIteration.
Require Export Kernel.
Definition atbounds (bound: positive) (p: atom): Prop :=
match p with
| guassign l c ⇒ lbounds bound l ∧ cbounds bound c
| skip ⇒ True
| xrequire c _ ⇒ cbounds bound c
| ensure c ⇒ cbounds bound c
| assign x t ⇒ cbounds bound (ceq x t)
end.
Lemma atbounds_Zle p bound1:
atbounds bound1 p → ∀ bound2:positive, (Zpos bound1) ≤ (Zpos bound2) → atbounds bound2 p.
Proof.
case p; simpl; intuition eauto with echecker echecker2.
Qed.
Hint Resolve atbounds_Zle: echecker.
Definition atbound (p: atom) (bound: positive): positive :=
match p with
| guassign l c ⇒ lbound l (cbound c bound)
| skip ⇒ bound
| xrequire c _ ⇒ cbound c bound
| ensure c ⇒ cbound c bound
| assign x t ⇒ cbound (ceq x t) bound
end.
Lemma atbound_monotonic p: ∀ bound, (Zpos bound) ≤ Zpos (atbound p bound).
Proof.
case p; simpl; intros; auto with checker.
eapply Zle_trans.
2: eapply lbound_monotonic.
auto with checker.
eapply Zle_trans.
2: eapply Zle_Pmax_l.
auto with checker.
Qed.
Hint Resolve atbound_monotonic: checker.
Lemma atbound_atbounds p: ∀ bound, (atbounds (atbound p bound) p).
Proof.
induction p; simpl; intuition eauto with checker echecker echecker2.
Qed.
Hint Resolve atbound_atbounds: checker.
match p with
| guassign l c ⇒ lbounds bound l ∧ cbounds bound c
| skip ⇒ True
| xrequire c _ ⇒ cbounds bound c
| ensure c ⇒ cbounds bound c
| assign x t ⇒ cbounds bound (ceq x t)
end.
Lemma atbounds_Zle p bound1:
atbounds bound1 p → ∀ bound2:positive, (Zpos bound1) ≤ (Zpos bound2) → atbounds bound2 p.
Proof.
case p; simpl; intuition eauto with echecker echecker2.
Qed.
Hint Resolve atbounds_Zle: echecker.
Definition atbound (p: atom) (bound: positive): positive :=
match p with
| guassign l c ⇒ lbound l (cbound c bound)
| skip ⇒ bound
| xrequire c _ ⇒ cbound c bound
| ensure c ⇒ cbound c bound
| assign x t ⇒ cbound (ceq x t) bound
end.
Lemma atbound_monotonic p: ∀ bound, (Zpos bound) ≤ Zpos (atbound p bound).
Proof.
case p; simpl; intros; auto with checker.
eapply Zle_trans.
2: eapply lbound_monotonic.
auto with checker.
eapply Zle_trans.
2: eapply Zle_Pmax_l.
auto with checker.
Qed.
Hint Resolve atbound_monotonic: checker.
Lemma atbound_atbounds p: ∀ bound, (atbounds (atbound p bound) p).
Proof.
induction p; simpl; intuition eauto with checker echecker echecker2.
Qed.
Hint Resolve atbound_atbounds: checker.
Frame bound for kernel
Fixpoint Kbounds (bound: positive) (p: kernel): Prop :=
match p with
| Kle_iter _ _ body last next ⇒ Kbounds bound body ∧ Kbounds bound last ∧ Kbounds bound next
| Kgjoin min max pf ⇒ ∀ z, min ≤ z ≤ max → Kbounds bound (pf z)
| Kiat inst ⇒ atbounds bound inst
| Kseq pf pn ⇒ Kbounds bound pf ∧ Kbounds bound pn
| Kjoin pl pr ⇒ Kbounds bound pl ∧ Kbounds bound pr
| Kjoinch pl pr a ⇒ Kbounds bound pl ∧ Kbounds bound pr ∧ abounds bound a
| Kloop body a ⇒ Kbounds bound body ∧ abounds bound a
| Kclone x body ⇒ tbounds bound x ∧ Kbounds bound body
| Kdeflabel _ _ p ⇒ Kbounds bound p
| Kbranch2 _ p ⇒ Kbounds bound (p true) ∧ Kbounds bound (p false)
| Kbranch l p ⇒ ∀ z, (labmin l) ≤ z ≤ (labmax l) → Kbounds bound (p z)
end.
Opaque tbounds.
Lemma Kbounds_Zle p bound1:
Kbounds bound1 p → ∀ bound2:positive, (Zpos bound1) ≤ (Zpos bound2) → Kbounds bound2 p.
Proof.
induction p; simpl; intuition eauto with echecker.
Qed.
Hint Resolve Kbounds_Zle: echecker.
Fixpoint Kbound (p: kernel) (bound: positive): positive :=
match p with
| Kle_iter _ _ body last next ⇒ Kbound body (Kbound last (Kbound next bound))
| Kgjoin min max pf ⇒ biter min max (fun z ⇒ Kbound (pf z)) bound
| Kiat inst ⇒ atbound inst bound
| Kseq pf pn ⇒ Kbound pf (Kbound pn bound)
| Kjoin pl pr ⇒ Kbound pl (Kbound pr bound)
| Kjoinch pl pr a ⇒ Kbound pl (Kbound pr (abound a bound))
| Kloop body a ⇒ Kbound body (abound a bound)
| Kclone x body ⇒ tbound x (Kbound body bound)
| Kdeflabel _ _ p ⇒ Kbound p bound
| Kbranch2 _ p ⇒ Kbound (p true) (Kbound (p false) bound)
| Kbranch l p ⇒ biter (labmin l) (labmax l) (fun z ⇒ Kbound (p z)) bound
end.
Opaque tbound.
Lemma Kbound_monotonic p: ∀ bound, (Zpos bound) ≤ Zpos (Kbound p bound).
Proof.
induction p; simpl; intros; auto with checker;
try (eapply Zle_trans; [ idtac | eauto ]; auto with checker; fail).
eapply Zle_trans.
2: eauto.
eapply Zle_trans.
2: eauto.
eapply Zle_trans.
2: eauto.
eauto with checker.
biter_ind.
intros; omega.
intros; generalize (H n x); omega.
eapply Zle_trans.
2: eauto.
eapply Zle_trans.
2: eauto.
eauto with checker.
biter_ind.
intros; omega.
intros; generalize (H n x); omega.
Qed.
Hint Resolve Kbound_monotonic: checker.
Lemma Kbound_Kbounds p: ∀ bound, (Kbounds (Kbound p bound) p).
Proof.
induction p; simpl; do_except_on @biter ltac:(intuition eauto with checker echecker).
intros bound z; biter_ind.
intros n x H0 H1 H2.
biter_split_le H2.
intros; eapply Kbounds_Zle.
eapply H1.
omega.
auto with checker.
intros bound z; biter_ind.
intros n x H0 H1 H2.
biter_split_le H2.
intros; eapply Kbounds_Zle.
eapply H1.
omega.
auto with checker.
Qed.
Transparent tbound tbounds.
Hint Resolve Kbound_Kbounds: checker.
Definition bound p := Kbound p 1.
Theorem bound_Kbounds p: Kbounds (bound p) p.
Proof.
unfold bound; auto with checker.
Qed.
match p with
| Kle_iter _ _ body last next ⇒ Kbounds bound body ∧ Kbounds bound last ∧ Kbounds bound next
| Kgjoin min max pf ⇒ ∀ z, min ≤ z ≤ max → Kbounds bound (pf z)
| Kiat inst ⇒ atbounds bound inst
| Kseq pf pn ⇒ Kbounds bound pf ∧ Kbounds bound pn
| Kjoin pl pr ⇒ Kbounds bound pl ∧ Kbounds bound pr
| Kjoinch pl pr a ⇒ Kbounds bound pl ∧ Kbounds bound pr ∧ abounds bound a
| Kloop body a ⇒ Kbounds bound body ∧ abounds bound a
| Kclone x body ⇒ tbounds bound x ∧ Kbounds bound body
| Kdeflabel _ _ p ⇒ Kbounds bound p
| Kbranch2 _ p ⇒ Kbounds bound (p true) ∧ Kbounds bound (p false)
| Kbranch l p ⇒ ∀ z, (labmin l) ≤ z ≤ (labmax l) → Kbounds bound (p z)
end.
Opaque tbounds.
Lemma Kbounds_Zle p bound1:
Kbounds bound1 p → ∀ bound2:positive, (Zpos bound1) ≤ (Zpos bound2) → Kbounds bound2 p.
Proof.
induction p; simpl; intuition eauto with echecker.
Qed.
Hint Resolve Kbounds_Zle: echecker.
Fixpoint Kbound (p: kernel) (bound: positive): positive :=
match p with
| Kle_iter _ _ body last next ⇒ Kbound body (Kbound last (Kbound next bound))
| Kgjoin min max pf ⇒ biter min max (fun z ⇒ Kbound (pf z)) bound
| Kiat inst ⇒ atbound inst bound
| Kseq pf pn ⇒ Kbound pf (Kbound pn bound)
| Kjoin pl pr ⇒ Kbound pl (Kbound pr bound)
| Kjoinch pl pr a ⇒ Kbound pl (Kbound pr (abound a bound))
| Kloop body a ⇒ Kbound body (abound a bound)
| Kclone x body ⇒ tbound x (Kbound body bound)
| Kdeflabel _ _ p ⇒ Kbound p bound
| Kbranch2 _ p ⇒ Kbound (p true) (Kbound (p false) bound)
| Kbranch l p ⇒ biter (labmin l) (labmax l) (fun z ⇒ Kbound (p z)) bound
end.
Opaque tbound.
Lemma Kbound_monotonic p: ∀ bound, (Zpos bound) ≤ Zpos (Kbound p bound).
Proof.
induction p; simpl; intros; auto with checker;
try (eapply Zle_trans; [ idtac | eauto ]; auto with checker; fail).
eapply Zle_trans.
2: eauto.
eapply Zle_trans.
2: eauto.
eapply Zle_trans.
2: eauto.
eauto with checker.
biter_ind.
intros; omega.
intros; generalize (H n x); omega.
eapply Zle_trans.
2: eauto.
eapply Zle_trans.
2: eauto.
eauto with checker.
biter_ind.
intros; omega.
intros; generalize (H n x); omega.
Qed.
Hint Resolve Kbound_monotonic: checker.
Lemma Kbound_Kbounds p: ∀ bound, (Kbounds (Kbound p bound) p).
Proof.
induction p; simpl; do_except_on @biter ltac:(intuition eauto with checker echecker).
intros bound z; biter_ind.
intros n x H0 H1 H2.
biter_split_le H2.
intros; eapply Kbounds_Zle.
eapply H1.
omega.
auto with checker.
intros bound z; biter_ind.
intros n x H0 H1 H2.
biter_split_le H2.
intros; eapply Kbounds_Zle.
eapply H1.
omega.
auto with checker.
Qed.
Transparent tbound tbounds.
Hint Resolve Kbound_Kbounds: checker.
Definition bound p := Kbound p 1.
Theorem bound_Kbounds p: Kbounds (bound p) p.
Proof.
unfold bound; auto with checker.
Qed.
Operators used by our VCG
Module Type VCGparameters.
Parameter tauto: cond.
Parameter absurd: cond.
Parameter hard_and: cond → cond → cond.
Parameter ceq: var → term → cond.
Parameter trename: term → positive → positive → term.
Parameter rename: cond → positive → positive → cond.
Parameter tauto: cond.
Parameter absurd: cond.
Parameter hard_and: cond → cond → cond.
Parameter ceq: var → term → cond.
Parameter trename: term → positive → positive → term.
Parameter rename: cond → positive → positive → cond.
A Writer Monad for collecting result of checker. Typically :
- a error monad (when a inclusion test fails).
- a state monad with state = a list of undischarged VC.
Parameter monad: Type → Type.
Parameter ret: ∀ {A}, A → monad A.
Parameter bind: ∀ {A B}, (monad A) → (A → monad B) → monad B.
Parameter ret: ∀ {A}, A → monad A.
Parameter bind: ∀ {A B}, (monad A) → (A → monad B) → monad B.
check_entails mesg pre post k
means that computation k is guarded by inclusion test pre ⇒ post
and mesg gives info on the origin of the inclusion test.
soft_or c1 c2 typically calls an external untrusted tool to compute c = c1 ∨ c2
but "check" c1 ⇒ c and c2 ⇒ c.
May generate some VC and returns c.
Some notations in order to have a more readable code
Bind Scope VCG_scope with monad.
Notation "'do' x <- p1 ';' p2" := (bind p1 (fun x ⇒ p2))
(at level 95, p1 at level 93, right associativity): VCG_scope.
Notation "{ mesg # n # c1 |= c2 } k" := (check_entails mesg n c1 c2 k)
(at level 95, right associativity): VCG_scope.
End VCGparameters.
Module GenericVCG(Arg: VCGparameters).
Export Arg.
Record postfinder_result (A:Type): Type := {
pbnd: positive ;
post: A
}.
Implicit Arguments pbnd [A].
Implicit Arguments post [A].
Implicit Arguments Build_postfinder_result [A].
Section VCGCode.
Open Scope VCG_scope.
Let xret := fun {A} ⇒ ret (A:=postfinder_result A).
Coercion xret: postfinder_result >-> monad.
Definition atpostfinder (p: atom) (pre: cond) (cour: positive): monad (postfinder_result cond) :=
match p with
| guassign l c ⇒
let r:=lfresh l cour in
{| pbnd:=rbound r ; post:=hard_and (rsubst pre r) (orsubst c r) |}
| skip ⇒
{| pbnd:=cour ; post:=pre |}
| xrequire c m ⇒
{ Req c m # cour # pre |= c }
{| pbnd:=cour ; post:=pre |}
| ensure c ⇒
{| pbnd:=cour ; post:=hard_and pre c |}
| assign x t ⇒
{| pbnd:=(cour+1)%positive ; post:=hard_and (ceq x (trename t (vid x) cour)) (rename pre (vid x) cour) |}
end.
Fixpoint postfinder_le_iter (n:nat) (ol:option alabel) (body next: cond → positive → aenvironment → monad (postfinder_result cond))
(pre: cond) (cour: positive) (aenv: aenvironment) (zof_n: Z): monad (postfinder_result (cond × (postfinder_result cond))) :=
match n with
| O ⇒ do res <- next pre cour (oadd ol pre 0 aenv) ;
{| pbnd := cour ; post := (pre, res) |}
| S n ⇒ do aux <- postfinder_le_iter n ol body next pre cour aenv (zof_n-1) ;
let post1 := fst (post aux) in
let res1 := snd (post aux) in
do res2 <- body post1 (pbnd aux) (oadd ol post1 zof_n aenv) ;
do res3 <- next (post res2) (pbnd res2) (oadd ol (post res2) zof_n aenv) ;
{| pbnd := pbnd res2 ;
post := (post res2,
{| pbnd := Pmax (pbnd res1) (pbnd res3) ; post := bin OR (post res1) (post res3) |})
|}
end.
Definition internal_error := xrequire absurd "internal error".
Fixpoint postfinder (p: kernel) (pre: cond) (cour: positive) (aenv: aenvironment): monad (postfinder_result cond) :=
match p with
| Kle_iter n ol body last next ⇒
let zof_n:=(Z_of_nat n) in
let succ_zof_n:=zof_n+1 in
do aux <- postfinder_le_iter n ol (postfinder body) (postfinder next) pre cour aenv zof_n ;
let post1 := fst (post aux) in
let res1 := snd (post aux) in
do res2 <- postfinder body post1 (pbnd aux) (oadd ol post1 succ_zof_n aenv) ;
do res3 <- postfinder last (post res2) (pbnd res2) (oadd ol (post res2) succ_zof_n aenv) ;
{| pbnd := Pmax (pbnd res1) (pbnd res3) ; post := bin OR (post res1) (post res3)|}
| Kgjoin min max pf ⇒
biter min max (fun z K ⇒ do aux1 <- K ;
do aux2 <- postfinder (pf z) pre cour aenv ;
{| pbnd := Pmax (pbnd aux1) (pbnd aux2) ; post := bin OR (post aux1) (post aux2) |})
{| pbnd := cour ; post := absurd |}
| Kiat inst ⇒ atpostfinder inst pre cour
| Kseq pf pn ⇒
do resf <- postfinder pf pre cour aenv ;
postfinder pn (post resf) (pbnd resf) aenv
| Kjoin pl pr ⇒
do resl <- postfinder pl pre cour aenv ;
do resr <- postfinder pr pre cour aenv ;
let cour := Pmax (pbnd resl) (pbnd resr) in
do res <- soft_or cour (post resl) (post resr) ;
{| pbnd := cour ; post := res |}
| Kjoinch pl pr a ⇒
let convexhull := aeval a aenv in
do resl <- postfinder pl pre cour aenv ;
do resr <- postfinder pr pre cour aenv ;
let cour0 := Pmax (pbnd resl) (pbnd resr) in
{ Unchecked_Union # cour0 # post resl |= convexhull }
{ Unchecked_Union # cour0 # post resr |= convexhull }
{| pbnd := cour ; post := convexhull |}
| Kloop body a ⇒
let inv := aeval a aenv in
do res <- postfinder body inv cour aenv ;
{ LoopPre # pbnd res # pre |= inv }
{ LoopPost # pbnd res # post res |= inv }
{| pbnd := cour ; post := inv |}
| Kclone x body ⇒
let old:=(mkvar (vtag x) cour) in
do res <- postfinder body (hard_and (ceq x old) (rename pre (vid x) cour)) (cour+1)%positive aenv ;
let rb := pbnd res in
{| pbnd := rb ; post := rsubst (post res) (swap x old rb) |}
| Kdeflabel l x p ⇒ postfinder p pre cour (aadd (labid l) {| acond := pre ; abranch := x |} aenv)
| Kbranch2 l p ⇒ postfinder (p (Zeq_bool (abranch (afind (labid l) aenv)) (labmin l))) pre cour aenv
| Kbranch l p ⇒ safe_branch l aenv (fun z ⇒ postfinder (p z) pre cour aenv)
(atpostfinder internal_error pre cour)
end.
Let void := (Arg.ret tt).
Definition Kvcgen (p: kernel): monad unit :=
do res <- postfinder p tauto (bound p) aempty ;
void.
End VCGCode.
End GenericVCG.
Open Scope list_scope.
Instantiation of VCG parameters
Module ConcreteCondWrapper.
Definition tauto := tauto.
Definition absurd := absurd.
Definition hard_and := bin AND.
Definition trename := trename.
Definition rename := rename.
Definition ceq := ceq.
Record VC : Type := {
mesg: trace ;
tbnd: positive ;
hyp: cond ;
goal: cond
}.
Record result {A}: Type := {
vcl: list VC;
value: A
}.
Definition monad := fun A ⇒ list VC → result (A:=A).
Definition ret {A} (value: A) : monad A
:= fun l ⇒ {| vcl := l ; value := value |}.
Definition bind {A B} (k1: monad A) (k2: A → monad B) : monad B
:= fun l ⇒ let res := k1 l in
k2 (value res) (vcl res).
Definition check_entails {A} (mesg:trace) (bound: positive) (p q: cond) (k:monad A): monad A
:= fun l ⇒ k ({| mesg:=mesg ;
tbnd:=bound ;
hyp:=p ;
goal:=q |}::l).
Definition soft_or := fun (bound: positive) (c1 c2:cond) ⇒
(ret (bin OR c1 c2)).
End ConcreteCondWrapper.
Module KVCG := GenericVCG(ConcreteCondWrapper).
Export KVCG.
Fixpoint vc_eval (l: list VC): Prop :=
match l with
| vc::l ⇒ (∀ s, eval (hyp vc) s → eval (goal vc) s) ∧ (vc_eval l)
| nil ⇒ True
end.
Definition tauto := tauto.
Definition absurd := absurd.
Definition hard_and := bin AND.
Definition trename := trename.
Definition rename := rename.
Definition ceq := ceq.
Record VC : Type := {
mesg: trace ;
tbnd: positive ;
hyp: cond ;
goal: cond
}.
Record result {A}: Type := {
vcl: list VC;
value: A
}.
Definition monad := fun A ⇒ list VC → result (A:=A).
Definition ret {A} (value: A) : monad A
:= fun l ⇒ {| vcl := l ; value := value |}.
Definition bind {A B} (k1: monad A) (k2: A → monad B) : monad B
:= fun l ⇒ let res := k1 l in
k2 (value res) (vcl res).
Definition check_entails {A} (mesg:trace) (bound: positive) (p q: cond) (k:monad A): monad A
:= fun l ⇒ k ({| mesg:=mesg ;
tbnd:=bound ;
hyp:=p ;
goal:=q |}::l).
Definition soft_or := fun (bound: positive) (c1 c2:cond) ⇒
(ret (bin OR c1 c2)).
End ConcreteCondWrapper.
Module KVCG := GenericVCG(ConcreteCondWrapper).
Export KVCG.
Fixpoint vc_eval (l: list VC): Prop :=
match l with
| vc::l ⇒ (∀ s, eval (hyp vc) s → eval (goal vc) s) ∧ (vc_eval l)
| nil ⇒ True
end.