Theory /Cortex /Wire /AdmissionArtifact /PrimitiveReconstruction

Cortex.Wire.AdmissionArtifact.PrimitiveReconstruction

proofs

On this page

Overview
Primitive-Key Membership Helpers
Frame-Level Linearity Facts
Primitive Node Row Uniqueness
Primitive Frontier Accounting
Reconstruction Contract

Imports

import Cortex.Wire.AdmissionArtifact.Sound

Overview

Primitive graph reconstruction from a validator-sound admission artifact.

The decoded admission artifact is lower-level than GraphElaboration.CertifiedGraph: it carries primitive boundary rows and a replay stack, not accepted node declarations inside an AdmittedModuleShell. This module therefore names the strongest honest primitive reconstruction target at the artifact boundary.

A PrimitiveGraphReconstruction says:

primitive rows replay to one final frame;
the final frame is exactly the top-level serialized summary, up to permutation;
source-visible frontier rows are duplicate-free;
every primitive node-frontier key is accounted for as exposed, consumed, or select-internal; and
top-level raw connections are exactly the raw projection of replayed primitive contractions.

The later CertifiedGraph reconstruction step must add the accepted-node/module evidence that is intentionally absent from the serialized artifact rows.

              namespace Cortex.Wirenamespace AdmissionArtifactopen Cortex.Wire.ElaborationIRnamespace PrimitiveGraphStep

Primitive-Key Membership Helpers

A primitive node-entry key belongs to the global primitive entry-key ledger.

