Deep Embedding Packages

This file defines packages for the deep embedding of CatCrypt computations.

Main definitions

• DeepInterface - Specifies operation signatures (id, domain, codomain)
• ValidCode - Code that only uses declared locations
• DeepPackage - A package with location support and interface specifications
• DeepPackage.link - Sequential composition of packages
• DeepPackage.par - Parallel composition of packages
• DeepPackage.sep - Separation predicate (disjoint locations)

Nominal Structure

Packages support nominal operations for automatic state separation:

• NomPackage.atoms - Get the atoms used by a package
• NomPackage.atomSep - Separation based on disjoint atoms
• NomPackage.sep_of_atomSep - Atom separation implies location separation

Overview

In the deep embedding, packages represent cryptographic protocol implementations with explicit state management. Each package:

1. Has a finite set of locations (memory cells) it uses
2. Imports operations from other packages
3. Exports operations it implements
4. Contains code implementations for exported operations

Separation reasoning can be based on either:

• Location id disjointness (DeepPackage.sep)
• Atom disjointness (NomPackage.atomSep) for nominal reasoning

References

• Larsen and Schürmann, Nominal State-Separating Proofs
• SSProve Rocq: theories/Crypt/nominal/Nominal.v, free_code.v

Interfaces

structure CatCrypt.Deep.DeepInterface : Type (u + 1)

An interface specifies the signature of operations. Each operation has an id (for identification), a domain type, and a codomain type. All types are at the same universe u, matching RawCode.oracleCall.

Example: A PRF interface might have:

• Operation 0: Unit → BitVec 128 (key generation)
• Operation 1: BitVec 128 → BitVec 128 (evaluation)

• ops : List (ℕ × Type u × Type u)

  The operations in this interface. Each entry is (operation_id, domain_type, codomain_type).

def CatCrypt.Deep.DeepInterface.empty : DeepInterface

The empty interface with no operations

Equations

• CatCrypt.Deep.DeepInterface.empty = { ops := [] }

@[implicit_reducible]

instance CatCrypt.Deep.DeepInterface.instEmptyCollection : EmptyCollection DeepInterface

Equations

• CatCrypt.Deep.DeepInterface.instEmptyCollection = { emptyCollection := CatCrypt.Deep.DeepInterface.empty }

@[implicit_reducible]

instance CatCrypt.Deep.DeepInterface.instInhabited : Inhabited DeepInterface

Equations

• CatCrypt.Deep.DeepInterface.instInhabited = { default := CatCrypt.Deep.DeepInterface.empty }

def CatCrypt.Deep.DeepInterface.contains (i : DeepInterface) (op_id : ℕ) (dom codom : Type u) : Prop

Check if an operation is in the interface

Equations

• i.contains op_id dom codom = ((op_id, dom, codom) ∈ i.ops)

theorem CatCrypt.Deep.DeepInterface.ext {i₁ i₂ : DeepInterface} (h : i₁.ops = i₂.ops) : i₁ = i₂

Two interfaces are equal if they have the same operations

Valid Code (Inductive Definition)

Following Rocq SSProve, we define validity inductively. This approach:

1. Avoids the problem of computing continuation locations for bind
2. Makes HEq proofs trivial via proof irrelevance
3. Matches the Rocq implementation exactly

inductive CatCrypt.Deep.ValidCode (L : Core.LocSet) (α : Type u) : RawCode α → Prop

Valid code uses only locations from a declared set.

Defined inductively following Rocq SSProve's valid_code. Each constructor checks that location accesses are within the declared set L. Note: We use LocSet (= Finset Nat) for location id sets.

