Cortex.Wire.GeneratedForms

proofs

On this page

Overview
Context
Theorem Split
Generated Name Policy
Default Prefixed-Index Carrier
Generated Form Diagnostics
Make Items For makeEach
Kind-Instantiated Child Frontiers
make(N, K) Admission
makeEach(items, K) Admission
* (Star) Admission

Imports

import Mathlib.Data.Fintype.Basic
import Cortex.Wire.PortLinearity
import Cortex.Wire.Make
import Cortex.Wire.PhantomAdapter
import Cortex.Wire.ElaborationIR

Overview

Source-linearity admission for Wire's three generated graph forms.

Context

ADR 0048 introduces make(N, K), ADR 0051 introduces makeEach(items, K), ADR 0049 introduces record-form *, and ADR 0052 generalizes * to finite product adapters. None of the three forms is admitted as a runtime operator: each elaborates at compile time to ordinary structure inside the closed source linear-port algebra of Cortex.Wire.PortLinearity.

This module is the integration point that turns the carriers in Cortex.Wire.Make and Cortex.Wire.PhantomAdapter into named admission functions targeted at LinearPortObject. Each function returns either a diagnostic from a small named sum, or a certified LinearPortObject. No admission decision is hardcoded against any specific identity scheme. Generated node identities come through the abstract GeneratedNamePolicy; the Haskell side will supply a concrete instance later.

Theorem Split

GeneratedNamePolicy is the identity-scheme abstraction. prefixedIndex is the default ADR 0048 name-policy: <binding>_<index>. KindInstantiatedFrontiers is the kind-expansion handoff: callers substitute the generated PortLabel and any static Value parameters, then supply exact per-child frontiers indexed by the AcceptedKindDecl that was instantiated. Make.accept, MakeEach.accept, and Star.accept are the three admission entry points; they return Except <Error> (LinearPortObject ...). The work of overlay, contraction, and phantom synthesis is delegated to MakeWitness and PhantomAdapterWitness in the dependent modules; this file does not reprove what those carriers already establish.

              namespace Cortex.Wirenamespace LinearPortGraphopen Cortex.Wire.ElaborationIRvariable {binding node outputPort inputPort productContract label : Type}variable [DecidableEq node]variable [DecidableEq outputPort]variable [DecidableEq inputPort]

Generated Name Policy

GeneratedNamePolicy abstracts how generated children of a binding receive stable identities.

ADR 0048 fixes one identity scheme (<binding>_<index>) for emitted Haskell. The proof side does not commit to that exact scheme: the policy supplies an opaque per-binding indexing function plus the injectivity and binding-namespace facts that MakeWitness requires. The Haskell side is free to instantiate this with the concrete ADR 0048 hash.

structure GeneratedNamePolicy
    (binding node : Type)
    (nodeBinding : node → binding) where

Generated child node for one binding-and-index pair.

childNode : binding → Nat → node

Distinct indices under one binding produce distinct generated nodes.

  childNode_injective :
    ∀ (sourceBinding : binding) {left right : Nat},
      childNode sourceBinding left = childNode sourceBinding right → left = right

Every generated child belongs to its binding's namespace under the supplied projection.

  childNode_binding :
    ∀ (sourceBinding : binding) (index : Nat),
      nodeBinding (childNode sourceBinding index) = sourceBinding

namespace GeneratedNamePolicy

The per-binding child indexing function viewed at a fixed binding and a count.

def childIndex
    (policy : GeneratedNamePolicy binding node nodeBinding)
    (sourceBinding : binding)
    {count : Nat}
    (index : Fin count) :
    node :=
  policy.childNode sourceBinding index.val

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

Fixed-binding child indexing is injective on its index domain.

theorem childIndex_injective
    (policy : GeneratedNamePolicy binding node nodeBinding)
    (sourceBinding : binding)
    {count : Nat} :
    Function.Injective (policy.childIndex sourceBinding (count := count)) := bybinding:Typenode:TypenodeBinding:node → bindingpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕ⊢ Function.Injective (policy.childIndex sourceBinding)
  intro left rightbinding:Typenode:TypenodeBinding:node → bindingpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕleft:Fin countright:Fin count⊢ policy.childIndex sourceBinding left = policy.childIndex sourceBinding right → left = right hEqbinding:Typenode:TypenodeBinding:node → bindingpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕleft:Fin countright:Fin counthEq:policy.childIndex sourceBinding left = policy.childIndex sourceBinding right⊢ left = right
  have hVal : left.val = right.val :=
    policy.childNode_injective sourceBinding hEqbinding:Typenode:TypenodeBinding:node → bindingpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕleft:Fin countright:Fin counthEq:policy.childIndex sourceBinding left = policy.childIndex sourceBinding righthVal:↑left = ↑right⊢ left = right
  exact Fin.ext hValAll goals completed! 🐙

end GeneratedNamePolicy

Default Prefixed-Index Carrier

ADR 0048's default identity scheme <binding>_<index>.

The proof side keeps the suffix encoding opaque so the Haskell elaborator can pick its own deterministic serialization without invalidating the proof. The string-side injectivity of prefixedIndexNodeId (cancellation through binding-prefix-and-_) is supplied as carrier data: because Lean's standard library does not expose a String.append_left_cancel lemma, callers prove this once for their chosen suffix encoder and once for their binding-name discipline.

This module does not commit to one encoder. The carrier is the public seam between the proof side and the Haskell elaborator's identity scheme.

def prefixedIndexNodeId
    (suffix : Nat → String)
    (sourceBinding : ElaborationIR.BindingName)
    (index : Nat) :
    ElaborationIR.NodeId :=
  { name := sourceBinding.name ++ "_" ++ suffix index }

Carrier collecting the obligations that turn prefixedIndexNodeId into a GeneratedNamePolicy.

prefixed_injective is supplied directly because the Lean standard library lacks a String.append_left_cancel lemma. Concrete carriers prove it from their chosen encoder.

structure PrefixedIndexCarrier where

Deterministic encoding from indices to suffix strings.

suffix : Nat → String

The opaque projection from generated nodes back to their owning binding.

nodeBinding : ElaborationIR.NodeId → ElaborationIR.BindingName

Every prefixed node projects back to its binding.

  prefixed_binding :
    ∀ (sourceBinding : ElaborationIR.BindingName) (index : Nat),
      nodeBinding (prefixedIndexNodeId suffix sourceBinding index) = sourceBinding

Distinct indices at one binding produce distinct prefixed nodes.

  prefixed_injective :
    ∀ (sourceBinding : ElaborationIR.BindingName) {left right : Nat},
      prefixedIndexNodeId suffix sourceBinding left =
          prefixedIndexNodeId suffix sourceBinding right →
        left = right

Default GeneratedNamePolicy derived from a PrefixedIndexCarrier.

def prefixedIndexPolicy (carrier : PrefixedIndexCarrier) :
    GeneratedNamePolicy ElaborationIR.BindingName ElaborationIR.NodeId carrier.nodeBinding where
  childNode := prefixedIndexNodeId carrier.suffix
  childNode_injective := carrier.prefixed_injective
  childNode_binding := carrier.prefixed_binding

Generated Form Diagnostics

Reasons a make(N, K) admission can be rejected at the source-linearity layer.

Make.accept consumes an already-proved KindSupportsMake witness, so it does not branch over these constructors directly. They are reserved for the front-end admission pass that constructs that witness from source kinds.

inductive MakeError where

The kind exposes no PortLabel parameter to drive per-child instantiation.

| missingPortLabel (binding : ElaborationIR.BindingName) (kind : ElaborationIR.KindName)

The kind exposes more than one PortLabel parameter, which make cannot resolve.

| multiplePortLabels (binding : ElaborationIR.BindingName) (kind : ElaborationIR.KindName)

The static count is malformed. ADR 0048 only accepts a non-negative integer literal.

  | invalidCount (binding : ElaborationIR.BindingName)
  deriving DecidableEq, Repr

Reasons a makeEach(items, K) admission can be rejected at the source-linearity layer.

MakeEach.accept consumes KindSupportsMakeEach; the missing/multiple PortLabel diagnostics belong to the front-end pass that constructs that witness. This module emits only item-label diagnostics directly.

inductive MakeEachError where

The static items list contained a duplicate generated label.

  | duplicateGeneratedLabel
      (binding : ElaborationIR.BindingName)
      (label : ElaborationIR.FieldLabel)

The kind exposes no PortLabel parameter to drive per-item instantiation.

| missingPortLabel (binding : ElaborationIR.BindingName) (kind : ElaborationIR.KindName)

The kind exposes more than one PortLabel parameter, which makeEach cannot resolve.

| multiplePortLabels (binding : ElaborationIR.BindingName) (kind : ElaborationIR.KindName)

