diff --git a/.gitignore b/.gitignore index 17c9381..9acaeaf 100755 --- a/.gitignore +++ b/.gitignore @@ -28,4 +28,7 @@ qcp qualifiedcprogramming sets .gitmodules -_CoqProject \ No newline at end of file +_CoqProject + +.devcontainer/ +.vscode/ \ No newline at end of file diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index c3ff11a..7bbdf01 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -21,6 +21,18 @@ 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_mod_add_uncarry: forall (a b m: Z), + m > 0 -> 0 <= a < m -> 0 <= b < m -> + (a + b) mod m >= b -> + a + b = (a + b) mod m. +Proof. Admitted. + Lemma Z_of_nat_succ: forall (n: nat), Z.of_nat (S n) = Z.of_nat n + 1. Proof. lia. Qed. @@ -314,6 +326,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 21db244..9d2ae7d 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 a70468a..4a9d0ed 100755 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -15,11 +15,11 @@ Local Open Scope Z_scope. Local Open Scope sets. Local Open Scope string. Local Open Scope list. +Require Import Coq.ZArith.ZArith. +Local Open Scope Z_scope. Import naive_C_Rules. Local Open Scope sac. -Definition Zmax := Z.max. - (*----- Function gmp_abs -----*) Definition gmp_abs_safety_wit_1 := @@ -61,7 +61,7 @@ forall (b_pre: Z) (a_pre: Z) , [| (a_pre <= b_pre) |] && emp |-- - [| (b_pre = (Zmax (a_pre) (b_pre))) |] + [| (b_pre = (Z.max (a_pre) (b_pre))) |] && emp . @@ -70,7 +70,7 @@ forall (b_pre: Z) (a_pre: Z) , [| (a_pre > b_pre) |] && emp |-- - [| (a_pre = (Zmax (a_pre) (b_pre))) |] + [| (a_pre = (Z.max (a_pre) (b_pre))) |] && emp . @@ -1753,6 +1753,904 @@ forall (xp_pre: Z) (val: Z) (cap: Z) (n: Z) , ** (store_undef_uint_array_rec xp_pre n cap ) . +(*----- Function mpn_add_1 -----*) + +Definition mpn_add_1_safety_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: (@list Z)) , + [| (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) |] + && ((( &( "i" ) )) # Int |->_) + ** (store_uint_array ap_pre n_pre l ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** ((( &( "b" ) )) # UInt |-> b_pre) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) + ** (store_uint_array rp_pre cap2 l2 ) +|-- + [| (0 <= INT_MAX) |] + && [| ((INT_MIN) <= 0) |] +. + +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)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) (a: Z) (l''': (@list Z)) , + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (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) |] + && [| (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 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 ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| ((i + 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (i + 1 )) |] +. + +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)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) (a: Z) (l''': (@list Z)) , + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (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) |] + && [| (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 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 ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| ((i + 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (i + 1 )) |] +. + +Definition mpn_add_1_entail_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)) , + [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array_rec rp_pre 0 cap2 l2 ) + ** (store_uint_array rp_pre 0 nil ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +|-- + EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , + [| (0 <= 0) |] + && [| (0 <= n_pre) |] + && [| (list_store_Z_compact l val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (0) (l)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((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) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 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 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre 0 l' ) + ** (store_uint_array_rec rp_pre 0 cap2 l'' ) +. + +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) |] + && [| (list_store_Z_compact l_3 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_3)) val1_2 ) |] + && [| (list_store_Z l'_2 val2_2 ) |] + && [| ((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) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32))) ((app (l'_2) ((cons (a) (nil)))))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) + ** (store_uint_array ap_pre n_pre l_3 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +|-- + EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , + [| (0 <= (i + 1 )) |] + && [| ((i + 1 ) <= n_pre) |] + && [| (list_store_Z_compact l val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) ((i + 1 )) (l)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((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) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 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 ) + ** (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'' ) +. + +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) |] + && [| (list_store_Z_compact l_3 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_3)) val1_2 ) |] + && [| (list_store_Z l'_2 val2_2 ) |] + && [| ((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) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32))) ((app (l'_2) ((cons (a) (nil)))))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) + ** (store_uint_array ap_pre n_pre l_3 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +|-- + EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , + [| (0 <= (i + 1 )) |] + && [| ((i + 1 ) <= n_pre) |] + && [| (list_store_Z_compact l val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) ((i + 1 )) (l)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((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) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 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 ) + ** (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'' ) +. + +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)) (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) |] + && [| (list_store_Z_compact l val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l)) 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_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 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 ) + ** (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'' ) +|-- + EX (val': Z) , + [| ((val' + (b * (Z.pow (UINT_MOD) (n_pre)) ) ) = (val + b_pre )) |] + && (mpd_store_Z_compact ap_pre val n_pre cap1 ) + ** (mpd_store_Z rp_pre val' n_pre cap2 ) +. + +Definition mpn_add_1_partial_solve_wit_1 := +forall (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) , + [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (mpd_store_Z_compact ap_pre val n_pre cap1 ) + ** (store_uint_array rp_pre cap2 l2 ) +|-- + [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (mpd_store_Z_compact ap_pre val n_pre cap1 ) + ** (store_uint_array rp_pre cap2 l2 ) +. + +Definition mpn_add_1_partial_solve_wit_2_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)) , + [| (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) |] + && ((( &( "i" ) )) # Int |-> 0) + ** (store_uint_array ap_pre n_pre l ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** ((( &( "b" ) )) # UInt |-> b_pre) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) + ** (store_uint_array rp_pre cap2 l2 ) +|-- + [| ((Zlength (l2)) = cap2) |] +. + +Definition mpn_add_1_partial_solve_wit_2_aux := +forall (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) , + [| (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 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre cap2 l2 ) +|-- + [| ((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 rp_pre cap2 l2 ) + ** (store_uint_array ap_pre n_pre l ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +. + +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)) (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 ) + ** (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'' ) +|-- + [| (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) |] + && (((ap_pre + (i * sizeof(UINT) ) )) # UInt |-> (Znth i l_2 0)) + ** (store_uint_array_missing_i_rec ap_pre i 0 n_pre l_2 ) + ** (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'' ) +. + +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) |] + && [| (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 |-> 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'' ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] +. + +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) |] + && [| (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 ) + ** (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'' ) +|-- + [| (0 <= i) |] + && [| (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) |] + && [| (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 rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +. + +Definition mpn_add_1_partial_solve_wit_4 := mpn_add_1_partial_solve_wit_4_pure -> mpn_add_1_partial_solve_wit_4_aux. + +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) |] + && [| (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 |-> 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'' ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] +. + +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) |] + && [| (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 ) + ** (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'' ) +|-- + [| (0 <= i) |] + && [| (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) |] + && [| (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 rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +. + +Definition mpn_add_1_partial_solve_wit_5 := mpn_add_1_partial_solve_wit_5_pure -> mpn_add_1_partial_solve_wit_5_aux. + +Definition mpn_add_1_partial_solve_wit_6 := +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) (a: Z) (l''': (@list Z)) , + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (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) |] + && [| (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_rec rp_pre (i + 1 ) cap2 l''' ) + ** (store_uint_array rp_pre (i + 1 ) (app (l') ((cons (a) (nil)))) ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +|-- + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (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) |] + && [| (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) |] + && (((rp_pre + (i * sizeof(UINT) ) )) # UInt |->_) + ** (store_uint_array_missing_i_rec rp_pre i 0 (i + 1 ) (app (l') ((cons (a) (nil)))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +. + +Definition mpn_add_1_partial_solve_wit_7 := +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) (a: Z) (l''': (@list Z)) , + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (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) |] + && [| (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_rec rp_pre (i + 1 ) cap2 l''' ) + ** (store_uint_array rp_pre (i + 1 ) (app (l') ((cons (a) (nil)))) ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +|-- + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (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) |] + && [| (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) |] + && (((rp_pre + (i * sizeof(UINT) ) )) # UInt |->_) + ** (store_uint_array_missing_i_rec rp_pre i 0 (i + 1 ) (app (l') ((cons (a) (nil)))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +. + +Definition mpn_add_1_which_implies_wit_1 := +forall (n_pre: Z) (ap_pre: Z) (cap1: Z) (val: Z) , + (mpd_store_Z_compact ap_pre val n_pre cap1 ) +|-- + EX (l: (@list Z)) , + [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && (store_uint_array ap_pre n_pre l ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +. + +Definition mpn_add_1_which_implies_wit_2 := +forall (rp_pre: Z) (cap2: Z) (l2: (@list Z)) , + [| ((Zlength (l2)) = cap2) |] + && (store_uint_array rp_pre cap2 l2 ) +|-- + [| ((Zlength (l2)) = cap2) |] + && (store_uint_array_rec rp_pre 0 cap2 l2 ) + ** (store_uint_array rp_pre 0 nil ) +. + +Definition mpn_add_1_which_implies_wit_3 := +forall (n_pre: Z) (rp_pre: Z) (cap2: Z) (l'': (@list Z)) (l': (@list Z)) (i: Z) , + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && (store_uint_array rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) +|-- + EX (a: Z) (l''': (@list Z)) , + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) + ** (store_uint_array rp_pre (i + 1 ) (app (l') ((cons (a) (nil)))) ) +. + (*----- Function mpz_clear -----*) Definition mpz_clear_return_wit_1_1 := @@ -2851,6 +3749,27 @@ Axiom proof_of_mpn_normalized_size_return_wit_1_2 : mpn_normalized_size_return_w Axiom proof_of_mpn_normalized_size_partial_solve_wit_1 : mpn_normalized_size_partial_solve_wit_1. Axiom proof_of_mpn_normalized_size_partial_solve_wit_2 : mpn_normalized_size_partial_solve_wit_2. Axiom proof_of_mpn_normalized_size_which_implies_wit_1 : mpn_normalized_size_which_implies_wit_1. +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 : 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. +Axiom proof_of_mpn_add_1_partial_solve_wit_2 : mpn_add_1_partial_solve_wit_2. +Axiom proof_of_mpn_add_1_partial_solve_wit_3 : mpn_add_1_partial_solve_wit_3. +Axiom proof_of_mpn_add_1_partial_solve_wit_4_pure : mpn_add_1_partial_solve_wit_4_pure. +Axiom proof_of_mpn_add_1_partial_solve_wit_4 : mpn_add_1_partial_solve_wit_4. +Axiom proof_of_mpn_add_1_partial_solve_wit_5_pure : mpn_add_1_partial_solve_wit_5_pure. +Axiom proof_of_mpn_add_1_partial_solve_wit_5 : mpn_add_1_partial_solve_wit_5. +Axiom proof_of_mpn_add_1_partial_solve_wit_6 : mpn_add_1_partial_solve_wit_6. +Axiom proof_of_mpn_add_1_partial_solve_wit_7 : mpn_add_1_partial_solve_wit_7. +Axiom proof_of_mpn_add_1_which_implies_wit_1 : mpn_add_1_which_implies_wit_1. +Axiom proof_of_mpn_add_1_which_implies_wit_2 : mpn_add_1_which_implies_wit_2. +Axiom proof_of_mpn_add_1_which_implies_wit_3 : mpn_add_1_which_implies_wit_3. Axiom proof_of_mpz_clear_return_wit_1_1 : mpz_clear_return_wit_1_1. Axiom proof_of_mpz_clear_return_wit_1_2 : mpz_clear_return_wit_1_2. Axiom proof_of_mpz_clear_return_wit_1_3 : mpz_clear_return_wit_1_3. diff --git a/projects/lib/gmp_proof_auto.v b/projects/lib/gmp_proof_auto.v index d7e29ef..37f0bbb 100755 --- a/projects/lib/gmp_proof_auto.v +++ b/projects/lib/gmp_proof_auto.v @@ -15,6 +15,8 @@ Local Open Scope Z_scope. Local Open Scope sets. Local Open Scope string. Local Open Scope list. +Require Import Coq.ZArith.ZArith. +Local Open Scope Z_scope. Import naive_C_Rules. Local Open Scope sac. @@ -141,6 +143,45 @@ Proof. Admitted. Lemma proof_of_mpn_normalized_size_partial_solve_wit_2 : mpn_normalized_size_partial_solve_wit_2. Proof. Admitted. +Lemma proof_of_mpn_add_1_safety_wit_1 : mpn_add_1_safety_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_safety_wit_2 : mpn_add_1_safety_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_safety_wit_3 : mpn_add_1_safety_wit_3. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_1 : mpn_add_1_partial_solve_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_2_pure : mpn_add_1_partial_solve_wit_2_pure. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_2 : mpn_add_1_partial_solve_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_3 : mpn_add_1_partial_solve_wit_3. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_4_pure : mpn_add_1_partial_solve_wit_4_pure. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_4 : mpn_add_1_partial_solve_wit_4. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_5_pure : mpn_add_1_partial_solve_wit_5_pure. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_5 : mpn_add_1_partial_solve_wit_5. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_6 : mpn_add_1_partial_solve_wit_6. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_7 : mpn_add_1_partial_solve_wit_7. +Proof. Admitted. + Lemma proof_of_mpz_clear_return_wit_1_3 : mpz_clear_return_wit_1_3. Proof. Admitted. @@ -202,5 +243,4 @@ Lemma proof_of_mpz_realloc_partial_solve_wit_9 : mpz_realloc_partial_solve_wit_9 Proof. Admitted. Lemma proof_of_mpz_realloc_partial_solve_wit_10 : mpz_realloc_partial_solve_wit_10. -Proof. Admitted. - +Proof. Admitted. \ No newline at end of file diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 2e51564..fc2b6fa 100755 --- 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. @@ -30,17 +30,11 @@ Proof. pre_process. Qed. Lemma proof_of_gmp_max_return_wit_1_1 : gmp_max_return_wit_1_1. Proof. pre_process. - entailer!. - unfold Zmax. - rewrite Z.max_r; lia. Qed. Lemma proof_of_gmp_max_return_wit_1_2 : gmp_max_return_wit_1_2. Proof. pre_process. - entailer!. - unfold Zmax. - rewrite Z.max_l; lia. Qed. Lemma proof_of_gmp_cmp_return_wit_1_2 : gmp_cmp_return_wit_1_2. @@ -412,6 +406,408 @@ Proof. tauto. Qed. +Lemma proof_of_mpn_add_1_entail_wit_1 : mpn_add_1_entail_wit_1. +Proof. + pre_process. + Exists l2 nil 0 0 l_2. + entailer!. + - unfold list_store_Z. + split. + + simpl. tauto. + + simpl. tauto. + - rewrite (sublist_nil l_2 0 0); try lia. + unfold list_store_Z. + split. + + simpl. tauto. + + simpl. tauto. +Qed. + +Lemma proof_of_mpn_add_1_entail_wit_2 : mpn_add_1_entail_wit_2. +Proof. + pre_process. + prop_apply (store_uint_range &("b") b). + entailer!. +Qed. + +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 H14. + assert (i - i = 0) by lia. + 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). { + unfold replace_Znth. + unfold Z.to_nat. + unfold replace_nth. + reflexivity. + } + 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 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 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 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. + } + 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 H28 in H12. + rewrite H14 in H12. + assert (new_b * 4294967296 ^ i + val2_2 = (val2_2 + new_b * 4294967296 ^ i)) by lia. + rewrite H29 in H12. + tauto. + subst new_b. + unfold unsigned_last_nbits. + assert (2 ^ 32 = 4294967296). { nia. } + 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 H28 in H9; try tauto. + } + + assert (i < Zlength l_3). { + subst l_3. + 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 <-H31. + apply H30. + lia. + subst l_3. + rewrite Zlength_correct in H29. + lia. + rewrite Zlength_correct in H29. + 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 H17. + lia. + apply list_within_bound_Znth. + lia. + unfold list_store_Z_compact in H9. + tauto. + - pose proof (Zlength_sublist0 i l'_2). + lia. +Qed. + +Lemma proof_of_mpn_add_1_entail_wit_3_2 : mpn_add_1_entail_wit_3_2. +Proof. + pre_process. + rewrite replace_Znth_app_r. + - Exists l'''. + rewrite H14. + assert (i - i = 0) by lia. + 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). { + unfold replace_Znth. + unfold Z.to_nat. + unfold replace_nth. + reflexivity. + } + 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 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 H28. + rewrite <- H13. + assert (Znth i l_3 0 + b = new_b). + { + subst new_b. + unfold unsigned_last_nbits. + unfold unsigned_last_nbits in H3. + assert (2^32 = 4294967296). { nia. } + 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_uncarry; try lia; try tauto. + } + assert (b * 4294967296 ^ i + Znth i l_3 0 * 4294967296 ^ i = new_b * 4294967296 ^ i + 0 * 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 H28 in H12. + rewrite H14 in H12. + assert (new_b * 4294967296 ^ i + val2_2 = (val2_2 + new_b * 4294967296 ^ i)) by lia. + rewrite H29 in H12. + tauto. + subst new_b. + unfold unsigned_last_nbits. + assert (2 ^ 32 = 4294967296). { nia. } + 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 H28 in H9; try tauto. + } + + assert (i < Zlength l_3). { + subst l_3. + 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 <-H31. + apply H30. + lia. + subst l_3. + rewrite Zlength_correct in H29. + lia. + rewrite Zlength_correct in H29. + 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 H17. + lia. + apply list_within_bound_Znth. + lia. + unfold list_store_Z_compact in H9. + tauto. + - pose proof (Zlength_sublist0 i l'_2). + lia. +Qed. + +Lemma proof_of_mpn_add_1_return_wit_1 : mpn_add_1_return_wit_1. +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. + pre_process. + unfold mpd_store_Z_compact. + Intros l. + Exists l. + unfold mpd_store_list. + entailer!. + subst n_pre. + entailer!. +Qed. + +Lemma proof_of_mpn_add_1_which_implies_wit_2 : mpn_add_1_which_implies_wit_2. +Proof. + pre_process. + pose proof (store_uint_array_divide rp_pre cap2 l2 0). + pose proof (Zlength_nonneg l2). + specialize (H0 ltac:(lia) ltac:(lia)). + destruct H0 as [H0 _]. + simpl in H0. + entailer!. + rewrite (sublist_nil l2 0 0) in H0; [ | lia]. + sep_apply H0. + entailer!. + unfold store_uint_array, store_uint_array_rec. + unfold store_array. + rewrite (sublist_self l2 cap2); [ | lia ]. + assert (rp_pre + 0 = rp_pre). { lia. } + rewrite H2; clear H2. + assert (cap2 - 0 = cap2). { lia. } + rewrite H2; clear H2. + reflexivity. +Qed. + +Lemma proof_of_mpn_add_1_which_implies_wit_3 : mpn_add_1_which_implies_wit_3. +Proof. + pre_process. + destruct l''. { + unfold store_uint_array_rec. + simpl. + entailer!. + } + pose proof (store_uint_array_rec_cons rp_pre i cap2 z l'' ltac:(lia)). + sep_apply H2. + Exists z l''. + entailer!. + assert (i = 0 \/ i > 0). { lia. } + destruct H3. + + subst. + simpl. + entailer!. + simpl in H2. + assert (rp_pre + 0 = rp_pre). { lia. } + rewrite H3. + rewrite H3 in H2. + clear H3. + pose proof (store_uint_array_empty rp_pre l'). + sep_apply H3. + rewrite logic_equiv_andp_comm. + rewrite logic_equiv_coq_prop_andp_sepcon. + Intros. + subst l'. + rewrite app_nil_l. + unfold store_uint_array. + unfold store_array. + unfold store_array_rec. + simpl. + assert (rp_pre + 0 = rp_pre). { lia. } + rewrite H4; clear H4. + entailer!. + + pose proof (Aux.uint_array_rec_to_uint_array rp_pre 0 i (sublist 0 i l') ltac:(lia)). + destruct H4 as [_ H4]. + assert (rp_pre + sizeof(UINT) * 0 = rp_pre). { lia. } + rewrite H5 in H4; clear H5. + assert (i - 0 = i). { lia. } + rewrite H5 in H4; clear H5. + pose proof (Aux.uint_array_rec_to_uint_array rp_pre 0 (i + 1) (sublist 0 i l' ++ z :: nil) ltac:(lia)). + destruct H5 as [H5 _]. + assert (i + 1 - 0 = i + 1). { lia. } + rewrite H6 in H5; clear H6. + assert (rp_pre + sizeof(UINT) * 0 = rp_pre). { lia. } + rewrite H6 in H5; clear H6. + pose proof (uint_array_rec_to_uint_array rp_pre 0 i l'). + specialize (H6 H). + assert ((rp_pre + sizeof ( UINT ) * 0) = rp_pre) by lia. + rewrite H7 in H6; clear H7. + assert ((i-0) = i) by lia. + rewrite H7 in H6; clear H7. + destruct H6 as [_ H6]. + sep_apply H6. + (* pose proof (uint_array_rec_to_uint_array rp_pre 0 (i+1) (l' ++ z :: nil)). + assert (H_i_plus_1 : 0 <= i + 1) by lia. + specialize (H7 H_i_plus_1); clear H_i_plus_1. + destruct H7 as [H7 _]. + assert (i + 1 - 0 = i + 1) by lia. + rewrite H8 in H7; clear H8. + assert ((rp_pre + sizeof ( UINT ) * 0) = rp_pre) by lia. + rewrite H8 in H7; clear H8. + rewrite <-H7. + clear H6. + clear H7. *) + pose proof (store_uint_array_divide_rec rp_pre (i+1) (l' ++ z :: nil) i). + assert (H_tmp: 0 <= i <= i+1) by lia. + specialize (H7 H_tmp); clear H_tmp. + rewrite <- store_uint_array_single. + sep_apply store_uint_array_rec_divide_rev. + entailer!. + lia. +Qed. Lemma proof_of_mpz_clear_return_wit_1_1 : mpz_clear_return_wit_1_1. Proof. diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index a60ffba..e6a2d2b 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -223,23 +223,94 @@ mpn_normalized_size (unsigned int *xp, int n) } /* 多精度数ap 加上单精度数b，返回最后产生的进位 */ -/*unsigned int +unsigned int mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) +/*@ + With val l2 cap1 cap2 + Require + mpd_store_Z_compact(ap, val, n, cap1) * + store_uint_array(rp, cap2, l2) && + Zlength(l2) == cap2 && + cap2 >= n && + cap1 <= 100000000 && + cap2 <= 100000000 && + n > 0 && n <= cap1 + Ensure + exists val', + mpd_store_Z_compact(ap@pre, val, n@pre, cap1) * + mpd_store_Z(rp@pre, val', n@pre, cap2) && + (val' + __return * Z::pow(UINT_MOD, n@pre) == val + b@pre) +*/ { + /*@ + mpd_store_Z_compact(ap@pre, val, n@pre, cap1) + which implies + exists l, + n@pre <= cap1 && + Zlength(l) == n@pre && + cap1 <= 100000000 && + store_uint_array(ap@pre, n@pre, l) * + store_undef_uint_array_rec(ap@pre, n@pre, cap1) && + list_store_Z_compact(l, val) + */ int i; //assert (n > 0); i = 0; + /* do { unsigned int r = ap[i] + b; // Carry out b = (r < b); rp[i] = r; + ++i; } - while (++i < n); + while (i < n); + */ + + /*@ + store_uint_array(rp@pre, cap2, l2) && Zlength(l2) == cap2 + which implies + store_uint_array_rec(rp@pre, 0, cap2, l2) * store_uint_array(rp@pre, 0, nil) && + Zlength(l2) == cap2 + */ + + /*@Inv + exists l l' l'' val1 val2, + 0 <= i && i <= n@pre && + list_store_Z_compact(l, val) && n@pre <= cap1 && + store_uint_array(ap@pre, n@pre, l) * + store_undef_uint_array_rec(ap@pre, n@pre, cap1) && + list_store_Z(sublist(0, i, l), val1) && + list_store_Z(l', val2) && + store_uint_array(rp@pre, i, l') * + store_uint_array_rec(rp@pre, i, cap2, l'') && + (val2 + b * Z::pow(UINT_MOD, i) == val1 + b@pre) && + Zlength(l') == i + */ + while (i