Theory /Cortex /Wire /AdmissionArtifact /ReadyGenerated

Cortex.Wire.AdmissionArtifact.ReadyGenerated

proofs

On this page

Overview

Imports

import Cortex.Wire.AdmissionArtifact.ReadyPrimitive

Overview

Validator-ready generated-form accessors.

This page exposes source-child, used-child, make, makeEach, and static-record consequences for generated form rows in a validator-ready artifact.

namespace Cortex.Wirenamespace AdmissionArtifactopen Cortex.Wire.ElaborationIRnamespace WireAdmissionArtifact

Validator-ready generated rows expose exact used-child backing.

theorem validatorReady_generated_usedChild_backed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    child.key ∈ generated.sourceChildKeys :=
  (validatorReady_generatedForm_valid hReady hGenerated).usedChildrenFromSource child hChild

Validator-ready generated rows recover the source row for every surviving child.

theorem validatorReady_generated_usedChild_sourceChild
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    ∃ source, source ∈ generated.sourceChildren ∧
      source.node = child.node ∧ source.label = child.label := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ ∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label
  have hBacked :=
    validatorReady_generated_usedChild_backed hReady hGenerated hChildartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenhBacked:child.key ∈ generated.sourceChildKeys⊢ ∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label
  rcases List.mem_map.mp hBacked with ⟨source, hSource, hKey⟩artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenhBacked:child.key ∈ generated.sourceChildKeyssource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhKey:source.key = child.key⊢ ∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label
  have hNode : source.node = child.node := Prod.mk.inj hKey |>.leftartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenhBacked:child.key ∈ generated.sourceChildKeyssource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhKey:source.key = child.keyhNode:source.node = child.node⊢ ∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label
  have hLabel : source.label = child.label := Prod.mk.inj hKey |>.rightartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenhBacked:child.key ∈ generated.sourceChildKeyssource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhKey:source.key = child.keyhNode:source.node = child.nodehLabel:source.label = child.label⊢ ∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label
  exact ⟨source, hSource, hNode, hLabel⟩All goals completed! 🐙

Validator-ready generated rows recover a unique source row for every surviving child.

This is the source-row provenance handoff needed by future executable makeEach correspondence: once the used generated child is known, the serialized source row, including any static payload, is unique.

theorem validatorReady_generated_usedChild_uniqueSourceChild
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    ∃ source, source ∈ generated.sourceChildren ∧
      source.node = child.node ∧
        source.label = child.label ∧
          ∀ other, other ∈ generated.sourceChildren →
            other.node = child.node →
              other.label = child.label →
                other = source := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ ∃ source ∈ generated.sourceChildren,
  source.node = child.node ∧
    source.label = child.label ∧
      ∀ other ∈ generated.sourceChildren, other.node = child.node → other.label = child.label → other = source
  obtain ⟨source, hSource, hNode, hLabel⟩ :=
    validatorReady_generated_usedChild_sourceChild hReady hGenerated hChildartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhNode:source.node = child.nodehLabel:source.label = child.label⊢ ∃ source ∈ generated.sourceChildren,
  source.node = child.node ∧
    source.label = child.label ∧
      ∀ other ∈ generated.sourceChildren, other.node = child.node → other.label = child.label → other = source
  have hSourceKeysUnique :=
    (validatorReady_generatedForm_valid hReady hGenerated).childKeysUnique.leftartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhNode:source.node = child.nodehLabel:source.label = child.labelhSourceKeysUnique:generated.sourceChildKeys.Nodup⊢ ∃ source ∈ generated.sourceChildren,
  source.node = child.node ∧
    source.label = child.label ∧
      ∀ other ∈ generated.sourceChildren, other.node = child.node → other.label = child.label → other = source
  have hUnique :
      ∀ other, other ∈ generated.sourceChildren →
        other.node = child.node →
          other.label = child.label →
            other = source := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ ∃ source ∈ generated.sourceChildren,
  source.node = child.node ∧
    source.label = child.label ∧
      ∀ other ∈ generated.sourceChildren, other.node = child.node → other.label = child.label → other = source
    intro other hOtherartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhNode:source.node = child.nodehLabel:source.label = child.labelhSourceKeysUnique:generated.sourceChildKeys.Nodupother:GeneratedChildSourceArtifacthOther:other ∈ generated.sourceChildren⊢ other.node = child.node → other.label = child.label → other = source hOtherNodeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhNode:source.node = child.nodehLabel:source.label = child.labelhSourceKeysUnique:generated.sourceChildKeys.Nodupother:GeneratedChildSourceArtifacthOther:other ∈ generated.sourceChildrenhOtherNode:other.node = child.node⊢ other.label = child.label → other = source hOtherLabelartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhNode:source.node = child.nodehLabel:source.label = child.labelhSourceKeysUnique:generated.sourceChildKeys.Nodupother:GeneratedChildSourceArtifacthOther:other ∈ generated.sourceChildrenhOtherNode:other.node = child.nodehOtherLabel:other.label = child.label⊢ other = source
    have hKeyEq : other.key = source.key := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ ∃ source ∈ generated.sourceChildren,
  source.node = child.node ∧
    source.label = child.label ∧
      ∀ other ∈ generated.sourceChildren, other.node = child.node → other.label = child.label → other = source
      unfold GeneratedChildSourceArtifact.keyartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhNode:source.node = child.nodehLabel:source.label = child.labelhSourceKeysUnique:generated.sourceChildKeys.Nodupother:GeneratedChildSourceArtifacthOther:other ∈ generated.sourceChildrenhOtherNode:other.node = child.nodehOtherLabel:other.label = child.label⊢ (other.node, other.label) = (source.node, source.label)
      exact Prod.ext (hOtherNode.trans hNode.symm) (hOtherLabel.trans hLabel.symm)All goals completed! 🐙
    exact
      List.inj_on_of_nodup_map hSourceKeysUnique hOther hSource hKeyEqAll goals completed! 🐙
  exact ⟨source, hSource, hNode, hLabel, hUnique⟩All goals completed! 🐙