• ret {L : Core.LocSet} {α : Type u} (x : α) : ValidCode L α (RawCode.ret x)
• bind {L : Core.LocSet} {α β : Type u} (c : RawCode α) (k : α → RawCode β) : ValidCode L α c → (∀ (a : α), ValidCode L β (k a)) → ValidCode L β (c.bind k)
• sample {L : Core.LocSet} (T : Type u) [Fintype T] [Nonempty T] : ValidCode L T (RawCode.sample T)
• get {L : Core.LocSet} (ℓ : Core.Location) : ℓ.id ∈ L → ValidCode L (ULift.{u, 0} ℓ.ty) (RawCode.get ℓ)
• put {L : Core.LocSet} (ℓ : Core.Location) (v : ℓ.ty) : ℓ.id ∈ L → ValidCode L (ULift.{u, 0} Unit) (RawCode.put ℓ v)
• fail {L : Core.LocSet} {α : Type u} : ValidCode L α RawCode.fail
• oracleCall {L : Core.LocSet} (op : ℕ) (dom codom : Type u) (x : dom) : ValidCode L codom (RawCode.oracleCall op dom codom x)
• embed {L : Core.LocSet} {α : Type u} (c : Core.SPComp α) : ValidCode L α (RawCode.embed c)

theorem CatCrypt.Deep.ValidCode.mono {L L' : Core.LocSet} (h_sub : L ⊆ L') {α : Type u} {c : RawCode α} (hv : ValidCode L α c) : ValidCode L' α c

Monotonicity: if code is valid for L and L ⊆ L', then code is valid for L'.

structure CatCrypt.Deep.ValidCodeBundle (L : Core.LocSet) (α : Type u_1) : Type (u_1 + 1)

A valid code bundle: code together with its validity proof. This is the structure used in packages.

• code : RawCode α
• valid : ValidCode L α self.code

Type Class for Automatic Validity Proofs

The IsValid type class provides automatic synthesis of ValidCode proofs. This hybrid approach gives the best of both worlds:

• RawCode remains a simple free monad without validity constraints
• ValidCode proofs are synthesized automatically via type class inference
• Manual proofs are still possible when needed

class CatCrypt.Deep.IsValid (L : Core.LocSet) {α : Type u} (c : RawCode α) : Prop

Type class for synthesizing ValidCode proofs automatically.

• proof : ValidCode L α c

instance CatCrypt.Deep.IsValid.ret {L : Core.LocSet} {α : Type u} (x : α) : IsValid L (RawCode.ret x)

ret x is always valid.

instance CatCrypt.Deep.IsValid.bind {L : Core.LocSet} {α β : Type u} (c : RawCode α) (k : α → RawCode β) [hc : IsValid L c] [hk : ∀ (a : α), IsValid L (k a)] : IsValid L (c.bind k)

bind c k is valid if c is valid and k a is valid for all a.

instance CatCrypt.Deep.IsValid.sample {L : Core.LocSet} (T : Type u) [Fintype T] [Nonempty T] : IsValid L (RawCode.sample T)

sample T is always valid.

instance CatCrypt.Deep.IsValid.get {L : Core.LocSet} (ℓ : Core.Location) [h : Fact (ℓ.id ∈ L)] : IsValid L (RawCode.get ℓ)

get ℓ is valid if ℓ.id ∈ L. Uses Fact (ℓ.id ∈ L) to allow instance synthesis when membership is decidable.

instance CatCrypt.Deep.IsValid.put {L : Core.LocSet} (ℓ : Core.Location) (v : ℓ.ty) [h : Fact (ℓ.id ∈ L)] : IsValid L (RawCode.put ℓ v)

put ℓ v is valid if ℓ.id ∈ L. Uses Fact (ℓ.id ∈ L) to allow instance synthesis when membership is decidable.

instance CatCrypt.Deep.IsValid.fail {L : Core.LocSet} {α : Type u} : IsValid L RawCode.fail

fail is always valid.

instance CatCrypt.Deep.IsValid.oracleCall {L : Core.LocSet} (op : ℕ) (dom codom : Type u) (x : dom) : IsValid L (RawCode.oracleCall op dom codom x)

oracleCall is always valid (no location access).

instance CatCrypt.Deep.IsValid.embed {L : Core.LocSet} {α : Type u} (c : Core.SPComp α) : IsValid L (RawCode.embed c)

embed c is always valid: an embedded shallow computation reads no declared location syntactically, so it is valid for every location set. This is the missing companion to the other IsValid instances and is what lets a reified opaque/abstract subterm carry an automatic validity proof.

