Theory /Cortex /Wire /AdmissionArtifact /ReadyGeneral

Cortex.Wire.AdmissionArtifact.ReadyGeneral

proofs

On this page

Overview

Imports

import Cortex.Wire.AdmissionArtifact.ValidatorCore

Overview

Validator-ready core replay and component-ledger accessors.

namespace Cortex.Wirenamespace AdmissionArtifactopen Cortex.Wire.ElaborationIRnamespace WireAdmissionArtifact

Validator readiness exposes current-schema equality.

theorem validatorReady_schemaCurrent
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.SchemaCurrent :=
  hReady.schemaCurrent

Validator readiness exposes top-level summary-key uniqueness.

theorem validatorReady_summaryKeysUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.SummaryKeysUnique :=
  hReady.summaryKeysUnique

Validator readiness exposes top-level summary-row validity.

theorem validatorReady_summaryRowsValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.SummaryRowsValid :=
  hReady.summaryRowsValid

Validator readiness exposes top-level summary-domain closure.

theorem validatorReady_summaryDomainClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.SummaryDomainClosed :=
  hReady.summaryDomainClosed

Validator readiness exposes raw connection summary coverage by primitive connect rows.

theorem validatorReady_rawConnectionsMatchPrimitive
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.RawConnectionsMatchPrimitive :=
  hReady.rawConnectionsMatchPrimitive

Validator readiness exposes exact primitive backing for node and binding summaries.

theorem validatorReady_summaryIdentitiesMatchPrimitive
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.SummaryIdentitiesMatchPrimitive :=
  hReady.summaryIdentitiesMatchPrimitive

Validator readiness exposes primitive backing for top-level entry/exit summaries.

theorem validatorReady_summaryFrontiersBackedByPrimitive
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.SummaryFrontiersBackedByPrimitive :=
  hReady.summaryFrontiersBackedByPrimitive

Validator readiness exposes exact primitive residual-frontier coverage.

theorem validatorReady_summaryFrontiersMatchPrimitive
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.SummaryFrontiersMatchPrimitive :=
  hReady.summaryFrontiersMatchPrimitive

Validator readiness exposes structured trace-row domain closure.

theorem validatorReady_componentDomainsClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.ComponentDomainsClosed :=
  hReady.componentDomainsClosed

Validator readiness exposes uniqueness for generated/phantom/select component rows.

theorem validatorReady_componentRowsUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.ComponentRowsUnique :=
  hReady.componentRowsUnique

Validator readiness exposes unique generated-family binding rows.

theorem validatorReady_generatedFormBindingsUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    (artifact.generatedForms.map GeneratedFormArtifact.binding).Nodup :=
  (validatorReady_componentRowsUnique hReady).generatedFormBindingsUnique

Validator readiness exposes unique phantom-adapter node rows.

theorem validatorReady_phantomAdapterNodesUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    (artifact.phantomAdapters.map PhantomAdapterArtifact.node).Nodup :=
  (validatorReady_componentRowsUnique hReady).phantomAdapterNodesUnique

Validator readiness exposes unique select condition-node rows.

theorem validatorReady_selectConditionNodesUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    (artifact.selects.map SelectAdmissionArtifact.conditionNode).Nodup :=
  (validatorReady_componentRowsUnique hReady).selectConditionNodesUnique

Validator readiness exposes global component-role node uniqueness.

theorem validatorReady_componentRoleNodesUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.componentRoleNodes.Nodup :=
  (validatorReady_componentRowsUnique hReady).componentRoleNodesUnique

Validator readiness exposes duplicate-free generated child component nodes.

theorem validatorReady_generatedUsedChildNodesUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.generatedUsedChildNodes.Nodup := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReady⊢ artifact.generatedUsedChildNodes.Nodup
  have hUnique := validatorReady_componentRoleNodesUnique hReadyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyhUnique:artifact.componentRoleNodes.Nodup⊢ artifact.generatedUsedChildNodes.Nodup
  have hGeneratedPhantomUnique :
      (artifact.generatedUsedChildNodes ++
        artifact.phantomAdapters.map PhantomAdapterArtifact.node).Nodup := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReady⊢ artifact.generatedUsedChildNodes.Nodup
    simpa [componentRoleNodes] using List.Nodup.of_append_left hUniqueAll goals completed! 🐙
  exact List.Nodup.of_append_left hGeneratedPhantomUniqueAll goals completed! 🐙

