Fix IEEE connection and AA validators

coq/CertificateChecker.v

@@ -57,24 +57,22 @@ Proof.
     intros. cbn in *; congruence. }
   rewrite <- andb_lazy_alt in certificate_valid.
   andb_to_prop certificate_valid.
-  clear R1.
   pose proof (NatSetProps.empty_union_2 (Expressions.usedVars e) NatSet.empty_spec) as union_empty.
   hnf in union_empty.
   assert (dVars_range_valid NatSet.empty E1 absenv).
   { unfold dVars_range_valid.
     intros; set_tac. }
-  (* assert (affine_dVars_range_valid NatSet.empty E1 absenv 1 (FloverMap.empty _) (fun _ => None))
+  assert (affine_dVars_range_valid NatSet.empty E1 absenv 1 (FloverMap.empty _) (fun _ => None))
     as affine_dvars_valid.
   { unfold affine_dVars_range_valid.
-    intros; set_tac. } *)
+    intros; set_tac. }
   assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
   { hnf; intros a in_empty.
     set_tac. }
   rename R0 into validFPRanges.
   assert (validRanges e absenv E1 (toRTMap (toRExpMap Gamma))) as valid_e.
   { eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (E:=E1));
-      auto.
-    unfold RangeValidator. rewrite L; auto. }
+      auto. }
   pose proof (validRanges_single _ _ _ _ valid_e) as valid_single;
     destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
   destruct iv_e as [elo ehi].
@@ -145,10 +143,9 @@ Proof.
     as freeVars_contained by set_tac.
   assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f.
   { eapply RangeValidatorCmd_sound; eauto.
-    unfold RangeValidatorCmd. rewrite L0. auto. }
-  (*
+    unfold RangeValidatorCmd.
     unfold affine_dVars_range_valid; intros.
-    set_tac. } *)
+    set_tac. }
   pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
   destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
   destruct iv as [f_lo f_hi].

coq/Commands.v

@@ -116,3 +116,16 @@ Proof.
     econstructor; try eauto.
     eapply swap_Gamma_eval_expr; eauto.
 Qed.
+
+Lemma bstep_Gamma_det f:
+  forall E1 E2 Gamma v1 v2 m1 m2,
+  bstep f E1 Gamma v1 m1 ->
+  bstep 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; eauto.
+Qed.
\ No newline at end of file

coq/ErrorValidationAA.v

@@ -12,7 +12,7 @@ From Coq
 
 From Flover
      Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
-     Infra.RealSimps Infra.Ltacs Environments IntervalValidation Typing
+     Infra.RealSimps Infra.Ltacs Environments IntervalValidation TypeValidator
      RealRangeValidator ErrorBounds AffineForm AffineArith AffineArithQ.
 
 (** Error bound validator **)
