ADR 0038 - Wire Proof-Track Theorem Ledger

Collects the Wire proof-track theorem targets and separates Lean proof work from Haskell correspondence obligations.

On this page
  1. Status
  2. Context
  3. Decision
  4. Ledger
  5. Ordering
  6. Consequences
  7. Positive
  8. Negative
  9. Wire Admission Artifact Notes
  10. Obligations
  11. Alternatives considered
  12. Related

ADR 0038 - Wire Proof-Track Theorem Ledger

Status

Proposed - this ADR is the theorem-ledger slice for the Wire boundary-resource ADR stack. It names the proof obligations that guide the next Lean and Haskell correspondence work without deciding that the Wire compiler must move into Lean.

Context

ADRs 0032-0037 define the semantic vocabulary for boundary resources, guarded-affine select(...), restricted actualization authority, rewrite boundary laws, selected-branch budget policy, and latent structural control operators.

The proof obligations from those ADRs are intentionally precise, but they are spread across several documents. The current Lean track also already proves a substantial subset of Wire rewrite and CorePure obligations, while other claims still depend on Haskell compiler/runtime correspondence or future runtime policy.

Cortex therefore needs one proof-track ledger that states which theorem targets exist, which layer owns each target, and which open issue advances it. This is the ADR-A slice from GitHub #103: it settles what must be proved before deciding whether the compiler remains Haskell-first, becomes a Lean-specified Haskell implementation, or eventually moves into Lean.

Decision

Wire proof work should use a theorem ledger that separates four classes of obligations:

  1. Mechanized Lean surfaces - theorem statements already present under theory/.
  2. Immediate Lean theorem targets - proof-side declarations that can be added before proving executable Haskell correspondence.
  3. Haskell correspondence targets - executable compiler/runtime paths that must produce the witnesses consumed by the Lean proof model, usually through tests or a future Lean oracle.
  4. Deferred semantic targets - obligations that require a later runtime or language decision before they should be mechanized.

The ledger is the canonical place to add or retire Wire proof targets. Individual ADRs should state their semantic obligations, while this ADR records the implementation-facing theorem names, dependencies, and status.

The human-readable dashboard for readers who want claims, counts, and Haskell correspondence status lives in Reference/proof-status.md. This ADR remains the decision record; the reference page is the current-state status view.

Ledger

In the status column, “Mechanized” means the named proof-side declaration has landed for the row’s claim. “Mechanized on the Lean side” emphasizes that the proof-side theorem exists while executable Haskell correspondence remains a separate open target.

Compiler admission gates, such as ADR 0023 duplicate and prefix-conflicting CorePure record-path rejection, are implementation preconditions rather than admitted-middle proof claims. They remain tracked by compiler tests and correspondence issues, but they are not theorem-ledger rows until the parser or elaborator itself is mechanized.

