Module CExprPedraZ

This module is closest to the abstract domain interface. This is where the discovery of linear expressions in arbitrary expressions takes place.

Require Import String.
Require Import List.
Require CoqAddOn.
Require Import NumC.
Require Import ProgVar.
Require ASCond.
Require Import Itv.

Require Import ZArith_base.
Local Open Scope Z_scope.

Module Cmp.
  Inductive t: Set
    := Eq | Le | Lt | Neq | Ge | Gt.

  Local Open Scope string_scope.

  Definition pr: t -> string
    := fun c =>
         match c with
           | Eq => "=" | Neq => "/="
           | Le => "<=" | Lt => "<"
           | Ge => ">=" | Gt => ">"
         end.

  Local Close Scope string_scope.

  Definition denote: t -> ZNum.t -> ZNum.t -> Prop
    := fun c z z' =>
         match c with
           | Eq => z = z'
           | Neq => z <> z'
           | Le => ZNum.Le z z'
           | Lt => ZNum.Lt z z'
           | Ge => ZNum.Le z' z
           | Gt => ZNum.Lt z' z
         end.

  Definition dec (c: t) (z z': ZNum.t): {denote c z z'} + {~ denote c z z'}.
    refine (
        match c return {denote c z z'} + {~ denote c z z'}
        with
          | Eq => ZNum.eqDec z z'
          | Neq =>
            match ZNum.eqDec z z' with
              | left _ => right _
              | right _ => left _
            end
          | Le =>
            match ZNum.ltLeDec z' z with
              | left _ => right _
              | right _ => left _
            end
          | Lt =>
            match ZNum.ltLeDec z z' with
              | left _ => left _
              | right _ => right _
            end
          | Ge =>
            match ZNum.ltLeDec z z' with
              | left _ => right _
              | right _ => left _
            end
          | Gt =>
            match ZNum.ltLeDec z' z with
              | left _ => left _
              | right _ => right _
            end
        end);
    simpl;
    match goal with
      | |- ~ ZNum.Le _ _ => apply ZNum.LtNotLe
      | |- ~ ZNum.Lt _ _ => apply ZNum.LeNotLt
      | |- ~ _ <> _ => destruct 1
      | _ => idtac
    end;
    assumption.
  Defined.

End Cmp.

Module Expr.

  Inductive binopT: Type :=
  | Oadd | Osub | Omul | Odiv | Omod
  | Oand | Oor | Oxor | Oshl | Oshr
  | Ocmp: Cmp.t -> binopT.

  Inductive unopT: Type :=
  | Oneg | Onot.

  Inductive t: Type :=
  | Evar: PVar.t -> t
  | Econst: ZNum.t -> t
  | Eitv: ZItv.t -> t
  | Eunknown
  | Eunop: unopT -> t -> t
  | Ebinop: binopT -> t -> t -> t.

  Local Open Scope string_scope.

  Fixpoint pr (e: t): string
    := match e with
         | Evar x => CoqAddOn.sprintf "Evar (%s)" ((PVar.pr x)::nil)
         | Econst n => CoqAddOn.sprintf "Econst (%s)" (ZNum.pr n :: nil)
         | Eitv i => CoqAddOn.sprintf "Eitv (%s)" ((ZItv.pr i)::nil)
         | Eunknown => "unknown"
         | Eunop op e =>
           let estr := pr e in
           match op with
             | Oneg => CoqAddOn.sprintf "-(%s)" (estr::nil)
             | Onot => CoqAddOn.sprintf "not(%s)" (estr::nil)
           end
         | Ebinop op e1 e2 =>
           let ostr :=
               match op with
   | Oadd => "+" | Osub => "-" | Omul => "*" | Odiv => "/"
   | Omod => "mod" | Oand => "&" | Oor => "|" | Oxor => "xor"
   | Oshl => "shl" | Oshr => "oshr"
   | Ocmp c => Cmp.pr c
               end
           in
           CoqAddOn.sprintf "(%s) %s (%s)" (pr e1 :: ostr :: pr e2 :: nil)
       end.

  Local Close Scope string_scope.

  Inductive EvalBinop: binopT -> ZNum.t -> ZNum.t -> ZNum.t -> Prop :=
  | EvalBinopAdd: forall z1 z2, EvalBinop Oadd z1 z2 (z1 + z2)
  | EvalBinopSub: forall z1 z2, EvalBinop Osub z1 z2 (z1 - z2)
  | EvalBinopMul: forall z1 z2, EvalBinop Omul z1 z2 (z1 * z2)
  | EvalBinopDiv: forall z1 z2, z2 <> 0 -> EvalBinop Odiv z1 z2 (Z.quot z1 z2)
  | EvalBinopMod: forall z1 z2, z2 <> 0 -> EvalBinop Omod z1 z2 (Z.rem z1 z2)
  | EvalBinopAnd: forall z1 z2, EvalBinop Oand z1 z2 (Z.land z1 z2)
  | EvalBinopOr: forall z1 z2, EvalBinop Oor z1 z2 (Z.lor z1 z2)
  | EvalBinopXor: forall z1 z2, EvalBinop Oxor z1 z2 (Z.lxor z1 z2)
  | EvalBinopShl: forall z1 z2, EvalBinop Oshl z1 z2 (Z.shiftl z1 z2)
  | EvalBinopShr: forall z1 z2, EvalBinop Oshr z1 z2 (Z.shiftr z1 z2)
  | EvalBinopCmp: forall c z1 z2,
                    EvalBinop (Ocmp c) z1 z2 (if Cmp.dec c z1 z2 then 1 else 0).

  Inductive EvalUnop: unopT -> ZNum.t -> ZNum.t -> Prop :=
  | EvalUnopNeg: forall z, EvalUnop Oneg z (-z)
  | EvalUnopNot: forall z, EvalUnop Onot z (Z.lnot z).

  Inductive denote (m: Mem.t ZNum.t): t -> ZNum.t -> Prop :=
  | EvalEvar: forall x z, m x = z -> denote m (Evar x) z
  | EvalEconst: forall z, denote m (Econst z) z
  | EvalEitv: forall z i, ZItv.sat i z -> denote m (Eitv i) z
  | EvalEunknown: forall z, denote m Eunknown z
  | EvalEunop: forall op e z1 z2,
                 denote m e z1 ->
                 EvalUnop op z1 z2 ->
                 denote m (Eunop op e) z2
  | EvalEbinop: forall op e1 e2 z1 z2 z3,
                  denote m e1 z1 ->
                  denote m e2 z2 ->
                  EvalBinop op z1 z2 z3 ->
                  denote m (Ebinop op e1 e2) z3.

End Expr.

Module Tr.

  Import ASTerm.
  Import ASCond.

Replace singleton intervals by integer constants.
  Fixpoint itv2z (e: Expr.t): Expr.t
    := match e with
         | Expr.Evar x => Expr.Evar x
         | Expr.Econst z => Expr.Econst z
         | Expr.Eitv (ZItv.NotBot (ZItv.Closed l) (ZItv.Closed u) _) as i =>
           if ZNum.eqDec l u then Expr.Econst l else i
         | Expr.Eitv i => Expr.Eitv i
         | Expr.Eunknown => Expr.Eunknown
         | Expr.Eunop op e' => Expr.Eunop op (itv2z e')
         | Expr.Ebinop op e1 e2 => Expr.Ebinop op (itv2z e1) (itv2z e2)
       end.

  Lemma itv2z_correct: forall e m z, Expr.denote m e z ->
                                     Expr.denote m (itv2z e) z.
