Cortex.Wire.AdmissionArtifact.PrimitiveTraceCheck

On this page
  1. Overview
Imports
import Cortex.Wire.AdmissionArtifact.ValidatorCore

Overview

Executable primitive-trace replay checks for decoded Wire admission artifacts.

PrimitiveTraceStackValid is currently relational: it says there exists a final primitive replay frame produced by the serialized postorder trace and that the frame matches the artifact summary. This module adds the first Lean-owned executable checker for that relation. The checker is not yet the full artifact validator; it is a sound executable core for one validator field.

namespace Cortex.Wirenamespace AdmissionArtifactopen Cortex.Wire.ElaborationIRnamespace WireAdmissionArtifact

Boolean form of SelectInternalTraceExit.

def selectInternalTraceExitCheck (artifact : WireAdmissionArtifact) (exit : AdmissionBoundaryPort) : Bool := artifact.selects.any fun selectAdmission => SelectInternalChoiceExit selectAdmission exit

The boolean hidden-exit classifier is exact for the relational classifier.

theorem selectInternalTraceExitCheck_eq_true_iff {artifact : WireAdmissionArtifact} {exit : AdmissionBoundaryPort} : artifact.selectInternalTraceExitCheck exit = true ↔ artifact.SelectInternalTraceExit exit := artifact:WireAdmissionArtifactexit:AdmissionBoundaryPort⊢ artifact.selectInternalTraceExitCheck exit = true ↔ artifact.SelectInternalTraceExit exit artifact:WireAdmissionArtifactexit:AdmissionBoundaryPort⊢ (artifact.selects.any fun selectAdmission => SelectInternalChoiceExit selectAdmission exit) = true ↔ ∃ selectAdmission ∈ artifact.selects, SelectInternalChoiceExit selectAdmission exit = true artifact:WireAdmissionArtifactexit:AdmissionBoundaryPort⊢ (artifact.selects.any fun selectAdmission => SelectInternalChoiceExit selectAdmission exit) = true → ∃ selectAdmission ∈ artifact.selects, SelectInternalChoiceExit selectAdmission exit = trueartifact:WireAdmissionArtifactexit:AdmissionBoundaryPort⊢ (∃ selectAdmission ∈ artifact.selects, SelectInternalChoiceExit selectAdmission exit = true) → (artifact.selects.any fun selectAdmission => SelectInternalChoiceExit selectAdmission exit) = true artifact:WireAdmissionArtifactexit:AdmissionBoundaryPort⊢ (artifact.selects.any fun selectAdmission => SelectInternalChoiceExit selectAdmission exit) = true → ∃ selectAdmission ∈ artifact.selects, SelectInternalChoiceExit selectAdmission exit = true artifact:WireAdmissionArtifactexit:AdmissionBoundaryPorthCheck:(artifact.selects.any fun selectAdmission => SelectInternalChoiceExit selectAdmission exit) = true⊢ ∃ selectAdmission ∈ artifact.selects, SelectInternalChoiceExit selectAdmission exit = true artifact:WireAdmissionArtifactexit:AdmissionBoundaryPorthCheck:(artifact.selects.any fun selectAdmission => SelectInternalChoiceExit selectAdmission exit) = trueselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshChoice:SelectInternalChoiceExit selectAdmission exit = true⊢ ∃ selectAdmission ∈ artifact.selects, SelectInternalChoiceExit selectAdmission exit = true All goals completed! 🐙 artifact:WireAdmissionArtifactexit:AdmissionBoundaryPort⊢ (∃ selectAdmission ∈ artifact.selects, SelectInternalChoiceExit selectAdmission exit = true) → (artifact.selects.any fun selectAdmission => SelectInternalChoiceExit selectAdmission exit) = true artifact:WireAdmissionArtifactexit:AdmissionBoundaryPortselectAdmission:SelectAdmissionArtifacthSelect:selectAdmission ∈ artifact.selectshChoice:SelectInternalChoiceExit selectAdmission exit = true⊢ (artifact.selects.any fun selectAdmission => SelectInternalChoiceExit selectAdmission exit) = true All goals completed! 🐙

Source-visible primitive node exits after erasing select-internal bridge exits.

def visiblePrimitiveExits (artifact : WireAdmissionArtifact) (exits : List AdmissionBoundaryPort) : List AdmissionBoundaryPort := exits.filter fun exit => !(artifact.selectInternalTraceExitCheck exit)

The executable visible-exit filter matches the primitive replay relation.

