From dd60b4a292b870e08c23ddcb363630cbb2ed1227 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 2 May 2019 08:16:37 +0200 Subject: [primitive integers] Make div21 implems consistent with its specification There are three implementations of this primitive: * one in OCaml on 63 bits integer in kernel/uint63_amd64.ml * one in OCaml on Int64 in kernel/uint63_x86.ml * one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h Its specification is the axiom `diveucl_21_spec` in theories/Numbers/Cyclic/Int63/Int63.v * comment the implementations with loop invariants to enable an easy pen&paper proof of correctness (note to reviewers: the one in uint63_amd64.ml might be the easiest to read) * make sure the three implementations are equivalent * fix the specification in Int63.v (only the lowest part of the result is actually returned) * make a little optimisation in div21 enabled by the proof of correctness (cmp is computed at the end of the first loop rather than at the beginning, potentially saving one loop iteration while remaining correct) * update the proofs in Int63.v and Cyclic63.v to take into account the new specifiation of div21 * add a test --- theories/Numbers/Cyclic/Int63/Cyclic63.v | 15 ------- theories/Numbers/Cyclic/Int63/Int63.v | 74 ++++++++++++++++++++++++-------- 2 files changed, 57 insertions(+), 32 deletions(-) (limited to 'theories/Numbers') diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v index 3b431d5b47..c03e6615cb 100644 --- a/theories/Numbers/Cyclic/Int63/Cyclic63.v +++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v @@ -177,21 +177,6 @@ Proof. inversion W;rewrite Zmult_comm;trivial. Qed. -Lemma diveucl_21_spec_aux : forall a1 a2 b, - wB/2 <= [|b|] -> - [|a1|] < [|b|] -> - let (q,r) := diveucl_21 a1 a2 b in - [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ - 0 <= [|r|] < [|b|]. -Proof. - intros a1 a2 b H1 H2;assert (W:= diveucl_21_spec a1 a2 b). - assert (W1:= to_Z_bounded a1). - assert ([|b|]>0) by (auto with zarith). - generalize (Z_div_mod ([|a1|]*wB+[|a2|]) [|b|] H). - destruct (diveucl_21 a1 a2 b);destruct (Z.div_eucl ([|a1|]*wB+[|a2|]) [|b|]). - inversion W;rewrite (Zmult_comm [|b|]);trivial. -Qed. - Lemma shift_unshift_mod_2 : forall n p a, 0 <= p <= n -> ((a * 2 ^ (n - p)) mod (2^n) / 2 ^ (n - p)) mod (2^n) = a mod 2 ^ p. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index eac26add03..3c96130bf3 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -387,7 +387,8 @@ Axiom diveucl_def_spec : forall x y, diveucl x y = diveucl_def x y. Axiom diveucl_21_spec : forall a1 a2 b, let (q,r) := diveucl_21 a1 a2 b in - ([|q|],[|r|]) = Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|]. + let (q',r') := Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|] in + [|q|] = Z.modulo q' wB /\ [|r|] = r'. Axiom addmuldiv_def_spec : forall p x y, addmuldiv p x y = addmuldiv_def p x y. @@ -1413,12 +1414,51 @@ Proof. apply Z.le_trans with ([|ih|] * wB)%Z;try rewrite Z.pow_2_r; auto with zarith. Qed. -Lemma div2_phi ih il j: - [|fst (diveucl_21 ih il j)|] = [|| WW ih il||] /[|j|]. -Proof. - generalize (diveucl_21_spec ih il j). - case diveucl_21; intros q r Heq. - simpl zn2z_to_Z;unfold Z.div;rewrite <- Heq;trivial. +Lemma diveucl_21_spec_aux : forall a1 a2 b, + wB/2 <= [|b|] -> + [|a1|] < [|b|] -> + let (q,r) := diveucl_21 a1 a2 b in + [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]. +Proof. + intros a1 a2 b H1 H2;assert (W:= diveucl_21_spec a1 a2 b). + assert (W1:= to_Z_bounded a1). + assert (W2:= to_Z_bounded a2). + assert (Wb:= to_Z_bounded b). + assert ([|b|]>0) by (auto with zarith). + generalize (Z_div_mod ([|a1|]*wB+[|a2|]) [|b|] H). + revert W. + destruct (diveucl_21 a1 a2 b); destruct (Z.div_eucl ([|a1|]*wB+[|a2|]) [|b|]). + intros (H', H''); rewrite H', H''; clear H' H''. + intros (H', H''); split; [ |exact H'']. + rewrite H', Zmult_comm, Z.mod_small; [reflexivity| ]. + split. + { revert H'; case z; [now simpl..|intros p H']. + exfalso; apply (Z.lt_irrefl 0), (Z.le_lt_trans _ ([|a1|] * wB + [|a2|])). + { now apply Z.add_nonneg_nonneg; [apply Z.mul_nonneg_nonneg| ]. } + rewrite H'; apply (Zplus_lt_reg_r _ _ (- z0)); ring_simplify. + apply (Z.le_lt_trans _ (- [|b|])); [ |now auto with zarith]. + rewrite Z.opp_eq_mul_m1; apply Zmult_le_compat_l; [ |now apply Wb]. + rewrite <-!Pos2Z.opp_pos, <-Z.opp_le_mono. + now change 1 with (Z.succ 0); apply Zlt_le_succ. } + rewrite <-Z.nle_gt; intro Hz; revert H2; apply Zle_not_lt. + rewrite (Z.div_unique_pos (wB * [|a1|] + [|a2|]) wB [|a1|] [|a2|]); + [ |now simpl..]. + rewrite Z.mul_comm, H'. + rewrite (Z.div_unique_pos (wB * [|b|] + z0) wB [|b|] z0) at 1; + [ |split; [ |apply (Z.lt_trans _ [|b|])]; now simpl|reflexivity]. + apply Z_div_le; [now simpl| ]; rewrite Z.mul_comm; apply Zplus_le_compat_r. + now apply Zmult_le_compat_l. +Qed. + +Lemma div2_phi ih il j: (2^62 <= [|j|] -> [|ih|] < [|j|] -> + [|fst (diveucl_21 ih il j)|] = [|| WW ih il||] /[|j|])%Z. +Proof. + intros Hj Hj1. + generalize (diveucl_21_spec_aux ih il j Hj Hj1). + case diveucl_21; intros q r (Hq, Hr). + apply Zdiv_unique with [|r|]; auto with zarith. + simpl @fst; apply eq_trans with (1 := Hq); ring. Qed. Lemma sqrt2_step_correct rec ih il j: @@ -1436,9 +1476,9 @@ Proof. case (to_Z_bounded il); intros Hil1 _. case (to_Z_bounded j); intros _ Hj1. assert (Hp3: (0 < [||WW ih il||])). - simpl zn2z_to_Z;apply Z.lt_le_trans with ([|ih|] * wB)%Z; auto with zarith. + {simpl zn2z_to_Z;apply Z.lt_le_trans with ([|ih|] * wB)%Z; auto with zarith. apply Zmult_lt_0_compat; auto with zarith. - refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. + refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. } cbv zeta. case_eq (ih < j)%int63;intros Heq. rewrite -> ltb_spec in Heq. @@ -1450,28 +1490,28 @@ Proof. 2: rewrite Zmult_comm, Z_div_plus_full_l; unfold base; auto with zarith. case (Zle_or_lt (2^(Z_of_nat size -1)) [|j|]); intros Hjj. case_eq (fst (diveucl_21 ih il j) < j)%int63;intros Heq0. - 2: rewrite <-not_true_iff_false, ltb_spec, div2_phi in Heq0. + 2: rewrite <-not_true_iff_false, ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0. 2: split; auto; apply sqrt_test_true; auto with zarith. - rewrite -> ltb_spec, div2_phi in Heq0. + rewrite -> ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0. match goal with |- context[rec _ _ ?X] => set (u := X) end. assert (H: [|u|] = ([|j|] + ([||WW ih il||])/([|j|]))/2). - unfold u; generalize (addc_spec j (fst (diveucl_21 ih il j))); - case addc;unfold interp_carry;rewrite div2_phi;simpl zn2z_to_Z. - intros i H;rewrite lsr_spec, H;trivial. + { unfold u; generalize (addc_spec j (fst (diveucl_21 ih il j))); + case addc;unfold interp_carry;rewrite (div2_phi _ _ _ Hjj Heq);simpl zn2z_to_Z. + { intros i H;rewrite lsr_spec, H;trivial. } intros i H;rewrite <- H. case (to_Z_bounded i); intros H1i H2i. rewrite -> add_spec, Zmod_small, lsr_spec. - change (1 * wB) with ([|(1 << (digits -1))|] * 2)%Z. - rewrite Z_div_plus_full_l; auto with zarith. + { change (1 * wB) with ([|(1 << (digits -1))|] * 2)%Z. + rewrite Z_div_plus_full_l; auto with zarith. } change wB with (2 * (wB/2))%Z; auto. replace [|(1 << (digits - 1))|] with (wB/2); auto. rewrite lsr_spec; auto. replace (2^[|1|]) with 2%Z; auto. split; auto with zarith. assert ([|i|]/2 < wB/2); auto with zarith. - apply Zdiv_lt_upper_bound; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. } apply Hrec; rewrite H; clear u H. assert (Hf1: 0 <= [||WW ih il||]/ [|j|]) by (apply Z_div_pos; auto with zarith). case (Zle_lt_or_eq 1 ([|j|])); auto with zarith; intros Hf2. -- cgit v1.2.3