Module PedraQ

This module implements the basic abstract domain of polyhedra on atomic conditions over rationals. It builds on ConsSet and adds to it the coupling with opaque Ocaml polyhedra, operations on which serve as an oracle for operations in ConsSet. It also adds the possibility for a polyhedron to be empty.

Require Import List.
Require Import String.
Require CoqAddOn.
Require Import LinTerm.
Require Import ConsSet.
Require Backend.
Require Import Itv.
Require Export ASCond.
Require Import Debugging.
Require Export Impure.

Open Scope impure.

Module BasicD <: BasicDomain QNum.

Coupling of a ConsSet with an opaque Ocaml polyhedron.
  Record polT: Type := mk {
    cons: Cs.t;
    ml: Backend.t
  }.

  Definition polPr: polT -> string
    := fun p =>
      CoqAddOn.sprintf "{coq:\n%s\nocaml:\n%s}"
      ((Cs.pr (cons p))::(Backend.pr (ml p))::nil).

  Definition polTop: polT
    := mk Cs.top Backend.top.

Empty polyhedron is encoded as None, Some p encodes a non-empty polyhedron
  Definition t:=option polT.

  Local Open Scope string_scope.
  Definition pr: t -> string
    := fun p =>
      match p with
        | None => "bot"
        | Some p' => "notbot " ++ (polPr p')
      end.


  Definition gamma (a: t) (m: Mem.t QNum.t) :=
    (EXISTS p <- a SUCH Cs.sat (cons p) m)%option.

   Instance gamma_ext: Proper (Logic.eq ==> pointwise_relation PVar.t Logic.eq ==> iff) gamma.
Proof.
     eapply sat_compat_iff; unfold gamma.
     intros x y H m1 m2 H0 H1. subst; PedraQsimplify.
     erewrite (eval_pointwise_compat Cs.sat_mdo); eauto.
   Qed.

  Definition top: t
    := Some polTop.

  Lemma top_correct: forall m, gamma top m.
    simpl; auto.
  Qed.
  Hint Resolve top_correct: vpl.

  Definition bottom: t := None.

  Lemma bottom_correct: forall m, ~(gamma bottom m).
Proof.
    simpl; auto.
  Qed.

  Definition isBottom : t -> imp bool
    := fun p =>
          match p with
          | None => pure true
          | Some pol =>
               BIND isEmpty <- Backend.isEmpty (ml pol) -;
               pure match isEmpty with
                     | None => false
                     | Some cert => Cs.chkEmpty (cons pol) cert
                     end
          end.

  Lemma isBottom_correct : forall a, If isBottom a THEN forall m, gamma a m -> False.
Proof.
    unfold isBottom.
    xasimplify ltac:(eauto with pedraQ).
  Qed.

  Global Opaque isBottom.

  Definition isIncl (p1 p2:t) : imp bool
    := match p1 with
          | None => pure true
          | Some pol1 =>
            match p2 with
              | None =>
                BIND isEmpty <- Backend.isEmpty (ml pol1) -;
                pure match isEmpty with
                     | None => false
                     | Some cert => Cs.chkEmpty (cons pol1) cert
                     end
              | Some pol2 =>
                BIND isIncl <- Backend.isIncl (ml pol1, ml pol2) -;
                pure match isIncl with
                     | None => false
                     | Some cert => Cs.chkIncl (cons pol1) (cons pol2) cert
                     end
            end
        end.

  Lemma isIncl_correct p1 p2: If isIncl p1 p2 THEN forall m, gamma p1 m -> gamma p2 m.
Proof.
    unfold isIncl. xasimplify ltac:(eauto with pedraQ).
  Qed.
  Hint Resolve isIncl_correct: vpl.
  Global Opaque isIncl.


  Definition meet (p1 p2:t): imp t :=
    SOME p1' <- p1 -;
    SOME p2' <- p2 -;
    BIND meet <- Backend.meet (ml p1', ml p2') -;
    pure (
      let (maybeP, ce) := meet in
      match maybeP with
        | Some p => Some (mk (Cs.meet (cons p1') (cons p2') ce) p)
        | None =>
          if Cs.meetEmpty (cons p1') (cons p2') ce
            then None
            else failwith "PedraQ.meet" top
      end).

  Lemma meet_correct p1 p2: WHEN p <- meet p1 p2 THEN forall m, gamma p1 m -> gamma p2 m ->gamma p m.
