Theory /Cortex /Wire /AdmissionArtifact /Boundary

Cortex.Wire.AdmissionArtifact.Boundary

proofs

On this page

Overview
Schema Version
Shared Boundary Rows

Imports

import Cortex.Wire.ElaborationIR

Overview

Shared boundary rows for decoded Wire admission artifacts.

This page contains schema-version constants, serialized boundary endpoints, raw connection rows, and list-level closure/validity predicates used by the primitive, generated, phantom, select, and validator artifact modules.

              namespace Cortex.Wirenamespace AdmissionArtifactopen Cortex.Wire.ElaborationIR

Schema Version

Schema version emitted by the current Haskell admission artifact encoder.

def currentSchemaVersion : Nat := 3

Shared Boundary Rows

Optional label attached to a serialized boundary port.

inductive AdmissionPortLabel where
  | noLabel
  | label (label : FieldLabel)
  deriving DecidableEq, Repr

namespace AdmissionPortLabel

Optional serialized labels are valid when every present label is non-empty.

def Valid : AdmissionPortLabel → Prop
  | .noLabel => True
  | .label portLabel => portLabel.Valid

end AdmissionPortLabel

Boundary-port row emitted by the compiler artifact.

structure AdmissionBoundaryPort where
  node : NodeId
  port : FieldLabel
  contract : ContractId
  label : AdmissionPortLabel
  exclusiveGroup : Option (NodeId × Nat)
  deriving DecidableEq, Repr

namespace AdmissionBoundaryPort

Identity key for a serialized boundary endpoint.

def key (boundary : AdmissionBoundaryPort) : NodeId × FieldLabel × ContractId :=
  (boundary.node, boundary.port, boundary.contract)

Compatibility shape for a boundary endpoint, ignoring local node and port names.

def compatibilityShape (boundary : AdmissionBoundaryPort) : AdmissionPortLabel × ContractId :=
  (boundary.label, boundary.contract)

Source-visible output shape, preserving the local exclusive-group index when present.

def outputShape (boundary : AdmissionBoundaryPort) :
    AdmissionPortLabel × ContractId × Option Nat :=
  (boundary.label, boundary.contract, boundary.exclusiveGroup.map Prod.snd)

Output shape produced by an identity select arm for a selected variant.

def identityOutputShape (boundary : AdmissionBoundaryPort) :
    AdmissionPortLabel × ContractId × Option Nat :=
  (boundary.label, boundary.contract, none)

Two boundary endpoints are compatible when Wire => may contract them.

def CompatibleWith (fromPort toPort : AdmissionBoundaryPort) : Prop :=
  fromPort.label = toPort.label ∧ fromPort.contract = toPort.contract

Boundary compatibility is decidable because serialized labels and contracts are decidable.

instance instDecidableCompatibleWith
    (fromPort toPort : AdmissionBoundaryPort) :
    Decidable (fromPort.CompatibleWith toPort) := byfromPort:AdmissionBoundaryPorttoPort:AdmissionBoundaryPort⊢ Decidable (fromPort.CompatibleWith toPort)
  unfold CompatibleWithfromPort:AdmissionBoundaryPorttoPort:AdmissionBoundaryPort⊢ Decidable (fromPort.label = toPort.label ∧ fromPort.contract = toPort.contract)
  infer_instanceAll goals completed! 🐙

Serialized boundary endpoints must carry valid node, port, contract, and label identities.

def Valid (boundary : AdmissionBoundaryPort) : Prop :=
  boundary.node.Valid ∧
    boundary.port.Valid ∧
    boundary.contract.Valid ∧
    boundary.label.Valid ∧
    match boundary.exclusiveGroup with
    | none => True
    | some (owner, _index) => owner = boundary.node ∧ owner.Valid

Serialized exclusive-group owner rows are node-local.

def ExclusiveGroupOwnerLocal (boundary : AdmissionBoundaryPort) : Prop :=
  match boundary.exclusiveGroup with
  | none => True
  | some (owner, _index) => owner = boundary.node

Valid boundary rows expose node-local exclusive-group owners.