Validator readiness exposes disjoint generated-child and phantom-adapter node ledgers.

theorem validatorReady_generatedChildNodes_disjoint_phantomAdapterNodes
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.generatedUsedChildNodes.Disjoint
      (artifact.phantomAdapters.map PhantomAdapterArtifact.node) := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReady⊢ artifact.generatedUsedChildNodes.Disjoint (List.map PhantomAdapterArtifact.node artifact.phantomAdapters)
  have hUnique := validatorReady_componentRoleNodesUnique hReadyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyhUnique:artifact.componentRoleNodes.Nodup⊢ artifact.generatedUsedChildNodes.Disjoint (List.map PhantomAdapterArtifact.node artifact.phantomAdapters)
  have hGeneratedPhantomUnique :
      (artifact.generatedUsedChildNodes ++
        artifact.phantomAdapters.map PhantomAdapterArtifact.node).Nodup := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReady⊢ artifact.generatedUsedChildNodes.Disjoint (List.map PhantomAdapterArtifact.node artifact.phantomAdapters)
    simpa [componentRoleNodes] using List.Nodup.of_append_left hUniqueAll goals completed! 🐙
  exact List.Nodup.disjoint hGeneratedPhantomUniqueAll goals completed! 🐙

Validator readiness exposes disjoint generated-child and select-condition node ledgers.

theorem validatorReady_generatedChildNodes_disjoint_selectConditionNodes
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.generatedUsedChildNodes.Disjoint
      (artifact.selects.map SelectAdmissionArtifact.conditionNode) := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReady⊢ artifact.generatedUsedChildNodes.Disjoint (List.map SelectAdmissionArtifact.conditionNode artifact.selects)
  have hUnique := validatorReady_componentRoleNodesUnique hReadyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyhUnique:artifact.componentRoleNodes.Nodup⊢ artifact.generatedUsedChildNodes.Disjoint (List.map SelectAdmissionArtifact.conditionNode artifact.selects)
  have hDisjoint :
      (artifact.generatedUsedChildNodes ++
        artifact.phantomAdapters.map PhantomAdapterArtifact.node).Disjoint
        (artifact.selects.map SelectAdmissionArtifact.conditionNode) := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReady⊢ artifact.generatedUsedChildNodes.Disjoint (List.map SelectAdmissionArtifact.conditionNode artifact.selects)
    simpa [componentRoleNodes] using List.Nodup.disjoint hUniqueAll goals completed! 🐙
  intro node hGeneratedartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyhUnique:artifact.componentRoleNodes.NoduphDisjoint:(artifact.generatedUsedChildNodes ++ List.map PhantomAdapterArtifact.node artifact.phantomAdapters).Disjoint
  (List.map SelectAdmissionArtifact.conditionNode artifact.selects)node:NodeIdhGenerated:node ∈ artifact.generatedUsedChildNodes⊢ node ∈ List.map SelectAdmissionArtifact.conditionNode artifact.selects → False hSelectartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyhUnique:artifact.componentRoleNodes.NoduphDisjoint:(artifact.generatedUsedChildNodes ++ List.map PhantomAdapterArtifact.node artifact.phantomAdapters).Disjoint
  (List.map SelectAdmissionArtifact.conditionNode artifact.selects)node:NodeIdhGenerated:node ∈ artifact.generatedUsedChildNodeshSelect:node ∈ List.map SelectAdmissionArtifact.conditionNode artifact.selects⊢ False
  exact hDisjoint (List.mem_append_left _ hGenerated) hSelectAll goals completed! 🐙

Validator readiness exposes disjoint phantom-adapter and select-condition node ledgers.

