Package Behavioral Equivalence

This file defines behavioral equivalence for deep packages and proves that package linking preserves it.

Main definitions

• DeepPackage.BehavEquiv - Two packages are behaviorally equivalent if they have the same exports and produce the same SPComp for every exported operation under every oracle handler.

Main results

• link_evalOp_eq - Linking correctness: evaluating a linked operation equals evaluating the original code with oracles resolved via evalWith.
• BehavEquiv.link_congr_right - If p₂ ≡ p₃, then p₁.link p₂ ≡ p₁.link p₃.
• BehavEquiv.advantage_link_congr - If p₂ ≡ p₃, the advantage of distinguishing p₁.link p₂ from p₁.link p₃ is zero.

Design

Behavioral equivalence is defined semantically using evalWith, which interprets RawCode into SPComp given an oracle handler. Two packages are equivalent when, for every shared exported operation, evaluating their implementations with any oracle handler yields the same SPComp computation.

This is stronger than just comparing eval (which maps unresolved oracles to fail), because it captures how the packages behave when composed with arbitrary environments.

References

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

Behavioral Equivalence

structure CatCrypt.Deep.DeepPackage.BehavEquiv (p₁ p₂ : DeepPackage) : Prop

Two deep packages are behaviorally equivalent if:

1. They have the same export interface.
2. For every exported operation and every oracle handler, their implementations produce the same SPComp computation.

This captures semantic equivalence: the packages are interchangeable in any context (linking environment). Using evalWith rather than eval ensures we account for how the code behaves when oracle calls are resolved by an arbitrary environment.

• exports_eq : p₁.exports = p₂.exports

  The packages export the same operations

• impl_eq (op : ℕ) (dom codom : Type u) (h₁ : (op, dom, codom) ∈ p₁.exports.ops) (h₂ : (op, dom, codom) ∈ p₂.exports.ops) (x : dom) (oracle : ℕ → (dom' codom' : Type u) → dom' → Core.SPComp codom') : RawCode.evalWith oracle (p₁.impl op dom codom h₁ x).code = RawCode.evalWith oracle (p₂.impl op dom codom h₂ x).code

  For every exported operation and oracle handler, the evaluations agree

theorem CatCrypt.Deep.DeepPackage.BehavEquiv.refl (p : DeepPackage) : p.BehavEquiv p

Behavioral equivalence is reflexive.

theorem CatCrypt.Deep.DeepPackage.BehavEquiv.symm {p₁ p₂ : DeepPackage} (h : p₁.BehavEquiv p₂) : p₂.BehavEquiv p₁

Behavioral equivalence is symmetric.

theorem CatCrypt.Deep.DeepPackage.BehavEquiv.trans {p₁ p₂ p₃ : DeepPackage} (h₁₂ : p₁.BehavEquiv p₂) (h₂₃ : p₂.BehavEquiv p₃) : p₁.BehavEquiv p₃

Behavioral equivalence is transitive.

Linking Correctness