Validator-ready generated children recover their projected source MakeItem.

This connects the lowered child row that survived graph pruning back to the exact source item list consumed by the Lean makeEach checker, including any static payload carried by the decoded source row.

theorem validatorReady_generated_usedChild_sourceMakeItem
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    ∃ item, item ∈ generated.sourceMakeItems ∧
      item.label = child.label ∧
        ∃ source, source ∈ generated.sourceChildren ∧
          source.node = child.node ∧
            source.label = child.label ∧
              item = source.toMakeItem := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ ∃ item ∈ generated.sourceMakeItems,
  item.label = child.label ∧
    ∃ source ∈ generated.sourceChildren,
      source.node = child.node ∧ source.label = child.label ∧ item = source.toMakeItem
  obtain ⟨source, hSource, hNode, hLabel⟩ :=
    validatorReady_generated_usedChild_sourceChild hReady hGenerated hChildartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhNode:source.node = child.nodehLabel:source.label = child.label⊢ ∃ item ∈ generated.sourceMakeItems,
  item.label = child.label ∧
    ∃ source ∈ generated.sourceChildren,
      source.node = child.node ∧ source.label = child.label ∧ item = source.toMakeItem
  refine
    ⟨ source.toMakeItem
    , ?_
    , ?_
    , ⟨source, hSource, hNode, hLabel, rfl⟩
    ⟩refine_1artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhNode:source.node = child.nodehLabel:source.label = child.label⊢ source.toMakeItem ∈ generated.sourceMakeItemsrefine_2artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhNode:source.node = child.nodehLabel:source.label = child.label⊢ source.toMakeItem.label = child.label
  ·refine_1artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhNode:source.node = child.nodehLabel:source.label = child.label⊢ source.toMakeItem ∈ generated.sourceMakeItems unfold GeneratedFormArtifact.sourceMakeItemsrefine_1artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhNode:source.node = child.nodehLabel:source.label = child.label⊢ source.toMakeItem ∈ List.map GeneratedChildSourceArtifact.toMakeItem generated.sourceChildren
    exact List.mem_map.mpr ⟨source, hSource, rfl⟩All goals completed! 🐙
  ·refine_2artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenhNode:source.node = child.nodehLabel:source.label = child.label⊢ source.toMakeItem.label = child.label simp [GeneratedChildSourceArtifact.toMakeItem, hLabel]All goals completed! 🐙

Validator-ready make children recover source items with no static payload.