theorem validatorReady_phantomAdapterNodes_disjoint_selectConditionNodes
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    (artifact.phantomAdapters.map PhantomAdapterArtifact.node).Disjoint
      (artifact.selects.map SelectAdmissionArtifact.conditionNode) := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReady⊢ (List.map PhantomAdapterArtifact.node artifact.phantomAdapters).Disjoint
  (List.map SelectAdmissionArtifact.conditionNode artifact.selects)
  have hUnique := validatorReady_componentRoleNodesUnique hReadyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyhUnique:artifact.componentRoleNodes.Nodup⊢ (List.map PhantomAdapterArtifact.node artifact.phantomAdapters).Disjoint
  (List.map SelectAdmissionArtifact.conditionNode artifact.selects)
  have hDisjoint :
      (artifact.generatedUsedChildNodes ++
        artifact.phantomAdapters.map PhantomAdapterArtifact.node).Disjoint
        (artifact.selects.map SelectAdmissionArtifact.conditionNode) := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReady⊢ (List.map PhantomAdapterArtifact.node artifact.phantomAdapters).Disjoint
  (List.map SelectAdmissionArtifact.conditionNode artifact.selects)
    simpa [componentRoleNodes] using List.Nodup.disjoint hUniqueAll goals completed! 🐙
  intro node hPhantomartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyhUnique:artifact.componentRoleNodes.NoduphDisjoint:(artifact.generatedUsedChildNodes ++ List.map PhantomAdapterArtifact.node artifact.phantomAdapters).Disjoint
  (List.map SelectAdmissionArtifact.conditionNode artifact.selects)node:NodeIdhPhantom:node ∈ List.map PhantomAdapterArtifact.node artifact.phantomAdapters⊢ node ∈ List.map SelectAdmissionArtifact.conditionNode artifact.selects → False hSelectartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyhUnique:artifact.componentRoleNodes.NoduphDisjoint:(artifact.generatedUsedChildNodes ++ List.map PhantomAdapterArtifact.node artifact.phantomAdapters).Disjoint
  (List.map SelectAdmissionArtifact.conditionNode artifact.selects)node:NodeIdhPhantom:node ∈ List.map PhantomAdapterArtifact.node artifact.phantomAdaptershSelect:node ∈ List.map SelectAdmissionArtifact.conditionNode artifact.selects⊢ False
  exact hDisjoint (List.mem_append_right _ hPhantom) hSelectAll goals completed! 🐙

Validator readiness exposes the anchor condition for empty generated-family rows.

theorem validatorReady_generatedFormsReferenced
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.GeneratedFormsReferenced :=
  hReady.generatedFormsReferenced

Validator-ready generated-form rows are anchored by used children or an empty binding ref.

theorem validatorReady_generatedForm_referenced
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms) :
    generated.usedChildren ≠ [] ∨
      (generated.sourceChildren = [] ∧ generated.binding ∈ artifact.bindingRefs) :=
  validatorReady_generatedFormsReferenced hReady generated hGenerated

Empty validator-ready generated-form rows have no source children.

theorem validatorReady_emptyGeneratedForm_sourceChildren_empty
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    (hEmpty : generated.usedChildren = []) :
    generated.sourceChildren = [] := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshEmpty:generated.usedChildren = []⊢ generated.sourceChildren = []
  cases validatorReady_generatedForm_referenced hReady hGenerated with
  | inl hUsed =>inlartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshEmpty:generated.usedChildren = []hUsed:generated.usedChildren ≠ []⊢ generated.sourceChildren = []
      exact False.elim (hUsed hEmpty)All goals completed! 🐙
  | inr hAnchor =>inrartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshEmpty:generated.usedChildren = []hAnchor:generated.sourceChildren = [] ∧ generated.binding ∈ artifact.bindingRefs⊢ generated.sourceChildren = []
      exact hAnchor.leftAll goals completed! 🐙

Empty validator-ready generated-form rows are anchored by a primitive binding ref.

theorem validatorReady_emptyGeneratedForm_bindingRef
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    (hEmpty : generated.usedChildren = []) :
    generated.binding ∈ artifact.bindingRefs := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshEmpty:generated.usedChildren = []⊢ generated.binding ∈ artifact.bindingRefs
  cases validatorReady_generatedForm_referenced hReady hGenerated with
  | inl hUsed =>inlartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshEmpty:generated.usedChildren = []hUsed:generated.usedChildren ≠ []⊢ generated.binding ∈ artifact.bindingRefs
      exact False.elim (hUsed hEmpty)All goals completed! 🐙
  | inr hAnchor =>inrartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshEmpty:generated.usedChildren = []hAnchor:generated.sourceChildren = [] ∧ generated.binding ∈ artifact.bindingRefs⊢ generated.binding ∈ artifact.bindingRefs
      exact hAnchor.rightAll goals completed! 🐙

Validator readiness exposes primitive backing for component-local frontier rows.

