Merge remote-tracking branch 'upstream/master'

coq/ErrorAnalysis.v

@@ -44,11 +44,16 @@ Qed.
 
 Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
   match c with
-  | Let m x e k => validErrorBounds e E1 E2 A Gamma DeltaMap /\
-                  (forall v__R v__FP,
-                      eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
-                      eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m ->
-                      validErrorBoundsCmd k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap)
+  | Let m x e k =>
+    validErrorBounds e E1 E2 A Gamma DeltaMap /\
+    (exists iv_e err_e iv_x err_x,
+       FloverMap.find e A = Some (iv_e, err_e) /\
+       FloverMap.find (Var Q x) A = Some (iv_x, err_x) /\
+       Qeq_bool err_e err_x = true) /\
+    (forall v__R v__FP,
+        eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
+        eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m ->
+        validErrorBoundsCmd k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap)
   | Ret e => validErrorBounds e E1 E2 A Gamma DeltaMap
   end  /\
   forall v__R (iv: intv) (err: error),

coq/ErrorValidation.v

@@ -2070,7 +2070,7 @@ Proof.
       eapply IHe1'; eauto.
       - specialize typing_ok as (? & ?).
         intuition.
-      - set_tac. split; set_tac.  
+      - set_tac. split; set_tac.
       - cbn in *; Flover_compute; try congruence; type_conv; subst;
           destruct b; Flover_compute; try congruence.
       - cbn in valid_intv.
@@ -2082,7 +2082,7 @@ Proof.
       eapply IHe2'; eauto.
       - specialize typing_ok as (? & ?).
         intuition.
-      - set_tac. split; set_tac.  
+      - set_tac. split; set_tac.
       - cbn in *; Flover_compute; try congruence; type_conv; subst;
           destruct b; Flover_compute; try congruence.
       - cbn in valid_intv.
@@ -2175,7 +2175,7 @@ Proof.
       eapply IHe1'; eauto.
       - specialize typing_ok as (? & ?).
         intuition.
-      - set_tac. split; set_tac.  
+      - set_tac. split; set_tac.
       - cbn in *; Flover_compute; try congruence; type_conv; subst;
           destruct b; Flover_compute; try congruence.
       - cbn in valid_intv.
@@ -2186,7 +2186,7 @@ Proof.
       eapply IHe2'; eauto.
       - specialize typing_ok as (? & ?).
         intuition.
-      - set_tac. split; set_tac.  
+      - set_tac. split; set_tac.
       - cbn in *; Flover_compute; try congruence; type_conv; subst;
           destruct b; Flover_compute; try congruence.
       - cbn in valid_intv.
@@ -2197,7 +2197,7 @@ Proof.
       eapply IHe3'; eauto.
       - specialize typing_ok as (? & ?).
         intuition.
-      - set_tac. split; set_tac.  
+      - set_tac. split; set_tac.
       - cbn in *; Flover_compute; try congruence; type_conv; subst;
           destruct b; Flover_compute; try congruence.
       - cbn in valid_intv.
@@ -2445,8 +2445,9 @@ Proof.
         by (eapply validErrorbound_sound; eauto).
     split.
     {
-      split.
+      repeat split.
       - eapply validErrorbound_sound; eauto.
+      - repeat eexists. eauto.
       - intros vR vF eval_real eval_float.
         eapply validErrorBounds_single in Hsound; eauto.
         destruct Hsound as [[vFe [mFe eval_float_e]] bounded_e].

coq/FPRangeValidator.v

@@ -166,10 +166,7 @@ Proof.
   induction f; intros;
     simpl in *;
     (match_pat (bstep _ _ (toRTMap _) _ _ _) (fun H => inversion H; subst; simpl in * ));
-     (match_pat (bstep _ _ (toRExpMap Gamma) _ _ _) (fun H => inversion H; subst; simpl in * ));
-      repeat match goal with
-             | H : _ = true |- _ => andb_to_prop H
-             end.
+     (match_pat (bstep _ _ (toRExpMap Gamma) _ _ _) (fun H => inversion H; subst; simpl in * )).
   - destruct H4
       as [[me [find_me [find_var [? [validt_e validt_f]]]]] valid_exec].
     assert (m = me) by (eapply validTypes_exec in find_me; eauto); subst.
@@ -198,9 +195,11 @@ Proof.
       apply (IHf (updEnv n vR_e E1) (updEnv n v1 E2)
                  Gamma DeltaMap v vR m0 A fVars
                  (NatSet.add n dVars) (outVars)); eauto.
-      * eapply approxUpdBound; eauto; simpl in *.
+    * destruct validerr_rec as [[iv_e2 [err_e2 [iv_x [err_x [find_e [find_x eqfind]]]]]] validerr_rec].
+      rewrite find_e in *; canonize_hyps. inversion map_e; subst.
+      eapply approxUpdBound; eauto; simpl in *.
         { eapply toRExpMap_some; eauto. simpl; auto. }
-        { admit. }
+        { rewrite <- eqfind. eapply err_bounded_e. eauto. }
       * eapply ssa_equal_set; eauto.
         hnf. intros a; split; intros in_set.
         { rewrite NatSet.add_spec, NatSet.union_spec;
@@ -216,6 +215,7 @@ Proof.
             { intros x; unfold toRMap, updDefVars.
               destruct (x =? n) eqn:?; auto. }
             { eapply valid_rec. auto. } *)
+      * destruct validerr_rec; auto.
       * set_tac; split.
         { split; try auto.
           hnf; intros; subst.
@@ -244,4 +244,4 @@ Proof.
           rewrite NatSet.add_spec in H5; destruct H5;
             auto; subst; congruence. }
   - destruct H5. destruct H4. destruct H6. eapply FPRangeValidator_sound; eauto.
-Admitted.
+Qed.

coq/IEEE_connection.v

@@ -885,8 +885,8 @@ Proof.
     assert (exists iv err, FloverMap.find (B2Qexpr e) A = Some (iv, err)) as Hcert.
     {
       intuition.
-      eapply validRanges_single in H10.
-      destruct H10 as (? & ? & ? & ? & ?); eauto.
+      eapply validRanges_single in H12.
+      destruct H12 as (? & ? & ? & ? & ?); eauto.
     }
     specialize Hcert as (? & ? & Hcert).
     pose proof valid_error as valid_error'.
@@ -913,9 +913,11 @@ Proof.
                   vR vF_new A fVars (NatSet.add n dVars) outVars); try eauto.
     + intros. unfold toREnv, updFlEnv, updEnv.
       destruct (x1 =? n); auto. rewrite <- envs_eq. unfold toREnv; auto.
-    + eapply approxUpdBound; eauto.
+    + destruct valid_error_cmd as [[? [? [? [? [? [? ?]]]]]] ?].
+      eapply approxUpdBound; eauto.
       * eapply toRExpMap_some with (e:=Var Q n); eauto.
-      * admit.
+      * canonize_hyps. rewrite Hcert in *. inversion H1; subst.
+        lra.
     + eapply ssa_equal_set; eauto.
       hnf; split; intros.
       * rewrite NatSet.add_spec, NatSet.union_spec in *.

hol4/.HOLCOMMIT

-7f7650b1f7d9fbc79f55646dabcf225b5cf0fff4
+ce7414f3a9b67a55c010a5194ca0029e347b7810

cakeml @ 9cc6eb00

-Subproject commit 401ed36dc008523f906716c7d93711c39edec3d5
+Subproject commit 9cc6eb009b0a3e368fdd31da541b59e171bbf8e4