Theory /Cortex /Wire /ActualizedBridge

Cortex.Wire.ActualizedBridge

proofs

On this page

Overview
Context
Theorem Split
Source-to-actualized port projection
Deterministic projection of source linear objects
Aligned port-use witnesses
Exactness corollary

Imports

import Cortex.Wire.PortLinearity

Overview

Source-to-actualized projection exactness bridge for compiled port-use witnesses. The theorems here pin source ↔ actualized port-set and edge bijection; they do not bridge the witness to a Haskell-compiled runtime artifact, so they are not yet "executable correspondence."

Context

Cortex.Wire.PortLinearity defines two complementary carriers. The source side uses LinearPortObject over SourcePortInstance; the closed actualized side uses ActualizedPortGraph over ActualizedPortInstance, plus the PortUseWitness shape that compiler or admission must eventually produce. portUseWitness_toGraph_closedPortLinear already proves sufficiency: a supplied witness establishes closed port linearity on its declared domain.

What it does not prove is projection exactness: the witness's actualized output and input port sets correspond bijectively to the source object's port instances, so a runtime cannot smuggle in actualized ports the source carrier never admitted, and its actualized edge consumers coincide with the source object's port edges. This file closes that gap as a deterministic structural projection. Runtime-witness production, terminal-discharge correspondence, and the bridge to compiled Haskell artifacts remain open.

Theorem Split

The page defines:

projectSourceOutput and projectSourceInput, the canonical injections from source to actualized port instances;
SourceToActualizedProjection, the deterministic projection of a source LinearPortObject onto an ActualizedPortGraph skeleton;
recovered port-node-domain, output, input, and edge correspondence equalities exposed as theorems (portNodeDomain_eq, projection_outputs_image_eq, etc.);
PortUseWitness.AlignedWith, the predicate that the witness's actualized graph coincides with the projection of a certified source object on domains and edge consumers;
compiledPortUseWitness_exact_forward, the load-bearing forward direction showing every actualized port of an aligned witness comes from a source port instance;
compiledPortUseWitness_exact_reverse, the symmetric reverse direction showing every source port instance is represented in the witness;
compiledPortUseWitness_exact, the iff combining both directions for one uniform exactness statement.

The projection is intentionally restricted to the case where the source-side output, input, and actualized-side output, input port label alphabets agree. That is enough to rule out the "runtime port not in source" failure mode for the compiler-emitted witness; richer projections that re-label ports remain out of scope for this slice.

namespace Cortex.Wireopen LinearPortGraph

Source-to-actualized port projection

section Projection

variable
  {node outputPort inputPort terminal : Type}
  [DecidableEq node]
  [DecidableEq outputPort]
  [DecidableEq inputPort]
  [DecidableEq terminal]

projectSourceOutput sp is the canonical actualized image of a source output port instance.

The map preserves node identity and port label literally, so every source-side declared output port becomes a distinct actualized port instance.

def projectSourceOutput
    (sp : SourcePortInstance node outputPort) :
    ActualizedPortInstance node outputPort :=
  { node := sp.node
    port := sp.port }

projectSourceInput sp is the canonical actualized image of a source input port instance.

The map preserves node identity and port label literally, so every source-side declared input port becomes a distinct actualized port instance.

def projectSourceInput
    (sp : SourcePortInstance node inputPort) :
    ActualizedPortInstance node inputPort :=
  { node := sp.node
    port := sp.port }

omit [DecidableEq node] [DecidableEq outputPort] [DecidableEq inputPort] [DecidableEq terminal] in

projectSourceOutput is injective.

theorem projectSourceOutput_injective :
    Function.Injective (projectSourceOutput (node := node) (outputPort := outputPort)) := bynode:TypeoutputPort:Type⊢ Function.Injective projectSourceOutput
  intro left rightnode:TypeoutputPort:Typeleft:SourcePortInstance node outputPortright:SourcePortInstance node outputPort⊢ projectSourceOutput left = projectSourceOutput right → left = right hEqnode:TypeoutputPort:Typeleft:SourcePortInstance node outputPortright:SourcePortInstance node outputPorthEq:projectSourceOutput left = projectSourceOutput right⊢ left = right
  have hNode : left.node = right.node := congrArg ActualizedPortInstance.node hEqnode:TypeoutputPort:Typeleft:SourcePortInstance node outputPortright:SourcePortInstance node outputPorthEq:projectSourceOutput left = projectSourceOutput righthNode:left.node = right.node⊢ left = right
  have hPort : left.port = right.port := congrArg ActualizedPortInstance.port hEqnode:TypeoutputPort:Typeleft:SourcePortInstance node outputPortright:SourcePortInstance node outputPorthEq:projectSourceOutput left = projectSourceOutput righthNode:left.node = right.nodehPort:left.port = right.port⊢ left = right
  cases leftmknode:TypeoutputPort:Typeright:SourcePortInstance node outputPortnode✝:nodeport✝:outputPorthEq:projectSourceOutput { node := node✝, port := port✝ } = projectSourceOutput righthNode:{ node := node✝, port := port✝ }.node = right.nodehPort:{ node := node✝, port := port✝ }.port = right.port⊢ { node := node✝, port := port✝ } = right
  cases rightmk.mknode:TypeoutputPort:Typenode✝¹:nodeport✝¹:outputPortnode✝:nodeport✝:outputPorthEq:projectSourceOutput { node := node✝¹, port := port✝¹ } = projectSourceOutput { node := node✝, port := port✝ }hNode:{ node := node✝¹, port := port✝¹ }.node = { node := node✝, port := port✝ }.nodehPort:{ node := node✝¹, port := port✝¹ }.port = { node := node✝, port := port✝ }.port⊢ { node := node✝¹, port := port✝¹ } = { node := node✝, port := port✝ }
  cases hNodemk.mk.reflnode:TypeoutputPort:Typenode✝:nodeport✝¹:outputPortport✝:outputPorthEq:projectSourceOutput { node := node✝, port := port✝¹ } = projectSourceOutput { node := node✝, port := port✝ }hPort:{ node := node✝, port := port✝¹ }.port = { node := node✝, port := port✝ }.port⊢ { node := node✝, port := port✝¹ } = { node := node✝, port := port✝ }
  cases hPortmk.mk.refl.reflnode:TypeoutputPort:Typenode✝:nodeport✝:outputPorthEq:projectSourceOutput { node := node✝, port := port✝ } = projectSourceOutput { node := node✝, port := port✝ }⊢ { node := node✝, port := port✝ } = { node := node✝, port := port✝ }
  rflAll goals completed! 🐙