theorem validatorReady_generated_make_usedChild_sourceMakeItem_value_empty
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    (hKind : generated.kind = GeneratedFormKind.make)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    ∃ item, item ∈ generated.sourceMakeItems ∧
      item.label = child.label ∧ item.value = none := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makechild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ ∃ item ∈ generated.sourceMakeItems, item.label = child.label ∧ item.value = none
  obtain ⟨source, hSource, _hNode, hLabel⟩ :=
    validatorReady_generated_usedChild_sourceChild hReady hGenerated hChildartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makechild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildren_hNode:source.node = child.nodehLabel:source.label = child.label⊢ ∃ item ∈ generated.sourceMakeItems, item.label = child.label ∧ item.value = none
  have hShape :=
    (validatorReady_generatedForm_valid hReady hGenerated).kindShapeMatchesartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makechild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildren_hNode:source.node = child.nodehLabel:source.label = child.labelhShape:generated.KindShapeMatches⊢ ∃ item ∈ generated.sourceMakeItems, item.label = child.label ∧ item.value = none
  unfold GeneratedFormArtifact.KindShapeMatches at hShapeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makechild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildren_hNode:source.node = child.nodehLabel:source.label = child.labelhShape:match generated.kind with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => True⊢ ∃ item ∈ generated.sourceMakeItems, item.label = child.label ∧ item.value = none
  rw [hKind] at hShapeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makechild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildren_hNode:source.node = child.nodehLabel:source.label = child.labelhShape:match GeneratedFormKind.make with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => True⊢ ∃ item ∈ generated.sourceMakeItems, item.label = child.label ∧ item.value = none
  have hValueEmpty := hShape.right source hSourceartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makechild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildren_hNode:source.node = child.nodehLabel:source.label = child.labelhShape:match GeneratedFormKind.make with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => TruehValueEmpty:source.value = none⊢ ∃ item ∈ generated.sourceMakeItems, item.label = child.label ∧ item.value = none
  refine
    ⟨ source.toMakeItem
    , ?_
    , ?_
    , ?_
    ⟩refine_1artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makechild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildren_hNode:source.node = child.nodehLabel:source.label = child.labelhShape:match GeneratedFormKind.make with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => TruehValueEmpty:source.value = none⊢ source.toMakeItem ∈ generated.sourceMakeItemsrefine_2artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makechild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildren_hNode:source.node = child.nodehLabel:source.label = child.labelhShape:match GeneratedFormKind.make with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => TruehValueEmpty:source.value = none⊢ source.toMakeItem.label = child.labelrefine_3artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makechild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildren_hNode:source.node = child.nodehLabel:source.label = child.labelhShape:match GeneratedFormKind.make with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => TruehValueEmpty:source.value = none⊢ source.toMakeItem.value = none
  ·refine_1artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makechild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildren_hNode:source.node = child.nodehLabel:source.label = child.labelhShape:match GeneratedFormKind.make with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => TruehValueEmpty:source.value = none⊢ source.toMakeItem ∈ generated.sourceMakeItems unfold GeneratedFormArtifact.sourceMakeItemsrefine_1artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makechild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildren_hNode:source.node = child.nodehLabel:source.label = child.labelhShape:match GeneratedFormKind.make with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => TruehValueEmpty:source.value = none⊢ source.toMakeItem ∈ List.map GeneratedChildSourceArtifact.toMakeItem generated.sourceChildren
    exact List.mem_map.mpr ⟨source, hSource, rfl⟩All goals completed! 🐙
  ·refine_2artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makechild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildren_hNode:source.node = child.nodehLabel:source.label = child.labelhShape:match GeneratedFormKind.make with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => TruehValueEmpty:source.value = none⊢ source.toMakeItem.label = child.label simp [GeneratedChildSourceArtifact.toMakeItem, hLabel]All goals completed! 🐙
  ·refine_3artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makechild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrensource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildren_hNode:source.node = child.nodehLabel:source.label = child.labelhShape:match GeneratedFormKind.make with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => TruehValueEmpty:source.value = none⊢ source.toMakeItem.value = none simp [GeneratedChildSourceArtifact.toMakeItem, hValueEmpty]All goals completed! 🐙

Validator-ready generated rows expose source-label backing for used children.