theorem mem_visiblePrimitiveExits_iff {artifact : WireAdmissionArtifact} {exits : List AdmissionBoundaryPort} {exit : AdmissionBoundaryPort} : exit ∈ artifact.visiblePrimitiveExits exits ↔ exit ∈ exits ∧ ¬ artifact.SelectInternalTraceExit exit := artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPort⊢ exit ∈ artifact.visiblePrimitiveExits exits ↔ exit ∈ exits ∧ ¬artifact.SelectInternalTraceExit exit artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPort⊢ exit ∈ List.filter (fun exit => !artifact.selectInternalTraceExitCheck exit) exits ↔ exit ∈ exits ∧ ¬artifact.SelectInternalTraceExit exit artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPort⊢ exit ∈ exits ∧ (!artifact.selectInternalTraceExitCheck exit) = true ↔ exit ∈ exits ∧ ¬artifact.SelectInternalTraceExit exit artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPort⊢ exit ∈ exits ∧ (!artifact.selectInternalTraceExitCheck exit) = true → exit ∈ exits ∧ ¬artifact.SelectInternalTraceExit exitartifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPort⊢ exit ∈ exits ∧ ¬artifact.SelectInternalTraceExit exit → exit ∈ exits ∧ (!artifact.selectInternalTraceExitCheck exit) = true artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPort⊢ exit ∈ exits ∧ (!artifact.selectInternalTraceExitCheck exit) = true → exit ∈ exits ∧ ¬artifact.SelectInternalTraceExit exit artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPorthMem:exit ∈ exits ∧ (!artifact.selectInternalTraceExitCheck exit) = true⊢ exit ∈ exits ∧ ¬artifact.SelectInternalTraceExit exit artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPorthMem:exit ∈ exits ∧ (!artifact.selectInternalTraceExitCheck exit) = true⊢ ¬artifact.SelectInternalTraceExit exit artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPorthMem:exit ∈ exits ∧ (!artifact.selectInternalTraceExitCheck exit) = truehHidden:artifact.SelectInternalTraceExit exit⊢ False artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPorthMem:exit ∈ exits ∧ (!artifact.selectInternalTraceExitCheck exit) = truehHidden:artifact.SelectInternalTraceExit exithCheck:artifact.selectInternalTraceExitCheck exit = true⊢ False artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPorthMem:exit ∈ exits ∧ (!true) = truehHidden:artifact.SelectInternalTraceExit exithCheck:artifact.selectInternalTraceExitCheck exit = true⊢ False All goals completed! 🐙 artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPort⊢ exit ∈ exits ∧ ¬artifact.SelectInternalTraceExit exit → exit ∈ exits ∧ (!artifact.selectInternalTraceExitCheck exit) = true artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPorthMem:exit ∈ exits ∧ ¬artifact.SelectInternalTraceExit exit⊢ exit ∈ exits ∧ (!artifact.selectInternalTraceExitCheck exit) = true artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPorthMem:exit ∈ exits ∧ ¬artifact.SelectInternalTraceExit exit⊢ (!artifact.selectInternalTraceExitCheck exit) = true cases hCheck : artifact.selectInternalTraceExitCheck exit with artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPorthMem:exit ∈ exits ∧ ¬artifact.SelectInternalTraceExit exithCheck:artifact.selectInternalTraceExitCheck exit = false⊢ (!false) = true All goals completed! 🐙 artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPorthMem:exit ∈ exits ∧ ¬artifact.SelectInternalTraceExit exithCheck:artifact.selectInternalTraceExitCheck exit = true⊢ (!true) = true artifact:WireAdmissionArtifactexits:List AdmissionBoundaryPortexit:AdmissionBoundaryPorthMem:exit ∈ exits ∧ ¬artifact.SelectInternalTraceExit exithCheck:artifact.selectInternalTraceExitCheck exit = truehHidden:artifact.SelectInternalTraceExit exit⊢ (!true) = true All goals completed! 🐙

Execute one primitive trace replay step, rejecting stack-shape or ledger mismatches.

def primitiveTraceStepCheck (artifact : WireAdmissionArtifact) (stack : List PrimitiveTraceFrame) : PrimitiveGraphStep → Option (List PrimitiveTraceFrame) | PrimitiveGraphStep.empty => some (PrimitiveTraceFrame.empty :: stack) | PrimitiveGraphStep.node node entries exits => some (PrimitiveTraceFrame.nodeFrame node entries (artifact.visiblePrimitiveExits exits) :: stack) | PrimitiveGraphStep.bindingRef binding => match stack with | frame :: rest => some ({ frame with bindingRefs := binding :: frame.bindingRefs } :: rest) | [] => none | PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings => match stack with | right :: left :: rest => if _hLeftNodes : leftNodes.Perm left.nodes then if _hRightNodes : rightNodes.Perm right.nodes then if _hLeftBindings : leftBindings.Perm left.bindingRefs then if _hRightBindings : rightBindings.Perm right.bindingRefs then some (PrimitiveTraceFrame.overlay left right :: rest) else none else none else none else none | [] => none | _only :: [] => none | PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries => match stack with | right :: left :: rest => if _hLeftExits : leftExits.Perm left.exits then if _hRightEntries : rightEntries.Perm right.entries then if _hUnmatchedLeft : ((matchedPairs.map (fun pair => pair.fromPort)) ++ unmatchedLeftExits).Perm left.exits then if _hUnmatchedRight : ((matchedPairs.map (fun pair => pair.toPort)) ++ unmatchedRightEntries).Perm right.entries then some (PrimitiveTraceFrame.connect left right matchedPairs unmatchedLeftExits unmatchedRightEntries :: rest) else none else none else none else none | [] => none | _only :: [] => none

