Theory Kyber_Values

```theory Kyber_Values
imports
Crypto_Scheme
(* Check_Prime *)
(* NTT_Scheme *)
begin

section ‹Specification for Kyber›

typedef fin7681 = "{0..<7681::int}"
morphisms fin7681_rep fin7681_abs
by (rule_tac x = 0 in exI, simp)

setup_lifting type_definition_fin7681

lemma CARD_fin7681 [simp]: "CARD (fin7681) = 7681"
unfolding type_definition.card [OF type_definition_fin7681]
by simp

lemma fin7681_nontriv [simp]: "1 < CARD(fin7681)"
unfolding CARD_fin7681 by auto

lemma prime_7681: "prime (7681::nat)" by eval

instantiation fin7681 :: comm_ring_1
begin

lift_definition zero_fin7681 :: "fin7681" is "0" by simp

lift_definition one_fin7681 :: "fin7681" is "1" by simp

lift_definition plus_fin7681 :: "fin7681 ⇒ fin7681 ⇒ fin7681"
is "(λx y. (x+y) mod 7681)"
by auto

lift_definition uminus_fin7681 :: "fin7681 ⇒ fin7681"
is "(λx. (uminus x) mod 7681)"
by auto

lift_definition minus_fin7681 :: "fin7681 ⇒ fin7681 ⇒ fin7681"
is "(λx y. (x-y) mod 7681)"
by auto

lift_definition times_fin7681 :: "fin7681 ⇒ fin7681 ⇒ fin7681"
is "(λx y. (x*y) mod 7681)"
by auto

instance
proof
fix a b c ::fin7681
show "a * b * c = a * (b * c)"
by (transfer, simp add: algebra_simps mod_mult_left_eq mod_mult_right_eq)
show "a + b + c = a + (b + c)"
show "(a + b) * c = a * c + b * c"
by (transfer, simp add: algebra_simps mod_add_right_eq  mod_mult_right_eq)
qed (transfer; simp add: algebra_simps mod_add_right_eq; fail)+

end

instantiation fin7681 :: finite
begin
instance
proof
show "finite (UNIV :: fin7681 set)" unfolding type_definition.univ [OF type_definition_fin7681]
by auto
qed
end

instantiation fin7681 :: equal
begin
lift_definition equal_fin7681 :: "fin7681 ⇒ fin7681 ⇒ bool" is "(=)" .
instance by (intro_classes, transfer, auto)
end

instantiation fin7681 :: nontriv
begin
instance
proof
show "1 < CARD(fin7681)" unfolding CARD_fin7681 by auto
qed
end

instantiation fin7681 :: prime_card
begin
instance
proof
show "prime CARD(fin7681)" unfolding CARD_fin7681 using prime_7681
by blast
qed
end

instantiation fin7681 :: qr_spec
begin

definition qr_poly'_fin7681:: "fin7681 itself ⇒ int poly" where
"qr_poly'_fin7681 ≡ (λ_. Polynomial.monom (1::int) 256 + 1)"

instance proof
have "lead_coeff (qr_poly' TYPE(fin7681)) = 1" unfolding qr_poly'_fin7681_def
then show "¬ int CARD(fin7681) dvd
unfolding CARD_fin7681 by auto
next
have "degree (qr_poly' TYPE(fin7681)) = 256" unfolding qr_poly'_fin7681_def
then show "0 < degree (qr_poly' TYPE(fin7681))"  by auto
qed
end

lift_definition to_int_fin7681 :: "fin7681 ⇒ int" is "λx. x" .

lift_definition of_int_fin7681 :: "int ⇒ fin7681" is "λx. (x mod 7681)"
by simp

interpretation to_int_fin7681_hom: inj_zero_hom to_int_fin7681
by (unfold_locales; transfer, auto)

interpretation of_int_fin7681_hom: zero_hom of_int_fin7681
by (unfold_locales, transfer, auto)

lemma to_int_fin7681_of_int_fin7681 [simp]:
"to_int_fin7681 (of_int_fin7681 x) = x mod 7681"
using of_int_fin7681.rep_eq to_int_fin7681.rep_eq by presburger

lemma of_int_fin7681_to_int_fin7681 [simp]:
"of_int_fin7681 (to_int_fin7681 x) = x"
using fin7681_rep to_int_fin7681.rep_eq to_int_fin7681_hom.injectivity
to_int_fin7681_of_int_fin7681 by force

lemma of_int_mod_ring_eq_iff [simp]:
"(of_int_fin7681 a = of_int_fin7681 b) ⟷
((a mod 7681) = (b mod 7681))"
by (metis of_int_fin7681.abs_eq of_int_fin7681.rep_eq)

interpretation kyber7681: kyber_spec 256 7681 3 8 "TYPE(fin7681)" "TYPE(3)"
proof (unfold_locales, goal_cases)
case 4
then show ?case using prime_7681 prime_int_numeral_eq by blast
next
case 5
then show ?case using CARD_fin7681 by auto
next
case 7
then show ?case unfolding qr_poly'_fin7681_def by auto
qed auto

end```