theorem validatorReady_generated_usedChild_label_mem
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    child.label ∈ generated.sourceLabels :=
  GeneratedFormArtifact.usedChildrenFromSource_label_mem
    (validatorReady_generatedForm_valid hReady hGenerated).usedChildrenFromSource
    hChild

Validator-ready generated rows expose source/used child-key uniqueness.

theorem validatorReady_generated_childKeysUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms) :
    generated.ChildKeysUnique :=
  (validatorReady_generatedForm_valid hReady hGenerated).childKeysUnique

Validator-ready generated rows expose binding/label ownership for child node identities.

theorem validatorReady_generated_childrenOwnedByBinding
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms) :
    generated.ChildrenOwnedByBinding :=
  (validatorReady_generatedForm_valid hReady hGenerated).childrenOwnedByBinding

Validator-ready generated rows expose structural validity of source static payloads.

theorem validatorReady_generated_sourceValuesValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms) :
    generated.SourceValuesValid :=
  (validatorReady_generatedForm_valid hReady hGenerated).sourceValuesValid

Validator-ready generated source rows project to valid Lean makeEach items.

theorem validatorReady_generated_sourceMakeItems_valid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms) :
    LinearPortGraph.MakeItem.ItemsValid generated.sourceMakeItems := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedForms⊢ LinearPortGraph.MakeItem.ItemsValid generated.sourceMakeItems
  have hRows : generated.RowsValid :=
    (validatorReady_generatedForm_valid hReady hGenerated).rowsValidartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshRows:generated.RowsValid⊢ LinearPortGraph.MakeItem.ItemsValid generated.sourceMakeItems
  exact
    GeneratedFormArtifact.sourceMakeItems_valid fun child hChild =>
      (hRows.sourceChildrenValid child hChild).labelValidAll goals completed! 🐙

Validator-ready generated source rows project to duplicate-free Lean makeEach item labels.

theorem validatorReady_generated_sourceMakeItems_labelsUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms) :
    LinearPortGraph.MakeItem.LabelsUnique generated.sourceMakeItems :=
  GeneratedFormArtifact.sourceMakeItems_labelsUnique
    (validatorReady_generated_childrenOwnedByBinding hReady hGenerated)
    (validatorReady_generated_childKeysUnique hReady hGenerated)

Validator-ready used children recover a unique projected source MakeItem.

theorem validatorReady_generated_usedChild_uniqueSourceMakeItem
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    ∃ item, item ∈ generated.sourceMakeItems ∧
      item.label = child.label ∧
        ∀ other, other ∈ generated.sourceMakeItems →
          other.label = child.label → other = item := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ ∃ item ∈ generated.sourceMakeItems,
  item.label = child.label ∧ ∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = item
  obtain ⟨item, hItem, hItemLabel, _source⟩ :=
    validatorReady_generated_usedChild_sourceMakeItem hReady hGenerated hChildartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.label_source:∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label ∧ item = source.toMakeItem⊢ ∃ item ∈ generated.sourceMakeItems,
  item.label = child.label ∧ ∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = item
  have hLabelsUnique :=
    validatorReady_generated_sourceMakeItems_labelsUnique hReady hGeneratedartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.label_source:∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label ∧ item = source.toMakeItemhLabelsUnique:LinearPortGraph.MakeItem.LabelsUnique generated.sourceMakeItems⊢ ∃ item ∈ generated.sourceMakeItems,
  item.label = child.label ∧ ∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = item
  have hUnique :
      ∀ other, other ∈ generated.sourceMakeItems →
        other.label = child.label → other = item := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildren⊢ ∃ item ∈ generated.sourceMakeItems,
  item.label = child.label ∧ ∀ other ∈ generated.sourceMakeItems, other.label = child.label → other = item
    intro other hOtherartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.label_source:∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label ∧ item = source.toMakeItemhLabelsUnique:LinearPortGraph.MakeItem.LabelsUnique generated.sourceMakeItemsother:LinearPortGraph.MakeItemhOther:other ∈ generated.sourceMakeItems⊢ other.label = child.label → other = item hOtherLabelartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormschild:GeneratedChildArtifacthChild:child ∈ generated.usedChildrenitem:LinearPortGraph.MakeItemhItem:item ∈ generated.sourceMakeItemshItemLabel:item.label = child.label_source:∃ source ∈ generated.sourceChildren, source.node = child.node ∧ source.label = child.label ∧ item = source.toMakeItemhLabelsUnique:LinearPortGraph.MakeItem.LabelsUnique generated.sourceMakeItemsother:LinearPortGraph.MakeItemhOther:other ∈ generated.sourceMakeItemshOtherLabel:other.label = child.label⊢ other = item
    exact
      List.inj_on_of_nodup_map
        hLabelsUnique
        hOther
        hItem
        (hOtherLabel.trans hItemLabel.symm)All goals completed! 🐙
  exact ⟨item, hItem, hItemLabel, hUnique⟩All goals completed! 🐙