theorem nodeEntryKeysList_mem_of_node_mem
    {primitiveSteps : List PrimitiveGraphStep}
    {node : NodeId}
    {entries exits : List AdmissionBoundaryPort}
    {key : NodeId × FieldLabel × ContractId}
    (hStep : PrimitiveGraphStep.node node entries exits ∈ primitiveSteps)
    (hKey : key ∈ entries.map AdmissionBoundaryPort.key) :
    key ∈ nodeEntryKeysList primitiveSteps := byprimitiveSteps:List PrimitiveGraphStepnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortkey:NodeId × FieldLabel × ContractIdhStep:PrimitiveGraphStep.node node entries exits ∈ primitiveStepshKey:key ∈ List.map AdmissionBoundaryPort.key entries⊢ key ∈ nodeEntryKeysList primitiveSteps
  induction primitiveSteps generalizing key with
  | nil =>nilnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortkey:NodeId × FieldLabel × ContractIdhStep:PrimitiveGraphStep.node node entries exits ∈ []hKey:key ∈ List.map AdmissionBoundaryPort.key entries⊢ key ∈ nodeEntryKeysList []
      cases hStepAll goals completed! 🐙
  | cons primitiveStep primitiveSteps ih =>consnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhStep:PrimitiveGraphStep.node node entries exits ∈ primitiveStep :: primitiveStepshKey:key ∈ List.map AdmissionBoundaryPort.key entries⊢ key ∈ nodeEntryKeysList (primitiveStep :: primitiveSteps)
      cases primitiveStep with
      | empty =>cons.emptynode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entrieshStep:PrimitiveGraphStep.node node entries exits ∈ empty :: primitiveSteps⊢ key ∈ nodeEntryKeysList (empty :: primitiveSteps)
          simp only [List.mem_cons] at hStepcons.emptynode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entrieshStep:PrimitiveGraphStep.node node entries exits = empty ∨ PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeEntryKeysList (empty :: primitiveSteps)
          cases hStep with
          | inl hHead =>cons.empty.inlnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entrieshHead:PrimitiveGraphStep.node node entries exits = empty⊢ key ∈ nodeEntryKeysList (empty :: primitiveSteps)
              cases hHeadAll goals completed! 🐙
          | inr hTail =>cons.empty.inrnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entrieshTail:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeEntryKeysList (empty :: primitiveSteps)
              simpa [nodeEntryKeysList, nodeEntryKeys] using ih hTail hKeyAll goals completed! 🐙
      | node rowNode rowEntries rowExits =>cons.nodenode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesrowNode:NodeIdrowEntries:List AdmissionBoundaryPortrowExits:List AdmissionBoundaryPorthStep:PrimitiveGraphStep.node node entries exits ∈ PrimitiveGraphStep.node rowNode rowEntries rowExits :: primitiveSteps⊢ key ∈ nodeEntryKeysList (PrimitiveGraphStep.node rowNode rowEntries rowExits :: primitiveSteps)
          simp only [List.mem_cons] at hStepcons.nodenode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesrowNode:NodeIdrowEntries:List AdmissionBoundaryPortrowExits:List AdmissionBoundaryPorthStep:PrimitiveGraphStep.node node entries exits = PrimitiveGraphStep.node rowNode rowEntries rowExits ∨
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeEntryKeysList (PrimitiveGraphStep.node rowNode rowEntries rowExits :: primitiveSteps)
          cases hStep with
          | inl hHead =>cons.node.inlnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesrowNode:NodeIdrowEntries:List AdmissionBoundaryPortrowExits:List AdmissionBoundaryPorthHead:PrimitiveGraphStep.node node entries exits = PrimitiveGraphStep.node rowNode rowEntries rowExits⊢ key ∈ nodeEntryKeysList (PrimitiveGraphStep.node rowNode rowEntries rowExits :: primitiveSteps)
              cases hHeadcons.node.inl.reflnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entries⊢ key ∈ nodeEntryKeysList (PrimitiveGraphStep.node node entries exits :: primitiveSteps)
              simp [nodeEntryKeysList, nodeEntryKeys, hKey]All goals completed! 🐙
          | inr hTail =>cons.node.inrnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesrowNode:NodeIdrowEntries:List AdmissionBoundaryPortrowExits:List AdmissionBoundaryPorthTail:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeEntryKeysList (PrimitiveGraphStep.node rowNode rowEntries rowExits :: primitiveSteps)
              exact
                List.mem_append.mpr
                  (Or.inr (ih hTail hKey))All goals completed! 🐙
      | bindingRef binding =>cons.bindingRefnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesbinding:BindingNamehStep:PrimitiveGraphStep.node node entries exits ∈ bindingRef binding :: primitiveSteps⊢ key ∈ nodeEntryKeysList (bindingRef binding :: primitiveSteps)
          simp only [List.mem_cons] at hStepcons.bindingRefnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesbinding:BindingNamehStep:PrimitiveGraphStep.node node entries exits = bindingRef binding ∨
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeEntryKeysList (bindingRef binding :: primitiveSteps)
          cases hStep with
          | inl hHead =>cons.bindingRef.inlnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesbinding:BindingNamehHead:PrimitiveGraphStep.node node entries exits = bindingRef binding⊢ key ∈ nodeEntryKeysList (bindingRef binding :: primitiveSteps)
              cases hHeadAll goals completed! 🐙
          | inr hTail =>cons.bindingRef.inrnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesbinding:BindingNamehTail:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeEntryKeysList (bindingRef binding :: primitiveSteps)
              simpa [nodeEntryKeysList, nodeEntryKeys] using ih hTail hKeyAll goals completed! 🐙
      | overlay leftNodes rightNodes leftBindings rightBindings =>cons.overlaynode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehStep:PrimitiveGraphStep.node node entries exits ∈ overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps⊢ key ∈ nodeEntryKeysList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps)
          simp only [List.mem_cons] at hStepcons.overlaynode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehStep:PrimitiveGraphStep.node node entries exits = overlay leftNodes rightNodes leftBindings rightBindings ∨
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeEntryKeysList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps)
          cases hStep with
          | inl hHead =>cons.overlay.inlnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehHead:PrimitiveGraphStep.node node entries exits = overlay leftNodes rightNodes leftBindings rightBindings⊢ key ∈ nodeEntryKeysList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps)
              cases hHeadAll goals completed! 🐙
          | inr hTail =>cons.overlay.inrnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehTail:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeEntryKeysList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps)
              simpa [nodeEntryKeysList, nodeEntryKeys] using ih hTail hKeyAll goals completed! 🐙
      | connect leftExits rightEntries matchedPairs unmatchedLeftExits
          unmatchedRightEntries =>cons.connectnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthStep:PrimitiveGraphStep.node node entries exits ∈
  connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps⊢ key ∈
  nodeEntryKeysList
    (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps)
          simp only [List.mem_cons] at hStepcons.connectnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthStep:PrimitiveGraphStep.node node entries exits =
    connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∨
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈
  nodeEntryKeysList
    (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps)
          cases hStep with
          | inl hHead =>cons.connect.inlnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthHead:PrimitiveGraphStep.node node entries exits =
  connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries⊢ key ∈
  nodeEntryKeysList
    (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps)
              cases hHeadAll goals completed! 🐙
          | inr hTail =>cons.connect.inrnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key entries → key ∈ nodeEntryKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key entriesleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthTail:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈
  nodeEntryKeysList
    (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps)
              simpa [nodeEntryKeysList, nodeEntryKeys] using ih hTail hKeyAll goals completed! 🐙

