Cortex.Wire.AdmissionArtifact.ReadySelectBridge

On this page
  1. Overview
Imports
import Cortex.Wire.AdmissionArtifact.ReadyGeneral

Overview

Validator-ready select bridge accessors backed by primitive replay.

namespace Cortex.Wirenamespace AdmissionArtifactopen Cortex.Wire.ElaborationIRnamespace WireAdmissionArtifact

Validator readiness exposes primitive backing for select condition bridge frontiers.

theorem validatorReady_selectBridgeFrontiersBackedByPrimitive {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) : artifact.SelectBridgeFrontiersBackedByPrimitive := hReady.selectBridgeFrontiersBackedByPrimitive

Validator readiness exposes that select bridge entries are replay-consumed.

theorem validatorReady_selectBridgeEntriesConsumed {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) : artifact.SelectBridgeEntriesConsumed := hReady.selectBridgeEntriesConsumed

Validator-ready select rows expose their primitive condition-node frontier row.

theorem validatorReady_selectBridge_conditionNodePrimitiveRow {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) {selectAdmission : SelectAdmissionArtifact} (hSelect : selectAdmission ∈ artifact.selects) : ∃ entries exits, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps := artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selects⊢ ∃ entries exits, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps_hVariants:∀ variant ∈ selectAdmission.variants, SelectBridgeEntryUnique variant entries ∧ SelectBridgeInternalExitUnique selectAdmission.conditionNode variant exits⊢ ∃ entries exits, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps All goals completed! 🐙

Validator-ready select condition nodes are backed by primitive node identity rows.

theorem validatorReady_select_conditionNode_mem_primitiveRows {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) {selectAdmission : SelectAdmissionArtifact} (hSelect : selectAdmission ∈ artifact.selects) : selectAdmission.conditionNode ∈ PrimitiveGraphStep.nodeRowsList artifact.primitiveSteps := artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selects⊢ selectAdmission.conditionNode ∈ PrimitiveGraphStep.nodeRowsList artifact.primitiveSteps artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selects_entries:List AdmissionBoundaryPort_exits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode _entries _exits ∈ artifact.primitiveSteps⊢ selectAdmission.conditionNode ∈ PrimitiveGraphStep.nodeRowsList artifact.primitiveSteps All goals completed! 🐙

Validator-ready select variants have unique primitive bridge entry and choice-exit rows.

theorem validatorReady_selectBridge_variantFrontiersBackedByPrimitive {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) {selectAdmission : SelectAdmissionArtifact} (hSelect : selectAdmission ∈ artifact.selects) {variant : SelectVariantArtifact} (hVariant : variant ∈ selectAdmission.variants) : ∃ entries exits, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ SelectBridgeEntryUnique variant entries ∧ SelectBridgeInternalExitUnique selectAdmission.conditionNode variant exits := artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variants⊢ ∃ entries exits, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ SelectBridgeEntryUnique variant entries ∧ SelectBridgeInternalExitUnique selectAdmission.conditionNode variant exits artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantsentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepshVariants:∀ variant ∈ selectAdmission.variants, SelectBridgeEntryUnique variant entries ∧ SelectBridgeInternalExitUnique selectAdmission.conditionNode variant exits⊢ ∃ entries exits, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ SelectBridgeEntryUnique variant entries ∧ SelectBridgeInternalExitUnique selectAdmission.conditionNode variant exits All goals completed! 🐙

Validator-ready select variants have a consumed condition-node bridge entry.

