Cortex.Wire.AdmissionArtifact.GeneratedReconstruction

On this page
  1. Overview
  2. Generated Reconstruction Contract
Imports
import Cortex.Wire.AdmissionArtifact.PrimitiveReconstruction

Overview

Generated-form reconstruction from validator-sound admission artifacts.

The generated artifact rows record source make/makeEach children, surviving lowered children, and primitive frontier rows for those surviving children. They do not carry the accepted kind declaration or the executable kind-substitution result, so this module does not claim to reconstruct KindInstantiatedFrontiers or MakeWitness directly.

Instead, GeneratedReconstruction is the artifact-boundary witness:

  • source MakeItem rows pass the Lean makeEach item checker;
  • every surviving generated child has a unique source row and projected MakeItem;
  • every surviving child frontier exactly matches a primitive node row;
  • every surviving child frontier key is accounted for by primitive replay; and
  • make rows expose canonical count labels and value-free items, while all source rows preserve decoded static payloads through toStaticValue.

The later accepted-kind reconstruction step must add the accepted kind and substitution evidence needed to build KindInstantiatedFrontiers.

namespace Cortex.Wirenamespace AdmissionArtifactopen Cortex.Wire.ElaborationIRnamespace WireAdmissionArtifact

Generated Reconstruction Contract

Evidence for one surviving generated child row.

The data arguments are parameters so the public reconstruction predicate can remain Prop while still naming the source row, projected MakeItem, and primitive frontier row that witness the child.

structure GeneratedUsedChildReconstructionEvidence (artifact : WireAdmissionArtifact) (generated : GeneratedFormArtifact) (child : GeneratedChildArtifact) (item : LinearPortGraph.MakeItem) (source : GeneratedChildSourceArtifact) (entries exits : List AdmissionBoundaryPort) : Prop where itemMem : item ∈ generated.sourceMakeItems itemLabel : item.label = child.label itemUnique : ∀ other, other ∈ generated.sourceMakeItems → other.label = child.label → other = item sourceMem : source ∈ generated.sourceChildren sourceNode : source.node = child.node sourceLabel : source.label = child.label

The source row backing the child is unique among sourceChildren.

Derived from GeneratedFormArtifact.Valid.childKeysUnique's sourceChildKeys.Nodup plus the (node, label) matching above. Exposed at the reconstruction boundary so downstream proofs don't have to re-derive it from the underlying validity contract.

sourceUnique : ∀ other, other ∈ generated.sourceChildren → other.node = child.node → other.label = child.label → other = source itemFromSource : item = source.toMakeItem primitiveNode : PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveSteps inputKeysMatchPrimitive : child.inputKeys.Perm (entries.map AdmissionBoundaryPort.key) outputKeysMatchPrimitive : child.outputKeys.Perm (exits.map AdmissionBoundaryPort.key) inputKeysAccounted : ∀ {key : NodeId × FieldLabel × ContractId}, key ∈ child.inputKeys → PrimitiveInputKeyAccounted artifact key outputKeysAccounted : ∀ {key : NodeId × FieldLabel × ContractId}, key ∈ child.outputKeys → PrimitiveOutputKeyAccounted artifact key

Artifact-boundary reconstruction evidence for one surviving generated child.

def GeneratedUsedChildReconstruction (artifact : WireAdmissionArtifact) (generated : GeneratedFormArtifact) (child : GeneratedChildArtifact) : Prop := ∃ item source entries exits, GeneratedUsedChildReconstructionEvidence artifact generated child item source entries exits

Artifact-boundary reconstruction evidence for one generated-form row.

structure GeneratedFormReconstruction (artifact : WireAdmissionArtifact) (generated : GeneratedFormArtifact) : Prop where sourceItemsAccepted : LinearPortGraph.MakeEach.acceptItems generated.binding generated.sourceMakeItems = Except.ok generated.sourceMakeItems usedChildren : ∀ child, child ∈ generated.usedChildren → GeneratedUsedChildReconstruction artifact generated child sourceValuesProjected : generated.sourceMakeItems.map LinearPortGraph.MakeItem.value = generated.sourceChildren.map (fun child => child.value.map AdmissionStaticValue.toStaticValue) makePayload : generated.kind = GeneratedFormKind.make → generated.sourceMakeItems.map LinearPortGraph.MakeItem.label = (List.range generated.sourceChildren.length).map (fun index => ⟨toString index⟩) ∧ ∀ {item : LinearPortGraph.MakeItem}, item ∈ generated.sourceMakeItems → item.value = none

Artifact-boundary generated-form reconstruction for every generated row.

def GeneratedReconstruction (artifact : WireAdmissionArtifact) : Prop := ∀ generated, generated ∈ artifact.generatedForms → GeneratedFormReconstruction artifact generated

Generated and primitive soundness reconstruct one surviving generated child row.

