# Theory Mod_Plus_Minus

```theory Mod_Plus_Minus

imports Kyber_spec

begin

lemma odd_half_floor:
‹⌊real_of_int x / 2⌋ = (x - 1) div 2› if ‹odd x›
using that by (rule oddE) simp

section ‹Re-centered Modulo Operation›
text ‹To define the compress and decompress functions,
we need some special form of modulo. It returns the
representation of the equivalence class in ‹(-q div 2, q div 2]›.
Using these representatives, we ensure that the norm of the
representative is as small as possible.›

definition mod_plus_minus :: "int ⇒ int ⇒ int"
(infixl "mod+-" 70) where
"m mod+- b =
(if m mod b > ⌊b/2⌋ then m mod b - b else m mod b)"

text ‹Range of the (re-centered) modulo operation›

lemma mod_range: "b>0 ⟹ (a::int) mod (b::int) ∈ {0..b-1}"
using range_mod by auto

lemma mod_rangeE:
assumes "(a::int)∈{0..<b}"
shows "a = a mod b"
using assms by auto

lemma half_mod_odd:
assumes "b > 0" "odd b" "⌊real_of_int b / 2⌋ < y mod b"
shows "- ⌊real_of_int b / 2⌋ ≤ y mod b - b"
"y mod b - b ≤ ⌊real_of_int b / 2⌋"
proof -
from odd_half_floor [of b]
show "- ⌊real_of_int b / 2⌋ ≤ y mod b - b"
using assms by linarith
then have "y mod b ≤ b + ⌊real_of_int b / 2⌋"
by (smt (verit) ‹b > 0› pos_mod_bound)
then show "y mod b - b ≤ ⌊real_of_int b / 2⌋"
by auto
qed

lemma half_mod:
assumes "b>0"
shows "- ⌊real_of_int b / 2⌋ ≤ y mod b"
using assms
by (smt (verit, best) floor_less_zero half_gt_zero mod_int_pos_iff of_int_pos)

lemma mod_plus_minus_range_odd:
assumes "b>0" "odd b"
shows "y mod+- b ∈ {-⌊b/2⌋..⌊b/2⌋}"
unfolding mod_plus_minus_def by (auto simp add: half_mod_odd[OF assms] half_mod[OF assms(1)])

lemma odd_smaller_b:
assumes "odd b"
shows "⌊ real_of_int b / 2 ⌋ + ⌊ real_of_int b / 2 ⌋ < b"
using assms
by (smt (z3) floor_divide_of_int_eq odd_two_times_div_two_succ

lemma mod_plus_minus_rangeE_neg:
assumes "y ∈ {-⌊real_of_int b/2⌋..⌊real_of_int b/2⌋}"
"odd b" "b > 0"
"⌊real_of_int b / 2⌋ < y mod b"
shows "y = y mod b - b"
proof -
have "y ∈ {-⌊real_of_int b/2⌋..<0}" using assms
by (meson atLeastAtMost_iff atLeastLessThan_iff linorder_not_le order_trans zmod_le_nonneg_dividend)
then have "y ∈ {-b..<0}" using assms(2-3)
by (metis atLeastLessThan_iff floor_divide_of_int_eq int_div_less_self linorder_linear
linorder_not_le neg_le_iff_le numeral_code(1) numeral_le_iff of_int_numeral order_trans
semiring_norm(69))
then have "y mod b = y + b"
by (smt (verit) atLeastLessThan_iff mod_add_self2 mod_pos_pos_trivial)
then show ?thesis by auto
qed

lemma mod_plus_minus_rangeE_pos:
assumes "y ∈ {-⌊real_of_int b/2⌋..⌊real_of_int b/2⌋}"
"odd b" "b > 0"
"⌊real_of_int b / 2⌋ ≥ y mod b"
shows "y = y mod b"
proof -
have "y ∈ {0..⌊real_of_int b/2⌋}"
proof (rule ccontr)
assume "y ∉ {0..⌊real_of_int b / 2⌋} "
then have "y ∈ {-⌊real_of_int b/2⌋..<0}" using assms(1) by auto
then have "y ∈ {-b..<0}" using assms(2-3)
by (metis atLeastLessThan_iff floor_divide_of_int_eq int_div_less_self linorder_linear
linorder_not_le neg_le_iff_le numeral_code(1) numeral_le_iff of_int_numeral order_trans
semiring_norm(69))
then have "y mod b = y + b"
by (smt (verit) atLeastLessThan_iff mod_add_self2 mod_pos_pos_trivial)
then have "y mod b ≥ b - ⌊real_of_int b/2⌋" using assms(1) by auto
then have "y mod b > ⌊real_of_int b/2⌋"
using assms(2) odd_smaller_b by fastforce
then show False using assms(4) by auto
qed
then have "y ∈ {0..<b}" using assms(2-3)
by (metis atLeastAtMost_iff atLeastLessThan_empty atLeastLessThan_iff floor_divide_of_int_eq
int_div_less_self linorder_not_le numeral_One numeral_less_iff of_int_numeral semiring_norm(76))
then show ?thesis by auto
qed

lemma mod_plus_minus_rangeE:
assumes "y ∈ {-⌊real_of_int b/2⌋..⌊real_of_int b/2⌋}"
"odd b" "b > 0"
shows "y = y mod+- b"
unfolding mod_plus_minus_def
using mod_plus_minus_rangeE_pos[OF assms] mod_plus_minus_rangeE_neg[OF assms]
by auto

text ‹Image of \$0\$.›

lemma mod_plus_minus_zero:
assumes "x mod+- b = 0"
shows "x mod b = 0"
using assms unfolding mod_plus_minus_def
by (metis eq_iff_diff_eq_0 mod_mod_trivial mod_self)

lemma mod_plus_minus_zero':
assumes "b>0" "odd b"
shows "0 mod+- b = (0::int)"
using assms(1) mod_plus_minus_def by force

text ‹‹mod+-› with negative values.›

lemma neg_mod_plus_minus:
assumes "odd b"
"b>0"
shows "(- x) mod+- b = - (x mod+- b)"
proof -
obtain k :: int where k_def: "(-x) mod+- b = (-x)+ k* b"
using mod_plus_minus_def
proof -
assume a1: "⋀k. - x mod+- b = - x + k * b ⟹ thesis"
have "∃i. i mod b + - (x + i) = - x mod+- b"
by (smt (verit, del_insts) mod_add_self1 mod_plus_minus_def)
then show ?thesis
mult.commute mult_minus_left)
qed
then have "(-x) mod+- b = -(x - k*b)" using k_def by auto
also have "… = - ((x-k*b) mod+- b)"
proof -
have range_xkb:"x - k * b ∈
{- ⌊real_of_int b / 2⌋..⌊real_of_int b / 2⌋}"
using k_def mod_plus_minus_range_odd[OF assms(2) assms(1)]
by (smt (verit, ccfv_SIG) atLeastAtMost_iff)
have "x - k*b = (x - k*b) mod+- b"
using mod_plus_minus_rangeE[OF range_xkb assms] by auto
then show ?thesis by auto
qed
also have "-((x - k*b) mod+- b) = -(x mod+- b)"
unfolding mod_plus_minus_def
by (smt (verit, best) mod_mult_self1)
finally show ?thesis by auto
qed

text ‹Representative with ‹mod+-››

lemma mod_plus_minus_rep_ex:
"∃k. x = k*b + x mod+- b"
unfolding mod_plus_minus_def