A primitive node-exit key belongs to the global primitive exit-key ledger.

theorem nodeExitKeysList_mem_of_node_mem
    {primitiveSteps : List PrimitiveGraphStep}
    {node : NodeId}
    {entries exits : List AdmissionBoundaryPort}
    {key : NodeId × FieldLabel × ContractId}
    (hStep : PrimitiveGraphStep.node node entries exits ∈ primitiveSteps)
    (hKey : key ∈ exits.map AdmissionBoundaryPort.key) :
    key ∈ nodeExitKeysList primitiveSteps := byprimitiveSteps:List PrimitiveGraphStepnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortkey:NodeId × FieldLabel × ContractIdhStep:PrimitiveGraphStep.node node entries exits ∈ primitiveStepshKey:key ∈ List.map AdmissionBoundaryPort.key exits⊢ key ∈ nodeExitKeysList primitiveSteps
  induction primitiveSteps generalizing key with
  | nil =>nilnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortkey:NodeId × FieldLabel × ContractIdhStep:PrimitiveGraphStep.node node entries exits ∈ []hKey:key ∈ List.map AdmissionBoundaryPort.key exits⊢ key ∈ nodeExitKeysList []
      cases hStepAll goals completed! 🐙
  | cons primitiveStep primitiveSteps ih =>consnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveStep:PrimitiveGraphStepprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhStep:PrimitiveGraphStep.node node entries exits ∈ primitiveStep :: primitiveStepshKey:key ∈ List.map AdmissionBoundaryPort.key exits⊢ key ∈ nodeExitKeysList (primitiveStep :: primitiveSteps)
      cases primitiveStep with
      | empty =>cons.emptynode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitshStep:PrimitiveGraphStep.node node entries exits ∈ empty :: primitiveSteps⊢ key ∈ nodeExitKeysList (empty :: primitiveSteps)
          simp only [List.mem_cons] at hStepcons.emptynode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitshStep:PrimitiveGraphStep.node node entries exits = empty ∨ PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeExitKeysList (empty :: primitiveSteps)
          cases hStep with
          | inl hHead =>cons.empty.inlnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitshHead:PrimitiveGraphStep.node node entries exits = empty⊢ key ∈ nodeExitKeysList (empty :: primitiveSteps)
              cases hHeadAll goals completed! 🐙
          | inr hTail =>cons.empty.inrnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitshTail:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeExitKeysList (empty :: primitiveSteps)
              simpa [nodeExitKeysList, nodeExitKeys] using ih hTail hKeyAll goals completed! 🐙
      | node rowNode rowEntries rowExits =>cons.nodenode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsrowNode:NodeIdrowEntries:List AdmissionBoundaryPortrowExits:List AdmissionBoundaryPorthStep:PrimitiveGraphStep.node node entries exits ∈ PrimitiveGraphStep.node rowNode rowEntries rowExits :: primitiveSteps⊢ key ∈ nodeExitKeysList (PrimitiveGraphStep.node rowNode rowEntries rowExits :: primitiveSteps)
          simp only [List.mem_cons] at hStepcons.nodenode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsrowNode:NodeIdrowEntries:List AdmissionBoundaryPortrowExits:List AdmissionBoundaryPorthStep:PrimitiveGraphStep.node node entries exits = PrimitiveGraphStep.node rowNode rowEntries rowExits ∨
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeExitKeysList (PrimitiveGraphStep.node rowNode rowEntries rowExits :: primitiveSteps)
          cases hStep with
          | inl hHead =>cons.node.inlnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsrowNode:NodeIdrowEntries:List AdmissionBoundaryPortrowExits:List AdmissionBoundaryPorthHead:PrimitiveGraphStep.node node entries exits = PrimitiveGraphStep.node rowNode rowEntries rowExits⊢ key ∈ nodeExitKeysList (PrimitiveGraphStep.node rowNode rowEntries rowExits :: primitiveSteps)
              cases hHeadcons.node.inl.reflnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exits⊢ key ∈ nodeExitKeysList (PrimitiveGraphStep.node node entries exits :: primitiveSteps)
              simp [nodeExitKeysList, nodeExitKeys, hKey]All goals completed! 🐙
          | inr hTail =>cons.node.inrnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsrowNode:NodeIdrowEntries:List AdmissionBoundaryPortrowExits:List AdmissionBoundaryPorthTail:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeExitKeysList (PrimitiveGraphStep.node rowNode rowEntries rowExits :: primitiveSteps)
              exact
                List.mem_append.mpr
                  (Or.inr (ih hTail hKey))All goals completed! 🐙
      | bindingRef binding =>cons.bindingRefnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsbinding:BindingNamehStep:PrimitiveGraphStep.node node entries exits ∈ bindingRef binding :: primitiveSteps⊢ key ∈ nodeExitKeysList (bindingRef binding :: primitiveSteps)
          simp only [List.mem_cons] at hStepcons.bindingRefnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsbinding:BindingNamehStep:PrimitiveGraphStep.node node entries exits = bindingRef binding ∨
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeExitKeysList (bindingRef binding :: primitiveSteps)
          cases hStep with
          | inl hHead =>cons.bindingRef.inlnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsbinding:BindingNamehHead:PrimitiveGraphStep.node node entries exits = bindingRef binding⊢ key ∈ nodeExitKeysList (bindingRef binding :: primitiveSteps)
              cases hHeadAll goals completed! 🐙
          | inr hTail =>cons.bindingRef.inrnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsbinding:BindingNamehTail:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeExitKeysList (bindingRef binding :: primitiveSteps)
              simpa [nodeExitKeysList, nodeExitKeys] using ih hTail hKeyAll goals completed! 🐙
      | overlay leftNodes rightNodes leftBindings rightBindings =>cons.overlaynode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehStep:PrimitiveGraphStep.node node entries exits ∈ overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps⊢ key ∈ nodeExitKeysList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps)
          simp only [List.mem_cons] at hStepcons.overlaynode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehStep:PrimitiveGraphStep.node node entries exits = overlay leftNodes rightNodes leftBindings rightBindings ∨
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeExitKeysList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps)
          cases hStep with
          | inl hHead =>cons.overlay.inlnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehHead:PrimitiveGraphStep.node node entries exits = overlay leftNodes rightNodes leftBindings rightBindings⊢ key ∈ nodeExitKeysList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps)
              cases hHeadAll goals completed! 🐙
          | inr hTail =>cons.overlay.inrnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehTail:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈ nodeExitKeysList (overlay leftNodes rightNodes leftBindings rightBindings :: primitiveSteps)
              simpa [nodeExitKeysList, nodeExitKeys] using ih hTail hKeyAll goals completed! 🐙
      | connect leftExits rightEntries matchedPairs unmatchedLeftExits
          unmatchedRightEntries =>cons.connectnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthStep:PrimitiveGraphStep.node node entries exits ∈
  connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps⊢ key ∈
  nodeExitKeysList
    (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps)
          simp only [List.mem_cons] at hStepcons.connectnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthStep:PrimitiveGraphStep.node node entries exits =
    connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries ∨
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈
  nodeExitKeysList
    (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps)
          cases hStep with
          | inl hHead =>cons.connect.inlnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthHead:PrimitiveGraphStep.node node entries exits =
  connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries⊢ key ∈
  nodeExitKeysList
    (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps)
              cases hHeadAll goals completed! 🐙
          | inr hTail =>cons.connect.inrnode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPortprimitiveSteps:List PrimitiveGraphStepih:∀ {key : NodeId × FieldLabel × ContractId},
  PrimitiveGraphStep.node node entries exits ∈ primitiveSteps →
    key ∈ List.map AdmissionBoundaryPort.key exits → key ∈ nodeExitKeysList primitiveStepskey:NodeId × FieldLabel × ContractIdhKey:key ∈ List.map AdmissionBoundaryPort.key exitsleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthTail:PrimitiveGraphStep.node node entries exits ∈ primitiveSteps⊢ key ∈
  nodeExitKeysList
    (connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries :: primitiveSteps)
              simpa [nodeExitKeysList, nodeExitKeys] using ih hTail hKeyAll goals completed! 🐙

