Require Export Assertions.
Require Export KernelVCG.
Require Import KernelProof.
Require Export Concrete.
Require Import Guassign.
Require Import MiscUtils.
Require Import BoundedIteration.

Coercion Kiat: atom >-> kernel.

Record certif := {
  concrete: prog ;
  abstract: kernel ;
  certif_correctness: ∀ R s, Kwlp abstract R s → wlp concrete R s
  

}.

Hint Resolve certif_correctness: checker.

Definition extract p := normalize (concrete p).

Definition vcg (p: certif) := Kvcg (abstract p).

Theorem vcg_simple_correctness (p: certif):
  vc_eval (vcg p) → is_ok (concrete p).
Proof.
  unfold vcg.
  intros; apply wlp_isok.
  intros; eapply certif_correctness.
  eapply Kvcg_correctness.
  eauto.
Qed.

Theorem vcg_correctness (cert: certif) (p:prog) :
  prog_eq (extract cert) (normalize p) = true → vc_eval (vcg cert) → is_ok p.
Proof.
  unfold extract; intros; eapply prog_eq_isok; eauto.
  apply vcg_simple_correctness.
  auto.
Qed.

Program Definition iat (inst: atom) :=
{| concrete := inst ;
   abstract := inst ;
   certif_correctness := _
|}.

Coercion iat: atom >-> certif.

Program Definition seq (pf: certif) (pn:certif) :=
{| concrete := concrete pf -; concrete pn ;
   abstract := Kseq (abstract pf) (abstract pn) ;
   certif_correctness := _
|}.
Obligation 1.
  eauto with checker echecker.
Qed.

Bind Scope certif_scope with certif.

Notation "p1 -; p2" := (seq p1 p2)
  (at level 95, right associativity): certif_scope.

Program Definition seqlabel (pf: certif) (l: alabel) (pn:certif) :=
{| concrete := concrete pf -; concrete pn ;
   abstract := Kseq (abstract pf) (Kdeflabel l 0 (abstract pn)) ;
   certif_correctness := _
|}.
Obligation 1.
  eauto with checker echecker.
Qed.

Notation "p1 -;[ l ] p2" := (seqlabel p1 l p2)
  (at level 95, right associativity): certif_scope.

Program Definition cjoin (pl pr: certif) :=
{| concrete := join (concrete pl) (concrete pr) ;
   abstract := Kjoin (abstract pl) (abstract pr) ;
   certif_correctness := _
|}.
Obligation 1.
  intuition eauto with checker echecker.
Qed.

Program Definition stdloop (body:certif) (inv: assertion) :=
{| concrete := loop (concrete body) ;
   abstract := Kloop (abstract body) inv ;
   certif_correctness := _
|}.
Obligation 1.
  firstorder.
Qed.

Notation "'bloop' p 'invariant' a 'done'" := (stdloop p a) (at level 95): certif_scope.

Program Definition joinseq (pl pr: certif) (label: alabel) (pn:certif) :=
{| concrete := join (concrete pl) (concrete pr) -; (concrete pn) ;
   abstract :=
     let p:=(abstract pn) in
     Kjoin (Kseq (abstract pl) (Kdeflabel label 0 p)) (Kseq (abstract pr) (Kdeflabel label 1 p));
   certif_correctness := _
|}.
Obligation 1.
  intuition eauto with checker echecker.
Qed.

Program Definition joinchseq (pl pr: certif) (label: alabel) (pn:certif) (convexhull: assertion):=
{| concrete := join (concrete pl) (concrete pr) -; (concrete pn) ;
   abstract :=
     let p:=(abstract pn) in
     Kjoinch (Kseq (abstract pl) (Kdeflabel label 0 p)) (Kseq (abstract pr) (Kdeflabel label 1 p)) convexhull;
   certif_correctness := _
|}.
Obligation 1.
  intuition eauto with checker echecker.
Qed.

Program Definition cbranch2 (label: alabel) (p: bool → certif) :=
let pl := p true in
let pr := p false in
{| concrete := concrete pl ;
   abstract :=
      if prog_eq (concrete pr) (concrete pl) then
         Kbranch2 label (fun b ⇒ abstract (p b))
      else
         xrequire absurd "cbranch2: concrete branches are not equal" ;
   certif_correctness := _
|}.
Obligation 1.
  generalize H; clear H. casebool (prog_eq (concrete (p false)) (concrete (p true))).
  intuition; eapply prog_eq_wlp; eauto.
  intuition.
  firstorder.
Qed.


Program Definition cbranch (label: alabel) (p: Z → certif) :=
let main := concrete (p (labmin label)) in
{| concrete := main ;
   abstract :=
      if (Zforall ((labmin label)+1) (labmax label) (fun z ⇒ prog_eq (concrete (p z)) main)) then
         Kbranch label (fun z ⇒ abstract (p z))
      else
         xrequire absurd "cbranch: concrete branches are not equal" ;
   certif_correctness := _
|}.
Obligation 1.
  generalize H; clear H.
  casebool (Zforall ((labmin label)+1) (labmax label) (fun z ⇒ prog_eq (concrete (p z)) (concrete (p (labmin label))))).
  generalize (Zforall_spec_1 _ _ _ H); clear H.
  intros H H1. case H1; clear H1.
  intros z H1.
  case (Z_eq_dec z (labmin label)).
  intros; subst; intuition.
  intuition; lapply (H z).
  intuition; eapply prog_eq_wlp; eauto.
  intuition.
  omega.
  intuition.
Qed.


Program Definition dead (p:prog) := {|
  concrete:= p ;
  abstract:= xrequire absurd "dead code" ;
  certif_correctness:= _
|}.
Obligation 1.
  tauto.
Qed.