Cortex.Wire.Planner

On this page
  1. Overview
  2. Context
  3. Theorem Split
  4. Namespaced Rewrite Inputs
  5. Runtime List Boundaries
  6. Planner Construction Bridge
Imports
import Cortex.Wire.Admission import Mathlib.Data.Finset.Card

Overview

Executable-planner correspondence support for Wire rewrites.

Context

Cortex.Wire.Admission states the runtime planning contract once a rewrite's inserted subgraph already lives in the final node namespace. The Haskell runtime obtains that shape by applying namespaceSubgraph before it constructs the final topology. This module names that proof-side boundary: subgraph namespacing, the namespace-discipline obligation, relation-level correspondence for the AST mapping, and the theorem that turns proof-shaped executable planner equations into PlanGraphRewriteChecks.

Theorem Split

The page defines graph/subgraph/rewrite namespacing, proves the denotation of namespaced graph expressions, and then packages runtime construction equations into the admission contract used by planGraphRewriteChecks_admissible.

namespace Cortex.Wireopen Cortex.Graph

Namespaced Rewrite Inputs

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

RuntimeNamespacePolicy is the proof-side model of executable namespace syntax.

For the Haskell NodeId planner, namespaceNode anchor local is namespaceNodeId anchor local, while localAllowed local records the reserved-delimiter check performed before namespacing. The policy carries syntax-level facts that are independent of the current topology; freshness against a particular graph remains a NamespaceDiscipline obligation.

structure RuntimeNamespacePolicy (node : Type) where

Namespace a local inserted node under the rewrite anchor.

namespaceNode : node β†’ node β†’ node

The runtime syntax predicate accepted for local inserted node ids.

localAllowed : node β†’ Prop

For a fixed anchor, namespacing does not collapse distinct local node ids.

namespaceNode_injective : βˆ€ anchor, Function.Injective (namespaceNode anchor)

mapGraph f g maps a graph expression over its vertex labels.

def mapGraph (f : node β†’ node) : Graph node β†’ Graph node | Graph.empty => Graph.empty | Graph.vertex vertex => Graph.vertex (f vertex) | Graph.overlay left right => Graph.overlay (mapGraph f left) (mapGraph f right) | Graph.connect left right => Graph.connect (mapGraph f left) (mapGraph f right)

mapRelation f relation is the relation-level counterpart of mapGraph f.

def mapRelation (f : node β†’ node) (relation : Relation node) : Relation node := { vertices := relation.vertices.image f edges := relation.edges.image (fun edge => (f edge.1, f edge.2)) }

Relation mapping distributes over relation overlay.

theorem mapRelation_overlay (f : node β†’ node) (left right : Relation node) : mapRelation f (Relation.overlay left right) = Relation.overlay (mapRelation f left) (mapRelation f right) := node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Relation noderight:Relation node⊒ mapRelation f (left.overlay right) = (mapRelation f left).overlay (mapRelation f right) node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Relation noderight:Relation node⊒ (mapRelation f (left.overlay right)).vertices = ((mapRelation f left).overlay (mapRelation f right)).verticesnode:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Relation noderight:Relation node⊒ (mapRelation f (left.overlay right)).edges = ((mapRelation f left).overlay (mapRelation f right)).edges node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Relation noderight:Relation node⊒ (mapRelation f (left.overlay right)).vertices = ((mapRelation f left).overlay (mapRelation f right)).vertices All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Relation noderight:Relation node⊒ (mapRelation f (left.overlay right)).edges = ((mapRelation f left).overlay (mapRelation f right)).edges All goals completed! πŸ™

Relation mapping distributes over relation connect.

theorem mapRelation_connect (f : node β†’ node) (left right : Relation node) : mapRelation f (Relation.connect left right) = Relation.connect (mapRelation f left) (mapRelation f right) := node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Relation noderight:Relation node⊒ mapRelation f (left.connect right) = (mapRelation f left).connect (mapRelation f right) node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Relation noderight:Relation node⊒ (mapRelation f (left.connect right)).vertices = ((mapRelation f left).connect (mapRelation f right)).verticesnode:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Relation noderight:Relation node⊒ (mapRelation f (left.connect right)).edges = ((mapRelation f left).connect (mapRelation f right)).edges node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Relation noderight:Relation node⊒ (mapRelation f (left.connect right)).vertices = ((mapRelation f left).connect (mapRelation f right)).vertices All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Relation noderight:Relation node⊒ (mapRelation f (left.connect right)).edges = ((mapRelation f left).connect (mapRelation f right)).edges node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Relation noderight:Relation node⊒ Finset.image (fun edge => (f edge.1, f edge.2)) (left.edges βˆͺ right.edges βˆͺ left.vertices Γ—Λ’ right.vertices) = Finset.image (fun edge => (f edge.1, f edge.2)) left.edges βˆͺ Finset.image (fun edge => (f edge.1, f edge.2)) right.edges βˆͺ Finset.image f left.vertices Γ—Λ’ Finset.image f right.vertices node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Relation noderight:Relation node⊒ Finset.image (fun edge => (f edge.1, f edge.2)) left.edges βˆͺ Finset.image (fun edge => (f edge.1, f edge.2)) right.edges βˆͺ Finset.image (fun edge => (f edge.1, f edge.2)) (left.vertices Γ—Λ’ right.vertices) = Finset.image (fun edge => (f edge.1, f edge.2)) left.edges βˆͺ Finset.image (fun edge => (f edge.1, f edge.2)) right.edges βˆͺ Finset.image f left.vertices Γ—Λ’ Finset.image f right.vertices node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Relation noderight:Relation node⊒ Finset.image (Prod.map f f) left.edges βˆͺ Finset.image (Prod.map f f) right.edges βˆͺ Finset.image (Prod.map f f) (left.vertices Γ—Λ’ right.vertices) = Finset.image (Prod.map f f) left.edges βˆͺ Finset.image (Prod.map f f) right.edges βˆͺ Finset.image f left.vertices Γ—Λ’ Finset.image f right.vertices All goals completed! πŸ™

Mapping a graph expression and then denoting it equals mapping its denotation.

