Hybrid Argument Demonstration using Deep Embedding

This file demonstrates how the deep embedding of CatCrypt enables cleaner and more structured hybrid argument proofs in cryptography.

Overview

A hybrid argument is a proof technique where we show two games are equivalent by constructing a sequence of intermediate games:

Game0 ~ Game1 ~ Game2 ~ ... ~ GameN

where each adjacent pair differs in a small, analyzable way. The deep embedding provides several advantages for such proofs:

1. Structural Induction: We can analyze games by their syntactic structure using RawCode.inductionOn, rather than semantic simulation.

2. Separation Reasoning: The location set structure provides automatic reasoning about disjoint state through DeepPackage.sep.

3. Compositional Reasoning: Package composition (link, par) preserves separation properties.

Comparison with Shallow Embedding

In the shallow embedding (standard CatCrypt), games are represented as Lean functions. Proving equivalence requires manual tracking of state invariants, explicit coupling constructions, and complex simulation arguments.

In the deep embedding, games are syntax trees that allow structural induction on syntax, automatic support/disjointness reasoning, and compositional separation properties.

References

• Larsen and Schürmann, Nominal State-Separating Proofs
• Haselwarter et al., SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
• SSProve Rocq: theories/Crypt/examples/PRF_example.v

Example Interfaces

def CatCrypt.Deep.HybridDemo.queryInterface : DeepInterface

Simple interface with one operation: query : Unit -> Nat

Equations

• CatCrypt.Deep.HybridDemo.queryInterface = { ops := [(0, Unit, ℕ)] }

Behavioral Equivalence

def CatCrypt.Deep.HybridDemo.BehavioralEquiv (p₁ p₂ : DeepPackage) : Prop

Behavioral equivalence of deep packages based on export interface equality.

In a full development, this would compare implementations via denotational semantics. Here we use a simplified definition based on exports.

Equations

• (p₁ ≈ᵇ p₂) = (p₁.exports = p₂.exports)

def CatCrypt.Deep.HybridDemo.«term_≈ᵇ_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

Transitivity of Equivalence

theorem CatCrypt.Deep.HybridDemo.BehavioralEquiv.refl (p : DeepPackage) : p ≈ᵇ p

Behavioral equivalence is reflexive

theorem CatCrypt.Deep.HybridDemo.BehavioralEquiv.symm {p₁ p₂ : DeepPackage} (h : p₁ ≈ᵇ p₂) : p₂ ≈ᵇ p₁

Behavioral equivalence is symmetric

theorem CatCrypt.Deep.HybridDemo.BehavioralEquiv.trans {p₁ p₂ p₃ : DeepPackage} (h₁₂ : p₁ ≈ᵇ p₂) (h₂₃ : p₂ ≈ᵇ p₃) : p₁ ≈ᵇ p₃

Behavioral equivalence is transitive

Separation Properties Demo

theorem CatCrypt.Deep.HybridDemo.sep_of_disjoint_locs (p₁ : DeepPackage) (p₂ : DeepPackage) (h : Disjoint p₁.locs p₂.locs) : p₁.sep p₂

Demonstration: two packages with disjoint location ids are separated.

Hybrid Sequence Structure

structure CatCrypt.Deep.HybridDemo.HybridSequence : Type 1

A hybrid argument is a sequence of games with adjacent equivalences.

• games : List DeepPackage

  The games in the sequence

• nonempty : self.games ≠ []

  Non-empty sequence

theorem CatCrypt.Deep.HybridDemo.hybrid_transitivity (games : List DeepPackage) (h_nonempty : games ≠ []) (h_adj : ∀ (i : ℕ), i + 1 < games.length → games.getD i DeepPackage.empty ≈ᵇ games.getD (i + 1) DeepPackage.empty) : games.head h_nonempty ≈ᵇ games.getLast h_nonempty

The first and last games in a hybrid sequence are equivalent if all adjacent pairs are equivalent.

This is the key theorem for hybrid arguments: we can chain together local equivalences to get global equivalence.

Documentation: Benefits of Deep Embedding for Hybrid Arguments

Key Advantages

1. Explicit Syntax Trees

   • Games are data structures, not opaque functions
   • We can pattern match on code structure
   • Transformations are explicit and verifiable

2. Structural Induction

   • RawCode.inductionOn provides a principled way to analyze all code paths
   • No need for complex simulation relations
   • Proof follows the syntax structure

3. Separation via Location Sets

   • DeepPackage.sep p1 p2 captures state disjointness
   • Composition preserves separation (par_sep_left, par_sep_right)

4. Compositional Reasoning

   • Link and parallel composition have algebraic properties
   • Separation is compositional

Comparison: Shallow vs Deep

Aspect	Shallow	Deep
Games	Functions	Syntax trees
Equivalence	Coupling/simulation	Structural + semantic
State separation	Manual invariants	Automatic via sep
Induction	Semantic domain	Syntax structure

When to Use Deep Embedding

The deep embedding is particularly beneficial when:

• The proof involves multiple games with similar structure
• State separation is a key reasoning principle
• You want to apply program transformations

For simple proofs where semantic reasoning suffices, the shallow embedding may be more direct.