theorem CatCrypt.Deep.DeepPackage.link_evalOp_eq (p₁ p₂ : DeepPackage) (op : ℕ) (dom codom : Type u) (h : (op, dom, codom) ∈ p₁.exports.ops) (x : dom) : ((p₁.link p₂).impl op dom codom h x).code.eval = RawCode.evalWith (fun (op' : ℕ) (dom' codom' : Type u) (x' : dom') => (p₂.linkEnv op' dom' codom' x').eval) (p₁.impl op dom codom h x).code

Linking correctness: Evaluating a linked operation is the same as evaluating the original code with an oracle handler that dispatches to the linked package's implementations.

Concretely, for an operation (op, dom, codom) exported by p₁:

((p₁.link p₂).impl op dom codom h x).code.eval
  = (p₁.impl op dom codom h x).code.evalWith (fun op' dom' codom' x' =>
      linkEnv p₂ op' dom' codom' x' |>.eval)

This follows directly from eval_substOracle.

theorem CatCrypt.Deep.DeepPackage.link_evalWith_eq (p₁ p₂ : DeepPackage) (op : ℕ) (dom codom : Type u) (h : (op, dom, codom) ∈ p₁.exports.ops) (x : dom) (oracle : ℕ → (dom' codom' : Type u) → dom' → Core.SPComp codom') : RawCode.evalWith oracle ((p₁.link p₂).impl op dom codom h x).code = RawCode.evalWith (fun (op' : ℕ) (dom' codom' : Type u) (x' : dom') => RawCode.evalWith oracle (p₂.linkEnv op' dom' codom' x')) (p₁.impl op dom codom h x).code

Generalized linking correctness with an arbitrary outer oracle handler.

Evaluating a linked operation with handler oracle equals evaluating the original code with a composed handler: oracle calls first go through p₂'s link environment (via substOracle), then the result is evaluated with oracle.

This follows from evalWith_substOracle.

Linking Preserves Behavioral Equivalence

theorem CatCrypt.Deep.DeepPackage.BehavEquiv.link_congr_right (p₁ : DeepPackage) {p₂ p₃ : DeepPackage} (h : p₂.BehavEquiv p₃) : (p₁.link p₂).BehavEquiv (p₁.link p₃)

Right congruence for linking: If p₂ and p₃ are behaviorally equivalent, then p₁.link p₂ is behaviorally equivalent to p₁.link p₃.

The proof unfolds link on both sides, applies evalWith_substOracle to reduce to evaluating p₁'s code with composed handlers, then shows the handlers agree because p₂ and p₃ agree (by behavioral equivalence).

theorem CatCrypt.Deep.DeepPackage.BehavEquiv.link_congr_left {p₁ p₂ : DeepPackage} (q : DeepPackage) (h : p₁.BehavEquiv p₂) : (p₁.link q).BehavEquiv (p₂.link q)

Left congruence for linking: If p₁ and p₂ are behaviorally equivalent and have the same imports, then p₁.link q is behaviorally equivalent to p₂.link q.

The proof uses evalWith_congr in the other direction: now the outer code differs (p₁ vs p₂) but the oracle environment is the same (q).

Advantage from Behavioral Equivalence

theorem CatCrypt.Deep.DeepPackage.BehavEquiv.evalOp_eq {p₁ p₂ : DeepPackage} (h : p₁.BehavEquiv p₂) (op : ℕ) (dom codom : Type u) (h₁ : (op, dom, codom) ∈ p₁.exports.ops) (h₂ : (op, dom, codom) ∈ p₂.exports.ops) (x : dom) : p₁.evalOp op dom codom h₁ x = p₂.evalOp op dom codom h₂ x

If two packages are behaviorally equivalent, evaluating any exported operation (with eval, i.e., unresolved oracles become fail) gives the same SPComp.

theorem CatCrypt.Deep.DeepPackage.BehavEquiv.advantage_link_congr (p₁ : DeepPackage) {p₂ p₃ : DeepPackage} (h : p₂.BehavEquiv p₃) (op : ℕ) (dom codom : Type) (h₁₂ : (op, dom, codom) ∈ (p₁.link p₂).exports.ops) (h₁₃ : (op, dom, codom) ∈ (p₁.link p₃).exports.ops) (x : dom) (A : codom → Core.SPComp Bool) : Crypto.AdvantageA ((p₁.link p₂).evalOp op dom codom h₁₂ x) ((p₁.link p₃).evalOp op dom codom h₁₃ x) A = 0

Zero advantage from behavioral equivalence of linked packages.

If p₂ ≡ p₃, then for any distinguisher package p₁ and any adversary A, the advantage of distinguishing p₁.link p₂ from p₁.link p₃ is zero (for any exported operation used as the game).

Specialized to universe 0 because AdvantageA requires {α : Type}.

This follows from:

1. link_congr_right gives p₁.link p₂ ≡ p₁.link p₃
2. Behavioral equivalence implies evalOp equality
3. Equal SPComps have zero advantage

Useful Derived Lemmas

theorem CatCrypt.Deep.DeepPackage.link_evalOp_congr_right (p₁ : DeepPackage) {p₂ p₃ : DeepPackage} (h : p₂.BehavEquiv p₃) (op : ℕ) (dom codom : Type u) (h₁₂ : (op, dom, codom) ∈ (p₁.link p₂).exports.ops) (h₁₃ : (op, dom, codom) ∈ (p₁.link p₃).exports.ops) (x : dom) : (p₁.link p₂).evalOp op dom codom h₁₂ x = (p₁.link p₃).evalOp op dom codom h₁₃ x

Linking with behaviorally equivalent packages gives the same evalOp.

This is a convenience wrapper combining link_congr_right and evalOp_eq.

theorem CatCrypt.Deep.DeepPackage.BehavEquiv.rHoare_evalOp {p₁ p₂ : DeepPackage} (h : p₁.BehavEquiv p₂) (op : ℕ) (dom codom : Type u) (h₁ : (op, dom, codom) ∈ p₁.exports.ops) (h₂ : (op, dom, codom) ∈ p₂.exports.ops) (x : dom) : Relational.rHoare Relational.eqPre (p₁.evalOp op dom codom h₁ x) (p₂.evalOp op dom codom h₂ x) Relational.eqPost

rHoare from behavioral equivalence: equivalent packages satisfy relational Hoare logic with eqPre/eqPost.