Demo: the reflective SSP tactic on the real one-time-pad games

Examples/OneTimePad.lean closes its perfect-security stack with a ~40-line hand-written "Reflection into the Package / UC Stack" section: otpGameRaw, the IsValid instance, otpGameRaw_eval, otpGameRaw_eval_eq, otpGameTrue, otpGameFalse, otp_eval_eq, and then the four package theorems (otp_deepnom_zero, otp_nompkg_secure, otp_sdist_zero, otp_uc).

This file reproduces the two headline package results — otp_nompkg_secure and otp_uc — on the same one-time-pad games, each in a single reflect_ofOracle_* invocation, given only the shallow game family and the one shallow coupling reused from OneTimePad.

noncomputable def CatCrypt.Examples.ReflectTacticDemo.otpBody (m : Bool) : Core.SPComp Bool

The shallow one-time-pad oracle body (the SPComp game the package reflects): sample a uniform key and return the ciphertext k ⊕ m.

Equations

• CatCrypt.Examples.ReflectTacticDemo.otpBody m = (CatCrypt.Core.SPComp.sample Bool).bind fun (k : Bool) => CatCrypt.Core.SPComp.pure (k ^^ m)

theorem CatCrypt.Examples.ReflectTacticDemo.otpBody_eq (m₀ m₁ : Bool) : otpBody m₀ = otpBody m₁

The single shallow coupling the tactic consumes, reused from OneTimePad: the two one-time-pad game bodies coincide as SPComp computations (each is the uniform sample). Obtained from OneTimePad's reflected coupling otp_eval_eq via the round-trip otpGameRaw_eval.

theorem CatCrypt.Examples.ReflectTacticDemo.demo_otp_nompkg_secure (m₀ m₁ : Bool) : Crypto.NomPkgSecure (OTP.otpGameTrue m₀) (OTP.otpGameFalse m₁) fun (x : Deep.NomPackage) => 0

otp_nompkg_secure reproduced in one invocation. Package-level perfect security of the reflected OTP games, from the shallow body + shallow coupling.

theorem CatCrypt.Examples.ReflectTacticDemo.demo_otp_uc (m₀ m₁ : Bool) : Crypto.UCEmulates 0 { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool } (fun (A : { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (Crypto.runPkg (A.pkg.link (OTP.otpGameTrue m₀).pkg))) fun (A : { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (Crypto.runPkg (A.pkg.link (OTP.otpGameFalse m₁).pkg))

otp_uc reproduced in one invocation. Perfect UC emulation of the linked OTP game families over the trivial-leak interface, from the shallow body + shallow coupling.