Theory CRYSTALS-Kyber.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 
  of_int_hom.hom_add of_int_hom.hom_one)
 

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
      using a1 by (metis (no_types) diff_add_cancel diff_diff_add 
      diff_minus_eq_add minus_diff_eq minus_mult_div_eq_mod 
      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 
by (split if_splits)(metis add.right_neutral add_diff_eq div_mod_decomp_int 
  eq_iff_diff_eq_0 mod_add_self2)


lemma mod_plus_minus_rep: 
  obtains k where "x = k*b + x mod+- b"
using mod_plus_minus_rep_ex by auto

text ‹Multiplication in mod+-›

lemma mod_plus_minus_mult: 
  "s*x mod+- q = (s mod+- q) * (x mod+- q) mod+- q"
unfolding mod_plus_minus_def 
by (smt (verit, ccfv_threshold) minus_mod_self2 mod_mult_left_eq mod_mult_right_eq)
end