Proof.
    unfold meet. xasimplify ltac:(eauto with pedraQ).
  Qed.

  Definition join (p1 p2:t) : imp t :=
    match p1, p2 with
      | None, None => pure None
      | None, pol
      | pol, None => pure pol
      | Some pol1, Some pol2 =>
        BIND join <- Backend.join (ml pol1, ml pol2) -;
        let (shadow, cert) := join in
          pure (Some (mk (Cs.buildJoin (cons pol1) (cons pol2) cert) shadow))
    end.

  Lemma join_correct p1 p2: WHEN p <- join p1 p2 THEN forall m, gamma p1 m \/ gamma p2 m -> gamma p m.
Proof.
    unfold join; xasimplify ltac:(intuition eauto with pedraQ).
  Qed.
  Global Hint Resolve join_correct: vpl.

  Definition widen (p1 p2: t): imp t :=
    match p1, p2 with
      | None, None => pure None
      | None, p | p, None => pure p
      | Some pol1, Some pol2 =>
        BIND widen <- Backend.widen (ml pol1, ml pol2) -;
        let (cs, shadow) := widen in
          pure (Some (mk shadow cs))
    end.

  Definition project (p: t) (x: PVar.t): imp t
    := SOME p1 <- p -;
       BIND project <- Backend.project (ml p1, x) -;
       pure (
         let (p2, c) := project in
         let cs:= Cs.approx (cons p1) c in
           if Cs.isFree x cs then
             Some (mk cs p2)
           else
             failwith ("PedraQ.project: "++(PVar.pr x)++" not free in "++(Cs.pr cs)) top).

  Lemma project_correct a x: WHEN p <- project a x THEN forall m v, gamma a m -> gamma p (Mem.assign x v m).
Proof.
    unfold project; xasimplify ltac:(eauto with pedraQ).
    intros; erewrite (mdoExt_free Cs.sat_mdo); eauto with pedraQ progvar.
  Qed.
  Global Hint Resolve project_correct: vpl.

End BasicD.

Module ItvD.

  Import BasicD.

  Definition buildLow (p: polT) (v: LinQ.t) (b: Backend.bndT): QItv.bndT :=
      match b with
        | Backend.Infty => QItv.Infty
        | Backend.Open n f =>
          let c:=Cs.combine (cons p) f in
            if Cstr.isIncl c (Cstr.lowerToCstr v n) then QItv.Open n else QItv.Infty
        | Backend.Closed n f =>
          let c:=Cs.combine (cons p) f in
            if Cstr.isIncl c (Cstr.lowerOrEqualsToCstr v n) then QItv.Closed n else QItv.Infty
      end.

  Lemma buildLow_correct (p: polT) (v: LinQ.t) (b: Backend.bndT) m:
    gamma (Some p) m -> QItv.satLower (buildLow p v b) (LinQ.eval v m).
Proof.
    unfold buildLow; destruct b; simpl; auto; PedraQsimplify.
  Qed.

  Definition buildUp (p: polT) (v: LinQ.t) (b: Backend.bndT): QItv.bndT :=
      match b with
        | Backend.Infty => QItv.Infty
        | Backend.Open n f =>
          let c:=Cs.combine (cons p) f in
            if Cstr.isIncl c (Cstr.upperToCstr v n) then QItv.Open n else QItv.Infty
        | Backend.Closed n f =>
          let c:=Cs.combine (cons p) f in
            if Cstr.isIncl c (Cstr.upperOrEqualsToCstr v n) then QItv.Closed n else QItv.Infty
      end.

  Lemma buildUp_correct (p: polT) (v: LinQ.t) (b: Backend.bndT) m:
    gamma (Some p) m -> QItv.satUpper (buildUp p v b) (LinQ.eval v m).
