From f462570ccdcc7a8329ceb4f167401308a8b7bb0c Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sat, 21 Jun 2025 05:45:27 +0000 Subject: [PATCH] ready to finalize proof_of_mpn_add_1_entail_wit_2_1 --- projects/lib/gmp_goal.v | 350 +++++++++++++++++++++++++++----- projects/lib/gmp_proof_auto.v | 12 ++ projects/lib/gmp_proof_manual.v | 115 ++++++++++- projects/mini-gmp.c | 10 + 4 files changed, 435 insertions(+), 52 deletions(-) diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v index 1e185ca..911faa4 100644 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -1781,8 +1781,12 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ . Definition mpn_add_1_safety_wit_2 := -forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , - [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) (a: Z) (l''': (@list Z)) , + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1803,12 +1807,12 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (cap2 <= 100000000) |] && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] - && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) (l'')) ) + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ((app (l') ((cons (a) (nil)))))) ) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) ** (store_uint_array ap_pre n_pre l_2 ) ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) - ** ((( &( "i" ) )) # Int |-> i) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) - ** (store_uint_array rp_pre i l' ) ** ((( &( "b" ) )) # UInt |-> 0) ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) @@ -1819,8 +1823,12 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ . Definition mpn_add_1_safety_wit_3 := -forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , - [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) (a: Z) (l''': (@list Z)) , + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1841,12 +1849,12 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (cap2 <= 100000000) |] && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] - && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) (l'')) ) + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ((app (l') ((cons (a) (nil)))))) ) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) ** (store_uint_array ap_pre n_pre l_2 ) ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) - ** ((( &( "i" ) )) # Int |-> i) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) - ** (store_uint_array rp_pre i l' ) ** ((( &( "b" ) )) # UInt |-> 1) ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) @@ -1901,8 +1909,12 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ . Definition mpn_add_1_entail_wit_2_1 := -forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (b: Z) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) , - [| ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32)) < b) |] +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (b: Z) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) (a: Z) (l''': (@list Z)) , + [| (l''_2 = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && [| ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32)) < b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1923,10 +1935,10 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (cap2 <= 100000000) |] && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] - && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32))) (l''_2)) ) + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32))) ((app (l'_2) ((cons (a) (nil)))))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) ** (store_uint_array ap_pre n_pre l_3 ) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) - ** (store_uint_array rp_pre i l'_2 ) |-- EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , [| (0 <= (i + 1 )) |] @@ -1955,8 +1967,12 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ . Definition mpn_add_1_entail_wit_2_2 := -forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (b: Z) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) , - [| ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32)) >= b) |] +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (b: Z) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) (a: Z) (l''': (@list Z)) , + [| (l''_2 = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && [| ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32)) >= b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1977,10 +1993,10 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (cap2 <= 100000000) |] && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] - && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32))) (l''_2)) ) + && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32))) ((app (l'_2) ((cons (a) (nil)))))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) ** (store_uint_array ap_pre n_pre l_3 ) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) - ** (store_uint_array rp_pre i l'_2 ) |-- EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , [| (0 <= (i + 1 )) |] @@ -2174,9 +2190,9 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_uint_array_rec rp_pre i cap2 l'' ) . -Definition mpn_add_1_partial_solve_wit_4 := +Definition mpn_add_1_partial_solve_wit_4_pure := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , - [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2198,39 +2214,22 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] && (store_uint_array ap_pre n_pre l_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) + ** ((( &( "i" ) )) # Int |-> i) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre i l' ) ** (store_uint_array_rec rp_pre i cap2 l'' ) + ** ((( &( "b" ) )) # UInt |-> 0) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) |-- - [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + [| (0 <= i) |] && [| (i < n_pre) |] - && [| (0 <= i) |] - && [| (i <= n_pre) |] - && [| (list_store_Z_compact l_2 val ) |] - && [| (n_pre <= cap1) |] - && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] - && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] - && [| ((Zlength (l')) = i) |] - && [| ((Zlength (l2)) = cap2) |] - && [| (n_pre <= cap1) |] - && [| ((Zlength (l)) = n_pre) |] - && [| (cap1 <= 100000000) |] - && [| (list_store_Z_compact l val ) |] - && [| ((Zlength (l2)) = cap2) |] - && [| (cap2 >= n_pre) |] - && [| (cap1 <= 100000000) |] - && [| (cap2 <= 100000000) |] - && [| (n_pre > 0) |] - && [| (n_pre <= cap1) |] - && (((rp_pre + (i * sizeof(UINT) ) )) # UInt |->_) - ** (store_uint_array_missing_i_rec rp_pre i i cap2 l'' ) - ** (store_uint_array ap_pre n_pre l_2 ) - ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) - ** (store_uint_array rp_pre i l' ) + && [| (n_pre <= cap2) |] . -Definition mpn_add_1_partial_solve_wit_5 := +Definition mpn_add_1_partial_solve_wit_4_aux := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] && [| (i < n_pre) |] @@ -2258,7 +2257,174 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_uint_array rp_pre i l' ) ** (store_uint_array_rec rp_pre i cap2 l'' ) |-- - [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +. + +Definition mpn_add_1_partial_solve_wit_4 := mpn_add_1_partial_solve_wit_4_pure -> mpn_add_1_partial_solve_wit_4_aux. + +Definition mpn_add_1_partial_solve_wit_5_pure := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array ap_pre n_pre l_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) + ** ((( &( "b" ) )) # UInt |-> 1) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] +. + +Definition mpn_add_1_partial_solve_wit_5_aux := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) +|-- + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +. + +Definition mpn_add_1_partial_solve_wit_5 := mpn_add_1_partial_solve_wit_5_pure -> mpn_add_1_partial_solve_wit_5_aux. + +Definition mpn_add_1_partial_solve_wit_6 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) (a: Z) (l''': (@list Z)) , + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) + ** (store_uint_array rp_pre (i + 1 ) (app (l') ((cons (a) (nil)))) ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +|-- + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2280,10 +2446,74 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] && (((rp_pre + (i * sizeof(UINT) ) )) # UInt |->_) - ** (store_uint_array_missing_i_rec rp_pre i i cap2 l'' ) + ** (store_uint_array_missing_i_rec rp_pre i 0 (i + 1 ) (app (l') ((cons (a) (nil)))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +. + +Definition mpn_add_1_partial_solve_wit_7 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) (a: Z) (l''': (@list Z)) , + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) + ** (store_uint_array rp_pre (i + 1 ) (app (l') ((cons (a) (nil)))) ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +|-- + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (((rp_pre + (i * sizeof(UINT) ) )) # UInt |->_) + ** (store_uint_array_missing_i_rec rp_pre i 0 (i + 1 ) (app (l') ((cons (a) (nil)))) ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) ** (store_uint_array ap_pre n_pre l_2 ) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) - ** (store_uint_array rp_pre i l' ) . Definition mpn_add_1_which_implies_wit_1 := @@ -2309,6 +2539,23 @@ forall (rp_pre: Z) (cap2: Z) (l2: (@list Z)) , ** (store_uint_array rp_pre 0 nil ) . +Definition mpn_add_1_which_implies_wit_3 := +forall (n_pre: Z) (rp_pre: Z) (cap2: Z) (l'': (@list Z)) (l': (@list Z)) (i: Z) , + [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && (store_uint_array rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) +|-- + EX (a: Z) (l''': (@list Z)) , + [| (l'' = (cons (a) (l'''))) |] + && [| (0 <= i) |] + && [| (i < n_pre) |] + && [| (n_pre <= cap2) |] + && (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) + ** (store_uint_array rp_pre (i + 1 ) (app (l') ((cons (a) (nil)))) ) +. + Module Type VC_Correct. Axiom proof_of_gmp_abs_safety_wit_1 : gmp_abs_safety_wit_1. @@ -2390,9 +2637,14 @@ Axiom proof_of_mpn_add_1_partial_solve_wit_1 : mpn_add_1_partial_solve_wit_1. Axiom proof_of_mpn_add_1_partial_solve_wit_2_pure : mpn_add_1_partial_solve_wit_2_pure. Axiom proof_of_mpn_add_1_partial_solve_wit_2 : mpn_add_1_partial_solve_wit_2. Axiom proof_of_mpn_add_1_partial_solve_wit_3 : mpn_add_1_partial_solve_wit_3. +Axiom proof_of_mpn_add_1_partial_solve_wit_4_pure : mpn_add_1_partial_solve_wit_4_pure. Axiom proof_of_mpn_add_1_partial_solve_wit_4 : mpn_add_1_partial_solve_wit_4. +Axiom proof_of_mpn_add_1_partial_solve_wit_5_pure : mpn_add_1_partial_solve_wit_5_pure. Axiom proof_of_mpn_add_1_partial_solve_wit_5 : mpn_add_1_partial_solve_wit_5. +Axiom proof_of_mpn_add_1_partial_solve_wit_6 : mpn_add_1_partial_solve_wit_6. +Axiom proof_of_mpn_add_1_partial_solve_wit_7 : mpn_add_1_partial_solve_wit_7. Axiom proof_of_mpn_add_1_which_implies_wit_1 : mpn_add_1_which_implies_wit_1. Axiom proof_of_mpn_add_1_which_implies_wit_2 : mpn_add_1_which_implies_wit_2. +Axiom proof_of_mpn_add_1_which_implies_wit_3 : mpn_add_1_which_implies_wit_3. End VC_Correct. diff --git a/projects/lib/gmp_proof_auto.v b/projects/lib/gmp_proof_auto.v index b664c03..2c2f9d2 100644 --- a/projects/lib/gmp_proof_auto.v +++ b/projects/lib/gmp_proof_auto.v @@ -164,9 +164,21 @@ Proof. Admitted. Lemma proof_of_mpn_add_1_partial_solve_wit_3 : mpn_add_1_partial_solve_wit_3. Proof. Admitted. +Lemma proof_of_mpn_add_1_partial_solve_wit_4_pure : mpn_add_1_partial_solve_wit_4_pure. +Proof. Admitted. + Lemma proof_of_mpn_add_1_partial_solve_wit_4 : mpn_add_1_partial_solve_wit_4. Proof. Admitted. +Lemma proof_of_mpn_add_1_partial_solve_wit_5_pure : mpn_add_1_partial_solve_wit_5_pure. +Proof. Admitted. + Lemma proof_of_mpn_add_1_partial_solve_wit_5 : mpn_add_1_partial_solve_wit_5. Proof. Admitted. +Lemma proof_of_mpn_add_1_partial_solve_wit_6 : mpn_add_1_partial_solve_wit_6. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_7 : mpn_add_1_partial_solve_wit_7. +Proof. Admitted. + diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 32fbea2..f7e7044 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -407,13 +407,119 @@ Proof. Qed. Lemma proof_of_mpn_add_1_entail_wit_1 : mpn_add_1_entail_wit_1. -Proof. Admitted. +Proof. + pre_process. + Exists l2 nil 0 0 l_2. + entailer!. + - unfold list_store_Z. + split. + + simpl. tauto. + + simpl. tauto. + - rewrite (sublist_nil l_2 0 0); try lia. + unfold list_store_Z. + split. + + simpl. tauto. + + simpl. tauto. +Qed. Lemma proof_of_mpn_add_1_entail_wit_2_1 : mpn_add_1_entail_wit_2_1. -Proof. Admitted. +Proof. + pre_process. + rewrite replace_Znth_app_r. + - Exists l'''. + rewrite H12. + assert (i - i = 0) by lia. + rewrite H24. + set (new_b := (unsigned_last_nbits (Znth i l_3 0 + b) 32)). + rewrite replace_Znth_nothing; try lia. + assert (replace_Znth 0 new_b (a :: nil) = new_b :: nil). { + unfold replace_Znth. + unfold Z.to_nat. + unfold replace_nth. + reflexivity. + } + rewrite H25. + Exists (l'_2 ++ new_b :: nil). + Exists (val2_2 + new_b * (UINT_MOD^ i)). + Exists (val1_2 + (Znth i l_3 0) * (UINT_MOD^ i)). + Exists l_3. + entailer!. + + rewrite Zlength_app. + rewrite H12. + unfold Zlength. + unfold Zlength_aux. + lia. + + assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i + b_pre = (val1_2 + b_pre) + Znth i l_3 0 * 4294967296 ^ i) by lia. + rewrite H26. + rewrite <- H11. + assert (Znth i l_3 0 + b = new_b + UINT_MOD). + { + subst new_b. + unfold unsigned_last_nbits. + unfold unsigned_last_nbits in H3. + assert (2^32 = 4294967296). { nia. } + rewrite H27 in *. + admit. + } + admit. + + pose proof (__list_store_Z_concat_r l'_2 val2_2 new_b). + apply H26 in H10. + rewrite H12 in H10. + assert (new_b * 4294967296 ^ i + val2_2 = (val2_2 + new_b * 4294967296 ^ i)) by lia. + rewrite H27 in H10. + tauto. + subst new_b. + unfold unsigned_last_nbits. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H27. + apply Z.mod_pos_bound. + lia. + + assert (l_2=l_3). + { + pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val). + apply H26 in H7; try tauto. + } + + assert (i < Zlength l_3). { + subst l_3. + rewrite H15. + tauto. + } + + assert((sublist 0 (i + 1) l_3) = (sublist 0 i l_3) ++ (Znth i l_3 0) :: nil). { + pose proof (sublist_split 0 (i+1) i l_3). + pose proof (sublist_single i l_3 0). + rewrite <-H29. + apply H28. + lia. + subst l_3. + rewrite Zlength_correct in H27. + lia. + rewrite Zlength_correct in H27. + lia. + } + rewrite H28. + pose proof (__list_store_Z_concat_r (sublist 0 i l_3) val1_2 (Znth i l_3 0)). + apply H29 in H9. + rewrite Zlength_sublist0 in H9. + assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i = Znth i l_3 0 * 4294967296 ^ i + val1_2) by lia. + rewrite H30. + tauto. + subst l_3. + rewrite H15. + lia. + apply list_within_bound_Znth. + lia. + unfold list_store_Z_compact in H7. + tauto. + - pose proof (Zlength_sublist0 i l'_2). + lia. +Admitted. Lemma proof_of_mpn_add_1_entail_wit_2_2 : mpn_add_1_entail_wit_2_2. -Proof. Admitted. +Proof. + pre_process. +Admitted. Lemma proof_of_mpn_add_1_return_wit_1 : mpn_add_1_return_wit_1. Proof. @@ -455,4 +561,7 @@ Lemma proof_of_mpn_add_1_which_implies_wit_1 : mpn_add_1_which_implies_wit_1. Proof. Admitted. Lemma proof_of_mpn_add_1_which_implies_wit_2 : mpn_add_1_which_implies_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_which_implies_wit_3 : mpn_add_1_which_implies_wit_3. Proof. Admitted. \ No newline at end of file diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index b446b28..926016c 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -294,6 +294,16 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) */ unsigned int r = ap[i] + b; b = (r < b); + /*@ + 0 <= i && i < n@pre && n@pre <= cap2 && + store_uint_array(rp@pre, i, l') * + store_uint_array_rec(rp@pre, i, cap2, l'') + which implies + exists a l''', + l'' == cons(a, l''') && 0<= i && i