From 7859b9dea3f8b66e03a7b78917cd005244fd03e7 Mon Sep 17 00:00:00 2001 From: mbbarbosa Date: Thu, 7 May 2026 14:05:21 +0100 Subject: [PATCH 1/7] Adds theories/algebra/ZqCentered.ec providing the centered (signed) integer representation of Z/pZ elements. --- theories/algebra/ZqCentered.ec | 300 +++++++++++++++++++++++++++++++++ 1 file changed, 300 insertions(+) create mode 100644 theories/algebra/ZqCentered.ec diff --git a/theories/algebra/ZqCentered.ec b/theories/algebra/ZqCentered.ec new file mode 100644 index 000000000..1c92904b0 --- /dev/null +++ b/theories/algebra/ZqCentered.ec @@ -0,0 +1,300 @@ +(* ==================================================================== *) +require import AllCore IntDiv. +require import StdOrder. +(*---*) import IntOrder. +require ZModP. + +(* ==================================================================== *) +(* Centered (signed) representation of elements of the ring Z/pZ. *) +(* *) +(* For p >= 2, the centered representative `crepr : zmod -> int' maps *) +(* every element to the unique integer in the half-open centered *) +(* interval [(p+1)/2 - p, (p+1)/2). For odd primes p > 2 this interval *) +(* is exactly {-(p-1)/2, ..., (p-1)/2}, the standard "balanced" *) +(* representation used in lattice-based cryptography. *) +(* *) +(* Provides: *) +(* - `to_crepr', `crepr' (centered representative on int and Zq) *) +(* - range, round-trip, equality lemmas *) +(* - algebraic laws under +, * *) +(* - centered absolute value `"`|_|"' with triangle / product / *) +(* monotonicity inequalities *) +(* *) +(* The sub-theory `ZqCenteredField' adds prime-only lemmas: *) +(* - `creprN', `creprN2', `creprND' (negation symmetry) *) +(* - `abs_zpN' *) +(* ==================================================================== *) + +(* ==================================================================== *) +abstract theory ZqCentered. + +clone include ZModP.ZModRing. + +(* -------------------------------------------------------------------- *) +(* Auxiliary congruence lemmas. *) + +lemma zmodcgr_ceq a b : + (p + 1) %/ 2 - p <= a < (p + 1) %/ 2 + => (p + 1) %/ 2 - p <= b < (p + 1) %/ 2 + => zmodcgr a b + => a = b + by case (0 <= a); case (0 <= b); smt(). + +lemma zmodcgr_transitive b a c : + zmodcgr a b => zmodcgr b c => zmodcgr a c. +proof. smt(). qed. + +lemma zmodcgr_mp a : zmodcgr a (a - p) by smt(). + +lemma zmodcgr_refl a b : zmodcgr a b <=> zmodcgr b a by smt(). + +(* -------------------------------------------------------------------- *) +(* Centered representative on int. *) +(* *) +(* "Halfway" is rounded down: when 2 %| p the unique value with *) +(* asint = p/2 maps to -p/2. For odd p the choice is irrelevant. *) + +op to_crepr (x : int) : int = + let y = x %% p in + if (p + 1) %/ 2 <= y then y - p else y. + +lemma to_crepr_idempotent : to_crepr \o to_crepr = to_crepr. +proof. by rewrite fun_ext /(\o) => x; smt(ge2_p). qed. + +lemma rg_to_crepr x : + (p + 1) %/ 2 - p <= to_crepr x < (p + 1) %/ 2. +proof. smt(ge2_p rg_asint). qed. + +lemma to_crepr_zmodcgr x : zmodcgr x (to_crepr x). +proof. smt(ge2_p). qed. + +lemma to_crepr_id x : + (p + 1) %/ 2 - p <= x < (p + 1) %/ 2 => to_crepr x = x. +proof. smt(). qed. + +lemma to_crepr_eq x y : to_crepr x = to_crepr y <=> zmodcgr x y. +proof. rewrite /to_crepr /= /#. qed. + +(* -------------------------------------------------------------------- *) +(* Centered representative on Zq. *) + +op crepr (x : zmod) : int = + let y = asint x in + if (p + 1) %/ 2 <= y then y - p else y. + +lemma rg_crepr x : + (p + 1) %/ 2 - p <= crepr x < (p + 1) %/ 2. +proof. smt(ge2_p rg_asint). qed. + +lemma crepr_eq x y : crepr x = crepr y <=> x = y. +proof. smt(rg_asint asint_eq). qed. + +lemma asint_crepr x : asint x = (crepr x) %% p. +proof. +rewrite /crepr /=. +case ((p + 1) %/ 2 <= asint x) => _. +- by rewrite -modzDr; smt(modz_small rg_asint). +- by smt(modz_small rg_asint). +qed. + +lemma creprK (x : zmod) : inzmod (crepr x) = x. +proof. +rewrite /crepr /=. +case ((p + 1) %/ 2 <= asint x) => ?; last by exact asintK. +rewrite inzmod_mod. +suff : (asint x - p) %% p = asint x by smt(asintK). +smt(rg_asint). +qed. + +lemma inzmodK_centered x : + (p + 1) %/ 2 - p <= x + => x < (p + 1) %/ 2 + => crepr (inzmod x) = x. +proof. by rewrite /crepr inzmodK /#. qed. + +(* -------------------------------------------------------------------- *) +(* Algebraic laws under multiplication and addition. *) + +lemma crepr_mulE x y : + crepr (x * y) = to_crepr (crepr x * crepr y). +proof. +suff : zmodcgr (crepr (x * y)) (crepr x * crepr y). ++ move => *. + have ? := to_crepr_zmodcgr (crepr x * crepr y). + by have : zmodcgr (crepr (x * y)) (to_crepr (crepr x * crepr y)); + smt(to_crepr_zmodcgr rg_to_crepr rg_crepr zmodcgr_ceq). +rewrite /crepr /=. +case ((p + 1) %/ 2 <= asint (x * y)) => ?. +- case ((p + 1) %/ 2 <= asint x) => ?. + + case ((p + 1) %/ 2 <= asint y) => ?. + + rewrite -modzMm -(zmodcgr_mp (asint x)) -(zmodcgr_mp (asint y)). + by rewrite -(zmodcgr_mp (asint (x * y))) mulE -modzMm modz_mod. + + rewrite -modzMm -(zmodcgr_mp (asint x)) -(zmodcgr_mp (asint (x * y))). + by rewrite mulE -modzMm modz_mod. + + case ((p + 1) %/ 2 <= asint y) => ?. + + rewrite -modzMm -(zmodcgr_mp (asint y)). + by rewrite -(zmodcgr_mp (asint (x * y))) mulE -modzMm modz_mod. + + rewrite -modzMm -(zmodcgr_mp (asint (x * y))). + by rewrite mulE -modzMm modz_mod. +- case ((p + 1) %/ 2 <= asint x) => ?. + + case ((p + 1) %/ 2 <= asint y) => ?. + + rewrite -modzMm -(zmodcgr_mp (asint x)) -(zmodcgr_mp (asint y)). + by rewrite mulE -modzMm modz_mod. + + rewrite -modzMm -(zmodcgr_mp (asint x)). + by rewrite mulE -modzMm modz_mod. + + case ((p + 1) %/ 2 <= asint y) => ?. + + rewrite -modzMm -(zmodcgr_mp (asint y)). + by rewrite mulE -modzMm modz_mod. + + rewrite -modzMm. + by rewrite mulE -modzMm modz_mod. +qed. + +lemma creprD (x y : zmod) : + crepr (x + y) = to_crepr (crepr x + crepr y). +proof. +suff : zmodcgr (crepr (x + y)) (crepr x + crepr y). ++ move => *. + have ? := to_crepr_zmodcgr (crepr x + crepr y). + by have : zmodcgr (crepr (x + y)) (to_crepr (crepr x + crepr y)); + smt(to_crepr_zmodcgr rg_to_crepr rg_crepr zmodcgr_ceq). +rewrite /crepr addE /=. +apply (zmodcgr_transitive (asint x + asint y)). +- case ((p + 1) %/ 2 <= (asint x + asint y) %% p) => _. + + have -> : (asint x + asint y) %% p - p + = (asint x + asint y) %% p + (-1) * p by ring. + by rewrite modzMDr modz_mod. + + by rewrite modz_mod. +case ((p + 1) %/ 2 <= asint x) => _. +- case ((p + 1) %/ 2 <= asint y) => _. + + have -> : asint x - p + (asint y - p) + = asint x + asint y + (-2) * p by ring. + by rewrite modzMDr. + + have -> : asint x - p + asint y + = asint x + asint y + (-1) * p by ring. + by rewrite modzMDr. +- case ((p + 1) %/ 2 <= asint y) => _ //. + have -> : asint x + (asint y - p) + = asint x + asint y + (-1) * p by ring. + by rewrite modzMDr. +qed. + +(* -------------------------------------------------------------------- *) +(* Centered absolute value. *) + +op "`|_|" (x : zmod) : int = `| crepr x |. + +lemma to_crepr_abs x : `|to_crepr x| <= `|x|. +proof. smt(rg_to_crepr). qed. + +lemma abs_zp_small (x : int) : + `|x| < p %/ 2 => `|inzmod x| = `|x|. +proof. by move=> ?; rewrite /"`|_|"; smt(ltr_norml inzmodK). qed. + +lemma abs_zp_triangle (x y : zmod) : + `|x + y| <= `|x| + `|y|. +proof. +rewrite /"`|_|" creprD. +have := to_crepr_abs (crepr x + crepr y). +smt(). +qed. + +lemma abs_zp_zero : `|zero| = 0. +proof. by rewrite /"`|_|" /crepr zeroE /=; smt(ge2_p). qed. + +lemma abs_zp_one : `|one| = 1. +proof. by rewrite /"`|_|" /crepr /=; rewrite oneE; smt(ge2_p). qed. + +lemma ge0_abs_zp (x : zmod) : 0 <= `|x|. +proof. smt(). qed. + +lemma abs_zp_ub (x : zmod) : `|x| <= p %/ 2. +proof. smt(rg_asint). qed. + +lemma abs_zp_prod (x y : zmod) : + `|x * y| <= `|x| * `|y|. +proof. by rewrite /"`|_|" crepr_mulE; smt(to_crepr_abs). qed. + +lemma abs_zpN (x : zmod) : `|x| = `|-x|. +proof. +rewrite /"`|_|" /crepr /=. +case (x = zero) => ?; first by smt(ZModpRing.oppr0). +have ? : asint x <> 0 by have := asint_inj x zero; smt(zeroE). +suff : asint (-x) = p - asint x by smt(). +rewrite oppE -modzDl. +suff : (p - asint x) %% p = ((p - asint x) + p) %% p by smt(rg_asint). +by smt(modzDr). +qed. + +end ZqCentered. + +(* ==================================================================== *) +(* Field version: when p is prime, additionally provide negation *) +(* symmetry for the centered representative. *) +(* ==================================================================== *) +abstract theory ZqCenteredField. + +const p : { int | prime p } as prime_p. + +clone include ZqCentered with + op p <- p + proof ge2_p by smt(gt1_prime prime_p). + +(* prime_p is now in scope; ZqCentered's content is available. *) + +lemma modz_small2 a : + p <= a < 2 * p => a %% p = a - p + by smt(). + +lemma zmodcgrN a : + a <> zero => + (- asint a) %% p = - asint a %% p + p. +proof. +move => ?; have ? := rg_asint a. +have ? : asint a <> 0 by have := asint_inj a zero; smt(zeroE). +rewrite modNz; 1,2: by smt(prime_p). +rewrite -modzDm modNz //=; 1: smt(prime_p). +suff : (asint a %% p + (p - 1)) %% p = (asint a %% p + (p - 1)) - p by smt(). +rewrite (modz_small (asint a) p) 1:/# /=. +by rewrite modz_small2 /#. +qed. + +lemma creprN (a : zmod) : + p <> 2 => crepr (-a) = -crepr a. +proof. +have ? := rg_asint a. +rewrite /crepr !oppE; case (a = zero). ++ by move => -> /=; rewrite zeroE /=; smt(prime_p). +move => ? /=; rewrite !zmodcgrN //. +have -> : (- asint a %% p) + p = p - asint a + by smt(rg_asint modz_small edivzP). +have ? : asint a <> 0 by have := asint_inj a zero; smt(zeroE). +case ((p + 1) %/ 2 < asint a); 1: by smt(). +case (asint a < (p + 1) %/ 2); 1: by smt(). +move => *; have -> : asint a = (p + 1) %/ 2 by smt(rg_asint). +have ? : p + 1 = (p + 1) %/ 2 + (p + 1) %/ 2; last by smt(). +have ? : p %% 2 <> 0. ++ have := prime_p. + rewrite /prime => [#? Hmod]. + by have := Hmod 2 => /= /#. + smt(). +qed. + +lemma creprN2 (a : zmod) : + p = 2 => crepr (-a) = crepr a. +proof. +move => Hp. +have ? := rg_asint a. +rewrite /crepr !oppE; case (a = zero). ++ by move => -> /=; rewrite zeroE /=; smt(prime_p). +move => ? /=; rewrite !zmodcgrN /#. +qed. + +lemma creprND (a b : zmod) : + crepr (a - b) = to_crepr (crepr a - crepr b). +proof. +have ? := rg_asint a; have ? := rg_asint b. +case (p = 2); 2: by smt(creprD creprN). +by smt(creprD creprN2). +qed. + +end ZqCenteredField. From f7dd38922aaf3da015e833cf756df6538ab421a9 Mon Sep 17 00:00:00 2001 From: mbbarbosa Date: Thu, 7 May 2026 14:05:21 +0100 Subject: [PATCH 2/7] Adds theories/algebra/ZqCentered.ec providing the centered (signed) integer representation of Z/pZ elements. --- theories/algebra/ZqCentered.ec | 300 +++++++++++++++++++++++++++++++++ 1 file changed, 300 insertions(+) create mode 100644 theories/algebra/ZqCentered.ec diff --git a/theories/algebra/ZqCentered.ec b/theories/algebra/ZqCentered.ec new file mode 100644 index 000000000..1c92904b0 --- /dev/null +++ b/theories/algebra/ZqCentered.ec @@ -0,0 +1,300 @@ +(* ==================================================================== *) +require import AllCore IntDiv. +require import StdOrder. +(*---*) import IntOrder. +require ZModP. + +(* ==================================================================== *) +(* Centered (signed) representation of elements of the ring Z/pZ. *) +(* *) +(* For p >= 2, the centered representative `crepr : zmod -> int' maps *) +(* every element to the unique integer in the half-open centered *) +(* interval [(p+1)/2 - p, (p+1)/2). For odd primes p > 2 this interval *) +(* is exactly {-(p-1)/2, ..., (p-1)/2}, the standard "balanced" *) +(* representation used in lattice-based cryptography. *) +(* *) +(* Provides: *) +(* - `to_crepr', `crepr' (centered representative on int and Zq) *) +(* - range, round-trip, equality lemmas *) +(* - algebraic laws under +, * *) +(* - centered absolute value `"`|_|"' with triangle / product / *) +(* monotonicity inequalities *) +(* *) +(* The sub-theory `ZqCenteredField' adds prime-only lemmas: *) +(* - `creprN', `creprN2', `creprND' (negation symmetry) *) +(* - `abs_zpN' *) +(* ==================================================================== *) + +(* ==================================================================== *) +abstract theory ZqCentered. + +clone include ZModP.ZModRing. + +(* -------------------------------------------------------------------- *) +(* Auxiliary congruence lemmas. *) + +lemma zmodcgr_ceq a b : + (p + 1) %/ 2 - p <= a < (p + 1) %/ 2 + => (p + 1) %/ 2 - p <= b < (p + 1) %/ 2 + => zmodcgr a b + => a = b + by case (0 <= a); case (0 <= b); smt(). + +lemma zmodcgr_transitive b a c : + zmodcgr a b => zmodcgr b c => zmodcgr a c. +proof. smt(). qed. + +lemma zmodcgr_mp a : zmodcgr a (a - p) by smt(). + +lemma zmodcgr_refl a b : zmodcgr a b <=> zmodcgr b a by smt(). + +(* -------------------------------------------------------------------- *) +(* Centered representative on int. *) +(* *) +(* "Halfway" is rounded down: when 2 %| p the unique value with *) +(* asint = p/2 maps to -p/2. For odd p the choice is irrelevant. *) + +op to_crepr (x : int) : int = + let y = x %% p in + if (p + 1) %/ 2 <= y then y - p else y. + +lemma to_crepr_idempotent : to_crepr \o to_crepr = to_crepr. +proof. by rewrite fun_ext /(\o) => x; smt(ge2_p). qed. + +lemma rg_to_crepr x : + (p + 1) %/ 2 - p <= to_crepr x < (p + 1) %/ 2. +proof. smt(ge2_p rg_asint). qed. + +lemma to_crepr_zmodcgr x : zmodcgr x (to_crepr x). +proof. smt(ge2_p). qed. + +lemma to_crepr_id x : + (p + 1) %/ 2 - p <= x < (p + 1) %/ 2 => to_crepr x = x. +proof. smt(). qed. + +lemma to_crepr_eq x y : to_crepr x = to_crepr y <=> zmodcgr x y. +proof. rewrite /to_crepr /= /#. qed. + +(* -------------------------------------------------------------------- *) +(* Centered representative on Zq. *) + +op crepr (x : zmod) : int = + let y = asint x in + if (p + 1) %/ 2 <= y then y - p else y. + +lemma rg_crepr x : + (p + 1) %/ 2 - p <= crepr x < (p + 1) %/ 2. +proof. smt(ge2_p rg_asint). qed. + +lemma crepr_eq x y : crepr x = crepr y <=> x = y. +proof. smt(rg_asint asint_eq). qed. + +lemma asint_crepr x : asint x = (crepr x) %% p. +proof. +rewrite /crepr /=. +case ((p + 1) %/ 2 <= asint x) => _. +- by rewrite -modzDr; smt(modz_small rg_asint). +- by smt(modz_small rg_asint). +qed. + +lemma creprK (x : zmod) : inzmod (crepr x) = x. +proof. +rewrite /crepr /=. +case ((p + 1) %/ 2 <= asint x) => ?; last by exact asintK. +rewrite inzmod_mod. +suff : (asint x - p) %% p = asint x by smt(asintK). +smt(rg_asint). +qed. + +lemma inzmodK_centered x : + (p + 1) %/ 2 - p <= x + => x < (p + 1) %/ 2 + => crepr (inzmod x) = x. +proof. by rewrite /crepr inzmodK /#. qed. + +(* -------------------------------------------------------------------- *) +(* Algebraic laws under multiplication and addition. *) + +lemma crepr_mulE x y : + crepr (x * y) = to_crepr (crepr x * crepr y). +proof. +suff : zmodcgr (crepr (x * y)) (crepr x * crepr y). ++ move => *. + have ? := to_crepr_zmodcgr (crepr x * crepr y). + by have : zmodcgr (crepr (x * y)) (to_crepr (crepr x * crepr y)); + smt(to_crepr_zmodcgr rg_to_crepr rg_crepr zmodcgr_ceq). +rewrite /crepr /=. +case ((p + 1) %/ 2 <= asint (x * y)) => ?. +- case ((p + 1) %/ 2 <= asint x) => ?. + + case ((p + 1) %/ 2 <= asint y) => ?. + + rewrite -modzMm -(zmodcgr_mp (asint x)) -(zmodcgr_mp (asint y)). + by rewrite -(zmodcgr_mp (asint (x * y))) mulE -modzMm modz_mod. + + rewrite -modzMm -(zmodcgr_mp (asint x)) -(zmodcgr_mp (asint (x * y))). + by rewrite mulE -modzMm modz_mod. + + case ((p + 1) %/ 2 <= asint y) => ?. + + rewrite -modzMm -(zmodcgr_mp (asint y)). + by rewrite -(zmodcgr_mp (asint (x * y))) mulE -modzMm modz_mod. + + rewrite -modzMm -(zmodcgr_mp (asint (x * y))). + by rewrite mulE -modzMm modz_mod. +- case ((p + 1) %/ 2 <= asint x) => ?. + + case ((p + 1) %/ 2 <= asint y) => ?. + + rewrite -modzMm -(zmodcgr_mp (asint x)) -(zmodcgr_mp (asint y)). + by rewrite mulE -modzMm modz_mod. + + rewrite -modzMm -(zmodcgr_mp (asint x)). + by rewrite mulE -modzMm modz_mod. + + case ((p + 1) %/ 2 <= asint y) => ?. + + rewrite -modzMm -(zmodcgr_mp (asint y)). + by rewrite mulE -modzMm modz_mod. + + rewrite -modzMm. + by rewrite mulE -modzMm modz_mod. +qed. + +lemma creprD (x y : zmod) : + crepr (x + y) = to_crepr (crepr x + crepr y). +proof. +suff : zmodcgr (crepr (x + y)) (crepr x + crepr y). ++ move => *. + have ? := to_crepr_zmodcgr (crepr x + crepr y). + by have : zmodcgr (crepr (x + y)) (to_crepr (crepr x + crepr y)); + smt(to_crepr_zmodcgr rg_to_crepr rg_crepr zmodcgr_ceq). +rewrite /crepr addE /=. +apply (zmodcgr_transitive (asint x + asint y)). +- case ((p + 1) %/ 2 <= (asint x + asint y) %% p) => _. + + have -> : (asint x + asint y) %% p - p + = (asint x + asint y) %% p + (-1) * p by ring. + by rewrite modzMDr modz_mod. + + by rewrite modz_mod. +case ((p + 1) %/ 2 <= asint x) => _. +- case ((p + 1) %/ 2 <= asint y) => _. + + have -> : asint x - p + (asint y - p) + = asint x + asint y + (-2) * p by ring. + by rewrite modzMDr. + + have -> : asint x - p + asint y + = asint x + asint y + (-1) * p by ring. + by rewrite modzMDr. +- case ((p + 1) %/ 2 <= asint y) => _ //. + have -> : asint x + (asint y - p) + = asint x + asint y + (-1) * p by ring. + by rewrite modzMDr. +qed. + +(* -------------------------------------------------------------------- *) +(* Centered absolute value. *) + +op "`|_|" (x : zmod) : int = `| crepr x |. + +lemma to_crepr_abs x : `|to_crepr x| <= `|x|. +proof. smt(rg_to_crepr). qed. + +lemma abs_zp_small (x : int) : + `|x| < p %/ 2 => `|inzmod x| = `|x|. +proof. by move=> ?; rewrite /"`|_|"; smt(ltr_norml inzmodK). qed. + +lemma abs_zp_triangle (x y : zmod) : + `|x + y| <= `|x| + `|y|. +proof. +rewrite /"`|_|" creprD. +have := to_crepr_abs (crepr x + crepr y). +smt(). +qed. + +lemma abs_zp_zero : `|zero| = 0. +proof. by rewrite /"`|_|" /crepr zeroE /=; smt(ge2_p). qed. + +lemma abs_zp_one : `|one| = 1. +proof. by rewrite /"`|_|" /crepr /=; rewrite oneE; smt(ge2_p). qed. + +lemma ge0_abs_zp (x : zmod) : 0 <= `|x|. +proof. smt(). qed. + +lemma abs_zp_ub (x : zmod) : `|x| <= p %/ 2. +proof. smt(rg_asint). qed. + +lemma abs_zp_prod (x y : zmod) : + `|x * y| <= `|x| * `|y|. +proof. by rewrite /"`|_|" crepr_mulE; smt(to_crepr_abs). qed. + +lemma abs_zpN (x : zmod) : `|x| = `|-x|. +proof. +rewrite /"`|_|" /crepr /=. +case (x = zero) => ?; first by smt(ZModpRing.oppr0). +have ? : asint x <> 0 by have := asint_inj x zero; smt(zeroE). +suff : asint (-x) = p - asint x by smt(). +rewrite oppE -modzDl. +suff : (p - asint x) %% p = ((p - asint x) + p) %% p by smt(rg_asint). +by smt(modzDr). +qed. + +end ZqCentered. + +(* ==================================================================== *) +(* Field version: when p is prime, additionally provide negation *) +(* symmetry for the centered representative. *) +(* ==================================================================== *) +abstract theory ZqCenteredField. + +const p : { int | prime p } as prime_p. + +clone include ZqCentered with + op p <- p + proof ge2_p by smt(gt1_prime prime_p). + +(* prime_p is now in scope; ZqCentered's content is available. *) + +lemma modz_small2 a : + p <= a < 2 * p => a %% p = a - p + by smt(). + +lemma zmodcgrN a : + a <> zero => + (- asint a) %% p = - asint a %% p + p. +proof. +move => ?; have ? := rg_asint a. +have ? : asint a <> 0 by have := asint_inj a zero; smt(zeroE). +rewrite modNz; 1,2: by smt(prime_p). +rewrite -modzDm modNz //=; 1: smt(prime_p). +suff : (asint a %% p + (p - 1)) %% p = (asint a %% p + (p - 1)) - p by smt(). +rewrite (modz_small (asint a) p) 1:/# /=. +by rewrite modz_small2 /#. +qed. + +lemma creprN (a : zmod) : + p <> 2 => crepr (-a) = -crepr a. +proof. +have ? := rg_asint a. +rewrite /crepr !oppE; case (a = zero). ++ by move => -> /=; rewrite zeroE /=; smt(prime_p). +move => ? /=; rewrite !zmodcgrN //. +have -> : (- asint a %% p) + p = p - asint a + by smt(rg_asint modz_small edivzP). +have ? : asint a <> 0 by have := asint_inj a zero; smt(zeroE). +case ((p + 1) %/ 2 < asint a); 1: by smt(). +case (asint a < (p + 1) %/ 2); 1: by smt(). +move => *; have -> : asint a = (p + 1) %/ 2 by smt(rg_asint). +have ? : p + 1 = (p + 1) %/ 2 + (p + 1) %/ 2; last by smt(). +have ? : p %% 2 <> 0. ++ have := prime_p. + rewrite /prime => [#? Hmod]. + by have := Hmod 2 => /= /#. + smt(). +qed. + +lemma creprN2 (a : zmod) : + p = 2 => crepr (-a) = crepr a. +proof. +move => Hp. +have ? := rg_asint a. +rewrite /crepr !oppE; case (a = zero). ++ by move => -> /=; rewrite zeroE /=; smt(prime_p). +move => ? /=; rewrite !zmodcgrN /#. +qed. + +lemma creprND (a b : zmod) : + crepr (a - b) = to_crepr (crepr a - crepr b). +proof. +have ? := rg_asint a; have ? := rg_asint b. +case (p = 2); 2: by smt(creprD creprN). +by smt(creprD creprN2). +qed. + +end ZqCenteredField. From bcca6100971780e237cd3c1d0bac666e86a1bd52 Mon Sep 17 00:00:00 2001 From: mbbarbosa Date: Mon, 11 May 2026 17:55:21 +0100 Subject: [PATCH 3/7] Extended version of PolyReduce --- theories/algebra/MaxBigop.eca | 66 +++++ theories/algebra/PolyReduce.ec | 228 +++++++++++++++++- theories/algebra/TypeWithBot.eca | 24 ++ .../{ZqCentered.ec => ZModPCentered.ec} | 18 +- theories/datatypes/Nneg.ec | 81 +++++++ 5 files changed, 399 insertions(+), 18 deletions(-) create mode 100644 theories/algebra/MaxBigop.eca create mode 100644 theories/algebra/TypeWithBot.eca rename theories/algebra/{ZqCentered.ec => ZModPCentered.ec} (97%) create mode 100644 theories/datatypes/Nneg.ec diff --git a/theories/algebra/MaxBigop.eca b/theories/algebra/MaxBigop.eca new file mode 100644 index 000000000..1b18cf3e2 --- /dev/null +++ b/theories/algebra/MaxBigop.eca @@ -0,0 +1,66 @@ +(* ==================================================================== *) +require import AllCore List. +require Bigop TypeWithBot. + +(* ==================================================================== *) +(* Generic big-fold of [max] over a list, built atop [Bigop] using the *) +(* max-monoid induced by a [TypeWithBot] instance. *) +(* ==================================================================== *) + +clone include TypeWithBot. + +(* -------------------------------------------------------------------- *) +op maxr (x y : t) : t = if x <= y then y else x. + +lemma maxrA : associative maxr. +proof. by move=> x y z; rewrite /maxr; smt(le_refl le_trans le_anti le_total). qed. + +lemma maxrC : commutative maxr. +proof. by move=> x y; rewrite /maxr; smt(le_anti le_total). qed. + +lemma max0r : left_id bot maxr. +proof. by move=> x; rewrite /maxr bot_le. qed. + +lemma maxrr (x : t) : maxr x x = x. +proof. by rewrite /maxr; case (x <= x). qed. + +lemma maxr_lel (x y : t) : x <= y => maxr x y = y. +proof. by rewrite /maxr => ->. qed. + +lemma maxr_ler (x y : t) : y <= x => maxr x y = x. +proof. by rewrite /maxr => H; case (x <= y) => Hxy //; smt(le_anti). qed. + +lemma maxr_ge_l (x y : t) : x <= maxr x y. +proof. by rewrite /maxr; case (x <= y) => // ?; apply le_refl. qed. + +lemma maxr_ge_r (x y : t) : y <= maxr x y. +proof. by rewrite /maxr; case (x <= y) => H; [apply le_refl | smt(le_total)]. qed. + +lemma maxr_le_max (x y b : t) : x <= b => y <= b => maxr x y <= b. +proof. by rewrite /maxr; case (x <= y). qed. + +lemma maxr_le_max_iff (x y b : t) : (maxr x y <= b) <=> (x <= b /\ y <= b). +proof. +split; last by case=> *; apply maxr_le_max. +move=> H; split; smt(maxr_ge_l maxr_ge_r le_trans). +qed. + +(* -------------------------------------------------------------------- *) +clone include Bigop with + type t <- t, + op Support.idm <- bot, + op Support.( + ) <- maxr +proof Support.Axioms.* by smt(maxrA maxrC max0r). + +(* -------------------------------------------------------------------- *) +(* Soundness: the big-max is bounded above iff every element is. *) + +lemma big_le_iff (P : 'a -> bool) (F : 'a -> t) (s : 'a list) (b : t) : + big P F s <= b <=> bot <= b /\ forall x, x \in s => P x => F x <= b. +proof. +elim: s => [|x xs IH] /=. +- by rewrite big_nil; smt(). +rewrite big_cons; case (P x) => Px /=. +- rewrite maxr_le_max_iff IH; smt(). +- by rewrite IH; smt(). +qed. \ No newline at end of file diff --git a/theories/algebra/PolyReduce.ec b/theories/algebra/PolyReduce.ec index 7d65744eb..357981a7f 100644 --- a/theories/algebra/PolyReduce.ec +++ b/theories/algebra/PolyReduce.ec @@ -460,17 +460,12 @@ end PolyReduce. (* ==================================================================== *) abstract theory PolyReduceZp. -type coeff. - -op p : { int | 2 <= p } as ge2_p. -clone import ZModRing as Zp with - op p <= p - proof ge2_p by exact/ge2_p. +clone import ZModRing as Zp. clone import PolyReduce with - type coeff <- Zp.zmod, - theory Coeff <- ZModpRing. + type coeff <= Zp.zmod, + theory Coeff <= ZModpRing. (* ==================================================================== *) (* We already know that polyXnD1 is finite. However, we prove here that *) @@ -526,3 +521,220 @@ lemma reduced_dpoly d p : p \in dpoly n d => reduced p. proof. by rewrite supp_dpoly // => -[ltn_deg _]; apply/reducedP. qed. end PolyReduceZp. + +(* ==================================================================== *) +(* PolyReduceZpCentered: same scaffolding as [PolyReduceZp] but the *) +(* coefficient sub-theory is [ZqCentered] (extends [ZModRing] with *) +(* centered representation [crepr], absolute value `|_|`, and the *) +(* abs_zp lemma family). *) +(* *) +(* Built by first cloning [ZqCentered] (to get the extended Zp), then *) +(* clone-including [PolyReduceZp] with PolyReduceZp's internal Zp *) +(* rebound to ours — so the polynomial-ring construction and the *) +(* distributions are inherited without copy-paste. *) +(* ==================================================================== *) +require import ZModPCentered Nneg. + +abstract theory PolyReduceZpCentered. + +clone import ZpCentered as ZpC. + +clone import PolyReduceZp with + theory Zp <- Zp. +import PolyReduce. +import Zp. + +(* ==================================================================== *) +(* Distributions over polyXnD1 — duplicated from PolyReduceZp because *) +(* PolyReduceZp's internal Zp is not exposed as a rebindable theory *) +(* parameter, so we cannot clone-include it with our extended Zp. *) +(* ==================================================================== *) +op dpolyX (dcoeff : zmod distr) : polyXnD1 distr = + dmap (dpoly n dcoeff) pinject. + +lemma dpolyX_ll d : is_lossless d => is_lossless (dpolyX d). +proof. by move=> ll_d; apply/dmap_ll/BasePoly.dpoly_ll. qed. + +lemma dpolyX_uni d : is_uniform d => is_uniform (dpolyX d). +proof. +move=> uni_d; apply/dmap_uni_in_inj/dpoly_uni/uni_d => //. +move=> p q; rewrite !supp_dpoly //; case=> [degp _] [deqq _]. +by move/eqv_pi/reduce_eqP; rewrite !reduce_reduced // !reducedP. +qed. + +lemma dpolyX_full d : is_full d => is_full (dpolyX d). +proof. +move=> fu_d; apply/dmap_fu_in=> p; exists (crepr p). +by rewrite creprK /=; apply/dpoly_fu/deg_crepr. +qed. + +lemma dpolyX_suppP d p : + p \in dpolyX d <=> (forall i, 0 <= i < n => p.[i] \in d). +proof. split. +- case/supp_dmap=> q [+ ->>] i rg_i. + rewrite supp_dpoly => // -[? /(_ i rg_i)]. + by rewrite piK //; apply/reducedP. +- move=> h; apply/supp_dmap; exists (crepr p). + by rewrite creprK /= &(supp_dpoly) // deg_crepr. +qed. + +(* -------------------------------------------------------------------- *) +op dpolyXnD1 = dpolyX Zp.DZmodP.dunifin. + +lemma dpolyXnD1_ll : is_lossless dpolyXnD1. +proof. by apply/dpolyX_ll/DZmodP.dunifin_ll. qed. + +lemma dpolyXnD1_uni : is_uniform dpolyXnD1. +proof. by apply/dpolyX_uni/DZmodP.dunifin_uni. qed. + +lemma dpolyXnD1_full : is_full dpolyXnD1. +proof. by apply/dpolyX_full/DZmodP.dunifin_fu. qed. + +lemma dpolyXnD1_funi : is_funiform dpolyXnD1. +proof. by apply/is_full_funiform/dpolyXnD1_uni/dpolyXnD1_full. qed. + +(* -------------------------------------------------------------------- *) +lemma reduced_dpoly d p : p \in dpoly n d => reduced p. +proof. by rewrite supp_dpoly // => -[ltn_deg _]; apply/reducedP. qed. + +(* ==================================================================== *) +(* Centered-representation infinity-norm machinery on polyXnD1. *) +(* *) +(* Two complementary views, equivalent under non-negative bounds: *) +(* - predicate-style checks: poly_infnorm_le, poly_infnorm_lt *) +(* - computed norm: inf_norm : polyXnD1 -> Nneg.nneg *) +(* The soundness lemmas tie them together. *) +(* ==================================================================== *) + +(* -------------------------------------------------------------------- *) +(* Predicate-style inf-norm bound checks on coefficients. *) + +op poly_infnorm_lt (q : polyXnD1) (b : int) : bool = + forall i, 0 <= i < n => `|q.[i]| < b. + +op poly_infnorm_le (q : polyXnD1) (b : int) : bool = + forall i, 0 <= i < n => `|q.[i]| <= b. + +(* -------------------------------------------------------------------- *) +(* Basic monotonicity / equivalence lemmas. *) + +lemma poly_infnorm_lt_le (q : polyXnD1) (b : int) : + poly_infnorm_lt q b => poly_infnorm_le q b. +proof. by move=> H i Hi; have := H i Hi; smt(). qed. + +lemma poly_infnorm_le_mono (q : polyXnD1) (b1 b2 : int) : + b1 <= b2 => poly_infnorm_le q b1 => poly_infnorm_le q b2. +proof. by move=> Hb H i Hi; have := H i Hi; smt(). qed. + +lemma poly_infnorm_lt_mono (q : polyXnD1) (b1 b2 : int) : + b1 <= b2 => poly_infnorm_lt q b1 => poly_infnorm_lt q b2. +proof. by move=> Hb H i Hi; have := H i Hi; smt(). qed. + +(* -------------------------------------------------------------------- *) +(* Trivial bounds. *) + +lemma poly_infnorm_le_ub (q : polyXnD1) : + poly_infnorm_le q (p %/ 2) + by move=> i Hi; smt(abs_zp_ub). + +lemma poly_infnorm_le_zero : + poly_infnorm_le zeroXnD1 0. +proof. move=> i Hi; rewrite rcoeff0; smt(abs_zp_zero). qed. + +(* -------------------------------------------------------------------- *) +(* Triangle inequality and negation bounds. *) + +lemma poly_infnorm_le_add (q r : polyXnD1) (bq br : int) : + poly_infnorm_le q bq + => poly_infnorm_le r br + => poly_infnorm_le (q + r) (bq + br). +proof. +move=> Hq Hr i Hi. +rewrite rcoeffD; have := abs_zp_triangle q.[i] r.[i]. +have := Hq i Hi; have := Hr i Hi; smt(). +qed. + +lemma poly_infnorm_lt_add (q r : polyXnD1) (bq br : int) : + poly_infnorm_lt q bq + => poly_infnorm_lt r br + => poly_infnorm_lt (q + r) (bq + br). +proof. +move=> Hq Hr i Hi. +rewrite rcoeffD; have := abs_zp_triangle q.[i] r.[i]. +have := Hq i Hi; have := Hr i Hi; smt(). +qed. + +lemma poly_infnorm_le_opp (q : polyXnD1) (b : int) : + poly_infnorm_le q b => poly_infnorm_le (- q) b. +proof. +move=> H i Hi. +rewrite -rcoeffN -abs_zpN. +have := H i Hi; smt(). +qed. + +lemma poly_infnorm_lt_opp (q : polyXnD1) (b : int) : + poly_infnorm_lt q b => poly_infnorm_lt (- q) b. +proof. +move=> H i Hi. +rewrite -rcoeffN -abs_zpN. +have := H i Hi; smt(). +qed. + +(* -------------------------------------------------------------------- *) +(* Computed inf-norm via big-max of coefficient absolute values. *) + +op inf_norm (q : polyXnD1) : Nneg.nneg = + Nneg.BMaxN.bigi predT (fun i => Nneg.ofint `|q.[i]|) 0 n. + +(* Soundness against the [_le] check (for non-negative bounds). *) +lemma poly_infnorm_le_iff (q : polyXnD1) (b : int) : + 0 <= b => + (poly_infnorm_le q b <=> Nneg.(<=) (inf_norm q) (Nneg.ofint b)). +proof. +move=> ge0_b; rewrite /poly_infnorm_le /inf_norm Nneg.BMaxN.big_le_iff. +have valK_b : Nneg.val (Nneg.ofint b) = b by apply Nneg.valK_pos. +have step : forall a, 0 <= a => + Nneg.(<=) (Nneg.ofint a) (Nneg.ofint b) <=> a <= b. +- move=> a ge0_a; rewrite /Nneg.(<=) valK_b. + by have -> : Nneg.val (Nneg.ofint a) = a by apply Nneg.valK_pos. +split. +- move=> H; split; first by apply Nneg.zero_le. + move=> i; rewrite mem_range => Hi _ /=. + have ge0_a : 0 <= `|q.[i]| by smt(). + by rewrite step //; apply H; smt(). +- case=> _ H i Hi. + have Hi' : i \in range 0 n by rewrite mem_range; smt(). + have ge0_a : 0 <= `|q.[i]| by smt(). + have := H i Hi' _; first by []. + by rewrite /= step. +qed. + +(* Soundness against the [_lt] check. Strictly-less bound means *) +(* coefficient bounds by [b - 1] (since values are integers). *) +lemma poly_infnorm_lt_iff (q : polyXnD1) (b : int) : + 1 <= b => + (poly_infnorm_lt q b <=> Nneg.(<=) (inf_norm q) (Nneg.ofint (b - 1))). +proof. +move=> ge1_b. +have -> : poly_infnorm_lt q b <=> poly_infnorm_le q (b - 1) + by rewrite /poly_infnorm_lt /poly_infnorm_le; smt(). +by apply poly_infnorm_le_iff; smt(). +qed. + +end PolyReduceZpCentered. + +(* ==================================================================== *) +(* Field version: when [p] is prime, additionally make available the *) +(* prime-only coefficient lemmas (creprN, creprND, creprN2) on the same *) +(* polyXnD1 coefficient instantiation. *) +(* ==================================================================== *) +abstract theory PolyReduceZpCenteredField. + +clone import ZpCenteredField as ZpCF. +import ZpC. + +clone import PolyReduceZpCentered with + theory ZpC <- ZpC. +import Zp. + +end PolyReduceZpCenteredField. diff --git a/theories/algebra/TypeWithBot.eca b/theories/algebra/TypeWithBot.eca new file mode 100644 index 000000000..bb25caf0f --- /dev/null +++ b/theories/algebra/TypeWithBot.eca @@ -0,0 +1,24 @@ +(* ==================================================================== *) +require import AllCore. + +(* ==================================================================== *) +(* A type equipped with a total order having a least element [bot]. *) +(* *) +(* This abstraction is exactly what is needed to form a max-monoid: *) +(* [maxr x y = if x <= y then y else x] is associative, commutative, *) +(* and has [bot] as identity (since [bot <= x] for all [x]). *) +(* *) +(* On types without a global minimum (e.g. plain [int]) one must *) +(* restrict to a subtype bounded below. *) +(* ==================================================================== *) + +type t. + +op (<=) : t -> t -> bool. +op bot : t. + +axiom le_refl (x : t) : x <= x. +axiom le_trans (y x z : t) : x <= y => y <= z => x <= z. +axiom le_anti (x y : t) : x <= y => y <= x => x = y. +axiom le_total (x y : t) : x <= y \/ y <= x. +axiom bot_le (x : t) : bot <= x. \ No newline at end of file diff --git a/theories/algebra/ZqCentered.ec b/theories/algebra/ZModPCentered.ec similarity index 97% rename from theories/algebra/ZqCentered.ec rename to theories/algebra/ZModPCentered.ec index 1c92904b0..d3d410d3b 100644 --- a/theories/algebra/ZqCentered.ec +++ b/theories/algebra/ZModPCentered.ec @@ -26,9 +26,9 @@ require ZModP. (* ==================================================================== *) (* ==================================================================== *) -abstract theory ZqCentered. +abstract theory ZpCentered. -clone include ZModP.ZModRing. +clone import ZModP.ZModRing as Zp. (* -------------------------------------------------------------------- *) (* Auxiliary congruence lemmas. *) @@ -225,19 +225,17 @@ suff : (p - asint x) %% p = ((p - asint x) + p) %% p by smt(rg_asint). by smt(modzDr). qed. -end ZqCentered. +end ZpCentered. (* ==================================================================== *) (* Field version: when p is prime, additionally provide negation *) (* symmetry for the centered representative. *) (* ==================================================================== *) -abstract theory ZqCenteredField. +abstract theory ZpCenteredField. -const p : { int | prime p } as prime_p. - -clone include ZqCentered with - op p <- p - proof ge2_p by smt(gt1_prime prime_p). +clone import ZpCentered as ZpC. +import Zp. +axiom prime_p : prime p. (* prime_p is now in scope; ZqCentered's content is available. *) @@ -297,4 +295,4 @@ case (p = 2); 2: by smt(creprD creprN). by smt(creprD creprN2). qed. -end ZqCenteredField. +end ZpCenteredField. diff --git a/theories/datatypes/Nneg.ec b/theories/datatypes/Nneg.ec new file mode 100644 index 000000000..231125606 --- /dev/null +++ b/theories/datatypes/Nneg.ec @@ -0,0 +1,81 @@ +(* ==================================================================== *) +require import AllCore IntDiv. +require Subtype. +require MaxBigop. + +(* ==================================================================== *) +(* Non-negative integers as a subtype of [int]. *) +(* *) +(* This type exists so that constructions requiring a globally-minimal *) +(* element (e.g. the identity of a max-monoid) can sit on something *) +(* simpler than [int]. The traditional name "nat" is avoided because *) +(* of overload with OCaml's primitive [nat] and because it conflates *) +(* "natural numbers" (sometimes 0+, sometimes 1+) with the more *) +(* specific "non-negative integers" we mean here. *) +(* ==================================================================== *) + +(* -------------------------------------------------------------------- *) +subtype nneg = { x : int | 0 <= x }. +realize inhabited by exists 0. + +(* -------------------------------------------------------------------- *) +(* Conversions and constants. *) + +(* val : nneg -> int (canonical injection) *) +(* insubd : int -> nneg (saturates negatives to witness, but we use *) +(* ofint below for a saturating-to-zero version) *) + +op ofint (x : int) : nneg = insubd (max 0 x). + +op zero : nneg = ofint 0. +op one : nneg = ofint 1. + +op (<=) (x y : nneg) : bool = val x <= val y. + +(* -------------------------------------------------------------------- *) +lemma ge0_val (x : nneg) : 0 <= val x. +proof. exact valP. qed. + +lemma valK_pos (x : int) : 0 <= x => val (ofint x) = x. +proof. +move=> h; rewrite /ofint. +have -> : max 0 x = x by smt(). +by rewrite insubdK. +qed. + +lemma val_zero : val zero = 0. +proof. by rewrite /zero valK_pos. qed. + +lemma val_one : val one = 1. +proof. by rewrite /one valK_pos. qed. + +(* -------------------------------------------------------------------- *) +(* Order properties. *) + +lemma le_refl (x : nneg) : x <= x. +proof. by rewrite /(<=). qed. + +lemma le_trans (y x z : nneg) : x <= y => y <= z => x <= z. +proof. by rewrite /(<=); smt(). qed. + +lemma le_anti (x y : nneg) : x <= y => y <= x => x = y. +proof. by rewrite /(<=); smt(val_inj). qed. + +lemma le_total (x y : nneg) : x <= y \/ y <= x. +proof. by rewrite /(<=); smt(). qed. + +lemma zero_le (x : nneg) : zero <= x. +proof. by rewrite /(<=) val_zero ge0_val. qed. + +(* ==================================================================== *) +(* Big-fold of [max] over [nneg]. *) +(* ==================================================================== *) +clone import MaxBigop as BMaxN with + type t <- nneg, + op (<=) <- (<=), + op bot <- zero + proof le_refl by exact le_refl, + le_trans by exact le_trans, + le_anti by exact le_anti, + le_total by exact le_total, + bot_le by exact zero_le. \ No newline at end of file From 8bedf39c3dffec8ae0c3dff44e2d5845bc15ed85 Mon Sep 17 00:00:00 2001 From: mbbarbosa Date: Mon, 11 May 2026 17:58:13 +0100 Subject: [PATCH 4/7] cleanup --- theories/algebra/ZqCentered.ec | 300 --------------------------------- 1 file changed, 300 deletions(-) delete mode 100644 theories/algebra/ZqCentered.ec diff --git a/theories/algebra/ZqCentered.ec b/theories/algebra/ZqCentered.ec deleted file mode 100644 index 1c92904b0..000000000 --- a/theories/algebra/ZqCentered.ec +++ /dev/null @@ -1,300 +0,0 @@ -(* ==================================================================== *) -require import AllCore IntDiv. -require import StdOrder. -(*---*) import IntOrder. -require ZModP. - -(* ==================================================================== *) -(* Centered (signed) representation of elements of the ring Z/pZ. *) -(* *) -(* For p >= 2, the centered representative `crepr : zmod -> int' maps *) -(* every element to the unique integer in the half-open centered *) -(* interval [(p+1)/2 - p, (p+1)/2). For odd primes p > 2 this interval *) -(* is exactly {-(p-1)/2, ..., (p-1)/2}, the standard "balanced" *) -(* representation used in lattice-based cryptography. *) -(* *) -(* Provides: *) -(* - `to_crepr', `crepr' (centered representative on int and Zq) *) -(* - range, round-trip, equality lemmas *) -(* - algebraic laws under +, * *) -(* - centered absolute value `"`|_|"' with triangle / product / *) -(* monotonicity inequalities *) -(* *) -(* The sub-theory `ZqCenteredField' adds prime-only lemmas: *) -(* - `creprN', `creprN2', `creprND' (negation symmetry) *) -(* - `abs_zpN' *) -(* ==================================================================== *) - -(* ==================================================================== *) -abstract theory ZqCentered. - -clone include ZModP.ZModRing. - -(* -------------------------------------------------------------------- *) -(* Auxiliary congruence lemmas. *) - -lemma zmodcgr_ceq a b : - (p + 1) %/ 2 - p <= a < (p + 1) %/ 2 - => (p + 1) %/ 2 - p <= b < (p + 1) %/ 2 - => zmodcgr a b - => a = b - by case (0 <= a); case (0 <= b); smt(). - -lemma zmodcgr_transitive b a c : - zmodcgr a b => zmodcgr b c => zmodcgr a c. -proof. smt(). qed. - -lemma zmodcgr_mp a : zmodcgr a (a - p) by smt(). - -lemma zmodcgr_refl a b : zmodcgr a b <=> zmodcgr b a by smt(). - -(* -------------------------------------------------------------------- *) -(* Centered representative on int. *) -(* *) -(* "Halfway" is rounded down: when 2 %| p the unique value with *) -(* asint = p/2 maps to -p/2. For odd p the choice is irrelevant. *) - -op to_crepr (x : int) : int = - let y = x %% p in - if (p + 1) %/ 2 <= y then y - p else y. - -lemma to_crepr_idempotent : to_crepr \o to_crepr = to_crepr. -proof. by rewrite fun_ext /(\o) => x; smt(ge2_p). qed. - -lemma rg_to_crepr x : - (p + 1) %/ 2 - p <= to_crepr x < (p + 1) %/ 2. -proof. smt(ge2_p rg_asint). qed. - -lemma to_crepr_zmodcgr x : zmodcgr x (to_crepr x). -proof. smt(ge2_p). qed. - -lemma to_crepr_id x : - (p + 1) %/ 2 - p <= x < (p + 1) %/ 2 => to_crepr x = x. -proof. smt(). qed. - -lemma to_crepr_eq x y : to_crepr x = to_crepr y <=> zmodcgr x y. -proof. rewrite /to_crepr /= /#. qed. - -(* -------------------------------------------------------------------- *) -(* Centered representative on Zq. *) - -op crepr (x : zmod) : int = - let y = asint x in - if (p + 1) %/ 2 <= y then y - p else y. - -lemma rg_crepr x : - (p + 1) %/ 2 - p <= crepr x < (p + 1) %/ 2. -proof. smt(ge2_p rg_asint). qed. - -lemma crepr_eq x y : crepr x = crepr y <=> x = y. -proof. smt(rg_asint asint_eq). qed. - -lemma asint_crepr x : asint x = (crepr x) %% p. -proof. -rewrite /crepr /=. -case ((p + 1) %/ 2 <= asint x) => _. -- by rewrite -modzDr; smt(modz_small rg_asint). -- by smt(modz_small rg_asint). -qed. - -lemma creprK (x : zmod) : inzmod (crepr x) = x. -proof. -rewrite /crepr /=. -case ((p + 1) %/ 2 <= asint x) => ?; last by exact asintK. -rewrite inzmod_mod. -suff : (asint x - p) %% p = asint x by smt(asintK). -smt(rg_asint). -qed. - -lemma inzmodK_centered x : - (p + 1) %/ 2 - p <= x - => x < (p + 1) %/ 2 - => crepr (inzmod x) = x. -proof. by rewrite /crepr inzmodK /#. qed. - -(* -------------------------------------------------------------------- *) -(* Algebraic laws under multiplication and addition. *) - -lemma crepr_mulE x y : - crepr (x * y) = to_crepr (crepr x * crepr y). -proof. -suff : zmodcgr (crepr (x * y)) (crepr x * crepr y). -+ move => *. - have ? := to_crepr_zmodcgr (crepr x * crepr y). - by have : zmodcgr (crepr (x * y)) (to_crepr (crepr x * crepr y)); - smt(to_crepr_zmodcgr rg_to_crepr rg_crepr zmodcgr_ceq). -rewrite /crepr /=. -case ((p + 1) %/ 2 <= asint (x * y)) => ?. -- case ((p + 1) %/ 2 <= asint x) => ?. - + case ((p + 1) %/ 2 <= asint y) => ?. - + rewrite -modzMm -(zmodcgr_mp (asint x)) -(zmodcgr_mp (asint y)). - by rewrite -(zmodcgr_mp (asint (x * y))) mulE -modzMm modz_mod. - + rewrite -modzMm -(zmodcgr_mp (asint x)) -(zmodcgr_mp (asint (x * y))). - by rewrite mulE -modzMm modz_mod. - + case ((p + 1) %/ 2 <= asint y) => ?. - + rewrite -modzMm -(zmodcgr_mp (asint y)). - by rewrite -(zmodcgr_mp (asint (x * y))) mulE -modzMm modz_mod. - + rewrite -modzMm -(zmodcgr_mp (asint (x * y))). - by rewrite mulE -modzMm modz_mod. -- case ((p + 1) %/ 2 <= asint x) => ?. - + case ((p + 1) %/ 2 <= asint y) => ?. - + rewrite -modzMm -(zmodcgr_mp (asint x)) -(zmodcgr_mp (asint y)). - by rewrite mulE -modzMm modz_mod. - + rewrite -modzMm -(zmodcgr_mp (asint x)). - by rewrite mulE -modzMm modz_mod. - + case ((p + 1) %/ 2 <= asint y) => ?. - + rewrite -modzMm -(zmodcgr_mp (asint y)). - by rewrite mulE -modzMm modz_mod. - + rewrite -modzMm. - by rewrite mulE -modzMm modz_mod. -qed. - -lemma creprD (x y : zmod) : - crepr (x + y) = to_crepr (crepr x + crepr y). -proof. -suff : zmodcgr (crepr (x + y)) (crepr x + crepr y). -+ move => *. - have ? := to_crepr_zmodcgr (crepr x + crepr y). - by have : zmodcgr (crepr (x + y)) (to_crepr (crepr x + crepr y)); - smt(to_crepr_zmodcgr rg_to_crepr rg_crepr zmodcgr_ceq). -rewrite /crepr addE /=. -apply (zmodcgr_transitive (asint x + asint y)). -- case ((p + 1) %/ 2 <= (asint x + asint y) %% p) => _. - + have -> : (asint x + asint y) %% p - p - = (asint x + asint y) %% p + (-1) * p by ring. - by rewrite modzMDr modz_mod. - + by rewrite modz_mod. -case ((p + 1) %/ 2 <= asint x) => _. -- case ((p + 1) %/ 2 <= asint y) => _. - + have -> : asint x - p + (asint y - p) - = asint x + asint y + (-2) * p by ring. - by rewrite modzMDr. - + have -> : asint x - p + asint y - = asint x + asint y + (-1) * p by ring. - by rewrite modzMDr. -- case ((p + 1) %/ 2 <= asint y) => _ //. - have -> : asint x + (asint y - p) - = asint x + asint y + (-1) * p by ring. - by rewrite modzMDr. -qed. - -(* -------------------------------------------------------------------- *) -(* Centered absolute value. *) - -op "`|_|" (x : zmod) : int = `| crepr x |. - -lemma to_crepr_abs x : `|to_crepr x| <= `|x|. -proof. smt(rg_to_crepr). qed. - -lemma abs_zp_small (x : int) : - `|x| < p %/ 2 => `|inzmod x| = `|x|. -proof. by move=> ?; rewrite /"`|_|"; smt(ltr_norml inzmodK). qed. - -lemma abs_zp_triangle (x y : zmod) : - `|x + y| <= `|x| + `|y|. -proof. -rewrite /"`|_|" creprD. -have := to_crepr_abs (crepr x + crepr y). -smt(). -qed. - -lemma abs_zp_zero : `|zero| = 0. -proof. by rewrite /"`|_|" /crepr zeroE /=; smt(ge2_p). qed. - -lemma abs_zp_one : `|one| = 1. -proof. by rewrite /"`|_|" /crepr /=; rewrite oneE; smt(ge2_p). qed. - -lemma ge0_abs_zp (x : zmod) : 0 <= `|x|. -proof. smt(). qed. - -lemma abs_zp_ub (x : zmod) : `|x| <= p %/ 2. -proof. smt(rg_asint). qed. - -lemma abs_zp_prod (x y : zmod) : - `|x * y| <= `|x| * `|y|. -proof. by rewrite /"`|_|" crepr_mulE; smt(to_crepr_abs). qed. - -lemma abs_zpN (x : zmod) : `|x| = `|-x|. -proof. -rewrite /"`|_|" /crepr /=. -case (x = zero) => ?; first by smt(ZModpRing.oppr0). -have ? : asint x <> 0 by have := asint_inj x zero; smt(zeroE). -suff : asint (-x) = p - asint x by smt(). -rewrite oppE -modzDl. -suff : (p - asint x) %% p = ((p - asint x) + p) %% p by smt(rg_asint). -by smt(modzDr). -qed. - -end ZqCentered. - -(* ==================================================================== *) -(* Field version: when p is prime, additionally provide negation *) -(* symmetry for the centered representative. *) -(* ==================================================================== *) -abstract theory ZqCenteredField. - -const p : { int | prime p } as prime_p. - -clone include ZqCentered with - op p <- p - proof ge2_p by smt(gt1_prime prime_p). - -(* prime_p is now in scope; ZqCentered's content is available. *) - -lemma modz_small2 a : - p <= a < 2 * p => a %% p = a - p - by smt(). - -lemma zmodcgrN a : - a <> zero => - (- asint a) %% p = - asint a %% p + p. -proof. -move => ?; have ? := rg_asint a. -have ? : asint a <> 0 by have := asint_inj a zero; smt(zeroE). -rewrite modNz; 1,2: by smt(prime_p). -rewrite -modzDm modNz //=; 1: smt(prime_p). -suff : (asint a %% p + (p - 1)) %% p = (asint a %% p + (p - 1)) - p by smt(). -rewrite (modz_small (asint a) p) 1:/# /=. -by rewrite modz_small2 /#. -qed. - -lemma creprN (a : zmod) : - p <> 2 => crepr (-a) = -crepr a. -proof. -have ? := rg_asint a. -rewrite /crepr !oppE; case (a = zero). -+ by move => -> /=; rewrite zeroE /=; smt(prime_p). -move => ? /=; rewrite !zmodcgrN //. -have -> : (- asint a %% p) + p = p - asint a - by smt(rg_asint modz_small edivzP). -have ? : asint a <> 0 by have := asint_inj a zero; smt(zeroE). -case ((p + 1) %/ 2 < asint a); 1: by smt(). -case (asint a < (p + 1) %/ 2); 1: by smt(). -move => *; have -> : asint a = (p + 1) %/ 2 by smt(rg_asint). -have ? : p + 1 = (p + 1) %/ 2 + (p + 1) %/ 2; last by smt(). -have ? : p %% 2 <> 0. -+ have := prime_p. - rewrite /prime => [#? Hmod]. - by have := Hmod 2 => /= /#. - smt(). -qed. - -lemma creprN2 (a : zmod) : - p = 2 => crepr (-a) = crepr a. -proof. -move => Hp. -have ? := rg_asint a. -rewrite /crepr !oppE; case (a = zero). -+ by move => -> /=; rewrite zeroE /=; smt(prime_p). -move => ? /=; rewrite !zmodcgrN /#. -qed. - -lemma creprND (a b : zmod) : - crepr (a - b) = to_crepr (crepr a - crepr b). -proof. -have ? := rg_asint a; have ? := rg_asint b. -case (p = 2); 2: by smt(creprD creprN). -by smt(creprD creprN2). -qed. - -end ZqCenteredField. From 0aaab067d5129e778268e1e9c8c8872f0319b5ef Mon Sep 17 00:00:00 2001 From: mbbarbosa Date: Mon, 11 May 2026 18:33:42 +0100 Subject: [PATCH 5/7] trying to fix smt instability --- theories/algebra/ZModPCentered.ec | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/theories/algebra/ZModPCentered.ec b/theories/algebra/ZModPCentered.ec index d3d410d3b..dc68332d5 100644 --- a/theories/algebra/ZModPCentered.ec +++ b/theories/algebra/ZModPCentered.ec @@ -37,8 +37,13 @@ lemma zmodcgr_ceq a b : (p + 1) %/ 2 - p <= a < (p + 1) %/ 2 => (p + 1) %/ 2 - p <= b < (p + 1) %/ 2 => zmodcgr a b - => a = b - by case (0 <= a); case (0 <= b); smt(). + => a = b. +proof. +move=> Ha Hb Hcgr. +have Hp := ge2_p. +have Hdvd : p %| (a - b) by smt(zmodcgrP). +smt(). +qed. lemma zmodcgr_transitive b a c : zmodcgr a b => zmodcgr b c => zmodcgr a c. From d041d90035a39bc5be3243d1c8bcd53e37c90116 Mon Sep 17 00:00:00 2001 From: mbbarbosa Date: Mon, 11 May 2026 18:53:06 +0100 Subject: [PATCH 6/7] trying to fix smt instability --- theories/algebra/ZModPCentered.ec | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/theories/algebra/ZModPCentered.ec b/theories/algebra/ZModPCentered.ec index dc68332d5..92405e956 100644 --- a/theories/algebra/ZModPCentered.ec +++ b/theories/algebra/ZModPCentered.ec @@ -71,7 +71,12 @@ lemma rg_to_crepr x : proof. smt(ge2_p rg_asint). qed. lemma to_crepr_zmodcgr x : zmodcgr x (to_crepr x). -proof. smt(ge2_p). qed. +proof. +rewrite /to_crepr /=; case ((p + 1) %/ 2 <= x %% p) => _. +- have -> : x %% p - p = x %% p + (-1) * p by ring. + by rewrite /zmodcgr modzMDr modz_mod. +- by rewrite /zmodcgr modz_mod. +qed. lemma to_crepr_id x : (p + 1) %/ 2 - p <= x < (p + 1) %/ 2 => to_crepr x = x. From f362d36521682723c5baae6184dd0ee41950ca38 Mon Sep 17 00:00:00 2001 From: mbbarbosa Date: Mon, 11 May 2026 19:58:45 +0100 Subject: [PATCH 7/7] trying to fix smt instability --- theories/algebra/ZModPCentered.ec | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/theories/algebra/ZModPCentered.ec b/theories/algebra/ZModPCentered.ec index 92405e956..983beba00 100644 --- a/theories/algebra/ZModPCentered.ec +++ b/theories/algebra/ZModPCentered.ec @@ -80,7 +80,16 @@ qed. lemma to_crepr_id x : (p + 1) %/ 2 - p <= x < (p + 1) %/ 2 => to_crepr x = x. -proof. smt(). qed. +proof. +move=> [Hl Hu]; rewrite /to_crepr /=. +have Hp := ge2_p. +case (0 <= x) => Hx. +- have -> : x %% p = x by apply modz_small; smt(). + by rewrite ifF /#. +- have Hxp : (x + p) %% p = x + p by apply modz_small; smt(). + have -> : x %% p = x + p by rewrite -(modzDr x) Hxp. + by rewrite ifT 1:/# /#. +qed. lemma to_crepr_eq x y : to_crepr x = to_crepr y <=> zmodcgr x y. proof. rewrite /to_crepr /= /#. qed.