theorem denote_mapGraph (f : node β†’ node) (g : Graph node) : denote (mapGraph f g) = mapRelation f (denote g) := node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph node⊒ denote (mapGraph f g) = mapRelation f (denote g) induction g with node:Typeinst✝:DecidableEq nodef:node β†’ node⊒ denote (mapGraph f Graph.empty) = mapRelation f (denote Graph.empty) node:Typeinst✝:DecidableEq nodef:node β†’ nodex:node⊒ x ∈ (denote (mapGraph f Graph.empty)).vertices ↔ x ∈ (mapRelation f (denote Graph.empty)).verticesnode:Typeinst✝:DecidableEq nodef:node β†’ nodex:node Γ— node⊒ x ∈ (denote (mapGraph f Graph.empty)).edges ↔ x ∈ (mapRelation f (denote Graph.empty)).edges node:Typeinst✝:DecidableEq nodef:node β†’ nodex:node⊒ x ∈ (denote (mapGraph f Graph.empty)).vertices ↔ x ∈ (mapRelation f (denote Graph.empty)).vertices All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodef:node β†’ nodex:node Γ— node⊒ x ∈ (denote (mapGraph f Graph.empty)).edges ↔ x ∈ (mapRelation f (denote Graph.empty)).edges All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodef:node β†’ nodevertex:node⊒ denote (mapGraph f (Graph.vertex vertex)) = mapRelation f (denote (Graph.vertex vertex)) node:Typeinst✝:DecidableEq nodef:node β†’ nodevertex:nodex:node⊒ x ∈ (denote (mapGraph f (Graph.vertex vertex))).vertices ↔ x ∈ (mapRelation f (denote (Graph.vertex vertex))).verticesnode:Typeinst✝:DecidableEq nodef:node β†’ nodevertex:nodex:node Γ— node⊒ x ∈ (denote (mapGraph f (Graph.vertex vertex))).edges ↔ x ∈ (mapRelation f (denote (Graph.vertex vertex))).edges node:Typeinst✝:DecidableEq nodef:node β†’ nodevertex:nodex:node⊒ x ∈ (denote (mapGraph f (Graph.vertex vertex))).vertices ↔ x ∈ (mapRelation f (denote (Graph.vertex vertex))).vertices node:Typeinst✝:DecidableEq nodef:node β†’ nodevertex:nodex:node⊒ x = f vertex ↔ βˆƒ a, a = vertex ∧ f a = x node:Typeinst✝:DecidableEq nodef:node β†’ nodevertex:nodex:node⊒ x = f vertex β†’ βˆƒ a, a = vertex ∧ f a = xnode:Typeinst✝:DecidableEq nodef:node β†’ nodevertex:nodex:node⊒ (βˆƒ a, a = vertex ∧ f a = x) β†’ x = f vertex node:Typeinst✝:DecidableEq nodef:node β†’ nodevertex:nodex:node⊒ x = f vertex β†’ βˆƒ a, a = vertex ∧ f a = x node:Typeinst✝:DecidableEq nodef:node β†’ nodevertex:nodex:nodehMapped:x = f vertex⊒ βˆƒ a, a = vertex ∧ f a = x All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodef:node β†’ nodevertex:nodex:node⊒ (βˆƒ a, a = vertex ∧ f a = x) β†’ x = f vertex node:Typeinst✝:DecidableEq nodef:node β†’ nodex:node_local:nodehMapped:f _local = x⊒ x = f _local All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodef:node β†’ nodevertex:nodex:node Γ— node⊒ x ∈ (denote (mapGraph f (Graph.vertex vertex))).edges ↔ x ∈ (mapRelation f (denote (Graph.vertex vertex))).edges All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Graph noderight:Graph nodeleft_ih:denote (mapGraph f left) = mapRelation f (denote left)right_ih:denote (mapGraph f right) = mapRelation f (denote right)⊒ denote (mapGraph f (left.overlay right)) = mapRelation f (denote (left.overlay right)) calc denote (mapGraph f (Graph.overlay left right)) = Relation.overlay (denote (mapGraph f left)) (denote (mapGraph f right)) := rfl _ = Relation.overlay (mapRelation f (denote left)) (mapRelation f (denote right)) := node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Graph noderight:Graph nodeleft_ih:denote (mapGraph f left) = mapRelation f (denote left)right_ih:denote (mapGraph f right) = mapRelation f (denote right)⊒ (denote (mapGraph f left)).overlay (denote (mapGraph f right)) = (mapRelation f (denote left)).overlay (mapRelation f (denote right)) All goals completed! πŸ™ _ = mapRelation f (denote (Graph.overlay left right)) := node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Graph noderight:Graph nodeleft_ih:denote (mapGraph f left) = mapRelation f (denote left)right_ih:denote (mapGraph f right) = mapRelation f (denote right)⊒ (mapRelation f (denote left)).overlay (mapRelation f (denote right)) = mapRelation f (denote (left.overlay right)) All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Graph noderight:Graph nodeleft_ih:denote (mapGraph f left) = mapRelation f (denote left)right_ih:denote (mapGraph f right) = mapRelation f (denote right)⊒ denote (mapGraph f (left.connect right)) = mapRelation f (denote (left.connect right)) calc denote (mapGraph f (Graph.connect left right)) = Relation.connect (denote (mapGraph f left)) (denote (mapGraph f right)) := rfl _ = Relation.connect (mapRelation f (denote left)) (mapRelation f (denote right)) := node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Graph noderight:Graph nodeleft_ih:denote (mapGraph f left) = mapRelation f (denote left)right_ih:denote (mapGraph f right) = mapRelation f (denote right)⊒ (denote (mapGraph f left)).connect (denote (mapGraph f right)) = (mapRelation f (denote left)).connect (mapRelation f (denote right)) All goals completed! πŸ™ _ = mapRelation f (denote (Graph.connect left right)) := node:Typeinst✝:DecidableEq nodef:node β†’ nodeleft:Graph noderight:Graph nodeleft_ih:denote (mapGraph f left) = mapRelation f (denote left)right_ih:denote (mapGraph f right) = mapRelation f (denote right)⊒ (mapRelation f (denote left)).connect (mapRelation f (denote right)) = mapRelation f (denote (left.connect right)) All goals completed! πŸ™

NamespaceDiscipline records the proof-side safety of runtime node namespacing.

The localAllowed predicate is the generic Lean hook for executable syntax rules such as the Haskell NodeId restriction that local inserted ids must not contain the reserved namespace delimiter. Injectivity comes from the RuntimeNamespacePolicy; this discipline records the topology-specific checks.

structure NamespaceDiscipline (isLocalAllowed : node β†’ Prop) (ns : node β†’ node) (context : PlanningContext node) (spec : SubgraphSpec node) : Prop where

Local inserted node ids are accepted by the runtime namespace syntax.

localAllowed : βˆ€ localNode, localNode ∈ (denote spec.topology).vertices β†’ isLocalAllowed localNode

Namespaced inserted nodes are fresh against the current topology.

fresh : βˆ€ localNode, localNode ∈ (denote spec.topology).vertices β†’ ns localNode βˆ‰ (denote context.topology).vertices

namespaceSubgraphSpec ns spec maps an inserted subgraph into final node IDs.

def namespaceSubgraphSpec (ns : node β†’ node) (spec : SubgraphSpec node) : SubgraphSpec node := { topology := mapGraph ns spec.topology definitions := spec.definitions.image ns entryNodes := spec.entryNodes.image ns exitNodes := spec.exitNodes.image ns }

Namespaced inserted topology vertices remain fresh against the context topology.

theorem namespaceSubgraphSpec_fresh_against_context {isLocalAllowed : node β†’ Prop} {ns : node β†’ node} {context : PlanningContext node} {spec : SubgraphSpec node} (hDiscipline : NamespaceDiscipline isLocalAllowed ns context spec) : βˆ€ mappedNode, mappedNode ∈ (denote (namespaceSubgraphSpec ns spec).topology).vertices β†’ mappedNode βˆ‰ (denote context.topology).vertices := node:Typeinst✝:DecidableEq nodeisLocalAllowed:node β†’ Propns:node β†’ nodecontext:PlanningContext nodespec:SubgraphSpec nodehDiscipline:NamespaceDiscipline isLocalAllowed ns context spec⊒ βˆ€ mappedNode ∈ (denote (namespaceSubgraphSpec ns spec).topology).vertices, mappedNode βˆ‰ (denote context.topology).vertices intro mappedNode node:Typeinst✝:DecidableEq nodeisLocalAllowed:node β†’ Propns:node β†’ nodecontext:PlanningContext nodespec:SubgraphSpec nodehDiscipline:NamespaceDiscipline isLocalAllowed ns context specmappedNode:nodehNode:mappedNode ∈ (denote (namespaceSubgraphSpec ns spec).topology).vertices⊒ mappedNode βˆ‰ (denote context.topology).vertices node:Typeinst✝:DecidableEq nodeisLocalAllowed:node β†’ Propns:node β†’ nodecontext:PlanningContext nodespec:SubgraphSpec nodehDiscipline:NamespaceDiscipline isLocalAllowed ns context specmappedNode:nodehNode:βˆƒ a ∈ (denote spec.topology).vertices, ns a = mappedNode⊒ mappedNode βˆ‰ (denote context.topology).vertices node:Typeinst✝:DecidableEq nodeisLocalAllowed:node β†’ Propns:node β†’ nodecontext:PlanningContext nodespec:SubgraphSpec nodehDiscipline:NamespaceDiscipline isLocalAllowed ns context speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).vertices⊒ ns localNode βˆ‰ (denote context.topology).vertices All goals completed! πŸ™

Namespace discipline exposes the executable local-node syntax predicate.

theorem namespaceSubgraphSpec_local_allowed {isLocalAllowed : node β†’ Prop} {ns : node β†’ node} {context : PlanningContext node} {spec : SubgraphSpec node} (hDiscipline : NamespaceDiscipline isLocalAllowed ns context spec) : βˆ€ localNode, localNode ∈ (denote spec.topology).vertices β†’ isLocalAllowed localNode := hDiscipline.localAllowed

Namespaced graph paths are images of source graph paths.

theorem graphPath_mapGraph_of_graphPath (f : node β†’ node) {g : Graph node} {source target : node} (hPath : GraphPath g source target) : GraphPath (mapGraph f g) (f source) (f target) := node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodesource:nodetarget:nodehPath:GraphPath g source target⊒ GraphPath (mapGraph f g) (f source) (f target) induction hPath with node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodesource:nodetarget:nodea✝:nodeb✝:nodehEdge:(a✝, b✝) ∈ (denote g).edges⊒ GraphPath (mapGraph f g) (f a✝) (f b✝) node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodesource:nodetarget:nodea✝:nodeb✝:nodehEdge:(a✝, b✝) ∈ (denote g).edges⊒ (f a✝, f b✝) ∈ (denote (mapGraph f g)).edges node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodesource:nodetarget:nodea✝:nodeb✝:nodehEdge:(a✝, b✝) ∈ (denote g).edges⊒ βˆƒ a ∈ (denote g).edges, (f a.1, f a.2) = (f a✝, f b✝) All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodesource:nodetarget:nodea✝:nodeb✝:nodec✝:nodeleftPath:GraphPath g a✝ b✝rightPath:GraphPath g b✝ c✝left_ih:GraphPath (mapGraph f g) (f a✝) (f b✝)right_ih:GraphPath (mapGraph f g) (f b✝) (f c✝)⊒ GraphPath (mapGraph f g) (f a✝) (f c✝) All goals completed! πŸ™