AreaTheorem or witness targetRuntime or proof counterpartStatus
CorePure output keyspureNode_evalOutputs_keys_in_outputPorts, pureNode_evalOutputs_outputPorts_presentSource pure nodes lower to one native pure task whose successful output map exposes exactly the declared ports.Mechanized.
CorePure where fieldswhereStaticFields_sound, pureNode_evalWhereEnv_record_hasOnlyFields, pureNode_evalWhereEnv_localEnv_matchStatic where discovery is sound for matching runtime environments, and opened fields hide same-named static facts.Mechanized.
CorePure loweringpureNode_lowering_evalOutputs_eqLowered native pure-task configs evaluate like their source pure node in the proof model.Mechanized.
CorePure value contractspureNode_evalOutputs_values_satisfy_outputContracts, pureNode_evalOutputs_values_satisfy_valueContractsSuccessful pure outputs propagate abstract output-expression contracts and a first concrete proof-side value-contract table. Haskell validates native-pure task configs before compiler/runtime evaluation and wraps outputs through the shared node-boundary egress helpers.Lean value-contract carrier and Haskell preflight/egress checks landed; full Wire contract wrapping correspondence remains tracked by GitHub #117.
CorePure builtin authorityclosedBuiltinSignature_eq, closedBuiltinEnv_authorityFreeThe proof-side builtin signature mirror contains only pure-value entries; Haskell exposes corePureBuiltinAuthorityReport so builtin-table changes have a closed-authority review hook.Lean mirror and Haskell authority report landed; evaluator correspondence remains tracked by GitHub #116.
CorePure static context correspondencetopLevelBindings_establish_staticContextSuccessful proof-side top-level binding evaluation from the empty environment constructs EnvMatchesStatic; Haskell now builds a CorePureStaticContext from top-level pure bindings and uses it for static where discovery.Lean bridge target and Haskell static-context witness landed; stronger shared-oracle/evaluator correspondence remains tracked by GitHub #114.
Pulse transition envelopeSafePulseRunState, pulseRecoveryStep_preserves_safeRunState, pulseExecutionStep_preserves_safeRunState, pulseReplayDeterminism_modulo_fixedOutcomesFixed-topology Pulse recovery and admissible frontier fact folds after recovery normalization preserve structural wellFormedGraphState, classify without stuck, and replay fixed distinct-node facts independently of fold order.Mechanized on the Lean side; executable correspondence has proof-shaped GraphRuntime tests.
Rewrite admissionplanGraphRewriteChecks_admissible, runtimePlannerConstruction_admissible, constructedPlannedRewriteDelta_admissible_of_inputsRuntime-shaped planner witnesses instantiate abstract admissible rewrites.Mechanized on the Lean side.
Constructed chainsConstructedPlanningChain.toRewriteChain, .preserves_sourceValid, .steps_le_rewriteOps, .finalBudget_le_initialFinite constructed chains erase to abstract rewrite chains and preserve source validity and budget bounds.Mechanized on the Lean side.
Registry boundaryconstructedPlannedRewriteDelta_preserves_registryBoundary, constructedPlanningChain_preserves_registryBoundary_of_constructedDeltaConstructed deltas and chains preserve registryBoundary registry from bundled added-node and added-edge admission obligations.Mechanized on the Lean side; runtime witness production remains #110.
Planner/runtime correspondenceplanGraphRewrite_produces_RuntimeConstructionInputs and admitRewriteDelta_produces_AdmittedRewriteDeltaHaskell planGraphRewrite, consumeRewriteBudget, and admitRewriteDelta produce the Lean witness fields; planGraphRewriteWithAdmissionWitness and tamper tests now check the runtime/planned/admitted drift rails.Haskell witness checks landed for known rewrite forms and budget drift; full field-by-field RuntimeConstructionInputs production remains #110.
Boundary resourcesBoundaryLaw, BoundaryResourceUse, BudgetedBoundaryResourceUse, GraphRewrite.resourceUse, GraphRewrite.expandNode_resourceUse, GraphRewrite.appendAfter_resourceUse, ConstructedPlanningStep.boundaryResourceUse, .boundaryResourceCost_fits_budget, .rewriteSlotsUnique, ConstructedPlanningChain.ContainsRewriteSlot, .SlotUnique, .SlotUniqueTrace, RewriteSlotsUnique, rewriteSlot_spent_at_most_once, BoundaryResource.boundaryPreservedRuntime-shaped rewrites declare their boundary law and anchor rewrite slot; constructed planner steps expose budgeted resource use, fit the incoming budget, and form a one-slot no-double-spend epoch. Proof-relevant slot-unique traces expose occurrence-sensitive multi-step no-double-spend through Nodup over projected rewrite slots.Lean single-step and proof-relevant slot-unique epoch surfaces landed; Haskell admission witnesses now carry BudgetedBoundaryResourceUse. Port-level accounting and durable multi-step witness production remain #151.
Node boundary normal formNodeBoundaryNormalForm, ingress_sound, body_sound, egress_sound, edge_sound, registered_body_sound, CorePure.corePureBoundary, CorePure.corePure_ingress_sound, CorePure.corePure_body_sound, CorePure.corePure_egress_sound, CorePure.corePure_evalOutputs_eq_egress_after_body_after_ingress, registry_contract_edge_sound, registry_edge_soundCompiler/materialization witnesses expose input environments, body arguments, body results, output environments, and edge satisfaction without edge-local computation. CorePure instantiates the generic carrier and factors through ingress/body/egress; registry edges discharge edge compatibility through EdgeSound.Mechanized on the Lean side; private Haskell node-boundary IR, compiler validation hooks, and shared runtime egress wrappers landed. Executor body certificates remain open.
Source linear port carrierSourcePortInstance, LinearPortGraph, LinearPortGraph.PortLinear, LinearPortGraph.forgetPorts, forgetPorts_edgeEndpointsInVertices, forgetPorts_overlay, overlay_preserves_portLinear, contract_preserves_portLinear, forgetPorts_contract, BulkContract, BulkContract.loweredEdges, bulkContract_preserves_portLinear, forgetPorts_bulkContract, LinearPortObject.nodePorts, LinearPortOperation.apply_result_portLinear, LinearPortSystem.certified_portLinear, AdmissionArtifact.PrimitiveTraceStackValid, AdmissionArtifact.SelectBridgeEntriesConsumed, AdmissionArtifact.PhantomBridgeBulkConnectionsReplayed, AdmissionArtifact.validatorReady_primitiveConnect_compatiblePair_consumed, AdmissionArtifact.validatorReady_primitiveOverlay_mem_prefixAvailable, AdmissionArtifact.validatorReady_primitiveConnect_mem_prefixAvailableCertified Wire/Circuit source objects carry source endpoint linearity and lower to relation topology without importing Mokhov contraction/distributivity before ports are forgotten. Raw syntax such as => is not assumed linear until elaboration supplies the certified operation boundary.Mechanized on the Lean side as the source carrier, source linear endpoint rule, endpoint-closed lowering, overlay and certified single-pair/bulk contraction preservation, contraction lowering, exact bulk-contraction lowering, node-port resource generator, and certified operation interface. Primitive graph admission now consumes certified BulkContract traces plus exact match-set witnesses. Haskell admission artifacts validate primitive row summaries as a single postorder replay stack, including overlay ledgers, connect operand frontiers, source-visible residual frontiers, exact select bridge variant-to-condition matches, exact phantom-adapter bulk matches, prefix-order availability, and compatible-pair consumption; direct Lean witness construction from JSON remains open.
Bounded fan compositionLinearPortGraph.MakeWitness, LinearPortGraph.MakeWitness.toObject, LinearPortGraph.MakeWitness.make_disjoint_of_distinctBindings, LinearPortGraph.PhantomDirection, LinearPortGraph.ProductAdapterKind, LinearPortGraph.PhantomProductShape, LinearPortGraph.BulkContractContainsPair, LinearPortGraph.LinearPortObject.bulkContract, LinearPortGraph.PhantomAdapterWitness, LinearPortGraph.PhantomAdapterWitness.starInsertion, LinearPortGraph.KindInstantiatedFrontiers, LinearPortGraph.Make.accept_portLinear, LinearPortGraph.MakeEach.accept_portLinear, LinearPortGraph.Star.accept_portLinear, AdmissionArtifact.GeneratedFormArtifact.sourceMakeItems, AdmissionArtifact.AdmissionStaticValue.toStaticValue, AdmissionArtifact.validatorReady_generated_sourceChild_staticRecordFieldsUnique, AdmissionArtifact.validatorReady_generated_sourceChild_staticRecordFieldsUnique_toStaticValue, AdmissionArtifact.validatorReady_generated_make_sourceMakeItems_labelsCanonical, AdmissionArtifact.validatorReady_generated_make_sourceMakeItems_valuesEmpty, AdmissionArtifact.validatorReady_emptyGeneratedForm_bindingRow, AdmissionArtifact.validatorReady_phantomAdapter_record_multi_boundary_labeled, AdmissionArtifact.validatorReady_phantomAdapter_indexed_multi_contract_eq, AdmissionArtifact.validatorReady_phantomAdapter_indexed_multiCompatibilityShapesUniqueADR 0048’s make, ADR 0051’s makeEach, and ADR 0049/0052’s finite-product * are represented as source-level constructions over certified-linear primitives: open node ports, overlay, and bulk contraction. MakeWitness pins generated nodes to a shared binding projection and exact kind-derived child port sets. KindInstantiatedFrontiers is the accepted-kind-indexed proof-side result of kind substitution, preserves template contracts under generated child labels, and requires template frontier labels to be the declared PortLabel formal. PhantomProductShape pins the generated adapter to one phantom node with a declared multi/singular boundary, singular aggregate contract, indexed element-contract uniformity, indexed label uniqueness, and source-order enumeration; PhantomAdapterWitness pins the two * bulk traces to exact phantom-side boundary coverage. The decoded admission-artifact schema names the proof-side target for Haskell generated-family rows, maps source makeEach payloads into StaticValue, exposes Haskell’s duplicate-free static record fields plus value-free/count-label checks for make rows as named Lean accessors, and projects phantom products into record-boundary, indexed element-contract, and indexed compatibility-key facts.Mechanized on the Lean side as proof-facing construction witnesses. Haskell now expands literal/pre-bound numeric make, makeEach, record-form *, and bounded-indexed [T; N] *; compile-from-text admission artifacts expose generated-family provenance, Lean-shaped makeEach Value payloads, and phantom-adapter products, with Haskell decode/re-encode tests pinning the persisted schema and compiler metadata emission gated by wireAdmissionArtifactValidatorReady. Lean names the decoded artifact target; exact witness production from executable kind/product substitution remains open.
Ephemeral frontier reclaimLinearPortGraph.FrontierFinished, LinearPortGraph.OutputReclaimable, LinearPortGraph.InputReclaimable, frontierFinished_noRemainingConsumerObligations, frontierFinished_noRemainingProducerObligations, frontierFinished_reclaimableA finished linear source frontier exposes no remaining input or output endpoints. Therefore every owned output has one internal consumer, every owned input has one internal producer, and the in-memory endpoint resources have no open frontier obligations left. Durable provenance and observability profiles may still retain settled records intentionally.Mechanized on the Lean side for the source frontier model. Runtime reclaim hooks, source-to-actualized projection, and durable-profile retention policy remain open.
Closed actualized port linearityActualizedPortInstance, OutputPortUse, ActualizedPortGraph.ClosedPortLinear, actualizedOutputPort_consumed_exactly_once, actualizedInputPort_produced_exactly_once, compiledPortUseWitness_edge_input_uniqueProducer, portUseWitness_toGraph_closedPortLinear, selectActualize_preserves_closedPortLinearityCompiler or admission witnesses should account for each closed actualized port instance exactly once: one producer edge for each input; and one downstream edge consumer or one terminal egress, sink, or exported boundary discharge for each output. Direct edge-level fan-out and fan-in are rejected; explicit fan-out, sharing, persistence, broadcast, projection, and record↔ports adapter nodes consume one source port and produce fresh output port instances.Mechanized on the Lean side as a closed proof-side port-use witness model over the supplied witness domain. Haskell port-use witness production and source-to-actualized projection remain open; source fan-in/fan-out rejection is tested at admission.
Rewrite boundary lawsBoundaryResource.SubstitutionExposesAnchorBoundary, GraphRewrite.substitution_consumes_anchor_boundary, GraphRewrite.appendContinuation_retains_anchor_boundary, BoundaryResource.substitution_preserves_boundary, BoundaryResource.appendContinuation_preserves_boundaryReplacement and append are separate boundary laws even when both pass through runtime rewrite admission; substitution carries an explicit consumed-anchor-boundary exposure hook that append does not require.Mechanized on the Lean side; Haskell rewrite classification mirrors the Lean laws. Concrete substitution boundary-exposure witnesses remain #151 and #110.
Select source admissionSelectAdmission.SelectableOutputShape, SelectAdmission.resolveArmKey, SelectAdmission.admitClause, SelectAdmission.admitClauseAtNode, SelectAdmission.LatentSelectAdmission.FromClause, SelectAdmission.LatentSelectAdmission.toLatentBranchFamily, AdmissionArtifact.validatorReady_select_identityArm_bridgeShape, AdmissionArtifact.validatorReady_select_nonIdentityArm_bodyShapes, AdmissionArtifact.validatorReady_select_variantsShareExclusiveGroupSource select(...) clauses are admitted against a two-or-more exclusive output sum projected from the base node. Admission resolves exact labels before unique contract-name fallback, rejects duplicate canonical arms, missing coverage, ambiguous contract fallback, and non-exclusive bases, keeps branch bodies latent until selected-arm actualization, and names body provenance as a separate FromClause obligation. The decoded admission-artifact surface exposes identity and non-identity branch body-shape facts and the source exclusive group shared by persisted base variants, all validated by Haskell.Mechanized on the Lean side as source-level admission and a bridge into LatentBranchFamily; executable production of the admitted latent branch evidence and body-provenance witnesses remains a correspondence target.
Select actualizationLatentBranchFamily.fragmentsValid, .fragmentsPairwiseDisjoint, selectActualize_lowers_to_appendAfter, selectActualize_runtimeRewrite_spec_eq, selectActualize_admissible_of_constructedStep, selectActualize_preserves_registryBoundaryCertified latent families carry per-fragment validity and disjointness; the selected arm then lowers definitionally to the current retained-owner AppendAfter realization and inherits existing admission and boundary proofs.Mechanized on the Lean side; Haskell condition lowering emits AppendAfter and latent branch delta signatures with boundary-resource classification. Persisted materialization audit remains #138.
Unselected branchesselectActualize_unselected_not_in_selectedFragment, selectedBranch_unselected_not_replayed, selectedBranch_unselected_not_in_delta_topologyUnselected branch fragments are outside the selected raw fragment by the certified-family disjointness invariant; under the runtime namespace-freshness premise they are also outside the constructed selected-branch delta topology.Mechanized on the Lean side; Haskell selected-branch lowering tests check that unselected branch nodes do not enter the admitted selected delta.
Latent branch budgetselectActualize_consumes_selected_cost, SelectedBranchRecoveryRecord.step_toRewrite_admissibleThe admitted selected-arm constructed delta consumes runtime rewrite budget under ADR 0036’s selected-cost policy.Mechanized on the Lean side; Haskell selected-branch admission tests cover selected-cost accounting through planGraphRewriteWithAdmissionWitness.
CorePure execution factscorePureExecutionStep_preserves_safeRunStateSuccessful admitted CorePure output evaluation can be emitted as a Pulse success fact, retaining output-port and proof-side value-contract evidence while preserving the safe-run envelope.Mechanized on the Lean side; runtime fact production remains a Haskell correspondence target.
Wire/Pulse admitted run traceWireTopologyDAGBridge, WireTopologyDAGBridge.ofAcyclic, MaterializedPulseState, SafeWireRunState, WirePulseSnapshot, WirePulseSnapshot.recovered, WirePulseSnapshot.runStart_establishes_safeRunState, AdmittedWirePulseStep, AdmittedWirePulseTrace, AdmittedWirePulseStep.preserves_safeRunState, AdmittedWirePulseTrace.preserves_safeRunState, AdmittedWirePulseTrace.preserves_safeRunState_from_runStart, AdmittedWirePulseTrace.final_not_stuck, AdmittedWirePulseTrace.final_not_stuck_from_runStartWire planning validity, registry boundary, rewrite budget bounds, and Pulse wellFormedGraphState move together across every finite trace over the closed admitted-middle alphabet: recovery, frontier facts, CorePure facts, constructed rewrites, selected-arm actualization, and selected-branch recovery. CorePure-success steps require the trace payload CorePure.Name → Option CorePure.Value; the other constructors are payload-polymorphic.Mechanized on the Lean side as the closed middle proof, including composition from persisted recovery preconditions; executable transition witnesses, materialization witnesses, retained-state continuity, and durable provenance decoding remain correspondence targets.
Fixed-result replaywirePulseExecutionFacts_replay_deterministicGiven the same external frontier facts for distinct nodes, recovered state is invariant under fact order.Mechanized for the fixed-topology Pulse/Wire envelope.
Latent recoveryPersistedSelectedBranchAdmission, PersistedSelectedBranchAdmission.provenance_of_recovered_eq, SelectedBranchRecoveryRecord.Provenance, replayedRewrite_eq_of_selected_eq, selectedBranch_recovery_deterministic, selectedBranch_recovery_preserves_safeRunStateRecovery records loaded from the same persisted selected-branch admission replay the same selected branch, constructed delta, and remaining budget, and never replay unselected alternatives.Mechanized on the Lean side as replay of the proven persisted selected append rewrite; Haskell selected-branch lowering/admission tests hook the executable path, and durable lineage decoding remains a runtime correspondence obligation.

