Valid Packages

This file defines valid packages - raw packages with proofs that they correctly implement their interface and only access declared locations.

Main definitions

• ValidCode - A computation that only accesses locations in L and imports from I
• ValidPackage - A package that correctly implements interface E using imports from I
• fseparate - Two packages have disjoint locations

References

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

structure CatCrypt.Package.LocAccess : Type 1

Specification of location access in code. A full implementation would track this syntactically; this uses a semantic characterization.

• reads : Locations

  Locations that may be read

• writes : Locations

  Locations that may be written

class CatCrypt.Package.ValidCode (L : Locations) (I : Interface) (α : Type u_1) (c : Core.SPComp α) : Prop

Code validity: only accesses locations in L and imports from I. This is a predicate on computations asserting they respect the declared locations and import interface.

Note: A full implementation would require tracking access syntactically or using a free monad representation. This uses a Prop-level assertion.

The reads_in_L condition says the return-value distribution is unchanged when an out-of-scope location is overwritten — the code doesn't read it.

• reads_in_L (l : Core.Location) (v : l.ty) (h : Core.Heap) : l ∉ L → ((c h).bind fun (x : α × Core.Heap) => match x with | (a, snd) => Prob.SDistr.pure a) = (c (h.set l v)).bind fun (x : α × Core.Heap) => match x with | (a, snd) => Prob.SDistr.pure a

  The code's return-value distribution does not depend on locations outside L

• writes_in_L (l : Core.Location) (h : Core.Heap) : l ∉ L → ((c h).bind fun (x : α × Core.Heap) => match x with | (a, h₁) => Prob.SDistr.pure (a, h₁.get l)) = (c h).bind fun (x : α × Core.Heap) => match x with | (a, snd) => Prob.SDistr.pure (a, h.get l)

  The code only writes to locations in L

structure CatCrypt.Package.ValidPackage (L : Locations) (I E : Interface) (P : RawPackage) : Prop

A valid package correctly implements an export interface using an import interface.

• L: the locations the package may access
• I: the interface the package may import
• E: the interface the package exports

• exports_complete (id : ℕ) (S T : Type) : E.has id S T → P.has id S T

  The package implements all operations in E

• exports_only (id : ℕ) (S T : Type) : P.has id S T → E.has id S T

  The package only implements operations in E

• valid_impl (e : PackageEntry) : e ∈ P.entries → ∀ (x : e.fun_.src), ValidCode L I e.fun_.tgt (e.fun_.impl x)

  All implementations are valid code

def CatCrypt.Package.fseparate (L₁ L₂ : Locations) : Prop

Two packages have separate (disjoint) locations

Equations

• CatCrypt.Package.fseparate L₁ L₂ = L₁.Separate L₂

theorem CatCrypt.Package.ValidPackage.validCode_weaken {L₁ L₂ : Locations} {I₁ I₂ : Interface} {α : Type u_1} {c : Core.SPComp α} (hL : L₁ ⊆ L₂) (hv : ValidCode L₁ I₁ α c) : ValidCode L₂ I₂ α c

Valid code for a smaller location set is valid for a larger one. This is mathematically sound: if code only accesses L₁, and L₁ ⊆ L₂, then the code trivially satisfies validity for L₂.

theorem CatCrypt.Package.ValidPackage.empty_valid (I : Interface) : ValidPackage ∅ I ∅ ∅

Empty package is valid for empty interface

theorem CatCrypt.Package.ValidPackage.par_valid {L₁ L₂ : Locations} {I₁ I₂ E₁ E₂ : Interface} {P₁ P₂ : RawPackage} (h₁ : ValidPackage L₁ I₁ E₁ P₁) (h₂ : ValidPackage L₂ I₂ E₂ P₂) (hL : L₁.Separate L₂) (hI : I₁.Disjoint I₂) (hP : P₁.Disjoint P₂) (hE : E₁.Disjoint E₂) : ValidPackage (L₁.union L₂ hL) (I₁.union I₂ hI) (E₁.union E₂ hE) (P₁.par P₂ hP)

Parallel composition of valid packages

def CatCrypt.Package.ValidPackage.locs (L : Locations) (_I _E : Interface) (_P : RawPackage) : ValidPackage L _I _E _P → Locations

Location tracking: get the locations from a ValidPackage

Equations

• CatCrypt.Package.ValidPackage.locs L _I _E _P x✝ = L

def CatCrypt.Package.Game_import : Interface

The game import interface (empty for basic games)

Equations

• CatCrypt.Package.Game_import = CatCrypt.Package.Interface.empty

def CatCrypt.Package.A_export : Interface

The adversary export interface (empty for basic adversaries)

Equations

• CatCrypt.Package.A_export = CatCrypt.Package.Interface.empty