ZYM/MiniGmp-Verification
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

first version annotation for mpn_add_n

Browse Source
This commit is contained in:
ZhuangYumin
2025-06-21 16:03:04 +00:00
parent f4db688a30
commit 94581ea60d
5 changed files with 2407 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2218
projects/lib/gmp_goal.v
View File

File diff suppressed because it is too large Load Diff

72
projects/lib/gmp_proof_auto.v
View File

@ -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.

33
projects/lib/gmp_proof_manual.v
View File

@ -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.

86
projects/mini-gmp.c
View File

@ -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

2
projects/mini-gmp.h
View File

@ -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);