A static item produced an empty or otherwise invalid label.

  | invalidItemLabel (binding : ElaborationIR.BindingName) (label : ElaborationIR.FieldLabel)
  deriving DecidableEq, Repr

Reasons a * admission can be rejected at the source-linearity layer.

inductive StarError where

The singular side did not expose a finite product contract.

| nonProductSingularSide (contract : ElaborationIR.ContractId)

The multi-side label set did not match a nominal record's field labels.

  | nominalRecordFieldMismatch
      (contract : ElaborationIR.ContractId)
      (recordFields : List ElaborationIR.FieldLabel)
      (multiLabels : List ElaborationIR.FieldLabel)

The multi-side arity did not match the bounded indexed product count.

  | indexedArityMismatch
      (contract : ElaborationIR.ContractId)
      (expected observed : Nat)

One indexed multi-side endpoint carried the wrong element contract.

  | indexedContractMismatch
      (expected observed : ElaborationIR.ContractId)

The indexed multi-side repeated a label/contract endpoint key.

  | duplicateIndexedEndpoint
      (label : ElaborationIR.FieldLabel)
      (contract : ElaborationIR.ContractId)

Phantom synthesis would produce a port clash with one of the operands.

  | phantomPortClash
  deriving DecidableEq, Repr

Make Items For `makeEach`

One static-list item presented to makeEach.

ADR 0051 derives this from include-resolved values: directory entries with a label field, plain strings, or homogeneous record items. The proof carrier keeps only the generated label and a parallel StaticValue payload that downstream consumers can use for kind parameter binding.

structure MakeItem where

Source-stable label that names the generated child.

label : ElaborationIR.FieldLabel

Optional original static value for kinds that take a Value parameter.

value : Option ElaborationIR.StaticValuenamespace MakeItem

A makeEach item has a locally valid generated label.

def Valid (item : MakeItem) : Prop :=
  item.label.Valid

instance validDecidable (item : MakeItem) : Decidable item.Valid :=
  inferInstanceAs (Decidable item.label.Valid)

Every generated label in a makeEach item list is locally valid.

def ItemsValid (items : List MakeItem) : Prop :=
  ∀ item, item ∈ items → item.Valid

instance itemsValidDecidable (items : List MakeItem) :
    Decidable (MakeItem.ItemsValid items) :=
  inferInstanceAs (Decidable (∀ item, item ∈ items → item.Valid))

A list of make-items has no duplicate labels.

def LabelsUnique (items : List MakeItem) : Prop :=
  (items.map MakeItem.label).Nodup

LabelsUnique is decidable because FieldLabel has decidable equality.

instance labelsUniqueDecidable (items : List MakeItem) :
    Decidable (MakeItem.LabelsUnique items) :=
  inferInstanceAs (Decidable (items.map MakeItem.label).Nodup)

end MakeItem

Kind-Instantiated Child Frontiers

Default generated port label for make(N, K) children.

This mirrors the source-facing <binding>_<index> convention at the port-label level. Name freshness for graph nodes is handled by GeneratedNamePolicy; this label helper only pins the generated frontier labels used by the kind substitution witness.

The helper is not an injectivity proof: it uses ordinary string concatenation. Callers that rely on generated label distinctness must carry a separate MakeItem.LabelsUnique witness or prove injectivity from their chosen binding/index grammar.

def makeIndexLabel
    (sourceBinding : BindingName)
    (index : Nat) :
    FieldLabel :=
  ⟨sourceBinding.name ++ "_" ++ toString index⟩

Generated nodes for one binding under a name policy.

def generatedNodes
    {nodeBinding : node → binding}
    (policy : GeneratedNamePolicy binding node nodeBinding)
    (sourceBinding : binding)
    (count : Nat) :
    Finset node :=
  (Finset.univ : Finset (Fin count)).image (policy.childIndex sourceBinding)

Concrete child frontiers after a reusable kind has been instantiated.

This is the proof-side handoff from kind-parameter substitution to source-linearity admission. Haskell already substitutes PortLabel/Value parameters before lowering; Lean receives the result as exact generated output/input port sets plus the per-child port families that MakeWitness needs. The accepted kind is a type index, not data used during projection: this prevents callers from pairing KindSupportsMake evidence for one kind with frontiers produced for another kind.

The child frontier fields are also tied back to the kind's accepted template frontier: each generated child receives one input/output port per template port, preserving the template contract and replacing the authored label with the generated child label. The KindSupportsMake/KindSupportsMakeEach preconditions on the admission entry points prove that those authored labels are exactly the kind's PortLabel formal, so replacement is parameter substitution rather than arbitrary label overwrite.

structure KindInstantiatedFrontiers
    (kind : AcceptedKindDecl)
    {nodeBinding : node → binding}
    (policy : GeneratedNamePolicy binding node nodeBinding)
    (sourceBinding : binding)
    (count : Nat) where

Generated source port label for each child instance.

childLabel : Fin count → FieldLabel

Concrete generated output instances after kind substitution.

outputs : Finset (SourcePortInstance node OutputPortSignature)

Concrete generated input instances after kind substitution.

inputs : Finset (SourcePortInstance node InputPortSignature)

Per-child output ports after substituting the generated PortLabel.

childOutputPorts : Fin count → Finset OutputPortSignature

Per-child input ports after substituting the generated PortLabel.

childInputPorts : Fin count → Finset InputPortSignature

Per-child output ports are exactly the kind template outputs with the generated label.

  childOutputPorts_exact :
    ∀ index port,
      port ∈ childOutputPorts index ↔
        ∃ template,
          template ∈ kind.outputPorts ∧
            port.signature =
              { label := childLabel index
                contract := template.contract }

Per-child input ports are exactly the kind template inputs with the generated label.

  childInputPorts_exact :
    ∀ index port,
      port ∈ childInputPorts index ↔
        ∃ template,
          template ∈ kind.inputs ∧
            port.signature =
              { label := childLabel index
                contract := template.contract }

Every generated output belongs to a generated child node.

  output_nodes :
    ∀ output,
      output ∈ outputs →
        output.node ∈ generatedNodes policy sourceBinding count

Every generated input belongs to a generated child node.

  input_nodes :
    ∀ input,
      input ∈ inputs →
        input.node ∈ generatedNodes policy sourceBinding count

The output set exactly reflects the per-child output ports.

  outputs_exact :
    ∀ output,
      output ∈ outputs ↔
        ∃ index port,
          port ∈ childOutputPorts index ∧
            output = { node := policy.childIndex sourceBinding index, port := port }

The input set exactly reflects the per-child input ports.

  inputs_exact :
    ∀ input,
      input ∈ inputs ↔
        ∃ index port,
          port ∈ childInputPorts index ∧
            input = { node := policy.childIndex sourceBinding index, port := port }

namespace KindInstantiatedFrontiers

Convert already-instantiated child frontiers into the canonical MakeWitness.

