Cortex.Wire.Planner.Chain

On this page
  1. Overview
  2. Context
  3. Theorem Split
  4. Constructed Planning Steps
  5. Constructed Planning Chains
  6. Registry Boundary Specialization
Imports
import Cortex.Wire.Planner.Construction

Overview

Runtime-shaped chains for constructed Wire planner rewrites.

Context

Cortex.Wire.Planner.Construction proves that one runtime-shaped planner step can construct an admissible proof-carrying rewrite and carry the SourcePlanningContextValid invariant to the next planned topology. This module lifts that single-step surface to finite chains over PlanningContext.

The abstraction remains proof-side. It does not execute Haskell and does not prove that planGraphRewrite produces the witnesses. Instead, every chain step carries the same runtime-shaped witnesses used by the single-step construction: source validity, namespace discipline, anchor membership, raw subgraph validity, inserted-depth agreement, final acyclicity, budget admission, and caller-supplied contract preservation.

Theorem Split

The page defines constructed planning steps, constructed planning chains, the conversion from constructed chains to abstract RewriteChains, and the chain-level preservation theorems for source validity, budget, generic contracts, and the registry boundary specialization.

namespace Cortex.Wireopen Cortex.Graph

Constructed Planning Steps

section ConstructedPlanningStepvariable {node : Type}variable [DecidableEq node]

ConstructedPlanningStep is one runtime-shaped planned rewrite.

The step starts from a PlanningContext, consumes a RewriteBudget, and uses the concrete planner construction from Cortex.Wire.Planner.Construction. It keeps the caller-supplied contract preservation witness because contract meaning is external to the generic planner model.

structure ConstructedPlanningStep (policy : RuntimeNamespacePolicy node) (contractOk : Graph node → Prop) (context : PlanningContext node) (budget : RewriteBudget) (rawRewrite : GraphRewrite node) (insertedDepth : Nat) (remaining : RewriteBudget) : Prop where

Runtime-shaped construction inputs for this step.

inputs : RuntimeConstructionInputs policy context rawRewrite insertedDepth

Budget admission for the constructed delta.

admitted : AdmittedRewriteDelta budget (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth) remaining

Caller-specific contract preservation for this planned rewrite.

contractPreserved : ∀ g, denote g = denote context.topology → contractOk g → contractOk (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth).topologynamespace ConstructedPlanningStepvariable {policy : RuntimeNamespacePolicy node}variable {contractOk : Graph node → Prop}variable {context : PlanningContext node}variable {budget remaining : RewriteBudget}variable {rawRewrite : GraphRewrite node}variable {insertedDepth : Nat}

The constructed planned delta for this step.

noncomputable def delta (_step : ConstructedPlanningStep policy contractOk context budget rawRewrite insertedDepth remaining) : PlannedRewriteDelta node := constructedPlannedRewriteDelta policy context rawRewrite insertedDepth

The next planning context produced by this step.

noncomputable def nextContext (step : ConstructedPlanningStep policy contractOk context budget rawRewrite insertedDepth remaining) : PlanningContext node := { topology := step.delta.topology definitions := step.delta.definitions }

The proof-carrying rewrite induced by this constructed planning step.

noncomputable def toRewrite (step : ConstructedPlanningStep policy contractOk context budget rawRewrite insertedDepth remaining) : Rewrite node contractOk := step.delta.toRewrite context.topology (plannedRewriteSafety_of_checks (runtimePlannerConstruction_planGraphRewriteChecks (constructedPlannedRewriteDelta_runtimePlannerConstruction step.inputs.toValidation)) step.contractPreserved)

Constructed planning steps derive the older validation bundle.

theorem toValidation (step : ConstructedPlanningStep policy contractOk context budget rawRewrite insertedDepth remaining) : RuntimeConstructionValidation policy context rawRewrite insertedDepth := step.inputs.toValidation

Constructed planning steps instantiate the abstract admissibility predicate.

theorem toAdmissible (step : ConstructedPlanningStep policy contractOk context budget rawRewrite insertedDepth remaining) : admissible step.toRewrite context.topology budget := constructedPlannedRewriteDelta_admissible_of_inputs step.inputs step.admitted step.contractPreserved

Constructed planning steps carry source validity to their next context.