theorem CatCrypt.Deep.IsValid.toValidCode {L : Core.LocSet} {α : Type u} (c : RawCode α) [h : IsValid L c] : ValidCode L α c

Convert an IsValid instance to a ValidCode proof.

def CatCrypt.Deep.ValidCodeBundle.auto {L : Core.LocSet} {α : Type u} (c : RawCode α) [h : IsValid L c] : ValidCodeBundle L α

Create a ValidCodeBundle automatically using type class synthesis.

Equations

• CatCrypt.Deep.ValidCodeBundle.auto c = { code := c, valid := ⋯ }

def CatCrypt.Deep.ValidCodeBundle.mono {L : Core.LocSet} {α : Type u_1} {L' : Core.LocSet} (h_sub : L ⊆ L') (vc : ValidCodeBundle L α) : ValidCodeBundle L' α

Monotonicity: if code bundle is valid for L, we can extend to any superset L'.

Equations

• CatCrypt.Deep.ValidCodeBundle.mono h_sub vc = { code := vc.code, valid := ⋯ }

theorem CatCrypt.Deep.ValidCodeBundle.eq_of_code_eq {L : Core.LocSet} {α : Type u_3} (vc₁ vc₂ : ValidCodeBundle L α) (h : vc₁.code = vc₂.code) : vc₁ = vc₂

Two ValidCodeBundles with the same location set and code are equal (proof irrelevance).

Oracle Substitution Validity

When we substitute oracle calls with valid code, the result is valid.

theorem CatCrypt.Deep.substOracle_valid {L₁ L₂ : Core.LocSet} {α : Type u} {c : RawCode α} (env : ℕ → (dom codom : Type u) → dom → RawCode codom) (hv : ValidCode L₁ α c) (henv : ∀ (op : ℕ) (dom codom : Type u) (x : dom), ValidCode (L₁ ∪ L₂) codom (env op dom codom x)) : ValidCode (L₁ ∪ L₂) α (c.substOracle env)

Substituting oracle calls with valid code preserves validity.

If c is valid for locations L₁ and every oracle call's replacement is valid for locations L₂, then c.substOracle env is valid for L₁ ∪ L₂.

This is needed for DeepPackage.link: p₁'s code is valid for p₁.locs, and p₂'s implementations are valid for p₂.locs, so the linked code is valid for p₁.locs ∪ p₂.locs.

Deep Packages

structure CatCrypt.Deep.DeepPackage : Type (u + 1)

A package bundles code implementations with interface specifications.

A package consists of:

• A finite set of location ids (state) it uses
• An import interface (operations it calls)
• An export interface (operations it implements)
• Code implementations for each exported operation

The key invariant is that implementations only use declared locations, enabling modular composition and separation reasoning.

• locs : Core.LocSet

  The finite set of location ids used by this package

• imports : DeepInterface

  Operations this package imports (calls from other packages)

• exports : DeepInterface

  Operations this package exports (implements)

• impl (op : ℕ) (dom codom : Type u) : (op, dom, codom) ∈ self.exports.ops → dom → ValidCodeBundle self.locs codom

  Implementation of exported operations. For each operation in the export interface, we provide code (bundled with validity proof) that maps domain values to a computation producing codomain values. All types are at universe u, matching RawCode.oracleCall and substOracle.

Basic operations

def CatCrypt.Deep.DeepPackage.empty : DeepPackage

Empty package with no locations, no imports, no exports

Equations

• CatCrypt.Deep.DeepPackage.empty = { locs := ∅, imports := ∅, exports := ∅, impl := fun (x : ℕ) (x_1 x_2 : Type ?u.1) (h : (x, x_1, x_2) ∈ ∅.ops) (x_3 : x_1) => nomatch h }

@[implicit_reducible]

instance CatCrypt.Deep.DeepPackage.instEmptyCollection : EmptyCollection DeepPackage

Equations

• CatCrypt.Deep.DeepPackage.instEmptyCollection = { emptyCollection := CatCrypt.Deep.DeepPackage.empty }

@[implicit_reducible]

instance CatCrypt.Deep.DeepPackage.instInhabited : Inhabited DeepPackage