theorem validatorReady_componentFrontiersBackedByPrimitive
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.ComponentFrontiersBackedByPrimitive :=
  hReady.componentFrontiersBackedByPrimitive

Validator readiness exposes exact generated-child primitive frontier matching.

theorem validatorReady_generatedChildFrontiersMatchPrimitive
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.GeneratedChildFrontiersMatchPrimitive :=
  hReady.generatedChildFrontiersMatchPrimitive

Validator readiness exposes primitive graph-step stack replay validity.

theorem validatorReady_primitiveTraceStackValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.PrimitiveTraceStackValid :=
  hReady.primitiveTraceStackValid

Validator readiness exposes a primitive replay final frame matching the summary.

theorem validatorReady_primitiveTrace_replaysToSummary
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    ∃ finalFrame,
      PrimitiveTraceReplays artifact.SelectInternalTraceExit
        artifact.primitiveSteps [] [finalFrame] ∧
        finalFrame.MatchesSummary artifact :=
  validatorReady_primitiveTraceStackValid hReady

A validator-ready generated child has a matching primitive node frontier row.

theorem validatorReady_generatedChild_frontiersMatchPrimitive
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    ∃ entries exits,
      PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveSteps ∧
        child.inputKeys.Perm (entries.map AdmissionBoundaryPort.key) ∧
        child.outputKeys.Perm (exits.map AdmissionBoundaryPort.key) :=
  validatorReady_generatedChildFrontiersMatchPrimitive
    hReady generated hGenerated child hChild

Validator-ready generated children are backed by primitive node identity rows.

theorem validatorReady_generatedChild_node_mem_primitiveRows
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    child.node ∈ PrimitiveGraphStep.nodeRowsList artifact.primitiveSteps := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ child.node ∈ PrimitiveGraphStep.nodeRowsList artifact.primitiveSteps
  obtain ⟨_entries, _exits, hNode, _hInputs, _hOutputs⟩ :=
    validatorReady_generatedChild_frontiersMatchPrimitive hReady hGenerated hChildartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren_entries:List AdmissionBoundaryPort_exits:List AdmissionBoundaryPorthNode:PrimitiveGraphStep.node child.node _entries _exits ∈ artifact.primitiveSteps_hInputs:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key _entries)_hOutputs:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key _exits)⊢ child.node ∈ PrimitiveGraphStep.nodeRowsList artifact.primitiveSteps
  exact PrimitiveGraphStep.nodeRowsList_mem_of_node_mem hNodeAll goals completed! 🐙

Validator readiness exposes primitive overlay prefix-availability.

theorem validatorReady_primitiveOverlayLedgersPrefixAvailable
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.PrimitiveOverlayLedgersPrefixAvailable :=
  hReady.primitiveOverlayLedgersPrefixAvailable

Validator-ready primitive overlay rows draw node and binding ledgers from their trace prefix.

theorem validatorReady_primitiveOverlay_prefixAvailable
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {tracePrefix suffix : List PrimitiveGraphStep}
    {leftNodes rightNodes : List NodeId}
    {leftBindings rightBindings : List BindingName}
    (hTrace :
      artifact.primitiveSteps =
        tracePrefix ++
          [PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings] ++
          suffix) :
    (∀ node, node ∈ leftNodes ++ rightNodes →
      node ∈ PrimitiveGraphStep.nodeRowsList tracePrefix) ∧
    (∀ binding, binding ∈ leftBindings ++ rightBindings →
      binding ∈ PrimitiveGraphStep.bindingRowsList tracePrefix) :=
  validatorReady_primitiveOverlayLedgersPrefixAvailable
    hReady tracePrefix suffix leftNodes rightNodes leftBindings rightBindings hTrace

Validator-ready primitive overlay rows have a replay prefix that already contains their ledgers.