theorem validatorReady_select_variant_bridgeEntryConsumed {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) {selectAdmission : SelectAdmissionArtifact} (hSelect : selectAdmission ∈ artifact.selects) {variant : SelectVariantArtifact} (hVariant : variant ∈ selectAdmission.variants) : ∃ entries exits entry, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ entry ∈ entries ∧ variant.port.CompatibleWith entry ∧ { fromPort := variant.port, toPort := entry } ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps ∧ entry.key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps := artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variants⊢ ∃ entries exits entry, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ entry ∈ entries ∧ variant.port.CompatibleWith entry ∧ { fromPort := variant.port, toPort := entry } ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps ∧ entry.key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantsentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepshEntryUnique:SelectBridgeEntryUnique variant entries_hExitUnique:SelectBridgeInternalExitUnique selectAdmission.conditionNode variant exits⊢ ∃ entries exits entry, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ entry ∈ entries ∧ variant.port.CompatibleWith entry ∧ { fromPort := variant.port, toPort := entry } ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps ∧ entry.key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantsentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepshEntryUnique:SelectBridgeEntryUnique variant entries_hExitUnique:SelectBridgeInternalExitUnique selectAdmission.conditionNode variant exitsentry:AdmissionBoundaryPorthEntry:entry ∈ entrieshCompatible:variant.port.CompatibleWith entry⊢ ∃ entries exits entry, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ entry ∈ entries ∧ variant.port.CompatibleWith entry ∧ { fromPort := variant.port, toPort := entry } ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps ∧ entry.key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantsentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepshEntryUnique:SelectBridgeEntryUnique variant entries_hExitUnique:SelectBridgeInternalExitUnique selectAdmission.conditionNode variant exitsentry:AdmissionBoundaryPorthEntry:entry ∈ entrieshCompatible:variant.port.CompatibleWith entryhMatched:{ fromPort := variant.port, toPort := entry } ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps⊢ ∃ entries exits entry, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ entry ∈ entries ∧ variant.port.CompatibleWith entry ∧ { fromPort := variant.port, toPort := entry } ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps ∧ entry.key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps have hConsumed : entry.key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps := artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variants⊢ ∃ entries exits entry, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ entry ∈ entries ∧ variant.port.CompatibleWith entry ∧ { fromPort := variant.port, toPort := entry } ∈ PrimitiveGraphStep.matchedConnectionsList artifact.primitiveSteps ∧ entry.key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps All goals completed! 🐙 All goals completed! 🐙

Validator readiness exposes select arm body boundary compatibility.

theorem validatorReady_selectArmBodyBoundariesMatchCondition {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) : artifact.SelectArmBodyBoundariesMatchCondition := hReady.selectArmBodyBoundariesMatchCondition

Validator-ready select arms consume their selected variant and produce the bridge shape.

theorem validatorReady_select_armBodyBoundariesMatchCondition {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) {selectAdmission : SelectAdmissionArtifact} (hSelect : selectAdmission ∈ artifact.selects) {arm : SelectArmAdmissionArtifact} (hArm : arm ∈ selectAdmission.arms) : ∃ entries exits, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ ∃ variant, variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ (((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape]) ∨ (arm.bodyEntries.map AdmissionBoundaryPort.compatibilityShape = [variant.port.compatibilityShape] ∧ (arm.bodyExits.map AdmissionBoundaryPort.outputShape).Perm (SelectConditionBridgeOutputShapes selectAdmission exits))) := artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.arms⊢ ∃ entries exits, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ ∃ variant ∈ selectAdmission.variants, variant.key = arm.canonicalKey ∧ ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape] ∨ List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits)) artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armsentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepshArms:∀ arm ∈ selectAdmission.arms, ∃ variant ∈ selectAdmission.variants, variant.key = arm.canonicalKey ∧ ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape] ∨ List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits))⊢ ∃ entries exits, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ ∃ variant ∈ selectAdmission.variants, variant.key = arm.canonicalKey ∧ ((arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape] ∨ List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits)) All goals completed! 🐙

Validator-ready identity select arms expose the condition bridge identity shape.

theorem validatorReady_select_identityArm_bridgeShape {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) {selectAdmission : SelectAdmissionArtifact} (hSelect : selectAdmission ∈ artifact.selects) {arm : SelectArmAdmissionArtifact} (hArm : arm ∈ selectAdmission.arms) (hIdentity : arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) : ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape] := artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshIdentity:arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []⊢ ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape] artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshIdentity:arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []entries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshKey:variant.key = arm.canonicalKeyhShape:(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape] ∨ List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits)⊢ ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape] artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshIdentity:arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []entries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshKey:variant.key = arm.canonicalKeyhIdentityShape:(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape]⊢ ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape]artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshIdentity:arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []entries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshKey:variant.key = arm.canonicalKeyhBodyShape:List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits)⊢ ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape] artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshIdentity:arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []entries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshKey:variant.key = arm.canonicalKeyhIdentityShape:(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape]⊢ ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape] All goals completed! 🐙 artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshIdentity:arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []entries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshKey:variant.key = arm.canonicalKeyhBodyShape:List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits)⊢ ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape] have hImpossible : ([] : List (AdmissionPortLabel × ContractId)) = [variant.port.compatibilityShape] := artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshIdentity:arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []⊢ ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape] All goals completed! 🐙 All goals completed! 🐙

