Contracts.lean

View source on GitHub

Contract / ContractPreserving

A contract is a predicate on outputs (b → Prop). A kernel is contract-preserving if every reachable output satisfies the contract, for every input. This quantifies over the support — all possible outputs, not just the likely ones.

def ContractPreserving [Monad M] [Support M]
    (f : Kernel M α β) (contract : Contract β) : Prop :=
  ∀ a : α, ∀ b : β, Support.support (f a) b → contract b

IterationStable

A kernel is iteration-stable if its contract survives re-application. Sort a sorted list — still sorted. Run MMR on a diverse slate — still diverse. This is the loop invariant: the postcondition holds after any number of iterations.

def IterationStable [Monad M] [Support M]
    (f : Kernel M α α) (contract : Contract α) : Prop :=
  ∀ a : α, contract a → ∀ b : α, Support.support (f a) b → contract b

FilterContract

Filter's specific contract: every output is strictly smaller than the input. This is what forces information reduction — data gets smaller as it passes through Filter.

AttendContract

Attend's contract: outputs are bounded in size and diverse. The capacity bound limits how much Attend can produce; diversity prevents degenerate selections.

ConsolidateContract

Consolidate's contract: the operation is lossy. The output policy carries no more information than the input policy. Consolidate is the only procedure that writes procedures.

RememberContract

Remember's contract: lossless relative to its input. Every output equals the input — no additional information is lost at this step.

contract_composition_base

This says: when you compose two kernels, only the second kernel's contract matters for the final guarantee. The first kernel feeds intermediates; the postcondition is checked at the end.

theorem contract_composition_base [Monad M] [LawfulMonad M] [Support M]
    {f : Kernel M α β} {g : Kernel M β γ}
    {cg : Contract γ}
    (hg : ContractPreserving g cg)
    : ContractPreserving (Kernel.comp f g) cg

The proof decomposes the composite's support via support_bind: any output c came from some intermediate b, and since g preserves its contract, c satisfies it.

# ContractPreserving: every possible output satisfies the contract
# IterationStable: the contract survives re-application

import random

def filter_stage(items):
    """Filter contract: output is strictly smaller than input"""
    return random.sample(items, k=max(1, len(items)//2))

def is_sorted(lst):
    return all(lst[i] <= lst[i+1] for i in range(len(lst)-1))

def sort_stage(items):
    return sorted(items)

# ContractPreserving: every output of sort_stage is sorted
data = [5, 2, 8, 1, 9, 3]
result = sort_stage(data)
print(f"sort({data}) = {result}")
print(f"contract 'is_sorted' holds: {is_sorted(result)}")

# IterationStable: sort a sorted list — still sorted
result2 = sort_stage(result)
print(f"sort(sort(data)) = {result2}")
print(f"contract still holds: {is_sorted(result2)}")

# Filter contract: output strictly smaller
filtered = filter_stage(data)
print(f"\nfilter({data}) = {filtered}")
print(f"len shrinks: {len(data)} -> {len(filtered)}")

Connections

• Pipeline.lean — imported; contracts apply to pipeline stages
• Handshake.lean — chains contracts between adjacent stages
• Removal.lean — shows removing each contract kills the system
• Hoare/Bridge.lean — proves ContractPreserving is a Hoare triple with trivial precondition
• Variational.lean — derives contracts from optimization problems