Cortex.Wire.Make
Imports
import Cortex.Wire.PortLinearityOverview
Proof-facing make(N, K) construction for the source linear port algebra.
Context
ADR 0048 makes make(N, K) a compile-time elaboration form, not a runtime
operator. This module models the proof-side witness that such elaboration
produces: a finite family of fresh child nodes with open node-port resources.
The linearity content is inherited from LinearPortObject.nodePorts. The
interesting make-specific obligation is identity discipline: generated nodes
belong to one binding namespace, and distinct binding namespaces give disjoint
source domains for later overlay.
namespace Cortex.Wirenamespace LinearPortGraphvariable {binding node outputPort inputPort : Type}variable {nodeBinding : node → binding}variable [DecidableEq node]variable [DecidableEq outputPort]variable [DecidableEq inputPort]Domain Disjointness From Node Disjointness
Node disjointness implies output-endpoint disjointness by endpoint ownership.
theorem outputDisjoint_of_nodeDisjoint
(left right : LinearPortGraph node outputPort inputPort)
(hNodeDisjoint : NodeDisjoint left right) :
OutputDisjoint left right := node:TypeoutputPort:TypeinputPort:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortleft:LinearPortGraph node outputPort inputPortright:LinearPortGraph node outputPort inputPorthNodeDisjoint:left.NodeDisjoint right⊢ left.OutputDisjoint right
intro output node:TypeoutputPort:TypeinputPort:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortleft:LinearPortGraph node outputPort inputPortright:LinearPortGraph node outputPort inputPorthNodeDisjoint:left.NodeDisjoint rightoutput:SourcePortInstance node outputPorthLeft:output ∈ left.outputs⊢ output ∈ right.outputs → False node:TypeoutputPort:TypeinputPort:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortleft:LinearPortGraph node outputPort inputPortright:LinearPortGraph node outputPort inputPorthNodeDisjoint:left.NodeDisjoint rightoutput:SourcePortInstance node outputPorthLeft:output ∈ left.outputshRight:output ∈ right.outputs⊢ False
All goals completed! 🐙Node disjointness implies input-endpoint disjointness by endpoint ownership.
theorem inputDisjoint_of_nodeDisjoint
(left right : LinearPortGraph node outputPort inputPort)
(hNodeDisjoint : NodeDisjoint left right) :
InputDisjoint left right := node:TypeoutputPort:TypeinputPort:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortleft:LinearPortGraph node outputPort inputPortright:LinearPortGraph node outputPort inputPorthNodeDisjoint:left.NodeDisjoint right⊢ left.InputDisjoint right
intro input node:TypeoutputPort:TypeinputPort:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortleft:LinearPortGraph node outputPort inputPortright:LinearPortGraph node outputPort inputPorthNodeDisjoint:left.NodeDisjoint rightinput:SourcePortInstance node inputPorthLeft:input ∈ left.inputs⊢ input ∈ right.inputs → False node:TypeoutputPort:TypeinputPort:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortleft:LinearPortGraph node outputPort inputPortright:LinearPortGraph node outputPort inputPorthNodeDisjoint:left.NodeDisjoint rightinput:SourcePortInstance node inputPorthLeft:input ∈ left.inputshRight:input ∈ right.inputs⊢ False
All goals completed! 🐙Node disjointness is enough to supply the full overlay domain-disjointness certificate.
theorem domainDisjoint_of_nodeDisjoint
(left right : LinearPortGraph node outputPort inputPort)
(hNodeDisjoint : NodeDisjoint left right) :
DomainDisjoint left right :=
⟨ hNodeDisjoint
, outputDisjoint_of_nodeDisjoint left right hNodeDisjoint
, inputDisjoint_of_nodeDisjoint left right hNodeDisjoint
⟩Make Witnesses
MakeWitness is the proof-side identity witness for one make(N, K) expansion.
The witness does not model the parser or kind expander. It records the finite source graph produced by expansion, the binding namespace that owns generated nodes, and the child-node indexing evidence that ADR 0048 requires from the identity scheme.
The fields split into identity data (sourceBinding, nodes, outputs, inputs, and their node
invariants), binding namespace evidence (nodeBinding_eq), and indexing data (count,
childNode, child port families, exactness lemmas, and injectivity). The bijection between
Fin count and generated nodes is established by childNode_mem, nodes_exact, and
childNode_inj together.
structure MakeWitness (binding node outputPort inputPort : Type)
[DecidableEq node]
[DecidableEq outputPort]
[DecidableEq inputPort]
(nodeBinding : node → binding) whereSource binding that names this generated family.
sourceBinding : bindingGenerated source nodes.
nodes : Finset nodeGenerated source output ports.
outputs : Finset (SourcePortInstance node outputPort)Generated source input ports.
inputs : Finset (SourcePortInstance node inputPort)Every generated output belongs to a generated node.
output_nodes : ∀ output, output ∈ outputs → output.node ∈ nodesEvery generated input belongs to a generated node.
input_nodes : ∀ input, input ∈ inputs → input.node ∈ nodesEvery generated node belongs to this witness's binding namespace.
nodeBinding_eq : ∀ graphNode, graphNode ∈ nodes → nodeBinding graphNode = sourceBinding
ADR 0048's N: the post-elaboration static expansion count.
count : NatSource-stable child node for each generated index.
childNode : Fin count → nodeKind-derived output labels instantiated for each generated child.
childOutputPorts : Fin count → Finset outputPortKind-derived input labels instantiated for each generated child.
childInputPorts : Fin count → Finset inputPortEach indexed child is present in the generated node set.
childNode_mem : ∀ index, childNode index ∈ nodesEvery generated node is one of the indexed children.
nodes_exact : ∀ graphNode, graphNode ∈ nodes → ∃ index, childNode index = graphNodeThe generated output port set is exactly the kind-derived ports for each child.
outputs_exact :
∀ output,
output ∈ outputs ↔
∃ index port,
port ∈ childOutputPorts index ∧
output = { node := childNode index, port := port }The generated input port set is exactly the kind-derived ports for each child.
inputs_exact :
∀ input,
input ∈ inputs ↔
∃ index port,
port ∈ childInputPorts index ∧
input = { node := childNode index, port := port }Generated child identities are injective in their index.
childNode_inj : Function.Injective childNodenamespace MakeWitness
The source object produced by a certified make(N, K) expansion.
def toObject
(witness : MakeWitness binding node outputPort inputPort nodeBinding) :
LinearPortObject node outputPort inputPort :=
LinearPortObject.nodePorts
witness.nodes
witness.outputs
witness.inputs
witness.output_nodes
witness.input_nodesDistinct make bindings have disjoint generated node domains.
theorem nodeDisjoint_of_distinctBindings
(left right : MakeWitness binding node outputPort inputPort nodeBinding)
(hDistinct : left.sourceBinding ≠ right.sourceBinding) :
NodeDisjoint left.toObject.graph right.toObject.graph := binding:Typenode:TypeoutputPort:TypeinputPort:TypenodeBinding:node → bindinginst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortleft:MakeWitness binding node outputPort inputPort nodeBindingright:MakeWitness binding node outputPort inputPort nodeBindinghDistinct:left.sourceBinding ≠ right.sourceBinding⊢ left.toObject.graph.NodeDisjoint right.toObject.graph
intro graphNode binding:Typenode:TypeoutputPort:TypeinputPort:TypenodeBinding:node → bindinginst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortleft:MakeWitness binding node outputPort inputPort nodeBindingright:MakeWitness binding node outputPort inputPort nodeBindinghDistinct:left.sourceBinding ≠ right.sourceBindinggraphNode:nodehLeft:graphNode ∈ left.toObject.graph.nodes⊢ graphNode ∈ right.toObject.graph.nodes → False binding:Typenode:TypeoutputPort:TypeinputPort:TypenodeBinding:node → bindinginst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortleft:MakeWitness binding node outputPort inputPort nodeBindingright:MakeWitness binding node outputPort inputPort nodeBindinghDistinct:left.sourceBinding ≠ right.sourceBindinggraphNode:nodehLeft:graphNode ∈ left.toObject.graph.nodeshRight:graphNode ∈ right.toObject.graph.nodes⊢ False
have hLeftNode : graphNode ∈ left.nodes := binding:Typenode:TypeoutputPort:TypeinputPort:TypenodeBinding:node → bindinginst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortleft:MakeWitness binding node outputPort inputPort nodeBindingright:MakeWitness binding node outputPort inputPort nodeBindinghDistinct:left.sourceBinding ≠ right.sourceBinding⊢ left.toObject.graph.NodeDisjoint right.toObject.graph
All goals completed! 🐙
have hRightNode : graphNode ∈ right.nodes := binding:Typenode:TypeoutputPort:TypeinputPort:TypenodeBinding:node → bindinginst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortleft:MakeWitness binding node outputPort inputPort nodeBindingright:MakeWitness binding node outputPort inputPort nodeBindinghDistinct:left.sourceBinding ≠ right.sourceBinding⊢ left.toObject.graph.NodeDisjoint right.toObject.graph
All goals completed! 🐙
binding:Typenode:TypeoutputPort:TypeinputPort:TypenodeBinding:node → bindinginst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortleft:MakeWitness binding node outputPort inputPort nodeBindingright:MakeWitness binding node outputPort inputPort nodeBindinghDistinct:left.sourceBinding ≠ right.sourceBindinggraphNode:nodehLeft:graphNode ∈ left.toObject.graph.nodeshRight:graphNode ∈ right.toObject.graph.nodeshLeftNode:graphNode ∈ left.nodeshRightNode:graphNode ∈ right.nodeshLeftBinding:nodeBinding graphNode = left.sourceBinding⊢ False
binding:Typenode:TypeoutputPort:TypeinputPort:TypenodeBinding:node → bindinginst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortleft:MakeWitness binding node outputPort inputPort nodeBindingright:MakeWitness binding node outputPort inputPort nodeBindinghDistinct:left.sourceBinding ≠ right.sourceBindinggraphNode:nodehLeft:graphNode ∈ left.toObject.graph.nodeshRight:graphNode ∈ right.toObject.graph.nodeshLeftNode:graphNode ∈ left.nodeshRightNode:graphNode ∈ right.nodeshLeftBinding:nodeBinding graphNode = left.sourceBindinghRightBinding:nodeBinding graphNode = right.sourceBinding⊢ False
All goals completed! 🐙Distinct make bindings have disjoint overlay domains.
theorem make_disjoint_of_distinctBindings
(left right : MakeWitness binding node outputPort inputPort nodeBinding)
(hDistinct : left.sourceBinding ≠ right.sourceBinding) :
DomainDisjoint left.toObject.graph right.toObject.graph :=
domainDisjoint_of_nodeDisjoint
left.toObject.graph
right.toObject.graph
(nodeDisjoint_of_distinctBindings left right hDistinct)end MakeWitnessend LinearPortGraphend Cortex.Wire