end PrimitiveGraphStepnamespace WireAdmissionArtifactnamespace PrimitiveTraceFrame

Frame-Level Linearity Facts

Duplicate-free primitive replay rows after summary matching.

This is the artifact-level frontier-linearity fact: source-visible entry and exit endpoints have unique boundary keys, and the raw connection summary has no duplicate serialized connection rows. It is deliberately phrased over the primitive replay frame rather than over LinearPortObject, because artifact rows do not carry accepted node declarations.

structure SourceVisibleRowsUnique (frame : PrimitiveTraceFrame) : Prop where
  nodesUnique : frame.nodes.Nodup
  bindingRefsUnique : frame.bindingRefs.Nodup
  entriesUnique : (frame.entries.map AdmissionBoundaryPort.key).Nodup
  exitsUnique : (frame.exits.map AdmissionBoundaryPort.key).Nodup
  connectionsUnique : frame.connections.Nodup

A summary-matching frame inherits the artifact's duplicate-free summary rows.

theorem sourceVisibleRowsUnique_of_matchesSummary
    {frame : PrimitiveTraceFrame}
    {artifact : WireAdmissionArtifact}
    (hMatch : frame.MatchesSummary artifact)
    (hUnique : artifact.SummaryKeysUnique) :
    frame.SourceVisibleRowsUnique where
  nodesUnique := byframe:PrimitiveTraceFrameartifact:WireAdmissionArtifacthMatch:frame.MatchesSummary artifacthUnique:artifact.SummaryKeysUnique⊢ frame.nodes.Nodup
    exact
      (matchesSummary_nodes_perm hMatch).nodup_iff.mpr
        hUnique.nodesUniqueAll goals completed! 🐙
  bindingRefsUnique := byframe:PrimitiveTraceFrameartifact:WireAdmissionArtifacthMatch:frame.MatchesSummary artifacthUnique:artifact.SummaryKeysUnique⊢ frame.bindingRefs.Nodup
    exact
      (matchesSummary_bindingRefs_perm hMatch).nodup_iff.mpr
        hUnique.bindingRefsUniqueAll goals completed! 🐙
  entriesUnique := byframe:PrimitiveTraceFrameartifact:WireAdmissionArtifacthMatch:frame.MatchesSummary artifacthUnique:artifact.SummaryKeysUnique⊢ (List.map AdmissionBoundaryPort.key frame.entries).Nodup
    have hPerm :
        (frame.entries.map AdmissionBoundaryPort.key).Perm
          (artifact.entries.map AdmissionBoundaryPort.key) :=
      (matchesSummary_entries_perm hMatch).map AdmissionBoundaryPort.keyframe:PrimitiveTraceFrameartifact:WireAdmissionArtifacthMatch:frame.MatchesSummary artifacthUnique:artifact.SummaryKeysUniquehPerm:(List.map AdmissionBoundaryPort.key frame.entries).Perm (List.map AdmissionBoundaryPort.key artifact.entries)⊢ (List.map AdmissionBoundaryPort.key frame.entries).Nodup
    exact hPerm.nodup_iff.mpr hUnique.entriesUniqueAll goals completed! 🐙
  exitsUnique := byframe:PrimitiveTraceFrameartifact:WireAdmissionArtifacthMatch:frame.MatchesSummary artifacthUnique:artifact.SummaryKeysUnique⊢ (List.map AdmissionBoundaryPort.key frame.exits).Nodup
    have hPerm :
        (frame.exits.map AdmissionBoundaryPort.key).Perm
          (artifact.exits.map AdmissionBoundaryPort.key) :=
      (matchesSummary_exits_perm hMatch).map AdmissionBoundaryPort.keyframe:PrimitiveTraceFrameartifact:WireAdmissionArtifacthMatch:frame.MatchesSummary artifacthUnique:artifact.SummaryKeysUniquehPerm:(List.map AdmissionBoundaryPort.key frame.exits).Perm (List.map AdmissionBoundaryPort.key artifact.exits)⊢ (List.map AdmissionBoundaryPort.key frame.exits).Nodup
    exact hPerm.nodup_iff.mpr hUnique.exitsUniqueAll goals completed! 🐙
  connectionsUnique := byframe:PrimitiveTraceFrameartifact:WireAdmissionArtifacthMatch:frame.MatchesSummary artifacthUnique:artifact.SummaryKeysUnique⊢ frame.connections.Nodup
    exact
      (matchesSummary_connections_perm hMatch).nodup_iff.mpr
        hUnique.connectionsUniqueAll goals completed! 🐙