Current Haskell correspondence checks include corePureStaticContextFromBindings, corePureWhereStaticFields, corePureBuiltinAuthorityReport, validatePureTaskConfig, validateNodeBoundaryNormalForm, shared node-boundary egress wrappers, rewriteBoundaryResourceUse, latent condition delta signatures, and selected-branch lowering tests over planGraphRewriteWithAdmissionWitness for runtime planner, budget, and boundary-resource equations. These checks are executable drift detectors, not Lean proofs that the compiler produces every RuntimeConstructionInputs field.

Ordering

This ordering covers the Haskell correspondence engineering side of the ledger. For the substrate-novelty priority (which research questions actually need answering before correspondence engineering is worth investing in), see Roadmap/Epics/substrate-soundness-closure.md. The epic argues that closing the novel-middle composition (four cross-layer bridges plus one stitch-up theorem) is the load-bearing research deliverable, and that the four engineering steps below become amplification work afterwards.

The next implementation proof work should proceed in this order:

  1. CorePure evaluator and contract correspondence - continue from the Haskell static-context witness, builtin-authority report, duplicate-record preflight, and node-boundary egress checks toward a fuller evaluator/contract oracle.
  2. Planner/runtime correspondence - complete field-by-field RuntimeConstructionInputs production, registry-boundary admission, and budget-admission correspondence beyond the current drift-check harness.
  3. Materialization correspondence - continue from WireTopologyDAGBridge.ofAcyclic toward executable materialization witnesses that produce MaterializedPulseState.
  4. Recovery correspondence - connect persisted rewrite-lineage rows to the selected-branch recovery record and materialized Pulse-state witness more directly.