omit [DecidableEq node] [DecidableEq outputPort] [DecidableEq inputPort] [DecidableEq terminal] in

projectSourceInput is injective.

theorem projectSourceInput_injective :
    Function.Injective (projectSourceInput (node := node) (inputPort := inputPort)) := bynode:TypeinputPort:Type⊢ Function.Injective projectSourceInput
  intro left rightnode:TypeinputPort:Typeleft:SourcePortInstance node inputPortright:SourcePortInstance node inputPort⊢ projectSourceInput left = projectSourceInput right → left = right hEqnode:TypeinputPort:Typeleft:SourcePortInstance node inputPortright:SourcePortInstance node inputPorthEq:projectSourceInput left = projectSourceInput right⊢ left = right
  have hNode : left.node = right.node := congrArg ActualizedPortInstance.node hEqnode:TypeinputPort:Typeleft:SourcePortInstance node inputPortright:SourcePortInstance node inputPorthEq:projectSourceInput left = projectSourceInput righthNode:left.node = right.node⊢ left = right
  have hPort : left.port = right.port := congrArg ActualizedPortInstance.port hEqnode:TypeinputPort:Typeleft:SourcePortInstance node inputPortright:SourcePortInstance node inputPorthEq:projectSourceInput left = projectSourceInput righthNode:left.node = right.nodehPort:left.port = right.port⊢ left = right
  cases leftmknode:TypeinputPort:Typeright:SourcePortInstance node inputPortnode✝:nodeport✝:inputPorthEq:projectSourceInput { node := node✝, port := port✝ } = projectSourceInput righthNode:{ node := node✝, port := port✝ }.node = right.nodehPort:{ node := node✝, port := port✝ }.port = right.port⊢ { node := node✝, port := port✝ } = right
  cases rightmk.mknode:TypeinputPort:Typenode✝¹:nodeport✝¹:inputPortnode✝:nodeport✝:inputPorthEq:projectSourceInput { node := node✝¹, port := port✝¹ } = projectSourceInput { node := node✝, port := port✝ }hNode:{ node := node✝¹, port := port✝¹ }.node = { node := node✝, port := port✝ }.nodehPort:{ node := node✝¹, port := port✝¹ }.port = { node := node✝, port := port✝ }.port⊢ { node := node✝¹, port := port✝¹ } = { node := node✝, port := port✝ }
  cases hNodemk.mk.reflnode:TypeinputPort:Typenode✝:nodeport✝¹:inputPortport✝:inputPorthEq:projectSourceInput { node := node✝, port := port✝¹ } = projectSourceInput { node := node✝, port := port✝ }hPort:{ node := node✝, port := port✝¹ }.port = { node := node✝, port := port✝ }.port⊢ { node := node✝, port := port✝¹ } = { node := node✝, port := port✝ }
  cases hPortmk.mk.refl.reflnode:TypeinputPort:Typenode✝:nodeport✝:inputPorthEq:projectSourceInput { node := node✝, port := port✝ } = projectSourceInput { node := node✝, port := port✝ }⊢ { node := node✝, port := port✝ } = { node := node✝, port := port✝ }
  rflAll goals completed! 🐙

end Projection

Deterministic projection of source linear objects

section SourceProjection

variable
  {node outputPort inputPort terminal : Type}
  [DecidableEq node]
  [DecidableEq outputPort]
  [DecidableEq inputPort]
  [DecidableEq terminal]

projectedActualizedGraph object is the canonical ActualizedPortGraph projection of a certified source linear object.

Outputs and inputs are the literal images of the source object's source port instances under projectSourceOutput and projectSourceInput. Edge consumers, terminal discharges, and input producers are derived from the source portEdges: the consumer of a source-image output is the projected input that the source edge targets; the producer of a source-image input is the projected output that produces it. Source frontier endpoints map to empty edge consumers, leaving terminal-discharge accounting to the caller's witness layer.

def projectedActualizedGraph
    (object : LinearPortObject node outputPort inputPort) :
    ActualizedPortGraph node outputPort inputPort terminal where
  outputs := object.graph.outputs.image projectSourceOutput
  inputs := object.graph.inputs.image projectSourceInput
  edgeConsumers := fun output =>
    (object.graph.portEdges.filter (fun edge => projectSourceOutput edge.1 = output)).image
      (fun edge => projectSourceInput edge.2)
  terminalDischarges := fun _ => ∅
  inputProducers := fun input =>
    (object.graph.portEdges.filter (fun edge => projectSourceInput edge.2 = input)).image
      (fun edge => projectSourceOutput edge.1)

SourceToActualizedProjection object actualized records the exact correspondence between a source object and a candidate actualized port graph.

The bridge is a structure rather than a definitional equality so callers can supply alternate but equivalent runtime materializations. The fields demand extensional equality on every port-instance domain, plus on the edge relation; the canonical witness is SourceToActualizedProjection.canonical.