theorem valid_exclusiveGroupOwnerLocal
    {boundary : AdmissionBoundaryPort}
    (hValid : boundary.Valid) :
    boundary.ExclusiveGroupOwnerLocal := byboundary:AdmissionBoundaryPorthValid:boundary.Valid⊢ boundary.ExclusiveGroupOwnerLocal
  cases hGroup : boundary.exclusiveGroup with
  | none =>noneboundary:AdmissionBoundaryPorthValid:boundary.ValidhGroup:boundary.exclusiveGroup = none⊢ boundary.ExclusiveGroupOwnerLocal
      simp [ExclusiveGroupOwnerLocal, hGroup]All goals completed! 🐙
  | some group =>someboundary:AdmissionBoundaryPorthValid:boundary.Validgroup:NodeId × ℕhGroup:boundary.exclusiveGroup = some group⊢ boundary.ExclusiveGroupOwnerLocal
      have hOwner := hValid.right.right.right.rightsomeboundary:AdmissionBoundaryPorthValid:boundary.Validgroup:NodeId × ℕhGroup:boundary.exclusiveGroup = some grouphOwner:match boundary.exclusiveGroup with
| none => True
| some (owner, _index) => owner = boundary.node ∧ owner.Valid⊢ boundary.ExclusiveGroupOwnerLocal
      rw [hGroup] at hOwnersomeboundary:AdmissionBoundaryPorthValid:boundary.Validgroup:NodeId × ℕhGroup:boundary.exclusiveGroup = some grouphOwner:match some group with
| none => True
| some (owner, _index) => owner = boundary.node ∧ owner.Valid⊢ boundary.ExclusiveGroupOwnerLocal
      simpa [ExclusiveGroupOwnerLocal, hGroup] using hOwner.leftAll goals completed! 🐙

Valid boundary rows expose valid endpoint contract identifiers.

theorem valid_contractValid
    {boundary : AdmissionBoundaryPort}
    (hValid : boundary.Valid) :
    boundary.contract.Valid :=
  hValid.right.right.left

Boundary rows are closed over a node summary when both their endpoint node and optional exclusive-group owner are present.

def ClosedOver (nodes : List NodeId) (boundary : AdmissionBoundaryPort) : Prop :=
  boundary.node ∈ nodes ∧
    match boundary.exclusiveGroup with
    | none => True
    | some (owner, _index) => owner ∈ nodes

Label-first select key exposed by a serialized boundary endpoint.

def selectKey (boundary : AdmissionBoundaryPort) : FieldLabel :=
  match boundary.label with
  | .noLabel => ⟨boundary.contract.name⟩
  | .label label => label

end AdmissionBoundaryPort

Serialized source-level connection between two boundary ports.

structure AdmissionConnection where
  fromPort : AdmissionBoundaryPort
  toPort : AdmissionBoundaryPort
  deriving DecidableEq, Repr

namespace AdmissionConnection

Source node of a serialized boundary contraction.

def fromNode (connection : AdmissionConnection) : NodeId :=
  connection.fromPort.node

Target node of a serialized boundary contraction.

def toNode (connection : AdmissionConnection) : NodeId :=
  connection.toPort.node

Source endpoint key of a serialized boundary contraction.

def fromKey (connection : AdmissionConnection) : NodeId × FieldLabel × ContractId :=
  connection.fromPort.key

Target endpoint key of a serialized boundary contraction.

def toKey (connection : AdmissionConnection) : NodeId × FieldLabel × ContractId :=
  connection.toPort.key

Boundary contractions connect endpoints with the same source-visible label and contract.

def BoundaryCompatible (connection : AdmissionConnection) : Prop :=
  connection.fromPort.CompatibleWith connection.toPort

Serialized connections are valid when both endpoint rows are valid and compatible.

def Valid (connection : AdmissionConnection) : Prop :=
  connection.fromPort.Valid ∧ connection.toPort.Valid ∧ connection.BoundaryCompatible

Valid serialized connections expose source-visible boundary compatibility.

theorem valid_boundaryCompatible
    {connection : AdmissionConnection}
    (hValid : connection.Valid) :
    connection.BoundaryCompatible :=
  hValid.right.right

end AdmissionConnection

Record-field view of a labeled boundary endpoint, if it carries a field label.

def AdmissionBoundaryPort.recordField
    (boundary : AdmissionBoundaryPort) :
    Option (FieldLabel × ContractId) :=
  match boundary.label with
  | .noLabel => none
  | .label label => some (label, boundary.contract)

