Nominal Advantage

This file defines advantage for nominal packages via the deep embedding.

DeepNomAdvantage uses DeepPackage.link for actual oracle substitution via RawCode.substOracle, enabling adversary-game composition.

Main definitions

• runPkg - Evaluate a DeepPackage's main export (0, Unit, Bool)
• DeepNomAdvantage - Distinguishing probability with adversary composition
• NomPkgSecure - Adversary-dependent game-based security

References

• Larsen and Schürmann, Nominal State-Separating Proofs

Running deep packages

noncomputable def CatCrypt.Crypto.runPkg (p : Deep.DeepPackage) : Core.SPComp Bool

Run a deep package by evaluating its "main" exported operation.

Convention: the main entry point is export operation (0, Unit, Bool). This mirrors the cryptographic game convention where the adversary's main procedure takes no input and returns a boolean guess.

If the package exports (0, Unit, Bool), we evaluate the corresponding RawCode Bool via RawCode.eval to get an SPComp Bool. Otherwise, the package has no main entry point and we return pure true.

In the adversary-composition model:

• The adversary A exports (0, Unit, Bool) (its main procedure)
• The adversary imports operations from the game G
• DeepPackage.link A.pkg G.pkg resolves A's oracle calls via G's exports
• runPkg evaluates the linked adversary's main procedure

Equations

• CatCrypt.Crypto.runPkg p = if h : (0, Unit, Bool) ∈ p.exports.ops then have vc := p.impl 0 Unit Bool h (); vc.code.eval else CatCrypt.Core.SPComp.pure true

noncomputable def CatCrypt.Crypto.runDeep (p : Deep.NomPackage) : Core.SPComp Bool

Run a deep nominal package by delegating to runPkg on the underlying DeepPackage. The nominal structure (registry, atoms) is used only for separation reasoning, not for evaluation.

Equations

• CatCrypt.Crypto.runDeep p = CatCrypt.Crypto.runPkg p.pkg

noncomputable def CatCrypt.Crypto.DeepNomAdvantage (G G' A : Deep.NomPackage) : ENNReal

Advantage on deep nominal packages with adversary composition.

DeepNomAdvantage G G' A measures how well adversary A can distinguish game G from game G':

DeepNomAdvantage G G' A = |Pr[eval(A ∥ G) => 1] - Pr[eval(A ∥ G') => 1]|

The adversary A is linked with each game via DeepPackage.link:

• A.pkg exports the main procedure (0, Unit, Bool)
• A.pkg imports operations that G.pkg / G'.pkg export
• Linking resolves A's oracle calls with G's (resp. G's) implementations
• runPkg evaluates the linked package's main procedure

The atom separation between A and G/G' is an implicit precondition for meaningful security statements.

Equations

• CatCrypt.Crypto.DeepNomAdvantage G G' A = CatCrypt.Crypto.Advantage (CatCrypt.Crypto.runPkg (A.pkg.link G.pkg)) (CatCrypt.Crypto.runPkg (A.pkg.link G'.pkg))

theorem CatCrypt.Crypto.DeepNomAdvantage_triangle (G₁ G₂ G₃ A : Deep.NomPackage) : DeepNomAdvantage G₁ G₃ A ≤ DeepNomAdvantage G₁ G₂ A + DeepNomAdvantage G₂ G₃ A

Triangle inequality for deep nominal advantage.

theorem CatCrypt.Crypto.DeepNomAdvantage_self (G A : Deep.NomPackage) : DeepNomAdvantage G G A = 0

Self-advantage is zero for deep nominal packages.