theorem toNextSourceValid (step : ConstructedPlanningStep policy contractOk context budget rawRewrite insertedDepth remaining) : SourcePlanningContextValid step.nextContext := step.inputs.toNextSourceValid

The induced proof-carrying rewrite applies to the context it was planned against.

theorem apply_eq_some (step : ConstructedPlanningStep policy contractOk context budget rawRewrite insertedDepth remaining) : step.toRewrite.apply context.topology = some step.nextContext.topology := node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetremaining:RewriteBudgetrawRewrite:GraphRewrite nodeinsertedDepth:ℕstep:ConstructedPlanningStep policy contractOk context budget rawRewrite insertedDepth remaining⊢ step.toRewrite.apply context.topology = some step.nextContext.topology All goals completed! 🐙

The admitted remaining budget matches the induced rewrite's consumed budget.

theorem remaining_eq_consume (step : ConstructedPlanningStep policy contractOk context budget rawRewrite insertedDepth remaining) : remaining = budget.consume step.toRewrite.cost := node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodebudget:RewriteBudgetremaining:RewriteBudgetrawRewrite:GraphRewrite nodeinsertedDepth:ℕstep:ConstructedPlanningStep policy contractOk context budget rawRewrite insertedDepth remaining⊢ remaining = budget.consume step.toRewrite.cost All goals completed! 🐙end ConstructedPlanningStepend ConstructedPlanningStep

Constructed Planning Chains

section ConstructedPlanningChainvariable {node : Type}variable [DecidableEq node]

ConstructedPlanningChain is a finite sequence of runtime-shaped planner steps.

The chain indexes current context, current budget, final context, final budget, and step count. Each step constructs the next PlanningContext from the planned delta's topology and definition domain before continuing.

inductive ConstructedPlanningChain (policy : RuntimeNamespacePolicy node) (contractOk : Graph node → Prop) : PlanningContext node → RewriteBudget → PlanningContext node → RewriteBudget → Nat → Prop where | done {context : PlanningContext node} {budget : RewriteBudget} : ConstructedPlanningChain policy contractOk context budget context budget 0 | step {context finalContext : PlanningContext node} {budget remaining finalBudget : RewriteBudget} {rawRewrite : GraphRewrite node} {insertedDepth steps : Nat} (planningStep : ConstructedPlanningStep policy contractOk context budget rawRewrite insertedDepth remaining) (tail : ConstructedPlanningChain policy contractOk planningStep.nextContext remaining finalContext finalBudget steps) : ConstructedPlanningChain policy contractOk context budget finalContext finalBudget (Nat.succ steps)namespace ConstructedPlanningChainvariable {policy : RuntimeNamespacePolicy node}variable {contractOk : Graph node → Prop}variable {context finalContext : PlanningContext node}variable {budget finalBudget : RewriteBudget}variable {steps : Nat}

Constructed planner chains erase to abstract proof-carrying rewrite chains.

theorem toRewriteChain (chain : ConstructedPlanningChain policy contractOk context budget finalContext finalBudget steps) : RewriteChain contractOk context.topology budget finalContext.topology finalBudget steps := node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodefinalContext:PlanningContext nodebudget:RewriteBudgetfinalBudget:RewriteBudgetsteps:ℕchain:ConstructedPlanningChain policy contractOk context budget finalContext finalBudget steps⊢ RewriteChain contractOk context.topology budget finalContext.topology finalBudget steps induction chain with node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodefinalContext:PlanningContext nodebudget:RewriteBudgetfinalBudget:RewriteBudgetsteps:ℕcontext✝:PlanningContext nodebudget✝:RewriteBudget⊢ RewriteChain contractOk context✝.topology budget✝ context✝.topology budget✝ 0 All goals completed! 🐙 node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodefinalContext:PlanningContext nodebudget:RewriteBudgetfinalBudget:RewriteBudgetsteps:ℕcontext✝:PlanningContext nodefinalContext✝:PlanningContext nodebudget✝:RewriteBudgetremaining✝:RewriteBudgetfinalBudget✝:RewriteBudgetrawRewrite✝:GraphRewrite nodeinsertedDepth✝:ℕsteps✝:ℕplanningStep:ConstructedPlanningStep policy contractOk context✝ budget✝ rawRewrite✝ insertedDepth✝ remaining✝_tail:ConstructedPlanningChain policy contractOk planningStep.nextContext remaining✝ finalContext✝ finalBudget✝ steps✝ih:RewriteChain contractOk planningStep.nextContext.topology remaining✝ finalContext✝.topology finalBudget✝ steps✝⊢ RewriteChain contractOk context✝.topology budget✝ finalContext✝.topology finalBudget✝ steps✝.succ All goals completed! 🐙