theorem filterMap_length_le
    {α β : Type}
    (f : α → Option β)
    (items : List α) :
    (items.filterMap f).length ≤ items.length := byα:Typeβ:Typef:α → Option βitems:List α⊢ (List.filterMap f items).length ≤ items.length
  induction items with
  | nil =>nilα:Typeβ:Typef:α → Option β⊢ (List.filterMap f []).length ≤ [].length
      simpAll goals completed! 🐙
  | cons item rest ih =>consα:Typeβ:Typef:α → Option βitem:αrest:List αih:(List.filterMap f rest).length ≤ rest.length⊢ (List.filterMap f (item :: rest)).length ≤ (item :: rest).length
      cases hItem : f item with
      | none =>cons.noneα:Typeβ:Typef:α → Option βitem:αrest:List αih:(List.filterMap f rest).length ≤ rest.lengthhItem:f item = none⊢ (List.filterMap f (item :: rest)).length ≤ (item :: rest).length
          simp [List.filterMap_cons_none, hItem, Nat.le_trans ih (Nat.le_succ rest.length)]All goals completed! 🐙
      | some value =>cons.someα:Typeβ:Typef:α → Option βitem:αrest:List αih:(List.filterMap f rest).length ≤ rest.lengthvalue:βhItem:f item = some value⊢ (List.filterMap f (item :: rest)).length ≤ (item :: rest).length
          simp [List.filterMap_cons_some, hItem, Nat.succ_le_succ ih]All goals completed! 🐙

theorem exists_some_of_filterMap_length_eq
    {α β : Type}
    {f : α → Option β}
    {items : List α}
    (hLength : (items.filterMap f).length = items.length)
    {item : α}
    (hItem : item ∈ items) :
    ∃ value, f item = some value := byα:Typeβ:Typef:α → Option βitems:List αhLength:(List.filterMap f items).length = items.lengthitem:αhItem:item ∈ items⊢ ∃ value, f item = some value
  induction items with
  | nil =>nilα:Typeβ:Typef:α → Option βitem:αhLength:(List.filterMap f []).length = [].lengthhItem:item ∈ []⊢ ∃ value, f item = some value
      cases hItemAll goals completed! 🐙
  | cons head tail ih =>consα:Typeβ:Typef:α → Option βitem:αhead:αtail:List αih:(List.filterMap f tail).length = tail.length → item ∈ tail → ∃ value, f item = some valuehLength:(List.filterMap f (head :: tail)).length = (head :: tail).lengthhItem:item ∈ head :: tail⊢ ∃ value, f item = some value
      cases hHead : f head with
      | none =>cons.noneα:Typeβ:Typef:α → Option βitem:αhead:αtail:List αih:(List.filterMap f tail).length = tail.length → item ∈ tail → ∃ value, f item = some valuehLength:(List.filterMap f (head :: tail)).length = (head :: tail).lengthhItem:item ∈ head :: tailhHead:f head = none⊢ ∃ value, f item = some value
          have hLe := filterMap_length_le f tailcons.noneα:Typeβ:Typef:α → Option βitem:αhead:αtail:List αih:(List.filterMap f tail).length = tail.length → item ∈ tail → ∃ value, f item = some valuehLength:(List.filterMap f (head :: tail)).length = (head :: tail).lengthhItem:item ∈ head :: tailhHead:f head = nonehLe:(List.filterMap f tail).length ≤ tail.length⊢ ∃ value, f item = some value
          have hBad : (tail.filterMap f).length = Nat.succ tail.length := byα:Typeβ:Typef:α → Option βitems:List αhLength:(List.filterMap f items).length = items.lengthitem:αhItem:item ∈ items⊢ ∃ value, f item = some value
            simpa [List.filterMap_cons_none, hHead] using hLengthAll goals completed! 🐙
          have hImpossible : Nat.succ tail.length ≤ tail.length := byα:Typeβ:Typef:α → Option βitems:List αhLength:(List.filterMap f items).length = items.lengthitem:αhItem:item ∈ items⊢ ∃ value, f item = some value
            rw [← hBad]α:Typeβ:Typef:α → Option βitem:αhead:αtail:List αih:(List.filterMap f tail).length = tail.length → item ∈ tail → ∃ value, f item = some valuehLength:(List.filterMap f (head :: tail)).length = (head :: tail).lengthhItem:item ∈ head :: tailhHead:f head = nonehLe:(List.filterMap f tail).length ≤ tail.lengthhBad:(List.filterMap f tail).length = tail.length.succ⊢ (List.filterMap f tail).length ≤ tail.length
            exact hLeAll goals completed! 🐙
          exact False.elim (Nat.not_succ_le_self tail.length hImpossible)All goals completed! 🐙
      | some value =>cons.someα:Typeβ:Typef:α → Option βitem:αhead:αtail:List αih:(List.filterMap f tail).length = tail.length → item ∈ tail → ∃ value, f item = some valuehLength:(List.filterMap f (head :: tail)).length = (head :: tail).lengthhItem:item ∈ head :: tailvalue:βhHead:f head = some value⊢ ∃ value, f item = some value
          rw [List.mem_cons] at hItemcons.someα:Typeβ:Typef:α → Option βitem:αhead:αtail:List αih:(List.filterMap f tail).length = tail.length → item ∈ tail → ∃ value, f item = some valuehLength:(List.filterMap f (head :: tail)).length = (head :: tail).lengthhItem:item = head ∨ item ∈ tailvalue:βhHead:f head = some value⊢ ∃ value, f item = some value
          rcases hItem with hEq | hTailcons.some.inlα:Typeβ:Typef:α → Option βitem:αhead:αtail:List αih:(List.filterMap f tail).length = tail.length → item ∈ tail → ∃ value, f item = some valuehLength:(List.filterMap f (head :: tail)).length = (head :: tail).lengthvalue:βhHead:f head = some valuehEq:item = head⊢ ∃ value, f item = some valuecons.some.inrα:Typeβ:Typef:α → Option βitem:αhead:αtail:List αih:(List.filterMap f tail).length = tail.length → item ∈ tail → ∃ value, f item = some valuehLength:(List.filterMap f (head :: tail)).length = (head :: tail).lengthvalue:βhHead:f head = some valuehTail:item ∈ tail⊢ ∃ value, f item = some value
          ·cons.some.inlα:Typeβ:Typef:α → Option βitem:αhead:αtail:List αih:(List.filterMap f tail).length = tail.length → item ∈ tail → ∃ value, f item = some valuehLength:(List.filterMap f (head :: tail)).length = (head :: tail).lengthvalue:βhHead:f head = some valuehEq:item = head⊢ ∃ value, f item = some value subst itemcons.some.inlα:Typeβ:Typef:α → Option βhead:αtail:List αhLength:(List.filterMap f (head :: tail)).length = (head :: tail).lengthvalue:βhHead:f head = some valueih:(List.filterMap f tail).length = tail.length → head ∈ tail → ∃ value, f head = some value⊢ ∃ value, f head = some value
            exact ⟨value, hHead⟩All goals completed! 🐙
          ·cons.some.inrα:Typeβ:Typef:α → Option βitem:αhead:αtail:List αih:(List.filterMap f tail).length = tail.length → item ∈ tail → ∃ value, f item = some valuehLength:(List.filterMap f (head :: tail)).length = (head :: tail).lengthvalue:βhHead:f head = some valuehTail:item ∈ tail⊢ ∃ value, f item = some value have hTailLength : (tail.filterMap f).length = tail.length := byα:Typeβ:Typef:α → Option βitems:List αhLength:(List.filterMap f items).length = items.lengthitem:αhItem:item ∈ items⊢ ∃ value, f item = some value
              apply Nat.succ.injaα:Typeβ:Typef:α → Option βitem:αhead:αtail:List αih:(List.filterMap f tail).length = tail.length → item ∈ tail → ∃ value, f item = some valuehLength:(List.filterMap f (head :: tail)).length = (head :: tail).lengthvalue:βhHead:f head = some valuehTail:item ∈ tail⊢ (List.filterMap f tail).length.succ = tail.length.succ
              simpa [List.filterMap_cons_some, hHead] using hLengthAll goals completed! 🐙
            exact ih hTailLength hTailAll goals completed! 🐙