end PrimitiveTraceFrame

Primitive Node Row Uniqueness

Sound artifacts have duplicate-free primitive node identity rows.

Sound.primitive carries summaryIdentitiesMatchPrimitive and summaryKeysUnique.nodesUnique; together they force the primitive node-row ledger to inherit the top-level summary's Nodup. Reconstruction proofs use this to identify the unique primitive node row for a given NodeId.

theorem PrimitiveSound.primitiveNodeRowsUnique
    {artifact : WireAdmissionArtifact}
    (hPrimitive : artifact.PrimitiveSound) :
    (PrimitiveGraphStep.nodeRowsList artifact.primitiveSteps).Nodup :=
  hPrimitive.summaryIdentitiesMatchPrimitive.left.nodup_iff.mp
    hPrimitive.summaryKeysUnique.nodesUnique

Sound artifacts have at most one primitive node row per NodeId.

theorem PrimitiveSound.primitiveNode_frontiers_unique
    {artifact : WireAdmissionArtifact}
    (hPrimitive : artifact.PrimitiveSound)
    {node : NodeId}
    {entries₁ exits₁ entries₂ exits₂ : List AdmissionBoundaryPort}
    (hLeft :
      PrimitiveGraphStep.node node entries₁ exits₁ ∈ artifact.primitiveSteps)
    (hRight :
      PrimitiveGraphStep.node node entries₂ exits₂ ∈ artifact.primitiveSteps) :
    entries₁ = entries₂ ∧ exits₁ = exits₂ :=
  PrimitiveGraphStep.node_frontiers_eq_of_nodeRowsList_nodup
    hPrimitive.primitiveNodeRowsUnique hLeft hRight