Every mapped graph path has a source-level preimage when the mapping is injective.

theorem graphPath_mapGraph_preimage {f : node β†’ node} {g : Graph node} (hInjective : Function.Injective f) {mappedSource mappedTarget : node} (hPath : GraphPath (mapGraph f g) mappedSource mappedTarget) : βˆƒ source target, mappedSource = f source ∧ mappedTarget = f target ∧ GraphPath g source target := node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fmappedSource:nodemappedTarget:nodehPath:GraphPath (mapGraph f g) mappedSource mappedTarget⊒ βˆƒ source target, mappedSource = f source ∧ mappedTarget = f target ∧ GraphPath g source target induction hPath with node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fmappedSource:nodemappedTarget:nodea✝:nodeb✝:nodehEdge:(a✝, b✝) ∈ (denote (mapGraph f g)).edges⊒ βˆƒ source target, a✝ = f source ∧ b✝ = f target ∧ GraphPath g source target node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fmappedSource:nodemappedTarget:nodea✝:nodeb✝:nodehEdge:βˆƒ a ∈ (denote g).edges, (f a.1, f a.2) = (a✝, b✝)⊒ βˆƒ source target, a✝ = f source ∧ b✝ = f target ∧ GraphPath g source target node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fmappedSource:nodemappedTarget:nodea✝:nodeb✝:nodeedge:node Γ— nodehEdge:edge ∈ (denote g).edgeshMapped:(f edge.1, f edge.2) = (a✝, b✝)⊒ βˆƒ source target, a✝ = f source ∧ b✝ = f target ∧ GraphPath g source target node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fmappedSource:nodemappedTarget:nodea✝:nodeb✝:nodesource:nodetarget:nodehEdge:(source, target) ∈ (denote g).edgeshMapped:(f (source, target).1, f (source, target).2) = (a✝, b✝)⊒ βˆƒ source target, a✝ = f source ∧ b✝ = f target ∧ GraphPath g source target node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fmappedSource:nodemappedTarget:nodesource:nodetarget:nodehEdge:(source, target) ∈ (denote g).edges⊒ βˆƒ source_1 target_1, f (source, target).1 = f source_1 ∧ f (source, target).2 = f target_1 ∧ GraphPath g source_1 target_1 All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fmappedSource:nodemappedTarget:nodea✝:nodeb✝:nodec✝:nodeleftPath:GraphPath (mapGraph f g) a✝ b✝rightPath:GraphPath (mapGraph f g) b✝ c✝left_ih:βˆƒ source target, a✝ = f source ∧ b✝ = f target ∧ GraphPath g source targetright_ih:βˆƒ source target, b✝ = f source ∧ c✝ = f target ∧ GraphPath g source target⊒ βˆƒ source target, a✝ = f source ∧ c✝ = f target ∧ GraphPath g source target node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fmappedSource:nodemappedTarget:nodea✝:nodeb✝:nodec✝:nodeleftPath:GraphPath (mapGraph f g) a✝ b✝rightPath:GraphPath (mapGraph f g) b✝ c✝right_ih:βˆƒ source target, b✝ = f source ∧ c✝ = f target ∧ GraphPath g source targetsource:nodemiddleLeft:nodehSource:a✝ = f sourcehMiddleLeft:b✝ = f middleLefthLeftPath:GraphPath g source middleLeft⊒ βˆƒ source target, a✝ = f source ∧ c✝ = f target ∧ GraphPath g source target node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fmappedSource:nodemappedTarget:nodea✝:nodeb✝:nodec✝:nodeleftPath:GraphPath (mapGraph f g) a✝ b✝rightPath:GraphPath (mapGraph f g) b✝ c✝source:nodemiddleLeft:nodehSource:a✝ = f sourcehMiddleLeft:b✝ = f middleLefthLeftPath:GraphPath g source middleLeftmiddleRight:nodetarget:nodehMiddleRight:b✝ = f middleRighthTarget:c✝ = f targethRightPath:GraphPath g middleRight target⊒ βˆƒ source target, a✝ = f source ∧ c✝ = f target ∧ GraphPath g source target have hMiddle : middleLeft = middleRight := node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fmappedSource:nodemappedTarget:nodehPath:GraphPath (mapGraph f g) mappedSource mappedTarget⊒ βˆƒ source target, mappedSource = f source ∧ mappedTarget = f target ∧ GraphPath g source target All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fmappedSource:nodemappedTarget:nodea✝:nodeb✝:nodec✝:nodeleftPath:GraphPath (mapGraph f g) a✝ b✝rightPath:GraphPath (mapGraph f g) b✝ c✝source:nodemiddleLeft:nodehSource:a✝ = f sourcehMiddleLeft:b✝ = f middleLefthLeftPath:GraphPath g source middleLeftmiddleRight:nodetarget:nodehMiddleRight:b✝ = f middleRighthTarget:c✝ = f targethRightPath:GraphPath g middleRight targethMiddle:middleLeft = middleRight⊒ GraphPath g source target node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fmappedSource:nodemappedTarget:nodea✝:nodeb✝:nodec✝:nodeleftPath:GraphPath (mapGraph f g) a✝ b✝rightPath:GraphPath (mapGraph f g) b✝ c✝source:nodemiddleLeft:nodehSource:a✝ = f sourcehMiddleLeft:b✝ = f middleLefthLeftPath:GraphPath g source middleLeftmiddleRight:nodetarget:nodehMiddleRight:b✝ = f middleRighthTarget:c✝ = f targethRightPath:GraphPath g middleLeft targethMiddle:middleLeft = middleRight⊒ GraphPath g source target All goals completed! πŸ™

Injective graph mapping preserves acyclicity.

theorem mapGraph_preserves_acyclic {f : node β†’ node} {g : Graph node} (hInjective : Function.Injective f) (hAcyclic : Acyclic g) : Acyclic (mapGraph f g) := node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fhAcyclic:Acyclic g⊒ Acyclic (mapGraph f g) intro mappedNode node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fhAcyclic:Acyclic gmappedNode:nodehCycle:GraphPath (mapGraph f g) mappedNode mappedNode⊒ False node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fhAcyclic:Acyclic gmappedNode:nodehCycle:GraphPath (mapGraph f g) mappedNode mappedNodesource:nodetarget:nodehSource:mappedNode = f sourcehTarget:mappedNode = f targethPath:GraphPath g source target⊒ False node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fhAcyclic:Acyclic gmappedNode:nodehCycle:GraphPath (mapGraph f g) mappedNode mappedNodesource:nodetarget:nodehSource:mappedNode = f sourcehTarget:mappedNode = f targethPath:GraphPath g source targethSame:source = target⊒ False node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodehInjective:Function.Injective fhAcyclic:Acyclic gmappedNode:nodehCycle:GraphPath (mapGraph f g) mappedNode mappedNodesource:nodetarget:nodehSource:mappedNode = f sourcehTarget:mappedNode = f targethPath:GraphPath g target targethSame:source = target⊒ False All goals completed! πŸ™

Reachability is preserved by graph mapping.

theorem reachableOrSame_mapGraph_of_reachableOrSame (f : node β†’ node) {g : Graph node} {source target : node} (hReachable : ReachableOrSame g source target) : ReachableOrSame (mapGraph f g) (f source) (f target) := node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodesource:nodetarget:nodehReachable:ReachableOrSame g source target⊒ ReachableOrSame (mapGraph f g) (f source) (f target) node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodesource:nodetarget:nodehSame:source = target⊒ ReachableOrSame (mapGraph f g) (f source) (f target)node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodesource:nodetarget:nodehPath:GraphPath g source target⊒ ReachableOrSame (mapGraph f g) (f source) (f target) node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodesource:nodetarget:nodehSame:source = target⊒ ReachableOrSame (mapGraph f g) (f source) (f target) node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodesource:nodetarget:nodehSame:source = target⊒ f source = f target All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodesource:nodetarget:nodehPath:GraphPath g source target⊒ ReachableOrSame (mapGraph f g) (f source) (f target) node:Typeinst✝:DecidableEq nodef:node β†’ nodeg:Graph nodesource:nodetarget:nodehPath:GraphPath g source target⊒ GraphPath (mapGraph f g) (f source) (f target) All goals completed! πŸ™