@@ -232,7 +232,6 @@ Fixpoint validErrorboundAACmd (f:cmd Q) (* analyzed cmd with let's *)
 (*     (Rabs (vR - vF) <= (Q2R mAbs))%R. *)
 
 
-
 (* Theorem validErrorboundAA_sound e: *)
 (*   forall E1 E2 P Gamma defVars nR A elo ehi tMap fVars dVars currNoise maxNoise initMap resMap M1, *)
 (*     (forall e vR, *)

coq/ExpressionSemantics.v

@@ -169,9 +169,9 @@ Qed.
 
 Hint Resolve Fma_dist'.
 
-Lemma Gamma_det e E Gamma v1 v2 m1 m2:
-  eval_expr E Gamma e v1 m1 ->
-  eval_expr E Gamma e v2 m2 ->
+Lemma Gamma_det e E1 E2 Gamma v1 v2 m1 m2:
+  eval_expr E1 Gamma e v1 m1 ->
+  eval_expr E2 Gamma e v2 m2 ->
   m1 = m2.
 Proof.
   induction e; intros * eval_e1 eval_e2;
@@ -352,8 +352,8 @@ Lemma eval_expr_ignore_bind e:
   forall x v m Gamma E,
     eval_expr E Gamma e v m ->
     ~ NatSet.In x (usedVars e) ->
-    forall m_new v_new,
-    eval_expr (updEnv x v_new E) (updDefVars (Var R x) m_new Gamma) e v m.
+    forall v_new,
+    eval_expr (updEnv x v_new E) Gamma e v m.
 Proof.
   induction e; intros * eval_e no_usedVar *; cbn in *;
     inversion eval_e; subst; try eauto.
@@ -365,7 +365,6 @@ Proof.
       cbn.
       apply beq_nat_false in H.
       destruct (n ?= x)%nat eqn:?; try auto.
-      apply Nat.compare_eq in Heqc; subst; congruence.
     + unfold updEnv.
       rewrite H; auto.
   - eapply Binop_dist'; eauto;

coq/RealRangeArith.v

@@ -293,7 +293,7 @@ Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma vR' m n c fV
   NatSet.Subset (usedVars e) (fVars ∪ dVars) ->
   ~ (n ∈ fVars ∪ dVars) ->
   validRanges e A E Gamma ->
-  validRanges e A (updEnv n vR' E) (updDefVars (Var R n) REAL Gamma).
+  validRanges e A (updEnv n vR' E) Gamma.
   (*(updDefVars (Var R n) REAL Gamma). *)
 Proof.
   intros Hssa Hsub Hnotin Hranges.

coq/RealRangeValidator.v

@@ -5,28 +5,26 @@ From Flover
      Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
      Infra.Ltacs AffineForm TypeValidator.
 
-(*Flover.AffineValidation*)
 From Coq Require Export QArith.QArith.
 
 From Flover
-     Require Export IntervalValidation RealRangeArith Infra.ExpressionAbbrevs Commands.
+     Require Export IntervalValidation AffineValidation RealRangeArith
+     Infra.ExpressionAbbrevs Commands.
 
 Definition RangeValidator e A P dVars:=
   if
     validIntervalbounds e A P dVars
   then true
-  else false
-         (*
   else match validAffineBounds e A P dVars (FloverMap.empty (affine_form Q)) 1 with
        | Some _ => true
        | None => false
-       end.*).
+       end.
 
 Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : precond) dVars
         (E : env) (Gamma : FloverMap.t mType):
   RangeValidator e A P dVars = true ->
   dVars_range_valid dVars E A ->
- (* affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) -> *)
+  affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
   validTypes e Gamma ->
   fVars_P_sound (usedVars e) E P ->
   validRanges e A E (toRTMap (toRExpMap Gamma)).
@@ -36,9 +34,6 @@ Proof.
   destruct (validIntervalbounds e A P dVars) eqn: Hivcheck.
   - eapply validIntervalbounds_sound; eauto.
     unfold dVars_range_valid; intros; set_tac.
-  - congruence.
-Qed.
-(*
   - pose (iexpmap := (FloverMap.empty (affine_form Q))).
     pose (inoise := 1%nat).
     epose (imap := (fun _ : nat => None)).
@@ -50,41 +45,35 @@ Qed.
     pose proof (validAffineBounds_sound) as sound_affine.
     assert ((forall e' : FloverMap.key,
                 (exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e' iexpmap = Some af) ->
-                checked_expressions A E Gamma fBits (usedVars e) dVars e' iexpmap inoise imap)) as Hchecked
+                checked_expressions A E Gamma (usedVars e) dVars e' iexpmap inoise imap)) as Hchecked
         by (intros e' Hein; destruct Hein as [af Hein]; unfold iexpmap in Hein;
             rewrite FloverMapFacts.P.F.empty_o in Hein;
             congruence).
     assert (1 > 0)%nat as Hinoise by omega.
     eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
     assert (NatSet.Subset (usedVars e -- dVars) (usedVars e)) as Hsubset by set_tac.
-    assert (fVars_P_sound (usedVars e) E P) as HfVars by exact H2.
-    assert (vars_typed (usedVars e ∪ dVars) Gamma) as Hvarstyped
-        by exact H3.
-    specialize (sound_affine e A P (usedVars e) dVars E Gamma fBits
+    assert (fVars_P_sound (usedVars e) E P) as HfVars by exact H3.
+    specialize (sound_affine e A P (usedVars e) dVars E Gamma
                              exprAfs noise iexpmap inoise imap
-                             Hchecked Hinoise Himap Hafcheck H1 Hsubset HfVars Hvarstyped)
-      as [map2 [af [vR [aiv [aerr sound_affine]]]]].
-    intuition.
+                             Hchecked Hinoise Himap Hafcheck H1 Hsubset HfVars)
+      as [map2 [af [vR [aiv [aerr sound_affine]]]]]; intuition.
 Qed.
- *)
 
 Definition RangeValidatorCmd e A P dVars:=
   if
     validIntervalboundsCmd e A P dVars
   then true
-  else false
-         (*
   else match validAffineBoundsCmd e A P dVars (FloverMap.empty (affine_form Q)) 1 with
        | Some _ => true
        | None => false
-       end*).
+       end.
 
 Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond) dVars
         (E : env) Gamma fVars outVars:
   RangeValidatorCmd f A P dVars = true ->
   ssa f (NatSet.union fVars dVars) outVars ->
   dVars_range_valid dVars E A ->
-  (*affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->*)
+  affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
   fVars_P_sound fVars E P ->
   NatSet.Subset (freeVars f -- dVars) fVars ->
   validTypesCmd f Gamma ->
@@ -94,9 +83,6 @@ Proof.
   unfold RangeValidatorCmd in ranges_valid.
   destruct (validIntervalboundsCmd f A P dVars) eqn:iv_valid.
   - eapply validIntervalboundsCmd_sound; eauto.
-  - congruence.
-Qed.
-(*
   - pose (iexpmap := (FloverMap.empty (affine_form Q))).
     pose (inoise := 1%nat).
     epose (imap := (fun _ : nat => None)).
@@ -107,19 +93,15 @@ Qed.
     pose proof (validAffineBoundsCmd_sound) as sound_affine.
     assert ((forall e' : FloverMap.key,
                 (exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e' iexpmap = Some af) ->
-                checked_expressions A E Gamma fBits fVars dVars e' iexpmap inoise imap)) as Hchecked
+                checked_expressions A E Gamma fVars dVars e' iexpmap inoise imap)) as Hchecked
         by (intros e' Hein; destruct Hein as [af Hein]; unfold iexpmap in Hein;
             rewrite FloverMapFacts.P.F.empty_o in Hein;
             congruence).
     assert (1 > 0)%nat as Hinoise by omega.
     eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
     assert (fVars_P_sound fVars E P) as HfVars by exact H2.
-    assert (vars_typed (fVars ∪ dVars) Gamma) as Hvarstyped
-        by exact H3.
-    specialize (sound_affine f A P fBits fVars dVars outVars E Gamma
+    specialize (sound_affine f A P fVars dVars outVars E Gamma
                              exprAfs noise iexpmap inoise imap
-                             Hchecked Hinoise Himap Hafcheck H H1 H4 HfVars Hvarstyped)
-      as [map2 [af [vR [aiv [aerr sound_affine]]]]].
-    intuition.
-Qed.
-*)
\ No newline at end of file
+                             Hchecked Hinoise Himap Hafcheck H H1 H3 HfVars)
+      as [map2 [af [vR [aiv [aerr sound_affine]]]]]; intuition.
+Qed.
\ No newline at end of file

coq/TypeValidator.v

@@ -80,23 +80,39 @@ Qed.
 Ltac validTypes_split :=
   match goal with
   | [ H: validTypes (Const ?m ?v) ?Gamma |- _] => idtac
-  | [ H: validTypes (Var ?x) ?Gamma |- _] => idtac
+  | [ H: validTypes (Var ?t ?x) ?Gamma |- _] => idtac
   | [ H: validTypes (Unop ?u ?e) ?Gamma |- _] =>
-    assert (validTypes e Gamma) by (destruct H as [? [? [[? ?] ?]]]; eauto)
+    let n := fresh "valid_arg" in
+    assert (validTypes e Gamma)
+      as n
+        by (destruct H as [? [? [[? ?] ?]]]; eauto)
   | [ H: validTypes (Binop ?b ?e1 ?e2) ?Gamma |- _] =>
+    let n1 := fresh "valid_arg" in
+    let n2 := fresh "valid_arg" in
     assert (validTypes e1 Gamma)
-      by (destruct H as [? [? [[? [? ?]] ?]]]; auto);
+      as n1
+        by (destruct H as [? [? [[? [? ?]] ?]]]; auto);
     assert (validTypes e2 Gamma)
-      by (destruct H as [? [? [[? [? ?]] ?]]]; auto)
+      as n2
+        by (destruct H as [? [? [[? [? ?]] ?]]]; auto)
   | [ H: validTypes (Fma ?e1 ?e2 ?e3) ?Gamma |- _] =>
+    let n1 := fresh "valid_arg" in
+    let n2 := fresh "valid_arg" in
+    let n3 := fresh "valid_arg" in
     assert (validTypes e1 Gamma)
-      by (destruct H as [? [? [[? [? [? ?]]] ?]]]; auto);
+      as n1
+        by (destruct H as [? [? [[? [? [? ?]]] ?]]]; auto);
     assert (validTypes e2 Gamma)
-      by (destruct H as [? [? [[? [? [? ?]]] ?]]]; auto);
+      as n2
+        by (destruct H as [? [? [[? [? [? ?]]] ?]]]; auto);
     assert (validTypes e3 Gamma)
-      by (destruct H as [? [? [[? [? [? ?]]] ?]]]; auto)
+      as n3
+        by (destruct H as [? [? [[? [? [? ?]]] ?]]]; auto)
   | [ H: validTypes (Downcast ?m ?e) ?Gamma |- _] =>
-    assert (validTypes e ?Gamma) by (destruct H as [? [? [[? ?] ?]]]; eauto)
+    let n := fresh "valid_arg" in
+    assert (validTypes e Gamma)
+      as n
+        by (destruct H as [? [? [[? ?] ?]]]; eauto)
   end.
 
 Ltac validTypes_simp :=

coq/floverParser.v

@@ -12,7 +12,6 @@ Inductive Token:Type :=
 | DABS
 | DCOND
 | DGAMMA
-| DFBITS
 | DTYPE:mType -> Token
 | DFIXED
 | DVAR
@@ -96,7 +95,6 @@ match fuel with
                  | "Let" => DLET :: lex input'' fuel'
                  | "PRE" => DPRE :: lex input'' fuel'
                  | "ABS" => DABS :: lex input'' fuel'
-                 | "FBITS" => DFBITS :: lex input'' fuel'
                  | "GAMMA" => DGAMMA :: lex input'' fuel'
                  | "Var" => DVAR :: lex input'' fuel'
                  | "Cast" => DCAST :: lex input'' fuel'
@@ -161,7 +159,6 @@ Definition pp_token (token:Token) :=
   | DABS => "ABS"
   | DCOND => "?"
   | DVAR => "Var"
-  | DFBITS => "FBITS"
   | DCONST num => str_of_num num (N.to_nat num)
   | DGAMMA => "Gamma"
   | DTYPE m => str_join "MTYPE " (type_to_string m)
@@ -388,51 +385,32 @@ Definition parseAbsEnv (input:list Token) fuel :=
   | _ => None
   end.
 
-Definition defaultGamma := fun n:nat => None:option mType.
+Definition defaultGamma := FloverMap.empty mType.
 
-Fixpoint parseGammaRec (input: list Token) : option ((nat -> option mType) * list Token) :=
-  match input with
-  | DVAR :: DCONST n :: DTYPE m :: inputRest =>
-    match parseGammaRec inputRest with
-    | Some (Gamma, rest) => Some (updDefVars (N.to_nat n) m Gamma, rest)
-    | None => None
+Fixpoint parseGammaRec (input: list Token) (fuel:nat): option ((FloverMap.t mType) * list Token) :=
+  match fuel with
+  |0%nat => None
+  |S fuel' =>
+   match parseExp input fuel with
+   |None => Some (defaultGamma, input)
+   | Some (e, rest) =>
+     match rest with
+     |DTYPE m :: inputRest =>
+      match parseGammaRec inputRest fuel' with
+      |Some (Gamma, rest) => Some (FloverMap.add e m Gamma, rest)
+      |None => None
+      end
+     | _ => None
      end
-  | _  => Some (defaultGamma, input)
+   end
   end.
 
 Definition parseGamma (input:list Token) :=
   match input with
-  | DGAMMA :: tokenRest => parseGammaRec tokenRest
+  | DGAMMA :: tokenRest => parseGammaRec tokenRest (length tokenRest)
   | _ => None
   end.
 
-Definition defaultFBits := FloverMap.empty N.
-
-Fixpoint parseFBitsRec (input: list Token) akk (fuel:nat)
-: option (FloverMap.t N * list Token) :=
-  match fuel with
-  | 0%nat => None
-  | S fuel' =>
-    match input with
-    |[] => Some (akk, [])
-    | _ =>
-      match parseExp input fuel with
-      | None => Some (akk, input)
-      | Some (e, res1) =>
-        match res1 with
-        |DCONST n :: res2 => parseFBitsRec res2 (FloverMap.add e n akk) fuel'
-        | _ => Some (akk, input)
-        end
-      end
-    end
-  end.
-
-Definition parseFBits input fuel :=
-  match input with
-  |DFBITS :: tokRest => parseFBitsRec tokRest defaultFBits fuel
-  |_ => None
-  end.
-
 Definition dParse  (input:list Token) fuel :=
   let cmdParse :=
       match input with
@@ -452,11 +430,7 @@ Definition dParse  (input:list Token) fuel :=
       | Some (P, absenvRest) =>
         match parseAbsEnv absenvRest fuel with
         | None => None
-        | Some (A, residual) =>
-          match parseFBits residual fuel with
-          |None => None
-          |Some (fBits, residual) => Some ((dCmd, P, A, Gamma, fBits), residual)
-          end
+        | Some (A, residual) => Some ((dCmd, P, A, Gamma), residual)
         end
       end
     end
@@ -468,9 +442,9 @@ Fixpoint str_length s :=
   |"" => O
   end.
 
-Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) Gamma fBits (n:nat) :=
+Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) Gamma (n:nat) :=
   match n with
-  |S n' => CertificateCheckerCmd f A P Gamma fBits && (check f P A Gamma fBits n')
+  |S n' => CertificateCheckerCmd f A P Gamma && (check f P A Gamma n')
   |_ => true
   end.
 
@@ -478,8 +452,8 @@ Fixpoint check_all (num_fun:nat) (iters:nat) (input:list Token) fuel:=
   match num_fun with
   |S nf =>
    match (dParse input fuel) with
-   |Some ((f,P,A, Gamma, fBits), residual) =>
-    if (check f P A Gamma fBits iters)
+   |Some ((f,P,A, Gamma), residual) =>
+    if (check f P A Gamma iters)
     then
       match residual with
       |a :: b => check_all nf iters residual fuel

coq/ssaPrgs.v

@@ -215,7 +215,7 @@ Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma vR vR' m n c fVa
   NatSet.Subset (usedVars e) (fVars ∪ dVars) ->
   ~ (n ∈ fVars ∪ dVars) ->
   eval_expr E Gamma e vR REAL ->
-  eval_expr (updEnv n vR' E) (updDefVars (Var R n) REAL Gamma) e vR REAL.
+  eval_expr (updEnv n vR' E) Gamma e vR REAL.
 Proof.
   intros Hssa Hsub Hnotin Heval.
   eapply eval_expr_ignore_bind; [auto |].