structure SourceToActualizedProjection
    (object : LinearPortObject node outputPort inputPort)
    (actualized : ActualizedPortGraph node outputPort inputPort terminal) :
    Prop where

Actualized outputs are exactly the projected source outputs.

outputs_eq : actualized.outputs = object.graph.outputs.image projectSourceOutput

Actualized inputs are exactly the projected source inputs.

inputs_eq : actualized.inputs = object.graph.inputs.image projectSourceInput

An actualized edge runs between projected source endpoints iff the source carries it.

  edge_iff :
    ∀ output input,
      input ∈ actualized.edgeConsumers output ↔
        ∃ source,
          source ∈ object.graph.portEdges ∧
            projectSourceOutput source.1 = output ∧
              projectSourceInput source.2 = input

namespace SourceToActualizedProjection

variable
  {object : LinearPortObject node outputPort inputPort}
  {actualized : ActualizedPortGraph node outputPort inputPort terminal}

Nodes that occur in an actualized port domain. ActualizedPortGraph has no separate node set, so the domain is recovered from output and input instances.

def actualizedPortNodeDomain
    (graph : ActualizedPortGraph node outputPort inputPort terminal) :
    Finset node :=
  graph.outputs.image ActualizedPortInstance.node ∪
    graph.inputs.image ActualizedPortInstance.node

Nodes that occur in a source object's port domain. This intentionally ignores isolated source nodes with no port instances; those are not recoverable from an actualized port-use graph.

def sourcePortNodeDomain
    (object : LinearPortObject node outputPort inputPort) :
    Finset node :=
  object.graph.outputs.image SourcePortInstance.node ∪
    object.graph.inputs.image SourcePortInstance.node

The canonical projection always satisfies the bridge predicate.

theorem canonical
    (object : LinearPortObject node outputPort inputPort) :
    SourceToActualizedProjection
      (terminal := terminal)
      object
      (projectedActualizedGraph object) := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPort⊢ SourceToActualizedProjection object (projectedActualizedGraph object)
  refine ⟨rfl, rfl, ?_⟩node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPort⊢ ∀ (output : ActualizedPortInstance node outputPort) (input : ActualizedPortInstance node inputPort),
  input ∈ (projectedActualizedGraph object).edgeConsumers output ↔
    ∃ source ∈ object.graph.portEdges, projectSourceOutput source.1 = output ∧ projectSourceInput source.2 = input
  intro output inputnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortoutput:ActualizedPortInstance node outputPortinput:ActualizedPortInstance node inputPort⊢ input ∈ (projectedActualizedGraph object).edgeConsumers output ↔
  ∃ source ∈ object.graph.portEdges, projectSourceOutput source.1 = output ∧ projectSourceInput source.2 = input
  simp only [projectedActualizedGraph, Finset.mem_image, Finset.mem_filter]node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortoutput:ActualizedPortInstance node outputPortinput:ActualizedPortInstance node inputPort⊢ (∃ a, (a ∈ object.graph.portEdges ∧ projectSourceOutput a.1 = output) ∧ projectSourceInput a.2 = input) ↔
  ∃ source ∈ object.graph.portEdges, projectSourceOutput source.1 = output ∧ projectSourceInput source.2 = input
  constructormpnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortoutput:ActualizedPortInstance node outputPortinput:ActualizedPortInstance node inputPort⊢ (∃ a, (a ∈ object.graph.portEdges ∧ projectSourceOutput a.1 = output) ∧ projectSourceInput a.2 = input) →
  ∃ source ∈ object.graph.portEdges, projectSourceOutput source.1 = output ∧ projectSourceInput source.2 = inputmprnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortoutput:ActualizedPortInstance node outputPortinput:ActualizedPortInstance node inputPort⊢ (∃ source ∈ object.graph.portEdges, projectSourceOutput source.1 = output ∧ projectSourceInput source.2 = input) →
  ∃ a, (a ∈ object.graph.portEdges ∧ projectSourceOutput a.1 = output) ∧ projectSourceInput a.2 = input
  ·mpnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortoutput:ActualizedPortInstance node outputPortinput:ActualizedPortInstance node inputPort⊢ (∃ a, (a ∈ object.graph.portEdges ∧ projectSourceOutput a.1 = output) ∧ projectSourceInput a.2 = input) →
  ∃ source ∈ object.graph.portEdges, projectSourceOutput source.1 = output ∧ projectSourceInput source.2 = input rintro ⟨edge, ⟨hEdge, hOutput⟩, hInput⟩mpnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortoutput:ActualizedPortInstance node outputPortinput:ActualizedPortInstance node inputPortedge:SourcePortInstance node outputPort × SourcePortInstance node inputPorthInput:projectSourceInput edge.2 = inputhEdge:edge ∈ object.graph.portEdgeshOutput:projectSourceOutput edge.1 = output⊢ ∃ source ∈ object.graph.portEdges, projectSourceOutput source.1 = output ∧ projectSourceInput source.2 = input
    exact ⟨edge, hEdge, hOutput, hInput⟩All goals completed! 🐙
  ·mprnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortoutput:ActualizedPortInstance node outputPortinput:ActualizedPortInstance node inputPort⊢ (∃ source ∈ object.graph.portEdges, projectSourceOutput source.1 = output ∧ projectSourceInput source.2 = input) →
  ∃ a, (a ∈ object.graph.portEdges ∧ projectSourceOutput a.1 = output) ∧ projectSourceInput a.2 = input rintro ⟨edge, hEdge, hOutput, hInput⟩mprnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortoutput:ActualizedPortInstance node outputPortinput:ActualizedPortInstance node inputPortedge:SourcePortInstance node outputPort × SourcePortInstance node inputPorthEdge:edge ∈ object.graph.portEdgeshOutput:projectSourceOutput edge.1 = outputhInput:projectSourceInput edge.2 = input⊢ ∃ a, (a ∈ object.graph.portEdges ∧ projectSourceOutput a.1 = output) ∧ projectSourceInput a.2 = input
    exact ⟨edge, ⟨hEdge, hOutput⟩, hInput⟩All goals completed! 🐙