Equations

• CatCrypt.Deep.DeepPackage.instInhabited = { default := CatCrypt.Deep.DeepPackage.empty }

Separation

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

Two packages are separated if their location ids are disjoint.

This is the key property for modular reasoning: separated packages cannot interfere with each other's state.

Equations

• p₁.sep p₂ = Disjoint p₁.locs p₂.locs

theorem CatCrypt.Deep.DeepPackage.sep_comm (p₁ : DeepPackage) (p₂ : DeepPackage) : p₁.sep p₂ ↔ p₂.sep p₁

theorem CatCrypt.Deep.DeepPackage.sep_empty_left (p : DeepPackage) : empty.sep p

theorem CatCrypt.Deep.DeepPackage.sep_empty_right (p : DeepPackage) : p.sep empty

Package Composition

noncomputable def CatCrypt.Deep.DeepPackage.link (p₁ p₂ : DeepPackage) : DeepPackage

Sequential composition (linking) of packages.

link p₁ p₂ connects p₂'s exported operations to p₁'s imports. The resulting package:

• Uses locations from both packages
• Imports p₂'s imports (operations not provided by p₂)
• Exports p₁'s exports
• Implementations from p₁, with oracle calls resolved via substOracle

Oracle calls in p₁'s code are resolved as follows:

• If the called operation is in p₂'s exports, the call is replaced with p₂'s implementation (extended to the union of locations)
• If not, the oracle call is left as-is (evaluates to failure or is resolved by further linking)

Equations

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

noncomputable def CatCrypt.Deep.DeepPackage.linkCode {L₁ L₂ : Core.LocSet} {α : Type u} (vc : ValidCodeBundle L₁ α) (env : ℕ → (dom codom : Type u) → dom → RawCode codom) (henv : ∀ (op : ℕ) (dom codom : Type u) (x : dom), ValidCode (L₁ ∪ L₂) codom (env op dom codom x)) : ValidCodeBundle (L₁ ∪ L₂) α

Link a specific operation's code with an oracle environment.

Given code c at universe u and an oracle environment env that provides implementations for oracle calls, this produces linked code where oracle calls are substituted with implementations.

This is a lower-level building block than link. Use it when you need custom oracle environments rather than linking two packages.

Equations

• CatCrypt.Deep.DeepPackage.linkCode vc env henv = { code := vc.code.substOracle env, valid := ⋯ }

noncomputable def CatCrypt.Deep.DeepPackage.par (p₁ p₂ : DeepPackage) (_h_sep : p₁.sep p₂) : DeepPackage

Parallel composition of packages with disjoint locations.

par p₁ p₂ sep_proof combines two packages that don't share state. The resulting package:

• Uses locations from both packages (guaranteed disjoint)
• Imports operations from both packages
• Exports operations from both packages
• Implementations from both packages (extended to the larger location set)

The separation proof ensures no interference between packages.

Equations

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

Par Implementation Characterization

theorem CatCrypt.Deep.DeepPackage.par_impl_code_eq_left (p₁ p₂ : DeepPackage) (h_sep : p₁.sep p₂) (op : ℕ) (dom codom : Type u) (h₁ : (op, dom, codom) ∈ p₁.exports.ops) (h_par : (op, dom, codom) ∈ (p₁.par p₂ h_sep).exports.ops) (x : dom) : ((p₁.par p₂ h_sep).impl op dom codom h_par x).code = (p₁.impl op dom codom h₁ x).code

When the operation is in p₁'s exports, par dispatches to p₁'s implementation. The code is the same (mono only affects the validity proof, not the code).

theorem CatCrypt.Deep.DeepPackage.par_impl_code_eq_right (p₁ p₂ : DeepPackage) (h_sep : p₁.sep p₂) (op : ℕ) (dom codom : Type u) (h₁ : (op, dom, codom) ∉ p₁.exports.ops) (h₂ : (op, dom, codom) ∈ p₂.exports.ops) (h_par : (op, dom, codom) ∈ (p₁.par p₂ h_sep).exports.ops) (x : dom) : ((p₁.par p₂ h_sep).impl op dom codom h_par x).code = (p₂.impl op dom codom h₂ x).code

