Game Package View: UC-Free Game/Handler Layer

The UC-free core of the PackageView framework: the isomorphism between SPComp games and single-operation typed handlers, plus the handler simp lemmas that drive the pkg_coherence tactic.

The statistical-distance / UC machinery (handlerSdist, oracle-swap theorems, OracleGame, PackageView) lives downstream in the dev-repo layer over this file.

Main Definitions

• singleIface — interface with one operation
• GamePkg.ofGame / GamePkg.toGame — isomorphism (A → SPComp B) ≃ GamePkg A B

Supporting SPComp law

bind_fail_right' is a pure SPComp algebra law consumed by the pkg_coherence simp set (and by uc_coherence in the larger UC development).

theorem CatCrypt.Core.SPComp.bind_fail_right' {α β : Type} (c : SPComp α) : (c.bind fun (x : α) => fail) = fail

Binding into a constant-failure continuation gives failure.

Single-Operation Interface

def CatCrypt.Bridge.PkgView.singleIface (A B : Type) : Category.PkgInterface

A package interface with exactly one operation of type A → SPComp B.

Equations

• CatCrypt.Bridge.PkgView.singleIface A B = { ι := Unit, doms := fun (x : Unit) => A, codoms := fun (x : Unit) => B }

@[reducible, inline]

abbrev CatCrypt.Bridge.PkgView.GamePkg (A B : Type) : Type

A handler for a single-operation interface. Isomorphic to A → SPComp B via ofGame/toGame.

Equations

• CatCrypt.Bridge.PkgView.GamePkg A B = CatCrypt.Category.TypedHandler (CatCrypt.Bridge.PkgView.singleIface A B)

def CatCrypt.Bridge.PkgView.GamePkg.ofGame {A B : Type} (game : A → Core.SPComp B) : GamePkg A B

Wrap an SPComp game as a single-operation handler.

Equations

• CatCrypt.Bridge.PkgView.GamePkg.ofGame game x✝ = game

def CatCrypt.Bridge.PkgView.GamePkg.toGame {A B : Type} (pkg : GamePkg A B) : A → Core.SPComp B

Extract the game from a single-operation handler.

Equations

• pkg.toGame = pkg ()

@[simp]

theorem CatCrypt.Bridge.PkgView.GamePkg.ofGame_toGame {A B : Type} (game : A → Core.SPComp B) : (ofGame game).toGame = game

@[simp]

theorem CatCrypt.Bridge.PkgView.GamePkg.toGame_ofGame {A B : Type} (pkg : GamePkg A B) : ofGame pkg.toGame = pkg

def CatCrypt.Bridge.PkgView.gamePkgEquiv (A B : Type) : (A → Core.SPComp B) ≃ GamePkg A B

The isomorphism between games and single-operation handlers.

Equations

• CatCrypt.Bridge.PkgView.gamePkgEquiv A B = { toFun := CatCrypt.Bridge.PkgView.GamePkg.ofGame, invFun := CatCrypt.Bridge.PkgView.GamePkg.toGame, left_inv := ⋯, right_inv := ⋯ }

Oracle Games (Package Category Morphisms)

@[reducible, inline]

abbrev CatCrypt.Bridge.PkgView.OracleGame (O : Category.PkgInterface) (A B : Type) : Type

An oracle game is a morphism in the package category: it takes an oracle handler and produces a game.

Concretely, OracleGame O A B is TypedHandler O → TypedHandler (singleIface A B), i.e., a morphism O ⟶ singleIface A B in pkgCat.

Equations

• CatCrypt.Bridge.PkgView.OracleGame O A B = (O ⟶ CatCrypt.Bridge.PkgView.singleIface A B)

def CatCrypt.Bridge.PkgView.OracleGame.mk {O : Category.PkgInterface} {A B : Type} (run : Category.TypedHandler O → A → Core.SPComp B) : OracleGame O A B

Construct an oracle game from a function that takes an oracle handler and produces a game.

Equations

• CatCrypt.Bridge.PkgView.OracleGame.mk run h = CatCrypt.Bridge.PkgView.GamePkg.ofGame (run h)

def CatCrypt.Bridge.PkgView.OracleGame.run {O : Category.PkgInterface} {A B : Type} (game : OracleGame O A B) (h : Category.TypedHandler O) : A → Core.SPComp B

Run an oracle game with a specific handler.

Equations

• game.run h = CatCrypt.Bridge.PkgView.GamePkg.toGame (game h)

def CatCrypt.Bridge.PkgView.OracleGame.ofSingleOracle {X Y A B : Type} (run : (X → Core.SPComp Y) → A → Core.SPComp B) : OracleGame (singleIface X Y) A B

An oracle game from a single-oracle function. The common case: the game takes one oracle X → SPComp Y.

Equations

• CatCrypt.Bridge.PkgView.OracleGame.ofSingleOracle run = CatCrypt.Bridge.PkgView.OracleGame.mk fun (h : CatCrypt.Category.TypedHandler (CatCrypt.Bridge.PkgView.singleIface X Y)) => run (h ())

Handler Simp Lemmas for pkg_coherence

These lemmas reduce handler operations to pointwise equalities, enabling the pkg_coherence tactic.

@[simp]

theorem CatCrypt.Bridge.PkgView.TypedHandler.pair_inl {I J : Category.PkgInterface} (h₁ : Category.TypedHandler I) (h₂ : Category.TypedHandler J) (i : I.ι) : h₁.pair h₂ (Sum.inl i) = h₁ i

@[simp]

theorem CatCrypt.Bridge.PkgView.TypedHandler.pair_inr {I J : Category.PkgInterface} (h₁ : Category.TypedHandler I) (h₂ : Category.TypedHandler J) (j : J.ι) : h₁.pair h₂ (Sum.inr j) = h₂ j

@[simp]

theorem CatCrypt.Bridge.PkgView.GamePkg.ofGame_apply {A B : Type} (game : A → Core.SPComp B) : ofGame game () = game

@[simp]

theorem CatCrypt.Bridge.PkgView.singleIface_doms {A B : Type} : (singleIface A B).doms = fun (x : (singleIface A B).ι) => A

@[simp]

theorem CatCrypt.Bridge.PkgView.singleIface_codoms {A B : Type} : (singleIface A B).codoms = fun (x : (singleIface A B).ι) => B