From f4db688a3035b1ef81f64b2bfb170f8cf04f9f20 Mon Sep 17 00:00:00 2001 From: xiaoh105 Date: Sat, 21 Jun 2025 22:23:37 +0800 Subject: [PATCH] fix(mpz_realloc): fix minor bugs in proof of mpz_realloc. --- projects/lib/gmp_goal.v | 80 ++++++++--------- projects/lib/gmp_proof_auto.v | 5 +- projects/lib/gmp_proof_manual.v | 147 +++++++++++--------------------- projects/mini-gmp.c | 2 +- projects/mini-gmp.h | 4 +- 5 files changed, 97 insertions(+), 141 deletions(-) diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v index 4a9d0ed..2df150a 100755 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -2826,7 +2826,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) [| (retval > retval_2) |] && [| (retval = (Zabs (old))) |] && [| (cap = 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -2850,7 +2850,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) [| (retval > retval_2) |] && [| (retval = (Zabs (old))) |] && [| (cap = 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -2874,7 +2874,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval_3 [| (retval > retval_2) |] && [| (retval = (Zabs (old))) |] && [| (cap <> 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -2897,7 +2897,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval_3 [| (retval > retval_2) |] && [| (retval = (Zabs (old))) |] && [| (cap <> 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -2920,7 +2920,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval_3 [| (retval <= retval_2) |] && [| (retval = (Zabs (old))) |] && [| (cap <> 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -2954,7 +2954,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval_3 [| (retval <= retval_2) |] && [| (retval = (Zabs (old))) |] && [| (cap <> 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -2988,7 +2988,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) [| (retval <= retval_2) |] && [| (retval = (Zabs (old))) |] && [| (cap = 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3023,7 +3023,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) [| (retval <= retval_2) |] && [| (retval = (Zabs (old))) |] && [| (cap = 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3058,7 +3058,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) [| (retval > retval_2) |] && [| (retval = (Zabs (old))) |] && [| (cap = 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3093,7 +3093,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) [| (retval > retval_2) |] && [| (retval = (Zabs (old))) |] && [| (cap = 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3128,7 +3128,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval_3 [| (retval > retval_2) |] && [| (retval = (Zabs (old))) |] && [| (cap <> 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3162,7 +3162,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval_3 [| (retval > retval_2) |] && [| (retval = (Zabs (old))) |] && [| (cap <> 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3244,7 +3244,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) , Definition mpz_realloc_partial_solve_wit_3_pure := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , [| (cap <> 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3260,13 +3260,13 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , |-- [| (cap >= 0) |] && [| (retval >= cap) |] - && [| ((Zmax (size_pre) (1)) >= cap) |] + && [| ((Z.max (size_pre) (1)) >= cap) |] . Definition mpz_realloc_partial_solve_wit_3_aux := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , [| (cap <> 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3280,9 +3280,9 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , |-- [| (cap >= 0) |] && [| (retval >= cap) |] - && [| ((Zmax (size_pre) (1)) >= cap) |] + && [| ((Z.max (size_pre) (1)) >= cap) |] && [| (cap <> 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3300,7 +3300,7 @@ Definition mpz_realloc_partial_solve_wit_3 := mpz_realloc_partial_solve_wit_3_pu Definition mpz_realloc_partial_solve_wit_4_pure := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , [| (cap <> 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3316,13 +3316,13 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , |-- [| (cap >= 0) |] && [| (retval >= cap) |] - && [| ((Zmax (size_pre) (1)) >= cap) |] + && [| ((Z.max (size_pre) (1)) >= cap) |] . Definition mpz_realloc_partial_solve_wit_4_aux := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , [| (cap <> 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3336,9 +3336,9 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , |-- [| (cap >= 0) |] && [| (retval >= cap) |] - && [| ((Zmax (size_pre) (1)) >= cap) |] + && [| ((Z.max (size_pre) (1)) >= cap) |] && [| (cap <> 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3356,7 +3356,7 @@ Definition mpz_realloc_partial_solve_wit_4 := mpz_realloc_partial_solve_wit_4_pu Definition mpz_realloc_partial_solve_wit_5_pure := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , [| (cap = 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3376,7 +3376,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , Definition mpz_realloc_partial_solve_wit_5_aux := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , [| (cap = 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3390,7 +3390,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , |-- [| (retval >= 0) |] && [| (cap = 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3408,7 +3408,7 @@ Definition mpz_realloc_partial_solve_wit_5 := mpz_realloc_partial_solve_wit_5_pu Definition mpz_realloc_partial_solve_wit_6_pure := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , [| (cap = 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3428,7 +3428,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , Definition mpz_realloc_partial_solve_wit_6_aux := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , [| (cap = 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3442,7 +3442,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) , |-- [| (retval >= 0) |] && [| (cap = 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3460,7 +3460,7 @@ Definition mpz_realloc_partial_solve_wit_6 := mpz_realloc_partial_solve_wit_6_pu Definition mpz_realloc_partial_solve_wit_7_pure := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) (retval: Z) , [| (cap = 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3482,7 +3482,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) Definition mpz_realloc_partial_solve_wit_7_aux := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) (retval_2: Z) , [| (cap = 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3498,7 +3498,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) (r [| (old <= INT_MAX) |] && [| (INT_MIN < old) |] && [| (cap = 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3517,7 +3517,7 @@ Definition mpz_realloc_partial_solve_wit_7 := mpz_realloc_partial_solve_wit_7_pu Definition mpz_realloc_partial_solve_wit_8_pure := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) (retval: Z) , [| (cap = 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3539,7 +3539,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval_2: Z) Definition mpz_realloc_partial_solve_wit_8_aux := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) (retval_2: Z) , [| (cap = 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3555,7 +3555,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (ptr: Z) (retval: Z) (r [| (INT_MIN < old) |] && [| (old <= INT_MAX) |] && [| (cap = 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3574,7 +3574,7 @@ Definition mpz_realloc_partial_solve_wit_8 := mpz_realloc_partial_solve_wit_8_pu Definition mpz_realloc_partial_solve_wit_9_pure := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval: Z) , [| (cap <> 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3595,7 +3595,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval: Definition mpz_realloc_partial_solve_wit_9_aux := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval: Z) (retval_2: Z) , [| (cap <> 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3610,7 +3610,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval: Z) (retval_2: [| (old <= INT_MAX) |] && [| (INT_MIN < old) |] && [| (cap <> 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3628,7 +3628,7 @@ Definition mpz_realloc_partial_solve_wit_9 := mpz_realloc_partial_solve_wit_9_pu Definition mpz_realloc_partial_solve_wit_10_pure := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval: Z) , [| (cap <> 0) |] - && [| (retval_2 = (Zmax (size_pre) (1))) |] + && [| (retval_2 = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3649,7 +3649,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval_2: Z) (retval: Definition mpz_realloc_partial_solve_wit_10_aux := forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval: Z) (retval_2: Z) , [| (cap <> 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] @@ -3664,7 +3664,7 @@ forall (size_pre: Z) (r_pre: Z) (n: Z) (cap: Z) (old: Z) (retval: Z) (retval_2: [| (INT_MIN < old) |] && [| (old <= INT_MAX) |] && [| (cap <> 0) |] - && [| (retval = (Zmax (size_pre) (1))) |] + && [| (retval = (Z.max (size_pre) (1))) |] && [| (size_pre >= cap) |] && [| (size_pre <= 100000000) |] && [| (cap >= 0) |] diff --git a/projects/lib/gmp_proof_auto.v b/projects/lib/gmp_proof_auto.v index 37f0bbb..dd60026 100755 --- a/projects/lib/gmp_proof_auto.v +++ b/projects/lib/gmp_proof_auto.v @@ -15,8 +15,6 @@ 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. @@ -243,4 +241,5 @@ Lemma proof_of_mpz_realloc_partial_solve_wit_9 : mpz_realloc_partial_solve_wit_9 Proof. Admitted. Lemma proof_of_mpz_realloc_partial_solve_wit_10 : mpz_realloc_partial_solve_wit_10. -Proof. Admitted. \ No newline at end of file +Proof. Admitted. + diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index fc2b6fa..0580a17 100755 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -487,7 +487,6 @@ Proof. 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. } @@ -604,7 +603,6 @@ Proof. 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. } @@ -883,9 +881,6 @@ Proof. Right. Exists retval_3 retval_2. entailer!. - unfold Zmax in *. - pose proof (Z.le_max_l size_pre 1). - lia. Qed. Lemma proof_of_mpz_realloc_return_wit_1_2 : mpz_realloc_return_wit_1_2. @@ -894,9 +889,6 @@ Proof. Left. Exists retval_3 retval_2. entailer!. - unfold Zmax in *. - pose proof (Z.le_max_l size_pre 1). - lia. Qed. Lemma proof_of_mpz_realloc_return_wit_1_3 : mpz_realloc_return_wit_1_3. @@ -905,33 +897,25 @@ Proof. Right. Exists retval_3 retval_2. entailer!. - + subst. - unfold mpd_store_Z_compact. - Intros data. - Exists data. - unfold mpd_store_list, store_undef_uint_array_rec. - entailer!. - - assert (Zlength data = 0). { - pose proof (Zlength_nonneg data). - lia. - } - rewrite H8 in *. - simpl. - entailer!. - pose proof (Zlength_nil_inv data H8). - repeat subst. - unfold store_uint_array, store_array; simpl; entailer!. - unfold store_undef_uint_array, store_undef_array. - rewrite Z.sub_0_r. - reflexivity. - - unfold Zmax in *. - assert (size_pre < 1 \/ size_pre >= 1). { lia. } - destruct H8. - * rewrite (Z.max_r size_pre 1 ltac:(lia)); lia. - * rewrite (Z.max_l size_pre 1 ltac:(lia)); lia. - + pose proof (Z.le_max_l size_pre 1). - unfold Zmax in *. + subst. + unfold mpd_store_Z_compact. + Intros data. + Exists data. + unfold mpd_store_list, store_undef_uint_array_rec. + entailer!. + assert (Zlength data = 0). { + pose proof (Zlength_nonneg data). lia. + } + rewrite H10 in *. + simpl. + entailer!. + pose proof (Zlength_nil_inv data H10). + repeat subst. + unfold store_uint_array, store_array; simpl; entailer!. + unfold store_undef_uint_array, store_undef_array. + rewrite Z.sub_0_r. + reflexivity. Qed. Lemma proof_of_mpz_realloc_return_wit_1_4 : mpz_realloc_return_wit_1_4. @@ -940,23 +924,20 @@ Proof. Left. Exists retval_3 retval_2. entailer!. - + subst. - unfold mpd_store_Z_compact, mpd_store_list. - Intros data. - Exists data. - assert (Zlength data = 0). { - pose proof (Zlength_nonneg data). - lia. - } - rewrite H8 in *; clear H2. - pose proof (Zlength_nil_inv data H8). - rewrite H2 in *; clear H2 H8. - unfold store_uint_array, store_array. - simpl. - entailer!. - + pose proof (Z.le_max_l size_pre 1). - unfold Zmax in *. + subst. + unfold mpd_store_Z_compact, mpd_store_list. + Intros data. + Exists data. + assert (Zlength data = 0). { + pose proof (Zlength_nonneg data). lia. + } + rewrite H10 in *; clear H2. + pose proof (Zlength_nil_inv data H10). + rewrite H2 in *; clear H2 H10. + unfold store_uint_array, store_array. + simpl. + entailer!. Qed. Lemma proof_of_mpz_realloc_return_wit_1_5 : mpz_realloc_return_wit_1_5. @@ -965,16 +946,13 @@ Proof. Left. Exists retval_3 retval_2. entailer!. - + subst. - unfold mpd_store_Z_compact, mpd_store_list. - Intros data. - Exists data. - unfold store_uint_array, store_array. - simpl. - entailer!. - + pose proof (Z.le_max_l size_pre 1). - unfold Zmax in *. - lia. + subst. + unfold mpd_store_Z_compact, mpd_store_list. + Intros data. + Exists data. + unfold store_uint_array, store_array. + simpl. + entailer!. Qed. Lemma proof_of_mpz_realloc_return_wit_1_6 : mpz_realloc_return_wit_1_6. @@ -984,29 +962,20 @@ Proof. Exists retval_3 retval_2. subst. entailer!. - + unfold mpd_store_Z_compact, mpd_store_list. - Intros data; Exists data. - unfold store_uint_array, store_array. - assert (Zlength data = 0). { - pose proof (Zlength_nonneg data). - lia. - } - rewrite H8 in *; clear H2. - pose proof (Zlength_nil_inv data H8). - rewrite H2 in *; clear H2 H8. - unfold store_undef_uint_array, store_undef_uint_array_rec, store_undef_array. - subst. - simpl. - entailer!. - - rewrite Z.sub_0_r. - entailer!. - - pose proof (Z.le_max_r size_pre 1). - simpl in H. - unfold Zmax in *. - lia. - + unfold Zmax in *. - pose proof (Z.le_max_l size_pre 1). + unfold mpd_store_Z_compact, mpd_store_list. + Intros data; Exists data. + unfold store_uint_array, store_array. + assert (Zlength data = 0). { + pose proof (Zlength_nonneg data). lia. + } + rewrite H10 in *; clear H2. + pose proof (Zlength_nil_inv data H10). + rewrite H2 in *; clear H2 H10. + unfold store_undef_uint_array, store_undef_uint_array_rec, store_undef_array. + subst. + simpl. + entailer!. Qed. Lemma proof_of_mpz_realloc_return_wit_1_7 : mpz_realloc_return_wit_1_7. @@ -1015,7 +984,6 @@ Proof. Left. Exists retval_3 retval_2. subst. - unfold Zmax in *. rewrite (Z.abs_neq old ltac:(lia)) in H. pose proof (Z.le_max_l size_pre 1). unfold mpd_store_Z_compact. @@ -1030,7 +998,6 @@ Proof. Right. Exists retval_3 retval_2. subst. - unfold Zmax in *. rewrite (Z.abs_eq old ltac:(lia)) in H. pose proof (Z.le_max_l size_pre 1). unfold mpd_store_Z_compact. @@ -1042,33 +1009,21 @@ Qed. Lemma proof_of_mpz_realloc_partial_solve_wit_3_pure : mpz_realloc_partial_solve_wit_3_pure. Proof. pre_process. - unfold Zmax in *. - pose proof (Z.le_max_l size_pre 1). - entailer!. Qed. Lemma proof_of_mpz_realloc_partial_solve_wit_4_pure : mpz_realloc_partial_solve_wit_4_pure. Proof. pre_process. - unfold Zmax in *. - pose proof (Z.le_max_l size_pre 1). - entailer!. Qed. Lemma proof_of_mpz_realloc_partial_solve_wit_5_pure : mpz_realloc_partial_solve_wit_5_pure. Proof. pre_process. - unfold Zmax in *. - pose proof (Z.le_max_l size_pre 1). - entailer!. Qed. Lemma proof_of_mpz_realloc_partial_solve_wit_6_pure : mpz_realloc_partial_solve_wit_6_pure. Proof. pre_process. - unfold Zmax in *. - pose proof (Z.le_max_l size_pre 1). - entailer!. Qed. Lemma proof_of_mpz_realloc_partial_solve_wit_7_pure : mpz_realloc_partial_solve_wit_7_pure. diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index e6a2d2b..43b2ab9 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 58a27c5..08af83a 100755 --- a/projects/mini-gmp.h +++ b/projects/mini-gmp.h @@ -1,6 +1,7 @@ /*@ Extern Coq (Zabs : Z -> Z) - (Zmax : Z -> Z -> 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) @@ -8,6 +9,7 @@ (list_store_Z : list Z -> Z -> Prop) (list_store_Z_compact: list Z -> Z -> Prop) (last: list Z -> Z -> Z) + (UINT_MOD: Z) */ typedef struct __mpz_struct