Theory /Cortex /Wire /AdmissionArtifact /SelectReconstruction

Cortex.Wire.AdmissionArtifact.SelectReconstruction

proofs

On this page

Overview
Select Reconstruction Contract
Reconstruction Theorems

Imports

import Cortex.Wire.AdmissionArtifact.PrimitiveReconstruction

Overview

Select-admission reconstruction from validator-sound admission artifacts.

The select artifact rows already project to the generic SelectAdmission.LatentSelectAdmission carrier. This module names the artifact-boundary reconstruction theorem that downstream correspondence proofs should consume:

every select row carries the projected latent admission and key coverage;
latent entries come from decoded source arm rows;
label-first and unique-contract-fallback resolution facts are preserved;
latent body nodes are fresh from the top-level summary and pairwise disjoint;
arm body boundary rows match the condition bridge; and
selected-variant bridge entries are consumed by primitive replay.

The reconstruction record exposes one shared (conditionEntries, conditionExits) primitive node row at the top level so that all per-arm and per-variant bridge facts witness the same primitive backing for the condition node.

This is still source-side admission. Replaying a chosen latent body into durable selected-branch recovery remains a separate proof surface.

              namespace Cortex.Wirenamespace AdmissionArtifactopen Cortex.Wire.ElaborationIRnamespace WireAdmissionArtifact

Select Reconstruction Contract

Resolution evidence for one persisted source select arm.

inductive SelectArmResolutionReconstruction
    (selectAdmission : SelectAdmissionArtifact)
    (arm : SelectArmAdmissionArtifact) : Prop where
  | byLabel
      (mode_eq : arm.mode = SelectResolutionMode.resolvedByLabel)
      (sourceKey_eq : arm.sourceKey = arm.canonicalKey)
      (variant :
        ∃ variant, variant ∈ selectAdmission.variants ∧
          variant.key = arm.canonicalKey ∧
          variant.port.label = AdmissionPortLabel.label arm.sourceKey) :
        SelectArmResolutionReconstruction selectAdmission arm
  | byContract
      (mode_eq : arm.mode = SelectResolutionMode.resolvedByContract)
      (noLabelShadow :
        ∀ variant, variant ∈ selectAdmission.variants →
          variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey)
      (contractFallbackUnique :
        ∀ variant, variant ∈ selectAdmission.variants →
          (variant.port.contract.name = arm.sourceKey.name ↔
            variant.key = arm.canonicalKey)) :
        SelectArmResolutionReconstruction selectAdmission arm

Body-shape evidence for one source select arm against its chosen variant and the shared condition-bridge exits.

inductive SelectArmBodyShapeReconstruction
    (selectAdmission : SelectAdmissionArtifact)
    (arm : SelectArmAdmissionArtifact)
    (conditionExits : List AdmissionBoundaryPort)
    (variant : SelectVariantArtifact) : Prop where
  | emptyBody
      (bodyNodesEmpty : arm.bodyNodes = [])
      (bodyEntriesEmpty : arm.bodyEntries = [])
      (bodyExitsEmpty : arm.bodyExits = [])
      (conditionOutputShapesIdentity :
        SelectConditionBridgeOutputShapes selectAdmission conditionExits =
          [variant.port.identityOutputShape]) :
        SelectArmBodyShapeReconstruction
          selectAdmission arm conditionExits variant
  | nonEmptyBody
      (bodyEntriesMatch :
        arm.bodyEntries.map AdmissionBoundaryPort.compatibilityShape =
          [variant.port.compatibilityShape])
      (bodyExitsPerm :
        (arm.bodyExits.map AdmissionBoundaryPort.outputShape).Perm
          (SelectConditionBridgeOutputShapes selectAdmission conditionExits)) :
        SelectArmBodyShapeReconstruction
          selectAdmission arm conditionExits variant

Condition-bridge variant evidence for one source select arm, indexed by the shared condition-node exits and the resolved variant.

structure SelectArmBridgeReconstruction
    (selectAdmission : SelectAdmissionArtifact)
    (arm : SelectArmAdmissionArtifact)
    (conditionExits : List AdmissionBoundaryPort)
    (variant : SelectVariantArtifact) : Prop where
  variantMem : variant ∈ selectAdmission.variants
  variantKey : variant.key = arm.canonicalKey
  bodyShape :
    SelectArmBodyShapeReconstruction selectAdmission arm conditionExits variant