Namespacing preserves definition-domain coverage for inserted subgraphs.

theorem namespaceSubgraphSpec_preserves_definitionCoverage (ns : node β†’ node) {spec : SubgraphSpec node} (hCoverage : DefinitionCoverage spec.topology spec.definitions) : DefinitionCoverage (namespaceSubgraphSpec ns spec).topology (namespaceSubgraphSpec ns spec).definitions := node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehCoverage:DefinitionCoverage spec.topology spec.definitions⊒ DefinitionCoverage (namespaceSubgraphSpec ns spec).topology (namespaceSubgraphSpec ns spec).definitions node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehCoverage:spec.definitions = (denote spec.topology).vertices⊒ (namespaceSubgraphSpec ns spec).definitions = (denote (namespaceSubgraphSpec ns spec).topology).vertices All goals completed! πŸ™

Namespacing preserves node-inside-topology facts for inserted node sets.

theorem namespaceSubgraphSpec_preserves_nodesInside (ns : node β†’ node) {spec : SubgraphSpec node} {nodes : Finset node} (hInside : NodesInside nodes spec.topology) : NodesInside (nodes.image ns) (namespaceSubgraphSpec ns spec).topology := node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodenodes:Finset nodehInside:NodesInside nodes spec.topology⊒ NodesInside (Finset.image ns nodes) (namespaceSubgraphSpec ns spec).topology intro mappedNode node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodenodes:Finset nodehInside:NodesInside nodes spec.topologymappedNode:nodehMappedNode:mappedNode ∈ Finset.image ns nodes⊒ mappedNode ∈ (denote (namespaceSubgraphSpec ns spec).topology).vertices node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodenodes:Finset nodehInside:NodesInside nodes spec.topologymappedNode:nodehMappedNode:βˆƒ a ∈ nodes, ns a = mappedNode⊒ βˆƒ a ∈ (denote spec.topology).vertices, ns a = mappedNode node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodenodes:Finset nodehInside:NodesInside nodes spec.topologylocalNode:nodehLocalNode:localNode ∈ nodes⊒ βˆƒ a ∈ (denote spec.topology).vertices, ns a = ns localNode All goals completed! πŸ™

Namespacing preserves orphan-freedom for inserted subgraphs.

theorem namespaceSubgraphSpec_preserves_orphanFree (ns : node β†’ node) {spec : SubgraphSpec node} (hOrphanFree : OrphanFree spec) : OrphanFree (namespaceSubgraphSpec ns spec) := node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree spec⊒ OrphanFree (namespaceSubgraphSpec ns spec) intro mappedNode node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree specmappedNode:nodehMappedNode:mappedNode ∈ (denote (namespaceSubgraphSpec ns spec).topology).vertices⊒ (βˆƒ entry ∈ (namespaceSubgraphSpec ns spec).entryNodes, ReachableOrSame (namespaceSubgraphSpec ns spec).topology entry mappedNode) ∧ βˆƒ exit ∈ (namespaceSubgraphSpec ns spec).exitNodes, ReachableOrSame (namespaceSubgraphSpec ns spec).topology mappedNode exit node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree specmappedNode:nodehMappedNode:βˆƒ a ∈ (denote spec.topology).vertices, ns a = mappedNode⊒ (βˆƒ entry ∈ (namespaceSubgraphSpec ns spec).entryNodes, ReachableOrSame (namespaceSubgraphSpec ns spec).topology entry mappedNode) ∧ βˆƒ exit ∈ (namespaceSubgraphSpec ns spec).exitNodes, ReachableOrSame (namespaceSubgraphSpec ns spec).topology mappedNode exit node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).vertices⊒ (βˆƒ entry ∈ (namespaceSubgraphSpec ns spec).entryNodes, ReachableOrSame (namespaceSubgraphSpec ns spec).topology entry (ns localNode)) ∧ βˆƒ exit ∈ (namespaceSubgraphSpec ns spec).exitNodes, ReachableOrSame (namespaceSubgraphSpec ns spec).topology (ns localNode) exit node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).verticesentry:nodehEntry:entry ∈ spec.entryNodeshEntryReachable:ReachableOrSame spec.topology entry localNodeexit:nodehExit:exit ∈ spec.exitNodeshExitReachable:ReachableOrSame spec.topology localNode exit⊒ (βˆƒ entry ∈ (namespaceSubgraphSpec ns spec).entryNodes, ReachableOrSame (namespaceSubgraphSpec ns spec).topology entry (ns localNode)) ∧ βˆƒ exit ∈ (namespaceSubgraphSpec ns spec).exitNodes, ReachableOrSame (namespaceSubgraphSpec ns spec).topology (ns localNode) exit node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).verticesentry:nodehEntry:entry ∈ spec.entryNodeshEntryReachable:ReachableOrSame spec.topology entry localNodeexit:nodehExit:exit ∈ spec.exitNodeshExitReachable:ReachableOrSame spec.topology localNode exit⊒ βˆƒ entry ∈ (namespaceSubgraphSpec ns spec).entryNodes, ReachableOrSame (namespaceSubgraphSpec ns spec).topology entry (ns localNode)node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).verticesentry:nodehEntry:entry ∈ spec.entryNodeshEntryReachable:ReachableOrSame spec.topology entry localNodeexit:nodehExit:exit ∈ spec.exitNodeshExitReachable:ReachableOrSame spec.topology localNode exit⊒ βˆƒ exit ∈ (namespaceSubgraphSpec ns spec).exitNodes, ReachableOrSame (namespaceSubgraphSpec ns spec).topology (ns localNode) exit node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).verticesentry:nodehEntry:entry ∈ spec.entryNodeshEntryReachable:ReachableOrSame spec.topology entry localNodeexit:nodehExit:exit ∈ spec.exitNodeshExitReachable:ReachableOrSame spec.topology localNode exit⊒ βˆƒ entry ∈ (namespaceSubgraphSpec ns spec).entryNodes, ReachableOrSame (namespaceSubgraphSpec ns spec).topology entry (ns localNode) node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).verticesentry:nodehEntry:entry ∈ spec.entryNodeshEntryReachable:ReachableOrSame spec.topology entry localNodeexit:nodehExit:exit ∈ spec.exitNodeshExitReachable:ReachableOrSame spec.topology localNode exit⊒ ns entry ∈ (namespaceSubgraphSpec ns spec).entryNodesnode:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).verticesentry:nodehEntry:entry ∈ spec.entryNodeshEntryReachable:ReachableOrSame spec.topology entry localNodeexit:nodehExit:exit ∈ spec.exitNodeshExitReachable:ReachableOrSame spec.topology localNode exit⊒ ReachableOrSame (namespaceSubgraphSpec ns spec).topology (ns entry) (ns localNode) node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).verticesentry:nodehEntry:entry ∈ spec.entryNodeshEntryReachable:ReachableOrSame spec.topology entry localNodeexit:nodehExit:exit ∈ spec.exitNodeshExitReachable:ReachableOrSame spec.topology localNode exit⊒ ns entry ∈ (namespaceSubgraphSpec ns spec).entryNodes All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).verticesentry:nodehEntry:entry ∈ spec.entryNodeshEntryReachable:ReachableOrSame spec.topology entry localNodeexit:nodehExit:exit ∈ spec.exitNodeshExitReachable:ReachableOrSame spec.topology localNode exit⊒ ReachableOrSame (namespaceSubgraphSpec ns spec).topology (ns entry) (ns localNode) All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).verticesentry:nodehEntry:entry ∈ spec.entryNodeshEntryReachable:ReachableOrSame spec.topology entry localNodeexit:nodehExit:exit ∈ spec.exitNodeshExitReachable:ReachableOrSame spec.topology localNode exit⊒ βˆƒ exit ∈ (namespaceSubgraphSpec ns spec).exitNodes, ReachableOrSame (namespaceSubgraphSpec ns spec).topology (ns localNode) exit node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).verticesentry:nodehEntry:entry ∈ spec.entryNodeshEntryReachable:ReachableOrSame spec.topology entry localNodeexit:nodehExit:exit ∈ spec.exitNodeshExitReachable:ReachableOrSame spec.topology localNode exit⊒ ns exit ∈ (namespaceSubgraphSpec ns spec).exitNodesnode:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).verticesentry:nodehEntry:entry ∈ spec.entryNodeshEntryReachable:ReachableOrSame spec.topology entry localNodeexit:nodehExit:exit ∈ spec.exitNodeshExitReachable:ReachableOrSame spec.topology localNode exit⊒ ReachableOrSame (namespaceSubgraphSpec ns spec).topology (ns localNode) (ns exit) node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).verticesentry:nodehEntry:entry ∈ spec.entryNodeshEntryReachable:ReachableOrSame spec.topology entry localNodeexit:nodehExit:exit ∈ spec.exitNodeshExitReachable:ReachableOrSame spec.topology localNode exit⊒ ns exit ∈ (namespaceSubgraphSpec ns spec).exitNodes All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodens:node β†’ nodespec:SubgraphSpec nodehOrphanFree:OrphanFree speclocalNode:nodehLocalNode:localNode ∈ (denote spec.topology).verticesentry:nodehEntry:entry ∈ spec.entryNodeshEntryReachable:ReachableOrSame spec.topology entry localNodeexit:nodehExit:exit ∈ spec.exitNodeshExitReachable:ReachableOrSame spec.topology localNode exit⊒ ReachableOrSame (namespaceSubgraphSpec ns spec).topology (ns localNode) (ns exit) All goals completed! πŸ™

