Theory /Cortex /Wire /AdmissionArtifact /ReadyPhantomBridge

Cortex.Wire.AdmissionArtifact.ReadyPhantomBridge

proofs

On this page

Overview

Imports

import Cortex.Wire.AdmissionArtifact.ReadySelectBridge

Overview

Validator-ready phantom bridge accessors backed by primitive replay.

namespace Cortex.Wirenamespace AdmissionArtifactopen Cortex.Wire.ElaborationIRnamespace WireAdmissionArtifact

Validator readiness exposes primitive backing for phantom adapter bridge frontiers.

theorem validatorReady_phantomBridgeFrontiersBackedByPrimitive
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.PhantomBridgeFrontiersBackedByPrimitive :=
  hReady.phantomBridgeFrontiersBackedByPrimitive

Validator-ready gather artifacts expose primitive backing for the singular entry.

theorem validatorReady_phantomAdapter_gather_singularEntryBacked
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.gather) :
    phantom.singular.key ∈
      PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gather⊢ phantom.singular.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps
  have hComponents := validatorReady_componentFrontiersBackedByPrimitive hReadyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhComponents:artifact.ComponentFrontiersBackedByPrimitive⊢ phantom.singular.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps
  have hPhantomBacked := hComponents.phantomAdapters phantom hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhComponents:artifact.ComponentFrontiersBackedByPrimitivehPhantomBacked:match phantom.direction with
| PhantomAdapterDirection.gather =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
| PhantomAdapterDirection.scatter =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps⊢ phantom.singular.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps
  rw [hDirection] at hPhantomBackedartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gatherhComponents:artifact.ComponentFrontiersBackedByPrimitivehPhantomBacked:match PhantomAdapterDirection.gather with
| PhantomAdapterDirection.gather =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
| PhantomAdapterDirection.scatter =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps⊢ phantom.singular.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps
  exact hPhantomBacked.leftAll goals completed! 🐙

Validator-ready gather artifacts expose primitive backing for each multi-side exit.

theorem validatorReady_phantomAdapter_gather_multiExitBacked
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.gather)
    {multi : AdmissionBoundaryPort}
    (hMulti : multi ∈ phantom.multi) :
    multi.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gathermulti:AdmissionBoundaryPorthMulti:multi ∈ phantom.multi⊢ multi.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
  have hComponents := validatorReady_componentFrontiersBackedByPrimitive hReadyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gathermulti:AdmissionBoundaryPorthMulti:multi ∈ phantom.multihComponents:artifact.ComponentFrontiersBackedByPrimitive⊢ multi.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
  have hPhantomBacked := hComponents.phantomAdapters phantom hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gathermulti:AdmissionBoundaryPorthMulti:multi ∈ phantom.multihComponents:artifact.ComponentFrontiersBackedByPrimitivehPhantomBacked:match phantom.direction with
| PhantomAdapterDirection.gather =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
| PhantomAdapterDirection.scatter =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps⊢ multi.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
  rw [hDirection] at hPhantomBackedartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.gathermulti:AdmissionBoundaryPorthMulti:multi ∈ phantom.multihComponents:artifact.ComponentFrontiersBackedByPrimitivehPhantomBacked:match PhantomAdapterDirection.gather with
| PhantomAdapterDirection.gather =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
| PhantomAdapterDirection.scatter =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps⊢ multi.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
  exact hPhantomBacked.right multi hMultiAll goals completed! 🐙

Validator-ready scatter artifacts expose primitive backing for the singular exit.

theorem validatorReady_phantomAdapter_scatter_singularExitBacked
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.scatter) :
    phantom.singular.key ∈
      PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatter⊢ phantom.singular.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
  have hComponents := validatorReady_componentFrontiersBackedByPrimitive hReadyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhComponents:artifact.ComponentFrontiersBackedByPrimitive⊢ phantom.singular.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
  have hPhantomBacked := hComponents.phantomAdapters phantom hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhComponents:artifact.ComponentFrontiersBackedByPrimitivehPhantomBacked:match phantom.direction with
| PhantomAdapterDirection.gather =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
| PhantomAdapterDirection.scatter =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps⊢ phantom.singular.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
  rw [hDirection] at hPhantomBackedartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scatterhComponents:artifact.ComponentFrontiersBackedByPrimitivehPhantomBacked:match PhantomAdapterDirection.scatter with
| PhantomAdapterDirection.gather =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
| PhantomAdapterDirection.scatter =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps⊢ phantom.singular.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
  exact hPhantomBacked.leftAll goals completed! 🐙

Validator-ready scatter artifacts expose primitive backing for each multi-side entry.

