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

feat(mpz_sgn): Proved correctness of function mpz_sgn.

Browse Source
This commit is contained in:
xiaoh105
2025-06-22 19:10:35 +08:00
parent f4db688a30
commit 3a102d0d65
6 changed files with 382 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

46
projects/lib/GmpNumber.v
View File

@ -358,6 +358,52 @@ Proof.
- pose proof (Zlength_nonneg l1); lia.
Qed.
Lemma list_store_Z_compact_bound: forall (l1: list Z) (n: Z),
list_store_Z_compact l1 n ->
UINT_MOD ^ ((Zlength l1) - 1) <= n < UINT_MOD ^ (Zlength l1).
Proof.
intros.
destruct l1.
+ rewrite Zlength_nil.
simpl.
unfold list_store_Z_compact; destruct H.
simpl in H.
lia.
+ remember (z :: l1) as l eqn: Hl.
unfold list_store_Z_compact in H.
destruct H, H0.
assert (list_store_Z l n). {
unfold list_store_Z.
tauto.
}
clear H1 H.
split.
- pose proof (@nil_cons Z z l1); rewrite <-Hl in H.
pose proof (@app_removelast_last Z l 1 ltac:(auto)).
clear H.
rewrite H1 in H2.
apply list_store_Z_split in H2; destruct H2.
remember (Zlength (removelast l)) as len_lo eqn:Hlen_lo.
remember (n mod UINT_MOD ^ len_lo) as n_lo eqn:Hnlo.
remember (n / UINT_MOD ^ len_lo) as n_hi eqn:Hnhi.
assert (n = n_lo + n_hi * UINT_MOD ^ len_lo). {
pose proof (Z_div_mod_eq_full n (UINT_MOD ^ len_lo)).
lia.
}
unfold list_store_Z in H2; destruct H2.
simpl in H2.
apply list_store_Z_bound in H.
pose proof (@nil_cons Z z l1); rewrite <-Hl in H5.
pose proof (Aux.Zlength_removelast l ltac:(auto)).
clear H5.
rewrite H6 in *.
rewrite H2 in H0.
rewrite Hlen_lo in *.
nia.
- apply list_store_Z_bound in H2.
lia.
Qed.
Lemma list_store_Z_nth: forall (l: list Z) (n: Z) (i: Z),
0 <= i < Zlength l ->
list_store_Z l n ->

221
projects/lib/gmp_goal.v
View File