Sound artifacts have at most one primitive node row per NodeId.

theorem Sound.primitiveNode_frontiers_unique
    {artifact : WireAdmissionArtifact}
    (hSound : artifact.Sound)
    {node : NodeId}
    {entries₁ exits₁ entries₂ exits₂ : List AdmissionBoundaryPort}
    (hLeft :
      PrimitiveGraphStep.node node entries₁ exits₁ ∈ artifact.primitiveSteps)
    (hRight :
      PrimitiveGraphStep.node node entries₂ exits₂ ∈ artifact.primitiveSteps) :
    entries₁ = entries₂ ∧ exits₁ = exits₂ :=
  hSound.primitive.primitiveNode_frontiers_unique hLeft hRight

Primitive Frontier Accounting

A primitive input key is accounted for either as a source-visible entry or as an input consumed by a primitive contraction.

inductive PrimitiveInputKeyAccounted
    (artifact : WireAdmissionArtifact)
    (key : NodeId × FieldLabel × ContractId) : Prop where
  | exposed :
      key ∈ artifact.entries.map AdmissionBoundaryPort.key →
        PrimitiveInputKeyAccounted artifact key
  | consumed :
      key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps →
        PrimitiveInputKeyAccounted artifact key

A primitive output key is accounted for as a source-visible exit, as an output consumed by a primitive contraction, or as a select-condition internal choice exit hidden from the source-visible summary.

inductive PrimitiveOutputKeyAccounted
    (artifact : WireAdmissionArtifact)
    (key : NodeId × FieldLabel × ContractId) : Prop where
  | exposed :
      key ∈ artifact.exits.map AdmissionBoundaryPort.key →
        PrimitiveOutputKeyAccounted artifact key
  | consumed :
      key ∈ PrimitiveGraphStep.consumedExitKeysList artifact.primitiveSteps →
        PrimitiveOutputKeyAccounted artifact key
  | selectInternal :
      artifact.SelectInternalExitKey key →
        PrimitiveOutputKeyAccounted artifact key