Successful executable primitive-step replay is accepted by the relational replay step.

theorem primitiveTraceStepCheck_sound {artifact : WireAdmissionArtifact} {stack next : List PrimitiveTraceFrame} {step : PrimitiveGraphStep} (hCheck : artifact.primitiveTraceStepCheck stack step = some next) : PrimitiveTraceStep artifact.SelectInternalTraceExit stack step next := artifact:WireAdmissionArtifactstack:List PrimitiveTraceFramenext:List PrimitiveTraceFramestep:PrimitiveGraphStephCheck:artifact.primitiveTraceStepCheck stack step = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit stack step next cases step with artifact:WireAdmissionArtifactstack:List PrimitiveTraceFramenext:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck stack PrimitiveGraphStep.empty = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit stack PrimitiveGraphStep.empty next artifact:WireAdmissionArtifactstack:List PrimitiveTraceFramenext:List PrimitiveTraceFramehCheck:(match PrimitiveGraphStep.empty with | PrimitiveGraphStep.empty => some (PrimitiveTraceFrame.empty :: stack) | PrimitiveGraphStep.node node entries exits => some (PrimitiveTraceFrame.nodeFrame node entries (artifact.visiblePrimitiveExits exits) :: stack) | PrimitiveGraphStep.bindingRef binding => match stack with | frame :: rest => some ({ nodes := frame.nodes, bindingRefs := binding :: frame.bindingRefs, entries := frame.entries, exits := frame.exits, connections := frame.connections } :: rest) | [] => none | PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings => match stack with | right :: left :: rest => if _hLeftNodes : leftNodes.Perm left.nodes then if _hRightNodes : rightNodes.Perm right.nodes then if _hLeftBindings : leftBindings.Perm left.bindingRefs then if _hRightBindings : rightBindings.Perm right.bindingRefs then some (left.overlay right :: rest) else none else none else none else none | [] => none | [_only] => none | PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries => match stack with | right :: left :: rest => if _hLeftExits : leftExits.Perm left.exits then if _hRightEntries : rightEntries.Perm right.entries then if _hUnmatchedLeft : (List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exits then if _hUnmatchedRight : (List.map (fun pair => pair.toPort) matchedPairs ++ unmatchedRightEntries).Perm right.entries then some (left.connect right matchedPairs unmatchedLeftExits unmatchedRightEntries :: rest) else none else none else none else none | [] => none | [_only] => none) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit stack PrimitiveGraphStep.empty next artifact:WireAdmissionArtifactstack:List PrimitiveTraceFrame⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit stack PrimitiveGraphStep.empty (PrimitiveTraceFrame.empty :: stack) All goals completed! 🐙 artifact:WireAdmissionArtifactstack:List PrimitiveTraceFramenext:List PrimitiveTraceFramenode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthCheck:artifact.primitiveTraceStepCheck stack (PrimitiveGraphStep.node node entries exits) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit stack (PrimitiveGraphStep.node node entries exits) next artifact:WireAdmissionArtifactstack:List PrimitiveTraceFramenext:List PrimitiveTraceFramenode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPorthCheck:(match PrimitiveGraphStep.node node entries exits with | PrimitiveGraphStep.empty => some (PrimitiveTraceFrame.empty :: stack) | PrimitiveGraphStep.node node entries exits => some (PrimitiveTraceFrame.nodeFrame node entries (artifact.visiblePrimitiveExits exits) :: stack) | PrimitiveGraphStep.bindingRef binding => match stack with | frame :: rest => some ({ nodes := frame.nodes, bindingRefs := binding :: frame.bindingRefs, entries := frame.entries, exits := frame.exits, connections := frame.connections } :: rest) | [] => none | PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings => match stack with | right :: left :: rest => if _hLeftNodes : leftNodes.Perm left.nodes then if _hRightNodes : rightNodes.Perm right.nodes then if _hLeftBindings : leftBindings.Perm left.bindingRefs then if _hRightBindings : rightBindings.Perm right.bindingRefs then some (left.overlay right :: rest) else none else none else none else none | [] => none | [_only] => none | PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries => match stack with | right :: left :: rest => if _hLeftExits : leftExits.Perm left.exits then if _hRightEntries : rightEntries.Perm right.entries then if _hUnmatchedLeft : (List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exits then if _hUnmatchedRight : (List.map (fun pair => pair.toPort) matchedPairs ++ unmatchedRightEntries).Perm right.entries then some (left.connect right matchedPairs unmatchedLeftExits unmatchedRightEntries :: rest) else none else none else none else none | [] => none | [_only] => none) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit stack (PrimitiveGraphStep.node node entries exits) next artifact:WireAdmissionArtifactstack:List PrimitiveTraceFramenode:NodeIdentries:List AdmissionBoundaryPortexits:List AdmissionBoundaryPort⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit stack (PrimitiveGraphStep.node node entries exits) (PrimitiveTraceFrame.nodeFrame node entries (artifact.visiblePrimitiveExits exits) :: stack) All goals completed! 🐙 artifact:WireAdmissionArtifactstack:List PrimitiveTraceFramenext:List PrimitiveTraceFramebinding:BindingNamehCheck:artifact.primitiveTraceStepCheck stack (PrimitiveGraphStep.bindingRef binding) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit stack (PrimitiveGraphStep.bindingRef binding) next artifact:WireAdmissionArtifactstack:List PrimitiveTraceFramenext:List PrimitiveTraceFramebinding:BindingNamehCheck:(match PrimitiveGraphStep.bindingRef binding with | PrimitiveGraphStep.empty => some (PrimitiveTraceFrame.empty :: stack) | PrimitiveGraphStep.node node entries exits => some (PrimitiveTraceFrame.nodeFrame node entries (artifact.visiblePrimitiveExits exits) :: stack) | PrimitiveGraphStep.bindingRef binding => match stack with | frame :: rest => some ({ nodes := frame.nodes, bindingRefs := binding :: frame.bindingRefs, entries := frame.entries, exits := frame.exits, connections := frame.connections } :: rest) | [] => none | PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings => match stack with | right :: left :: rest => if _hLeftNodes : leftNodes.Perm left.nodes then if _hRightNodes : rightNodes.Perm right.nodes then if _hLeftBindings : leftBindings.Perm left.bindingRefs then if _hRightBindings : rightBindings.Perm right.bindingRefs then some (left.overlay right :: rest) else none else none else none else none | [] => none | [_only] => none | PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries => match stack with | right :: left :: rest => if _hLeftExits : leftExits.Perm left.exits then if _hRightEntries : rightEntries.Perm right.entries then if _hUnmatchedLeft : (List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exits then if _hUnmatchedRight : (List.map (fun pair => pair.toPort) matchedPairs ++ unmatchedRightEntries).Perm right.entries then some (left.connect right matchedPairs unmatchedLeftExits unmatchedRightEntries :: rest) else none else none else none else none | [] => none | [_only] => none) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit stack (PrimitiveGraphStep.bindingRef binding) next cases stack with artifact:WireAdmissionArtifactnext:List PrimitiveTraceFramebinding:BindingNamehCheck:(match PrimitiveGraphStep.bindingRef binding with | PrimitiveGraphStep.empty => some [PrimitiveTraceFrame.empty] | PrimitiveGraphStep.node node entries exits => some [PrimitiveTraceFrame.nodeFrame node entries (artifact.visiblePrimitiveExits exits)] | PrimitiveGraphStep.bindingRef binding => match [] with | frame :: rest => some ({ nodes := frame.nodes, bindingRefs := binding :: frame.bindingRefs, entries := frame.entries, exits := frame.exits, connections := frame.connections } :: rest) | [] => none | PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings => match [] with | right :: left :: rest => if _hLeftNodes : leftNodes.Perm left.nodes then if _hRightNodes : rightNodes.Perm right.nodes then if _hLeftBindings : leftBindings.Perm left.bindingRefs then if _hRightBindings : rightBindings.Perm right.bindingRefs then some (left.overlay right :: rest) else none else none else none else none | [] => none | [_only] => none | PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries => match [] with | right :: left :: rest => if _hLeftExits : leftExits.Perm left.exits then if _hRightEntries : rightEntries.Perm right.entries then if _hUnmatchedLeft : (List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exits then if _hUnmatchedRight : (List.map (fun pair => pair.toPort) matchedPairs ++ unmatchedRightEntries).Perm right.entries then some (left.connect right matchedPairs unmatchedLeftExits unmatchedRightEntries :: rest) else none else none else none else none | [] => none | [_only] => none) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit [] (PrimitiveGraphStep.bindingRef binding) next All goals completed! 🐙 artifact:WireAdmissionArtifactnext:List PrimitiveTraceFramebinding:BindingNameframe:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:(match PrimitiveGraphStep.bindingRef binding with | PrimitiveGraphStep.empty => some (PrimitiveTraceFrame.empty :: frame :: rest) | PrimitiveGraphStep.node node entries exits => some (PrimitiveTraceFrame.nodeFrame node entries (artifact.visiblePrimitiveExits exits) :: frame :: rest) | PrimitiveGraphStep.bindingRef binding => match frame :: rest with | frame :: rest => some ({ nodes := frame.nodes, bindingRefs := binding :: frame.bindingRefs, entries := frame.entries, exits := frame.exits, connections := frame.connections } :: rest) | [] => none | PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings => match frame :: rest with | right :: left :: rest => if _hLeftNodes : leftNodes.Perm left.nodes then if _hRightNodes : rightNodes.Perm right.nodes then if _hLeftBindings : leftBindings.Perm left.bindingRefs then if _hRightBindings : rightBindings.Perm right.bindingRefs then some (left.overlay right :: rest) else none else none else none else none | [] => none | [_only] => none | PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries => match frame :: rest with | right :: left :: rest => if _hLeftExits : leftExits.Perm left.exits then if _hRightEntries : rightEntries.Perm right.entries then if _hUnmatchedLeft : (List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exits then if _hUnmatchedRight : (List.map (fun pair => pair.toPort) matchedPairs ++ unmatchedRightEntries).Perm right.entries then some (left.connect right matchedPairs unmatchedLeftExits unmatchedRightEntries :: rest) else none else none else none else none | [] => none | [_only] => none) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (frame :: rest) (PrimitiveGraphStep.bindingRef binding) next artifact:WireAdmissionArtifactbinding:BindingNameframe:PrimitiveTraceFramerest:List PrimitiveTraceFrame⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (frame :: rest) (PrimitiveGraphStep.bindingRef binding) ({ nodes := frame.nodes, bindingRefs := binding :: frame.bindingRefs, entries := frame.entries, exits := frame.exits, connections := frame.connections } :: rest) All goals completed! 🐙 artifact:WireAdmissionArtifactstack:List PrimitiveTraceFramenext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehCheck:artifact.primitiveTraceStepCheck stack (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit stack (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next cases stack with artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNamehCheck:artifact.primitiveTraceStepCheck [] (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit [] (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next All goals completed! 🐙 artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrametail:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: tail) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: tail) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next cases tail with artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck [right] (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit [right] (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next All goals completed! 🐙 artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodes⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) nextartifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:¬leftNodes.Perm left.nodes⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodes⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodeshRightNodes:rightNodes.Perm right.nodes⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) nextartifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodeshRightNodes:¬rightNodes.Perm right.nodes⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodeshRightNodes:rightNodes.Perm right.nodes⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodeshRightNodes:rightNodes.Perm right.nodeshLeftBindings:leftBindings.Perm left.bindingRefs⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) nextartifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodeshRightNodes:rightNodes.Perm right.nodeshLeftBindings:¬leftBindings.Perm left.bindingRefs⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodeshRightNodes:rightNodes.Perm right.nodeshLeftBindings:leftBindings.Perm left.bindingRefs⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodeshRightNodes:rightNodes.Perm right.nodeshLeftBindings:leftBindings.Perm left.bindingRefshRightBindings:rightBindings.Perm right.bindingRefs⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) nextartifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodeshRightNodes:rightNodes.Perm right.nodeshLeftBindings:leftBindings.Perm left.bindingRefshRightBindings:¬rightBindings.Perm right.bindingRefs⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodeshRightNodes:rightNodes.Perm right.nodeshLeftBindings:leftBindings.Perm left.bindingRefshRightBindings:rightBindings.Perm right.bindingRefs⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehLeftNodes:leftNodes.Perm left.nodeshRightNodes:rightNodes.Perm right.nodeshLeftBindings:leftBindings.Perm left.bindingRefshRightBindings:rightBindings.Perm right.bindingRefshCheck:left.overlay right :: rest = next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next artifact:WireAdmissionArtifactleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehLeftNodes:leftNodes.Perm left.nodeshRightNodes:rightNodes.Perm right.nodeshLeftBindings:leftBindings.Perm left.bindingRefshRightBindings:rightBindings.Perm right.bindingRefs⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) (left.overlay right :: rest) All goals completed! 🐙 artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodeshRightNodes:rightNodes.Perm right.nodeshLeftBindings:leftBindings.Perm left.bindingRefshRightBindings:¬rightBindings.Perm right.bindingRefs⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next All goals completed! 🐙 artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodeshRightNodes:rightNodes.Perm right.nodeshLeftBindings:¬leftBindings.Perm left.bindingRefs⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next All goals completed! 🐙 artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:leftNodes.Perm left.nodeshRightNodes:¬rightNodes.Perm right.nodes⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next All goals completed! 🐙 artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftNodes:List NodeIdrightNodes:List NodeIdleftBindings:List BindingNamerightBindings:List BindingNameright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) = some nexthLeftNodes:¬leftNodes.Perm left.nodes⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.overlay leftNodes rightNodes leftBindings rightBindings) next All goals completed! 🐙 artifact:WireAdmissionArtifactstack:List PrimitiveTraceFramenext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthCheck:artifact.primitiveTraceStepCheck stack (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit stack (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next cases stack with artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPorthCheck:artifact.primitiveTraceStepCheck [] (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit [] (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next All goals completed! 🐙 artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrametail:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: tail) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: tail) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next cases tail with artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck [right] (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit [right] (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next All goals completed! 🐙 artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exits⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) nextartifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:¬leftExits.Perm left.exits⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exits⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exitshRightEntries:rightEntries.Perm right.entries⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) nextartifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exitshRightEntries:¬rightEntries.Perm right.entries⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exitshRightEntries:rightEntries.Perm right.entries⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exitshRightEntries:rightEntries.Perm right.entrieshUnmatchedLeft:(List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exits⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) nextartifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exitshRightEntries:rightEntries.Perm right.entrieshUnmatchedLeft:¬(List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exits⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exitshRightEntries:rightEntries.Perm right.entrieshUnmatchedLeft:(List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exits⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exitshRightEntries:rightEntries.Perm right.entrieshUnmatchedLeft:(List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exitshUnmatchedRight:(List.map (fun pair => pair.toPort) matchedPairs ++ unmatchedRightEntries).Perm right.entries⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) nextartifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exitshRightEntries:rightEntries.Perm right.entrieshUnmatchedLeft:(List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exitshUnmatchedRight:¬(List.map (fun pair => pair.toPort) matchedPairs ++ unmatchedRightEntries).Perm right.entries⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exitshRightEntries:rightEntries.Perm right.entrieshUnmatchedLeft:(List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exitshUnmatchedRight:(List.map (fun pair => pair.toPort) matchedPairs ++ unmatchedRightEntries).Perm right.entries⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehLeftExits:leftExits.Perm left.exitshRightEntries:rightEntries.Perm right.entrieshUnmatchedLeft:(List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exitshUnmatchedRight:(List.map (fun pair => pair.toPort) matchedPairs ++ unmatchedRightEntries).Perm right.entrieshCheck:left.connect right matchedPairs unmatchedLeftExits unmatchedRightEntries :: rest = next⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next artifact:WireAdmissionArtifactleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehLeftExits:leftExits.Perm left.exitshRightEntries:rightEntries.Perm right.entrieshUnmatchedLeft:(List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exitshUnmatchedRight:(List.map (fun pair => pair.toPort) matchedPairs ++ unmatchedRightEntries).Perm right.entries⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) (left.connect right matchedPairs unmatchedLeftExits unmatchedRightEntries :: rest) All goals completed! 🐙 artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exitshRightEntries:rightEntries.Perm right.entrieshUnmatchedLeft:(List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exitshUnmatchedRight:¬(List.map (fun pair => pair.toPort) matchedPairs ++ unmatchedRightEntries).Perm right.entries⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next All goals completed! 🐙 artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exitshRightEntries:rightEntries.Perm right.entrieshUnmatchedLeft:¬(List.map (fun pair => pair.fromPort) matchedPairs ++ unmatchedLeftExits).Perm left.exits⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next All goals completed! 🐙 artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:leftExits.Perm left.exitshRightEntries:¬rightEntries.Perm right.entries⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next All goals completed! 🐙 artifact:WireAdmissionArtifactnext:List PrimitiveTraceFrameleftExits:List AdmissionBoundaryPortrightEntries:List AdmissionBoundaryPortmatchedPairs:List AdmissionConnectionunmatchedLeftExits:List AdmissionBoundaryPortunmatchedRightEntries:List AdmissionBoundaryPortright:PrimitiveTraceFrameleft:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:artifact.primitiveTraceStepCheck (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) = some nexthLeftExits:¬leftExits.Perm left.exits⊢ PrimitiveTraceStep artifact.SelectInternalTraceExit (right :: left :: rest) (PrimitiveGraphStep.connect leftExits rightEntries matchedPairs unmatchedLeftExits unmatchedRightEntries) next All goals completed! 🐙

Execute the primitive trace stack from a starting stack.

def primitiveTraceReplayCheck (artifact : WireAdmissionArtifact) : List PrimitiveGraphStep → List PrimitiveTraceFrame → Option (List PrimitiveTraceFrame) | [], stack => some stack | step :: rest, stack => match artifact.primitiveTraceStepCheck stack step with | none => none | some next => artifact.primitiveTraceReplayCheck rest next

Successful executable primitive-trace replay is accepted by the relational replay.

theorem primitiveTraceReplayCheck_sound {artifact : WireAdmissionArtifact} {steps : List PrimitiveGraphStep} {stack finalStack : List PrimitiveTraceFrame} (hCheck : artifact.primitiveTraceReplayCheck steps stack = some finalStack) : PrimitiveTraceReplays artifact.SelectInternalTraceExit steps stack finalStack := artifact:WireAdmissionArtifactsteps:List PrimitiveGraphStepstack:List PrimitiveTraceFramefinalStack:List PrimitiveTraceFramehCheck:artifact.primitiveTraceReplayCheck steps stack = some finalStack⊢ PrimitiveTraceReplays artifact.SelectInternalTraceExit steps stack finalStack induction steps generalizing stack with artifact:WireAdmissionArtifactfinalStack:List PrimitiveTraceFramestack:List PrimitiveTraceFramehCheck:artifact.primitiveTraceReplayCheck [] stack = some finalStack⊢ PrimitiveTraceReplays artifact.SelectInternalTraceExit [] stack finalStack artifact:WireAdmissionArtifactfinalStack:List PrimitiveTraceFramestack:List PrimitiveTraceFramehCheck:some stack = some finalStack⊢ PrimitiveTraceReplays artifact.SelectInternalTraceExit [] stack finalStack artifact:WireAdmissionArtifactfinalStack:List PrimitiveTraceFrame⊢ PrimitiveTraceReplays artifact.SelectInternalTraceExit [] finalStack finalStack All goals completed! 🐙 artifact:WireAdmissionArtifactfinalStack:List PrimitiveTraceFramestep:PrimitiveGraphSteprest:List PrimitiveGraphStepih:∀ {stack : List PrimitiveTraceFrame}, artifact.primitiveTraceReplayCheck rest stack = some finalStack → PrimitiveTraceReplays artifact.SelectInternalTraceExit rest stack finalStackstack:List PrimitiveTraceFramehCheck:artifact.primitiveTraceReplayCheck (step :: rest) stack = some finalStack⊢ PrimitiveTraceReplays artifact.SelectInternalTraceExit (step :: rest) stack finalStack artifact:WireAdmissionArtifactfinalStack:List PrimitiveTraceFramestep:PrimitiveGraphSteprest:List PrimitiveGraphStepih:∀ {stack : List PrimitiveTraceFrame}, artifact.primitiveTraceReplayCheck rest stack = some finalStack → PrimitiveTraceReplays artifact.SelectInternalTraceExit rest stack finalStackstack:List PrimitiveTraceFramehCheck:(match artifact.primitiveTraceStepCheck stack step with | none => none | some next => artifact.primitiveTraceReplayCheck rest next) = some finalStack⊢ PrimitiveTraceReplays artifact.SelectInternalTraceExit (step :: rest) stack finalStack cases hStep : artifact.primitiveTraceStepCheck stack step with artifact:WireAdmissionArtifactfinalStack:List PrimitiveTraceFramestep:PrimitiveGraphSteprest:List PrimitiveGraphStepih:∀ {stack : List PrimitiveTraceFrame}, artifact.primitiveTraceReplayCheck rest stack = some finalStack → PrimitiveTraceReplays artifact.SelectInternalTraceExit rest stack finalStackstack:List PrimitiveTraceFramehCheck:(match artifact.primitiveTraceStepCheck stack step with | none => none | some next => artifact.primitiveTraceReplayCheck rest next) = some finalStackhStep:artifact.primitiveTraceStepCheck stack step = none⊢ PrimitiveTraceReplays artifact.SelectInternalTraceExit (step :: rest) stack finalStack artifact:WireAdmissionArtifactfinalStack:List PrimitiveTraceFramestep:PrimitiveGraphSteprest:List PrimitiveGraphStepih:∀ {stack : List PrimitiveTraceFrame}, artifact.primitiveTraceReplayCheck rest stack = some finalStack → PrimitiveTraceReplays artifact.SelectInternalTraceExit rest stack finalStackstack:List PrimitiveTraceFramehCheck:(match none with | none => none | some next => artifact.primitiveTraceReplayCheck rest next) = some finalStackhStep:artifact.primitiveTraceStepCheck stack step = none⊢ PrimitiveTraceReplays artifact.SelectInternalTraceExit (step :: rest) stack finalStack All goals completed! 🐙 artifact:WireAdmissionArtifactfinalStack:List PrimitiveTraceFramestep:PrimitiveGraphSteprest:List PrimitiveGraphStepih:∀ {stack : List PrimitiveTraceFrame}, artifact.primitiveTraceReplayCheck rest stack = some finalStack → PrimitiveTraceReplays artifact.SelectInternalTraceExit rest stack finalStackstack:List PrimitiveTraceFramehCheck:(match artifact.primitiveTraceStepCheck stack step with | none => none | some next => artifact.primitiveTraceReplayCheck rest next) = some finalStacknext:List PrimitiveTraceFramehStep:artifact.primitiveTraceStepCheck stack step = some next⊢ PrimitiveTraceReplays artifact.SelectInternalTraceExit (step :: rest) stack finalStack artifact:WireAdmissionArtifactfinalStack:List PrimitiveTraceFramestep:PrimitiveGraphSteprest:List PrimitiveGraphStepih:∀ {stack : List PrimitiveTraceFrame}, artifact.primitiveTraceReplayCheck rest stack = some finalStack → PrimitiveTraceReplays artifact.SelectInternalTraceExit rest stack finalStackstack:List PrimitiveTraceFramenext:List PrimitiveTraceFramehCheck:(match some next with | none => none | some next => artifact.primitiveTraceReplayCheck rest next) = some finalStackhStep:artifact.primitiveTraceStepCheck stack step = some next⊢ PrimitiveTraceReplays artifact.SelectInternalTraceExit (step :: rest) stack finalStack All goals completed! 🐙instance primitiveTraceFrameMatchesSummaryDecidable (frame : PrimitiveTraceFrame) (artifact : WireAdmissionArtifact) : Decidable (frame.MatchesSummary artifact) := frame:PrimitiveTraceFrameartifact:WireAdmissionArtifact⊢ Decidable (frame.MatchesSummary artifact) frame:PrimitiveTraceFrameartifact:WireAdmissionArtifact⊢ Decidable (frame.nodes.Perm artifact.nodes ∧ frame.bindingRefs.Perm artifact.bindingRefs ∧ frame.entries.Perm artifact.entries ∧ frame.exits.Perm artifact.exits ∧ frame.connections.Perm artifact.connections) All goals completed! 🐙

Execute primitive replay and require exactly one final frame matching the artifact summary.

def primitiveTraceStackValidCheck (artifact : WireAdmissionArtifact) : Bool := match artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] with | some [finalFrame] => decide (finalFrame.MatchesSummary artifact) | some [] => false | some (_first :: _second :: _rest) => false | none => false

The executable primitive-stack checker is sound for PrimitiveTraceStackValid.

theorem primitiveTraceStackValidCheck_sound {artifact : WireAdmissionArtifact} (hCheck : artifact.primitiveTraceStackValidCheck = true) : artifact.PrimitiveTraceStackValid := artifact:WireAdmissionArtifacthCheck:artifact.primitiveTraceStackValidCheck = true⊢ artifact.PrimitiveTraceStackValid artifact:WireAdmissionArtifacthCheck:(match artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] with | some [finalFrame] => decide (finalFrame.MatchesSummary artifact) | some [] => false | some (_first :: _second :: _rest) => false | none => false) = true⊢ artifact.PrimitiveTraceStackValid cases hReplay : artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] with artifact:WireAdmissionArtifacthCheck:(match artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] with | some [finalFrame] => decide (finalFrame.MatchesSummary artifact) | some [] => false | some (_first :: _second :: _rest) => false | none => false) = truehReplay:artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] = none⊢ artifact.PrimitiveTraceStackValid artifact:WireAdmissionArtifacthCheck:(match none with | some [finalFrame] => decide (finalFrame.MatchesSummary artifact) | some [] => false | some (_first :: _second :: _rest) => false | none => false) = truehReplay:artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] = none⊢ artifact.PrimitiveTraceStackValid All goals completed! 🐙 artifact:WireAdmissionArtifacthCheck:(match artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] with | some [finalFrame] => decide (finalFrame.MatchesSummary artifact) | some [] => false | some (_first :: _second :: _rest) => false | none => false) = truestack:List PrimitiveTraceFramehReplay:artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] = some stack⊢ artifact.PrimitiveTraceStackValid artifact:WireAdmissionArtifactstack:List PrimitiveTraceFramehCheck:(match some stack with | some [finalFrame] => decide (finalFrame.MatchesSummary artifact) | some [] => false | some (_first :: _second :: _rest) => false | none => false) = truehReplay:artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] = some stack⊢ artifact.PrimitiveTraceStackValid cases stack with artifact:WireAdmissionArtifacthCheck:(match some [] with | some [finalFrame] => decide (finalFrame.MatchesSummary artifact) | some [] => false | some (_first :: _second :: _rest) => false | none => false) = truehReplay:artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] = some []⊢ artifact.PrimitiveTraceStackValid All goals completed! 🐙 artifact:WireAdmissionArtifactfinalFrame:PrimitiveTraceFramerest:List PrimitiveTraceFramehCheck:(match some (finalFrame :: rest) with | some [finalFrame] => decide (finalFrame.MatchesSummary artifact) | some [] => false | some (_first :: _second :: _rest) => false | none => false) = truehReplay:artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] = some (finalFrame :: rest)⊢ artifact.PrimitiveTraceStackValid cases rest with artifact:WireAdmissionArtifactfinalFrame:PrimitiveTraceFramehCheck:(match some [finalFrame] with | some [finalFrame] => decide (finalFrame.MatchesSummary artifact) | some [] => false | some (_first :: _second :: _rest) => false | none => false) = truehReplay:artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] = some [finalFrame]⊢ artifact.PrimitiveTraceStackValid artifact:WireAdmissionArtifactfinalFrame:PrimitiveTraceFramehCheck:(match some [finalFrame] with | some [finalFrame] => decide (finalFrame.MatchesSummary artifact) | some [] => false | some (_first :: _second :: _rest) => false | none => false) = truehReplay:artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] = some [finalFrame]hMatch:finalFrame.MatchesSummary artifact⊢ artifact.PrimitiveTraceStackValid All goals completed! 🐙 artifact:WireAdmissionArtifactfinalFrame:PrimitiveTraceFramenext:PrimitiveTraceFrametail:List PrimitiveTraceFramehCheck:(match some (finalFrame :: next :: tail) with | some [finalFrame] => decide (finalFrame.MatchesSummary artifact) | some [] => false | some (_first :: _second :: _rest) => false | none => false) = truehReplay:artifact.primitiveTraceReplayCheck artifact.primitiveSteps [] = some (finalFrame :: next :: tail)⊢ artifact.PrimitiveTraceStackValid All goals completed! 🐙end WireAdmissionArtifactend AdmissionArtifactend Cortex.Wire