Validator-ready generated source rows pass the generated-form makeEach item checker.

theorem validatorReady_generated_sourceMakeItems_acceptItems_ok
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms) :
    LinearPortGraph.MakeEach.acceptItems generated.binding generated.sourceMakeItems =
      Except.ok generated.sourceMakeItems :=
  LinearPortGraph.MakeEach.acceptItems_ok_eq_self
    generated.binding
    generated.sourceMakeItems
    (validatorReady_generated_sourceMakeItems_valid hReady hGenerated)
    (validatorReady_generated_sourceMakeItems_labelsUnique hReady hGenerated)

Validator-ready generated rows expose generated-form kind payload-shape matching.

theorem validatorReady_generated_kindShapeMatches
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms) :
    generated.KindShapeMatches :=
  (validatorReady_generatedForm_valid hReady hGenerated).kindShapeMatches

Validator-ready make rows expose count-derived source labels.

theorem validatorReady_generated_makeSourceLabelsCanonical
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    (hKind : generated.kind = GeneratedFormKind.make) :
    generated.MakeSourceLabelsCanonical := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.make⊢ generated.MakeSourceLabelsCanonical
  have hShape := validatorReady_generated_kindShapeMatches hReady hGeneratedartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makehShape:generated.KindShapeMatches⊢ generated.MakeSourceLabelsCanonical
  unfold GeneratedFormArtifact.KindShapeMatches at hShapeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makehShape:match generated.kind with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => True⊢ generated.MakeSourceLabelsCanonical
  rw [hKind] at hShapeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makehShape:match GeneratedFormKind.make with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => True⊢ generated.MakeSourceLabelsCanonical
  exact hShape.leftAll goals completed! 🐙

Validator-ready make rows carry no per-child static value payload.

theorem validatorReady_generated_makeSourceValuesEmpty
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    (hKind : generated.kind = GeneratedFormKind.make) :
    generated.MakeSourceValuesEmpty := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.make⊢ generated.MakeSourceValuesEmpty
  have hShape := validatorReady_generated_kindShapeMatches hReady hGeneratedartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makehShape:generated.KindShapeMatches⊢ generated.MakeSourceValuesEmpty
  unfold GeneratedFormArtifact.KindShapeMatches at hShapeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makehShape:match generated.kind with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => True⊢ generated.MakeSourceValuesEmpty
  rw [hKind] at hShapeartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makehShape:match GeneratedFormKind.make with
| GeneratedFormKind.make => generated.MakeSourceLabelsCanonical ∧ generated.MakeSourceValuesEmpty
| GeneratedFormKind.makeEach => True⊢ generated.MakeSourceValuesEmpty
  exact hShape.rightAll goals completed! 🐙

Validator-ready make source rows project to the canonical generated label sequence.

theorem validatorReady_generated_make_sourceMakeItems_labelsCanonical
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    (hKind : generated.kind = GeneratedFormKind.make) :
    generated.sourceMakeItems.map LinearPortGraph.MakeItem.label =
      (List.range generated.sourceChildren.length).map (fun index => ⟨toString index⟩) := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated: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)
  rw [GeneratedFormArtifact.sourceMakeItems_labels]artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.make⊢ List.map GeneratedChildSourceArtifact.label generated.sourceChildren =
  List.map (fun index => { name := toString index }) (List.range generated.sourceChildren.length)
  exact validatorReady_generated_makeSourceLabelsCanonical hReady hGenerated hKindAll goals completed! 🐙

Validator-ready make source rows project to value-free generated items.

