Start error validation command proof

coq/CommandsDeterministic.v

+(**
+ Formalization of the Abstract Syntax Tree of a subset used in the Flover framework
+ **)
+Require Import Coq.Reals.Reals Coq.QArith.QArith.
+Require Export Flover.ExpressionSemanticsDeterministic Flover.Commands.
+Require Export Flover.Infra.ExpressionAbbrevs Flover.Infra.NatSet.
+
+(**
+  Define big step semantics for the Flover language, terminating on a "returned"
+  result value
+ **)
+Inductive bstep_det DeltaMap: cmd R -> env -> (expr R -> option mType) -> R -> mType -> Prop :=
+ | let_b_det m m' x e s E v res defVars:
+    eval_expr_det E defVars DeltaMap e v m ->
+    bstep_det DeltaMap s (updEnv x v E) defVars res m' ->
+    bstep_det DeltaMap (Let m x e s) E defVars res m'
+ | ret_b_det m e E v defVars:
+    eval_expr_det E defVars DeltaMap e v m ->
+    bstep_det DeltaMap (Ret e) E defVars v m.
+
+Lemma bstep_eq_env_det f DeltaMap:
+  forall E1 E2 Gamma v m,
+  (forall x, E1 x = E2 x) ->
+  bstep_det DeltaMap f E1 Gamma v m ->
+  bstep_det DeltaMap f E2 Gamma v m.
+Proof.
+  induction f; intros * eq_envs bstep_E1;
+    inversion bstep_E1; subst; simpl in *.
+  - eapply eval_eq_env_det in H7; eauto. eapply let_b_det; eauto.
+     eapply IHf. instantiate (1:=(updEnv n v0 E1)).
+     + intros; unfold updEnv.
+       destruct (x=? n); auto.
+     + auto.
+  - apply ret_b_det. eapply eval_eq_env_det; eauto.
+Qed.
+
+Lemma swap_Gamma_bstep_det f DeltaMap E vR m Gamma1 Gamma2 :
+  (forall n, Gamma1 n = Gamma2 n) ->
+  bstep_det DeltaMap f E Gamma1 vR m ->
+  bstep_det DeltaMap f E Gamma2 vR m.
+Proof.
+  revert E Gamma1 Gamma2;
+  induction f; intros * Gamma_eq eval_f.
+  all: inversion eval_f; subst.
+  all: econstructor; try eauto.
+  all: eapply swap_Gamma_eval_expr_det; eauto.
+Qed.
+
+Lemma bstep_Gamma_det_det f DeltaMap:
+  forall E1 E2 Gamma v1 v2 m1 m2,
+  bstep_det DeltaMap f E1 Gamma v1 m1 ->
+  bstep_det DeltaMap f E2 Gamma v2 m2 ->
+  m1 = m2.
+Proof.
+  induction f; intros * eval_f1 eval_f2;
+    inversion eval_f1; subst;
+      inversion eval_f2; subst; try auto.
+  - eapply IHf; eauto.
+  - eapply Gamma_det_det; eauto.
+Qed.
+
+Lemma bstep_det_functional f DeltaMap:
+  forall E Gamma v1 v2 m,
+  bstep_det DeltaMap f E Gamma v1 m ->
+  bstep_det DeltaMap f E Gamma v2 m ->
+  v1 = v2.
+Proof.
+  induction f; intros * eval_f1 eval_f2;
+    inversion eval_f1; subst;
+      inversion eval_f2; subst; try auto.
+  - erewrite eval_expr_det_functional with (v1 := v) (v2 := v0) in *; eauto.
+  - eapply eval_expr_det_functional; eauto.
+Qed.

coq/ErrorValidationAA.v

@@ -12,9 +12,9 @@ From Coq
 
 From Flover
      Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
-     Infra.RealSimps Infra.Ltacs Environments ExpressionSemanticsDeterministic
-     IntervalValidation TypeValidator RealRangeValidator ErrorBounds ErrorValidation
-     AffineForm AffineArithQ AffineArith.
+     Infra.RealSimps Infra.Ltacs CommandsDeterministic Environments
+     ExpressionSemanticsDeterministic IntervalValidation TypeValidator
+     RealRangeValidator ErrorBounds ErrorValidation AffineForm AffineArithQ AffineArith.
 
 Definition mkErrorPolyQ (err: Q) noise :=
   if Qeq_bool err 0 then
