From 596f66206e333148bb94941fa6b449f8371373b9 Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Tue, 3 Jun 2025 09:31:20 +0000 Subject: [PATCH 1/9] chore: add devcontainer to gitignore --- .gitignore | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 17c9381..e5996c4 100755 --- a/.gitignore +++ b/.gitignore @@ -28,4 +28,6 @@ qcp qualifiedcprogramming sets .gitmodules -_CoqProject \ No newline at end of file +_CoqProject + +.devcontainer/ \ No newline at end of file From 8c52269a5e45e75bee87c44d223946ed8c395dff Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Fri, 20 Jun 2025 13:24:36 +0000 Subject: [PATCH 2/9] first version for annotations of mpn_add_1 --- .gitignore | 3 ++- projects/mini-gmp.c | 65 ++++++++++++++++++++++++++++++++++++++++++--- projects/mini-gmp.h | 3 ++- 3 files changed, 66 insertions(+), 5 deletions(-) diff --git a/.gitignore b/.gitignore index e5996c4..9acaeaf 100755 --- a/.gitignore +++ b/.gitignore @@ -30,4 +30,5 @@ sets .gitmodules _CoqProject -.devcontainer/ \ No newline at end of file +.devcontainer/ +.vscode/ \ No newline at end of file diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 8b9dd25..47fe743 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -223,23 +223,82 @@ mpn_normalized_size (unsigned int *xp, int n) } /* 多精度数ap 加上单精度数b，返回最后产生的进位 */ -/*unsigned int +unsigned int mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) +/*@ + With val l2 cap1 cap2 + Require + mpd_store_Z_compact(ap, val, n, cap1) * + store_uint_array(rp, cap2, l2) && + Zlength(l2) == cap2 && + cap2 >= n && + cap1 <= 100000000 && + cap2 <= 100000000 && + n > 0 && n <= cap1 + Ensure + exists val', + mpd_store_Z_compact(ap@pre, val, n@pre, cap1) * + mpd_store_Z_compact(rp@pre, val', n@pre, cap2) && + (val' + __return * (UINT_MOD ^ n@pre) == val + b@pre) +*/ { + /*@ + mpd_store_Z_compact(ap@pre, val, n@pre, cap1) + which implies + exists l, + n@pre <= cap1 && + Zlength(l) == n@pre && + cap1 <= 100000000 && + store_uint_array(ap@pre, n@pre, l) * + store_undef_uint_array_rec(ap@pre, n@pre, cap1) && + list_store_Z_compact(l, val) + */ int i; //assert (n > 0); i = 0; + /* do { unsigned int r = ap[i] + b; // Carry out b = (r < b); rp[i] = r; + ++i; } - while (++i < n); + while (i < n); + */ + + /*@ + store_uint_array(rp@pre, cap2, l2) && Zlength(l2) == cap2 + which implies + store_uint_array_rec(rp@pre, 0, cap2, l2) * store_uint_array(rp@pre, 0, nil) && + Zlength(l2) == cap2 + */ + + /*@Inv + exists l l' l'' val1 val2, + 0 <= i && i <= n@pre && + list_store_Z_compact(l, val) && n@pre <= cap1 && + store_uint_array(ap@pre, n@pre, l) * + store_undef_uint_array_rec(ap@pre, n@pre, cap1) && + list_store_Z(sublist(0, i, l), val1) && + list_store_Z(l', val2) && + store_uint_array(rp@pre, i, l') * + store_uint_array_rec(rp@pre, i, cap2, l'') && + (val2 + b@pre * (UINT_MOD ^ i) == val1 + b@pre) + */ + while (i Z -> Prop) (list_store_Z_compact: list Z -> Z -> Prop) (last: list Z -> Z -> Z) + (UINT_MOD: Z) */ \ No newline at end of file From c206e4165f4e484d44d7188db899487a78f32a4b Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Fri, 20 Jun 2025 13:57:21 +0000 Subject: [PATCH 3/9] finish symexec --- projects/lib/gmp_goal.v | 569 +++++++++++++++++++++++++++++++- projects/lib/gmp_proof_auto.v | 29 ++ projects/lib/gmp_proof_manual.v | 26 +- projects/mini-gmp.c | 2 +- projects/mini-gmp.h | 5 +- 5 files changed, 618 insertions(+), 13 deletions(-) diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v index bbb692e..4967d19 100644 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -15,11 +15,11 @@ Local Open Scope Z_scope. Local Open Scope sets. Local Open Scope string. Local Open Scope list. +Require Import Coq.ZArith.ZArith. +Local Open Scope Z_scope. Import naive_C_Rules. Local Open Scope sac. -Definition Zmax := Z.max. - (*----- Function gmp_abs -----*) Definition gmp_abs_safety_wit_1 := @@ -61,7 +61,7 @@ forall (b_pre: Z) (a_pre: Z) , [| (a_pre <= b_pre) |] && emp |-- - [| (b_pre = (Zmax (a_pre) (b_pre))) |] + [| (b_pre = (Z.max (a_pre) (b_pre))) |] && emp . @@ -70,7 +70,7 @@ forall (b_pre: Z) (a_pre: Z) , [| (a_pre > b_pre) |] && emp |-- - [| (a_pre = (Zmax (a_pre) (b_pre))) |] + [| (a_pre = (Z.max (a_pre) (b_pre))) |] && emp . @@ -1753,6 +1753,552 @@ forall (xp_pre: Z) (val: Z) (cap: Z) (n: Z) , ** (store_undef_uint_array_rec xp_pre n cap ) . +(*----- Function mpn_add_1 -----*) + +Definition mpn_add_1_safety_wit_1 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) , + [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && ((( &( "i" ) )) # Int |->_) + ** (store_uint_array ap_pre n_pre l ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** ((( &( "b" ) )) # UInt |-> b_pre) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) + ** (store_uint_array rp_pre cap2 l2 ) +|-- + [| (0 <= INT_MAX) |] + && [| ((INT_MIN) <= 0) |] +. + +Definition mpn_add_1_safety_wit_2 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) >= b_pre) |] + && [| (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_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((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 cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32))) (l'')) ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (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) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| ((i + 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (i + 1 )) |] +. + +Definition mpn_add_1_safety_wit_3 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) < b_pre) |] + && [| (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_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((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 cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32))) (l'')) ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (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) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| ((i + 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (i + 1 )) |] +. + +Definition mpn_add_1_entail_wit_1 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) , + [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array_rec rp_pre 0 cap2 l2 ) + ** (store_uint_array rp_pre 0 nil ) + ** (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +|-- + EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , + [| (0 <= 0) |] + && [| (0 <= n_pre) |] + && [| (list_store_Z_compact l val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (0) (l)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b_pre * (Z.lxor UINT_MOD 0) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array ap_pre n_pre l ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre 0 l' ) + ** (store_uint_array_rec rp_pre 0 cap2 l'' ) +. + +Definition mpn_add_1_entail_wit_2_1 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_3 0) + b_pre )) (32)) < b_pre) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_3 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_3)) val1_2 ) |] + && [| (list_store_Z l'_2 val2_2 ) |] + && [| ((val2_2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1_2 + b_pre )) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_3 0) + b_pre )) (32))) (l''_2)) ) + ** (store_uint_array ap_pre n_pre l_3 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre i l'_2 ) + ** ((( &( "b" ) )) # UInt |-> 1) +|-- + EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , + [| (0 <= (i + 1 )) |] + && [| ((i + 1 ) <= n_pre) |] + && [| (list_store_Z_compact l val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) ((i + 1 )) (l)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b_pre * (Z.lxor UINT_MOD (i + 1 )) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array ap_pre n_pre l ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre (i + 1 ) l' ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l'' ) + ** ((( &( "b" ) )) # UInt |-> b_pre) +. + +Definition mpn_add_1_entail_wit_2_2 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_3 0) + b_pre )) (32)) >= b_pre) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_3 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_3)) val1_2 ) |] + && [| (list_store_Z l'_2 val2_2 ) |] + && [| ((val2_2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1_2 + b_pre )) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_3 0) + b_pre )) (32))) (l''_2)) ) + ** (store_uint_array ap_pre n_pre l_3 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre i l'_2 ) + ** ((( &( "b" ) )) # UInt |-> 0) +|-- + EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , + [| (0 <= (i + 1 )) |] + && [| ((i + 1 ) <= n_pre) |] + && [| (list_store_Z_compact l val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) ((i + 1 )) (l)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b_pre * (Z.lxor UINT_MOD (i + 1 )) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array ap_pre n_pre l ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre (i + 1 ) l' ) + ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l'' ) + ** ((( &( "b" ) )) # UInt |-> b_pre) +. + +Definition mpn_add_1_return_wit_1 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) (i: Z) , + [| (i >= n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array ap_pre n_pre l ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) +|-- + EX (val': Z) , + [| ((val' + (b_pre * (Z.lxor UINT_MOD n_pre) ) ) = (val + b_pre )) |] + && (mpd_store_Z_compact ap_pre val n_pre cap1 ) + ** (mpd_store_Z_compact rp_pre val' n_pre cap2 ) +. + +Definition mpn_add_1_partial_solve_wit_1 := +forall (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) , + [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (mpd_store_Z_compact ap_pre val n_pre cap1 ) + ** (store_uint_array rp_pre cap2 l2 ) +|-- + [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (mpd_store_Z_compact ap_pre val n_pre cap1 ) + ** (store_uint_array rp_pre cap2 l2 ) +. + +Definition mpn_add_1_partial_solve_wit_2_pure := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) , + [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && ((( &( "i" ) )) # Int |-> 0) + ** (store_uint_array ap_pre n_pre l ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** ((( &( "b" ) )) # UInt |-> b_pre) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) + ** (store_uint_array rp_pre cap2 l2 ) +|-- + [| ((Zlength (l2)) = cap2) |] +. + +Definition mpn_add_1_partial_solve_wit_2_aux := +forall (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) , + [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array ap_pre n_pre l ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre cap2 l2 ) +|-- + [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array rp_pre cap2 l2 ) + ** (store_uint_array ap_pre n_pre l ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +. + +Definition mpn_add_1_partial_solve_wit_2 := mpn_add_1_partial_solve_wit_2_pure -> mpn_add_1_partial_solve_wit_2_aux. + +Definition mpn_add_1_partial_solve_wit_3 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , + [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array ap_pre n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) +|-- + [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (((ap_pre + (i * sizeof(UINT) ) )) # UInt |-> (Znth i l_2 0)) + ** (store_uint_array_missing_i_rec ap_pre i 0 n_pre l_2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) +. + +Definition mpn_add_1_partial_solve_wit_4 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) < b_pre) |] + && [| (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_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((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'' ) +|-- + [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) < b_pre) |] + && [| (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_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((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' ) +. + +Definition mpn_add_1_partial_solve_wit_5 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) >= b_pre) |] + && [| (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_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((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'' ) +|-- + [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) >= b_pre) |] + && [| (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_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((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' ) +. + +Definition mpn_add_1_which_implies_wit_1 := +forall (n_pre: Z) (ap_pre: Z) (cap1: Z) (val: Z) , + (mpd_store_Z_compact ap_pre val n_pre cap1 ) +|-- + EX (l: (@list Z)) , + [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && (store_uint_array ap_pre n_pre l ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) +. + +Definition mpn_add_1_which_implies_wit_2 := +forall (rp_pre: Z) (cap2: Z) (l2: (@list Z)) , + [| ((Zlength (l2)) = cap2) |] + && (store_uint_array rp_pre cap2 l2 ) +|-- + [| ((Zlength (l2)) = cap2) |] + && (store_uint_array_rec rp_pre 0 cap2 l2 ) + ** (store_uint_array rp_pre 0 nil ) +. + Module Type VC_Correct. Axiom proof_of_gmp_abs_safety_wit_1 : gmp_abs_safety_wit_1. @@ -1823,5 +2369,20 @@ Axiom proof_of_mpn_normalized_size_return_wit_1_2 : mpn_normalized_size_return_w Axiom proof_of_mpn_normalized_size_partial_solve_wit_1 : mpn_normalized_size_partial_solve_wit_1. Axiom proof_of_mpn_normalized_size_partial_solve_wit_2 : mpn_normalized_size_partial_solve_wit_2. Axiom proof_of_mpn_normalized_size_which_implies_wit_1 : mpn_normalized_size_which_implies_wit_1. +Axiom proof_of_mpn_add_1_safety_wit_1 : mpn_add_1_safety_wit_1. +Axiom proof_of_mpn_add_1_safety_wit_2 : mpn_add_1_safety_wit_2. +Axiom proof_of_mpn_add_1_safety_wit_3 : mpn_add_1_safety_wit_3. +Axiom proof_of_mpn_add_1_entail_wit_1 : mpn_add_1_entail_wit_1. +Axiom proof_of_mpn_add_1_entail_wit_2_1 : mpn_add_1_entail_wit_2_1. +Axiom proof_of_mpn_add_1_entail_wit_2_2 : mpn_add_1_entail_wit_2_2. +Axiom proof_of_mpn_add_1_return_wit_1 : mpn_add_1_return_wit_1. +Axiom proof_of_mpn_add_1_partial_solve_wit_1 : mpn_add_1_partial_solve_wit_1. +Axiom proof_of_mpn_add_1_partial_solve_wit_2_pure : mpn_add_1_partial_solve_wit_2_pure. +Axiom proof_of_mpn_add_1_partial_solve_wit_2 : mpn_add_1_partial_solve_wit_2. +Axiom proof_of_mpn_add_1_partial_solve_wit_3 : mpn_add_1_partial_solve_wit_3. +Axiom proof_of_mpn_add_1_partial_solve_wit_4 : mpn_add_1_partial_solve_wit_4. +Axiom proof_of_mpn_add_1_partial_solve_wit_5 : mpn_add_1_partial_solve_wit_5. +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. End VC_Correct. diff --git a/projects/lib/gmp_proof_auto.v b/projects/lib/gmp_proof_auto.v index 153a2b3..b664c03 100644 --- a/projects/lib/gmp_proof_auto.v +++ b/projects/lib/gmp_proof_auto.v @@ -15,6 +15,8 @@ Local Open Scope Z_scope. Local Open Scope sets. Local Open Scope string. Local Open Scope list. +Require Import Coq.ZArith.ZArith. +Local Open Scope Z_scope. Import naive_C_Rules. Local Open Scope sac. @@ -141,3 +143,30 @@ Proof. Admitted. Lemma proof_of_mpn_normalized_size_partial_solve_wit_2 : mpn_normalized_size_partial_solve_wit_2. Proof. Admitted. +Lemma proof_of_mpn_add_1_safety_wit_1 : mpn_add_1_safety_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_safety_wit_2 : mpn_add_1_safety_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_safety_wit_3 : mpn_add_1_safety_wit_3. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_1 : mpn_add_1_partial_solve_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_2_pure : mpn_add_1_partial_solve_wit_2_pure. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_2 : mpn_add_1_partial_solve_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_3 : mpn_add_1_partial_solve_wit_3. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_4 : mpn_add_1_partial_solve_wit_4. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_partial_solve_wit_5 : mpn_add_1_partial_solve_wit_5. +Proof. Admitted. + diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 8aedbd0..4b544d2 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -30,17 +30,11 @@ Proof. pre_process. Qed. Lemma proof_of_gmp_max_return_wit_1_1 : gmp_max_return_wit_1_1. Proof. pre_process. - entailer!. - unfold Zmax. - rewrite Z.max_r; lia. Qed. Lemma proof_of_gmp_max_return_wit_1_2 : gmp_max_return_wit_1_2. Proof. pre_process. - entailer!. - unfold Zmax. - rewrite Z.max_l; lia. Qed. Lemma proof_of_gmp_cmp_return_wit_1_2 : gmp_cmp_return_wit_1_2. @@ -410,4 +404,22 @@ Proof. entailer!. + rewrite sublist_self; try lia. tauto. -Qed. \ No newline at end of file +Qed. + +Lemma proof_of_mpn_add_1_entail_wit_1 : mpn_add_1_entail_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_entail_wit_2_1 : mpn_add_1_entail_wit_2_1. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_entail_wit_2_2 : mpn_add_1_entail_wit_2_2. +Proof. Admitted. + +Lemma proof_of_mpn_add_1_return_wit_1 : mpn_add_1_return_wit_1. +Proof. Admitted. + +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. \ No newline at end of file diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 47fe743..7db66bf 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -15,7 +15,7 @@ int gmp_abs(int x) int gmp_max(int a, int b) /*@ Require emp - Ensure __return == Zmax(a, b) + Ensure __return == Z::max(a, b) */ { return a > b ? a : b; diff --git a/projects/mini-gmp.h b/projects/mini-gmp.h index f231c8e..3150d84 100755 --- a/projects/mini-gmp.h +++ b/projects/mini-gmp.h @@ -58,9 +58,12 @@ void mpz_sub (mpz_t, const mpz_t, const mpz_t); void mpz_set (mpz_t, const mpz_t); +/*@ Import Coq Require Import Coq.ZArith.ZArith */ +/*@ Import Coq Local Open Scope Z_scope */ + /*@ Extern Coq (Zabs : Z -> Z) - (Zmax : Z -> Z -> Z) + (Z::max : Z -> Z -> Z) (mpd_store_Z : Z -> Z -> Z -> Z -> Assertion) (mpd_store_Z_compact: Z -> Z -> Z -> Z -> Assertion) (mpd_store_list : Z -> list Z -> Z -> Assertion) From 49848bd048921e024a5eba315dbb2a4c7cec2dad Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Fri, 20 Jun 2025 16:57:26 +0000 Subject: [PATCH 4/9] finish proof_of_mpn_add_1_return_wit_1 --- projects/lib/GmpAux.v | 5 ++ projects/lib/GmpNumber.v | 6 +++ projects/lib/gmp_goal.v | 94 ++++++++++++++++++--------------- projects/lib/gmp_proof_manual.v | 37 ++++++++++++- projects/mini-gmp.c | 7 +-- projects/mini-gmp.h | 1 + 6 files changed, 103 insertions(+), 47 deletions(-) diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index c3ff11a..3a4c199 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -314,6 +314,11 @@ Proof. split; tauto. Qed. +Lemma store_uint_array_rec_def2undef: forall x a b l, + store_uint_array_rec x a b l |-- + store_undef_uint_array_rec x a b. +Proof. Admitted. + Lemma store_undef_uint_array_rec_divide: forall x l mid r, 0 <= l <= r -> l <= mid <= r -> diff --git a/projects/lib/GmpNumber.v b/projects/lib/GmpNumber.v index 787c79e..2bae2ab 100755 --- a/projects/lib/GmpNumber.v +++ b/projects/lib/GmpNumber.v @@ -89,6 +89,12 @@ Proof. reflexivity. Qed. +Lemma list_store_Z_compact_reverse_injection: forall l1 l2 n1 n2, + list_store_Z_compact l1 n1 -> + list_store_Z_compact l2 n2 -> + n1 = n2 -> l1 = l2. +Proof. Admitted. + Lemma __list_within_bound_concat_r: forall (l1: list Z) (a: Z), list_within_bound l1 -> 0 <= a < UINT_MOD -> diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v index 4967d19..1e185ca 100644 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -1781,8 +1781,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ . Definition mpn_add_1_safety_wit_2 := -forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , - [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) >= b_pre) |] +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1790,7 +1790,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -1802,9 +1803,9 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (cap2 <= 100000000) |] && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] - && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32))) (l'')) ) + && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) (l'')) ) ** (store_uint_array ap_pre n_pre l_2 ) - ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32))) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ** ((( &( "i" ) )) # Int |-> i) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre i l' ) @@ -1818,8 +1819,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ . Definition mpn_add_1_safety_wit_3 := -forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , - [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) < b_pre) |] +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1827,7 +1828,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -1839,9 +1841,9 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (cap2 <= 100000000) |] && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] - && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32))) (l'')) ) + && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) (l'')) ) ** (store_uint_array ap_pre n_pre l_2 ) - ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32))) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ** ((( &( "i" ) )) # Int |-> i) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre i l' ) @@ -1879,7 +1881,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (0) (l)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD 0) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b_pre * (Z.pow (UINT_MOD) (0)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = 0) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] @@ -1898,8 +1901,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ . Definition mpn_add_1_entail_wit_2_1 := -forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) , - [| ((unsigned_last_nbits (((Znth i l_3 0) + b_pre )) (32)) < b_pre) |] +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (b: Z) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32)) < b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1907,7 +1910,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_3)) val1_2 ) |] && [| (list_store_Z l'_2 val2_2 ) |] - && [| ((val2_2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1_2 + b_pre )) |] + && [| ((val2_2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1_2 + b_pre )) |] + && [| ((Zlength (l'_2)) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] @@ -1919,11 +1923,10 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (cap2 <= 100000000) |] && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] - && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_3 0) + b_pre )) (32))) (l''_2)) ) + && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32))) (l''_2)) ) ** (store_uint_array ap_pre n_pre l_3 ) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre i l'_2 ) - ** ((( &( "b" ) )) # UInt |-> 1) |-- EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , [| (0 <= (i + 1 )) |] @@ -1932,7 +1935,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD (i + 1 )) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (1 * (Z.pow (UINT_MOD) ((i + 1 ))) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = (i + 1 )) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] @@ -1948,12 +1952,11 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre (i + 1 ) l' ) ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l'' ) - ** ((( &( "b" ) )) # UInt |-> b_pre) . Definition mpn_add_1_entail_wit_2_2 := -forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) , - [| ((unsigned_last_nbits (((Znth i l_3 0) + b_pre )) (32)) >= b_pre) |] +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (b: Z) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32)) >= b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1961,7 +1964,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_3)) val1_2 ) |] && [| (list_store_Z l'_2 val2_2 ) |] - && [| ((val2_2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1_2 + b_pre )) |] + && [| ((val2_2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1_2 + b_pre )) |] + && [| ((Zlength (l'_2)) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] @@ -1973,11 +1977,10 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (cap2 <= 100000000) |] && [| (n_pre > 0) |] && [| (n_pre <= cap1) |] - && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_3 0) + b_pre )) (32))) (l''_2)) ) + && (store_uint_array_rec rp_pre i cap2 (replace_Znth ((i - i )) ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32))) (l''_2)) ) ** (store_uint_array ap_pre n_pre l_3 ) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre i l'_2 ) - ** ((( &( "b" ) )) # UInt |-> 0) |-- EX (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) , [| (0 <= (i + 1 )) |] @@ -1986,7 +1989,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) ((i + 1 )) (l)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD (i + 1 )) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (0 * (Z.pow (UINT_MOD) ((i + 1 ))) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = (i + 1 )) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] @@ -2002,11 +2006,10 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre (i + 1 ) l' ) ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l'' ) - ** ((( &( "b" ) )) # UInt |-> b_pre) . Definition mpn_add_1_return_wit_1 := -forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) (i: Z) , +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l: (@list Z)) (i: Z) , [| (i >= n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2014,7 +2017,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l_2)) = n_pre) |] @@ -2032,9 +2036,9 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_uint_array_rec rp_pre i cap2 l'' ) |-- EX (val': Z) , - [| ((val' + (b_pre * (Z.lxor UINT_MOD n_pre) ) ) = (val + b_pre )) |] + [| ((val' + (b * (Z.pow (UINT_MOD) (n_pre)) ) ) = (val + b_pre )) |] && (mpd_store_Z_compact ap_pre val n_pre cap1 ) - ** (mpd_store_Z_compact rp_pre val' n_pre cap2 ) + ** (mpd_store_Z rp_pre val' n_pre cap2 ) . Definition mpn_add_1_partial_solve_wit_1 := @@ -2117,7 +2121,7 @@ forall (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (v Definition mpn_add_1_partial_solve_wit_2 := mpn_add_1_partial_solve_wit_2_pure -> mpn_add_1_partial_solve_wit_2_aux. Definition mpn_add_1_partial_solve_wit_3 := -forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2125,7 +2129,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -2149,7 +2154,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -2169,8 +2175,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ . Definition mpn_add_1_partial_solve_wit_4 := -forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , - [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) < b_pre) |] +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2178,7 +2184,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -2195,7 +2202,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_uint_array rp_pre i l' ) ** (store_uint_array_rec rp_pre i cap2 l'' ) |-- - [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) < b_pre) |] + [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2203,7 +2210,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -2223,8 +2231,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ . Definition mpn_add_1_partial_solve_wit_5 := -forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , - [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) >= b_pre) |] +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , + [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2232,7 +2240,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] @@ -2249,7 +2258,7 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_uint_array rp_pre i l' ) ** (store_uint_array_rec rp_pre i cap2 l'' ) |-- - [| ((unsigned_last_nbits (((Znth i l_2 0) + b_pre )) (32)) >= b_pre) |] + [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2257,7 +2266,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (n_pre <= cap1) |] && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] && [| (list_store_Z l' val2 ) |] - && [| ((val2 + (b_pre * (Z.lxor UINT_MOD i) ) ) = (val1 + b_pre )) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] && [| ((Zlength (l2)) = cap2) |] && [| (n_pre <= cap1) |] && [| ((Zlength (l)) = n_pre) |] diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 4b544d2..32fbea2 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -11,7 +11,7 @@ Require Import SetsClass.SetsClass. Import SetsNotation. From SimpleC.SL Require Import Mem SeparationLogic. From GmpLib Require Import gmp_goal. Require Import GmpLib.GmpNumber. Import Internal. -Require Import GmpLib.GmpAux. +Require Import GmpLib.GmpAux. Import Aux. Require Import Logic.LogicGenerator.demo932.Interface. Local Open Scope Z_scope. Local Open Scope sets. @@ -416,7 +416,40 @@ Lemma proof_of_mpn_add_1_entail_wit_2_2 : mpn_add_1_entail_wit_2_2. Proof. Admitted. Lemma proof_of_mpn_add_1_return_wit_1 : mpn_add_1_return_wit_1. -Proof. Admitted. +Proof. + pre_process. + unfold mpd_store_Z_compact. + unfold mpd_store_list. + Exists val2. + pose proof (list_store_Z_compact_reverse_injection l l_2 val val). + apply H19 in H2; try tauto. + rewrite <-H2 in H10. + assert (i = n_pre) by lia. + rewrite H20 in H4. + rewrite <- H10 in H4. + rewrite (sublist_self l (Zlength l)) in H4; try tauto. + rewrite <-H2 in H12. + assert (list_store_Z l val). { apply list_store_Z_compact_to_normal. tauto. } + pose proof (list_store_Z_injection l l val1 val). + apply H22 in H4; try tauto. + rewrite H4 in H6. + entailer!. + Exists l. + entailer!. + entailer!; try rewrite H20; try tauto. + - rewrite H10. + entailer!. + unfold mpd_store_Z. + unfold mpd_store_list. + Exists l'. + rewrite H7. + subst i. + entailer!. + rewrite H20. + entailer!. + apply store_uint_array_rec_def2undef. + - rewrite <- H20. tauto. +Qed. Lemma proof_of_mpn_add_1_which_implies_wit_1 : mpn_add_1_which_implies_wit_1. Proof. Admitted. diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 7db66bf..b446b28 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -238,8 +238,8 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) Ensure exists val', mpd_store_Z_compact(ap@pre, val, n@pre, cap1) * - mpd_store_Z_compact(rp@pre, val', n@pre, cap2) && - (val' + __return * (UINT_MOD ^ n@pre) == val + b@pre) + mpd_store_Z(rp@pre, val', n@pre, cap2) && + (val' + __return * Z::pow(UINT_MOD, n@pre) == val + b@pre) */ { /*@ @@ -285,7 +285,8 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) list_store_Z(l', val2) && store_uint_array(rp@pre, i, l') * store_uint_array_rec(rp@pre, i, cap2, l'') && - (val2 + b@pre * (UINT_MOD ^ i) == val1 + b@pre) + (val2 + b * Z::pow(UINT_MOD, i) == val1 + b@pre) && + Zlength(l') == i */ while (i Z) (Z::max : Z -> Z -> Z) + (Z::pow : Z -> Z -> Z) (mpd_store_Z : Z -> Z -> Z -> Z -> Assertion) (mpd_store_Z_compact: Z -> Z -> Z -> Z -> Assertion) (mpd_store_list : Z -> list Z -> Z -> Assertion) From f462570ccdcc7a8329ceb4f167401308a8b7bb0c Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sat, 21 Jun 2025 05:45:27 +0000 Subject: [PATCH 5/9] 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 Date: Sat, 21 Jun 2025 07:50:20 +0000 Subject: [PATCH 6/9] finish carry proof --- projects/lib/GmpAux.v | 6 ++ projects/lib/gmp_goal.v | 116 +++++++++++++++++++++++++++++--- projects/lib/gmp_proof_manual.v | 87 ++++++++++++++++-------- projects/mini-gmp.c | 1 + 4 files changed, 171 insertions(+), 39 deletions(-) diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index 3a4c199..8d1c1ac 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -21,6 +21,12 @@ Local Open Scope sac. Module Aux. +Lemma Z_mod_add_carry: forall (a b m: Z), + m > 0 -> 0 <= a < m -> 0 <= b < m -> + (a + b) mod m < b -> + a + b = (a + b) mod m + m. +Proof. Admitted. + Lemma Z_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_goal.v b/projects/lib/gmp_goal.v index 911faa4..220809d 100644 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -1787,6 +1787,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1810,10 +1812,10 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ((app (l') ((cons (a) (nil)))))) ) ** ((( &( "i" ) )) # Int |-> i) ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) + ** ((( &( "b" ) )) # UInt |-> 0) ** (store_uint_array ap_pre n_pre l_2 ) ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) - ** ((( &( "b" ) )) # UInt |-> 0) ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) ** ((( &( "rp" ) )) # Ptr |-> rp_pre) @@ -1829,6 +1831,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1852,10 +1856,10 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && (store_uint_array rp_pre (i + 1 ) (replace_Znth (i) ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ((app (l') ((cons (a) (nil)))))) ) ** ((( &( "i" ) )) # Int |-> i) ** (store_uint_array_rec rp_pre (i + 1 ) cap2 l''' ) + ** ((( &( "b" ) )) # UInt |-> 1) ** (store_uint_array ap_pre n_pre l_2 ) ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) - ** ((( &( "b" ) )) # UInt |-> 1) ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) ** ((( &( "rp" ) )) # Ptr |-> rp_pre) @@ -1908,13 +1912,82 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ ** (store_uint_array_rec rp_pre 0 cap2 l'' ) . -Definition mpn_add_1_entail_wit_2_1 := +Definition mpn_add_1_entail_wit_2 := +forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , + [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && (store_uint_array ap_pre n_pre l_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) + ** ((( &( "b" ) )) # UInt |-> b) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +|-- + [| (0 <= b) |] + && [| (b <= UINT_MAX) |] + && [| (i < n_pre) |] + && [| (0 <= i) |] + && [| (i <= n_pre) |] + && [| (list_store_Z_compact l_2 val ) |] + && [| (n_pre <= cap1) |] + && [| (list_store_Z (sublist (0) (i) (l_2)) val1 ) |] + && [| (list_store_Z l' val2 ) |] + && [| ((val2 + (b * (Z.pow (UINT_MOD) (i)) ) ) = (val1 + b_pre )) |] + && [| ((Zlength (l')) = i) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z_compact l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (n_pre > 0) |] + && [| (n_pre <= cap1) |] + && ((( &( "b" ) )) # UInt |-> b) + ** (store_uint_array ap_pre n_pre l_2 ) + ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) + ** ((( &( "i" ) )) # Int |-> i) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_uint_array rp_pre i l' ) + ** (store_uint_array_rec rp_pre i cap2 l'' ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** ((( &( "rp" ) )) # Ptr |-> rp_pre) +. + +Definition mpn_add_1_entail_wit_3_1 := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (b: Z) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) (a: Z) (l''': (@list Z)) , [| (l''_2 = (cons (a) (l'''))) |] && [| (0 <= i) |] && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -1966,13 +2039,15 @@ 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 + 1 ) cap2 l'' ) . -Definition mpn_add_1_entail_wit_2_2 := +Definition mpn_add_1_entail_wit_3_2 := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (b: Z) (l''_2: (@list Z)) (l'_2: (@list Z)) (val2_2: Z) (val1_2: Z) (l_3: (@list Z)) (i: Z) (a: Z) (l''': (@list Z)) , [| (l''_2 = (cons (a) (l'''))) |] && [| (0 <= i) |] && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_3 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2193,6 +2268,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ Definition mpn_add_1_partial_solve_wit_4_pure := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2213,13 +2290,13 @@ 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 ap_pre n_pre l_2 ) + && ((( &( "b" ) )) # UInt |-> 0) + ** (store_uint_array ap_pre n_pre l_2 ) ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ** ((( &( "i" ) )) # Int |-> i) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre i l' ) ** (store_uint_array_rec rp_pre i cap2 l'' ) - ** ((( &( "b" ) )) # UInt |-> 0) ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) ** ((( &( "rp" ) )) # Ptr |-> rp_pre) @@ -2232,6 +2309,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ Definition mpn_add_1_partial_solve_wit_4_aux := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2261,6 +2340,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2292,6 +2373,8 @@ Definition mpn_add_1_partial_solve_wit_4 := mpn_add_1_partial_solve_wit_4_pure - Definition mpn_add_1_partial_solve_wit_5_pure := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2312,13 +2395,13 @@ 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 ap_pre n_pre l_2 ) + && ((( &( "b" ) )) # UInt |-> 1) + ** (store_uint_array ap_pre n_pre l_2 ) ** ((( &( "r" ) )) # UInt |-> (unsigned_last_nbits (((Znth i l_2 0) + b )) (32))) ** ((( &( "i" ) )) # Int |-> i) ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) ** (store_uint_array rp_pre i l' ) ** (store_uint_array_rec rp_pre i cap2 l'' ) - ** ((( &( "b" ) )) # UInt |-> 1) ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) ** ((( &( "rp" ) )) # Ptr |-> rp_pre) @@ -2331,6 +2414,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ Definition mpn_add_1_partial_solve_wit_5_aux := forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (b: Z) (l'': (@list Z)) (l': (@list Z)) (val2: Z) (val1: Z) (l_2: (@list Z)) (i: Z) , [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2360,6 +2445,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2395,6 +2482,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2425,6 +2514,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) < b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2459,6 +2550,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2489,6 +2582,8 @@ forall (b_pre: Z) (n_pre: Z) (ap_pre: Z) (rp_pre: Z) (cap2: Z) (cap1: Z) (l2: (@ && [| (i < n_pre) |] && [| (n_pre <= cap2) |] && [| ((unsigned_last_nbits (((Znth i l_2 0) + b )) (32)) >= b) |] + && [| (0 <= b) |] + && [| (b <= UINT_MAX) |] && [| (i < n_pre) |] && [| (0 <= i) |] && [| (i <= n_pre) |] @@ -2630,8 +2725,9 @@ Axiom proof_of_mpn_add_1_safety_wit_1 : mpn_add_1_safety_wit_1. Axiom proof_of_mpn_add_1_safety_wit_2 : mpn_add_1_safety_wit_2. Axiom proof_of_mpn_add_1_safety_wit_3 : mpn_add_1_safety_wit_3. Axiom proof_of_mpn_add_1_entail_wit_1 : mpn_add_1_entail_wit_1. -Axiom proof_of_mpn_add_1_entail_wit_2_1 : mpn_add_1_entail_wit_2_1. -Axiom proof_of_mpn_add_1_entail_wit_2_2 : mpn_add_1_entail_wit_2_2. +Axiom proof_of_mpn_add_1_entail_wit_2 : mpn_add_1_entail_wit_2. +Axiom proof_of_mpn_add_1_entail_wit_3_1 : mpn_add_1_entail_wit_3_1. +Axiom proof_of_mpn_add_1_entail_wit_3_2 : mpn_add_1_entail_wit_3_2. Axiom proof_of_mpn_add_1_return_wit_1 : mpn_add_1_return_wit_1. Axiom proof_of_mpn_add_1_partial_solve_wit_1 : mpn_add_1_partial_solve_wit_1. Axiom proof_of_mpn_add_1_partial_solve_wit_2_pure : mpn_add_1_partial_solve_wit_2_pure. diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index f7e7044..ba68a43 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -422,14 +422,20 @@ Proof. + simpl. tauto. Qed. -Lemma proof_of_mpn_add_1_entail_wit_2_1 : mpn_add_1_entail_wit_2_1. +Lemma proof_of_mpn_add_1_entail_wit_2 : mpn_add_1_entail_wit_2. +Proof. + pre_process. + entailer!. +Admitted. + +Lemma proof_of_mpn_add_1_entail_wit_3_1 : mpn_add_1_entail_wit_3_1. Proof. pre_process. rewrite replace_Znth_app_r. - Exists l'''. - rewrite H12. + rewrite H14. assert (i - i = 0) by lia. - rewrite H24. + rewrite H26. set (new_b := (unsigned_last_nbits (Znth i l_3 0 + b) 32)). rewrite replace_Znth_nothing; try lia. assert (replace_Znth 0 new_b (a :: nil) = new_b :: nil). { @@ -438,85 +444,108 @@ Proof. unfold replace_nth. reflexivity. } - rewrite H25. + rewrite H27. Exists (l'_2 ++ new_b :: nil). Exists (val2_2 + new_b * (UINT_MOD^ i)). Exists (val1_2 + (Znth i l_3 0) * (UINT_MOD^ i)). Exists l_3. entailer!. + rewrite Zlength_app. - rewrite H12. + rewrite H14. unfold Zlength. unfold Zlength_aux. lia. + assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i + b_pre = (val1_2 + b_pre) + Znth i l_3 0 * 4294967296 ^ i) by lia. - rewrite H26. - rewrite <- H11. + rewrite H28. + rewrite <- H13. assert (Znth i l_3 0 + b = new_b + UINT_MOD). { subst new_b. unfold unsigned_last_nbits. unfold unsigned_last_nbits in H3. assert (2^32 = 4294967296). { nia. } - rewrite H27 in *. - admit. + rewrite H29 in *. + assert (0 <= Znth i l_3 0 < 4294967296). { + assert (l_2=l_3). + { + pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val). + apply H30 in H9; try tauto. + } + assert (i < Zlength l_3). { + subst l_3. + rewrite H17. + tauto. + } + unfold list_store_Z_compact in H9. + apply list_within_bound_Znth. + lia. + tauto. + } + apply Z_mod_add_carry; try lia; try tauto. } - admit. + assert (b * 4294967296 ^ i + Znth i l_3 0 * 4294967296 ^ i = new_b * 4294967296 ^ i + 1 * 4294967296 ^ (i + 1)). + { + subst new_b. + Search [ Zmult Zplus "distr" ]. + rewrite <- Z.mul_add_distr_r. + rewrite (Zpow_add_1 4294967296 i); try lia. + } + lia. + pose proof (__list_store_Z_concat_r l'_2 val2_2 new_b). - apply H26 in H10. - rewrite H12 in H10. + apply H28 in H12. + rewrite H14 in H12. assert (new_b * 4294967296 ^ i + val2_2 = (val2_2 + new_b * 4294967296 ^ i)) by lia. - rewrite H27 in H10. + rewrite H29 in H12. tauto. subst new_b. unfold unsigned_last_nbits. assert (2 ^ 32 = 4294967296). { nia. } - rewrite H27. + rewrite H29. apply Z.mod_pos_bound. lia. + assert (l_2=l_3). { pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val). - apply H26 in H7; try tauto. + apply H28 in H9; try tauto. } assert (i < Zlength l_3). { subst l_3. - rewrite H15. + rewrite H17. tauto. } assert((sublist 0 (i + 1) l_3) = (sublist 0 i l_3) ++ (Znth i l_3 0) :: nil). { pose proof (sublist_split 0 (i+1) i l_3). pose proof (sublist_single i l_3 0). - rewrite <-H29. - apply H28. + rewrite <-H31. + apply H30. lia. subst l_3. - rewrite Zlength_correct in H27. + rewrite Zlength_correct in H29. lia. - rewrite Zlength_correct in H27. + rewrite Zlength_correct in H29. 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. + pose proof (__list_store_Z_concat_r (sublist 0 i l_3) val1_2 (Znth i l_3 0)). + apply H31 in H11. + rewrite Zlength_sublist0 in H11. + assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i = Znth i l_3 0 * 4294967296 ^ i + val1_2) by lia. + rewrite H32. tauto. subst l_3. - rewrite H15. + rewrite H17. lia. apply list_within_bound_Znth. lia. - unfold list_store_Z_compact in H7. + unfold list_store_Z_compact in H9. tauto. - pose proof (Zlength_sublist0 i l'_2). lia. -Admitted. +Qed. -Lemma proof_of_mpn_add_1_entail_wit_2_2 : mpn_add_1_entail_wit_2_2. +Lemma proof_of_mpn_add_1_entail_wit_3_2 : mpn_add_1_entail_wit_3_2. Proof. pre_process. Admitted. diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 926016c..53dd6d5 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -293,6 +293,7 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) Given l l' l'' val1 val2 */ unsigned int r = ap[i] + b; + /*@ 0 <= b && b <= UINT_MAX by local */ b = (r < b); /*@ 0 <= i && i < n@pre && n@pre <= cap2 && From 9ccea058357c3fe072e3536010712b0fc7acbb4a Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sat, 21 Jun 2025 08:00:17 +0000 Subject: [PATCH 7/9] finish uncarry --- projects/lib/GmpAux.v | 6 ++ projects/lib/gmp_proof_manual.v | 114 +++++++++++++++++++++++++++++++- 2 files changed, 119 insertions(+), 1 deletion(-) diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index 8d1c1ac..7bbdf01 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -27,6 +27,12 @@ Lemma Z_mod_add_carry: forall (a b m: Z), a + b = (a + b) mod m + m. Proof. Admitted. +Lemma Z_mod_add_uncarry: forall (a b m: Z), + m > 0 -> 0 <= a < m -> 0 <= b < m -> + (a + b) mod m >= b -> + a + b = (a + b) mod m. +Proof. Admitted. + Lemma Z_of_nat_succ: forall (n: nat), Z.of_nat (S n) = Z.of_nat n + 1. Proof. lia. Qed. diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index ba68a43..c82e028 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -548,7 +548,119 @@ Qed. Lemma proof_of_mpn_add_1_entail_wit_3_2 : mpn_add_1_entail_wit_3_2. Proof. pre_process. -Admitted. + rewrite replace_Znth_app_r. + - Exists l'''. + rewrite H14. + assert (i - i = 0) by lia. + rewrite H26. + set (new_b := (unsigned_last_nbits (Znth i l_3 0 + b) 32)). + rewrite replace_Znth_nothing; try lia. + assert (replace_Znth 0 new_b (a :: nil) = new_b :: nil). { + unfold replace_Znth. + unfold Z.to_nat. + unfold replace_nth. + reflexivity. + } + rewrite H27. + Exists (l'_2 ++ new_b :: nil). + Exists (val2_2 + new_b * (UINT_MOD^ i)). + Exists (val1_2 + (Znth i l_3 0) * (UINT_MOD^ i)). + Exists l_3. + entailer!. + + rewrite Zlength_app. + rewrite H14. + unfold Zlength. + unfold Zlength_aux. + lia. + + assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i + b_pre = (val1_2 + b_pre) + Znth i l_3 0 * 4294967296 ^ i) by lia. + rewrite H28. + rewrite <- H13. + assert (Znth i l_3 0 + b = new_b). + { + subst new_b. + unfold unsigned_last_nbits. + unfold unsigned_last_nbits in H3. + assert (2^32 = 4294967296). { nia. } + rewrite H29 in *. + assert (0 <= Znth i l_3 0 < 4294967296). { + assert (l_2=l_3). + { + pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val). + apply H30 in H9; try tauto. + } + assert (i < Zlength l_3). { + subst l_3. + rewrite H17. + tauto. + } + unfold list_store_Z_compact in H9. + apply list_within_bound_Znth. + lia. + tauto. + } + apply Z_mod_add_uncarry; try lia; try tauto. + } + assert (b * 4294967296 ^ i + Znth i l_3 0 * 4294967296 ^ i = new_b * 4294967296 ^ i + 0 * 4294967296 ^ (i + 1)). + { + subst new_b. + Search [ Zmult Zplus "distr" ]. + rewrite <- Z.mul_add_distr_r. + rewrite (Zpow_add_1 4294967296 i); try lia. + } + lia. + + pose proof (__list_store_Z_concat_r l'_2 val2_2 new_b). + apply H28 in H12. + rewrite H14 in H12. + assert (new_b * 4294967296 ^ i + val2_2 = (val2_2 + new_b * 4294967296 ^ i)) by lia. + rewrite H29 in H12. + tauto. + subst new_b. + unfold unsigned_last_nbits. + assert (2 ^ 32 = 4294967296). { nia. } + rewrite H29. + apply Z.mod_pos_bound. + lia. + + assert (l_2=l_3). + { + pose proof (list_store_Z_compact_reverse_injection l_2 l_3 val val). + apply H28 in H9; try tauto. + } + + assert (i < Zlength l_3). { + subst l_3. + rewrite H17. + tauto. + } + + assert((sublist 0 (i + 1) l_3) = (sublist 0 i l_3) ++ (Znth i l_3 0) :: nil). { + pose proof (sublist_split 0 (i+1) i l_3). + pose proof (sublist_single i l_3 0). + rewrite <-H31. + apply H30. + lia. + subst l_3. + rewrite Zlength_correct in H29. + lia. + rewrite Zlength_correct in H29. + lia. + } + rewrite H30. + pose proof (__list_store_Z_concat_r (sublist 0 i l_3) val1_2 (Znth i l_3 0)). + apply H31 in H11. + rewrite Zlength_sublist0 in H11. + assert (val1_2 + Znth i l_3 0 * 4294967296 ^ i = Znth i l_3 0 * 4294967296 ^ i + val1_2) by lia. + rewrite H32. + tauto. + subst l_3. + rewrite H17. + lia. + apply list_within_bound_Znth. + lia. + unfold list_store_Z_compact in H9. + tauto. + - pose proof (Zlength_sublist0 i l'_2). + lia. +Qed. Lemma proof_of_mpn_add_1_return_wit_1 : mpn_add_1_return_wit_1. Proof. From bb22511fef108219be24c5c48664d142caad1caf Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sat, 21 Jun 2025 08:17:32 +0000 Subject: [PATCH 8/9] only last wh ich implies left --- projects/lib/gmp_proof_manual.v | 32 ++++++++++++++++++++++++++++++-- 1 file changed, 30 insertions(+), 2 deletions(-) diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index c82e028..3b5fa6e 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -699,10 +699,38 @@ Proof. Qed. Lemma proof_of_mpn_add_1_which_implies_wit_1 : mpn_add_1_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_1_which_implies_wit_2 : mpn_add_1_which_implies_wit_2. -Proof. Admitted. +Proof. + pre_process. + pose proof (store_uint_array_divide rp_pre cap2 l2 0). + pose proof (Zlength_nonneg l2). + specialize (H0 ltac:(lia) ltac:(lia)). + destruct H0 as [H0 _]. + simpl in H0. + entailer!. + rewrite (sublist_nil l2 0 0) in H0; [ | lia]. + sep_apply H0. + entailer!. + unfold store_uint_array, store_uint_array_rec. + unfold store_array. + rewrite (sublist_self l2 cap2); [ | lia ]. + assert (rp_pre + 0 = rp_pre). { lia. } + rewrite H2; clear H2. + assert (cap2 - 0 = cap2). { lia. } + rewrite H2; clear H2. + reflexivity. +Qed. Lemma proof_of_mpn_add_1_which_implies_wit_3 : mpn_add_1_which_implies_wit_3. Proof. Admitted. \ No newline at end of file From 5c69a81a44aa3f102db8ea4db681c0f3afb1cb79 Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sat, 21 Jun 2025 11:47:52 +0000 Subject: [PATCH 9/9] finish mpn_add_1 --- projects/lib/gmp_proof_manual.v | 78 ++++++++++++++++++++++++++++++++- 1 file changed, 76 insertions(+), 2 deletions(-) diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 3b5fa6e..ee5ea4b 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -425,8 +425,9 @@ Qed. Lemma proof_of_mpn_add_1_entail_wit_2 : mpn_add_1_entail_wit_2. Proof. pre_process. + prop_apply (store_uint_range &("b") b). entailer!. -Admitted. +Qed. Lemma proof_of_mpn_add_1_entail_wit_3_1 : mpn_add_1_entail_wit_3_1. Proof. @@ -733,4 +734,77 @@ Proof. Qed. 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 +Proof. + pre_process. + destruct l''. { + unfold store_uint_array_rec. + simpl. + entailer!. + } + pose proof (store_uint_array_rec_cons rp_pre i cap2 z l'' ltac:(lia)). + sep_apply H2. + Exists z l''. + entailer!. + assert (i = 0 \/ i > 0). { lia. } + destruct H3. + + subst. + simpl. + entailer!. + simpl in H2. + assert (rp_pre + 0 = rp_pre). { lia. } + rewrite H3. + rewrite H3 in H2. + clear H3. + pose proof (store_uint_array_empty rp_pre l'). + sep_apply H3. + rewrite logic_equiv_andp_comm. + rewrite logic_equiv_coq_prop_andp_sepcon. + Intros. + subst l'. + rewrite app_nil_l. + unfold store_uint_array. + unfold store_array. + unfold store_array_rec. + simpl. + assert (rp_pre + 0 = rp_pre). { lia. } + rewrite H4; clear H4. + entailer!. + + pose proof (Aux.uint_array_rec_to_uint_array rp_pre 0 i (sublist 0 i l') ltac:(lia)). + destruct H4 as [_ H4]. + assert (rp_pre + sizeof(UINT) * 0 = rp_pre). { lia. } + rewrite H5 in H4; clear H5. + assert (i - 0 = i). { lia. } + rewrite H5 in H4; clear H5. + pose proof (Aux.uint_array_rec_to_uint_array rp_pre 0 (i + 1) (sublist 0 i l' ++ z :: nil) ltac:(lia)). + destruct H5 as [H5 _]. + assert (i + 1 - 0 = i + 1). { lia. } + rewrite H6 in H5; clear H6. + assert (rp_pre + sizeof(UINT) * 0 = rp_pre). { lia. } + rewrite H6 in H5; clear H6. + pose proof (uint_array_rec_to_uint_array rp_pre 0 i l'). + specialize (H6 H). + assert ((rp_pre + sizeof ( UINT ) * 0) = rp_pre) by lia. + rewrite H7 in H6; clear H7. + assert ((i-0) = i) by lia. + rewrite H7 in H6; clear H7. + destruct H6 as [_ H6]. + sep_apply H6. + (* pose proof (uint_array_rec_to_uint_array rp_pre 0 (i+1) (l' ++ z :: nil)). + assert (H_i_plus_1 : 0 <= i + 1) by lia. + specialize (H7 H_i_plus_1); clear H_i_plus_1. + destruct H7 as [H7 _]. + assert (i + 1 - 0 = i + 1) by lia. + rewrite H8 in H7; clear H8. + assert ((rp_pre + sizeof ( UINT ) * 0) = rp_pre) by lia. + rewrite H8 in H7; clear H8. + rewrite <-H7. + clear H6. + clear H7. *) + pose proof (store_uint_array_divide_rec rp_pre (i+1) (l' ++ z :: nil) i). + assert (H_tmp: 0 <= i <= i+1) by lia. + specialize (H7 H_tmp); clear H_tmp. + rewrite <- store_uint_array_single. + sep_apply store_uint_array_rec_divide_rev. + entailer!. + lia. +Qed. \ No newline at end of file