theorem CatCrypt.Crypto.DeepNomAdvantage_comm (G G' A : Deep.NomPackage) : DeepNomAdvantage G G' A = DeepNomAdvantage G' G A

Deep nominal advantage is symmetric.

theorem CatCrypt.Crypto.DeepNomAdvantage_runPkg_eq (G₀ G₁ G₀' G₁' A : Deep.NomPackage) (h₀ : runPkg (A.pkg.link G₀.pkg) = runPkg (A.pkg.link G₀'.pkg)) (h₁ : runPkg (A.pkg.link G₁.pkg) = runPkg (A.pkg.link G₁'.pkg)) : DeepNomAdvantage G₀ G₁ A = DeepNomAdvantage G₀' G₁' A

Advantage equality under runPkg equivalence.

If two game pairs produce the same SPComp Bool when linked with adversary A, then they have the same advantage. This is the key lemma for code equivalence proofs: show that runPkg (link A G₀) = runPkg (link A G₀') (and similarly for G₁/G₁'), then conclude the advantages are equal.

Typical use: after showing that G₀ and G₀' have the same oracle implementations via runPkg_link_congr, apply this lemma to rewrite the advantage.

theorem CatCrypt.Crypto.DeepNomAdvantage_congr (G₀ G₁ G₀' G₁' A : Deep.NomPackage) (h₀ : G₀ = G₀') (h₁ : G₁ = G₁') : DeepNomAdvantage G₀ G₁ A = DeepNomAdvantage G₀' G₁' A

Advantage equality when games are NomPackage-equal.

A corollary of DeepNomAdvantage_runPkg_eq for the common case where the games are literally equal as NomPackage values.

Linking Correctness

The foundational theorem connecting DeepPackage.link with RawCode.eval: running a linked package is the same as running the first package's main procedure with oracle calls resolved through the second package.

theorem CatCrypt.Crypto.runPkg_link (p₁ p₂ : Deep.DeepPackage) : runPkg (p₁.link p₂) = have this := Classical.dec ((0, Unit, Bool) ∈ p₁.exports.ops); if h : (0, Unit, Bool) ∈ p₁.exports.ops then have vc := p₁.impl 0 Unit Bool h (); have env := fun (op' : ℕ) (dom' codom' : Type) (x' : dom') => have this := Classical.dec ((op', dom', codom') ∈ p₂.exports.ops); if h₂ : (op', dom', codom') ∈ p₂.exports.ops then (p₂.impl op' dom' codom' h₂ x').code else Deep.RawCode.fail; Deep.RawCode.evalWith (fun (op : ℕ) (dom codom : Type) (x : dom) => (env op dom codom x).eval) vc.code else Core.SPComp.pure true

Correctness of package linking with respect to evaluation.

Running a linked package runPkg (link p₁ p₂) is equivalent to evaluating p₁'s main procedure (0, Unit, Bool) with an oracle handler that resolves oracle calls through p₂:

• If (op, dom, codom) is in p₂'s exports, the oracle call is replaced by evaluating p₂'s implementation.
• Otherwise, the oracle call evaluates to SPComp.fail.

This theorem is the semantic justification for DeepNomAdvantage: it shows that DeepPackage.link (a syntactic operation on the free monad) correctly implements oracle resolution at the semantic level (SPComp).

Proof: Unfolds runPkg and DeepPackage.link, then applies eval_substOracle which proves the commutativity of substOracle with eval by structural induction on RawCode.

theorem CatCrypt.Crypto.runPkg_link_congr (A G G' : Deep.DeepPackage) (h_exp : ∀ (op : ℕ) (dom codom : Type) (h₁ : (op, dom, codom) ∈ G.exports.ops) (h₂ : (op, dom, codom) ∈ G'.exports.ops) (x : dom), (G.impl op dom codom h₁ x).code.eval = (G'.impl op dom codom h₂ x).code.eval) (h_ops : G.exports.ops = G'.exports.ops) : runPkg (A.link G) = runPkg (A.link G')

Corollary: If two games have the same oracle implementations for all operations that the adversary calls, then the linked packages produce the same computation.

This is the key lemma for proving DeepNomAdvantage G G' A = 0 when G and G' agree on the operations that A imports.

Link Associativity

Definitional equality link (link p₁ p₂) p₃ = link p₁ (link p₂ p₃) does NOT hold because the oracle substitution environments have different structure. However, both sides produce the same SPComp Bool when evaluated via runPkg.

The key insight: in both formulations, oracle calls in p₁ are resolved as follows:

• If the operation is in p₂'s exports: use p₂'s implementation, with p₂'s own oracle calls resolved through p₃
• If the operation is NOT in p₂'s exports: evaluate to fail (Left: fail.substOracle env₃ = fail; Right: link p₂ p₃ only exports p₂.exports, so the lookup fails)

Therefore the two sides agree semantically.

theorem CatCrypt.Crypto.runPkg_link_assoc (p₁ p₂ p₃ : Deep.DeepPackage) : runPkg ((p₁.link p₂).link p₃) = runPkg (p₁.link (p₂.link p₃))

Link associativity at the evaluation level.

runPkg (link (link p₁ p₂) p₃) = runPkg (link p₁ (link p₂ p₃))

This is the correct formulation of link associativity. We cannot prove link (link p₁ p₂) p₃ = link p₁ (link p₂ p₃) as a definitional equality on DeepPackage because the oracle substitution environments differ structurally. But at the semantic level (after evaluation to SPComp via runPkg), they agree.

The proof uses:

• eval_substOracle: substOracle commutes with eval
• evalWith_substOracle: composed evalWith decomposes
• substOracle_comp: double substitution equals composed substitution

This theorem is critical for the reduction lemma DeepNomAdvantage_link.

Advantage Link (Reduction Lemma)

The key theorem for security reductions: composing a reduction R with both games is equivalent to having R as part of the adversary.

DeepNomAdvantage G₀ G₁ ⟨link A R⟩ = DeepNomAdvantage ⟨link R G₀⟩ ⟨link R G₁⟩ A

This follows from link associativity: link (link A R) G = link A (link R G) So: runPkg (link (link A R) G₀) = runPkg (link A (link R G₀)) runPkg (link (link A R) G₁) = runPkg (link A (link R G₁))

theorem CatCrypt.Crypto.DeepNomAdvantage_link (G₀ G₁ A R : Deep.NomPackage) (hregAR : A.registry = R.registry) (hregRG₀ : R.registry = G₀.registry) (hregRG₁ : R.registry = G₁.registry) : DeepNomAdvantage G₀ G₁ (A.link R hregAR) = DeepNomAdvantage (R.link G₀ hregRG₀) (R.link G₁ hregRG₁) A

Advantage link (reduction lemma) using NomPackage.link.

Composing a reduction wrapper R with both games is equivalent to having R as part of the adversary:

DeepNomAdvantage G₀ G₁ (link A R) = DeepNomAdvantage (link R G₀) (link R G₁) A

This follows directly from runPkg_link_assoc:

• link (link A.pkg R.pkg) G₀.pkg evaluates the same as link A.pkg (link R.pkg G₀.pkg)
• link (link A.pkg R.pkg) G₁.pkg evaluates the same as link A.pkg (link R.pkg G₁.pkg)

This theorem is critical for modular security proofs: it allows us to "absorb" a reduction wrapper R into the adversary A, which is the standard technique for composing security games in hybrid arguments.

Requires compatible registries (all packages use the same registry).

ID Package Properties

theorem CatCrypt.Crypto.runPkg_link_id_right (p : Deep.DeepPackage) : runPkg (p.link (Deep.DeepPackage.id p.imports)) = runPkg p

Linking with the identity package on the right preserves evaluation.

runPkg (link p (id p.imports)) = runPkg p

This holds because:

• id forwards all oracle calls, so oracleCall -> oracleCall
• For p's code, after substOracle with id's env, oracle calls that are in p.imports remain as oracle calls (id forwards them)
• Oracle calls not in p.imports become fail (same as unlinked evaluation)
• In both cases, eval maps unresolved oracle calls to SPComp.fail

So the link with id is semantically a no-op.

theorem CatCrypt.Crypto.runPkg_link_id_left (p : Deep.DeepPackage) (h_main : (0, Unit, Bool) ∈ p.exports.ops) : runPkg ((Deep.DeepPackage.id p.exports).link p) = runPkg p

Linking with the identity package on the left preserves evaluation, provided the main entry point (0, Unit, Bool) is in p's exports.

runPkg (link (id p.exports) p) = runPkg p

This holds because id p.exports's implementation is just oracleCall, which after linking with p gets substituted with p's actual implementation.

Interchange Law

The fundamental interchange law for packages:

link (par p₁ p₂) (par p₃ p₄) ≈ par (link p₁ p₃) (link p₂ p₄)

at the evaluation level (runPkg equality).

This requires an interface matching condition: the oracle environment from par p₃ p₄ must agree with p₃'s environment for operations that p₁ calls (and symmetrically with p₄ for operations that p₂ calls).

In a fully typed setting (where package types encode P : package M E), this condition holds by construction: p₁ only calls operations in M, which are exactly p₃'s exports.

theorem CatCrypt.Crypto.runPkg_interchange (p₁ p₂ p₃ p₄ : Deep.DeepPackage) (h₁₂ : p₁.sep p₂) (h₃₄ : p₃.sep p₄) (h_link_sep : (p₁.link p₃).sep (p₂.link p₄)) (h_main : (0, Unit, Bool) ∈ p₁.exports.ops) (h_env : ∀ (op : ℕ) (dom codom : Type) (x : dom), ((p₃.par p₄ h₃₄).linkEnv op dom codom x).eval = (p₃.linkEnv op dom codom x).eval) : runPkg ((p₁.par p₂ h₁₂).link (p₃.par p₄ h₃₄)) = runPkg ((p₁.link p₃).par (p₂.link p₄) h_link_sep)

Interchange law for package composition.

At the evaluation level:

runPkg (link (par p₁ p₂ h₁₂) (par p₃ p₄ h₃₄)) = runPkg (par (link p₁ p₃) (link p₂ p₄) h_link)

The interface matching condition h_env requires that the oracle environment from par p₃ p₄ agrees with p₃'s environment at the eval level. This is automatically satisfied when:

• p₃ and p₄ have disjoint export operation ids, AND
• p₁ only makes oracle calls to operations in p₃.exports

The proof reduces both sides to evalWith form on the same code, then uses evalWith_congr with the environment agreement hypothesis.

Advantage under Parallel Composition

The interchange law enables reasoning about advantage under parallel composition: the common component C can be absorbed into the adversary.

NomPackage.par / NomPackage.link now exist (Deep/Package.lean), and the runPkg-level interchange law is runPkg_interchange above. The remaining ingredient for DeepNomAdvantage_par is a runPkg-projection lemma (runPkg (par X Y) = runPkg Y when the main export (0, Unit, Bool) ∈ Y), after which the common-component-absorption statement DeepNomAdvantage (par C G₀) (par C G₁) (par A_C A_G) = DeepNomAdvantage G₀ G₁ A_G follows by rewriting each linked run through runPkg_interchange (adversary par A_C A_G, game par C G) and projecting onto the varying link A_G G component.

theorem CatCrypt.Crypto.runPkg_par_right (X Y : Deep.DeepPackage) (hsep : X.sep Y) (h_main : (0, Unit, Bool) ∈ Y.exports.ops) (h_notX : (0, Unit, Bool) ∉ X.exports.ops) : runPkg (X.par Y hsep) = runPkg Y

runPkg projection onto the right component of a parallel composition.

When the main export (0, Unit, Bool) is provided by the right package Y (and NOT by the left package X), running the parallel composition par X Y dispatches the main entry to Y, so it evaluates exactly as runPkg Y.

The par implementation dispatches (0, Unit, Bool) to Y because it is absent from X.exports (h_notX); par_impl_code_eq_right then equates the dispatched code with Y's implementation code (the mono extension to the union of locations is code-preserving).

theorem CatCrypt.Crypto.runPkg_interchange_right (p₁ p₂ p₃ p₄ : Deep.DeepPackage) (h₁₂ : p₁.sep p₂) (h₃₄ : p₃.sep p₄) (h_link_sep : (p₁.link p₃).sep (p₂.link p₄)) (h_notMain : (0, Unit, Bool) ∉ p₁.exports.ops) (h_main : (0, Unit, Bool) ∈ p₂.exports.ops) (h_env : ∀ (op : ℕ) (dom codom : Type) (x : dom), ((p₃.par p₄ h₃₄).linkEnv op dom codom x).eval = (p₄.linkEnv op dom codom x).eval) : runPkg ((p₁.par p₂ h₁₂).link (p₃.par p₄ h₃₄)) = runPkg ((p₁.link p₃).par (p₂.link p₄) h_link_sep)

Interchange law (right-dispatch variant).

The mirror of runPkg_interchange for the case where the main entry (0, Unit, Bool) is exported by the right adversary component p₂ (and not by p₁). Running link (par p₁ p₂) (par p₃ p₄) then dispatches the main entry through p₂, whose oracle calls resolve against p₄, so it equals running par (link p₁ p₃) (link p₂ p₄).

The interface-matching hypothesis h_env requires the oracle environment of par p₃ p₄ to agree (at eval level) with p₄'s environment — the game component that the main-bearing adversary p₂ actually calls.

theorem CatCrypt.Crypto.DeepNomAdvantage_par (C G₀ G₁ A_C A_G : Deep.NomPackage) (hAsep : A_C.atomSep A_G) (hregA : A_C.registry = A_G.registry) (hGsep₀ : C.atomSep G₀) (hregG₀ : C.registry = G₀.registry) (hGsep₁ : C.atomSep G₁) (hregG₁ : C.registry = G₁.registry) (h_notMain : (0, Unit, Bool) ∉ A_C.pkg.exports.ops) (h_main : (0, Unit, Bool) ∈ A_G.pkg.exports.ops) (h_link_sep₀ : (A_C.pkg.link C.pkg).sep (A_G.pkg.link G₀.pkg)) (h_link_sep₁ : (A_C.pkg.link C.pkg).sep (A_G.pkg.link G₁.pkg)) (h_env₀ : ∀ (op : ℕ) (dom codom : Type) (x : dom), ((C.pkg.par G₀.pkg ⋯).linkEnv op dom codom x).eval = (G₀.pkg.linkEnv op dom codom x).eval) (h_env₁ : ∀ (op : ℕ) (dom codom : Type) (x : dom), ((C.pkg.par G₁.pkg ⋯).linkEnv op dom codom x).eval = (G₁.pkg.linkEnv op dom codom x).eval) : DeepNomAdvantage (C.par G₀ hGsep₀ hregG₀) (C.par G₁ hGsep₁ hregG₁) (A_C.par A_G hAsep hregA) = DeepNomAdvantage G₀ G₁ A_G

Advantage under parallel composition: common-component absorption.

A common component C shared by both games can be absorbed into the adversary: distinguishing par C G₀ from par C G₁ with the composed adversary par A_C A_G is exactly as hard as distinguishing G₀ from G₁ with A_G, where A_G is the main-bearing adversary component and A_C is the wrapper connecting to C.

DeepNomAdvantage (par C G₀) (par C G₁) (par A_C A_G) = DeepNomAdvantage G₀ G₁ A_G

Each linked run is rewritten through runPkg_interchange_right (adversary par A_C A_G, game par C Gᵢ, main entry in the right component A_G) into par (link A_C C) (link A_G Gᵢ), then projected with runPkg_par_right onto the varying link A_G Gᵢ component.

The two h_env hypotheses are the interchange interface-matching conditions: the oracle environment of par C Gᵢ must agree at eval level with Gᵢ's environment — the game part that A_G actually calls. The two h_link_sep hypotheses record location-separation of the absorbed runs.

NomPkgSecure: Game-Based UC for Deep Packages

NomPkgSecure G G' ε says that for all adversaries A, the advantage of distinguishing G from G' (via deep linking) is bounded by ε A.

This is the analogue of GameUCEmulates (UC.lean) for the deep package model where adversaries are NomPackage rather than oracle-to-SPComp functions.

The bound is adversary-dependent: ε : NomPackage → ℝ≥0∞. This is essential for concrete security (time/query complexity bounds). For composition, the adversary-dependent bounds add pointwise.

Relationship to other security notions

Notion	Adversary	Composable	Axioms
NomPkgSecure	NomPkg	via triangle	0
GameUCEmulates	OracleIf → SPComp Bool	via triangle	0
sdist ≤ ε	(absorbed)	full PPL	0
UCEmulates	(∀A ∃S)	full UC	0

For TLS games (which use heap state), NomPkgSecure is the strongest notion achievable without proving IsPure for linked packages.

def CatCrypt.Crypto.NomPkgSecure (G G' : Deep.NomPackage) (ε : Deep.NomPackage → ENNReal) : Prop

Adversary-dependent game-based security for NomPkg games.

NomPkgSecure G G' ε states that for all adversaries A : NomPackage, the advantage of distinguishing G from G' is bounded by ε A.

This captures the standard cryptographic game-based security notion where the bound depends on the adversary's complexity (time, oracle queries).

Equations

• CatCrypt.Crypto.NomPkgSecure G G' ε = ∀ (A : CatCrypt.Deep.NomPackage), CatCrypt.Crypto.DeepNomAdvantage G G' A ≤ ε A

theorem CatCrypt.Crypto.NomPkgSecure_refl (G : Deep.NomPackage) : NomPkgSecure G G fun (x : Deep.NomPackage) => 0

Reflexivity: any game is trivially secure against itself.

theorem CatCrypt.Crypto.NomPkgSecure_sym {G G' : Deep.NomPackage} {ε : Deep.NomPackage → ENNReal} (h : NomPkgSecure G G' ε) : NomPkgSecure G' G ε

Symmetry: swapping real and ideal preserves the bound.

theorem CatCrypt.Crypto.NomPkgSecure_trans {G₁ G₂ G₃ : Deep.NomPackage} {ε₁ ε₂ : Deep.NomPackage → ENNReal} (h₁ : NomPkgSecure G₁ G₂ ε₁) (h₂ : NomPkgSecure G₂ G₃ ε₂) : NomPkgSecure G₁ G₃ fun (A : Deep.NomPackage) => ε₁ A + ε₂ A

Transitivity: composition via triangle inequality. The adversary-dependent bounds add pointwise.

theorem CatCrypt.Crypto.NomPkgSecure_mono {G G' : Deep.NomPackage} {ε₁ ε₂ : Deep.NomPackage → ENNReal} (h : NomPkgSecure G G' ε₁) (hle : ∀ (A : Deep.NomPackage), ε₁ A ≤ ε₂ A) : NomPkgSecure G G' ε₂

Monotonicity: weakening the bound.

theorem CatCrypt.Crypto.NomPkgSecure_uniform {G G' : Deep.NomPackage} {ε : Deep.NomPackage → ENNReal} {ε_u : ENNReal} (h : NomPkgSecure G G' ε) (hle : ∀ (A : Deep.NomPackage), ε A ≤ ε_u) : NomPkgSecure G G' fun (x : Deep.NomPackage) => ε_u

Uniform bound version: when the bound doesn't depend on the adversary.