Validator-ready non-identity select arms expose body-entry and bridge-output shapes.

theorem validatorReady_select_nonIdentityArm_bodyShapes {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) {selectAdmission : SelectAdmissionArtifact} (hSelect : selectAdmission ∈ artifact.selects) {arm : SelectArmAdmissionArtifact} (hArm : arm ∈ selectAdmission.arms) (hNotIdentity : ¬ (arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = [])) : ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ arm.bodyEntries.map AdmissionBoundaryPort.compatibilityShape = [variant.port.compatibilityShape] ∧ (arm.bodyExits.map AdmissionBoundaryPort.outputShape).Perm (SelectConditionBridgeOutputShapes selectAdmission exits) := artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshNotIdentity:¬(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = [])⊢ ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits) artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshNotIdentity:¬(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = [])entries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshKey:variant.key = arm.canonicalKeyhShape:(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape] ∨ List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits)⊢ ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits) artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshNotIdentity:¬(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = [])entries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshKey:variant.key = arm.canonicalKeyhIdentityShape:(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape]⊢ ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits)artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshNotIdentity:¬(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = [])entries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshKey:variant.key = arm.canonicalKeyhBodyShape:List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits)⊢ ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits) artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshNotIdentity:¬(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = [])entries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshKey:variant.key = arm.canonicalKeyhIdentityShape:(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = []) ∧ SelectConditionBridgeOutputShapes selectAdmission exits = [variant.port.identityOutputShape]⊢ ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits) All goals completed! 🐙 artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectsarm:SelectArmAdmissionArtifacthArm:arm ∈ selectAdmission.armshNotIdentity:¬(arm.bodyNodes = [] ∧ arm.bodyEntries = [] ∧ arm.bodyExits = [])entries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveStepsvariant:SelectVariantArtifacthVariant:variant ∈ selectAdmission.variantshKey:variant.key = arm.canonicalKeyhBodyShape:List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits)⊢ ∃ entries exits variant, PrimitiveGraphStep.node selectAdmission.conditionNode entries exits ∈ artifact.primitiveSteps ∧ variant ∈ selectAdmission.variants ∧ variant.key = arm.canonicalKey ∧ List.map AdmissionBoundaryPort.compatibilityShape arm.bodyEntries = [variant.port.compatibilityShape] ∧ (List.map AdmissionBoundaryPort.outputShape arm.bodyExits).Perm (SelectConditionBridgeOutputShapes selectAdmission exits) All goals completed! 🐙

Validator readiness exposes disjoint latent select-arm body node domains.

theorem validatorReady_selectArmBodyNodesPairwiseDisjoint {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) : artifact.SelectArmBodyNodesPairwiseDisjoint := hReady.selectArmBodyNodesPairwiseDisjoint

Validator readiness exposes freshness of latent select-arm bodies.

theorem validatorReady_selectArmBodyNodesFreshFromSummary {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) : artifact.SelectArmBodyNodesFreshFromSummary := hReady.selectArmBodyNodesFreshFromSummary

Validator-ready select arm body nodes are absent from the top-level node summary.

theorem validatorReady_select_armBodyNodeFresh {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) {selectAdmission : SelectAdmissionArtifact} (hSelect : selectAdmission ∈ artifact.selects) {arm : SelectArmAdmissionArtifact} (hArm : arm ∈ selectAdmission.arms) {node : NodeId} (hNode : node ∈ arm.bodyNodes) : node ∉ artifact.nodes := validatorReady_selectArmBodyNodesFreshFromSummary hReady selectAdmission hSelect arm hArm node hNode

Validator-ready select arms with different canonical keys cannot share body nodes.

theorem validatorReady_select_armBodyNodesDisjoint {artifact : WireAdmissionArtifact} (hReady : artifact.ValidatorReady) {selectAdmission : SelectAdmissionArtifact} (hSelect : selectAdmission ∈ artifact.selects) {left right : SelectArmAdmissionArtifact} (hLeft : left ∈ selectAdmission.arms) (hRight : right ∈ selectAdmission.arms) (hKeys : left.canonicalKey ≠ right.canonicalKey) {node : NodeId} (hNode : node ∈ left.bodyNodes) : node ∉ right.bodyNodes := validatorReady_selectArmBodyNodesPairwiseDisjoint hReady selectAdmission hSelect left hLeft right hRight hKeys node hNodeend WireAdmissionArtifactend AdmissionArtifactend Cortex.Wire