theorem Sound.generatedUsedChildReconstruction {artifact : WireAdmissionArtifact} (hSound : artifact.Sound) {generated : GeneratedFormArtifact} (hGenerated : generated ∈ artifact.generatedForms) {child : GeneratedChildArtifact} (hChild : child ∈ generated.usedChildren) : GeneratedUsedChildReconstruction artifact generated child := artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ artifact.GeneratedUsedChildReconstruction generated child artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labelhSource:∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label ∧ item = source.toMakeItem⊢ artifact.GeneratedUsedChildReconstruction generated child artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labelhSource:∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label ∧ item = source.toMakeItemuniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItem⊢ artifact.GeneratedUsedChildReconstruction generated child artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labelhSource:∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label ∧ item = source.toMakeItemuniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItem⊢ artifact.GeneratedUsedChildReconstruction generated child have hItemUnique : ∀ other, other ∈ generated.sourceMakeItems → other.label = child.label → other = item := artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ artifact.GeneratedUsedChildReconstruction generated child intro other artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labelhSource:∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label ∧ item = source.toMakeItemuniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemother:LinearPortGraph.MakeItemhOtherMem:other ∈ generated.sourceMakeItems⊢ other.label = child.label → other = item artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labelhSource:∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label ∧ item = source.toMakeItemuniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemother:LinearPortGraph.MakeItemhOtherMem:other ∈ generated.sourceMakeItemshOtherLabel:other.label = child.label⊢ other = item All goals completed! 🐙 artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItem⊢ artifact.GeneratedUsedChildReconstruction generated child artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)⊢ artifact.GeneratedUsedChildReconstruction generated child artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)hFrontierAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ artifact.GeneratedUsedChildReconstruction generated child artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)hFrontierAccounted:artifact.PrimitiveFrontierKeysAccounted⊢ artifact.GeneratedUsedChildReconstructionEvidence generated child item source entries exits artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)hFrontierAccounted:artifact.PrimitiveFrontierKeysAccountedhSourceChildKeysUnique:generated.sourceChildKeys.Nodup⊢ artifact.GeneratedUsedChildReconstructionEvidence generated child item source entries exits have hSourceUnique : ∀ other, other ∈ generated.sourceChildren → other.node = child.node → other.label = child.label → other = source := artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ artifact.GeneratedUsedChildReconstruction generated child intro other artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)hFrontierAccounted:artifact.PrimitiveFrontierKeysAccountedhSourceChildKeysUnique:generated.sourceChildKeys.Nodupother:GeneratedChildSourceArtifacthOther:other ∈ generated.sourceChildren⊢ other.node = child.node → other.label = child.label → other = source artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)hFrontierAccounted:artifact.PrimitiveFrontierKeysAccountedhSourceChildKeysUnique:generated.sourceChildKeys.Nodupother:GeneratedChildSourceArtifacthOther:other ∈ generated.sourceChildrenhOtherNode:other.node = child.node⊢ other.label = child.label → other = source artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)hFrontierAccounted:artifact.PrimitiveFrontierKeysAccountedhSourceChildKeysUnique:generated.sourceChildKeys.Nodupother:GeneratedChildSourceArtifacthOther:other ∈ generated.sourceChildrenhOtherNode:other.node = child.nodehOtherLabel:other.label = child.label⊢ other = source have hKeyEq : other.key = source.key := artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ artifact.GeneratedUsedChildReconstruction generated child artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)hFrontierAccounted:artifact.PrimitiveFrontierKeysAccountedhSourceChildKeysUnique:generated.sourceChildKeys.Nodupother:GeneratedChildSourceArtifacthOther:other ∈ generated.sourceChildrenhOtherNode:other.node = child.nodehOtherLabel:other.label = child.label⊢ (other.node, other.label) = (source.node, source.label) All goals completed! 🐙 All goals completed! 🐙 exact { itemMem := hItemMem itemLabel := hItemLabel itemUnique := hItemUnique sourceMem := hSourceMem sourceNode := hSourceNode sourceLabel := hSourceLabel sourceUnique := hSourceUnique itemFromSource := hItemFromSource primitiveNode := hPrimitiveNode inputKeysMatchPrimitive := hInputKeys outputKeysMatchPrimitive := hOutputKeys inputKeysAccounted := artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)hFrontierAccounted:artifact.PrimitiveFrontierKeysAccountedhSourceChildKeysUnique:generated.sourceChildKeys.NoduphSourceUnique:∀ other ∈ generated.sourceChildren, other.node = child.node → other.label = child.label → other = source⊢ ∀ {key : NodeId × FieldLabel × ContractId}, key ∈ child.inputKeys → artifact.PrimitiveInputKeyAccounted key intro key artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)hFrontierAccounted:artifact.PrimitiveFrontierKeysAccountedhSourceChildKeysUnique:generated.sourceChildKeys.NoduphSourceUnique:∀ other ∈ generated.sourceChildren, other.node = child.node → other.label = child.label → other = sourcekey:NodeId × FieldLabel × ContractIdhKey:key ∈ child.inputKeys⊢ artifact.PrimitiveInputKeyAccounted key artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)hFrontierAccounted:artifact.PrimitiveFrontierKeysAccountedhSourceChildKeysUnique:generated.sourceChildKeys.NoduphSourceUnique:∀ other ∈ generated.sourceChildren, other.node = child.node → other.label = child.label → other = sourcekey:NodeId × FieldLabel × ContractIdhKey:key ∈ child.inputKeyshPrimitiveKey:key ∈ PrimitiveGraphStep.nodeEntryKeysList artifact.primitiveSteps⊢ artifact.PrimitiveInputKeyAccounted key All goals completed! 🐙 outputKeysAccounted := artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)hFrontierAccounted:artifact.PrimitiveFrontierKeysAccountedhSourceChildKeysUnique:generated.sourceChildKeys.NoduphSourceUnique:∀ other ∈ generated.sourceChildren, other.node = child.node → other.label = child.label → other = source⊢ ∀ {key : NodeId × FieldLabel × ContractId}, key ∈ child.outputKeys → artifact.PrimitiveOutputKeyAccounted key intro key artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)hFrontierAccounted:artifact.PrimitiveFrontierKeysAccountedhSourceChildKeysUnique:generated.sourceChildKeys.NoduphSourceUnique:∀ other ∈ generated.sourceChildren, other.node = child.node → other.label = child.label → other = sourcekey:NodeId × FieldLabel × ContractIdhKey:key ∈ child.outputKeys⊢ artifact.PrimitiveOutputKeyAccounted key artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItemMem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.labeluniqueItem:LinearPortGraph.MakeItemhUniqueItemMem:uniqueItem ∈ generated.sourceMakeItemshUniqueItemLabel:uniqueItem.label = child.labelhUniqueItem:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = uniqueItemhItemEqUnique:item = uniqueItemhItemUnique:∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = itemsource:GeneratedChildSourceArtifacthSourceMem:source ∈ generated.sourceChildrenhSourceNode:source.node = child.nodehSourceLabel:source.label = child.labelhItemFromSource:item = source.toMakeItementries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthPrimitiveNode:PrimitiveGraphStep.node child.node entries exits ∈ artifact.primitiveStepshInputKeys:child.inputKeys.Perm (List.map AdmissionBoundaryPort.key entries)hOutputKeys:child.outputKeys.Perm (List.map AdmissionBoundaryPort.key exits)hFrontierAccounted:artifact.PrimitiveFrontierKeysAccountedhSourceChildKeysUnique:generated.sourceChildKeys.NoduphSourceUnique:∀ other ∈ generated.sourceChildren, other.node = child.node → other.label = child.label → other = sourcekey:NodeId × FieldLabel × ContractIdhKey:key ∈ child.outputKeyshPrimitiveKey:key ∈ PrimitiveGraphStep.nodeExitKeysList artifact.primitiveSteps⊢ artifact.PrimitiveOutputKeyAccounted key All goals completed! 🐙 }