theorem validatorReady_primitiveOverlay_mem_prefixAvailable
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {leftNodes rightNodes : List NodeId}
    {leftBindings rightBindings : List BindingName}
    (hPrimitiveStep :
      PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings ∈
        artifact.primitiveSteps) :
    ∃ tracePrefix suffix,
      artifact.primitiveSteps =
        tracePrefix ++
          [PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings] ++
          suffix ∧
        (∀ node, node ∈ leftNodes ++ rightNodes →
          node ∈ PrimitiveGraphStep.nodeRowsList tracePrefix) ∧
        (∀ binding, binding ∈ leftBindings ++ rightBindings →
          binding ∈ PrimitiveGraphStep.bindingRowsList tracePrefix) := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehPrimitiveStep:PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings ∈ artifact.primitiveSteps⊢ ∃ tracePrefix suffix,
  artifact.primitiveSteps =
      tracePrefix ++ [PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings] ++ suffix ∧
    (∀ node ∈ leftNodes ++ rightNodes, node ∈ PrimitiveGraphStep.nodeRowsList tracePrefix) ∧
      ∀ binding ∈ leftBindings ++ rightBindings, binding ∈ PrimitiveGraphStep.bindingRowsList tracePrefix
  obtain ⟨tracePrefix, suffix, hTrace⟩ :=
    exists_append_singleton_of_mem hPrimitiveStepartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehPrimitiveStep:PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings ∈ artifact.primitiveStepstracePrefix:List PrimitiveGraphStepsuffix:List PrimitiveGraphStephTrace:artifact.primitiveSteps =
  tracePrefix ++ [PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings] ++ suffix⊢ ∃ tracePrefix suffix,
  artifact.primitiveSteps =
      tracePrefix ++ [PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings] ++ suffix ∧
    (∀ node ∈ leftNodes ++ rightNodes, node ∈ PrimitiveGraphStep.nodeRowsList tracePrefix) ∧
      ∀ binding ∈ leftBindings ++ rightBindings, binding ∈ PrimitiveGraphStep.bindingRowsList tracePrefix
  refine ⟨tracePrefix, suffix, hTrace, ?_⟩artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehPrimitiveStep:PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings ∈ artifact.primitiveStepstracePrefix:List PrimitiveGraphStepsuffix:List PrimitiveGraphStephTrace:artifact.primitiveSteps =
  tracePrefix ++ [PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings] ++ suffix⊢ (∀ node ∈ leftNodes ++ rightNodes, node ∈ PrimitiveGraphStep.nodeRowsList tracePrefix) ∧
  ∀ binding ∈ leftBindings ++ rightBindings, binding ∈ PrimitiveGraphStep.bindingRowsList tracePrefix
  exact validatorReady_primitiveOverlay_prefixAvailable hReady hTraceAll goals completed! 🐙

Validator readiness exposes primitive backing for primitive connect frontier rows.

theorem validatorReady_primitiveConnectFrontiersBackedByNodes
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.PrimitiveConnectFrontiersBackedByNodes :=
  hReady.primitiveConnectFrontiersBackedByNodes

Validator readiness exposes primitive connect prefix-availability.

theorem validatorReady_primitiveConnectFrontiersPrefixAvailable
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady) :
    artifact.PrimitiveConnectFrontiersPrefixAvailable :=
  hReady.primitiveConnectFrontiersPrefixAvailable

Validator-ready primitive connect rows draw frontiers from their trace prefix.

theorem validatorReady_primitiveConnect_prefixAvailable
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {tracePrefix suffix : List PrimitiveGraphStep}
    {leftExits rightEntries : List AdmissionBoundaryPort}
    {matchedPairs : List AdmissionConnection}
    {unmatchedLeftExits unmatchedRightEntries : List AdmissionBoundaryPort}
    (hTrace :
      artifact.primitiveSteps =
        tracePrefix ++
          [PrimitiveGraphStep.connect
            leftExits rightEntries matchedPairs unmatchedLeftExits
            unmatchedRightEntries] ++
          suffix) :
    (∀ leftExit, leftExit ∈ leftExits →
      leftExit.key ∈ PrimitiveGraphStep.nodeExitKeysList tracePrefix ∧
        leftExit.key ∉ PrimitiveGraphStep.consumedExitKeysList tracePrefix) ∧
    (∀ rightEntry, rightEntry ∈ rightEntries →
      rightEntry.key ∈ PrimitiveGraphStep.nodeEntryKeysList tracePrefix ∧
        rightEntry.key ∉ PrimitiveGraphStep.consumedEntryKeysList tracePrefix) :=
  validatorReady_primitiveConnectFrontiersPrefixAvailable
    hReady tracePrefix suffix leftExits rightEntries matchedPairs
      unmatchedLeftExits unmatchedRightEntries hTrace

Validator-ready primitive connect rows have a replay prefix where their frontiers are live.

