Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* This file was originally generated by why. It can be modified; only the generated parts will be overwritten. *) Require Export Why2Gappa. Require Export WhyFloatsStrictLegacy. Open Scope Z_scope. Local Coercion FtoRradix: Float.float >-> R. (*Why type*) Definition int32: Set. Admitted. (*Why logic*) Definition integer_of_int32 : int32 -> Z. Admitted. (* Why obligation from file "Malcolm.c", line 8, characters 21-35: *) (*Why goal*) Lemma malcolm1_ensures_default_po_1 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), (* JC_35 *) (* JC_32 *) (eq (double_value A) (powerRZ (2)%R (integer_of_int32 i))). Proof. intuition. rewrite HW_7, H; rewrite HW_9, HW_8. simpl; ring. Save. (* Why obligation from file "Malcolm.c", line 9, characters 15-21: *) (*Why goal*) Lemma malcolm1_ensures_default_po_2 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), (* JC_35 *) (* JC_33 *) 1 <= (integer_of_int32 i). Proof. intuition. rewrite HW_9; rewrite HW_8; auto with zarith. Save. (* Why obligation from file "Malcolm.c", line 9, characters 20-27: *) (*Why goal*) Lemma malcolm1_ensures_default_po_3 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), (* JC_35 *) (* JC_34 *) (integer_of_int32 i) <= 53. Proof. intuition. rewrite HW_9; rewrite HW_8; auto with zarith. Save. (* Why obligation from file "Malcolm.c", line 8, characters 21-35: *) (*Why goal*) Lemma malcolm1_ensures_default_po_4 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_35 *) ((* JC_32 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_33 *) 1 <= (integer_of_int32 i0) /\ (* JC_34 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (result2: double), forall (HW_13: (add_double_post nearest_even A0 result1 result2)), forall (HW_14: ~(eq (double_value A0) (double_value result2))), forall (result3: double), forall (HW_15: (eq (double_value result3) (2)%R) /\ (eq (double_exact result3) (2)%R) /\ (eq (double_model result3) (2)%R)), forall (result4: double), forall (HW_16: (mul_double_post nearest_even A0 result3 result4)), forall (A1: double), forall (HW_17: A1 = result4), forall (result5: int32), forall (HW_18: (integer_of_int32 result5) = ((integer_of_int32 i0) + 1)), forall (i1: int32), forall (HW_19: i1 = result5), (* JC_35 *) (* JC_32 *) (eq (double_value A1) (powerRZ (2)%R (integer_of_int32 i1))). Proof. intuition. why2float. rewrite HW_19; rewrite HW_18; rewrite powerRZ_add; auto with real. rewrite <- H1; simpl; ring_simplify. rewrite H15; rewrite HW_16. replace (FtoRradix result3) with 2%R. assert (2 * A0=(FtoRradix (Float (Float.Fnum A0) (Float.Fexp A0+1))))%R. unfold FtoRradix, FtoR; simpl; rewrite powerRZ_add; auto with real. simpl; ring. rewrite H1, <- H0; rewrite Rmult_comm; rewrite H21; unfold FtoRradix. apply sym_eq; apply RoundedModeProjectorIdemEq with bdouble 53%nat (EvenClosest bdouble radix 53); try apply pdGivesBound; auto with zarith. assert (Fbounded bdouble A0); auto with zarith. destruct H22; split. apply Zle_lt_trans with (2:=H22); auto with zarith. apply Zle_trans with (1:=H23); simpl; auto with zarith. Save. (* Why obligation from file "Malcolm.c", line 9, characters 15-21: *) (*Why goal*) Lemma malcolm1_ensures_default_po_5 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_35 *) ((* JC_32 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_33 *) 1 <= (integer_of_int32 i0) /\ (* JC_34 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (result2: double), forall (HW_13: (add_double_post nearest_even A0 result1 result2)), forall (HW_14: ~(eq (double_value A0) (double_value result2))), forall (result3: double), forall (HW_15: (eq (double_value result3) (2)%R) /\ (eq (double_exact result3) (2)%R) /\ (eq (double_model result3) (2)%R)), forall (result4: double), forall (HW_16: (mul_double_post nearest_even A0 result3 result4)), forall (A1: double), forall (HW_17: A1 = result4), forall (result5: int32), forall (HW_18: (integer_of_int32 result5) = ((integer_of_int32 i0) + 1)), forall (i1: int32), forall (HW_19: i1 = result5), (* JC_35 *) (* JC_33 *) 1 <= (integer_of_int32 i1). Proof. intuition. rewrite HW_19; rewrite HW_18; auto with zarith. Save. (* Why obligation from file "Malcolm.c", line 9, characters 20-27: *) (*Why goal*) Lemma malcolm1_ensures_default_po_6 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_35 *) ((* JC_32 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_33 *) 1 <= (integer_of_int32 i0) /\ (* JC_34 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (result2: double), forall (HW_13: (add_double_post nearest_even A0 result1 result2)), forall (HW_14: ~(eq (double_value A0) (double_value result2))), forall (result3: double), forall (HW_15: (eq (double_value result3) (2)%R) /\ (eq (double_exact result3) (2)%R) /\ (eq (double_model result3) (2)%R)), forall (result4: double), forall (HW_16: (mul_double_post nearest_even A0 result3 result4)), forall (A1: double), forall (HW_17: A1 = result4), forall (result5: int32), forall (HW_18: (integer_of_int32 result5) = ((integer_of_int32 i0) + 1)), forall (i1: int32), forall (HW_19: i1 = result5), (* JC_35 *) (* JC_34 *) (integer_of_int32 i1) <= 53. Proof. intuition. rewrite HW_19; rewrite HW_18. assert (53 <= integer_of_int32 i0 -> False); auto with zarith. intros. apply HW_14. why2float. rewrite HW_13. replace (FtoRradix result1) with 1%R. clear -H0 H9 A0_C. generalize H9 H0; generalize (integer_of_int32 i0). clear H9 H0; intros. case (Zle_lt_or_eq 53 z H9); intros. apply ImplyClosestStrict with bdouble 53%nat (A0+1)%R (z-52); try apply pdGivesBound; auto with zarith. replace (z - 52 + 53%nat - 1) with z. rewrite H0; auto with real. simpl; auto with zarith. replace (z - 52 + 53%nat - 1) with z. fold FtoRradix; rewrite H0; auto with real. simpl; auto with zarith. simpl; auto with zarith. fold FtoRradix; ring_simplify (A0+1-A0)%R. rewrite Rabs_right; try apply Rle_ge; auto with real. apply Rlt_le_trans with 2%R; auto with real. apply Rle_trans with ((powerRZ radix 2)/2)%R. right; simpl; field. unfold Rdiv; apply Rmult_le_compat_r; auto with real. apply Rle_powerRZ; auto with real zarith. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. generalize EvenClosestUniqueP; unfold UniqueP. intros T; unfold FtoRradix; apply T with bdouble 53%nat (A0+1)%R; clear T; try apply pdGivesBound; auto with zarith. split. apply ImplyClosest with 53%nat 1%Z; try apply pdGivesBound; auto with zarith. replace (1 + 53%nat - 1) with 53%Z. rewrite H0; rewrite <- H; auto with real. simpl; auto with zarith. fold FtoRradix; replace (1 + 53%nat - 1) with 53%Z; auto with real zarith. rewrite H0; rewrite <- H; auto with real. fold FtoRradix; ring_simplify (A0+1-A0)%R. rewrite Rabs_right; try apply Rle_ge; auto with real. right; simpl; field. left; unfold FNeven. rewrite FcanonicUnique with radix bdouble 53%nat (Fnormalize radix bdouble 53 A0) (Float (nNormMin 2%nat 53%nat) 1%Z). apply FevenNormMin; auto with zarith. apply bdouble. auto with zarith. auto with zarith. apply pdGivesBound. apply FnormalizeCanonic; try apply pdGivesBound; auto with zarith. left; split; try split. replace (Float.Fnum (Float (nNormMin 2%nat 53) 1)) with (nNormMin 2%nat 53) by reflexivity. rewrite Zabs_eq. apply ZltNormMinVnum; auto with zarith. apply Zlt_le_weak; apply nNormPos; auto with zarith. simpl; auto with zarith. replace (Float.Fnum (Float (nNormMin 2%nat 53) 1)) with (nNormMin 2%nat 53) by reflexivity. replace (Z_of_nat 2) with radix by reflexivity. rewrite <- PosNormMin with radix bdouble 53%nat. rewrite Zabs_eq. apply Zle_refl. rewrite pdGivesBound; auto with zarith. auto with zarith. apply pdGivesBound. rewrite FnormalizeCorrect;[idtac|auto with zarith]. fold FtoRradix; rewrite H0; rewrite <- H. unfold FtoRradix, FtoR. replace (Float.Fnum (Float (nNormMin 2%nat 53) 1)) with (nNormMin 2%nat 53) by reflexivity. replace (Float.Fexp (Float (nNormMin 2%nat 53) 1)) with 1 by reflexivity. unfold nNormMin; rewrite Zpower_nat_powerRZ. rewrite <- powerRZ_add; auto with real. Save. (* Why obligation from file "Malcolm.c", line 17, characters 13-33: *) (*Why goal*) Lemma malcolm1_ensures_default_po_7 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_35 *) ((* JC_32 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_33 *) 1 <= (integer_of_int32 i0) /\ (* JC_34 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (result2: double), forall (HW_13: (add_double_post nearest_even A0 result1 result2)), forall (HW_20: (eq (double_value A0) (double_value result2))), (* JC_41 *) (integer_of_int32 i0) = 53. Proof. intuition. case (Zle_lt_or_eq (integer_of_int32 i0) 53 H5); trivial; intros. absurd (double_value A0 = double_value A0 +1)%R. auto with real. rewrite HW_20 at 1. why2float. rewrite HW_13. replace (FtoRradix result1) with 1%R. assert (exists f:float, Fbounded bdouble f /\ (FtoRradix f=FtoRradix A0+1)%R). exists (Float (Zpower_nat radix (Zabs_nat (integer_of_int32 i0)) + 1) 0). split; try split. replace (Float.Fnum (Float (Zpower_nat radix (Zabs_nat (integer_of_int32 i0)) + 1) 0)) with (Zpower_nat radix (Zabs_nat (integer_of_int32 i0)) + 1) by reflexivity. rewrite pdGivesBound. apply lt_IZR. rewrite <- Rabs_Zabs; rewrite plus_IZR. replace radix with (Z_of_nat 2%nat) by reflexivity. repeat rewrite Zpower_nat_powerRZ. rewrite Rabs_right. apply Rle_lt_trans with (powerRZ 2%nat 52 + 1%Z)%R. apply Rplus_le_compat_r; apply Rle_powerRZ; auto with zarith real. rewrite inj_abs; auto with zarith. apply Rlt_le_trans with (powerRZ 2%nat 52 + powerRZ 2%nat 52)%R. apply Rplus_lt_compat_l; apply Rle_lt_trans with (powerRZ 2%nat 0). simpl; right; ring. apply Rlt_powerRZ; auto with real zarith. apply Rle_trans with (powerRZ 2%nat 1*powerRZ 2%nat 52)%R. simpl (powerRZ 2%nat 1); right; ring. rewrite <- powerRZ_add; auto with real zarith. apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real. apply Rplus_le_compat; auto with real zarith. simpl; auto with zarith. rewrite H0; unfold FtoRradix, FtoR. replace (Float.Fnum (Float (Zpower_nat radix (Zabs_nat (integer_of_int32 i0)) + 1) 0)) with (Zpower_nat radix (Zabs_nat (integer_of_int32 i0)) + 1) by reflexivity. replace (powerRZ radix (Float.Fexp (Float (Zpower_nat radix (Zabs_nat (integer_of_int32 i0)) + 1) 0))) with 1%R by reflexivity. rewrite Rmult_1_r; rewrite plus_IZR. replace radix with (Z_of_nat 2%nat) by reflexivity. rewrite Zpower_nat_powerRZ; simpl (IZR 1). rewrite inj_abs; auto with zarith real. destruct H14 as (ff, (K1,K2)). rewrite <- K2; apply sym_eq. apply RoundedModeProjectorIdemEq with bdouble 53%nat (EvenClosest bdouble radix 53%nat); try apply pdGivesBound; auto with zarith float. Save. (* Why obligation from file "Malcolm.c", line 17, characters 13-33: *) (*Why goal*) Lemma malcolm1_ensures_default_po_8 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_35 *) ((* JC_32 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_33 *) 1 <= (integer_of_int32 i0) /\ (* JC_34 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (result2: double), forall (HW_13: (add_double_post nearest_even A0 result1 result2)), forall (HW_20: (eq (double_value A0) (double_value result2))), (* JC_41 *) (eq (double_value A0) (1 * 9007199254740992)%R). Proof. intuition. assert (integer_of_int32 i0 = 53). apply malcolm1_ensures_default_po_7 with result A result0 i A0 result1 result2; auto. rewrite H0; rewrite H6. simpl; ring. Save. (* Why obligation from file "Malcolm.c", line 22, characters 20-26: *) (*Why goal*) Lemma malcolm1_ensures_default_po_9 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_35 *) ((* JC_32 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_33 *) 1 <= (integer_of_int32 i0) /\ (* JC_34 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (result2: double), forall (HW_13: (add_double_post nearest_even A0 result1 result2)), forall (HW_20: (eq (double_value A0) (double_value result2))), forall (HW_21: (* JC_41 *) ((integer_of_int32 i0) = 53 /\ (eq (double_value A0) (1 * 9007199254740992)%R))), forall (result3: double), forall (HW_22: (eq (double_value result3) (1)%R) /\ (eq (double_exact result3) (1)%R) /\ (eq (double_model result3) (1)%R)), forall (B: double), forall (HW_23: B = result3), forall (result4: int32), forall (HW_24: (integer_of_int32 result4) = 1), forall (i1: int32), forall (HW_25: i1 = result4), (* JC_44 *) (* JC_42 *) (eq (double_value B) (IZR (integer_of_int32 i1))). Proof. intuition. rewrite HW_23; rewrite HW_25; rewrite HW_24; rewrite H10;reflexivity. Save. (* Why obligation from file "Malcolm.c", line 22, characters 30-46: *) (*Why goal*) Lemma malcolm1_ensures_default_po_10 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_35 *) ((* JC_32 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_33 *) 1 <= (integer_of_int32 i0) /\ (* JC_34 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (result2: double), forall (HW_13: (add_double_post nearest_even A0 result1 result2)), forall (HW_20: (eq (double_value A0) (double_value result2))), forall (HW_21: (* JC_41 *) ((integer_of_int32 i0) = 53 /\ (eq (double_value A0) (1 * 9007199254740992)%R))), forall (result3: double), forall (HW_22: (eq (double_value result3) (1)%R) /\ (eq (double_exact result3) (1)%R) /\ (eq (double_model result3) (1)%R)), forall (B: double), forall (HW_23: B = result3), forall (result4: int32), forall (HW_24: (integer_of_int32 result4) = 1), forall (i1: int32), forall (HW_25: i1 = result4), (* JC_44 *) (* JC_43 *) ((integer_of_int32 i1) = 1 \/ (integer_of_int32 i1) = 2). Proof. intuition. rewrite HW_25; rewrite HW_24; auto. Save. (* Why obligation from file "Malcolm.c", line 22, characters 20-26: *) (*Why goal*) Lemma malcolm1_ensures_default_po_11 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_35 *) ((* JC_32 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_33 *) 1 <= (integer_of_int32 i0) /\ (* JC_34 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (result2: double), forall (HW_13: (add_double_post nearest_even A0 result1 result2)), forall (HW_20: (eq (double_value A0) (double_value result2))), forall (HW_21: (* JC_41 *) ((integer_of_int32 i0) = 53 /\ (eq (double_value A0) (1 * 9007199254740992)%R))), forall (result3: double), forall (HW_22: (eq (double_value result3) (1)%R) /\ (eq (double_exact result3) (1)%R) /\ (eq (double_model result3) (1)%R)), forall (B: double), forall (HW_23: B = result3), forall (result4: int32), forall (HW_24: (integer_of_int32 result4) = 1), forall (i1: int32), forall (HW_25: i1 = result4), forall (B0: double), forall (i2: int32), forall (HW_26: (* JC_44 *) ((* JC_42 *) (eq (double_value B0) (IZR (integer_of_int32 i2))) /\ (* JC_43 *) ((integer_of_int32 i2) = 1 \/ (integer_of_int32 i2) = 2))), forall (result5: double), forall (HW_28: (add_double_post nearest_even A0 B0 result5)), forall (result6: double), forall (HW_29: (sub_double_post nearest_even result5 A0 result6)), forall (HW_30: ~(eq (double_value result6) (double_value B0))), forall (result7: double), forall (HW_31: (eq (double_value result7) (1)%R) /\ (eq (double_exact result7) (1)%R) /\ (eq (double_model result7) (1)%R)), forall (result8: double), forall (HW_32: (add_double_post nearest_even B0 result7 result8)), forall (B1: double), forall (HW_33: B1 = result8), forall (result9: int32), forall (HW_34: (integer_of_int32 result9) = ((integer_of_int32 i2) + 1)), forall (i3: int32), forall (HW_35: i3 = result9), (* JC_44 *) (* JC_42 *) (eq (double_value B1) (IZR (integer_of_int32 i3))). Proof. intuition. rewrite HW_35; rewrite HW_34; rewrite H15. why2gappa. rewrite H26, HW_32, H14, H11, H15. simpl; gappa. rewrite HW_35; rewrite HW_34; rewrite H15. why2gappa. rewrite H26; rewrite HW_32; rewrite H14; rewrite H11; rewrite H15. simpl; ring_simplify (2+1)%R; gappa. Save. (* Why obligation from file "Malcolm.c", line 22, characters 30-46: *) (*Why goal*) Lemma malcolm1_ensures_default_po_12 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_35 *) ((* JC_32 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_33 *) 1 <= (integer_of_int32 i0) /\ (* JC_34 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (result2: double), forall (HW_13: (add_double_post nearest_even A0 result1 result2)), forall (HW_20: (eq (double_value A0) (double_value result2))), forall (HW_21: (* JC_41 *) ((integer_of_int32 i0) = 53 /\ (eq (double_value A0) (1 * 9007199254740992)%R))), forall (result3: double), forall (HW_22: (eq (double_value result3) (1)%R) /\ (eq (double_exact result3) (1)%R) /\ (eq (double_model result3) (1)%R)), forall (B: double), forall (HW_23: B = result3), forall (result4: int32), forall (HW_24: (integer_of_int32 result4) = 1), forall (i1: int32), forall (HW_25: i1 = result4), forall (B0: double), forall (i2: int32), forall (HW_26: (* JC_44 *) ((* JC_42 *) (eq (double_value B0) (IZR (integer_of_int32 i2))) /\ (* JC_43 *) ((integer_of_int32 i2) = 1 \/ (integer_of_int32 i2) = 2))), forall (result5: double), forall (HW_28: (add_double_post nearest_even A0 B0 result5)), forall (result6: double), forall (HW_29: (sub_double_post nearest_even result5 A0 result6)), forall (HW_30: ~(eq (double_value result6) (double_value B0))), forall (result7: double), forall (HW_31: (eq (double_value result7) (1)%R) /\ (eq (double_exact result7) (1)%R) /\ (eq (double_model result7) (1)%R)), forall (result8: double), forall (HW_32: (add_double_post nearest_even B0 result7 result8)), forall (B1: double), forall (HW_33: B1 = result8), forall (result9: int32), forall (HW_34: (integer_of_int32 result9) = ((integer_of_int32 i2) + 1)), forall (i3: int32), forall (HW_35: i3 = result9), (* JC_44 *) (* JC_43 *) ((integer_of_int32 i3) = 1 \/ (integer_of_int32 i3) = 2). Proof. intros. destruct HW_26; case H0; intros. right; rewrite HW_35; rewrite HW_34; rewrite H1; reflexivity. absurd (double_value result6 = double_value B0); try apply HW_30. destruct HW_29; destruct HW_28; destruct HW_20; why2gappa. rewrite H2; rewrite H4; rewrite (proj1 HW_10),H. destruct HW_21; rewrite H19, H1. simpl; rewrite Rmult_1_r. ring_simplify (9007199254740992 + 2)%R. replace (round radix2 (FLT_exp (-1074) 53) ZnearestE 9007199254740994) with 9007199254740994%R. ring_simplify ((9007199254740994 - 9007199254740992))%R. gappa. apply sym_eq; gappa. Save. (* Why obligation from file "Malcolm.c", line 1, characters 12-25: *) (*Why goal*) Lemma malcolm1_ensures_default_po_13 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_35 *) ((* JC_32 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_33 *) 1 <= (integer_of_int32 i0) /\ (* JC_34 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (result2: double), forall (HW_13: (add_double_post nearest_even A0 result1 result2)), forall (HW_20: (eq (double_value A0) (double_value result2))), forall (HW_21: (* JC_41 *) ((integer_of_int32 i0) = 53 /\ (eq (double_value A0) (1 * 9007199254740992)%R))), forall (result3: double), forall (HW_22: (eq (double_value result3) (1)%R) /\ (eq (double_exact result3) (1)%R) /\ (eq (double_model result3) (1)%R)), forall (B: double), forall (HW_23: B = result3), forall (result4: int32), forall (HW_24: (integer_of_int32 result4) = 1), forall (i1: int32), forall (HW_25: i1 = result4), forall (B0: double), forall (i2: int32), forall (HW_26: (* JC_44 *) ((* JC_42 *) (eq (double_value B0) (IZR (integer_of_int32 i2))) /\ (* JC_43 *) ((integer_of_int32 i2) = 1 \/ (integer_of_int32 i2) = 2))), forall (result5: double), forall (HW_28: (add_double_post nearest_even A0 B0 result5)), forall (result6: double), forall (HW_29: (sub_double_post nearest_even result5 A0 result6)), forall (HW_36: (eq (double_value result6) (double_value B0))), forall (why__return: double), forall (HW_37: why__return = B0), (* JC_5 *) (eq (double_value why__return) (2)%R). Proof. intuition. absurd (double_value result6 = double_value B0); try apply HW_36. why2gappa. rewrite HW_29,HW_28, H11, H15, H9. simpl. replace (round radix2 (FLT_exp (-1074) 53) ZnearestE (round radix2 (FLT_exp (-1074) 53) ZnearestE (1 * 9007199254740992 + 1) - 1 * 9007199254740992)) with 0%R. auto with real. rewrite Rmult_1_l. ring_simplify (9007199254740992 + 1)%R. replace (round radix2 (FLT_exp (-1074) 53) ZnearestE 9007199254740993) with 9007199254740992%R. ring_simplify ((9007199254740992 - 9007199254740992))%R. apply sym_eq, round_0. apply valid_rnd_N. assert (9007199254740992%R <= round radix2 (FLT_exp (-1074) 53) ZnearestE 9007199254740993 <= 9007199254740992%R)%R. gappa. now apply Rle_antisym. rewrite HW_37; rewrite H11; rewrite H15; reflexivity. Save. (* Why obligation from file "Malcolm.c", line 12, characters 15-18: *) (*Why goal*) Lemma malcolm1_safety_po_1 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_14 *) True), forall (HW_11: (* JC_12 *) ((* JC_9 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_10 *) 1 <= (integer_of_int32 i0) /\ (* JC_11 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), (no_overflow_double nearest_even (Rplus (double_value A0) (double_value result1))). Proof. intuition. unfold no_overflow_double. why2gappa. assert (2 <= A0 <= powerRZ 2 53)%R. rewrite H0; split. apply Rle_trans with (powerRZ 2 1);[right; simpl; ring|idtac]. apply Rle_powerRZ; auto with real zarith. apply Rle_powerRZ; auto with real zarith. gappa. Save. (* Why obligation from file "Malcolm.c", line 13, characters 4-10: *) (*Why goal*) Lemma malcolm1_safety_po_2 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_14 *) True), forall (HW_11: (* JC_12 *) ((* JC_9 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_10 *) 1 <= (integer_of_int32 i0) /\ (* JC_11 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (HW_13: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value result1)))), forall (result2: double), forall (HW_14: (add_double_post nearest_even A0 result1 result2)), forall (HW_15: ~(eq (double_value A0) (double_value result2))), forall (result3: double), forall (HW_16: (eq (double_value result3) (2)%R) /\ (eq (double_exact result3) (2)%R) /\ (eq (double_model result3) (2)%R)), (no_overflow_double nearest_even (Rmult (double_value A0) (double_value result3))). Proof. intuition. unfold no_overflow_double; why2gappa. assert (2 <= A0 <= powerRZ 2 53)%R. rewrite H0; split. apply Rle_trans with (powerRZ 2 1);[right; simpl; ring|idtac]. apply Rle_powerRZ; auto with real zarith. apply Rle_powerRZ; auto with real zarith. gappa. Save. (* Why obligation from file "Malcolm.c", line 14, characters 14-17: *) (*Why goal*) Lemma malcolm1_safety_po_3 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_14 *) True), forall (HW_11: (* JC_12 *) ((* JC_9 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_10 *) 1 <= (integer_of_int32 i0) /\ (* JC_11 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (HW_13: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value result1)))), forall (result2: double), forall (HW_14: (add_double_post nearest_even A0 result1 result2)), forall (HW_15: ~(eq (double_value A0) (double_value result2))), forall (result3: double), forall (HW_16: (eq (double_value result3) (2)%R) /\ (eq (double_exact result3) (2)%R) /\ (eq (double_model result3) (2)%R)), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value A0) (double_value result3)))), forall (result4: double), forall (HW_18: (mul_double_post nearest_even A0 result3 result4)), forall (A1: double), forall (HW_19: A1 = result4), (-2147483648) <= ((integer_of_int32 i0) + 1). Proof. intuition. Save. (* Why obligation from file "Malcolm.c", line 14, characters 14-17: *) (*Why goal*) Lemma malcolm1_safety_po_4 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_14 *) True), forall (HW_11: (* JC_12 *) ((* JC_9 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_10 *) 1 <= (integer_of_int32 i0) /\ (* JC_11 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (HW_13: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value result1)))), forall (result2: double), forall (HW_14: (add_double_post nearest_even A0 result1 result2)), forall (HW_15: ~(eq (double_value A0) (double_value result2))), forall (result3: double), forall (HW_16: (eq (double_value result3) (2)%R) /\ (eq (double_exact result3) (2)%R) /\ (eq (double_model result3) (2)%R)), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value A0) (double_value result3)))), forall (result4: double), forall (HW_18: (mul_double_post nearest_even A0 result3 result4)), forall (A1: double), forall (HW_19: A1 = result4), ((integer_of_int32 i0) + 1) <= 2147483647. Proof. intuition. Save. (* Why obligation from file "Malcolm.c", line 10, characters 19-25: *) (*Why goal*) Lemma malcolm1_safety_po_5 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_14 *) True), forall (HW_11: (* JC_12 *) ((* JC_9 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_10 *) 1 <= (integer_of_int32 i0) /\ (* JC_11 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (HW_13: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value result1)))), forall (result2: double), forall (HW_14: (add_double_post nearest_even A0 result1 result2)), forall (HW_15: ~(eq (double_value A0) (double_value result2))), forall (result3: double), forall (HW_16: (eq (double_value result3) (2)%R) /\ (eq (double_exact result3) (2)%R) /\ (eq (double_model result3) (2)%R)), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value A0) (double_value result3)))), forall (result4: double), forall (HW_18: (mul_double_post nearest_even A0 result3 result4)), forall (A1: double), forall (HW_19: A1 = result4), forall (HW_20: (-2147483648) <= ((integer_of_int32 i0) + 1) /\ ((integer_of_int32 i0) + 1) <= 2147483647), forall (result5: int32), forall (HW_21: (integer_of_int32 result5) = ((integer_of_int32 i0) + 1)), forall (i1: int32), forall (HW_22: i1 = result5), 0 <= ((* JC_19 *) (53 - (integer_of_int32 i0))). Proof. intuition. Save. (* Why obligation from file "Malcolm.c", line 10, characters 19-25: *) (*Why goal*) Lemma malcolm1_safety_po_6 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_14 *) True), forall (HW_11: (* JC_12 *) ((* JC_9 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_10 *) 1 <= (integer_of_int32 i0) /\ (* JC_11 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (HW_13: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value result1)))), forall (result2: double), forall (HW_14: (add_double_post nearest_even A0 result1 result2)), forall (HW_15: ~(eq (double_value A0) (double_value result2))), forall (result3: double), forall (HW_16: (eq (double_value result3) (2)%R) /\ (eq (double_exact result3) (2)%R) /\ (eq (double_model result3) (2)%R)), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value A0) (double_value result3)))), forall (result4: double), forall (HW_18: (mul_double_post nearest_even A0 result3 result4)), forall (A1: double), forall (HW_19: A1 = result4), forall (HW_20: (-2147483648) <= ((integer_of_int32 i0) + 1) /\ ((integer_of_int32 i0) + 1) <= 2147483647), forall (result5: int32), forall (HW_21: (integer_of_int32 result5) = ((integer_of_int32 i0) + 1)), forall (i1: int32), forall (HW_22: i1 = result5), ((* JC_19 *) (53 - (integer_of_int32 i1))) < ((* JC_19 *) (53 - (integer_of_int32 i0))). Proof. intuition. rewrite HW_22; rewrite HW_21. auto with zarith. Save. (* Why obligation from file "Malcolm.c", line 25, characters 10-13: *) (*Why goal*) Lemma malcolm1_safety_po_7 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_14 *) True), forall (HW_11: (* JC_12 *) ((* JC_9 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_10 *) 1 <= (integer_of_int32 i0) /\ (* JC_11 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (HW_13: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value result1)))), forall (result2: double), forall (HW_14: (add_double_post nearest_even A0 result1 result2)), forall (HW_23: (eq (double_value A0) (double_value result2))), forall (HW_24: (* JC_20 *) ((integer_of_int32 i0) = 53 /\ (eq (double_value A0) (1 * 9007199254740992)%R))), forall (result3: double), forall (HW_25: (eq (double_value result3) (1)%R) /\ (eq (double_exact result3) (1)%R) /\ (eq (double_model result3) (1)%R)), forall (B: double), forall (HW_26: B = result3), forall (result4: int32), forall (HW_27: (integer_of_int32 result4) = 1), forall (i1: int32), forall (HW_28: i1 = result4), forall (B0: double), forall (i2: int32), forall (HW_29: (* JC_25 *) True), forall (HW_30: (* JC_23 *) ((* JC_21 *) (eq (double_value B0) (IZR (integer_of_int32 i2))) /\ (* JC_22 *) ((integer_of_int32 i2) = 1 \/ (integer_of_int32 i2) = 2))), (no_overflow_double nearest_even (Rplus (double_value A0) (double_value B0))). Proof. intuition. rewrite H11, H15, H9. clear; why2gappa; gappa. rewrite H11, H15, H9. clear; why2gappa; gappa. Save. (* Why obligation from file "Malcolm.c", line 25, characters 9-16: *) (*Why goal*) Lemma malcolm1_safety_po_8 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_14 *) True), forall (HW_11: (* JC_12 *) ((* JC_9 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_10 *) 1 <= (integer_of_int32 i0) /\ (* JC_11 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (HW_13: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value result1)))), forall (result2: double), forall (HW_14: (add_double_post nearest_even A0 result1 result2)), forall (HW_23: (eq (double_value A0) (double_value result2))), forall (HW_24: (* JC_20 *) ((integer_of_int32 i0) = 53 /\ (eq (double_value A0) (1 * 9007199254740992)%R))), forall (result3: double), forall (HW_25: (eq (double_value result3) (1)%R) /\ (eq (double_exact result3) (1)%R) /\ (eq (double_model result3) (1)%R)), forall (B: double), forall (HW_26: B = result3), forall (result4: int32), forall (HW_27: (integer_of_int32 result4) = 1), forall (i1: int32), forall (HW_28: i1 = result4), forall (B0: double), forall (i2: int32), forall (HW_29: (* JC_25 *) True), forall (HW_30: (* JC_23 *) ((* JC_21 *) (eq (double_value B0) (IZR (integer_of_int32 i2))) /\ (* JC_22 *) ((integer_of_int32 i2) = 1 \/ (integer_of_int32 i2) = 2))), forall (HW_31: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value B0)))), forall (result5: double), forall (HW_32: (add_double_post nearest_even A0 B0 result5)), (no_overflow_double nearest_even (Rminus (double_value result5) (double_value A0))). Proof. intuition. why2gappa. rewrite HW_32,H11, H15, H9. simpl; gappa. why2gappa. rewrite HW_32,H11, H15, H9. simpl; gappa. Save. (* Why obligation from file "Malcolm.c", line 26, characters 4-7: *) (*Why goal*) Lemma malcolm1_safety_po_9 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_14 *) True), forall (HW_11: (* JC_12 *) ((* JC_9 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_10 *) 1 <= (integer_of_int32 i0) /\ (* JC_11 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (HW_13: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value result1)))), forall (result2: double), forall (HW_14: (add_double_post nearest_even A0 result1 result2)), forall (HW_23: (eq (double_value A0) (double_value result2))), forall (HW_24: (* JC_20 *) ((integer_of_int32 i0) = 53 /\ (eq (double_value A0) (1 * 9007199254740992)%R))), forall (result3: double), forall (HW_25: (eq (double_value result3) (1)%R) /\ (eq (double_exact result3) (1)%R) /\ (eq (double_model result3) (1)%R)), forall (B: double), forall (HW_26: B = result3), forall (result4: int32), forall (HW_27: (integer_of_int32 result4) = 1), forall (i1: int32), forall (HW_28: i1 = result4), forall (B0: double), forall (i2: int32), forall (HW_29: (* JC_25 *) True), forall (HW_30: (* JC_23 *) ((* JC_21 *) (eq (double_value B0) (IZR (integer_of_int32 i2))) /\ (* JC_22 *) ((integer_of_int32 i2) = 1 \/ (integer_of_int32 i2) = 2))), forall (HW_31: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value B0)))), forall (result5: double), forall (HW_32: (add_double_post nearest_even A0 B0 result5)), forall (HW_33: (no_overflow_double nearest_even (Rminus (double_value result5) (double_value A0)))), forall (result6: double), forall (HW_34: (sub_double_post nearest_even result5 A0 result6)), forall (HW_35: ~(eq (double_value result6) (double_value B0))), forall (result7: double), forall (HW_36: (eq (double_value result7) (1)%R) /\ (eq (double_exact result7) (1)%R) /\ (eq (double_model result7) (1)%R)), (no_overflow_double nearest_even (Rplus (double_value B0) (double_value result7))). Proof. intuition; why2gappa. rewrite H14,H11,H15. simpl; gappa. rewrite H14,H11,H15. simpl; gappa. Save. (* Why obligation from file "Malcolm.c", line 27, characters 14-17: *) (*Why goal*) Lemma malcolm1_safety_po_10 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_14 *) True), forall (HW_11: (* JC_12 *) ((* JC_9 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_10 *) 1 <= (integer_of_int32 i0) /\ (* JC_11 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (HW_13: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value result1)))), forall (result2: double), forall (HW_14: (add_double_post nearest_even A0 result1 result2)), forall (HW_23: (eq (double_value A0) (double_value result2))), forall (HW_24: (* JC_20 *) ((integer_of_int32 i0) = 53 /\ (eq (double_value A0) (1 * 9007199254740992)%R))), forall (result3: double), forall (HW_25: (eq (double_value result3) (1)%R) /\ (eq (double_exact result3) (1)%R) /\ (eq (double_model result3) (1)%R)), forall (B: double), forall (HW_26: B = result3), forall (result4: int32), forall (HW_27: (integer_of_int32 result4) = 1), forall (i1: int32), forall (HW_28: i1 = result4), forall (B0: double), forall (i2: int32), forall (HW_29: (* JC_25 *) True), forall (HW_30: (* JC_23 *) ((* JC_21 *) (eq (double_value B0) (IZR (integer_of_int32 i2))) /\ (* JC_22 *) ((integer_of_int32 i2) = 1 \/ (integer_of_int32 i2) = 2))), forall (HW_31: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value B0)))), forall (result5: double), forall (HW_32: (add_double_post nearest_even A0 B0 result5)), forall (HW_33: (no_overflow_double nearest_even (Rminus (double_value result5) (double_value A0)))), forall (result6: double), forall (HW_34: (sub_double_post nearest_even result5 A0 result6)), forall (HW_35: ~(eq (double_value result6) (double_value B0))), forall (result7: double), forall (HW_36: (eq (double_value result7) (1)%R) /\ (eq (double_exact result7) (1)%R) /\ (eq (double_model result7) (1)%R)), forall (HW_37: (no_overflow_double nearest_even (Rplus (double_value B0) (double_value result7)))), forall (result8: double), forall (HW_38: (add_double_post nearest_even B0 result7 result8)), forall (B1: double), forall (HW_39: B1 = result8), (-2147483648) <= ((integer_of_int32 i2) + 1). Proof. intuition. Save. (* Why obligation from file "Malcolm.c", line 27, characters 14-17: *) (*Why goal*) Lemma malcolm1_safety_po_11 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_14 *) True), forall (HW_11: (* JC_12 *) ((* JC_9 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_10 *) 1 <= (integer_of_int32 i0) /\ (* JC_11 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (HW_13: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value result1)))), forall (result2: double), forall (HW_14: (add_double_post nearest_even A0 result1 result2)), forall (HW_23: (eq (double_value A0) (double_value result2))), forall (HW_24: (* JC_20 *) ((integer_of_int32 i0) = 53 /\ (eq (double_value A0) (1 * 9007199254740992)%R))), forall (result3: double), forall (HW_25: (eq (double_value result3) (1)%R) /\ (eq (double_exact result3) (1)%R) /\ (eq (double_model result3) (1)%R)), forall (B: double), forall (HW_26: B = result3), forall (result4: int32), forall (HW_27: (integer_of_int32 result4) = 1), forall (i1: int32), forall (HW_28: i1 = result4), forall (B0: double), forall (i2: int32), forall (HW_29: (* JC_25 *) True), forall (HW_30: (* JC_23 *) ((* JC_21 *) (eq (double_value B0) (IZR (integer_of_int32 i2))) /\ (* JC_22 *) ((integer_of_int32 i2) = 1 \/ (integer_of_int32 i2) = 2))), forall (HW_31: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value B0)))), forall (result5: double), forall (HW_32: (add_double_post nearest_even A0 B0 result5)), forall (HW_33: (no_overflow_double nearest_even (Rminus (double_value result5) (double_value A0)))), forall (result6: double), forall (HW_34: (sub_double_post nearest_even result5 A0 result6)), forall (HW_35: ~(eq (double_value result6) (double_value B0))), forall (result7: double), forall (HW_36: (eq (double_value result7) (1)%R) /\ (eq (double_exact result7) (1)%R) /\ (eq (double_model result7) (1)%R)), forall (HW_37: (no_overflow_double nearest_even (Rplus (double_value B0) (double_value result7)))), forall (result8: double), forall (HW_38: (add_double_post nearest_even B0 result7 result8)), forall (B1: double), forall (HW_39: B1 = result8), ((integer_of_int32 i2) + 1) <= 2147483647. Proof. intuition. Save. (* Why obligation from file "Malcolm.c", line 23, characters 18-23: *) (*Why goal*) Lemma malcolm1_safety_po_12 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_14 *) True), forall (HW_11: (* JC_12 *) ((* JC_9 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_10 *) 1 <= (integer_of_int32 i0) /\ (* JC_11 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (HW_13: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value result1)))), forall (result2: double), forall (HW_14: (add_double_post nearest_even A0 result1 result2)), forall (HW_23: (eq (double_value A0) (double_value result2))), forall (HW_24: (* JC_20 *) ((integer_of_int32 i0) = 53 /\ (eq (double_value A0) (1 * 9007199254740992)%R))), forall (result3: double), forall (HW_25: (eq (double_value result3) (1)%R) /\ (eq (double_exact result3) (1)%R) /\ (eq (double_model result3) (1)%R)), forall (B: double), forall (HW_26: B = result3), forall (result4: int32), forall (HW_27: (integer_of_int32 result4) = 1), forall (i1: int32), forall (HW_28: i1 = result4), forall (B0: double), forall (i2: int32), forall (HW_29: (* JC_25 *) True), forall (HW_30: (* JC_23 *) ((* JC_21 *) (eq (double_value B0) (IZR (integer_of_int32 i2))) /\ (* JC_22 *) ((integer_of_int32 i2) = 1 \/ (integer_of_int32 i2) = 2))), forall (HW_31: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value B0)))), forall (result5: double), forall (HW_32: (add_double_post nearest_even A0 B0 result5)), forall (HW_33: (no_overflow_double nearest_even (Rminus (double_value result5) (double_value A0)))), forall (result6: double), forall (HW_34: (sub_double_post nearest_even result5 A0 result6)), forall (HW_35: ~(eq (double_value result6) (double_value B0))), forall (result7: double), forall (HW_36: (eq (double_value result7) (1)%R) /\ (eq (double_exact result7) (1)%R) /\ (eq (double_model result7) (1)%R)), forall (HW_37: (no_overflow_double nearest_even (Rplus (double_value B0) (double_value result7)))), forall (result8: double), forall (HW_38: (add_double_post nearest_even B0 result7 result8)), forall (B1: double), forall (HW_39: B1 = result8), forall (HW_40: (-2147483648) <= ((integer_of_int32 i2) + 1) /\ ((integer_of_int32 i2) + 1) <= 2147483647), forall (result9: int32), forall (HW_41: (integer_of_int32 result9) = ((integer_of_int32 i2) + 1)), forall (i3: int32), forall (HW_42: i3 = result9), 0 <= ((* JC_31 *) (2 - (integer_of_int32 i2))). Proof. intuition. Save. (* Why obligation from file "Malcolm.c", line 23, characters 18-23: *) (*Why goal*) Lemma malcolm1_safety_po_13 : forall (HW_1: (* JC_4 *) True), forall (result: double), forall (HW_6: (eq (double_value result) (2)%R) /\ (eq (double_exact result) (2)%R) /\ (eq (double_model result) (2)%R)), forall (A: double), forall (HW_7: A = result), forall (result0: int32), forall (HW_8: (integer_of_int32 result0) = 1), forall (i: int32), forall (HW_9: i = result0), forall (A0: double), forall (i0: int32), forall (HW_10: (* JC_14 *) True), forall (HW_11: (* JC_12 *) ((* JC_9 *) (eq (double_value A0) (powerRZ (2)%R (integer_of_int32 i0))) /\ (* JC_10 *) 1 <= (integer_of_int32 i0) /\ (* JC_11 *) (integer_of_int32 i0) <= 53)), forall (result1: double), forall (HW_12: (eq (double_value result1) (1)%R) /\ (eq (double_exact result1) (1)%R) /\ (eq (double_model result1) (1)%R)), forall (HW_13: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value result1)))), forall (result2: double), forall (HW_14: (add_double_post nearest_even A0 result1 result2)), forall (HW_23: (eq (double_value A0) (double_value result2))), forall (HW_24: (* JC_20 *) ((integer_of_int32 i0) = 53 /\ (eq (double_value A0) (1 * 9007199254740992)%R))), forall (result3: double), forall (HW_25: (eq (double_value result3) (1)%R) /\ (eq (double_exact result3) (1)%R) /\ (eq (double_model result3) (1)%R)), forall (B: double), forall (HW_26: B = result3), forall (result4: int32), forall (HW_27: (integer_of_int32 result4) = 1), forall (i1: int32), forall (HW_28: i1 = result4), forall (B0: double), forall (i2: int32), forall (HW_29: (* JC_25 *) True), forall (HW_30: (* JC_23 *) ((* JC_21 *) (eq (double_value B0) (IZR (integer_of_int32 i2))) /\ (* JC_22 *) ((integer_of_int32 i2) = 1 \/ (integer_of_int32 i2) = 2))), forall (HW_31: (no_overflow_double nearest_even (Rplus (double_value A0) (double_value B0)))), forall (result5: double), forall (HW_32: (add_double_post nearest_even A0 B0 result5)), forall (HW_33: (no_overflow_double nearest_even (Rminus (double_value result5) (double_value A0)))), forall (result6: double), forall (HW_34: (sub_double_post nearest_even result5 A0 result6)), forall (HW_35: ~(eq (double_value result6) (double_value B0))), forall (result7: double), forall (HW_36: (eq (double_value result7) (1)%R) /\ (eq (double_exact result7) (1)%R) /\ (eq (double_model result7) (1)%R)), forall (HW_37: (no_overflow_double nearest_even (Rplus (double_value B0) (double_value result7)))), forall (result8: double), forall (HW_38: (add_double_post nearest_even B0 result7 result8)), forall (B1: double), forall (HW_39: B1 = result8), forall (HW_40: (-2147483648) <= ((integer_of_int32 i2) + 1) /\ ((integer_of_int32 i2) + 1) <= 2147483647), forall (result9: int32), forall (HW_41: (integer_of_int32 result9) = ((integer_of_int32 i2) + 1)), forall (i3: int32), forall (HW_42: i3 = result9), ((* JC_31 *) (2 - (integer_of_int32 i3))) < ((* JC_31 *) (2 - (integer_of_int32 i2))). Proof. intuition; rewrite HW_42, HW_41; auto with zarith. Save.