The canonical projection has no terminal discharges.

This names the current source-side target for future runtime witness production: terminal discharge correspondence is not part of SourceToActualizedProjection, but the deterministic projection used by this file leaves every output undischarged at the terminal layer.

theorem canonical_terminalDischarges_eq_empty
    (object : LinearPortObject node outputPort inputPort)
    (output : ActualizedPortInstance node outputPort) :
    (projectedActualizedGraph (terminal := terminal) object).terminalDischarges output = ∅ :=
  rfl

The actualized port-node domain is exactly the source port-node domain.

theorem portNodeDomain_eq
    (hProj : SourceToActualizedProjection (terminal := terminal) object actualized) :
    actualizedPortNodeDomain actualized = sourcePortNodeDomain object := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualized⊢ actualizedPortNodeDomain actualized = sourcePortNodeDomain object
  ext portNodehnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedportNode:node⊢ portNode ∈ actualizedPortNodeDomain actualized ↔ portNode ∈ sourcePortNodeDomain object
  unfold actualizedPortNodeDomain sourcePortNodeDomainhnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedportNode:node⊢ portNode ∈
    Finset.image ActualizedPortInstance.node actualized.outputs ∪
      Finset.image ActualizedPortInstance.node actualized.inputs ↔
  portNode ∈
    Finset.image SourcePortInstance.node object.graph.outputs ∪ Finset.image SourcePortInstance.node object.graph.inputs
  rw [hProj.outputs_eq, hProj.inputs_eq]hnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedportNode:node⊢ portNode ∈
    Finset.image ActualizedPortInstance.node (Finset.image projectSourceOutput object.graph.outputs) ∪
      Finset.image ActualizedPortInstance.node (Finset.image projectSourceInput object.graph.inputs) ↔
  portNode ∈
    Finset.image SourcePortInstance.node object.graph.outputs ∪ Finset.image SourcePortInstance.node object.graph.inputs
  simp only [Finset.mem_union, Finset.mem_image]hnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedportNode:node⊢ ((∃ a, (∃ a_1 ∈ object.graph.outputs, projectSourceOutput a_1 = a) ∧ a.node = portNode) ∨
    ∃ a, (∃ a_1 ∈ object.graph.inputs, projectSourceInput a_1 = a) ∧ a.node = portNode) ↔
  (∃ a ∈ object.graph.outputs, a.node = portNode) ∨ ∃ a ∈ object.graph.inputs, a.node = portNode
  constructorh.mpnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedportNode:node⊢ ((∃ a, (∃ a_1 ∈ object.graph.outputs, projectSourceOutput a_1 = a) ∧ a.node = portNode) ∨
    ∃ a, (∃ a_1 ∈ object.graph.inputs, projectSourceInput a_1 = a) ∧ a.node = portNode) →
  (∃ a ∈ object.graph.outputs, a.node = portNode) ∨ ∃ a ∈ object.graph.inputs, a.node = portNodeh.mprnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedportNode:node⊢ ((∃ a ∈ object.graph.outputs, a.node = portNode) ∨ ∃ a ∈ object.graph.inputs, a.node = portNode) →
  (∃ a, (∃ a_1 ∈ object.graph.outputs, projectSourceOutput a_1 = a) ∧ a.node = portNode) ∨
    ∃ a, (∃ a_1 ∈ object.graph.inputs, projectSourceInput a_1 = a) ∧ a.node = portNode
  ·h.mpnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedportNode:node⊢ ((∃ a, (∃ a_1 ∈ object.graph.outputs, projectSourceOutput a_1 = a) ∧ a.node = portNode) ∨
    ∃ a, (∃ a_1 ∈ object.graph.inputs, projectSourceInput a_1 = a) ∧ a.node = portNode) →
  (∃ a ∈ object.graph.outputs, a.node = portNode) ∨ ∃ a ∈ object.graph.inputs, a.node = portNode rintro (⟨_, ⟨output, hOutput, rfl⟩, rfl⟩ | ⟨_, ⟨input, hInput, rfl⟩, rfl⟩)h.mp.inlnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedoutput:SourcePortInstance node outputPorthOutput:output ∈ object.graph.outputs⊢ (∃ a ∈ object.graph.outputs, a.node = (projectSourceOutput output).node) ∨
  ∃ a ∈ object.graph.inputs, a.node = (projectSourceOutput output).nodeh.mp.inrnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedinput:SourcePortInstance node inputPorthInput:input ∈ object.graph.inputs⊢ (∃ a ∈ object.graph.outputs, a.node = (projectSourceInput input).node) ∨
  ∃ a ∈ object.graph.inputs, a.node = (projectSourceInput input).node
    ·h.mp.inlnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedoutput:SourcePortInstance node outputPorthOutput:output ∈ object.graph.outputs⊢ (∃ a ∈ object.graph.outputs, a.node = (projectSourceOutput output).node) ∨
  ∃ a ∈ object.graph.inputs, a.node = (projectSourceOutput output).node exact Or.inl ⟨output, hOutput, rfl⟩All goals completed! 🐙
    ·h.mp.inrnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedinput:SourcePortInstance node inputPorthInput:input ∈ object.graph.inputs⊢ (∃ a ∈ object.graph.outputs, a.node = (projectSourceInput input).node) ∨
  ∃ a ∈ object.graph.inputs, a.node = (projectSourceInput input).node exact Or.inr ⟨input, hInput, rfl⟩All goals completed! 🐙
  ·h.mprnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedportNode:node⊢ ((∃ a ∈ object.graph.outputs, a.node = portNode) ∨ ∃ a ∈ object.graph.inputs, a.node = portNode) →
  (∃ a, (∃ a_1 ∈ object.graph.outputs, projectSourceOutput a_1 = a) ∧ a.node = portNode) ∨
    ∃ a, (∃ a_1 ∈ object.graph.inputs, projectSourceInput a_1 = a) ∧ a.node = portNode rintro (⟨output, hOutput, rfl⟩ | ⟨input, hInput, rfl⟩)h.mpr.inlnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedoutput:SourcePortInstance node outputPorthOutput:output ∈ object.graph.outputs⊢ (∃ a, (∃ a_1 ∈ object.graph.outputs, projectSourceOutput a_1 = a) ∧ a.node = output.node) ∨
  ∃ a, (∃ a_1 ∈ object.graph.inputs, projectSourceInput a_1 = a) ∧ a.node = output.nodeh.mpr.inrnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedinput:SourcePortInstance node inputPorthInput:input ∈ object.graph.inputs⊢ (∃ a, (∃ a_1 ∈ object.graph.outputs, projectSourceOutput a_1 = a) ∧ a.node = input.node) ∨
  ∃ a, (∃ a_1 ∈ object.graph.inputs, projectSourceInput a_1 = a) ∧ a.node = input.node
    ·h.mpr.inlnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedoutput:SourcePortInstance node outputPorthOutput:output ∈ object.graph.outputs⊢ (∃ a, (∃ a_1 ∈ object.graph.outputs, projectSourceOutput a_1 = a) ∧ a.node = output.node) ∨
  ∃ a, (∃ a_1 ∈ object.graph.inputs, projectSourceInput a_1 = a) ∧ a.node = output.node exact Or.inl ⟨projectSourceOutput output, ⟨output, hOutput, rfl⟩, rfl⟩All goals completed! 🐙
    ·h.mpr.inrnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedinput:SourcePortInstance node inputPorthInput:input ∈ object.graph.inputs⊢ (∃ a, (∃ a_1 ∈ object.graph.outputs, projectSourceOutput a_1 = a) ∧ a.node = input.node) ∨
  ∃ a, (∃ a_1 ∈ object.graph.inputs, projectSourceInput a_1 = a) ∧ a.node = input.node exact Or.inr ⟨projectSourceInput input, ⟨input, hInput, rfl⟩, rfl⟩All goals completed! 🐙