Every primitive node frontier key has a linear accounting classification.

structure PrimitiveFrontierKeysAccounted
    (artifact : WireAdmissionArtifact) : Prop where
  inputs :
    ∀ {key : NodeId × FieldLabel × ContractId},
      key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps →
        PrimitiveInputKeyAccounted artifact key
  outputs :
    ∀ {key : NodeId × FieldLabel × ContractId},
      key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps →
        PrimitiveOutputKeyAccounted artifact key

Exact residual-frontier coverage classifies every primitive input key.

theorem primitiveInputKey_accounted
    {artifact : WireAdmissionArtifact}
    (hFrontiers : artifact.SummaryFrontiersMatchPrimitive)
    {key : NodeId × FieldLabel × ContractId}
    (hPrimitiveKey :
      key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps) :
    PrimitiveInputKeyAccounted artifact key := byartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps⊢ artifact.PrimitiveInputKeyAccounted key
  by_cases hConsumed :
      key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveStepsposartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveStepshConsumed:key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps⊢ artifact.PrimitiveInputKeyAccounted keynegartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveStepshConsumed:key ∉ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps⊢ artifact.PrimitiveInputKeyAccounted key
  ·posartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveStepshConsumed:key ∈ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps⊢ artifact.PrimitiveInputKeyAccounted key exact PrimitiveInputKeyAccounted.consumed hConsumedAll goals completed! 🐙
  ·negartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveStepshConsumed:key ∉ PrimitiveGraphStep.consumedEntryKeysList artifact.primitiveSteps⊢ artifact.PrimitiveInputKeyAccounted key exact
      PrimitiveInputKeyAccounted.exposed
        ((hFrontiers.left key).mpr ⟨hPrimitiveKey, hConsumed⟩)All goals completed! 🐙

Exact residual-frontier coverage classifies every primitive output key.

theorem primitiveOutputKey_accounted
    {artifact : WireAdmissionArtifact}
    (hFrontiers : artifact.SummaryFrontiersMatchPrimitive)
    {key : NodeId × FieldLabel × ContractId}
    (hPrimitiveKey :
      key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps) :
    PrimitiveOutputKeyAccounted artifact key := byartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps⊢ artifact.PrimitiveOutputKeyAccounted key
  by_cases hConsumed :
      key ∈ PrimitiveGraphStep.consumedExitKeysList artifact.primitiveStepsposartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveStepshConsumed:key ∈ PrimitiveGraphStep.consumedExitKeysList artifact.primitiveSteps⊢ artifact.PrimitiveOutputKeyAccounted keynegartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveStepshConsumed:key ∉ PrimitiveGraphStep.consumedExitKeysList artifact.primitiveSteps⊢ artifact.PrimitiveOutputKeyAccounted key
  ·posartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveStepshConsumed:key ∈ PrimitiveGraphStep.consumedExitKeysList artifact.primitiveSteps⊢ artifact.PrimitiveOutputKeyAccounted key exact PrimitiveOutputKeyAccounted.consumed hConsumedAll goals completed! 🐙
  ·negartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveStepshConsumed:key ∉ PrimitiveGraphStep.consumedExitKeysList artifact.primitiveSteps⊢ artifact.PrimitiveOutputKeyAccounted key by_cases hInternal : artifact.SelectInternalExitKey keyposartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveStepshConsumed:key ∉ PrimitiveGraphStep.consumedExitKeysList artifact.primitiveStepshInternal:artifact.SelectInternalExitKey key⊢ artifact.PrimitiveOutputKeyAccounted keynegartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveStepshConsumed:key ∉ PrimitiveGraphStep.consumedExitKeysList artifact.primitiveStepshInternal:¬artifact.SelectInternalExitKey key⊢ artifact.PrimitiveOutputKeyAccounted key
    ·posartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveStepshConsumed:key ∉ PrimitiveGraphStep.consumedExitKeysList artifact.primitiveStepshInternal:artifact.SelectInternalExitKey key⊢ artifact.PrimitiveOutputKeyAccounted key exact PrimitiveOutputKeyAccounted.selectInternal hInternalAll goals completed! 🐙
    ·negartifact:WireAdmissionArtifacthFrontiers:artifact.SummaryFrontiersMatchPrimitivekey:NodeId × FieldLabel × ContractIdhPrimitiveKey:key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveStepshConsumed:key ∉ PrimitiveGraphStep.consumedExitKeysList artifact.primitiveStepshInternal:¬artifact.SelectInternalExitKey key⊢ artifact.PrimitiveOutputKeyAccounted key exact
        PrimitiveOutputKeyAccounted.exposed
          ((hFrontiers.right key).mpr
            ⟨hPrimitiveKey, hConsumed, hInternal⟩)All goals completed! 🐙

