From e7bc194ec78b7f7fb928c75308aa75bbdb347bd3 Mon Sep 17 00:00:00 2001 From: xiaoh105 Date: Tue, 3 Jun 2025 17:52:15 +0800 Subject: [PATCH 1/6] feat: Add list_store_Z_nth lemma. --- projects/lib/gmp_number.v | 63 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 62 insertions(+), 1 deletion(-) diff --git a/projects/lib/gmp_number.v b/projects/lib/gmp_number.v index cb07e65..c06b840 100755 --- a/projects/lib/gmp_number.v +++ b/projects/lib/gmp_number.v @@ -371,6 +371,67 @@ Proof. - pose proof (Zlength_nonneg l1); lia. Qed. +Lemma list_store_Z_nth: forall (l: list Z) (n: Z) (i: Z), + 0 <= i < Zlength l -> + list_store_Z l n -> + Znth i l 0 = (n / (UINT_MOD ^ i)) mod UINT_MOD. +Proof. + intros. + revert n i H H0. + induction l; intros. + + rewrite Zlength_nil in H. + lia. + + rewrite Zlength_cons in H; unfold Z.succ in H. + assert (i = 0 \/ i > 0). { lia. } + destruct H1. + - pose proof (list_store_Z_split [a] l n). + assert (a :: l = app [a] l). { auto. } + rewrite <-H3 in H2; clear H3. + specialize (H2 H0); destruct H2. + unfold list_store_Z, list_to_Z in H2. + unfold Zlength, Zlength_aux, Z.succ in H2. + destruct H2. + rewrite (Aux.Zpow_add_1 UINT_MOD 0) in H2; try lia. + rewrite Z.pow_0_r, Z.mul_1_l in H2. + simpl in H2. + rewrite H1; rewrite Znth0_cons. + rewrite Z.pow_0_r, Z.div_1_r. + lia. + - rewrite Znth_cons; [ | lia ]. + unfold list_store_Z in H0; destruct H0. + simpl in H0. + simpl in H2. + unfold list_store_Z in IHl. + assert (list_to_Z l = (n - a) / UINT_MOD /\ list_within_bound l). { + rewrite (Z.div_unique_exact (n - a) UINT_MOD (list_to_Z l)); try lia; try tauto. + } + specialize (IHl ((n - a) / UINT_MOD) (i - 1) ltac:(lia) H3). + rewrite IHl. + assert ((n - a) / UINT_MOD / (UINT_MOD ^ (i - 1)) = (n - a) / (UINT_MOD ^ 1 * UINT_MOD ^ (i - 1))). { + rewrite Zdiv_Zdiv; try lia. + rewrite Z.pow_1_r. + reflexivity. + } + rewrite H4. + rewrite <-Z.pow_add_r; try lia. + assert (n / UINT_MOD ^ i = (n - a) / UINT_MOD ^ i). { + assert (i = 1 + (i - 1)). { lia. } + rewrite H5. + rewrite (Z.pow_add_r UINT_MOD 1 (i - 1)); try lia. + repeat rewrite <-Zdiv_Zdiv; try lia. + repeat rewrite Z.pow_1_r. + rewrite <-(Zdiv_unique_full n UINT_MOD (list_to_Z l) a); try lia. + + destruct H3. + rewrite <-H3. + reflexivity. + + unfold Remainder; lia. + } + rewrite H5. + assert (1 + (i - 1) = i). { lia. } + rewrite H6. + reflexivity. +Qed. + End Internal. Record bigint_ent: Type := { @@ -379,7 +440,7 @@ Record bigint_ent: Type := { sign: Prop; }. -Definition store_bigint_ent (x: addr) (n: bigint_ent): Assertion := +Definition store_bigint_ent (x: addr) (n: bigint_ent): Asrtion := EX size, &(x # "__mpz_struct" ->ₛ "_mp_size") # Int |-> size && ([| size < 0 |] && [| sign n |] && [| size = -Zlength (data n) |] || From 1873d949ceab6684b0f11265234bd3a2e3eee257 Mon Sep 17 00:00:00 2001 From: xiaoh105 Date: Sat, 7 Jun 2025 15:23:11 +0800 Subject: [PATCH 2/6] Add annotations to gmp.c --- Makefile | 23 ++-- projects/int_array.strategies | 126 +++++++++++++++++ projects/int_array_def.h | 18 +++ projects/lib/{gmp_aux.v => GmpAux.v} | 45 +++++- projects/lib/{gmp_number.v => GmpNumber.v} | 89 +----------- projects/mini-gmp.c | 151 ++++++++++++++------- projects/mini-gmp.h | 45 +++--- projects/uint_array.strategies | 126 +++++++++++++++++ 8 files changed, 448 insertions(+), 175 deletions(-) create mode 100644 projects/int_array.strategies create mode 100644 projects/int_array_def.h rename projects/lib/{gmp_aux.v => GmpAux.v} (65%) rename projects/lib/{gmp_number.v => GmpNumber.v} (83%) create mode 100644 projects/uint_array.strategies diff --git a/Makefile b/Makefile index fec44ab..54672ff 100755 --- a/Makefile +++ b/Makefile @@ -15,7 +15,9 @@ SETS_FLAG = -R $(SETS_DIR) SetsClass COMPCERT_FLAG = -R $(COMPCERT_DIR) compcert.lib -DEP_FLAG = -R $(PV_DIR) PV -R $(SETS_DIR) SetsClass -R $(COMPCERT_DIR) compcert.lib +GMP_FLAG = $(shell grep -E '^-([RQ])' _CoqProject) + +DEP_FLAG = $(GMP_FLAG) SETS_FILE_NAMES = \ SetsClass.v SetsDomain.v SetElement.v RelsDomain.v SetElementProperties.v SetProd.v SetsClass_AxiomFree.v SetsDomain_Classic.v @@ -35,21 +37,18 @@ PV_FILE_NAMES = \ PV_FILES=$(PV_FILE_NAMES:%.v=$(PV_DIR)/%.v) +GMP_FILES = ./projects/lib/GmpAux.v ./projects/lib/GmpNumber.v + FILES = $(PV_FILES) \ - $(SETS_FILES) \ - $(COMPCERT_FILES) - -$(SETS_FILES:%.v=%.vo): %.vo: %.v - @echo COQC $< - @$(COQC) $(SETS_FLAG) $< - -$(COMPCERT_FILES:%.v=%.vo): %.vo: %.v - @echo COQC $< - @$(COQC) $(COMPCERT_FLAG) $< + $(GMP_FILES) $(PV_FILES:%.v=%.vo): %.vo: %.v @echo COQC $( Z) + (sublist : {A} -> Z -> Z -> list A -> list A) + (store_int_array : Z -> Z -> list Z -> Assertion) + (store_uint_array : Z -> Z -> list Z -> Assertion)(store_uint_array : Z -> Z -> list Z -> Assertion) + (store_int_array_missing_i_rec: Z -> Z -> Z -> Z -> list Z -> Assertion) + (store_uint_array_missing_i_rec: Z -> Z -> Z -> Z -> list Z -> Assertion) + (store_array_box: Z -> Z -> list Z -> Assertion) + (store_array_box_array: Z -> list Z -> Assertion) + (store_int_array_rec: Z -> Z -> Z -> list Z -> Assertion) + (store_uint_array_rec: Z -> Z -> Z -> list Z -> Assertion) + (Znth: {A} -> Z -> list A -> A -> A) + (replace_Znth: {A} -> Z -> A -> list A -> list A) + (zeros: Z -> list Z) +*/ + +/*@ include strategies "int_array.strategies" */ + +/*@ include strategies "uint_array.strategies" */ \ No newline at end of file diff --git a/projects/lib/gmp_aux.v b/projects/lib/GmpAux.v similarity index 65% rename from projects/lib/gmp_aux.v rename to projects/lib/GmpAux.v index 54a2317..4701085 100755 --- a/projects/lib/gmp_aux.v +++ b/projects/lib/GmpAux.v @@ -21,6 +21,10 @@ Local Open Scope sac. Module Aux. +Lemma Z_of_nat_succ: forall (n: nat), + Z.of_nat (S n) = Z.of_nat n + 1. +Proof. lia. Qed. + Lemma Zpow_add_1: forall (a b: Z), a >= 0 -> b >= 0 -> a ^ (b + 1) = a ^ b * a. @@ -29,8 +33,29 @@ Proof. rewrite (Z.pow_add_r a b 1); lia. Qed. -Lemma Z_of_nat_succ: forall (n: nat), - Z.of_nat (S n) = Z.of_nat n + 1. +Lemma Zmul_mod_cancel: forall (n a b: Z), + n >= 0 -> a > 0 -> b >= 0 -> + (n * a) mod (a ^ (b + 1)) = a * (n mod (a ^ b)). +Proof. + intros. + pose proof (Z_div_mod_eq_full n (a ^ b)). + pose proof (Z.mod_bound_pos n (a ^ b) ltac:(lia) ltac:(nia)). + remember (n / a ^ b) as q eqn:Hq. + remember (n mod a ^ b) as rem eqn:Hrem. + rewrite H2. + rewrite Z.mul_add_distr_r. + rewrite (Z.mul_comm (a ^ b) q); rewrite <-Z.mul_assoc. + rewrite <-Zpow_add_1; try lia. + assert (0 <= rem * a < a ^ (b + 1)). { + rewrite Zpow_add_1; try lia. + nia. + } + rewrite <-(Zmod_unique_full (q * a ^ (b + 1) + rem * a) (a ^ (b + 1)) q (rem * a)). + + lia. + + unfold Remainder. + lia. + + lia. +Qed. Lemma Zdiv_mod_pow: forall (n a b: Z), a > 0 -> b >= 0 -> n >= 0 -> @@ -59,5 +84,21 @@ Proof. exists q. lia. Qed. + +Lemma list_app_cons: forall (l1 l2: list Z) (a: Z), + app l1 (a :: l2) = app (app l1 (a :: nil)) l2. +Proof. + intros. + revert a l2. + induction l1. + + intros. + rewrite app_nil_l. + reflexivity. + + intros. + simpl in *. + specialize (IHl1 a0 l2). + rewrite IHl1. + reflexivity. +Qed. End Aux. \ No newline at end of file diff --git a/projects/lib/gmp_number.v b/projects/lib/GmpNumber.v similarity index 83% rename from projects/lib/gmp_number.v rename to projects/lib/GmpNumber.v index c06b840..7104900 100755 --- a/projects/lib/gmp_number.v +++ b/projects/lib/GmpNumber.v @@ -9,6 +9,7 @@ Require Import String. From AUXLib Require Import int_auto Axioms Feq Idents List_lemma VMap. Require Import SetsClass.SetsClass. Import SetsNotation. From SimpleC.SL Require Import CommonAssertion Mem SeparationLogic IntLib. +Require Import GmpLib.GmpAux. Require Import Logic.LogicGenerator.demo932.Interface. Local Open Scope Z_scope. Local Open Scope sets. @@ -21,95 +22,11 @@ Local Open Scope sac. Notation "'UINT_MOD'" := (4294967296). -Module Aux. - -Lemma Z_of_nat_succ: forall (n: nat), - Z.of_nat (S n) = Z.of_nat n + 1. -Proof. lia. Qed. - -Lemma Zpow_add_1: forall (a b: Z), - a >= 0 -> b >= 0 -> - a ^ (b + 1) = a ^ b * a. -Proof. - intros. - rewrite (Z.pow_add_r a b 1); lia. -Qed. - -Lemma Zmul_mod_cancel: forall (n a b: Z), - n >= 0 -> a > 0 -> b >= 0 -> - (n * a) mod (a ^ (b + 1)) = a * (n mod (a ^ b)). -Proof. - intros. - pose proof (Z_div_mod_eq_full n (a ^ b)). - pose proof (Z.mod_bound_pos n (a ^ b) ltac:(lia) ltac:(nia)). - remember (n / a ^ b) as q eqn:Hq. - remember (n mod a ^ b) as rem eqn:Hrem. - rewrite H2. - rewrite Z.mul_add_distr_r. - rewrite (Z.mul_comm (a ^ b) q); rewrite <-Z.mul_assoc. - rewrite <-Zpow_add_1; try lia. - assert (0 <= rem * a < a ^ (b + 1)). { - rewrite Zpow_add_1; try lia. - nia. - } - rewrite <-(Zmod_unique_full (q * a ^ (b + 1) + rem * a) (a ^ (b + 1)) q (rem * a)). - + lia. - + unfold Remainder. - lia. - + lia. -Qed. - -Lemma Zdiv_mod_pow: forall (n a b: Z), - a > 0 -> b >= 0 -> n >= 0 -> - (n / a) mod (a ^ b) = (n mod (a ^ (b + 1))) / a. -Proof. - intros. - pose proof (Z_div_mod_eq_full n (a ^ (b + 1))). - remember (n / (a ^ (b + 1))) as q eqn:Hq. - remember (n mod a ^ (b + 1)) as rem eqn:Hrem. - assert (n / a = a ^ b * q + rem / a). { - rewrite H2. - rewrite Zpow_add_1; try lia. - pose proof (Z_div_plus_full_l (a ^ b * q) a rem ltac:(lia)). - assert (a ^ b * q * a + rem = a ^ b * a * q + rem). { lia. } - rewrite H4 in H3. - tauto. - } - apply Znumtheory.Zdivide_mod_minus. - + pose proof (Z.mod_bound_pos n (a ^ (b + 1)) ltac:(lia) (Z.pow_pos_nonneg a (b + 1) ltac:(lia) ltac:(lia))). - rewrite <-Hrem in H4. - rewrite Zpow_add_1 in H4; try lia. - pose proof (Z.div_lt_upper_bound rem a (a ^ b) ltac:(lia) ltac:(lia)). - split; try lia. - apply (Z_div_pos rem a ltac:(lia) ltac:(lia)). - + unfold Z.divide. - exists q. - lia. -Qed. - -Lemma list_app_cons: forall (l1 l2: list Z) (a: Z), - app l1 (a :: l2) = app (app l1 (a :: nil)) l2. -Proof. - intros. - revert a l2. - induction l1. - + intros. - rewrite app_nil_l. - reflexivity. - + intros. - simpl in *. - specialize (IHl1 a0 l2). - rewrite IHl1. - reflexivity. -Qed. - -End Aux. - Module Internal. Definition mpd_store_list (ptr: addr) (data: list Z) (cap: Z): Assertion := [| Zlength data <= cap |] && - store_uint_array ptr (Zlength data) data && + store_uint_array ptr (Zlength data) data ** store_undef_uint_array_rec ptr ((Zlength data) + 1) cap. Fixpoint list_to_Z (data: list Z): Z := @@ -440,7 +357,7 @@ Record bigint_ent: Type := { sign: Prop; }. -Definition store_bigint_ent (x: addr) (n: bigint_ent): Asrtion := +Definition store_bigint_ent (x: addr) (n: bigint_ent): Assertion := EX size, &(x # "__mpz_struct" ->ₛ "_mp_size") # Int |-> size && ([| size < 0 |] && [| sign n |] && [| size = -Zlength (data n) |] || diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 1d03734..3dc0c43 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -1,14 +1,35 @@ #include "mini-gmp.h" +#include "verification_stdlib.h" +#include "verification_list.h" +#include "int_array_def.h" -mp_size_t gmp_abs(mp_size_t x) { +int gmp_abs(int x) +/*@ + Require emp + Ensure __return == Zabs(x) +*/ +{ return x >= 0 ? x : -x; } -mp_size_t gmp_max(mp_size_t a, mp_size_t b) { +int gmp_max(int a, int b) +/*@ + Require emp + Ensure __return == Zmax(a, b) +*/ +{ return a > b ? a : b; } -int gmp_cmp(mp_size_t a, mp_size_t b) { +int gmp_cmp(int a, int b) +/*@ + Require emp + Ensure + a > b && __return == 1 || + a == b && __return == 0 || + a < b && __return == -1 +*/ +{ return (a > b) - (a < b); } @@ -16,16 +37,42 @@ int gmp_cmp(mp_size_t a, mp_size_t b) { /* 从 低地址向高地址 顺序复制 */ void -mpn_copyi (mp_ptr d, mp_srcptr s, mp_size_t n) +mpn_copyi (unsigned int *d, unsigned int *s, int n) +/*@ + With val data cap1 cap2 + Require + mpd_store_Z(s, val, n, cap1) * + store_uint_array(d, cap2, data) + Ensure + mpd_store_Z(s, val, n, cap1) * + mpd_store_Z(d, val, n, cap2) +*/ { - mp_size_t i; + /* + mpd_store_Z(s, val, n, cap1) + which implies + exists l, + store_uint_array(s, n, l) ** + store_undef + */ + int i; for (i = 0; i < n; i++) d[i] = s[i]; } /* 大于返回1，小于返回-1，等于返回0 */ int -mpn_cmp (mp_srcptr ap, mp_srcptr bp, mp_size_t n) +mpn_cmp (unsigned int *ap, unsigned int *bp, int n) +/*@ + With cap1 cap2 val1 val2 + Require + mpd_store_Z(ap, val1, n, cap1) ** + mpd_store_Z(bp, val2, n, cap2) + Ensure + val1 > val2 && __return == 1 || + val1 == val2 && __return == 0 || + val1 < val2 && __return == -1 +*/ { while (--n >= 0) { @@ -37,7 +84,7 @@ mpn_cmp (mp_srcptr ap, mp_srcptr bp, mp_size_t n) /*处理位数不同的情况*/ static int -mpn_cmp4 (mp_srcptr ap, mp_size_t an, mp_srcptr bp, mp_size_t bn) +mpn_cmp4 (unsigned int *ap, int an, unsigned int *bp, int bn) { if (an != bn) return an < bn ? -1 : 1; @@ -46,8 +93,8 @@ mpn_cmp4 (mp_srcptr ap, mp_size_t an, mp_srcptr bp, mp_size_t bn) } /*返回非0的位数*/ -static mp_size_t -mpn_normalized_size (mp_srcptr xp, mp_size_t n) +static int +mpn_normalized_size (unsigned int *xp, int n) { while (n > 0 && xp[n-1] == 0) --n; @@ -55,15 +102,15 @@ mpn_normalized_size (mp_srcptr xp, mp_size_t n) } /* 多精度数ap 加上单精度数b，返回最后产生的进位 */ -mp_limb_t -mpn_add_1 (mp_ptr rp, mp_srcptr ap, mp_size_t n, mp_limb_t b) +unsigned int +mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) { - mp_size_t i; + int i; //assert (n > 0); i = 0; do { - mp_limb_t r = ap[i] + b; + unsigned int r = ap[i] + b; /* Carry out */ b = (r < b); rp[i] = r; @@ -74,15 +121,15 @@ mpn_add_1 (mp_ptr rp, mp_srcptr ap, mp_size_t n, mp_limb_t b) } /* 位数相同的多精度数ap 加上多精度数bp，返回最后产生的进位 */ -mp_limb_t -mpn_add_n (mp_ptr rp, mp_srcptr ap, mp_srcptr bp, mp_size_t n) +unsigned int +mpn_add_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n) { - mp_size_t i; - mp_limb_t cy; + int i; + unsigned int cy; for (i = 0, cy = 0; i < n; i++) { - mp_limb_t a, b, r; + unsigned int a, b, r; a = ap[i]; b = bp[i]; r = a + cy; cy = (r < cy); @@ -94,10 +141,10 @@ mpn_add_n (mp_ptr rp, mp_srcptr ap, mp_srcptr bp, mp_size_t n) } /*不同位数的多精度数相加，返回最后的进位*/ -mp_limb_t -mpn_add (mp_ptr rp, mp_srcptr ap, mp_size_t an, mp_srcptr bp, mp_size_t bn) +unsigned int +mpn_add (unsigned int *rp, unsigned int *ap, int an, unsigned int *bp, int bn) { - mp_limb_t cy; + unsigned int cy; //assert (an >= bn); cy = mpn_add_n (rp, ap, bp, bn); if (an > bn) @@ -105,17 +152,17 @@ mpn_add (mp_ptr rp, mp_srcptr ap, mp_size_t an, mp_srcptr bp, mp_size_t bn) return cy; } -mp_limb_t -mpn_sub_1 (mp_ptr rp, mp_srcptr ap, mp_size_t n, mp_limb_t b) +unsigned int +mpn_sub_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) { - mp_size_t i; + int i; //assert (n > 0); i = 0; do { - mp_limb_t a = ap[i]; + unsigned int a = ap[i]; /* Carry out */ - mp_limb_t cy = a < b; + unsigned int cy = a < b; rp[i] = a - b; b = cy; } @@ -124,15 +171,15 @@ mpn_sub_1 (mp_ptr rp, mp_srcptr ap, mp_size_t n, mp_limb_t b) return b; } -mp_limb_t -mpn_sub_n (mp_ptr rp, mp_srcptr ap, mp_srcptr bp, mp_size_t n) +unsigned int +mpn_sub_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n) { - mp_size_t i; - mp_limb_t cy; + int i; + unsigned int cy; for (i = 0, cy = 0; i < n; i++) { - mp_limb_t a, b; + unsigned int a, b; a = ap[i]; b = bp[i]; b += cy; cy = (b < cy); @@ -142,10 +189,10 @@ mpn_sub_n (mp_ptr rp, mp_srcptr ap, mp_srcptr bp, mp_size_t n) return cy; } -mp_limb_t -mpn_sub (mp_ptr rp, mp_srcptr ap, mp_size_t an, mp_srcptr bp, mp_size_t bn) +unsigned int +mpn_sub (unsigned int *rp, unsigned int *ap, int an, unsigned int *bp, int bn) { - mp_limb_t cy; + unsigned int cy; //assert (an >= bn); cy = mpn_sub_n (rp, ap, bp, bn); if (an > bn) @@ -162,8 +209,8 @@ mpz_clear (mpz_t r) gmp_free_limbs (r->_mp_d, r->_mp_alloc); } -static mp_ptr -mpz_realloc (mpz_t r, mp_size_t size) +static unsigned int * +mpz_realloc (mpz_t r, int size) { size = gmp_max (size, 1); @@ -180,7 +227,7 @@ mpz_realloc (mpz_t r, mp_size_t size) } /* Realloc for an mpz_t WHAT if it has less than NEEDED limbs. */ -mp_ptr mrz_realloc_if(mpz_t z,mp_size_t n) { +unsigned int *mrz_realloc_if(mpz_t z,int n) { return n > z->_mp_alloc ? mpz_realloc(z, n) : z->_mp_d; } @@ -194,25 +241,25 @@ mpz_sgn (const mpz_t u) void mpz_swap (mpz_t u, mpz_t v) { - mp_size_t_swap (u->_mp_alloc, v->_mp_alloc); - mp_ptr_swap(u->_mp_d, v->_mp_d); - mp_size_t_swap (u->_mp_size, v->_mp_size); + int_swap (u->_mp_alloc, v->_mp_alloc); + unsigned int *_swap(u->_mp_d, v->_mp_d); + int_swap (u->_mp_size, v->_mp_size); } /* MPZ addition and subtraction */ -static mp_size_t +static int mpz_abs_add (mpz_t r, const mpz_t a, const mpz_t b) { - mp_size_t an = gmp_abs (a->_mp_size); - mp_size_t bn = gmp_abs (b->_mp_size); - mp_ptr rp; - mp_limb_t cy; + int an = gmp_abs (a->_mp_size); + int bn = gmp_abs (b->_mp_size); + unsigned int *rp; + unsigned int cy; if (an < bn) { mpz_srcptr_swap (a, b); - mp_size_t_swap (an, bn); + int_swap (an, bn); } rp = mrz_realloc_if (r, an + 1); @@ -223,13 +270,13 @@ mpz_abs_add (mpz_t r, const mpz_t a, const mpz_t b) return an + cy; } -static mp_size_t +static int mpz_abs_sub (mpz_t r, const mpz_t a, const mpz_t b) { - mp_size_t an = gmp_abs (a->_mp_size); - mp_size_t bn = gmp_abs (b->_mp_size); + int an = gmp_abs (a->_mp_size); + int bn = gmp_abs (b->_mp_size); int cmp; - mp_ptr rp; + unsigned int *rp; cmp = mpn_cmp4 (a->_mp_d, an, b->_mp_d, bn); if (cmp > 0) @@ -251,7 +298,7 @@ mpz_abs_sub (mpz_t r, const mpz_t a, const mpz_t b) void mpz_add (mpz_t r, const mpz_t a, const mpz_t b) { - mp_size_t rn; + int rn; if ( (a->_mp_size ^ b->_mp_size) >= 0) rn = mpz_abs_add (r, a, b); @@ -264,7 +311,7 @@ mpz_add (mpz_t r, const mpz_t a, const mpz_t b) void mpz_sub (mpz_t r, const mpz_t a, const mpz_t b) { - mp_size_t rn; + int rn; if ( (a->_mp_size ^ b->_mp_size) >= 0) rn = mpz_abs_sub (r, a, b); diff --git a/projects/mini-gmp.h b/projects/mini-gmp.h index ba16619..4b50d45 100755 --- a/projects/mini-gmp.h +++ b/projects/mini-gmp.h @@ -1,10 +1,3 @@ -typedef unsigned long mp_limb_t; -typedef long mp_size_t; -typedef unsigned long mp_bitcnt_t; - -typedef mp_limb_t *mp_ptr; -typedef const mp_limb_t *mp_srcptr; - typedef struct { int _mp_alloc; /* Number of *limbs* allocated and pointed @@ -12,7 +5,7 @@ typedef struct int _mp_size; /* abs(_mp_size) is the number of limbs the last field points to. If _mp_size is negative this is a negative number. */ - mp_limb_t *_mp_d; /* Pointer to the limbs. */ + unsigned int *_mp_d; /* Pointer to the limbs. */ } __mpz_struct; /* mpz_t is an array type that contains a single element of __mpz_struct, acting as a reference. */ @@ -23,35 +16,35 @@ typedef const __mpz_struct *mpz_srcptr; /* BEGIN Given Functions */ /* Swap functions. */ -void mp_size_t_swap(mp_size_t x, mp_size_t y); +void int_swap(int x, int y); -void mp_ptr_swap(mp_ptr x, mp_ptr y); +void mp_ptr_swap(unsigned int *x, unsigned int *y); void mpz_srcptr_swap(mpz_srcptr x, mpz_srcptr y); /* Memory allocation functions. */ -static mp_ptr -gmp_alloc_limbs (mp_size_t size); +static unsigned int * +gmp_alloc_limbs (int size); -static mp_ptr -gmp_realloc_limbs (mp_ptr old, mp_size_t old_size, mp_size_t size); +static unsigned int * +gmp_realloc_limbs (unsigned int *old, int old_size, int size); static void -gmp_free_limbs (mp_ptr old, mp_size_t size); +gmp_free_limbs (unsigned int *old, int size); /* END Given Functions */ -void mpn_copyi (mp_ptr, mp_srcptr, mp_size_t); +void mpn_copyi (unsigned int *d, unsigned int *s, int n); -int mpn_cmp (mp_srcptr, mp_srcptr, mp_size_t); +int mpn_cmp (unsigned int *, unsigned int *, int); -mp_limb_t mpn_add_1 (mp_ptr, mp_srcptr, mp_size_t, mp_limb_t); -mp_limb_t mpn_add_n (mp_ptr, mp_srcptr, mp_srcptr, mp_size_t); -mp_limb_t mpn_add (mp_ptr, mp_srcptr, mp_size_t, mp_srcptr, mp_size_t); +unsigned int mpn_add_1 (unsigned int *, unsigned int *, int, unsigned int); +unsigned int mpn_add_n (unsigned int *, unsigned int *, unsigned int *, int); +unsigned int mpn_add (unsigned int *, unsigned int *, int, unsigned int *, int); -mp_limb_t mpn_sub_1 (mp_ptr, mp_srcptr, mp_size_t, mp_limb_t); -mp_limb_t mpn_sub_n (mp_ptr, mp_srcptr, mp_srcptr, mp_size_t); -mp_limb_t mpn_sub (mp_ptr, mp_srcptr, mp_size_t, mp_srcptr, mp_size_t); +unsigned int mpn_sub_1 (unsigned int *, unsigned int *, int, unsigned int); +unsigned int mpn_sub_n (unsigned int *, unsigned int *, unsigned int *, int); +unsigned int mpn_sub (unsigned int *, unsigned int *, int, unsigned int *, int); void mpz_clear (mpz_t); @@ -64,3 +57,9 @@ void mpz_add (mpz_t, const mpz_t, const mpz_t); void mpz_sub (mpz_t, const mpz_t, const mpz_t); void mpz_set (mpz_t, const mpz_t); + +/*@ + Extern Coq (Zabs: Z -> Z) + (Zmax: Z -> Z -> Z) + (mpd_store_Z: Z -> Z -> Z -> Z -> Assertion) +*/ \ No newline at end of file diff --git a/projects/uint_array.strategies b/projects/uint_array.strategies new file mode 100644 index 0000000..a8e3822 --- /dev/null +++ b/projects/uint_array.strategies @@ -0,0 +1,126 @@ +//test curent rules +//max rule id:30 + +#include "int_array_def.h" + +#include "verification_list.h" +#include "verification_stdlib.h" + +id : 1 +priority : core(1) +left : store_uint_array(?p, ?n, ?l) at 0 +right : data_at(?p + (?i * sizeof(I32)), I32, ?v) at 1 +check : infer(0 <= i); + infer(i < n); +action : right_erase(1); + left_erase(0); + left_add(store_uint_array_missing_i_rec(p, i, 0, n, l)); + right_add(v == l[i]); + +id : 2 +priority : post(1) +left : store_uint_array_missing_i_rec(?p, ?i, 0, ?n, ?l) at 0 + data_at(p + i * sizeof(I32), I32, l[i]) at 1 +check : infer(0 <= i); + infer(i < n); +action : left_erase(1); + left_erase(0); + left_add(store_uint_array(p, n, l)); + +id : 3 +priority : post(3) +left : store_uint_array_missing_i_rec(?p, ?i, 0, ?n, ?l) at 0 + data_at(p + i * sizeof(I32), I32, ?v) at 1 +check : infer(0 <= i); + infer(i < n); +action : left_erase(1); + left_erase(0); + left_add(store_uint_array(p, n, replace_Znth{Z}(i, v, l))); + +id : 4 +priority : core(1) +left : store_uint_array(?p, ?n, ?l1) at 0 +right : store_uint_array(p, n, ?l2) at 1 +action : right_erase(1); + left_erase(0); + right_add(l1 == l2); + +id : 5 +priority : core(1) +left : store_uint_array_missing_i_rec(?p, ?i, ?v, ?n, ?l) at 0 +right : store_uint_array_missing_i_rec(p, i, v, n, l) at 1 +action : left_erase(0); + right_erase(1); + + +id : 6 +priority : core(1) +left : store_uint_array_rec(?p, ?x, ?y, ?l1) at 0 +right : store_uint_array_rec(?p, ?x, ?y, ?l2) at 1 +action : right_erase(1); + left_erase(0); + right_add(l1 == l2); + + +id : 7 +priority : core(1) +left : store_uint_array_rec(?p, ?x, ?y, ?l) at 0 +right : data_at(?p + (?i * sizeof(I32)), I32, ?v) at 1 +check : infer(x <= i); + infer(i < y); +action : right_erase(1); + left_erase(0); + left_add(store_uint_array_missing_i_rec(p, i, x, y, l)); + right_add(v == l[i - x]); + +id : 8 +priority : core(1) +left : store_uint_array_rec(?p, ?x, ?y, ?l1) at 0 + store_uint_array_rec(?p, ?y, ?z, ?l2) at 1 +right : store_uint_array_rec(?p, ?x, ?z, ?l3) at 2 +check : infer(y <= z); + infer(x <= y); +action : right_erase(2); + left_erase(0); + left_erase(1); + right_add(l3 == app{Z}(l1, l2)); + +id : 9 +priority : core(1) +left : store_uint_array_rec(?p, ?x, ?z, ?l3) at 2 +right : store_uint_array_rec(?p, ?x, ?y, ?l1) at 0 + store_uint_array_rec(?p, ?y, ?z, ?l2) at 1 +check : infer(y <= z); + infer(x <= y); +action : left_erase(2); + right_erase(0); + right_erase(1); + right_add(l3 == app{Z}(l1, l2)); + right_add(Zlength{Z}(l1) == y - x); + +id : 10 +priority : core(1) +right : store_uint_array_rec(?p, ?x, ?x, ?l) at 0 +action : right_erase(0); + right_add(l == nil{Z}); + + +id : 11 +priority : post(1) +left : store_uint_array_missing_i_rec(?p, ?i, ?x, ?y, ?l) at 0 + data_at(p + ?i * sizeof(I32), I32, l[?i - ?x]) at 1 +check : infer(x <= i); + infer(i < y); +action : left_erase(1); + left_erase(0); + left_add(store_uint_array_rec(p, x, y, l)); + +id : 12 +priority : post(4) +left : store_uint_array_missing_i_rec(?p, ?i, ?x, ?y, ?l) at 0 + data_at(p + ?i * sizeof(I32), I32, ?v) at 1 +check : infer(x <= i); + infer(i < y); +action : left_erase(1); + left_erase(0); + left_add(store_uint_array_rec(p, x, y, replace_Znth{Z}(i - x, v, l))); \ No newline at end of file From 4c0b0e98fa49b68ca88166ed326f902bcc1c1808 Mon Sep 17 00:00:00 2001 From: xiaoh105 Date: Tue, 10 Jun 2025 17:54:33 +0800 Subject: [PATCH 3/6] feat(mpn_copyi): Proved correctness of mpn_copyi and other simple util functions. --- Makefile | 4 +- projects/int_array_def.h | 3 +- projects/lib/GmpAux.v | 86 +++++ projects/lib/GmpNumber.v | 5 +- projects/lib/gmp_goal.v | 624 ++++++++++++++++++++++++++++++++ projects/lib/gmp_goal_check.v | 6 + projects/lib/gmp_proof_auto.v | 65 ++++ projects/lib/gmp_proof_manual.v | 152 ++++++++ projects/mini-gmp.c | 94 ++++- projects/mini-gmp.h | 10 +- projects/uint_array.strategies | 12 +- 11 files changed, 1035 insertions(+), 26 deletions(-) create mode 100644 projects/lib/gmp_goal.v create mode 100644 projects/lib/gmp_goal_check.v create mode 100644 projects/lib/gmp_proof_auto.v create mode 100644 projects/lib/gmp_proof_manual.v diff --git a/Makefile b/Makefile index 54672ff..4be80a5 100755 --- a/Makefile +++ b/Makefile @@ -37,7 +37,9 @@ PV_FILE_NAMES = \ PV_FILES=$(PV_FILE_NAMES:%.v=$(PV_DIR)/%.v) -GMP_FILES = ./projects/lib/GmpAux.v ./projects/lib/GmpNumber.v +GMP_FILES = \ + ./projects/lib/GmpAux.v ./projects/lib/GmpNumber.v \ + ./projects/lib/gmp_goal.v FILES = $(PV_FILES) \ $(GMP_FILES) diff --git a/projects/int_array_def.h b/projects/int_array_def.h index e5f5957..095107e 100644 --- a/projects/int_array_def.h +++ b/projects/int_array_def.h @@ -1,7 +1,8 @@ /*@ Extern Coq (sum : list Z -> Z) (sublist : {A} -> Z -> Z -> list A -> list A) (store_int_array : Z -> Z -> list Z -> Assertion) - (store_uint_array : Z -> Z -> list Z -> Assertion)(store_uint_array : Z -> Z -> list Z -> Assertion) + (store_uint_array : Z -> Z -> list Z -> Assertion) + (store_undef_uint_array_rec : Z -> Z -> Z -> Assertion) (store_int_array_missing_i_rec: Z -> Z -> Z -> Z -> list Z -> Assertion) (store_uint_array_missing_i_rec: Z -> Z -> Z -> Z -> list Z -> Assertion) (store_array_box: Z -> Z -> list Z -> Assertion) diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index 4701085..6d4d524 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -100,5 +100,91 @@ Proof. rewrite IHl1. reflexivity. Qed. + +Lemma store_array_rec_false: forall x storeA lo hi (l: list Z), + lo > hi -> + store_array_rec storeA x lo hi l |-- [| False |]. +Proof. + intros. + revert x storeA lo hi H. + induction l; intros. + + simpl. + entailer!. + + simpl. + specialize (IHl x storeA (lo + 1) hi ltac:(lia)). + sep_apply IHl. + entailer!. +Qed. + +Lemma store_array_rec_empty: forall x storeA lo (l: list Z), + store_array_rec storeA x lo lo l |-- emp && [| l = nil |]. +Proof. + intros. + destruct l. + + simpl. + entailer!. + + simpl. + sep_apply store_array_rec_false; [ entailer! | lia ]. +Qed. + +Lemma store_uint_array_rec_false: forall x lo hi l, + lo > hi -> + store_uint_array_rec x lo hi l |-- [| False |]. +Proof. + intros. + unfold store_uint_array_rec. + sep_apply store_array_rec_false; [ entailer! | lia ]. +Qed. + +Lemma store_uint_array_rec_empty: forall x lo l, + store_uint_array_rec x lo lo l |-- emp && [| l = nil |]. +Proof. + induction l. + + unfold store_uint_array_rec. + simpl. + entailer!. + + pose proof (store_uint_array_rec_false x (lo + 1) lo l ltac:(lia)). + unfold store_uint_array_rec in *. + simpl in *. + sep_apply H. + entailer!. +Qed. + +Lemma store_uint_array_empty: forall x l, + store_uint_array x 0 l |-- emp && [| l = nil |]. +Proof. + intros x l. + revert x. + induction l; intros. + + unfold store_uint_array, store_array. + simpl. + entailer!. + + unfold store_uint_array, store_array. + simpl. + sep_apply store_array_rec_false; [ entailer! | lia ]. +Qed. + +Lemma store_uarray_rec_equals_store_uarray: forall x lo hi l, + lo < hi -> + store_uint_array_rec x lo hi l --||-- + store_uint_array (x + sizeof(UINT) * lo) (hi - lo) l. +Proof. + intros. + unfold store_uint_array_rec, store_uint_array, store_array. + pose proof (store_array_rec_base x 0 lo hi l (sizeof(UINT)) + store_uint + (fun (x: addr) (lo a: Z) => + (x + lo * sizeof(UINT)) # UInt |-> a) ltac:(reflexivity)). + assert (x + sizeof(UINT) * lo = x + lo * sizeof(UINT)). { lia. } + rewrite H1; clear H1. + assert (0 + lo = lo). { lia. } + repeat rewrite H1 in H0; clear H1. + destruct H0. + split. + + sep_apply H0. + entailer!. + + sep_apply H1. + entailer!. +Qed. End Aux. \ No newline at end of file diff --git a/projects/lib/GmpNumber.v b/projects/lib/GmpNumber.v index 7104900..9ba0593 100755 --- a/projects/lib/GmpNumber.v +++ b/projects/lib/GmpNumber.v @@ -21,11 +21,12 @@ Import naive_C_Rules. Local Open Scope sac. Notation "'UINT_MOD'" := (4294967296). +Notation "'LENGTH_MAX'" := (100000000). Module Internal. Definition mpd_store_list (ptr: addr) (data: list Z) (cap: Z): Assertion := - [| Zlength data <= cap |] && + [| Zlength data <= cap |] && [| cap <= LENGTH_MAX |] && store_uint_array ptr (Zlength data) data ** store_undef_uint_array_rec ptr ((Zlength data) + 1) cap. @@ -46,7 +47,7 @@ Definition list_store_Z (data: list Z) (n: Z): Prop := Definition mpd_store_Z (ptr: addr) (n: Z) (size: Z) (cap: Z): Assertion := EX data, - mpd_store_list ptr data cap && [| list_store_Z data n|] && [| size = Zlength data |]. + mpd_store_list ptr data cap && [| list_store_Z data n |] && [| size = Zlength data |]. Lemma __list_within_bound_concat_r: forall (l1: list Z) (a: Z), list_within_bound l1 -> diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v new file mode 100644 index 0000000..0456f92 --- /dev/null +++ b/projects/lib/gmp_goal.v @@ -0,0 +1,624 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.Bool.Bool. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import Coq.Classes.RelationClasses. +Require Import Coq.Classes.Morphisms. +Require Import Coq.micromega.Psatz. +Require Import Coq.Sorting.Permutation. +From AUXLib Require Import int_auto Axioms Feq Idents List_lemma VMap. +Require Import SetsClass.SetsClass. Import SetsNotation. +From SimpleC.SL Require Import Mem SeparationLogic. +Require Import GmpLib.GmpNumber. Import Internal. +Require Import Logic.LogicGenerator.demo932.Interface. +Local Open Scope Z_scope. +Local Open Scope sets. +Local Open Scope string. +Local Open Scope list. +Import naive_C_Rules. +Local Open Scope sac. + +Definition Zmax := Z.max. + +(*----- Function gmp_abs -----*) + +Definition gmp_abs_safety_wit_1 := +forall (x_pre: Z) , + [| (x_pre < 0) |] + && [| (INT_MIN < x_pre) |] + && [| (x_pre <= INT_MAX) |] + && ((( &( "x" ) )) # Int |-> x_pre) +|-- + [| (x_pre <> (INT_MIN)) |] +. + +Definition gmp_abs_return_wit_1_1 := +forall (x_pre: Z) , + [| (x_pre < 0) |] + && [| (INT_MIN < x_pre) |] + && [| (x_pre <= INT_MAX) |] + && emp +|-- + [| ((-x_pre) = (Zabs (x_pre))) |] + && emp +. + +Definition gmp_abs_return_wit_1_2 := +forall (x_pre: Z) , + [| (x_pre >= 0) |] + && [| (INT_MIN < x_pre) |] + && [| (x_pre <= INT_MAX) |] + && emp +|-- + [| (x_pre = (Zabs (x_pre))) |] + && emp +. + +(*----- Function gmp_max -----*) + +Definition gmp_max_return_wit_1_1 := +forall (b_pre: Z) (a_pre: Z) , + [| (a_pre <= b_pre) |] + && emp +|-- + [| (b_pre = (Zmax (a_pre) (b_pre))) |] + && emp +. + +Definition gmp_max_return_wit_1_2 := +forall (b_pre: Z) (a_pre: Z) , + [| (a_pre > b_pre) |] + && emp +|-- + [| (a_pre = (Zmax (a_pre) (b_pre))) |] + && emp +. + +(*----- Function gmp_cmp -----*) + +Definition gmp_cmp_safety_wit_1 := +forall (b_pre: Z) (a_pre: Z) , + [| (a_pre >= b_pre) |] + && [| (a_pre <= b_pre) |] + && ((( &( "b" ) )) # Int |-> b_pre) + ** ((( &( "a" ) )) # Int |-> a_pre) +|-- + [| ((0 - 0 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (0 - 0 )) |] +. + +Definition gmp_cmp_safety_wit_2 := +forall (b_pre: Z) (a_pre: Z) , + [| (a_pre < b_pre) |] + && [| (a_pre <= b_pre) |] + && ((( &( "b" ) )) # Int |-> b_pre) + ** ((( &( "a" ) )) # Int |-> a_pre) +|-- + [| ((0 - 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (0 - 1 )) |] +. + +Definition gmp_cmp_safety_wit_3 := +forall (b_pre: Z) (a_pre: Z) , + [| (a_pre >= b_pre) |] + && [| (a_pre > b_pre) |] + && ((( &( "b" ) )) # Int |-> b_pre) + ** ((( &( "a" ) )) # Int |-> a_pre) +|-- + [| ((1 - 0 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (1 - 0 )) |] +. + +Definition gmp_cmp_safety_wit_4 := +forall (b_pre: Z) (a_pre: Z) , + [| (a_pre < b_pre) |] + && [| (a_pre > b_pre) |] + && ((( &( "b" ) )) # Int |-> b_pre) + ** ((( &( "a" ) )) # Int |-> a_pre) +|-- + [| False |] +. + +Definition gmp_cmp_return_wit_1_1 := +forall (b_pre: Z) (a_pre: Z) , + [| (a_pre >= b_pre) |] + && [| (a_pre > b_pre) |] + && emp +|-- + ([| (a_pre < b_pre) |] + && [| ((1 - 0 ) = (-1)) |] + && emp) + || + ([| (a_pre = b_pre) |] + && [| ((1 - 0 ) = 0) |] + && emp) + || + ([| (a_pre > b_pre) |] + && [| ((1 - 0 ) = 1) |] + && emp) +. + +Definition gmp_cmp_return_wit_1_2 := +forall (b_pre: Z) (a_pre: Z) , + [| (a_pre < b_pre) |] + && [| (a_pre <= b_pre) |] + && emp +|-- + ([| (a_pre < b_pre) |] + && [| ((0 - 1 ) = (-1)) |] + && emp) + || + ([| (a_pre = b_pre) |] + && [| ((0 - 1 ) = 0) |] + && emp) + || + ([| (a_pre > b_pre) |] + && [| ((0 - 1 ) = 1) |] + && emp) +. + +Definition gmp_cmp_return_wit_1_3 := +forall (b_pre: Z) (a_pre: Z) , + [| (a_pre >= b_pre) |] + && [| (a_pre <= b_pre) |] + && emp +|-- + ([| (a_pre < b_pre) |] + && [| ((0 - 0 ) = (-1)) |] + && emp) + || + ([| (a_pre = b_pre) |] + && [| ((0 - 0 ) = 0) |] + && emp) + || + ([| (a_pre > b_pre) |] + && [| ((0 - 0 ) = 1) |] + && emp) +. + +(*----- Function mpn_copyi -----*) + +Definition mpn_copyi_safety_wit_1 := +forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) , + [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && ((( &( "i" ) )) # Int |->_) + ** ((( &( "d" ) )) # Ptr |-> d_pre) + ** (store_uint_array_rec d_pre 0 cap2 l2 ) + ** (store_uint_array d_pre 0 nil ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "s" ) )) # Ptr |-> s_pre) + ** (store_uint_array s_pre n_pre l ) + ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) +|-- + [| (0 <= INT_MAX) |] + && [| ((INT_MIN) <= 0) |] +. + +Definition mpn_copyi_safety_wit_2 := +forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l': (@list Z)) (d: Z) (s: Z) (l_2: (@list Z)) (n: Z) (i: Z) (a: Z) (l2': (@list Z)) , + [| (l' = (cons (a) (l2'))) |] + && [| (i < n) |] + && [| (n <= cap2) |] + && [| (i < n) |] + && [| (0 <= i) |] + && [| (i <= n) |] + && [| ((Zlength (l_2)) = n) |] + && [| (list_store_Z l_2 val ) |] + && [| (n <= cap1) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (store_uint_array d (i + 1 ) (replace_Znth (i) ((Znth i l_2 0)) ((app ((sublist (0) (i) (l_2))) ((cons (a) (nil)))))) ) + ** (store_uint_array s n l_2 ) + ** ((( &( "i" ) )) # Int |-> i) + ** ((( &( "n" ) )) # Int |-> n) + ** ((( &( "d" ) )) # Ptr |-> d) + ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) + ** ((( &( "s" ) )) # Ptr |-> s) + ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) +|-- + [| ((i + 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (i + 1 )) |] +. + +Definition mpn_copyi_entail_wit_1 := +forall (n_pre: Z) (s_pre: Z) (d_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 l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (store_uint_array_rec d_pre 0 cap2 l2 ) + ** (store_uint_array d_pre 0 nil ) + ** (store_uint_array s_pre n_pre l_2 ) + ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) +|-- + EX (l': (@list Z)) (l: (@list Z)) , + [| (0 <= 0) |] + && [| (0 <= n_pre) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (list_store_Z l val ) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (store_uint_array s_pre n_pre l ) + ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_uint_array d_pre 0 (sublist (0) (0) (l)) ) + ** (store_uint_array_rec d_pre 0 cap2 l' ) +. + +Definition mpn_copyi_entail_wit_2 := +forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (l'_2: (@list Z)) (d: Z) (s: Z) (l_3: (@list Z)) (n: Z) (i: Z) (a: Z) (l2': (@list Z)) , + [| (l'_2 = (cons (a) (l2'))) |] + && [| (i < n) |] + && [| (n <= cap2) |] + && [| (i < n) |] + && [| (0 <= i) |] + && [| (i <= n) |] + && [| ((Zlength (l_3)) = n) |] + && [| (list_store_Z l_3 val ) |] + && [| (n <= cap1) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (store_uint_array d (i + 1 ) (replace_Znth (i) ((Znth i l_3 0)) ((app ((sublist (0) (i) (l_3))) ((cons (a) (nil)))))) ) + ** (store_uint_array s n l_3 ) + ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) + ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) +|-- + EX (l': (@list Z)) (l: (@list Z)) , + [| (0 <= (i + 1 )) |] + && [| ((i + 1 ) <= n) |] + && [| ((Zlength (l)) = n) |] + && [| (list_store_Z l val ) |] + && [| (n <= cap1) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (store_uint_array s n l ) + ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_uint_array d (i + 1 ) (sublist (0) ((i + 1 )) (l)) ) + ** (store_uint_array_rec d (i + 1 ) cap2 l' ) +. + +Definition mpn_copyi_return_wit_1 := +forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (l': (@list Z)) (d: Z) (s: Z) (l: (@list Z)) (n: Z) (i: Z) , + [| (i >= n) |] + && [| (0 <= i) |] + && [| (i <= n) |] + && [| ((Zlength (l)) = n) |] + && [| (list_store_Z l val ) |] + && [| (n <= cap1) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (store_uint_array s n l ) + ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_uint_array d i (sublist (0) (i) (l)) ) + ** (store_uint_array_rec d i cap2 l' ) +|-- + (mpd_store_Z s_pre val n_pre cap1 ) + ** (mpd_store_Z d_pre val n_pre cap2 ) +. + +Definition mpn_copyi_partial_solve_wit_1 := +forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) , + [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (mpd_store_Z s_pre val n_pre cap1 ) + ** (store_uint_array d_pre cap2 l2 ) +|-- + [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (mpd_store_Z s_pre val n_pre cap1 ) + ** (store_uint_array d_pre cap2 l2 ) +. + +Definition mpn_copyi_partial_solve_wit_2_pure := +forall (n_pre: Z) (s_pre: Z) (d_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 l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "s" ) )) # Ptr |-> s_pre) + ** (store_uint_array s_pre n_pre l ) + ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** ((( &( "d" ) )) # Ptr |-> d_pre) + ** (store_uint_array d_pre cap2 l2 ) +|-- + [| ((Zlength (l2)) = cap2) |] +. + +Definition mpn_copyi_partial_solve_wit_2_aux := +forall (n_pre: Z) (s_pre: Z) (d_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 l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (store_uint_array s_pre n_pre l ) + ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_uint_array d_pre cap2 l2 ) +|-- + [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (store_uint_array d_pre cap2 l2 ) + ** (store_uint_array s_pre n_pre l ) + ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) +. + +Definition mpn_copyi_partial_solve_wit_2 := mpn_copyi_partial_solve_wit_2_pure -> mpn_copyi_partial_solve_wit_2_aux. + +Definition mpn_copyi_partial_solve_wit_3_pure := +forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) (l': (@list Z)) (d: Z) (s: Z) (l: (@list Z)) (n: Z) (i: Z) , + [| (i < n) |] + && [| (0 <= i) |] + && [| (i <= n) |] + && [| ((Zlength (l)) = n) |] + && [| (list_store_Z l val ) |] + && [| (n <= cap1) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l_2)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l_2 val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && ((( &( "i" ) )) # Int |-> i) + ** ((( &( "n" ) )) # Int |-> n) + ** ((( &( "s" ) )) # Ptr |-> s) + ** (store_uint_array s n l ) + ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** ((( &( "d" ) )) # Ptr |-> d) + ** (store_uint_array d i (sublist (0) (i) (l)) ) + ** (store_uint_array_rec d i cap2 l' ) +|-- + [| (0 <= i) |] + && [| (i < n) |] + && [| (n <= cap2) |] +. + +Definition mpn_copyi_partial_solve_wit_3_aux := +forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l': (@list Z)) (d: Z) (s: Z) (l_2: (@list Z)) (n: Z) (i: Z) , + [| (i < n) |] + && [| (0 <= i) |] + && [| (i <= n) |] + && [| ((Zlength (l_2)) = n) |] + && [| (list_store_Z l_2 val ) |] + && [| (n <= cap1) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (store_uint_array s n l_2 ) + ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_uint_array d i (sublist (0) (i) (l_2)) ) + ** (store_uint_array_rec d i cap2 l' ) +|-- + [| (0 <= i) |] + && [| (i < n) |] + && [| (n <= cap2) |] + && [| (i < n) |] + && [| (0 <= i) |] + && [| (i <= n) |] + && [| ((Zlength (l_2)) = n) |] + && [| (list_store_Z l_2 val ) |] + && [| (n <= cap1) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (store_uint_array_rec d i cap2 l' ) + ** (store_uint_array d i (sublist (0) (i) (l_2)) ) + ** (store_uint_array s n l_2 ) + ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) +. + +Definition mpn_copyi_partial_solve_wit_3 := mpn_copyi_partial_solve_wit_3_pure -> mpn_copyi_partial_solve_wit_3_aux. + +Definition mpn_copyi_partial_solve_wit_4 := +forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l': (@list Z)) (d: Z) (s: Z) (l_2: (@list Z)) (n: Z) (i: Z) (a: Z) (l2': (@list Z)) , + [| (l' = (cons (a) (l2'))) |] + && [| (i < n) |] + && [| (n <= cap2) |] + && [| (i < n) |] + && [| (0 <= i) |] + && [| (i <= n) |] + && [| ((Zlength (l_2)) = n) |] + && [| (list_store_Z l_2 val ) |] + && [| (n <= cap1) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (store_uint_array_rec d (i + 1 ) cap2 l2' ) + ** (store_uint_array d (i + 1 ) (app ((sublist (0) (i) (l_2))) ((cons (a) (nil)))) ) + ** (store_uint_array s n l_2 ) + ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) +|-- + [| (l' = (cons (a) (l2'))) |] + && [| (i < n) |] + && [| (n <= cap2) |] + && [| (i < n) |] + && [| (0 <= i) |] + && [| (i <= n) |] + && [| ((Zlength (l_2)) = n) |] + && [| (list_store_Z l_2 val ) |] + && [| (n <= cap1) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (((s + (i * sizeof(UINT) ) )) # UInt |-> (Znth i l_2 0)) + ** (store_uint_array_missing_i_rec s i 0 n l_2 ) + ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) + ** (store_uint_array d (i + 1 ) (app ((sublist (0) (i) (l_2))) ((cons (a) (nil)))) ) + ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) +. + +Definition mpn_copyi_partial_solve_wit_5 := +forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l': (@list Z)) (d: Z) (s: Z) (l_2: (@list Z)) (n: Z) (i: Z) (a: Z) (l2': (@list Z)) , + [| (l' = (cons (a) (l2'))) |] + && [| (i < n) |] + && [| (n <= cap2) |] + && [| (i < n) |] + && [| (0 <= i) |] + && [| (i <= n) |] + && [| ((Zlength (l_2)) = n) |] + && [| (list_store_Z l_2 val ) |] + && [| (n <= cap1) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (store_uint_array s n l_2 ) + ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) + ** (store_uint_array d (i + 1 ) (app ((sublist (0) (i) (l_2))) ((cons (a) (nil)))) ) + ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) +|-- + [| (l' = (cons (a) (l2'))) |] + && [| (i < n) |] + && [| (n <= cap2) |] + && [| (i < n) |] + && [| (0 <= i) |] + && [| (i <= n) |] + && [| ((Zlength (l_2)) = n) |] + && [| (list_store_Z l_2 val ) |] + && [| (n <= cap1) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (n_pre <= cap1) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l val ) |] + && [| ((Zlength (l2)) = cap2) |] + && [| (cap2 >= n_pre) |] + && (((d + (i * sizeof(UINT) ) )) # UInt |->_) + ** (store_uint_array_missing_i_rec d i 0 (i + 1 ) (app ((sublist (0) (i) (l_2))) ((cons (a) (nil)))) ) + ** (store_uint_array s n l_2 ) + ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) + ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) +. + +Definition mpn_copyi_which_implies_wit_1 := +forall (cap1: Z) (val: Z) (n: Z) (s: Z) , + (mpd_store_Z s val n cap1 ) +|-- + EX (l: (@list Z)) , + [| (n <= cap1) |] + && [| ((Zlength (l)) = n) |] + && [| (cap1 <= 100000000) |] + && [| (list_store_Z l val ) |] + && (store_uint_array s n l ) + ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) +. + +Definition mpn_copyi_which_implies_wit_2 := +forall (cap2: Z) (l2: (@list Z)) (d: Z) , + [| ((Zlength (l2)) = cap2) |] + && (store_uint_array d cap2 l2 ) +|-- + [| ((Zlength (l2)) = cap2) |] + && (store_uint_array_rec d 0 cap2 l2 ) + ** (store_uint_array d 0 nil ) +. + +Definition mpn_copyi_which_implies_wit_3 := +forall (cap2: Z) (l': (@list Z)) (l: (@list Z)) (i: Z) (n: Z) (d: Z) , + [| (0 <= i) |] + && [| (i < n) |] + && [| (n <= cap2) |] + && (store_uint_array_rec d i cap2 l' ) + ** (store_uint_array d i (sublist (0) (i) (l)) ) +|-- + EX (a: Z) (l2': (@list Z)) , + [| (l' = (cons (a) (l2'))) |] + && [| (i < n) |] + && [| (n <= cap2) |] + && (store_uint_array_rec d (i + 1 ) cap2 l2' ) + ** (store_uint_array d (i + 1 ) (app ((sublist (0) (i) (l))) ((cons (a) (nil)))) ) +. + +Module Type VC_Correct. + +Axiom proof_of_gmp_abs_safety_wit_1 : gmp_abs_safety_wit_1. +Axiom proof_of_gmp_abs_return_wit_1_1 : gmp_abs_return_wit_1_1. +Axiom proof_of_gmp_abs_return_wit_1_2 : gmp_abs_return_wit_1_2. +Axiom proof_of_gmp_max_return_wit_1_1 : gmp_max_return_wit_1_1. +Axiom proof_of_gmp_max_return_wit_1_2 : gmp_max_return_wit_1_2. +Axiom proof_of_gmp_cmp_safety_wit_1 : gmp_cmp_safety_wit_1. +Axiom proof_of_gmp_cmp_safety_wit_2 : gmp_cmp_safety_wit_2. +Axiom proof_of_gmp_cmp_safety_wit_3 : gmp_cmp_safety_wit_3. +Axiom proof_of_gmp_cmp_safety_wit_4 : gmp_cmp_safety_wit_4. +Axiom proof_of_gmp_cmp_return_wit_1_1 : gmp_cmp_return_wit_1_1. +Axiom proof_of_gmp_cmp_return_wit_1_2 : gmp_cmp_return_wit_1_2. +Axiom proof_of_gmp_cmp_return_wit_1_3 : gmp_cmp_return_wit_1_3. +Axiom proof_of_mpn_copyi_safety_wit_1 : mpn_copyi_safety_wit_1. +Axiom proof_of_mpn_copyi_safety_wit_2 : mpn_copyi_safety_wit_2. +Axiom proof_of_mpn_copyi_entail_wit_1 : mpn_copyi_entail_wit_1. +Axiom proof_of_mpn_copyi_entail_wit_2 : mpn_copyi_entail_wit_2. +Axiom proof_of_mpn_copyi_return_wit_1 : mpn_copyi_return_wit_1. +Axiom proof_of_mpn_copyi_partial_solve_wit_1 : mpn_copyi_partial_solve_wit_1. +Axiom proof_of_mpn_copyi_partial_solve_wit_2_pure : mpn_copyi_partial_solve_wit_2_pure. +Axiom proof_of_mpn_copyi_partial_solve_wit_2 : mpn_copyi_partial_solve_wit_2. +Axiom proof_of_mpn_copyi_partial_solve_wit_3_pure : mpn_copyi_partial_solve_wit_3_pure. +Axiom proof_of_mpn_copyi_partial_solve_wit_3 : mpn_copyi_partial_solve_wit_3. +Axiom proof_of_mpn_copyi_partial_solve_wit_4 : mpn_copyi_partial_solve_wit_4. +Axiom proof_of_mpn_copyi_partial_solve_wit_5 : mpn_copyi_partial_solve_wit_5. +Axiom proof_of_mpn_copyi_which_implies_wit_1 : mpn_copyi_which_implies_wit_1. +Axiom proof_of_mpn_copyi_which_implies_wit_2 : mpn_copyi_which_implies_wit_2. +Axiom proof_of_mpn_copyi_which_implies_wit_3 : mpn_copyi_which_implies_wit_3. + +End VC_Correct. diff --git a/projects/lib/gmp_goal_check.v b/projects/lib/gmp_goal_check.v new file mode 100644 index 0000000..43755db --- /dev/null +++ b/projects/lib/gmp_goal_check.v @@ -0,0 +1,6 @@ +From Require Import gmp_goal gmp_proof_auto gmp_proof_manual. + +Module VC_Correctness : VC_Correct. + Include gmp_proof_auto. + Include gmp_proof_manual. +End VC_Correctness. diff --git a/projects/lib/gmp_proof_auto.v b/projects/lib/gmp_proof_auto.v new file mode 100644 index 0000000..1cb2659 --- /dev/null +++ b/projects/lib/gmp_proof_auto.v @@ -0,0 +1,65 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.Bool.Bool. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import Coq.Classes.RelationClasses. +Require Import Coq.Classes.Morphisms. +Require Import Coq.micromega.Psatz. +Require Import Coq.Sorting.Permutation. +From AUXLib Require Import int_auto Axioms Feq Idents List_lemma VMap. +Require Import SetsClass.SetsClass. Import SetsNotation. +From SimpleC.SL Require Import Mem SeparationLogic. +From Require Import gmp_goal. +Require Import Logic.LogicGenerator.demo932.Interface. +Local Open Scope Z_scope. +Local Open Scope sets. +Local Open Scope string. +Local Open Scope list. +Import naive_C_Rules. +Local Open Scope sac. + +Lemma proof_of_gmp_abs_safety_wit_1 : gmp_abs_safety_wit_1. +Proof. Admitted. + +Lemma proof_of_gmp_cmp_safety_wit_1 : gmp_cmp_safety_wit_1. +Proof. Admitted. + +Lemma proof_of_gmp_cmp_safety_wit_2 : gmp_cmp_safety_wit_2. +Proof. Admitted. + +Lemma proof_of_gmp_cmp_safety_wit_3 : gmp_cmp_safety_wit_3. +Proof. Admitted. + +Lemma proof_of_gmp_cmp_safety_wit_4 : gmp_cmp_safety_wit_4. +Proof. Admitted. + +Lemma proof_of_gmp_cmp_return_wit_1_1 : gmp_cmp_return_wit_1_1. +Proof. Admitted. + +Lemma proof_of_gmp_cmp_return_wit_1_3 : gmp_cmp_return_wit_1_3. +Proof. Admitted. + +Lemma proof_of_mpn_copyi_safety_wit_1 : mpn_copyi_safety_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_copyi_safety_wit_2 : mpn_copyi_safety_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_copyi_partial_solve_wit_1 : mpn_copyi_partial_solve_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_copyi_partial_solve_wit_2_pure : mpn_copyi_partial_solve_wit_2_pure. +Proof. Admitted. + +Lemma proof_of_mpn_copyi_partial_solve_wit_2 : mpn_copyi_partial_solve_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_copyi_partial_solve_wit_3 : mpn_copyi_partial_solve_wit_3. +Proof. Admitted. + +Lemma proof_of_mpn_copyi_partial_solve_wit_4 : mpn_copyi_partial_solve_wit_4. +Proof. Admitted. + +Lemma proof_of_mpn_copyi_partial_solve_wit_5 : mpn_copyi_partial_solve_wit_5. +Proof. Admitted. + diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v new file mode 100644 index 0000000..5fbd764 --- /dev/null +++ b/projects/lib/gmp_proof_manual.v @@ -0,0 +1,152 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.Bool.Bool. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import Coq.Classes.RelationClasses. +Require Import Coq.Classes.Morphisms. +Require Import Coq.micromega.Psatz. +Require Import Coq.Sorting.Permutation. +From AUXLib Require Import int_auto Axioms Feq Idents List_lemma VMap. +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 Logic.LogicGenerator.demo932.Interface. +Local Open Scope Z_scope. +Local Open Scope sets. +Local Open Scope string. +Local Open Scope list. +Import naive_C_Rules. +Local Open Scope sac. + +Lemma proof_of_gmp_abs_return_wit_1_1 : gmp_abs_return_wit_1_1. +Proof. pre_process. Qed. + + +Lemma proof_of_gmp_abs_return_wit_1_2 : gmp_abs_return_wit_1_2. +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. +Proof. + pre_process. + repeat rewrite <-derivable1_orp_intros1. + entailer!. +Qed. + +Lemma proof_of_mpn_copyi_entail_wit_1 : mpn_copyi_entail_wit_1. +Proof. + pre_process. + Exists l2 l_2. + entailer!. + pose proof (Zlength_nonneg l_2). + lia. +Qed. + +Lemma proof_of_mpn_copyi_entail_wit_2 : mpn_copyi_entail_wit_2. +Proof. + pre_process. + Exists l2' l_3. + entailer!. + rewrite replace_Znth_app_r. + + rewrite Zlength_sublist0; [ | lia ]. + assert (i - i = 0). { lia. } + rewrite H15; clear H15. + assert (replace_Znth 0 (Znth i l_3 0) (a :: nil) = sublist i (i + 1) l_3). { + unfold replace_Znth, Z.to_nat, replace_nth. + rewrite (sublist_single i l_3 0); [ reflexivity | ]. + rewrite <-Zlength_correct; lia. + } + rewrite H15; clear H15. + rewrite replace_Znth_nothing. + - rewrite <-sublist_split; try lia; try reflexivity. + rewrite <-Zlength_correct; lia. + - pose proof (Zlength_sublist0 i l_3 ltac:(lia)). + lia. + + pose proof (Zlength_sublist0 i l_3); lia. +Qed. + +Lemma proof_of_mpn_copyi_which_implies_wit_1 : mpn_copyi_which_implies_wit_1. +Proof. + pre_process. + unfold mpd_store_Z. + Intros l. + Exists l. + unfold mpd_store_list. + entailer!. + subst. + entailer!. +Qed. + +Lemma proof_of_mpn_copyi_which_implies_wit_2 : mpn_copyi_which_implies_wit_2. +Proof. + pre_process. + pose proof (store_uint_array_divide d 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 (d + 0 = d). { lia. } + rewrite H2; clear H2. + assert (cap2 - 0 = cap2). { lia. } + rewrite H2; clear H2. + reflexivity. +Qed. + +Lemma proof_of_mpn_copyi_which_implies_wit_3 : mpn_copyi_which_implies_wit_3. +Proof. + pre_process. + destruct l'. { + unfold store_uint_array_rec. + simpl. + entailer!. + } + pose proof (store_uint_array_rec_cons d i cap2 z l' ltac:(lia)). + sep_apply H2. + Exists z l'. + entailer!. + assert (i = 0 \/ i > 0). { lia. } + destruct H3. + + subst. + unfold store_uint_array, store_array. + simpl. + entailer!. + + pose proof (Aux.store_uarray_rec_equals_store_uarray d 0 i (sublist 0 i l) ltac:(lia)). + destruct H4 as [_ H4]. + assert (d + sizeof(UINT) * 0 = d). { lia. } + rewrite H5 in H4; clear H5. + assert (i - 0 = i). { lia. } + rewrite H5 in H4; clear H5. + sep_apply H4; clear H4. + pose proof (Aux.store_uarray_rec_equals_store_uarray d 0 (i + 1) (sublist 0 i l ++ z :: nil) ltac:(lia)). + destruct H4 as [H4 _]. + assert (i + 1 - 0 = i + 1). { lia. } + rewrite H5 in H4; clear H5. + assert (d + sizeof(UINT) * 0 = d). { lia. } + rewrite H5 in H4; clear H5. + rewrite <-H4. + sep_apply store_uint_array_rec_tail_merge; [ reflexivity | lia ]. +Qed. \ No newline at end of file diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 3dc0c43..734d342 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -5,7 +5,7 @@ int gmp_abs(int x) /*@ - Require emp + Require INT_MIN < x && x <= INT_MAX Ensure __return == Zabs(x) */ { @@ -25,9 +25,10 @@ int gmp_cmp(int a, int b) /*@ Require emp Ensure - a > b && __return == 1 || + emp * + (a > b && __return == 1 || a == b && __return == 0 || - a < b && __return == -1 + a < b && __return == -1) */ { return (a > b) - (a < b); @@ -39,25 +40,60 @@ int gmp_cmp(int a, int b) void mpn_copyi (unsigned int *d, unsigned int *s, int n) /*@ - With val data cap1 cap2 + With val l2 cap1 cap2 Require mpd_store_Z(s, val, n, cap1) * - store_uint_array(d, cap2, data) + store_uint_array(d, cap2, l2) && + Zlength(l2) == cap2 && + cap2 >= n Ensure mpd_store_Z(s, val, n, cap1) * mpd_store_Z(d, val, n, cap2) */ { - /* + /*@ mpd_store_Z(s, val, n, cap1) which implies exists l, - store_uint_array(s, n, l) ** - store_undef + n <= cap1 && + Zlength(l) == n && + cap1 <= 100000000 && + store_uint_array(s, n, l) * + store_undef_uint_array_rec(s, n + 1, cap1) && + list_store_Z(l, val) + */ + /*@ + store_uint_array(d, cap2, l2) && Zlength(l2) == cap2 + which implies + store_uint_array_rec(d, 0, cap2, l2) * store_uint_array(d, 0, nil) && + Zlength(l2) == cap2 */ int i; - for (i = 0; i < n; i++) - d[i] = s[i]; + /*@ Inv + exists l l', + 0 <= i && i <= n && Zlength(l) == n && + list_store_Z(l, val) && n <= cap1 && + store_uint_array(s, n, l) * + store_undef_uint_array_rec(s, n + 1, cap1) * + store_uint_array(d, i, sublist(0, i, l)) * + store_uint_array_rec(d, i, cap2, l') + */ + for (i = 0; i < n; i++) { + /*@ + Given l l' + */ + /*@ + 0 <= i && i < n && n <= cap2 && + store_uint_array_rec(d, i, cap2, l') * + store_uint_array(d, i, sublist(0, i, l)) + which implies + exists a l2', + l' == cons(a, l2') && i < n && n <= cap2 && + store_uint_array_rec(d, i + 1, cap2, l2') * + store_uint_array(d, i + 1, app(sublist(0, i, l), cons(a, nil))) + */ + d[i] = s[i]; + } } /* 大于返回1，小于返回-1，等于返回0 */ @@ -66,19 +102,53 @@ mpn_cmp (unsigned int *ap, unsigned int *bp, int n) /*@ With cap1 cap2 val1 val2 Require - mpd_store_Z(ap, val1, n, cap1) ** - mpd_store_Z(bp, val2, n, cap2) + mpd_store_Z(ap, val1, n, cap1) * + mpd_store_Z(bp, val2, n, cap2) && + n <= cap1 && n <= cap2 Ensure val1 > val2 && __return == 1 || val1 == val2 && __return == 0 || val1 < val2 && __return == -1 */ { + /*@ + mpd_store_Z(ap, val1, n, cap1) * mpd_store_Z(bp, val2, n, cap2) + which implies + exists l1 l2, + mpd_store_list(ap, l1, cap1) * mpd_store_list(bp, l2, cap2) && + list_store_Z(l1, val1) && list_store_Z(l2, val2) && + n == Zlength(l1) && n == Zlength(l2) + */ + /*@ + Given l1 l2 + */ + --n; + /*@Inv + mpd_store_list(ap, l1, cap1) * mpd_store_list(bp, l2, cap2) && + list_store_Z(l1, val1) && list_store_Z(l2, val2) && + n@pre == Zlength(l1) && n@pre == Zlength(l2) && + sublist(n, n@pre, l1) == sublist(n, n@pre, l2) + */ + while (n >= 0) + { + /*@ + mpd_store_list(ap, l1, cap1) * mpd_store_list(bp, l2, cap2) + which implies + store_uint_array(ap, n, l1) * store_uint_array(bp, n, l2) * + store_undef_uint_array(ap, n + 1, cap1) * store_uint_array(bp, n + 1, cap2) && + */ + if (ap[n] != bp[n]) + return ap[n] > bp[n] ? 1 : -1; + --n; + } + // Note: The parser cannot parse "--n" in loop so we paraphrased it. + /* while (--n >= 0) { if (ap[n] != bp[n]) return ap[n] > bp[n] ? 1 : -1; } + */ return 0; } diff --git a/projects/mini-gmp.h b/projects/mini-gmp.h index 4b50d45..b5a22b5 100755 --- a/projects/mini-gmp.h +++ b/projects/mini-gmp.h @@ -36,7 +36,7 @@ gmp_free_limbs (unsigned int *old, int size); void mpn_copyi (unsigned int *d, unsigned int *s, int n); -int mpn_cmp (unsigned int *, unsigned int *, int); +int mpn_cmp (unsigned int *ap, unsigned int *bp, int n); unsigned int mpn_add_1 (unsigned int *, unsigned int *, int, unsigned int); unsigned int mpn_add_n (unsigned int *, unsigned int *, unsigned int *, int); @@ -59,7 +59,9 @@ void mpz_sub (mpz_t, const mpz_t, const mpz_t); void mpz_set (mpz_t, const mpz_t); /*@ - Extern Coq (Zabs: Z -> Z) - (Zmax: Z -> Z -> Z) - (mpd_store_Z: Z -> Z -> Z -> Z -> Assertion) + Extern Coq (Zabs : Z -> Z) + (Zmax : Z -> Z -> Z) + (mpd_store_Z : Z -> Z -> Z -> Z -> Assertion) + (mpd_store_list : Z -> list Z -> Z -> Assertion) + (list_store_Z : list Z -> Z -> Prop) */ \ No newline at end of file diff --git a/projects/uint_array.strategies b/projects/uint_array.strategies index a8e3822..00feb3f 100644 --- a/projects/uint_array.strategies +++ b/projects/uint_array.strategies @@ -9,7 +9,7 @@ id : 1 priority : core(1) left : store_uint_array(?p, ?n, ?l) at 0 -right : data_at(?p + (?i * sizeof(I32)), I32, ?v) at 1 +right : data_at(?p + (?i * sizeof(U32)), U32, ?v) at 1 check : infer(0 <= i); infer(i < n); action : right_erase(1); @@ -20,7 +20,7 @@ action : right_erase(1); id : 2 priority : post(1) left : store_uint_array_missing_i_rec(?p, ?i, 0, ?n, ?l) at 0 - data_at(p + i * sizeof(I32), I32, l[i]) at 1 + data_at(p + i * sizeof(U32), U32, l[i]) at 1 check : infer(0 <= i); infer(i < n); action : left_erase(1); @@ -30,7 +30,7 @@ action : left_erase(1); id : 3 priority : post(3) left : store_uint_array_missing_i_rec(?p, ?i, 0, ?n, ?l) at 0 - data_at(p + i * sizeof(I32), I32, ?v) at 1 + data_at(p + i * sizeof(U32), U32, ?v) at 1 check : infer(0 <= i); infer(i < n); action : left_erase(1); @@ -65,7 +65,7 @@ action : right_erase(1); id : 7 priority : core(1) left : store_uint_array_rec(?p, ?x, ?y, ?l) at 0 -right : data_at(?p + (?i * sizeof(I32)), I32, ?v) at 1 +right : data_at(?p + (?i * sizeof(U32)), U32, ?v) at 1 check : infer(x <= i); infer(i < y); action : right_erase(1); @@ -108,7 +108,7 @@ action : right_erase(0); id : 11 priority : post(1) left : store_uint_array_missing_i_rec(?p, ?i, ?x, ?y, ?l) at 0 - data_at(p + ?i * sizeof(I32), I32, l[?i - ?x]) at 1 + data_at(p + ?i * sizeof(U32), U32, l[?i - ?x]) at 1 check : infer(x <= i); infer(i < y); action : left_erase(1); @@ -118,7 +118,7 @@ action : left_erase(1); id : 12 priority : post(4) left : store_uint_array_missing_i_rec(?p, ?i, ?x, ?y, ?l) at 0 - data_at(p + ?i * sizeof(I32), I32, ?v) at 1 + data_at(p + ?i * sizeof(U32), U32, ?v) at 1 check : infer(x <= i); infer(i < y); action : left_erase(1); From 36204b8877b34f147edb48fe4367edd078c70137 Mon Sep 17 00:00:00 2001 From: xiaoh105 Date: Wed, 11 Jun 2025 16:54:36 +0800 Subject: [PATCH 4/6] feat(cmp): Proved correctness of mpn_cmp. --- projects/lib/GmpAux.v | 11 + projects/lib/GmpNumber.v | 100 ++++++ projects/lib/gmp_goal.v | 574 +++++++++++++++++++++++++++++++- projects/lib/gmp_goal_check.v | 4 +- projects/lib/gmp_proof_auto.v | 30 ++ projects/lib/gmp_proof_manual.v | 91 +++++ projects/mini-gmp.c | 32 +- 7 files changed, 824 insertions(+), 18 deletions(-) diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index 6d4d524..40a1bcb 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -101,6 +101,17 @@ Proof. reflexivity. Qed. +Lemma list_app_single_l: forall (l: list Z) (a: Z), + ([a] ++ l)%list = a :: l. +Proof. + intros. + induction l. + + simpl; reflexivity. + + rewrite list_app_cons. + simpl. + reflexivity. +Qed. + Lemma store_array_rec_false: forall x storeA lo hi (l: list Z), lo > hi -> store_array_rec storeA x lo hi l |-- [| False |]. diff --git a/projects/lib/GmpNumber.v b/projects/lib/GmpNumber.v index 9ba0593..d6dacae 100755 --- a/projects/lib/GmpNumber.v +++ b/projects/lib/GmpNumber.v @@ -49,6 +49,19 @@ Definition mpd_store_Z (ptr: addr) (n: Z) (size: Z) (cap: Z): Assertion := EX data, mpd_store_list ptr data cap && [| list_store_Z data n |] && [| size = Zlength data |]. +Lemma list_store_Z_injection: forall l1 l2 n1 n2, + list_store_Z l1 n1 -> + list_store_Z l2 n2 -> + l1 = l2 -> n1 = n2. +Proof. + intros. + unfold list_store_Z in *. + destruct H, H0. + rewrite <-H, <-H0. + rewrite <-H1. + reflexivity. +Qed. + Lemma __list_within_bound_concat_r: forall (l1: list Z) (a: Z), list_within_bound l1 -> 0 <= a < UINT_MOD -> @@ -350,6 +363,93 @@ Proof. reflexivity. Qed. +Lemma list_store_Z_cmp: forall l1 l2 n1 n2 i, + 0 <= i < Zlength l1 -> + Zlength l1 = Zlength l2 -> + list_store_Z l1 n1 -> + list_store_Z l2 n2 -> + sublist (i + 1) (Zlength l1) l1 = sublist (i + 1) (Zlength l2) l2 -> + Znth i l1 0 < Znth i l2 0 -> + n1 < n2. +Proof. + intros. + assert (Zlength l1 = Z.of_nat (Datatypes.length l1)). { apply Zlength_correct. } + pose proof (sublist_split 0 (Zlength l1) i l1 ltac:(lia) ltac:(lia)). + assert (Zlength l2 = Z.of_nat (Datatypes.length l2)). { apply Zlength_correct. } + pose proof (sublist_split 0 (Zlength l2) i l2 ltac:(lia) ltac:(lia)). + clear H5 H7. + rewrite (sublist_self l1 (Zlength l1) ltac:(lia)) in H6. + rewrite (sublist_self l2 (Zlength l2) ltac:(lia)) in H8. + rewrite H6 in H1. + rewrite H8 in H2. + apply list_store_Z_split in H1, H2. + remember (Zlength l1) as n eqn:Hn. + assert (Zlength l2 = n). { lia. } + rewrite H5 in *. + rewrite Zlength_sublist0 in H1, H2; try lia. + destruct H1, H2. + remember (n1 mod UINT_MOD ^ i) as n1_lo eqn:Hn1_lo. + remember (n1 / UINT_MOD ^ i) as n1_hi eqn:Hn1_hi. + remember (n2 mod UINT_MOD ^ i) as n2_lo eqn:Hn2_lo. + remember (n2 / UINT_MOD ^ i) as n2_hi eqn:Hn2_hi. + remember (sublist 0 i l1) as l1_lo eqn:Hl1_lo. + remember (sublist i n l1) as l1_hi eqn:Hl1_hi. + remember (sublist 0 i l2) as l2_lo eqn:Hl2_lo. + remember (sublist i n l2) as l2_hi eqn:Hl2_hi. + assert (n1_lo - n2_lo < UINT_MOD ^ i). { + pose proof (list_store_Z_bound l1_lo n1_lo H1). + pose proof (list_store_Z_bound l2_lo n2_lo H2). + rewrite Hl1_lo, Zlength_sublist0 in H10; lia. + } + assert (n2_hi - n1_hi >= 1). { + assert (Zlength l1_hi >= 1 /\ Zlength l2_hi >= 1). { + pose proof (Zlength_sublist i n l1 ltac:(lia)). + pose proof (Zlength_sublist i n l2 ltac:(lia)). + rewrite <-Hl1_hi in H11. + rewrite <-Hl2_hi in H12. + lia. + } + destruct H11. + destruct l1_hi, l2_hi; try rewrite Zlength_nil in *; try lia. + unfold list_store_Z in H7, H9. + destruct H7, H9. + simpl in H7, H9. + assert (forall a (l0 l: list Z), + a :: l0 = sublist i n l -> + Zlength l = n -> + l0 = sublist (i + 1) n l /\ a = Znth i l 0 + ). { + intros. + assert (n = Z.of_nat(Datatypes.length l)). { rewrite <-Zlength_correct. lia. } + pose proof (sublist_split i n (i + 1) l ltac:(lia) ltac:(lia)). + rewrite (sublist_single i l 0) in H18; try lia. + rewrite <-H15 in H18. + rewrite Aux.list_app_single_l in H18. + injection H18; intros. + rewrite H19, H20. + split; reflexivity. + } + pose proof (H15 z0 l2_hi l2 Hl2_hi ltac:(lia)). + specialize (H15 z l1_hi l1 Hl1_hi ltac:(lia)). + destruct H15, H16. + rewrite H15, H17 in H7. + rewrite H16, H18 in H9. + rewrite <-H3 in H9. + lia. + } + pose proof (Zmod_eq_full n1 (UINT_MOD ^ i) ltac:(lia)). + pose proof (Zmod_eq_full n2 (UINT_MOD ^ i) ltac:(lia)). + rewrite <-Hn1_lo, <-Hn1_hi in H12. + rewrite <-Hn2_lo, <-Hn2_hi in H13. + assert (n2_hi * UINT_MOD ^ i - n1_hi * UINT_MOD ^ i >= UINT_MOD ^ i). { + rewrite <-Z.mul_sub_distr_r. + pose proof (Zmult_ge_compat_r (n2_hi - n1_hi) 1 (UINT_MOD ^ i) ltac:(lia) ltac:(lia)). + rewrite Z.mul_1_l in H14. + lia. + } + lia. +Qed. + End Internal. Record bigint_ent: Type := { diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v index 0456f92..0b3e985 100644 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -9,8 +9,8 @@ Require Import Coq.Sorting.Permutation. From AUXLib Require Import int_auto Axioms Feq Idents List_lemma VMap. Require Import SetsClass.SetsClass. Import SetsNotation. From SimpleC.SL Require Import Mem SeparationLogic. -Require Import GmpLib.GmpNumber. Import Internal. Require Import Logic.LogicGenerator.demo932.Interface. +Require Import GmpLib.GmpNumber. Import Internal. Local Open Scope Z_scope. Local Open Scope sets. Local Open Scope string. @@ -591,6 +591,562 @@ forall (cap2: Z) (l': (@list Z)) (l: (@list Z)) (i: Z) (n: Z) (d: Z) , ** (store_uint_array d (i + 1 ) (app ((sublist (0) (i) (l))) ((cons (a) (nil)))) ) . +(*----- Function mpn_cmp -----*) + +Definition mpn_cmp_safety_wit_1 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) , + [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array ap_pre n_pre l1 ) + ** (store_uint_array bp_pre n_pre l2 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** ((( &( "n" ) )) # Int |-> n_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) +|-- + [| ((n_pre - 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (n_pre - 1 )) |] +. + +Definition mpn_cmp_safety_wit_2 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) (n: Z) , + [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && ((( &( "n" ) )) # Int |-> n) + ** (store_uint_array ap_pre n_pre l1 ) + ** (store_uint_array bp_pre n_pre l2 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) +|-- + [| (0 <= INT_MAX) |] + && [| ((INT_MIN) <= 0) |] +. + +Definition mpn_cmp_safety_wit_3 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) (n: Z) , + [| ((Znth n l1 0) <= (Znth n l2 0)) |] + && [| ((Znth n l1 0) <> (Znth n l2 0)) |] + && [| (n >= 0) |] + && [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array bp_pre n_pre l2 ) + ** (store_uint_array ap_pre n_pre l1 ) + ** ((( &( "n" ) )) # Int |-> n) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) +|-- + [| (1 <> (INT_MIN)) |] +. + +Definition mpn_cmp_safety_wit_4 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) (n: Z) , + [| ((Znth n l1 0) <= (Znth n l2 0)) |] + && [| ((Znth n l1 0) <> (Znth n l2 0)) |] + && [| (n >= 0) |] + && [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array bp_pre n_pre l2 ) + ** (store_uint_array ap_pre n_pre l1 ) + ** ((( &( "n" ) )) # Int |-> n) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) +|-- + [| (1 <= INT_MAX) |] + && [| ((INT_MIN) <= 1) |] +. + +Definition mpn_cmp_safety_wit_5 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) (n: Z) , + [| ((Znth n l1 0) > (Znth n l2 0)) |] + && [| ((Znth n l1 0) <> (Znth n l2 0)) |] + && [| (n >= 0) |] + && [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array bp_pre n_pre l2 ) + ** (store_uint_array ap_pre n_pre l1 ) + ** ((( &( "n" ) )) # Int |-> n) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) +|-- + [| (1 <= INT_MAX) |] + && [| ((INT_MIN) <= 1) |] +. + +Definition mpn_cmp_safety_wit_6 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) (n: Z) , + [| ((Znth n l1 0) = (Znth n l2 0)) |] + && [| (n >= 0) |] + && [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array bp_pre n_pre l2 ) + ** (store_uint_array ap_pre n_pre l1 ) + ** ((( &( "n" ) )) # Int |-> n) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) +|-- + [| ((n - 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (n - 1 )) |] +. + +Definition mpn_cmp_safety_wit_7 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) (n: Z) , + [| (n < 0) |] + && [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && ((( &( "n" ) )) # Int |-> n) + ** (store_uint_array ap_pre n_pre l1 ) + ** (store_uint_array bp_pre n_pre l2 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) +|-- + [| (0 <= INT_MAX) |] + && [| ((INT_MIN) <= 0) |] +. + +Definition mpn_cmp_entail_wit_1 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) , + [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array ap_pre n_pre l1 ) + ** (store_uint_array bp_pre n_pre l2 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) +|-- + [| ((-1) <= (n_pre - 1 )) |] + && [| ((n_pre - 1 ) < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist (((n_pre - 1 ) + 1 )) (n_pre) (l1)) = (sublist (((n_pre - 1 ) + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array ap_pre n_pre l1 ) + ** (store_uint_array bp_pre n_pre l2 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) +. + +Definition mpn_cmp_entail_wit_2 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) (n: Z) , + [| ((Znth n l1 0) = (Znth n l2 0)) |] + && [| (n >= 0) |] + && [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array bp_pre n_pre l2 ) + ** (store_uint_array ap_pre n_pre l1 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) +|-- + [| ((-1) <= (n - 1 )) |] + && [| ((n - 1 ) < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist (((n - 1 ) + 1 )) (n_pre) (l1)) = (sublist (((n - 1 ) + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array ap_pre n_pre l1 ) + ** (store_uint_array bp_pre n_pre l2 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) +. + +Definition mpn_cmp_return_wit_1_1 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) (n: Z) , + [| ((Znth n l1 0) <= (Znth n l2 0)) |] + && [| ((Znth n l1 0) <> (Znth n l2 0)) |] + && [| (n >= 0) |] + && [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array bp_pre n_pre l2 ) + ** (store_uint_array ap_pre n_pre l1 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) +|-- + ([| (val1 < val2) |] + && [| ((-1) = (-1)) |] + && (mpd_store_Z ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + || + ([| (val1 = val2) |] + && [| ((-1) = 0) |] + && (mpd_store_Z ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + || + ([| (val1 > val2) |] + && [| ((-1) = 1) |] + && (mpd_store_Z ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z bp_pre val2 n_pre cap2 )) +. + +Definition mpn_cmp_return_wit_1_2 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) (n: Z) , + [| ((Znth n l1 0) > (Znth n l2 0)) |] + && [| ((Znth n l1 0) <> (Znth n l2 0)) |] + && [| (n >= 0) |] + && [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array bp_pre n_pre l2 ) + ** (store_uint_array ap_pre n_pre l1 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) +|-- + ([| (val1 < val2) |] + && [| (1 = (-1)) |] + && (mpd_store_Z ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + || + ([| (val1 = val2) |] + && [| (1 = 0) |] + && (mpd_store_Z ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + || + ([| (val1 > val2) |] + && [| (1 = 1) |] + && (mpd_store_Z ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z bp_pre val2 n_pre cap2 )) +. + +Definition mpn_cmp_return_wit_2 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) (n: Z) , + [| (n < 0) |] + && [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array ap_pre n_pre l1 ) + ** (store_uint_array bp_pre n_pre l2 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) +|-- + ([| (val1 < val2) |] + && [| (0 = (-1)) |] + && (mpd_store_Z ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + || + ([| (val1 = val2) |] + && [| (0 = 0) |] + && (mpd_store_Z ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + || + ([| (val1 > val2) |] + && [| (0 = 1) |] + && (mpd_store_Z ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z bp_pre val2 n_pre cap2 )) +. + +Definition mpn_cmp_partial_solve_wit_1 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) , + [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (mpd_store_Z ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z bp_pre val2 n_pre cap2 ) +|-- + [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (mpd_store_Z ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z bp_pre val2 n_pre cap2 ) +. + +Definition mpn_cmp_partial_solve_wit_2 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) (n: Z) , + [| (n >= 0) |] + && [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array ap_pre n_pre l1 ) + ** (store_uint_array bp_pre n_pre l2 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) +|-- + [| (n >= 0) |] + && [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (((ap_pre + (n * sizeof(UINT) ) )) # UInt |-> (Znth n l1 0)) + ** (store_uint_array_missing_i_rec ap_pre n 0 n_pre l1 ) + ** (store_uint_array bp_pre n_pre l2 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) +. + +Definition mpn_cmp_partial_solve_wit_3 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) (n: Z) , + [| (n >= 0) |] + && [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (store_uint_array ap_pre n_pre l1 ) + ** (store_uint_array bp_pre n_pre l2 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) +|-- + [| (n >= 0) |] + && [| ((-1) <= n) |] + && [| (n < n_pre) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] + && [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && [| (0 < n_pre) |] + && [| (n_pre <= cap1) |] + && [| (n_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (((bp_pre + (n * sizeof(UINT) ) )) # UInt |-> (Znth n l2 0)) + ** (store_uint_array_missing_i_rec bp_pre n 0 n_pre l2 ) + ** (store_uint_array ap_pre n_pre l1 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) +. + +Definition mpn_cmp_which_implies_wit_1 := +forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) , + (mpd_store_Z ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z bp_pre val2 n_pre cap2 ) +|-- + EX (l2: (@list Z)) (l1: (@list Z)) , + [| (list_store_Z l1 val1 ) |] + && [| (list_store_Z l2 val2 ) |] + && [| (n_pre = (Zlength (l1))) |] + && [| (n_pre = (Zlength (l2))) |] + && (store_uint_array ap_pre n_pre l1 ) + ** (store_uint_array bp_pre n_pre l2 ) + ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) +. + Module Type VC_Correct. Axiom proof_of_gmp_abs_safety_wit_1 : gmp_abs_safety_wit_1. @@ -620,5 +1176,21 @@ Axiom proof_of_mpn_copyi_partial_solve_wit_5 : mpn_copyi_partial_solve_wit_5. Axiom proof_of_mpn_copyi_which_implies_wit_1 : mpn_copyi_which_implies_wit_1. Axiom proof_of_mpn_copyi_which_implies_wit_2 : mpn_copyi_which_implies_wit_2. Axiom proof_of_mpn_copyi_which_implies_wit_3 : mpn_copyi_which_implies_wit_3. +Axiom proof_of_mpn_cmp_safety_wit_1 : mpn_cmp_safety_wit_1. +Axiom proof_of_mpn_cmp_safety_wit_2 : mpn_cmp_safety_wit_2. +Axiom proof_of_mpn_cmp_safety_wit_3 : mpn_cmp_safety_wit_3. +Axiom proof_of_mpn_cmp_safety_wit_4 : mpn_cmp_safety_wit_4. +Axiom proof_of_mpn_cmp_safety_wit_5 : mpn_cmp_safety_wit_5. +Axiom proof_of_mpn_cmp_safety_wit_6 : mpn_cmp_safety_wit_6. +Axiom proof_of_mpn_cmp_safety_wit_7 : mpn_cmp_safety_wit_7. +Axiom proof_of_mpn_cmp_entail_wit_1 : mpn_cmp_entail_wit_1. +Axiom proof_of_mpn_cmp_entail_wit_2 : mpn_cmp_entail_wit_2. +Axiom proof_of_mpn_cmp_return_wit_1_1 : mpn_cmp_return_wit_1_1. +Axiom proof_of_mpn_cmp_return_wit_1_2 : mpn_cmp_return_wit_1_2. +Axiom proof_of_mpn_cmp_return_wit_2 : mpn_cmp_return_wit_2. +Axiom proof_of_mpn_cmp_partial_solve_wit_1 : mpn_cmp_partial_solve_wit_1. +Axiom proof_of_mpn_cmp_partial_solve_wit_2 : mpn_cmp_partial_solve_wit_2. +Axiom proof_of_mpn_cmp_partial_solve_wit_3 : mpn_cmp_partial_solve_wit_3. +Axiom proof_of_mpn_cmp_which_implies_wit_1 : mpn_cmp_which_implies_wit_1. End VC_Correct. diff --git a/projects/lib/gmp_goal_check.v b/projects/lib/gmp_goal_check.v index 43755db..81ae445 100644 --- a/projects/lib/gmp_goal_check.v +++ b/projects/lib/gmp_goal_check.v @@ -1,6 +1,6 @@ -From Require Import gmp_goal gmp_proof_auto gmp_proof_manual. +From Require Import gmp_goal gmp_proof_auto gmp_proof_manual_tmp. Module VC_Correctness : VC_Correct. Include gmp_proof_auto. - Include gmp_proof_manual. + Include gmp_proof_manual_tmp. End VC_Correctness. diff --git a/projects/lib/gmp_proof_auto.v b/projects/lib/gmp_proof_auto.v index 1cb2659..300c3f1 100644 --- a/projects/lib/gmp_proof_auto.v +++ b/projects/lib/gmp_proof_auto.v @@ -63,3 +63,33 @@ Proof. Admitted. Lemma proof_of_mpn_copyi_partial_solve_wit_5 : mpn_copyi_partial_solve_wit_5. Proof. Admitted. +Lemma proof_of_mpn_cmp_safety_wit_1 : mpn_cmp_safety_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_cmp_safety_wit_2 : mpn_cmp_safety_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_cmp_safety_wit_3 : mpn_cmp_safety_wit_3. +Proof. Admitted. + +Lemma proof_of_mpn_cmp_safety_wit_4 : mpn_cmp_safety_wit_4. +Proof. Admitted. + +Lemma proof_of_mpn_cmp_safety_wit_5 : mpn_cmp_safety_wit_5. +Proof. Admitted. + +Lemma proof_of_mpn_cmp_safety_wit_6 : mpn_cmp_safety_wit_6. +Proof. Admitted. + +Lemma proof_of_mpn_cmp_safety_wit_7 : mpn_cmp_safety_wit_7. +Proof. Admitted. + +Lemma proof_of_mpn_cmp_partial_solve_wit_1 : mpn_cmp_partial_solve_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_cmp_partial_solve_wit_2 : mpn_cmp_partial_solve_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_cmp_partial_solve_wit_3 : mpn_cmp_partial_solve_wit_3. +Proof. Admitted. + diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 5fbd764..5278efd 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -149,4 +149,95 @@ Proof. rewrite H5 in H4; clear H5. rewrite <-H4. sep_apply store_uint_array_rec_tail_merge; [ reflexivity | lia ]. +Qed. + +Lemma proof_of_mpn_cmp_safety_wit_1 : mpn_cmp_safety_wit_1. +Proof. + pre_process. +Qed. + +Lemma proof_of_mpn_cmp_entail_wit_1 : mpn_cmp_entail_wit_1. +Proof. + pre_process. + entailer!. + assert (n_pre - 1 + 1 = n_pre). { lia. } + rewrite H8; clear H8. + pose proof (Zlength_sublist n_pre n_pre l1 ltac:(lia)). + pose proof (Zlength_nil_inv (sublist n_pre n_pre l1) ltac:(lia)). + rewrite H9. + pose proof (Zlength_sublist n_pre n_pre l2 ltac:(lia)). + pose proof (Zlength_nil_inv (sublist n_pre n_pre l2) ltac:(lia)). + rewrite H11. + reflexivity. +Qed. + +Lemma proof_of_mpn_cmp_entail_wit_2 : mpn_cmp_entail_wit_2. +Proof. + pre_process. + entailer!; try lia. + assert (n - 1 + 1 = n). { lia. } + rewrite H17; clear H17. + assert (n_pre <= Z.of_nat (Datatypes.length l1)). { + rewrite <-Zlength_correct. + lia. + } + assert (n_pre <= Z.of_nat (Datatypes.length l2)). { + rewrite <-Zlength_correct. + lia. + } + rewrite (sublist_split n n_pre (n + 1) l1 ltac:(lia) ltac:(lia)). + rewrite (sublist_split n n_pre (n + 1) l2 ltac:(lia) ltac:(lia)). + rewrite (sublist_single n l1 0 ltac:(lia)). + rewrite (sublist_single n l2 0 ltac:(lia)). + rewrite H. + rewrite H7. + reflexivity. +Qed. + +Lemma proof_of_mpn_cmp_return_wit_1_1 : mpn_cmp_return_wit_1_1. +Proof. + pre_process. + entailer!. + repeat rewrite <-derivable1_orp_intros1. + entailer!. + + unfold mpd_store_Z. + Exists l1 l2. + unfold mpd_store_list. + entailer!. + rewrite <-H6, <-H7. + entailer!. + + assert (Znth n l1 0 < Znth n l2 0). { lia. } + clear H H0. + apply (list_store_Z_cmp l1 l2 val1 val2 n ltac:(lia) ltac:(lia) H4 H5). + - rewrite <-H6, <-H7. + tauto. + - lia. +Qed. + +Lemma proof_of_mpn_cmp_return_wit_1_2 : mpn_cmp_return_wit_1_2. +Proof. + pre_process. + rewrite <-derivable1_orp_intros2. + entailer!. + + unfold mpd_store_Z, mpd_store_list. + Exists l1 l2. + rewrite <-H6, <-H7. + entailer!. + + pose proof (list_store_Z_cmp l2 l1 val2 val1 n ltac:(lia) ltac:(lia) H5 H4). + rewrite <-H6, <-H7 in H18. + rewrite H8 in H18. + specialize (H18 ltac:(reflexivity) ltac:(lia)). + lia. +Qed. + +Lemma proof_of_mpn_cmp_which_implies_wit_1 : mpn_cmp_which_implies_wit_1. +Proof. + pre_process. + unfold mpd_store_Z. + Intros l1 l2. + Exists l2 l1. + unfold mpd_store_list. + entailer!. + rewrite <-H4, <-H6. + entailer!. Qed. \ No newline at end of file diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 734d342..1f69d74 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -104,44 +104,46 @@ mpn_cmp (unsigned int *ap, unsigned int *bp, int n) Require mpd_store_Z(ap, val1, n, cap1) * mpd_store_Z(bp, val2, n, cap2) && - n <= cap1 && n <= cap2 + 0 < n && n <= cap1 && n <= cap2 && + cap1 <= 100000000 && cap2 <= 100000000 Ensure - val1 > val2 && __return == 1 || + (val1 > val2 && __return == 1 || val1 == val2 && __return == 0 || - val1 < val2 && __return == -1 + val1 < val2 && __return == -1) && + mpd_store_Z(ap@pre, val1, n@pre, cap1) * + mpd_store_Z(bp@pre, val2, n@pre, cap2) */ { /*@ - mpd_store_Z(ap, val1, n, cap1) * mpd_store_Z(bp, val2, n, cap2) + mpd_store_Z(ap@pre, val1, n@pre, cap1) * mpd_store_Z(bp@pre, val2, n@pre, cap2) which implies exists l1 l2, - mpd_store_list(ap, l1, cap1) * mpd_store_list(bp, l2, cap2) && + store_uint_array(ap@pre, n@pre, l1) * store_uint_array(bp@pre, n@pre, l2) * + store_undef_uint_array_rec(ap@pre, n@pre + 1, cap1) * + store_undef_uint_array_rec(bp@pre, n@pre + 1, cap2) && list_store_Z(l1, val1) && list_store_Z(l2, val2) && - n == Zlength(l1) && n == Zlength(l2) + n@pre == Zlength(l1) && n@pre == Zlength(l2) */ /*@ Given l1 l2 */ --n; /*@Inv - mpd_store_list(ap, l1, cap1) * mpd_store_list(bp, l2, cap2) && + -1 <= n && n < n@pre && + store_uint_array(ap@pre, n@pre, l1) * store_uint_array(bp@pre, n@pre, l2) * + store_undef_uint_array_rec(ap@pre, n@pre + 1, cap1) * + store_undef_uint_array_rec(bp@pre, n@pre + 1, cap2) && list_store_Z(l1, val1) && list_store_Z(l2, val2) && n@pre == Zlength(l1) && n@pre == Zlength(l2) && - sublist(n, n@pre, l1) == sublist(n, n@pre, l2) + sublist(n + 1, n@pre, l1) == sublist(n + 1, n@pre, l2) */ while (n >= 0) { - /*@ - mpd_store_list(ap, l1, cap1) * mpd_store_list(bp, l2, cap2) - which implies - store_uint_array(ap, n, l1) * store_uint_array(bp, n, l2) * - store_undef_uint_array(ap, n + 1, cap1) * store_uint_array(bp, n + 1, cap2) && - */ if (ap[n] != bp[n]) return ap[n] > bp[n] ? 1 : -1; --n; } - // Note: The parser cannot parse "--n" in loop so we paraphrased it. + // Note: The parser cannot parse "--n" in loop condition so we paraphrased it. /* while (--n >= 0) { From f7432dca8412fb96a4736f9581146b3f933ab519 Mon Sep 17 00:00:00 2001 From: xiaoh105 Date: Thu, 12 Jun 2025 12:37:01 +0800 Subject: [PATCH 5/6] feat(cmp4): modied certain annotations for mpn_cmp and proved correctness of mpn_cmp4. --- projects/lib/GmpAux.v | 61 ++++ projects/lib/GmpNumber.v | 118 ++++++- projects/lib/gmp_goal.v | 569 +++++++++++++++++++++++++------- projects/lib/gmp_proof_auto.v | 24 ++ projects/lib/gmp_proof_manual.v | 72 +++- projects/mini-gmp.c | 107 +++--- projects/mini-gmp.h | 3 + 7 files changed, 788 insertions(+), 166 deletions(-) diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index 40a1bcb..326dbc1 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -112,6 +112,67 @@ Proof. reflexivity. Qed. +Lemma list_last_cons: forall (a: Z) (l: list Z), + l <> nil -> + last (a :: l) 0 = last l 0. +Proof. + intros. + destruct l. + + contradiction. + + simpl. + reflexivity. +Qed. + +Lemma list_last_to_Znth: forall (l: list Z), + l <> nil -> + last l 0 = Znth ((Zlength l) - 1) l 0. +Proof. + intros. + induction l. + + auto. + + destruct l. + - simpl. + rewrite Znth0_cons. + lia. + - pose proof (@nil_cons Z z l). + specialize (IHl ltac:(auto)); clear H0. + rewrite list_last_cons; [ | pose proof (@nil_cons Z z l); auto ]. + rewrite IHl. + pose proof (Zlength_cons a (z :: l)). + unfold Z.succ in H0; rewrite H0; clear H0. + pose proof (Zlength_nonneg l). + pose proof (Zlength_cons z l); unfold Z.succ in H1. + pose proof (Znth_cons (Zlength (z :: l)) a (z :: l) 0 ltac:(lia)). + assert (Zlength (z :: l) + 1 - 1 = Zlength (z :: l)). { lia. } + rewrite H3; clear H3. + rewrite H2. + reflexivity. +Qed. + +Lemma Zlength_removelast: forall (l: list Z), + l <> [] -> + Zlength (removelast l) = Zlength l - 1. +Proof. + intros. + induction l. + + contradiction. + + destruct l. + - simpl. + rewrite Zlength_nil. + lia. + - pose proof (@nil_cons Z z l). + specialize (IHl ltac:(auto)). + assert (removelast (a :: z :: l) = a :: removelast(z :: l)). { + simpl. + reflexivity. + } + rewrite H1; clear H1. + repeat rewrite Zlength_cons; unfold Z.succ. + rewrite IHl. + rewrite Zlength_cons; unfold Z.succ. + lia. +Qed. + Lemma store_array_rec_false: forall x storeA lo hi (l: list Z), lo > hi -> store_array_rec storeA x lo hi l |-- [| False |]. diff --git a/projects/lib/GmpNumber.v b/projects/lib/GmpNumber.v index d6dacae..8c2e754 100755 --- a/projects/lib/GmpNumber.v +++ b/projects/lib/GmpNumber.v @@ -47,7 +47,34 @@ Definition list_store_Z (data: list Z) (n: Z): Prop := Definition mpd_store_Z (ptr: addr) (n: Z) (size: Z) (cap: Z): Assertion := EX data, - mpd_store_list ptr data cap && [| list_store_Z data n |] && [| size = Zlength data |]. + [| list_store_Z data n |] && [| size = Zlength data |] && mpd_store_list ptr data cap. + +Definition list_store_Z_compact (data: list Z) (n: Z): Prop := + list_to_Z data = n /\ last data 0 >= 1 /\ list_within_bound data. + +Definition mpd_store_Z_compact (ptr: addr) (n size cap: Z): Assertion := + EX data, + [| list_store_Z_compact data n |] && [| size = Zlength data |] && mpd_store_list ptr data cap. + +Lemma list_store_Z_normal_to_compact: forall (data: list Z) (n: Z), + list_store_Z data n -> + last data 0 >= 1 -> + list_store_Z_compact data n. +Proof. + unfold list_store_Z_compact, list_store_Z. + intros. + tauto. +Qed. + +Lemma list_store_Z_compact_to_normal: forall data n, + list_store_Z_compact data n -> + list_store_Z data n. +Proof. + intros. + unfold list_store_Z_compact in H. + unfold list_store_Z. + tauto. +Qed. Lemma list_store_Z_injection: forall l1 l2 n1 n2, list_store_Z l1 n1 -> @@ -450,6 +477,95 @@ Proof. lia. Qed. +Lemma list_store_Z_compact_cmp: forall l1 l2 n1 n2 i, + 0 <= i < Zlength l1 -> + Zlength l1 = Zlength l2 -> + list_store_Z_compact l1 n1 -> + list_store_Z_compact l2 n2 -> + sublist (i + 1) (Zlength l1) l1 = sublist (i + 1) (Zlength l2) l2 -> + Znth i l1 0 < Znth i l2 0 -> + n1 < n2. +Proof. + intros. + apply list_store_Z_compact_to_normal in H1, H2. + apply (list_store_Z_cmp l1 l2 n1 n2 i); tauto. +Qed. + +Lemma list_store_Z_cmp_length: forall l1 l2 n1 n2, + Zlength l1 < Zlength l2 -> + list_store_Z_compact l1 n1 -> + list_store_Z_compact l2 n2 -> + n1 < n2. +Proof. + intros. + unfold list_store_Z_compact in *. + destruct H0, H1, H2, H3. + assert (list_store_Z l1 n1 /\ list_store_Z l2 n2). { + unfold list_store_Z. + tauto. + } + clear H0 H1 H4 H5. + destruct H6. + assert (l2 <> []). { + pose proof (Zlength_nonneg l1). + assert (Zlength l2 >= 1). { lia. } + destruct l2. + + rewrite Zlength_nil in H5. + lia. + + pose proof (@nil_cons Z z l2). + auto. + } + pose proof (list_store_Z_bound l2 n2 H1) as Hn2. + pose proof (@app_removelast_last Z l2 0 H4). + rewrite H5 in H1. + apply list_store_Z_split in H1; destruct H1. + rewrite (Aux.Zlength_removelast l2) in H1, H6; try auto. + remember (Zlength l2 - 1) as n eqn:Hn. + unfold list_store_Z in H6; destruct H6. + simpl in H6. + assert (n2 >= UINT_MOD ^ n). { + assert (n2 / UINT_MOD ^ n >= 1). { lia. } + pose proof (Zmult_ge_compat_r (n2 / UINT_MOD ^ n) 1 (UINT_MOD ^ n) ltac:(lia) ltac:(lia)). + rewrite Z.mul_1_l in H9. + assert (n2 >= n2 / UINT_MOD ^ n * UINT_MOD ^ n). { + assert (n >= 0). { + destruct l2. + + contradiction. + + rewrite Zlength_cons in Hn; unfold Z.succ in Hn. + pose proof (Zlength_nonneg l2). + lia. + } + pose proof (Zmod_eq n2 (UINT_MOD ^ n) ltac:(lia)). + assert (n2 mod UINT_MOD ^ n >= 0). { + pose proof (Z.mod_bound_pos n2 (UINT_MOD ^ n) ltac:(lia) ltac:(lia)). + lia. + } + lia. + } + lia. + } + assert (Zlength l1 <= n). { lia. } + pose proof (list_store_Z_bound l1 n1 H0). + assert (UINT_MOD ^ n >= UINT_MOD ^ (Zlength l1)). { + assert (Zlength l1 = n \/ Zlength l1 < n). { lia. } + destruct H11. + + rewrite H11. + lia. + + assert (n >= 0). { + destruct l2. + + contradiction. + + rewrite Zlength_cons in Hn; unfold Z.succ in Hn. + pose proof (Zlength_nonneg l2). + lia. + } + pose proof (Z.pow_lt_mono_r_iff UINT_MOD (Zlength l1) n ltac:(lia) ltac:(lia)). + destruct H13 as [H13 _]. + specialize (H13 H11). + lia. + } + lia. +Qed. + End Internal. Record bigint_ent: Type := { diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v index 0b3e985..39ce9b4 100644 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -595,11 +595,11 @@ forall (cap2: Z) (l': (@list Z)) (l: (@list Z)) (i: Z) (n: Z) (d: Z) , Definition mpn_cmp_safety_wit_1 := forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) , - [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -620,16 +620,16 @@ Definition mpn_cmp_safety_wit_2 := forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) (n: Z) , [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -653,16 +653,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (n >= 0) |] && [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -685,16 +685,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (n >= 0) |] && [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -718,16 +718,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (n >= 0) |] && [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -750,16 +750,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (n >= 0) |] && [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -781,16 +781,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z [| (n < 0) |] && [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -809,11 +809,11 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z Definition mpn_cmp_entail_wit_1 := forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (l1: (@list Z)) , - [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -825,16 +825,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z |-- [| ((-1) <= (n_pre - 1 )) |] && [| ((n_pre - 1 ) < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist (((n_pre - 1 ) + 1 )) (n_pre) (l1)) = (sublist (((n_pre - 1 ) + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -851,16 +851,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (n >= 0) |] && [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -872,16 +872,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z |-- [| ((-1) <= (n - 1 )) |] && [| ((n - 1 ) < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist (((n - 1 ) + 1 )) (n_pre) (l1)) = (sublist (((n - 1 ) + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -899,16 +899,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (n >= 0) |] && [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -920,18 +920,18 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z |-- ([| (val1 < val2) |] && [| ((-1) = (-1)) |] - && (mpd_store_Z ap_pre val1 n_pre cap1 ) - ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + && (mpd_store_Z_compact ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 n_pre cap2 )) || ([| (val1 = val2) |] && [| ((-1) = 0) |] - && (mpd_store_Z ap_pre val1 n_pre cap1 ) - ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + && (mpd_store_Z_compact ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 n_pre cap2 )) || ([| (val1 > val2) |] && [| ((-1) = 1) |] - && (mpd_store_Z ap_pre val1 n_pre cap1 ) - ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + && (mpd_store_Z_compact ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 n_pre cap2 )) . Definition mpn_cmp_return_wit_1_2 := @@ -941,16 +941,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (n >= 0) |] && [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -962,18 +962,18 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z |-- ([| (val1 < val2) |] && [| (1 = (-1)) |] - && (mpd_store_Z ap_pre val1 n_pre cap1 ) - ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + && (mpd_store_Z_compact ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 n_pre cap2 )) || ([| (val1 = val2) |] && [| (1 = 0) |] - && (mpd_store_Z ap_pre val1 n_pre cap1 ) - ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + && (mpd_store_Z_compact ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 n_pre cap2 )) || ([| (val1 > val2) |] && [| (1 = 1) |] - && (mpd_store_Z ap_pre val1 n_pre cap1 ) - ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + && (mpd_store_Z_compact ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 n_pre cap2 )) . Definition mpn_cmp_return_wit_2 := @@ -981,16 +981,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z [| (n < 0) |] && [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -1002,37 +1002,37 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z |-- ([| (val1 < val2) |] && [| (0 = (-1)) |] - && (mpd_store_Z ap_pre val1 n_pre cap1 ) - ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + && (mpd_store_Z_compact ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 n_pre cap2 )) || ([| (val1 = val2) |] && [| (0 = 0) |] - && (mpd_store_Z ap_pre val1 n_pre cap1 ) - ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + && (mpd_store_Z_compact ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 n_pre cap2 )) || ([| (val1 > val2) |] && [| (0 = 1) |] - && (mpd_store_Z ap_pre val1 n_pre cap1 ) - ** (mpd_store_Z bp_pre val2 n_pre cap2 )) + && (mpd_store_Z_compact ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 n_pre cap2 )) . Definition mpn_cmp_partial_solve_wit_1 := forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) , - [| (0 < n_pre) |] + [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] && [| (cap2 <= 100000000) |] - && (mpd_store_Z ap_pre val1 n_pre cap1 ) - ** (mpd_store_Z bp_pre val2 n_pre cap2 ) + && (mpd_store_Z_compact ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 n_pre cap2 ) |-- - [| (0 < n_pre) |] + [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] && [| (cap2 <= 100000000) |] - && (mpd_store_Z ap_pre val1 n_pre cap1 ) - ** (mpd_store_Z bp_pre val2 n_pre cap2 ) + && (mpd_store_Z_compact ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 n_pre cap2 ) . Definition mpn_cmp_partial_solve_wit_2 := @@ -1040,16 +1040,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z [| (n >= 0) |] && [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -1062,16 +1062,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z [| (n >= 0) |] && [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -1088,16 +1088,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z [| (n >= 0) |] && [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -1110,16 +1110,16 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z [| (n >= 0) |] && [| ((-1) <= n) |] && [| (n < n_pre) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && [| ((sublist ((n + 1 )) (n_pre) (l1)) = (sublist ((n + 1 )) (n_pre) (l2))) |] - && [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + && [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] - && [| (0 < n_pre) |] + && [| (0 <= n_pre) |] && [| (n_pre <= cap1) |] && [| (n_pre <= cap2) |] && [| (cap1 <= 100000000) |] @@ -1133,12 +1133,12 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z Definition mpn_cmp_which_implies_wit_1 := forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) , - (mpd_store_Z ap_pre val1 n_pre cap1 ) - ** (mpd_store_Z bp_pre val2 n_pre cap2 ) + (mpd_store_Z_compact ap_pre val1 n_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 n_pre cap2 ) |-- EX (l2: (@list Z)) (l1: (@list Z)) , - [| (list_store_Z l1 val1 ) |] - && [| (list_store_Z l2 val2 ) |] + [| (list_store_Z_compact l1 val1 ) |] + && [| (list_store_Z_compact l2 val2 ) |] && [| (n_pre = (Zlength (l1))) |] && [| (n_pre = (Zlength (l2))) |] && (store_uint_array ap_pre n_pre l1 ) @@ -1147,6 +1147,334 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) . +(*----- Function mpn_cmp4 -----*) + +Definition mpn_cmp4_safety_wit_1 := +forall (bn_pre: Z) (bp_pre: Z) (an_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) , + [| (an_pre >= bn_pre) |] + && [| (an_pre <> bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && ((( &( "bn" ) )) # Int |-> bn_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "an" ) )) # Int |-> an_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 ) +|-- + [| (1 <= INT_MAX) |] + && [| ((INT_MIN) <= 1) |] +. + +Definition mpn_cmp4_safety_wit_2 := +forall (bn_pre: Z) (bp_pre: Z) (an_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) , + [| (an_pre < bn_pre) |] + && [| (an_pre <> bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && ((( &( "bn" ) )) # Int |-> bn_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "an" ) )) # Int |-> an_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 ) +|-- + [| (1 <> (INT_MIN)) |] +. + +Definition mpn_cmp4_safety_wit_3 := +forall (bn_pre: Z) (bp_pre: Z) (an_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) , + [| (an_pre < bn_pre) |] + && [| (an_pre <> bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && ((( &( "bn" ) )) # Int |-> bn_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "an" ) )) # Int |-> an_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 ) +|-- + [| (1 <= INT_MAX) |] + && [| ((INT_MIN) <= 1) |] +. + +Definition mpn_cmp4_return_wit_1_1 := +forall (bn_pre: Z) (bp_pre: Z) (an_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) , + [| (an_pre >= bn_pre) |] + && [| (an_pre <> bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 ) +|-- + ([| (val1 < val2) |] + && [| (1 = (-1)) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) + || + ([| (val1 = val2) |] + && [| (1 = 0) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) + || + ([| (val1 > val2) |] + && [| (1 = 1) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) +. + +Definition mpn_cmp4_return_wit_1_2 := +forall (bn_pre: Z) (bp_pre: Z) (an_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) , + [| (an_pre < bn_pre) |] + && [| (an_pre <> bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 ) +|-- + ([| (val1 < val2) |] + && [| ((-1) = (-1)) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) + || + ([| (val1 = val2) |] + && [| ((-1) = 0) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) + || + ([| (val1 > val2) |] + && [| ((-1) = 1) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) +. + +Definition mpn_cmp4_return_wit_2_1 := +forall (bn_pre: Z) (bp_pre: Z) (an_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (retval: Z) , + [| (val1 > val2) |] + && [| (retval = 1) |] + && [| (an_pre <= cap2) |] + && [| (an_pre = bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 an_pre cap2 ) +|-- + ([| (val1 < val2) |] + && [| (retval = (-1)) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) + || + ([| (val1 = val2) |] + && [| (retval = 0) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) + || + ([| (val1 > val2) |] + && [| (retval = 1) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) +. + +Definition mpn_cmp4_return_wit_2_2 := +forall (bn_pre: Z) (bp_pre: Z) (an_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (retval: Z) , + [| (val1 = val2) |] + && [| (retval = 0) |] + && [| (an_pre <= cap2) |] + && [| (an_pre = bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 an_pre cap2 ) +|-- + ([| (val1 < val2) |] + && [| (retval = (-1)) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) + || + ([| (val1 = val2) |] + && [| (retval = 0) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) + || + ([| (val1 > val2) |] + && [| (retval = 1) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) +. + +Definition mpn_cmp4_return_wit_2_3 := +forall (bn_pre: Z) (bp_pre: Z) (an_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) (retval: Z) , + [| (val1 < val2) |] + && [| (retval = (-1)) |] + && [| (an_pre <= cap2) |] + && [| (an_pre = bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 an_pre cap2 ) +|-- + ([| (val1 < val2) |] + && [| (retval = (-1)) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) + || + ([| (val1 = val2) |] + && [| (retval = 0) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) + || + ([| (val1 > val2) |] + && [| (retval = 1) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 )) +. + +Definition mpn_cmp4_partial_solve_wit_1_pure := +forall (bn_pre: Z) (bp_pre: Z) (an_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) , + [| (an_pre = bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && ((( &( "bn" ) )) # Int |-> bn_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "an" ) )) # Int |-> an_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 ) +|-- + [| (an_pre = bn_pre) |] + && [| (bn_pre <= cap2) |] +. + +Definition mpn_cmp4_partial_solve_wit_1_aux := +forall (bn_pre: Z) (bp_pre: Z) (an_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) , + [| (an_pre = bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 ) +|-- + [| (an_pre = bn_pre) |] + && [| (bn_pre <= cap2) |] + && [| (an_pre = bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 ) +. + +Definition mpn_cmp4_partial_solve_wit_1 := mpn_cmp4_partial_solve_wit_1_pure -> mpn_cmp4_partial_solve_wit_1_aux. + +Definition mpn_cmp4_partial_solve_wit_2_pure := +forall (bn_pre: Z) (bp_pre: Z) (an_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) , + [| (an_pre <= cap2) |] + && [| (an_pre = bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && ((( &( "bn" ) )) # Int |-> bn_pre) + ** ((( &( "bp" ) )) # Ptr |-> bp_pre) + ** ((( &( "an" ) )) # Int |-> an_pre) + ** ((( &( "ap" ) )) # Ptr |-> ap_pre) + ** (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 ) +|-- + [| (0 <= an_pre) |] + && [| (an_pre <= cap1) |] + && [| (an_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] +. + +Definition mpn_cmp4_partial_solve_wit_2_aux := +forall (bn_pre: Z) (bp_pre: Z) (an_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z) , + [| (an_pre <= cap2) |] + && [| (an_pre = bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 bn_pre cap2 ) +|-- + [| (0 <= an_pre) |] + && [| (an_pre <= cap1) |] + && [| (an_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && [| (an_pre <= cap2) |] + && [| (an_pre = bn_pre) |] + && [| (an_pre >= 0) |] + && [| (bn_pre >= 0) |] + && [| (an_pre <= cap1) |] + && [| (bn_pre <= cap2) |] + && [| (cap1 <= 100000000) |] + && [| (cap2 <= 100000000) |] + && (mpd_store_Z_compact ap_pre val1 an_pre cap1 ) + ** (mpd_store_Z_compact bp_pre val2 an_pre cap2 ) +. + +Definition mpn_cmp4_partial_solve_wit_2 := mpn_cmp4_partial_solve_wit_2_pure -> mpn_cmp4_partial_solve_wit_2_aux. + +Definition mpn_cmp4_which_implies_wit_1 := +forall (bn_pre: Z) (an_pre: Z) (cap2: Z) , + [| (an_pre = bn_pre) |] + && [| (bn_pre <= cap2) |] + && emp +|-- + [| (an_pre <= cap2) |] + && emp +. + Module Type VC_Correct. Axiom proof_of_gmp_abs_safety_wit_1 : gmp_abs_safety_wit_1. @@ -1192,5 +1520,18 @@ Axiom proof_of_mpn_cmp_partial_solve_wit_1 : mpn_cmp_partial_solve_wit_1. Axiom proof_of_mpn_cmp_partial_solve_wit_2 : mpn_cmp_partial_solve_wit_2. Axiom proof_of_mpn_cmp_partial_solve_wit_3 : mpn_cmp_partial_solve_wit_3. Axiom proof_of_mpn_cmp_which_implies_wit_1 : mpn_cmp_which_implies_wit_1. +Axiom proof_of_mpn_cmp4_safety_wit_1 : mpn_cmp4_safety_wit_1. +Axiom proof_of_mpn_cmp4_safety_wit_2 : mpn_cmp4_safety_wit_2. +Axiom proof_of_mpn_cmp4_safety_wit_3 : mpn_cmp4_safety_wit_3. +Axiom proof_of_mpn_cmp4_return_wit_1_1 : mpn_cmp4_return_wit_1_1. +Axiom proof_of_mpn_cmp4_return_wit_1_2 : mpn_cmp4_return_wit_1_2. +Axiom proof_of_mpn_cmp4_return_wit_2_1 : mpn_cmp4_return_wit_2_1. +Axiom proof_of_mpn_cmp4_return_wit_2_2 : mpn_cmp4_return_wit_2_2. +Axiom proof_of_mpn_cmp4_return_wit_2_3 : mpn_cmp4_return_wit_2_3. +Axiom proof_of_mpn_cmp4_partial_solve_wit_1_pure : mpn_cmp4_partial_solve_wit_1_pure. +Axiom proof_of_mpn_cmp4_partial_solve_wit_1 : mpn_cmp4_partial_solve_wit_1. +Axiom proof_of_mpn_cmp4_partial_solve_wit_2_pure : mpn_cmp4_partial_solve_wit_2_pure. +Axiom proof_of_mpn_cmp4_partial_solve_wit_2 : mpn_cmp4_partial_solve_wit_2. +Axiom proof_of_mpn_cmp4_which_implies_wit_1 : mpn_cmp4_which_implies_wit_1. End VC_Correct. diff --git a/projects/lib/gmp_proof_auto.v b/projects/lib/gmp_proof_auto.v index 300c3f1..92895cf 100644 --- a/projects/lib/gmp_proof_auto.v +++ b/projects/lib/gmp_proof_auto.v @@ -93,3 +93,27 @@ Proof. Admitted. Lemma proof_of_mpn_cmp_partial_solve_wit_3 : mpn_cmp_partial_solve_wit_3. Proof. Admitted. +Lemma proof_of_mpn_cmp4_safety_wit_1 : mpn_cmp4_safety_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_cmp4_safety_wit_2 : mpn_cmp4_safety_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_cmp4_safety_wit_3 : mpn_cmp4_safety_wit_3. +Proof. Admitted. + +Lemma proof_of_mpn_cmp4_partial_solve_wit_1_pure : mpn_cmp4_partial_solve_wit_1_pure. +Proof. Admitted. + +Lemma proof_of_mpn_cmp4_partial_solve_wit_1 : mpn_cmp4_partial_solve_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_cmp4_partial_solve_wit_2_pure : mpn_cmp4_partial_solve_wit_2_pure. +Proof. Admitted. + +Lemma proof_of_mpn_cmp4_partial_solve_wit_2 : mpn_cmp4_partial_solve_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_cmp4_which_implies_wit_1 : mpn_cmp4_which_implies_wit_1. +Proof. Admitted. + diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 5278efd..2f1ddf3 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -198,9 +198,9 @@ Lemma proof_of_mpn_cmp_return_wit_1_1 : mpn_cmp_return_wit_1_1. Proof. pre_process. entailer!. - repeat rewrite <-derivable1_orp_intros1. + Left; Left. entailer!. - + unfold mpd_store_Z. + + unfold mpd_store_Z_compact. Exists l1 l2. unfold mpd_store_list. entailer!. @@ -208,7 +208,7 @@ Proof. entailer!. + assert (Znth n l1 0 < Znth n l2 0). { lia. } clear H H0. - apply (list_store_Z_cmp l1 l2 val1 val2 n ltac:(lia) ltac:(lia) H4 H5). + apply (list_store_Z_compact_cmp l1 l2 val1 val2 n ltac:(lia) ltac:(lia) H4 H5). - rewrite <-H6, <-H7. tauto. - lia. @@ -217,13 +217,13 @@ Qed. Lemma proof_of_mpn_cmp_return_wit_1_2 : mpn_cmp_return_wit_1_2. Proof. pre_process. - rewrite <-derivable1_orp_intros2. + Right. entailer!. - + unfold mpd_store_Z, mpd_store_list. + + unfold mpd_store_Z_compact, mpd_store_list. Exists l1 l2. rewrite <-H6, <-H7. entailer!. - + pose proof (list_store_Z_cmp l2 l1 val2 val1 n ltac:(lia) ltac:(lia) H5 H4). + + pose proof (list_store_Z_compact_cmp l2 l1 val2 val1 n ltac:(lia) ltac:(lia) H5 H4). rewrite <-H6, <-H7 in H18. rewrite H8 in H18. specialize (H18 ltac:(reflexivity) ltac:(lia)). @@ -233,11 +233,67 @@ Qed. Lemma proof_of_mpn_cmp_which_implies_wit_1 : mpn_cmp_which_implies_wit_1. Proof. pre_process. - unfold mpd_store_Z. + unfold mpd_store_Z_compact. Intros l1 l2. Exists l2 l1. unfold mpd_store_list. entailer!. - rewrite <-H4, <-H6. + rewrite <-H0, <-H2. + entailer!. +Qed. + +Lemma proof_of_mpn_cmp4_return_wit_1_1 : mpn_cmp4_return_wit_1_1. +Proof. + pre_process. + Right. + unfold mpd_store_Z_compact. + Intros l1 l2. + Exists l1 l2. + entailer!. + pose proof (list_store_Z_cmp_length l2 l1 val2 val1 ltac:(lia) H9 H7). + lia. +Qed. + +Lemma proof_of_mpn_cmp4_return_wit_1_2 : mpn_cmp4_return_wit_1_2. +Proof. + pre_process. + Left; Left. + unfold mpd_store_Z_compact. + entailer!. + Intros l1 l2. + Exists l1 l2. + entailer!. + pose proof (list_store_Z_cmp_length l1 l2 val1 val2 ltac:(lia) H7 H9). + lia. +Qed. + +Lemma proof_of_mpn_cmp4_return_wit_2_1 : mpn_cmp4_return_wit_2_1. +Proof. + pre_process. + Right. + unfold mpd_store_Z_compact. + Intros l1 l2. + Exists l1 l2. + entailer!. +Qed. + + +Lemma proof_of_mpn_cmp4_return_wit_2_2 : mpn_cmp4_return_wit_2_2. +Proof. + pre_process. + Left; Right. + unfold mpd_store_Z_compact. + Intros l1 l2. + Exists l1 l2. + entailer!. +Qed. + +Lemma proof_of_mpn_cmp4_return_wit_2_3 : mpn_cmp4_return_wit_2_3. +Proof. + pre_process. + Left; Left. + unfold mpd_store_Z_compact. + Intros l1 l2. + Exists l1 l2. entailer!. Qed. \ No newline at end of file diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 1f69d74..96859ec 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -102,26 +102,26 @@ mpn_cmp (unsigned int *ap, unsigned int *bp, int n) /*@ With cap1 cap2 val1 val2 Require - mpd_store_Z(ap, val1, n, cap1) * - mpd_store_Z(bp, val2, n, cap2) && - 0 < n && n <= cap1 && n <= cap2 && + mpd_store_Z_compact(ap, val1, n, cap1) * + mpd_store_Z_compact(bp, val2, n, cap2) && + 0 <= n && n <= cap1 && n <= cap2 && cap1 <= 100000000 && cap2 <= 100000000 Ensure (val1 > val2 && __return == 1 || val1 == val2 && __return == 0 || val1 < val2 && __return == -1) && - mpd_store_Z(ap@pre, val1, n@pre, cap1) * - mpd_store_Z(bp@pre, val2, n@pre, cap2) + mpd_store_Z_compact(ap@pre, val1, n@pre, cap1) * + mpd_store_Z_compact(bp@pre, val2, n@pre, cap2) */ { /*@ - mpd_store_Z(ap@pre, val1, n@pre, cap1) * mpd_store_Z(bp@pre, val2, n@pre, cap2) + mpd_store_Z_compact(ap@pre, val1, n@pre, cap1) * mpd_store_Z_compact(bp@pre, val2, n@pre, cap2) which implies exists l1 l2, store_uint_array(ap@pre, n@pre, l1) * store_uint_array(bp@pre, n@pre, l2) * store_undef_uint_array_rec(ap@pre, n@pre + 1, cap1) * store_undef_uint_array_rec(bp@pre, n@pre + 1, cap2) && - list_store_Z(l1, val1) && list_store_Z(l2, val2) && + list_store_Z_compact(l1, val1) && list_store_Z_compact(l2, val2) && n@pre == Zlength(l1) && n@pre == Zlength(l2) */ /*@ @@ -133,7 +133,7 @@ mpn_cmp (unsigned int *ap, unsigned int *bp, int n) store_uint_array(ap@pre, n@pre, l1) * store_uint_array(bp@pre, n@pre, l2) * store_undef_uint_array_rec(ap@pre, n@pre + 1, cap1) * store_undef_uint_array_rec(bp@pre, n@pre + 1, cap2) && - list_store_Z(l1, val1) && list_store_Z(l2, val2) && + list_store_Z_compact(l1, val1) && list_store_Z_compact(l2, val2) && n@pre == Zlength(l1) && n@pre == Zlength(l2) && sublist(n + 1, n@pre, l1) == sublist(n + 1, n@pre, l2) */ @@ -157,24 +157,45 @@ mpn_cmp (unsigned int *ap, unsigned int *bp, int n) /*处理位数不同的情况*/ static int mpn_cmp4 (unsigned int *ap, int an, unsigned int *bp, int bn) +/*@ + With cap1 cap2 val1 val2 + Require + mpd_store_Z_compact(ap, val1, an, cap1) * + mpd_store_Z_compact(bp, val2, bn, cap2) && + an >= 0 && bn >= 0 && an <= cap1 && bn <= cap2 && + cap1 <= 100000000 && cap2 <= 100000000 + Ensure + (val1 > val2 && __return == 1 || + val1 == val2 && __return == 0 || + val1 < val2 && __return == -1) && + mpd_store_Z_compact(ap@pre, val1, an@pre, cap1) * + mpd_store_Z_compact(bp@pre, val2, bn@pre, cap2) +*/ { if (an != bn) return an < bn ? -1 : 1; - else + else { + /*@ + an@pre == bn@pre && bn@pre <= cap2 + which implies + an@pre <= cap2 + */ return mpn_cmp (ap, bp, an); + } } + /*返回非0的位数*/ -static int +/*static int mpn_normalized_size (unsigned int *xp, int n) { while (n > 0 && xp[n-1] == 0) --n; return n; -} +}*/ /* 多精度数ap 加上单精度数b，返回最后产生的进位 */ -unsigned int +/*unsigned int mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) { int i; @@ -183,17 +204,17 @@ mpn_add_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) do { unsigned int r = ap[i] + b; - /* Carry out */ + // Carry out b = (r < b); rp[i] = r; } while (++i < n); return b; -} +}*/ /* 位数相同的多精度数ap 加上多精度数bp，返回最后产生的进位 */ -unsigned int +/*unsigned int mpn_add_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n) { int i; @@ -210,10 +231,10 @@ mpn_add_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n) rp[i] = r; } return cy; -} +}*/ /*不同位数的多精度数相加，返回最后的进位*/ -unsigned int +/*unsigned int mpn_add (unsigned int *rp, unsigned int *ap, int an, unsigned int *bp, int bn) { unsigned int cy; @@ -222,9 +243,9 @@ mpn_add (unsigned int *rp, unsigned int *ap, int an, unsigned int *bp, int bn) if (an > bn) cy = mpn_add_1 (rp + bn, ap + bn, an - bn, cy); return cy; -} +}*/ -unsigned int +/*unsigned int mpn_sub_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) { int i; @@ -233,7 +254,7 @@ mpn_sub_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) do { unsigned int a = ap[i]; - /* Carry out */ + // Carry out unsigned int cy = a < b; rp[i] = a - b; b = cy; @@ -241,9 +262,9 @@ mpn_sub_1 (unsigned int *rp, unsigned int *ap, int n, unsigned int b) while (++i < n); return b; -} +}*/ -unsigned int +/*unsigned int mpn_sub_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n) { int i; @@ -259,9 +280,9 @@ mpn_sub_n (unsigned int *rp, unsigned int *ap, unsigned int *bp, int n) rp[i] = a - b; } return cy; -} +}*/ -unsigned int +/*unsigned int mpn_sub (unsigned int *rp, unsigned int *ap, int an, unsigned int *bp, int bn) { unsigned int cy; @@ -270,18 +291,18 @@ mpn_sub (unsigned int *rp, unsigned int *ap, int an, unsigned int *bp, int bn) if (an > bn) cy = mpn_sub_1 (rp + bn, ap + bn, an - bn, cy); return cy; -} +}*/ /* MPZ interface */ -void +/*void mpz_clear (mpz_t r) { if (r->_mp_alloc) gmp_free_limbs (r->_mp_d, r->_mp_alloc); -} +}*/ -static unsigned int * +/*static unsigned int * mpz_realloc (mpz_t r, int size) { size = gmp_max (size, 1); @@ -296,31 +317,31 @@ mpz_realloc (mpz_t r, int size) r->_mp_size = 0; return r->_mp_d; -} +}*/ /* Realloc for an mpz_t WHAT if it has less than NEEDED limbs. */ -unsigned int *mrz_realloc_if(mpz_t z,int n) { +/*unsigned int *mrz_realloc_if(mpz_t z,int n) { return n > z->_mp_alloc ? mpz_realloc(z, n) : z->_mp_d; -} +}*/ /* MPZ comparisons and the like. */ -int +/*int mpz_sgn (const mpz_t u) { return gmp_cmp (u->_mp_size, 0); -} +}*/ -void +/*void mpz_swap (mpz_t u, mpz_t v) { int_swap (u->_mp_alloc, v->_mp_alloc); unsigned int *_swap(u->_mp_d, v->_mp_d); int_swap (u->_mp_size, v->_mp_size); -} +}*/ /* MPZ addition and subtraction */ -static int +/*static int mpz_abs_add (mpz_t r, const mpz_t a, const mpz_t b) { int an = gmp_abs (a->_mp_size); @@ -340,9 +361,9 @@ mpz_abs_add (mpz_t r, const mpz_t a, const mpz_t b) rp[an] = cy; return an + cy; -} +}*/ -static int +/*static int mpz_abs_sub (mpz_t r, const mpz_t a, const mpz_t b) { int an = gmp_abs (a->_mp_size); @@ -365,9 +386,9 @@ mpz_abs_sub (mpz_t r, const mpz_t a, const mpz_t b) } else return 0; -} +}*/ -void +/*void mpz_add (mpz_t r, const mpz_t a, const mpz_t b) { int rn; @@ -378,9 +399,9 @@ mpz_add (mpz_t r, const mpz_t a, const mpz_t b) rn = mpz_abs_sub (r, a, b); r->_mp_size = a->_mp_size >= 0 ? rn : - rn; -} +}*/ -void +/*void mpz_sub (mpz_t r, const mpz_t a, const mpz_t b) { int rn; @@ -391,4 +412,4 @@ mpz_sub (mpz_t r, const mpz_t a, const mpz_t b) rn = mpz_abs_add (r, a, b); r->_mp_size = a->_mp_size >= 0 ? rn : - rn; -} +}*/ diff --git a/projects/mini-gmp.h b/projects/mini-gmp.h index b5a22b5..2c952b8 100755 --- a/projects/mini-gmp.h +++ b/projects/mini-gmp.h @@ -62,6 +62,9 @@ void mpz_set (mpz_t, const mpz_t); Extern Coq (Zabs : Z -> Z) (Zmax : 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) (list_store_Z : list Z -> Z -> Prop) + (list_store_Z_compact: list Z -> Z -> Prop) + (last: list Z -> Z -> Z) */ \ No newline at end of file From 257241df90954c4e8520ed654ce02a5b07f7a9bd Mon Sep 17 00:00:00 2001 From: xiaoh105 Date: Thu, 12 Jun 2025 22:11:54 +0800 Subject: [PATCH 6/6] feat(normalized_size): Proved correctness of mpd_normalized_size. Fix minor bugs in previous proves. --- projects/lib/GmpAux.v | 95 +++++++- projects/lib/GmpNumber.v | 31 ++- projects/lib/gmp_goal.v | 402 +++++++++++++++++++++++++++----- projects/lib/gmp_proof_auto.v | 24 ++ projects/lib/gmp_proof_manual.v | 128 +++++++++- projects/mini-gmp.c | 44 +++- 6 files changed, 643 insertions(+), 81 deletions(-) diff --git a/projects/lib/GmpAux.v b/projects/lib/GmpAux.v index 326dbc1..c3ff11a 100755 --- a/projects/lib/GmpAux.v +++ b/projects/lib/GmpAux.v @@ -114,7 +114,7 @@ Qed. Lemma list_last_cons: forall (a: Z) (l: list Z), l <> nil -> - last (a :: l) 0 = last l 0. + last (a :: l) 1 = last l 1. Proof. intros. destruct l. @@ -125,11 +125,11 @@ Qed. Lemma list_last_to_Znth: forall (l: list Z), l <> nil -> - last l 0 = Znth ((Zlength l) - 1) l 0. + last l 1 = Znth ((Zlength l) - 1) l 0. Proof. intros. induction l. - + auto. + + contradiction. + destruct l. - simpl. rewrite Znth0_cons. @@ -236,8 +236,8 @@ Proof. sep_apply store_array_rec_false; [ entailer! | lia ]. Qed. -Lemma store_uarray_rec_equals_store_uarray: forall x lo hi l, - lo < hi -> +Lemma uint_array_rec_to_uint_array: forall x lo hi l, + lo <= hi -> store_uint_array_rec x lo hi l --||-- store_uint_array (x + sizeof(UINT) * lo) (hi - lo) l. Proof. @@ -258,5 +258,88 @@ Proof. + sep_apply H1. entailer!. Qed. - + +Lemma store_uint_array_single: forall x n a, + store_uint_array_rec x n (n + 1) [a] --||-- + (x + n * sizeof(UINT)) # UInt |-> a. +Proof. + intros. + unfold store_uint_array_rec. + simpl. + split; entailer!. +Qed. + +Lemma store_undef_uint_array_single: forall x n a, + (x + n * sizeof(UINT)) # UInt |-> a |-- + store_undef_uint_array_rec x n (n + 1). +Proof. + intros. + unfold store_undef_uint_array_rec. + assert (Z.to_nat (n + 1 - n) = S O). { lia. } + rewrite H; clear H. + simpl. + entailer!. + sep_apply store_uint_undef_store_uint. + entailer!. +Qed. + +Lemma store_uint_array_single_to_undef: forall x n a, + store_uint_array_rec x n (n + 1) [a] |-- + store_undef_uint_array_rec x n (n + 1). +Proof. + intros. + pose proof (store_uint_array_single x n a). + destruct H as [H _]. + sep_apply H. + sep_apply store_undef_uint_array_single. + entailer!. +Qed. + +Lemma store_uint_array_divide_rec: forall x n l m, + 0 <= m <= n -> + Zlength l = n -> + store_uint_array x n l --||-- + store_uint_array x m (sublist 0 m l) ** + store_uint_array_rec x m n (sublist m n l). +Proof. + intros. + pose proof (store_uint_array_divide x n l m H H0). + pose proof (uint_array_rec_to_uint_array x m n (sublist m n l) ltac:(lia)). + destruct H2 . + destruct H1. + rewrite Z.mul_comm in H2, H3. + rewrite H3 in H1. + rewrite <-H2 in H4. + clear H2 H3. + split; tauto. +Qed. + +Lemma store_undef_uint_array_rec_divide: forall x l mid r, + 0 <= l <= r -> + l <= mid <= r -> + store_undef_uint_array_rec x l r --||-- + store_undef_uint_array_rec x l mid ** store_undef_uint_array_rec x mid r. +Proof. + intros. + unfold store_undef_uint_array_rec. + pose proof (store_undef_array_divide (x + l * sizeof(UINT)) (r - l) (mid - l) (sizeof(UINT)) + (fun x => x # UInt |->_) + (fun x0 lo => (x0 + lo * sizeof(UINT)) # UInt |->_) ltac:(lia) ltac:(reflexivity)). + unfold store_undef_array in H1. + pose (fun (l: Z) (n: Z) (len: nat) => store_undef_array_rec_base x 0 l n len (sizeof(UINT)) + (fun x => x # UInt |->_) + (fun x0 lo => (x0 + lo * sizeof(UINT)) # UInt |->_) ltac:(reflexivity)). + rewrite <-(l0 l r (Z.to_nat (r - l))) in H1. + rewrite <-(l0 l mid (Z.to_nat (mid - l))) in H1. + assert (r - l - (mid - l) = r - mid). { lia. } + rewrite H2 in H1; clear H2. + rewrite <-Z.add_assoc, <-Z.mul_add_distr_r in H1. + assert (l + (mid - l) = mid). { lia. } + rewrite H2 in H1; clear H2. + rewrite <-(l0 mid r (Z.to_nat (r - mid))) in H1. + repeat rewrite Z.add_0_l in H1. + clear l0. + rewrite H1. + split; entailer!. +Qed. End Aux. \ No newline at end of file diff --git a/projects/lib/GmpNumber.v b/projects/lib/GmpNumber.v index 8c2e754..787c79e 100755 --- a/projects/lib/GmpNumber.v +++ b/projects/lib/GmpNumber.v @@ -28,7 +28,7 @@ Module Internal. Definition mpd_store_list (ptr: addr) (data: list Z) (cap: Z): Assertion := [| Zlength data <= cap |] && [| cap <= LENGTH_MAX |] && store_uint_array ptr (Zlength data) data ** - store_undef_uint_array_rec ptr ((Zlength data) + 1) cap. + store_undef_uint_array_rec ptr (Zlength data) cap. Fixpoint list_to_Z (data: list Z): Z := match data with @@ -50,7 +50,7 @@ Definition mpd_store_Z (ptr: addr) (n: Z) (size: Z) (cap: Z): Assertion := [| list_store_Z data n |] && [| size = Zlength data |] && mpd_store_list ptr data cap. Definition list_store_Z_compact (data: list Z) (n: Z): Prop := - list_to_Z data = n /\ last data 0 >= 1 /\ list_within_bound data. + list_to_Z data = n /\ last data 1 >= 1 /\ list_within_bound data. Definition mpd_store_Z_compact (ptr: addr) (n size cap: Z): Assertion := EX data, @@ -58,7 +58,7 @@ Definition mpd_store_Z_compact (ptr: addr) (n size cap: Z): Assertion := Lemma list_store_Z_normal_to_compact: forall (data: list Z) (n: Z), list_store_Z data n -> - last data 0 >= 1 -> + last data 1 >= 1 -> list_store_Z_compact data n. Proof. unfold list_store_Z_compact, list_store_Z. @@ -122,6 +122,29 @@ Proof. tauto. Qed. +Lemma list_within_bound_Znth: forall (l: list Z) (i: Z), + 0 <= i < Zlength l -> + list_within_bound l -> + 0 <= Znth i l 0 < UINT_MOD. +Proof. + intros. + revert i H. + induction l; intros. + + rewrite Zlength_nil in H. + lia. + + assert (i = 0 \/ i > 0). { lia. } + destruct H1. + - rewrite H1. + rewrite (Znth0_cons a l 0). + simpl in H0. + lia. + - rewrite Znth_cons; try lia. + simpl in H0; destruct H0. + rewrite Zlength_cons in H; unfold Z.succ in H. + specialize (IHl H2 (i - 1) ltac:(lia)). + lia. +Qed. + Lemma __list_within_bound_split_r: forall (l1: list Z) (a: Z), list_within_bound (l1 ++ [a]) -> list_within_bound l1 /\ 0 <= a < UINT_MOD. @@ -516,7 +539,7 @@ Proof. auto. } pose proof (list_store_Z_bound l2 n2 H1) as Hn2. - pose proof (@app_removelast_last Z l2 0 H4). + pose proof (@app_removelast_last Z l2 1 H4). rewrite H5 in H1. apply list_store_Z_split in H1; destruct H1. rewrite (Aux.Zlength_removelast l2) in H1, H6; try auto. diff --git a/projects/lib/gmp_goal.v b/projects/lib/gmp_goal.v index 39ce9b4..bbb692e 100644 --- a/projects/lib/gmp_goal.v +++ b/projects/lib/gmp_goal.v @@ -194,7 +194,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "s" ) )) # Ptr |-> s_pre) ** (store_uint_array s_pre n_pre l ) - ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec s_pre n_pre cap1 ) |-- [| (0 <= INT_MAX) |] && [| ((INT_MIN) <= 0) |] @@ -225,7 +225,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l ** ((( &( "d" ) )) # Ptr |-> d) ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) ** ((( &( "s" ) )) # Ptr |-> s) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) |-- [| ((i + 1 ) <= INT_MAX) |] && [| ((INT_MIN) <= (i + 1 )) |] @@ -243,7 +243,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val && (store_uint_array_rec d_pre 0 cap2 l2 ) ** (store_uint_array d_pre 0 nil ) ** (store_uint_array s_pre n_pre l_2 ) - ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec s_pre n_pre cap1 ) |-- EX (l': (@list Z)) (l: (@list Z)) , [| (0 <= 0) |] @@ -259,7 +259,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && (store_uint_array s_pre n_pre l ) - ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec s_pre n_pre cap1 ) ** (store_uint_array d_pre 0 (sublist (0) (0) (l)) ) ** (store_uint_array_rec d_pre 0 cap2 l' ) . @@ -285,7 +285,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) && (store_uint_array d (i + 1 ) (replace_Znth (i) ((Znth i l_3 0)) ((app ((sublist (0) (i) (l_3))) ((cons (a) (nil)))))) ) ** (store_uint_array s n l_3 ) ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) |-- EX (l': (@list Z)) (l: (@list Z)) , [| (0 <= (i + 1 )) |] @@ -301,7 +301,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && (store_uint_array s n l ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) ** (store_uint_array d (i + 1 ) (sublist (0) ((i + 1 )) (l)) ) ** (store_uint_array_rec d (i + 1 ) cap2 l' ) . @@ -322,7 +322,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && (store_uint_array s n l ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) ** (store_uint_array d i (sublist (0) (i) (l)) ) ** (store_uint_array_rec d i cap2 l' ) |-- @@ -354,7 +354,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val && ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "s" ) )) # Ptr |-> s_pre) ** (store_uint_array s_pre n_pre l ) - ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec s_pre n_pre cap1 ) ** ((( &( "d" ) )) # Ptr |-> d_pre) ** (store_uint_array d_pre cap2 l2 ) |-- @@ -370,7 +370,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && (store_uint_array s_pre n_pre l ) - ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec s_pre n_pre cap1 ) ** (store_uint_array d_pre cap2 l2 ) |-- [| ((Zlength (l2)) = cap2) |] @@ -382,7 +382,7 @@ forall (n_pre: Z) (s_pre: Z) (d_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val && [| (cap2 >= n_pre) |] && (store_uint_array d_pre cap2 l2 ) ** (store_uint_array s_pre n_pre l ) - ** (store_undef_uint_array_rec s_pre (n_pre + 1 ) cap1 ) + ** (store_undef_uint_array_rec s_pre n_pre cap1 ) . Definition mpn_copyi_partial_solve_wit_2 := mpn_copyi_partial_solve_wit_2_pure -> mpn_copyi_partial_solve_wit_2_aux. @@ -406,7 +406,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l_2: (@list Z)) ** ((( &( "n" ) )) # Int |-> n) ** ((( &( "s" ) )) # Ptr |-> s) ** (store_uint_array s n l ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) ** ((( &( "d" ) )) # Ptr |-> d) ** (store_uint_array d i (sublist (0) (i) (l)) ) ** (store_uint_array_rec d i cap2 l' ) @@ -432,7 +432,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l && [| ((Zlength (l2)) = cap2) |] && [| (cap2 >= n_pre) |] && (store_uint_array s n l_2 ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) ** (store_uint_array d i (sublist (0) (i) (l_2)) ) ** (store_uint_array_rec d i cap2 l' ) |-- @@ -455,7 +455,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l && (store_uint_array_rec d i cap2 l' ) ** (store_uint_array d i (sublist (0) (i) (l_2)) ) ** (store_uint_array s n l_2 ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) . Definition mpn_copyi_partial_solve_wit_3 := mpn_copyi_partial_solve_wit_3_pure -> mpn_copyi_partial_solve_wit_3_aux. @@ -481,7 +481,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l && (store_uint_array_rec d (i + 1 ) cap2 l2' ) ** (store_uint_array d (i + 1 ) (app ((sublist (0) (i) (l_2))) ((cons (a) (nil)))) ) ** (store_uint_array s n l_2 ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) |-- [| (l' = (cons (a) (l2'))) |] && [| (i < n) |] @@ -503,7 +503,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l ** (store_uint_array_missing_i_rec s i 0 n l_2 ) ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) ** (store_uint_array d (i + 1 ) (app ((sublist (0) (i) (l_2))) ((cons (a) (nil)))) ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) . Definition mpn_copyi_partial_solve_wit_5 := @@ -527,7 +527,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l && (store_uint_array s n l_2 ) ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) ** (store_uint_array d (i + 1 ) (app ((sublist (0) (i) (l_2))) ((cons (a) (nil)))) ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) |-- [| (l' = (cons (a) (l2'))) |] && [| (i < n) |] @@ -549,7 +549,7 @@ forall (n_pre: Z) (cap2: Z) (cap1: Z) (l2: (@list Z)) (val: Z) (l: (@list Z)) (l ** (store_uint_array_missing_i_rec d i 0 (i + 1 ) (app ((sublist (0) (i) (l_2))) ((cons (a) (nil)))) ) ** (store_uint_array s n l_2 ) ** (store_uint_array_rec d (i + 1 ) cap2 l2' ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) . Definition mpn_copyi_which_implies_wit_1 := @@ -562,7 +562,7 @@ forall (cap1: Z) (val: Z) (n: Z) (s: Z) , && [| (cap1 <= 100000000) |] && [| (list_store_Z l val ) |] && (store_uint_array s n l ) - ** (store_undef_uint_array_rec s (n + 1 ) cap1 ) + ** (store_undef_uint_array_rec s n cap1 ) . Definition mpn_copyi_which_implies_wit_2 := @@ -606,8 +606,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "n" ) )) # Int |-> n_pre) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) @@ -637,8 +637,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && ((( &( "n" ) )) # Int |-> n) ** (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) |-- @@ -670,8 +670,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) ** ((( &( "n" ) )) # Int |-> n) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) |-- @@ -702,8 +702,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) ** ((( &( "n" ) )) # Int |-> n) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) |-- @@ -735,8 +735,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) ** ((( &( "n" ) )) # Int |-> n) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) |-- @@ -767,8 +767,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) ** ((( &( "n" ) )) # Int |-> n) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) |-- @@ -798,8 +798,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && ((( &( "n" ) )) # Int |-> n) ** (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) ** ((( &( "bp" ) )) # Ptr |-> bp_pre) ** ((( &( "ap" ) )) # Ptr |-> ap_pre) |-- @@ -820,8 +820,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- [| ((-1) <= (n_pre - 1 )) |] && [| ((n_pre - 1 ) < n_pre) |] @@ -841,8 +841,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) . Definition mpn_cmp_entail_wit_2 := @@ -867,8 +867,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- [| ((-1) <= (n - 1 )) |] && [| ((n - 1 ) < n_pre) |] @@ -888,8 +888,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) . Definition mpn_cmp_return_wit_1_1 := @@ -915,8 +915,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- ([| (val1 < val2) |] && [| ((-1) = (-1)) |] @@ -957,8 +957,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array bp_pre n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- ([| (val1 < val2) |] && [| (1 = (-1)) |] @@ -997,8 +997,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- ([| (val1 < val2) |] && [| (0 = (-1)) |] @@ -1056,8 +1056,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- [| (n >= 0) |] && [| ((-1) <= n) |] @@ -1079,8 +1079,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && (((ap_pre + (n * sizeof(UINT) ) )) # UInt |-> (Znth n l1 0)) ** (store_uint_array_missing_i_rec ap_pre n 0 n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) . Definition mpn_cmp_partial_solve_wit_3 := @@ -1104,8 +1104,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (cap2 <= 100000000) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) |-- [| (n >= 0) |] && [| ((-1) <= n) |] @@ -1127,8 +1127,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && (((bp_pre + (n * sizeof(UINT) ) )) # UInt |-> (Znth n l2 0)) ** (store_uint_array_missing_i_rec bp_pre n 0 n_pre l2 ) ** (store_uint_array ap_pre n_pre l1 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) . Definition mpn_cmp_which_implies_wit_1 := @@ -1143,8 +1143,8 @@ forall (n_pre: Z) (bp_pre: Z) (ap_pre: Z) (val2: Z) (val1: Z) (cap2: Z) (cap1: Z && [| (n_pre = (Zlength (l2))) |] && (store_uint_array ap_pre n_pre l1 ) ** (store_uint_array bp_pre n_pre l2 ) - ** (store_undef_uint_array_rec ap_pre (n_pre + 1 ) cap1 ) - ** (store_undef_uint_array_rec bp_pre (n_pre + 1 ) cap2 ) + ** (store_undef_uint_array_rec ap_pre n_pre cap1 ) + ** (store_undef_uint_array_rec bp_pre n_pre cap2 ) . (*----- Function mpn_cmp4 -----*) @@ -1475,6 +1475,284 @@ forall (bn_pre: Z) (an_pre: Z) (cap2: Z) , && emp . +(*----- Function mpn_normalized_size -----*) + +Definition mpn_normalized_size_safety_wit_1 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && ((( &( "n" ) )) # Int |-> n) + ** (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) + ** ((( &( "xp" ) )) # Ptr |-> xp_pre) +|-- + [| (0 <= INT_MAX) |] + && [| ((INT_MIN) <= 0) |] +. + +Definition mpn_normalized_size_safety_wit_2 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && ((( &( "n" ) )) # Int |-> n) + ** (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) + ** ((( &( "xp" ) )) # Ptr |-> xp_pre) +|-- + [| ((n - 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (n - 1 )) |] +. + +Definition mpn_normalized_size_safety_wit_3 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && ((( &( "n" ) )) # Int |-> n) + ** (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) + ** ((( &( "xp" ) )) # Ptr |-> xp_pre) +|-- + [| (1 <= INT_MAX) |] + && [| ((INT_MIN) <= 1) |] +. + +Definition mpn_normalized_size_safety_wit_4 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** ((( &( "n" ) )) # Int |-> n) + ** (store_undef_uint_array_rec xp_pre n cap ) + ** ((( &( "xp" ) )) # Ptr |-> xp_pre) +|-- + [| (0 <= INT_MAX) |] + && [| ((INT_MIN) <= 0) |] +. + +Definition mpn_normalized_size_safety_wit_5 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| ((Znth (n - 1 ) (sublist (0) (n) (l)) 0) = 0) |] + && [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** ((( &( "n" ) )) # Int |-> n) + ** (store_undef_uint_array_rec xp_pre n cap ) + ** ((( &( "xp" ) )) # Ptr |-> xp_pre) +|-- + [| ((n - 1 ) <= INT_MAX) |] + && [| ((INT_MIN) <= (n - 1 )) |] +. + +Definition mpn_normalized_size_entail_wit_1 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) , + [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n_pre (sublist (0) (n_pre) (l)) ) + ** (store_undef_uint_array_rec xp_pre n_pre cap ) +|-- + [| (n_pre >= 0) |] + && [| (n_pre <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n_pre (sublist (0) (n_pre) (l)) ) + ** (store_undef_uint_array_rec xp_pre n_pre cap ) +. + +Definition mpn_normalized_size_entail_wit_2 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| ((Znth (n - 1 ) (sublist (0) (n) (l)) 0) = 0) |] + && [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) +|-- + [| ((n - 1 ) >= 0) |] + && [| ((n - 1 ) <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) ((n - 1 )) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre (n - 1 ) (sublist (0) ((n - 1 )) (l)) ) + ** (store_undef_uint_array_rec xp_pre (n - 1 ) cap ) +. + +Definition mpn_normalized_size_return_wit_1_1 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| (n <= 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) +|-- + [| (0 <= n) |] + && [| (n <= cap) |] + && (mpd_store_Z_compact xp_pre val n cap ) +. + +Definition mpn_normalized_size_return_wit_1_2 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| ((Znth (n - 1 ) (sublist (0) (n) (l)) 0) <> 0) |] + && [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) +|-- + [| (0 <= n) |] + && [| (n <= cap) |] + && (mpd_store_Z_compact xp_pre val n cap ) +. + +Definition mpn_normalized_size_partial_solve_wit_1 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) , + [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (mpd_store_Z xp_pre val n_pre cap ) +|-- + [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (mpd_store_Z xp_pre val n_pre cap ) +. + +Definition mpn_normalized_size_partial_solve_wit_2 := +forall (n_pre: Z) (xp_pre: Z) (val: Z) (cap: Z) (l: (@list Z)) (n: Z) , + [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) +|-- + [| (n > 0) |] + && [| (n >= 0) |] + && [| (n <= n_pre) |] + && [| (n_pre >= 0) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| (list_store_Z (sublist (0) (n_pre) (l)) val ) |] + && [| ((Zlength (l)) = n_pre) |] + && [| (0 <= n_pre) |] + && [| (n_pre <= cap) |] + && [| (cap <= 100000000) |] + && (((xp_pre + ((n - 1 ) * sizeof(UINT) ) )) # UInt |-> (Znth (n - 1 ) (sublist (0) (n) (l)) 0)) + ** (store_uint_array_missing_i_rec xp_pre (n - 1 ) 0 n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) +. + +Definition mpn_normalized_size_which_implies_wit_1 := +forall (xp_pre: Z) (val: Z) (cap: Z) (n: Z) , + (mpd_store_Z xp_pre val n cap ) +|-- + EX (l: (@list Z)) , + [| (list_store_Z (sublist (0) (n) (l)) val ) |] + && [| ((Zlength (l)) = n) |] + && (store_uint_array xp_pre n (sublist (0) (n) (l)) ) + ** (store_undef_uint_array_rec xp_pre n cap ) +. + Module Type VC_Correct. Axiom proof_of_gmp_abs_safety_wit_1 : gmp_abs_safety_wit_1. @@ -1533,5 +1811,17 @@ Axiom proof_of_mpn_cmp4_partial_solve_wit_1 : mpn_cmp4_partial_solve_wit_1. Axiom proof_of_mpn_cmp4_partial_solve_wit_2_pure : mpn_cmp4_partial_solve_wit_2_pure. Axiom proof_of_mpn_cmp4_partial_solve_wit_2 : mpn_cmp4_partial_solve_wit_2. Axiom proof_of_mpn_cmp4_which_implies_wit_1 : mpn_cmp4_which_implies_wit_1. +Axiom proof_of_mpn_normalized_size_safety_wit_1 : mpn_normalized_size_safety_wit_1. +Axiom proof_of_mpn_normalized_size_safety_wit_2 : mpn_normalized_size_safety_wit_2. +Axiom proof_of_mpn_normalized_size_safety_wit_3 : mpn_normalized_size_safety_wit_3. +Axiom proof_of_mpn_normalized_size_safety_wit_4 : mpn_normalized_size_safety_wit_4. +Axiom proof_of_mpn_normalized_size_safety_wit_5 : mpn_normalized_size_safety_wit_5. +Axiom proof_of_mpn_normalized_size_entail_wit_1 : mpn_normalized_size_entail_wit_1. +Axiom proof_of_mpn_normalized_size_entail_wit_2 : mpn_normalized_size_entail_wit_2. +Axiom proof_of_mpn_normalized_size_return_wit_1_1 : mpn_normalized_size_return_wit_1_1. +Axiom proof_of_mpn_normalized_size_return_wit_1_2 : mpn_normalized_size_return_wit_1_2. +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. End VC_Correct. diff --git a/projects/lib/gmp_proof_auto.v b/projects/lib/gmp_proof_auto.v index 92895cf..153a2b3 100644 --- a/projects/lib/gmp_proof_auto.v +++ b/projects/lib/gmp_proof_auto.v @@ -117,3 +117,27 @@ Proof. Admitted. Lemma proof_of_mpn_cmp4_which_implies_wit_1 : mpn_cmp4_which_implies_wit_1. Proof. Admitted. +Lemma proof_of_mpn_normalized_size_safety_wit_1 : mpn_normalized_size_safety_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_safety_wit_2 : mpn_normalized_size_safety_wit_2. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_safety_wit_3 : mpn_normalized_size_safety_wit_3. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_safety_wit_4 : mpn_normalized_size_safety_wit_4. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_safety_wit_5 : mpn_normalized_size_safety_wit_5. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_entail_wit_1 : mpn_normalized_size_entail_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_partial_solve_wit_1 : mpn_normalized_size_partial_solve_wit_1. +Proof. Admitted. + +Lemma proof_of_mpn_normalized_size_partial_solve_wit_2 : mpn_normalized_size_partial_solve_wit_2. +Proof. Admitted. + diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index 2f1ddf3..8aedbd0 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -134,14 +134,14 @@ Proof. unfold store_uint_array, store_array. simpl. entailer!. - + pose proof (Aux.store_uarray_rec_equals_store_uarray d 0 i (sublist 0 i l) ltac:(lia)). + + pose proof (Aux.uint_array_rec_to_uint_array d 0 i (sublist 0 i l) ltac:(lia)). destruct H4 as [_ H4]. assert (d + sizeof(UINT) * 0 = d). { lia. } rewrite H5 in H4; clear H5. assert (i - 0 = i). { lia. } rewrite H5 in H4; clear H5. sep_apply H4; clear H4. - pose proof (Aux.store_uarray_rec_equals_store_uarray d 0 (i + 1) (sublist 0 i l ++ z :: nil) ltac:(lia)). + pose proof (Aux.uint_array_rec_to_uint_array d 0 (i + 1) (sublist 0 i l ++ z :: nil) ltac:(lia)). destruct H4 as [H4 _]. assert (i + 1 - 0 = i + 1). { lia. } rewrite H5 in H4; clear H5. @@ -151,11 +151,6 @@ Proof. sep_apply store_uint_array_rec_tail_merge; [ reflexivity | lia ]. Qed. -Lemma proof_of_mpn_cmp_safety_wit_1 : mpn_cmp_safety_wit_1. -Proof. - pre_process. -Qed. - Lemma proof_of_mpn_cmp_entail_wit_1 : mpn_cmp_entail_wit_1. Proof. pre_process. @@ -296,4 +291,123 @@ Proof. Intros l1 l2. Exists l1 l2. entailer!. +Qed. + +Lemma proof_of_mpn_normalized_size_entail_wit_2 : mpn_normalized_size_entail_wit_2. +Proof. + pre_process. + entailer!. + + pose proof (store_uint_array_divide_rec + xp_pre n (sublist 0 n l) (n - 1) ltac:(lia)). + rewrite (Zlength_sublist0 n l ltac:(lia)) in H12. + specialize (H12 ltac:(lia)). + destruct H12 as [H12 _]. + rewrite H12; clear H12. + rewrite (sublist_sublist00 (n - 1) n l ltac:(lia)). + rewrite (sublist_sublist0 n n (n - 1) l ltac:(lia) ltac:(lia)). + pose proof (Aux.uint_array_rec_to_uint_array xp_pre 0 (n - 1) (sublist 0 (n - 1) l) ltac:(lia)). + destruct H12 as [H12 _]. + rewrite Z.mul_0_r, Z.add_0_r, Z.sub_0_r in H12. + rewrite H12; clear H12. + entailer!. + assert (n - 1 < Z.of_nat (Datatypes.length l)). { + rewrite <-Zlength_correct. + lia. + } + pose proof (sublist_single (n - 1) l 0 ltac:(lia)). + clear H12. + pose proof (Aux.store_uint_array_single_to_undef xp_pre (n - 1) (Znth (n - 1) l 0)). + assert (n - 1 + 1 = n). { lia. } + rewrite H14 in H12, H13; clear H14. + rewrite H13, H12; clear H13 H12. + pose proof (Aux.store_undef_uint_array_rec_divide xp_pre (n - 1) n cap ltac:(lia) ltac:(lia)). + rewrite <-H12. + entailer!. + + assert (n <= Z.of_nat (Datatypes.length l)). { + rewrite <-Zlength_correct. + lia. + } + pose proof (sublist_split 0 n (n - 1) l ltac:(lia) ltac:(lia)). + clear H12. + rewrite H13 in H6. + apply (list_store_Z_split) in H6; destruct H6. + assert (Z.of_nat (Datatypes.length l) = Zlength l). { + rewrite (Zlength_correct l); reflexivity. + } + pose proof (sublist_single (n - 1) l 0 ltac:(lia)). + assert (n - 1 + 1 = n). { lia. } + rewrite H16 in H15; clear H16. + rewrite H15 in H12. + unfold list_store_Z in H12; destruct H12. + simpl in H12. + rewrite Znth_sublist0 in H; try lia. + rewrite H in H12. + rewrite (Zlength_sublist0 (n - 1) l) in *; try lia. + pose proof (Z_div_mod_eq_full val (UINT_MOD ^ (n - 1))). + rewrite <-H12, Z.mul_0_r, Z.add_0_l in H17. + rewrite <-H17 in H6. + tauto. +Qed. + +Lemma proof_of_mpn_normalized_size_return_wit_1_1 : mpn_normalized_size_return_wit_1_1. +Proof. + pre_process. + assert (n = 0). { lia. } + clear H H0. + rewrite H11 in *. + unfold mpd_store_Z_compact, mpd_store_list. + Exists nil. + entailer!. + + rewrite Zlength_nil. + lia. + + unfold list_store_Z_compact. + simpl. + rewrite sublist_nil in H5; try lia. + unfold list_store_Z in H5; simpl in H5. + destruct H5. + lia. +Qed. + +Lemma proof_of_mpn_normalized_size_return_wit_1_2 : mpn_normalized_size_return_wit_1_2. +Proof. + pre_process. + unfold mpd_store_Z_compact, mpd_store_list. + Exists (sublist 0 n l). + entailer!. + + rewrite Zlength_sublist0; try lia. + entailer!. + + rewrite Zlength_sublist0; lia. + + rewrite Zlength_sublist0; lia. + + unfold list_store_Z_compact. + unfold list_store_Z in H6. + destruct H6. + rewrite Aux.list_last_to_Znth. + - rewrite Zlength_sublist0; try lia. + repeat split; try tauto. + pose proof (list_within_bound_Znth (sublist 0 n l) (n - 1)). + rewrite Zlength_sublist0 in H13; try lia. + specialize (H13 ltac:(lia) H12). + lia. + - assert (sublist 0 n l = nil \/ sublist 0 n l <> nil). { tauto. } + destruct H13. + * pose proof (Zlength_sublist0 n l ltac:(lia)). + rewrite H13 in H14. + rewrite Zlength_nil in H14. + lia. + * tauto. +Qed. + +Lemma proof_of_mpn_normalized_size_which_implies_wit_1 : mpn_normalized_size_which_implies_wit_1. +Proof. + pre_process. + unfold mpd_store_Z. + Intros l. + Exists l. + unfold mpd_store_list. + entailer!. + + rewrite H0. + rewrite sublist_self; try lia. + entailer!. + + rewrite sublist_self; try lia. + tauto. Qed. \ No newline at end of file diff --git a/projects/mini-gmp.c b/projects/mini-gmp.c index 96859ec..8b9dd25 100755 --- a/projects/mini-gmp.c +++ b/projects/mini-gmp.c @@ -59,7 +59,7 @@ mpn_copyi (unsigned int *d, unsigned int *s, int n) Zlength(l) == n && cap1 <= 100000000 && store_uint_array(s, n, l) * - store_undef_uint_array_rec(s, n + 1, cap1) && + store_undef_uint_array_rec(s, n, cap1) && list_store_Z(l, val) */ /*@ @@ -74,7 +74,7 @@ mpn_copyi (unsigned int *d, unsigned int *s, int n) 0 <= i && i <= n && Zlength(l) == n && list_store_Z(l, val) && n <= cap1 && store_uint_array(s, n, l) * - store_undef_uint_array_rec(s, n + 1, cap1) * + store_undef_uint_array_rec(s, n, cap1) * store_uint_array(d, i, sublist(0, i, l)) * store_uint_array_rec(d, i, cap2, l') */ @@ -119,8 +119,8 @@ mpn_cmp (unsigned int *ap, unsigned int *bp, int n) which implies exists l1 l2, store_uint_array(ap@pre, n@pre, l1) * store_uint_array(bp@pre, n@pre, l2) * - store_undef_uint_array_rec(ap@pre, n@pre + 1, cap1) * - store_undef_uint_array_rec(bp@pre, n@pre + 1, cap2) && + store_undef_uint_array_rec(ap@pre, n@pre, cap1) * + store_undef_uint_array_rec(bp@pre, n@pre, cap2) && list_store_Z_compact(l1, val1) && list_store_Z_compact(l2, val2) && n@pre == Zlength(l1) && n@pre == Zlength(l2) */ @@ -131,8 +131,8 @@ mpn_cmp (unsigned int *ap, unsigned int *bp, int n) /*@Inv -1 <= n && n < n@pre && store_uint_array(ap@pre, n@pre, l1) * store_uint_array(bp@pre, n@pre, l2) * - store_undef_uint_array_rec(ap@pre, n@pre + 1, cap1) * - store_undef_uint_array_rec(bp@pre, n@pre + 1, cap2) && + store_undef_uint_array_rec(ap@pre, n@pre, cap1) * + store_undef_uint_array_rec(bp@pre, n@pre, cap2) && list_store_Z_compact(l1, val1) && list_store_Z_compact(l2, val2) && n@pre == Zlength(l1) && n@pre == Zlength(l2) && sublist(n + 1, n@pre, l1) == sublist(n + 1, n@pre, l2) @@ -186,13 +186,41 @@ mpn_cmp4 (unsigned int *ap, int an, unsigned int *bp, int bn) /*返回非0的位数*/ -/*static int +static int mpn_normalized_size (unsigned int *xp, int n) +/*@ + With cap val + Require + mpd_store_Z(xp, val, n, cap) && + 0 <= n && n <= cap && cap <= 100000000 + Ensure + 0 <= __return && __return <= cap && + mpd_store_Z_compact(xp@pre, val, __return, cap) +*/ { + /*@ + mpd_store_Z(xp@pre, val, n, cap) + which implies + exists l, + list_store_Z(sublist(0, n, l), val) && + Zlength(l) == n && + store_uint_array(xp@pre, n, sublist(0, n, l)) * + store_undef_uint_array_rec(xp@pre, n, cap) + */ + /*@ + Given l + */ + /*@Inv + n >= 0 && n <= n@pre && + n@pre >= 0 && n@pre <= cap && cap <= 100000000 && + list_store_Z(sublist(0, n, l), val) && + store_uint_array(xp@pre, n, sublist(0, n, l)) * + store_undef_uint_array_rec(xp@pre, n, cap) + */ while (n > 0 && xp[n-1] == 0) --n; return n; -}*/ +} /* 多精度数ap 加上单精度数b，返回最后产生的进位 */ /*unsigned int