# 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