theorem validatorReady_phantomAdapter_scatter_multiEntryBacked
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    (hDirection : phantom.direction = PhantomAdapterDirection.scatter)
    {multi : AdmissionBoundaryPort}
    (hMulti : multi ∈ phantom.multi) :
    multi.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scattermulti:AdmissionBoundaryPorthMulti:multi ∈ phantom.multi⊢ multi.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps
  have hComponents := validatorReady_componentFrontiersBackedByPrimitive hReadyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scattermulti:AdmissionBoundaryPorthMulti:multi ∈ phantom.multihComponents:artifact.ComponentFrontiersBackedByPrimitive⊢ multi.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps
  have hPhantomBacked := hComponents.phantomAdapters phantom hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scattermulti:AdmissionBoundaryPorthMulti:multi ∈ phantom.multihComponents:artifact.ComponentFrontiersBackedByPrimitivehPhantomBacked:match phantom.direction with
| PhantomAdapterDirection.gather =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
| PhantomAdapterDirection.scatter =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps⊢ multi.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps
  rw [hDirection] at hPhantomBackedartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdaptershDirection:phantom.direction = PhantomAdapterDirection.scattermulti:AdmissionBoundaryPorthMulti:multi ∈ phantom.multihComponents:artifact.ComponentFrontiersBackedByPrimitivehPhantomBacked:match PhantomAdapterDirection.scatter with
| PhantomAdapterDirection.gather =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps
| PhantomAdapterDirection.scatter =>
  phantom.singular.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps ∧
    ∀ multi ∈ phantom.multi, multi.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps⊢ multi.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps
  exact hPhantomBacked.right multi hMultiAll goals completed! 🐙

Validator-ready phantom artifacts expose primitive backing for left-bulk phantom targets.

theorem validatorReady_phantomBridge_leftBulkTargetBacked
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.leftBulk) :
    pair.toPort.key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps :=
  (validatorReady_phantomBridgeFrontiersBackedByPrimitive
    hReady phantom hPhantom).left pair hPair

Validator-ready phantom artifacts expose primitive backing for right-bulk phantom sources.

theorem validatorReady_phantomBridge_rightBulkSourceBacked
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters)
    {pair : AdmissionConnection}
    (hPair : pair ∈ phantom.rightBulk) :
    pair.fromPort.key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps :=
  (validatorReady_phantomBridgeFrontiersBackedByPrimitive
    hReady phantom hPhantom).right pair hPair

Validator readiness exposes exact phantom bridge primitive frontier matching.

theorem validatorReady_phantomBridgeFrontiersMatchPrimitive
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.PhantomBridgeFrontiersMatchPrimitive :=
  hReady.phantomBridgeFrontiersMatchPrimitive

Validator readiness exposes replay backing for phantom-adapter bulk contraction rows.

theorem validatorReady_phantomBridgeBulkConnectionsReplayed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.PhantomBridgeBulkConnectionsReplayed :=
  hReady.phantomBridgeBulkConnectionsReplayed

A validator-ready phantom adapter has a matching primitive phantom-node frontier row.

theorem validatorReady_phantomBridge_frontiersMatchPrimitive
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    ∃ entries exits,
      PrimitiveGraphStep.node phantom.node entries exits ∈ artifact.primitiveSteps ∧
        phantom.leftBulkTargetKeys.Perm (entries.map AdmissionBoundaryPort.key) ∧
        phantom.rightBulkSourceKeys.Perm (exits.map AdmissionBoundaryPort.key) :=
  validatorReady_phantomBridgeFrontiersMatchPrimitive hReady phantom hPhantom

Validator-ready phantom adapters are backed by primitive node identity rows.

theorem validatorReady_phantomAdapter_node_mem_primitiveRows
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {phantom : PhantomAdapterArtifact}
    (hPhantom : phantom ∈ artifact.phantomAdapters) :
    phantom.node ∈ PrimitiveGraphStep.nodeRowsList artifact.primitiveSteps := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapters⊢ phantom.node ∈ PrimitiveGraphStep.nodeRowsList artifact.primitiveSteps
  obtain ⟨_entries, _exits, hNode, _hInputs, _hOutputs⟩ :=
    validatorReady_phantomBridge_frontiersMatchPrimitive hReady hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyphantom:PhantomAdapterArtifacthPhantom:phantom ∈ artifact.phantomAdapters_entries:List AdmissionBoundaryPort_exits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node phantom.node _entries _exits ∈ artifact.primitiveSteps_hInputs:phantom.leftBulkTargetKeys.Perm (List.map AdmissionBoundaryPort.key _entries)_hOutputs:phantom.rightBulkSourceKeys.Perm (List.map AdmissionBoundaryPort.key _exits)⊢ phantom.node ∈ PrimitiveGraphStep.nodeRowsList artifact.primitiveSteps
  exact PrimitiveGraphStep.nodeRowsList_mem_of_node_mem hNodeAll goals completed! 🐙

end WireAdmissionArtifactend AdmissionArtifactend Cortex.Wire

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

← PreviousCortex.Wire.AdmissionArtifact.ReadyPhantom Next →Cortex.Wire.AdmissionArtifact.ReadyPrimitive