theorem validatorReady_generated_make_sourceMakeItems_valuesEmpty
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    (hKind : generated.kind = GeneratedFormKind.make)
    {item : LinearPortGraph.MakeItem}
    (hItem : item ∈ generated.sourceMakeItems) :
    item.value = none := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makeitem:LinearPortGraph.MakeItemhItem:item ∈ generated.sourceMakeItems⊢ item.value = none
  unfold GeneratedFormArtifact.sourceMakeItems at hItemartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makeitem:LinearPortGraph.MakeItemhItem:item ∈ List.map GeneratedChildSourceArtifact.toMakeItem generated.sourceChildren⊢ item.value = none
  rcases List.mem_map.mp hItem with ⟨child, hChild, hItemEq⟩artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makeitem:LinearPortGraph.MakeItemhItem:item ∈ List.map GeneratedChildSourceArtifact.toMakeItem generated.sourceChildrenchild:GeneratedChildSourceArtifacthChild:child ∈ generated.sourceChildrenhItemEq:child.toMakeItem = item⊢ item.value = none
  rw [← hItemEq]artifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormshKind:generated.kind = GeneratedFormKind.makeitem:LinearPortGraph.MakeItemhItem:item ∈ List.map GeneratedChildSourceArtifact.toMakeItem generated.sourceChildrenchild:GeneratedChildSourceArtifacthChild:child ∈ generated.sourceChildrenhItemEq:child.toMakeItem = item⊢ child.toMakeItem.value = none
  simp [GeneratedChildSourceArtifact.toMakeItem,
    validatorReady_generated_makeSourceValuesEmpty hReady hGenerated hKind child hChild]All goals completed! 🐙

Validator-ready generated rows expose structural row validity.

theorem validatorReady_generated_rowsValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms) :
    generated.RowsValid :=
  (validatorReady_generatedForm_valid hReady hGenerated).rowsValid

Validator-ready generated rows expose valid kind identifiers.

theorem validatorReady_generated_kindNameValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms) :
    generated.kindName.Valid :=
  (validatorReady_generated_rowsValid hReady hGenerated).kindNameValid

Validator-ready generated rows expose valid binding identifiers.

theorem validatorReady_generated_bindingValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms) :
    generated.binding.Valid :=
  (validatorReady_generated_rowsValid hReady hGenerated).bindingValid

Validator-ready generated source rows expose row validity directly.

theorem validatorReady_generated_sourceChild_valid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {source : GeneratedChildSourceArtifact}
    (hSource : source ∈ generated.sourceChildren) :
    source.Valid :=
  (validatorReady_generated_rowsValid hReady hGenerated).sourceChildrenValid source hSource

Validator-ready generated source rows expose valid node identifiers.

theorem validatorReady_generated_sourceChild_nodeValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {source : GeneratedChildSourceArtifact}
    (hSource : source ∈ generated.sourceChildren) :
    source.node.Valid :=
  (validatorReady_generated_sourceChild_valid hReady hGenerated hSource).nodeValid

Validator-ready generated source rows expose valid child labels.

theorem validatorReady_generated_sourceChild_labelValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {source : GeneratedChildSourceArtifact}
    (hSource : source ∈ generated.sourceChildren) :
    source.label.Valid :=
  (validatorReady_generated_sourceChild_valid hReady hGenerated hSource).labelValid

Validator-ready generated source rows expose optional static payload validity.

theorem validatorReady_generated_sourceChild_staticValueValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {source : GeneratedChildSourceArtifact}
    (hSource : source ∈ generated.sourceChildren) :
    source.StaticValueValid :=
  (validatorReady_generated_sourceChild_valid hReady hGenerated hSource).staticValueValid

Validator-ready generated static record payloads have duplicate-free field labels.

theorem validatorReady_generated_sourceChild_staticRecordFieldsUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {source : GeneratedChildSourceArtifact}
    (hSource : source ∈ generated.sourceChildren)
    {fields : List (FieldLabel × AdmissionStaticValue)}
    (hValue : source.value = some (AdmissionStaticValue.record fields)) :
    (fields.map Prod.fst).Nodup := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormssource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenfields:List (FieldLabel × AdmissionStaticValue)hValue:source.value = some (AdmissionStaticValue.record fields)⊢ (List.map Prod.fst fields).Nodup
  have hStaticValueValid :
      source.StaticValueValid :=
    validatorReady_generated_sourceChild_staticValueValid hReady hGenerated hSourceartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormssource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenfields:List (FieldLabel × AdmissionStaticValue)hValue:source.value = some (AdmissionStaticValue.record fields)hStaticValueValid:source.StaticValueValid⊢ (List.map Prod.fst fields).Nodup
  unfold GeneratedChildSourceArtifact.StaticValueValid at hStaticValueValidartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormssource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenfields:List (FieldLabel × AdmissionStaticValue)hValue:source.value = some (AdmissionStaticValue.record fields)hStaticValueValid:match source.value with