@ -3679,6 +3679,215 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval: Z) (retval_2:
Definition mpz_realloc_partial_solve_wit_10 := mpz_realloc_partial_solve_wit_10_pure -> mpz_realloc_partial_solve_wit_10_aux.
(*----- Function mpz_sgn -----*)
Definition mpz_sgn_safety_wit_1 :=
forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) ,
[| (size >= 0) |]
&& [| (n >= 0) |]
&& (mpd_store_Z_compact ptr n size cap )
** ((( &( "u" ) )) # Ptr |-> u_pre)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr)
|--
[| (0 <= INT_MAX) |]
&& [| ((INT_MIN) <= 0) |]
.
Definition mpz_sgn_safety_wit_2 :=
forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) (retval: Z) ,
[| (size < 0) |]
&& [| (retval = (-1)) |]
&& [| (size >= 0) |]
&& [| (n >= 0) |]
&& (mpd_store_Z_compact ptr n size cap )
** ((( &( "u" ) )) # Ptr |-> u_pre)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr)
|--
[| False |]
.
Definition mpz_sgn_safety_wit_3 :=
forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) ,
[| (size < 0) |]
&& [| (n < 0) |]
&& (mpd_store_Z_compact ptr (-n) (-size) cap )
** ((( &( "u" ) )) # Ptr |-> u_pre)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr)
|--
[| (0 <= INT_MAX) |]
&& [| ((INT_MIN) <= 0) |]
.
Definition mpz_sgn_safety_wit_4 :=
forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) (retval: Z) ,
[| (size = 0) |]
&& [| (retval = 0) |]
&& [| (size < 0) |]
&& [| (n < 0) |]
&& (mpd_store_Z_compact ptr (-n) (-size) cap )
** ((( &( "u" ) )) # Ptr |-> u_pre)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr)
|--
[| False |]
.
Definition mpz_sgn_safety_wit_5 :=
forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) (retval: Z) ,
[| (size > 0) |]
&& [| (retval = 1) |]
&& [| (size < 0) |]
&& [| (n < 0) |]
&& (mpd_store_Z_compact ptr (-n) (-size) cap )
** ((( &( "u" ) )) # Ptr |-> u_pre)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr)
|--
[| False |]
.
Definition mpz_sgn_return_wit_1_1 :=
forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) (retval: Z) ,
[| (size < 0) |]
&& [| (retval = (-1)) |]
&& [| (size < 0) |]
&& [| (n < 0) |]
&& (mpd_store_Z_compact ptr (-n) (-size) cap )
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr)
|--
([| (n < 0) |]
&& [| (retval = (-1)) |]
&& (store_Z u_pre n ))
||
([| (n = 0) |]
&& [| (retval = 0) |]
&& (store_Z u_pre n ))
||
([| (n > 0) |]
&& [| (retval = 1) |]
&& (store_Z u_pre n ))
.
Definition mpz_sgn_return_wit_1_2 :=
forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) (retval: Z) ,
[| (size > 0) |]
&& [| (retval = 1) |]
&& [| (size >= 0) |]
&& [| (n >= 0) |]
&& (mpd_store_Z_compact ptr n size cap )
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr)
|--
([| (n < 0) |]
&& [| (retval = (-1)) |]
&& (store_Z u_pre n ))
||
([| (n = 0) |]
&& [| (retval = 0) |]
&& (store_Z u_pre n ))
||
([| (n > 0) |]
&& [| (retval = 1) |]
&& (store_Z u_pre n ))
.
Definition mpz_sgn_return_wit_1_3 :=
forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) (retval: Z) ,
[| (size = 0) |]
&& [| (retval = 0) |]
&& [| (size >= 0) |]
&& [| (n >= 0) |]
&& (mpd_store_Z_compact ptr n size cap )
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr)
|--
([| (n < 0) |]
&& [| (retval = (-1)) |]
&& (store_Z u_pre n ))
||
([| (n = 0) |]
&& [| (retval = 0) |]
&& (store_Z u_pre n ))
||
([| (n > 0) |]
&& [| (retval = 1) |]
&& (store_Z u_pre n ))
.
Definition mpz_sgn_partial_solve_wit_1 :=
forall (u_pre: Z) (n: Z) ,
(store_Z u_pre n )
|--
(store_Z u_pre n )
.
Definition mpz_sgn_partial_solve_wit_2 :=
forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) ,
[| (size >= 0) |]
&& [| (n >= 0) |]
&& (mpd_store_Z_compact ptr n size cap )
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr)
|--
[| (size >= 0) |]
&& [| (n >= 0) |]
&& (mpd_store_Z_compact ptr n size cap )
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr)
.
Definition mpz_sgn_partial_solve_wit_3 :=
forall (u_pre: Z) (n: Z) (ptr: Z) (cap: Z) (size: Z) ,
[| (size < 0) |]
&& [| (n < 0) |]
&& (mpd_store_Z_compact ptr (-n) (-size) cap )
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr)
|--
[| (size < 0) |]
&& [| (n < 0) |]
&& (mpd_store_Z_compact ptr (-n) (-size) cap )
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u_pre) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr)
.
Definition mpz_sgn_which_implies_wit_1 :=
forall (n: Z) (u: Z) ,
(store_Z u n )
|--
(EX (ptr: Z) (cap: Z) (size: Z) ,
[| (size >= 0) |]
&& [| (n >= 0) |]
&& (mpd_store_Z_compact ptr n size cap )
** ((&((u) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr))
||
(EX (ptr: Z) (cap: Z) (size: Z) ,
[| (size < 0) |]
&& [| (n < 0) |]
&& (mpd_store_Z_compact ptr (-n) (-size) cap )
** ((&((u) # "__mpz_struct" ->ₛ "_mp_size")) # Int |-> size)
** ((&((u) # "__mpz_struct" ->ₛ "_mp_alloc")) # Int |-> cap)
** ((&((u) # "__mpz_struct" ->ₛ "_mp_d")) # Ptr |-> ptr))
.
Module Type VC_Correct.
Axiom proof_of_gmp_abs_safety_wit_1 : gmp_abs_safety_wit_1.
@ -3810,5 +4019,17 @@ Axiom proof_of_mpz_realloc_partial_solve_wit_9_pure : mpz_realloc_partial_solve_
Axiom proof_of_mpz_realloc_partial_solve_wit_9 : mpz_realloc_partial_solve_wit_9.
Axiom proof_of_mpz_realloc_partial_solve_wit_10_pure : mpz_realloc_partial_solve_wit_10_pure.
Axiom proof_of_mpz_realloc_partial_solve_wit_10 : mpz_realloc_partial_solve_wit_10.
Axiom proof_of_mpz_sgn_safety_wit_1 : mpz_sgn_safety_wit_1.
Axiom proof_of_mpz_sgn_safety_wit_2 : mpz_sgn_safety_wit_2.
Axiom proof_of_mpz_sgn_safety_wit_3 : mpz_sgn_safety_wit_3.
Axiom proof_of_mpz_sgn_safety_wit_4 : mpz_sgn_safety_wit_4.
Axiom proof_of_mpz_sgn_safety_wit_5 : mpz_sgn_safety_wit_5.
Axiom proof_of_mpz_sgn_return_wit_1_1 : mpz_sgn_return_wit_1_1.
Axiom proof_of_mpz_sgn_return_wit_1_2 : mpz_sgn_return_wit_1_2.
Axiom proof_of_mpz_sgn_return_wit_1_3 : mpz_sgn_return_wit_1_3.
Axiom proof_of_mpz_sgn_partial_solve_wit_1 : mpz_sgn_partial_solve_wit_1.
Axiom proof_of_mpz_sgn_partial_solve_wit_2 : mpz_sgn_partial_solve_wit_2.
Axiom proof_of_mpz_sgn_partial_solve_wit_3 : mpz_sgn_partial_solve_wit_3.
Axiom proof_of_mpz_sgn_which_implies_wit_1 : mpz_sgn_which_implies_wit_1.
End VC_Correct.

24
projects/lib/gmp_proof_auto.v
View File

@ -243,3 +243,27 @@ Proof. Admitted.
Lemma proof_of_mpz_realloc_partial_solve_wit_10 : mpz_realloc_partial_solve_wit_10.
Proof. Admitted.
Lemma proof_of_mpz_sgn_safety_wit_1 : mpz_sgn_safety_wit_1.
Proof. Admitted.
Lemma proof_of_mpz_sgn_safety_wit_2 : mpz_sgn_safety_wit_2.
Proof. Admitted.
Lemma proof_of_mpz_sgn_safety_wit_3 : mpz_sgn_safety_wit_3.
Proof. Admitted.
Lemma proof_of_mpz_sgn_safety_wit_4 : mpz_sgn_safety_wit_4.
Proof. Admitted.
Lemma proof_of_mpz_sgn_safety_wit_5 : mpz_sgn_safety_wit_5.
Proof. Admitted.
Lemma proof_of_mpz_sgn_partial_solve_wit_1 : mpz_sgn_partial_solve_wit_1.
Proof. Admitted.
Lemma proof_of_mpz_sgn_partial_solve_wit_2 : mpz_sgn_partial_solve_wit_2.
Proof. Admitted.
Lemma proof_of_mpz_sgn_partial_solve_wit_3 : mpz_sgn_partial_solve_wit_3.
Proof. Admitted.

65
projects/lib/gmp_proof_manual.v
View File

@ -1057,3 +1057,68 @@ Proof.
Intros data.
entailer!.
Qed.
Lemma proof_of_mpz_sgn_return_wit_1_1 : mpz_sgn_return_wit_1_1.
Proof.
pre_process.
Left; Left.
entailer!.
unfold store_Z.
Exists ptr cap size.
Left.
entailer!.
Qed.
Lemma proof_of_mpz_sgn_return_wit_1_2 : mpz_sgn_return_wit_1_2.
Proof.
pre_process.
Right.
unfold mpd_store_Z_compact.
Intros data.
assert (size >= 1). { lia. }
clear H H1.
entailer!.
+ unfold store_Z.
Exists ptr cap size.
Right.
unfold mpd_store_Z_compact.
Exists data.
entailer!.
+ apply list_store_Z_compact_bound in H3.
rewrite <-H4 in *.
nia.
Qed.
Lemma proof_of_mpz_sgn_return_wit_1_3 : mpz_sgn_return_wit_1_3.
Proof.
pre_process.
Left; Right.
unfold store_Z.
Exists ptr cap size.
Right.
unfold mpd_store_Z_compact.
Intros data.
Exists data.
entailer!.
subst.
pose proof (Zlength_nil_inv data ltac:(auto)).
subst.
unfold list_store_Z_compact in H3; destruct H3, H0.
unfold list_to_Z in H.
lia.
Qed.
Lemma proof_of_mpz_sgn_which_implies_wit_1 : mpz_sgn_which_implies_wit_1.
Proof.
pre_process.
unfold store_Z.
Intros ptr cap size.
rewrite orp_sepcon_left.
Split.
+ Right.
Exists ptr cap size.
entailer!.
+ Left.
Exists ptr cap size.
entailer!.
Qed.