Operation Signatures and Interfaces

This file defines operation signatures and interfaces for the CatCrypt package system. An interface is a finite collection of operation signatures indexed by identifiers.

Main definitions

• OpSig - Operation signature: specifies input and output types
• Interface - Collection of operation signatures indexed by natural numbers
• Interface.empty - Empty interface
• Interface.has - Check if interface contains an operation

References

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

structure CatCrypt.Package.OpSig : Type 1

Operation signature: specifies the input type (src) and output type (tgt)

• src : Type
• tgt : Type

@[implicit_reducible]

noncomputable instance CatCrypt.Package.instDecidableEqOpSig : DecidableEq OpSig

Two operation signatures are equal if their types are the same. Note: This uses heterogeneous equality for Type universes.

Equations

• CatCrypt.Package.instDecidableEqOpSig = Classical.decEq CatCrypt.Package.OpSig

structure CatCrypt.Package.InterfaceEntry : Type 1

An interface entry: an operation id with its signature

• id : ℕ
• sig : OpSig

@[implicit_reducible]

noncomputable instance CatCrypt.Package.instDecidableEqInterfaceEntry : DecidableEq InterfaceEntry

DecidableEq for InterfaceEntry (needed for Finset operations)

Equations

• CatCrypt.Package.instDecidableEqInterfaceEntry = Classical.decEq CatCrypt.Package.InterfaceEntry

structure CatCrypt.Package.Interface : Type 1

Interface: a finite collection of operation signatures indexed by identifiers. We represent this as a finite set of entries with unique ids.

• entries : Finset InterfaceEntry
• unique_ids (e₁ e₂ : InterfaceEntry) : e₁ ∈ self.entries → e₂ ∈ self.entries → e₁.id = e₂.id → e₁ = e₂

def CatCrypt.Package.Interface.empty : Interface

Empty interface

Equations

• CatCrypt.Package.Interface.empty = { entries := ∅, unique_ids := CatCrypt.Package.Interface.empty._proof_1 }

@[implicit_reducible]

instance CatCrypt.Package.Interface.instEmptyCollection : EmptyCollection Interface

Equations

• CatCrypt.Package.Interface.instEmptyCollection = { emptyCollection := CatCrypt.Package.Interface.empty }

def CatCrypt.Package.Interface.has (I : Interface) (id : ℕ) (S T : Type) : Prop

Check if an interface declares an operation with given id and signature

Equations

• I.has id S T = ∃ e ∈ I.entries, e.id = id ∧ e.sig = { src := S, tgt := T }

noncomputable def CatCrypt.Package.Interface.ids (I : Interface) : Finset ℕ

The set of operation ids in the interface

Equations

• I.ids = Finset.image (fun (x : CatCrypt.Package.InterfaceEntry) => x.id) I.entries

noncomputable def CatCrypt.Package.Interface.lookup (I : Interface) (id : ℕ) : Option OpSig

Lookup a signature by id (noncomputable since types aren't decidable)

Equations

• I.lookup id = if h : ∃ e ∈ I.entries, e.id = id then some (Classical.choose h).sig else none

def CatCrypt.Package.Interface.Disjoint (I₁ I₂ : Interface) : Prop

Two interfaces are disjoint if they share no operation ids

Equations

• I₁.Disjoint I₂ = Disjoint I₁.ids I₂.ids

noncomputable def CatCrypt.Package.Interface.singleton (id : ℕ) (S T : Type) : Interface

A single operation interface

Equations

• CatCrypt.Package.Interface.singleton id S T = { entries := {{ id := id, sig := { src := S, tgt := T } }}, unique_ids := ⋯ }

theorem CatCrypt.Package.Interface.singleton_has (id : ℕ) (S T : Type) : (singleton id S T).has id S T

theorem CatCrypt.Package.Interface.empty_not_has (id : ℕ) (S T : Type) : ¬empty.has id S T

Empty interface has no operations

noncomputable def CatCrypt.Package.Interface.union (I₁ I₂ : Interface) (h : I₁.Disjoint I₂) : Interface

Union of interfaces (requires disjoint ids for uniqueness)

Equations

• I₁.union I₂ h = { entries := I₁.entries ∪ I₂.entries, unique_ids := ⋯ }

theorem CatCrypt.Package.Interface.union_has_left {I₁ I₂ : Interface} (h : I₁.Disjoint I₂) (id : ℕ) (S T : Type) (hI₁ : I₁.has id S T) : (I₁.union I₂ h).has id S T

Union contains operations from both interfaces

theorem CatCrypt.Package.Interface.union_has_right {I₁ I₂ : Interface} (h : I₁.Disjoint I₂) (id : ℕ) (S T : Type) (hI₂ : I₂.has id S T) : (I₁.union I₂ h).has id S T