When the operation is NOT in p₁'s exports, par dispatches to p₂'s implementation.

Properties

theorem CatCrypt.Deep.DeepPackage.par_sep_left (p₁ : DeepPackage) (p₂ p₃ : DeepPackage) (h₁₂ : p₁.sep p₂) (h₁₃ : p₁.sep p₃) (h₂₃ : p₂.sep p₃) : p₁.sep (p₂.par p₃ h₂₃)

Separation is preserved by parallel composition

theorem CatCrypt.Deep.DeepPackage.par_sep_right (p₁ p₂ : DeepPackage) (p₃ : DeepPackage) (h₁₂ : p₁.sep p₂) (h₁₃ : p₁.sep p₃) (h₂₃ : p₂.sep p₃) : (p₁.par p₂ h₁₂).sep p₃

Separation is preserved by parallel composition (right)

theorem CatCrypt.Deep.DeepPackage.par_comm (p₁ p₂ : DeepPackage) (h₁₂ : p₁.sep p₂) (h₂₁ : p₂.sep p₁) : (p₁.par p₂ h₁₂).locs = (p₂.par p₁ h₂₁).locs

Parallel composition is commutative up to reordering

Identity Package

The identity (passthrough) package for an interface. It forwards all operations from its exports to its imports by making oracle calls. This is the unit of linking: link p (id p.imports) = p and link (id p.exports) p = p (up to evaluation equivalence).

noncomputable def CatCrypt.Deep.DeepPackage.id (iface : DeepInterface) : DeepPackage

The identity package for an interface: forwards every operation to the oracle.

For each operation in the interface, the implementation is simply an oracle call, i.e., it passes the request through unchanged. This package has no locations (no state of its own).

This is the monoidal unit for link:

• link p (id p.imports) is evaluation-equivalent to p
• link (id p.exports) p is evaluation-equivalent to p

Equations

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

Linking Properties

noncomputable def CatCrypt.Deep.DeepPackage.linkEnv (p₂ : DeepPackage) (op : ℕ) (dom codom : Type u) : dom → RawCode codom

The oracle environment built by link from a package p₂.

This extracts the oracle substitution function from link's definition for use in compositional reasoning. For each operation:

• If (op, dom, codom) ∈ p₂.exports.ops, use p₂'s implementation
• Otherwise, return fail

Equations

• p₂.linkEnv op dom codom x = if h : (op, dom, codom) ∈ p₂.exports.ops then (p₂.impl op dom codom h x).code else CatCrypt.Deep.RawCode.fail

theorem CatCrypt.Deep.DeepPackage.link_id_right_code (p : DeepPackage) (op : ℕ) (dom codom : Type u) (h : (op, dom, codom) ∈ p.exports.ops) (x : dom) : ((p.link (id p.imports)).impl op dom codom h x).code = (p.impl op dom codom h x).code.substOracle (id p.imports).linkEnv

Linking with the identity package on the right preserves the code of each exported operation (up to oracle calls becoming identity).

Specifically, for any operation in p.exports, the linked code (link p (id p.imports)).impl op dom codom h x has the same substOracle structure: oracle calls not in p.imports become fail, oracle calls in p.imports remain as oracle calls.

At the evaluation level, this means link p (id p.imports) behaves the same as p (since unlinked oracle calls evaluate to fail anyway).

Nominal Packages

NomPackage wraps DeepPackage with a location registry, enabling atom-based separation reasoning.

structure CatCrypt.Deep.NomPackage : Type 1

Nominal package: DeepPackage with an associated location registry. This enables nominal reasoning (atom-based separation) while maintaining compatibility with evaluation.

The key invariant locs_eq ensures that the location set is exactly the image of atoms under the registry mapping. This enables proving that atom separation implies location separation.

• pkg : DeepPackage

  The underlying DeepPackage

• registry : LocRegistry

  The registry mapping atoms to Core.Location ids

• usedAtoms : Finset Nominal.Atom

  The atoms used by this package