@@ -221,27 +221,27 @@ Fixpoint validErrorboundAA (e:expr Q) (* analyzed expression *)
     end.
 
 (** Error bound command validator **)
-Fixpoint validErrorboundAACmd (f:cmd Q) (* analyzed cmd with let's *)
-         (typeMap:FloverMap.t mType) (* derived types for e *)
-         (A:analysisResult) (* encoded result of Flover *)
-         (dVars:NatSet.t) (* let-bound variables encountered previously *)
+Fixpoint validErrorboundAACmd (f: cmd Q) (* analyzed cmd with let's *)
+         (typeMap: FloverMap.t mType) (* derived types for e *)
+         (A: analysisResult) (* encoded result of Flover *)
+         (dVars: NatSet.t) (* let-bound variables encountered previously *)
          (currNoise: nat) (* current maximal noise term *)
-         (errMap:FloverMap.t (affine_form Q)) (* previously seen affine polys *)
+         (errMap: FloverMap.t (affine_form Q)) (* previously seen affine polys *)
   : option (FloverMap.t (affine_form Q) * nat) :=
   match f with
   | Let m x e g =>
-   olet res1 := validErrorboundAA e typeMap A dVars currNoise errMap in
-   let (errMap1, maxNoise1) := res1 in
-   olet afPolye := FloverMap.find e errMap1 in
-   match FloverMap.find e A, FloverMap.find (Var Q x) A with
-   | Some (iv_e, err_e), Some (iv_x, err_x) =>
-     if Qeq_bool err_e err_x then
-       validErrorboundAACmd g typeMap A (NatSet.add x dVars) maxNoise1
-                               (FloverMap.add (Var Q x) afPolye errMap1)
-     else
-       None
-   | _,_ => None
-   end
+    olet res1 := validErrorboundAA e typeMap A dVars currNoise errMap in
+    let (errMap1, maxNoise1) := res1 in
+    olet afPolye := FloverMap.find e errMap1 in
+    match FloverMap.find e A, FloverMap.find (Var Q x) A with
+    | Some (iv_e, err_e), Some (iv_x, err_x) =>
+      if Qeq_bool err_e err_x then
+          validErrorboundAACmd g typeMap A (NatSet.add x dVars) maxNoise1
+                              (FloverMap.add (Var Q x) afPolye errMap1)
+      else
+          None
+    | _,_ => None
+    end
   | Ret e => validErrorboundAA e typeMap A dVars currNoise errMap
   end.
 
@@ -4121,3 +4121,107 @@ Proof.
   - apply validErrorboundAA_sound_fma; auto.
   - apply validErrorboundAA_sound_downcast; auto.
 Qed.
+
+Lemma validErrorboundAAcmd_sound_existential c:
+  forall E1 E2 A Gamma DeltaMap fVars dVars outVars
+    (expr_map1 expr_map2 : FloverMap.t (affine_form Q))
+    (noise_map1 : nat -> option noise_type) (noise1 noise2 : nat) (v__R : R) 
+    (iv__A : intv) (err__A : error),
+    (forall (e' : expr R) (m' : mType),
+        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
+    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
+    bstep_det (fun x m => Some 0%R) (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) v__R REAL ->
+    validRangesCmd c A E1 (toRTMap (toRExpMap Gamma)) ->
+    validErrorboundAACmd c Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) ->
+    ssa c (NatSet.union fVars dVars) outVars ->
+    NatSet.Subset (Commands.freeVars c -- dVars) fVars ->
+    validTypesCmd c Gamma ->
+    FloverMap.find (getRetExp c) A = Some (iv__A, err__A) ->
+    (0 < noise1)%nat ->
+    (forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) ->
+    affine_dVars_error_valid E1 E2 A Gamma DeltaMap dVars noise_map1 noise1 expr_map1 ->
+    (forall e' : FloverMap.key,
+        FloverMap.In (elt:=affine_form Q) e' expr_map1 ->
+        exists (v__FP' : R) (m__FP' : mType),
+          eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP') ->
+    (forall e' : FloverMap.key,
+        FloverMap.In (elt:=affine_form Q) e' expr_map1 ->
+        checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1) ->
+    ((exists (v__FP : R) (m__FP : mType),
+         bstep_det DeltaMap (toRCmd c) E2 (toRExpMap Gamma) v__FP m__FP) /\
+     (forall e' : FloverMap.key,
+         ~ FloverMap.In (elt:=affine_form Q) e' expr_map1 ->
+         FloverMap.In (elt:=affine_form Q) e' expr_map2 ->
+         exists (v__FP' : R) (m__FP' : mType),
+           eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP')).
+Proof.
+  induction c;
+    intros * Hdeltamap Henv Heval__R Hrange Hvalidbounds Hssa Hsubset Htypes Hcert Hnoise1
+                       Hnoise_map1 Hdvars Hcheckedex Hcheckedall;
+    cbn in Hvalidbounds.
+  - destruct (validErrorboundAA e Gamma A dVars noise1 expr_map1) eqn: Hvalidbounds';
+      cbn in Hvalidbounds; [|congruence].
+    destruct p as (subexpr_map, subnoise).
+    destruct (FloverMap.find e subexpr_map) eqn: Hsubfind;
+      cbn in Hvalidbounds; [|congruence].
+    destruct (FloverMap.find e A) eqn: Hsubcert;
+      cbn in Hvalidbounds; [|congruence].
+    destruct p as (subiv, suberr).
+    destruct (FloverMap.find (Var Q n) A) eqn: Hvarcert;
+      cbn in Hvalidbounds; [|congruence].
+    destruct p as (variv, varerr).
+    destruct (Qeq_bool suberr varerr) eqn: Heqerr;
+      cbn in Hvalidbounds; [|congruence].
+    admit.
+  - inversion Heval__R; subst.
+    edestruct (validErrorboundAA_sound e) as (((v__FP & m__FP & Hex) & Hcheckedex') & _); eauto;
+      [now destruct Hrange|now destruct Htypes|].
+    assert (exists (v__FP : R) (m__FP : mType),
+               bstep_det DeltaMap (toRCmd (Ret e)) E2 (toRExpMap Gamma) v__FP m__FP).
+    {
+      exists v__FP, m__FP.
+      constructor; auto.
+    }
+    split; auto.
+Admitted.
+
+Lemma validErrorboundAAcmd_sound_universal c:
+  forall E1 E2 A Gamma DeltaMap fVars dVars outVars
+    (expr_map1 expr_map2 : FloverMap.t (affine_form Q))
+    (noise_map1 : nat -> option noise_type) (noise1 noise2 : nat) (v__R : R) 
+    (iv__A : intv) (err__A : error),
+    (forall (e' : expr R) (m' : mType),
+        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
+    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
+    bstep_det (fun x m => Some 0%R) (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) v__R REAL ->
+    validRangesCmd c A E1 (toRTMap (toRExpMap Gamma)) ->
+    validErrorboundAACmd c Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) ->
+    ssa c (NatSet.union fVars dVars) outVars ->
+    NatSet.Subset (Commands.freeVars c -- dVars) fVars ->
+    validTypesCmd c Gamma ->
+    FloverMap.find (getRetExp c) A = Some (iv__A, err__A) ->
+    (0 < noise1)%nat ->
+    (forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) ->
+    affine_dVars_error_valid E1 E2 A Gamma DeltaMap dVars noise_map1 noise1 expr_map1 ->
+    (forall e' : FloverMap.key,
+        FloverMap.In (elt:=affine_form Q) e' expr_map1 ->
+        checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1) ->
+    (forall (v__FP : R) (m__FP : mType),
+        bstep_det DeltaMap (toREvalCmd (toRCmd c)) E2 (toRExpMap Gamma) v__FP m__FP ->
+        exists (af : affine_form Q) (err__af : R) (noise_map2 : noise_mapping),
+          contained_flover_map expr_map1 expr_map2 /\
+          (noise1 <= noise2)%nat /\
+          fresh noise2 (afQ2R af) /\
+          contained_map noise_map1 noise_map2 /\
+          (forall n0 : nat, (n0 >= noise2)%nat -> noise_map2 n0 = None) /\
+          FloverMap.find (elt:=affine_form Q) (getRetExp c) expr_map2 = Some af /\
+          (0 <= err__af)%R /\
+          toInterval (afQ2R af) = ((- err__af)%R, err__af) /\
+          (err__af <= Q2R err__A)%R /\
+          af_evals (afQ2R af) (v__R - v__FP) noise_map2 /\
+          (forall e' : FloverMap.key,
+              ~ FloverMap.In (elt:=affine_form Q) e' expr_map1 ->
+              FloverMap.In (elt:=affine_form Q) e' expr_map2 ->
+              checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map2 noise2 expr_map2)).
+Proof.
+Admitted.