theorem validatorReady_primitiveConnect_mem_prefixAvailable
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {leftExits rightEntries : List AdmissionBoundaryPort}
    {matchedPairs : List AdmissionConnection}
    {unmatchedLeftExits unmatchedRightEntries : List AdmissionBoundaryPort}
    (hPrimitiveStep :
      PrimitiveGraphStep.connect
        leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈
        artifact.primitiveSteps) :
    ∃ tracePrefix suffix,
      artifact.primitiveSteps =
        tracePrefix ++
          [PrimitiveGraphStep.connect
            leftExits rightEntries matchedPairs unmatchedLeftExits
            unmatchedRightEntries] ++
          suffix ∧
        (∀ leftExit, leftExit ∈ leftExits →
          leftExit.key ∈ PrimitiveGraphStep.nodeExitKeysList tracePrefix ∧
            leftExit.key ∉ PrimitiveGraphStep.consumedExitKeysList tracePrefix) ∧
        (∀ rightEntry, rightEntry ∈ rightEntries →
          rightEntry.key ∈ PrimitiveGraphStep.nodeEntryKeysList tracePrefix ∧
            rightEntry.key ∉ PrimitiveGraphStep.consumedEntryKeysList tracePrefix) := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthPrimitiveStep:PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈
  artifact.primitiveSteps⊢ ∃ tracePrefix suffix,
  artifact.primitiveSteps =
      tracePrefix ++
          [PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries] ++
        suffix ∧
    (∀ leftExit ∈ leftExits,
        leftExit.key ∈ PrimitiveGraphStep.nodeExitKeysList tracePrefix ∧
          leftExit.key ∉ PrimitiveGraphStep.consumedExitKeysList tracePrefix) ∧
      ∀ rightEntry ∈ rightEntries,
        rightEntry.key ∈ PrimitiveGraphStep.nodeEntryKeysList tracePrefix ∧
          rightEntry.key ∉ PrimitiveGraphStep.consumedEntryKeysList tracePrefix
  obtain ⟨tracePrefix, suffix, hTrace⟩ :=
    exists_append_singleton_of_mem hPrimitiveStepartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthPrimitiveStep:PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈
  artifact.primitiveStepstracePrefix:List PrimitiveGraphStepsuffix:List PrimitiveGraphStephTrace:artifact.primitiveSteps =
  tracePrefix ++
      [PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries] ++
    suffix⊢ ∃ tracePrefix suffix,
  artifact.primitiveSteps =
      tracePrefix ++
          [PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries] ++
        suffix ∧
    (∀ leftExit ∈ leftExits,
        leftExit.key ∈ PrimitiveGraphStep.nodeExitKeysList tracePrefix ∧
          leftExit.key ∉ PrimitiveGraphStep.consumedExitKeysList tracePrefix) ∧
      ∀ rightEntry ∈ rightEntries,
        rightEntry.key ∈ PrimitiveGraphStep.nodeEntryKeysList tracePrefix ∧
          rightEntry.key ∉ PrimitiveGraphStep.consumedEntryKeysList tracePrefix
  refine ⟨tracePrefix, suffix, hTrace, ?_⟩artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadyleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthPrimitiveStep:PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∈
  artifact.primitiveStepstracePrefix:List PrimitiveGraphStepsuffix:List PrimitiveGraphStephTrace:artifact.primitiveSteps =
  tracePrefix ++
      [PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries] ++
    suffix⊢ (∀ leftExit ∈ leftExits,
    leftExit.key ∈ PrimitiveGraphStep.nodeExitKeysList tracePrefix ∧
      leftExit.key ∉ PrimitiveGraphStep.consumedExitKeysList tracePrefix) ∧
  ∀ rightEntry ∈ rightEntries,
    rightEntry.key ∈ PrimitiveGraphStep.nodeEntryKeysList tracePrefix ∧
      rightEntry.key ∉ PrimitiveGraphStep.consumedEntryKeysList tracePrefix
  exact validatorReady_primitiveConnect_prefixAvailable hReady hTraceAll goals completed! 🐙

end WireAdmissionArtifactend AdmissionArtifactend Cortex.Wire

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

← PreviousCortex.Wire.AdmissionArtifact.PrimitiveTraceCheck Next →Cortex.Wire.AdmissionArtifact.ReadyGenerated