(* This file was originally generated by why. It can be modified; only the generated parts will be overwritten. *) Require Export jessie_why. Require Export floats_strict. (*Why type*) Definition char_P: Set. Admitted. (*Why type*) Definition int8: Set. Admitted. (*Why type*) Definition padding: Set. Admitted. (*Why type*) Definition void_P: Set. Admitted. (*Why logic*) Definition char_P_tag : (tag_id char_P). Admitted. (*Why axiom*) Lemma char_P_int : (int_of_tag char_P_tag) = 1. Admitted. (*Why logic*) Definition char_P_of_pointer_address : (pointer unit) -> (pointer char_P). Admitted. (*Why axiom*) Lemma char_P_of_pointer_address_of_pointer_addr : (forall (p:(pointer char_P)), p = (char_P_of_pointer_address (pointer_address p))). Admitted. (*Why axiom*) Lemma char_P_parenttag_bottom : (parenttag char_P_tag (@bottom_tag char_P)). Admitted. (*Why axiom*) Lemma char_P_tags : (forall (x:(pointer char_P)), (forall (char_P_tag_table:(tag_table char_P)), (instanceof char_P_tag_table x char_P_tag))). Admitted. (*Why logic*) Definition integer_of_int8 : int8 -> Z. Admitted. (*Why predicate*) Definition eq_int8 (x:int8) (y:int8) := (integer_of_int8 x) = (integer_of_int8 y). (*Why logic*) Definition int8_of_integer : Z -> int8. Admitted. (*Why axiom*) Lemma int8_coerce : (forall (x:Z), ((-128) <= x /\ x <= 127 -> (integer_of_int8 (int8_of_integer x)) = x)). Admitted. (*Why axiom*) Lemma int8_range : (forall (x:int8), (-128) <= (integer_of_int8 x) /\ (integer_of_int8 x) <= 127). Admitted. (*Why predicate*) Definition left_valid_struct_char_P (p:(pointer char_P)) (a:Z) (char_P_alloc_table:(alloc_table char_P)) := (offset_min char_P_alloc_table p) <= a. (*Why predicate*) Definition left_valid_struct_void_P (p:(pointer void_P)) (a:Z) (void_P_alloc_table:(alloc_table void_P)) := (offset_min void_P_alloc_table p) <= a. (*Why axiom*) Lemma pointer_addr_of_char_P_of_pointer_address : (forall (p:(pointer unit)), p = (pointer_address (char_P_of_pointer_address p))). Admitted. (*Why logic*) Definition void_P_of_pointer_address : (pointer unit) -> (pointer void_P). Admitted. (*Why axiom*) Lemma pointer_addr_of_void_P_of_pointer_address : (forall (p:(pointer unit)), p = (pointer_address (void_P_of_pointer_address p))). Admitted. (*Why predicate*) Definition right_valid_struct_char_P (p:(pointer char_P)) (b:Z) (char_P_alloc_table:(alloc_table char_P)) := (offset_max char_P_alloc_table p) >= b. (*Why predicate*) Definition right_valid_struct_void_P (p:(pointer void_P)) (b:Z) (void_P_alloc_table:(alloc_table void_P)) := (offset_max void_P_alloc_table p) >= b. (*Why predicate*) Definition strict_valid_root_char_P (p:(pointer char_P)) (a:Z) (b:Z) (char_P_alloc_table:(alloc_table char_P)) := (offset_min char_P_alloc_table p) = a /\ (offset_max char_P_alloc_table p) = b. (*Why predicate*) Definition strict_valid_root_void_P (p:(pointer void_P)) (a:Z) (b:Z) (void_P_alloc_table:(alloc_table void_P)) := (offset_min void_P_alloc_table p) = a /\ (offset_max void_P_alloc_table p) = b. (*Why predicate*) Definition strict_valid_struct_char_P (p:(pointer char_P)) (a:Z) (b:Z) (char_P_alloc_table:(alloc_table char_P)) := (offset_min char_P_alloc_table p) = a /\ (offset_max char_P_alloc_table p) = b. (*Why predicate*) Definition strict_valid_struct_void_P (p:(pointer void_P)) (a:Z) (b:Z) (void_P_alloc_table:(alloc_table void_P)) := (offset_min void_P_alloc_table p) = a /\ (offset_max void_P_alloc_table p) = b. (*Why predicate*) Definition valid_bitvector_struct_char_P (p:(pointer unit)) (a:Z) (b:Z) (bitvector_alloc_table:(alloc_table unit)) := (offset_min bitvector_alloc_table p) = a /\ (offset_max bitvector_alloc_table p) = b. (*Why predicate*) Definition valid_bitvector_struct_void_P (p:(pointer unit)) (a:Z) (b:Z) (bitvector_alloc_table:(alloc_table unit)) := (offset_min bitvector_alloc_table p) = a /\ (offset_max bitvector_alloc_table p) = b. (*Why predicate*) Definition valid_root_char_P (p:(pointer char_P)) (a:Z) (b:Z) (char_P_alloc_table:(alloc_table char_P)) := (offset_min char_P_alloc_table p) <= a /\ (offset_max char_P_alloc_table p) >= b. (*Why predicate*) Definition valid_root_void_P (p:(pointer void_P)) (a:Z) (b:Z) (void_P_alloc_table:(alloc_table void_P)) := (offset_min void_P_alloc_table p) <= a /\ (offset_max void_P_alloc_table p) >= b. (*Why predicate*) Definition valid_struct_char_P (p:(pointer char_P)) (a:Z) (b:Z) (char_P_alloc_table:(alloc_table char_P)) := (offset_min char_P_alloc_table p) <= a /\ (offset_max char_P_alloc_table p) >= b. (*Why predicate*) Definition valid_struct_void_P (p:(pointer void_P)) (a:Z) (b:Z) (void_P_alloc_table:(alloc_table void_P)) := (offset_min void_P_alloc_table p) <= a /\ (offset_max void_P_alloc_table p) >= b. (*Why logic*) Definition void_P_tag : (tag_id void_P). Admitted. (*Why axiom*) Lemma void_P_int : (int_of_tag void_P_tag) = 1. Admitted. (*Why axiom*) Lemma void_P_of_pointer_address_of_pointer_addr : (forall (p:(pointer void_P)), p = (void_P_of_pointer_address (pointer_address p))). Admitted. (*Why axiom*) Lemma void_P_parenttag_bottom : (parenttag void_P_tag (@bottom_tag void_P)). Admitted. (*Why axiom*) Lemma void_P_tags : (forall (x:(pointer void_P)), (forall (void_P_tag_table:(tag_table void_P)), (instanceof void_P_tag_table x void_P_tag))). Admitted. (* Why obligation from file "Sterbenz.c", line 2, characters 12-26: *) (*Why goal*) Lemma Sterbenz_ensures_default_po_1 : forall (x: single), forall (y: single), forall (HW_1: (* JC_7 *) ((* JC_5 *) (Rle (Rdiv (single_value y) (2)%R) (single_value x)) /\ (* JC_6 *) (Rle (single_value x) (Rmult (2)%R (single_value y))))), forall (result: single), forall (HW_4: (no_overflow_single nearest_even (Rminus (single_value x) (single_value y))) /\ (sub_single_post nearest_even x y result)), forall (__retres: single), forall (HW_5: __retres = result), forall (why__return: single), forall (HW_6: why__return = __retres), (* JC_9 *) (eq (single_value why__return) (Rminus (single_value x) (single_value y))). Proof. intros x y (H1,H2) r (H4,(H5a,H5b)) r' H6 r'' H7. rewrite H7,H6,H5a; unfold single_value in *. unfold FtoRradix; rewrite <- Fminus_correct; auto with zarith. elim (mode_single_RoundingMode nearest_even); intros P (H8,H9). apply sym_eq; apply RoundedModeProjectorIdemEq with bsingle 24%nat P; try apply psGivesBound; auto with zarith. apply Sterbenz; auto with zarith; try apply FcanonicBound with radix; try now destruct x; try now destruct y. fold FtoRradix; apply Rle_trans with (2:=H1); unfold Rdiv; simpl; right; ring. Save. (* Why obligation from file "Sterbenz.c", line 6, characters 2-8: *) (*Why goal*) Lemma Sterbenz_safety_po_1 : forall (x: single), forall (y: single), forall (HW_1: (* JC_7 *) ((* JC_5 *) (Rle (Rdiv (single_value y) (2)%R) (single_value x)) /\ (* JC_6 *) (Rle (single_value x) (Rmult (2)%R (single_value y))))), (no_overflow_single nearest_even (Rminus (single_value x) (single_value y))). Proof. intros; apply bounded_real_no_overflow_single. cut (0 <= single_value y)%R; try intros. cut (0 <= single_value x)%R; try intros. case (Rle_or_lt (single_value x) (single_value y)); intros. rewrite Rabs_left1; ring_simplify. apply Rle_trans with (-0+single_value y)%R;auto with real. ring_simplify; rewrite <- (Rabs_right (single_value y));[apply single_le_strict|auto with real]. apply Rplus_le_reg_l with (single_value y); now ring_simplify. rewrite Rabs_right; ring_simplify. apply Rle_trans with (single_value x-0)%R. apply Rplus_le_compat_l; auto with real. ring_simplify; rewrite <- (Rabs_right (single_value x));[apply single_le_strict|auto with real]. apply Rle_ge; apply Rplus_le_reg_l with (single_value y); ring_simplify; auto with real. apply Rle_trans with (single_value y / 2)%R;[idtac|apply HW_1]. unfold Rdiv; apply Rmult_le_pos; auto with real. apply Rmult_le_reg_l with 3%R;[apply Rlt_le_trans with 2%R; auto with real|idtac]. apply Rplus_le_reg_l with (single_value y); apply Rmult_le_reg_l with (/2)%R; auto with real. replace (/ 2 * (single_value y + 3 * 0))%R with (single_value y / 2)%R by (unfold Rdiv; ring). apply Rle_trans with (single_value x);[eapply HW_1|idtac]. apply Rle_trans with (2 * single_value y)%R;[eapply HW_1|right;field]. Save.