Every source output appears as an actualized output.

theorem source_output_mem
    (hProj : SourceToActualizedProjection (terminal := terminal) object actualized)
    {sp : SourcePortInstance node outputPort}
    (hSource : sp ∈ object.graph.outputs) :
    projectSourceOutput sp ∈ actualized.outputs := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedsp:SourcePortInstance node outputPorthSource:sp ∈ object.graph.outputs⊢ projectSourceOutput sp ∈ actualized.outputs
  rw [hProj.outputs_eq]node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedsp:SourcePortInstance node outputPorthSource:sp ∈ object.graph.outputs⊢ projectSourceOutput sp ∈ Finset.image projectSourceOutput object.graph.outputs
  exact Finset.mem_image.mpr ⟨sp, hSource, rfl⟩All goals completed! 🐙

Every source input appears as an actualized input.

theorem source_input_mem
    (hProj : SourceToActualizedProjection (terminal := terminal) object actualized)
    {sp : SourcePortInstance node inputPort}
    (hSource : sp ∈ object.graph.inputs) :
    projectSourceInput sp ∈ actualized.inputs := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedsp:SourcePortInstance node inputPorthSource:sp ∈ object.graph.inputs⊢ projectSourceInput sp ∈ actualized.inputs
  rw [hProj.inputs_eq]node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedsp:SourcePortInstance node inputPorthSource:sp ∈ object.graph.inputs⊢ projectSourceInput sp ∈ Finset.image projectSourceInput object.graph.inputs
  exact Finset.mem_image.mpr ⟨sp, hSource, rfl⟩All goals completed! 🐙

Every actualized output traces back to a unique source output.

theorem actualized_output_source
    (hProj : SourceToActualizedProjection (terminal := terminal) object actualized)
    {output : ActualizedPortInstance node outputPort}
    (hOutput : output ∈ actualized.outputs) :
    ∃ sp, sp ∈ object.graph.outputs ∧ projectSourceOutput sp = output := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedoutput:ActualizedPortInstance node outputPorthOutput:output ∈ actualized.outputs⊢ ∃ sp ∈ object.graph.outputs, projectSourceOutput sp = output
  have hImage : output ∈ object.graph.outputs.image projectSourceOutput := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedoutput:ActualizedPortInstance node outputPorthOutput:output ∈ actualized.outputs⊢ ∃ sp ∈ object.graph.outputs, projectSourceOutput sp = output
    rw [← hProj.outputs_eq]node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedoutput:ActualizedPortInstance node outputPorthOutput:output ∈ actualized.outputs⊢ output ∈ actualized.outputs; exact hOutputAll goals completed! 🐙
  exact Finset.mem_image.mp hImageAll goals completed! 🐙

Every actualized input traces back to a unique source input.