theorem exists_append_singleton_of_mem
    {α : Type}
    {item : α}
    {items : List α}
    (hItem : item ∈ items) :
    ∃ before after, items = before ++ [item] ++ after := byα:Typeitem:αitems:List αhItem:item ∈ items⊢ ∃ before after, items = before ++ [item] ++ after
  induction items with
  | nil =>nilα:Typeitem:αhItem:item ∈ []⊢ ∃ before after, [] = before ++ [item] ++ after
      cases hItemAll goals completed! 🐙
  | cons head tail ih =>consα:Typeitem:αhead:αtail:List αih:item ∈ tail → ∃ before after, tail = before ++ [item] ++ afterhItem:item ∈ head :: tail⊢ ∃ before after, head :: tail = before ++ [item] ++ after
      rw [List.mem_cons] at hItemconsα:Typeitem:αhead:αtail:List αih:item ∈ tail → ∃ before after, tail = before ++ [item] ++ afterhItem:item = head ∨ item ∈ tail⊢ ∃ before after, head :: tail = before ++ [item] ++ after
      cases hItem with
      | inl hHead =>cons.inlα:Typeitem:αhead:αtail:List αih:item ∈ tail → ∃ before after, tail = before ++ [item] ++ afterhHead:item = head⊢ ∃ before after, head :: tail = before ++ [item] ++ after
          subst itemcons.inlα:Typehead:αtail:List αih:head ∈ tail → ∃ before after, tail = before ++ [head] ++ after⊢ ∃ before after, head :: tail = before ++ [head] ++ after
          exact ⟨[], tail, byα:Typehead:αtail:List αih:head ∈ tail → ∃ before after, tail = before ++ [head] ++ after⊢ head :: tail = [] ++ [head] ++ tail simpAll goals completed! 🐙⟩
      | inr hTail =>cons.inrα:Typeitem:αhead:αtail:List αih:item ∈ tail → ∃ before after, tail = before ++ [item] ++ afterhTail:item ∈ tail⊢ ∃ before after, head :: tail = before ++ [item] ++ after
          obtain ⟨before, after, hTailEq⟩ := ih hTailcons.inrα:Typeitem:αhead:αtail:List αih:item ∈ tail → ∃ before after, tail = before ++ [item] ++ afterhTail:item ∈ tailbefore:List αafter:List αhTailEq:tail = before ++ [item] ++ after⊢ ∃ before after, head :: tail = before ++ [item] ++ after
          exact ⟨head :: before, after, byα:Typeitem:αhead:αtail:List αih:item ∈ tail → ∃ before after, tail = before ++ [item] ++ afterhTail:item ∈ tailbefore:List αafter:List αhTailEq:tail = before ++ [item] ++ after⊢ head :: tail = head :: before ++ [item] ++ after simp [hTailEq]All goals completed! 🐙⟩