Validator soundness reconstructs generated-form artifact-boundary witnesses.

theorem Sound.toGeneratedReconstruction {artifact : WireAdmissionArtifact} (hSound : artifact.Sound) : artifact.GeneratedReconstruction := artifact:WireAdmissionArtifacthSound:artifact.Sound⊢ artifact.GeneratedReconstruction intro generated artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedForms⊢ artifact.GeneratedFormReconstruction generated exact { sourceItemsAccepted := hSound.generated.sourceMakeItemsAcceptItems hGenerated usedChildren := artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedForms⊢ ∀ child ∈ generated.usedChildren, artifact.GeneratedUsedChildReconstruction generated child intro child artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ artifact.GeneratedUsedChildReconstruction generated child All goals completed! 🐙 sourceValuesProjected := GeneratedFormArtifact.sourceMakeItems_values generated makePayload := artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedForms⊢ generated.kind = GeneratedFormKind.make → List.map LinearPortGraph.MakeItem.label generated.sourceMakeItems = List.map (fun index => { name := toString index }) (List.range generated.sourceChildren.length) ∧ ∀ {item : LinearPortGraph.MakeItem}, item ∈ generated.sourceMakeItems → item.value = none artifact:WireAdmissionArtifacthSound:artifact.Soundgenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.make⊢ List.map LinearPortGraph.MakeItem.label generated.sourceMakeItems = List.map (fun index => { name := toString index }) (List.range generated.sourceChildren.length) ∧ ∀ {item : LinearPortGraph.MakeItem}, item ∈ generated.sourceMakeItems → item.value = none All goals completed! 🐙 }end WireAdmissionArtifactend AdmissionArtifactend Cortex.Wire