Namespacing preserves the runtime inserted-subgraph validity bundle.

theorem namespaceSubgraphSpec_preserves_valid {ns : node β†’ node} {spec : SubgraphSpec node} (hInjective : Function.Injective ns) (hValid : spec.Valid) : (namespaceSubgraphSpec ns spec).Valid := { acyclic := mapGraph_preserves_acyclic hInjective hValid.acyclic definitionsCover := namespaceSubgraphSpec_preserves_definitionCoverage ns hValid.definitionsCover entryNodesNonempty := Finset.Nonempty.image hValid.entryNodesNonempty ns exitNodesNonempty := Finset.Nonempty.image hValid.exitNodesNonempty ns entryNodesInside := namespaceSubgraphSpec_preserves_nodesInside ns hValid.entryNodesInside exitNodesInside := namespaceSubgraphSpec_preserves_nodesInside ns hValid.exitNodesInside orphanFree := namespaceSubgraphSpec_preserves_orphanFree ns hValid.orphanFree }

namespaceGraphRewrite ns rewrite maps only the inserted subgraph.

The rewrite anchor already lives in the current topology namespace, matching the executable Haskell planner.

def namespaceGraphRewrite (ns : node β†’ node) (rewrite : GraphRewrite node) : GraphRewrite node := match rewrite with | GraphRewrite.expandNode anchor mode spec => GraphRewrite.expandNode anchor mode (namespaceSubgraphSpec ns spec) | GraphRewrite.appendAfter anchor spec => GraphRewrite.appendAfter anchor (namespaceSubgraphSpec ns spec)

Namespacing does not change the rewrite anchor.

theorem namespaceGraphRewrite_anchor (ns : node β†’ node) (rewrite : GraphRewrite node) : (namespaceGraphRewrite ns rewrite).anchor = rewrite.anchor := node:Typeinst✝:DecidableEq nodens:node β†’ noderewrite:GraphRewrite node⊒ (namespaceGraphRewrite ns rewrite).anchor = rewrite.anchor node:Typeinst✝:DecidableEq nodens:node β†’ nodea✝²:nodea✝¹:ExpansionModea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.expandNode a✝² a✝¹ a✝)).anchor = (GraphRewrite.expandNode a✝² a✝¹ a✝).anchornode:Typeinst✝:DecidableEq nodens:node β†’ nodea✝¹:nodea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.appendAfter a✝¹ a✝)).anchor = (GraphRewrite.appendAfter a✝¹ a✝).anchor node:Typeinst✝:DecidableEq nodens:node β†’ nodea✝²:nodea✝¹:ExpansionModea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.expandNode a✝² a✝¹ a✝)).anchor = (GraphRewrite.expandNode a✝² a✝¹ a✝).anchornode:Typeinst✝:DecidableEq nodens:node β†’ nodea✝¹:nodea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.appendAfter a✝¹ a✝)).anchor = (GraphRewrite.appendAfter a✝¹ a✝).anchor All goals completed! πŸ™

Namespacing does not change whether the anchor is removed or retained.

theorem namespaceGraphRewrite_anchorDisposition (ns : node β†’ node) (rewrite : GraphRewrite node) : (namespaceGraphRewrite ns rewrite).anchorDisposition = rewrite.anchorDisposition := node:Typeinst✝:DecidableEq nodens:node β†’ noderewrite:GraphRewrite node⊒ (namespaceGraphRewrite ns rewrite).anchorDisposition = rewrite.anchorDisposition cases rewrite with node:Typeinst✝:DecidableEq nodens:node β†’ nodea✝¹:nodemode:ExpansionModea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.expandNode a✝¹ mode a✝)).anchorDisposition = (GraphRewrite.expandNode a✝¹ mode a✝).anchorDisposition node:Typeinst✝:DecidableEq nodens:node β†’ nodea✝¹:nodea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.expandNode a✝¹ ExpansionMode.replaceNode a✝)).anchorDisposition = (GraphRewrite.expandNode a✝¹ ExpansionMode.replaceNode a✝).anchorDispositionnode:Typeinst✝:DecidableEq nodens:node β†’ nodea✝¹:nodea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.expandNode a✝¹ ExpansionMode.retainNodeAsEnvelope a✝)).anchorDisposition = (GraphRewrite.expandNode a✝¹ ExpansionMode.retainNodeAsEnvelope a✝).anchorDisposition node:Typeinst✝:DecidableEq nodens:node β†’ nodea✝¹:nodea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.expandNode a✝¹ ExpansionMode.replaceNode a✝)).anchorDisposition = (GraphRewrite.expandNode a✝¹ ExpansionMode.replaceNode a✝).anchorDispositionnode:Typeinst✝:DecidableEq nodens:node β†’ nodea✝¹:nodea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.expandNode a✝¹ ExpansionMode.retainNodeAsEnvelope a✝)).anchorDisposition = (GraphRewrite.expandNode a✝¹ ExpansionMode.retainNodeAsEnvelope a✝).anchorDisposition All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodens:node β†’ nodea✝¹:nodea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.appendAfter a✝¹ a✝)).anchorDisposition = (GraphRewrite.appendAfter a✝¹ a✝).anchorDisposition All goals completed! πŸ™

Namespacing maps the inserted rewrite spec and leaves the rewrite form unchanged.

theorem namespaceGraphRewrite_spec (ns : node β†’ node) (rewrite : GraphRewrite node) : (namespaceGraphRewrite ns rewrite).spec = namespaceSubgraphSpec ns rewrite.spec := node:Typeinst✝:DecidableEq nodens:node β†’ noderewrite:GraphRewrite node⊒ (namespaceGraphRewrite ns rewrite).spec = namespaceSubgraphSpec ns rewrite.spec node:Typeinst✝:DecidableEq nodens:node β†’ nodea✝²:nodea✝¹:ExpansionModea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.expandNode a✝² a✝¹ a✝)).spec = namespaceSubgraphSpec ns (GraphRewrite.expandNode a✝² a✝¹ a✝).specnode:Typeinst✝:DecidableEq nodens:node β†’ nodea✝¹:nodea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.appendAfter a✝¹ a✝)).spec = namespaceSubgraphSpec ns (GraphRewrite.appendAfter a✝¹ a✝).spec node:Typeinst✝:DecidableEq nodens:node β†’ nodea✝²:nodea✝¹:ExpansionModea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.expandNode a✝² a✝¹ a✝)).spec = namespaceSubgraphSpec ns (GraphRewrite.expandNode a✝² a✝¹ a✝).specnode:Typeinst✝:DecidableEq nodens:node β†’ nodea✝¹:nodea✝:SubgraphSpec node⊒ (namespaceGraphRewrite ns (GraphRewrite.appendAfter a✝¹ a✝)).spec = namespaceSubgraphSpec ns (GraphRewrite.appendAfter a✝¹ a✝).spec All goals completed! πŸ™

runtimePlannerRewrite policy rewrite is the rewrite after runtime namespacing.

def runtimePlannerRewrite (policy : RuntimeNamespacePolicy node) (rewrite : GraphRewrite node) : GraphRewrite node := namespaceGraphRewrite (policy.namespaceNode rewrite.anchor) rewriteend Namespacing