Constructed planner chains preserve the source-valid planning-context invariant.

theorem preserves_sourceValid (chain : ConstructedPlanningChain policy contractOk context budget finalContext finalBudget steps) (hSource : SourcePlanningContextValid context) : SourcePlanningContextValid finalContext := node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodefinalContext:PlanningContext nodebudget:RewriteBudgetfinalBudget:RewriteBudgetsteps:ℕchain:ConstructedPlanningChain policy contractOk context budget finalContext finalBudget stepshSource:SourcePlanningContextValid context⊢ SourcePlanningContextValid finalContext induction chain with node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodefinalContext:PlanningContext nodebudget:RewriteBudgetfinalBudget:RewriteBudgetsteps:ℕcontext✝:PlanningContext nodebudget✝:RewriteBudgethSource:SourcePlanningContextValid context✝⊢ SourcePlanningContextValid context✝ All goals completed! 🐙 node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodefinalContext:PlanningContext nodebudget:RewriteBudgetfinalBudget:RewriteBudgetsteps:ℕcontext✝:PlanningContext nodefinalContext✝:PlanningContext nodebudget✝:RewriteBudgetremaining✝:RewriteBudgetfinalBudget✝:RewriteBudgetrawRewrite✝:GraphRewrite nodeinsertedDepth✝:ℕsteps✝:ℕplanningStep:ConstructedPlanningStep policy contractOk context✝ budget✝ rawRewrite✝ insertedDepth✝ remaining✝_tail:ConstructedPlanningChain policy contractOk planningStep.nextContext remaining✝ finalContext✝ finalBudget✝ steps✝ih:SourcePlanningContextValid planningStep.nextContext → SourcePlanningContextValid finalContext✝hSource:SourcePlanningContextValid context✝⊢ SourcePlanningContextValid finalContext✝ All goals completed! 🐙

Non-empty constructed planner chains expose terminal source validity directly.

The initial source-validity hypothesis is only needed by the empty chain case; once at least one constructed step exists, that step's runtime inputs already carry the invariant to the tail.

theorem terminal_sourceValid_of_nonempty (chain : ConstructedPlanningChain policy contractOk context budget finalContext finalBudget (Nat.succ steps)) : SourcePlanningContextValid finalContext := node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodefinalContext:PlanningContext nodebudget:RewriteBudgetfinalBudget:RewriteBudgetsteps:ℕchain:ConstructedPlanningChain policy contractOk context budget finalContext finalBudget steps.succ⊢ SourcePlanningContextValid finalContext cases chain with node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontractOk:Graph node → Propcontext:PlanningContext nodefinalContext:PlanningContext nodebudget:RewriteBudgetfinalBudget:RewriteBudgetsteps:ℕremaining✝:RewriteBudgetrawRewrite✝:GraphRewrite nodeinsertedDepth✝:ℕplanningStep:ConstructedPlanningStep policy contractOk context budget rawRewrite✝ insertedDepth✝ remaining✝tail:ConstructedPlanningChain policy contractOk planningStep.nextContext remaining✝ finalContext finalBudget steps⊢ SourcePlanningContextValid finalContext All goals completed! 🐙

Non-empty constructed planner chains expose terminal acyclicity directly.

This is the acyclicity projection of terminal_sourceValid_of_nonempty; the first constructed step supplies the source-valid tail input.

theorem terminal_acyclic_of_nonempty (chain : ConstructedPlanningChain policy contractOk context budget finalContext finalBudget (Nat.succ steps)) : Acyclic finalContext.topology := chain.terminal_sourceValid_of_nonempty.sourceAcyclic

Constructed planner chain length is bounded by the initial rewrite-operation budget.

theorem steps_le_rewriteOps (chain : ConstructedPlanningChain policy contractOk context budget finalContext finalBudget steps) : steps ≤ budget.rewriteOps := rewriteChain_steps_le_rewriteOps chain.toRewriteChain

Constructed planner chains never replenish rewrite budget.

