Module TrustedPedraZ

Require Import PedraZ.
Import ASCond.
Import Itv.
Require Import TrustedDomainInterfaces.

Module FullDom <: FullItvAbstractDomain ZNum ZCond ZItv.

  Import PedraZ.FullDom.
  Open Scope option.

  Definition t:=t.

  Definition gamma:=gamma.

  Instance gamma_ext: Proper (Logic.eq ==> pointwise_relation PVar.t Logic.eq ==> iff) gamma.
  Proof gamma_ext.

  Definition isIncl:t -> t -> bool := isIncl.
  Lemma isIncl_correct: forall a1 a2, If isIncl a1 a2 THEN forall m, gamma a1 m -> gamma a2 m.

  Definition top:=top.
  Lemma top_correct: forall m, gamma top m.
  Proof top_correct.

  Definition join: t -> t -> t := join.
  Lemma join_correct1: forall a1 a2 m, gamma a1 m -> gamma (join a1 a2) m.

  Lemma join_correct2: forall a1 a2 m, gamma a2 m -> gamma (join a1 a2) m.

  Definition widen: t -> t -> t := widen.

  Definition bottom:= bottom.
  Lemma bottom_correct:forall m, (gamma bottom m)->False.
  Proof bottom_correct.

  Definition project: t -> PVar.t -> t := project.
  Lemma project_correct: forall a x m v, gamma a m -> gamma (project a x) (Mem.assign x v m).

  Hint Resolve isIncl_correct top_correct join_correct1 join_correct2 bottom_correct project_correct: vpl.

  Definition isBottom: t -> bool := isBottom.
  Lemma isBottom_correct: forall a, If isBottom a THEN forall m, (gamma a m)->False.
  Hint Resolve isBottom_correct: vpl.

  Definition pr:= pr.

  Definition get_itv: ZTerm.t -> t -> ZItv.t := get_itv.

  Lemma get_itv_correct: forall te m a,
    gamma a m -> ZItv.sat (get_itv te a) (ZTerm.eval te m).
  Hint Resolve get_itv_correct: vpl.

  Definition assume: ZCond.t -> t -> t := assume.

  Lemma assume_correct: forall c a m, ZCond.sat c m -> gamma a m -> gamma (assume c a) m.
  Hint Resolve assume_correct: vpl.

  Definition assert: ZCond.t -> t -> bool := assert.
  Lemma assert_correct: forall c a, If assert c a THEN forall m, gamma a m -> ZCond.sat c m.
  Hint Resolve assert_correct: vpl.

  Definition assign: PVar.t -> ZTerm.t -> t -> t := assign.
  
  Lemma assign_correct: forall x te a m,
    gamma a m -> gamma (assign x te a) (Mem.assign x (ZTerm.eval te m) m).
  Hint Resolve assign_correct: vpl.

  Definition guassign: PVar.t -> ZCond.t -> t -> t := guassign.

  Lemma guassign_correct: forall x c a m v,
    (ZCond.xsat c m (Mem.assign x v m)) -> gamma a m -> gamma (guassign x c a) (Mem.assign x v m).
  Hint Resolve guassign_correct: vpl.

End FullDom.