Primitive replay evidence for one selected variant's bridge entry, indexed by the shared condition-node entries and the chosen entry.

structure SelectVariantBridgeReconstruction
    (artifact : WireAdmissionArtifact)
    (variant : SelectVariantArtifact)
    (conditionEntries : List AdmissionBoundaryPort)
    (entry : AdmissionBoundaryPort) : Prop where
  entryMem : entry ∈ conditionEntries
  compatible : variant.port.CompatibleWith entry
  replayed :
    { fromPort := variant.port, toPort := entry } ∈
      PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps
  entryConsumed :
    entry.key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps

Reconstruction evidence for one projected latent select entry.

structure SelectLatentEntryReconstruction
    (artifact : WireAdmissionArtifact)
    (selectAdmission : SelectAdmissionArtifact)
    (hValid : selectAdmission.Valid)
    (entry : SelectArmKey × SelectArmAdmissionArtifact) : Prop where
  sourceArm :
    ∃ arm, arm ∈ selectAdmission.arms ∧
      entry = (arm.canonicalSelectArmKey, arm)
  bodyValid : entry.snd.Valid
  bodyNodeFresh :
    ∀ {node : NodeId}, node ∈ entry.snd.bodyNodes → node ∉ artifact.nodes
  bodyNodesDisjoint :
    ∀ {other : SelectArmKey × SelectArmAdmissionArtifact},
      other ∈ (selectAdmission.toLatentSelectAdmission hValid).entries →
        entry.fst ≠ other.fst →
          ∀ {node : NodeId},
            node ∈ entry.snd.bodyNodes → node ∉ other.snd.bodyNodes

Artifact-boundary reconstruction evidence for one select-admission row, indexed by a shared condition-node primitive row.

Sharing conditionEntries / conditionExits at this layer rules out the formal countermodel where armBridge and variantBridge could pick different primitive node rows for the same selectAdmission.conditionNode.

structure SelectAdmissionReconstructionRecord
    (artifact : WireAdmissionArtifact)
    (selectAdmission : SelectAdmissionArtifact)
    (conditionEntries conditionExits : List AdmissionBoundaryPort) : Prop where
  valid : selectAdmission.Valid
  ownerMatchesCondition : selectAdmission.owner = selectAdmission.conditionNode
  armsAtLeastTwo : 2 ≤ selectAdmission.arms.length
  latentKeyCoverage :
    ((selectAdmission.toLatentSelectAdmission valid).entries.map Prod.fst).Perm
      (selectAdmission.toLatentSelectAdmission valid).shape.armKeys
  primitiveConditionNode :
    PrimitiveGraphStep.node selectAdmission.conditionNode
        conditionEntries conditionExits ∈
      artifact.primitiveSteps
  conditionInputKeysAccounted :
    ∀ {key : NodeId × FieldLabel × ContractId},
      key ∈ conditionEntries.map AdmissionBoundaryPort.key →
        PrimitiveInputKeyAccounted artifact key
  conditionOutputKeysAccounted :
    ∀ {key : NodeId × FieldLabel × ContractId},
      key ∈ conditionExits.map AdmissionBoundaryPort.key →
        PrimitiveOutputKeyAccounted artifact key
  latentEntries :
    ∀ {entry : SelectArmKey × SelectArmAdmissionArtifact},
      entry ∈ (selectAdmission.toLatentSelectAdmission valid).entries →
        SelectLatentEntryReconstruction artifact selectAdmission valid entry
  armResolution :
    ∀ {arm : SelectArmAdmissionArtifact},
      arm ∈ selectAdmission.arms →
        SelectArmResolutionReconstruction selectAdmission arm
  armBridge :
    ∀ {arm : SelectArmAdmissionArtifact},
      arm ∈ selectAdmission.arms →
        ∃ variant,
          SelectArmBridgeReconstruction
            selectAdmission arm conditionExits variant
  variantBridge :
    ∀ {variant : SelectVariantArtifact},
      variant ∈ selectAdmission.variants →
        ∃ entry,
          SelectVariantBridgeReconstruction
            artifact variant conditionEntries entry

Artifact-boundary reconstruction evidence for one select-admission row.

def SelectAdmissionReconstruction
    (artifact : WireAdmissionArtifact)
    (selectAdmission : SelectAdmissionArtifact) : Prop :=
  ∃ conditionEntries conditionExits,
    SelectAdmissionReconstructionRecord
      artifact selectAdmission conditionEntries conditionExits