theorem finalBudget_le_initial (chain : ConstructedPlanningChain policy contractOk context budget finalContext finalBudget steps) : finalBudget.le budget := rewriteChain_finalBudget_le_initial chain.toRewriteChain

Constructed planner chains preserve the caller-supplied contract predicate.

theorem preserves_contracts (chain : ConstructedPlanningChain policy contractOk context budget finalContext finalBudget steps) (hContracts : contractOk context.topology) : contractOk finalContext.topology := rewriteChain_preserves_contracts chain.toRewriteChain hContracts

Constructed planner chains preserve acyclicity of the materialized topology.

theorem preserves_acyclic (chain : ConstructedPlanningChain policy contractOk context budget finalContext finalBudget steps) (hAcyclic : Acyclic context.topology) : Acyclic finalContext.topology := rewriteChain_preserves_acyclic chain.toRewriteChain hAcyclicend ConstructedPlanningChainend ConstructedPlanningChain

Registry Boundary Specialization

section RegistryBoundaryvariable {executor config contract authority : Type}variable [DecidableEq contract]variable [DecidableEq (StagedExecutorNode executor config authority)]namespace ConstructedPlanningStepvariable {policy : RuntimeNamespacePolicy (StagedExecutorNode executor config authority)}variable {context : PlanningContext (StagedExecutorNode executor config authority)}variable {budget remaining : RewriteBudget}variable {rawRewrite : GraphRewrite (StagedExecutorNode executor config authority)}variable {insertedDepth : Nat}

Build a registry-boundary constructed planning step from explicit new-node and added-edge admission obligations.

theorem ofRegistryBoundary (registry : ExecutorRegistry executor config contract authority) (inputs : RuntimeConstructionInputs policy context rawRewrite insertedDepth) (admitted : AdmittedRewriteDelta budget (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth) remaining) (hDelta : RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth)) : ConstructedPlanningStep policy (registryBoundary registry) context budget rawRewrite insertedDepth remaining := { inputs := inputs admitted := admitted contractPreserved := constructedPlannedRewriteDelta_registryBoundaryContractPreserved registry hDelta }

Constructed planning steps preserve the registry boundary from their explicit delta-admission obligations.

theorem registryBoundaryPreserved (registry : ExecutorRegistry executor config contract authority) (step : ConstructedPlanningStep policy (registryBoundary registry) context budget rawRewrite insertedDepth remaining) (hBoundary : registryBoundary registry context.topology) (hDelta : RegistryBoundaryDeltaAdmitted registry step.delta) : registryBoundary registry step.nextContext.topology := executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)policy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)budget:RewriteBudgetremaining:RewriteBudgetrawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕregistry:ExecutorRegistry executor config contract authoritystep:ConstructedPlanningStep policy (registryBoundary registry) context budget rawRewrite insertedDepth remaininghBoundary:registryBoundary registry context.topologyhDelta:RegistryBoundaryDeltaAdmitted registry step.delta⊢ registryBoundary registry step.nextContext.topology have hDeltaConstructed : RegistryBoundaryDeltaAdmitted registry (constructedPlannedRewriteDelta policy context rawRewrite insertedDepth) := executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)policy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)budget:RewriteBudgetremaining:RewriteBudgetrawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕregistry:ExecutorRegistry executor config contract authoritystep:ConstructedPlanningStep policy (registryBoundary registry) context budget rawRewrite insertedDepth remaininghBoundary:registryBoundary registry context.topologyhDelta:RegistryBoundaryDeltaAdmitted registry step.delta⊢ registryBoundary registry step.nextContext.topology All goals completed! 🐙 All goals completed! 🐙

Delta-admission evidence reconstructs the generic contractPreserved witness for a registry-boundary step.

