Merge branch 'master' into 'certificates'

Finish porting proofs to new semantics

See merge request !86

.gitignore

@@ -29,6 +29,7 @@ hol4/*/*.uo
 hol4/*/.*
 hol4/heap
 hol4/output/heap
+hol4/output/certificate_*
 daisy
 rawdata/*
 .ensime*

.gitmodules

+[submodule "hol4/cakeml"]
+	branch = daisy
+	path = hol4/cakeml
+	url = https://github.com/CakeML/cakeml.git
+

coq/CertificateChecker.v

@@ -9,7 +9,7 @@ Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealR
 Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments.
 
 Require Export Coq.QArith.QArith.
-Require Export Daisy.Infra.ExpressionAbbrevs.
+Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
 
 (** Certificate checking function **)
 Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
@@ -104,4 +104,4 @@ Proof.
   - intros v v_in_empty.
     rewrite NatSet.mem_spec in v_in_empty.
     inversion v_in_empty.
-Qed.
\ No newline at end of file
+Qed.

coq/Commands.v

@@ -43,4 +43,14 @@ Fixpoint definedVars V (f:cmd V) :NatSet.t :=
   match f with
   | Let x _ g => NatSet.add x (definedVars g)
   | Ret _ => NatSet.empty
+  end.
+
+(**
+  The live variables of a command are all variables which occur on the right
+  hand side of an assignment or at a return statement
+ **)
+Fixpoint liveVars V (f:cmd V) :NatSet.t :=
+  match f with
+  | Let _ e g => NatSet.union (usedVars e) (liveVars g)
+  | Ret e => usedVars e
   end.
\ No newline at end of file

coq/ErrorBounds.v

@@ -60,21 +60,21 @@ Proof.
   rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
   unfold evalBinop in *; simpl in *.
   clear delta H2.
-  rewrite (meps_0_deterministic H4 e1_real);
+  rewrite (meps_0_deterministic H3 e1_real);
     rewrite (meps_0_deterministic H5 e2_real).
-  rewrite (meps_0_deterministic H4 e1_real) in plus_real.
+  rewrite (meps_0_deterministic H3 e1_real) in plus_real.
   rewrite (meps_0_deterministic H5 e2_real) in plus_real.
-  clear H4 H5 v1 v2.
+  clear H3 H5 H6 v1 v2.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion plus_float; subst.
   unfold perturb; simpl.
-  inversion H4; subst; inversion H5; subst.
+  inversion H3; subst; inversion H5; subst.
   unfold updEnv; simpl.
   unfold updEnv in H0,H1; simpl in *.
   symmetry in H0, H1.
   inversion H0; inversion H1; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear plus_float H4 H5 plus_real e1_real e1_float e2_real e2_float H0 H1.
+  clear plus_float H3 H5 plus_real e1_real e1_float e2_real e2_float H0 H1.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
@@ -123,21 +123,21 @@ Proof.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
   clear delta H2.
-  rewrite (meps_0_deterministic H4 e1_real);
+  rewrite (meps_0_deterministic H3 e1_real);
     rewrite (meps_0_deterministic H5 e2_real).
-  rewrite (meps_0_deterministic H4 e1_real) in sub_real.
+  rewrite (meps_0_deterministic H3 e1_real) in sub_real.
   rewrite (meps_0_deterministic H5 e2_real) in sub_real.
-  clear H4 H5 v1 v2.
+  clear H3 H5 H6 v1 v2.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion sub_float; subst.
   unfold perturb; simpl.
-  inversion H4; subst; inversion H5; subst.
+  inversion H3; subst; inversion H5; subst.
   unfold updEnv; simpl.
   symmetry in H0, H1.
   unfold updEnv in H0, H1; simpl in H0, H1.
   inversion H0; inversion H1; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear sub_float H4 H5 sub_real e1_real e1_float e2_real e2_float H0 H1.
+  clear sub_float H3 H5 sub_real e1_real e1_float e2_real e2_float H0 H1.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   repeat rewrite Rsub_eq_Ropp_Rplus.
@@ -177,20 +177,20 @@ Proof.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
   clear delta H2.
-  rewrite (meps_0_deterministic H4 e1_real);
+  rewrite (meps_0_deterministic H3 e1_real);
     rewrite (meps_0_deterministic H5 e2_real).
-  rewrite (meps_0_deterministic H4 e1_real) in mult_real.
+  rewrite (meps_0_deterministic H3 e1_real) in mult_real.
   rewrite (meps_0_deterministic H5 e2_real) in mult_real.
-  clear H4 H5 v1 v2.
+  clear H3 H5 H6 v1 v2.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion mult_float; subst.
   unfold perturb; simpl.
-  inversion H4; subst; inversion H5; subst.
+  inversion H3; subst; inversion H5; subst.
   symmetry in H0, H1;
     unfold updEnv in *; simpl in *.
   inversion H0; inversion H1; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear mult_float H4 H5 mult_real e1_real e1_float e2_real e2_float H0 H1.
+  clear mult_float H3 H5 mult_real e1_real e1_float e2_real e2_float H0 H1.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
@@ -224,20 +224,20 @@ Proof.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
   clear delta H2.
-  rewrite (meps_0_deterministic H4 e1_real);
+  rewrite (meps_0_deterministic H3 e1_real);
     rewrite (meps_0_deterministic H5 e2_real).
-  rewrite (meps_0_deterministic H4 e1_real) in div_real.
+  rewrite (meps_0_deterministic H3 e1_real) in div_real.
   rewrite (meps_0_deterministic H5 e2_real) in div_real.
-  clear H4 H5 v1 v2.
+  clear H3 H5 H6 v1 v2.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion div_float; subst.
   unfold perturb; simpl.
-  inversion H4; subst; inversion H5; subst.
+  inversion H3; subst; inversion H5; subst.
   symmetry in H0, H1;
     unfold updEnv in *; simpl in *.
   inversion H0; inversion H1; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear div_float H4 H5 div_real e1_real e1_float e2_real e2_float H0 H1.
+  clear div_float H3 H5 div_real e1_real e1_float e2_real e2_float H0 H1.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.

coq/ErrorValidation.v

@@ -23,7 +23,11 @@ Fixpoint validErrorbound (e:exp Q) (absenv:analysisResult) (dVars:NatSet.t):=
      else (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
     |Const n =>
      Qleb (maxAbs intv * RationalSimps.machineEpsilon) err
-    |Unop _ _ => false
+    |Unop Neg e =>
+     if (validErrorbound e absenv dVars)
+     then Qeq_bool err (snd (absenv e))
+     else false
+    |Unop Inv e => false
     |Binop b e1 e2 =>
      if ((validErrorbound e1 absenv dVars) && (validErrorbound e2 absenv dVars))
      then
@@ -80,7 +84,9 @@ Proof.
       andb_to_prop validErrorbound_e.
   - apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
   - apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
-  - inversion R.
+  - destruct u; simpl in *; try congruence.
+    andb_to_prop R.
+    apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
   - apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
 Qed.
 
@@ -1961,7 +1967,26 @@ Proof.
   - unfold validErrorbound in valid_error.
     rewrite absenv_eq in valid_error.
     andb_to_prop valid_error.
-    inversion R.
+    destruct u; try congruence.
+    env_assert absenv e absenv_e.
+    destruct absenv_e as  [iv [err_e absenv_e]].
+    rename R into valid_error.
+    andb_to_prop valid_error.
+    apply Qeq_bool_iff in R.
+    apply Qeq_eqR in R.
+    rewrite R.
+    destruct iv as [e_lo e_hi].
+    inversion eval_real; subst.
+    inversion eval_float; subst.
+    unfold evalUnop.
+    apply bound_flip_sub.
+    eapply IHe; eauto.
+    simpl in valid_intv.
+    rewrite absenv_eq in valid_intv; andb_to_prop valid_intv.
+    auto.
+    instantiate (1 := e_hi).
+    instantiate (1 := e_lo).
+    rewrite absenv_e; auto.
   - pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_intv) as env_approx_p.
     simpl in valid_error.
     env_assert absenv e1 absenv_e1.
@@ -2079,36 +2104,6 @@ Proof.
           - andb_to_prop R1; auto. }
 Qed.
 
-Lemma validErrorbound_subset e absenv dVars dVars':
-  validErrorbound e absenv dVars = true ->
-  NatSet.Subset dVars dVars' ->
-  validErrorbound e absenv dVars' = true.
-Proof.
-  induction e; intros validBound_e_dV subset_dV; simpl in *; try auto.
-  - destruct (absenv (Var Q n)); simpl in *.
-    andb_to_prop validBound_e_dV.
-    apply Is_true_eq_true; apply andb_prop_intro; split.
-    + apply Is_true_eq_left in L; auto.
-    + case_eq (NatSet.mem n dVars);
-        intros case_mem; rewrite case_mem in *; simpl in *.
-      * hnf in subset_dV.
-        rewrite NatSet.mem_spec in case_mem.
-        specialize (subset_dV n case_mem).
-        rewrite <- NatSet.mem_spec in subset_dV.
-        rewrite subset_dV.
-        apply Is_true_eq_left; auto.
-      * case_eq (NatSet.mem n dVars'); intros case_mem';
-          apply Is_true_eq_left; auto.
-  - destruct (absenv (Binop b e1 e2)); simpl in *.
-    rewrite <- andb_lazy_alt in *.
-    andb_to_prop validBound_e_dV.
-    rewrite andb_true_iff; split; try auto.
-    destruct (absenv e1); destruct (absenv e2).
-    rewrite <- andb_lazy_alt.
-    rewrite andb_true_iff; split; try auto.
-    repeat (rewrite andb_true_iff; split); auto.
-Qed.
-
 Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
   forall E1 E2 outVars fVars dVars vR vF elo ehi err P,
     approxEnv E1 absenv fVars dVars E2 ->

coq/Expressions.v

+
 (**
   Formalization of the base expression language for the daisy framework
  **)
@@ -120,6 +121,7 @@ Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop :=
     Rle (Rabs delta) eps ->
     eval_exp eps E f1 v1 ->
     eval_exp eps E f2 v2 ->
+    ((op = Div) -> (~ v2 = 0)%R) ->
     eval_exp eps E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
 
 (**

coq/IntervalValidation.v

@@ -137,32 +137,6 @@ Qed.
 Ltac env_assert absenv e name :=
   assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto).
 
-Lemma validBoundsDiv_uneq_zero e1 e2 absenv P V ivlo_e2 ivhi_e2 err:
-  absenv e2 = ((ivlo_e2,ivhi_e2), err) ->
-  validIntervalbounds (Binop Div e1 e2) absenv P V = true ->
-  (ivhi_e2 < 0) \/ (0 < ivlo_e2).
-Proof.
-  intros absenv_eq validBounds.
-  unfold validIntervalbounds in validBounds.
-  env_assert absenv (Binop Div e1 e2) abs_div; destruct abs_div as [iv_div [err_div abs_div]].
-  env_assert absenv e1 abs_e1; destruct abs_e1 as [iv_e1 [err_e1 abs_e1]].
-  rewrite abs_div, abs_e1, absenv_eq in validBounds.
-  repeat (rewrite <- andb_lazy_alt in validBounds).
-  apply Is_true_eq_left in validBounds.
-  apply andb_prop_elim in validBounds.
-  destruct validBounds as [_ validBounds]; apply andb_prop_elim in validBounds.
-  destruct validBounds as [nodiv0 _].
-  apply Is_true_eq_true in nodiv0.
-  unfold isSupersetIntv in *; simpl in *.
-  apply le_neq_bool_to_lt_prop; auto.
-Qed.
-
-Fixpoint getRetExp (V:Type) (f:cmd V) :=
-  match f with
-  |Let x e g => getRetExp g
-  | Ret e => e
-  end.
-
 Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars E:
   forall vR,
     validIntervalbounds f absenv P dVars = true ->
@@ -490,6 +464,12 @@ Proof.
                     rewrite <- Q2R_max4 in valid_div_hi; auto. } }
 Qed.
 
+Fixpoint getRetExp (V:Type) (f:cmd V) :=
+  match f with
+  |Let x e g => getRetExp g
+  | Ret e => e
+  end.
+
 Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult):
   forall E vR fVars dVars outVars elo ehi err P,
     ssa f (NatSet.union fVars dVars) outVars ->
@@ -502,7 +482,7 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult):
           exists vR,
             E v = Some vR /\
             (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
-    NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
+    NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars ->
     validIntervalboundsCmd f absenv P dVars = true ->
     absenv (getRetExp f) = ((elo, ehi), err) ->
     (Q2R elo <=  vR <= Q2R ehi)%R.

coq/ssaPrgs.v

@@ -37,6 +37,7 @@ Proof.
       rewrite NatSet.union_spec; auto.
 Qed.
 
+(*
 Lemma validVars_non_stuck (e:exp Q) inVars E:
  NatSet.Subset (usedVars e) inVars ->
   (forall v, NatSet.In v (usedVars e) ->
@@ -80,7 +81,7 @@ Proof.
           destruct eval_e2_def as [vR2 eval_e2_def].
         exists (perturb (evalBinop b vR1 vR2) 0); constructor; auto.
         rewrite Rabs_R0; lra.
-Qed.
+Qed. *)
 
 Inductive ssa (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
  ssaLet x e s inVars Vterm:
@@ -95,7 +96,7 @@ Inductive ssa (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
 
 Lemma ssa_subset_freeVars V (f:cmd V) inVars outVars:
   ssa f inVars outVars ->
-  NatSet.Subset (Commands.freeVars f) inVars.
+  NatSet.Subset (freeVars f) inVars.
 Proof.
   intros ssa_f; induction ssa_f.
   - simpl in *. hnf; intros a in_fVars.
@@ -392,17 +393,135 @@ Qed.
 Fixpoint let_subst (f:cmd Q) :=
   match f with
   | Let x e1 g =>
-    match (let_subst g) with
-    |Some e' =>  Some (exp_subst e' x e1)
-    |None => None
-    end
-  | Ret e1 =>  Some e1
+    exp_subst (let_subst g) x e1
+  | Ret e1 => e1
   end.
 
+Lemma eval_subst_subexp E e' n e vR:
+  NatSet.In n (usedVars e) ->
+  eval_exp 0 E (toRExp (exp_subst e n e')) vR ->
+  exists v, eval_exp 0 E (toRExp e') v.
+Proof.
+  revert E e' n vR.
+  induction e;
+  intros E e' n' vR n_fVar eval_subst; simpl in *; try eauto.
+  - case_eq (n =? n'); intros case_n; rewrite case_n in *; eauto.
+    rewrite NatSet.singleton_spec in n_fVar.
+    exfalso.
+    rewrite Nat.eqb_neq in case_n.
+    apply case_n; auto.
+  - inversion n_fVar.
+  - inversion eval_subst; subst;
+      eapply IHe; eauto.
+  - inversion eval_subst; subst.
+    rewrite NatSet.union_spec in n_fVar.
+    destruct n_fVar as [n_fVar_e1 | n_fVare2];
+      [eapply IHe1; eauto | eapply IHe2; eauto].
+Qed.
+
+Lemma bstep_subst_subexp_any E e x f vR:
+  NatSet.In x (liveVars f) ->
+  bstep (toRCmd (map_subst f x e)) E 0 vR ->
+  exists E' v, eval_exp 0 E' (toRExp e) v.
+Proof.
+  revert E e x vR;
+    induction f;
+    intros E e' x vR x_live eval_f.
+  - inversion eval_f; subst.
+    simpl in x_live.
+    rewrite NatSet.union_spec in x_live.
+    destruct x_live as [x_used | x_live].
+    + exists E. eapply eval_subst_subexp; eauto.
+    + eapply IHf; eauto.
+  - simpl in *.
+    inversion eval_f; subst.
+    exists E. eapply eval_subst_subexp; eauto.
+Qed.
+
+Lemma bstep_subst_subexp_ret E e x e' vR:
+  NatSet.In x (liveVars (Ret e')) ->
+  bstep (toRCmd (map_subst (Ret e') x e)) E 0 vR ->
+  exists v, eval_exp 0 E (toRExp e) v.
+Proof.
+  simpl; intros x_live bstep_ret.
+  inversion bstep_ret; subst.
+  eapply eval_subst_subexp; eauto.
+Qed.
+Lemma no_forward_refs V (f:cmd V) inVars outVars:
+  ssa f inVars outVars ->
+  forall v, NatSet.In v (definedVars f) ->
+       NatSet.mem v inVars = false.
+Proof.
+  intros ssa_f; induction ssa_f; simpl.
+  - intros v v_defVar.
+    rewrite NatSet.add_spec in v_defVar.
+    destruct v_defVar as [v_x | v_defVar].
+    + subst; auto.
+    + specialize (IHssa_f v v_defVar).
+      case_eq (NatSet.mem v inVars); intros mem_inVars; try auto.
+      assert (NatSet.mem v (NatSet.add x inVars) = true) by (rewrite NatSet.mem_spec, NatSet.add_spec, <- NatSet.mem_spec; auto).
+      congruence.
+  - intros v v_in_empty; inversion v_in_empty.
+Qed.
+
+Lemma bstep_subst_subexp_let E e x y e' g vR:
+  NatSet.In x (liveVars (Let y e' g)) ->
+  (forall x, NatSet.In x (usedVars e) ->
+        exists v, E x = v) ->
+  bstep (toRCmd (map_subst (Let y e' g) x e)) E 0 vR ->
+  exists v, eval_exp 0 E (toRExp e) v.
+Proof.
+  revert E e x y e' vR;
+    induction g;
+    intros E e0 x y e' vR x_live uedVars_def bstep_f.
+  - simpl in *.
+    inversion bstep_f; subst.
+    specialize (IHg (updEnv y v E) e0 x n e).
+    rewrite NatSet.union_spec in x_live.
+    destruct x_live as [x_used | x_live].
+    + eapply eval_subst_subexp; eauto.
+    + edestruct IHg as [v0 eval_v0]; eauto.
+Admitted.
+
+Theorem let_free_agree f E vR inVars outVars e:
+  ssa f inVars outVars ->
+  (forall v, NatSet.In v (definedVars f) ->
+        NatSet.In v (liveVars f)) ->
+  let_subst f = e ->
+  bstep (toRCmd (Ret e)) E 0 vR ->
+  bstep (toRCmd f) E 0 vR.
+Proof.
+  intros ssa_f.
+  revert E vR e;
+    induction ssa_f;
+    intros E vR e_subst dVars_live subst_step bstep_e;
+    simpl in *.
+  (* Let Case, prove that the value of the let binding must be used somewhere *)
+  - case_eq (let_subst s).
+    + intros e0 subst_s; rewrite subst_s in *.
+Admitted.
+      (*inversion subst_step; subst.
+      clear subst_s subst_step.
+      inversion bstep_e; subst.
+      specialize (dVars_live x).
+      rewrite NatSet.add_spec in dVars_live.
+      assert (NatSet.In x (NatSet.union (usedVars e) (liveVars s)))
+        as x_used_or_live
+          by (apply dVars_live; auto).
+      rewrite NatSet.union_spec in x_used_or_live.
+      destruct x_used_or_live as [x_used | x_live].
+      * specialize (H x x_used).
+        rewrite <- NatSet.mem_spec in H; congruence.
+      *
+
+    eapply let_b.
+    Focus 2.
+    eapply IHssa_f; try auto. *)
+
 Theorem let_free_form f E vR inVars outVars e:
   ssa f inVars outVars ->
   bstep (toRCmd f) E 0 vR ->
-  let_subst f = Some e ->
+  let_subst f = e ->
   bstep (toRCmd (Ret e)) E 0 vR.
 Proof.
   revert E vR inVars outVars e;
@@ -411,8 +530,8 @@ Proof.
   - simpl.
     inversion bstep_f; subst.
     inversion ssa_f; subst.
-    simpl in subst_step.
-    case_eq (let_subst f).
+Admitted.
+(* case_eq (let_subst f).
     + intros f_subst subst_f_eq.
       specialize (IHf (updEnv n v E) vR (NatSet.add n inVars) outVars f_subst H8 H6 subst_f_eq).
       rewrite subst_f_eq in subst_step.
@@ -428,6 +547,7 @@ Proof.
     inversion subst_step; subst.
     assumption.
 Qed.
+ *)
 
 (*
 Lemma ssa_non_stuck (f:cmd Q) (inVars outVars:NatSet.t) (VarEnv:var_env)

hol4/AbbrevsScript.sml

@@ -36,9 +36,4 @@ val emptyEnv_def = Define `
 val updEnv_def = Define `
 updEnv (x:num) (v:real) (E:env) (y:num) :real option = if y = x then SOME v else E y`;
 
-(**
-  Abbreviation for insertion into "num_set" type
-**)
-val Insert_def = Define `Insert x V  = insert x () V`;
-
 val - = export_theory();

hol4/CertificateCheckerScript.sml

@@ -6,7 +6,7 @@
 **)
 open preamble
 open simpLib realTheory realLib RealArith
-open AbbrevsTheory ExpressionsTheory RealSimpsTheory
+open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
 open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
 open IntervalValidationTheory ErrorValidationTheory
 
@@ -15,11 +15,15 @@ val _ = new_theory "CertificateChecker";
 (** Certificate checking function **)
 val CertificateChecker_def = Define
   `CertificateChecker (e:real exp) (absenv:analysisResult) (P:precond) =
-   ((validIntervalbounds e absenv P EMPTY) /\ (validErrorbound e absenv))`;
+     if (validIntervalbounds e absenv P LN)
+       then (validErrorbound e absenv LN)
+       else F`;
 
 val CertificateCheckerCmd_def = Define
   `CertificateCheckerCmd (f:real cmd) (absenv:analysisResult) (P:precond) =
-   ((validIntervalboundsCmd f absenv P EMPTY) /\ (validErrorboundCmd f absenv))`;
+     if (validIntervalboundsCmd f absenv P LN)
+       then (validErrorboundCmd f absenv LN)
+       else F`;
 
 (**
    Soundness proof for the certificate checker.
@@ -27,44 +31,56 @@ val CertificateCheckerCmd_def = Define
    the real valued execution respects the precondition.
 **)
 val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
-  ``!(e:real exp) (absenv:analysisResult) P (VarEnv1 VarEnv2 ParamEnv:env)
-     (vR:real) (vF:real).
-      approxEnv VarEnv1 absenv VarEnv2 /\
-      eval_exp 0 VarEnv1 ParamEnv P e vR /\
-      eval_exp machineEpsilon VarEnv2 ParamEnv P e vF /\
+  ``!(e:real exp) (absenv:analysisResult) (P:precond) (E1 E2:env)
+     (vR:real) (vF:real) fVars.
+      approxEnv E1 absenv fVars LN E2 /\
+      (!v.
+          v IN (domain fVars) ==>
+          ?vR.
+            (E1 v = SOME vR) /\
+            FST (P v) <= vR /\ vR <= SND (P v)) /\
+      (domain (usedVars e)) SUBSET (domain fVars) /\
+      eval_exp 0 E1 e vR /\
+      eval_exp machineEpsilon E2 e vF /\
       CertificateChecker e absenv P ==>
       abs (vR - vF) <= (SND (absenv e))``,
 (**
    The proofs is a simple composition of the soundness proofs for the range
    validator and the error bound validator.
 **)
-  simp [CertificateChecker_def] \\
-  rpt strip_tac \\
-  Cases_on `absenv e` \\
-  rename1 `absenv e = (iv, err)` \\
-  Cases_on `iv` \\
-  rename1 `absenv e = ((elo, ehi), err)` \\
-  match_mp_tac validErrorbound_sound \\
-  qexistsl_tac [`e`, `VarEnv1`, `VarEnv2`, `ParamEnv`, `absenv`, `P`, `elo`, `ehi`, `EMPTY`] \\
-  fs[]);
+  simp [CertificateChecker_def]
+  \\ rpt strip_tac
+  \\ Cases_on `absenv e`
+  \\ rename1 `absenv e = (iv, err)`
+  \\ Cases_on `iv`
+  \\ rename1 `absenv e = ((elo, ehi), err)`
+  \\ match_mp_tac validErrorbound_sound
+  \\ qexistsl_tac [`e`, `E1`, `E2`, `absenv`, `P`, `elo`, `ehi`, `fVars`, `LN`]
+  \\ fs[]);
 
 val CertificateCmd_checking_is_sound = store_thm ("CertificateCmd_checking_is_sound",
   ``!(f:real cmd) (absenv:analysisResult) (P:precond)
-     (VarEnv1 VarEnv2 ParamEnv:env) (outVars:num set) (envR envF:env).
-      approxEnv VarEnv1 absenv VarEnv2 /\
-      ssaPrg f EMPTY outVars /\
-      bstep f VarEnv1 ParamEnv P 0 Nop envR /\
-      bstep f VarEnv2 ParamEnv P machineEpsilon Nop envF /\
+     (E1 E2:env) (outVars:num_set) (vR vF:real) fVars.
+      approxEnv E1 absenv fVars LN E2 /\
+      (!v.
+          v IN (domain fVars) ==>
+          ?vR.
+            (E1 v = SOME vR) /\
+            FST (P v) <= vR /\ vR <= SND (P v)) /\