From 94581ea60dd84532bb2d37f84c7d9cf8f5d4f70c Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sat, 21 Jun 2025 16:03:04 +0000 Subject: [PATCH 1/8] first version annotation for mpn_add_n --- projects/lib/gmp_goal.v | 2218 +++++++++++++++++++++++++++++++ projects/lib/gmp_proof_auto.v | 72 + projects/lib/gmp_proof_manual.v | 33 + projects/mini-gmp.c | 86 +- projects/mini-gmp.h | 2 +- 5 files changed, 2407 insertions(+), 4 deletions(-) diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v index 2df150a..448952c 100755 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -2651,6 +2651,2189 @@ forall (n_pre: Z) (rp_pre: Z) (cap2: Z) (l'': (@list Z)) (l': (@list Z)) (i: Z) ** (store_uint_array rp_pre (i + 1 ) (app (l') ((cons (a) (nil)))) ) . +(*----- Function mpn_add_n -----*) + +Definition mpn_add_n_safety_wit_1 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) , + [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array_rec rp_pre 0 cap_r l_r ) + ** (store_uint_array rp_pre 0 nil ) + ** ((( &( "cy" ) )) # UInt |->_) + ** ((( &( "i" ) )) # Int |->_) + ** (store_uint_array bp_pre n_pre l_b ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| (0 <= INT_MAX) |] + && [| ((INT_MIN) <= 0) |] +. + +Definition mpn_add_n_safety_wit_2 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) , + [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array_rec rp_pre 0 cap_r l_r ) + ** (store_uint_array rp_pre 0 nil ) + ** ((( &( "cy" ) )) # UInt |->_) + ** ((( &( "i" ) )) # Int |-> 0) + ** (store_uint_array bp_pre n_pre l_b ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| (0 <= INT_MAX) |] + && [| ((INT_MIN) <= 0) |] +. + +Definition mpn_add_n_safety_wit_3 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) , + [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) ((app (l_r_prefix) ((cons (a) (nil)))))) ) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) + ** ((( &( "b" ) )) # UInt |-> (Znth i l_b_2 0)) + ** ((( &( "a" ) )) # UInt |-> (Znth i l_a_2 0)) + ** ((( &( "cy" ) )) # UInt |-> (0 + 1 )) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| ((i + 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (i + 1 )) |] +. + +Definition mpn_add_n_safety_wit_4 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) , + [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) ((app (l_r_prefix) ((cons (a) (nil)))))) ) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) + ** ((( &( "b" ) )) # UInt |-> (Znth i l_b_2 0)) + ** ((( &( "a" ) )) # UInt |-> (Znth i l_a_2 0)) + ** ((( &( "cy" ) )) # UInt |-> (0 + 0 )) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| ((i + 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (i + 1 )) |] +. + +Definition mpn_add_n_safety_wit_5 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) , + [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) ((app (l_r_prefix) ((cons (a) (nil)))))) ) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) + ** ((( &( "b" ) )) # UInt |-> (Znth i l_b_2 0)) + ** ((( &( "a" ) )) # UInt |-> (Znth i l_a_2 0)) + ** ((( &( "cy" ) )) # UInt |-> (1 + 1 )) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| ((i + 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (i + 1 )) |] +. + +Definition mpn_add_n_safety_wit_6 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) , + [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) ((app (l_r_prefix) ((cons (a) (nil)))))) ) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) + ** ((( &( "b" ) )) # UInt |-> (Znth i l_b_2 0)) + ** ((( &( "a" ) )) # UInt |-> (Znth i l_a_2 0)) + ** ((( &( "cy" ) )) # UInt |-> (1 + 0 )) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| ((i + 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (i + 1 )) |] +. + +Definition mpn_add_n_entail_wit_1 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a_2: (@list Z)) (l_b_2: (@list Z)) , + [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b_2)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a_2)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array_rec rp_pre 0 cap_r l_r ) + ** (store_uint_array rp_pre 0 nil ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) +|-- + EX (l_r_suffix: (@list Z)) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b: (@list Z)) (l_a: (@list Z)) , + [| (0 <= 0) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z (sublist (0) (0) (l_a)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (0) (l_b)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = 0) |] + && [| ((val_r_prefix + (0 * (Z.pow (UINT_MOD) (0)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b_2)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a_2)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_uint_array bp_pre n_pre l_b ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre 0 l_r_prefix ) + ** (store_uint_array_rec rp_pre 0 cap_r l_r_suffix ) +. + +Definition mpn_add_n_entail_wit_2 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) , + [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && ((( &( "i" ) )) # Int |-> i) + ** ((( &( "cy" ) )) # UInt |-> cy) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && ((( &( "cy" ) )) # UInt |-> cy) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +. + +Definition mpn_add_n_entail_wit_3_1 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a_2: (@list Z)) (l_b_2: (@list Z)) (l_r_suffix_2: (@list Z)) (cy: Z) (l_r_prefix_2: (@list Z)) (val_r_prefix_2: Z) (val_b_prefix_2: Z) (val_a_prefix_2: Z) (l_b_3: (@list Z)) (l_a_3: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) , + [| (l_r_suffix_2 = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32)) >= (Znth i l_b_3 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_3 val_a ) |] + && [| (list_store_Z_compact l_b_3 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_3)) val_a_prefix_2 ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_3)) val_b_prefix_2 ) |] + && [| (list_store_Z l_r_prefix_2 val_r_prefix_2 ) |] + && [| ((Zlength (l_r_prefix_2)) = i) |] + && [| ((val_r_prefix_2 + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix_2 + val_b_prefix_2 )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b_2)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a_2)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32))) ((app (l_r_prefix_2) ((cons (a) (nil)))))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array bp_pre n_pre l_b_3 ) + ** (store_uint_array ap_pre n_pre l_a_3 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +|-- + EX (l_r_suffix: (@list Z)) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b: (@list Z)) (l_a: (@list Z)) , + [| (0 <= (i + 1 )) |] + && [| ((i + 1 ) <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z (sublist (0) ((i + 1 )) (l_a)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) ((i + 1 )) (l_b)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = (i + 1 )) |] + && [| ((val_r_prefix + ((1 + 0 ) * (Z.pow (UINT_MOD) ((i + 1 ))) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b_2)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a_2)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_uint_array bp_pre n_pre l_b ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre (i + 1 ) l_r_prefix ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix ) +. + +Definition mpn_add_n_entail_wit_3_2 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a_2: (@list Z)) (l_b_2: (@list Z)) (l_r_suffix_2: (@list Z)) (cy: Z) (l_r_prefix_2: (@list Z)) (val_r_prefix_2: Z) (val_b_prefix_2: Z) (val_a_prefix_2: Z) (l_b_3: (@list Z)) (l_a_3: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) , + [| (l_r_suffix_2 = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32)) < (Znth i l_b_3 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_3 val_a ) |] + && [| (list_store_Z_compact l_b_3 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_3)) val_a_prefix_2 ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_3)) val_b_prefix_2 ) |] + && [| (list_store_Z l_r_prefix_2 val_r_prefix_2 ) |] + && [| ((Zlength (l_r_prefix_2)) = i) |] + && [| ((val_r_prefix_2 + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix_2 + val_b_prefix_2 )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b_2)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a_2)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32))) ((app (l_r_prefix_2) ((cons (a) (nil)))))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array bp_pre n_pre l_b_3 ) + ** (store_uint_array ap_pre n_pre l_a_3 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +|-- + EX (l_r_suffix: (@list Z)) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b: (@list Z)) (l_a: (@list Z)) , + [| (0 <= (i + 1 )) |] + && [| ((i + 1 ) <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z (sublist (0) ((i + 1 )) (l_a)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) ((i + 1 )) (l_b)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = (i + 1 )) |] + && [| ((val_r_prefix + ((1 + 1 ) * (Z.pow (UINT_MOD) ((i + 1 ))) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b_2)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a_2)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_uint_array bp_pre n_pre l_b ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre (i + 1 ) l_r_prefix ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix ) +. + +Definition mpn_add_n_entail_wit_3_3 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a_2: (@list Z)) (l_b_2: (@list Z)) (l_r_suffix_2: (@list Z)) (cy: Z) (l_r_prefix_2: (@list Z)) (val_r_prefix_2: Z) (val_b_prefix_2: Z) (val_a_prefix_2: Z) (l_b_3: (@list Z)) (l_a_3: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) , + [| (l_r_suffix_2 = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32)) >= (Znth i l_b_3 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_3 val_a ) |] + && [| (list_store_Z_compact l_b_3 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_3)) val_a_prefix_2 ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_3)) val_b_prefix_2 ) |] + && [| (list_store_Z l_r_prefix_2 val_r_prefix_2 ) |] + && [| ((Zlength (l_r_prefix_2)) = i) |] + && [| ((val_r_prefix_2 + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix_2 + val_b_prefix_2 )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b_2)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a_2)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32))) ((app (l_r_prefix_2) ((cons (a) (nil)))))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array bp_pre n_pre l_b_3 ) + ** (store_uint_array ap_pre n_pre l_a_3 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +|-- + EX (l_r_suffix: (@list Z)) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b: (@list Z)) (l_a: (@list Z)) , + [| (0 <= (i + 1 )) |] + && [| ((i + 1 ) <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z (sublist (0) ((i + 1 )) (l_a)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) ((i + 1 )) (l_b)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = (i + 1 )) |] + && [| ((val_r_prefix + ((0 + 0 ) * (Z.pow (UINT_MOD) ((i + 1 ))) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b_2)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a_2)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_uint_array bp_pre n_pre l_b ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre (i + 1 ) l_r_prefix ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix ) +. + +Definition mpn_add_n_entail_wit_3_4 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a_2: (@list Z)) (l_b_2: (@list Z)) (l_r_suffix_2: (@list Z)) (cy: Z) (l_r_prefix_2: (@list Z)) (val_r_prefix_2: Z) (val_b_prefix_2: Z) (val_a_prefix_2: Z) (l_b_3: (@list Z)) (l_a_3: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) , + [| (l_r_suffix_2 = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32)) < (Znth i l_b_3 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_3 val_a ) |] + && [| (list_store_Z_compact l_b_3 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_3)) val_a_prefix_2 ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_3)) val_b_prefix_2 ) |] + && [| (list_store_Z l_r_prefix_2 val_r_prefix_2 ) |] + && [| ((Zlength (l_r_prefix_2)) = i) |] + && [| ((val_r_prefix_2 + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix_2 + val_b_prefix_2 )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b_2)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a_2)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_3 0) + cy )) (32)) + (Znth i l_b_3 0) )) (32))) ((app (l_r_prefix_2) ((cons (a) (nil)))))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array bp_pre n_pre l_b_3 ) + ** (store_uint_array ap_pre n_pre l_a_3 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +|-- + EX (l_r_suffix: (@list Z)) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b: (@list Z)) (l_a: (@list Z)) , + [| (0 <= (i + 1 )) |] + && [| ((i + 1 ) <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z (sublist (0) ((i + 1 )) (l_a)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) ((i + 1 )) (l_b)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = (i + 1 )) |] + && [| ((val_r_prefix + ((0 + 1 ) * (Z.pow (UINT_MOD) ((i + 1 ))) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b_2)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a_2)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_uint_array bp_pre n_pre l_b ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre (i + 1 ) l_r_prefix ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix ) +. + +Definition mpn_add_n_return_wit_1 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a_2: (@list Z)) (l_b_2: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b: (@list Z)) (l_a: (@list Z)) (i: Z) , + [| (i >= n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b_2)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a_2)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_uint_array bp_pre n_pre l_b ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) +|-- + EX (val_r_out: Z) , + [| ((val_r_out + (cy * (Z.pow (UINT_MOD) (n_pre)) ) ) = (val_a + val_b )) |] + && (mpd_store_Z_compact ap_pre val_a n_pre cap_a ) + ** (mpd_store_Z_compact bp_pre val_b n_pre cap_b ) + ** (mpd_store_Z rp_pre val_r_out n_pre cap_r ) +. + +Definition mpn_add_n_partial_solve_wit_1 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) , + [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (mpd_store_Z_compact ap_pre val_a n_pre cap_a ) + ** (mpd_store_Z_compact bp_pre val_b n_pre cap_b ) + ** (store_uint_array rp_pre cap_r l_r ) +|-- + [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (mpd_store_Z_compact ap_pre val_a n_pre cap_a ) + ** (mpd_store_Z_compact bp_pre val_b n_pre cap_b ) + ** (store_uint_array rp_pre cap_r l_r ) +. + +Definition mpn_add_n_partial_solve_wit_2 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) , + [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (mpd_store_Z_compact bp_pre val_b n_pre cap_b ) + ** (store_uint_array rp_pre cap_r l_r ) +|-- + [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (mpd_store_Z_compact bp_pre val_b n_pre cap_b ) + ** (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_uint_array rp_pre cap_r l_r ) +. + +Definition mpn_add_n_partial_solve_wit_3_pure := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) , + [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && ((( &( "cy" ) )) # UInt |->_) + ** ((( &( "i" ) )) # Int |->_) + ** (store_uint_array bp_pre n_pre l_b ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) + ** (store_uint_array rp_pre cap_r l_r ) +|-- + [| ((Zlength (l_r)) = cap_r) |] +. + +Definition mpn_add_n_partial_solve_wit_3_aux := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) , + [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array bp_pre n_pre l_b ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_uint_array rp_pre cap_r l_r ) +|-- + [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre cap_r l_r ) + ** (store_uint_array bp_pre n_pre l_b ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) +. + +Definition mpn_add_n_partial_solve_wit_3 := mpn_add_n_partial_solve_wit_3_pure -> mpn_add_n_partial_solve_wit_3_aux. + +Definition mpn_add_n_partial_solve_wit_4 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) , + [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) +|-- + [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (((ap_pre + (i * sizeof(UINT) ) )) # UInt |-> (Znth i l_a_2 0)) + ** (store_uint_array_missing_i_rec ap_pre i 0 n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) +. + +Definition mpn_add_n_partial_solve_wit_5 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) , + [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) +|-- + [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (((bp_pre + (i * sizeof(UINT) ) )) # UInt |-> (Znth i l_b_2 0)) + ** (store_uint_array_missing_i_rec bp_pre i 0 n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) +. + +Definition mpn_add_n_partial_solve_wit_6_pure := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) + ** ((( &( "b" ) )) # UInt |-> (Znth i l_b_2 0)) + ** ((( &( "a" ) )) # UInt |-> (Znth i l_a_2 0)) + ** ((( &( "cy" ) )) # UInt |-> (0 + 1 )) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] +. + +Definition mpn_add_n_partial_solve_wit_6_aux := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) +|-- + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +. + +Definition mpn_add_n_partial_solve_wit_6 := mpn_add_n_partial_solve_wit_6_pure -> mpn_add_n_partial_solve_wit_6_aux. + +Definition mpn_add_n_partial_solve_wit_7_pure := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) + ** ((( &( "b" ) )) # UInt |-> (Znth i l_b_2 0)) + ** ((( &( "a" ) )) # UInt |-> (Znth i l_a_2 0)) + ** ((( &( "cy" ) )) # UInt |-> (0 + 0 )) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] +. + +Definition mpn_add_n_partial_solve_wit_7_aux := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) +|-- + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +. + +Definition mpn_add_n_partial_solve_wit_7 := mpn_add_n_partial_solve_wit_7_pure -> mpn_add_n_partial_solve_wit_7_aux. + +Definition mpn_add_n_partial_solve_wit_8_pure := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) + ** ((( &( "b" ) )) # UInt |-> (Znth i l_b_2 0)) + ** ((( &( "a" ) )) # UInt |-> (Znth i l_a_2 0)) + ** ((( &( "cy" ) )) # UInt |-> (1 + 1 )) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] +. + +Definition mpn_add_n_partial_solve_wit_8_aux := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) +|-- + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +. + +Definition mpn_add_n_partial_solve_wit_8 := mpn_add_n_partial_solve_wit_8_pure -> mpn_add_n_partial_solve_wit_8_aux. + +Definition mpn_add_n_partial_solve_wit_9_pure := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32))) + ** ((( &( "b" ) )) # UInt |-> (Znth i l_b_2 0)) + ** ((( &( "a" ) )) # UInt |-> (Znth i l_a_2 0)) + ** ((( &( "cy" ) )) # UInt |-> (1 + 0 )) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] +. + +Definition mpn_add_n_partial_solve_wit_9_aux := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) + ** (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) +|-- + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +. + +Definition mpn_add_n_partial_solve_wit_9 := mpn_add_n_partial_solve_wit_9_pure -> mpn_add_n_partial_solve_wit_9_aux. + +Definition mpn_add_n_partial_solve_wit_10 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) , + [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array rp_pre (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +|-- + [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (((rp_pre + (i * sizeof(UINT) ) )) # UInt |->_) + ** (store_uint_array_missing_i_rec rp_pre i 0 (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +. + +Definition mpn_add_n_partial_solve_wit_11 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) , + [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array rp_pre (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +|-- + [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) < cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (((rp_pre + (i * sizeof(UINT) ) )) # UInt |->_) + ** (store_uint_array_missing_i_rec rp_pre i 0 (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +. + +Definition mpn_add_n_partial_solve_wit_12 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) , + [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array rp_pre (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +|-- + [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) >= (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (((rp_pre + (i * sizeof(UINT) ) )) # UInt |->_) + ** (store_uint_array_missing_i_rec rp_pre i 0 (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +. + +Definition mpn_add_n_partial_solve_wit_13 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (rp_pre: Z) (l_r: (@list Z)) (val_b: Z) (val_a: Z) (cap_r: Z) (cap_b: Z) (cap_a: Z) (l_a: (@list Z)) (l_b: (@list Z)) (l_r_suffix: (@list Z)) (cy: Z) (l_r_prefix: (@list Z)) (val_r_prefix: Z) (val_b_prefix: Z) (val_a_prefix: Z) (l_b_2: (@list Z)) (l_a_2: (@list Z)) (i: Z) (a: Z) (l_r_suffix': (@list Z)) , + [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array rp_pre (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +|-- + [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && [| ((unsigned_last_nbits (((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) + (Znth i l_b_2 0) )) (32)) < (Znth i l_b_2 0)) |] + && [| ((unsigned_last_nbits (((Znth i l_a_2 0) + cy )) (32)) >= cy) |] + && [| (0 <= cy) |] + && [| (cy <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && [| (list_store_Z_compact l_a_2 val_a ) |] + && [| (list_store_Z_compact l_b_2 val_b ) |] + && [| (list_store_Z (sublist (0) (i) (l_a_2)) val_a_prefix ) |] + && [| (list_store_Z (sublist (0) (i) (l_b_2)) val_b_prefix ) |] + && [| (list_store_Z l_r_prefix val_r_prefix ) |] + && [| ((Zlength (l_r_prefix)) = i) |] + && [| ((val_r_prefix + (cy * (Z.pow (UINT_MOD) (i)) ) ) = (val_a_prefix + val_b_prefix )) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && [| ((Zlength (l_r)) = cap_r) |] + && [| (cap_a <= 100000000) |] + && [| (cap_b <= 100000000) |] + && [| (cap_r <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap_a) |] + && [| (n_pre <= cap_b) |] + && [| (n_pre <= cap_r) |] + && (((rp_pre + (i * sizeof(UINT) ) )) # UInt |->_) + ** (store_uint_array_missing_i_rec rp_pre i 0 (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array bp_pre n_pre l_b_2 ) + ** (store_uint_array ap_pre n_pre l_a_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +. + +Definition mpn_add_n_which_implies_wit_1 := +forall (n_pre: Z) (ap_pre: Z) (val_a: Z) (cap_a: Z) , + (mpd_store_Z_compact ap_pre val_a n_pre cap_a ) +|-- + EX (l_a: (@list Z)) , + [| (n_pre <= cap_a) |] + && [| ((Zlength (l_a)) = n_pre) |] + && [| (cap_a <= 100000000) |] + && [| (list_store_Z_compact l_a val_a ) |] + && (store_uint_array ap_pre n_pre l_a ) + ** (store_undef_uint_array_rec ap_pre n_pre cap_a ) +. + +Definition mpn_add_n_which_implies_wit_2 := +forall (n_pre: Z) (bp_pre: Z) (val_b: Z) (cap_b: Z) , + (mpd_store_Z_compact bp_pre val_b n_pre cap_b ) +|-- + EX (l_b: (@list Z)) , + [| (n_pre <= cap_b) |] + && [| ((Zlength (l_b)) = n_pre) |] + && [| (cap_b <= 100000000) |] + && [| (list_store_Z_compact l_b val_b ) |] + && (store_uint_array bp_pre n_pre l_b ) + ** (store_undef_uint_array_rec bp_pre n_pre cap_b ) +. + +Definition mpn_add_n_which_implies_wit_3 := +forall (rp_pre: Z) (l_r: (@list Z)) (cap_r: Z) , + [| ((Zlength (l_r)) = cap_r) |] + && (store_uint_array rp_pre cap_r l_r ) +|-- + [| ((Zlength (l_r)) = cap_r) |] + && (store_uint_array_rec rp_pre 0 cap_r l_r ) + ** (store_uint_array rp_pre 0 nil ) +. + +Definition mpn_add_n_which_implies_wit_4 := +forall (n_pre: Z) (rp_pre: Z) (cap_r: Z) (l_r_suffix: (@list Z)) (l_r_prefix: (@list Z)) (i: Z) , + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array rp_pre i l_r_prefix ) + ** (store_uint_array_rec rp_pre i cap_r l_r_suffix ) +|-- + EX (a: Z) (l_r_suffix': (@list Z)) , + [| (l_r_suffix = (cons (a) (l_r_suffix'))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap_r) |] + && (store_uint_array_rec rp_pre (i + 1 ) cap_r l_r_suffix' ) + ** (store_uint_array rp_pre (i + 1 ) (app (l_r_prefix) ((cons (a) (nil)))) ) +. + (*----- Function mpz_clear -----*) Definition mpz_clear_return_wit_1_1 := @@ -3770,6 +5953,41 @@ 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_mpn_add_n_safety_wit_1 : mpn_add_n_safety_wit_1. +Axiom proof_of_mpn_add_n_safety_wit_2 : mpn_add_n_safety_wit_2. +Axiom proof_of_mpn_add_n_safety_wit_3 : mpn_add_n_safety_wit_3. +Axiom proof_of_mpn_add_n_safety_wit_4 : mpn_add_n_safety_wit_4. +Axiom proof_of_mpn_add_n_safety_wit_5 : mpn_add_n_safety_wit_5. +Axiom proof_of_mpn_add_n_safety_wit_6 : mpn_add_n_safety_wit_6. +Axiom proof_of_mpn_add_n_entail_wit_1 : mpn_add_n_entail_wit_1. +Axiom proof_of_mpn_add_n_entail_wit_2 : mpn_add_n_entail_wit_2. +Axiom proof_of_mpn_add_n_entail_wit_3_1 : mpn_add_n_entail_wit_3_1. +Axiom proof_of_mpn_add_n_entail_wit_3_2 : mpn_add_n_entail_wit_3_2. +Axiom proof_of_mpn_add_n_entail_wit_3_3 : mpn_add_n_entail_wit_3_3. +Axiom proof_of_mpn_add_n_entail_wit_3_4 : mpn_add_n_entail_wit_3_4. +Axiom proof_of_mpn_add_n_return_wit_1 : mpn_add_n_return_wit_1. +Axiom proof_of_mpn_add_n_partial_solve_wit_1 : mpn_add_n_partial_solve_wit_1. +Axiom proof_of_mpn_add_n_partial_solve_wit_2 : mpn_add_n_partial_solve_wit_2. +Axiom proof_of_mpn_add_n_partial_solve_wit_3_pure : mpn_add_n_partial_solve_wit_3_pure. +Axiom proof_of_mpn_add_n_partial_solve_wit_3 : mpn_add_n_partial_solve_wit_3. +Axiom proof_of_mpn_add_n_partial_solve_wit_4 : mpn_add_n_partial_solve_wit_4. +Axiom proof_of_mpn_add_n_partial_solve_wit_5 : mpn_add_n_partial_solve_wit_5. +Axiom proof_of_mpn_add_n_partial_solve_wit_6_pure : mpn_add_n_partial_solve_wit_6_pure. +Axiom proof_of_mpn_add_n_partial_solve_wit_6 : mpn_add_n_partial_solve_wit_6. +Axiom proof_of_mpn_add_n_partial_solve_wit_7_pure : mpn_add_n_partial_solve_wit_7_pure. +Axiom proof_of_mpn_add_n_partial_solve_wit_7 : mpn_add_n_partial_solve_wit_7. +Axiom proof_of_mpn_add_n_partial_solve_wit_8_pure : mpn_add_n_partial_solve_wit_8_pure. +Axiom proof_of_mpn_add_n_partial_solve_wit_8 : mpn_add_n_partial_solve_wit_8. +Axiom proof_of_mpn_add_n_partial_solve_wit_9_pure : mpn_add_n_partial_solve_wit_9_pure. +Axiom proof_of_mpn_add_n_partial_solve_wit_9 : mpn_add_n_partial_solve_wit_9. +Axiom proof_of_mpn_add_n_partial_solve_wit_10 : mpn_add_n_partial_solve_wit_10. +Axiom proof_of_mpn_add_n_partial_solve_wit_11 : mpn_add_n_partial_solve_wit_11. +Axiom proof_of_mpn_add_n_partial_solve_wit_12 : mpn_add_n_partial_solve_wit_12. +Axiom proof_of_mpn_add_n_partial_solve_wit_13 : mpn_add_n_partial_solve_wit_13. +Axiom proof_of_mpn_add_n_which_implies_wit_1 : mpn_add_n_which_implies_wit_1. +Axiom proof_of_mpn_add_n_which_implies_wit_2 : mpn_add_n_which_implies_wit_2. +Axiom proof_of_mpn_add_n_which_implies_wit_3 : mpn_add_n_which_implies_wit_3. +Axiom proof_of_mpn_add_n_which_implies_wit_4 : mpn_add_n_which_implies_wit_4. 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 dd60026..21ed069 100755 --- a/projects/lib/gmp_proof_auto.v +++ b/projects/lib/gmp_proof_auto.v @@ -180,6 +180,78 @@ Proof. Admitted. Lemma proof_of_mpn_add_1_partial_solve_wit_7 : mpn_add_1_partial_solve_wit_7. Proof. Admitted. +Lemma proof_of_mpn_add_n_safety_wit_1 : mpn_add_n_safety_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_safety_wit_2 : mpn_add_n_safety_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_safety_wit_3 : mpn_add_n_safety_wit_3. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_safety_wit_4 : mpn_add_n_safety_wit_4. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_safety_wit_5 : mpn_add_n_safety_wit_5. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_safety_wit_6 : mpn_add_n_safety_wit_6. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_1 : mpn_add_n_partial_solve_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_2 : mpn_add_n_partial_solve_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_3_pure : mpn_add_n_partial_solve_wit_3_pure. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_3 : mpn_add_n_partial_solve_wit_3. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_4 : mpn_add_n_partial_solve_wit_4. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_5 : mpn_add_n_partial_solve_wit_5. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_6_pure : mpn_add_n_partial_solve_wit_6_pure. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_6 : mpn_add_n_partial_solve_wit_6. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_7_pure : mpn_add_n_partial_solve_wit_7_pure. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_7 : mpn_add_n_partial_solve_wit_7. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_8_pure : mpn_add_n_partial_solve_wit_8_pure. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_8 : mpn_add_n_partial_solve_wit_8. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_9_pure : mpn_add_n_partial_solve_wit_9_pure. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_9 : mpn_add_n_partial_solve_wit_9. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_10 : mpn_add_n_partial_solve_wit_10. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_11 : mpn_add_n_partial_solve_wit_11. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_12 : mpn_add_n_partial_solve_wit_12. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_partial_solve_wit_13 : mpn_add_n_partial_solve_wit_13. +Proof. Admitted. + Lemma proof_of_mpz_clear_return_wit_1_3 : mpz_clear_return_wit_1_3. Proof. Admitted. diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 0580a17..fd3b8d4 100755 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -807,6 +807,39 @@ Proof. lia. Qed. +Lemma proof_of_mpn_add_n_entail_wit_1 : mpn_add_n_entail_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_entail_wit_2 : mpn_add_n_entail_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_entail_wit_3_1 : mpn_add_n_entail_wit_3_1. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_entail_wit_3_2 : mpn_add_n_entail_wit_3_2. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_entail_wit_3_3 : mpn_add_n_entail_wit_3_3. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_entail_wit_3_4 : mpn_add_n_entail_wit_3_4. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_return_wit_1 : mpn_add_n_return_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_which_implies_wit_1 : mpn_add_n_which_implies_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_which_implies_wit_2 : mpn_add_n_which_implies_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_which_implies_wit_3 : mpn_add_n_which_implies_wit_3. +Proof. Admitted. + +Lemma proof_of_mpn_add_n_which_implies_wit_4 : mpn_add_n_which_implies_wit_4. +Proof. Admitted. + Lemma proof_of_mpz_clear_return_wit_1_1 : mpz_clear_return_wit_1_1. Proof. pre_process. diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 43b2ab9..8c9f618 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -313,24 +313,104 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) } /* 位数相同的多精度数ap 加上多精度数bp，返回最后产生的进位 */ -/*unsigned int +unsigned int mpn_add_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n) +/*@ + With cap_a cap_b cap_r val_a val_b l_r + Require + mpd_store_Z_compact(ap, val_a, n, cap_a) * + mpd_store_Z_compact(bp, val_b, n, cap_b) * + store_uint_array(rp, cap_r, l_r) && + Zlength(l_r) == cap_r && + cap_a <= 100000000 && + cap_b <= 100000000 && + cap_r <= 100000000 && + n > 0 && n <= cap_a && n <= cap_b && n <= cap_r + Ensure + exists val_r_out, + mpd_store_Z_compact(ap@pre, val_a, n@pre, cap_a) * + mpd_store_Z_compact(bp@pre, val_b, n@pre, cap_b) * + mpd_store_Z(rp@pre, val_r_out, n@pre, cap_r) && + (val_r_out + __return * Z::pow(UINT_MOD, n@pre) == val_a + val_b) +*/ { + /*@ + mpd_store_Z_compact(ap@pre, val_a, n@pre, cap_a) + which implies + exists l_a, + n@pre <= cap_a && + Zlength(l_a) == n@pre && + cap_a <= 100000000 && + store_uint_array(ap@pre, n@pre, l_a) * + store_undef_uint_array_rec(ap@pre, n@pre, cap_a) && + list_store_Z_compact(l_a, val_a) + */ + /*@ + mpd_store_Z_compact(bp@pre, val_b, n@pre, cap_b) + which implies + exists l_b, + n@pre <= cap_b && + Zlength(l_b) == n@pre && + cap_b <= 100000000 && + store_uint_array(bp@pre, n@pre, l_b) * + store_undef_uint_array_rec(bp@pre, n@pre, cap_b) && + list_store_Z_compact(l_b, val_b) + */ int i; unsigned int cy; - for (i = 0, cy = 0; i < n; i++) + /*@ + store_uint_array(rp@pre, cap_r, l_r) && Zlength(l_r) == cap_r + which implies + store_uint_array_rec(rp@pre, 0, cap_r, l_r) * store_uint_array(rp@pre, 0, nil) && + Zlength(l_r) == cap_r + */ + i = 0; + cy = 0; + /*@Inv + exists l_a l_b l_r_prefix l_r_suffix val_a_prefix val_b_prefix val_r_prefix, + 0 <= i && i <= n@pre && n@pre <= cap_a && n@pre <= cap_b && n@pre <= cap_r && + list_store_Z_compact(l_a, val_a) && + list_store_Z_compact(l_b, val_b) && + list_store_Z(sublist(0, i, l_a), val_a_prefix) && + list_store_Z(sublist(0, i, l_b), val_b_prefix) && + list_store_Z(l_r_prefix, val_r_prefix) && + Zlength(l_r_prefix) == i && + (val_r_prefix + cy * Z::pow(UINT_MOD, i) == val_a_prefix + val_b_prefix) && + store_uint_array(ap@pre, n@pre, l_a) * + store_undef_uint_array_rec(ap@pre, n@pre, cap_a) * + store_uint_array(bp@pre, n@pre, l_b) * + store_undef_uint_array_rec(bp@pre, n@pre, cap_b) * + store_uint_array(rp@pre, i, l_r_prefix) * + store_uint_array_rec(rp@pre, i, cap_r, l_r_suffix) + */ + while (i < n) { + /*@ + Given l_a l_b l_r_prefix l_r_suffix val_a_prefix val_b_prefix val_r_prefix + */ + /*@ 0 <= cy && cy <= UINT_MAX by local */ unsigned int a, b, r; a = ap[i]; b = bp[i]; r = a + cy; cy = (r < cy); r += b; cy += (r < b); + /*@ + 0 <= i && i < n@pre && n@pre <= cap_r && + store_uint_array(rp@pre, i, l_r_prefix) * + store_uint_array_rec(rp@pre, i, cap_r, l_r_suffix) + which implies + exists a l_r_suffix', + l_r_suffix == cons(a, l_r_suffix') && 0 <= i && i < n@pre && n@pre <= cap_r && + store_uint_array_rec(rp@pre, i+1, cap_r, l_r_suffix') * + store_uint_array(rp@pre, i+1, app(l_r_prefix, cons(a, nil))) + */ rp[i] = r; + ++i; } return cy; -}*/ +} /*不同位数的多精度数相加，返回最后的进位*/ /*unsigned int diff --git a/projects/mini-gmp.h b/projects/mini-gmp.h index 08af83a..2c67d96 100755 --- a/projects/mini-gmp.h +++ b/projects/mini-gmp.h @@ -84,7 +84,7 @@ void mpn_copyi (unsigned int *d, unsigned int *s, int n); int mpn_cmp (unsigned int *ap, unsigned int *bp, int n); unsigned int mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b); -unsigned int mpn_add_n (unsigned int *, unsigned int *, unsigned int *, int); +unsigned int mpn_add_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n); unsigned int mpn_add (unsigned int *, unsigned int *, int, unsigned int *, int); unsigned int mpn_sub_1 (unsigned int *, unsigned int *, int, unsigned int); From 1e3c1ea7ec06d4b5211468c7bcc8fea952c84d41 Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sun, 22 Jun 2025 05:12:16 +0000 Subject: [PATCH 2/8] ready to prove four carry and uncarry in mpn_add_n --- projects/lib/gmp_proof_manual.v | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index fd3b8d4..dd5256f 100755 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -808,10 +808,30 @@ Proof. Qed. Lemma proof_of_mpn_add_n_entail_wit_1 : mpn_add_n_entail_wit_1. -Proof. Admitted. +Proof. + pre_process. + Exists l_r nil 0 0 0. + Exists l_b_2 l_a_2. + entailer!. + - unfold list_store_Z. + simpl. + tauto. + - rewrite sublist_nil; try lia; try tauto. + unfold list_store_Z. + simpl. + tauto. + - rewrite sublist_nil; try lia; try tauto. + unfold list_store_Z. + simpl. + tauto. +Qed. Lemma proof_of_mpn_add_n_entail_wit_2 : mpn_add_n_entail_wit_2. -Proof. Admitted. +Proof. + pre_process. + prop_apply (store_uint_range &("cy") cy). + entailer!. +Qed. Lemma proof_of_mpn_add_n_entail_wit_3_1 : mpn_add_n_entail_wit_3_1. Proof. Admitted. From 61678166137fef5201456d9136e2b4675f9b48a2 Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sun, 22 Jun 2025 06:58:57 +0000 Subject: [PATCH 3/8] ready to prove the correctness of 3-carry --- projects/lib/GmpNumber.v | 35 +++++++++++++++ projects/lib/gmp_proof_manual.v | 77 ++++++++++++++++++++++++++++++++- 2 files changed, 111 insertions(+), 1 deletion(-) diff --git a/projects/lib/GmpNumber.v b/projects/lib/GmpNumber.v index 9d2ae7d..248978b 100755 --- a/projects/lib/GmpNumber.v +++ b/projects/lib/GmpNumber.v @@ -282,6 +282,41 @@ Proof. pose proof (Zlength_nonneg l1); lia. Qed. +Lemma list_store_Z_list_append: forall (l: list Z) (i: Z) (val_prefix: Z) (val_full: Z), + 0 <= i < Zlength l -> + list_store_Z_compact l val_full -> + list_store_Z (sublist 0 i l) val_prefix -> + list_store_Z (sublist 0 (i+1) l) (val_prefix + Znth i l 0 * UINT_MOD ^ i). +Proof. + intros. + assert ((sublist 0 (i + 1) l) = ((sublist 0 i l) ++ ((Znth i l 0) :: nil)))%list. { + pose proof (sublist_split 0 (i+1) i l). + pose proof (sublist_single i l 0). + rewrite <-H3; try rewrite <- Zlength_correct. + apply H2; try rewrite <- Zlength_correct. + lia. lia. lia. + } + rewrite H2. + pose proof (list_store_Z_concat (sublist 0 i l) (Znth i l 0 :: nil) (val_prefix) (Znth i l 0)). + assert (Zlength (sublist 0 i l) = i). { + rewrite Zlength_sublist0. + lia. + lia. + } + rewrite H4 in H3. + apply H3. + tauto. + unfold list_store_Z. + simpl. + split. + reflexivity. + split; try tauto. + apply list_within_bound_Znth. + lia. + unfold list_store_Z_compact in H0. + tauto. +Qed. + Lemma list_store_Z_split: forall (l1 l2: list Z) (n: Z), list_store_Z (l1 ++ l2) n -> list_store_Z l1 (n mod UINT_MOD ^ (Zlength l1)) /\ diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index dd5256f..16d0213 100755 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -834,7 +834,82 @@ Proof. Qed. Lemma proof_of_mpn_add_n_entail_wit_3_1 : mpn_add_n_entail_wit_3_1. -Proof. Admitted. +Proof. + pre_process. + rewrite replace_Znth_app_r. + assert (l_a_3 = l_a_2). { + pose proof (list_store_Z_compact_reverse_injection l_a_3 l_a_2 val_a val_a). + specialize (H37 H13 H28). + apply H37. + reflexivity. + } + subst l_a_3. + assert (l_b_3 = l_b_2). { + pose proof (list_store_Z_compact_reverse_injection l_b_3 l_b_2 val_b val_b). + specialize (H37 H14 H24). + apply H37. + reflexivity. + } + subst l_b_3. + - Exists l_r_suffix'. + rewrite H29. + rewrite H18. + assert (i - i = 0) by lia. + rewrite H37; clear H37. + set (partial_result_1 := (unsigned_last_nbits (Znth i l_a_2 0 + cy) 32)). + set (partial_result_2 := (unsigned_last_nbits (partial_result_1 + Znth i l_b_2 0) 32)). + rewrite replace_Znth_nothing; try lia. + assert ((replace_Znth 0 partial_result_2 (a :: nil)) = partial_result_2 :: nil). { + unfold replace_Znth. + simpl. + reflexivity. + } + rewrite H37; clear H37. + Exists (l_r_prefix_2 ++ partial_result_2 :: nil). + Exists (val_r_prefix_2 + partial_result_2 * (UINT_MOD ^ i)). + Exists (val_b_prefix_2 + (Znth i l_b_2 0) * (UINT_MOD ^ i)). + Exists (val_a_prefix_2 + (Znth i l_a_2 0) * (UINT_MOD ^ i)). + Exists l_b_2 l_a_2. + entailer!. + + admit. + + pose proof (Zlength_app l_r_prefix_2 (partial_result_2 :: nil)). + assert (Zlength (partial_result_2 :: nil) = 1). { + unfold Zlength. + simpl. + reflexivity. + } + rewrite H38 in H37; clear H38. + rewrite H18 in H37. + apply H37. + + pose proof (list_store_Z_concat l_r_prefix_2 (partial_result_2 :: nil) val_r_prefix_2 partial_result_2). + rewrite H18 in H37. + apply H37. + tauto. + unfold list_store_Z. + simpl. + split. + reflexivity. + split. + unfold partial_result_2. + unfold unsigned_last_nbits. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H38; clear H38. + apply Z.mod_pos_bound. + lia. + tauto. + + pose proof (list_store_Z_list_append l_b_2 i val_b_prefix_2 val_b). + apply H37. + lia. + tauto. + tauto. + + pose proof (list_store_Z_list_append l_a_2 i val_a_prefix_2 val_a). + apply H37. + lia. + tauto. + tauto. + - pose proof (Zlength_sublist0 i l_r_prefix_2). + lia. +Admitted. Lemma proof_of_mpn_add_n_entail_wit_3_2 : mpn_add_n_entail_wit_3_2. Proof. Admitted. From 0fdf4fc328c91d132d5890b604bfd8ea3ebb9437 Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sun, 22 Jun 2025 07:25:46 +0000 Subject: [PATCH 4/8] finish proof_of_mpn_add_n_entail_wit_3_1 --- projects/lib/GmpAux.v | 28 ++++++++++++++++++++++++++++ projects/lib/gmp_proof_manual.v | 24 ++++++++++++++++++++++-- 2 files changed, 50 insertions(+), 2 deletions(-) diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index 7bbdf01..4ece64f 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -33,6 +33,34 @@ Lemma Z_mod_add_uncarry: forall (a b m: Z), a + b = (a + b) mod m. Proof. Admitted. +Lemma Z_mod_3add_carry10: forall (a b c m: Z), + m > 0 -> 0 <= a < m -> 0 <= b < m -> 0 <= c < m -> + (a + c) mod m < c -> + ((a + c) mod m + b) mod m >= b -> + a + b + c = ((a + c) mod m + b) mod m + m. +Proof. Admitted. + +Lemma Z_mod_3add_carry01: forall (a b c m: Z), + m > 0 -> 0 <= a < m -> 0 <= b < m -> 0 <= c < m -> + (a + c) mod m >= c -> + ((a + c) mod m + b) mod m < b -> + a + b + c = ((a + c) mod m + b) mod m + m. +Proof. Admitted. + +Lemma Z_mod_3add_carry11: forall (a b c m: Z), + m > 0 -> 0 <= a < m -> 0 <= b < m -> 0 <= c < m -> + (a + c) mod m < c -> + ((a + c) mod m + b) mod m < b -> + a + b + c = ((a + c) mod m + b) mod m + m. +Proof. Admitted. + +Lemma Z_mod_3add_carry00: forall (a b c m: Z), + m > 0 -> 0 <= a < m -> 0 <= b < m -> 0 <= c < m -> + (a + c) mod m >= c -> + ((a + c) mod m + b) mod m >= b -> + a + b + c = ((a + c) mod m + 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. diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 16d0213..c062a48 100755 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -871,7 +871,27 @@ Proof. Exists (val_a_prefix_2 + (Znth i l_a_2 0) * (UINT_MOD ^ i)). Exists l_b_2 l_a_2. entailer!. - + admit. + + assert ( (val_a_prefix_2 + Znth i l_a_2 0 * 4294967296 ^ i +(val_b_prefix_2 + Znth i l_b_2 0 * 4294967296 ^ i)) = (val_a_prefix_2 + val_b_prefix_2) + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). + { + lia. + } + rewrite H37; clear H37. + rewrite <- H19. + assert ( (Znth i l_a_2 0) + (Znth i l_b_2 0) + cy = partial_result_2 + UINT_MOD). { + unfold unsigned_last_nbits in H4, H3. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H37 in H4, H3; clear H37. + apply Z_mod_3add_carry10; try lia; try tauto; + try unfold list_store_Z_compact in H13, H14; + try apply list_within_bound_Znth; + try lia; + try tauto. + } + assert ( partial_result_2 * 4294967296 ^ i + (1 + 0) * 4294967296 ^ (i + 1) = cy * 4294967296 ^ i + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). { + rewrite <- Z.mul_add_distr_r. + rewrite (Zpow_add_1 4294967296 i); try lia. + } + lia. + pose proof (Zlength_app l_r_prefix_2 (partial_result_2 :: nil)). assert (Zlength (partial_result_2 :: nil) = 1). { unfold Zlength. @@ -909,7 +929,7 @@ Proof. tauto. - pose proof (Zlength_sublist0 i l_r_prefix_2). lia. -Admitted. +Qed. Lemma proof_of_mpn_add_n_entail_wit_3_2 : mpn_add_n_entail_wit_3_2. Proof. Admitted. From fd26d9669e205a8a1eda7ad78a4ff0f76438d3d4 Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sun, 22 Jun 2025 07:37:10 +0000 Subject: [PATCH 5/8] finish all adder proof for mpn_add_n --- projects/lib/GmpAux.v | 2 +- projects/lib/gmp_proof_manual.v | 291 +++++++++++++++++++++++++++++++- 2 files changed, 289 insertions(+), 4 deletions(-) diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index 4ece64f..640cbaa 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -51,7 +51,7 @@ Lemma Z_mod_3add_carry11: forall (a b c m: Z), m > 0 -> 0 <= a < m -> 0 <= b < m -> 0 <= c < m -> (a + c) mod m < c -> ((a + c) mod m + b) mod m < b -> - a + b + c = ((a + c) mod m + b) mod m + m. + a + b + c = ((a + c) mod m + b) mod m + m * 2. Proof. Admitted. Lemma Z_mod_3add_carry00: forall (a b c m: Z), diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index c062a48..053adc5 100755 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -932,13 +932,298 @@ Proof. Qed. Lemma proof_of_mpn_add_n_entail_wit_3_2 : mpn_add_n_entail_wit_3_2. -Proof. Admitted. +Proof. + pre_process. + rewrite replace_Znth_app_r. + assert (l_a_3 = l_a_2). { + pose proof (list_store_Z_compact_reverse_injection l_a_3 l_a_2 val_a val_a). + specialize (H37 H13 H28). + apply H37. + reflexivity. + } + subst l_a_3. + assert (l_b_3 = l_b_2). { + pose proof (list_store_Z_compact_reverse_injection l_b_3 l_b_2 val_b val_b). + specialize (H37 H14 H24). + apply H37. + reflexivity. + } + subst l_b_3. + - Exists l_r_suffix'. + rewrite H29. + rewrite H18. + assert (i - i = 0) by lia. + rewrite H37; clear H37. + set (partial_result_1 := (unsigned_last_nbits (Znth i l_a_2 0 + cy) 32)). + set (partial_result_2 := (unsigned_last_nbits (partial_result_1 + Znth i l_b_2 0) 32)). + rewrite replace_Znth_nothing; try lia. + assert ((replace_Znth 0 partial_result_2 (a :: nil)) = partial_result_2 :: nil). { + unfold replace_Znth. + simpl. + reflexivity. + } + rewrite H37; clear H37. + Exists (l_r_prefix_2 ++ partial_result_2 :: nil). + Exists (val_r_prefix_2 + partial_result_2 * (UINT_MOD ^ i)). + Exists (val_b_prefix_2 + (Znth i l_b_2 0) * (UINT_MOD ^ i)). + Exists (val_a_prefix_2 + (Znth i l_a_2 0) * (UINT_MOD ^ i)). + Exists l_b_2 l_a_2. + entailer!. + + assert ( (val_a_prefix_2 + Znth i l_a_2 0 * 4294967296 ^ i +(val_b_prefix_2 + Znth i l_b_2 0 * 4294967296 ^ i)) = (val_a_prefix_2 + val_b_prefix_2) + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). + { + lia. + } + rewrite H37; clear H37. + rewrite <- H19. + assert ( (Znth i l_a_2 0) + (Znth i l_b_2 0) + cy = partial_result_2 + UINT_MOD * 2). { + unfold unsigned_last_nbits in H4, H3. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H37 in H4, H3; clear H37. + apply Z_mod_3add_carry11; try lia; try tauto; + try unfold list_store_Z_compact in H13, H14; + try apply list_within_bound_Znth; + try lia; + try tauto. + } + assert ( partial_result_2 * 4294967296 ^ i + (1 + 1) * 4294967296 ^ (i + 1) = cy * 4294967296 ^ i + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). { + rewrite <- Z.mul_add_distr_r. + rewrite (Zpow_add_1 4294967296 i); try lia. + } + lia. + + pose proof (Zlength_app l_r_prefix_2 (partial_result_2 :: nil)). + assert (Zlength (partial_result_2 :: nil) = 1). { + unfold Zlength. + simpl. + reflexivity. + } + rewrite H38 in H37; clear H38. + rewrite H18 in H37. + apply H37. + + pose proof (list_store_Z_concat l_r_prefix_2 (partial_result_2 :: nil) val_r_prefix_2 partial_result_2). + rewrite H18 in H37. + apply H37. + tauto. + unfold list_store_Z. + simpl. + split. + reflexivity. + split. + unfold partial_result_2. + unfold unsigned_last_nbits. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H38; clear H38. + apply Z.mod_pos_bound. + lia. + tauto. + + pose proof (list_store_Z_list_append l_b_2 i val_b_prefix_2 val_b). + apply H37. + lia. + tauto. + tauto. + + pose proof (list_store_Z_list_append l_a_2 i val_a_prefix_2 val_a). + apply H37. + lia. + tauto. + tauto. + - pose proof (Zlength_sublist0 i l_r_prefix_2). + lia. +Qed. Lemma proof_of_mpn_add_n_entail_wit_3_3 : mpn_add_n_entail_wit_3_3. -Proof. Admitted. +Proof. + pre_process. + rewrite replace_Znth_app_r. + assert (l_a_3 = l_a_2). { + pose proof (list_store_Z_compact_reverse_injection l_a_3 l_a_2 val_a val_a). + specialize (H37 H13 H28). + apply H37. + reflexivity. + } + subst l_a_3. + assert (l_b_3 = l_b_2). { + pose proof (list_store_Z_compact_reverse_injection l_b_3 l_b_2 val_b val_b). + specialize (H37 H14 H24). + apply H37. + reflexivity. + } + subst l_b_3. + - Exists l_r_suffix'. + rewrite H29. + rewrite H18. + assert (i - i = 0) by lia. + rewrite H37; clear H37. + set (partial_result_1 := (unsigned_last_nbits (Znth i l_a_2 0 + cy) 32)). + set (partial_result_2 := (unsigned_last_nbits (partial_result_1 + Znth i l_b_2 0) 32)). + rewrite replace_Znth_nothing; try lia. + assert ((replace_Znth 0 partial_result_2 (a :: nil)) = partial_result_2 :: nil). { + unfold replace_Znth. + simpl. + reflexivity. + } + rewrite H37; clear H37. + Exists (l_r_prefix_2 ++ partial_result_2 :: nil). + Exists (val_r_prefix_2 + partial_result_2 * (UINT_MOD ^ i)). + Exists (val_b_prefix_2 + (Znth i l_b_2 0) * (UINT_MOD ^ i)). + Exists (val_a_prefix_2 + (Znth i l_a_2 0) * (UINT_MOD ^ i)). + Exists l_b_2 l_a_2. + entailer!. + + assert ( (val_a_prefix_2 + Znth i l_a_2 0 * 4294967296 ^ i +(val_b_prefix_2 + Znth i l_b_2 0 * 4294967296 ^ i)) = (val_a_prefix_2 + val_b_prefix_2) + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). + { + lia. + } + rewrite H37; clear H37. + rewrite <- H19. + assert ( (Znth i l_a_2 0) + (Znth i l_b_2 0) + cy = partial_result_2). { + unfold unsigned_last_nbits in H4, H3. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H37 in H4, H3; clear H37. + apply Z_mod_3add_carry00; try lia; try tauto; + try unfold list_store_Z_compact in H13, H14; + try apply list_within_bound_Znth; + try lia; + try tauto. + } + assert ( partial_result_2 * 4294967296 ^ i + (0 + 0) * 4294967296 ^ (i + 1) = cy * 4294967296 ^ i + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). { + rewrite <- Z.mul_add_distr_r. + rewrite (Zpow_add_1 4294967296 i); try lia. + } + lia. + + pose proof (Zlength_app l_r_prefix_2 (partial_result_2 :: nil)). + assert (Zlength (partial_result_2 :: nil) = 1). { + unfold Zlength. + simpl. + reflexivity. + } + rewrite H38 in H37; clear H38. + rewrite H18 in H37. + apply H37. + + pose proof (list_store_Z_concat l_r_prefix_2 (partial_result_2 :: nil) val_r_prefix_2 partial_result_2). + rewrite H18 in H37. + apply H37. + tauto. + unfold list_store_Z. + simpl. + split. + reflexivity. + split. + unfold partial_result_2. + unfold unsigned_last_nbits. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H38; clear H38. + apply Z.mod_pos_bound. + lia. + tauto. + + pose proof (list_store_Z_list_append l_b_2 i val_b_prefix_2 val_b). + apply H37. + lia. + tauto. + tauto. + + pose proof (list_store_Z_list_append l_a_2 i val_a_prefix_2 val_a). + apply H37. + lia. + tauto. + tauto. + - pose proof (Zlength_sublist0 i l_r_prefix_2). + lia. +Qed. Lemma proof_of_mpn_add_n_entail_wit_3_4 : mpn_add_n_entail_wit_3_4. -Proof. Admitted. +Proof. + pre_process. + rewrite replace_Znth_app_r. + assert (l_a_3 = l_a_2). { + pose proof (list_store_Z_compact_reverse_injection l_a_3 l_a_2 val_a val_a). + specialize (H37 H13 H28). + apply H37. + reflexivity. + } + subst l_a_3. + assert (l_b_3 = l_b_2). { + pose proof (list_store_Z_compact_reverse_injection l_b_3 l_b_2 val_b val_b). + specialize (H37 H14 H24). + apply H37. + reflexivity. + } + subst l_b_3. + - Exists l_r_suffix'. + rewrite H29. + rewrite H18. + assert (i - i = 0) by lia. + rewrite H37; clear H37. + set (partial_result_1 := (unsigned_last_nbits (Znth i l_a_2 0 + cy) 32)). + set (partial_result_2 := (unsigned_last_nbits (partial_result_1 + Znth i l_b_2 0) 32)). + rewrite replace_Znth_nothing; try lia. + assert ((replace_Znth 0 partial_result_2 (a :: nil)) = partial_result_2 :: nil). { + unfold replace_Znth. + simpl. + reflexivity. + } + rewrite H37; clear H37. + Exists (l_r_prefix_2 ++ partial_result_2 :: nil). + Exists (val_r_prefix_2 + partial_result_2 * (UINT_MOD ^ i)). + Exists (val_b_prefix_2 + (Znth i l_b_2 0) * (UINT_MOD ^ i)). + Exists (val_a_prefix_2 + (Znth i l_a_2 0) * (UINT_MOD ^ i)). + Exists l_b_2 l_a_2. + entailer!. + + assert ( (val_a_prefix_2 + Znth i l_a_2 0 * 4294967296 ^ i +(val_b_prefix_2 + Znth i l_b_2 0 * 4294967296 ^ i)) = (val_a_prefix_2 + val_b_prefix_2) + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). + { + lia. + } + rewrite H37; clear H37. + rewrite <- H19. + assert ( (Znth i l_a_2 0) + (Znth i l_b_2 0) + cy = partial_result_2 + UINT_MOD). { + unfold unsigned_last_nbits in H4, H3. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H37 in H4, H3; clear H37. + apply Z_mod_3add_carry01; try lia; try tauto; + try unfold list_store_Z_compact in H13, H14; + try apply list_within_bound_Znth; + try lia; + try tauto. + } + assert ( partial_result_2 * 4294967296 ^ i + (0 + 1) * 4294967296 ^ (i + 1) = cy * 4294967296 ^ i + Znth i l_a_2 0 * 4294967296 ^ i + Znth i l_b_2 0 * 4294967296 ^ i). { + rewrite <- Z.mul_add_distr_r. + rewrite (Zpow_add_1 4294967296 i); try lia. + } + lia. + + pose proof (Zlength_app l_r_prefix_2 (partial_result_2 :: nil)). + assert (Zlength (partial_result_2 :: nil) = 1). { + unfold Zlength. + simpl. + reflexivity. + } + rewrite H38 in H37; clear H38. + rewrite H18 in H37. + apply H37. + + pose proof (list_store_Z_concat l_r_prefix_2 (partial_result_2 :: nil) val_r_prefix_2 partial_result_2). + rewrite H18 in H37. + apply H37. + tauto. + unfold list_store_Z. + simpl. + split. + reflexivity. + split. + unfold partial_result_2. + unfold unsigned_last_nbits. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H38; clear H38. + apply Z.mod_pos_bound. + lia. + tauto. + + pose proof (list_store_Z_list_append l_b_2 i val_b_prefix_2 val_b). + apply H37. + lia. + tauto. + tauto. + + pose proof (list_store_Z_list_append l_a_2 i val_a_prefix_2 val_a). + apply H37. + lia. + tauto. + tauto. + - pose proof (Zlength_sublist0 i l_r_prefix_2). + lia. +Qed. Lemma proof_of_mpn_add_n_return_wit_1 : mpn_add_n_return_wit_1. Proof. Admitted. From e4317a303f59e93786ce370a78b30ab33a1205e4 Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sun, 22 Jun 2025 08:28:31 +0000 Subject: [PATCH 6/8] finish proof_of_mpn_add_n_return_wit_1 --- projects/lib/gmp_proof_manual.v | 63 ++++++++++++++++++++++++++++++++- 1 file changed, 62 insertions(+), 1 deletion(-) diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 053adc5..1cf4570 100755 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -1226,7 +1226,68 @@ Proof. Qed. Lemma proof_of_mpn_add_n_return_wit_1 : mpn_add_n_return_wit_1. -Proof. Admitted. +Proof. + pre_process. + assert (l_a_2 = l_a). { + pose proof (list_store_Z_compact_reverse_injection l_a_2 l_a val_a val_a). + specialize (H29 H20 H5). + apply H29. + reflexivity. + } + subst l_a_2. + assert (l_b_2 = l_b). { + pose proof (list_store_Z_compact_reverse_injection l_b_2 l_b val_b val_b). + specialize (H29 H16 H6). + apply H29. + reflexivity. + } + subst l_b_2. + assert (i = n_pre) by lia. + Exists val_r_prefix. + unfold mpd_store_Z_compact. + unfold mpd_store_list. + Exists l_a. + Exists l_b. + entailer!. + + rewrite H14. + rewrite H18. + entailer!. + unfold mpd_store_Z. + Exists l_r_prefix. + rewrite H29 in *. + entailer!. + unfold mpd_store_list. + entailer!. + rewrite H10. + entailer!. + apply store_uint_array_rec_def2undef. + + rewrite <- H29. + assert (val_a_prefix = val_a). { + assert (i = Zlength l_a). { + lia. + } + rewrite H30 in H7. + rewrite sublist_self in H7. + unfold list_store_Z_compact in H5. + unfold list_store_Z in H7. + lia. + reflexivity. + } + rewrite <- H30; clear H30. + assert (val_b_prefix = val_b). { + assert (i = Zlength l_b). { + lia. + } + rewrite H30 in H8. + rewrite sublist_self in H8. + unfold list_store_Z_compact in H6. + unfold list_store_Z in H8. + lia. + reflexivity. + } + rewrite <- H30; clear H30. + tauto. +Qed. Lemma proof_of_mpn_add_n_which_implies_wit_1 : mpn_add_n_which_implies_wit_1. Proof. Admitted. From d88a2acd6dcd9626e02267f33c2569ecb05f3b57 Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sun, 22 Jun 2025 08:32:38 +0000 Subject: [PATCH 7/8] ready to prove proof_of_mpn_add_n_which_implies_wit_4 --- projects/lib/gmp_proof_manual.v | 43 ++++++++++++++++++++++++++++++--- 1 file changed, 40 insertions(+), 3 deletions(-) diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 1cf4570..348c9a0 100755 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -1290,13 +1290,50 @@ Proof. Qed. Lemma proof_of_mpn_add_n_which_implies_wit_1 : mpn_add_n_which_implies_wit_1. -Proof. Admitted. +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_n_which_implies_wit_2 : mpn_add_n_which_implies_wit_2. -Proof. Admitted. +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_n_which_implies_wit_3 : mpn_add_n_which_implies_wit_3. -Proof. Admitted. +Proof. + pre_process. + pose proof (store_uint_array_divide rp_pre cap_r l_r 0). + pose proof (Zlength_nonneg l_r). + specialize (H0 ltac:(lia) ltac:(lia)). + destruct H0 as [H0 _]. + simpl in H0. + entailer!. + rewrite (sublist_nil l_r 0 0) in H0; [ | lia]. + sep_apply H0. + entailer!. + unfold store_uint_array, store_uint_array_rec. + unfold store_array. + rewrite (sublist_self l_r cap_r); [ | lia ]. + assert (rp_pre + 0 = rp_pre). { lia. } + rewrite H2; clear H2. + assert (cap_r - 0 = cap_r). { lia. } + rewrite H2; clear H2. + reflexivity. +Qed. Lemma proof_of_mpn_add_n_which_implies_wit_4 : mpn_add_n_which_implies_wit_4. Proof. Admitted. From 7876f2ecbfcf8d4ef60e87b7d04be7a9ed6496f2 Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sun, 22 Jun 2025 08:41:55 +0000 Subject: [PATCH 8/8] finish proof_of_mpn_add_n_which_implies_wit_4 --- projects/lib/gmp_proof_manual.v | 75 ++++++++++++++++++++++++++++++++- 1 file changed, 74 insertions(+), 1 deletion(-) diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 348c9a0..0977238 100755 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -1336,7 +1336,80 @@ Proof. Qed. Lemma proof_of_mpn_add_n_which_implies_wit_4 : mpn_add_n_which_implies_wit_4. -Proof. Admitted. +Proof. + pre_process. + destruct l_r_suffix. { + unfold store_uint_array_rec. + simpl. + entailer!. + } + pose proof (store_uint_array_rec_cons rp_pre i cap_r z l_r_suffix ltac:(lia)). + sep_apply H2. + Exists z l_r_suffix. + 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_r_prefix). + sep_apply H3. + rewrite logic_equiv_andp_comm. + rewrite logic_equiv_coq_prop_andp_sepcon. + Intros. + subst l_r_prefix. + 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_r_prefix) 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_r_prefix ++ 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_r_prefix). + 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_r_prefix ++ 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.