| none => True
| some value => value.Valid⊢ (List.map Prod.fst fields).Nodup
  rw [hValue] at hStaticValueValidartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormssource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenfields:List (FieldLabel × AdmissionStaticValue)hValue:source.value = some (AdmissionStaticValue.record fields)hStaticValueValid:match some (AdmissionStaticValue.record fields) with
| none => True
| some value => value.Valid⊢ (List.map Prod.fst fields).Nodup
  exact AdmissionStaticValue.valid_record_fieldsUnique hStaticValueValidAll goals completed! 🐙

Validator-ready generated static record payloads remain duplicate-free after conversion.

theorem validatorReady_generated_sourceChild_staticRecordFieldsUnique_toStaticValue
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {source : GeneratedChildSourceArtifact}
    (hSource : source ∈ generated.sourceChildren)
    {fields : List (FieldLabel × AdmissionStaticValue)}
    (hValue : source.value = some (AdmissionStaticValue.record fields)) :
    ((AdmissionStaticValue.toStaticValueFields fields).map Prod.fst).Nodup := byartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormssource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenfields:List (FieldLabel × AdmissionStaticValue)hValue:source.value = some (AdmissionStaticValue.record fields)⊢ (List.map Prod.fst (AdmissionStaticValue.toStaticValueFields fields)).Nodup
  have hStaticValueValid :
      source.StaticValueValid :=
    validatorReady_generated_sourceChild_staticValueValid hReady hGenerated hSourceartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormssource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenfields:List (FieldLabel × AdmissionStaticValue)hValue:source.value = some (AdmissionStaticValue.record fields)hStaticValueValid:source.StaticValueValid⊢ (List.map Prod.fst (AdmissionStaticValue.toStaticValueFields fields)).Nodup
  unfold GeneratedChildSourceArtifact.StaticValueValid at hStaticValueValidartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormssource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenfields:List (FieldLabel × AdmissionStaticValue)hValue:source.value = some (AdmissionStaticValue.record fields)hStaticValueValid:match source.value with
| none => True
| some value => value.Valid⊢ (List.map Prod.fst (AdmissionStaticValue.toStaticValueFields fields)).Nodup
  rw [hValue] at hStaticValueValidartifact:WireAdmissionArtifacthReady:artifact.ValidatorReadygenerated:GeneratedFormArtifacthGenerated:generated ∈ artifact.generatedFormssource:GeneratedChildSourceArtifacthSource:source ∈ generated.sourceChildrenfields:List (FieldLabel × AdmissionStaticValue)hValue:source.value = some (AdmissionStaticValue.record fields)hStaticValueValid:match some (AdmissionStaticValue.record fields) with
| none => True
| some value => value.Valid⊢ (List.map Prod.fst (AdmissionStaticValue.toStaticValueFields fields)).Nodup
  exact AdmissionStaticValue.valid_record_toStaticValueFields_labelsUnique hStaticValueValidAll goals completed! 🐙

Validator-ready generated used rows expose row validity directly.

theorem validatorReady_generated_usedChild_valid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    child.Valid :=
  (validatorReady_generated_rowsValid hReady hGenerated).usedChildrenValid child hChild

Validator-ready generated used rows expose valid node identifiers.

theorem validatorReady_generated_usedChild_nodeValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    child.node.Valid :=
  (validatorReady_generated_usedChild_valid hReady hGenerated hChild).nodeValid

Validator-ready generated used rows expose valid child labels.

theorem validatorReady_generated_usedChild_labelValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    child.label.Valid :=
  (validatorReady_generated_usedChild_valid hReady hGenerated hChild).labelValid

Validator-ready generated source rows follow the binding/label node-name policy.