Proof.
    unfold buildUp; destruct b; simpl; auto; PedraQsimplify.
  Qed.

wrapping "mk" function of QItv
  Definition QItv_mk (l u: QItv.bndT): QItv.t
   := projT1 (QItv.mk l u).

  Lemma QItv_mk_correct l u x: QItv.satLower l x -> QItv.satUpper u x -> QItv.sat (QItv_mk l u) x.
Proof.
    unfold QItv_mk. destruct (QItv.mk l u); simpl; auto.
  Qed.

  Definition getItv (p: t) (v: LinQ.t): imp QItv.t :=
    match p with
    | None => pure QItv.Bot
    | Some pol =>
      BIND sItv <- Backend.getItv (ml pol, v) -;
      let low := buildLow pol v (Backend.low sItv) in
      let up := buildUp pol v (Backend.up sItv) in
          pure (QItv_mk low up)
    end.

  Local Hint Resolve buildUp_correct buildLow_correct QItv_mk_correct: pedraQ.

  Lemma getItv_correct (p: t) (v: LinQ.t):
    WHEN i <- getItv p v THEN forall m, gamma p m -> QItv.sat i (LinQ.eval v m).
Proof.
    unfold getItv; xasimplify ltac: (eauto with pedraQ).
  Qed.
  Global Hint Resolve getItv_correct: pedraQ.

  Definition getLowerBound : t -> LinQ.t -> imp QItv.bndT
    := fun p v =>
         match p with
           | None => failwith "PedraQ.ItvD.getLowerBound" (pure QItv.Infty)
           | Some pol =>
             BIND b <- Backend.getLowerBound (ml pol, v) -;
                  pure (buildLow pol v b)
         end.

  Lemma getLowerBound_correct (p : t) (v : LinQ.t) :
    WHEN b <- getLowerBound p v THEN forall m, gamma p m -> QItv.satLower b (LinQ.eval v m).
Proof.
    unfold getLowerBound; xasimplify ltac: (eauto with pedraQ).
  Qed.

  Definition getUpperBound : t -> LinQ.t -> imp QItv.bndT
    := fun p v =>
         match p with
           | None => failwith "PedraQ.ItvD.getUpperBound" (pure QItv.Infty)
           | Some pol =>
             BIND b <- Backend.getUpperBound (ml pol, v) -;
                  pure (buildUp pol v b)
         end.

  Lemma getUpperBound_correct (p : t) (v : LinQ.t) :
    WHEN b <- getUpperBound p v THEN forall m, gamma p m -> QItv.satUpper b (LinQ.eval v m).
Proof.
    unfold getUpperBound; xasimplify ltac: (eauto with pedraQ).
  Qed.
  Hint Resolve getUpperBound_correct getLowerBound_correct: pedraQ.

  Definition getItvMode mo (v: LinQ.t) (p:t): imp QItv.t :=
    match mo with
    | BOTH => getItv p v
    | UP => BIND b <- getUpperBound p v -;
            pure (QItv_mk QItv.Infty b)
    | LOW => BIND b <- getLowerBound p v -;
            pure (QItv_mk b QItv.Infty)
    end.
  Extraction Inline getItvMode.

  Lemma getItvMode_correct mo v p:
    WHEN i <- (getItvMode mo v p) THEN
      forall m, gamma p m -> QItv.sat i (LinQ.eval v m).
Proof.
    unfold getItvMode; destruct mo; xasimplify ltac: (eauto with pedraQ).
    simpl in * |- *; intros; eapply QItv_mk_correct; simpl; eauto.
  Qed.
  Hint Resolve getItvMode_correct: vpl.

End ItvD.


Module CstrD <: HasConcreteConditions QNum Cstr BasicD.

  Import BasicD.

  Definition assume (c: Cstr.t) (p: t): imp t :=
    SOME p1 <- p -;
    BIND cid <- Backend.freshId (ml p1) -;
    BIND aux <- Backend.add (ml p1, c) -;
    pure (let (opt, cert) := aux in
      match opt with
        | None =>
          if (Cs.chkEmpty (Cs.add (cons p1) cid c) cert) then
            None
          else
            failwith "CstrD.assume" top
        | Some s => Some (mk (Cs.redAdd (cons p1) cid c cert) s)
      end).
  
  Lemma assume_correct: forall c a, WHEN p <- assume c a THEN forall m, Cstr.sat c m -> gamma a m -> gamma p m.