theorem registryBoundaryContractPreserved (registry : ExecutorRegistry executor config contract authority) (step : ConstructedPlanningStep policy (registryBoundary registry) context budget rawRewrite insertedDepth remaining) (hDelta : RegistryBoundaryDeltaAdmitted registry step.delta) : ∀ g, denote g = denote context.topology → registryBoundary registry g → registryBoundary registry step.delta.topology := executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)policy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)budget:RewriteBudgetremaining:RewriteBudgetrawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕregistry:ExecutorRegistry executor config contract authoritystep:ConstructedPlanningStep policy (registryBoundary registry) context budget rawRewrite insertedDepth remaininghDelta:RegistryBoundaryDeltaAdmitted registry step.delta⊢ ∀ (g : Graph (StagedExecutorNode executor config authority)), denote g = denote context.topology → registryBoundary registry g → registryBoundary registry step.delta.topology intro g executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)policy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)budget:RewriteBudgetremaining:RewriteBudgetrawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕregistry:ExecutorRegistry executor config contract authoritystep:ConstructedPlanningStep policy (registryBoundary registry) context budget rawRewrite insertedDepth remaininghDelta:RegistryBoundaryDeltaAdmitted registry step.deltag:Graph (StagedExecutorNode executor config authority)hGraphEq:denote g = denote context.topology⊢ registryBoundary registry g → registryBoundary registry step.delta.topology executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)policy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)budget:RewriteBudgetremaining:RewriteBudgetrawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕregistry:ExecutorRegistry executor config contract authoritystep:ConstructedPlanningStep policy (registryBoundary registry) context budget rawRewrite insertedDepth remaininghDelta:RegistryBoundaryDeltaAdmitted registry step.deltag:Graph (StagedExecutorNode executor config authority)hGraphEq:denote g = denote context.topologyhBoundary:registryBoundary registry g⊢ registryBoundary registry step.delta.topology executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)policy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)budget:RewriteBudgetremaining:RewriteBudgetrawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕregistry:ExecutorRegistry executor config contract authoritystep:ConstructedPlanningStep policy (registryBoundary registry) context budget rawRewrite insertedDepth remaininghDelta:RegistryBoundaryDeltaAdmitted registry step.deltag:Graph (StagedExecutorNode executor config authority)hGraphEq:denote g = denote context.topologyhBoundary:registryBoundary registry ghContextBoundary:registryBoundary registry context.topology⊢ registryBoundary registry step.delta.topology All goals completed! 🐙end ConstructedPlanningStepnamespace ConstructedPlanningChain

Per-step registry obligations for a constructed planner chain.

The predicate records exactly the obligations that are not implied by vertex admission: newly introduced vertices must be admitted by the registry, and newly introduced edges must be admitted as endpoint-compatible edges. The same per-step payload reconstructs the generic contractPreserved witness through ConstructedPlanningStep.registryBoundaryContractPreserved.

inductive RegistryBoundaryDeltasAdmitted (registry : ExecutorRegistry executor config contract authority) {policy : RuntimeNamespacePolicy (StagedExecutorNode executor config authority)} : {context finalContext : PlanningContext (StagedExecutorNode executor config authority)} → {budget finalBudget : RewriteBudget} → {steps : Nat} → ConstructedPlanningChain policy (registryBoundary registry) context budget finalContext finalBudget steps → Prop where | done {context : PlanningContext (StagedExecutorNode executor config authority)} {budget : RewriteBudget} : RegistryBoundaryDeltasAdmitted registry (ConstructedPlanningChain.done (policy := policy) (contractOk := registryBoundary registry) (context := context) (budget := budget)) | step {context finalContext : PlanningContext (StagedExecutorNode executor config authority)} {budget remaining finalBudget : RewriteBudget} {rawRewrite : GraphRewrite (StagedExecutorNode executor config authority)} {insertedDepth steps : Nat} {planningStep : ConstructedPlanningStep policy (registryBoundary registry) context budget rawRewrite insertedDepth remaining} {tail : ConstructedPlanningChain policy (registryBoundary registry) planningStep.nextContext remaining finalContext finalBudget steps} (hDelta : RegistryBoundaryDeltaAdmitted registry planningStep.delta) (hTail : RegistryBoundaryDeltasAdmitted registry tail) : RegistryBoundaryDeltasAdmitted registry (ConstructedPlanningChain.step planningStep tail)

Constructed planner chains preserve the registry boundary from constructed-delta registry obligations, without using the generic contractPreserved witness carried by each step.

