Raw Code: Free Monad for Computations

This file defines the deep embedding of CatCrypt computations as a free monad.

Main definitions

• RawCode - The free monad representing computation syntax trees
• RawCode.ret - Pure return
• RawCode.bind - Monadic bind (sequencing)
• RawCode.sample - Sample from a uniform distribution
• RawCode.get - Read from a location
• RawCode.put - Write to a location
• RawCode.fail - Failure/exception

Location model

Nominal Structure

Location validity is tracked by the ValidCode inductive predicate (see Package.lean), not by a syntactic locs function on RawCode.

Implementation notes

This is a free monad, meaning it represents computation syntax trees without any semantic interpretation. The monad instance allows using do-notation for building computations, but the monad laws are not necessarily satisfied at the syntactic level (they hold after quotienting by observational equivalence).

We use Core.Location directly to enable axiom-free interpretation to the shallow embedding (SPComp). This unifies the heap model between the deep and shallow embeddings.

References

• SSProve theories/Crypt/rhl_semantics/free_prot/free_code.v
• Larsen and Schürmann, Nominal State-Separating Proofs

inductive CatCrypt.Deep.RawCode : Type u → Type (u + 1)

Raw code: syntax tree for probabilistic stateful computations.

This is a free monad representing:

• Pure computations (ret)
• Sequencing (bind)
• Probabilistic choice (sample)
• State access (get/put)
• Failure (fail)

The type parameter α is the return type of the computation.

Note: We use Core.Location directly to enable axiom-free interpretation to the shallow embedding. Location types are at Type 0 (universe level 0), so get returns ULift.{u} ℓ.ty to lift to universe u.

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

  Embed an arbitrary SPComp value as opaque code. Used to express completeness: any heap-manipulating probabilistic computation has a corresponding RawCode representation whose eval is the original SPComp.

@[match_pattern]

def CatCrypt.Deep.RawCode.pure {α : Type u} (a : α) : RawCode α

Pure return: lift a value into a computation

Equations

• CatCrypt.Deep.RawCode.pure a = CatCrypt.Deep.RawCode.ret a

@[match_pattern]

def CatCrypt.Deep.RawCode.seq {α β : Type u} (c : RawCode α) (k : α → RawCode β) : RawCode β

Monadic bind: sequence two computations

Equations

• c.seq k = c.bind k

@[implicit_reducible]

instance CatCrypt.Deep.RawCode.instMonad : Monad RawCode

Monad instance for RawCode.

Note: This instance is not lawful at the syntactic level! The monad laws hold only after quotienting by observational equivalence. This instance is provided to enable do-notation.

Equations

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

@[implicit_reducible]

instance CatCrypt.Deep.RawCode.instApplicative : Applicative RawCode

Applicative functor instance (derived from Monad)

Equations

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

def CatCrypt.Deep.RawCode.inductionOn {α : Type u} {motive : {α : Type u} → RawCode α → Prop} (c : RawCode α) (ret : ∀ {α : Type u} (a : α), motive (ret a)) (bind : ∀ {α β : Type u} (c : RawCode α) (k : α → RawCode β), motive c → (∀ (a : α), motive (k a)) → motive (c.bind k)) (sample : ∀ (T : Type u) [inst : Fintype T] [inst_1 : Nonempty T], motive (sample T)) (get : ∀ (ℓ : Core.Location), motive (get ℓ)) (put : ∀ (ℓ : Core.Location) (v : ℓ.ty), motive (put ℓ v)) (fail : ∀ {α : Type u}, motive fail) (oracleCall : ∀ (op : ℕ) (dom codom : Type u) (x : dom), motive (oracleCall op dom codom x)) (embed : ∀ {α : Type u} (c : Core.SPComp α), motive (embed c)) : motive c

Structural induction principle for RawCode.

This provides a convenient way to prove properties by structural induction, handling all constructors of the free monad.

Equations

• ⋯ = ⋯

def CatCrypt.Deep.RawCode.sampleFrom (T : Type u) [Fintype T] [Nonempty T] : RawCode T

Helper: sample from a non-empty fintype (with explicit instance arguments)

Equations

• CatCrypt.Deep.RawCode.sampleFrom T = CatCrypt.Deep.RawCode.sample T

@[inline]

def CatCrypt.Deep.RawCode.failure {α : Type u} : RawCode α

Helper: failing computation

Equations

• CatCrypt.Deep.RawCode.failure = CatCrypt.Deep.RawCode.fail

Oracle Call Substitution

substOracle replaces oracle calls in code with concrete implementations. This is the key operation for package linking: after constructing code with oracleCall placeholders, linking substitutes the linked package's implementations.

def CatCrypt.Deep.RawCode.substOracle {α : Type u} (c : RawCode α) (env : ℕ → (dom codom : Type u) → dom → RawCode codom) : RawCode α

Substitute all oracle calls in code with concrete implementations.

Given an environment env that maps operation identifiers and types to RawCode implementations, this function recursively replaces every oracleCall op dom codom x with env op dom codom x.

This is the core of DeepPackage.link: the linked package's implementations become the oracle environment.

Equations

