From 0656f30a162fc3cf07bf853072db2b830026f61f Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sat, 21 Jun 2025 07:50:20 +0000 Subject: [PATCH] finish carry proof --- projects/lib/GmpAux.v | 6 ++ projects/lib/gmp_goal.v | 116 +++++++++++++++++++++++++++++--- projects/lib/gmp_proof_manual.v | 87 ++++++++++++++++-------- projects/mini-gmp.c | 1 + 4 files changed, 171 insertions(+), 39 deletions(-) diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index 3a4c199..8d1c1ac 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -21,6 +21,12 @@ Local Open Scope sac. Module Aux. +Lemma Z_mod_add_carry: forall (a b m: Z), + m > 0 -> 0 <= a < m -> 0 <= b < m -> + (a + b) mod m < b -> + a + b = (a + b) mod m + m. +Proof. Admitted. + Lemma Z_of_nat_succ: forall (n: nat), Z.of_nat (S n) = Z.of_nat n + 1. Proof. lia. Qed. diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v index 911faa4..220809d 100644 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -1787,6 +1787,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1810,10 +1812,10 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ((app (l') ((cons (a) (nil)))))) ) ** ((( &( "i" ) )) # Int |-> i) ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) + ** ((( &( "b" ) )) # UInt |-> 0) ** (store_uint_array ap_pre n_pre l_2 ) ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) - ** ((( &( "b" ) )) # UInt |-> 0) ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) ** ((( &( "rp" ) )) # Ptr |-> rp_pre) @@ -1829,6 +1831,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1852,10 +1856,10 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ((app (l') ((cons (a) (nil)))))) ) ** ((( &( "i" ) )) # Int |-> i) ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) + ** ((( &( "b" ) )) # UInt |-> 1) ** (store_uint_array ap_pre n_pre l_2 ) ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) - ** ((( &( "b" ) )) # UInt |-> 1) ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) ** ((( &( "rp" ) )) # Ptr |-> rp_pre) @@ -1908,13 +1912,82 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_uint_array_rec rp_pre 0 cap2 l'' ) . -Definition mpn_add_1_entail_wit_2_1 := +Definition mpn_add_1_entail_wit_2 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , + [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array ap_pre n_pre l_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) + ** ((( &( "b" ) )) # UInt |-> b) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| (0 <= b) |] + && [| (b <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && ((( &( "b" ) )) # UInt |-> b) + ** (store_uint_array ap_pre n_pre l_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +. + +Definition mpn_add_1_entail_wit_3_1 := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (b: Z) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) (a: Z) (l''': (@list Z)) , [| (l''_2 = (cons (a) (l'''))) |] && [| (0 <= i) |] && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1966,13 +2039,15 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l'' ) . -Definition mpn_add_1_entail_wit_2_2 := +Definition mpn_add_1_entail_wit_3_2 := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (b: Z) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) (a: Z) (l''': (@list Z)) , [| (l''_2 = (cons (a) (l'''))) |] && [| (0 <= i) |] && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2193,6 +2268,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ Definition mpn_add_1_partial_solve_wit_4_pure := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2213,13 +2290,13 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (cap2 <= 100000000) |] && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] - && (store_uint_array ap_pre n_pre l_2 ) + && ((( &( "b" ) )) # UInt |-> 0) + ** (store_uint_array ap_pre n_pre l_2 ) ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ** ((( &( "i" ) )) # Int |-> i) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre i l' ) ** (store_uint_array_rec rp_pre i cap2 l'' ) - ** ((( &( "b" ) )) # UInt |-> 0) ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) ** ((( &( "rp" ) )) # Ptr |-> rp_pre) @@ -2232,6 +2309,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ Definition mpn_add_1_partial_solve_wit_4_aux := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2261,6 +2340,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2292,6 +2373,8 @@ Definition mpn_add_1_partial_solve_wit_4 := mpn_add_1_partial_solve_wit_4_pure - Definition mpn_add_1_partial_solve_wit_5_pure := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2312,13 +2395,13 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (cap2 <= 100000000) |] && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] - && (store_uint_array ap_pre n_pre l_2 ) + && ((( &( "b" ) )) # UInt |-> 1) + ** (store_uint_array ap_pre n_pre l_2 ) ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ** ((( &( "i" ) )) # Int |-> i) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre i l' ) ** (store_uint_array_rec rp_pre i cap2 l'' ) - ** ((( &( "b" ) )) # UInt |-> 1) ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) ** ((( &( "rp" ) )) # Ptr |-> rp_pre) @@ -2331,6 +2414,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ Definition mpn_add_1_partial_solve_wit_5_aux := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2360,6 +2445,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2395,6 +2482,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2425,6 +2514,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2459,6 +2550,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2489,6 +2582,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2630,8 +2725,9 @@ Axiom proof_of_mpn_add_1_safety_wit_1 : mpn_add_1_safety_wit_1. Axiom proof_of_mpn_add_1_safety_wit_2 : mpn_add_1_safety_wit_2. Axiom proof_of_mpn_add_1_safety_wit_3 : mpn_add_1_safety_wit_3. Axiom proof_of_mpn_add_1_entail_wit_1 : mpn_add_1_entail_wit_1. -Axiom proof_of_mpn_add_1_entail_wit_2_1 : mpn_add_1_entail_wit_2_1. -Axiom proof_of_mpn_add_1_entail_wit_2_2 : mpn_add_1_entail_wit_2_2. +Axiom proof_of_mpn_add_1_entail_wit_2 : mpn_add_1_entail_wit_2. +Axiom proof_of_mpn_add_1_entail_wit_3_1 : mpn_add_1_entail_wit_3_1. +Axiom proof_of_mpn_add_1_entail_wit_3_2 : mpn_add_1_entail_wit_3_2. Axiom proof_of_mpn_add_1_return_wit_1 : mpn_add_1_return_wit_1. Axiom proof_of_mpn_add_1_partial_solve_wit_1 : mpn_add_1_partial_solve_wit_1. Axiom proof_of_mpn_add_1_partial_solve_wit_2_pure : mpn_add_1_partial_solve_wit_2_pure. diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index f7e7044..ba68a43 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -422,14 +422,20 @@ Proof. + simpl. tauto. Qed. -Lemma proof_of_mpn_add_1_entail_wit_2_1 : mpn_add_1_entail_wit_2_1. +Lemma proof_of_mpn_add_1_entail_wit_2 : mpn_add_1_entail_wit_2. +Proof. + pre_process. + entailer!. +Admitted. + +Lemma proof_of_mpn_add_1_entail_wit_3_1 : mpn_add_1_entail_wit_3_1. Proof. pre_process. rewrite replace_Znth_app_r. - Exists l'''. - rewrite H12. + rewrite H14. assert (i - i = 0) by lia. - rewrite H24. + rewrite H26. set (new_b := (unsigned_last_nbits (Znth i l_3 0 + b) 32)). rewrite replace_Znth_nothing; try lia. assert (replace_Znth 0 new_b (a :: nil) = new_b :: nil). { @@ -438,85 +444,108 @@ Proof. unfold replace_nth. reflexivity. } - rewrite H25. + rewrite H27. Exists (l'_2 ++ new_b :: nil). Exists (val2_2 + new_b * (UINT_MOD^ i)). Exists (val1_2 + (Znth i l_3 0) * (UINT_MOD^ i)). Exists l_3. entailer!. + rewrite Zlength_app. - rewrite H12. + rewrite H14. unfold Zlength. unfold Zlength_aux. lia. + assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i + b_pre = (val1_2 + b_pre) + Znth i l_3 0 * 4294967296 ^ i) by lia. - rewrite H26. - rewrite <- H11. + rewrite H28. + rewrite <- H13. assert (Znth i l_3 0 + b = new_b + UINT_MOD). { subst new_b. unfold unsigned_last_nbits. unfold unsigned_last_nbits in H3. assert (2^32 = 4294967296). { nia. } - rewrite H27 in *. - admit. + rewrite H29 in *. + assert (0 <= Znth i l_3 0 < 4294967296). { + assert (l_2=l_3). + { + pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val). + apply H30 in H9; try tauto. + } + assert (i < Zlength l_3). { + subst l_3. + rewrite H17. + tauto. + } + unfold list_store_Z_compact in H9. + apply list_within_bound_Znth. + lia. + tauto. + } + apply Z_mod_add_carry; try lia; try tauto. } - admit. + assert (b * 4294967296 ^ i + Znth i l_3 0 * 4294967296 ^ i = new_b * 4294967296 ^ i + 1 * 4294967296 ^ (i + 1)). + { + subst new_b. + Search [ Zmult Zplus "distr" ]. + rewrite <- Z.mul_add_distr_r. + rewrite (Zpow_add_1 4294967296 i); try lia. + } + lia. + pose proof (__list_store_Z_concat_r l'_2 val2_2 new_b). - apply H26 in H10. - rewrite H12 in H10. + apply H28 in H12. + rewrite H14 in H12. assert (new_b * 4294967296 ^ i + val2_2 = (val2_2 + new_b * 4294967296 ^ i)) by lia. - rewrite H27 in H10. + rewrite H29 in H12. tauto. subst new_b. unfold unsigned_last_nbits. assert (2 ^ 32 = 4294967296). { nia. } - rewrite H27. + rewrite H29. apply Z.mod_pos_bound. lia. + assert (l_2=l_3). { pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val). - apply H26 in H7; try tauto. + apply H28 in H9; try tauto. } assert (i < Zlength l_3). { subst l_3. - rewrite H15. + rewrite H17. tauto. } assert((sublist 0 (i + 1) l_3) = (sublist 0 i l_3) ++ (Znth i l_3 0) :: nil). { pose proof (sublist_split 0 (i+1) i l_3). pose proof (sublist_single i l_3 0). - rewrite <-H29. - apply H28. + rewrite <-H31. + apply H30. lia. subst l_3. - rewrite Zlength_correct in H27. + rewrite Zlength_correct in H29. lia. - rewrite Zlength_correct in H27. + rewrite Zlength_correct in H29. lia. } - rewrite H28. - pose proof (__list_store_Z_concat_r (sublist 0 i l_3) val1_2 (Znth i l_3 0)). - apply H29 in H9. - rewrite Zlength_sublist0 in H9. - assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i = Znth i l_3 0 * 4294967296 ^ i + val1_2) by lia. rewrite H30. + pose proof (__list_store_Z_concat_r (sublist 0 i l_3) val1_2 (Znth i l_3 0)). + apply H31 in H11. + rewrite Zlength_sublist0 in H11. + assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i = Znth i l_3 0 * 4294967296 ^ i + val1_2) by lia. + rewrite H32. tauto. subst l_3. - rewrite H15. + rewrite H17. lia. apply list_within_bound_Znth. lia. - unfold list_store_Z_compact in H7. + unfold list_store_Z_compact in H9. tauto. - pose proof (Zlength_sublist0 i l'_2). lia. -Admitted. +Qed. -Lemma proof_of_mpn_add_1_entail_wit_2_2 : mpn_add_1_entail_wit_2_2. +Lemma proof_of_mpn_add_1_entail_wit_3_2 : mpn_add_1_entail_wit_3_2. Proof. pre_process. Admitted. diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 926016c..53dd6d5 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -293,6 +293,7 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) Given l l' l'' val1 val2 */ unsigned int r = ap[i] + b; + /*@ 0 <= b && b <= UINT_MAX by local */ b = (r < b); /*@ 0 <= i && i < n@pre && n@pre <= cap2 &&