Proof.
    unfold assume; xasimplify ltac:(unfold not; eauto with pedraQ).
  Qed.

fromCstr c builds a polyhedron from a constraint. If it fails, default is returned. Hence default may be chosen according to the fact that precision or soundness is required
  Definition fromCstr: Cstr.t -> t -> imp t
    := fun c default =>
         BIND cid <- Backend.freshId Backend.top -;
         BIND res <- Backend.addp (Backend.top,c) -;
         pure match res with
           | Backend.Added p (fwd, bwd) =>
             match Cs.addp Cs.top cid c fwd bwd with
               | Some cs => Some (mk cs p)
               | None => failwith "CstrD.fromCstr" default
             end
           | Backend.Contrad ce =>
             if Cs.chkEmpty (Cs.add Cs.top cid c) ce
             then None
             else failwith "CstrD.fromCstr" default
         end.

Currently useless ?? TODO: adapt with default Lemma fromCstr_correct: forall c p, fromCstr c = Some p -> forall m, Cstr.sat c m -> gamma p m. Proof. intros c p hr m hc. unfold fromCstr in hr. destruct (Backend.addp Backend.top c) as p' [fwd bwd]|ce. - assert (pf := fun cs' => Cs.addp_correct Cs.top cs' (Backend.getId Backend.top) c fwd bwd m). destruct (Cs.addp Cs.top (Backend.getId Backend.top) c fwd bwd) as cs|. + inversion hr. apply pf; reflexivity|constructor|assumption. + discriminate hr. - assert (pf := Cs.chkEmpty_correct (Cs.add Cs.top (Backend.getId Backend.top) c) ce). destruct (Cs.chkEmpty (Cs.add Cs.top (Backend.getId Backend.top) c) ce). + inversion hr. contradiction pf with (m := m). apply Cs.Add_correct; constructor|assumption. + discriminate hr. Qed.
  Local Hint Resolve Cs.addp_precise_c: pedraQ.

  Lemma fromCstr_precise c: WHEN p <- fromCstr c None THEN forall m, gamma p m -> Cstr.sat c m.
Proof.
    unfold fromCstr; unfoldDebug; xtsimplify ltac:idtac; intros m.
    destruct exta0 as [p' [fwd bwd]|ce].
    - apply try_catch_decomp.
      PedraQsimplify.
    - apply if_decomp.
      PedraQsimplify.
  Qed.

Test whether a polyhedron is included in a given half space.
  Definition assert (c: Cstr.t) (p: t): imp bool :=
    BIND p' <- fromCstr c None -;
    isIncl p p'.

  Local Opaque fromCstr.
  Local Hint Resolve fromCstr_precise isIncl_correct: pedraQ.

  Lemma assert_correct: forall c a, If assert c a THEN forall m, gamma a m -> Cstr.sat c m.
Proof.
    intros c a.
    unfold assert.
    xasimplify ltac: (eauto with pedraQ).
  Qed.
  Global Opaque assert assume.
  Global Hint Resolve assert_correct assume_correct: vpl.

End CstrD.


Module Rename <: HasRename QNum BasicD.

  Import BasicD.

  Definition rename (x y: PVar.t) (a:t) : imp t :=
  SOME p <- a -;
  BIND aux <- Backend.rename (x,y,ml p) -;
  pure (Some {| cons := Cs.rename x y (cons p) ; ml := aux |}).

  Lemma rename_correct: forall x y a, WHEN p <- (rename x y a) THEN
    forall m, gamma a (Mem.assign x (m y) m) -> gamma p m.
Proof.
    unfold Basics.impl, rename.
    intros; xasimplify ltac:idtac.
    intros; rewrite Cs.rename_correct.
    auto.
  Qed.
  Global Hint Resolve rename_correct: vpl.

End Rename.


Generated by coq2html