Runtime List Boundaries

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

A runtime list and proof-side Finset describe the same node boundary.

The Haskell planner computes frontier-delta cost from duplicate-free entry lists. Lean uses Finset boundaries, so this predicate records the duplicate-free list bridge explicitly.

def RuntimeNodeListMatches (values : List node) (nodes : Finset node) : Prop := values.Nodup ∧ values.toFinset = nodes

Duplicate-free runtime lists have the same length as their proof-side node set cardinality.

theorem RuntimeNodeListMatches.card_eq_length {values : List node} {nodes : Finset node} (hMatches : RuntimeNodeListMatches values nodes) : nodes.card = values.length := node:Typeinst✝:DecidableEq nodevalues:List nodenodes:Finset nodehMatches:RuntimeNodeListMatches values nodes⊒ nodes.card = values.length node:Typeinst✝:DecidableEq nodevalues:List nodenodes:Finset nodehNodup:values.NoduphToFinset:values.toFinset = nodes⊒ nodes.card = values.length node:Typeinst✝:DecidableEq nodevalues:List nodenodes:Finset nodehNodup:values.NoduphToFinset:values.toFinset = nodes⊒ values.toFinset.card = values.length All goals completed! πŸ™end RuntimeLists

Planner Construction Bridge

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

Runtime anchor fields agree with the namespaced rewrite and final topology.

The absence/presence fields are explicit construction obligations: this module does not derive them from the topology equation. The executable planner is responsible for producing a final topology whose anchor membership agrees with the rewrite disposition.

structure RuntimeAnchorMatches (policy : RuntimeNamespacePolicy node) (rawRewrite : GraphRewrite node) (delta : PlannedRewriteDelta node) : Prop where

The delta records the raw rewrite anchor.

anchorNode_eq : delta.anchorNode = rawRewrite.anchor

The delta records the rewrite-form anchor disposition.

anchorDisposition_eq : delta.anchorDisposition = (runtimePlannerRewrite policy rawRewrite).anchorDisposition

Runtime construction obligation: removed anchors are absent from the final topology.

removed_absent : delta.anchorDisposition = RewriteAnchorDisposition.removed β†’ (runtimePlannerRewrite policy rawRewrite).anchor βˆ‰ (denote delta.topology).vertices

Runtime construction obligation: retained anchors remain in the final topology.

retained_present : delta.anchorDisposition = RewriteAnchorDisposition.retained β†’ (runtimePlannerRewrite policy rawRewrite).anchor ∈ (denote delta.topology).vertices

Runtime topology and definition fields agree with the relation-level planner model.

structure RuntimeDeltaMatches (policy : RuntimeNamespacePolicy node) (context : PlanningContext node) (rawRewrite : GraphRewrite node) (delta : PlannedRewriteDelta node) : Prop where

The planned final topology follows the relation-level planner construction.

topology_eq : denote delta.topology = plannedFinalRelation context.topology (runtimePlannerRewrite policy rawRewrite)

Delta entry nodes are the namespaced inserted entry nodes.

entryNodes_eq : delta.entryNodes = (runtimePlannerRewrite policy rawRewrite).spec.entryNodes

Delta exit nodes are the namespaced inserted exit nodes.

exitNodes_eq : delta.exitNodes = (runtimePlannerRewrite policy rawRewrite).spec.exitNodes

Delta new nodes are computed from the relation diff.

newNodes_eq : delta.newNodes = relationAddedNodes (denote context.topology) (denote delta.topology)

Delta removed nodes are computed from the relation diff.

removedNodes_eq : delta.removedNodes = relationRemovedNodes (denote context.topology) (denote delta.topology)

Delta added edges are computed from the relation diff.

addedEdges_eq : delta.addedEdges = relationAddedEdges (denote context.topology) (denote delta.topology)

Final definitions follow the runtime delete-or-retain formula.

definitions_eq : delta.definitions = plannedFinalDefinitions context (runtimePlannerRewrite policy rawRewrite)

Runtime structural cost fields agree with computed rewrite-delta data.

structure RuntimeCostMatches (policy : RuntimeNamespacePolicy node) (rawRewrite : GraphRewrite node) (delta : PlannedRewriteDelta node) : Prop where

Added-node cost equals the computed new-node count.

addedNodes_eq : delta.cost.addedNodes = delta.newNodes.card

Added-edge cost equals the computed added-edge count.

addedEdges_eq : delta.cost.addedEdges = delta.addedEdges.card

Added-depth cost follows the inserted longest-path computation.

addedDepth_eq : βˆƒ insertedDepth, LongestInsertedPathNodeCount (runtimePlannerRewrite policy rawRewrite).spec insertedDepth ∧ delta.cost.addedDepth = match delta.anchorDisposition with | RewriteAnchorDisposition.removed => insertedDepth - 1 | RewriteAnchorDisposition.retained => insertedDepth

Entry nodes match the duplicate-free runtime list used for frontier-delta cost.

entryNodes_runtimeList : βˆƒ entryList, RuntimeNodeListMatches entryList delta.entryNodes ∧ delta.cost.frontierDelta = entryList.length - 1

Each accepted graph rewrite consumes one rewrite-operation unit.

rewriteOps_eq : delta.cost.rewriteOps = 1

RuntimePlannerConstruction is the proof-shaped output of executable planning.

It starts from the raw rewrite accepted by the runtime, records the namespacing discipline that turns the raw inserted subgraph into the final node namespace, and carries constructor equations for the planned delta. The bridge below derives PlanGraphRewriteChecks; those checks are not restated as fields here.

structure RuntimePlannerConstruction (policy : RuntimeNamespacePolicy node) (context : PlanningContext node) (rawRewrite : GraphRewrite node) (delta : PlannedRewriteDelta node) : Prop where

The runtime namespace validator accepted the raw inserted subgraph.

namespaceDiscipline : NamespaceDiscipline policy.localAllowed (policy.namespaceNode rawRewrite.anchor) context rawRewrite.spec

The raw anchor exists in the current topology.

anchorInTopology : rawRewrite.anchor ∈ (denote context.topology).vertices

The raw anchor has a current stage definition.

anchorHasDefinition : rawRewrite.anchor ∈ context.definitions

The raw inserted subgraph passed runtime subgraph validation.

rawSubgraphValid : rawRewrite.spec.Valid

Anchor identity and disposition agree with the namespaced rewrite.

anchorMatches : RuntimeAnchorMatches policy rawRewrite delta

Delta topology and definitions agree with the relation-level planner model.

deltaMatches : RuntimeDeltaMatches policy context rawRewrite delta

Structural cost agrees with computed delta data and runtime boundary lists.

costMatches : RuntimeCostMatches policy rawRewrite delta

Final definitions exactly cover final topology vertices.

finalDefinitionsCover : DefinitionCoverage delta.topology delta.definitions

Final topology passed runtime DAG validation.

finalAcyclic : Acyclic delta.topology

Existing vertices remain after adding edges to a relation.

theorem relationVertices_subset_addEdgesToRelation (relation : Relation node) (edges : Finset (node Γ— node)) : relation.vertices βŠ† (addEdgesToRelation relation edges).vertices := node:Typeinst✝:DecidableEq noderelation:Relation nodeedges:Finset (node Γ— node)⊒ relation.vertices βŠ† (addEdgesToRelation relation edges).vertices intro vertex node:Typeinst✝:DecidableEq noderelation:Relation nodeedges:Finset (node Γ— node)vertex:nodehVertex:vertex ∈ relation.vertices⊒ vertex ∈ (addEdgesToRelation relation edges).vertices node:Typeinst✝:DecidableEq noderelation:Relation nodeedges:Finset (node Γ— node)vertex:nodehVertex:vertex ∈ relation.vertices⊒ (vertex ∈ relation.vertices ∨ vertex ∈ Finset.image Prod.fst edges) ∨ vertex ∈ Finset.image Prod.snd edges All goals completed! πŸ™

Existing edges remain after adding edges to a relation.

theorem relationEdges_subset_addEdgesToRelation (relation : Relation node) (edges : Finset (node Γ— node)) : relation.edges βŠ† (addEdgesToRelation relation edges).edges := node:Typeinst✝:DecidableEq noderelation:Relation nodeedges:Finset (node Γ— node)⊒ relation.edges βŠ† (addEdgesToRelation relation edges).edges intro edge node:Typeinst✝:DecidableEq noderelation:Relation nodeedges:Finset (node Γ— node)edge:node Γ— nodehEdge:edge ∈ relation.edges⊒ edge ∈ (addEdgesToRelation relation edges).edges node:Typeinst✝:DecidableEq noderelation:Relation nodeedges:Finset (node Γ— node)edge:node Γ— nodehEdge:edge ∈ relation.edges⊒ edge ∈ relation.edges ∨ edge ∈ edges All goals completed! πŸ™