theorem actualized_input_source
    (hProj : SourceToActualizedProjection (terminal := terminal) object actualized)
    {input : ActualizedPortInstance node inputPort}
    (hInput : input ∈ actualized.inputs) :
    ∃ sp, sp ∈ object.graph.inputs ∧ projectSourceInput sp = input := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedinput:ActualizedPortInstance node inputPorthInput:input ∈ actualized.inputs⊢ ∃ sp ∈ object.graph.inputs, projectSourceInput sp = input
  have hImage : input ∈ object.graph.inputs.image projectSourceInput := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedinput:ActualizedPortInstance node inputPorthInput:input ∈ actualized.inputs⊢ ∃ sp ∈ object.graph.inputs, projectSourceInput sp = input
    rw [← hProj.inputs_eq]node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalobject:LinearPortObject node outputPort inputPortactualized:ActualizedPortGraph node outputPort inputPort terminalhProj:SourceToActualizedProjection object actualizedinput:ActualizedPortInstance node inputPorthInput:input ∈ actualized.inputs⊢ input ∈ actualized.inputs; exact hInputAll goals completed! 🐙
  exact Finset.mem_image.mp hImageAll goals completed! 🐙

end SourceToActualizedProjectionend SourceProjection

Aligned port-use witnesses

section Alignment

variable
  {node outputPort inputPort terminal : Type}
  [DecidableEq node]
  [DecidableEq outputPort]
  [DecidableEq inputPort]
  [DecidableEq terminal]

PortUseWitness.AlignedWith witness object says the witness's actualized graph is exactly the projection of the source object on port domains and edge consumers.

This is the proof-side closure of the open exactness obligation called out in PortUseWitness's docstring. Once a compiler discharges the predicate, the runtime cannot operate on actualized ports that the source side did not declare, and cannot add or omit source port edges. Terminal-discharge correspondence remains a later runtime-facing obligation.

def PortUseWitness.AlignedWith
    (witness : PortUseWitness node outputPort inputPort terminal)
    (object : LinearPortObject node outputPort inputPort) : Prop :=
  SourceToActualizedProjection object witness.toGraph

namespace PortUseWitness

An aligned witness's outputs equal the canonical projection's outputs.

theorem alignedWith_outputs
    {witness : PortUseWitness node outputPort inputPort terminal}
    {object : LinearPortObject node outputPort inputPort}
    (hAligned : witness.AlignedWith object) :
    witness.outputs = object.graph.outputs.image projectSourceOutput :=
  hAligned.outputs_eq

An aligned witness's inputs equal the canonical projection's inputs.

theorem alignedWith_inputs
    {witness : PortUseWitness node outputPort inputPort terminal}
    {object : LinearPortObject node outputPort inputPort}
    (hAligned : witness.AlignedWith object) :
    witness.inputs = object.graph.inputs.image projectSourceInput :=
  hAligned.inputs_eq

An aligned witness's edge consumers are exactly the projected source edges.

theorem alignedWith_edge_iff
    {witness : PortUseWitness node outputPort inputPort terminal}
    {object : LinearPortObject node outputPort inputPort}
    (hAligned : witness.AlignedWith object)
    (output : ActualizedPortInstance node outputPort)
    (input : ActualizedPortInstance node inputPort) :
    input ∈ witness.toGraph.edgeConsumers output ↔
      ∃ source,
        source ∈ object.graph.portEdges ∧
          projectSourceOutput source.1 = output ∧
            projectSourceInput source.2 = input :=
  hAligned.edge_iff output input

Aligned witnesses match the canonical projection's actualized domain extensionally.

theorem alignedWith_canonical
    {witness : PortUseWitness node outputPort inputPort terminal}
    {object : LinearPortObject node outputPort inputPort}
    (hAligned : witness.AlignedWith object) :
    witness.outputs = (projectedActualizedGraph
        (terminal := terminal) object).outputs ∧
      witness.inputs = (projectedActualizedGraph
        (terminal := terminal) object).inputs := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith object⊢ witness.outputs = (projectedActualizedGraph object).outputs ∧ witness.inputs = (projectedActualizedGraph object).inputs
  refine ⟨?_, ?_⟩refine_1node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith object⊢ witness.outputs = (projectedActualizedGraph object).outputsrefine_2node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith object⊢ witness.inputs = (projectedActualizedGraph object).inputs
  ·refine_1node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith object⊢ witness.outputs = (projectedActualizedGraph object).outputs simpa [projectedActualizedGraph, PortUseWitness.toGraph] using hAligned.outputs_eqAll goals completed! 🐙
  ·refine_2node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith object⊢ witness.inputs = (projectedActualizedGraph object).inputs simpa [projectedActualizedGraph, PortUseWitness.toGraph] using hAligned.inputs_eqAll goals completed! 🐙

end PortUseWitness

Exactness corollary

Forward direction of the exactness corollary.

Every actualized output port that an aligned witness operates on is the image of a source-side declared output port. This is the load-bearing claim that prevents the runtime from using actualized output ports the source admission carrier never declared.

theorem compiledPortUseWitness_exact_output_forward
    {witness : PortUseWitness node outputPort inputPort terminal}
    {object : LinearPortObject node outputPort inputPort}
    (hAligned : witness.AlignedWith object)
    {output : ActualizedPortInstance node outputPort}
    (hOutput : output ∈ witness.outputs) :
    ∃ sp, sp ∈ object.graph.outputs ∧ projectSourceOutput sp = output := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectoutput:ActualizedPortInstance node outputPorthOutput:output ∈ witness.outputs⊢ ∃ sp ∈ object.graph.outputs, projectSourceOutput sp = output
  have hImage : output ∈ object.graph.outputs.image projectSourceOutput := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectoutput:ActualizedPortInstance node outputPorthOutput:output ∈ witness.outputs⊢ ∃ sp ∈ object.graph.outputs, projectSourceOutput sp = output
    rw [← hAligned.outputs_eq]node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectoutput:ActualizedPortInstance node outputPorthOutput:output ∈ witness.outputs⊢ output ∈ witness.toGraph.outputs
    simpa [PortUseWitness.toGraph] using hOutputAll goals completed! 🐙
  exact Finset.mem_image.mp hImageAll goals completed! 🐙