Proof.
    intros e m z h.
    induction h.
    - constructor.
      assumption.
    - constructor.
    - destruct i;
      [contradiction H|idtac].
      destruct low;
        [constructor;assumption|constructor;assumption|idtac].
      destruct up;
        [constructor;assumption|constructor;assumption|idtac].
      unfold itv2z.
      destruct (ZNum.eqDec t t0) as [ht|ht];
        [idtac|constructor;assumption].
      unfold ZItv.sat, ZItv.satLower, ZItv.satUpper in H.
      subst.
      apply ZNum.LeLeEq in H.
      subst.
      constructor.
    - constructor.
    - apply Expr.EvalEunop with (z1 := z1);
      assumption.
    - apply Expr.EvalEbinop with (z1 := z1) (z2 := z2);
      assumption.
  Qed.

Replace e1 - e2 with e1 + (-e2).
  Fixpoint sub2add (e: Expr.t): Expr.t
    := match e with
         | Expr.Ebinop Expr.Osub e1 e2 =>
           Expr.Ebinop Expr.Oadd (sub2add e1) (Expr.Eunop Expr.Oneg (sub2add e2))
         | Expr.Eunop op e' => Expr.Eunop op (sub2add e')
         | _ as e' => e'
       end.

  Lemma sub2add_correct: forall e m z, Expr.denote m e z ->
                                       Expr.denote m (sub2add e) z.
Proof.
    intros e m z h.
    induction h;
      try (constructor; assumption).
    - simpl.
      constructor 5 with (z1 := z1);
        assumption.
    - destruct op;
      try (constructor 6 with (z1 := z1) (z2 := z2);assumption).
      inversion H.
      simpl.
      constructor 6 with (z1 := z1) (z2 := -z2).
      assumption.
      constructor 5 with (z1 := z2).
      assumption.
      constructor.
      constructor.
  Qed.

  Definition simplify: Expr.t -> Expr.t
    := fun e => sub2add (itv2z e).

  Lemma simplify_correct: forall e m z, Expr.denote m e z ->
                                        Expr.denote m (simplify e) z.