Right-overlay vertices are present in the overlay.

theorem relationVertices_right_subset_overlay (left right : Relation node) : right.vertices βŠ† (Relation.overlay left right).vertices := node:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation node⊒ right.vertices βŠ† (left.overlay right).vertices intro vertex node:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodevertex:nodehVertex:vertex ∈ right.vertices⊒ vertex ∈ (left.overlay right).vertices node:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodevertex:nodehVertex:vertex ∈ right.vertices⊒ vertex ∈ left.vertices ∨ vertex ∈ right.vertices All goals completed! πŸ™

Right-overlay edges are present in the overlay.

theorem relationEdges_right_subset_overlay (left right : Relation node) : right.edges βŠ† (Relation.overlay left right).edges := node:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation node⊒ right.edges βŠ† (left.overlay right).edges intro edge node:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodeedge:node Γ— nodehEdge:edge ∈ right.edges⊒ edge ∈ (left.overlay right).edges node:Typeinst✝:DecidableEq nodeleft:Relation noderight:Relation nodeedge:node Γ— nodehEdge:edge ∈ right.edges⊒ edge ∈ left.edges ∨ edge ∈ right.edges All goals completed! πŸ™

Inserted-subgraph vertices are present in the relation-level planned final topology.

theorem insertedVertices_subset_plannedFinalRelation (context : Graph node) (rewrite : GraphRewrite node) : (denote rewrite.spec.topology).vertices βŠ† (plannedFinalRelation context rewrite).vertices := node:Typeinst✝:DecidableEq nodecontext:Graph noderewrite:GraphRewrite node⊒ (denote rewrite.spec.topology).vertices βŠ† (plannedFinalRelation context rewrite).vertices intro vertex node:Typeinst✝:DecidableEq nodecontext:Graph noderewrite:GraphRewrite nodevertex:nodehVertex:vertex ∈ (denote rewrite.spec.topology).vertices⊒ vertex ∈ (plannedFinalRelation context rewrite).vertices node:Typeinst✝:DecidableEq nodecontext:Graph noderewrite:GraphRewrite nodevertex:nodehVertex:vertex ∈ (denote rewrite.spec.topology).vertices⊒ vertex ∈ (addEdgesToRelation (addEdgesToRelation ((match rewrite with | GraphRewrite.expandNode _anchor ExpansionMode.replaceNode _spec => removeVertexFromRelation (denote context) rewrite.anchor | GraphRewrite.expandNode _anchor ExpansionMode.retainNodeAsEnvelope _spec => removeOutgoingFromRelation (denote context) rewrite.anchor | GraphRewrite.appendAfter _anchor _spec => removeOutgoingFromRelation (denote context) rewrite.anchor).overlay (denote rewrite.spec.topology)) ((match rewrite.anchorDisposition with | RewriteAnchorDisposition.removed => predecessorsOf (denote context) rewrite.anchor | RewriteAnchorDisposition.retained => {rewrite.anchor}) Γ—Λ’ rewrite.spec.entryNodes)) (rewrite.spec.exitNodes Γ—Λ’ successorsOf (denote context) rewrite.anchor)).vertices All goals completed! πŸ™

Inserted-subgraph edges are present in the relation-level planned final topology.

theorem insertedEdges_subset_plannedFinalRelation (context : Graph node) (rewrite : GraphRewrite node) : (denote rewrite.spec.topology).edges βŠ† (plannedFinalRelation context rewrite).edges := node:Typeinst✝:DecidableEq nodecontext:Graph noderewrite:GraphRewrite node⊒ (denote rewrite.spec.topology).edges βŠ† (plannedFinalRelation context rewrite).edges intro edge node:Typeinst✝:DecidableEq nodecontext:Graph noderewrite:GraphRewrite nodeedge:node Γ— nodehEdge:edge ∈ (denote rewrite.spec.topology).edges⊒ edge ∈ (plannedFinalRelation context rewrite).edges node:Typeinst✝:DecidableEq nodecontext:Graph noderewrite:GraphRewrite nodeedge:node Γ— nodehEdge:edge ∈ (denote rewrite.spec.topology).edges⊒ edge ∈ (addEdgesToRelation (addEdgesToRelation ((match rewrite with | GraphRewrite.expandNode _anchor ExpansionMode.replaceNode _spec => removeVertexFromRelation (denote context) rewrite.anchor | GraphRewrite.expandNode _anchor ExpansionMode.retainNodeAsEnvelope _spec => removeOutgoingFromRelation (denote context) rewrite.anchor | GraphRewrite.appendAfter _anchor _spec => removeOutgoingFromRelation (denote context) rewrite.anchor).overlay (denote rewrite.spec.topology)) ((match rewrite.anchorDisposition with | RewriteAnchorDisposition.removed => predecessorsOf (denote context) rewrite.anchor | RewriteAnchorDisposition.retained => {rewrite.anchor}) Γ—Λ’ rewrite.spec.entryNodes)) (rewrite.spec.exitNodes Γ—Λ’ successorsOf (denote context) rewrite.anchor)).edges All goals completed! πŸ™

A topology construction equation proves the inserted subgraph is present in the final graph.

theorem subgraphContainedInFinal_of_topology_eq {context : PlanningContext node} {rewrite : GraphRewrite node} {delta : PlannedRewriteDelta node} (hTopology : denote delta.topology = plannedFinalRelation context.topology rewrite) : SubgraphContainedInFinal rewrite delta := node:Typeinst✝:DecidableEq nodecontext:PlanningContext noderewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehTopology:denote delta.topology = plannedFinalRelation context.topology rewrite⊒ SubgraphContainedInFinal rewrite delta node:Typeinst✝:DecidableEq nodecontext:PlanningContext noderewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehTopology:denote delta.topology = plannedFinalRelation context.topology rewrite⊒ βˆ€ node_1 ∈ (denote rewrite.spec.topology).vertices, node_1 ∈ (denote delta.topology).verticesnode:Typeinst✝:DecidableEq nodecontext:PlanningContext noderewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehTopology:denote delta.topology = plannedFinalRelation context.topology rewrite⊒ βˆ€ edge ∈ (denote rewrite.spec.topology).edges, edge ∈ (denote delta.topology).edges node:Typeinst✝:DecidableEq nodecontext:PlanningContext noderewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehTopology:denote delta.topology = plannedFinalRelation context.topology rewrite⊒ βˆ€ node_1 ∈ (denote rewrite.spec.topology).vertices, node_1 ∈ (denote delta.topology).vertices intro vertex node:Typeinst✝:DecidableEq nodecontext:PlanningContext noderewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehTopology:denote delta.topology = plannedFinalRelation context.topology rewritevertex:nodehVertex:vertex ∈ (denote rewrite.spec.topology).vertices⊒ vertex ∈ (denote delta.topology).vertices node:Typeinst✝:DecidableEq nodecontext:PlanningContext noderewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehTopology:denote delta.topology = plannedFinalRelation context.topology rewritevertex:nodehVertex:vertex ∈ (denote rewrite.spec.topology).vertices⊒ vertex ∈ (plannedFinalRelation context.topology rewrite).vertices All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodecontext:PlanningContext noderewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehTopology:denote delta.topology = plannedFinalRelation context.topology rewrite⊒ βˆ€ edge ∈ (denote rewrite.spec.topology).edges, edge ∈ (denote delta.topology).edges intro edge node:Typeinst✝:DecidableEq nodecontext:PlanningContext noderewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehTopology:denote delta.topology = plannedFinalRelation context.topology rewriteedge:node Γ— nodehEdge:edge ∈ (denote rewrite.spec.topology).edges⊒ edge ∈ (denote delta.topology).edges node:Typeinst✝:DecidableEq nodecontext:PlanningContext noderewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehTopology:denote delta.topology = plannedFinalRelation context.topology rewriteedge:node Γ— nodehEdge:edge ∈ (denote rewrite.spec.topology).edges⊒ edge ∈ (plannedFinalRelation context.topology rewrite).edges All goals completed! πŸ™

Runtime construction exposes the local-node syntax acceptance checked before namespacing.