Forward direction of the exactness corollary, input side.

Every actualized input port that an aligned witness operates on is the image of a source-side declared input port.

theorem compiledPortUseWitness_exact_input_forward
    {witness : PortUseWitness node outputPort inputPort terminal}
    {object : LinearPortObject node outputPort inputPort}
    (hAligned : witness.AlignedWith object)
    {input : ActualizedPortInstance node inputPort}
    (hInput : input ∈ witness.inputs) :
    ∃ sp, sp ∈ object.graph.inputs ∧ projectSourceInput sp = input := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectinput:ActualizedPortInstance node inputPorthInput:input ∈ witness.inputs⊢ ∃ sp ∈ object.graph.inputs, projectSourceInput sp = input
  have hImage : input ∈ object.graph.inputs.image projectSourceInput := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectinput:ActualizedPortInstance node inputPorthInput:input ∈ witness.inputs⊢ ∃ sp ∈ object.graph.inputs, projectSourceInput sp = input
    rw [← hAligned.inputs_eq]node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectinput:ActualizedPortInstance node inputPorthInput:input ∈ witness.inputs⊢ input ∈ witness.toGraph.inputs
    simpa [PortUseWitness.toGraph] using hInputAll goals completed! 🐙
  exact Finset.mem_image.mp hImageAll goals completed! 🐙

Reverse direction of the exactness corollary, output side.

Every source-side declared output port appears in the aligned witness's output domain. This rules out the dual under-approximation failure mode where the witness silently drops a source port.

theorem compiledPortUseWitness_exact_output_reverse
    {witness : PortUseWitness node outputPort inputPort terminal}
    {object : LinearPortObject node outputPort inputPort}
    (hAligned : witness.AlignedWith object)
    {sp : SourcePortInstance node outputPort}
    (hSource : sp ∈ object.graph.outputs) :
    projectSourceOutput sp ∈ witness.outputs := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectsp:SourcePortInstance node outputPorthSource:sp ∈ object.graph.outputs⊢ projectSourceOutput sp ∈ witness.outputs
  have hProjected : projectSourceOutput sp ∈ witness.toGraph.outputs := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectsp:SourcePortInstance node outputPorthSource:sp ∈ object.graph.outputs⊢ projectSourceOutput sp ∈ witness.outputs
    rw [hAligned.outputs_eq]node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectsp:SourcePortInstance node outputPorthSource:sp ∈ object.graph.outputs⊢ projectSourceOutput sp ∈ Finset.image projectSourceOutput object.graph.outputs
    exact Finset.mem_image.mpr ⟨sp, hSource, rfl⟩All goals completed! 🐙
  simpa [PortUseWitness.toGraph] using hProjectedAll goals completed! 🐙

Reverse direction of the exactness corollary, input side.

theorem compiledPortUseWitness_exact_input_reverse
    {witness : PortUseWitness node outputPort inputPort terminal}
    {object : LinearPortObject node outputPort inputPort}
    (hAligned : witness.AlignedWith object)
    {sp : SourcePortInstance node inputPort}
    (hSource : sp ∈ object.graph.inputs) :
    projectSourceInput sp ∈ witness.inputs := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectsp:SourcePortInstance node inputPorthSource:sp ∈ object.graph.inputs⊢ projectSourceInput sp ∈ witness.inputs
  have hProjected : projectSourceInput sp ∈ witness.toGraph.inputs := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectsp:SourcePortInstance node inputPorthSource:sp ∈ object.graph.inputs⊢ projectSourceInput sp ∈ witness.inputs
    rw [hAligned.inputs_eq]node:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectsp:SourcePortInstance node inputPorthSource:sp ∈ object.graph.inputs⊢ projectSourceInput sp ∈ Finset.image projectSourceInput object.graph.inputs
    exact Finset.mem_image.mpr ⟨sp, hSource, rfl⟩All goals completed! 🐙
  simpa [PortUseWitness.toGraph] using hProjectedAll goals completed! 🐙

Combined exactness biconditional for output ports.

A port instance is in the aligned witness's output domain iff it is the image of a source output port.

theorem compiledPortUseWitness_exact_output
    {witness : PortUseWitness node outputPort inputPort terminal}
    {object : LinearPortObject node outputPort inputPort}
    (hAligned : witness.AlignedWith object)
    (output : ActualizedPortInstance node outputPort) :
    output ∈ witness.outputs ↔
      ∃ sp, sp ∈ object.graph.outputs ∧ projectSourceOutput sp = output := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectoutput:ActualizedPortInstance node outputPort⊢ output ∈ witness.outputs ↔ ∃ sp ∈ object.graph.outputs, projectSourceOutput sp = output
  constructormpnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectoutput:ActualizedPortInstance node outputPort⊢ output ∈ witness.outputs → ∃ sp ∈ object.graph.outputs, projectSourceOutput sp = outputmprnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectoutput:ActualizedPortInstance node outputPort⊢ (∃ sp ∈ object.graph.outputs, projectSourceOutput sp = output) → output ∈ witness.outputs
  ·mpnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectoutput:ActualizedPortInstance node outputPort⊢ output ∈ witness.outputs → ∃ sp ∈ object.graph.outputs, projectSourceOutput sp = output intro hOutputmpnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectoutput:ActualizedPortInstance node outputPorthOutput:output ∈ witness.outputs⊢ ∃ sp ∈ object.graph.outputs, projectSourceOutput sp = output
    exact compiledPortUseWitness_exact_output_forward hAligned hOutputAll goals completed! 🐙
  ·mprnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectoutput:ActualizedPortInstance node outputPort⊢ (∃ sp ∈ object.graph.outputs, projectSourceOutput sp = output) → output ∈ witness.outputs rintro ⟨sp, hSource, hEq⟩mprnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectoutput:ActualizedPortInstance node outputPortsp:SourcePortInstance node outputPorthSource:sp ∈ object.graph.outputshEq:projectSourceOutput sp = output⊢ output ∈ witness.outputs
    rw [← hEq]mprnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectoutput:ActualizedPortInstance node outputPortsp:SourcePortInstance node outputPorthSource:sp ∈ object.graph.outputshEq:projectSourceOutput sp = output⊢ projectSourceOutput sp ∈ witness.outputs
    exact compiledPortUseWitness_exact_output_reverse hAligned hSourceAll goals completed! 🐙

