From 1873d949ceab6684b0f11265234bd3a2e3eee257 Mon Sep 17 00:00:00 2001 From: xiaoh105 Date: Sat, 7 Jun 2025 15:23:11 +0800 Subject: [PATCH] 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