From 49848bd048921e024a5eba315dbb2a4c7cec2dad Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Fri, 20 Jun 2025 16:57:26 +0000 Subject: [PATCH] finish proof_of_mpn_add_1_return_wit_1 --- projects/lib/GmpAux.v | 5 ++ projects/lib/GmpNumber.v | 6 +++ projects/lib/gmp_goal.v | 94 ++++++++++++++++++--------------- projects/lib/gmp_proof_manual.v | 37 ++++++++++++- projects/mini-gmp.c | 7 +-- projects/mini-gmp.h | 1 + 6 files changed, 103 insertions(+), 47 deletions(-) diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index c3ff11a..3a4c199 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -314,6 +314,11 @@ Proof. split; tauto. Qed. +Lemma store_uint_array_rec_def2undef: forall x a b l, + store_uint_array_rec x a b l |-- + store_undef_uint_array_rec x a b. +Proof. Admitted. + Lemma store_undef_uint_array_rec_divide: forall x l mid r, 0 <= l <= r -> l <= mid <= r -> diff --git a/projects/lib/GmpNumber.v b/projects/lib/GmpNumber.v index 787c79e..2bae2ab 100755 --- a/projects/lib/GmpNumber.v +++ b/projects/lib/GmpNumber.v @@ -89,6 +89,12 @@ Proof. reflexivity. Qed. +Lemma list_store_Z_compact_reverse_injection: forall l1 l2 n1 n2, + list_store_Z_compact l1 n1 -> + list_store_Z_compact l2 n2 -> + n1 = n2 -> l1 = l2. +Proof. Admitted. + Lemma __list_within_bound_concat_r: forall (l1: list Z) (a: Z), list_within_bound l1 -> 0 <= a < UINT_MOD -> diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v index 4967d19..1e185ca 100644 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -1781,8 +1781,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ . Definition mpn_add_1_safety_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)) (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_pre )) (32)) >= b_pre) |] +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) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1790,7 +1790,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -1802,9 +1803,9 @@ 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_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32))) (l'')) ) + && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) (l'')) ) ** (store_uint_array ap_pre n_pre l_2 ) - ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32))) + ** ((( &( "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' ) @@ -1818,8 +1819,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ . Definition mpn_add_1_safety_wit_3 := -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)) (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_pre )) (32)) < b_pre) |] +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) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1827,7 +1828,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -1839,9 +1841,9 @@ 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_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32))) (l'')) ) + && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) (l'')) ) ** (store_uint_array ap_pre n_pre l_2 ) - ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32))) + ** ((( &( "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' ) @@ -1879,7 +1881,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (0) (l)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD 0) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b_pre * (Z.pow (UINT_MOD) (0)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = 0) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] @@ -1898,8 +1901,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ . Definition mpn_add_1_entail_wit_2_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)) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) , - [| ((unsigned_last_nbits (((Znth i l_3 0) + b_pre )) (32)) < b_pre) |] +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) , + [| ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32)) < b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1907,7 +1910,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_3)) val1_2 ) |] && [| (list_store_Z l'_2 val2_2 ) |] - && [| ((val2_2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1_2 + b_pre )) |] + && [| ((val2_2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1_2 + b_pre )) |] + && [| ((Zlength (l'_2)) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] @@ -1919,11 +1923,10 @@ 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_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_3 0) + b_pre )) (32))) (l''_2)) ) + && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32))) (l''_2)) ) ** (store_uint_array ap_pre n_pre l_3 ) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre i l'_2 ) - ** ((( &( "b" ) )) # UInt |-> 1) |-- EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , [| (0 <= (i + 1 )) |] @@ -1932,7 +1935,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD (i + 1 )) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (1 * (Z.pow (UINT_MOD) ((i + 1 ))) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = (i + 1 )) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] @@ -1948,12 +1952,11 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre (i + 1 ) l' ) ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l'' ) - ** ((( &( "b" ) )) # UInt |-> b_pre) . Definition mpn_add_1_entail_wit_2_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)) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) , - [| ((unsigned_last_nbits (((Znth i l_3 0) + b_pre )) (32)) >= b_pre) |] +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) , + [| ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32)) >= b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1961,7 +1964,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_3)) val1_2 ) |] && [| (list_store_Z l'_2 val2_2 ) |] - && [| ((val2_2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1_2 + b_pre )) |] + && [| ((val2_2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1_2 + b_pre )) |] + && [| ((Zlength (l'_2)) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] @@ -1973,11 +1977,10 @@ 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_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_3 0) + b_pre )) (32))) (l''_2)) ) + && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32))) (l''_2)) ) ** (store_uint_array ap_pre n_pre l_3 ) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre i l'_2 ) - ** ((( &( "b" ) )) # UInt |-> 0) |-- EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , [| (0 <= (i + 1 )) |] @@ -1986,7 +1989,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD (i + 1 )) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (0 * (Z.pow (UINT_MOD) ((i + 1 ))) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = (i + 1 )) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] @@ -2002,11 +2006,10 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre (i + 1 ) l' ) ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l'' ) - ** ((( &( "b" ) )) # UInt |-> b_pre) . Definition mpn_add_1_return_wit_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)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) (i: Z) , +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'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) (i: Z) , [| (i >= n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2014,7 +2017,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] @@ -2032,9 +2036,9 @@ 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 cap2 l'' ) |-- EX (val': Z) , - [| ((val' + (b_pre * (Z.lxor UINT_MOD n_pre) ) ) = (val + b_pre )) |] + [| ((val' + (b * (Z.pow (UINT_MOD) (n_pre)) ) ) = (val + b_pre )) |] && (mpd_store_Z_compact ap_pre val n_pre cap1 ) - ** (mpd_store_Z_compact rp_pre val' n_pre cap2 ) + ** (mpd_store_Z rp_pre val' n_pre cap2 ) . Definition mpn_add_1_partial_solve_wit_1 := @@ -2117,7 +2121,7 @@ forall (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (v Definition mpn_add_1_partial_solve_wit_2 := mpn_add_1_partial_solve_wit_2_pure -> mpn_add_1_partial_solve_wit_2_aux. Definition mpn_add_1_partial_solve_wit_3 := -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)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , +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) |] @@ -2125,7 +2129,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -2149,7 +2154,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -2169,8 +2175,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 := -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)) (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_pre )) (32)) < b_pre) |] +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) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2178,7 +2184,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -2195,7 +2202,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_uint_array rp_pre i l' ) ** (store_uint_array_rec rp_pre i cap2 l'' ) |-- - [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) < b_pre) |] + [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2203,7 +2210,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -2223,8 +2231,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 := -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)) (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_pre )) (32)) >= b_pre) |] +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) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2232,7 +2240,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -2249,7 +2258,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_uint_array rp_pre i l' ) ** (store_uint_array_rec rp_pre i cap2 l'' ) |-- - [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) >= b_pre) |] + [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2257,7 +2266,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 4b544d2..32fbea2 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -11,7 +11,7 @@ Require Import SetsClass.SetsClass. Import SetsNotation. From SimpleC.SL Require Import Mem SeparationLogic. From GmpLib Require Import gmp_goal. Require Import GmpLib.GmpNumber. Import Internal. -Require Import GmpLib.GmpAux. +Require Import GmpLib.GmpAux. Import Aux. Require Import Logic.LogicGenerator.demo932.Interface. Local Open Scope Z_scope. Local Open Scope sets. @@ -416,7 +416,40 @@ Lemma proof_of_mpn_add_1_entail_wit_2_2 : mpn_add_1_entail_wit_2_2. Proof. Admitted. Lemma proof_of_mpn_add_1_return_wit_1 : mpn_add_1_return_wit_1. -Proof. Admitted. +Proof. + pre_process. + unfold mpd_store_Z_compact. + unfold mpd_store_list. + Exists val2. + pose proof (list_store_Z_compact_reverse_injection l l_2 val val). + apply H19 in H2; try tauto. + rewrite <-H2 in H10. + assert (i = n_pre) by lia. + rewrite H20 in H4. + rewrite <- H10 in H4. + rewrite (sublist_self l (Zlength l)) in H4; try tauto. + rewrite <-H2 in H12. + assert (list_store_Z l val). { apply list_store_Z_compact_to_normal. tauto. } + pose proof (list_store_Z_injection l l val1 val). + apply H22 in H4; try tauto. + rewrite H4 in H6. + entailer!. + Exists l. + entailer!. + entailer!; try rewrite H20; try tauto. + - rewrite H10. + entailer!. + unfold mpd_store_Z. + unfold mpd_store_list. + Exists l'. + rewrite H7. + subst i. + entailer!. + rewrite H20. + entailer!. + apply store_uint_array_rec_def2undef. + - rewrite <- H20. tauto. +Qed. Lemma proof_of_mpn_add_1_which_implies_wit_1 : mpn_add_1_which_implies_wit_1. Proof. Admitted. diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 7db66bf..b446b28 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -238,8 +238,8 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) Ensure exists val', mpd_store_Z_compact(ap@pre, val, n@pre, cap1) * - mpd_store_Z_compact(rp@pre, val', n@pre, cap2) && - (val' + __return * (UINT_MOD ^ n@pre) == val + b@pre) + mpd_store_Z(rp@pre, val', n@pre, cap2) && + (val' + __return * Z::pow(UINT_MOD, n@pre) == val + b@pre) */ { /*@ @@ -285,7 +285,8 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) list_store_Z(l', val2) && store_uint_array(rp@pre, i, l') * store_uint_array_rec(rp@pre, i, cap2, l'') && - (val2 + b@pre * (UINT_MOD ^ i) == val1 + b@pre) + (val2 + b * Z::pow(UINT_MOD, i) == val1 + b@pre) && + Zlength(l') == i */ while (i Z) (Z::max : Z -> Z -> Z) + (Z::pow : Z -> Z -> Z) (mpd_store_Z : Z -> Z -> Z -> Z -> Assertion) (mpd_store_Z_compact: Z -> Z -> Z -> Z -> Assertion) (mpd_store_list : Z -> list Z -> Z -> Assertion)