def toMakeWitness
    {nodeBinding : node → binding}
    {kind : AcceptedKindDecl}
    {policy : GeneratedNamePolicy binding node nodeBinding}
    {sourceBinding : binding}
    {count : Nat}
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := node)) :
    MakeWitness binding node OutputPortSignature InputPortSignature nodeBinding where
  sourceBinding := sourceBinding
  nodes := generatedNodes policy sourceBinding count
  outputs := frontiers.outputs
  inputs := frontiers.inputs
  output_nodes := frontiers.output_nodes
  input_nodes := frontiers.input_nodes
  nodeBinding_eq := bybinding:Typenode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortnodeBinding:node → bindingkind:AcceptedKindDeclpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding count⊢ ∀ graphNode ∈ generatedNodes policy sourceBinding count, nodeBinding graphNode = sourceBinding
    intro graphNode hGraphNodebinding:Typenode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortnodeBinding:node → bindingkind:AcceptedKindDeclpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding countgraphNode:nodehGraphNode:graphNode ∈ generatedNodes policy sourceBinding count⊢ nodeBinding graphNode = sourceBinding
    rcases Finset.mem_image.mp hGraphNode with ⟨index, _hIndex, hEq⟩binding:Typenode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortnodeBinding:node → bindingkind:AcceptedKindDeclpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding countgraphNode:nodehGraphNode:graphNode ∈ generatedNodes policy sourceBinding countindex:Fin count_hIndex:index ∈ Finset.univhEq:policy.childIndex sourceBinding index = graphNode⊢ nodeBinding graphNode = sourceBinding
    have hBinding := policy.childNode_binding sourceBinding index.valbinding:Typenode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortnodeBinding:node → bindingkind:AcceptedKindDeclpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding countgraphNode:nodehGraphNode:graphNode ∈ generatedNodes policy sourceBinding countindex:Fin count_hIndex:index ∈ Finset.univhEq:policy.childIndex sourceBinding index = graphNodehBinding:nodeBinding (policy.childNode sourceBinding ↑index) = sourceBinding⊢ nodeBinding graphNode = sourceBinding
    have hChild :
        policy.childIndex sourceBinding index = policy.childNode sourceBinding index.val :=
      rflbinding:Typenode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortnodeBinding:node → bindingkind:AcceptedKindDeclpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding countgraphNode:nodehGraphNode:graphNode ∈ generatedNodes policy sourceBinding countindex:Fin count_hIndex:index ∈ Finset.univhEq:policy.childIndex sourceBinding index = graphNodehBinding:nodeBinding (policy.childNode sourceBinding ↑index) = sourceBindinghChild:policy.childIndex sourceBinding index = policy.childNode sourceBinding ↑index⊢ nodeBinding graphNode = sourceBinding
    rw [← hEq, hChild]binding:Typenode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortnodeBinding:node → bindingkind:AcceptedKindDeclpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding countgraphNode:nodehGraphNode:graphNode ∈ generatedNodes policy sourceBinding countindex:Fin count_hIndex:index ∈ Finset.univhEq:policy.childIndex sourceBinding index = graphNodehBinding:nodeBinding (policy.childNode sourceBinding ↑index) = sourceBindinghChild:policy.childIndex sourceBinding index = policy.childNode sourceBinding ↑index⊢ nodeBinding (policy.childNode sourceBinding ↑index) = sourceBinding
    exact hBindingAll goals completed! 🐙
  count := count
  childNode := policy.childIndex sourceBinding
  childOutputPorts := frontiers.childOutputPorts
  childInputPorts := frontiers.childInputPorts
  childNode_mem := bybinding:Typenode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortnodeBinding:node → bindingkind:AcceptedKindDeclpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding count⊢ ∀ (index : Fin count), policy.childIndex sourceBinding index ∈ generatedNodes policy sourceBinding count
    intro indexbinding:Typenode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortnodeBinding:node → bindingkind:AcceptedKindDeclpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding countindex:Fin count⊢ policy.childIndex sourceBinding index ∈ generatedNodes policy sourceBinding count
    exact Finset.mem_image.mpr ⟨index, Finset.mem_univ index, rfl⟩All goals completed! 🐙
  nodes_exact := bybinding:Typenode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortnodeBinding:node → bindingkind:AcceptedKindDeclpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding count⊢ ∀ graphNode ∈ generatedNodes policy sourceBinding count, ∃ index, policy.childIndex sourceBinding index = graphNode
    intro graphNode hGraphNodebinding:Typenode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortnodeBinding:node → bindingkind:AcceptedKindDeclpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding countgraphNode:nodehGraphNode:graphNode ∈ generatedNodes policy sourceBinding count⊢ ∃ index, policy.childIndex sourceBinding index = graphNode
    rcases Finset.mem_image.mp hGraphNode with ⟨index, _hIndex, hEq⟩binding:Typenode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortnodeBinding:node → bindingkind:AcceptedKindDeclpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding countgraphNode:nodehGraphNode:graphNode ∈ generatedNodes policy sourceBinding countindex:Fin count_hIndex:index ∈ Finset.univhEq:policy.childIndex sourceBinding index = graphNode⊢ ∃ index, policy.childIndex sourceBinding index = graphNode
    exact ⟨index, hEq⟩All goals completed! 🐙
  outputs_exact := frontiers.outputs_exact
  inputs_exact := frontiers.inputs_exact
  childNode_inj := policy.childIndex_injective sourceBinding

Kind-instantiated child frontiers produce a source-linear object.

theorem toMakeWitness_portLinear
    {nodeBinding : node → binding}
    {kind : AcceptedKindDecl}
    {policy : GeneratedNamePolicy binding node nodeBinding}
    {sourceBinding : binding}
    {count : Nat}
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := node)) :
    frontiers.toMakeWitness.toObject.graph.PortLinear :=
  frontiers.toMakeWitness.toObject.linear

The source-linear object built from kind-instantiated frontiers exposes exactly the generated output instances promised by the witness.

theorem toMakeWitness_toObject_outputs_exact
    {nodeBinding : node → binding}
    {kind : AcceptedKindDecl}
    {policy : GeneratedNamePolicy binding node nodeBinding}
    {sourceBinding : binding}
    {count : Nat}
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := node)) :
    ∀ output,
      output ∈ frontiers.toMakeWitness.toObject.graph.outputs ↔
        ∃ index port,
          port ∈ frontiers.childOutputPorts index ∧
            output = { node := policy.childIndex sourceBinding index, port := port } := bybinding:Typenode:Typeinst✝:DecidableEq nodenodeBinding:node → bindingkind:AcceptedKindDeclpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding count⊢ ∀ (output : SourcePortInstance node OutputPortSignature),
  output ∈ frontiers.toMakeWitness.toObject.graph.outputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childOutputPorts index,
        output = { node := policy.childIndex sourceBinding index, port := port }
  simpa
    [KindInstantiatedFrontiers.toMakeWitness, MakeWitness.toObject,
      LinearPortObject.nodePorts, openNodePorts]
    using frontiers.outputs_exactAll goals completed! 🐙

The source-linear object built from kind-instantiated frontiers exposes exactly the generated input instances promised by the witness.

theorem toMakeWitness_toObject_inputs_exact
    {nodeBinding : node → binding}
    {kind : AcceptedKindDecl}
    {policy : GeneratedNamePolicy binding node nodeBinding}
    {sourceBinding : binding}
    {count : Nat}
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := node)) :
    ∀ input,
      input ∈ frontiers.toMakeWitness.toObject.graph.inputs ↔
        ∃ index port,
          port ∈ frontiers.childInputPorts index ∧
            input = { node := policy.childIndex sourceBinding index, port := port } := bybinding:Typenode:Typeinst✝:DecidableEq nodenodeBinding:node → bindingkind:AcceptedKindDeclpolicy:GeneratedNamePolicy binding node nodeBindingsourceBinding:bindingcount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding count⊢ ∀ (input : SourcePortInstance node InputPortSignature),
  input ∈ frontiers.toMakeWitness.toObject.graph.inputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childInputPorts index, input = { node := policy.childIndex sourceBinding index, port := port }
  simpa
    [KindInstantiatedFrontiers.toMakeWitness, MakeWitness.toObject,
      LinearPortObject.nodePorts, openNodePorts]
    using frontiers.inputs_exactAll goals completed! 🐙

end KindInstantiatedFrontiers

`make(N, K)` Admission

namespace Make

Admit make(N, K) from a kind-instantiated frontier witness.

The AcceptedKindDecl.KindSupportsMake precondition pins the kind-parameter shape from ADR 0048. The caller supplies frontiers, which is the result of substituting each generated PortLabel into the kind's authored frontier. This function does not redo substitution; it turns the supplied exact child-frontier evidence into the canonical MakeWitness object.

The public admission function is intentionally Wire-specific: it targets the direction-tagged OutputPortSignature/InputPortSignature wrappers from ElaborationIR, so the accepted kind and the generated frontier witness live in the same IR vocabulary. The label witness pins make to the generated <binding>_<index> labels.

Because accept consumes KindSupportsMake and the label witness as preconditions, this function has no remaining rejection branch. MakeError is reserved for the front-end checker that constructs those witnesses.

def accept
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (_hKind : kind.KindSupportsMake)
    (count : Nat)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := NodeId))
    (_hLabels :
      ∀ index,
        frontiers.childLabel index = makeIndexLabel sourceBinding index.val) :
    Except MakeError (LinearPortObject NodeId OutputPortSignature InputPortSignature) :=
  Except.ok frontiers.toMakeWitness.toObject

Once kind-shape and label witnesses exist, make(N, K) admission is the canonical object and cannot emit a MakeError.

theorem accept_eq_ok
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (hKind : kind.KindSupportsMake)
    (count : Nat)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := NodeId))
    (hLabels :
      ∀ index,
        frontiers.childLabel index = makeIndexLabel sourceBinding index.val) :
    accept policy sourceBinding kind hKind count frontiers hLabels =
      Except.ok frontiers.toMakeWitness.toObject :=
  rfl

Make.accept never returns an error once its proof preconditions are supplied.

theorem accept_never_errors
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (hKind : kind.KindSupportsMake)
    (count : Nat)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := NodeId))
    (hLabels :
      ∀ index,
        frontiers.childLabel index = makeIndexLabel sourceBinding index.val)
    (error : MakeError) :
    accept policy sourceBinding kind hKind count frontiers hLabels ≠ Except.error error := bynodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑indexerror:MakeError⊢ accept policy sourceBinding kind hKind count frontiers hLabels ≠ Except.error error
  intro hErrornodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑indexerror:MakeErrorhError:accept policy sourceBinding kind hKind count frontiers hLabels = Except.error error⊢ False
  cases hErrorAll goals completed! 🐙

Successful make(N, K) admission returns exactly the supplied instantiated frontier object.

theorem accept_ok_eq
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (hKind : kind.KindSupportsMake)
    (count : Nat)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := NodeId))
    (hLabels :
      ∀ index,
        frontiers.childLabel index = makeIndexLabel sourceBinding index.val)
    (object : LinearPortObject NodeId OutputPortSignature InputPortSignature)
    (hAccept :
      accept policy sourceBinding kind hKind count frontiers hLabels = Except.ok object) :
    object = frontiers.toMakeWitness.toObject := bynodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑indexobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind count frontiers hLabels = Except.ok object⊢ object = frontiers.toMakeWitness.toObject
  unfold accept at hAcceptnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑indexobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:Except.ok frontiers.toMakeWitness.toObject = Except.ok object⊢ object = frontiers.toMakeWitness.toObject
  cases hAcceptreflnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑index⊢ frontiers.toMakeWitness.toObject = frontiers.toMakeWitness.toObject
  rflAll goals completed! 🐙

The make(N, K) frontier witness exposes the generated child-label equation.

theorem accept_childLabel_eq
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (count : Nat)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := NodeId))
    (hLabels :
      ∀ index,
        frontiers.childLabel index = makeIndexLabel sourceBinding index.val)
    (index : Fin count) :
    frontiers.childLabel index = makeIndexLabel sourceBinding index.val :=
  hLabels index

The make(N, K) frontier witness exposes exact generated output frontiers.

theorem accept_childOutputPorts_exact
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (count : Nat)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := NodeId)) :
    ∀ index port,
      port ∈ frontiers.childOutputPorts index ↔
        ∃ template,
          template ∈ kind.outputPorts ∧
            port.signature =
              { label := frontiers.childLabel index
                contract := template.contract } :=
  frontiers.childOutputPorts_exact

The make(N, K) frontier witness exposes exact generated input frontiers.

theorem accept_childInputPorts_exact
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (count : Nat)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := NodeId)) :
    ∀ index port,
      port ∈ frontiers.childInputPorts index ↔
        ∃ template,
          template ∈ kind.inputs ∧
            port.signature =
              { label := frontiers.childLabel index
                contract := template.contract } :=
  frontiers.childInputPorts_exact

Successful make(N, K) admission exposes the exact output instances on the returned object.

theorem accept_outputs_exact
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (hKind : kind.KindSupportsMake)
    (count : Nat)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := NodeId))
    (hLabels :
      ∀ index,
        frontiers.childLabel index = makeIndexLabel sourceBinding index.val)
    (object : LinearPortObject NodeId OutputPortSignature InputPortSignature)
    (hAccept :
      accept policy sourceBinding kind hKind count frontiers hLabels = Except.ok object) :
    ∀ output,
      output ∈ object.graph.outputs ↔
        ∃ index port,
          port ∈ frontiers.childOutputPorts index ∧
            output = { node := policy.childIndex sourceBinding index, port := port } := bynodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑indexobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind count frontiers hLabels = Except.ok object⊢ ∀ (output : SourcePortInstance NodeId OutputPortSignature),
  output ∈ object.graph.outputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childOutputPorts index,
        output = { node := policy.childIndex sourceBinding index, port := port }
  have hEq : object = frontiers.toMakeWitness.toObject :=
    accept_ok_eq policy sourceBinding kind hKind count frontiers hLabels object hAcceptnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑indexobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind count frontiers hLabels = Except.ok objecthEq:object = frontiers.toMakeWitness.toObject⊢ ∀ (output : SourcePortInstance NodeId OutputPortSignature),
  output ∈ object.graph.outputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childOutputPorts index,
        output = { node := policy.childIndex sourceBinding index, port := port }
  rw [hEq]nodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑indexobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind count frontiers hLabels = Except.ok objecthEq:object = frontiers.toMakeWitness.toObject⊢ ∀ (output : SourcePortInstance NodeId OutputPortSignature),
  output ∈ frontiers.toMakeWitness.toObject.graph.outputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childOutputPorts index,
        output = { node := policy.childIndex sourceBinding index, port := port }
  exact frontiers.toMakeWitness_toObject_outputs_exactAll goals completed! 🐙

Successful make(N, K) admission exposes the exact input instances on the returned object.

theorem accept_inputs_exact
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (hKind : kind.KindSupportsMake)
    (count : Nat)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := NodeId))
    (hLabels :
      ∀ index,
        frontiers.childLabel index = makeIndexLabel sourceBinding index.val)
    (object : LinearPortObject NodeId OutputPortSignature InputPortSignature)
    (hAccept :
      accept policy sourceBinding kind hKind count frontiers hLabels = Except.ok object) :
    ∀ input,
      input ∈ object.graph.inputs ↔
        ∃ index port,
          port ∈ frontiers.childInputPorts index ∧
            input = { node := policy.childIndex sourceBinding index, port := port } := bynodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑indexobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind count frontiers hLabels = Except.ok object⊢ ∀ (input : SourcePortInstance NodeId InputPortSignature),
  input ∈ object.graph.inputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childInputPorts index, input = { node := policy.childIndex sourceBinding index, port := port }
  have hEq : object = frontiers.toMakeWitness.toObject :=
    accept_ok_eq policy sourceBinding kind hKind count frontiers hLabels object hAcceptnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑indexobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind count frontiers hLabels = Except.ok objecthEq:object = frontiers.toMakeWitness.toObject⊢ ∀ (input : SourcePortInstance NodeId InputPortSignature),
  input ∈ object.graph.inputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childInputPorts index, input = { node := policy.childIndex sourceBinding index, port := port }
  rw [hEq]nodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑indexobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind count frontiers hLabels = Except.ok objecthEq:object = frontiers.toMakeWitness.toObject⊢ ∀ (input : SourcePortInstance NodeId InputPortSignature),
  input ∈ frontiers.toMakeWitness.toObject.graph.inputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childInputPorts index, input = { node := policy.childIndex sourceBinding index, port := port }
  exact frontiers.toMakeWitness_toObject_inputs_exactAll goals completed! 🐙

A successful make(N, K) admission carries source linearity.

theorem accept_portLinear
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (hKind : kind.KindSupportsMake)
    (count : Nat)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding count
        (node := NodeId))
    (hLabels :
      ∀ index,
        frontiers.childLabel index = makeIndexLabel sourceBinding index.val)
    (object : LinearPortObject NodeId OutputPortSignature InputPortSignature)
    (hAccept :
      accept policy sourceBinding kind hKind count frontiers hLabels = Except.ok object) :
    object.graph.PortLinear := bynodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑indexobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind count frontiers hLabels = Except.ok object⊢ object.graph.PortLinear
  unfold accept at hAcceptnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑indexobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:Except.ok frontiers.toMakeWitness.toObject = Except.ok object⊢ object.graph.PortLinear
  cases hAcceptreflnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakecount:ℕfrontiers:KindInstantiatedFrontiers kind policy sourceBinding counthLabels:∀ (index : Fin count), frontiers.childLabel index = makeIndexLabel sourceBinding ↑index⊢ frontiers.toMakeWitness.toObject.graph.PortLinear
  exact KindInstantiatedFrontiers.toMakeWitness_portLinear frontiersAll goals completed! 🐙

end Make

`makeEach(items, K)` Admission

namespace MakeEach

Validate makeEach items while tracking labels seen so far.

def acceptItemsWithSeen
    (sourceBinding : ElaborationIR.BindingName)
    (seen : List ElaborationIR.FieldLabel) :
    List MakeItem → Except MakeEachError (List MakeItem)
  | [] => Except.ok []
  | head :: tail =>
      if head.Valid then
        if head.label ∈ seen then
          Except.error (MakeEachError.duplicateGeneratedLabel sourceBinding head.label)
        else
          match acceptItemsWithSeen sourceBinding (head.label :: seen) tail with
          | Except.error error => Except.error error
          | Except.ok acceptedTail => Except.ok (head :: acceptedTail)
      else
        Except.error (MakeEachError.invalidItemLabel sourceBinding head.label)

Reject invalid or duplicate labels in a static makeEach item list.

def acceptItems
    (sourceBinding : ElaborationIR.BindingName)
    (items : List MakeItem) :
    Except MakeEachError (List MakeItem) :=
  acceptItemsWithSeen sourceBinding [] items

Valid, duplicate-free makeEach rows pass the item checker unchanged.

The auxiliary seen list is the accumulator used by acceptItemsWithSeen. The freshness premise says no remaining item label has already been seen.

theorem acceptItemsWithSeen_ok_eq_self
    (sourceBinding : ElaborationIR.BindingName)
    (seen : List ElaborationIR.FieldLabel) :
    ∀ items,
      MakeItem.ItemsValid items →
        MakeItem.LabelsUnique items →
          (∀ item, item ∈ items → item.label ∉ seen) →
            acceptItemsWithSeen sourceBinding seen items = Except.ok items := bysourceBinding:BindingNameseen:List FieldLabel⊢ ∀ (items : List MakeItem),
  MakeItem.ItemsValid items →
    MakeItem.LabelsUnique items →
      (∀ item ∈ items, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen items = Except.ok items
  intro itemssourceBinding:BindingNameseen:List FieldLabelitems:List MakeItem⊢ MakeItem.ItemsValid items →
  MakeItem.LabelsUnique items →
    (∀ item ∈ items, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen items = Except.ok items
  induction items generalizing seen with
  | nil =>nilsourceBinding:BindingNameseen:List FieldLabel⊢ MakeItem.ItemsValid [] →
  MakeItem.LabelsUnique [] → (∀ item ∈ [], item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen [] = Except.ok []
      intro _hValid _hUniquenilsourceBinding:BindingNameseen:List FieldLabel_hValid:MakeItem.ItemsValid []_hUnique:MakeItem.LabelsUnique []⊢ (∀ item ∈ [], item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen [] = Except.ok [] _hFreshnilsourceBinding:BindingNameseen:List FieldLabel_hValid:MakeItem.ItemsValid []_hUnique:MakeItem.LabelsUnique []_hFresh:∀ item ∈ [], item.label ∉ seen⊢ acceptItemsWithSeen sourceBinding seen [] = Except.ok []
      rflAll goals completed! 🐙
  | cons head tail ih =>conssourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabel⊢ MakeItem.ItemsValid (head :: tail) →
  MakeItem.LabelsUnique (head :: tail) →
    (∀ item ∈ head :: tail, item.label ∉ seen) →
      acceptItemsWithSeen sourceBinding seen (head :: tail) = Except.ok (head :: tail)
      intro hValid hUniqueconssourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)⊢ (∀ item ∈ head :: tail, item.label ∉ seen) →
  acceptItemsWithSeen sourceBinding seen (head :: tail) = Except.ok (head :: tail) hFreshconssourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seen⊢ acceptItemsWithSeen sourceBinding seen (head :: tail) = Except.ok (head :: tail)
      have hHeadValid : head.Valid :=
        hValid head (bysourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seen⊢ head ∈ head :: tail simpAll goals completed! 🐙)
      have hHeadFresh : head.label ∉ seen :=
        hFresh head (bysourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.Valid⊢ head ∈ head :: tail simpAll goals completed! 🐙)
      have hTailValid : MakeItem.ItemsValid tail := bysourceBinding:BindingNameseen:List FieldLabel⊢ ∀ (items : List MakeItem),
  MakeItem.ItemsValid items →
    MakeItem.LabelsUnique items →
      (∀ item ∈ items, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen items = Except.ok items
        intro item hItemsourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenitem:MakeItemhItem:item ∈ tail⊢ item.Valid
        exact hValid item (bysourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenitem:MakeItemhItem:item ∈ tail⊢ item ∈ head :: tail simp [hItem]All goals completed! 🐙)
      have hLabelsNodup :
          (head.label :: tail.map MakeItem.label).Nodup := bysourceBinding:BindingNameseen:List FieldLabel⊢ ∀ (items : List MakeItem),
  MakeItem.ItemsValid items →
    MakeItem.LabelsUnique items →
      (∀ item ∈ items, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen items = Except.ok items
        simpa [MakeItem.LabelsUnique] using hUniqueAll goals completed! 🐙
      have hTailUnique : MakeItem.LabelsUnique tail := bysourceBinding:BindingNameseen:List FieldLabel⊢ ∀ (items : List MakeItem),
  MakeItem.ItemsValid items →
    MakeItem.LabelsUnique items →
      (∀ item ∈ items, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen items = Except.ok items
        simpa [MakeItem.LabelsUnique] using hLabelsNodup.tailAll goals completed! 🐙
      have hHeadNotInTail : head.label ∉ tail.map MakeItem.label :=
        hLabelsNodup.notMemconssourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenhTailValid:MakeItem.ItemsValid tailhLabelsNodup:(head.label :: List.map MakeItem.label tail).NoduphTailUnique:MakeItem.LabelsUnique tailhHeadNotInTail:head.label ∉ List.map MakeItem.label tail⊢ acceptItemsWithSeen sourceBinding seen (head :: tail) = Except.ok (head :: tail)
      have hTailFresh :
          ∀ item, item ∈ tail → item.label ∉ head.label :: seen := bysourceBinding:BindingNameseen:List FieldLabel⊢ ∀ (items : List MakeItem),
  MakeItem.ItemsValid items →
    MakeItem.LabelsUnique items →
      (∀ item ∈ items, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen items = Except.ok items
        intro item hItemsourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenhTailValid:MakeItem.ItemsValid tailhLabelsNodup:(head.label :: List.map MakeItem.label tail).NoduphTailUnique:MakeItem.LabelsUnique tailhHeadNotInTail:head.label ∉ List.map MakeItem.label tailitem:MakeItemhItem:item ∈ tail⊢ item.label ∉ head.label :: seen hSeensourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenhTailValid:MakeItem.ItemsValid tailhLabelsNodup:(head.label :: List.map MakeItem.label tail).NoduphTailUnique:MakeItem.LabelsUnique tailhHeadNotInTail:head.label ∉ List.map MakeItem.label tailitem:MakeItemhItem:item ∈ tailhSeen:item.label ∈ head.label :: seen⊢ False
        rcases List.mem_cons.mp hSeen with hSame | hOldSeeninlsourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenhTailValid:MakeItem.ItemsValid tailhLabelsNodup:(head.label :: List.map MakeItem.label tail).NoduphTailUnique:MakeItem.LabelsUnique tailhHeadNotInTail:head.label ∉ List.map MakeItem.label tailitem:MakeItemhItem:item ∈ tailhSeen:item.label ∈ head.label :: seenhSame:item.label = head.label⊢ FalseinrsourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenhTailValid:MakeItem.ItemsValid tailhLabelsNodup:(head.label :: List.map MakeItem.label tail).NoduphTailUnique:MakeItem.LabelsUnique tailhHeadNotInTail:head.label ∉ List.map MakeItem.label tailitem:MakeItemhItem:item ∈ tailhSeen:item.label ∈ head.label :: seenhOldSeen:item.label ∈ seen⊢ False
        ·inlsourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenhTailValid:MakeItem.ItemsValid tailhLabelsNodup:(head.label :: List.map MakeItem.label tail).NoduphTailUnique:MakeItem.LabelsUnique tailhHeadNotInTail:head.label ∉ List.map MakeItem.label tailitem:MakeItemhItem:item ∈ tailhSeen:item.label ∈ head.label :: seenhSame:item.label = head.label⊢ False have hLabelMem : item.label ∈ tail.map MakeItem.label :=
            List.mem_map.mpr ⟨item, hItem, rfl⟩inlsourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenhTailValid:MakeItem.ItemsValid tailhLabelsNodup:(head.label :: List.map MakeItem.label tail).NoduphTailUnique:MakeItem.LabelsUnique tailhHeadNotInTail:head.label ∉ List.map MakeItem.label tailitem:MakeItemhItem:item ∈ tailhSeen:item.label ∈ head.label :: seenhSame:item.label = head.labelhLabelMem:item.label ∈ List.map MakeItem.label tail⊢ False
          exact hHeadNotInTail (bysourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenhTailValid:MakeItem.ItemsValid tailhLabelsNodup:(head.label :: List.map MakeItem.label tail).NoduphTailUnique:MakeItem.LabelsUnique tailhHeadNotInTail:head.label ∉ List.map MakeItem.label tailitem:MakeItemhItem:item ∈ tailhSeen:item.label ∈ head.label :: seenhSame:item.label = head.labelhLabelMem:item.label ∈ List.map MakeItem.label tail⊢ head.label ∈ List.map MakeItem.label tail rw [← hSame]sourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenhTailValid:MakeItem.ItemsValid tailhLabelsNodup:(head.label :: List.map MakeItem.label tail).NoduphTailUnique:MakeItem.LabelsUnique tailhHeadNotInTail:head.label ∉ List.map MakeItem.label tailitem:MakeItemhItem:item ∈ tailhSeen:item.label ∈ head.label :: seenhSame:item.label = head.labelhLabelMem:item.label ∈ List.map MakeItem.label tail⊢ item.label ∈ List.map MakeItem.label tail; exact hLabelMemAll goals completed! 🐙)
        ·inrsourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenhTailValid:MakeItem.ItemsValid tailhLabelsNodup:(head.label :: List.map MakeItem.label tail).NoduphTailUnique:MakeItem.LabelsUnique tailhHeadNotInTail:head.label ∉ List.map MakeItem.label tailitem:MakeItemhItem:item ∈ tailhSeen:item.label ∈ head.label :: seenhOldSeen:item.label ∈ seen⊢ False exact hFresh item (bysourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenhTailValid:MakeItem.ItemsValid tailhLabelsNodup:(head.label :: List.map MakeItem.label tail).NoduphTailUnique:MakeItem.LabelsUnique tailhHeadNotInTail:head.label ∉ List.map MakeItem.label tailitem:MakeItemhItem:item ∈ tailhSeen:item.label ∈ head.label :: seenhOldSeen:item.label ∈ seen⊢ item ∈ head :: tail simp [hItem]All goals completed! 🐙) hOldSeen
      have hTailAccept :
          acceptItemsWithSeen sourceBinding (head.label :: seen) tail = Except.ok tail :=
        ih (head.label :: seen) hTailValid hTailUnique hTailFreshconssourceBinding:BindingNamehead:MakeItemtail:List MakeItemih:∀ (seen : List FieldLabel),
  MakeItem.ItemsValid tail →
    MakeItem.LabelsUnique tail →
      (∀ item ∈ tail, item.label ∉ seen) → acceptItemsWithSeen sourceBinding seen tail = Except.ok tailseen:List FieldLabelhValid:MakeItem.ItemsValid (head :: tail)hUnique:MakeItem.LabelsUnique (head :: tail)hFresh:∀ item ∈ head :: tail, item.label ∉ seenhHeadValid:head.ValidhHeadFresh:head.label ∉ seenhTailValid:MakeItem.ItemsValid tailhLabelsNodup:(head.label :: List.map MakeItem.label tail).NoduphTailUnique:MakeItem.LabelsUnique tailhHeadNotInTail:head.label ∉ List.map MakeItem.label tailhTailFresh:∀ item ∈ tail, item.label ∉ head.label :: seenhTailAccept:acceptItemsWithSeen sourceBinding (head.label :: seen) tail = Except.ok tail⊢ acceptItemsWithSeen sourceBinding seen (head :: tail) = Except.ok (head :: tail)
      simp [acceptItemsWithSeen, hHeadValid, hHeadFresh, hTailAccept]All goals completed! 🐙

Valid, duplicate-free makeEach rows pass the public item checker unchanged.

theorem acceptItems_ok_eq_self
    (sourceBinding : ElaborationIR.BindingName)
    (items : List MakeItem)
    (hValid : MakeItem.ItemsValid items)
    (hUnique : MakeItem.LabelsUnique items) :
    acceptItems sourceBinding items = Except.ok items := bysourceBinding:BindingNameitems:List MakeItemhValid:MakeItem.ItemsValid itemshUnique:MakeItem.LabelsUnique items⊢ acceptItems sourceBinding items = Except.ok items
  unfold acceptItemssourceBinding:BindingNameitems:List MakeItemhValid:MakeItem.ItemsValid itemshUnique:MakeItem.LabelsUnique items⊢ acceptItemsWithSeen sourceBinding [] items = Except.ok items
  exact
    acceptItemsWithSeen_ok_eq_self
      sourceBinding
      []
      items
      hValid
      hUnique
      (bysourceBinding:BindingNameitems:List MakeItemhValid:MakeItem.ItemsValid itemshUnique:MakeItem.LabelsUnique items⊢ ∀ item ∈ items, item.label ∉ []
        intro item _hItemsourceBinding:BindingNameitems:List MakeItemhValid:MakeItem.ItemsValid itemshUnique:MakeItem.LabelsUnique itemsitem:MakeItem_hItem:item ∈ items⊢ item.label ∉ []
        simpAll goals completed! 🐙)

private def makeEachExampleBinding : ElaborationIR.BindingName := ⟨"workers"⟩

private def makeEachExampleItem : MakeItem :=
  { label := ⟨"worker_0"⟩
    value := none }

private def makeEachDuplicateItem : MakeItem :=
  { label := ⟨"worker_0"⟩
    value := none }

private def makeEachInvalidItem : MakeItem :=
  { label := ⟨""⟩
    value := none }

Invalid generated labels are rejected with the concrete offending label.

example :
    acceptItems makeEachExampleBinding [makeEachInvalidItem] =
      Except.error
        (MakeEachError.invalidItemLabel makeEachExampleBinding makeEachInvalidItem.label) := bybinding:Typenode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPort⊢ acceptItems makeEachExampleBinding [makeEachInvalidItem] =
  Except.error (MakeEachError.invalidItemLabel makeEachExampleBinding makeEachInvalidItem.label)
  rflAll goals completed! 🐙

Duplicate generated labels are rejected with the concrete duplicate label.

example :
    acceptItems makeEachExampleBinding [makeEachExampleItem, makeEachDuplicateItem] =
      Except.error
        (MakeEachError.duplicateGeneratedLabel
          makeEachExampleBinding
          makeEachDuplicateItem.label) := bybinding:Typenode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPort⊢ acceptItems makeEachExampleBinding [makeEachExampleItem, makeEachDuplicateItem] =
  Except.error (MakeEachError.duplicateGeneratedLabel makeEachExampleBinding makeEachDuplicateItem.label)
  rflAll goals completed! 🐙

Admit makeEach(items, K) from checked items and instantiated child frontiers.

The function still performs the source-level label checks over items: labels must be locally valid and duplicate-free. The kind-shape precondition requires either a generated PortLabel parameter or generated PortLabel plus static Value; the supplied frontiers is the exact post-substitution port family.

The checked item list is not stored in the returned object. Its relationship to the generated frontier is the explicit hLabels proof obligation, exposed for callers through accept_childLabel_eq. Missing/multiple PortLabel diagnostics are front-end obligations discharged before this entry point.

def accept
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (_hKind : kind.KindSupportsMakeEach)
    (items : List MakeItem)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding items.length
        (node := NodeId))
    (_hLabels :
      ∀ index,
        frontiers.childLabel index = (items.get index).label) :
    Except MakeEachError
      (LinearPortObject NodeId OutputPortSignature InputPortSignature) :=
  match acceptItems sourceBinding items with
  | Except.error error => Except.error error
  | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject

makeEach errors exactly when source item-label checking errors.

Kind-shape diagnostics are not produced by this function: callers must supply KindSupportsMakeEach before admission reaches this layer.

theorem accept_error_iff_acceptItems_error
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (hKind : kind.KindSupportsMakeEach)
    (items : List MakeItem)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding items.length
        (node := NodeId))
    (hLabels :
      ∀ index,
        frontiers.childLabel index = (items.get index).label)
    (error : MakeEachError) :
    accept policy sourceBinding kind hKind items frontiers hLabels = Except.error error ↔
      acceptItems sourceBinding items = Except.error error := bynodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachError⊢ accept policy sourceBinding kind hKind items frontiers hLabels = Except.error error ↔
  acceptItems sourceBinding items = Except.error error
  unfold acceptnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachError⊢ (match acceptItems sourceBinding items with
    | Except.error error => Except.error error
    | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject) =
    Except.error error ↔
  acceptItems sourceBinding items = Except.error error
  cases hItems : acceptItems sourceBinding items with
  | error itemError =>errornodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroritemError:MakeEachErrorhItems:acceptItems sourceBinding items = Except.error itemError⊢ (match Except.error itemError with
    | Except.error error => Except.error error
    | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject) =
    Except.error error ↔
  Except.error itemError = Except.error error
      change Except.error itemError = Except.error error ↔
        Except.error itemError = Except.error errorerrornodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroritemError:MakeEachErrorhItems:acceptItems sourceBinding items = Except.error itemError⊢ Except.error itemError = Except.error error ↔ Except.error itemError = Except.error error
      constructorerror.mpnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroritemError:MakeEachErrorhItems:acceptItems sourceBinding items = Except.error itemError⊢ Except.error itemError = Except.error error → Except.error itemError = Except.error errorerror.mprnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroritemError:MakeEachErrorhItems:acceptItems sourceBinding items = Except.error itemError⊢ Except.error itemError = Except.error error → Except.error itemError = Except.error error
      ·error.mpnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroritemError:MakeEachErrorhItems:acceptItems sourceBinding items = Except.error itemError⊢ Except.error itemError = Except.error error → Except.error itemError = Except.error error intro hErrorerror.mpnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroritemError:MakeEachErrorhItems:acceptItems sourceBinding items = Except.error itemErrorhError:Except.error itemError = Except.error error⊢ Except.error itemError = Except.error error
        cases hErrorerror.mp.reflnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErrorhItems:acceptItems sourceBinding items = Except.error error⊢ Except.error error = Except.error error
        rflAll goals completed! 🐙
      ·error.mprnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroritemError:MakeEachErrorhItems:acceptItems sourceBinding items = Except.error itemError⊢ Except.error itemError = Except.error error → Except.error itemError = Except.error error intro hErrorerror.mprnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroritemError:MakeEachErrorhItems:acceptItems sourceBinding items = Except.error itemErrorhError:Except.error itemError = Except.error error⊢ Except.error itemError = Except.error error
        cases hErrorerror.mpr.reflnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErrorhItems:acceptItems sourceBinding items = Except.error error⊢ Except.error error = Except.error error
        rflAll goals completed! 🐙
  | ok accepted =>oknodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroraccepted:List MakeItemhItems:acceptItems sourceBinding items = Except.ok accepted⊢ (match Except.ok accepted with
    | Except.error error => Except.error error
    | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject) =
    Except.error error ↔
  Except.ok accepted = Except.error error
      change Except.ok frontiers.toMakeWitness.toObject = Except.error error ↔
        Except.ok accepted = Except.error erroroknodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroraccepted:List MakeItemhItems:acceptItems sourceBinding items = Except.ok accepted⊢ Except.ok frontiers.toMakeWitness.toObject = Except.error error ↔ Except.ok accepted = Except.error error
      constructorok.mpnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroraccepted:List MakeItemhItems:acceptItems sourceBinding items = Except.ok accepted⊢ Except.ok frontiers.toMakeWitness.toObject = Except.error error → Except.ok accepted = Except.error errorok.mprnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroraccepted:List MakeItemhItems:acceptItems sourceBinding items = Except.ok accepted⊢ Except.ok accepted = Except.error error → Except.ok frontiers.toMakeWitness.toObject = Except.error error
      ·ok.mpnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroraccepted:List MakeItemhItems:acceptItems sourceBinding items = Except.ok accepted⊢ Except.ok frontiers.toMakeWitness.toObject = Except.error error → Except.ok accepted = Except.error error intro hErrorok.mpnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroraccepted:List MakeItemhItems:acceptItems sourceBinding items = Except.ok acceptedhError:Except.ok frontiers.toMakeWitness.toObject = Except.error error⊢ Except.ok accepted = Except.error error
        cases hErrorAll goals completed! 🐙
      ·ok.mprnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroraccepted:List MakeItemhItems:acceptItems sourceBinding items = Except.ok accepted⊢ Except.ok accepted = Except.error error → Except.ok frontiers.toMakeWitness.toObject = Except.error error intro hErrorok.mprnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelerror:MakeEachErroraccepted:List MakeItemhItems:acceptItems sourceBinding items = Except.ok acceptedhError:Except.ok accepted = Except.error error⊢ Except.ok frontiers.toMakeWitness.toObject = Except.error error
        cases hErrorAll goals completed! 🐙

Successful makeEach(items, K) admission returns the supplied frontier object.

theorem accept_ok_eq
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (hKind : kind.KindSupportsMakeEach)
    (items : List MakeItem)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding items.length
        (node := NodeId))
    (hLabels :
      ∀ index,
        frontiers.childLabel index = (items.get index).label)
    (object : LinearPortObject NodeId OutputPortSignature InputPortSignature)
    (hAccept :
      accept policy sourceBinding kind hKind items frontiers hLabels = Except.ok object) :
    object = frontiers.toMakeWitness.toObject := bynodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind items frontiers hLabels = Except.ok object⊢ object = frontiers.toMakeWitness.toObject
  unfold accept at hAcceptnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:(match acceptItems sourceBinding items with
  | Except.error error => Except.error error
  | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject) =
  Except.ok object⊢ object = frontiers.toMakeWitness.toObject
  cases hItems : acceptItems sourceBinding items with
  | error error =>errornodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:(match acceptItems sourceBinding items with
  | Except.error error => Except.error error
  | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject) =
  Except.ok objecterror:MakeEachErrorhItems:acceptItems sourceBinding items = Except.error error⊢ object = frontiers.toMakeWitness.toObject
      rw [hItems] at hAccepterrornodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignatureerror:MakeEachErrorhAccept:(match Except.error error with
  | Except.error error => Except.error error
  | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject) =
  Except.ok objecthItems:acceptItems sourceBinding items = Except.error error⊢ object = frontiers.toMakeWitness.toObject
      cases hAcceptAll goals completed! 🐙
  | ok _accepted =>oknodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:(match acceptItems sourceBinding items with
  | Except.error error => Except.error error
  | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject) =
  Except.ok object_accepted:List MakeItemhItems:acceptItems sourceBinding items = Except.ok _accepted⊢ object = frontiers.toMakeWitness.toObject
      rw [hItems] at hAcceptoknodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignature_accepted:List MakeItemhAccept:(match Except.ok _accepted with
  | Except.error error => Except.error error
  | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject) =
  Except.ok objecthItems:acceptItems sourceBinding items = Except.ok _accepted⊢ object = frontiers.toMakeWitness.toObject
      cases hAcceptok.reflnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).label_accepted:List MakeItemhItems:acceptItems sourceBinding items = Except.ok _accepted⊢ frontiers.toMakeWitness.toObject = frontiers.toMakeWitness.toObject
      rflAll goals completed! 🐙

The makeEach(items, K) frontier witness exposes item-derived generated labels.

theorem accept_childLabel_eq
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (items : List MakeItem)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding items.length
        (node := NodeId))
    (hLabels :
      ∀ index,
        frontiers.childLabel index = (items.get index).label)
    (index : Fin items.length) :
    frontiers.childLabel index = (items.get index).label :=
  hLabels index

The makeEach(items, K) frontier witness exposes exact generated output frontiers.

theorem accept_childOutputPorts_exact
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (items : List MakeItem)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding items.length
        (node := NodeId)) :
    ∀ index port,
      port ∈ frontiers.childOutputPorts index ↔
        ∃ template,
          template ∈ kind.outputPorts ∧
            port.signature =
              { label := frontiers.childLabel index
                contract := template.contract } :=
  frontiers.childOutputPorts_exact

The makeEach(items, K) frontier witness exposes exact generated input frontiers.

theorem accept_childInputPorts_exact
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (items : List MakeItem)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding items.length
        (node := NodeId)) :
    ∀ index port,
      port ∈ frontiers.childInputPorts index ↔
        ∃ template,
          template ∈ kind.inputs ∧
            port.signature =
              { label := frontiers.childLabel index
                contract := template.contract } :=
  frontiers.childInputPorts_exact

Successful makeEach(items, K) admission exposes exact output instances on the result.

theorem accept_outputs_exact
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (hKind : kind.KindSupportsMakeEach)
    (items : List MakeItem)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding items.length
        (node := NodeId))
    (hLabels :
      ∀ index,
        frontiers.childLabel index = (items.get index).label)
    (object : LinearPortObject NodeId OutputPortSignature InputPortSignature)
    (hAccept :
      accept policy sourceBinding kind hKind items frontiers hLabels = Except.ok object) :
    ∀ output,
      output ∈ object.graph.outputs ↔
        ∃ index port,
          port ∈ frontiers.childOutputPorts index ∧
            output = { node := policy.childIndex sourceBinding index, port := port } := bynodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind items frontiers hLabels = Except.ok object⊢ ∀ (output : SourcePortInstance NodeId OutputPortSignature),
  output ∈ object.graph.outputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childOutputPorts index,
        output = { node := policy.childIndex sourceBinding index, port := port }
  have hEq : object = frontiers.toMakeWitness.toObject :=
    accept_ok_eq policy sourceBinding kind hKind items frontiers hLabels object hAcceptnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind items frontiers hLabels = Except.ok objecthEq:object = frontiers.toMakeWitness.toObject⊢ ∀ (output : SourcePortInstance NodeId OutputPortSignature),
  output ∈ object.graph.outputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childOutputPorts index,
        output = { node := policy.childIndex sourceBinding index, port := port }
  rw [hEq]nodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind items frontiers hLabels = Except.ok objecthEq:object = frontiers.toMakeWitness.toObject⊢ ∀ (output : SourcePortInstance NodeId OutputPortSignature),
  output ∈ frontiers.toMakeWitness.toObject.graph.outputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childOutputPorts index,
        output = { node := policy.childIndex sourceBinding index, port := port }
  exact frontiers.toMakeWitness_toObject_outputs_exactAll goals completed! 🐙

Successful makeEach(items, K) admission exposes exact input instances on the result.

theorem accept_inputs_exact
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (hKind : kind.KindSupportsMakeEach)
    (items : List MakeItem)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding items.length
        (node := NodeId))
    (hLabels :
      ∀ index,
        frontiers.childLabel index = (items.get index).label)
    (object : LinearPortObject NodeId OutputPortSignature InputPortSignature)
    (hAccept :
      accept policy sourceBinding kind hKind items frontiers hLabels = Except.ok object) :
    ∀ input,
      input ∈ object.graph.inputs ↔
        ∃ index port,
          port ∈ frontiers.childInputPorts index ∧
            input = { node := policy.childIndex sourceBinding index, port := port } := bynodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind items frontiers hLabels = Except.ok object⊢ ∀ (input : SourcePortInstance NodeId InputPortSignature),
  input ∈ object.graph.inputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childInputPorts index, input = { node := policy.childIndex sourceBinding index, port := port }
  have hEq : object = frontiers.toMakeWitness.toObject :=
    accept_ok_eq policy sourceBinding kind hKind items frontiers hLabels object hAcceptnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind items frontiers hLabels = Except.ok objecthEq:object = frontiers.toMakeWitness.toObject⊢ ∀ (input : SourcePortInstance NodeId InputPortSignature),
  input ∈ object.graph.inputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childInputPorts index, input = { node := policy.childIndex sourceBinding index, port := port }
  rw [hEq]nodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind items frontiers hLabels = Except.ok objecthEq:object = frontiers.toMakeWitness.toObject⊢ ∀ (input : SourcePortInstance NodeId InputPortSignature),
  input ∈ frontiers.toMakeWitness.toObject.graph.inputs ↔
    ∃ index,
      ∃ port ∈ frontiers.childInputPorts index, input = { node := policy.childIndex sourceBinding index, port := port }
  exact frontiers.toMakeWitness_toObject_inputs_exactAll goals completed! 🐙

