# Lean Verification Code Map

<!-- GENERATED_METRICS:BEGIN -->
**Last Updated:** 2026-03-26
<!-- GENERATED_METRICS:END -->

Comprehensive map of the Telltale Lean 4 verification library — formal verification of choreographic programming with multiparty session types.

## Table of Contents

1. [Overview](#overview)
2. [SessionTypes](#sessiontypes)
3. [SessionCoTypes](#sessioncotypes)
4. [Choreography](#choreography)
5. [Semantics](#semantics)
6. [Classical](#classical)
7. [Distributed](#distributed)
8. [Protocol](#protocol)
9. [Runtime](#runtime)
10. [Entropy](#entropy)
11. [Build Configuration](#build-configuration)
12. [Axiom Inventory](#axiom-inventory)
13. [Proof Strategies](#proof-strategies)
14. [Quick Navigation Guide](#quick-navigation-guide)

---

## Overview

**Toolchain:** Lean 4 v4.26.0
**Build:** Lake with 9 library targets
**Dependencies:** mathlib, paco-lean v0.1.3, iris-lean

<!-- GENERATED_OVERVIEW_TABLE:BEGIN -->
| Library        | Files | Lines   | Focus                                                      |
|----------------|------:|--------:|------------------------------------------------------------|
| SessionTypes   |    47 |   9,967 | Global/local type definitions, de Bruijn, participation    |
| SessionCoTypes |    78 |  16,302 | Coinductive EQ2, bisimulation, duality, async subtyping    |
| Choreography   |    89 |  19,308 | Projection, harmony, blindness, embedding, erasure         |
| Semantics      |    14 |   2,359 | Operational semantics, determinism, deadlock freedom       |
| Classical      |    16 |   2,193 | Transported theorems (queueing, large deviations, mixing)  |
| ClassicalAnalysis |     3 |   1,128 | Real analysis concrete models for classical transport      |
| Distributed    |    59 |   7,266 | Distributed assumptions, validation, FLP/CAP theorem packaging |
| Protocol       |   170 |  40,077 | Async buffered MPST, coherence, preservation, monitoring   |
| Runtime        |   168 |  32,240 | Protocol machine, Iris backend via iris-lean, resource algebras, WP |
| IrisExtraction |     3 |     830 | Iris ghost state and program logic extraction              |
| **Total**      | **647** | **131,670** |                                                            |
<!-- GENERATED_OVERVIEW_TABLE:END -->

**Architectural Layers:**
```
Layer 8: Runtime          → Protocol machine, iris-lean backend, resource algebras, WP, adequacy
Layer 7: Protocol         → Async MPST, coherence, typing, preservation, monitoring, deployment
Layer 6: Distributed      → Distributed assumptions, validation, FLP/CAP theorem packaging
Layer 5: Classical        → Transported theorems from queueing/probability theory
Layer 4: Semantics        → Operational semantics, typing judgments, determinism, deadlock freedom
Layer 3: Choreography     → Projection, harmony, blindness, embedding, erasure
Layer 2: SessionCoTypes   → Coinductive EQ2, bisimulation, duality, roundtrip bridge, async subtyping
Layer 1: SessionTypes     → Global/local types, de Bruijn, participation
```

---

## SessionTypes

**Root Module:** `SessionTypes.lean`
**Description:** Inductive session type definitions with de Bruijn indices and recursive binders.

### Global Types

| File | Lines | Description |
|------|-------|-------------|
| GlobalType/Core.lean | 329 | Global type definitions and operations |
| GlobalType/Semantics.lean | 357 | Global type substitution |
| GlobalType/WellFormedLemmas.lean | 346 | Global stepping semantics |
| GlobalType/ProductivityLemmas.lean | 294 | Well-formedness and properties |
| GlobalType/Closedness.lean | 577 | Observable behavior and duality |

### Local Types (Recursive)

| File | Lines | Description |
|------|-------|-------------|
| LocalTypeR/Core.lean | 513 | Recursive local type definitions |
| LocalTypeR/Environments.lean | 354 | Well-formedness and operations |
| LocalTypeR/Unfolding.lean | 249 | Observable predicates |
| LocalTypeR/Substitution.lean | 398 | Substitution and operations |
| LocalTypeR/WellFormedness.lean | 274 | Duality and properties |

### Local Types (De Bruijn)

| File | Lines | Description |
|------|-------|-------------|
| LocalTypeDB/Core.lean | 258 | De Bruijn representation with clean substitution |
| LocalTypeDB/Preservation.lean | 556 | De Bruijn type preservation and correctness |
| LocalTypeDBExamples.lean | 157 | Examples demonstrating de Bruijn usage |

### Conversions

| File | Lines | Description |
|------|-------|-------------|
| LocalTypeConv.lean | 187 | Named ↔ de Bruijn conversions |
| LocalTypeConvDefs.lean | 210 | Conversion definition predicates |
| LocalTypeConvProofs/Helpers.lean | 433 | Soundness of named → de Bruijn |
| LocalTypeConvProofs/ClosedRoundtrip.lean | 404 | Completeness of named → de Bruijn |
| LocalTypeConvProofs/Roundtrip.lean | 575 | Substitution equivalence under conversion |
| LocalTypeRDBBridge.lean | 47 | Bridge between LocalTypeR and LocalTypeDB |

### Supporting Modules

| File | Lines | Description |
|------|-------|-------------|
| Core.lean | 72 | Core protocol types |
| Participation/Core.lean | 297 | Participant classification in global protocols |
| Participation/Extra.lean | 410 | Extended participation properties |
| TypeContext.lean | 518 | Unified parametric context infrastructure |
| ValType.lean | 39 | Shared value types for message payloads (unit, bool, nat, string, prod, chan) |
| ObservableClosed.lean | 267 | Termination for observable behavior of closed types |

---

## SessionCoTypes

**Root Module:** `SessionCoTypes.lean`
**Description:** Coinductive theory — equi-recursive equality (EQ2), bisimulation, duality, observables, and inductive/coinductive roundtrip bridge.

### Coinductive Infrastructure

| File | Lines | Description |
|------|-------|-------------|
| CoinductiveRel.lean | 50 | Monotone endofunctors on complete lattices |
| CoinductiveRelPaco.lean | 45 | Wrappers around paco coinduction principles |

### EQ2 (Equi-Recursive Equality)

| File | Lines | Description |
|------|-------|-------------|
| EQ2/Core.lean | 493 | Core EQ2 definition and basic properties |
| EQ2/TransBase.lean | 182 | Base transitivity properties |
| EQ2Paco.lean | 243 | EQ2 with paco parametrized coinduction |
| EQ2Props.lean | 24 | Properties via bisimulation |

### Bisimulation (10 parts)

| File | Lines | Description |
|------|-------|-------------|
| Bisim/Core.lean | 360 | Definition and basic properties |
| Bisim/UnfoldingLemmas.lean | 356 | Preservation and respects relations |
| Bisim/Bisimulation.lean | 337 | Transitivity and composition |
| Bisim/EQ2Equivalence.lean | 476 | Duality and observable predicates |
| Bisim/ObservableFromEQ2.lean | 220 | Symmetry and equivalence |
| Bisim/EQ2Extraction.lean | 464 | Mu-unfold preservation |
| Bisim/EQ2ToBisim.lean | 156 | Transitive closure |
| Bisim/Congruence.lean | 367 | Substitution and duality |
| Bisim/Substitution.lean | 491 | Bisimulation as equivalence for EQ2 |
| Bisim/UnfoldSubstitute.lean | 219 | Auxiliary lemmas |

### Substitution Theory

| File | Lines | Description |
|------|-------|-------------|
| Substitute.lean | 230 | Substitution preserves EQ2 |
| SubstCommBarendregt/General.lean | 235 | General substitution commutation |
| SubstCommBarendregt/Main.lean | 551 | Main proof under Barendregt convention |
| SubstCommBarendregt/Predicates.lean | 388 | Auxiliary predicates |
| SubstCommBarendregt/SubstRel.lean | 115 | Substitution relation properties |

### Coinductive Type System

| File | Lines | Description |
|------|-------|-------------|
| Coinductive/LocalTypeC.lean | 156 | Coinductive local types via polynomial functors |
| Coinductive/Observable.lean | 138 | Observable behavior predicates |
| Coinductive/ProjectC.lean | 322 | Coinductive projection as greatest fixed point |
| Coinductive/EQ2C.lean | 419 | Equi-recursive equality for coinductive types |
| Coinductive/EQ2CProps.lean | 451 | EQ2C properties |
| Coinductive/EQ2CEnv.lean | 354 | EQ2C under environments and substitution |
| Coinductive/EQ2CMu.lean | 183 | Mu-unfolding properties for EQ2C |
| Coinductive/EQ2CPaco.lean | 73 | EQ2C with paco |

### Decidable Bisimulation

| File | Lines | Description |
|------|-------|-------------|
| Coinductive/BisimDecidable/Core.lean | 392 | Decidability framework and fuel-based computation |
| Coinductive/BisimDecidable/BisimAux.lean | 382 | Decision procedure implementation |
| Coinductive/BisimDecidable/Correctness.lean | 410 | Correctness proofs |

### Roundtrip Bridge (Inductive ↔ Coinductive)

| File | Lines | Description |
|------|-------|-------------|
| Coinductive/Bridge.lean | 52 | Bridge between representations |
| Coinductive/Regularity.lean | 101 | Regularity constraints |
| Coinductive/ToInductive.lean | 172 | Coinductive → inductive conversion |
| Coinductive/WellFormed.lean | 125 | Well-formedness conditions |
| Coinductive/Roundtrip/Core.lean | 302 | Inductive → coinductive correctness |
| Coinductive/Roundtrip/PacoCollapse.lean | 321 | Coinductive → inductive conversion |
| Coinductive/Roundtrip/EnvDefs.lean | 200 | Roundtrip composition |
| Coinductive/Roundtrip/RoundtripTheorem.lean | 544 | Completeness and characterization |
| Coinductive/Roundtrip/RoundtripCorollaries.lean | 86 | Final auxiliary lemmas |
| Coinductive/RoundtripHelpers.lean | 394 | Helper lemmas |
| Coinductive/ToCoindInjectivity.lean | 145 | Injectivity of toCoind conversion |
| Coinductive/ToCoindRegular.lean | 86 | Regularity preservation for toCoind |
| Coinductive/RegularityLemmas.lean | 81 | Auxiliary regularity lemmas |
| Coinductive/Roundtrip/GpacoCollapse.lean | 111 | Paco collapse for roundtrip proofs |

### Supporting Modules

| File | Lines | Description |
|------|-------|-------------|
| Observable.lean | 394 | Membership predicates for observable behavior |
| Dual.lean | 266 | Duality lemmas |
| FullUnfold.lean | 265 | Full unfolding with termination argument |
| Quotient.lean | 111 | Quotient by EQ2 equivalence |
| DBBridge.lean | 50 | Bridge lemmas for de Bruijn |
| Coinductive/Bisim.lean | 84 | Coinductive bisimulation definition |
| Coinductive/BisimHelpers.lean | 322 | Bisimulation helpers |
| Coinductive/Congruence.lean | 36 | Congruence properties |
| Coinductive/Coalgebra.lean | 30 | Coalgebraic structure |
| Coinductive/Dual.lean | 140 | Duality for coinductive types |
| Coinductive/RegularSystemBisim.lean | 159 | Bisimulation for finite regular systems |
| Coinductive/FiniteSystem.lean | 68 | Finite regular system representation |

### Asynchronous Subtyping

| File | Lines | Description |
|------|-------|-------------|
| AsyncSubtyping.lean | 39 | Re-export wrapper for async subtyping module |
| AsyncSubtyping/Core.lean | 382 | AsyncTriple, MsgBuffer, 7 async step rules, AsyncSubtypeRel coinductive relation |
| AsyncSubtyping/Decidable.lean | 381 | checkAsync worklist algorithm, isAsyncSubtype decision function, soundness/completeness |

Plus 5 namespace re-export modules: Bisim.lean, EQ2.lean, SubstCommBarendregt.lean, Coinductive/BisimDecidable.lean, Coinductive/Roundtrip.lean.

---

## Choreography

**Root Module:** `Choreography.lean`
**Description:** Projection from global to local session types and its correctness (harmony), includes blindness predicates, erasure, and embedding.

### Trans Projection (Coq-style)

| File | Lines | Description |
|------|-------|-------------|
| Projection/Trans/Core.lean | 428 | Core projection algorithm |
| Projection/Trans/Participation.lean | 196 | Participation filtering |
| Projection/Trans/Contractive.lean | 333 | Guardedness analysis for recursive projection |

### Boolean Projection Checker

| File | Lines | Description |
|------|-------|-------------|
| Projection/Projectb/Checker.lean | 205 | Boolean projection definition |
| Projection/Projectb/Coinductive.lean | 465 | Branch handling |
| Projection/Projectb/Soundness.lean | 387 | Correctness lemmas |
| Projection/Projectb/Completeness.lean | 566 | Mu-type handling |

### Proof-Carrying Projection API

| File | Lines | Description |
|------|-------|-------------|
| Projection/Project/Core.lean | 123 | Core API definitions |
| Projection/Project/MuveImplBase.lean | 561 | Base mu-unfolding cases |
| Projection/Project/MuveImplParticipant.lean | 544 | Participant mu-unfolding elimination |
| Projection/Project/MuveImplNonPart.lean | 429 | Non-participant mu-unfolding elimination |
| Projection/Project/ImplBase.lean | 431 | Base projection implementation |
| Projection/Project/ImplConstructors/Base.lean | 427 | End, var, mu cases |
| Projection/Project/ImplConstructors/SendRecv.lean | 366 | Send/recv cases |
| Projection/Project/ImplConstructors/Mu.lean | 192 | Branching cases |
| Projection/Project/ImplCompleteness.lean | 314 | Completeness proof |
| Projection/Project/ImplObservables.lean | 362 | Observable properties preservation |
| Projection/Project/ImplHeadPreservation.lean | 463 | Head shape preservation |
| Projection/Project/ImplExtraction/ObservableExtraction.lean | 306 | Observable extraction |
| Projection/Project/ImplExtraction/RecvExtraction.lean | 330 | Payload and branch extraction |
| Projection/Project/ImplTransRelComp/Core.lean | 331 | Transition relation base cases |
| Projection/Project/ImplTransRelComp/CommCases.lean | 354 | Transition relation properties |
| Projection/Project/ImplCompPostfix/WellFormedClosure.lean | 321 | Observable postfix computation |
| Projection/Project/ImplCompPostfix/PrefixCases.lean | 219 | Observable list postfix |
| Projection/Project/ImplCompPostfix/SuffixCases.lean | 356 | Postfix properties |
| Projection/Project/ImplU/EQ2Closure.lean | 355 | Unfolding base cases |
| Projection/Project/ImplU/CommCases.lean | 363 | Unfolding lemmas and composition |

### Blindness Predicate

| File | Lines | Description |
|------|-------|-------------|
| Projection/Blind/Core.lean | 492 | Definition and basic properties |
| Projection/Blind/Preservation.lean | 187 | Preservation and composition |
| Projection/Blind.lean | 7 | Re-export wrapper for Blind/Core and Blind/Preservation |

### Harmony (Projection Correctness)

| File | Lines | Description |
|------|-------|-------------|
| Harmony.lean | 150 | Main harmony structure |
| Harmony/MuUnfoldLemmas.lean | 257 | Mu-unfolding auxiliary lemmas |
| Harmony/StepProjection.lean | 255 | Projection preserves stepping semantics |
| Harmony/SubstEndUnguarded.lean | 239 | Substitution with guardedness constraints |
| Harmony/StepHarmony.lean | 423 | Main structure |
| Harmony/Substitution.lean | 519 | Communication handling |
| Harmony/ParticipantSteps.lean | 533 | Branching |
| Harmony/NonParticipantHelpers.lean | 126 | Recursion |
| Harmony/NonParticipantSteps.lean | 147 | Final properties |

### Supporting Modules

| File | Lines | Description |
|------|-------|-------------|
| Projection/ProjSubst.lean | 410 | Projection-substitution commutation |
| Projection/ProjectProps.lean | 143 | General projection properties |
| Projection/ComposeProof.lean | 60 | Composition of projection lemmas |
| Projection/Embed.lean | 233 | Coinductive embedding relation |
| Projection/EmbedProps.lean | 510 | Embedding properties |
| Projection/Erasure/Core.lean | 80 | Erasure definition |
| Projection/Erasure/Merge.lean | 358 | Erasure lemmas |
| Projection/Erasure/MergeSoundness.lean | 425 | Erasure correctness |
| Assumptions.lean | 15 | Centralized assumptions |

### JSON and Validation Infrastructure

| File | Lines | Description |
|------|-------|-------------|
| Projection/Json.lean | 177 | JSON serialization for GlobalType, LocalTypeR matching lean-bridge schema |
| Projection/Validator.lean | 198 | CLI validator for projection results, runValidation, runExportProjection |

---

## Semantics

**Root Module:** `Semantics.lean`
**Description:** Operational semantics, typing judgments, determinism, deadlock freedom, subject reduction.

| File | Lines | Description |
|------|-------|-------------|
| Environment.lean | 299 | Environment configuration (message queues, timeouts, actions) |
| EnvStep.lean | 191 | Environment-step relation |
| Typing.lean | 23 | Typing judgment interface |
| Determinism/Core.lean | 600 | Determinism proof part 1 |
| Determinism/Diamond.lean | 516 | Determinism proof part 2 |
| DeadlockFreedom.lean | 293 | Deadlock freedom with fairness |
| SubjectReduction.lean | 201 | Subject reduction for well-typed processes |

---

## Classical

**Root Module:** `Classical.lean`
**Description:** Transported theorems from queueing theory, probability, and stochastic processes, organized into family kernels and a layered transport API.

### Families

| File | Description |
|------|-------------|
| Families/FosterLyapunovHarris.lean | Foster-Lyapunov-Harris theorem for stability/recurrence |
| Families/MaxWeightBackpressure.lean | MaxWeight scheduling optimality and backpressure |
| Families/LargeDeviationPrinciple.lean | Large deviation bounds for rare events |
| Families/HeavyTrafficDiffusion.lean | Heavy traffic diffusion limits |
| Families/MixingTimeBounds.lean | Mixing-time bounds for Markov chains |
| Families/FluidLimitStability.lean | Fluid-limit stability analysis |
| Families/ConcentrationInequalities.lean | Concentration inequalities |
| Families/LittlesLaw.lean | Little's law identities |
| Families/FunctionalCLT.lean | Functional central limit theorem |
| Families/PropagationOfChaos.lean | Mean-field limits and propagation of chaos |
| Families/SpectralGapTermination.lean | Spectral-gap / Cheeger / hitting-time interfaces |

### Transport Layers

| File | Description |
|------|-------------|
| Transport/Context.lean | Shared transport context |
| Transport/Contracts.lean | Input/Conclusion contracts per theorem family |
| Transport/Theorems.lean | Facade theorem wrappers |
| Transport/API.lean | Stable transport facade import |

---

## Distributed

**Root Module:** `Distributed.lean`
**Description:** Family-oriented distributed characterization with a transport layer for validation and family usage.

### Model

| File | Description |
|------|-------------|
| Model/Assumptions.lean | Base distributed assumptions and assumption-check functions |
| Model/Types.lean | Protocol-space model types and protocol spec |
| Model/Classifier.lean | BFT/Nakamoto/Hybrid classification predicates |

### Families

| File | Description |
|------|-------------|
| Families/FLP.lean | FLP assumptions, premises, and auto-derived lower-bound/impossibility packaging |
| Families/CAP.lean | CAP assumptions, premises, and auto-derived impossibility packaging |
| Families/QuorumGeometry.lean | Quorum-intersection safety family: no-conflict commits, fork exclusion, safe finality |
| Families/PartialSynchrony.lean | Partial-synchrony liveness family: eventual decision and bounded post-GST termination |
| Families/Responsiveness.lean | Responsiveness family: optimistic post-GST latency bound independent of timeout |
| Families/Nakamoto.lean | Nakamoto security family: probabilistic safety, settlement-depth finality, churn-liveness |
| Families/Reconfiguration.lean | Reconfiguration safety family: no split-brain, safe handoff, liveness preservation |
| Families/AtomicBroadcast.lean | Atomic-broadcast family: total-order consistency, log-prefix compatibility, consensus bridge |
| Families/AccountableSafety.lean | Accountable-safety family: safety-or-evidence theorem with slashable fault evidence |
| Families/FailureDetectors.lean | Failure-detector family: detector-class solvability/impossibility boundary forms |
| Families/DataAvailability.lean | Data-availability family: k-of-n availability/retrievability under sampling and withholding bounds |
| Families/Coordination.lean | Coordination family: CALM-style monotonicity characterization of coordination necessity |

### Transport

| File | Description |
|------|-------------|
| Transport/Context.lean | Transported-family eligibility context and assumption atoms |
| Transport/Contracts.lean | Validation summary contracts |
| Transport/Theorems.lean | High-level validation/combination APIs |
| Transport/API.lean | Transport facade import |

### Facade

| File | Description |
|------|-------------|
| Distributed.lean | Distributed root facade import |

---

## Protocol

**Root Module:** `Protocol.lean`
**Description:** Async buffered multiparty session types with coherence invariant, preservation, deadlock freedom, monitoring, and deployment composition.

### Foundational Types

| File | Lines | Description |
|------|-------|-------------|
| Basic.lean | 185 | SessionId, Role, Endpoint, Label, Edge, RoleSet |
| LocalType.lean | 254 | Local session types with send/recv/select/branch/mu, depth functions |
| Values.lean | 191 | Runtime values, linear capability tokens, session ID bounds |
| Process.lean | 149 | Process language (skip, seq, par, send, recv, select, branch, newSession) |

### Environments

| File | Lines | Description |
|------|------:|-------------|
| Environments/Core.lean | 1,338 | Store, SEnv, GEnv, DEnv, Buffers — lookup/update/init, DEnvUnion |
| Environments/Renaming.lean | 493 | Session renaming with injectivity/commutativity |
| Environments/RoleRenaming.lean | 83 | Role-based session renaming with correctness properties |

### Coherence (21 parts)

Central invariant replacing traditional duality for multiparty async settings.

| File | Lines | Description |
|------|------:|-------------|
| Coherence/Consume.lean | 253 | `Consume`, `EdgeCoherent`, `Coherent`, `HasTypeVal` |
| Coherence/EdgeCoherence.lean | 525 | `BufferTyped`, `StoreTyped`, `ActiveEdge` |
| Coherence/StoreTyping.lean | 136 | `StoreTypedStrong`, irrelevance lemmas |
| Coherence/Preservation.lean | 545 | `Coherent_send_preserved`, `Coherent_recv_preserved` |
| Coherence/SelectPreservation.lean | 356 | `Coherent_select_preserved`, `Coherent_branch_preserved` |
| Coherence/HeadPreservationSend.lean | 507 | Helper lemmas |
| Coherence/HeadPreservationSelect.lean | 376 | `HeadCoherent_select/branch_preserved` |
| Coherence/ValidLabels.lean | 660 | `Coherent_empty`, `initSession_coherent`, ValidLabels |
| Coherence/Renaming.lean | 305 | `CoherentRenaming`, `Dual_implies_Coherent_empty` |
| Coherence/ConfigEquiv.lean | 737 | `CoherenceConfig`, `ConfigEquiv`, quotient structure for session isomorphisms |
| Coherence/Unified.lean | 31 | `edge_case_split` — 3-way edge case analysis for preservation proofs |
| Coherence/EdgeCoherenceM.lean | 115 | Model-parametric `EdgeCoherent` variants |
| Coherence/HeadCoherenceM.lean | 28 | Model-parametric `HeadCoherent` |
| Coherence/PreservationDeliveryModels.lean | 157 | Parametrized preservation lemmas for different delivery models |
| Coherence/SubtypeReplacement.lean | 517 | `RecvCompatible`, `Consume_mono`, `Coherent_type_replacement`, liveness preservation |
| Coherence/GraphDelta.lean | 547 | Higher-order `Consume` with graph deltas for channel delegation |
| Coherence/Delegation.lean | 878 | `DelegationStep`, `DelegationWF`, `delegation_preserves_coherent` |
| Coherence/RoleSwap.lean | 895 | Bijective role renaming within session, coherence preservation under role swap |
| Coherence/ErasureCharacterization.lean | 165 | Erasure characterization and configuration equivalence |
| Coherence/Conserved.lean | 203 | Conserved quantities and Noether-style correspondence |
| Coherence/Minimality.lean | 207 | Weak coherence, strictness witness, minimality theorem |

### Typing (8 parts)

| File | Lines | Description |
|------|-------|-------------|
| Typing/Core.lean | 651 | Disjointness, splitting (`ParSplit`), `DConsistent` |
| Typing/Judgments.lean | 567 | `HasTypeProcN` / `HasTypeProcPreOut` / `TypedStep`, plus `ParWitness` inversion and par-index irrelevance |
| Typing/Compatibility.lean | 992 | SEnv append/lookup lemmas |
| Typing/MergeLemmas.lean | 327 | Additional environment lemmas |
| Typing/StepLemmas.lean | 478 | `WTConfigN` well-typed configuration |
| Typing/Framing.lean | 13 | Framing entry point (re-exports) |
| Typing/Framing/Lemmas.lean | 1,331 | Constructive frame lemmas (including middle-frame preservation; no framing axioms) |
| Typing/Framing/FramedPreUpdate.lean | 308 | Pre-out preservation under G frames |
| Typing/Framing/PreUpdateHelpers.lean | 293 | Alignment helpers for framed pre-update proofs |
| Typing/Framing/LeftCases.lean | 266 | Left-frame step cases for pre-update |
| Typing/Framing/RightCases.lean | 280 | Right-frame step cases for pre-update |
| Typing/Framing/PreUpdatePreservation.lean | 409 | Lifting pre-update preservation to main theorems |
| Typing/Framing/GEnvFrame.lean | 11 | GEnv framing re-exports |
| Typing/Framing/GEnvFramePre.lean | 81 | Pre-typing right-frame lemma |
| Typing/Framing/GEnvFrameHelpers.lean | 50 | Shared disjointness helpers |
| Typing/Framing/GEnvFrameRight.lean | 202 | Pre-out right-frame lemma + framed par `nG` irrelevance regression lemma |
| Typing/Framing/GEnvFrameLeft.lean | 280 | Pre-out left-frame lemma + framed par `nG` irrelevance regression lemma |
| Typing/Preservation.lean | 2,137 | Constructive preservation sub-lemmas (`Compatible`) |
| Typing/Progress.lean | 472 | DEnv union and environment append properties |

### Par Witness / Quotient View (Typing Layer)

- `Typing/Judgments.lean` now encodes par split identity via `ParWitness` (split + left-length witness).
- Inversion APIs are witness-oriented: `HasTypeProcPreOut_par_inv_witness`, `TypedStep_par_inv`.
- Ambient par index on the right (`nG`) is quotient-style/irrelevant at typing level:
  - `HasTypeProcPre_par_nG_irrel`
  - `HasTypeProcPreOut_par_nG_irrel`
- Framed regression lemmas make this explicit at transport boundaries:
  - `HasTypeProcPreOut_frame_G_right_par_nG_irrel` (`Typing/Framing/GEnvFrameRight.lean`)
  - `HasTypeProcPreOut_frame_G_left_par_nG_irrel` (`Typing/Framing/GEnvFrameLeft.lean`)

### Operational Semantics

| File | Lines | Description |
|------|-------|-------------|
| Semantics.lean | 358 | `StepBase` (send/recv/select/branch/newSession/assign), `Step` (contextual closure) |

### Main Theorems

| File | Lines | Description |
|------|-------|-------------|
| Preservation.lean | 1,933 | `preservation_typed`, `progress_*`, `subject_reduction` |
| Determinism.lean | 359 | `stepBase_det`, `diamond_independent`, `session_isolation` |
| DeadlockFreedom.lean | 7 | Re-export wrapper for DeadlockFreedomCore and DeadlockFreedomReachability |
| DeadlockFreedomCore.lean | 291 | `Guarded`, `ReachesComm`, core deadlock freedom definitions |
| DeadlockFreedomReachability.lean | 380 | `deadlock_free`, `not_stuck`, reachability-based proofs |

### Runtime Monitoring

| File | Lines | Description |
|------|-------|-------------|
| Monitor/Core.lean | 477 | `ProtoAction`, `MonitorState`, `MonStep`, `WTMon` |
| Monitor/Preservation.lean | 187 | `MonStep_preserves_WTMon`, `newSession_preserves_WTMon` — 2 axioms |

### Deployment Composition

| File | Lines | Description |
|------|-------|-------------|
| Deployment/Interface.lean | 438 | `InterfaceType`, `DeployedProtocol`, `ProtocolBundle` |
| Deployment/Merge.lean | 296 | `MergeDEnv`, disjoint sessions |
| Deployment/Linking.lean | 87 | Composition metatheory — 8 axioms |

### Supporting Modules

| File | Lines | Description |
|------|------:|-------------|
| Spatial.lean | 7 | Re-export wrapper for SpatialCore and SpatialBranching |
| SpatialCore.lean | 351 | `SpatialReq`, `Topology`, `Satisfies`, `spatial_le_sound` |
| SpatialBranching.lean | 306 | `ConfusabilityGraph`, branching feasibility |
| Symmetry.lean | 8 | Re-export wrapper for Symmetry* modules |
| SymmetryCore.lean | 216 | Core symmetry properties and role-symmetric protocols |
| SymmetryConsumeRenaming.lean | 451 | Consume renaming under role bijections |
| SymmetryInverseStep.lean | 265 | Symmetry-preserving step operations |
| BufferBoundedness.lean | 1,217 | Buffer boundedness analysis, depth bounds, capacity constraints |
| Simulation.lean | 540 | `stepDecide`, `runSteps`, `traceSteps`, soundness/completeness |
| Decidability.lean | 108 | DecidableEq instances |
| Examples.lean | 19 | Protocol examples (stubbed) |
| CrashTolerance.lean | 225 | `CommGraph`, `CrashTolerant`, `Critical`, crash tolerance predicates |
| Noninterference.lean | 8 | Re-export wrapper for Noninterference* modules |
| NoninterferenceCore.lean | 471 | `CEquiv`, `BlindTo`, core noninterference definitions |
| NoninterferenceExtensions.lean | 178 | `blind_step_preserves_CEquiv` and extended noninterference proofs |
| DeliveryModel.lean | 214 | `DeliveryModel` typeclass, FIFO/causal/lossy instances |
| CoherenceM.lean | 15 | Model-parametric coherence re-export wrapper |
| InformationCost.lean | 1050 | `ProjectionMap`, entropy, mutual information, blind projection |

### Classical Regime (5 parts)

Protocol-specific instantiation of the classical transport framework.

| File | Lines | Description |
|------|-------|-------------|
| Classical/Regime.lean | 74 | Classical regime definition, totality, determinism, exchangeability |
| Classical/Framework.lean | 126 | TransportFramework, step induction, classical regime instantiation |
| Classical/TransportLedger.lean | 88 | Ledger bookkeeping for transported theorem discharge planning |
| Classical/SpectralGap.lean | 97 | Spectral gap bounds, mixing time analysis, Cheeger inequality interface |
| Classical/Instantiation.lean | 474 | Protocol-facing instantiation (Foster-Lyapunov, MaxWeight, Mean-field) |

---

## Runtime

**Root Module:** `Runtime.lean`
**Description:** Protocol machine definition, Iris separation logic backend via iris-lean, resource algebras, session invariants, WP rules, and adequacy.

### Iris Bridge (iris-lean integration)

Consolidated interface to iris-lean separation logic via the Entropy trust boundary layer. Ghost maps use `Positive` keys with encoding.

| File | Lines | Description |
|------|------:|-------------|
| IrisExtractionAPI.lean | 173 | Pure API: `TelltaleIris` parameter bundle, iProp, GhostName, Mask, Namespace typeclasses |
| IrisExtractionInstance/Core.lean | 427 | Core iris-lean integration with WP rules |
| IrisExtractionInstance/GhostAndProgramLogic.lean | 230 | Ghost state and program logic wiring |

See [Entropy](#entropy) section for full trust boundary documentation.

### Protocol Machine Model (ProtocolMachine/Model/)

| File | Lines | Description |
|------|------:|-------------|
| Core.lean | 67 | Register file, instruction set, coroutine |
| Config.lean | 85 | VMConfig, VMState, ResourcePool |
| State.lean | 304 | Full machine state, session table, buffer management |
| Program.lean | 137 | Program representation and code segments |
| Effects.lean | 167 | Effect-interface metadata, request/outcome exchange objects, and reentrancy primitives |
| EffectAlgebra.lean | 111 | Effect classification, immediate-effect discipline, and multi-effect composition semantics |
| SemanticObjects/Core.lean | 241 | Canonical protocol-machine semantic object implementation layer |
| SemanticObjects/Discipline.lean | 96 | Semantic-object predicate surface for identity, ownership, and observed-read discipline |
| SemanticObjects/OutstandingEffects.lean | 132 | Deferred-effect lifecycle model: issuance, blocking, completion, timeout, cancellation, invalidation, retry |
| SemanticObjects/SemanticHandoffTransition.lean | 134 | Semantic handoff realization for owner transfer, dependent work, effect transport, and publication authority |
| SemanticObjects.lean | 9 | Re-export facade for semantic object implementation + invariants |
| TypeClasses.lean | 251 | Identity, guard, persistence, effect, verification model typeclasses |
| CompileLocalTypeR.lean | 190 | Compiler from LocalTypeR to protocol machine bytecode instructions |
| Knowledge.lean | 30 | Knowledge base and fact management |
| Violation.lean | 29 | Violation policy and fault types |
| SchedulerTypes.lean | 26 | Scheduler type definitions |
| UnitModel.lean | 184 | Minimal computable instances for all protocol machine domain typeclasses |
| OutputCondition.lean | 54 | Output-condition model for commit gating |

### Protocol Machine Semantics (ProtocolMachine/Semantics/)

| File | Lines | Description |
|------|------:|-------------|
| Exec.lean | 127 | Top-level step function dispatch |
| ExecHelpers.lean | 422 | Register operations, buffer lookup, shared helpers |
| ExecComm.lean | 449 | Send/recv/select/branch execution |
| ExecSession.lean | 304 | Session open/close/fork/join |
| ExecOwnership.lean | 162 | Ownership transfer and capability operations |
| ExecControl.lean | 103 | Control flow (jump, call, return, halt) |
| ExecGuardEffect.lean | 111 | Guard chain evaluation and effect dispatch |
| ExecSpeculation.lean | 197 | V2: Speculative execution semantics (fork/join/abort with checkpoint store) |
| ExecSteps.lean | 54 | Multi-step execution wrapper |
| InstrSpec.lean | 324 | Denotational specs for 8 instruction types |

### Protocol Machine Runtime (ProtocolMachine/Runtime/)

Executable runtime surface used for Lean↔Rust parity. Proof theorems and
proof-only contract vocabularies live under `Runtime/Proofs/ProtocolMachine/`.

| File | Lines | Description |
|------|------:|-------------|
| Loader.lean | 234 | Dynamic choreography loading into running protocol machine state (result-typed admission + compatibility API) |
| Runner.lean | 104 | N-concurrent scheduler-driven execution loop |
| ThreadedRunner.lean | 445 | V2: Deterministic threaded execution with wave planning |
| Scheduler.lean | 294 | Barrel import for executable scheduler helpers and stepping |
| SchedulerHelpers.lean | 386 | Shared scheduler utility functions |
| SchedulerStep.lean | 78 | Executable scheduler step orchestration only; proof contracts moved out |
| Monitor.lean | 163 | SessionKind, WellTypedInstr judgment, unified session monitor (executable monitor only) |
| Failure.lean | 40 | Failure runtime facade (executable symbols only) |
| Failure/Core.lean | 418 | Failure modes (crash/partition/heal/corrupt/timeout), ingress updates, deterministic recovery actions |
| Failure/Transitions.lean | 201 | Deterministic recovery transition helpers and mode classifiers |
| Json.lean | 145 | JSON serialization for runtime values and trace events |

### Protocol Machine Composition (ProtocolMachine/Composition/)

| File | Lines | Description |
|------|------:|-------------|
| DomainComposition.lean | 326 | Domain-specific composition and guard chain |

### Resources

| File | Lines | Description |
|------|-------|-------------|
| Resources/ResourceModel.lean | 179 | Resource model interface and profiles |
| Resources/SessionRA.lean | 88 | Session resource algebra with auth/frag |
| Resources/BufferRA.lean | 317 | Message buffer resource algebra with auth/frag |
| Resources/Arena.lean | 1,379 | Memory arena with pointsto, allocation, and ownership tracking |
| Resources/ProfilesV1.lean | 42 | V1 resource profile definitions |

### Program Logic

| File | Lines | Description |
|------|-------|-------------|
| ProgramLogic/LanguageInstance.lean | 93 | Iris `Language`/`EctxLanguage` instances |
| ProgramLogic/SessionWP.lean | 122 | Session-level WP rules |
| ProgramLogic/GhostState.lean | 281 | Ghost state management (session maps, buffer maps) |
| ProgramLogic/CodeLoading.lean | 99 | Code loading and program verification |
| ProgramLogic/ProofInterfaces.lean | 91 | Proof interface typeclasses |
| ProgramLogic/WPPair.lean | 131 | WP pairing for send/recv duality |
| ProgramLogic/WPPipeline.lean | 25 | WP pipeline composition |
| ProgramLogic/FinalizationWP.lean | 39 | Finalization and cleanup WP rules |

### Invariants and Transport

| File | Lines | Description |
|------|------:|-------------|
| Invariants/SessionInv.lean | 256 | Session invariant: coherence, buffers, endpoint state |
| Transport/Transport.lean | 232 | Abstract transport layer with handler specs |
| Cost/Credits.lean | 56 | Cost credit resource algebra |

### Proofs/ProtocolMachine (Instruction Proofs)

| File | Lines | Description |
|------|------:|-------------|
| Proofs/ProtocolMachine/InstrSpec.lean | 1,415 | Preservation theorems for all 8 instruction types, quotient-respecting variants |
| Proofs/ProtocolMachine/Effects.lean | 247 | Effect admissibility, classification, immediate-effect, and multi-effect composition theorem layer |
| Proofs/BridgeStrengthening.lean | 143 | Protocol-machine bridge premise bundle (`ProtocolMachineBridgePremises`), handler local/trace/step typing bridge, composed `ConfigEquiv`→`EffectBisim`→observational transport |
| Proofs/ProtocolMachine/MonitorContracts.lean | 23 | Proof-only monitor contract predicates moved out of `Runtime/ProtocolMachine/Runtime/Monitor.lean` |
| Proofs/ProtocolMachine/Monitor.lean | 24 | Monitor soundness/identity preservation lemmas moved from `Runtime/ProtocolMachine/Runtime/Monitor` |
| Proofs/ProtocolMachine/SchedulerContracts.lean | 91 | Proof-only scheduler contract predicates moved out of `Runtime/ProtocolMachine/Runtime/SchedulerStep.lean` |
| Proofs/ProtocolMachine/Scheduler.lean | 265 | Scheduler proof infrastructure, including single-lane/policy determinism compatibility lemmas |
| Proofs/ProtocolMachine/SemanticObjects/OutstandingEffects.lean | 116 | Outstanding-effect admissibility, late-result rejection, and observer / `EffectBisim` lemmas |
| Proofs/ProtocolMachine/SemanticObjects/SemanticHandoff.lean | 171 | Semantic-handoff theorems and delegation / envelope bridge lemmas |
| Proofs/ProtocolMachine/SemanticObjects/AuthoritativeReadsPublication.lean | 185 | Authoritative-read/publication theorems and observer-projection consequences |
| Proofs/ProtocolMachine/SemanticObjects/MaterializationSuccess.lean | 156 | Success/materialization theorem layer |
| Proofs/ProtocolMachine/SemanticObjects/ProgressContracts.lean | 189 | Progress-contract theorem layer, parity-critical contract discipline, and failure-evidence consequences |
| Proofs/ProtocolMachine/SemanticObjects/ReplayFailureExactness.lean | 131 | Replay/failure exactness theorem layer |
| Proofs/ProtocolMachine/SemanticObjects/CrossTargetProgressDependentWork.lean | 107 | Cross-target progress and dependent-work theorem layer |
| Proofs/ProtocolMachine/SemanticObjects/TransformationLocalObligations.lean | 176 | Transformation-local obligation theorems and deployment/reconfiguration bridges |
| Proofs/ProtocolMachine/DomainComposition.lean | 49 | Domain composition and guard chain proofs |
| Proofs/ProtocolMachine/ExecOwnership.lean | 22 | Ownership transfer proof bridge |
| Proofs/ProtocolMachine/LoadChoreography.lean | 83 | Loader monotonicity and choreography-load disjointness proofs |
| Proofs/ProtocolMachine/Knowledge.lean | 20 | Flow-policy serialization roundtrip theorems moved from `Runtime.protocol machine.Model.Knowledge` |
| Proofs/ProtocolMachine/Failure.lean | 53 | Retry/deterministic recovery lemmas moved from failure runtime modules |
| Proofs/ProtocolMachine/FailurePredicates.lean | 135 | Recovery predicate vocabulary (proof-only) moved from protocol machine failure runtime |
| Proofs/ProtocolMachine/ProgramWitnesses.lean | 31 | Proof-only verified image witnesses now tied to the theoremized lowering/artifact chain |
| Proofs/ProtocolMachine/Speculation.lean | 84 | V2: Speculation correctness (depth monotonicity, abort restore, join cleanup) |
| Proofs/ProtocolMachine/InstrSpec/ConfigEquivSendRecv.lean | 338 | V2: Send/recv configuration equivalence |
| Proofs/ProtocolMachine/InstrSpec/ConfigEquivSelectBranch.lean | 341 | V2: Select/branch configuration equivalence |
| Proofs/ProtocolMachine/InstrSpec/ConfigEquivAcquire.lean | 240 | V2: Acquire configuration equivalence |
| Proofs/ProtocolMachine/InstrSpec/ConfigEquivOpenCloseTransfer.lean | 493 | V2: Open/close/transfer configuration equivalence |
| Proofs/ProtocolMachine/InstrSpec/ErasureExactness.lean | 357 | V2: Erasure exactness proofs |
| Proofs/ProtocolMachine/InstrSpec/Preservation.lean | 290 | V2: Instruction preservation proofs |

### Proofs/Conservation

| File | Lines | Description |
|------|------:|-------------|
| Proofs/Conservation/API.lean | 17 | Public facade for the six conservation-law theorem families |
| Proofs/Conservation/Evidence.lean | 76 | Evidence conservation theorems over authoritative reads, canonical publication, and materialization |
| Proofs/Conservation/Authority.lean | 93 | Authority conservation theorems over effect authority classes, handoff, and single-owner discipline |
| Proofs/Conservation/Identity.lean | 62 | Identity conservation theorems over replay stability, terminal truth, and monitor-preserved session ids |
| Proofs/Conservation/Commitment.lean | 73 | Commitment conservation theorems over outstanding effects, progress measures, and dependent work |
| Proofs/Conservation/Structure.lean | 60 | Structure conservation theorems over delegation-preserved coherence and scheduler-normalized traces |
| Proofs/Conservation/Premise.lean | 68 | Premise conservation theorems over timeout discipline, progress contracts, scheduler fairness, and liveness bundles |

### Proofs/Lowering

| File | Lines | Description |
|------|------:|-------------|
| Proofs/Lowering/API.lean | 10 | Public facade for the theoremized surface→AST→semantic→protocol-machine→artifact lowering chain |
| Proofs/Lowering/Core.lean | 155 | Core lowering structures, subset predicates, rejection reasons, and artifact-generation surface |
| Proofs/Lowering/Correctness.lean | 184 | Stage-by-stage refinement theorems and theorem-backed rejection conditions for non-projectable/non-executable forms |

### Adequacy (V2 Envelope-Based)

| File | Lines | Description |
|------|------:|-------------|
| Adequacy/Adequacy.lean | 297 | Adequacy theorem connecting WP to execution |
| Adequacy/CompileRefinesEffectBisim.lean | 39 | Compilation refinement via effect bisimulation |
| Adequacy/EnvelopeCore.lean | 54 | V2: Envelope core re-exports |
| Adequacy/EnvelopeCore/CoreFoundations.lean | 267 | V2: Core envelope definitions and axioms |
| Adequacy/EnvelopeCore/AdmissionLogic.lean | 379 | V2: Runtime admission checks and capability gates |
| Adequacy/EnvelopeCore/ProtocolMachineAdherence.lean | 314 | V2: protocol-machine adherence proofs for determinism envelope |
| Adequacy/EnvelopeCore/ReconfigurationBridge.lean | 499 | V2: Reconfiguration integration with coherence |
| Adequacy/EnvelopeCore/FailureTaxonomy.lean | 7 | V2: Failure taxonomy re-exports |
| Adequacy/EnvelopeCore/FailureTaxonomy/Core.lean | 451 | V2: Core failure classification plus explicit progress-failure taxonomy mapping |
| Adequacy/EnvelopeCore/FailureTaxonomy/ProtocolPack.lean | 112 | V2: Protocol-specific failure handling |

### Proofs
| Proofs/Contracts/RuntimeTheorems.lean | 493 | Runtime theorem facade unifying proof exports |
| Proofs/Contracts/DeterminismApi.lean | 105 | Determinism profile artifacts and hypothesis bundles for runtime gating |
| Proofs/Contracts/RuntimeContracts.lean | 274 | Runtime admission/capability contract surfaces for theorem-guided protocol machine policy |
| Proofs/Concurrency.lean | 109 | Iris-backed N-invariance and policy-invariance proofs |
| Proofs/ConcurrencyThreaded.lean | 102 | V2: Threaded concurrency proofs with wave certification |
| Proofs/SchedulerTheoremPack.lean | 200 | V2: Scheduler theorem bundle for runtime admission and proof-space packaging |
| Proofs/SchedulerApi.lean | 257 | Scheduler API surface for runtime admission |
| Proofs/CompileLocalTypeRCorrectness.lean | 53 | Compiler correctness properties (nonempty, ends with halt/jmp) |
| Proofs/SessionLocal.lean | 337 | `SessionSlice`, `SessionCoherent`, session-local frame infrastructure |
| Proofs/Frame.lean | 128 | `session_local_op_preserves_other`, `disjoint_ops_preserve_unrelated` |
| Proofs/Delegation.lean | 6 | Re-export wrapper importing `Protocol.Coherence.Delegation` |
| Proofs/Progress.lean | 7 | Re-export wrapper for Progress* modules |
| Proofs/ProgressCore.lean | 395 | `CoherentVMState`, `ProgressVMState`, core progress definitions |
| Proofs/ProgressTheorems.lean | 233 | `protocol_machine_progress`, instruction enablement theorems |
| Proofs/ProgressApi.lean | 185 | Bundle-oriented liveness API with required progress hypothesis and explicit scheduler/fairness linkage |
| Proofs/ObserverProjection.lean | 206 | Observer projection for trace equivalence |
| Proofs/ReconfigurationObserver.lean | 253 | Canonical proof-facing surface for region layering, linking/delegation harmony, observer equivalence, and replay/cross-target observer alignment |
| Proofs/HandlerEquivalence.lean | 145 | Handler equivalence proofs |
| Proofs/InvariantSpace.lean | 231 | Proof-carrying invariant-space bundle with tightened progress-contract witnesses and integrated semantic-object families |
| Proofs/Adapters/Progress.lean | 50 | Invariant-space adapters for liveness/progress theorems |
| Proofs/Adapters/Classical.lean | 416 | Invariant-space adapters for classical transport profiles and artifacts |
| Proofs/Adapters/Distributed.lean | 87 | V2: Distributed adapter re-exports |
| Proofs/Adapters/Distributed/CoreProfiles.lean | 10 | V2: Distributed profile definitions |
| Proofs/Adapters/Distributed/ProfileSetters.lean | 223 | V2: Profile configuration utilities |
| Proofs/Adapters/Distributed/ProfileWrappers.lean | 146 | V2: Canonical distributed profile wrapper types, including protocol-machine envelope profiles |
| Proofs/Adapters/Distributed/ProfileExtractionTheorems.lean | 217 | V2: Profile extraction theorems |
| Proofs/Adapters/Distributed/EnvelopeTheorems.lean | 488 | V2: Envelope theorem facade |
| Proofs/Adapters/Distributed/EnvelopeTheoremsAdmissionBridge.lean | 133 | V2: Admission and bridge theorems |

### Proofs/TheoremPack (V2 Theorem Bundle Infrastructure)

| File | Lines | Description |
|------|------:|-------------|
| Proofs/TheoremPack/API.lean | 334 | V2: Public theorem-pack interface including proof-carrying metadata, semantic-object composition, inventory, and runtime gate APIs |
| Proofs/TheoremPack/Build.lean | 418 | V2: Theorem-pack construction plus execution-profile/adherence correspondence theorems |
| Proofs/TheoremPack/Artifacts.lean | 555 | V2: Artifact generation plus semantic-object packaging and proof-carrying metadata surfaces |
| Proofs/TheoremPack/Profiles.lean | 407 | V2: Proof-carrying execution-profile definitions, theorem-pack eligibility, and minimality hooks |
| Proofs/TheoremPack/Inventory.lean | 111 | V2: Capability inventory management including semantic-object and proof-carrying metadata inventories |
| Proofs/TheoremPack/ReleaseConformance.lean | 299 | V2: Release gate conformance checking |

### Proofs/EffectBisim (V2 Handler Equivalence)

| File | Lines | Description |
|------|------:|-------------|
| Proofs/EffectBisim/Core.lean | 231 | V2: Effect bisimulation definition |
| Proofs/EffectBisim/Bridge.lean | 41 | V2: Bridge to protocol coherence |
| Proofs/EffectBisim/ConfigEquivBridge.lean | 78 | V2: Configuration equivalence integration |
| Proofs/EffectBisim/Congruence.lean | 127 | V2: Congruence properties |
| Proofs/EffectBisim/RationalFragment.lean | 138 | V2: Rational fragment handling |
| Proofs/EffectBisim/Examples.lean | 87 | V2: Usage examples |

### Proofs (Additional V2 Files)
| Proofs/Lyapunov.lean | 381 | `progressMeasure`, weighted measure W = 2·depth + buffer |
| Proofs/ProtocolMachinePotential.lean | 266 | Protocol-machine potential integration and transported Foster bridge |
| Proofs/WeightedMeasure.lean | 1,198 | Lyapunov measure infrastructure, step decrease theorems |
| Proofs/SchedulingBound.lean | 7 | Re-export wrapper for SchedulingBound* modules |
| Proofs/SchedulingBoundCore.lean | 424 | Core k-fair scheduler termination bounds |
| Proofs/SchedulingBoundTightness.lean | 328 | Tightness proofs and round-robin corollary |
| Proofs/Diamond.lean | 468 | Cross-session diamond lemmas and main confluence theorem |
| Proofs/Examples/DistributedProfiles.lean | 115 | End-to-end protocol machine examples: profile attachment auto-materializes distributed theorem artifacts |
| Proofs/Examples/ComposedProofPack.lean | 347 | End-to-end theorem-pack example showing semantic-object witness bundles flowing through the canonical composition and inventory path |
| Proofs/Examples/InvariantBundle.lean | 74 | One-shot invariant-bundle examples for liveness/progress, FLP/CAP, and classical artifact derivation |

### Examples and Tests

| File | Lines | Description |
|------|-------|-------------|
| Examples/SimpleProtocol.lean | 127 | Simple two-party protocol example |
| Tests/Main.lean | 98 | Runtime test harness |
| Tests/SimulatorParity.lean | 54 | Lean/Rust simulator parity tests |
| Tests/ProtocolMachineRunner.lean | 116 | JSON-driven protocol machine runner (stdin choreographies, stdout traces) |

---

## Entropy

**Root Modules:** `ClassicalAnalysisAPI.lean`, `IrisExtractionAPI.lean`
**Description:** Trust boundary layer providing pure API definitions with separate concrete implementations. This pattern isolates interface contracts from implementation details.

### Classical Analysis (Trust Boundary)

| File | Lines | Description |
|------|------:|-------------|
| ClassicalAnalysisAPI.lean | 437 | Pure API: `EntropyAPI.Model`, `EntropyAPI.Laws` typeclasses for Shannon entropy, KL divergence, mutual information; `AnalysisModel`/`AnalysisLaws` for real/complex analysis |
| ClassicalAnalysisInstance.lean | 3 | Re-export wrapper |
| ClassicalAnalysisInstance/Models.lean | 200 | Concrete model instances |
| ClassicalAnalysisInstance/RealConcrete.lean | 491 | Concrete real analysis models via Mathlib |

### Iris Extraction (Trust Boundary)

| File | Lines | Description |
|------|------:|-------------|
| IrisExtractionAPI.lean | 173 | Pure API: `TelltaleIris` parameter bundle, iProp, GhostName, Mask, Namespace; `GhostVarSlot`, `SavedPropSlot`, `GhostMapSlot` typeclasses |
| IrisExtractionInstance.lean | 3 | Re-export wrapper |
| IrisExtractionInstance/Core.lean | 427 | Core iris-lean integration |
| IrisExtractionInstance/GhostAndProgramLogic.lean | 230 | Ghost state and program logic wiring |

---

## Build Configuration

### lakefile.lean

Nine library targets with glob-based module discovery:

```
telltale (package)
├── SessionTypes     ← Global/local types, de Bruijn, participation
├── SessionCoTypes   ← Coinductive EQ2, bisimulation, roundtrip
├── Choreography     ← Projection, harmony, blindness, erasure
├── Semantics        ← Operational semantics, typing, determinism
├── ClassicalLayer   ← Transported queueing/probability theorem families + transport API
├── Distributed      ← Distributed theorem families (FLP/CAP, quorum safety, liveness, ordering, DA, coordination)
├── Protocol         ← Async MPST, coherence, preservation, monitoring
├── Runtime          ← Protocol machine, Iris backend, WP, adequacy (default target)
└── Entropy          ← Trust boundary: ClassicalAnalysis + IrisExtraction APIs and instances
```

**Dependencies:** mathlib, paco-lean v0.1.3, iris-lean

### Executables

Four executables defined in lakefile.lean:

| Executable | Root Module | Purpose |
|------------|-------------|---------|
| `runtime_tests` | `Runtime.Tests.Main` | protocol machine example tests |
| `simulator_parity_tests` | `Runtime.Tests.SimulatorParity` | Lean/Rust simulator parity tests |
| `protocol_machine_runner` | `Runtime.Tests.ProtocolMachineRunner` | Execute choreographies, emit observable traces |
| `telltale_validator` | `Choreography.Projection.Validator` | Projection validator (default target) |

---

## Axiom Inventory

### Global Status

`rg -n "^axiom " -g'*.lean'` returns no results. The repository is currently axiom-free.

### Sorry Concentration

**Status:** All sorries eliminated. The codebase is fully proved.

| Library | Sorry Count | Status |
|---------|------------:|--------|
| SessionCoTypes | 0 | AsyncSubtyping/Core.lean, Decidable.lean — complete |
| Protocol | 0 | Coherence, CrashTolerance, Noninterference — complete |
| Runtime | 0 | Progress, SchedulingBound, WeightedMeasure, Diamond — complete |
| **Total** | **0** | **Fully proved** |

---

## Proof Strategies

### 1. Coherence as Central Invariant
Replaces traditional binary duality with coherence: for each directed edge, consuming the in-flight message trace from the receiver's perspective succeeds. Generalizes to multiparty async settings.

### 2. Consumption Function
`Consume` models how a receiver's local type evolves as buffered messages arrive. Key composition: `Consume L (ts1 ++ ts2) = (Consume L ts1).bind (fun L' => Consume L' ts2)`.

### 3. Three-Way Edge Analysis
Coherence preservation proofs split per edge: updated (type+trace change), related (shares endpoint), unrelated (trivially preserved).

### 4. Parametrized Coinduction (paco)
EQ2 and bisimulation proofs use paco-lean for parametrized coinduction, avoiding manual guardedness arguments.

### 5. Iris Integration via iris-lean
Runtime library connects to iris-lean for separation logic primitives. Ghost maps use `Positive` keys with application-level encoding. The `GhostMapSlot V` typeclass registers value types.

### 6. Linear Capability Tokens
Unforgeable tokens tied to endpoints enforce linear resource usage. The monitor validates token ownership before permitting actions.

---

## Quick Navigation Guide

**Want to understand...**

- **Session type definitions?** → SessionTypes/GlobalType/Core.lean, LocalTypeR/Core.lean
- **De Bruijn indices?** → SessionTypes/LocalTypeDB/Core.lean
- **Coinductive equality (EQ2)?** → SessionCoTypes/EQ2/Core.lean
- **Bisimulation?** → SessionCoTypes/Bisim/Core.lean
- **Inductive ↔ coinductive bridge?** → SessionCoTypes/Coinductive/Roundtrip/
- **Asynchronous subtyping?** → SessionCoTypes/AsyncSubtyping/Core.lean, Decidable.lean
- **Projection algorithm?** → Choreography/Projection/Project/Core.lean, ImplBase.lean
- **Projection correctness (harmony)?** → Choreography/Harmony.lean, Harmony/StepHarmony.lean
- **Operational semantics?** → Semantics/Environment.lean, Protocol/Semantics.lean
- **Coherence invariant?** → Protocol/Coherence/Consume.lean, Protocol/Coherence/EdgeCoherence.lean
- **Coherence preservation?** → Protocol/Coherence/Preservation.lean, Protocol/Coherence/SelectPreservation.lean
- **Subtype replacement preservation?** → Protocol/Coherence/SubtypeReplacement.lean
- **Configuration equivalence (quotient)?** → Protocol/Coherence/ConfigEquiv.lean
- **Unified preservation skeleton?** → Protocol/Coherence/Unified.lean
- **Higher-order Consume (delegation)?** → Protocol/Coherence/GraphDelta.lean
- **Role renaming proofs?** → Protocol/Coherence/RoleSwap.lean
- **Type system?** → Protocol/Typing/Judgments.lean (`HasTypeProcN`, `WTConfigN`)
- **Type safety?** → Protocol/Preservation.lean
- **Deadlock freedom?** → Protocol/DeadlockFreedom.lean
- **Runtime monitoring?** → Protocol/Monitor/Core.lean
- **Deployment composition?** → Protocol/Deployment/Interface.lean, Protocol/Deployment/Linking.lean
- **Crash tolerance?** → Protocol/CrashTolerance.lean
- **Noninterference?** → Protocol/Noninterference.lean
- **Delivery models?** → Protocol/DeliveryModel.lean
- **Classical transport framework?** → Classical/Transport.lean
- **Foster-Lyapunov-Harris?** → Classical/FosterLyapunovHarris.lean
- **Protocol-level classical instantiation?** → Protocol/Classical/Instantiation.lean
- **Iris separation logic (iris-lean)?** → Runtime/IrisBridge.lean
- **Ghost state?** → Runtime/ProgramLogic/GhostState.lean
- **Session-local proofs?** → Runtime/Proofs/SessionLocal.lean, Runtime/Proofs/Frame.lean
- **Delegation proofs?** → Protocol/Coherence/Delegation.lean
- **protocol machine-level progress theorem?** → Runtime/Proofs/Progress.lean
- **Lyapunov measure?** → Runtime/Proofs/Lyapunov.lean, Runtime/Proofs/WeightedMeasure.lean
- **Scheduling bounds?** → Runtime/Proofs/SchedulingBound.lean
- **protocol machine instruction specifications?** → Runtime/ProtocolMachine/Semantics/InstrSpec.lean
- **protocol machine instruction preservation proofs?** → Runtime/Proofs/ProtocolMachine/InstrSpec.lean
- **protocol machine bytecode compiler?** → Runtime/ProtocolMachine/Model/CompileLocalTypeR.lean
- **Dynamic choreography loading (executable path)?** → Runtime/ProtocolMachine/Runtime/Loader.lean
- **Dynamic choreography loading proofs?** → Runtime/Proofs/ProtocolMachine/LoadChoreography.lean
- **N-concurrent scheduling?** → Runtime/ProtocolMachine/Runtime/Runner.lean, Runtime/Proofs/Concurrency.lean
- **protocol machine failure model (executable path)?** → Runtime/ProtocolMachine/Runtime/Failure.lean, Runtime/ProtocolMachine/Runtime/Failure/Core.lean
- **protocol machine failure proofs/predicates?** → Runtime/Proofs/ProtocolMachine/Failure.lean, Runtime/Proofs/ProtocolMachine/FailurePredicates.lean
- **Buffer boundedness?** → Protocol/BufferBoundedness.lean
- **Protocol symmetry?** → Protocol/Symmetry.lean
- **Spectral gap bounds?** → Protocol/Classical/SpectralGap.lean
- **protocol machine JSON runner?** → Runtime/Tests/ProtocolMachineRunner.lean
- **What is axiomatized?** → [Axiom Inventory](#axiom-inventory)

### V2 Additions

- **Speculation semantics?** → Runtime/ProtocolMachine/Semantics/ExecSpeculation.lean
- **Threaded execution?** → Runtime/ProtocolMachine/Runtime/ThreadedRunner.lean
- **Threaded concurrency proofs?** → Runtime/Proofs/ConcurrencyThreaded.lean
- **Envelope-based adequacy?** → Runtime/Adequacy/EnvelopeCore/
- **Theorem pack infrastructure?** → Runtime/Proofs/TheoremPack/
- **Effect bisimulation?** → Runtime/Proofs/EffectBisim/
- **Distributed profile adapters?** → Runtime/Proofs/Adapters/Distributed/
- **protocol machine speculation proofs?** → Runtime/Proofs/ProtocolMachine/Speculation.lean
- **Configuration equivalence proofs?** → Runtime/Proofs/ProtocolMachine/InstrSpec/
- **Iris extraction?** → IrisExtractionInstance/
- **Classical analysis?** → ClassicalAnalysisInstance/
- **Release conformance?** → Runtime/Proofs/TheoremPack/ReleaseConformance.lean