• locs_eq : self.pkg.locs = Finset.image self.registry.atomToId self.usedAtoms

  Invariant: locs is exactly the image of atoms under atomToId

def CatCrypt.Deep.NomPackage.locs (p : NomPackage) : Core.LocSet

Get the location ids used by the package

Equations

• p.locs = p.pkg.locs

def CatCrypt.Deep.NomPackage.atoms (p : NomPackage) : Finset Nominal.Atom

Get the atoms used by the package

Equations

• p.atoms = p.usedAtoms

def CatCrypt.Deep.NomPackage.empty : NomPackage

Empty nominal package

Equations

• CatCrypt.Deep.NomPackage.empty = { pkg := CatCrypt.Deep.DeepPackage.empty, locs_eq := CatCrypt.Deep.NomPackage.empty._proof_1 }

@[implicit_reducible]

instance CatCrypt.Deep.NomPackage.instEmptyCollection : EmptyCollection NomPackage

Equations

• CatCrypt.Deep.NomPackage.instEmptyCollection = { emptyCollection := CatCrypt.Deep.NomPackage.empty }

@[implicit_reducible]

instance CatCrypt.Deep.NomPackage.instInhabited : Inhabited NomPackage

Equations

• CatCrypt.Deep.NomPackage.instInhabited = { default := CatCrypt.Deep.NomPackage.empty }

def CatCrypt.Deep.NomPackage.atomSep (p₁ p₂ : NomPackage) : Prop

Two packages are atom-separated if their atoms are disjoint. This is the key property for nominal modular reasoning.

Equations

• p₁.atomSep p₂ = Disjoint p₁.atoms p₂.atoms

theorem CatCrypt.Deep.NomPackage.atomSep_comm (p₁ p₂ : NomPackage) : p₁.atomSep p₂ ↔ p₂.atomSep p₁

theorem CatCrypt.Deep.NomPackage.atomSep_empty_left (p : NomPackage) : empty.atomSep p

theorem CatCrypt.Deep.NomPackage.atomSep_empty_right (p : NomPackage) : p.atomSep empty

theorem CatCrypt.Deep.NomPackage.sep_of_atomSep (p₁ p₂ : NomPackage) (h : p₁.atomSep p₂) (hreg : p₁.registry = p₂.registry) : p₁.pkg.sep p₂.pkg

If packages are atom-separated with the same registry, they are location-separated. This follows from the locs_eq invariant and injectivity of the registry.

noncomputable def CatCrypt.Deep.NomPackage.par (p₁ p₂ : NomPackage) (h : p₁.atomSep p₂) (hreg : p₁.registry = p₂.registry) : NomPackage

Parallel composition of nominal packages. Requires atom separation and the same registry.

Equations

• p₁.par p₂ h hreg = { pkg := p₁.pkg.par p₂.pkg ⋯, registry := p₁.registry, usedAtoms := p₁.atoms ∪ p₂.atoms, locs_eq := ⋯ }

noncomputable def CatCrypt.Deep.NomPackage.link (p₁ p₂ : NomPackage) (hreg : p₁.registry = p₂.registry := by rfl) : NomPackage

Sequential composition (linking) of nominal packages. link p₁ p₂ connects p₂'s exports to p₁'s imports. The resulting package uses atoms from both packages.

Equations

• p₁.link p₂ hreg = { pkg := p₁.pkg.link p₂.pkg, registry := p₁.registry, usedAtoms := p₁.atoms ∪ p₂.atoms, locs_eq := ⋯ }

Documentation

This implementation provides the core package structure for the deep embedding. Key completed features:

1. DeepInterface: Operation signatures with (id, domain, codomain)
2. ValidCode: Code restricted to declared locations
3. DeepPackage: Packages with location sets and interface specifications
4. Composition: link (sequential) and par (parallel) operations
5. Separation: The sep predicate for disjoint location reasoning

Nominal Extension

The NomPackage type adds nominal structure:

• NomPackage.atoms - Atoms used by the package
• NomPackage.atomSep - Atom-based separation
• NomPackage.sep_of_atomSep - Atom separation implies location separation