Commit 5d57e590 authored by Heiko Becker's avatar Heiko Becker

Fix compilation bug in AA error validator draft

parent d32d2dcf
......@@ -231,24 +231,24 @@ Definition checked_error_expressions (A: analysisResult) (E1 E2:env) Gamma e
let mAbs := maxAbs (toIntv af) in
(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,
FloverMap.In e initMap ->
checked_error_expressions A E1 E2 Gamma e initMap currNoise M1 vR) ->
approxEnv E1 defVars A fVars dVars E2 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
affine_dVars_range_valid dVars E1 A currNoise initMap M1 ->
affine_fVars_P_sound fVars E1 P ->
affine_vars_typed fVars Gamma ->
validErrorboundAA e Gamma A tMap currNoise initMap = Some (resMap, maxNoise) ->
RangeValidator e A P dVars = true ->
typeCheck e defVars Gamma = true ->
vars_typed (NatSet.union fVars dVars) defVars ->
FloverMap.find e A = Some ((elo,ehi),err) ->
(exists nF m,
eval_expr E2 defVars (toRExp e) nF m) /\
(forall nF m,
eval_expr E2 defVars (toRExp e) nF m ->
(Rabs (nR - nF) <= (Q2R err))%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, *)
(* FloverMap.In e initMap -> *)
(* checked_error_expressions A E1 E2 Gamma e initMap currNoise M1 vR) -> *)
(* approxEnv E1 defVars A fVars dVars E2 -> *)
(* NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars -> *)
(* eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL -> *)
(* affine_dVars_range_valid dVars E1 A currNoise initMap M1 -> *)
(* affine_fVars_P_sound fVars E1 P -> *)
(* affine_vars_typed fVars Gamma -> *)
(* validErrorboundAA e Gamma A tMap currNoise initMap = Some (resMap, maxNoise) -> *)
(* RangeValidator e A P dVars = true -> *)
(* typeCheck e defVars Gamma = true -> *)
(* vars_typed (NatSet.union fVars dVars) defVars -> *)
(* FloverMap.find e A = Some ((elo,ehi),err) -> *)
(* (exists nF m, *)
(* eval_expr E2 defVars (toRExp e) nF m) /\ *)
(* (forall nF m, *)
(* eval_expr E2 defVars (toRExp e) nF m -> *)
(* (Rabs (nR - nF) <= (Q2R err))%R). *)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment