Cortex.Wire.SelectAdmission

proofs

On this page

Overview
Context
Theorem Split
Selectable Output Shape
Source Select Clause
Diagnostics
Latent Admission Carrier
Source Admission
Bridge Into LatentBranchFamily
Admission Sanity Examples

Imports

import Mathlib.Data.List.Perm.Basic
import Cortex.Wire.ElaborationIR
import Cortex.Wire.Select

Overview

Source-level admission for Wire select(...) clauses.

Context

ADR 0033 fixes select(...) as a guarded-affine collapse over an exclusive output sum on the base graph. ADR 0034 narrows the runtime authority of pure select to actualizing exactly one already-admitted latent arm. The downstream proof object for that selected arm is Cortex.Wire.Select.LatentBranchFamily, together with SelectActualize for the chosen arm.

This module sits one step earlier: it admits the source shape of a select(...) clause against the base graph's exclusive output sum boundary. Admission resolves arm keys, rejects duplicates, unknown source keys, and uncovered shape arms, and emits a LatentSelectAdmission carrier that records each arm body as latent — that is, attached to its admitted arm key without being overlaid into live topology. Conversion to a LatentBranchFamily is a separate bridge step that requires the caller to supply the per-arm SubgraphSpec together with its disjointness witness; this module does not synthesize one.

Theorem Split

The page proves:

arm-key resolution against an exclusive output sum is decidable, deterministic, and total: every admitted arm is matched to exactly one sum-group key, and the full sum-group must be covered;
admission rejects duplicate, unknown, and uncovered arms with explicit diagnostics;
successful admission produces a LatentSelectAdmission whose arm-key set is an order-insensitive permutation of the sum-group keys, and whose arm bodies remain latent;
successful admitClause and admitClauseAtNode construction witness LatentSelectAdmission.FromClause, tying admitted latent bodies back to their source arms;
a bridging constructor lifts a LatentSelectAdmission together with a caller-supplied SubgraphSpec family into a LatentBranchFamily.

              namespace Cortex.Wirenamespace SelectAdmissionopen Cortex.Wire.ElaborationIR

Selectable Output Shape

SelectableOutputShape is the resolved exclusive-output-sum boundary that source select(...) admission consumes.

OutputShape keeps authored node egresses in the local declaration carrier. SelectableOutputShape is its select-specific projection: a list of (SelectArmKey, PortSignature) entries describing the exclusive output sum carried by the base of a select clause, together with the uniqueness and validity witnesses required for arm-key resolution and frontier flattening.

The arm-key list, port-label list, and uniqueness witnesses are exactly the obligations projected from OutputShape.LocallyAdmissible.sumGroup.

structure SelectableOutputShape where

Arms of the exclusive output sum, in source order, paired with the port signature each arm exposes when selected.

armPorts : List (SelectArmKey × PortSignature)

Exclusive output sums have at least two arms; one-arm outputs are single.

armsAtLeastTwo : 2 ≤ armPorts.length

Sum-group arm keys are unique.

armKeysUnique : (armPorts.map Prod.fst).Nodup

Flattened port labels exposed by sum-group arms are unique.

portLabelsUnique : (armPorts.map (fun entry => entry.snd.label)).Nodup

Each arm key is locally valid.

armKeysValid : ∀ entry, entry ∈ armPorts → entry.fst.Valid

Each arm port signature is locally valid.

  armPortsValid : ∀ entry, entry ∈ armPorts → entry.snd.Valid
  deriving Repr

namespace SelectableOutputShape

Sum-group arm keys exposed by an output shape.

def armKeys (shape : SelectableOutputShape) : List SelectArmKey :=
  shape.armPorts.map Prod.fst

Look up the port signature for an arm key. The entry is unique because armKeysUnique rules out duplicate keys.

def portFor? (shape : SelectableOutputShape) (key : SelectArmKey) :
    Option PortSignature :=
  (shape.armPorts.find? (fun entry => entry.fst = key)).map Prod.snd

Membership in the arm-key projection is decidable.

instance hasKeyDecidable (shape : SelectableOutputShape) (key : SelectArmKey) :
    Decidable (key ∈ shape.armKeys) :=
  inferInstanceAs (Decidable (key ∈ shape.armPorts.map Prod.fst))

Build a SelectableOutputShape from the source data of an exclusive output sum group. The constructor consumes exactly the admissibility witnesses produced by OutputShape.LocallyAdmissible.sumGroup, so admitted accepted nodes can project into a select base shape without losing the source-side uniqueness obligations.

def ofSumGroupArms
    (arms : List OutputArmDecl)
    (hArmsAtLeastTwo : 2 ≤ arms.length)
    (hArmKeysUnique : (arms.map OutputArmDecl.armKey).Nodup)
    (hPortLabelsUnique : (arms.map (fun arm => arm.port.label)).Nodup)
    (hArmsValid : ∀ arm, arm ∈ arms → arm.Valid) :
    SelectableOutputShape :=
  let armPorts := arms.map (fun arm => (arm.armKey, arm.port))
  { armPorts := armPorts
    armsAtLeastTwo := byarms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) arms⊢ 2 ≤ armPorts.length
      show 2 ≤ (arms.map (fun arm => (arm.armKey, arm.port))).lengtharms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) arms⊢ 2 ≤ (List.map (fun arm => (arm.armKey, arm.port)) arms).length
      simpa using hArmsAtLeastTwoAll goals completed! 🐙
    armKeysUnique := byarms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) arms⊢ (List.map Prod.fst armPorts).Nodup
      show (arms.map (fun arm => (arm.armKey, arm.port)) |>.map Prod.fst).Noduparms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) arms⊢ (List.map Prod.fst (List.map (fun arm => (arm.armKey, arm.port)) arms)).Nodup
      simpa [List.map_map, Function.comp] using hArmKeysUniqueAll goals completed! 🐙
    portLabelsUnique := byarms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) arms⊢ (List.map (fun entry => entry.2.label) armPorts).Nodup
      show (arms.map (fun arm => (arm.armKey, arm.port))
              |>.map (fun entry => entry.snd.label)).Noduparms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) arms⊢ (List.map (fun entry => entry.2.label) (List.map (fun arm => (arm.armKey, arm.port)) arms)).Nodup
      simpa [List.map_map, Function.comp] using hPortLabelsUniqueAll goals completed! 🐙
    armKeysValid := byarms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) arms⊢ ∀ entry ∈ armPorts, entry.1.Valid
      intro entry hEntryarms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) armsentry:SelectArmKey × PortSignaturehEntry:entry ∈ armPorts⊢ entry.1.Valid
      have hEntry' :
          entry ∈ arms.map (fun arm => (arm.armKey, arm.port)) := hEntryarms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) armsentry:SelectArmKey × PortSignaturehEntry:entry ∈ armPortshEntry':entry ∈ List.map (fun arm => (arm.armKey, arm.port)) arms⊢ entry.1.Valid
      rcases List.mem_map.mp hEntry' with ⟨arm, hArmMem, hEq⟩arms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) armsentry:SelectArmKey × PortSignaturehEntry:entry ∈ armPortshEntry':entry ∈ List.map (fun arm => (arm.armKey, arm.port)) armsarm:OutputArmDeclhArmMem:arm ∈ armshEq:(arm.armKey, arm.port) = entry⊢ entry.1.Valid
      subst hEqarms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) armsarm:OutputArmDeclhArmMem:arm ∈ armshEntry:(arm.armKey, arm.port) ∈ armPortshEntry':(arm.armKey, arm.port) ∈ List.map (fun arm => (arm.armKey, arm.port)) arms⊢ (arm.armKey, arm.port).1.Valid
      exact (hArmsValid arm hArmMem).leftAll goals completed! 🐙
    armPortsValid := byarms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) arms⊢ ∀ entry ∈ armPorts, entry.2.Valid
      intro entry hEntryarms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) armsentry:SelectArmKey × PortSignaturehEntry:entry ∈ armPorts⊢ entry.2.Valid
      have hEntry' :
          entry ∈ arms.map (fun arm => (arm.armKey, arm.port)) := hEntryarms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) armsentry:SelectArmKey × PortSignaturehEntry:entry ∈ armPortshEntry':entry ∈ List.map (fun arm => (arm.armKey, arm.port)) arms⊢ entry.2.Valid
      rcases List.mem_map.mp hEntry' with ⟨arm, hArmMem, hEq⟩arms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) armsentry:SelectArmKey × PortSignaturehEntry:entry ∈ armPortshEntry':entry ∈ List.map (fun arm => (arm.armKey, arm.port)) armsarm:OutputArmDeclhArmMem:arm ∈ armshEq:(arm.armKey, arm.port) = entry⊢ entry.2.Valid
      subst hEqarms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.ValidarmPorts:List (SelectArmKey × PortSignature) := List.map (fun arm => (arm.armKey, arm.port)) armsarm:OutputArmDeclhArmMem:arm ∈ armshEntry:(arm.armKey, arm.port) ∈ armPortshEntry':(arm.armKey, arm.port) ∈ List.map (fun arm => (arm.armKey, arm.port)) arms⊢ (arm.armKey, arm.port).2.Valid
      exact (hArmsValid arm hArmMem).rightAll goals completed! 🐙 }

Extract the two-or-more arm-count obligation carried by a sum-group witness.

private theorem armsAtLeastTwo_of_sumGroup_admissible
    {arms : List OutputArmDecl}
    (h : ElaborationIR.OutputShape.LocallyAdmissible
          (ElaborationIR.OutputShape.sumGroup arms)) :
    2 ≤ arms.length := byarms:List OutputArmDeclh:(OutputShape.sumGroup arms).LocallyAdmissible⊢ 2 ≤ arms.length
  cases h with
  | sumGroup hAtLeastTwo _hValid _hKeyNodup _hLabelNodup =>sumGrouparms:List OutputArmDeclhAtLeastTwo:2 ≤ arms.length_hValid:∀ arm ∈ arms, arm.Valid_hKeyNodup:(List.map OutputArmDecl.armKey arms).Nodup_hLabelNodup:(List.map (fun arm => arm.port.label) arms).Nodup⊢ 2 ≤ arms.length exact hAtLeastTwoAll goals completed! 🐙

Extract the arm-key uniqueness obligation carried by a sum-group admissibility witness.

private theorem armKeysUnique_of_sumGroup_admissible
    {arms : List OutputArmDecl}
    (h : ElaborationIR.OutputShape.LocallyAdmissible
          (ElaborationIR.OutputShape.sumGroup arms)) :
    (arms.map OutputArmDecl.armKey).Nodup := byarms:List OutputArmDeclh:(OutputShape.sumGroup arms).LocallyAdmissible⊢ (List.map OutputArmDecl.armKey arms).Nodup
  cases h with
  | sumGroup _hAtLeastTwo _hValid hKeyNodup _hLabelNodup =>sumGrouparms:List OutputArmDecl_hAtLeastTwo:2 ≤ arms.length_hValid:∀ arm ∈ arms, arm.ValidhKeyNodup:(List.map OutputArmDecl.armKey arms).Nodup_hLabelNodup:(List.map (fun arm => arm.port.label) arms).Nodup⊢ (List.map OutputArmDecl.armKey arms).Nodup exact hKeyNodupAll goals completed! 🐙

Extract the port-label uniqueness obligation carried by a sum-group admissibility witness.

private theorem portLabelsUnique_of_sumGroup_admissible
    {arms : List OutputArmDecl}
    (h : ElaborationIR.OutputShape.LocallyAdmissible
          (ElaborationIR.OutputShape.sumGroup arms)) :
    (arms.map (fun arm => arm.port.label)).Nodup := byarms:List OutputArmDeclh:(OutputShape.sumGroup arms).LocallyAdmissible⊢ (List.map (fun arm => arm.port.label) arms).Nodup
  cases h with
  | sumGroup _hAtLeastTwo _hValid _hKeyNodup hLabelNodup =>sumGrouparms:List OutputArmDecl_hAtLeastTwo:2 ≤ arms.length_hValid:∀ arm ∈ arms, arm.Valid_hKeyNodup:(List.map OutputArmDecl.armKey arms).NoduphLabelNodup:(List.map (fun arm => arm.port.label) arms).Nodup⊢ (List.map (fun arm => arm.port.label) arms).Nodup exact hLabelNodupAll goals completed! 🐙

Extract per-arm validity from a sum-group admissibility witness.

private theorem armsValid_of_sumGroup_admissible
    {arms : List OutputArmDecl}
    (h : ElaborationIR.OutputShape.LocallyAdmissible
          (ElaborationIR.OutputShape.sumGroup arms)) :
    ∀ arm, arm ∈ arms → arm.Valid := byarms:List OutputArmDeclh:(OutputShape.sumGroup arms).LocallyAdmissible⊢ ∀ arm ∈ arms, arm.Valid
  cases h with
  | sumGroup _hAtLeastTwo hValid _hKeyNodup _hLabelNodup =>sumGrouparms:List OutputArmDecl_hAtLeastTwo:2 ≤ arms.lengthhValid:∀ arm ∈ arms, arm.Valid_hKeyNodup:(List.map OutputArmDecl.armKey arms).Nodup_hLabelNodup:(List.map (fun arm => arm.port.label) arms).Nodup⊢ ∀ arm ∈ arms, arm.Valid exact hValidAll goals completed! 🐙

Extract per-arm port validity from a sum-group admissibility witness.

private theorem armPortsValid_of_sumGroup_admissible
    {arms : List OutputArmDecl}
    (h : ElaborationIR.OutputShape.LocallyAdmissible
          (ElaborationIR.OutputShape.sumGroup arms)) :
    ∀ arm, arm ∈ arms → arm.port.Valid := byarms:List OutputArmDeclh:(OutputShape.sumGroup arms).LocallyAdmissible⊢ ∀ arm ∈ arms, arm.port.Valid
  cases h with
  | sumGroup _hAtLeastTwo hValid _hKeyNodup _hLabelNodup =>sumGrouparms:List OutputArmDecl_hAtLeastTwo:2 ≤ arms.lengthhValid:∀ arm ∈ arms, arm.Valid_hKeyNodup:(List.map OutputArmDecl.armKey arms).Nodup_hLabelNodup:(List.map (fun arm => arm.port.label) arms).Nodup⊢ ∀ arm ∈ arms, arm.port.Valid
      intro arm hArmMemsumGrouparms:List OutputArmDecl_hAtLeastTwo:2 ≤ arms.lengthhValid:∀ arm ∈ arms, arm.Valid_hKeyNodup:(List.map OutputArmDecl.armKey arms).Nodup_hLabelNodup:(List.map (fun arm => arm.port.label) arms).Noduparm:OutputArmDeclhArmMem:arm ∈ arms⊢ arm.port.Valid
      exact (hValid arm hArmMem).rightAll goals completed! 🐙

Project an authored OutputShape into a SelectableOutputShape. Returns none when the shape is a single non-sum output: select admission must surface SelectAdmissionError.nonExclusiveBase for that case.

def ofOutputShape? :
    (shape : ElaborationIR.OutputShape) → shape.LocallyAdmissible →
      Option SelectableOutputShape
  | ElaborationIR.OutputShape.single _, _ => none
  | ElaborationIR.OutputShape.sumGroup arms, h =>
      some
        (ofSumGroupArms arms
          (armsAtLeastTwo_of_sumGroup_admissible h)
          (armKeysUnique_of_sumGroup_admissible h)
          (portLabelsUnique_of_sumGroup_admissible h)
          (armsValid_of_sumGroup_admissible h))

Project an AcceptedNodeDecl whose authored output frontier is exactly one exclusive output sum group into a SelectableOutputShape. Any other frontier shape (no outputs, multiple shapes, or a single non-sum output) yields none, which select admission must report as SelectAdmissionError.nonExclusiveBase.

def ofAcceptedNode? (decl : AcceptedNodeDecl) :
    Option SelectableOutputShape :=
  match h : decl.outputs with
  | [] => none
  | [shape] =>
      have hMem : shape ∈ decl.outputs :=
        h.symm ▸ List.mem_singleton.mpr rfl
      ofOutputShape? shape (decl.outputShapesAdmissible shape hMem)
  | _ :: _ :: _ => none

Sum-group projection produces an arm count equal to the source arm count.

theorem ofSumGroupArms_armPorts_length
    (arms : List OutputArmDecl)
    (hArmsAtLeastTwo : 2 ≤ arms.length)
    (hArmKeysUnique : (arms.map OutputArmDecl.armKey).Nodup)
    (hPortLabelsUnique : (arms.map (fun arm => arm.port.label)).Nodup)
    (hArmsValid : ∀ arm, arm ∈ arms → arm.Valid) :
    (ofSumGroupArms
      arms
      hArmsAtLeastTwo
      hArmKeysUnique
      hPortLabelsUnique
      hArmsValid).armPorts.length =
      arms.length := byarms:List OutputArmDeclhArmsAtLeastTwo:2 ≤ arms.lengthhArmKeysUnique:(List.map OutputArmDecl.armKey arms).NoduphPortLabelsUnique:(List.map (fun arm => arm.port.label) arms).NoduphArmsValid:∀ arm ∈ arms, arm.Valid⊢ (ofSumGroupArms arms hArmsAtLeastTwo hArmKeysUnique hPortLabelsUnique hArmsValid).armPorts.length = arms.length
  simp [ofSumGroupArms]All goals completed! 🐙

end SelectableOutputShape

Source Select Clause

One source arm of a select(...) clause, parameterized over the latent body type so this carrier is reusable across slices that supply different downstream objects (raw GraphExpr, SubgraphSpec node, LinearPortObject, …).

structure SelectArm (body : Type) where

Source-stable arm key written by the author.

key : SelectArmKey

Latent body for this arm, kept opaque at this admission layer.

  body : body
  deriving Repr

Source select(...) clause carrier. The base is an opaque graph or graph-expression value; the integrator will refine it to the slice 1 base carrier. The arm-list shape mirrors the existing GraphExpr.select constructor in ElaborationIR.

structure SelectExpr (base : Type) (body : Type) where

Base graph exposing the exclusive output sum.

base : base

Arms in source order.

  arms : List (SelectArm body)
  deriving Repr

namespace SelectExpr

Project the arm key list from a source select clause.

def armKeys {base body : Type} (clause : SelectExpr base body) :
    List SelectArmKey :=
  clause.arms.map SelectArm.key

end SelectExpr

Diagnostics

Static admission diagnostics emitted while resolving a source select(...) clause against an exclusive output sum boundary.

inductive SelectAdmissionError where

Two source arms wrote the same arm key.

| duplicateSelectArmKey (key : SelectArmKey)

A source arm key does not resolve to any sum-group label or unique contract fallback.

| unknownSourceKey (key : SelectArmKey)

A sum-group entry has no source arm and total coverage is required.

| uncoveredShapeArm (key : SelectArmKey)

Contract-based fallback found multiple candidate keys for one arm.

| ambiguousContractFallback (contract : ContractId) (candidates : List SelectArmKey)

The base graph does not expose an exclusive output sum at this position.

  | nonExclusiveBase
  deriving DecidableEq, Repr

Latent Admission Carrier

LatentSelectAdmission is the proof-side carrier produced by successful source admission of a select(...) clause.

Each admitted entry pairs a sum-group arm key with the source arm body that was matched against it. The bodies are latent: this carrier intentionally does not overlay the bodies into live topology. The downstream SelectActualize model materializes one body when the runtime selector picks an arm.

This carrier is parameterized over the body type so callers can attach SubgraphSpec, GraphExpr, or any other latent payload without coupling admission to a single proof carrier.

By itself the record enforces key coverage up to permutation, not source order or body provenance: a hand-built value can pair the right keys with arbitrary bodies. Consumers that need runtime/source correspondence should require LatentSelectAdmission.FromClause for the concrete source clause.

structure LatentSelectAdmission (body : Type) where

The output shape the source clause was admitted against.

shape : SelectableOutputShape

Per-arm-key admitted entries, one for each sum-group key.

entries : List (SelectArmKey × body)

Admission emitted exactly the sum-group arm keys, up to ordering.

  entries_keys_perm : (entries.map Prod.fst).Perm shape.armKeys
  deriving Repr

namespace LatentSelectAdmission

The admitted arm-key list is a permutation of the sum-group key list.

theorem keys_perm_shape_keys
    {body : Type}
    (admission : LatentSelectAdmission body) :
    (admission.entries.map Prod.fst).Perm admission.shape.armKeys :=
  admission.entries_keys_perm

The admitted arm-key set equals the sum-group key set.

theorem keys_eq_shape_keys
    {body : Type}
    (admission : LatentSelectAdmission body) :
    (admission.entries.map Prod.fst).toFinset = admission.shape.armKeys.toFinset := bybody:Typeadmission:LatentSelectAdmission body⊢ (List.map Prod.fst admission.entries).toFinset = admission.shape.armKeys.toFinset
  ext keyhbody:Typeadmission:LatentSelectAdmission bodykey:SelectArmKey⊢ key ∈ (List.map Prod.fst admission.entries).toFinset ↔ key ∈ admission.shape.armKeys.toFinset
  simpa using admission.entries_keys_perm.mem_iff (a := key)All goals completed! 🐙

Admission produces one entry per sum-group arm key.

theorem length_eq_armPorts
    {body : Type}
    (admission : LatentSelectAdmission body) :
    admission.entries.length = admission.shape.armPorts.length := bybody:Typeadmission:LatentSelectAdmission body⊢ admission.entries.length = admission.shape.armPorts.length
  calc
    admission.entries.length = (admission.entries.map Prod.fst).length := bybody:Typeadmission:LatentSelectAdmission body⊢ admission.entries.length = (List.map Prod.fst admission.entries).length
      simpAll goals completed! 🐙
    _ = admission.shape.armKeys.length := bybody:Typeadmission:LatentSelectAdmission body⊢ (List.map Prod.fst admission.entries).length = admission.shape.armKeys.length
      exact admission.entries_keys_perm.length_eqAll goals completed! 🐙
    _ = admission.shape.armPorts.length := bybody:Typeadmission:LatentSelectAdmission body⊢ admission.shape.armKeys.length = admission.shape.armPorts.length
      simp [SelectableOutputShape.armKeys]All goals completed! 🐙

Admitted arm keys are unique.

theorem keys_nodup
    {body : Type}
    (admission : LatentSelectAdmission body) :
    (admission.entries.map Prod.fst).Nodup := bybody:Typeadmission:LatentSelectAdmission body⊢ (List.map Prod.fst admission.entries).Nodup
  exact admission.entries_keys_perm.nodup_iff.mpr admission.shape.armKeysUniqueAll goals completed! 🐙

end LatentSelectAdmission

Source Admission

Reject a select(...) source arm list that contains a duplicate key.

def detectDuplicateArm
    (keys : List SelectArmKey) :
    Except SelectAdmissionError Unit :=
  keys.foldl
    (fun (acc : Except SelectAdmissionError (List SelectArmKey)) (key : SelectArmKey) =>
      acc.bind (fun seen =>
        if key ∈ seen then
          Except.error (SelectAdmissionError.duplicateSelectArmKey key)
        else
          Except.ok (key :: seen)))
    (Except.ok []) |>.map (fun _ => ())

Look up an arm body in the source arm list by key. The list-shaped lookup preserves source-order diagnostics if the same key appears twice.

def findArmBody?
    {body : Type}
    (arms : List (SelectArm body))
    (key : SelectArmKey) :
    Option body :=
  (arms.find? (fun arm => arm.key = key)).map SelectArm.body

Candidate label keys whose variant contract matches a contract fallback key.

def contractFallbackCandidates
    (shape : SelectableOutputShape)
    (contract : ContractId) :
    List SelectArmKey :=
  (shape.armPorts.filter (fun entry => entry.snd.contract = contract)).map Prod.fst

Resolve a source arm key to the canonical variant label key.

Executable Wire resolves labels first. If no label matches, the same token is interpreted as a contract-name fallback and accepted only when that contract appears on exactly one variant.

def resolveArmKey
    (shape : SelectableOutputShape)
    (key : SelectArmKey) :
    Except SelectAdmissionError SelectArmKey :=
  if key ∈ shape.armKeys then
    Except.ok key
  else
    let contract : ContractId := ⟨key.name⟩
    match contractFallbackCandidates shape contract with
    | [] => Except.error (SelectAdmissionError.unknownSourceKey key)
    | [candidate] => Except.ok candidate
    | first :: second :: rest =>
        Except.error
          (SelectAdmissionError.ambiguousContractFallback contract (first :: second :: rest))

Resolve one source arm to the canonical label key it targets.

def resolveArm
    {body : Type}
    (shape : SelectableOutputShape)
    (arm : SelectArm body) :
    Except SelectAdmissionError (SelectArm body) :=
  (resolveArmKey shape arm.key).map
    (fun key => { key := key, body := arm.body })

Resolve all source arms in source order.

def resolveArms
    {body : Type}
    (shape : SelectableOutputShape) :
    List (SelectArm body) → Except SelectAdmissionError (List (SelectArm body))
  | [] => Except.ok []
  | arm :: rest =>
      (resolveArm shape arm).bind (fun resolved =>
        (resolveArms shape rest).map (fun resolvedRest => resolved :: resolvedRest))

Collected admitted entries with their key-list equality bundled.

private structure CollectedEntries (body : Type) (keys : List SelectArmKey) where

Entries collected in the exact key order.

entries : List (SelectArmKey × body)

Collected entry keys equal the requested key list.

entries_keys_exact : entries.map Prod.fst = keys

Build admitted entries for a concrete key list from already-resolved source arms.

private def collectEntriesFrom
    {body : Type}
    (armPorts : List (SelectArmKey × PortSignature))
    (arms : List (SelectArm body)) :
    Except SelectAdmissionError (CollectedEntries body (armPorts.map Prod.fst)) :=
  match armPorts with
  | [] =>
      Except.ok
        { entries := []
          entries_keys_exact := rfl }
  | armPort :: rest =>
      match findArmBody? arms armPort.fst with
      | none => Except.error (SelectAdmissionError.uncoveredShapeArm armPort.fst)
      | some bodyValue =>
          match collectEntriesFrom rest arms with
          | Except.error error => Except.error error
          | Except.ok collected =>
              Except.ok
                { entries := (armPort.fst, bodyValue) :: collected.entries
                  entries_keys_exact := bybody:TypearmPorts:List (SelectArmKey × PortSignature)arms:List (SelectArm body)armPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)bodyValue:bodycollected:CollectedEntries body (List.map Prod.fst rest)⊢ List.map Prod.fst ((armPort.1, bodyValue) :: collected.entries) = List.map Prod.fst (armPort :: rest)
                    simp only [List.map_cons]body:TypearmPorts:List (SelectArmKey × PortSignature)arms:List (SelectArm body)armPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)bodyValue:bodycollected:CollectedEntries body (List.map Prod.fst rest)⊢ armPort.1 :: List.map Prod.fst collected.entries = armPort.1 :: List.map Prod.fst rest
                    rw [collected.entries_keys_exact]All goals completed! 🐙 }

Build admitted entries for an output shape from already-resolved source arms. Returns an error if any sum-group key is missing in the source arm list.

private def collectEntries
    {body : Type}
    (shape : SelectableOutputShape)
    (arms : List (SelectArm body)) :
    Except SelectAdmissionError (CollectedEntries body shape.armKeys) :=
  collectEntriesFrom shape.armPorts arms

Forget the private ordered collection proof into the public latent carrier.

private def collectedEntriesAdmission
    {body : Type}
    (shape : SelectableOutputShape)
    (collected : CollectedEntries body shape.armKeys) :
    LatentSelectAdmission body :=
  { shape := shape
    entries := collected.entries
    entries_keys_perm := bybody:Typeshape:SelectableOutputShapecollected:CollectedEntries body shape.armKeys⊢ (List.map Prod.fst collected.entries).Perm shape.armKeys
      rw [collected.entries_keys_exact]All goals completed! 🐙 }

Admit a source select(...) clause against an exclusive output sum.

The integrator obtains shape by projecting slice 1's OutputShape. The admission first resolves source arms to canonical variant labels: labels win, and unique contract names are accepted as fallback keys. It then rejects duplicate canonical arms and sum-group keys without a matching source arm. On success, this constructor emits entries in shape order, while the public LatentSelectAdmission carrier only requires order-insensitive key coverage. The matched arm body remains latent.

def admitClause
    {base body : Type}
    (shape : SelectableOutputShape)
    (clause : SelectExpr base body) :
    Except SelectAdmissionError (LatentSelectAdmission body) :=
  (resolveArms shape clause.arms).bind (fun resolvedArms =>
    detectDuplicateArm (resolvedArms.map SelectArm.key) |>.bind (fun _ =>
      (collectEntries shape resolvedArms).map (fun collected =>
        collectedEntriesAdmission shape collected)))

The executable admitClause constructor emits entries in shape-key order.

The public LatentSelectAdmission carrier only requires permutation-level key coverage so hand-built witnesses are not order-coupled. This theorem exposes the stronger fact for values that specifically came from admitClause.

theorem admitClause_entries_keys_eq_shape
    {base body : Type}
    (shape : SelectableOutputShape)
    (clause : SelectExpr base body)
    {admission : LatentSelectAdmission body}
    (hAdmit : admitClause shape clause = Except.ok admission) :
    admission.entries.map Prod.fst = shape.armKeys := bybase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyhAdmit:admitClause shape clause = Except.ok admission⊢ List.map Prod.fst admission.entries = shape.armKeys
  unfold admitClause at hAdmitbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyhAdmit:((resolveArms shape clause.arms).bind fun resolvedArms =>
    (detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
      Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admission⊢ List.map Prod.fst admission.entries = shape.armKeys
  cases hResolved : resolveArms shape clause.arms with
  | error err =>errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyhAdmit:((resolveArms shape clause.arms).bind fun resolvedArms =>
    (detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
      Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionerr:SelectAdmissionErrorhResolved:resolveArms shape clause.arms = Except.error err⊢ List.map Prod.fst admission.entries = shape.armKeys
      rw [hResolved] at hAdmiterrorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyerr:SelectAdmissionErrorhAdmit:((Except.error err).bind fun resolvedArms =>
    (detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
      Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionhResolved:resolveArms shape clause.arms = Except.error err⊢ List.map Prod.fst admission.entries = shape.armKeys
      change Except.error err = Except.ok admission at hAdmiterrorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyerr:SelectAdmissionErrorhResolved:resolveArms shape clause.arms = Except.error errhAdmit:Except.error err = Except.ok admission⊢ List.map Prod.fst admission.entries = shape.armKeys
      cases hAdmitAll goals completed! 🐙
  | ok resolvedArms =>okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyhAdmit:((resolveArms shape clause.arms).bind fun resolvedArms =>
    (detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
      Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms⊢ List.map Prod.fst admission.entries = shape.armKeys
      rw [hResolved] at hAdmitokbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hAdmit:((Except.ok resolvedArms).bind fun resolvedArms =>
    (detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
      Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionhResolved:resolveArms shape clause.arms = Except.ok resolvedArms⊢ List.map Prod.fst admission.entries = shape.armKeys
      change
        (detectDuplicateArm (resolvedArms.map SelectArm.key)).bind
          (fun _ =>
            (collectEntries shape resolvedArms).map
              (fun collected => collectedEntriesAdmission shape collected)) =
          Except.ok admission at hAdmitokbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArmshAdmit:((detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
    Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admission⊢ List.map Prod.fst admission.entries = shape.armKeys
      cases hDuplicate : detectDuplicateArm (resolvedArms.map SelectArm.key) with
      | error err =>ok.errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArmshAdmit:((detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
    Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionerr:SelectAdmissionErrorhDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.error err⊢ List.map Prod.fst admission.entries = shape.armKeys
          rw [hDuplicate] at hAdmitok.errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArmserr:SelectAdmissionErrorhAdmit:((Except.error err).bind fun x =>
    Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionhDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.error err⊢ List.map Prod.fst admission.entries = shape.armKeys
          change Except.error err = Except.ok admission at hAdmitok.errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArmserr:SelectAdmissionErrorhDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.error errhAdmit:Except.error err = Except.ok admission⊢ List.map Prod.fst admission.entries = shape.armKeys
          cases hAdmitAll goals completed! 🐙
      | ok _unit =>ok.okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArmshAdmit:((detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
    Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admission_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unit⊢ List.map Prod.fst admission.entries = shape.armKeys
          rw [hDuplicate] at hAdmitok.okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithAdmit:((Except.ok _unit).bind fun x =>
    Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionhDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unit⊢ List.map Prod.fst admission.entries = shape.armKeys
          change
            (collectEntries shape resolvedArms).map
              (fun collected => collectedEntriesAdmission shape collected) =
            Except.ok admission at hAdmitok.okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unithAdmit:Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms) =
  Except.ok admission⊢ List.map Prod.fst admission.entries = shape.armKeys
          cases hCollected : collectEntries shape resolvedArms with
          | error err =>ok.ok.errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unithAdmit:Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms) =
  Except.ok admissionerr:SelectAdmissionErrorhCollected:collectEntries shape resolvedArms = Except.error err⊢ List.map Prod.fst admission.entries = shape.armKeys
              rw [hCollected] at hAdmitok.ok.errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _uniterr:SelectAdmissionErrorhAdmit:Except.map (fun collected => collectedEntriesAdmission shape collected) (Except.error err) = Except.ok admissionhCollected:collectEntries shape resolvedArms = Except.error err⊢ List.map Prod.fst admission.entries = shape.armKeys
              change Except.error err = Except.ok admission at hAdmitok.ok.errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _uniterr:SelectAdmissionErrorhCollected:collectEntries shape resolvedArms = Except.error errhAdmit:Except.error err = Except.ok admission⊢ List.map Prod.fst admission.entries = shape.armKeys
              cases hAdmitAll goals completed! 🐙
          | ok collected =>ok.ok.okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unithAdmit:Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms) =
  Except.ok admissioncollected:CollectedEntries body shape.armKeyshCollected:collectEntries shape resolvedArms = Except.ok collected⊢ List.map Prod.fst admission.entries = shape.armKeys
              rw [hCollected] at hAdmitok.ok.okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unitcollected:CollectedEntries body shape.armKeyshAdmit:Except.map (fun collected => collectedEntriesAdmission shape collected) (Except.ok collected) = Except.ok admissionhCollected:collectEntries shape resolvedArms = Except.ok collected⊢ List.map Prod.fst admission.entries = shape.armKeys
              change Except.ok (collectedEntriesAdmission shape collected) =
                Except.ok admission at hAdmitok.ok.okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unitcollected:CollectedEntries body shape.armKeyshCollected:collectEntries shape resolvedArms = Except.ok collectedhAdmit:Except.ok (collectedEntriesAdmission shape collected) = Except.ok admission⊢ List.map Prod.fst admission.entries = shape.armKeys
              cases hAdmitok.ok.ok.reflbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unitcollected:CollectedEntries body shape.armKeyshCollected:collectEntries shape resolvedArms = Except.ok collected⊢ List.map Prod.fst (collectedEntriesAdmission shape collected).entries = shape.armKeys
              exact collected.entries_keys_exactAll goals completed! 🐙

Successful arm-body lookup returns a source arm with the requested key and body.

private theorem findArmBody?_some
    {body : Type}
    {arms : List (SelectArm body)}
    {key : SelectArmKey}
    {bodyValue : body}
    (hFind : findArmBody? arms key = some bodyValue) :
    ∃ arm, arm ∈ arms ∧ arm.key = key ∧ arm.body = bodyValue := bybody:Typearms:List (SelectArm body)key:SelectArmKeybodyValue:bodyhFind:findArmBody? arms key = some bodyValue⊢ ∃ arm ∈ arms, arm.key = key ∧ arm.body = bodyValue
  induction arms with
  | nil =>nilbody:Typekey:SelectArmKeybodyValue:bodyhFind:findArmBody? [] key = some bodyValue⊢ ∃ arm ∈ [], arm.key = key ∧ arm.body = bodyValue
      unfold findArmBody? at hFindnilbody:Typekey:SelectArmKeybodyValue:bodyhFind:Option.map SelectArm.body (List.find? (fun arm => decide (arm.key = key)) []) = some bodyValue⊢ ∃ arm ∈ [], arm.key = key ∧ arm.body = bodyValue
      simp at hFindAll goals completed! 🐙
  | cons head tail ih =>consbody:Typekey:SelectArmKeybodyValue:bodyhead:SelectArm bodytail:List (SelectArm body)ih:findArmBody? tail key = some bodyValue → ∃ arm ∈ tail, arm.key = key ∧ arm.body = bodyValuehFind:findArmBody? (head :: tail) key = some bodyValue⊢ ∃ arm ∈ head :: tail, arm.key = key ∧ arm.body = bodyValue
      unfold findArmBody? at hFindconsbody:Typekey:SelectArmKeybodyValue:bodyhead:SelectArm bodytail:List (SelectArm body)ih:findArmBody? tail key = some bodyValue → ∃ arm ∈ tail, arm.key = key ∧ arm.body = bodyValuehFind:Option.map SelectArm.body (List.find? (fun arm => decide (arm.key = key)) (head :: tail)) = some bodyValue⊢ ∃ arm ∈ head :: tail, arm.key = key ∧ arm.body = bodyValue
      simp only [List.find?_cons] at hFindconsbody:Typekey:SelectArmKeybodyValue:bodyhead:SelectArm bodytail:List (SelectArm body)ih:findArmBody? tail key = some bodyValue → ∃ arm ∈ tail, arm.key = key ∧ arm.body = bodyValuehFind:Option.map SelectArm.body
    (match decide (head.key = key) with
    | true => some head
    | false => List.find? (fun arm => decide (arm.key = key)) tail) =
  some bodyValue⊢ ∃ arm ∈ head :: tail, arm.key = key ∧ arm.body = bodyValue
      by_cases hKey : head.key = keyposbody:Typekey:SelectArmKeybodyValue:bodyhead:SelectArm bodytail:List (SelectArm body)ih:findArmBody? tail key = some bodyValue → ∃ arm ∈ tail, arm.key = key ∧ arm.body = bodyValuehFind:Option.map SelectArm.body
    (match decide (head.key = key) with
    | true => some head
    | false => List.find? (fun arm => decide (arm.key = key)) tail) =
  some bodyValuehKey:head.key = key⊢ ∃ arm ∈ head :: tail, arm.key = key ∧ arm.body = bodyValuenegbody:Typekey:SelectArmKeybodyValue:bodyhead:SelectArm bodytail:List (SelectArm body)ih:findArmBody? tail key = some bodyValue → ∃ arm ∈ tail, arm.key = key ∧ arm.body = bodyValuehFind:Option.map SelectArm.body
    (match decide (head.key = key) with
    | true => some head
    | false => List.find? (fun arm => decide (arm.key = key)) tail) =
  some bodyValuehKey:¬head.key = key⊢ ∃ arm ∈ head :: tail, arm.key = key ∧ arm.body = bodyValue
      ·posbody:Typekey:SelectArmKeybodyValue:bodyhead:SelectArm bodytail:List (SelectArm body)ih:findArmBody? tail key = some bodyValue → ∃ arm ∈ tail, arm.key = key ∧ arm.body = bodyValuehFind:Option.map SelectArm.body
    (match decide (head.key = key) with
    | true => some head
    | false => List.find? (fun arm => decide (arm.key = key)) tail) =
  some bodyValuehKey:head.key = key⊢ ∃ arm ∈ head :: tail, arm.key = key ∧ arm.body = bodyValue simp [hKey] at hFindposbody:Typekey:SelectArmKeybodyValue:bodyhead:SelectArm bodytail:List (SelectArm body)ih:findArmBody? tail key = some bodyValue → ∃ arm ∈ tail, arm.key = key ∧ arm.body = bodyValuehKey:head.key = keyhFind:head.body = bodyValue⊢ ∃ arm ∈ head :: tail, arm.key = key ∧ arm.body = bodyValue
        cases hFindpos.reflbody:Typekey:SelectArmKeyhead:SelectArm bodytail:List (SelectArm body)hKey:head.key = keyih:findArmBody? tail key = some head.body → ∃ arm ∈ tail, arm.key = key ∧ arm.body = head.body⊢ ∃ arm ∈ head :: tail, arm.key = key ∧ arm.body = head.body
        exact ⟨head, bybody:Typekey:SelectArmKeyhead:SelectArm bodytail:List (SelectArm body)hKey:head.key = keyih:findArmBody? tail key = some head.body → ∃ arm ∈ tail, arm.key = key ∧ arm.body = head.body⊢ head ∈ head :: tail simpAll goals completed! 🐙, hKey, rfl⟩
      ·negbody:Typekey:SelectArmKeybodyValue:bodyhead:SelectArm bodytail:List (SelectArm body)ih:findArmBody? tail key = some bodyValue → ∃ arm ∈ tail, arm.key = key ∧ arm.body = bodyValuehFind:Option.map SelectArm.body
    (match decide (head.key = key) with
    | true => some head
    | false => List.find? (fun arm => decide (arm.key = key)) tail) =
  some bodyValuehKey:¬head.key = key⊢ ∃ arm ∈ head :: tail, arm.key = key ∧ arm.body = bodyValue simp [hKey] at hFindnegbody:Typekey:SelectArmKeybodyValue:bodyhead:SelectArm bodytail:List (SelectArm body)ih:findArmBody? tail key = some bodyValue → ∃ arm ∈ tail, arm.key = key ∧ arm.body = bodyValuehKey:¬head.key = keyhFind:∃ a, List.find? (fun arm => decide (arm.key = key)) tail = some a ∧ a.body = bodyValue⊢ ∃ arm ∈ head :: tail, arm.key = key ∧ arm.body = bodyValue
        rcases hFind with ⟨arm, hFindTail, hArmBody⟩negbody:Typekey:SelectArmKeybodyValue:bodyhead:SelectArm bodytail:List (SelectArm body)ih:findArmBody? tail key = some bodyValue → ∃ arm ∈ tail, arm.key = key ∧ arm.body = bodyValuehKey:¬head.key = keyarm:SelectArm bodyhFindTail:List.find? (fun arm => decide (arm.key = key)) tail = some armhArmBody:arm.body = bodyValue⊢ ∃ arm ∈ head :: tail, arm.key = key ∧ arm.body = bodyValue
        have hFindTailMapped : findArmBody? tail key = some bodyValue := bybody:Typearms:List (SelectArm body)key:SelectArmKeybodyValue:bodyhFind:findArmBody? arms key = some bodyValue⊢ ∃ arm ∈ arms, arm.key = key ∧ arm.body = bodyValue
          unfold findArmBody?body:Typekey:SelectArmKeybodyValue:bodyhead:SelectArm bodytail:List (SelectArm body)ih:findArmBody? tail key = some bodyValue → ∃ arm ∈ tail, arm.key = key ∧ arm.body = bodyValuehKey:¬head.key = keyarm:SelectArm bodyhFindTail:List.find? (fun arm => decide (arm.key = key)) tail = some armhArmBody:arm.body = bodyValue⊢ Option.map SelectArm.body (List.find? (fun arm => decide (arm.key = key)) tail) = some bodyValue
          rw [hFindTail]body:Typekey:SelectArmKeybodyValue:bodyhead:SelectArm bodytail:List (SelectArm body)ih:findArmBody? tail key = some bodyValue → ∃ arm ∈ tail, arm.key = key ∧ arm.body = bodyValuehKey:¬head.key = keyarm:SelectArm bodyhFindTail:List.find? (fun arm => decide (arm.key = key)) tail = some armhArmBody:arm.body = bodyValue⊢ Option.map SelectArm.body (some arm) = some bodyValue
          simp [hArmBody]All goals completed! 🐙
        rcases ih hFindTailMapped with ⟨arm, hArm, hArmKey, hArmBody⟩negbody:Typekey:SelectArmKeybodyValue:bodyhead:SelectArm bodytail:List (SelectArm body)ih:findArmBody? tail key = some bodyValue → ∃ arm ∈ tail, arm.key = key ∧ arm.body = bodyValuehKey:¬head.key = keyarm✝:SelectArm bodyhFindTail:List.find? (fun arm => decide (arm.key = key)) tail = some armhArmBody✝:arm.body = bodyValuehFindTailMapped:findArmBody? tail key = some bodyValuearm:SelectArm bodyhArm:arm ∈ tailhArmKey:arm.key = keyhArmBody:arm.body = bodyValue⊢ ∃ arm ∈ head :: tail, arm.key = key ∧ arm.body = bodyValue
        exact ⟨arm, List.mem_cons_of_mem head hArm, hArmKey, hArmBody⟩All goals completed! 🐙

Successful single-arm resolution preserves body provenance and records the canonical key.

private theorem resolveArm_ok_source
    {body : Type}
    {shape : SelectableOutputShape}
    {arm resolved : SelectArm body}
    (hResolve : resolveArm shape arm = Except.ok resolved) :
    arm.body = resolved.body ∧
      resolveArmKey shape arm.key = Except.ok resolved.key := bybody:Typeshape:SelectableOutputShapearm:SelectArm bodyresolved:SelectArm bodyhResolve:resolveArm shape arm = Except.ok resolved⊢ arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
  unfold resolveArm at hResolvebody:Typeshape:SelectableOutputShapearm:SelectArm bodyresolved:SelectArm bodyhResolve:Except.map (fun key => { key := key, body := arm.body }) (resolveArmKey shape arm.key) = Except.ok resolved⊢ arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
  cases hKey : resolveArmKey shape arm.key with
  | error err =>errorbody:Typeshape:SelectableOutputShapearm:SelectArm bodyresolved:SelectArm bodyhResolve:Except.map (fun key => { key := key, body := arm.body }) (resolveArmKey shape arm.key) = Except.ok resolvederr:SelectAdmissionErrorhKey:resolveArmKey shape arm.key = Except.error err⊢ arm.body = resolved.body ∧ Except.error err = Except.ok resolved.key
      rw [hKey] at hResolveerrorbody:Typeshape:SelectableOutputShapearm:SelectArm bodyresolved:SelectArm bodyerr:SelectAdmissionErrorhResolve:Except.map (fun key => { key := key, body := arm.body }) (Except.error err) = Except.ok resolvedhKey:resolveArmKey shape arm.key = Except.error err⊢ arm.body = resolved.body ∧ Except.error err = Except.ok resolved.key
      change Except.error err = Except.ok resolved at hResolveerrorbody:Typeshape:SelectableOutputShapearm:SelectArm bodyresolved:SelectArm bodyerr:SelectAdmissionErrorhKey:resolveArmKey shape arm.key = Except.error errhResolve:Except.error err = Except.ok resolved⊢ arm.body = resolved.body ∧ Except.error err = Except.ok resolved.key
      cases hResolveAll goals completed! 🐙
  | ok canonicalKey =>okbody:Typeshape:SelectableOutputShapearm:SelectArm bodyresolved:SelectArm bodyhResolve:Except.map (fun key => { key := key, body := arm.body }) (resolveArmKey shape arm.key) = Except.ok resolvedcanonicalKey:SelectArmKeyhKey:resolveArmKey shape arm.key = Except.ok canonicalKey⊢ arm.body = resolved.body ∧ Except.ok canonicalKey = Except.ok resolved.key
      rw [hKey] at hResolveokbody:Typeshape:SelectableOutputShapearm:SelectArm bodyresolved:SelectArm bodycanonicalKey:SelectArmKeyhResolve:Except.map (fun key => { key := key, body := arm.body }) (Except.ok canonicalKey) = Except.ok resolvedhKey:resolveArmKey shape arm.key = Except.ok canonicalKey⊢ arm.body = resolved.body ∧ Except.ok canonicalKey = Except.ok resolved.key
      change Except.ok { key := canonicalKey, body := arm.body } =
        Except.ok resolved at hResolveokbody:Typeshape:SelectableOutputShapearm:SelectArm bodyresolved:SelectArm bodycanonicalKey:SelectArmKeyhKey:resolveArmKey shape arm.key = Except.ok canonicalKeyhResolve:Except.ok { key := canonicalKey, body := arm.body } = Except.ok resolved⊢ arm.body = resolved.body ∧ Except.ok canonicalKey = Except.ok resolved.key
      cases hResolveok.reflbody:Typeshape:SelectableOutputShapearm:SelectArm bodycanonicalKey:SelectArmKeyhKey:resolveArmKey shape arm.key = Except.ok canonicalKey⊢ arm.body = { key := canonicalKey, body := arm.body }.body ∧
  Except.ok canonicalKey = Except.ok { key := canonicalKey, body := arm.body }.key
      exact ⟨rfl, bybody:Typeshape:SelectableOutputShapearm:SelectArm bodycanonicalKey:SelectArmKeyhKey:resolveArmKey shape arm.key = Except.ok canonicalKey⊢ Except.ok canonicalKey = Except.ok { key := canonicalKey, body := arm.body }.key simpAll goals completed! 🐙⟩

Successful source-arm resolution keeps every resolved arm tied to a source arm.

private theorem resolveArms_mem_source
    {body : Type}
    {shape : SelectableOutputShape}
    {arms resolvedArms : List (SelectArm body)}
    (hResolved : resolveArms shape arms = Except.ok resolvedArms)
    {resolved : SelectArm body}
    (hMem : resolved ∈ resolvedArms) :
    ∃ arm, arm ∈ arms ∧
      arm.body = resolved.body ∧
        resolveArmKey shape arm.key = Except.ok resolved.key := bybody:Typeshape:SelectableOutputShapearms:List (SelectArm body)resolvedArms:List (SelectArm body)hResolved:resolveArms shape arms = Except.ok resolvedArmsresolved:SelectArm bodyhMem:resolved ∈ resolvedArms⊢ ∃ arm ∈ arms, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
  induction arms generalizing resolvedArms with
  | nil =>nilbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape [] = Except.ok resolvedArmshMem:resolved ∈ resolvedArms⊢ ∃ arm ∈ [], arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
      unfold resolveArms at hResolvednilbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmshResolved:Except.ok [] = Except.ok resolvedArms⊢ ∃ arm ∈ [], arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
      cases hResolvednil.reflbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhMem:resolved ∈ []⊢ ∃ arm ∈ [], arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
      cases hMemAll goals completed! 🐙
  | cons head tail ih =>consbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hResolved:resolveArms shape (head :: tail) = Except.ok resolvedArmshMem:resolved ∈ resolvedArms⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
      unfold resolveArms at hResolvedconsbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmshResolved:((resolveArm shape head).bind fun resolved =>
    Except.map (fun resolvedRest => resolved :: resolvedRest) (resolveArms shape tail)) =
  Except.ok resolvedArms⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
      cases hHead : resolveArm shape head with
      | error err =>cons.errorbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmshResolved:((resolveArm shape head).bind fun resolved =>
    Except.map (fun resolvedRest => resolved :: resolvedRest) (resolveArms shape tail)) =
  Except.ok resolvedArmserr:SelectAdmissionErrorhHead:resolveArm shape head = Except.error err⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
          rw [hHead] at hResolvedcons.errorbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmserr:SelectAdmissionErrorhResolved:((Except.error err).bind fun resolved =>
    Except.map (fun resolvedRest => resolved :: resolvedRest) (resolveArms shape tail)) =
  Except.ok resolvedArmshHead:resolveArm shape head = Except.error err⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
          change Except.error err = Except.ok resolvedArms at hResolvedcons.errorbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmserr:SelectAdmissionErrorhHead:resolveArm shape head = Except.error errhResolved:Except.error err = Except.ok resolvedArms⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
          cases hResolvedAll goals completed! 🐙
      | ok resolvedHead =>cons.okbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmshResolved:((resolveArm shape head).bind fun resolved =>
    Except.map (fun resolvedRest => resolved :: resolvedRest) (resolveArms shape tail)) =
  Except.ok resolvedArmsresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHead⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
          rw [hHead] at hResolvedcons.okbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmsresolvedHead:SelectArm bodyhResolved:((Except.ok resolvedHead).bind fun resolved =>
    Except.map (fun resolvedRest => resolved :: resolvedRest) (resolveArms shape tail)) =
  Except.ok resolvedArmshHead:resolveArm shape head = Except.ok resolvedHead⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
          change
            (resolveArms shape tail).map
              (fun resolvedRest => resolvedHead :: resolvedRest) =
            Except.ok resolvedArms at hResolvedcons.okbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmsresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeadhResolved:Except.map (fun resolvedRest => resolvedHead :: resolvedRest) (resolveArms shape tail) = Except.ok resolvedArms⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
          cases hTail : resolveArms shape tail with
          | error err =>cons.ok.errorbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmsresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeadhResolved:Except.map (fun resolvedRest => resolvedHead :: resolvedRest) (resolveArms shape tail) = Except.ok resolvedArmserr:SelectAdmissionErrorhTail:resolveArms shape tail = Except.error err⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
              rw [hTail] at hResolvedcons.ok.errorbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmsresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeaderr:SelectAdmissionErrorhResolved:Except.map (fun resolvedRest => resolvedHead :: resolvedRest) (Except.error err) = Except.ok resolvedArmshTail:resolveArms shape tail = Except.error err⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
              change Except.error err = Except.ok resolvedArms at hResolvedcons.ok.errorbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmsresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeaderr:SelectAdmissionErrorhTail:resolveArms shape tail = Except.error errhResolved:Except.error err = Except.ok resolvedArms⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
              cases hResolvedAll goals completed! 🐙
          | ok resolvedTail =>cons.ok.okbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmsresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeadhResolved:Except.map (fun resolvedRest => resolvedHead :: resolvedRest) (resolveArms shape tail) = Except.ok resolvedArmsresolvedTail:List (SelectArm body)hTail:resolveArms shape tail = Except.ok resolvedTail⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
              rw [hTail] at hResolvedcons.ok.okbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmsresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeadresolvedTail:List (SelectArm body)hResolved:Except.map (fun resolvedRest => resolvedHead :: resolvedRest) (Except.ok resolvedTail) = Except.ok resolvedArmshTail:resolveArms shape tail = Except.ok resolvedTail⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
              change Except.ok (resolvedHead :: resolvedTail) =
                Except.ok resolvedArms at hResolvedcons.ok.okbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedArms:List (SelectArm body)hMem:resolved ∈ resolvedArmsresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeadresolvedTail:List (SelectArm body)hTail:resolveArms shape tail = Except.ok resolvedTailhResolved:Except.ok (resolvedHead :: resolvedTail) = Except.ok resolvedArms⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
              cases hResolvedcons.ok.ok.reflbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeadresolvedTail:List (SelectArm body)hTail:resolveArms shape tail = Except.ok resolvedTailhMem:resolved ∈ resolvedHead :: resolvedTail⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
              simp only [List.mem_cons] at hMemcons.ok.ok.reflbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeadresolvedTail:List (SelectArm body)hTail:resolveArms shape tail = Except.ok resolvedTailhMem:resolved = resolvedHead ∨ resolved ∈ resolvedTail⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
              rcases hMem with hHeadMem | hTailMemcons.ok.ok.refl.inlbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeadresolvedTail:List (SelectArm body)hTail:resolveArms shape tail = Except.ok resolvedTailhHeadMem:resolved = resolvedHead⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keycons.ok.ok.refl.inrbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeadresolvedTail:List (SelectArm body)hTail:resolveArms shape tail = Except.ok resolvedTailhTailMem:resolved ∈ resolvedTail⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
              ·cons.ok.ok.refl.inlbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeadresolvedTail:List (SelectArm body)hTail:resolveArms shape tail = Except.ok resolvedTailhHeadMem:resolved = resolvedHead⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key subst hHeadMemcons.ok.ok.refl.inlbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedTail:List (SelectArm body)hTail:resolveArms shape tail = Except.ok resolvedTailhHead:resolveArm shape head = Except.ok resolved⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
                have hSource := resolveArm_ok_source hHeadcons.ok.ok.refl.inlbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedTail:List (SelectArm body)hTail:resolveArms shape tail = Except.ok resolvedTailhHead:resolveArm shape head = Except.ok resolvedhSource:head.body = resolved.body ∧ resolveArmKey shape head.key = Except.ok resolved.key⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
                exact
                  ⟨ head
                  , bybody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedTail:List (SelectArm body)hTail:resolveArms shape tail = Except.ok resolvedTailhHead:resolveArm shape head = Except.ok resolvedhSource:head.body = resolved.body ∧ resolveArmKey shape head.key = Except.ok resolved.key⊢ head ∈ head :: tail simpAll goals completed! 🐙
                  , hSource.left
                  , hSource.right
                  ⟩
              ·cons.ok.ok.refl.inrbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeadresolvedTail:List (SelectArm body)hTail:resolveArms shape tail = Except.ok resolvedTailhTailMem:resolved ∈ resolvedTail⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key rcases ih hTail hTailMem with
                  ⟨arm, hArm, hBody, hResolvedKey⟩cons.ok.ok.refl.inrbody:Typeshape:SelectableOutputShaperesolved:SelectArm bodyhead:SelectArm bodytail:List (SelectArm body)ih:∀ {resolvedArms : List (SelectArm body)},
  resolveArms shape tail = Except.ok resolvedArms →
    resolved ∈ resolvedArms →
      ∃ arm ∈ tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.keyresolvedHead:SelectArm bodyhHead:resolveArm shape head = Except.ok resolvedHeadresolvedTail:List (SelectArm body)hTail:resolveArms shape tail = Except.ok resolvedTailhTailMem:resolved ∈ resolvedTailarm:SelectArm bodyhArm:arm ∈ tailhBody:arm.body = resolved.bodyhResolvedKey:resolveArmKey shape arm.key = Except.ok resolved.key⊢ ∃ arm ∈ head :: tail, arm.body = resolved.body ∧ resolveArmKey shape arm.key = Except.ok resolved.key
                exact
                  ⟨ arm
                  , List.mem_cons_of_mem head hArm
                  , hBody
                  , hResolvedKey
                  ⟩All goals completed! 🐙

Collected entries are sourced from the already-resolved source arm list.

private theorem collectEntriesFrom_mem_resolved
    {body : Type}
    {armPorts : List (SelectArmKey × PortSignature)}
    {arms : List (SelectArm body)}
    {collected : CollectedEntries body (armPorts.map Prod.fst)}
    (hCollected : collectEntriesFrom armPorts arms = Except.ok collected)
    {entry : SelectArmKey × body}
    (hEntry : entry ∈ collected.entries) :
    ∃ arm, arm ∈ arms ∧ arm.key = entry.fst ∧ arm.body = entry.snd := bybody:TypearmPorts:List (SelectArmKey × PortSignature)arms:List (SelectArm body)collected:CollectedEntries body (List.map Prod.fst armPorts)hCollected:collectEntriesFrom armPorts arms = Except.ok collectedentry:SelectArmKey × bodyhEntry:entry ∈ collected.entries⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
  induction armPorts with
  | nil =>nilbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodycollected:CollectedEntries body (List.map Prod.fst [])hCollected:collectEntriesFrom [] arms = Except.ok collectedhEntry:entry ∈ collected.entries⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
      unfold collectEntriesFrom at hCollectednilbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodycollected:CollectedEntries body (List.map Prod.fst [])hEntry:entry ∈ collected.entrieshCollected:Except.ok { entries := [], entries_keys_exact := ⋯ } = Except.ok collected⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
      change Except.ok { entries := [], entries_keys_exact := rfl } =
        Except.ok collected at hCollectednilbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodycollected:CollectedEntries body (List.map Prod.fst [])hEntry:entry ∈ collected.entrieshCollected:Except.ok { entries := [], entries_keys_exact := ⋯ } = Except.ok collected⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
      cases hCollectednil.reflbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyhEntry:entry ∈ { entries := [], entries_keys_exact := ⋯ }.entries⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
      cases hEntryAll goals completed! 🐙
  | cons armPort rest ih =>consbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2collected:CollectedEntries body (List.map Prod.fst (armPort :: rest))hCollected:collectEntriesFrom (armPort :: rest) arms = Except.ok collectedhEntry:entry ∈ collected.entries⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
      unfold collectEntriesFrom at hCollectedconsbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2collected:CollectedEntries body (List.map Prod.fst (armPort :: rest))hEntry:entry ∈ collected.entrieshCollected:(match findArmBody? arms armPort.1 with
  | none => Except.error (SelectAdmissionError.uncoveredShapeArm armPort.1)
  | some bodyValue =>
    match collectEntriesFrom rest arms with
    | Except.error error => Except.error error
    | Except.ok collected =>
      Except.ok { entries := (armPort.1, bodyValue) :: collected.entries, entries_keys_exact := ⋯ }) =
  Except.ok collected⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
      cases hFind : findArmBody? arms armPort.fst with
      | none =>cons.nonebody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2collected:CollectedEntries body (List.map Prod.fst (armPort :: rest))hEntry:entry ∈ collected.entrieshCollected:(match findArmBody? arms armPort.1 with
  | none => Except.error (SelectAdmissionError.uncoveredShapeArm armPort.1)
  | some bodyValue =>
    match collectEntriesFrom rest arms with
    | Except.error error => Except.error error
    | Except.ok collected =>
      Except.ok { entries := (armPort.1, bodyValue) :: collected.entries, entries_keys_exact := ⋯ }) =
  Except.ok collectedhFind:findArmBody? arms armPort.1 = none⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
          rw [hFind] at hCollectedcons.nonebody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2collected:CollectedEntries body (List.map Prod.fst (armPort :: rest))hEntry:entry ∈ collected.entrieshCollected:(match none with
  | none => Except.error (SelectAdmissionError.uncoveredShapeArm armPort.1)
  | some bodyValue =>
    match collectEntriesFrom rest arms with
    | Except.error error => Except.error error
    | Except.ok collected =>
      Except.ok { entries := (armPort.1, bodyValue) :: collected.entries, entries_keys_exact := ⋯ }) =
  Except.ok collectedhFind:findArmBody? arms armPort.1 = none⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
          change Except.error (SelectAdmissionError.uncoveredShapeArm armPort.fst) =
            Except.ok collected at hCollectedcons.nonebody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2collected:CollectedEntries body (List.map Prod.fst (armPort :: rest))hEntry:entry ∈ collected.entrieshFind:findArmBody? arms armPort.1 = nonehCollected:Except.error (SelectAdmissionError.uncoveredShapeArm armPort.1) = Except.ok collected⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
          cases hCollectedAll goals completed! 🐙
      | some bodyValue =>cons.somebody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2collected:CollectedEntries body (List.map Prod.fst (armPort :: rest))hEntry:entry ∈ collected.entrieshCollected:(match findArmBody? arms armPort.1 with
  | none => Except.error (SelectAdmissionError.uncoveredShapeArm armPort.1)
  | some bodyValue =>
    match collectEntriesFrom rest arms with
    | Except.error error => Except.error error
    | Except.ok collected =>
      Except.ok { entries := (armPort.1, bodyValue) :: collected.entries, entries_keys_exact := ⋯ }) =
  Except.ok collectedbodyValue:bodyhFind:findArmBody? arms armPort.1 = some bodyValue⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
          rw [hFind] at hCollectedcons.somebody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2collected:CollectedEntries body (List.map Prod.fst (armPort :: rest))hEntry:entry ∈ collected.entriesbodyValue:bodyhCollected:(match some bodyValue with
  | none => Except.error (SelectAdmissionError.uncoveredShapeArm armPort.1)
  | some bodyValue =>
    match collectEntriesFrom rest arms with
    | Except.error error => Except.error error
    | Except.ok collected =>
      Except.ok { entries := (armPort.1, bodyValue) :: collected.entries, entries_keys_exact := ⋯ }) =
  Except.ok collectedhFind:findArmBody? arms armPort.1 = some bodyValue⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
          cases hRest : collectEntriesFrom rest arms with
          | error err =>cons.some.errorbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2collected:CollectedEntries body (List.map Prod.fst (armPort :: rest))hEntry:entry ∈ collected.entriesbodyValue:bodyhCollected:(match some bodyValue with
  | none => Except.error (SelectAdmissionError.uncoveredShapeArm armPort.1)
  | some bodyValue =>
    match collectEntriesFrom rest arms with
    | Except.error error => Except.error error
    | Except.ok collected =>
      Except.ok { entries := (armPort.1, bodyValue) :: collected.entries, entries_keys_exact := ⋯ }) =
  Except.ok collectedhFind:findArmBody? arms armPort.1 = some bodyValueerr:SelectAdmissionErrorhRest:collectEntriesFrom rest arms = Except.error err⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
              rw [hRest] at hCollectedcons.some.errorbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2collected:CollectedEntries body (List.map Prod.fst (armPort :: rest))hEntry:entry ∈ collected.entriesbodyValue:bodyhFind:findArmBody? arms armPort.1 = some bodyValueerr:SelectAdmissionErrorhCollected:(match some bodyValue with
  | none => Except.error (SelectAdmissionError.uncoveredShapeArm armPort.1)
  | some bodyValue =>
    match Except.error err with
    | Except.error error => Except.error error
    | Except.ok collected =>
      Except.ok { entries := (armPort.1, bodyValue) :: collected.entries, entries_keys_exact := ⋯ }) =
  Except.ok collectedhRest:collectEntriesFrom rest arms = Except.error err⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
              change Except.error err = Except.ok collected at hCollectedcons.some.errorbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2collected:CollectedEntries body (List.map Prod.fst (armPort :: rest))hEntry:entry ∈ collected.entriesbodyValue:bodyhFind:findArmBody? arms armPort.1 = some bodyValueerr:SelectAdmissionErrorhRest:collectEntriesFrom rest arms = Except.error errhCollected:Except.error err = Except.ok collected⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
              cases hCollectedAll goals completed! 🐙
          | ok collectedRest =>cons.some.okbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2collected:CollectedEntries body (List.map Prod.fst (armPort :: rest))hEntry:entry ∈ collected.entriesbodyValue:bodyhCollected:(match some bodyValue with
  | none => Except.error (SelectAdmissionError.uncoveredShapeArm armPort.1)
  | some bodyValue =>
    match collectEntriesFrom rest arms with
    | Except.error error => Except.error error
    | Except.ok collected =>
      Except.ok { entries := (armPort.1, bodyValue) :: collected.entries, entries_keys_exact := ⋯ }) =
  Except.ok collectedhFind:findArmBody? arms armPort.1 = some bodyValuecollectedRest:CollectedEntries body (List.map Prod.fst rest)hRest:collectEntriesFrom rest arms = Except.ok collectedRest⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
              rw [hRest] at hCollectedcons.some.okbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2collected:CollectedEntries body (List.map Prod.fst (armPort :: rest))hEntry:entry ∈ collected.entriesbodyValue:bodyhFind:findArmBody? arms armPort.1 = some bodyValuecollectedRest:CollectedEntries body (List.map Prod.fst rest)hCollected:(match some bodyValue with
  | none => Except.error (SelectAdmissionError.uncoveredShapeArm armPort.1)
  | some bodyValue =>
    match Except.ok collectedRest with
    | Except.error error => Except.error error
    | Except.ok collected =>
      Except.ok { entries := (armPort.1, bodyValue) :: collected.entries, entries_keys_exact := ⋯ }) =
  Except.ok collectedhRest:collectEntriesFrom rest arms = Except.ok collectedRest⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
              change
                Except.ok
                  { entries := (armPort.fst, bodyValue) :: collectedRest.entries
                    entries_keys_exact := _ } =
                Except.ok collected at hCollectedcons.some.okbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2collected:CollectedEntries body (List.map Prod.fst (armPort :: rest))hEntry:entry ∈ collected.entriesbodyValue:bodyhFind:findArmBody? arms armPort.1 = some bodyValuecollectedRest:CollectedEntries body (List.map Prod.fst rest)hRest:collectEntriesFrom rest arms = Except.ok collectedResthCollected:Except.ok { entries := (armPort.1, bodyValue) :: collectedRest.entries, entries_keys_exact := ⋯ } = Except.ok collected⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
              cases hCollectedcons.some.ok.reflbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2bodyValue:bodyhFind:findArmBody? arms armPort.1 = some bodyValuecollectedRest:CollectedEntries body (List.map Prod.fst rest)hRest:collectEntriesFrom rest arms = Except.ok collectedResthEntry:entry ∈ { entries := (armPort.1, bodyValue) :: collectedRest.entries, entries_keys_exact := ⋯ }.entries⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
              simp only [List.mem_cons] at hEntrycons.some.ok.reflbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2bodyValue:bodyhFind:findArmBody? arms armPort.1 = some bodyValuecollectedRest:CollectedEntries body (List.map Prod.fst rest)hRest:collectEntriesFrom rest arms = Except.ok collectedResthEntry:entry = (armPort.1, bodyValue) ∨ entry ∈ collectedRest.entries⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
              rcases hEntry with hHead | hTailcons.some.ok.refl.inlbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2bodyValue:bodyhFind:findArmBody? arms armPort.1 = some bodyValuecollectedRest:CollectedEntries body (List.map Prod.fst rest)hRest:collectEntriesFrom rest arms = Except.ok collectedResthHead:entry = (armPort.1, bodyValue)⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2cons.some.ok.refl.inrbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2bodyValue:bodyhFind:findArmBody? arms armPort.1 = some bodyValuecollectedRest:CollectedEntries body (List.map Prod.fst rest)hRest:collectEntriesFrom rest arms = Except.ok collectedResthTail:entry ∈ collectedRest.entries⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2
              ·cons.some.ok.refl.inlbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2bodyValue:bodyhFind:findArmBody? arms armPort.1 = some bodyValuecollectedRest:CollectedEntries body (List.map Prod.fst rest)hRest:collectEntriesFrom rest arms = Except.ok collectedResthHead:entry = (armPort.1, bodyValue)⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2 cases hHeadcons.some.ok.refl.inl.reflbody:Typearms:List (SelectArm body)armPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)bodyValue:bodyhFind:findArmBody? arms armPort.1 = some bodyValuecollectedRest:CollectedEntries body (List.map Prod.fst rest)hRest:collectEntriesFrom rest arms = Except.ok collectedRestih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    (armPort.1, bodyValue) ∈ collected.entries →
      ∃ arm ∈ arms, arm.key = (armPort.1, bodyValue).1 ∧ arm.body = (armPort.1, bodyValue).2⊢ ∃ arm ∈ arms, arm.key = (armPort.1, bodyValue).1 ∧ arm.body = (armPort.1, bodyValue).2
                rcases findArmBody?_some hFind with
                  ⟨arm, hArm, hArmKey, hArmBody⟩cons.some.ok.refl.inl.reflbody:Typearms:List (SelectArm body)armPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)bodyValue:bodyhFind:findArmBody? arms armPort.1 = some bodyValuecollectedRest:CollectedEntries body (List.map Prod.fst rest)hRest:collectEntriesFrom rest arms = Except.ok collectedRestih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    (armPort.1, bodyValue) ∈ collected.entries →
      ∃ arm ∈ arms, arm.key = (armPort.1, bodyValue).1 ∧ arm.body = (armPort.1, bodyValue).2arm:SelectArm bodyhArm:arm ∈ armshArmKey:arm.key = armPort.1hArmBody:arm.body = bodyValue⊢ ∃ arm ∈ arms, arm.key = (armPort.1, bodyValue).1 ∧ arm.body = (armPort.1, bodyValue).2
                exact ⟨arm, hArm, hArmKey, hArmBody⟩All goals completed! 🐙
              ·cons.some.ok.refl.inrbody:Typearms:List (SelectArm body)entry:SelectArmKey × bodyarmPort:SelectArmKey × PortSignaturerest:List (SelectArmKey × PortSignature)ih:∀ {collected : CollectedEntries body (List.map Prod.fst rest)},
  collectEntriesFrom rest arms = Except.ok collected →
    entry ∈ collected.entries → ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2bodyValue:bodyhFind:findArmBody? arms armPort.1 = some bodyValuecollectedRest:CollectedEntries body (List.map Prod.fst rest)hRest:collectEntriesFrom rest arms = Except.ok collectedResthTail:entry ∈ collectedRest.entries⊢ ∃ arm ∈ arms, arm.key = entry.1 ∧ arm.body = entry.2 exact ih hRest hTailAll goals completed! 🐙

Admit a source select(...) clause whose base is an AcceptedNodeDecl, projecting the exclusive output sum from the node's authored OutputShape.

This is the certified entry point: it ties admission to the actual base graph boundary instead of consuming an unrelated SelectableOutputShape. The projection through SelectableOutputShape.ofAcceptedNode? returns none for any node whose authored output frontier is not exactly one exclusive output sum group; that case yields SelectAdmissionError.nonExclusiveBase rather than admitting against an unrelated shape.

def admitClauseAtNode
    {body : Type}
    (clause : SelectExpr AcceptedNodeDecl body) :
    Except SelectAdmissionError (LatentSelectAdmission body) :=
  match SelectableOutputShape.ofAcceptedNode? clause.base with
  | none => Except.error SelectAdmissionError.nonExclusiveBase
  | some shape => admitClause shape clause

A non-exclusive node base is rejected by admitClauseAtNode.

theorem admitClauseAtNode_nonExclusive
    {body : Type}
    (clause : SelectExpr AcceptedNodeDecl body)
    (hShape : SelectableOutputShape.ofAcceptedNode? clause.base = none) :
    admitClauseAtNode clause =
      Except.error SelectAdmissionError.nonExclusiveBase := bybody:Typeclause:SelectExpr AcceptedNodeDecl bodyhShape:SelectableOutputShape.ofAcceptedNode? clause.base = none⊢ admitClauseAtNode clause = Except.error SelectAdmissionError.nonExclusiveBase
  unfold admitClauseAtNodebody:Typeclause:SelectExpr AcceptedNodeDecl bodyhShape:SelectableOutputShape.ofAcceptedNode? clause.base = none⊢ (match SelectableOutputShape.ofAcceptedNode? clause.base with
  | none => Except.error SelectAdmissionError.nonExclusiveBase
  | some shape => admitClause shape clause) =
  Except.error SelectAdmissionError.nonExclusiveBase
  rw [hShape]All goals completed! 🐙

namespace LatentSelectAdmission

Body-provenance predicate for an admitted select clause.

LatentSelectAdmission intentionally stays a reusable key-set carrier. This predicate is the named obligation for slices that need to prove each latent body came from a source arm, and that the source arm resolves to the admitted canonical key.

def FromClause
    {base body : Type}
    (admission : LatentSelectAdmission body)
    (clause : SelectExpr base body) :
    Prop :=
  ∀ entry,
    entry ∈ admission.entries →
      ∃ arm,
        arm ∈ clause.arms ∧
          arm.body = entry.snd ∧
            resolveArmKey admission.shape arm.key = Except.ok entry.fst

end LatentSelectAdmission

Successful admitClause construction witnesses source-arm body provenance.

theorem admitClause_fromClause
    {base body : Type}
    (shape : SelectableOutputShape)
    (clause : SelectExpr base body)
    {admission : LatentSelectAdmission body}
    (hAdmit : admitClause shape clause = Except.ok admission) :
    admission.FromClause clause := bybase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyhAdmit:admitClause shape clause = Except.ok admission⊢ admission.FromClause clause
  unfold admitClause at hAdmitbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyhAdmit:((resolveArms shape clause.arms).bind fun resolvedArms =>
    (detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
      Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admission⊢ admission.FromClause clause
  cases hResolved : resolveArms shape clause.arms with
  | error err =>errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyhAdmit:((resolveArms shape clause.arms).bind fun resolvedArms =>
    (detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
      Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionerr:SelectAdmissionErrorhResolved:resolveArms shape clause.arms = Except.error err⊢ admission.FromClause clause
      rw [hResolved] at hAdmiterrorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyerr:SelectAdmissionErrorhAdmit:((Except.error err).bind fun resolvedArms =>
    (detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
      Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionhResolved:resolveArms shape clause.arms = Except.error err⊢ admission.FromClause clause
      change Except.error err = Except.ok admission at hAdmiterrorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyerr:SelectAdmissionErrorhResolved:resolveArms shape clause.arms = Except.error errhAdmit:Except.error err = Except.ok admission⊢ admission.FromClause clause
      cases hAdmitAll goals completed! 🐙
  | ok resolvedArms =>okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyhAdmit:((resolveArms shape clause.arms).bind fun resolvedArms =>
    (detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
      Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms⊢ admission.FromClause clause
      rw [hResolved] at hAdmitokbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hAdmit:((Except.ok resolvedArms).bind fun resolvedArms =>
    (detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
      Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionhResolved:resolveArms shape clause.arms = Except.ok resolvedArms⊢ admission.FromClause clause
      change
        (detectDuplicateArm (resolvedArms.map SelectArm.key)).bind
          (fun _ =>
            (collectEntries shape resolvedArms).map
              (fun collected => collectedEntriesAdmission shape collected)) =
          Except.ok admission at hAdmitokbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArmshAdmit:((detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
    Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admission⊢ admission.FromClause clause
      cases hDuplicate : detectDuplicateArm (resolvedArms.map SelectArm.key) with
      | error err =>ok.errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArmshAdmit:((detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
    Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionerr:SelectAdmissionErrorhDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.error err⊢ admission.FromClause clause
          rw [hDuplicate] at hAdmitok.errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArmserr:SelectAdmissionErrorhAdmit:((Except.error err).bind fun x =>
    Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionhDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.error err⊢ admission.FromClause clause
          change Except.error err = Except.ok admission at hAdmitok.errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArmserr:SelectAdmissionErrorhDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.error errhAdmit:Except.error err = Except.ok admission⊢ admission.FromClause clause
          cases hAdmitAll goals completed! 🐙
      | ok _unit =>ok.okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArmshAdmit:((detectDuplicateArm (List.map SelectArm.key resolvedArms)).bind fun x =>
    Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admission_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unit⊢ admission.FromClause clause
          rw [hDuplicate] at hAdmitok.okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithAdmit:((Except.ok _unit).bind fun x =>
    Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms)) =
  Except.ok admissionhDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unit⊢ admission.FromClause clause
          change
            (collectEntries shape resolvedArms).map
              (fun collected => collectedEntriesAdmission shape collected) =
            Except.ok admission at hAdmitok.okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unithAdmit:Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms) =
  Except.ok admission⊢ admission.FromClause clause
          cases hCollected : collectEntries shape resolvedArms with
          | error err =>ok.ok.errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unithAdmit:Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms) =
  Except.ok admissionerr:SelectAdmissionErrorhCollected:collectEntries shape resolvedArms = Except.error err⊢ admission.FromClause clause
              rw [hCollected] at hAdmitok.ok.errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _uniterr:SelectAdmissionErrorhAdmit:Except.map (fun collected => collectedEntriesAdmission shape collected) (Except.error err) = Except.ok admissionhCollected:collectEntries shape resolvedArms = Except.error err⊢ admission.FromClause clause
              change Except.error err = Except.ok admission at hAdmitok.ok.errorbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _uniterr:SelectAdmissionErrorhCollected:collectEntries shape resolvedArms = Except.error errhAdmit:Except.error err = Except.ok admission⊢ admission.FromClause clause
              cases hAdmitAll goals completed! 🐙
          | ok collected =>ok.ok.okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unithAdmit:Except.map (fun collected => collectedEntriesAdmission shape collected) (collectEntries shape resolvedArms) =
  Except.ok admissioncollected:CollectedEntries body shape.armKeyshCollected:collectEntries shape resolvedArms = Except.ok collected⊢ admission.FromClause clause
              rw [hCollected] at hAdmitok.ok.okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unitcollected:CollectedEntries body shape.armKeyshAdmit:Except.map (fun collected => collectedEntriesAdmission shape collected) (Except.ok collected) = Except.ok admissionhCollected:collectEntries shape resolvedArms = Except.ok collected⊢ admission.FromClause clause
              change Except.ok (collectedEntriesAdmission shape collected) =
                Except.ok admission at hAdmitok.ok.okbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyadmission:LatentSelectAdmission bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unitcollected:CollectedEntries body shape.armKeyshCollected:collectEntries shape resolvedArms = Except.ok collectedhAdmit:Except.ok (collectedEntriesAdmission shape collected) = Except.ok admission⊢ admission.FromClause clause
              cases hAdmitok.ok.ok.reflbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unitcollected:CollectedEntries body shape.armKeyshCollected:collectEntries shape resolvedArms = Except.ok collected⊢ (collectedEntriesAdmission shape collected).FromClause clause
              intro entry hEntryok.ok.ok.reflbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unitcollected:CollectedEntries body shape.armKeyshCollected:collectEntries shape resolvedArms = Except.ok collectedentry:SelectArmKey × bodyhEntry:entry ∈ (collectedEntriesAdmission shape collected).entries⊢ ∃ arm ∈ clause.arms,
  arm.body = entry.2 ∧ resolveArmKey (collectedEntriesAdmission shape collected).shape arm.key = Except.ok entry.1
              rcases collectEntriesFrom_mem_resolved hCollected hEntry with
                ⟨resolvedArm, hResolvedArm, hResolvedKey, hResolvedBody⟩ok.ok.ok.reflbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unitcollected:CollectedEntries body shape.armKeyshCollected:collectEntries shape resolvedArms = Except.ok collectedentry:SelectArmKey × bodyhEntry:entry ∈ (collectedEntriesAdmission shape collected).entriesresolvedArm:SelectArm bodyhResolvedArm:resolvedArm ∈ resolvedArmshResolvedKey:resolvedArm.key = entry.1hResolvedBody:resolvedArm.body = entry.2⊢ ∃ arm ∈ clause.arms,
  arm.body = entry.2 ∧ resolveArmKey (collectedEntriesAdmission shape collected).shape arm.key = Except.ok entry.1
              rcases resolveArms_mem_source hResolved hResolvedArm with
                ⟨sourceArm, hSourceArm, hSourceBody, hSourceKey⟩ok.ok.ok.reflbase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unitcollected:CollectedEntries body shape.armKeyshCollected:collectEntries shape resolvedArms = Except.ok collectedentry:SelectArmKey × bodyhEntry:entry ∈ (collectedEntriesAdmission shape collected).entriesresolvedArm:SelectArm bodyhResolvedArm:resolvedArm ∈ resolvedArmshResolvedKey:resolvedArm.key = entry.1hResolvedBody:resolvedArm.body = entry.2sourceArm:SelectArm bodyhSourceArm:sourceArm ∈ clause.armshSourceBody:sourceArm.body = resolvedArm.bodyhSourceKey:resolveArmKey shape sourceArm.key = Except.ok resolvedArm.key⊢ ∃ arm ∈ clause.arms,
  arm.body = entry.2 ∧ resolveArmKey (collectedEntriesAdmission shape collected).shape arm.key = Except.ok entry.1
              exact
                ⟨ sourceArm
                , hSourceArm
                , bybase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unitcollected:CollectedEntries body shape.armKeyshCollected:collectEntries shape resolvedArms = Except.ok collectedentry:SelectArmKey × bodyhEntry:entry ∈ (collectedEntriesAdmission shape collected).entriesresolvedArm:SelectArm bodyhResolvedArm:resolvedArm ∈ resolvedArmshResolvedKey:resolvedArm.key = entry.1hResolvedBody:resolvedArm.body = entry.2sourceArm:SelectArm bodyhSourceArm:sourceArm ∈ clause.armshSourceBody:sourceArm.body = resolvedArm.bodyhSourceKey:resolveArmKey shape sourceArm.key = Except.ok resolvedArm.key⊢ sourceArm.body = entry.2 rw [hSourceBody, hResolvedBody]All goals completed! 🐙
                , bybase:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unitcollected:CollectedEntries body shape.armKeyshCollected:collectEntries shape resolvedArms = Except.ok collectedentry:SelectArmKey × bodyhEntry:entry ∈ (collectedEntriesAdmission shape collected).entriesresolvedArm:SelectArm bodyhResolvedArm:resolvedArm ∈ resolvedArmshResolvedKey:resolvedArm.key = entry.1hResolvedBody:resolvedArm.body = entry.2sourceArm:SelectArm bodyhSourceArm:sourceArm ∈ clause.armshSourceBody:sourceArm.body = resolvedArm.bodyhSourceKey:resolveArmKey shape sourceArm.key = Except.ok resolvedArm.key⊢ resolveArmKey (collectedEntriesAdmission shape collected).shape sourceArm.key = Except.ok entry.1 rw [← hResolvedKey]base:Typebody:Typeshape:SelectableOutputShapeclause:SelectExpr base bodyresolvedArms:List (SelectArm body)hResolved:resolveArms shape clause.arms = Except.ok resolvedArms_unit:UnithDuplicate:detectDuplicateArm (List.map SelectArm.key resolvedArms) = Except.ok _unitcollected:CollectedEntries body shape.armKeyshCollected:collectEntries shape resolvedArms = Except.ok collectedentry:SelectArmKey × bodyhEntry:entry ∈ (collectedEntriesAdmission shape collected).entriesresolvedArm:SelectArm bodyhResolvedArm:resolvedArm ∈ resolvedArmshResolvedKey:resolvedArm.key = entry.1hResolvedBody:resolvedArm.body = entry.2sourceArm:SelectArm bodyhSourceArm:sourceArm ∈ clause.armshSourceBody:sourceArm.body = resolvedArm.bodyhSourceKey:resolveArmKey shape sourceArm.key = Except.ok resolvedArm.key⊢ resolveArmKey (collectedEntriesAdmission shape collected).shape sourceArm.key = Except.ok resolvedArm.key; exact hSourceKeyAll goals completed! 🐙
                ⟩

Successful node-based select(...) admission witnesses source-arm body provenance.

theorem admitClauseAtNode_fromClause
    {body : Type}
    (clause : SelectExpr AcceptedNodeDecl body)
    {admission : LatentSelectAdmission body}
    (hAdmit : admitClauseAtNode clause = Except.ok admission) :
    admission.FromClause clause := bybody:Typeclause:SelectExpr AcceptedNodeDecl bodyadmission:LatentSelectAdmission bodyhAdmit:admitClauseAtNode clause = Except.ok admission⊢ admission.FromClause clause
  unfold admitClauseAtNode at hAdmitbody:Typeclause:SelectExpr AcceptedNodeDecl bodyadmission:LatentSelectAdmission bodyhAdmit:(match SelectableOutputShape.ofAcceptedNode? clause.base with
  | none => Except.error SelectAdmissionError.nonExclusiveBase
  | some shape => admitClause shape clause) =
  Except.ok admission⊢ admission.FromClause clause
  cases hShape : SelectableOutputShape.ofAcceptedNode? clause.base with
  | none =>nonebody:Typeclause:SelectExpr AcceptedNodeDecl bodyadmission:LatentSelectAdmission bodyhAdmit:(match SelectableOutputShape.ofAcceptedNode? clause.base with
  | none => Except.error SelectAdmissionError.nonExclusiveBase
  | some shape => admitClause shape clause) =
  Except.ok admissionhShape:SelectableOutputShape.ofAcceptedNode? clause.base = none⊢ admission.FromClause clause
      rw [hShape] at hAdmitnonebody:Typeclause:SelectExpr AcceptedNodeDecl bodyadmission:LatentSelectAdmission bodyhAdmit:(match none with
  | none => Except.error SelectAdmissionError.nonExclusiveBase
  | some shape => admitClause shape clause) =
  Except.ok admissionhShape:SelectableOutputShape.ofAcceptedNode? clause.base = none⊢ admission.FromClause clause
      change Except.error SelectAdmissionError.nonExclusiveBase =
        Except.ok admission at hAdmitnonebody:Typeclause:SelectExpr AcceptedNodeDecl bodyadmission:LatentSelectAdmission bodyhShape:SelectableOutputShape.ofAcceptedNode? clause.base = nonehAdmit:Except.error SelectAdmissionError.nonExclusiveBase = Except.ok admission⊢ admission.FromClause clause
      cases hAdmitAll goals completed! 🐙
  | some shape =>somebody:Typeclause:SelectExpr AcceptedNodeDecl bodyadmission:LatentSelectAdmission bodyhAdmit:(match SelectableOutputShape.ofAcceptedNode? clause.base with
  | none => Except.error SelectAdmissionError.nonExclusiveBase
  | some shape => admitClause shape clause) =
  Except.ok admissionshape:SelectableOutputShapehShape:SelectableOutputShape.ofAcceptedNode? clause.base = some shape⊢ admission.FromClause clause
      rw [hShape] at hAdmitsomebody:Typeclause:SelectExpr AcceptedNodeDecl bodyadmission:LatentSelectAdmission bodyshape:SelectableOutputShapehAdmit:(match some shape with
  | none => Except.error SelectAdmissionError.nonExclusiveBase
  | some shape => admitClause shape clause) =
  Except.ok admissionhShape:SelectableOutputShape.ofAcceptedNode? clause.base = some shape⊢ admission.FromClause clause
      exact admitClause_fromClause shape clause hAdmitAll goals completed! 🐙

Bridge Into `LatentBranchFamily`

A caller-supplied per-arm SubgraphSpec family bundled with the disjointness and validity obligations required by LatentBranchFamily.

This is the minimal evidence the integrator must discharge to lift a LatentSelectAdmission (SubgraphSpec node) into the downstream branch family. The bridge is intentionally not derivable inside this admission layer: fragment validity and pairwise node disjointness depend on lower planner machinery that is outside the source-admission scope. The owner obligation keeps the retained rewrite anchor out of every latent fragment body before the runtime namespacing policy qualifies those body-local nodes.

structure FragmentEvidence
    {node : Type}
    [DecidableEq node]
    (admission : LatentSelectAdmission (Cortex.Wire.SubgraphSpec node))
    (owner : node) : Prop where

Every entry's body is a valid inserted subgraph.

  fragmentsValid :
    ∀ entry, entry ∈ admission.entries → entry.snd.Valid

The retained select owner is not one of the latent fragment's local nodes.

  ownerNotInFragments :
    ∀ entry,
      entry ∈ admission.entries →
        owner ∉ (Cortex.Graph.denote entry.snd.topology).vertices

Distinct admitted entries expose disjoint compiler-qualified fragment nodes.

  fragmentsPairwiseDisjoint :
    ∀ left right,
      left ∈ admission.entries →
        right ∈ admission.entries →
          left.fst ≠ right.fst →
            ∀ nodeId,
              nodeId ∈ (Cortex.Graph.denote left.snd.topology).vertices →
                nodeId ∈ (Cortex.Graph.denote right.snd.topology).vertices →
                  False

Local lookup lemma used by the bridge: for a duplicate-free key list, membership uniquely determines List.find? over the equality predicate.

Mathlib currently has general find? characterizations such as List.find?_eq_some_iff_getElem; under this file's imports there is no keyed Nodup convenience lemma with this exact shape, so we keep the local version.

private theorem find_key_eq_some_of_mem_nodup
    {α β : Type}
    [DecidableEq α]
    {entries : List (α × β)}
    (hUnique : (entries.map Prod.fst).Nodup)
    {entry : α × β}
    (hEntry : entry ∈ entries) :
    entries.find? (fun candidate => candidate.fst = entry.fst) = some entry := byα:Typeβ:Typeinst✝:DecidableEq αentries:List (α × β)hUnique:(List.map Prod.fst entries).Nodupentry:α × βhEntry:entry ∈ entries⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) entries = some entry
  induction entries with
  | nil =>nilα:Typeβ:Typeinst✝:DecidableEq αentry:α × βhUnique:(List.map Prod.fst []).NoduphEntry:entry ∈ []⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) [] = some entry cases hEntryAll goals completed! 🐙
  | cons head tail ih =>consα:Typeβ:Typeinst✝:DecidableEq αentry:α × βhead:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhUnique:(List.map Prod.fst (head :: tail)).NoduphEntry:entry ∈ head :: tail⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) (head :: tail) = some entry
      simp only [List.map_cons, List.nodup_cons] at hUniqueconsα:Typeβ:Typeinst✝:DecidableEq αentry:α × βhead:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhEntry:entry ∈ head :: tailhUnique:head.1 ∉ List.map Prod.fst tail ∧ (List.map Prod.fst tail).Nodup⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) (head :: tail) = some entry
      obtain ⟨hHeadFresh, hTailUnique⟩ := hUniqueconsα:Typeβ:Typeinst✝:DecidableEq αentry:α × βhead:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhEntry:entry ∈ head :: tailhHeadFresh:head.1 ∉ List.map Prod.fst tailhTailUnique:(List.map Prod.fst tail).Nodup⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) (head :: tail) = some entry
      simp only [List.mem_cons] at hEntryconsα:Typeβ:Typeinst✝:DecidableEq αentry:α × βhead:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhHeadFresh:head.1 ∉ List.map Prod.fst tailhTailUnique:(List.map Prod.fst tail).NoduphEntry:entry = head ∨ entry ∈ tail⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) (head :: tail) = some entry
      rcases hEntry with hHeadEq | hTailMemcons.inlα:Typeβ:Typeinst✝:DecidableEq αentry:α × βhead:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhHeadFresh:head.1 ∉ List.map Prod.fst tailhTailUnique:(List.map Prod.fst tail).NoduphHeadEq:entry = head⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) (head :: tail) = some entrycons.inrα:Typeβ:Typeinst✝:DecidableEq αentry:α × βhead:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhHeadFresh:head.1 ∉ List.map Prod.fst tailhTailUnique:(List.map Prod.fst tail).NoduphTailMem:entry ∈ tail⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) (head :: tail) = some entry
      ·cons.inlα:Typeβ:Typeinst✝:DecidableEq αentry:α × βhead:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhHeadFresh:head.1 ∉ List.map Prod.fst tailhTailUnique:(List.map Prod.fst tail).NoduphHeadEq:entry = head⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) (head :: tail) = some entry subst hHeadEqcons.inlα:Typeβ:Typeinst✝:DecidableEq αentry:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhTailUnique:(List.map Prod.fst tail).NoduphHeadFresh:entry.1 ∉ List.map Prod.fst tail⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) (entry :: tail) = some entry
        simpAll goals completed! 🐙
      ·cons.inrα:Typeβ:Typeinst✝:DecidableEq αentry:α × βhead:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhHeadFresh:head.1 ∉ List.map Prod.fst tailhTailUnique:(List.map Prod.fst tail).NoduphTailMem:entry ∈ tail⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) (head :: tail) = some entry have hHeadKey : head.fst ≠ entry.fst := byα:Typeβ:Typeinst✝:DecidableEq αentries:List (α × β)hUnique:(List.map Prod.fst entries).Nodupentry:α × βhEntry:entry ∈ entries⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) entries = some entry
          intro hEqα:Typeβ:Typeinst✝:DecidableEq αentry:α × βhead:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhHeadFresh:head.1 ∉ List.map Prod.fst tailhTailUnique:(List.map Prod.fst tail).NoduphTailMem:entry ∈ tailhEq:head.1 = entry.1⊢ False
          apply hHeadFreshα:Typeβ:Typeinst✝:DecidableEq αentry:α × βhead:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhHeadFresh:head.1 ∉ List.map Prod.fst tailhTailUnique:(List.map Prod.fst tail).NoduphTailMem:entry ∈ tailhEq:head.1 = entry.1⊢ head.1 ∈ List.map Prod.fst tail
          rw [hEq]α:Typeβ:Typeinst✝:DecidableEq αentry:α × βhead:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhHeadFresh:head.1 ∉ List.map Prod.fst tailhTailUnique:(List.map Prod.fst tail).NoduphTailMem:entry ∈ tailhEq:head.1 = entry.1⊢ entry.1 ∈ List.map Prod.fst tail
          exact List.mem_map_of_mem (f := Prod.fst) hTailMemAll goals completed! 🐙
        have hHeadDecide :
            (decide (head.fst = entry.fst)) = false :=
          decide_eq_false hHeadKeycons.inrα:Typeβ:Typeinst✝:DecidableEq αentry:α × βhead:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhHeadFresh:head.1 ∉ List.map Prod.fst tailhTailUnique:(List.map Prod.fst tail).NoduphTailMem:entry ∈ tailhHeadKey:head.1 ≠ entry.1hHeadDecide:decide (head.1 = entry.1) = false⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) (head :: tail) = some entry
        simp only [List.find?_cons, hHeadDecide]cons.inrα:Typeβ:Typeinst✝:DecidableEq αentry:α × βhead:α × βtail:List (α × β)ih:(List.map Prod.fst tail).Nodup →
  entry ∈ tail → List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entryhHeadFresh:head.1 ∉ List.map Prod.fst tailhTailUnique:(List.map Prod.fst tail).NoduphTailMem:entry ∈ tailhHeadKey:head.1 ≠ entry.1hHeadDecide:decide (head.1 = entry.1) = false⊢ List.find? (fun candidate => decide (candidate.1 = entry.1)) tail = some entry
        exact ih hTailUnique hTailMemAll goals completed! 🐙

namespace LatentSelectAdmission

Empty subgraph spec used as the unreachable fallback in fragmentLookup.

private def emptyFallback {node : Type} : Cortex.Wire.SubgraphSpec node :=
  { topology := Cortex.Graph.Graph.empty
    definitions := ∅
    entryNodes := ∅
    exitNodes := ∅ }

Per-arm-key subgraph lookup used by the bridge. The fallback case is unreachable on admitted keys and is unobservable through the FragmentEvidence obligations, which only quote admitted entries.

def fragmentLookup
    {node : Type}
    (entries : List (SelectArmKey × Cortex.Wire.SubgraphSpec node))
    (key : SelectArmKey) :
    Cortex.Wire.SubgraphSpec node :=
  match entries.find? (fun entry => entry.fst = key) with
  | some entry => entry.snd
  | none => emptyFallback

The lookup returns the entry's subgraph for an admitted key in a duplicate-free entry list.

theorem fragmentLookup_entry
    {node : Type}
    {entries : List (SelectArmKey × Cortex.Wire.SubgraphSpec node)}
    (hUnique : (entries.map Prod.fst).Nodup)
    {entry : SelectArmKey × Cortex.Wire.SubgraphSpec node}
    (hEntry : entry ∈ entries) :
    fragmentLookup entries entry.fst = entry.snd := bynode:Typeentries:List (SelectArmKey × SubgraphSpec node)hUnique:(List.map Prod.fst entries).Nodupentry:SelectArmKey × SubgraphSpec nodehEntry:entry ∈ entries⊢ fragmentLookup entries entry.1 = entry.2
  show
    (match entries.find? (fun candidate => candidate.fst = entry.fst) with
      | some entry => entry.snd
      | none => emptyFallback) = entry.sndnode:Typeentries:List (SelectArmKey × SubgraphSpec node)hUnique:(List.map Prod.fst entries).Nodupentry:SelectArmKey × SubgraphSpec nodehEntry:entry ∈ entries⊢ (match List.find? (fun candidate => decide (candidate.1 = entry.1)) entries with
  | some entry => entry.2
  | none => emptyFallback) =
  entry.2
  rw [find_key_eq_some_of_mem_nodup hUnique hEntry]All goals completed! 🐙

variable {node : Type}variable [DecidableEq node]omit [DecidableEq node] in

An admitted arm key resolves to its unique entry and fragment lookup result.

private theorem fragmentLookup_of_arms_mem
    {admission : LatentSelectAdmission (Cortex.Wire.SubgraphSpec node)}
    {key : SelectArmKey}
    (hKey : key ∈ (admission.entries.map Prod.fst).toFinset) :
    ∃ entry,
      entry ∈ admission.entries ∧
        entry.fst = key ∧
          fragmentLookup admission.entries key = entry.snd := bynode:Typeadmission:LatentSelectAdmission (SubgraphSpec node)key:SelectArmKeyhKey:key ∈ (List.map Prod.fst admission.entries).toFinset⊢ ∃ entry ∈ admission.entries, entry.1 = key ∧ fragmentLookup admission.entries key = entry.2
  have hKeyMem : key ∈ admission.entries.map Prod.fst :=
    List.mem_toFinset.mp hKeynode:Typeadmission:LatentSelectAdmission (SubgraphSpec node)key:SelectArmKeyhKey:key ∈ (List.map Prod.fst admission.entries).toFinsethKeyMem:key ∈ List.map Prod.fst admission.entries⊢ ∃ entry ∈ admission.entries, entry.1 = key ∧ fragmentLookup admission.entries key = entry.2
  rcases List.mem_map.mp hKeyMem with ⟨entry, hEntry, hEqKey⟩node:Typeadmission:LatentSelectAdmission (SubgraphSpec node)key:SelectArmKeyhKey:key ∈ (List.map Prod.fst admission.entries).toFinsethKeyMem:key ∈ List.map Prod.fst admission.entriesentry:SelectArmKey × SubgraphSpec nodehEntry:entry ∈ admission.entrieshEqKey:entry.1 = key⊢ ∃ entry ∈ admission.entries, entry.1 = key ∧ fragmentLookup admission.entries key = entry.2
  have hLookup : fragmentLookup admission.entries entry.fst = entry.snd :=
    fragmentLookup_entry admission.keys_nodup hEntrynode:Typeadmission:LatentSelectAdmission (SubgraphSpec node)key:SelectArmKeyhKey:key ∈ (List.map Prod.fst admission.entries).toFinsethKeyMem:key ∈ List.map Prod.fst admission.entriesentry:SelectArmKey × SubgraphSpec nodehEntry:entry ∈ admission.entrieshEqKey:entry.1 = keyhLookup:fragmentLookup admission.entries entry.1 = entry.2⊢ ∃ entry ∈ admission.entries, entry.1 = key ∧ fragmentLookup admission.entries key = entry.2
  refine ⟨entry, hEntry, hEqKey, ?_⟩node:Typeadmission:LatentSelectAdmission (SubgraphSpec node)key:SelectArmKeyhKey:key ∈ (List.map Prod.fst admission.entries).toFinsethKeyMem:key ∈ List.map Prod.fst admission.entriesentry:SelectArmKey × SubgraphSpec nodehEntry:entry ∈ admission.entrieshEqKey:entry.1 = keyhLookup:fragmentLookup admission.entries entry.1 = entry.2⊢ fragmentLookup admission.entries key = entry.2
  rw [← hEqKey]node:Typeadmission:LatentSelectAdmission (SubgraphSpec node)key:SelectArmKeyhKey:key ∈ (List.map Prod.fst admission.entries).toFinsethKeyMem:key ∈ List.map Prod.fst admission.entriesentry:SelectArmKey × SubgraphSpec nodehEntry:entry ∈ admission.entrieshEqKey:entry.1 = keyhLookup:fragmentLookup admission.entries entry.1 = entry.2⊢ fragmentLookup admission.entries entry.1 = entry.2
  exact hLookupAll goals completed! 🐙

Convert an admission carrying SubgraphSpec arms into the proof-side LatentBranchFamily consumed by Cortex.Wire.Select.

The arm-key set is admission.entries.map Prod.fst |>.toFinset, which equals admission.shape.armKeys.toFinset by keys_eq_shape_keys. The fragment lookup falls back to the empty SubgraphSpec when the arm key is not admitted; this fallback is unreachable on admitted keys and is unobservable through the FragmentEvidence obligations, which only quote admitted entries.

def toLatentBranchFamily
    {admission : LatentSelectAdmission (Cortex.Wire.SubgraphSpec node)}
    (owner : node)
    (hEvidence : FragmentEvidence admission owner) :
    Cortex.Wire.LatentBranchFamily node SelectArmKey :=
  { owner := owner
    arms := (admission.entries.map Prod.fst).toFinset
    fragment := fragmentLookup admission.entries
    fragmentsValid := bynode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission owner⊢ ∀ branch ∈ (List.map Prod.fst admission.entries).toFinset, (fragmentLookup admission.entries branch).Valid
      intro key hKeynode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerkey:SelectArmKeyhKey:key ∈ (List.map Prod.fst admission.entries).toFinset⊢ (fragmentLookup admission.entries key).Valid
      rcases fragmentLookup_of_arms_mem hKey with ⟨entry, hEntry, _hEqKey, hLookup⟩node:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerkey:SelectArmKeyhKey:key ∈ (List.map Prod.fst admission.entries).toFinsetentry:SelectArmKey × SubgraphSpec nodehEntry:entry ∈ admission.entries_hEqKey:entry.1 = keyhLookup:fragmentLookup admission.entries key = entry.2⊢ (fragmentLookup admission.entries key).Valid
      rw [hLookup]node:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerkey:SelectArmKeyhKey:key ∈ (List.map Prod.fst admission.entries).toFinsetentry:SelectArmKey × SubgraphSpec nodehEntry:entry ∈ admission.entries_hEqKey:entry.1 = keyhLookup:fragmentLookup admission.entries key = entry.2⊢ entry.2.Valid
      exact hEvidence.fragmentsValid entry hEntryAll goals completed! 🐙
    fragmentsPairwiseDisjoint := bynode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission owner⊢ ∀ (left right : SelectArmKey),
  left ∈ (List.map Prod.fst admission.entries).toFinset →
    right ∈ (List.map Prod.fst admission.entries).toFinset →
      left ≠ right →
        ∀ nodeId ∈ (Graph.denote (fragmentLookup admission.entries left).topology).vertices,
          nodeId ∈ (Graph.denote (fragmentLookup admission.entries right).topology).vertices → False
      intro leftKey rightKeynode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerleftKey:SelectArmKeyrightKey:SelectArmKey⊢ leftKey ∈ (List.map Prod.fst admission.entries).toFinset →
  rightKey ∈ (List.map Prod.fst admission.entries).toFinset →
    leftKey ≠ rightKey →
      ∀ nodeId ∈ (Graph.denote (fragmentLookup admission.entries leftKey).topology).vertices,
        nodeId ∈ (Graph.denote (fragmentLookup admission.entries rightKey).topology).vertices → False hLeftnode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerleftKey:SelectArmKeyrightKey:SelectArmKeyhLeft:leftKey ∈ (List.map Prod.fst admission.entries).toFinset⊢ rightKey ∈ (List.map Prod.fst admission.entries).toFinset →
  leftKey ≠ rightKey →
    ∀ nodeId ∈ (Graph.denote (fragmentLookup admission.entries leftKey).topology).vertices,
      nodeId ∈ (Graph.denote (fragmentLookup admission.entries rightKey).topology).vertices → False hRightnode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerleftKey:SelectArmKeyrightKey:SelectArmKeyhLeft:leftKey ∈ (List.map Prod.fst admission.entries).toFinsethRight:rightKey ∈ (List.map Prod.fst admission.entries).toFinset⊢ leftKey ≠ rightKey →
  ∀ nodeId ∈ (Graph.denote (fragmentLookup admission.entries leftKey).topology).vertices,
    nodeId ∈ (Graph.denote (fragmentLookup admission.entries rightKey).topology).vertices → False hDifferentnode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerleftKey:SelectArmKeyrightKey:SelectArmKeyhLeft:leftKey ∈ (List.map Prod.fst admission.entries).toFinsethRight:rightKey ∈ (List.map Prod.fst admission.entries).toFinsethDifferent:leftKey ≠ rightKey⊢ ∀ nodeId ∈ (Graph.denote (fragmentLookup admission.entries leftKey).topology).vertices,
  nodeId ∈ (Graph.denote (fragmentLookup admission.entries rightKey).topology).vertices → False nodeIdnode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerleftKey:SelectArmKeyrightKey:SelectArmKeyhLeft:leftKey ∈ (List.map Prod.fst admission.entries).toFinsethRight:rightKey ∈ (List.map Prod.fst admission.entries).toFinsethDifferent:leftKey ≠ rightKeynodeId:node⊢ nodeId ∈ (Graph.denote (fragmentLookup admission.entries leftKey).topology).vertices →
  nodeId ∈ (Graph.denote (fragmentLookup admission.entries rightKey).topology).vertices → False hLeftNodenode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerleftKey:SelectArmKeyrightKey:SelectArmKeyhLeft:leftKey ∈ (List.map Prod.fst admission.entries).toFinsethRight:rightKey ∈ (List.map Prod.fst admission.entries).toFinsethDifferent:leftKey ≠ rightKeynodeId:nodehLeftNode:nodeId ∈ (Graph.denote (fragmentLookup admission.entries leftKey).topology).vertices⊢ nodeId ∈ (Graph.denote (fragmentLookup admission.entries rightKey).topology).vertices → False hRightNodenode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerleftKey:SelectArmKeyrightKey:SelectArmKeyhLeft:leftKey ∈ (List.map Prod.fst admission.entries).toFinsethRight:rightKey ∈ (List.map Prod.fst admission.entries).toFinsethDifferent:leftKey ≠ rightKeynodeId:nodehLeftNode:nodeId ∈ (Graph.denote (fragmentLookup admission.entries leftKey).topology).verticeshRightNode:nodeId ∈ (Graph.denote (fragmentLookup admission.entries rightKey).topology).vertices⊢ False
      rcases fragmentLookup_of_arms_mem hLeft with
        ⟨leftEntry, hLeftEntry, hLeftEqKey, hLeftLookup⟩node:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerleftKey:SelectArmKeyrightKey:SelectArmKeyhLeft:leftKey ∈ (List.map Prod.fst admission.entries).toFinsethRight:rightKey ∈ (List.map Prod.fst admission.entries).toFinsethDifferent:leftKey ≠ rightKeynodeId:nodehLeftNode:nodeId ∈ (Graph.denote (fragmentLookup admission.entries leftKey).topology).verticeshRightNode:nodeId ∈ (Graph.denote (fragmentLookup admission.entries rightKey).topology).verticesleftEntry:SelectArmKey × SubgraphSpec nodehLeftEntry:leftEntry ∈ admission.entrieshLeftEqKey:leftEntry.1 = leftKeyhLeftLookup:fragmentLookup admission.entries leftKey = leftEntry.2⊢ False
      rcases fragmentLookup_of_arms_mem hRight with
        ⟨rightEntry, hRightEntry, hRightEqKey, hRightLookup⟩node:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerleftKey:SelectArmKeyrightKey:SelectArmKeyhLeft:leftKey ∈ (List.map Prod.fst admission.entries).toFinsethRight:rightKey ∈ (List.map Prod.fst admission.entries).toFinsethDifferent:leftKey ≠ rightKeynodeId:nodehLeftNode:nodeId ∈ (Graph.denote (fragmentLookup admission.entries leftKey).topology).verticeshRightNode:nodeId ∈ (Graph.denote (fragmentLookup admission.entries rightKey).topology).verticesleftEntry:SelectArmKey × SubgraphSpec nodehLeftEntry:leftEntry ∈ admission.entrieshLeftEqKey:leftEntry.1 = leftKeyhLeftLookup:fragmentLookup admission.entries leftKey = leftEntry.2rightEntry:SelectArmKey × SubgraphSpec nodehRightEntry:rightEntry ∈ admission.entrieshRightEqKey:rightEntry.1 = rightKeyhRightLookup:fragmentLookup admission.entries rightKey = rightEntry.2⊢ False
      have hLeftRaw :
          nodeId ∈ (Cortex.Graph.denote leftEntry.snd.topology).vertices := bynode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission owner⊢ ∀ (left right : SelectArmKey),
  left ∈ (List.map Prod.fst admission.entries).toFinset →
    right ∈ (List.map Prod.fst admission.entries).toFinset →
      left ≠ right →
        ∀ nodeId ∈ (Graph.denote (fragmentLookup admission.entries left).topology).vertices,
          nodeId ∈ (Graph.denote (fragmentLookup admission.entries right).topology).vertices → False
        rw [hLeftLookup] at hLeftNodenode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerleftKey:SelectArmKeyrightKey:SelectArmKeyhLeft:leftKey ∈ (List.map Prod.fst admission.entries).toFinsethRight:rightKey ∈ (List.map Prod.fst admission.entries).toFinsethDifferent:leftKey ≠ rightKeynodeId:nodehRightNode:nodeId ∈ (Graph.denote (fragmentLookup admission.entries rightKey).topology).verticesleftEntry:SelectArmKey × SubgraphSpec nodehLeftNode:nodeId ∈ (Graph.denote leftEntry.2.topology).verticeshLeftEntry:leftEntry ∈ admission.entrieshLeftEqKey:leftEntry.1 = leftKeyhLeftLookup:fragmentLookup admission.entries leftKey = leftEntry.2rightEntry:SelectArmKey × SubgraphSpec nodehRightEntry:rightEntry ∈ admission.entrieshRightEqKey:rightEntry.1 = rightKeyhRightLookup:fragmentLookup admission.entries rightKey = rightEntry.2⊢ nodeId ∈ (Graph.denote leftEntry.2.topology).vertices
        exact hLeftNodeAll goals completed! 🐙
      have hRightRaw :
          nodeId ∈ (Cortex.Graph.denote rightEntry.snd.topology).vertices := bynode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission owner⊢ ∀ (left right : SelectArmKey),
  left ∈ (List.map Prod.fst admission.entries).toFinset →
    right ∈ (List.map Prod.fst admission.entries).toFinset →
      left ≠ right →
        ∀ nodeId ∈ (Graph.denote (fragmentLookup admission.entries left).topology).vertices,
          nodeId ∈ (Graph.denote (fragmentLookup admission.entries right).topology).vertices → False
        rw [hRightLookup] at hRightNodenode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerleftKey:SelectArmKeyrightKey:SelectArmKeyhLeft:leftKey ∈ (List.map Prod.fst admission.entries).toFinsethRight:rightKey ∈ (List.map Prod.fst admission.entries).toFinsethDifferent:leftKey ≠ rightKeynodeId:nodehLeftNode:nodeId ∈ (Graph.denote (fragmentLookup admission.entries leftKey).topology).verticesleftEntry:SelectArmKey × SubgraphSpec nodehLeftEntry:leftEntry ∈ admission.entrieshLeftEqKey:leftEntry.1 = leftKeyhLeftLookup:fragmentLookup admission.entries leftKey = leftEntry.2rightEntry:SelectArmKey × SubgraphSpec nodehRightNode:nodeId ∈ (Graph.denote rightEntry.2.topology).verticeshRightEntry:rightEntry ∈ admission.entrieshRightEqKey:rightEntry.1 = rightKeyhRightLookup:fragmentLookup admission.entries rightKey = rightEntry.2hLeftRaw:nodeId ∈ (Graph.denote leftEntry.2.topology).vertices⊢ nodeId ∈ (Graph.denote rightEntry.2.topology).vertices
        exact hRightNodeAll goals completed! 🐙
      have hKeysDifferent : leftEntry.fst ≠ rightEntry.fst := bynode:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission owner⊢ ∀ (left right : SelectArmKey),
  left ∈ (List.map Prod.fst admission.entries).toFinset →
    right ∈ (List.map Prod.fst admission.entries).toFinset →
      left ≠ right →
        ∀ nodeId ∈ (Graph.denote (fragmentLookup admission.entries left).topology).vertices,
          nodeId ∈ (Graph.denote (fragmentLookup admission.entries right).topology).vertices → False
        rw [hLeftEqKey, hRightEqKey]node:Typeinst✝:DecidableEq nodeadmission:LatentSelectAdmission (SubgraphSpec node)owner:nodehEvidence:FragmentEvidence admission ownerleftKey:SelectArmKeyrightKey:SelectArmKeyhLeft:leftKey ∈ (List.map Prod.fst admission.entries).toFinsethRight:rightKey ∈ (List.map Prod.fst admission.entries).toFinsethDifferent:leftKey ≠ rightKeynodeId:nodehLeftNode:nodeId ∈ (Graph.denote (fragmentLookup admission.entries leftKey).topology).verticeshRightNode:nodeId ∈ (Graph.denote (fragmentLookup admission.entries rightKey).topology).verticesleftEntry:SelectArmKey × SubgraphSpec nodehLeftEntry:leftEntry ∈ admission.entrieshLeftEqKey:leftEntry.1 = leftKeyhLeftLookup:fragmentLookup admission.entries leftKey = leftEntry.2rightEntry:SelectArmKey × SubgraphSpec nodehRightEntry:rightEntry ∈ admission.entrieshRightEqKey:rightEntry.1 = rightKeyhRightLookup:fragmentLookup admission.entries rightKey = rightEntry.2hLeftRaw:nodeId ∈ (Graph.denote leftEntry.2.topology).verticeshRightRaw:nodeId ∈ (Graph.denote rightEntry.2.topology).vertices⊢ leftKey ≠ rightKey
        exact hDifferentAll goals completed! 🐙
      exact
        hEvidence.fragmentsPairwiseDisjoint
          leftEntry
          rightEntry
          hLeftEntry
          hRightEntry
          hKeysDifferent
          nodeId
          hLeftRaw
          hRightRawAll goals completed! 🐙 }

Fragment evidence pins the retained owner outside every admitted fragment body.

theorem owner_not_in_admitted_fragment
    {admission : LatentSelectAdmission (Cortex.Wire.SubgraphSpec node)}
    {owner : node}
    (hEvidence : FragmentEvidence admission owner)
    {entry : SelectArmKey × Cortex.Wire.SubgraphSpec node}
    (hEntry : entry ∈ admission.entries) :
    owner ∉ (Cortex.Graph.denote entry.snd.topology).vertices :=
  hEvidence.ownerNotInFragments entry hEntry

end LatentSelectAdmission

Admission Sanity Examples

section AdmissionSanity

A two-key SelectableOutputShape with two declared ports.

private def twoArmShape
    (leftKey rightKey : SelectArmKey)
    (leftPort rightPort : PortSignature)
    (hLeftKey : leftKey.Valid)
    (hRightKey : rightKey.Valid)
    (hLeftPort : leftPort.Valid)
    (hRightPort : rightPort.Valid)
    (hKeyDistinct : leftKey ≠ rightKey)
    (hLabelDistinct : leftPort.label ≠ rightPort.label) :
    SelectableOutputShape :=
  { armPorts := [(leftKey, leftPort), (rightKey, rightPort)]
    armsAtLeastTwo := byleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.label⊢ 2 ≤ [(leftKey, leftPort), (rightKey, rightPort)].length
      simpAll goals completed! 🐙
    armKeysUnique := byleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.label⊢ (List.map Prod.fst [(leftKey, leftPort), (rightKey, rightPort)]).Nodup
      simp [hKeyDistinct]All goals completed! 🐙
    portLabelsUnique := byleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.label⊢ (List.map (fun entry => entry.2.label) [(leftKey, leftPort), (rightKey, rightPort)]).Nodup
      simp [hLabelDistinct]All goals completed! 🐙
    armKeysValid := byleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.label⊢ ∀ entry ∈ [(leftKey, leftPort), (rightKey, rightPort)], entry.1.Valid
      intro entry hEntryleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry ∈ [(leftKey, leftPort), (rightKey, rightPort)]⊢ entry.1.Valid
      simp only [List.mem_cons, List.not_mem_nil, or_false] at hEntryleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (leftKey, leftPort) ∨ entry = (rightKey, rightPort)⊢ entry.1.Valid
      rcases hEntry with hEntry | hEntryinlleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (leftKey, leftPort)⊢ entry.1.ValidinrleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (rightKey, rightPort)⊢ entry.1.Valid
      ·inlleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (leftKey, leftPort)⊢ entry.1.Valid rw [hEntry]inlleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (leftKey, leftPort)⊢ (leftKey, leftPort).1.Valid
        exact hLeftKeyAll goals completed! 🐙
      ·inrleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (rightKey, rightPort)⊢ entry.1.Valid rw [hEntry]inrleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (rightKey, rightPort)⊢ (rightKey, rightPort).1.Valid
        exact hRightKeyAll goals completed! 🐙
    armPortsValid := byleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.label⊢ ∀ entry ∈ [(leftKey, leftPort), (rightKey, rightPort)], entry.2.Valid
      intro entry hEntryleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry ∈ [(leftKey, leftPort), (rightKey, rightPort)]⊢ entry.2.Valid
      simp only [List.mem_cons, List.not_mem_nil, or_false] at hEntryleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (leftKey, leftPort) ∨ entry = (rightKey, rightPort)⊢ entry.2.Valid
      rcases hEntry with hEntry | hEntryinlleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (leftKey, leftPort)⊢ entry.2.ValidinrleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (rightKey, rightPort)⊢ entry.2.Valid
      ·inlleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (leftKey, leftPort)⊢ entry.2.Valid rw [hEntry]inlleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (leftKey, leftPort)⊢ (leftKey, leftPort).2.Valid
        exact hLeftPortAll goals completed! 🐙
      ·inrleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (rightKey, rightPort)⊢ entry.2.Valid rw [hEntry]inrleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelentry:SelectArmKey × PortSignaturehEntry:entry = (rightKey, rightPort)⊢ (rightKey, rightPort).2.Valid
        exact hRightPortAll goals completed! 🐙 }

private def resolutionValidKey : SelectArmKey := ⟨"valid"⟩private def resolutionIssueKey : SelectArmKey := ⟨"issue"⟩private def resolutionResearchKey : SelectArmKey := ⟨"ResearchPlan"⟩private def resolutionUnknownKey : SelectArmKey := ⟨"Unknown"⟩private def resolutionResearchContract : ContractId := ⟨"ResearchPlan"⟩private def resolutionIssueContract : ContractId := ⟨"PlanIssue"⟩private def resolutionSharedContract : ContractId := ⟨"Shared"⟩

private def resolutionValidPort : PortSignature :=
  { label := ⟨"valid"⟩
    contract := resolutionResearchContract }

private def resolutionIssuePort : PortSignature :=
  { label := ⟨"issue"⟩
    contract := resolutionIssueContract }

private def resolutionShape : SelectableOutputShape :=
  twoArmShape
    resolutionValidKey
    resolutionIssueKey
    resolutionValidPort
    resolutionIssuePort
    (by⊢ resolutionValidKey.Valid decideAll goals completed! 🐙)
    (by⊢ resolutionIssueKey.Valid decideAll goals completed! 🐙)
    (by⊢ resolutionValidPort.Valid decideAll goals completed! 🐙)
    (by⊢ resolutionIssuePort.Valid decideAll goals completed! 🐙)
    (by⊢ resolutionValidKey ≠ resolutionIssueKey decideAll goals completed! 🐙)
    (by⊢ resolutionValidPort.label ≠ resolutionIssuePort.label decideAll goals completed! 🐙)

private def ambiguousLeftPort : PortSignature :=
  { label := ⟨"left"⟩
    contract := resolutionSharedContract }

private def ambiguousRightPort : PortSignature :=
  { label := ⟨"right"⟩
    contract := resolutionSharedContract }

private def ambiguousContractShape : SelectableOutputShape :=
  twoArmShape
    ⟨"left"⟩
    ⟨"right"⟩
    ambiguousLeftPort
    ambiguousRightPort
    (by⊢ { name := "left" }.Valid decideAll goals completed! 🐙)
    (by⊢ { name := "right" }.Valid decideAll goals completed! 🐙)
    (by⊢ ambiguousLeftPort.Valid decideAll goals completed! 🐙)
    (by⊢ ambiguousRightPort.Valid decideAll goals completed! 🐙)
    (by⊢ { name := "left" } ≠ { name := "right" } decideAll goals completed! 🐙)
    (by⊢ ambiguousLeftPort.label ≠ ambiguousRightPort.label decideAll goals completed! 🐙)

Exact label keys resolve to themselves.

example :
    resolveArmKey resolutionShape resolutionValidKey =
      Except.ok resolutionValidKey := by⊢ resolveArmKey resolutionShape resolutionValidKey = Except.ok resolutionValidKey
  rflAll goals completed! 🐙

Unique contract-name fallback resolves to the canonical label key.

example :
    resolveArmKey resolutionShape resolutionResearchKey =
      Except.ok resolutionValidKey := by⊢ resolveArmKey resolutionShape resolutionResearchKey = Except.ok resolutionValidKey
  rflAll goals completed! 🐙

Unknown source keys produce the unresolved-key diagnostic.

example :
    resolveArmKey resolutionShape resolutionUnknownKey =
      Except.error (SelectAdmissionError.unknownSourceKey resolutionUnknownKey) := by⊢ resolveArmKey resolutionShape resolutionUnknownKey =
  Except.error (SelectAdmissionError.unknownSourceKey resolutionUnknownKey)
  rflAll goals completed! 🐙

Non-unique contract-name fallback produces the ambiguity diagnostic.

example :
    resolveArmKey ambiguousContractShape ⟨"Shared"⟩ =
      Except.error
        (SelectAdmissionError.ambiguousContractFallback
          resolutionSharedContract
          [⟨"left"⟩, ⟨"right"⟩]) := by⊢ resolveArmKey ambiguousContractShape { name := "Shared" } =
  Except.error
    (SelectAdmissionError.ambiguousContractFallback resolutionSharedContract [{ name := "left" }, { name := "right" }])
  rflAll goals completed! 🐙

private def duplicateCanonicalClause : SelectExpr Unit Unit :=
  { base := ()
    arms :=
      [ { key := resolutionValidKey, body := () }
      , { key := resolutionResearchKey, body := () } ] }

Label and contract fallback targeting the same variant is a duplicate after resolution.

example :
    admitClause resolutionShape duplicateCanonicalClause =
      Except.error (SelectAdmissionError.duplicateSelectArmKey resolutionValidKey) := by⊢ admitClause resolutionShape duplicateCanonicalClause =
  Except.error (SelectAdmissionError.duplicateSelectArmKey resolutionValidKey)
  rflAll goals completed! 🐙

private def missingCoverageClause : SelectExpr Unit Unit :=
  { base := ()
    arms := [{ key := resolutionValidKey, body := () }] }

Missing source coverage reports the uncovered shape arm.

example :
    admitClause resolutionShape missingCoverageClause =
      Except.error (SelectAdmissionError.uncoveredShapeArm resolutionIssueKey) := by⊢ admitClause resolutionShape missingCoverageClause =
  Except.error (SelectAdmissionError.uncoveredShapeArm resolutionIssueKey)
  rflAll goals completed! 🐙

variable {node : Type}variable [DecidableEq node]

Two-arm admissions bridge into a LatentBranchFamily with the same two arm keys.

This is the smallest executable-shaped sanity check for the bridge machinery: one-arm output variants are represented by OutputShape.single, not by SelectableOutputShape.

private theorem two_arm_admission_bridge_arm_set
    (leftKey rightKey : SelectArmKey)
    (leftPort rightPort : PortSignature)
    (hLeftKey : leftKey.Valid)
    (hRightKey : rightKey.Valid)
    (hLeftPort : leftPort.Valid)
    (hRightPort : rightPort.Valid)
    (hKeyDistinct : leftKey ≠ rightKey)
    (hLabelDistinct : leftPort.label ≠ rightPort.label)
    (leftBody rightBody : Cortex.Wire.SubgraphSpec node)
    (owner : node)
    (admission : LatentSelectAdmission (Cortex.Wire.SubgraphSpec node))
    (_hShape :
      admission.shape =
        twoArmShape
          leftKey
          rightKey
          leftPort
          rightPort
          hLeftKey
          hRightKey
          hLeftPort
          hRightPort
          hKeyDistinct
          hLabelDistinct)
    (hEntries : admission.entries = [(leftKey, leftBody), (rightKey, rightBody)])
    (hEvidence : FragmentEvidence admission owner) :
    (LatentSelectAdmission.toLatentBranchFamily owner hEvidence).arms =
      ({leftKey, rightKey} : Finset SelectArmKey) := bynode:Typeinst✝:DecidableEq nodeleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelleftBody:SubgraphSpec noderightBody:SubgraphSpec nodeowner:nodeadmission:LatentSelectAdmission (SubgraphSpec node)_hShape:admission.shape =
  twoArmShape leftKey rightKey leftPort rightPort hLeftKey hRightKey hLeftPort hRightPort hKeyDistinct hLabelDistincthEntries:admission.entries = [(leftKey, leftBody), (rightKey, rightBody)]hEvidence:FragmentEvidence admission owner⊢ (LatentSelectAdmission.toLatentBranchFamily owner hEvidence).arms = {leftKey, rightKey}
  show ((admission.entries.map Prod.fst).toFinset : Finset SelectArmKey) =
      ({leftKey, rightKey} : Finset SelectArmKey)node:Typeinst✝:DecidableEq nodeleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelleftBody:SubgraphSpec noderightBody:SubgraphSpec nodeowner:nodeadmission:LatentSelectAdmission (SubgraphSpec node)_hShape:admission.shape =
  twoArmShape leftKey rightKey leftPort rightPort hLeftKey hRightKey hLeftPort hRightPort hKeyDistinct hLabelDistincthEntries:admission.entries = [(leftKey, leftBody), (rightKey, rightBody)]hEvidence:FragmentEvidence admission owner⊢ (List.map Prod.fst admission.entries).toFinset = {leftKey, rightKey}
  rw [hEntries]node:Typeinst✝:DecidableEq nodeleftKey:SelectArmKeyrightKey:SelectArmKeyleftPort:PortSignaturerightPort:PortSignaturehLeftKey:leftKey.ValidhRightKey:rightKey.ValidhLeftPort:leftPort.ValidhRightPort:rightPort.ValidhKeyDistinct:leftKey ≠ rightKeyhLabelDistinct:leftPort.label ≠ rightPort.labelleftBody:SubgraphSpec noderightBody:SubgraphSpec nodeowner:nodeadmission:LatentSelectAdmission (SubgraphSpec node)_hShape:admission.shape =
  twoArmShape leftKey rightKey leftPort rightPort hLeftKey hRightKey hLeftPort hRightPort hKeyDistinct hLabelDistincthEntries:admission.entries = [(leftKey, leftBody), (rightKey, rightBody)]hEvidence:FragmentEvidence admission owner⊢ (List.map Prod.fst [(leftKey, leftBody), (rightKey, rightBody)]).toFinset = {leftKey, rightKey}
  simpAll goals completed! 🐙

end AdmissionSanityend SelectAdmissionend Cortex.Wire

Overview

Context

Theorem Split

Selectable Output Shape

Source Select Clause

Diagnostics

Latent Admission Carrier

Source Admission

Bridge Into LatentBranchFamily

Admission Sanity Examples

Bridge Into `LatentBranchFamily`