This order is intentionally asymmetric: proof-side Lean targets should be named before Haskell correspondence attempts to produce their witnesses.

Consequences

Positive

  • Prevents proof obligations from being lost across ADRs, issues, and theory/README.md.
  • Makes the Lean/Haskell boundary explicit without prematurely moving the compiler into Lean.
  • Gives future proof PRs a canonical place to add, rename, discharge, or defer theorem targets.
  • Keeps select(...) proof work tied to existing rewrite admission instead of inventing a parallel proof stack.

Negative

  • Adds one more internal ADR that must be kept current as theorem targets land or change names.
  • Some theorem names in this ledger are target names, not current declarations.
  • Haskell correspondence remains a testing/oracle obligation until Cortex chooses a stronger compiler-spec authority model.

Wire Admission Artifact Notes

  • Generated-family artifact handoff now recovers a unique source generated-child row for every surviving used child, including the optional static payload, and exposes binding-owned child node names plus per-child frontier validity and uniqueness through named ValidatorReady accessors.
  • Phantom-adapter artifact handoff now names the row and domain facts Haskell validates for the phantom node, singular endpoint, multi-side endpoints, and left/right bulk ledgers. The Lean accessors keep the stronger boundary-closure shape, including optional exclusive-group owners, record aggregate-contract rows, indexed element-contract rows, indexed nominal-element rejection, and equality between the singular endpoint contract and the serialized aggregate product contract. Admission artifact schema version 3 carries the record aggregate contract explicitly.
  • Primitive replay has branch-specific exactness theorems for empty, node, binding-reference, overlay, and connect rows. Select admission now exposes both label-resolution and contract-fallback uniqueness.
  • SelectedBranchRecoveryRecord.PhantomAdapterEmbedding and selectedBranch_recovery_embeddedPhantomAdapter_artifact_replayed_and_pruned name the recovery hook for selected branches that contain a finite-product * adapter: the persisted adapter node is replayed in the selected branch and pruned from every unselected branch.

Obligations

  • When a listed theorem target lands, update this ADR or the Track 3 proof summary so the status is no longer stale.
  • New Wire proof work should link to the relevant ledger row and issue.
  • If GitHub #103 later chooses Lean as compiler spec or implementation, this ADR should be updated or superseded to reflect the new authority model.

Alternatives considered

  • Keep the proof roadmap only in theory/README.md - rejected because the README should summarize landed proof surfaces, not be the canonical decision record for future theorem targets.
  • Track every proof target only in GitHub issues - rejected because issues are active planning state, while the theorem split is an architectural decision.
  • Decide the Lean compiler question now - rejected because the theorem list should come before choosing Haskell-first, Lean-spec, or Lean-implementation authority.