Artifact-boundary select reconstruction for every select row.

def SelectReconstruction (artifact : WireAdmissionArtifact) : Prop :=
  ∀ selectAdmission, selectAdmission ∈ artifact.selects →
    SelectAdmissionReconstruction artifact selectAdmission

Reconstruction Theorems

Select soundness reconstructs source-arm resolution evidence for one arm.

theorem Sound.selectArmResolutionReconstruction
    {artifact : WireAdmissionArtifact}
    (hSound : artifact.Sound)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    {arm : SelectArmAdmissionArtifact}
    (hArm : arm ∈ selectAdmission.arms) :
    SelectArmResolutionReconstruction selectAdmission arm := byartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.arms⊢ SelectArmResolutionReconstruction selectAdmission arm
  have hValid := hSound.select.selectsValid selectAdmission hSelectartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshValid:selectAdmission.Valid⊢ SelectArmResolutionReconstruction selectAdmission arm
  have hResolution := hValid.armResolutionSound arm hArmartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshValid:selectAdmission.ValidhResolution:match arm.mode with
| SelectResolutionMode.resolvedByLabel =>
  arm.sourceKey = arm.canonicalKey ∧
    ∃ variant ∈ selectAdmission.variants,
      variant.key = arm.canonicalKey ∧ variant.port.label = AdmissionPortLabel.label arm.sourceKey