theorem preserves_registryBoundary_of_constructedDelta (registry : ExecutorRegistry executor config contract authority) {policy : RuntimeNamespacePolicy (StagedExecutorNode executor config authority)} {context finalContext : PlanningContext (StagedExecutorNode executor config authority)} {budget finalBudget : RewriteBudget} {steps : Nat} (chain : ConstructedPlanningChain policy (registryBoundary registry) context budget finalContext finalBudget steps) (hAdmissions : RegistryBoundaryDeltasAdmitted registry chain) (hBoundary : registryBoundary registry context.topology) : registryBoundary registry finalContext.topology := executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)finalContext:PlanningContext (StagedExecutorNode executor config authority)budget:RewriteBudgetfinalBudget:RewriteBudgetsteps:ℕchain:ConstructedPlanningChain policy (registryBoundary registry) context budget finalContext finalBudget stepshAdmissions:RegistryBoundaryDeltasAdmitted registry chainhBoundary:registryBoundary registry context.topology⊢ registryBoundary registry finalContext.topology induction hAdmissions with executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context:PlanningContext (StagedExecutorNode executor config authority)finalContext:PlanningContext (StagedExecutorNode executor config authority)budget:RewriteBudgetfinalBudget:RewriteBudgetsteps:ℕchain:ConstructedPlanningChain policy (registryBoundary registry) context budget finalContext finalBudget stepscontext✝:PlanningContext (StagedExecutorNode executor config authority)budget✝:RewriteBudgethBoundary:registryBoundary registry context✝.topology⊢ registryBoundary registry context✝.topology All goals completed! 🐙 executor:Typeconfig:Typecontract:Typeauthority:Typeinst✝¹:DecidableEq contractinst✝:DecidableEq (StagedExecutorNode executor config authority)registry:ExecutorRegistry executor config contract authoritypolicy:RuntimeNamespacePolicy (StagedExecutorNode executor config authority)context✝:PlanningContext (StagedExecutorNode executor config authority)finalContext✝:PlanningContext (StagedExecutorNode executor config authority)budget✝:RewriteBudgetfinalBudget✝:RewriteBudgetsteps✝:ℕchain:ConstructedPlanningChain policy (registryBoundary registry) context budget finalContext finalBudget stepscontext:PlanningContext (StagedExecutorNode executor config authority)finalContext:PlanningContext (StagedExecutorNode executor config authority)budget:RewriteBudgetremaining:RewriteBudgetfinalBudget:RewriteBudgetrawRewrite:GraphRewrite (StagedExecutorNode executor config authority)insertedDepth:ℕsteps:ℕplanningStep:ConstructedPlanningStep policy (registryBoundary registry) context budget rawRewrite insertedDepth remainingtail:ConstructedPlanningChain policy (registryBoundary registry) planningStep.nextContext remaining finalContext finalBudget stepshDelta:RegistryBoundaryDeltaAdmitted registry planningStep.delta_hTail:RegistryBoundaryDeltasAdmitted registry tailih:registryBoundary registry planningStep.nextContext.topology → registryBoundary registry finalContext.topologyhBoundary:registryBoundary registry context.topology⊢ registryBoundary registry finalContext.topology All goals completed! 🐙end ConstructedPlanningChain

Constructed planner chains preserve the Wire registry boundary.

theorem constructedPlanningChain_preserves_registryBoundary (registry : ExecutorRegistry executor config contract authority) {policy : RuntimeNamespacePolicy (StagedExecutorNode executor config authority)} {context finalContext : PlanningContext (StagedExecutorNode executor config authority)} {budget finalBudget : RewriteBudget} {steps : Nat} (chain : ConstructedPlanningChain policy (registryBoundary registry) context budget finalContext finalBudget steps) (hBoundary : registryBoundary registry context.topology) : registryBoundary registry finalContext.topology := rewriteChain_preserves_registryBoundary registry chain.toRewriteChain hBoundary

Constructed planner chains preserve the Wire registry boundary from explicit constructed-delta registry obligations.

theorem constructedPlanningChain_preserves_registryBoundary_of_constructedDelta (registry : ExecutorRegistry executor config contract authority) {policy : RuntimeNamespacePolicy (StagedExecutorNode executor config authority)} {context finalContext : PlanningContext (StagedExecutorNode executor config authority)} {budget finalBudget : RewriteBudget} {steps : Nat} (chain : ConstructedPlanningChain policy (registryBoundary registry) context budget finalContext finalBudget steps) (hAdmissions : ConstructedPlanningChain.RegistryBoundaryDeltasAdmitted registry chain) (hBoundary : registryBoundary registry context.topology) : registryBoundary registry finalContext.topology := ConstructedPlanningChain.preserves_registryBoundary_of_constructedDelta registry chain hAdmissions hBoundaryend RegistryBoundaryend Cortex.Wire