theorem validatorReady_generated_sourceChild_ownedByBinding
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {source : GeneratedChildSourceArtifact}
    (hSource : source ∈ generated.sourceChildren) :
    source.node = GeneratedFormArtifact.childNodeFor generated.binding source.label :=
  (validatorReady_generated_childrenOwnedByBinding hReady hGenerated).left source hSource

Validator-ready generated used rows follow the binding/label node-name policy.

theorem validatorReady_generated_usedChild_ownedByBinding
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    child.node = GeneratedFormArtifact.childNodeFor generated.binding child.label :=
  (validatorReady_generated_childrenOwnedByBinding hReady hGenerated).right child hChild

Validator-ready generated used rows own every serialized frontier endpoint.

theorem validatorReady_generated_usedChild_frontiersOwnedByChild
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    child.FrontiersOwnedByChild :=
  (validatorReady_generated_usedChild_valid hReady hGenerated hChild).frontiersOwnedByChild

Validator-ready generated used rows expose ownership of each output frontier endpoint.

theorem validatorReady_generated_usedChild_outputOwnedByChild
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren)
    {output : AdmissionBoundaryPort}
    (hOutput : output ∈ child.outputs) :
    output.node = child.node :=
  (validatorReady_generated_usedChild_frontiersOwnedByChild
    hReady hGenerated hChild).left output hOutput

Validator-ready generated used rows expose ownership of each input frontier endpoint.

theorem validatorReady_generated_usedChild_inputOwnedByChild
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren)
    {input : AdmissionBoundaryPort}
    (hInput : input ∈ child.inputs) :
    input.node = child.node :=
  (validatorReady_generated_usedChild_frontiersOwnedByChild
    hReady hGenerated hChild).right input hInput

Validator-ready generated used rows have duplicate-free output frontier keys.

theorem validatorReady_generated_usedChild_outputKeysUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    child.outputKeys.Nodup :=
  (validatorReady_generated_usedChild_valid hReady hGenerated hChild).frontierKeysUnique.left

Validator-ready generated used rows have duplicate-free input frontier keys.

theorem validatorReady_generated_usedChild_inputKeysUnique
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    child.inputKeys.Nodup :=
  (validatorReady_generated_usedChild_valid hReady hGenerated hChild).frontierKeysUnique.right

Validator-ready generated used rows expose valid output frontier rows.

theorem validatorReady_generated_usedChild_outputsValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    BoundaryPortsValid child.outputs :=
  (validatorReady_generated_usedChild_valid hReady hGenerated hChild).outputsValid

Validator-ready generated used rows expose valid input frontier rows.

theorem validatorReady_generated_usedChild_inputsValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    BoundaryPortsValid child.inputs :=
  (validatorReady_generated_usedChild_valid hReady hGenerated hChild).inputsValid

Validator-ready generated used rows expose validity of each output frontier endpoint.

theorem validatorReady_generated_usedChild_outputValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren)
    {output : AdmissionBoundaryPort}
    (hOutput : output ∈ child.outputs) :
    output.Valid :=
  validatorReady_generated_usedChild_outputsValid
    hReady hGenerated hChild output hOutput

Validator-ready generated used rows expose validity of each input frontier endpoint.

theorem validatorReady_generated_usedChild_inputValid
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren)
    {input : AdmissionBoundaryPort}
    (hInput : input ∈ child.inputs) :
    input.Valid :=
  validatorReady_generated_usedChild_inputsValid
    hReady hGenerated hChild input hInput

Validator-ready generated used rows close output frontier endpoints over the node summary.

theorem validatorReady_generated_usedChild_outputsClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    BoundaryPortsClosed artifact.nodes child.outputs :=
  (validatorReady_generatedForm_domainClosed hReady hGenerated child hChild).outputsClosed

Validator-ready generated used rows close input frontier endpoints over the node summary.

theorem validatorReady_generated_usedChild_inputsClosed
    {artifact : WireAdmissionArtifact}
    (hReady : artifact.ValidatorReady)
    {generated : GeneratedFormArtifact}
    (hGenerated : generated ∈ artifact.generatedForms)
    {child : GeneratedChildArtifact}
    (hChild : child ∈ generated.usedChildren) :
    BoundaryPortsClosed artifact.nodes child.inputs :=
  (validatorReady_generatedForm_domainClosed hReady hGenerated child hChild).inputsClosed

end WireAdmissionArtifactend AdmissionArtifactend Cortex.Wire

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

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