| SelectResolutionMode.resolvedByContract =>
  (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
    ∀ variant ∈ selectAdmission.variants,
      variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKey⊢ SelectArmResolutionReconstruction selectAdmission arm
  cases hMode : arm.mode with
  | resolvedByLabel =>resolvedByLabelartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshValid:selectAdmission.ValidhResolution:match arm.mode with
| SelectResolutionMode.resolvedByLabel =>
  arm.sourceKey = arm.canonicalKey ∧
    ∃ variant ∈ selectAdmission.variants,
      variant.key = arm.canonicalKey ∧ variant.port.label = AdmissionPortLabel.label arm.sourceKey
| SelectResolutionMode.resolvedByContract =>
  (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
    ∀ variant ∈ selectAdmission.variants,
      variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKeyhMode:arm.mode = SelectResolutionMode.resolvedByLabel⊢ SelectArmResolutionReconstruction selectAdmission arm
      rw [hMode] at hResolutionresolvedByLabelartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshValid:selectAdmission.ValidhResolution:match SelectResolutionMode.resolvedByLabel with
| SelectResolutionMode.resolvedByLabel =>
  arm.sourceKey = arm.canonicalKey ∧
    ∃ variant ∈ selectAdmission.variants,
      variant.key = arm.canonicalKey ∧ variant.port.label = AdmissionPortLabel.label arm.sourceKey
| SelectResolutionMode.resolvedByContract =>
  (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
    ∀ variant ∈ selectAdmission.variants,
      variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKeyhMode:arm.mode = SelectResolutionMode.resolvedByLabel⊢ SelectArmResolutionReconstruction selectAdmission arm
      exact
        SelectArmResolutionReconstruction.byLabel
          hMode hResolution.left hResolution.rightAll goals completed! 🐙
  | resolvedByContract =>resolvedByContractartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshValid:selectAdmission.ValidhResolution:match arm.mode with
| SelectResolutionMode.resolvedByLabel =>
  arm.sourceKey = arm.canonicalKey ∧
    ∃ variant ∈ selectAdmission.variants,
      variant.key = arm.canonicalKey ∧ variant.port.label = AdmissionPortLabel.label arm.sourceKey
| SelectResolutionMode.resolvedByContract =>
  (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
    ∀ variant ∈ selectAdmission.variants,
      variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKeyhMode:arm.mode = SelectResolutionMode.resolvedByContract⊢ SelectArmResolutionReconstruction selectAdmission arm
      rw [hMode] at hResolutionresolvedByContractartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshValid:selectAdmission.ValidhResolution:match SelectResolutionMode.resolvedByContract with
| SelectResolutionMode.resolvedByLabel =>
  arm.sourceKey = arm.canonicalKey ∧
    ∃ variant ∈ selectAdmission.variants,
      variant.key = arm.canonicalKey ∧ variant.port.label = AdmissionPortLabel.label arm.sourceKey
| SelectResolutionMode.resolvedByContract =>
  (∀ variant ∈ selectAdmission.variants, variant.port.label ≠ AdmissionPortLabel.label arm.sourceKey) ∧
    ∀ variant ∈ selectAdmission.variants,
      variant.port.contract.name = arm.sourceKey.name ↔ variant.key = arm.canonicalKeyhMode:arm.mode = SelectResolutionMode.resolvedByContract⊢ SelectArmResolutionReconstruction selectAdmission arm
      exact
        SelectArmResolutionReconstruction.byContract
          hMode hResolution.left hResolution.rightAll goals completed! 🐙

Select soundness reconstructs provenance and freshness for one latent entry.

theorem Sound.selectLatentEntryReconstruction
    {artifact : WireAdmissionArtifact}
    (hSound : artifact.Sound)
    {selectAdmission : SelectAdmissionArtifact}
    (hSelect : selectAdmission ∈ artifact.selects)
    (hValid : selectAdmission.Valid)
    {entry : SelectArmKey × SelectArmAdmissionArtifact}
    (hEntry :
      entry ∈ (selectAdmission.toLatentSelectAdmission hValid).entries) :
    SelectLatentEntryReconstruction artifact selectAdmission hValid entry := byartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshValid:selectAdmission.Validentry:SelectArmKey × SelectArmAdmissionArtifacthEntry:entry ∈ (selectAdmission.toLatentSelectAdmission hValid).entries⊢ artifact.SelectLatentEntryReconstruction selectAdmission hValid entry
  exact
    { sourceArm :=
        hSound.select.latentEntrySourceArm hSelect hValid hEntry
      bodyValid :=
        SelectAdmissionArtifact.toLatentSelectAdmission_entry_body_valid
          hEntry
      bodyNodeFresh := byartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshValid:selectAdmission.Validentry:SelectArmKey × SelectArmAdmissionArtifacthEntry:entry ∈ (selectAdmission.toLatentSelectAdmission hValid).entries⊢ ∀ {node : NodeId}, node ∈ entry.2.bodyNodes → node ∉ artifact.nodes
        intro node hNodeartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshValid:selectAdmission.Validentry:SelectArmKey × SelectArmAdmissionArtifacthEntry:entry ∈ (selectAdmission.toLatentSelectAdmission hValid).entriesnode:NodeIdhNode:node ∈ entry.2.bodyNodes⊢ node ∉ artifact.nodes
        exact
          hSound.select.latentEntryBodyNodeFresh
            hSelect hValid hEntry hNodeAll goals completed! 🐙
      bodyNodesDisjoint := byartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshValid:selectAdmission.Validentry:SelectArmKey × SelectArmAdmissionArtifacthEntry:entry ∈ (selectAdmission.toLatentSelectAdmission hValid).entries⊢ ∀ {other : SelectArmKey × SelectArmAdmissionArtifact},
  other ∈ (selectAdmission.toLatentSelectAdmission hValid).entries →
    entry.1 ≠ other.1 → ∀ {node : NodeId}, node ∈ entry.2.bodyNodes → node ∉ other.2.bodyNodes
        intro other hOtherartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshValid:selectAdmission.Validentry:SelectArmKey × SelectArmAdmissionArtifacthEntry:entry ∈ (selectAdmission.toLatentSelectAdmission hValid).entriesother:SelectArmKey × SelectArmAdmissionArtifacthOther:other ∈ (selectAdmission.toLatentSelectAdmission hValid).entries⊢ entry.1 ≠ other.1 → ∀ {node : NodeId}, node ∈ entry.2.bodyNodes → node ∉ other.2.bodyNodes hKeysartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshValid:selectAdmission.Validentry:SelectArmKey × SelectArmAdmissionArtifacthEntry:entry ∈ (selectAdmission.toLatentSelectAdmission hValid).entriesother:SelectArmKey × SelectArmAdmissionArtifacthOther:other ∈ (selectAdmission.toLatentSelectAdmission hValid).entrieshKeys:entry.1 ≠ other.1⊢ ∀ {node : NodeId}, node ∈ entry.2.bodyNodes → node ∉ other.2.bodyNodes nodeartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshValid:selectAdmission.Validentry:SelectArmKey × SelectArmAdmissionArtifacthEntry:entry ∈ (selectAdmission.toLatentSelectAdmission hValid).entriesother:SelectArmKey × SelectArmAdmissionArtifacthOther:other ∈ (selectAdmission.toLatentSelectAdmission hValid).entrieshKeys:entry.1 ≠ other.1node:NodeId⊢ node ∈ entry.2.bodyNodes → node ∉ other.2.bodyNodes hNodeartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshValid:selectAdmission.Validentry:SelectArmKey × SelectArmAdmissionArtifacthEntry:entry ∈ (selectAdmission.toLatentSelectAdmission hValid).entriesother:SelectArmKey × SelectArmAdmissionArtifacthOther:other ∈ (selectAdmission.toLatentSelectAdmission hValid).entrieshKeys:entry.1 ≠ other.1node:NodeIdhNode:node ∈ entry.2.bodyNodes⊢ node ∉ other.2.bodyNodes
        exact
          hSound.select.latentEntriesBodyNodesDisjoint
            hSelect hValid hEntry hOther hKeys hNodeAll goals completed! 🐙 }

Validator soundness reconstructs select-admission artifact-boundary witnesses indexed by a single shared condition-node primitive row.

Primitive node-row uniqueness (Sound.primitiveNode_frontiers_unique) collapses the per-variant existential in variantBridgeEntryConsumed onto the same (conditionEntries, conditionExits) chosen by selectArmBodyBoundariesMatchCondition.

theorem Sound.toSelectReconstruction
    {artifact : WireAdmissionArtifact}
    (hSound : artifact.Sound) :
    artifact.SelectReconstruction := byartifact:WireAdmissionArtifacthSound:artifact.Sound⊢ artifact.SelectReconstruction
  intro selectAdmission hSelectartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selects⊢ artifact.SelectAdmissionReconstruction selectAdmission
  obtain ⟨conditionEntries, conditionExits, hPrimitiveNode, hArms⟩ :=
    hSound.select.selectArmBodyBoundariesMatchCondition
      selectAdmission hSelectartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))⊢ artifact.SelectAdmissionReconstruction selectAdmission
  have hValid := hSound.select.selectsValid selectAdmission hSelectartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.Valid⊢ artifact.SelectAdmissionReconstruction selectAdmission
  have hAccounted :
      artifact.PrimitiveFrontierKeysAccounted :=
    primitiveFrontierKeysAccounted
      hSound.primitive.summaryFrontiersMatchPrimitiveartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ artifact.SelectAdmissionReconstruction selectAdmission
  refine ⟨conditionEntries, conditionExits, ?_⟩artifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ artifact.SelectAdmissionReconstructionRecord selectAdmission conditionEntries conditionExits
  refine
    { valid := hValid
      ownerMatchesCondition := hValid.ownerMatchesCondition
      armsAtLeastTwo := hSound.select.armsAtLeastTwo hSelect
      latentKeyCoverage :=
        (selectAdmission.toLatentSelectAdmission hValid).entries_keys_perm
      primitiveConditionNode := hPrimitiveNode
      conditionInputKeysAccounted := ?inputs
      conditionOutputKeysAccounted := ?outputs
      latentEntries := ?latent
      armResolution := ?resolution
      armBridge := ?bridge
      variantBridge := ?variantBridge }inputsartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {key : NodeId × FieldLabel × ContractId},
  key ∈ List.map AdmissionBoundaryPort.key conditionEntries → artifact.PrimitiveInputKeyAccounted keyoutputsartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {key : NodeId × FieldLabel × ContractId},
  key ∈ List.map AdmissionBoundaryPort.key conditionExits → artifact.PrimitiveOutputKeyAccounted keylatentartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {entry : SelectArmKey × SelectArmAdmissionArtifact},
  entry ∈ (selectAdmission.toLatentSelectAdmission hValid).entries →
    artifact.SelectLatentEntryReconstruction selectAdmission hValid entryresolutionartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {arm : SelectArmAdmissionArtifact}, arm ∈ selectAdmission.arms → SelectArmResolutionReconstruction selectAdmission armbridgeartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {arm : SelectArmAdmissionArtifact},
  arm ∈ selectAdmission.arms → ∃ variant, SelectArmBridgeReconstruction selectAdmission arm conditionExits variantvariantBridgeartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {variant : SelectVariantArtifact},
  variant ∈ selectAdmission.variants →
    ∃ entry, artifact.SelectVariantBridgeReconstruction variant conditionEntries entry
  case inputs =>artifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {key : NodeId × FieldLabel × ContractId},
  key ∈ List.map AdmissionBoundaryPort.key conditionEntries → artifact.PrimitiveInputKeyAccounted key
    intro key hKeyartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedkey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key conditionEntries⊢ artifact.PrimitiveInputKeyAccounted key
    exact
      hAccounted.inputs
        (PrimitiveGraphStep.nodeEntryKeysList_mem_of_node_mem
          hPrimitiveNode hKey)All goals completed! 🐙
  case outputs =>artifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {key : NodeId × FieldLabel × ContractId},
  key ∈ List.map AdmissionBoundaryPort.key conditionExits → artifact.PrimitiveOutputKeyAccounted key
    intro key hKeyartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedkey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key conditionExits⊢ artifact.PrimitiveOutputKeyAccounted key
    exact
      hAccounted.outputs
        (PrimitiveGraphStep.nodeExitKeysList_mem_of_node_mem
          hPrimitiveNode hKey)All goals completed! 🐙
  case latent =>artifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {entry : SelectArmKey × SelectArmAdmissionArtifact},
  entry ∈ (selectAdmission.toLatentSelectAdmission hValid).entries →
    artifact.SelectLatentEntryReconstruction selectAdmission hValid entry
    intro entry hEntryartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedentry:SelectArmKey × SelectArmAdmissionArtifacthEntry:entry ∈ (selectAdmission.toLatentSelectAdmission hValid).entries⊢ artifact.SelectLatentEntryReconstruction selectAdmission hValid entry
    exact hSound.selectLatentEntryReconstruction hSelect hValid hEntryAll goals completed! 🐙
  case resolution =>artifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {arm : SelectArmAdmissionArtifact}, arm ∈ selectAdmission.arms → SelectArmResolutionReconstruction selectAdmission arm
    intro arm hArmartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.arms⊢ SelectArmResolutionReconstruction selectAdmission arm
    exact hSound.selectArmResolutionReconstruction hSelect hArmAll goals completed! 🐙
  case bridge =>artifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {arm : SelectArmAdmissionArtifact},
  arm ∈ selectAdmission.arms → ∃ variant, SelectArmBridgeReconstruction selectAdmission arm conditionExits variant
    intro arm hArmartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.arms⊢ ∃ variant, SelectArmBridgeReconstruction selectAdmission arm conditionExits variant
    obtain ⟨variant, hVariantMem, hVariantKey, hBodyShape⟩ := hArms arm hArmartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsvariant:SelectVariantArtifacthVariantMem:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhBodyShape:(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
    SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
  List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
    (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
      (SelectConditionBridgeOutputShapes selectAdmission conditionExits)⊢ ∃ variant, SelectArmBridgeReconstruction selectAdmission arm conditionExits variant
    refine
      ⟨ variant
      , { variantMem := hVariantMem
          variantKey := hVariantKey
          bodyShape := ?_ }⟩artifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsvariant:SelectVariantArtifacthVariantMem:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhBodyShape:(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
    SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
  List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
    (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
      (SelectConditionBridgeOutputShapes selectAdmission conditionExits)⊢ SelectArmBodyShapeReconstruction selectAdmission arm conditionExits variant
    cases hBodyShape with
    | inl hEmpty =>inlartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsvariant:SelectVariantArtifacthVariantMem:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhEmpty:(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
  SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape]⊢ SelectArmBodyShapeReconstruction selectAdmission arm conditionExits variant
        obtain ⟨⟨hBodyNodes, hBodyEntries, hBodyExits⟩, hOutputShapes⟩ :=
          hEmptyinlartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsvariant:SelectVariantArtifacthVariantMem:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhOutputShapes:SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape]hBodyNodes:arm.bodyNodes = []hBodyEntries:arm.bodyEntries = []hBodyExits:arm.bodyExits = []⊢ SelectArmBodyShapeReconstruction selectAdmission arm conditionExits variant
        exact
          SelectArmBodyShapeReconstruction.emptyBody
            hBodyNodes hBodyEntries hBodyExits hOutputShapesAll goals completed! 🐙
    | inr hNonEmpty =>inrartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsvariant:SelectVariantArtifacthVariantMem:variant ∈ selectAdmission.variantshVariantKey:variant.key = arm.canonicalKeyhNonEmpty:List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
  (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
    (SelectConditionBridgeOutputShapes selectAdmission conditionExits)⊢ SelectArmBodyShapeReconstruction selectAdmission arm conditionExits variant
        exact
          SelectArmBodyShapeReconstruction.nonEmptyBody
            hNonEmpty.left hNonEmpty.rightAll goals completed! 🐙
  case variantBridge =>artifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ ∀ {variant : SelectVariantArtifact},
  variant ∈ selectAdmission.variants →
    ∃ entry, artifact.SelectVariantBridgeReconstruction variant conditionEntries entry
    intro variant hVariantartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variants⊢ ∃ entry, artifact.SelectVariantBridgeReconstruction variant conditionEntries entry
    obtain
      ⟨variantEntries, _variantExits, variantEntry,
        hVariantPrimitiveNode, hVariantEntryMem, hVariantCompat,
        hVariantReplayed, hVariantConsumed⟩ :=
      hSound.select.variantBridgeEntryConsumed hSelect hVariantartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantsvariantEntries:List AdmissionBoundaryPort_variantExits:List AdmissionBoundaryPortvariantEntry:AdmissionBoundaryPorthVariantPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode variantEntries _variantExits ∈ artifact.primitiveStepshVariantEntryMem:variantEntry ∈ variantEntrieshVariantCompat:variant.port.CompatibleWith variantEntryhVariantReplayed:{ fromPort := variant.port, toPort := variantEntry } ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveStepshVariantConsumed:variantEntry.key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps⊢ ∃ entry, artifact.SelectVariantBridgeReconstruction variant conditionEntries entry
    obtain ⟨hEntriesEq, _hExitsEq⟩ :=
      hSound.primitiveNode_frontiers_unique
        hVariantPrimitiveNode hPrimitiveNodeartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionEntries:List AdmissionBoundaryPortconditionExits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode conditionEntries conditionExits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantsvariantEntries:List AdmissionBoundaryPort_variantExits:List AdmissionBoundaryPortvariantEntry:AdmissionBoundaryPorthVariantPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode variantEntries _variantExits ∈ artifact.primitiveStepshVariantEntryMem:variantEntry ∈ variantEntrieshVariantCompat:variant.port.CompatibleWith variantEntryhVariantReplayed:{ fromPort := variant.port, toPort := variantEntry } ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveStepshVariantConsumed:variantEntry.key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveStepshEntriesEq:variantEntries = conditionEntries_hExitsEq:_variantExits = conditionExits⊢ ∃ entry, artifact.SelectVariantBridgeReconstruction variant conditionEntries entry
    subst hEntriesEqartifact:WireAdmissionArtifacthSound:artifact.SoundselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsconditionExits:List AdmissionBoundaryPorthArms:∀ arm ∈ selectAdmission.arms,
  ∃ variant ∈ selectAdmission.variants,
    variant.key = arm.canonicalKey ∧
      ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧
          SelectConditionBridgeOutputShapes selectAdmission conditionExits = [variant.port.identityOutputShape] ∨
        List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧
          (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm
            (SelectConditionBridgeOutputShapes selectAdmission conditionExits))hValid:selectAdmission.ValidhAccounted:artifact.PrimitiveFrontierKeysAccountedvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantsvariantEntries:List AdmissionBoundaryPort_variantExits:List AdmissionBoundaryPortvariantEntry:AdmissionBoundaryPorthVariantPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode variantEntries _variantExits ∈ artifact.primitiveStepshVariantEntryMem:variantEntry ∈ variantEntrieshVariantCompat:variant.port.CompatibleWith variantEntryhVariantReplayed:{ fromPort := variant.port, toPort := variantEntry } ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveStepshVariantConsumed:variantEntry.key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps_hExitsEq:_variantExits = conditionExitshPrimitiveNode:PrimitiveGraphStep.node selectAdmission.conditionNode variantEntries conditionExits ∈ artifact.primitiveSteps⊢ ∃ entry, artifact.SelectVariantBridgeReconstruction variant variantEntries entry
    exact
      ⟨ variantEntry
      , { entryMem := hVariantEntryMem
          compatible := hVariantCompat
          replayed := hVariantReplayed
          entryConsumed := hVariantConsumed }⟩All goals completed! 🐙

end WireAdmissionArtifactend AdmissionArtifactend Cortex.Wire

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

← PreviousCortex.Wire.AdmissionArtifact.Select Next →Cortex.Wire.AdmissionArtifact.Sound