Every boundary row in a list is structurally valid.

def BoundaryPortsValid (ports : List AdmissionBoundaryPort) : Prop :=
  ∀ port, port ∈ ports → port.Valid

Every serialized connection row in a list is structurally valid.

def ConnectionsValid (connections : List AdmissionConnection) : Prop :=
  ∀ connection, connection ∈ connections → connection.Valid

Valid serialized connection lists expose compatibility for every connection row.

theorem connectionsValid_boundaryCompatible
    {connections : List AdmissionConnection}
    (hValid : ConnectionsValid connections)
    {connection : AdmissionConnection}
    (hConnection : connection ∈ connections) :
    connection.BoundaryCompatible :=
  AdmissionConnection.valid_boundaryCompatible (hValid connection hConnection)

Every serialized boundary row and its optional exclusive-group owner belong to the node summary.

def BoundaryPortsClosed (nodes : List NodeId) (ports : List AdmissionBoundaryPort) : Prop :=
  ∀ port, port ∈ ports → port.ClosedOver nodes

Every serialized connection row endpoint is closed over the given node summary.

def ConnectionsClosed (nodes : List NodeId) (connections : List AdmissionConnection) : Prop :=
  ∀ connection, connection ∈ connections →
    connection.fromPort.ClosedOver nodes ∧ connection.toPort.ClosedOver nodes

Raw compiled endpoint reference emitted in the top-level connection ledger.

structure AdmissionEndpointRef where
  node : NodeId
  port : Option FieldLabel
  deriving DecidableEq, Repr

namespace AdmissionEndpointRef

Raw connection endpoints must carry a valid node and any present port name.

def Valid (endpoint : AdmissionEndpointRef) : Prop :=
  endpoint.node.Valid ∧
    match endpoint.port with
    | none => True
    | some port => port.Valid

Boundary-row projection used by Haskell's top-level raw connection ledger.

def ofBoundary (boundary : AdmissionBoundaryPort) : AdmissionEndpointRef :=
  { node := boundary.node, port := some boundary.port }

end AdmissionEndpointRef

Raw compiled connection emitted by the top-level artifact summary.

structure AdmissionRawConnection where
  fromEndpoint : AdmissionEndpointRef
  toEndpoint : AdmissionEndpointRef
  deriving DecidableEq, Repr

namespace AdmissionRawConnection

Boundary-contraction projection used by Haskell's top-level raw connection ledger.

def ofAdmissionConnection (connection : AdmissionConnection) : AdmissionRawConnection :=
  { fromEndpoint := AdmissionEndpointRef.ofBoundary connection.fromPort
  , toEndpoint := AdmissionEndpointRef.ofBoundary connection.toPort
  }

Raw summary connections are valid when both endpoint refs are valid.

def Valid (connection : AdmissionRawConnection) : Prop :=
  connection.fromEndpoint.Valid ∧ connection.toEndpoint.Valid

end AdmissionRawConnectionend AdmissionArtifactend Cortex.Wire

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

← PreviousCortex.Wire.AdmissionArtifact Next →Cortex.Wire.AdmissionArtifact.Check