From 96bc2e7ec9d749164ae0c5b8c9f7cd8c61d3a3d6 Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Thu, 16 Aug 2018 14:35:40 +0200 Subject: [PATCH] minor style changes in Coq dev and finish porting in HOL4 --- coq/Environments.v | 9 +- coq/ErrorValidation.v | 54 +-- coq/ExpressionSemantics.v | 2 +- coq/Infra/ExpressionAbbrevs.v | 86 +++++ coq/Infra/MachineType.v | 25 +- coq/RealRangeArith.v | 4 - coq/TypeValidator.v | 125 +------ hol4/IEEE_connectionScript.sml | 649 +++++++++++++++++++-------------- 8 files changed, 495 insertions(+), 459 deletions(-) diff --git a/coq/Environments.v b/coq/Environments.v index de6dda1..e071274 100644 --- a/coq/Environments.v +++ b/coq/Environments.v @@ -26,7 +26,7 @@ Inductive approxEnv : env -> (expr R -> option mType) -> analysisResult -> NatSe (Rabs (v1 - v2) <= computeErrorR v1 m)%R -> NatSet.mem x (NatSet.union fVars dVars) = false -> approxEnv (updEnv x v1 E1) - (updDefVars (Var R x) m Gamma) A (NatSet.add x fVars) dVars + Gamma A (NatSet.add x fVars) dVars (updEnv x v2 E2) |approxUpdBound E1 E2 Gamma A v1 v2 x fVars dVars m iv err: approxEnv E1 Gamma A fVars dVars E2 -> @@ -88,11 +88,7 @@ Section RelationProperties. destruct x_free as [x_x0 | [x_neq x_free]]; subst. + unfold updEnv in *; rewrite Nat.eqb_refl in *; simpl in *. - unfold updDefVars in x_typed. - cbn in x_typed. - rewrite Nat.compare_refl in x_typed. - inversion x_typed; subst. - inversion E1_def; inversion E2_def; subst; auto. + congruence. + unfold updEnv in *; simpl in *. rewrite <- Nat.eqb_neq in x_neq. rewrite x_neq in *; simpl in *. @@ -109,7 +105,6 @@ Section RelationProperties. apply H2. set_tac. } unfold updEnv in *; rewrite x_x0_neq in *. - unfold updDefVars in x_typed. cbn in x_typed. apply Nat.eqb_neq in x_x0_neq. destruct (x ?= x0)%nat eqn:?. diff --git a/coq/ErrorValidation.v b/coq/ErrorValidation.v index 2d6346b..6ce5cde 100644 --- a/coq/ErrorValidation.v +++ b/coq/ErrorValidation.v @@ -249,12 +249,11 @@ Proof. rewrite Rabs_R0. auto using mTypeToR_pos_R. Qed. -Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars exprTypes - Gamma: +Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars Gamma: eval_Real E1 Gamma (Const m n) nR -> eval_Fin E2 Gamma (Const m n) nF m -> validTypes (Const m n) Gamma -> - validErrorbound (Const m n) exprTypes A dVars = true -> + validErrorbound (Const m n) Gamma A dVars = true -> (Q2R nlo <= nR <= Q2R nhi)%R -> FloverMap.find (Const m n) A = Some ((nlo,nhi),e) -> (Rabs (nR - nF) <= (Q2R e))%R. @@ -275,28 +274,6 @@ Proof. simpl in *; auto. Qed. -(* -Lemma isFixedPoint_lift m1 m2 e fBits f: - (isFixedPoint m1 -> isFixedPoint m2 -> FloverMap.find e fBits = Some f) -> - isFixedPoint m1 -> isFixedPoint m2 -> toRBMap fBits (toRExp e) = Some f. -Proof. - intros isvalid fixed_m1 fixed_m2. - apply toRBMap_some. - auto. -Qed. - -Lemma isFixedPoint_lift3 m1 m2 m3 e fBits f: - (isFixedPoint m1 -> isFixedPoint m2 -> isFixedPoint m3 -> - FloverMap.find e fBits = Some f) -> - isFixedPoint m1 -> isFixedPoint m2 -> isFixedPoint m3 -> - toRBMap fBits (toRExp e) = Some f. -Proof. - intros isvalid fixed_m1 fixed_m2 fixed_m3. - apply toRBMap_some. - auto. -Qed. - *) - Lemma validErrorboundCorrectAddition E1 E2 A (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma: @@ -1994,7 +1971,7 @@ Qed. (** Soundness theorem for the error bound validator. - Proof is by induction on the exprression e. + Proof is by induction on the expression e. Each case requires the application of one of the soundness lemmata proven before **) Theorem validErrorbound_sound (e:expr Q): @@ -2004,7 +1981,6 @@ Theorem validErrorbound_sound (e:expr Q): NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars -> eval_Real E1 Gamma e nR -> validErrorbound e Gamma A dVars = true -> - validTypes e Gamma -> validRanges e A E1 (toRTMap (toRExpMap Gamma)) -> FloverMap.find e A = Some ((elo,ehi),err) -> (exists nF m, @@ -2014,8 +1990,8 @@ Theorem validErrorbound_sound (e:expr Q): (Rabs (nR - nF) <= (Q2R err))%R). Proof. revert e; induction e; - intros * typing_ok approxCEnv fVars_subset eval_real valid_error valid_types - valid_intv A_eq. + intros * typing_ok approxCEnv fVars_subset eval_real valid_error valid_intv + A_eq. - split. + eapply validErrorboundCorrectVariable_eval; eauto. + intros * eval_float. eapply validErrorboundCorrectVariable; eauto. @@ -2336,7 +2312,6 @@ Proof. { exists vF_res; exists m_res; try auto. econstructor; eauto. } + destruct valid_types as [[? [? [? [? [? ?]]]]] ?]; auto. - + destruct valid_types as [[? [? [? [? [? ?]]]]] ?]; auto. + destruct valid_intv as [[? ?] ?]; auto. - inversion eval_real; subst. unfold updEnv; simpl. @@ -2407,28 +2382,9 @@ Proof. simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. split; try auto. - (* + eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRTMap Gamma)); *) - (* eauto using Rmap_updVars_comm. *) - (* + apply validRangesCmd_swap with (Gamma1 := updDefVars n REAL Gamma). *) - (* * intros x. *) - (* unfold toRTMap, updDefVars. *) - (* destruct (x =? n) eqn:?; auto. *) - (* * destruct valid_intv as [[? valid_cont] ?]. *) - (* apply valid_cont. *) - (* apply swap_Gamma_eval_expr with (Gamma1 := toRTMap Gamma); try auto. *) + destruct valid_intv as [[? ?] ?]; auto. + destruct valid_types as [[? [? [? [? [? ?]]]]] ?]; auto. - + destruct valid_types as [[? [? [? [? [? ?]]]]] ?]; auto. + destruct valid_intv as [[? ?] ?]; auto. - (* + intros v1 v1_mem; set_tac. *) - (* unfold updDefVars. *) - (* case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try eauto. *) - (* apply types_defined. *) - (* rewrite NatSet.union_spec. *) - (* destruct v1_mem as [v_fVar | v_dVar]; try auto. *) - (* rewrite NatSet.add_spec in v_dVar. destruct v_dVar; try auto. *) - (* subst; rewrite Nat.eqb_refl in case_v1; congruence. *) - (* + destruct valid_intv as [[? ?] ?]; auto. *) - inversion eval_real; subst. inversion eval_float; subst. unfold updEnv; simpl. diff --git a/coq/ExpressionSemantics.v b/coq/ExpressionSemantics.v index e3b9f6f..af4ec9b 100644 --- a/coq/ExpressionSemantics.v +++ b/coq/ExpressionSemantics.v @@ -380,7 +380,7 @@ Proof. Qed. Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2: - (forall n, Gamma1 n = Gamma2 n) -> + (forall e, Gamma1 e = Gamma2 e) -> eval_expr E Gamma1 e vR m -> eval_expr E Gamma2 e vR m. Proof. diff --git a/coq/Infra/ExpressionAbbrevs.v b/coq/Infra/ExpressionAbbrevs.v index c5aef2c..ebffcdd 100644 --- a/coq/Infra/ExpressionAbbrevs.v +++ b/coq/Infra/ExpressionAbbrevs.v @@ -219,6 +219,32 @@ Proof. congruence. Qed. +Lemma map_find_add e1 e2 m map1: + FloverMap.find e1 (FloverMap.add e2 m map1) = + match Q_orderedExps.compare e2 e1 with + |Eq => Some m + |_ => FloverMap.find (elt:=mType) e1 map1 + end. +Proof. + rewrite FloverMapFacts.P.F.add_o. + unfold FloverMapFacts.P.F.eq_dec. + unfold Q_orderedExps.compare. + destruct (Q_orderedExps.exprCompare e2 e1) eqn:?; congruence. +Qed. + +Lemma map_mem_add e1 e2 m map1: + FloverMap.mem e1 (FloverMap.add e2 m map1) = + match Q_orderedExps.compare e2 e1 with + |Eq => true + | _ => FloverMap.mem (elt:=mType) e1 map1 + end. +Proof. + rewrite FloverMapFacts.P.F.mem_find_b. + rewrite map_find_add. + destruct (Q_orderedExps.compare e2 e1) eqn:?; try auto; + rewrite FloverMapFacts.P.F.mem_find_b; auto. +Qed. + Definition toRExpMap (tMap:FloverMap.t mType) : expr R -> option mType := let elements := FloverMap.elements (elt:=mType) tMap in fun (e:expr R) => @@ -378,6 +404,66 @@ Proof. rewrite Pos.eqb_refl, N.eqb_refl in e5; simpl in *; congruence. Qed. +Lemma no_cycle_unop e: + forall u, Q_orderedExps.exprCompare e (Unop u e) <> Eq. + induction e; intros *; cbn in *; try congruence. + destruct (unopEq u u0) eqn:?; try auto. + destruct (unopEq u Neg); congruence. +Qed. + +Lemma no_cycle_cast e: + forall m, Q_orderedExps.exprCompare e (Downcast m e) <> Eq. + induction e; intros *; cbn in *; try congruence. + destruct (mTypeEq m m0) eqn:?; try auto. + destruct m; destruct m0; type_conv; try congruence; + cbn; hnf; intros; try congruence. + destruct (w ?= w0)%positive eqn:?; try congruence. + apply Pos.compare_eq in Heqc. + apply N.compare_eq in H; subst; congruence. +Qed. + +Lemma no_cycle_binop_left e1: + forall b e2, Q_orderedExps.exprCompare e1 (Binop b e1 e2) <> Eq. + induction e1; intros *; cbn in *; try congruence. + pose (bOp := b); + destruct b; destruct b0; + try (hnf; intros; congruence); + destruct (Q_orderedExps.exprCompare e1_1 (Binop bOp e1_1 e1_2)) eqn:case_comp; + subst bOp; rewrite case_comp in *; + congruence. +Qed. + +Lemma no_cycle_binop_right e2: + forall b e1, Q_orderedExps.exprCompare e2 (Binop b e1 e2) <> Eq. + induction e2; intros *; cbn in *; try congruence. + pose (bOp := b); + destruct b; destruct b0; + try (hnf; intros; congruence); + destruct (Q_orderedExps.exprCompare e2_1 e1) eqn:?; congruence. +Qed. + +Lemma no_cycle_fma_left e1: + forall e2 e3, Q_orderedExps.exprCompare e1 (Fma e1 e2 e3) <> Eq. +Proof. + induction e1; intros *; cbn in *; try congruence; + destruct (Q_orderedExps.exprCompare e1_1 (Fma e1_1 e1_2 e1_3)) eqn:?; congruence. +Qed. + +Lemma no_cycle_fma_center e2: + forall e1 e3, Q_orderedExps.exprCompare e2 (Fma e1 e2 e3) <> Eq. +Proof. + induction e2; intros *; cbn in *; try congruence. + destruct (Q_orderedExps.exprCompare e2_1 e1) eqn:?; try congruence. + destruct (Q_orderedExps.exprCompare e2_2 (Fma e2_1 e2_2 e2_3)) eqn:?; congruence. +Qed. + +Lemma no_cycle_fma_right e3: + forall e1 e2, Q_orderedExps.exprCompare e3 (Fma e1 e2 e3) <> Eq. +Proof. + induction e3; intros *; cbn in *; try congruence. + destruct (Q_orderedExps.exprCompare e3_1 e1) eqn:?; try congruence. + destruct (Q_orderedExps.exprCompare e3_2 e2) eqn:?; try congruence. +Qed. (* Lemma toRExpMap_toRTMap e Gamma m: toRExpMap Gamma (toRExp e) = Some m -> diff --git a/coq/Infra/MachineType.v b/coq/Infra/MachineType.v index dc30477..4b9cea9 100644 --- a/coq/Infra/MachineType.v +++ b/coq/Infra/MachineType.v @@ -57,11 +57,6 @@ Definition mTypeToR (m:mType) :R := | M32 => 1/ 2^24 | M64 => 1/ 2^53 | F w f => 1/ 2^(N.to_nat f) - (* - (* the epsilons below match what is used internally in Daisy, - although these value do not match the IEEE standard *) - | M128 => (Qpower (2#1) (Zneg 105)) - | M256 => (Qpower (2#1) (Zneg 211)) *) end. Definition mTypeToQ (m:mType) :Q := @@ -71,11 +66,6 @@ Definition mTypeToQ (m:mType) :Q := | M32 => (Qpower (2#1) (Zneg 24)) | M64 => (Qpower (2#1) (Zneg 53)) | F w f => Qpower (2#1) (- Z.of_N f) - (* - (* the epsilons below match what is used internally in Daisy, - although these value do not match the IEEE standard *) - | M128 => (Qpower (2#1) (Zneg 105)) - | M256 => (Qpower (2#1) (Zneg 211)) *) end. Definition computeErrorR v m :R := @@ -201,8 +191,6 @@ Definition mTypeEq (m1:mType) (m2:mType) := | M32, M32 => true | M64, M64 => true | F w1 f1, F w2 f2 => (w1 =? w2)%positive && (f1 =? f2)%N - (* | M128, M128 => true *) - (* | M256, M256 => true *) | _, _ => false end. @@ -273,8 +261,10 @@ Definition isMorePrecise (m1:mType) (m2:mType) := | _, _ => Qle_bool (mTypeToQ m1) (mTypeToQ m2) end. -(* More efficient version for performance, unfortunately we cannot do better - for fixed-points *) +(** + More efficient version for performance, unfortunately we cannot do better + for fixed-points +**) Definition morePrecise (m1:mType) (m2:mType) := match m1, m2 with | REAL, _ => true @@ -302,12 +292,9 @@ Lemma morePrecise_trans m1 m2 m3: Proof. destruct m1; destruct m2; destruct m3; simpl; auto; intros le1 le2; try congruence. - (* andb_to_prop le1; andb_to_prop le2. *) apply Pos.leb_le in le1; apply Pos.leb_le in le2. - (* apply Pos.leb_le in L0; apply Pos.leb_le in R0. *) - (* split_bool; *) - apply Pos.leb_le; - eapply Pos.le_trans; eauto. + apply Pos.leb_le; + eapply Pos.le_trans; eauto. Qed. Lemma isMorePrecise_morePrecise m1 m2: diff --git a/coq/RealRangeArith.v b/coq/RealRangeArith.v index 110280b..9ac4ad2 100644 --- a/coq/RealRangeArith.v +++ b/coq/RealRangeArith.v @@ -19,10 +19,6 @@ Definition fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop := exists vR, E v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R. -Definition vars_typed (S:NatSet.t) (Gamma: nat -> option mType) := - forall v, NatSet.In v S -> - exists m :mType, Gamma v = Some m. - Ltac kill_trivial_exists := match goal with | [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e diff --git a/coq/TypeValidator.v b/coq/TypeValidator.v index 643d747..e9ccc93 100644 --- a/coq/TypeValidator.v +++ b/coq/TypeValidator.v @@ -29,13 +29,17 @@ Fixpoint validTypes e (Gamma:FloverMap.t mType) :Prop := | Var _ x => True | Const m v => m = mG | Unop u e1 => - validTypes e1 Gamma /\ exists me, FloverMap.find e1 Gamma = Some me /\ isCompat me mG = true + validTypes e1 Gamma /\ + exists me, FloverMap.find e1 Gamma = Some me /\ isCompat me mG = true | Binop b e1 e2 => - validTypes e1 Gamma /\ validTypes e2 Gamma /\ - exists m1 m2, FloverMap.find e1 Gamma = Some m1 /\ FloverMap.find e2 Gamma = Some m2 /\ + validTypes e1 Gamma /\ + validTypes e2 Gamma /\ + exists m1 m2, FloverMap.find e1 Gamma = Some m1 /\ + FloverMap.find e2 Gamma = Some m2 /\ isJoin m1 m2 mG = true | Fma e1 e2 e3 => - validTypes e1 Gamma /\ validTypes e2 Gamma /\ + validTypes e1 Gamma /\ + validTypes e2 Gamma /\ validTypes e3 Gamma /\ exists m1 m2 m3, FloverMap.find e1 Gamma = Some m1 /\ FloverMap.find e2 Gamma = Some m2 /\ @@ -47,7 +51,8 @@ Fixpoint validTypes e (Gamma:FloverMap.t mType) :Prop := (FloverMap.find e1 Gamma = Some m1 /\ isMorePrecise m1 mG = true) end /\ (forall E Gamma2 v m, - (forall e m, FloverMap.find e Gamma = Some m -> FloverMap.find e Gamma2 = Some m) -> + (forall e m, FloverMap.find e Gamma = Some m -> + FloverMap.find e Gamma2 = Some m) -> eval_expr E (toRExpMap Gamma2) (toRExp e) v m -> m = mG). @@ -123,12 +128,6 @@ Ltac validTypes_simp := Open Scope string_scope. -Definition getTypeMap (r:result (FloverMap.t mType)) :FloverMap.t mType:= - match r with - |Succes m => m - | _ => FloverMap.empty mType - end. - Definition isMonotone mOldO mNew := match mOldO with |None => true @@ -165,21 +164,21 @@ Fixpoint getValidMap (Gamma:FloverMap.t mType) (e:expr Q) | Unop u e1 => rlet akk_new := getValidMap Gamma e1 akk in match FloverMap.find e1 akk_new with + | None => Fail _ "Cannot Typecheck unary operator" | Some m_e1 => if (isFixedPointB m_e1) then match mOldO with + |None => Fail _ "Undefined fixed-point type" |Some mFix => if (isCompat m_e1 mFix) then addMono e mFix akk_new else Fail _ "Incompatible type assignment" - |None => Fail _ "Undefined fixed-point type" end else if (isMonotone mOldO m_e1) then addMono e m_e1 akk_new else Fail _ "Wrong type annotation for unary constant" - | None => Fail _ "Cannot Typecheck unary operator" end | Binop b e1 e2 => rlet akk1_map := getValidMap Gamma e1 akk in @@ -199,11 +198,11 @@ Fixpoint getValidMap (Gamma:FloverMap.t mType) (e:expr Q) end else match (join_fl t1 t2) with + | None => Fail _ "Could not compute join for arguments" | Some m => if (isMonotone mOldO m) then addMono e m akk2_map else Fail _ "Wrong type annotation for binary operator" - | None => Fail _ "Could not compute join for arguments" end | _, _ => Fail _ "Could not compute type for arguments" end @@ -239,20 +238,20 @@ Fixpoint getValidMap (Gamma:FloverMap.t mType) (e:expr Q) rlet akk_new := getValidMap Gamma e1 akk in let m1 := FloverMap.find e1 akk_new in match m1 with + | None => Fail _ "Could not find cast argument type" | Some t1 => if (isFixedPointB t1) then match mOldO with + |None => Fail _ "Could not find fixed-point type for cast" |Some mFix => if (mTypeEq m mFix && morePrecise t1 mFix) then addMono e mFix akk_new else Fail _ "Incorrect fixed-point type" - |None => Fail _ "Could not find fixed-point type for cast" end else if (morePrecise t1 m && isMonotone mOldO m) then addMono e m akk_new else Fail _ "Cannot cast down to lower precision" - | None => Fail _ "Could not find case argument type" end end. @@ -275,93 +274,6 @@ Proof. eauto using tMap_def. Qed. -Lemma no_cycle_unop e: - forall u, Q_orderedExps.exprCompare e (Unop u e) <> Eq. - induction e; intros *; cbn in *; try congruence. - destruct (unopEq u u0) eqn:?; try auto. - destruct (unopEq u Neg); congruence. -Qed. - -Lemma no_cycle_cast e: - forall m, Q_orderedExps.exprCompare e (Downcast m e) <> Eq. - induction e; intros *; cbn in *; try congruence. - destruct (mTypeEq m m0) eqn:?; try auto. - destruct m; destruct m0; type_conv; try congruence; - cbn; hnf; intros; try congruence. - destruct (w ?= w0)%positive eqn:?; try congruence. - apply Pos.compare_eq in Heqc. - apply N.compare_eq in H; subst; congruence. -Qed. - -Lemma no_cycle_binop_left e1: - forall b e2, Q_orderedExps.exprCompare e1 (Binop b e1 e2) <> Eq. - induction e1; intros *; cbn in *; try congruence. - pose (bOp := b); - destruct b; destruct b0; - try (hnf; intros; congruence); - destruct (Q_orderedExps.exprCompare e1_1 (Binop bOp e1_1 e1_2)) eqn:case_comp; - subst bOp; rewrite case_comp in *; - congruence. -Qed. - -Lemma no_cycle_binop_right e2: - forall b e1, Q_orderedExps.exprCompare e2 (Binop b e1 e2) <> Eq. - induction e2; intros *; cbn in *; try congruence. - pose (bOp := b); - destruct b; destruct b0; - try (hnf; intros; congruence); - destruct (Q_orderedExps.exprCompare e2_1 e1) eqn:?; congruence. -Qed. - -Lemma no_cycle_fma_left e1: - forall e2 e3, Q_orderedExps.exprCompare e1 (Fma e1 e2 e3) <> Eq. -Proof. - induction e1; intros *; cbn in *; try congruence; - destruct (Q_orderedExps.exprCompare e1_1 (Fma e1_1 e1_2 e1_3)) eqn:?; congruence. -Qed. - -Lemma no_cycle_fma_center e2: - forall e1 e3, Q_orderedExps.exprCompare e2 (Fma e1 e2 e3) <> Eq. -Proof. - induction e2; intros *; cbn in *; try congruence. - destruct (Q_orderedExps.exprCompare e2_1 e1) eqn:?; try congruence. - destruct (Q_orderedExps.exprCompare e2_2 (Fma e2_1 e2_2 e2_3)) eqn:?; congruence. -Qed. - -Lemma no_cycle_fma_right e3: - forall e1 e2, Q_orderedExps.exprCompare e3 (Fma e1 e2 e3) <> Eq. -Proof. - induction e3; intros *; cbn in *; try congruence. - destruct (Q_orderedExps.exprCompare e3_1 e1) eqn:?; try congruence. - destruct (Q_orderedExps.exprCompare e3_2 e2) eqn:?; try congruence. -Qed. - -Lemma map_find_add e1 e2 m map1: - FloverMap.find e1 (FloverMap.add e2 m map1) = - match Q_orderedExps.compare e2 e1 with - |Eq => Some m - |_ => FloverMap.find (elt:=mType) e1 map1 - end. -Proof. - rewrite FloverMapFacts.P.F.add_o. - unfold FloverMapFacts.P.F.eq_dec. - unfold Q_orderedExps.compare. - destruct (Q_orderedExps.exprCompare e2 e1) eqn:?; congruence. -Qed. - -Lemma map_mem_add e1 e2 m map1: - FloverMap.mem e1 (FloverMap.add e2 m map1) = - match Q_orderedExps.compare e2 e1 with - |Eq => true - | _ => FloverMap.mem (elt:=mType) e1 map1 - end. -Proof. - rewrite FloverMapFacts.P.F.mem_find_b. - rewrite map_find_add. - destruct (Q_orderedExps.compare e2 e1) eqn:?; try auto; - rewrite FloverMapFacts.P.F.mem_find_b; auto. -Qed. - Ltac by_monotonicity find_akk mem_case:= rewrite map_find_add; match goal with @@ -670,13 +582,6 @@ Proof. + Flover_compute. destruct (isCompat m m0) eqn:?; try congruence. unfold addMono in *; Flover_compute. - (* { destruct (mTypeEq m0 m1) eqn:?; try congruence. *) - (* inversion validMap_succ; subst. *) - (* exists m1; repeat split; try auto. *) - (* intros * map_mono eval_unop. *) - (* specialize (map_mono (Unop u e) m1 Heqo1). *) - (* eapply toRExpMap_some in map_mono; simpl; eauto. *) - (* inversion eval_unop; subst; congruence. } *) inversion validMap_succ; subst. assert (FloverMap.mem (Unop u e) t = false) by (rewrite FloverMapFacts.P.F.mem_find_b; rewrite Heqo1; eauto). diff --git a/hol4/IEEE_connectionScript.sml b/hol4/IEEE_connectionScript.sml index 8f2d500..12f5648 100644 --- a/hol4/IEEE_connectionScript.sml +++ b/hol4/IEEE_connectionScript.sml @@ -462,7 +462,7 @@ val is64BitEval_def = Define ` (is64BitEval (Unop _ e) = is64BitEval e) /\ (is64BitEval (Binop b e1 e2) = (is64BitEval e1 /\ is64BitEval e2)) /\ (is64BitEval (Fma e1 e2 e3) = (is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3)) /\ - (is64BitEval (Downcast m e) = is64BitEval e) /\ + (is64BitEval (Downcast m e) = ((m = M64) /\ is64BitEval e)) /\ (is64BitEval ((Var v):real expr) = T)`; val is64BitBstep_def = Define ` @@ -493,7 +493,7 @@ val typing_cmd_64bit = store_thm ( \\ res_tac); val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE", - ``!(e:word64 expr) E1 E2 E2_real Gamma vR A P fVars dVars. + ``!(e:word64 expr) E1 E2 E2_real Gamma vR A fVars dVars. (!x. (toREnv E2) x = E2_real x) /\ validTypes (toRExp e) Gamma /\ approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real /\ @@ -866,6 +866,35 @@ val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE", \\ fs[GSYM float_is_zero_to_real, float_is_zero_def, mTypeToR_pos, perturb_def]) (* Division *) + >- (fs[fp64_div_def, fp64_to_float_float_to_fp64, evalBinop_def] + \\ `normal (evalBinop Div (float_to_real (fp64_to_float vF1)) + (float_to_real (fp64_to_float vF2))) M64` + by (rw_thm_asm `validFloatValue (_ / _) _` validFloatValue_def + \\ fs[normal_def, denormal_def, evalBinop_def] + >- (`abs (float_to_real (fp64_to_float vF1) / + float_to_real (fp64_to_float vF2)) < + abs (float_to_real (fp64_to_float vF1) / + float_to_real (fp64_to_float vF2))` + suffices_by (fs[]) + \\ irule REAL_LTE_TRANS + \\ asm_exists_tac \\ fs[]) + \\ qpat_x_assum `_ = 0` (fn thm => fs[thm]) + \\ fs[maxValue_def, maxExponent_def]) + \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`, + `(fp64_to_float vF2):(52,11) float`] + impl_subgoal_tac + float_div_relative + >- (rpt conj_tac + \\ fs[validFloatValue_def, + normalTranslatedValue_implies_finiteness, + denormalTranslatedValue_implies_finiteness, + normalValue_implies_normalization, + GSYM float_is_zero_to_real, float_is_finite, evalBinop_def]) + \\ fs[dmode_def] + \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`, + `float_to_real (fp64_to_float vF2)`, `e`] + \\ fs[perturb_def, evalBinop_def] + \\ fs[mTypeToR_def]) >- (fs[fp64_div_def, fp64_to_float_float_to_fp64, evalBinop_def] \\ `normal (evalBinop Div (float_to_real (fp64_to_float vF1)) (float_to_real (fp64_to_float vF2))) M64` @@ -978,41 +1007,11 @@ val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE", \\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`) \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def \\ fs[domain_union, DIFF_DEF, SUBSET_DEF]) - \\ fs[] - \\ rename1 `eval_expr_float e1 _ = SOME vF1` - \\ rename1 `eval_expr_float e2 _ = SOME vF2` - \\ rename1 `eval_expr_float e3 _ = SOME vF3` - \\ IMP_RES_TAC validRanges_single - \\ rename1 `FloverMapTree_find (toRExp e3) A = SOME (iv3, err3)` - \\ rename1 `FloverMapTree_find (toRExp e2) A = SOME (iv2, err2)` - \\ rename1 `FloverMapTree_find (toRExp e1) A = SOME (iv1, err1)` - \\ rename1 `eval_expr E1 _ (toREval (toRExp e3)) nR3 REAL` - \\ rename1 `eval_expr E1 _ (toREval (toRExp e2)) nR2 REAL` - \\ rename1 `eval_expr E1 _ (toREval (toRExp e1)) nR1 REAL` - (* Obtain evaluation for E2_real*) - \\ `!vF2 m2. eval_expr E2_real (toRExpMap Gamma) (toRExp e2) vF2 m2 ==> - abs (nR2 - vF2) <= err2` - by (qspecl_then [`toRExp e2`, `E1`, `E2_real`, `A`,`nR2`, - `err2`, `FST iv2`, `SND iv2`, `fVars`, - `dVars`,`Gamma`] destruct validErrorbound_sound - \\ rpt conj_tac \\ fs[] - >- (fs [DIFF_DEF, SUBSET_DEF] - \\ rpt strip_tac \\ first_x_assum irule - \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) - \\ Flover_compute ``validErrorbound``) - \\ `contained (float_to_real (fp64_to_float vF2)) - (widenInterval (FST iv2, SND iv2) err2)` - by (irule distance_gives_iv - \\ qexists_tac `nR2` \\ fs [contained_def] - \\ first_x_assum irule - \\ qexists_tac `M64` - \\ drule eval_eq_env - \\ rpt (disch_then drule) \\ fs[]) \\ fs[optionLift_def])); val bstep_gives_IEEE = store_thm ( "bstep_gives_IEEE", - ``!(f:word64 cmd) E1 E2 E2_real Gamma vR vF A P fVars dVars outVars. + ``!(f:word64 cmd) E1 E2 E2_real Gamma vR vF A fVars dVars outVars. (!x. (toREnv E2) x = E2_real x) /\ approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real /\ ssa (toRCmd f) (union fVars dVars) outVars /\ @@ -1047,91 +1046,58 @@ val bstep_gives_IEEE = store_thm ( \\ Flover_compute ``validErrorboundCmd`` \\ fs[] \\ rveq \\ fs[] >- (`?v_e. eval_expr_float e E2 = SOME v_e /\ - eval_expr (toREnv E2) Gamma (toRBMap fBits) (toRExp e) + eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp e) (float_to_real (fp64_to_float v_e)) M64` by (irule eval_expr_gives_IEEE \\ rpt conj_tac \\ fs[] - >- (rpt strip_tac \\ first_x_assum irule - \\ fs[Once freeVars_def, domain_union] - \\ CCONTR_TAC \\ fs[] \\ rveq \\ fs[] - \\ fs[SUBSET_DEF, domain_union] - \\ `n IN domain fVars \/ n IN domain dVars` - by (first_x_assum irule \\ fs[])) - >- (qexistsl_tac [`A`, `E1`, `E2_real`, `P`, `dVars`, `fVars`, `tMap`] - \\ Flover_compute ``validIntervalboundsCmd`` - \\ Flover_compute ``validErrorboundCmd`` - \\ Flover_compute ``typeCheckCmd`` - \\ fs [Once FPRangeValidatorCmd_def] - \\ rpt conj_tac \\ fs[] \\ rpt strip_tac - \\ fs[Once freeVars_def, domain_union, DIFF_DEF, SUBSET_DEF] - \\ rveq \\ fs[] + >- (fs[Once validTypesCmd_def]) + >- (find_exists_tac \\ fs[]) + \\ qexistsl_tac [`A`, `E1`, `E2_real`, `dVars`, `fVars`] + \\ rpt conj_tac \\ fs[] + \\ Flover_compute ``validErrorboundCmd`` + >- (fs[Once freeVars_def, domain_union, DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ `x IN domain fVars \/ x IN domain dVars` by (first_x_assum irule \\ fs[])) - \\ rveq \\ asm_exists_tac \\ fs[]) - \\ qspecl_then [`(toRExp e)`, `A`, `P`, `fVars`, `dVars`, `E1`, `Gamma`, `toRBMap fBits`] - destruct validIntervalbounds_sound - >- (fs[DIFF_DEF, SUBSET_DEF] - \\ rpt strip_tac \\ first_x_assum irule \\ fs[Once freeVars_def, domain_union] - \\ CCONTR_TAC \\ fs[] \\ rveq \\ fs[] - \\ `n IN domain fVars \/ n IN domain dVars` - by (first_x_assum irule \\ fs[])) - \\ qspecl_then [`toRCmd f`, `A`, `updEnv n v' E1`, `fVars`, `insert n () dVars`, `outVars`, - `P`, `updDefVars n M64 Gamma`, `toRBMap fBits`] destruct validIntervalboundsCmd_sound - >- (fs[] \\ rpt conj_tac - >- (irule ssa_equal_set - \\ qexists_tac `insert n () (union fVars dVars)` - \\ conj_tac \\ TRY (fs[] \\ FAIL_TAC "") - \\ rewrite_tac [domain_union, domain_insert] - \\ rewrite_tac [UNION_DEF, INSERT_DEF] - \\ fs[EXTENSION] - \\ rpt strip_tac - \\ metis_tac[]) - >- (fs[dVars_range_valid_def, DIFF_DEF, domain_insert, SUBSET_DEF] - \\ rpt strip_tac \\ fs[] - >- (rveq \\ metis_tac [meps_0_deterministic]) - \\ IF_CASES_TAC - >- (rveq \\ metis_tac [meps_0_deterministic]) - \\ first_x_assum irule \\ fs []) - >- (fs[fVars_P_sound_def] - \\ rpt strip_tac - \\ IF_CASES_TAC - >- (rveq \\ fs[DIFF_DEF, SUBSET_DEF, domain_union]) - \\ first_x_assum irule \\ fs[]) - >- (fs[vars_typed_def] - \\ rpt strip_tac - \\ TRY (first_x_assum irule \\ fs[domain_union] \\ rveq) - \\ IF_CASES_TAC \\ fs[]) - \\ fs [domain_union, Once freeVars_def, DIFF_DEF, SUBSET_DEF] - \\ rpt strip_tac \\ first_x_assum irule \\ fs[] - \\ simp[Once freeVars_def]) + >- (fs [Once FPRangeValidatorCmd_def]) + \\ fs[Once validRangesCmd_def]) + \\ fs[Once validRangesCmd_def] + \\ IMP_RES_TAC validRanges_single + \\ IMP_RES_TAC validRangesCmd_single + \\ fs[Once validTypesCmd_def] (* prove validity of errorbound for floating-point value *) \\ qspecl_then - [`toRExp e`, `E1`, `E2_real`, `A`, `v'`, `err_e`, `P`, - `FST iv_e`, `SND iv_e`, `fVars`, `dVars`, `tMap`, `Gamma`, `fBits`] + [`toRExp e`, `E1`, `E2_real`, `A`, `v'`, `err_e`, + `FST iv_e`, `SND iv_e`, `fVars`, `dVars`, `Gamma`] impl_subgoal_tac validErrorbound_sound >- (fs[DIFF_DEF, SUBSET_DEF] - \\ rpt strip_tac \\ first_x_assum irule \\ fs[Once freeVars_def, domain_union] + \\ rpt strip_tac \\ first_x_assum irule + \\ fs[Once freeVars_def, domain_union] \\ CCONTR_TAC \\ fs[] \\ rveq \\ fs[] \\ `n IN domain fVars \/ n IN domain dVars` by (first_x_assum irule \\ fs[])) \\ fs[] - \\ `abs (v' - (float_to_real (fp64_to_float v_e))) <= err_e` + \\ IMP_RES_TAC meps_0_deterministic \\ rveq + \\ rename1 `FST iv <= vR_e` \\ rename1 `FST iv_e <= vR_e` + \\ rename1 `abs (vR_e - nF) <= err_e` + \\ `abs (vR_e - (float_to_real (fp64_to_float v_e))) <= err_e` by (first_x_assum irule \\ fs[] - \\ qexists_tac `M64` \\ irule eval_eq_env \\ asm_exists_tac \\ fs[]) + \\ qexists_tac `M64` + \\ irule eval_eq_env \\ asm_exists_tac \\ fs[]) + \\ fs[getRetExp_def] \\ rename1 `FloverMapTree_find (getRetExp (toRCmd f)) A = SOME (iv_f, err_f)` (* Now construct a new evaluation according to our big-step semantics using lemma validErrorboundCmd_gives_eval *) \\ qspecl_then - [ `toRCmd f`, `A`, `updEnv n v' E1`, + [ `toRCmd f`, `A`, `updEnv n vR_e E1`, `updEnv n (float_to_real (fp64_to_float v_e)) E2_real`, `outVars`, `fVars`, `insert n () dVars`, `vR`, `FST iv_f`, `SND iv_f`, - `err_f`, `P`, `M64`, `tMap`, `updDefVars n M64 Gamma`, `fBits`] + `err_f`, `M64`, `Gamma`] impl_subgoal_tac validErrorboundCmd_gives_eval >- (fs[] \\ rpt conj_tac >- (irule approxUpdBound - \\ fs[lookup_NONE_domain]) + \\ fs[lookup_NONE_domain, toRExpMap_def]) >- (irule ssa_equal_set \\ qexists_tac `insert n () (union fVars dVars)` \\ conj_tac \\ TRY (fs[] \\ FAIL_TAC "") @@ -1143,63 +1109,32 @@ val bstep_gives_IEEE = store_thm ( >- (fs[DIFF_DEF, domain_insert, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ fs[Once freeVars_def] - \\ simp[Once freeVars_def, domain_union]) - >- (irule swap_Gamma_bstep - \\ qexists_tac `updDefVars n REAL (toRMap Gamma)` \\ fs[] - \\ strip_tac - \\ qspecl_then [`Gamma`, `n`, `M64`, `n'`] assume_tac Rmap_updVars_comm - \\ fs[updDefVars_def]) - >- (fs[dVars_range_valid_def] \\ rpt strip_tac \\ simp[updEnv_def] - \\ rveq \\ fs[] - >- (drule validIntervalbounds_sound - \\ rpt (disch_then drule) - \\ disch_then (qspecl_then [`fVars`, `E1`, `Gamma`, `toRBMap fBits`] - impl_subgoal_tac) - >- (fs[] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) - \\ fs[domain_union, DIFF_DEF, SUBSET_DEF, dVars_range_valid_def] - \\ rpt strip_tac \\ first_x_assum irule - \\ simp[Once freeVars_def, domain_union] - \\ CCONTR_TAC \\ fs[] - \\ rveq - \\ `n IN domain fVars \/ n IN domain dVars` - by (first_x_assum irule \\ fs[])) - \\ fs[] - \\ metis_tac [meps_0_deterministic]) - \\ IF_CASES_TAC \\ fs[] - \\ rveq - \\ fs[domain_union]) - >- (fs[fVars_P_sound_def] \\ rpt strip_tac \\ simp[updEnv_def] - \\ IF_CASES_TAC \\ fs[] - \\ rveq - \\ fs[domain_union]) - \\ fs[vars_typed_def] \\ rpt strip_tac \\ fs[updDefVars_def] - \\ IF_CASES_TAC \\ fs[] - \\ first_x_assum irule \\ fs[]) + \\ simp[Once freeVars_def, domain_union])) \\ fs[optionLift_def] - \\ `FloverMapTree_find (getRetExp (toRCmd f)) tMap= SOME M64` - by (irule typingSoundnessCmd - \\ qexistsl_tac [`updEnv n v (toREnv E2)`, - `updDefVars n M64 Gamma`, `fBits`, `vF`] - \\ fs[] - \\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def - \\ EVERY_CASE_TAC \\ fs[]\\ rveq \\ fs[]) - \\ `m' = M64` - by (irule typing_agrees_cmd - \\ rewrite_tac [CONJ_ASSOC] \\ once_rewrite_tac[CONJ_COMM] - \\ rpt (asm_exists_tac \\ fs[]) - \\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def - \\ EVERY_CASE_TAC \\ fs[] \\ rveq \\ fs[]) - \\ rveq \\ fs[bstep_cases, PULL_EXISTS] + (* \\ `FloverMapTree_find (getRetExp (toRCmd f)) Gamma = SOME M64` *) + (* by (irule typingSoundnessCmd *) + (* \\ qexistsl_tac [`updEnv n v (toREnv E2)`, *) + (* `updDefVars n M64 Gamma`, `fBits`, `vF`] *) + (* \\ fs[] *) + (* \\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def *) + (* \\ EVERY_CASE_TAC \\ fs[]\\ rveq \\ fs[]) *) + (* \\ `m' = M64` *) + (* by (irule typing_agrees_cmd *) + (* \\ rewrite_tac [CONJ_ASSOC] \\ once_rewrite_tac[CONJ_COMM] *) + (* \\ rpt (asm_exists_tac \\ fs[]) *) + (* \\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def *) + (* \\ EVERY_CASE_TAC \\ fs[] \\ rveq \\ fs[]) *) + (* \\ rveq \\ fs[bstep_cases, PULL_EXISTS] *) (* Instantiate IH with newly obtained evaluation, to get the conclusion *) \\ first_x_assum - (qspecl_then [`updEnv n v' E1`, `updFlEnv n v_e E2`, + (qspecl_then [`updEnv n vR_e E1`, `updFlEnv n v_e E2`, `updEnv n (float_to_real (fp64_to_float v_e)) E2_real`, - `updDefVars n M64 Gamma`, `tMap`, `vR`, `vF'`, `A`, - `P`, `fVars`, `insert n () dVars`, `outVars`, `fBits`] + `Gamma`, `vR`, `vF'`, `A`, `fVars`, + `insert n () dVars`, `outVars`] impl_subgoal_tac) - >- (simp[Once validErrorboundCmd_def, Once validIntervalboundsCmd_def] - \\ fs [Once FPRangeValidatorCmd_def] - \\ rveq \\ fs[] + >- (simp[Once validErrorboundCmd_def] + \\ fs [Once FPRangeValidatorCmd_def, Once validTypesCmd_def, + Once validRangesCmd_def] \\ rpt conj_tac >- (strip_tac \\ fs[updFlEnv_def, updEnv_def, toREnv_def] \\ IF_CASES_TAC \\ fs[]) @@ -1208,7 +1143,7 @@ val bstep_gives_IEEE = store_thm ( (qspecl_then [`M64`, `v'`, `float_to_real (fp64_to_float v_e)`, `n`] irule) - \\ fs[domain_lookup, lookup_NONE_domain]) + \\ fs[domain_lookup, lookup_NONE_domain, toRExpMap_def]) >- (irule ssa_equal_set \\ qexists_tac `insert n () (union fVars dVars)` \\ conj_tac \\ TRY (fs[] \\ FAIL_TAC "") @@ -1217,36 +1152,24 @@ val bstep_gives_IEEE = store_thm ( \\ fs[EXTENSION] \\ rpt strip_tac \\ metis_tac[]) - >- (irule swap_Gamma_bstep - \\ qexists_tac `updDefVars n REAL (toRMap Gamma)` \\ fs[] - \\ rpt strip_tac - \\ qspecl_then [`Gamma`, `n`, `M64`, `n'`] assume_tac Rmap_updVars_comm - \\ fs[updDefVars_def]) + >- (first_x_assum MATCH_ACCEPT_TAC) >- (irule bstep_eq_env \\ qexists_tac `updEnv n (float_to_real (fp64_to_float v_e)) E2_real` - \\ fs[] - \\ strip_tac \\ fs[updEnv_def, toREnv_def, updFlEnv_def] - \\ IF_CASES_TAC \\ fs[]) + \\ conj_tac + >- (strip_tac \\ fs[updEnv_def, toREnv_def, updFlEnv_def] + \\ IF_CASES_TAC \\ fs[]) + \\ reverse (sg `m' = M64`) + >- (rveq \\ fs[]) + \\ irule bstep_Gamma_det \\ rpt (find_exists_tac \\ fs[])) >- (fs[DIFF_DEF, domain_insert, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ fs[Once freeVars_def] \\ simp[Once freeVars_def, domain_union]) - >- (fs[dVars_range_valid_def] \\ rpt strip_tac \\ simp[updEnv_def] - >- (rveq \\ metis_tac [meps_0_deterministic]) - \\ IF_CASES_TAC \\ fs[] - \\ rveq - \\ fs[domain_union]) - >- (fs[fVars_P_sound_def] \\ rpt strip_tac \\ simp[updEnv_def] - \\ rveq \\ fs[] - \\ IF_CASES_TAC \\ rveq \\ fs[] - \\ fs[DIFF_DEF, SUBSET_DEF, domain_union]) - >- (fs[vars_typed_def] \\ rpt strip_tac \\ simp[updDefVars_def] - \\ IF_CASES_TAC \\ fs[]) >- (rpt strip_tac \\ simp[updEnv_def] \\ rveq \\ fs[] >- (irule FPRangeValidator_sound - \\ qexistsl_tac [`A`, `E1`, `E2_real`, `Gamma`, `P`, `dVars`, - `toRExp e`, `fBits`, `fVars`, `tMap`] + \\ qexistsl_tac [`A`, `E1`, `E2_real`, `Gamma`, `dVars`, + `toRExp e`, `fVars`] \\ fs[] \\ rpt conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) >- (fs[Once freeVars_def, domain_union, DIFF_DEF, SUBSET_DEF] @@ -1258,8 +1181,8 @@ val bstep_gives_IEEE = store_thm ( \\ asm_exists_tac \\ fs[]) \\ IF_CASES_TAC \\ fs[] \\ irule FPRangeValidator_sound - \\ qexistsl_tac [`A`, `E1`, `E2_real`, `Gamma`, `P`, `dVars`, - `toRExp e`, `fBits`, `fVars`, `tMap`] + \\ qexistsl_tac [`A`, `E1`, `E2_real`, `Gamma`, `dVars`, + `toRExp e`, `fVars`] \\ fs[] \\ rpt conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) >- (fs[Once freeVars_def, domain_union, DIFF_DEF, SUBSET_DEF] @@ -1268,129 +1191,317 @@ val bstep_gives_IEEE = store_thm ( \\ rveq \\ fs[] \\ metis_tac []) \\ irule eval_eq_env - \\ asm_exists_tac \\ fs[]) - \\ rpt strip_tac \\ simp [updDefVars_def] - \\ IF_CASES_TAC \\ fs[] - \\ first_x_assum irule \\ fs[] - \\ simp[Once freeVars_def, domain_union]) + \\ asm_exists_tac \\ fs[])) \\ fs[] - \\ qexists_tac `float_to_real (fp64_to_float v_e)` \\ fs[] - \\ irule bstep_eq_env \\ once_rewrite_tac[CONJ_COMM] - \\ asm_exists_tac \\ fs[] + \\ irule let_b \\ find_exists_tac + \\ fs[] \\ irule bstep_eq_env + \\ find_exists_tac \\ fs[] \\ strip_tac \\ fs[toREnv_def, updEnv_def, updFlEnv_def] \\ IF_CASES_TAC \\ fs[]) - >- (fs[bstep_cases] \\ irule eval_expr_gives_IEEE \\ rpt conj_tac - \\ fs[] - >- (rpt strip_tac \\ first_x_assum irule - \\ fs[freeVars_def] \\ fs[]) - >- (rewrite_tac [CONJ_ASSOC] - \\ rpt (once_rewrite_tac [CONJ_COMM] - \\ asm_exists_tac \\ fs[]) - \\ fs [Once validIntervalboundsCmd_def, Once validErrorboundCmd_def, - Once typeCheckCmd_def, Once FPRangeValidatorCmd_def] - \\ rpt conj_tac \\ fs[] \\ rpt strip_tac - >- (qpat_x_assum `!v. _ ==> ?vF m. _` (qspec_then `v` destruct) - \\ fs[freeVars_def]) - \\ fs[Once freeVars_def, domain_union, DIFF_DEF, SUBSET_DEF]) - \\ rveq \\ asm_exists_tac \\ fs[])); + >- (fs[bstep_cases] \\ drule eval_expr_gives_IEEE + \\ disch_then irule \\ rpt conj_tac + \\ fs[Once validTypesCmd_def] + >- (find_exists_tac \\ fs[]) + \\ qexistsl_tac [`A`, `E1`, `dVars`, `fVars`] + \\ rpt conj_tac + \\ fs[freeVars_def, Once FPRangeValidatorCmd_def, validRangesCmd_def])); + +val found_tac = TRY (last_x_assum irule \\ find_exists_tac \\ fs[] \\ FAIL_TAC "") + \\ first_x_assum irule \\ find_exists_tac \\ fs[]; + +val getValidMap_preserving = store_thm ( + "getValidMap_preserving", + ``! e defVars akk res. + (! e m. FloverMapTree_find e akk = SOME m ==> m = M64) /\ + is64BitEval e /\ + getValidMap defVars e akk = Succes res /\ + (! e m. FloverMapTree_find e defVars = SOME m ==> m = M64) ==> + ! e m. FloverMapTree_find e res = SOME m ==> m = M64``, + Induct_on `e` \\ once_rewrite_tac[getValidMap_def] \\ rpt strip_tac + >- (fs[] \\ Cases_on `FloverMapTree_mem (Var n) akk` \\ fs[] + >- (rveq \\ found_tac) + \\ EVERY_CASE_TAC \\ fs[] + \\ rveq \\ fs[map_find_add] + \\ Cases_on `e = Var n` \\ fs[] + \\ rveq \\ found_tac) + >- (fs[] \\ Cases_on `FloverMapTree_mem (Const m v) akk` \\ fs[] + >- (rveq \\ found_tac) + \\ Cases_on `FloverMapTree_find (Const m v) defVars` \\ fs[isMonotone_def] + >- (rveq \\ fs[map_find_add] + \\ Cases_on `e = Const m v` \\ fs[] \\ rveq + >- (fs[is64BitEval_def]) + \\ found_tac) + \\ Cases_on `x = m` \\ fs[] + \\ rveq \\ fs[map_find_add] + \\ Cases_on `e = Const m v` \\ fs[] \\ rveq + >- (fs[is64BitEval_def]) + \\ found_tac) + >- (fs[is64BitEval_def] + \\ Cases_on `FloverMapTree_mem (Unop u e) akk` \\ fs[] \\ rveq + >- (res_tac) + \\ Cases_on `getValidMap defVars e akk` \\ fs[] + \\ fs[option_case_eq] + \\ Cases_on `isFixedPoint m_e1` \\ fs[option_case_eq] + >- (Cases_on `isCompat m_e1 mFix` \\ fs[addMono_def, option_case_eq] + \\ rveq \\ fs[map_find_add] + \\ Cases_on `e' = Unop u e` \\ fs[] \\ rveq + >- (found_tac) + \\ res_tac) + \\ Cases_on `FloverMapTree_find (Unop u e) defVars` \\ fs[isMonotone_def] + >- (fs[addMono_def, option_case_eq] \\ rveq \\ fs[map_find_add] + \\ Cases_on `e' = Unop u e` \\ fs[] \\ rveq + >- (last_x_assum irule \\ fs[] + \\ qexistsl_tac [`akk`, `defVars`, `e`, `a`] + \\ fs[] \\ conj_tac \\ first_x_assum MATCH_ACCEPT_TAC) + \\ res_tac) + \\ Cases_on `x = m_e1` \\ fs[addMono_def, option_case_eq] \\ rveq \\ fs[map_find_add] + \\ Cases_on `e' = Unop u e` \\ fs[] \\ rveq + >- (last_x_assum irule \\ fs[] + \\ qexistsl_tac [`akk`, `defVars`, `e`, `a`] + \\ fs[] \\ conj_tac \\ first_x_assum MATCH_ACCEPT_TAC) + \\ res_tac) + >- (fs[is64BitEval_def] + \\ rename1 `Binop b e1 e2` + \\ Cases_on `FloverMapTree_mem (Binop b e1 e2) akk` \\ fs[] \\ rveq + >- (res_tac) + \\ Cases_on `getValidMap defVars e1 akk` \\ fs[] + \\ Cases_on `getValidMap defVars e2 a` \\ fs[] + \\ last_x_assum (qspecl_then [`defVars`, `akk`, `a`] destruct) + >- (fs[] \\ conj_tac \\ first_x_assum MATCH_ACCEPT_TAC) + \\ last_x_assum (qspecl_then [`defVars`, `a`, `a'`] destruct) + >- (fs[] \\ conj_tac \\ first_x_assum MATCH_ACCEPT_TAC) + \\ fs[option_case_eq] + \\ qpat_x_assum `_ = Succes res` mp_tac + \\ TOP_CASE_TAC \\ pop_assum kall_tac \\ fs[option_case_eq] + >- (rpt strip_tac \\ qpat_x_assum `_ = Succes res` mp_tac + \\ TOP_CASE_TAC \\ fs[addMono_def, option_case_eq] + \\ rpt strip_tac \\ rveq \\ fs[map_find_add] + \\ Cases_on `e'' = Binop b e1 e2` \\ fs[] + >- (rveq \\ metis_tac[]) + \\ metis_tac[]) + \\ rpt strip_tac \\ qpat_x_assum `_ = Succes res` mp_tac + \\ TOP_CASE_TAC \\ fs[addMono_def, option_case_eq] + \\ rpt strip_tac \\ rveq \\ fs[map_find_add] + \\ Cases_on `e'' = Binop b e1 e2` \\ fs[] + >- (rveq + \\ `t1 = M64` by (metis_tac[]) + \\ `t2 = M64` by (metis_tac[]) \\ rveq \\ fs[join_fl_def]) + \\ metis_tac[]) + >- (fs[is64BitEval_def] + \\ rename1 `Fma e1 e2 e3` + \\ qpat_x_assum `_ = Succes res` mp_tac + \\ TOP_CASE_TAC + >- (strip_tac \\ rveq \\ res_tac) + \\ Cases_on `getValidMap defVars e1 akk` + \\ rewrite_tac [ResultsTheory.result_bind_def] \\ BETA_TAC + \\ TRY (rpt (first_x_assum kall_tac) \\ strip_tac \\ fs[] \\ FAIL_TAC "") + \\ Cases_on `getValidMap defVars e2 a` + \\ rewrite_tac [ResultsTheory.result_bind_def] \\ BETA_TAC + \\ TRY (rpt (first_x_assum kall_tac) \\ strip_tac \\ fs[] \\ FAIL_TAC "") + \\ Cases_on `getValidMap defVars e3 a'` + \\ rewrite_tac [ResultsTheory.result_bind_def] \\ BETA_TAC + \\ TRY (rpt (first_x_assum kall_tac) \\ strip_tac \\ fs[] \\ FAIL_TAC "") + \\ last_x_assum (qspecl_then [`defVars`, `akk`, `a`] destruct) + >- (rpt conj_tac \\ first_x_assum MATCH_ACCEPT_TAC) + \\ last_x_assum (qspecl_then [`defVars`, `a`, `a'`] destruct) + >- (rpt conj_tac \\ first_x_assum MATCH_ACCEPT_TAC) + \\ last_x_assum (qspecl_then [`defVars`, `a'`, `a''`] destruct) + >- (rpt conj_tac \\ first_x_assum MATCH_ACCEPT_TAC) + \\ fs[option_case_eq] \\ strip_tac \\ fs[] + \\ qpat_x_assum `_ = Succes res` mp_tac + \\ TOP_CASE_TAC \\ pop_assum kall_tac \\ fs[option_case_eq] + >- (rpt strip_tac \\ qpat_x_assum `_ = Succes res` mp_tac + \\ TOP_CASE_TAC \\ fs[addMono_def, option_case_eq] + \\ rpt strip_tac \\ rveq \\ fs[map_find_add] + \\ Cases_on `e''' = Fma e1 e2 e3` \\ fs[] + >- (rveq \\ metis_tac[]) + \\ metis_tac[]) + \\ rpt strip_tac \\ qpat_x_assum `_ = Succes res` mp_tac + \\ TOP_CASE_TAC \\ fs[addMono_def, option_case_eq] + \\ rpt strip_tac \\ rveq \\ fs[map_find_add] + \\ Cases_on `e''' = Fma e1 e2 e3` \\ fs[] + >- (rveq + \\ `t1 = M64` by (metis_tac[]) + \\ `t2 = M64` by (metis_tac[]) + \\ `t3 = M64` by (metis_tac[]) \\ rveq \\ fs[join_fl3_def, join_fl_def]) + \\ metis_tac[]) + \\ qpat_x_assum `_ = Succes res` mp_tac + \\ TOP_CASE_TAC \\ fs[] + >- (strip_tac \\ rveq \\ res_tac) + \\ Cases_on `getValidMap defVars e akk` \\ fs[option_case_eq] + \\ rpt strip_tac \\ pop_assum mp_tac + \\ fs[is64BitEval_def] + \\ first_x_assum (qspecl_then [`defVars`, `akk`, `a`] destruct) + >- (rpt conj_tac \\ first_x_assum MATCH_ACCEPT_TAC) + \\ TOP_CASE_TAC \\ pop_assum kall_tac \\ fs[option_case_eq] + >- (rpt strip_tac \\ pop_assum mp_tac + \\ TOP_CASE_TAC \\ fs[addMono_def, option_case_eq] + \\ strip_tac \\ rveq \\ fs[map_find_add] + \\ Cases_on `e' = Downcast m e` \\ fs[] \\ rveq \\ metis_tac[]) + \\ TOP_CASE_TAC \\ fs[addMono_def, option_case_eq] + \\ strip_tac \\ rveq \\ fs[map_find_add] + \\ Cases_on `e' = Downcast M64 e` \\ fs[] \\ rveq + \\ res_tac); + >- (Cases_on `m = M64` \\ fs[] + >- (Cases_on `FloverMapTree_find (Downcast m e) defVars` \\ fs[] + >- (fs[isMonotone_def] + +val getValidMapCmd_preserving = store_thm ( + "getValidMapCmd_preserving", + ``! f defVars akk res. + (! e m. FloverMapTree_find e akk = SOME m ==> m = M64) /\ + is64BitBstep f /\ + getValidMapCmd defVars f akk = Succes res /\ + (! e m. FloverMapTree_find e defVars = SOME m ==> m = M64) ==> + ! e m. FloverMapTree_find e res = SOME m ==> m = M64``, + Induct_on `f` \\ once_rewrite_tac [getValidMapCmd_def] + \\ rpt strip_tac \\ fs[] + >- (Cases_on `getValidMap defVars e akk` \\ fs[option_case_eq] + \\ Cases_on `m = m_e` \\ fs[addMono_def] + \\ Cases_on `FloverMapTree_find (Var n) a` \\ fs[] + \\ rveq + \\ first_x_assum + (qspecl_then [`defVars`, `FloverMapTree_insert (Var n) m a`, `res`] destruct) + >- (fs[is64BitBstep_def] \\ conj_tac + >- (rpt strip_tac \\ fs[map_find_add] + \\ Cases_on `e'' = Var n` \\ fs[] + \\ irule getValidMap_preserving + \\ qexistsl_tac [`akk`, `defVars`, `e`, `e''`, `a`] + \\ rpt conj_tac \\ fs[]) + \\ first_x_assum MATCH_ACCEPT_TAC) + \\ first_x_assum irule + \\ find_exists_tac \\ fs[]) + \\ irule getValidMap_preserving + \\ qexistsl_tac [`akk`, `defVars`, `e`, `e'`, `res`] + \\ rpt conj_tac \\ fs[is64BitBstep_def]); val IEEE_connection_expr = store_thm ( "IEEE_connection_expr", - ``!(e:word64 expr) (A:analysisResult) (P:precond) E1 E2 defVars fVars fBits. - approxEnv E1 defVars A fVars LN (toREnv E2) /\ + ``!(e:word64 expr) (A:analysisResult) (P:precond) E1 E2 defVars fVars. is64BitEval (toRExp e) /\ + is64BitEnv defVars /\ noDowncast (toRExp e) /\ eval_expr_valid e E2 /\ fVars_P_sound fVars E1 P /\ (domain (usedVars (toRExp e))) SUBSET (domain fVars) /\ - (!v. v IN domain fVars ==> ?m. defVars v = SOME m) /\ - (!v. v IN domain (usedVars (toRExp e)) ==> defVars v = SOME M64) /\ - CertificateChecker (toRExp e) A P defVars fBits ==> - ?iv err vR vF. (* m, currently = M64 *) - FloverMapTree_find (toRExp e) A = SOME (iv, err) /\ - eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e)) vR REAL /\ - eval_expr_float e E2 = SOME vF /\ - eval_expr (toREnv E2) defVars (toRBMap fBits) (toRExp e) - (float_to_real (fp64_to_float vF)) M64 /\ - abs (vR - (float_to_real (fp64_to_float vF))) <= err``, - rpt strip_tac - \\ drule Certificate_checking_is_sound + CertificateChecker (toRExp e) A P defVars ==> + ? Gamma. + approxEnv E1 (toRExpMap Gamma) A fVars LN (toREnv E2) ==> + ?iv err vR vF. (* m, currently = M64 *) + FloverMapTree_find (toRExp e) A = SOME (iv, err) /\ + eval_expr E1 (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) vR REAL /\ + eval_expr_float e E2 = SOME vF /\ + eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp e) + (float_to_real (fp64_to_float vF)) M64 /\ + abs (vR - (float_to_real (fp64_to_float vF))) <= err``, + simp [CertificateChecker_def] + \\ rpt strip_tac + \\ Cases_on `getValidMap defVars (toRExp e) FloverMapTree_empty` \\ fs[] + \\ IMP_RES_TAC getValidMap_top_correct + \\ `validTypes (toRExp e) a` + by (first_x_assum irule + \\ fs[FloverMapTree_empty_def, FloverMapTree_mem_def, FloverMapTree_find_def]) + \\ `! e m. FloverMapTree_find e a = SOME m ==> m = M64` + by (rpt strip_tac \\ irule getValidMap_preserving + \\ qexistsl_tac [`FloverMapTree_empty`, `defVars`, `toRExp e`, `e'`, `a`] + \\ rpt conj_tac \\ rpt strip_tac + \\ fs[FloverMapTree_empty_def, FloverMapTree_find_def , is64BitEnv_def] + \\ first_x_assum irule \\ find_exists_tac \\ fs[]) + \\ qexists_tac `a` \\ rpt strip_tac + \\ drule validIntervalbounds_sound \\ rpt (disch_then drule) - \\ disch_then (qspecl_then [`toRExp e`, `P`, `fBits`] destruct) - \\ fs[fVars_P_sound_def] - \\ rpt strip_tac \\ asm_exists_tac - \\ fs[CertificateChecker_def] - \\ qspecl_then [`e`, `E1`, `E2`, `toREnv E2`, `defVars`, - `typeMap defVars (toRExp e) FloverMapTree_empty fBits`, `vF`, `A`, `P`, `fVars`, - `LN`, `fBits`] + \\ disch_then (qspecl_then [`fVars`,`E1`, `a`] destruct) + \\ fs[dVars_range_valid_def, fVars_P_sound_def] + \\ drule validErrorbound_sound + \\ rpt (disch_then drule) + \\ IMP_RES_TAC validRanges_single + \\ disch_then (qspecl_then [`vR`, `err`, `FST iv`, `SND iv`] destruct) + \\ fs[] + \\ qspecl_then [`e`, `E1`, `E2`, `toREnv E2`, `a`, `nF`, `A`, `fVars`, `LN`] destruct eval_expr_gives_IEEE - >- (rpt conj_tac \\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def] - \\ `FloverMapTree_find (toRExp e) (typeMap defVars (toRExp e) FloverMapTree_empty fBits) = SOME M64` - by (drule typing_expr_64bit - \\ rpt (disch_then drule) - \\ fs[]) - \\ `m = M64` - by (drule typing_agrees_expr - \\ rpt (disch_then drule) - \\ fs[]) - \\ fs[]) - \\ res_tac \\ fs[]); + >- (rpt conj_tac \\ fs[] + >- (`FloverMapTree_find (toRExp e) a = SOME M64` + by (irule typing_expr_64bit \\ fs[is64BitEnv_def] + \\ first_x_assum MATCH_ACCEPT_TAC) + \\ `m = M64` + by (irule validTypes_exec \\ rpt (find_exists_tac \\ fs[])) + \\ rveq \\ fs[]) + \\ fs[is64BitEnv_def] \\ first_x_assum MATCH_ACCEPT_TAC) + \\ rpt (find_exists_tac \\ fs[]) + \\ first_x_assum irule \\ find_exists_tac \\ fs[]); val IEEE_connection_cmds = store_thm ( "IEEE_connection_cmds", - ``!(f:word64 cmd) (A:analysisResult) (P:precond) E1 E2 defVars (fVars:num_set) fBits. - approxEnv E1 defVars A (freeVars (toRCmd f)) LN (toREnv E2) /\ + ``! (f:word64 cmd) (A:analysisResult) (P:precond) E1 E2 defVars (fVars:num_set). is64BitBstep (toRCmd f) /\ + is64BitEnv defVars /\ noDowncastFun (toRCmd f) /\ bstep_valid f E2 /\ fVars_P_sound fVars E1 P /\ - (∀v. v ∈ domain (freeVars (toRCmd f)) ⇒ defVars v = SOME M64) /\ (domain (freeVars (toRCmd f))) SUBSET (domain fVars) /\ - (!v. v IN domain fVars ==> ?m. defVars v = SOME m) /\ - CertificateCheckerCmd (toRCmd f) A P defVars fBits ==> - ?iv err vR vF. (* m, currently = M64 *) - FloverMapTree_find (getRetExp (toRCmd f)) A = SOME (iv, err) /\ - bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) (toRBMap fBits) vR REAL /\ - bstep_float f E2 = SOME vF /\ - bstep (toRCmd f) (toREnv E2) defVars (toRBMap fBits) - (float_to_real (fp64_to_float vF)) M64 /\ - abs (vR - (float_to_real (fp64_to_float vF))) <= err``, - rpt strip_tac - \\ qspecl_then - [`toRCmd f`, `A`, `P`, `defVars`, `E1`, `toREnv E2`, `fVars`, `fBits`] - impl_subgoal_tac - CertificateCmd_checking_is_sound - >- (fs[fVars_P_sound_def] - \\ rpt strip_tac \\ first_x_assum irule - \\ fs[SUBSET_DEF]) - \\ fs[CertificateCheckerCmd_def] + CertificateCheckerCmd (toRCmd f) A P defVars ==> + ? Gamma. + approxEnv E1 (toRExpMap Gamma) A (freeVars (toRCmd f)) LN (toREnv E2) ==> + ?iv err vR vF. (* m, currently = M64 *) + FloverMapTree_find (getRetExp (toRCmd f)) A = SOME (iv, err) /\ + bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\ + bstep_float f E2 = SOME vF /\ + bstep (toRCmd f) (toREnv E2) (toRExpMap Gamma) + (float_to_real (fp64_to_float vF)) M64 /\ + abs (vR - (float_to_real (fp64_to_float vF))) <= err``, + simp [CertificateCheckerCmd_def] + \\ rpt strip_tac + \\ Cases_on `getValidMapCmd defVars (toRCmd f) FloverMapTree_empty` \\ fs[] + \\ IMP_RES_TAC getValidMapCmd_correct + \\ `validTypesCmd (toRCmd f) a` + by (first_x_assum irule + \\ fs[FloverMapTree_empty_def, FloverMapTree_mem_def, FloverMapTree_find_def]) + \\ `! e m. FloverMapTree_find e a = SOME m ==> m = M64` + by (rpt strip_tac \\ irule getValidMapCmd_preserving + \\ qexistsl_tac [`FloverMapTree_empty`, `defVars`, `e`, `toRCmd f`, `a`] + \\ rpt conj_tac \\ rpt strip_tac + \\ fs[FloverMapTree_empty_def, FloverMapTree_find_def , is64BitEnv_def] + \\ first_x_assum irule \\ find_exists_tac \\ fs[]) + \\ qexists_tac `a` \\ rpt strip_tac \\ `?outVars. ssa (toRCmd f) (freeVars (toRCmd f)) outVars` - by (drule validSSA_sound - \\ rpt (disch_then drule) - \\ fs[]) - \\ qspecl_then [`f`, `E1`, `E2`, `toREnv E2`, `defVars`, - `typeMapCmd defVars (toRCmd f) FloverMapTree_empty fBits`, `vR`, `vF`, `A`, `P`, - `freeVars (toRCmd f)`, `LN`, `outVars`, `fBits`] - destruct - bstep_gives_IEEE - >- (rpt conj_tac \\ fs[dVars_range_valid_def, fVars_P_sound_def, vars_typed_def] - >-(`FloverMapTree_find (getRetExp (toRCmd f)) - (typeMapCmd defVars (toRCmd f) FloverMapTree_empty fBits) = SOME M64` - by (drule typing_cmd_64bit - \\ rpt (disch_then drule) - \\ fs[]) - \\ `m = M64` - by (drule typing_agrees_cmd - \\ rpt (disch_then drule) - \\ fs[]) - \\ fs[]) - \\ rpt strip_tac - \\ first_x_assum irule - \\ fs[SUBSET_DEF]) - \\ qexistsl_tac [`vR`, `v`] + by (match_mp_tac validSSA_sound \\ fs[]) + \\ qspecl_then + [`toRCmd f`, `A`, `E1`, `freeVars (toRCmd f)`, `LN`, `outVars`, `P`, `a`] + destruct validIntervalboundsCmd_sound + \\ fs[dVars_range_valid_def, fVars_P_sound_def] + >- (rpt strip_tac \\ first_x_assum irule \\ fs[SUBSET_DEF]) + \\ IMP_RES_TAC validRangesCmd_single + \\ qspecl_then + [`toRCmd f`, `A`, `E1`, `toREnv E2`, `outVars`, `freeVars (toRCmd f)`, `LN`, `vR`, `FST iv_e`, + `SND iv_e`, `err_e`, `M64`, `a`] + destruct validErrorboundCmd_gives_eval \\ fs[] - \\ first_x_assum irule - \\ asm_exists_tac \\ fs[]); + \\ rpt (find_exists_tac \\ fs[]) + \\ qspecl_then + [`f`, `E1`, `E2`, `toREnv E2`, `a`, `vR`, `vF`, `A`, `freeVars (toRCmd f)`, `LN`, `outVars`] + destruct + bstep_gives_IEEE + >- (fs[is64BitEnv_def] + \\ conj_tac + >- (`FloverMapTree_find (getRetExp (toRCmd f)) a = SOME M64` + by (irule typing_cmd_64bit + \\ fs[is64BitEnv_def] \\ first_x_assum MATCH_ACCEPT_TAC) + \\ `m = M64` + by (drule validTypesCmd_single + \\ disch_then assume_tac \\ fs[] + \\ fs[] \\ rveq \\ fs[] + \\ first_x_assum irule + \\ qexistsl_tac [`toREnv E2`, `a`, `vF`] \\ fs[]) + \\ rveq \\ fs[]) + \\ first_x_assum MATCH_ACCEPT_TAC) + \\ find_exists_tac \\ fs[] + \\ drule validErrorboundCmd_sound + \\ rpt (disch_then drule) + \\ rename1 `bstep (toRCmd f) (toREnv E2) _ vF2 m2` + \\ disch_then + (qspecl_then + [`outVars`, `vR`, `vF2`, `FST iv_e`, `SND iv_e`, `err_e`, `m2`] destruct) + \\ fs[]); val _ = export_theory (); -- GitLab