Exact residual-frontier coverage gives the primitive frontier accounting needed by reconstruction.

theorem primitiveFrontierKeysAccounted
    {artifact : WireAdmissionArtifact}
    (hFrontiers : artifact.SummaryFrontiersMatchPrimitive) :
    artifact.PrimitiveFrontierKeysAccounted where
  inputs hPrimitiveKey :=
    primitiveInputKey_accounted hFrontiers hPrimitiveKey
  outputs hPrimitiveKey :=
    primitiveOutputKey_accounted hFrontiers hPrimitiveKey

Reconstruction Contract

Primitive graph evidence reconstructed for one final replay frame.

This is the current artifact-boundary target, not the final GraphElaboration.CertifiedGraph target. The latter additionally needs accepted-node declarations and module binding expansion that are not serialized in primitive artifact rows.

structure PrimitiveGraphReconstructionFrame
    (artifact : WireAdmissionArtifact)
    (finalFrame : PrimitiveTraceFrame) : Prop where
  replay :
    PrimitiveTraceReplays artifact.SelectInternalTraceExit
      artifact.primitiveSteps [] [finalFrame]
  matchesSummary : finalFrame.MatchesSummary artifact
  sourceVisibleRowsUnique : finalFrame.SourceVisibleRowsUnique
  frontierKeysAccounted : artifact.PrimitiveFrontierKeysAccounted
  rawConnectionsMatchPrimitive : artifact.RawConnectionsMatchPrimitive

Primitive graph evidence reconstructed from a sound admission artifact.

def PrimitiveGraphReconstruction
    (artifact : WireAdmissionArtifact) : Prop :=
  ∃ finalFrame, PrimitiveGraphReconstructionFrame artifact finalFrame

Primitive soundness reconstructs the artifact-level primitive graph witness.

theorem PrimitiveSound.toPrimitiveGraphReconstruction
    {artifact : WireAdmissionArtifact}
    (hPrimitive : artifact.PrimitiveSound) :
    artifact.PrimitiveGraphReconstruction := byartifact:WireAdmissionArtifacthPrimitive:artifact.PrimitiveSound⊢ artifact.PrimitiveGraphReconstruction
  obtain ⟨finalFrame, hReplay, hMatch⟩ :=
    hPrimitive.primitiveTraceStackValidartifact:WireAdmissionArtifacthPrimitive:artifact.PrimitiveSoundfinalFrame:PrimitiveTraceFramehReplay:PrimitiveTraceReplays artifact.SelectInternalTraceExit artifact.primitiveSteps [] [finalFrame]hMatch:finalFrame.MatchesSummary artifact⊢ artifact.PrimitiveGraphReconstruction
  exact
    ⟨ finalFrame
    , { replay := hReplay
        matchesSummary := hMatch
        sourceVisibleRowsUnique :=
          PrimitiveTraceFrame.sourceVisibleRowsUnique_of_matchesSummary
            hMatch hPrimitive.summaryKeysUnique
        frontierKeysAccounted :=
          primitiveFrontierKeysAccounted hPrimitive.summaryFrontiersMatchPrimitive
        rawConnectionsMatchPrimitive :=
          hPrimitive.rawConnectionsMatchPrimitive }
    ⟩All goals completed! 🐙

Validator soundness reconstructs the artifact-level primitive graph witness.

theorem Sound.toPrimitiveGraphReconstruction
    {artifact : WireAdmissionArtifact}
    (hSound : artifact.Sound) :
    artifact.PrimitiveGraphReconstruction :=
  hSound.primitive.toPrimitiveGraphReconstruction

end WireAdmissionArtifactend AdmissionArtifactend Cortex.Wire

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

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