• (CatCrypt.Deep.RawCode.ret a).substOracle env = CatCrypt.Deep.RawCode.ret a
• (c_2.bind k).substOracle env = (c_2.substOracle env).bind fun (a : α_3) => (k a).substOracle env
• (CatCrypt.Deep.RawCode.sample α).substOracle env = CatCrypt.Deep.RawCode.sample α
• (CatCrypt.Deep.RawCode.get ℓ).substOracle env = CatCrypt.Deep.RawCode.get ℓ
• (CatCrypt.Deep.RawCode.put ℓ v).substOracle env = CatCrypt.Deep.RawCode.put ℓ v
• CatCrypt.Deep.RawCode.fail.substOracle env = CatCrypt.Deep.RawCode.fail
• (CatCrypt.Deep.RawCode.oracleCall op dom α x).substOracle env = env op dom α x
• (CatCrypt.Deep.RawCode.embed c_2).substOracle env = CatCrypt.Deep.RawCode.embed c_2

theorem CatCrypt.Deep.RawCode.substOracle_id {α : Type u} (c : RawCode α) : (c.substOracle fun (op : ℕ) (dom codom : Type u) (x : dom) => oracleCall op dom codom x) = c

Substituting with the identity oracle environment (oracleCall) is a no-op.

substOracle c (fun op dom codom x => .oracleCall op dom codom x) = c

This is proved by structural induction on the code tree.

theorem CatCrypt.Deep.RawCode.substOracle_comp {α : Type u} (c : RawCode α) (env₁ env₂ : ℕ → (dom codom : Type u) → dom → RawCode codom) : (c.substOracle env₁).substOracle env₂ = c.substOracle fun (op : ℕ) (dom codom : Type u) (x : dom) => (env₁ op dom codom x).substOracle env₂

Double substitution can be composed into a single substitution.

(c.substOracle env₁).substOracle env₂ = c.substOracle (fun op dom codom x => (env₁ op dom codom x).substOracle env₂)

This is the key lemma for proving associativity of DeepPackage.link.

@[simp]

theorem CatCrypt.Deep.RawCode.substOracle_fail {α : Type u} (env : ℕ → (dom codom : Type u) → dom → RawCode codom) : fail.substOracle env = fail

Substituting into fail gives fail.

@[simp]

theorem CatCrypt.Deep.RawCode.substOracle_ret {α : Type u} (a : α) (env : ℕ → (dom codom : Type u) → dom → RawCode codom) : (ret a).substOracle env = ret a

Substituting into ret gives ret.

inductive CatCrypt.Deep.RawCode.NoOracleCall {α : Type u} : RawCode α → Prop

A predicate asserting that a RawCode tree contains no oracleCall nodes.

Code satisfying NoOracleCall is self-contained: it does not depend on any oracle environment. This is a key property for reduction packages, where non-delegated operations are handled by code that never calls imports.

All code produced by G_core_package_construction satisfies this predicate, since it has imports := ∅.

• ret {α : Type u} (a : α) : (RawCode.ret a).NoOracleCall
• bind {α β : Type u} {c : RawCode β} {k : β → RawCode α} (hc : c.NoOracleCall) (hk : ∀ (b : β), (k b).NoOracleCall) : (c.bind k).NoOracleCall
• sample {T : Type u} [Fintype T] [Nonempty T] : (RawCode.sample T).NoOracleCall
• get (ℓ : Core.Location) : (RawCode.get ℓ).NoOracleCall
• put (ℓ : Core.Location) (v : ℓ.ty) : (RawCode.put ℓ v).NoOracleCall
• fail {α : Type u} : RawCode.fail.NoOracleCall
• embed {α : Type u} (c : Core.SPComp α) : (RawCode.embed c).NoOracleCall

theorem CatCrypt.Deep.RawCode.substOracle_eq_self {α : Type u} {c : RawCode α} (h : c.NoOracleCall) (env : ℕ → (dom codom : Type u) → dom → RawCode codom) : c.substOracle env = c

substOracle is a no-op on code without oracle calls.

This is the foundational lemma for reduction package proofs: when the reduction delegates an operation to G_core's impl (which has no oracle calls), the linking substitution doesn't change the code.

Location Registry

A location registry maps atoms to Core.Locations. This enables nominal reasoning about code while maintaining compatibility with the evaluation that uses Core.Location (with nat ids).

The registry ensures:

1. Each atom maps to a unique Core.Location id
2. The mapping is consistent (same atom always gives same id)
3. Types are preserved

structure CatCrypt.Deep.LocRegistry : Type

A location registry maps atoms to Core.Location ids. This bridges the nominal (atom-based) and evaluation (nat-based) models.

• atomToId : Nominal.Atom → ℕ

  Map from atom to Core.Location id

• injective : Function.Injective self.atomToId

  The mapping is injective: different atoms map to different ids

def CatCrypt.Deep.LocRegistry.default : LocRegistry

Default registry: atoms map directly to their underlying nat value

Equations

• CatCrypt.Deep.LocRegistry.default = { atomToId := CatCrypt.Nominal.Atom.val, injective := ⋯ }

@[implicit_reducible]

instance CatCrypt.Deep.LocRegistry.instInhabited : Inhabited LocRegistry

Equations

• CatCrypt.Deep.LocRegistry.instInhabited = { default := CatCrypt.Deep.LocRegistry.default }

theorem CatCrypt.Deep.LocRegistry.atomToId_ne (reg : LocRegistry) (a₁ a₂ : Nominal.Atom) (h : a₁ ≠ a₂) : reg.atomToId a₁ ≠ reg.atomToId a₂

Two atoms with different values map to different ids