Theory Kyber_NTT_Values

theory Kyber_NTT_Values

imports Kyber_Values
  NTT_Scheme
  Powers3844

begin
section ‹Specification of Kyber with NTT›
text ‹Calculations for NTT specifications›

lemma "3844 * 6584 = (1 :: fin7681 mod_ring)"
  by simp 

lemma "62 * 1115 = (1 :: fin7681 mod_ring)"
  by simp

lemma "256 * 7651 = (1:: fin7681 mod_ring)"
  by simp

lemma "7681 = 30 * 256 + (1::int)" by simp 


lemma powr256:  "3844 ^ 256 = (1::fin7681 mod_ring)" 
proof -
  have calc1: "3844^16 = (7154::fin7681 mod_ring)" by simp
  have calc2: "7154^16 = (1::fin7681 mod_ring)" by simp
  have "(3844::fin7681 mod_ring)^256 = (3844^16)^16"
    by (metis (mono_tags, opaque_lifting) num_double numeral_times_numeral power_mult)
  also have "… = 1" unfolding calc1 calc2 by auto
  finally show ?thesis by blast
qed



lemma powr256':
  "62 ^ 256 = (- 1::fin7681 mod_ring)" 
proof -
  have calc1: "62^16 = (1366::fin7681 mod_ring)" by simp
  have calc2: "1366^16 = (-1::fin7681 mod_ring)" by simp
  have "(62::fin7681 mod_ring)^256 = (62^16)^16"
    by (metis (mono_tags, opaque_lifting) num_double numeral_times_numeral power_mult)
  also have "… = -1" unfolding calc1 calc2 by auto
  finally show ?thesis by blast
qed

(*
powrs 3844^l for l=1..<256 in Powrs_3844 file"
*)


interpretation kyber7681_ntt: kyber_ntt 256 7681 3 8 
  "TYPE(fin7681)" "TYPE(3)" 3844 6584 62 1115 7651 30
proof (unfold_locales, goal_cases)
  case 4
  then show ?case using kyber7681.q_prime by fastforce
next
  case 6
  then show ?case using kyber7681.CARD_k by blast
next
  case 7
  then show ?case by (simp add: qr_poly'_fin7681_def)
next
  case 9
  then show ?case using powr256 by blast
next
  case 11
  then show ?case proof (safe, goal_cases)
    case (1 m)
    then show ?case using powr_less256[OF 1(2)]
      using linorder_not_less by blast
  qed
next
  case 15
  then show ?case using powr256' by blast
next
  case 17
  have mult: "256 * 7651 = (1::fin7681 mod_ring)" by simp
  have of_int: "of_int_mod_ring (int 256) = 256"
    by (metis o_def of_nat_numeral of_nat_of_int_mod_ring)
  show ?case unfolding of_int mult by simp
qed (auto)

end