Combined exactness biconditional for input ports.

theorem compiledPortUseWitness_exact_input
    {witness : PortUseWitness node outputPort inputPort terminal}
    {object : LinearPortObject node outputPort inputPort}
    (hAligned : witness.AlignedWith object)
    (input : ActualizedPortInstance node inputPort) :
    input ∈ witness.inputs ↔
      ∃ sp, sp ∈ object.graph.inputs ∧ projectSourceInput sp = input := bynode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectinput:ActualizedPortInstance node inputPort⊢ input ∈ witness.inputs ↔ ∃ sp ∈ object.graph.inputs, projectSourceInput sp = input
  constructormpnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectinput:ActualizedPortInstance node inputPort⊢ input ∈ witness.inputs → ∃ sp ∈ object.graph.inputs, projectSourceInput sp = inputmprnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectinput:ActualizedPortInstance node inputPort⊢ (∃ sp ∈ object.graph.inputs, projectSourceInput sp = input) → input ∈ witness.inputs
  ·mpnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectinput:ActualizedPortInstance node inputPort⊢ input ∈ witness.inputs → ∃ sp ∈ object.graph.inputs, projectSourceInput sp = input intro hInputmpnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectinput:ActualizedPortInstance node inputPorthInput:input ∈ witness.inputs⊢ ∃ sp ∈ object.graph.inputs, projectSourceInput sp = input
    exact compiledPortUseWitness_exact_input_forward hAligned hInputAll goals completed! 🐙
  ·mprnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectinput:ActualizedPortInstance node inputPort⊢ (∃ sp ∈ object.graph.inputs, projectSourceInput sp = input) → input ∈ witness.inputs rintro ⟨sp, hSource, hEq⟩mprnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectinput:ActualizedPortInstance node inputPortsp:SourcePortInstance node inputPorthSource:sp ∈ object.graph.inputshEq:projectSourceInput sp = input⊢ input ∈ witness.inputs
    rw [← hEq]mprnode:TypeoutputPort:TypeinputPort:Typeterminal:Typeinst✝³:DecidableEq nodeinst✝²:DecidableEq outputPortinst✝¹:DecidableEq inputPortinst✝:DecidableEq terminalwitness:PortUseWitness node outputPort inputPort terminalobject:LinearPortObject node outputPort inputPorthAligned:witness.AlignedWith objectinput:ActualizedPortInstance node inputPortsp:SourcePortInstance node inputPorthSource:sp ∈ object.graph.inputshEq:projectSourceInput sp = input⊢ projectSourceInput sp ∈ witness.inputs
    exact compiledPortUseWitness_exact_input_reverse hAligned hSourceAll goals completed! 🐙

Named soundness package for an aligned actualized port-use witness.

The fields are the four obligations downstream consumers usually need: closed port linearity, exact projected output/input domains, and exact projected edge consumers. Keeping them named avoids positional tuple access in later compiler-correctness proofs.

structure AlignedPortUseWitnessSoundness
    (witness : PortUseWitness node outputPort inputPort terminal)
    (object : LinearPortObject node outputPort inputPort) : Prop where

The actualized graph induced by the witness is closed-port linear.

closedPortLinear : witness.toGraph.ClosedPortLinear

Every actualized output is exactly a projected source output, and conversely.

  outputsExact :
    ∀ output,
      output ∈ witness.outputs ↔
        ∃ sp, sp ∈ object.graph.outputs ∧ projectSourceOutput sp = output

Every actualized input is exactly a projected source input, and conversely.

  inputsExact :
    ∀ input,
      input ∈ witness.inputs ↔
        ∃ sp, sp ∈ object.graph.inputs ∧ projectSourceInput sp = input

Actualized edge consumers are exactly the projections of source port edges.

  edgeExact :
    ∀ output input,
      input ∈ witness.toGraph.edgeConsumers output ↔
        ∃ source,
          source ∈ object.graph.portEdges ∧
            projectSourceOutput source.1 = output ∧
              projectSourceInput source.2 = input

Aligned witnesses establish closed port linearity and projection exactness on the actualized graph.

This is the slice's named soundness corollary: an aligned witness simultaneously discharges port linearity on its declared domain and the exactness obligation that its declared output/input domains and edge consumers coincide with the source carrier's projection.

Compiler witness production, terminal-discharge correspondence, and the bridge to Haskell-compiled artifacts remain open.

theorem alignedPortUseWitness_closedPortLinear
    (witness : PortUseWitness node outputPort inputPort terminal)
    {object : LinearPortObject node outputPort inputPort}
    (hAligned : witness.AlignedWith object) :
    AlignedPortUseWitnessSoundness witness object where
  closedPortLinear := portUseWitness_toGraph_closedPortLinear witness
  outputsExact := fun output => compiledPortUseWitness_exact_output hAligned output
  inputsExact := fun input => compiledPortUseWitness_exact_input hAligned input
  edgeExact := fun output input => PortUseWitness.alignedWith_edge_iff hAligned output input

end Alignmentend Cortex.Wire

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

← PreviousCortex.Pulse.Validity Next →Cortex.Wire.Admission