theorem runtimePlannerConstruction_local_allowed {policy : RuntimeNamespacePolicy node} {context : PlanningContext node} {rawRewrite : GraphRewrite node} {delta : PlannedRewriteDelta node} (hConstruction : RuntimePlannerConstruction policy context rawRewrite delta) : βˆ€ localNode, localNode ∈ (denote rawRewrite.spec.topology).vertices β†’ policy.localAllowed localNode := namespaceSubgraphSpec_local_allowed hConstruction.namespaceDiscipline

Runtime construction exposes freshness of namespaced inserted nodes.

theorem runtimePlannerConstruction_namespaced_fresh {policy : RuntimeNamespacePolicy node} {context : PlanningContext node} {rawRewrite : GraphRewrite node} {delta : PlannedRewriteDelta node} (hConstruction : RuntimePlannerConstruction policy context rawRewrite delta) : βˆ€ mappedNode, mappedNode ∈ (denote (runtimePlannerRewrite policy rawRewrite).spec.topology).vertices β†’ mappedNode βˆ‰ (denote context.topology).vertices := node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehConstruction:RuntimePlannerConstruction policy context rawRewrite delta⊒ βˆ€ mappedNode ∈ (denote (runtimePlannerRewrite policy rawRewrite).spec.topology).vertices, mappedNode βˆ‰ (denote context.topology).vertices node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehConstruction:RuntimePlannerConstruction policy context rawRewrite delta⊒ βˆ€ mappedNode ∈ (denote (namespaceSubgraphSpec (policy.namespaceNode rawRewrite.anchor) rawRewrite.spec).topology).vertices, mappedNode βˆ‰ (denote context.topology).vertices All goals completed! πŸ™

Executable planner construction fields establish the admission planning contract.

theorem runtimePlannerConstruction_planGraphRewriteChecks {policy : RuntimeNamespacePolicy node} {context : PlanningContext node} {rawRewrite : GraphRewrite node} {delta : PlannedRewriteDelta node} (hConstruction : RuntimePlannerConstruction policy context rawRewrite delta) : PlanGraphRewriteChecks context (runtimePlannerRewrite policy rawRewrite) delta := node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehConstruction:RuntimePlannerConstruction policy context rawRewrite delta⊒ PlanGraphRewriteChecks context (runtimePlannerRewrite policy rawRewrite) delta have hAnchor : rawRewrite.anchor = (runtimePlannerRewrite policy rawRewrite).anchor := node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehConstruction:RuntimePlannerConstruction policy context rawRewrite delta⊒ PlanGraphRewriteChecks context (runtimePlannerRewrite policy rawRewrite) delta All goals completed! πŸ™ have hSubgraphValid : (runtimePlannerRewrite policy rawRewrite).spec.Valid := node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehConstruction:RuntimePlannerConstruction policy context rawRewrite delta⊒ PlanGraphRewriteChecks context (runtimePlannerRewrite policy rawRewrite) delta node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehConstruction:RuntimePlannerConstruction policy context rawRewrite deltahAnchor:rawRewrite.anchor = (runtimePlannerRewrite policy rawRewrite).anchor⊒ (namespaceSubgraphSpec (policy.namespaceNode rawRewrite.anchor) rawRewrite.spec).Valid All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehConstruction:RuntimePlannerConstruction policy context rawRewrite deltahAnchor:rawRewrite.anchor = (runtimePlannerRewrite policy rawRewrite).anchorhSubgraphValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidentryList:List nodehEntryMatches:RuntimeNodeListMatches entryList delta.entryNodeshFrontierDelta:delta.cost.frontierDelta = entryList.length - 1⊒ PlanGraphRewriteChecks context (runtimePlannerRewrite policy rawRewrite) delta node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehConstruction:RuntimePlannerConstruction policy context rawRewrite deltahAnchor:rawRewrite.anchor = (runtimePlannerRewrite policy rawRewrite).anchorhSubgraphValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidentryList:List nodehEntryMatches:RuntimeNodeListMatches entryList delta.entryNodeshFrontierDelta:delta.cost.frontierDelta = entryList.length - 1hEntryCard:delta.entryNodes.card = entryList.length⊒ PlanGraphRewriteChecks context (runtimePlannerRewrite policy rawRewrite) delta refine { anchorMatches := hConstruction.anchorMatches.anchorNode_eq.trans hAnchor anchorInTopology := ?_ anchorHasDefinition := ?_ subgraphValid := hSubgraphValid topologyMatches := hConstruction.deltaMatches.topology_eq subgraphContained := subgraphContainedInFinal_of_topology_eq hConstruction.deltaMatches.topology_eq entryExitMatches := { entryNodes_eq := hConstruction.deltaMatches.entryNodes_eq exitNodes_eq := hConstruction.deltaMatches.exitNodes_eq } anchorDispositionMatches := { disposition_eq := hConstruction.anchorMatches.anchorDisposition_eq removed_absent := hConstruction.anchorMatches.removed_absent retained_present := hConstruction.anchorMatches.retained_present } topologyDiffMatches := { newNodes_eq := hConstruction.deltaMatches.newNodes_eq removedNodes_eq := hConstruction.deltaMatches.removedNodes_eq addedEdges_eq := hConstruction.deltaMatches.addedEdges_eq } costMatches := { addedNodes_eq := hConstruction.costMatches.addedNodes_eq addedEdges_eq := hConstruction.costMatches.addedEdges_eq addedDepth_eq := hConstruction.costMatches.addedDepth_eq frontierDelta_eq := node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehConstruction:RuntimePlannerConstruction policy context rawRewrite deltahAnchor:rawRewrite.anchor = (runtimePlannerRewrite policy rawRewrite).anchorhSubgraphValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidentryList:List nodehEntryMatches:RuntimeNodeListMatches entryList delta.entryNodeshFrontierDelta:delta.cost.frontierDelta = entryList.length - 1hEntryCard:delta.entryNodes.card = entryList.length⊒ delta.cost.frontierDelta = delta.entryNodes.card - 1 All goals completed! πŸ™ rewriteOps_eq := hConstruction.costMatches.rewriteOps_eq } definitionUpdateMatches := { definitions_eq := hConstruction.deltaMatches.definitions_eq } finalDefinitionsCover := hConstruction.finalDefinitionsCover finalAcyclic := hConstruction.finalAcyclic } node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehConstruction:RuntimePlannerConstruction policy context rawRewrite deltahAnchor:rawRewrite.anchor = (runtimePlannerRewrite policy rawRewrite).anchorhSubgraphValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidentryList:List nodehEntryMatches:RuntimeNodeListMatches entryList delta.entryNodeshFrontierDelta:delta.cost.frontierDelta = entryList.length - 1hEntryCard:delta.entryNodes.card = entryList.length⊒ (runtimePlannerRewrite policy rawRewrite).anchor ∈ (denote context.topology).vertices All goals completed! πŸ™ node:Typeinst✝:DecidableEq nodepolicy:RuntimeNamespacePolicy nodecontext:PlanningContext noderawRewrite:GraphRewrite nodedelta:PlannedRewriteDelta nodehConstruction:RuntimePlannerConstruction policy context rawRewrite deltahAnchor:rawRewrite.anchor = (runtimePlannerRewrite policy rawRewrite).anchorhSubgraphValid:(runtimePlannerRewrite policy rawRewrite).spec.ValidentryList:List nodehEntryMatches:RuntimeNodeListMatches entryList delta.entryNodeshFrontierDelta:delta.cost.frontierDelta = entryList.length - 1hEntryCard:delta.entryNodes.card = entryList.length⊒ (runtimePlannerRewrite policy rawRewrite).anchor ∈ context.definitions All goals completed! πŸ™

Executable planner construction plus budget admission gives an abstract admissible rewrite.

theorem runtimePlannerConstruction_admissible {policy : RuntimeNamespacePolicy node} {context : PlanningContext node} {rawRewrite : GraphRewrite node} {budget remaining : RewriteBudget} {delta : PlannedRewriteDelta node} {contractOk : Graph node β†’ Prop} (hConstruction : RuntimePlannerConstruction policy context rawRewrite delta) (hAdmitted : AdmittedRewriteDelta budget delta remaining) (hContracts : βˆ€ g, denote g = denote context.topology β†’ contractOk g β†’ contractOk delta.topology) : admissible (delta.toRewrite context.topology (plannedRewriteSafety_of_checks (runtimePlannerConstruction_planGraphRewriteChecks hConstruction) hContracts)) context.topology budget := planGraphRewriteChecks_admissible (runtimePlannerConstruction_planGraphRewriteChecks hConstruction) hAdmitted hContractsend PlannerBridgeend Cortex.Wire