Proof.
    intros.
    apply sub2add_correct, itv2z_correct.
    assumption.
  Qed.

  Definition bind {A B: Type}: option A -> (A -> option B) -> option B
    := fun maybe =>
         match maybe with
           | Some e => fun f => f e
           | None => fun _ => None
         end.

  Fixpoint expr_aux (e: Expr.t): option ZTerm.t
    := match e with
         | Expr.Evar x => Some (ZTerm.Var x)
         | Expr.Econst z => Some (ZTerm.Cte z)
         | Expr.Eitv i => None
         | Expr.Eunknown => None
         | Expr.Eunop op e' =>
           match op with
             | Expr.Oneg => bind (expr_aux e') (fun e => Some (ZTerm.Opp e))
             | Expr.Onot => None
           end
         | Expr.Ebinop op e1 e2 =>
           match op with
             | Expr.Oadd =>
               bind (expr_aux e1) (fun e1 =>
                 bind (expr_aux e2) (fun e2 => Some (ZTerm.Add e1 e2)))
             | Expr.Osub =>
               bind (expr_aux e1) (fun e1 =>
                 bind (expr_aux e2) (fun e2 => Some (ZTerm.Add e1 (ZTerm.Opp e2))))
             | Expr.Omul =>
               bind (expr_aux e1) (fun e1 =>
                 bind (expr_aux e2) (fun e2 => Some (ZTerm.Mul e1 e2)))
             | _ => None
           end
       end.

  Lemma expr_aux_correct: forall (m: Mem.t ZNum.t) (e: Expr.t) (z: ZNum.t),
                        Expr.denote m e z ->
                        forall (e': ZTerm.t),
                          expr_aux e = Some e' -> ZTerm.eval e' m = z.
Proof.
    intros m e z hden.
    induction hden as [x z h|z|z i h|
                       |op e0 z1 z2 hden hind heval
                       |op e1 e2 z1 z2 z3 hden1 hind1 hden2 hind2 heval];
      intros e' hr.
    - (* Evar *)
      inversion hr.
      assumption.
    - (* Econst *)
      inversion hr.
      reflexivity.
    - (* Eitv *)
      discriminate hr.
    - (* Eunknown *)
      discriminate hr.
    - (* Eunop *)
      destruct op;
      [idtac|discriminate hr].
      simpl in hr.
      destruct (expr_aux e0);
        [idtac|discriminate hr].
      inversion hr.
      inversion heval.
      subst.
      simpl.
      rewrite hind;
        reflexivity.
    - (* Ebinop *)
      destruct op;
      try discriminate hr ;
      ( (* NB two cases: Oadd / Omul *)
        simpl in hr;
        destruct (expr_aux e1) as [e1'|];
          [idtac|discriminate hr];
        destruct (expr_aux e2) as [e2'|];
          [idtac|discriminate hr];
        inversion hr;
        inversion heval;
        subst;
        simpl;
        rewrite hind1, hind2;
          reflexivity ).
 OLD Omul case: 
      + simpl in hr.
        destruct e1;
          try (
              apply expr_aux_correct_mul1 with (e2 := e2) (z1 := z1) (z2 := z2);
              [assumption|assumption|assumption|idtac];
              inversion hden1;
              subst;
              assumption);
        destruct e2;
          try discriminate hr;
          match goal with
            | h: Expr.denote m ?e z1 |- _ =>
              apply expr_aux_correct_mul2
              with (e2 := e) (z1 := z2) (z2 := z1);
                [assumption|assumption|assumption|idtac];
                  inversion hden2;
                  subst;
                  assumption
            | _ => idtac
          end.
     *)  Qed.

  Definition expr (e: Expr.t): option ZTerm.t
    := expr_aux (simplify e).

  Lemma expr_correct: forall m e z, Expr.denote m e z ->
                                    forall e', expr e = Some e' ->
                                               ZTerm.eval e' m = z.
Proof.
    intros m e z h e' hr.
    unfold expr in hr.
    apply simplify_correct in h.
    apply expr_aux_correct with (e := simplify e);
      assumption.
  Qed.

  Definition cmp: Cmp.t -> ZTerm.t -> ZTerm.t -> ZCond.t
    := fun r e1 e2 =>
         match r with
           | Cmp.Eq => ZCond.Atom Eq e1 e2
           | Cmp.Le => ZCond.Atom Le e1 e2
           | Cmp.Lt => ZCond.Atom Lt e1 e2
           | Cmp.Neq => ZCond.Atom Neq e1 e2
           | Cmp.Ge => ZCond.Atom Le e2 e1
           | Cmp.Gt => ZCond.Atom Lt e2 e1
         end.

  Lemma cmp_correct: forall (r: Cmp.t) (e1 e2: ZTerm.t) (m: Mem.t ZNum.t),
                       Cmp.denote r (ZTerm.eval e1 m) (ZTerm.eval e2 m) <->
                       ZCond.sat (cmp r e1 e2) m.
Proof.
    intros r e1 e2 m.
    split;
      intro h;
      destruct r;
      assumption.
  Qed.

  Definition MatchingCorrect (e : Expr.t) (r : option ZCond.t) : Prop
    := forall (m: Mem.t ZNum.t) (z: ZNum.t),
         Expr.denote m e z ->
         forall c: ZCond.t,
           r = Some c ->
           (if ZCond.sat_dec c m then 1 else 0) = z.

  Definition simpl_cond (e: Expr.t): option ZCond.t
    := match e with
         | Expr.Ebinop (Expr.Ocmp r) e1 e2 =>
           bind (expr e1) (fun e1' =>
             bind (expr e2) (fun e2' => Some (cmp r e1' e2')))
         | _ => None
       end.

  Lemma simpl_cond_correct : forall e, MatchingCorrect e (simpl_cond e).
Proof.
    intros e m z hden.
    induction hden as [| | | | |op e1 e2 z1 z2 z3 hden1 hind1 hden2 hind2 heval];
      intros c hr.
    - discriminate hr.
    - discriminate hr.
    - discriminate hr.
    - discriminate hr.
    - discriminate hr.
    - destruct op as [| | | | | | | | | |op];
      try discriminate hr.
      simpl in hr.
      assert (pf1 := expr_correct m e1 z1 hden1).
      assert (pf2 := expr_correct m e2 z2 hden2).
      destruct (expr e1) as [e1'|];
        [idtac|discriminate hr].
      destruct (expr e2) as [e2'|];
        [idtac|discriminate hr].
      inversion hr.
      inversion heval.
      subst.
      destruct (Cmp.dec op z1 z2) as [h|h];
      destruct (ZCond.sat_dec (cmp op e1' e2') m) as [h'|h'].
      + reflexivity.
      + contradiction h'.
        apply cmp_correct.
        rewrite pf1, pf2.
        assumption.
        reflexivity.
        reflexivity.
      + contradiction h.
        rewrite <- pf1 with (e' := e1'), <- pf2 with (e' := e2').
        apply cmp_correct.
        assumption.
        reflexivity.
        reflexivity.
      + reflexivity.
  Qed.

  Lemma comparison_result : forall m r e1 e2 z,
                              Expr.denote m (Expr.Ebinop (Expr.Ocmp r) e1 e2) z ->
                              z = 1 \/ z = 0.
Proof.
    intros;
    match goal with
      | h : Expr.denote _ (Expr.Ebinop (Expr.Ocmp _) _ _) _ |- _ => inversion h
    end;
      match goal with
        | h : Expr.EvalBinop (Expr.Ocmp _) _ _ _ |- _ => inversion h
      end;
      match goal with
        | |- (if Cmp.dec ?r ?z1 ?z2 then 1 else 0) = 1 \/
             (if Cmp.dec ?r ?z1 ?z2 then 1 else 0) = 0 =>
          destruct (Cmp.dec r z1 z2); [left|right]; reflexivity
      end.
  Qed.

  Ltac inline_const :=
    match goal with
      | h : Expr.denote _ (Expr.Econst _) _ |- _ => inversion h; subst; clear h
    end.

  Lemma valued_test_simplify_true_true : forall m r e1 e2,
                                 Expr.denote m (Expr.Ebinop (Expr.Ocmp Cmp.Eq)
                                                            (Expr.Ebinop (Expr.Ocmp r) e1 e2)
                                                            (Expr.Econst 1)) 1 ->
                                 Expr.denote m (Expr.Ebinop (Expr.Ocmp r) e1 e2) 1.
Proof.
    intros ? ? ? ? h;
    inversion h; subst; clear h;
    inline_const;
    match goal with
      | h : Expr.denote _ _ ?z |- Expr.denote _ _ 1 =>
        replace 1 with z; [assumption|]
    end;
    match goal with
      | h : Expr.EvalBinop (Expr.Ocmp Cmp.Eq) ?z1 1 1 |- _ =>
        inversion h; destruct (ZNum.eqDec z1 1)
    end;
    solve [assumption|discriminate].
  Qed.

  Lemma valued_test_simplify_true_false : forall m r e1 e2,
                                 Expr.denote m (Expr.Ebinop (Expr.Ocmp Cmp.Eq)
                                                            (Expr.Ebinop (Expr.Ocmp r) e1 e2)
                                                            (Expr.Econst 1)) 0 ->
                                 Expr.denote m (Expr.Ebinop (Expr.Ocmp r) e1 e2) 0.
Proof.
    intros ? ? ? ? h;
    inversion h; subst; clear h;
    inline_const;
    match goal with
      | h : Expr.denote _ _ ?z |- Expr.denote _ _ 0 =>
        replace 0 with z; [assumption|apply comparison_result in h];
        match goal with
          | h' : Expr.EvalBinop (Expr.Ocmp Cmp.Eq) ?z1 1 0 |- _ =>
            inversion h'; subst; clear h'
        end;
        destruct (ZNum.eqDec z1 1); destruct h
    end;
    solve [assumption|discriminate|contradiction].
  Qed.

  Lemma valued_test_simplify_false_true : forall m r e1 e2,
                                 Expr.denote m (Expr.Ebinop (Expr.Ocmp Cmp.Eq)
                                                            (Expr.Ebinop (Expr.Ocmp r) e1 e2)
                                                            (Expr.Econst 0)) 1 ->
                                 Expr.denote m (Expr.Ebinop (Expr.Ocmp r) e1 e2) 0.
Proof.
    intros ? ? ? ? h;
    inversion h; subst; clear h;
    inline_const;
    match goal with
      | h : Expr.denote _ _ ?z |- Expr.denote _ _ 0 =>
        replace 0 with z; [assumption|]
    end;
    match goal with
      | h : Expr.EvalBinop (Expr.Ocmp Cmp.Eq) ?z1 0 1 |- _ =>
        inversion h; destruct (ZNum.eqDec z1 0)
    end;
    solve [assumption|discriminate].
  Qed.

  Lemma valued_test_simplify_false_false : forall m r e1 e2,
                                 Expr.denote m (Expr.Ebinop (Expr.Ocmp Cmp.Eq)
                                                            (Expr.Ebinop (Expr.Ocmp r) e1 e2)
                                                            (Expr.Econst 0)) 0 ->
                                 Expr.denote m (Expr.Ebinop (Expr.Ocmp r) e1 e2) 1.
Proof.
    intros ? ? ? ? h;
    inversion h; subst; clear h;
    inline_const.
    match goal with
      | h : Expr.denote _ _ ?z |- Expr.denote _ _ 1 =>
        replace 1 with z; [assumption|apply comparison_result in h];
        match goal with
          | h' : Expr.EvalBinop (Expr.Ocmp Cmp.Eq) ?z1 0 0 |- _ =>
            inversion h'; subst; clear h'
        end;
        destruct (ZNum.eqDec z1 0); destruct h
    end;
    solve [assumption|discriminate|contradiction].
  Qed.

  Definition is_const : ZNum.t -> Expr.t -> bool
    := fun n e =>
         match e with
           | Expr.Econst n' => if ZNum.eqDec n n' then true else false
           | _ => false
         end.

  Definition valued_cond : Expr.t -> option ZCond.t
    := fun e =>
         match e with
           | Expr.Ebinop (Expr.Ocmp Cmp.Eq) e1 e2 =>
             if is_const 1 e2
             then simpl_cond e1
             else
               if is_const 0 e2
               then bind (simpl_cond e1) (fun c => Some (ZCond.Not c))
               else None
           | _ => None
         end.

  Lemma valued_cond_correct : forall e, MatchingCorrect e (valued_cond e).
Proof.
    unfold MatchingCorrect.
    intros e m z hden c hres.
    destruct e; try discriminate hres.
    destruct b; try discriminate hres.
    destruct t; try discriminate hres.
    simpl in hres.
    unfold is_const in hres.
    destruct e2; try discriminate hres.
    destruct (ZNum.eqDec 1 t); [subst|clear n].
    - assert (hsimpl := simpl_cond_correct e1).
      destruct e1; try discriminate hres.
      destruct b; try discriminate hres.
      destruct (comparison_result _ _ _ _ _ hden); subst.
      + apply valued_test_simplify_true_true in hden.
        apply hsimpl; assumption.
      + apply valued_test_simplify_true_false in hden.
        apply hsimpl; assumption.
    - destruct (ZNum.eqDec 0 t); [subst|discriminate].
      assert (hsimpl := simpl_cond_correct e1).
      destruct e1; try discriminate.
      destruct b; try discriminate.
      destruct (simpl_cond (Expr.Ebinop (Expr.Ocmp t) e1_1 e1_2)); try discriminate.
      inversion hres; subst; clear hres.
      destruct (comparison_result _ _ _ _ _ hden); subst.
      + apply valued_test_simplify_false_true in hden.
        specialize (hsimpl m 0 hden t0 (eq_refl _)).
        destruct (ZCond.sat_dec t0 m); try discriminate.
        destruct (ZCond.sat_dec (ZCond.Not t0) m).
        reflexivity.
        contradiction n0.
      + apply valued_test_simplify_false_false in hden.
        specialize (hsimpl m 1 hden t0 (eq_refl _)).
        destruct (ZCond.sat_dec t0 m); try discriminate.
        destruct (ZCond.sat_dec (ZCond.Not t0) m).
        contradiction s0.
        reflexivity.
  Qed.

  Definition cond : Expr.t -> option ZCond.t
    := fun e =>
         let e' := simplify e in
         match valued_cond e' with
           | Some _ as r => r
           | None => simpl_cond e'
         end.

  Lemma cond_correct : forall e, MatchingCorrect e (cond e).
Proof.
    intro e.
    assert (h := valued_cond_correct (simplify e)).
    unfold cond.
    destruct (valued_cond (simplify e));
      unfold MatchingCorrect; intros.
    - apply h; [apply simplify_correct|]; assumption.
    - clear h.
      eapply simpl_cond_correct.
      apply simplify_correct.
      eassumption.
      assumption.
  Qed.

  Lemma cond_correct_inv1: forall (c: ZCond.t) (rho: Mem.t ZNum.t),
                            (if ZCond.sat_dec c rho then 1 else 0) = 1 ->
                            ZCond.sat c rho.
Proof.
    intros c rho h.
    destruct (ZCond.sat_dec c rho).
    assumption.
    discriminate h.
  Qed.

  Lemma cond_correct_inv2: forall (c: ZCond.t) (rho: Mem.t ZNum.t),
                            (if ZCond.sat_dec c rho then 1 else 0) = 0 ->
                            ~ ZCond.sat c rho.
Proof.
    intros c rho h.
    destruct (ZCond.sat_dec c rho).
    discriminate h.
    assumption.
  Qed.

  Definition asg_itv: PVar.t -> ZItv.t -> option ZCond.t
    := fun x i =>
         match i with
           | ZItv.Bot => None
           | ZItv.NotBot lbnd ubnd _ =>
             let mk: ZCond.t -> option ZCond.t
                 := fun l' =>
                      match ubnd with
                        | ZItv.Infty => Some l'
                        | ZItv.Open u =>
                          let u' := ZCond.Atom Lt (ZTerm.Var x) (ZTerm.Cte u) in
                          Some (ZCond.BinL AND l' u')
                        | ZItv.Closed u =>
                          let u' := ZCond.Atom Le (ZTerm.Var x) (ZTerm.Cte u) in
                          Some (ZCond.BinL AND l' u')
                      end
             in
             match lbnd with
               | ZItv.Infty =>
                 match ubnd with
                   | ZItv.Infty => None
                   | ZItv.Open u =>
                     Some (ZCond.Atom Lt (ZTerm.Var x) (ZTerm.Cte u))
                   | ZItv.Closed u =>
                     Some (ZCond.Atom Le (ZTerm.Var x) (ZTerm.Cte u))
                 end
               | ZItv.Open l =>
                 mk (ZCond.Atom Lt (ZTerm.Cte l) (ZTerm.Var x))
               | ZItv.Closed l =>
                 mk (ZCond.Atom Le (ZTerm.Cte l) (ZTerm.Var x))
             end
         end.

  Lemma asg_itv_correct: forall (x: PVar.t) (i: ZItv.t) (m: Mem.t ZNum.t)
                                (z: ZNum.t),
                           ZItv.sat i z ->
                           forall (c: ZCond.t),
                             asg_itv x i = Some c ->
                             ZCond.xsat c m (Mem.assign x z m).
Proof.
    intros x i m z hsat c hr.
    destruct i as [|lbnd ubnd pfbnd];
      [discriminate hr|idtac].
    unfold ZItv.sat, ZItv.satUpper, ZItv.satLower in hsat.
    destruct hsat as [hsatl hsatu].
    destruct lbnd as [|l|l];
      destruct ubnd as [|u|u];
      inversion hr;
      simpl;
      rewrite Mem.assign_in;
      match goal with
        | |- _ /\ _ => split; assumption
        | _ => assumption
      end.
  Qed.

  Definition asg: PVar.t -> Expr.t -> option ZCond.t
    := fun x e =>
         match simplify e with
           | Expr.Eitv i => asg_itv x i
           | _ as e =>
             match Tr.expr_aux e with
               | Some e' => Some (ZCond.Atom Eq (ZTerm.Var x) (ZTerm.Old e'))
               | None => None
             end
         end.

  Lemma asg_correct: forall (x: PVar.t) (e: Expr.t) (m: Mem.t ZNum.t) (z: ZNum.t),
                       Expr.denote m e z ->
                       forall (c: ZCond.t),
                         asg x e = Some c ->
                         ZCond.xsat c m (Mem.assign x z m).
Proof.
    intros x e m z hden c hasg.
    apply simplify_correct in hden.
    unfold asg in hasg.
    assert (pfexpr := expr_aux_correct m (simplify e) z hden).
    destruct (simplify e);
    match goal with
      | h: Expr.denote m (Expr.Eitv _) z |- _ =>
        inversion h;
        apply asg_itv_correct with (i := i);
        subst;
        assumption
      | h: Expr.denote m ?e z |- _ =>
        destruct (expr_aux e) as [e'|];
          [idtac|discriminate hasg];
          specialize (pfexpr e' (eq_refl _));
          inversion hasg as [hasg'];
          subst;
          apply Mem.assign_in
      | _ => idtac
    end.
  Qed.

End Tr.

Require TrustedPedraZ.

Module AbDom.

  Definition A: Type
    := TrustedPedraZ.FullDom.t.

  Definition pr: A -> String.string
    := TrustedPedraZ.FullDom.pr.

  Definition B: Type
    := Mem.t ZNum.t.

  Definition gamma: A -> B -> Prop
    := TrustedPedraZ.FullDom.gamma.

  Instance gamma_ext: Proper (Logic.eq ==> pointwise_relation PVar.t Logic.eq ==> iff) gamma.
   intros ab ab'.
   intros Heq m m' Heqm.
   apply TrustedPedraZ.FullDom.gamma_ext. auto. auto.
  Qed.
  Definition top: A
    := TrustedPedraZ.FullDom.top.

  Definition leb: A -> A -> bool
    := fun ab1 ab2 => TrustedPedraZ.FullDom.isIncl ab1 ab2.

  Lemma gamma_monotone: forall (ab1 ab2: A),
                          leb ab1 ab2 = true ->
                          forall rho: B, gamma ab1 rho -> gamma ab2 rho.
Proof.
    intros ab1 ab2 hleb.
    assert (pf := TrustedPedraZ.FullDom.isIncl_correct ab1 ab2).
    unfold OptionMonad.ifprop in pf.
    unfold leb in hleb.
    rewrite hleb in pf.
    assumption.
  Qed.

  Lemma gamma_top: forall x: B, gamma top x.
Proof.
    exact TrustedPedraZ.FullDom.top_correct.
  Qed.

  Definition bottom : A := TrustedPedraZ.FullDom.bottom.

  Definition isBottom : A -> bool := TrustedPedraZ.FullDom.isBottom.

  Lemma isBottom_correct : forall ab : A, isBottom ab = true -> forall m : B, ~ gamma ab m.
Proof.
    intros ab hyp m.
    assert (pf := TrustedPedraZ.FullDom.isBottom_correct ab).
    unfold OptionMonad.ifprop in pf.
    unfold isBottom in hyp.
    destruct TrustedPedraZ.FullDom.isBottom.
    exact (pf m).
    discriminate hyp.
  Qed.

  Definition join: A -> A -> A
    := fun ab1 ab2 => TrustedPedraZ.FullDom.join ab1 ab2.

  Lemma join_sound: forall (ab1 ab2: A) (x: B),
                      gamma ab1 x \/ gamma ab2 x -> gamma (join ab1 ab2) x.
Proof.
    intros ab1 ab2 x [h|h].
    apply TrustedPedraZ.FullDom.join_correct1.
    assumption.
    apply TrustedPedraZ.FullDom.join_correct2.
    assumption.
  Qed.

  Definition widen: A -> A -> A
    := TrustedPedraZ.FullDom.widen.

  Definition itv_one: ZItv.t.
    refine (ZItv.NotBot (ZItv.Closed 1) (ZItv.Closed 1) _).
    constructor.
    apply ZNum.LeRefl.
  Defined.
  Lemma itv_one_sat: ZItv.sat itv_one 1.
Proof.
    constructor; apply ZNum.LeRefl.
  Qed.

  Definition itv_zero: ZItv.t.
    refine (ZItv.NotBot (ZItv.Closed 0) (ZItv.Closed 0) _).
    constructor.
    apply ZNum.LeRefl.
  Defined.
  Lemma itv_zero_sat: ZItv.sat itv_zero 0.
Proof.
    constructor; apply ZNum.LeRefl.
  Qed.

  Definition itv_unit: ZItv.t.
    refine (ZItv.NotBot (ZItv.Closed 0) (ZItv.Closed 1) _).
    constructor.
    apply Z.le_0_1.
  Defined.
  Lemma itv_unit_sat0: ZItv.sat itv_unit 0.
Proof.
    constructor.
    apply ZNum.LeRefl.
    apply Z.le_0_1.
  Qed.

  Lemma itv_unit_sat1: ZItv.sat itv_unit 1.
Proof.
    constructor.
    apply Z.le_0_1.
    apply ZNum.LeRefl.
  Qed.

  Definition get_itv_cond: ASCond.ZCond.t -> A -> ZItv.t
    := fun c ab =>
         if TrustedPedraZ.FullDom.assert c ab
         then itv_one
         else
           if TrustedPedraZ.FullDom.assert (ASCond.ZCond.Not c) ab
           then itv_zero
           else itv_unit.

  Lemma get_itv_cond_correct: forall (c: ASCond.ZCond.t) (ab: A) (rho: B),
                                gamma ab rho ->
                                ZItv.sat (get_itv_cond c ab)
                                         (if ASCond.ZCond.sat_dec c rho
                                          then 1 else 0).
Proof.
    intros c ab rho hgamma.
    unfold get_itv_cond.
    assert (pf := TrustedPedraZ.FullDom.assert_correct c ab).
    destruct (TrustedPedraZ.FullDom.assert c ab).
    - simpl in pf.
      specialize (pf rho hgamma).
      destruct (ASCond.ZCond.sat_dec c rho) as [pfc|pfc].
      apply itv_one_sat.
      contradiction pfc.
    - clear pf.
      assert (pf := TrustedPedraZ.FullDom.assert_correct
                      (ASCond.ZCond.Not c) ab).
      destruct (TrustedPedraZ.FullDom.assert
                      (ASCond.ZCond.Not c) ab).
      + simpl in pf.
        specialize (pf rho hgamma).
        destruct (ASCond.ZCond.sat_dec c rho) as [pfc|pfc].
        contradiction pf.
        apply itv_zero_sat.
      + destruct (ASCond.ZCond.sat_dec c rho).
        apply itv_unit_sat1.
        apply itv_unit_sat0.
  Qed.

  Definition get_itv: Expr.t -> A -> ZItv.t
    := fun e ab =>
         match Tr.expr e with
           | Some e' => TrustedPedraZ.FullDom.get_itv e' ab
           | None =>
             match Tr.cond e with
               | Some c => get_itv_cond c ab
               | None => ZItv.NotBot ZItv.Infty ZItv.Infty (ZItv.BndInftyLow _)
             end
         end.

  Lemma get_itv_correct: forall (e: Expr.t) (rho: B) (ab: A),
                           gamma ab rho ->
                           forall z, Expr.denote rho e z ->
                                     ZItv.sat (get_itv e ab) z.
Proof.
    intros e rho ab hgamma z hden.
    assert (pfe := Tr.expr_correct rho e z hden).
    unfold get_itv.
    destruct (Tr.expr e) as [e'|].
    - specialize (pfe e' (eq_refl _)).
      rewrite <- pfe.
      apply TrustedPedraZ.FullDom.get_itv_correct.
      assumption.
    - clear pfe.
      assert (pfc := Tr.cond_correct e rho z hden).
      destruct (Tr.cond e) as [c|];
        [idtac|constructor;constructor].
      specialize (pfc c (eq_refl _)).
      rewrite <- pfc.
      apply get_itv_cond_correct.
      assumption.
  Qed.

  Definition assume: Expr.t -> bool -> A -> A
    := fun e b ab =>
         match Tr.cond e with
           | Some c =>
             if b
             then
               TrustedPedraZ.FullDom.assume c ab
             else
               TrustedPedraZ.FullDom.assume (ASCond.ZCond.Not c) ab
           | None => ab
         end.

  Lemma assume_correct: forall (c: Expr.t) (rho: B) (ab: A) (b: bool),
                          gamma ab rho ->
                          Expr.denote rho c (if b then 1 else 0) ->
                          gamma (assume c b ab) rho.
    intros e rho ab b hab hden.
    unfold assume.
    assert (hcond := Tr.cond_correct e rho (if b then 1 else 0) hden).
    destruct (Tr.cond e) as [c|];
      [idtac|assumption].
    specialize (hcond c (eq_refl _)).
    destruct b;
      [apply Tr.cond_correct_inv1 in hcond|apply Tr.cond_correct_inv2 in hcond];
    apply TrustedPedraZ.FullDom.assume_correct;
      [idtac|assumption|idtac|assumption];
    assumption.
  Qed.
  Definition project: A -> PVar.t -> A
    := fun ab x => TrustedPedraZ.FullDom.project ab x.

  Lemma project_correct: forall (ab: A) (x: PVar.t) (m: B) (z: ZNum.t),
                           gamma ab m -> gamma (project ab x) (Mem.assign x z m).
Proof.
    exact TrustedPedraZ.FullDom.project_correct.
  Qed.

  Definition assign: PVar.t -> Expr.t -> A -> A
    := fun x e ab =>
         match Tr.asg x e with
           | Some c => TrustedPedraZ.FullDom.guassign x c ab
           | None => project ab x
         end.

  Lemma assign_correct: forall (x: PVar.t) (e: Expr.t) (m: B) (z: ZNum.t)
                               (ab: A), gamma ab m ->
                                        Expr.denote m e z ->
                                        gamma (assign x e ab) (Mem.assign x z m).
Proof.
    intros x e m z ab h1 h2.
    unfold assign.
    assert (pfa := Tr.asg_correct x e m z h2).
    destruct (Tr.asg x e) as [c|];
      [idtac|apply project_correct;assumption].
    specialize (pfa c (eq_refl _)).
    unfold gamma.
    apply TrustedPedraZ.FullDom.guassign_correct; [idtac|assumption].
    assumption.
  Qed.

End AbDom.
Generated by coq2html