A successful makeEach(items, K) admission carries source linearity.

theorem accept_portLinear
    {nodeBinding : NodeId → BindingName}
    (policy : GeneratedNamePolicy BindingName NodeId nodeBinding)
    (sourceBinding : BindingName)
    (kind : ElaborationIR.AcceptedKindDecl)
    (hKind : kind.KindSupportsMakeEach)
    (items : List MakeItem)
    (frontiers :
      KindInstantiatedFrontiers kind policy sourceBinding items.length
        (node := NodeId))
    (hLabels :
      ∀ index,
        frontiers.childLabel index = (items.get index).label)
    (object : LinearPortObject NodeId OutputPortSignature InputPortSignature)
    (hAccept :
      accept policy sourceBinding kind hKind items frontiers hLabels = Except.ok object) :
    object.graph.PortLinear := bynodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:accept policy sourceBinding kind hKind items frontiers hLabels = Except.ok object⊢ object.graph.PortLinear
  unfold accept at hAcceptnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:(match acceptItems sourceBinding items with
  | Except.error error => Except.error error
  | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject) =
  Except.ok object⊢ object.graph.PortLinear
  cases hItems : acceptItems sourceBinding items with
  | error error =>errornodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:(match acceptItems sourceBinding items with
  | Except.error error => Except.error error
  | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject) =
  Except.ok objecterror:MakeEachErrorhItems:acceptItems sourceBinding items = Except.error error⊢ object.graph.PortLinear
      rw [hItems] at hAccepterrornodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignatureerror:MakeEachErrorhAccept:(match Except.error error with
  | Except.error error => Except.error error
  | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject) =
  Except.ok objecthItems:acceptItems sourceBinding items = Except.error error⊢ object.graph.PortLinear
      cases hAcceptAll goals completed! 🐙
  | ok _accepted =>oknodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignaturehAccept:(match acceptItems sourceBinding items with
  | Except.error error => Except.error error
  | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject) =
  Except.ok object_accepted:List MakeItemhItems:acceptItems sourceBinding items = Except.ok _accepted⊢ object.graph.PortLinear
      rw [hItems] at hAcceptoknodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).labelobject:LinearPortObject NodeId OutputPortSignature InputPortSignature_accepted:List MakeItemhAccept:(match Except.ok _accepted with
  | Except.error error => Except.error error
  | Except.ok _items => Except.ok frontiers.toMakeWitness.toObject) =
  Except.ok objecthItems:acceptItems sourceBinding items = Except.ok _accepted⊢ object.graph.PortLinear
      cases hAcceptok.reflnodeBinding:NodeId → BindingNamepolicy:GeneratedNamePolicy BindingName NodeId nodeBindingsourceBinding:BindingNamekind:AcceptedKindDeclhKind:kind.KindSupportsMakeEachitems:List MakeItemfrontiers:KindInstantiatedFrontiers kind policy sourceBinding items.lengthhLabels:∀ (index : Fin items.length), frontiers.childLabel index = (items.get index).label_accepted:List MakeItemhItems:acceptItems sourceBinding items = Except.ok _accepted⊢ frontiers.toMakeWitness.toObject.graph.PortLinear
      exact KindInstantiatedFrontiers.toMakeWitness_portLinear frontiersAll goals completed! 🐙

end MakeEach

`*` (Star) Admission

namespace Star

* admission at the source-linearity layer.

ADR 0049's record-form * and ADR 0052's bounded indexed-product * both elaborate to multi-side => phantom => singular-side. The phantom synthesis, finite-product discriminator, and phantom-boundary contraction exactness are mechanized in PhantomAdapterWitness. This entry point therefore consumes a fully constructed witness and returns the resulting LinearPortObject. The integrator slice constructs the witness from a product contract, the multi-side LinearPortObject, and the singular-side LinearPortObject; this file does not re-derive that machinery.

Returning Except StarError keeps the signature uniform with the other two admission entry points. The first-sketch implementation never produces an error, because witness construction has already discharged the structural obligations; the named diagnostics are reserved for slice 7's front-end before it builds the witness.

def accept
    (witness : PhantomAdapterWitness node outputPort inputPort productContract label) :
    Except StarError (LinearPortObject node outputPort inputPort) :=
  Except.ok witness.starInsertion

Successful * admission returns exactly the supplied phantom-adapter insertion.

theorem accept_ok_eq
    (witness : PhantomAdapterWitness node outputPort inputPort productContract label)
    (object : LinearPortObject node outputPort inputPort)
    (hAccept : accept witness = Except.ok object) :
    object = witness.starInsertion := bynode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortwitness:PhantomAdapterWitness node outputPort inputPort productContract labelobject:LinearPortObject node outputPort inputPorthAccept:accept witness = Except.ok object⊢ object = witness.starInsertion
  have hUnwrap :
      (Except.ok witness.starInsertion :
        Except StarError (LinearPortObject node outputPort inputPort)) =
          Except.ok object := hAcceptnode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortwitness:PhantomAdapterWitness node outputPort inputPort productContract labelobject:LinearPortObject node outputPort inputPorthAccept:accept witness = Except.ok objecthUnwrap:Except.ok witness.starInsertion = Except.ok object⊢ object = witness.starInsertion
  exact (Except.ok.inj hUnwrap).symmAll goals completed! 🐙

The witnessed * admission preserves source linearity.

theorem accept_portLinear
    (witness : PhantomAdapterWitness node outputPort inputPort productContract label)
    (object : LinearPortObject node outputPort inputPort)
    (hAccept : accept witness = Except.ok object) :
    object.graph.PortLinear := bynode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortwitness:PhantomAdapterWitness node outputPort inputPort productContract labelobject:LinearPortObject node outputPort inputPorthAccept:accept witness = Except.ok object⊢ object.graph.PortLinear
  have hEq : object = witness.starInsertion :=
    accept_ok_eq witness object hAcceptnode:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortwitness:PhantomAdapterWitness node outputPort inputPort productContract labelobject:LinearPortObject node outputPort inputPorthAccept:accept witness = Except.ok objecthEq:object = witness.starInsertion⊢ object.graph.PortLinear
  rw [hEq]node:TypeoutputPort:TypeinputPort:TypeproductContract:Typelabel:Typeinst✝²:DecidableEq nodeinst✝¹:DecidableEq outputPortinst✝:DecidableEq inputPortwitness:PhantomAdapterWitness node outputPort inputPort productContract labelobject:LinearPortObject node outputPort inputPorthAccept:accept witness = Except.ok objecthEq:object = witness.starInsertion⊢ witness.starInsertion.graph.PortLinear
  exact witness.starInsertion_portLinearAll goals completed! 🐙

end Starend LinearPortGraphend Cortex.Wire