From c206e4165f4e484d44d7188db899487a78f32a4b Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Fri, 20 Jun 2025 13:57:21 +0000 Subject: [PATCH] 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)