inductive CordialMiners.Runtime.Event (Wave : Type u_3) (Hash : Type u_4) : Type (max u_3 u_4)

A runtime input event. Proposal and ordering are spontaneous in TrecState.Step, so the runtime carries them in an inbox and consumes them by rewriting.

• propose {Wave : Type u_3} {Hash : Type u_4} (w : Wave) (h : Hash) : Event Wave Hash
• order {Wave : Type u_3} {Hash : Type u_4} (hs : List Hash) : Event Wave Hash

@[implicit_reducible]

instance CordialMiners.Runtime.instDecidableEqEvent {Wave✝ : Type u_3} {Hash✝ : Type u_4} [DecidableEq Wave✝] [DecidableEq Hash✝] : DecidableEq (Event Wave✝ Hash✝)

Equations

• CordialMiners.Runtime.instDecidableEqEvent = CordialMiners.Runtime.instDecidableEqEvent.decEq

def CordialMiners.Runtime.instDecidableEqEvent.decEq {Wave✝ : Type u_3} {Hash✝ : Type u_4} [DecidableEq Wave✝] [DecidableEq Hash✝] (x✝ x✝¹ : Event Wave✝ Hash✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• CordialMiners.Runtime.instDecidableEqEvent.decEq (CordialMiners.Runtime.Event.propose w h) (CordialMiners.Runtime.Event.order hs) = isFalse ⋯
• CordialMiners.Runtime.instDecidableEqEvent.decEq (CordialMiners.Runtime.Event.order hs) (CordialMiners.Runtime.Event.propose w h) = isFalse ⋯
• CordialMiners.Runtime.instDecidableEqEvent.decEq (CordialMiners.Runtime.Event.order a) (CordialMiners.Runtime.Event.order b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CordialMiners.Runtime.instReprEvent {Wave✝ : Type u_3} {Hash✝ : Type u_4} [Repr Wave✝] [Repr Hash✝] : Repr (Event Wave✝ Hash✝)

Equations

• CordialMiners.Runtime.instReprEvent = { reprPrec := CordialMiners.Runtime.instReprEvent.repr }

def CordialMiners.Runtime.instReprEvent.repr {Wave✝ : Type u_3} {Hash✝ : Type u_4} [Repr Wave✝] [Repr Hash✝] : Event Wave✝ Hash✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def CordialMiners.Runtime.symA (s : String) : MeTTaIL.AST

A nullary symbol leaf in the MeTTaIL AST.

Equations

• CordialMiners.Runtime.symA s = MeTTaIL.AST.sexp (MeTTaIL.Label.id s) []

def CordialMiners.Runtime.appA (s : String) (args : List MeTTaIL.AST) : MeTTaIL.AST

An S-expression with a string head.

Equations

• CordialMiners.Runtime.appA s args = MeTTaIL.AST.sexp (MeTTaIL.Label.id s) args

def CordialMiners.Runtime.listNilA : MeTTaIL.AST

Runtime list terminator for variable-length payloads.

Equations

• CordialMiners.Runtime.listNilA = CordialMiners.Runtime.appA "list-nil" []

def CordialMiners.Runtime.listConsA (head tail : MeTTaIL.AST) : MeTTaIL.AST

Runtime list cons for variable-length payloads.

Equations

• CordialMiners.Runtime.listConsA head tail = CordialMiners.Runtime.appA "list-cons" [head, tail]

def CordialMiners.Runtime.encodeListA {α : Type u_3} (e : α → MeTTaIL.AST) : List α → MeTTaIL.AST

Encode a Lean list as an explicit AST list payload.

Equations

• CordialMiners.Runtime.encodeListA e [] = CordialMiners.Runtime.listNilA
• CordialMiners.Runtime.encodeListA e (x_1 :: xs) = CordialMiners.Runtime.listConsA (e x_1) (CordialMiners.Runtime.encodeListA e xs)

def CordialMiners.Runtime.decodeListA {α : Type u_3} (d : MeTTaIL.AST → Option α) : MeTTaIL.AST → Option (List α)

Decode an explicit AST list payload.

Equations

• One or more equations did not get rendered due to their size.
• CordialMiners.Runtime.decodeListA d (MeTTaIL.AST.sexp (MeTTaIL.Label.id "list-nil") []) = some []
• CordialMiners.Runtime.decodeListA d x✝ = none

theorem CordialMiners.Runtime.decodeListA_encodeListA {α : Type u_3} (e : α → MeTTaIL.AST) (d : MeTTaIL.AST → Option α) (hd : ∀ (a : α), d (e a) = some a) (xs : List α) : decodeListA d (encodeListA e xs) = some xs

Encoded AST lists decode back to the original Lean list under a left-inverse element codec.

def CordialMiners.Runtime.eNat (n : ℕ) : MeTTaIL.AST

Executable natural-number encoder used by the Nat/Nat demo instance.

Equations

• CordialMiners.Runtime.eNat n = CordialMiners.Runtime.symA n.repr

def CordialMiners.Runtime.dNat : MeTTaIL.AST → Option ℕ

Executable natural-number decoder used by the Nat/Nat demo instance.

Equations

• CordialMiners.Runtime.dNat (MeTTaIL.AST.sexp (MeTTaIL.Label.id s) []) = s.toNat?
• CordialMiners.Runtime.dNat x✝ = none

theorem CordialMiners.Runtime.dNat_eNat (n : ℕ) : dNat (eNat n) = some n

The Nat codec is lossless on encoded naturals.

@[irreducible]

def CordialMiners.Runtime.sexprToAST : Sexpr → MeTTaIL.AST

Convert the older shallow CMIR atom syntax into the real MeTTaIL AST. Applications whose first element is a symbol become a headed AST node; other lists are preserved under an app head.

Equations

• CordialMiners.Runtime.sexprToAST (CordialMiners.Sexpr.sym s) = CordialMiners.Runtime.symA s
• CordialMiners.Runtime.sexprToAST (CordialMiners.Sexpr.num n) = CordialMiners.Runtime.eNat n
• CordialMiners.Runtime.sexprToAST (CordialMiners.Sexpr.app (CordialMiners.Sexpr.sym h :: args)) = CordialMiners.Runtime.appA h (List.map CordialMiners.Runtime.sexprToAST args)
• CordialMiners.Runtime.sexprToAST (CordialMiners.Sexpr.app args) = CordialMiners.Runtime.appA "app" (List.map CordialMiners.Runtime.sexprToAST args)

def CordialMiners.Runtime.encodeFactA {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) : TrecFact Wave Hash → MeTTaIL.AST

Encode one coarse protocol fact into the runtime AST.

Equations

• CordialMiners.Runtime.encodeFactA eW eH (CordialMiners.TrecFact.propose w h) = CordialMiners.Runtime.appA "propose" [eW w, eH h]
• CordialMiners.Runtime.encodeFactA eW eH (CordialMiners.TrecFact.qApprove w h) = CordialMiners.Runtime.appA "q-approve" [eW w, eH h]
• CordialMiners.Runtime.encodeFactA eW eH (CordialMiners.TrecFact.certThresh w h) = CordialMiners.Runtime.appA "cert-threshold" [eW w, eH h]
• CordialMiners.Runtime.encodeFactA eW eH (CordialMiners.TrecFact.final w h) = CordialMiners.Runtime.appA "final" [eW w, eH h]
• CordialMiners.Runtime.encodeFactA eW eH (CordialMiners.TrecFact.finalLeader w h) = CordialMiners.Runtime.appA "final-leader" [eW w, eH h]
• CordialMiners.Runtime.encodeFactA eW eH (CordialMiners.TrecFact.orderedPrefix hs) = CordialMiners.Runtime.appA "ordered-prefix" [CordialMiners.Runtime.encodeListA eH hs]

def CordialMiners.Runtime.decodePairA {Wave : Type u_1} {Hash : Type u_2} {α : Type u_3} (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (mk : Wave → Hash → α) (a b : MeTTaIL.AST) : Option α

Decode a pair of Wave/Hash fields and assemble the result.

Equations

• CordialMiners.Runtime.decodePairA dW dH mk a b = match dW a, dH b with | some w, some h => some (mk w h) | x, x_1 => none

def CordialMiners.Runtime.decodeOrderedPayloadA {Hash : Type u_2} (dH : MeTTaIL.AST → Option Hash) : List MeTTaIL.AST → Option (List Hash)

Decode an ordered-prefix payload. Runtime terms use one explicit list payload. Legacy shallow extraction used variadic hash arguments, so this decoder accepts that shape too.

Equations

• CordialMiners.Runtime.decodeOrderedPayloadA dH [MeTTaIL.AST.sexp (MeTTaIL.Label.id "list-nil") []] = some []
• CordialMiners.Runtime.decodeOrderedPayloadA dH [MeTTaIL.AST.sexp (MeTTaIL.Label.id "list-cons") [head, tail]] = CordialMiners.Runtime.decodeListA dH (CordialMiners.Runtime.listConsA head tail)
• CordialMiners.Runtime.decodeOrderedPayloadA dH x✝ = List.mapM dH x✝

theorem CordialMiners.Runtime.decodeOrderedPayloadA_encodeListA {Hash : Type u_2} (eH : Hash → MeTTaIL.AST) (dH : MeTTaIL.AST → Option Hash) (hH : ∀ (h : Hash), dH (eH h) = some h) (hs : List Hash) : decodeOrderedPayloadA dH [encodeListA eH hs] = some hs

Runtime ordered payloads decode back to the original hash list.

def CordialMiners.Runtime.decodeFactA {Wave : Type u_1} {Hash : Type u_2} (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) : MeTTaIL.AST → Option (TrecFact Wave Hash)

Decode one runtime AST fact back to the coarse protocol fact language. Unknown heads or malformed arities decode to none.

Equations

• One or more equations did not get rendered due to their size.
• CordialMiners.Runtime.decodeFactA dW dH (MeTTaIL.AST.sexp (MeTTaIL.Label.id "propose") [a, b]) = CordialMiners.Runtime.decodePairA dW dH CordialMiners.TrecFact.propose a b
• CordialMiners.Runtime.decodeFactA dW dH (MeTTaIL.AST.sexp (MeTTaIL.Label.id "q-approve") [a, b]) = CordialMiners.Runtime.decodePairA dW dH CordialMiners.TrecFact.qApprove a b
• CordialMiners.Runtime.decodeFactA dW dH (MeTTaIL.AST.sexp (MeTTaIL.Label.id "cert-threshold") [a, b]) = CordialMiners.Runtime.decodePairA dW dH CordialMiners.TrecFact.certThresh a b
• CordialMiners.Runtime.decodeFactA dW dH (MeTTaIL.AST.sexp (MeTTaIL.Label.id "final") [a, b]) = CordialMiners.Runtime.decodePairA dW dH CordialMiners.TrecFact.final a b
• CordialMiners.Runtime.decodeFactA dW dH (MeTTaIL.AST.sexp (MeTTaIL.Label.id "final-leader") [a, b]) = CordialMiners.Runtime.decodePairA dW dH CordialMiners.TrecFact.finalLeader a b
• CordialMiners.Runtime.decodeFactA dW dH x✝ = none

theorem CordialMiners.Runtime.mapM_map_leftInvA {Hash : Type u_2} (e : Hash → MeTTaIL.AST) (d : MeTTaIL.AST → Option Hash) (hd : ∀ (a : Hash), d (e a) = some a) (l : List Hash) : List.mapM d (List.map e l) = some l

A list of encoded AST items decodes back to the original list.

theorem CordialMiners.Runtime.decodeFactA_encodeFactA {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hW : ∀ (w : Wave), dW (eW w) = some w) (hH : ∀ (h : Hash), dH (eH h) = some h) (f : TrecFact Wave Hash) : decodeFactA dW dH (encodeFactA eW eH f) = some f

Direct AST extraction is lossless for individual facts under left-inverse field codecs.

def CordialMiners.Runtime.stateOp : MeTTaIL.Label

The AC label used for coarse states.

Equations

• CordialMiners.Runtime.stateOp = MeTTaIL.Label.id "state"

def CordialMiners.Runtime.inboxOp : MeTTaIL.Label

The AC label used for pending input events.

Equations

• CordialMiners.Runtime.inboxOp = MeTTaIL.Label.id "inbox"

def CordialMiners.Runtime.cmOp : MeTTaIL.Label

The top-level runtime configuration label.

Equations

• CordialMiners.Runtime.cmOp = MeTTaIL.Label.id "cm"

def CordialMiners.Runtime.cmNil : MeTTaIL.AST

Sentinel leaf for right-nested AC collections. The sentinel is not an identity law.

Equations

• CordialMiners.Runtime.cmNil = CordialMiners.Runtime.symA "nil"

def CordialMiners.Runtime.consA (op : MeTTaIL.Label) (x rest : MeTTaIL.AST) : MeTTaIL.AST

A binary collection node.

Equations

• CordialMiners.Runtime.consA op x rest = MeTTaIL.AST.sexp op [x, rest]

def CordialMiners.Runtime.encodeEventA {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) : Event Wave Hash → MeTTaIL.AST

Encode one runtime input event.

Equations

• CordialMiners.Runtime.encodeEventA eW eH (CordialMiners.Runtime.Event.propose a a_1) = CordialMiners.Runtime.appA "ev-propose" [eW a, eH a_1]
• CordialMiners.Runtime.encodeEventA eW eH (CordialMiners.Runtime.Event.order a) = CordialMiners.Runtime.appA "ev-order" [CordialMiners.Runtime.encodeListA eH a]

def CordialMiners.Runtime.decodeEventA {Wave : Type u_1} {Hash : Type u_2} (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) : MeTTaIL.AST → Option (Event Wave Hash)

Decode one runtime input event.

Equations

• CordialMiners.Runtime.decodeEventA dW dH (MeTTaIL.AST.sexp (MeTTaIL.Label.id "ev-propose") [a, b]) = CordialMiners.Runtime.decodePairA dW dH CordialMiners.Runtime.Event.propose a b
• CordialMiners.Runtime.decodeEventA dW dH (MeTTaIL.AST.sexp (MeTTaIL.Label.id "ev-order") rest) = Option.map CordialMiners.Runtime.Event.order (CordialMiners.Runtime.decodeOrderedPayloadA dH rest)
• CordialMiners.Runtime.decodeEventA dW dH x✝ = none

theorem CordialMiners.Runtime.decodeEventA_encodeEventA {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hW : ∀ (w : Wave), dW (eW w) = some w) (hH : ∀ (h : Hash), dH (eH h) = some h) (event : Event Wave Hash) : decodeEventA dW dH (encodeEventA eW eH event) = some event

Encoded runtime input events decode back to the original event under left-inverse field codecs.

def CordialMiners.Runtime.encStateList {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (facts : List (TrecFact Wave Hash)) : MeTTaIL.AST

Encode a list of coarse facts as a right-nested state collection. Executable scenarios use this encoder.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CordialMiners.Runtime.encState {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (s : TrecState Wave Hash) : MeTTaIL.AST

Encode a finite coarse state as a right-nested state collection. The wrapper is noncomputable because Finset forgets order; executable scenarios use encStateList.

Equations

• CordialMiners.Runtime.encState eW eH s = CordialMiners.Runtime.encStateList eW eH (Finset.toList s)

def CordialMiners.Runtime.encInbox {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (events : List (Event Wave Hash)) : MeTTaIL.AST

Encode an inbox as a right-nested inbox collection.

Equations

• One or more equations did not get rendered due to their size.

def CordialMiners.Runtime.encConfigList {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (events : List (Event Wave Hash)) (facts : List (TrecFact Wave Hash)) : MeTTaIL.AST

Encode a full runtime configuration from an ordered fact list. Executable scenarios use this encoder.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CordialMiners.Runtime.encConfig {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (events : List (Event Wave Hash)) (s : TrecState Wave Hash) : MeTTaIL.AST

Encode a full runtime configuration.

Equations

• CordialMiners.Runtime.encConfig eW eH events s = MeTTaIL.AST.sexp CordialMiners.Runtime.cmOp [CordialMiners.Runtime.encInbox eW eH events, CordialMiners.Runtime.encState eW eH s]

def CordialMiners.Runtime.NoEmbeddedConfig : MeTTaIL.AST → Prop

Payloads are clean when they do not contain an embedded runtime configuration head. Payload cleanliness is the syntactic side condition needed by the later backward classifier: protocol rules should fire at the configuration boundary, not inside encoded field payloads.

Equations

• CordialMiners.Runtime.NoEmbeddedConfig (MeTTaIL.AST.var path) = True
• CordialMiners.Runtime.NoEmbeddedConfig (MeTTaIL.AST.sexp l args) = (l ≠ CordialMiners.Runtime.cmOp ∧ CordialMiners.Runtime.NoEmbeddedConfigList args)
• CordialMiners.Runtime.NoEmbeddedConfig (body.subst repl v) = (CordialMiners.Runtime.NoEmbeddedConfig body ∧ CordialMiners.Runtime.NoEmbeddedConfig repl)

def CordialMiners.Runtime.NoEmbeddedConfigList : List MeTTaIL.AST → Prop

List form of NoEmbeddedConfig, used to keep the AST recursion structurally visible to Lean.

Equations

• CordialMiners.Runtime.NoEmbeddedConfigList [] = True
• CordialMiners.Runtime.NoEmbeddedConfigList (t :: ts) = (CordialMiners.Runtime.NoEmbeddedConfig t ∧ CordialMiners.Runtime.NoEmbeddedConfigList ts)

def CordialMiners.Runtime.RuntimeConfigShape : MeTTaIL.AST → Prop

A well-shaped runtime configuration has one top-level cm node and clean inbox and state payloads.

Equations

• CordialMiners.Runtime.RuntimeConfigShape (MeTTaIL.AST.sexp l [ib, st]) = (l = CordialMiners.Runtime.cmOp ∧ CordialMiners.Runtime.NoEmbeddedConfig ib ∧ CordialMiners.Runtime.NoEmbeddedConfig st)
• CordialMiners.Runtime.RuntimeConfigShape x✝ = False

theorem CordialMiners.Runtime.noEmbeddedConfig_cmNil : NoEmbeddedConfig cmNil

The runtime sentinel is clean payload.

theorem CordialMiners.Runtime.noEmbeddedConfig_encodeListA {α : Type u_3} (e : α → MeTTaIL.AST) (h : ∀ (x : α), NoEmbeddedConfig (e x)) (xs : List α) : NoEmbeddedConfig (encodeListA e xs)

Explicit AST lists preserve payload cleanliness.

theorem CordialMiners.Runtime.noEmbeddedConfig_encodeFactA {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (hW : ∀ (w : Wave), NoEmbeddedConfig (eW w)) (hH : ∀ (h : Hash), NoEmbeddedConfig (eH h)) (fact : TrecFact Wave Hash) : NoEmbeddedConfig (encodeFactA eW eH fact)

Encoded facts are clean when their field codecs are clean.

theorem CordialMiners.Runtime.noEmbeddedConfig_encodeEventA {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (hW : ∀ (w : Wave), NoEmbeddedConfig (eW w)) (hH : ∀ (h : Hash), NoEmbeddedConfig (eH h)) (event : Event Wave Hash) : NoEmbeddedConfig (encodeEventA eW eH event)

Encoded input events are clean when their field codecs are clean.

theorem CordialMiners.Runtime.noEmbeddedConfig_encStateList {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (hW : ∀ (w : Wave), NoEmbeddedConfig (eW w)) (hH : ∀ (h : Hash), NoEmbeddedConfig (eH h)) (facts : List (TrecFact Wave Hash)) : NoEmbeddedConfig (encStateList eW eH facts)

Encoded state lists are clean when their field codecs are clean.

theorem CordialMiners.Runtime.noEmbeddedConfig_encInbox {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (hW : ∀ (w : Wave), NoEmbeddedConfig (eW w)) (hH : ∀ (h : Hash), NoEmbeddedConfig (eH h)) (events : List (Event Wave Hash)) : NoEmbeddedConfig (encInbox eW eH events)

Encoded inboxes are clean when their field codecs are clean.

theorem CordialMiners.Runtime.runtimeConfigShape_encConfigList {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (hW : ∀ (w : Wave), NoEmbeddedConfig (eW w)) (hH : ∀ (h : Hash), NoEmbeddedConfig (eH h)) (events : List (Event Wave Hash)) (facts : List (TrecFact Wave Hash)) : RuntimeConfigShape (encConfigList eW eH events facts)

Encoded configuration lists satisfy the runtime configuration shape invariant.

theorem CordialMiners.Runtime.runtimeConfigShape_encConfig {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (hW : ∀ (w : Wave), NoEmbeddedConfig (eW w)) (hH : ∀ (h : Hash), NoEmbeddedConfig (eH h)) (events : List (Event Wave Hash)) (s : TrecState Wave Hash) : RuntimeConfigShape (encConfig eW eH events s)

Encoded finite-state configurations satisfy the runtime configuration shape invariant.

def CordialMiners.Runtime.collectA (op : MeTTaIL.Label) : MeTTaIL.AST → List MeTTaIL.AST

Flatten one binary collection label. Nonmatching nodes are leaves.

Equations

• One or more equations did not get rendered due to their size.
• CordialMiners.Runtime.collectA op x✝ = [x✝]

theorem CordialMiners.Runtime.decodedCollection_foldr {α : Type u_3} (op : MeTTaIL.Label) (encode : α → MeTTaIL.AST) (decode : MeTTaIL.AST → Option α) (hLeaf : ∀ (x : α), collectA op (encode x) = [encode x]) (hDecode : ∀ (x : α), decode (encode x) = some x) (hNil : decode cmNil = none) (hSelf : (op == op) = true) (xs : List α) : List.filterMap decode (collectA op (List.foldr (fun (x rest : MeTTaIL.AST) => consA op x rest) cmNil (List.map encode xs))) = xs

Decoding a right-nested encoded collection recovers the source list when encoded elements are leaves for that collection and the element codec is lossless.

def CordialMiners.Runtime.decodeInboxA {Wave : Type u_1} {Hash : Type u_2} (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (t : MeTTaIL.AST) : List (Event Wave Hash)

Decode an inbox collection to the list of well-formed input events it contains. Malformed leaves are ignored, matching the state decoder's abstraction.

Equations

• CordialMiners.Runtime.decodeInboxA dW dH t = List.filterMap (CordialMiners.Runtime.decodeEventA dW dH) (CordialMiners.Runtime.collectA CordialMiners.Runtime.inboxOp t)

def CordialMiners.Runtime.astToInbox {Wave : Type u_1} {Hash : Type u_2} (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) : MeTTaIL.AST → List (Event Wave Hash)

Decode the inbox component of a runtime configuration. A bare inbox collection is accepted too, which mirrors astToState and keeps intermediate lemmas small.

Equations

• CordialMiners.Runtime.astToInbox dW dH (MeTTaIL.AST.sexp (MeTTaIL.Label.id "cm") [ib, head]) = CordialMiners.Runtime.decodeInboxA dW dH ib
• CordialMiners.Runtime.astToInbox dW dH x✝ = CordialMiners.Runtime.decodeInboxA dW dH x✝

def CordialMiners.Runtime.decodeStateA {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (t : MeTTaIL.AST) : TrecState Wave Hash

Decode a state collection, ignoring malformed leaves and collapsing duplicates.

Equations

• CordialMiners.Runtime.decodeStateA dW dH t = (List.filterMap (CordialMiners.Runtime.decodeFactA dW dH) (CordialMiners.Runtime.collectA CordialMiners.Runtime.stateOp t)).toFinset

def CordialMiners.Runtime.astToState {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) : MeTTaIL.AST → TrecState Wave Hash

Decode the state component of a runtime configuration. A bare collection is accepted too, which makes the abstraction useful in intermediate lemmas.

Equations

• CordialMiners.Runtime.astToState dW dH (MeTTaIL.AST.sexp (MeTTaIL.Label.id "cm") [ib, head]) = CordialMiners.Runtime.decodeStateA dW dH head
• CordialMiners.Runtime.astToState dW dH x✝ = CordialMiners.Runtime.decodeStateA dW dH x✝

theorem CordialMiners.Runtime.collectA_stateOp_encodeFactA {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (fact : TrecFact Wave Hash) : collectA stateOp (encodeFactA eW eH fact) = [encodeFactA eW eH fact]

Encoded facts are leaves of the runtime state collection.

theorem CordialMiners.Runtime.collectA_inboxOp_encodeEventA {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (event : Event Wave Hash) : collectA inboxOp (encodeEventA eW eH event) = [encodeEventA eW eH event]

Encoded input events are leaves of the runtime inbox collection.

theorem CordialMiners.Runtime.decodedFacts_encStateList {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hW : ∀ (w : Wave), dW (eW w) = some w) (hH : ∀ (h : Hash), dH (eH h) = some h) (facts : List (TrecFact Wave Hash)) : List.filterMap (decodeFactA dW dH) (collectA stateOp (encStateList eW eH facts)) = facts

Decoding the flattened encoded state list recovers the source fact list.

theorem CordialMiners.Runtime.decodeStateA_encStateList {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hW : ∀ (w : Wave), dW (eW w) = some w) (hH : ∀ (h : Hash), dH (eH h) = some h) (facts : List (TrecFact Wave Hash)) : decodeStateA dW dH (encStateList eW eH facts) = facts.toFinset

Decoding an encoded state list gives the finite set represented by the list.

theorem CordialMiners.Runtime.decodeInboxA_encInbox {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hW : ∀ (w : Wave), dW (eW w) = some w) (hH : ∀ (h : Hash), dH (eH h) = some h) (events : List (Event Wave Hash)) : decodeInboxA dW dH (encInbox eW eH events) = events

Decoding an encoded inbox recovers the source event list.

theorem CordialMiners.Runtime.decodeInboxA_cons_encodeEventA {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hW : ∀ (w : Wave), dW (eW w) = some w) (hH : ∀ (h : Hash), dH (eH h) = some h) (event : Event Wave Hash) (rest : MeTTaIL.AST) : decodeInboxA dW dH (consA inboxOp (encodeEventA eW eH event) rest) = event :: decodeInboxA dW dH rest

Prepending an encoded event to a decoded inbox collection conses the decoded event.

theorem CordialMiners.Runtime.decodeStateA_cons_encodeFactA {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hW : ∀ (w : Wave), dW (eW w) = some w) (hH : ∀ (h : Hash), dH (eH h) = some h) (fact : TrecFact Wave Hash) (rest : MeTTaIL.AST) : decodeStateA dW dH (consA stateOp (encodeFactA eW eH fact) rest) = insert fact (decodeStateA dW dH rest)

Prepending an encoded fact to a decoded state collection inserts the decoded fact.

theorem CordialMiners.Runtime.decodeStateA_cons_comm {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (a b : MeTTaIL.AST) : decodeStateA dW dH (consA stateOp a b) = decodeStateA dW dH (consA stateOp b a)

Decoding a state collection is insensitive to the AC commutativity generator.

theorem CordialMiners.Runtime.decodeStateA_cons_assoc {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (a b c : MeTTaIL.AST) : decodeStateA dW dH (consA stateOp (consA stateOp a b) c) = decodeStateA dW dH (consA stateOp a (consA stateOp b c))

Decoding a state collection is insensitive to the AC associativity generator.

theorem CordialMiners.Runtime.astToState_inbox_irrelevant {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (ib ib' st : MeTTaIL.AST) : astToState dW dH (MeTTaIL.AST.sexp cmOp [ib, st]) = astToState dW dH (MeTTaIL.AST.sexp cmOp [ib', st])

The decoded state of a runtime configuration does not depend on its inbox component.

theorem CordialMiners.Runtime.astToState_cons_comm {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (ib a b : MeTTaIL.AST) : astToState dW dH (MeTTaIL.AST.sexp cmOp [ib, consA stateOp a b]) = astToState dW dH (MeTTaIL.AST.sexp cmOp [ib, consA stateOp b a])

The decoded state of a runtime configuration is insensitive to state commutativity.

theorem CordialMiners.Runtime.astToState_cons_assoc {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (ib a b c : MeTTaIL.AST) : astToState dW dH (MeTTaIL.AST.sexp cmOp [ib, consA stateOp (consA stateOp a b) c]) = astToState dW dH (MeTTaIL.AST.sexp cmOp [ib, consA stateOp a (consA stateOp b c)])

The decoded state of a runtime configuration is insensitive to state associativity.

theorem CordialMiners.Runtime.decodeStateA_cons_encodeFactA_stutter {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hW : ∀ (w : Wave), dW (eW w) = some w) (hH : ∀ (h : Hash), dH (eH h) = some h) (fact : TrecFact Wave Hash) (rest : MeTTaIL.AST) (hmem : fact ∈ decodeStateA dW dH rest) : decodeStateA dW dH (consA stateOp (encodeFactA eW eH fact) rest) = decodeStateA dW dH rest

Re-adding an already decoded fact is a stutter under decodeStateA.

theorem CordialMiners.Runtime.astToState_cons_encodeFactA_stutter {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hW : ∀ (w : Wave), dW (eW w) = some w) (hH : ∀ (h : Hash), dH (eH h) = some h) (fact : TrecFact Wave Hash) (ib rest : MeTTaIL.AST) (hmem : fact ∈ astToState dW dH (MeTTaIL.AST.sexp cmOp [ib, rest])) : astToState dW dH (MeTTaIL.AST.sexp cmOp [ib, consA stateOp (encodeFactA eW eH fact) rest]) = astToState dW dH (MeTTaIL.AST.sexp cmOp [ib, rest])

Re-adding an already decoded fact to a runtime configuration is a stutter under astToState.

theorem CordialMiners.Runtime.astToInbox_encConfigList {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hCodec : (∀ (w : Wave), dW (eW w) = some w) ∧ ∀ (h : Hash), dH (eH h) = some h) (events : List (Event Wave Hash)) (facts : List (TrecFact Wave Hash)) : astToInbox dW dH (encConfigList eW eH events facts) = events

Decoding an encoded configuration list gives back its inbox event list.

theorem CordialMiners.Runtime.astToInbox_encConfig {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) [DecidableEq Wave] [DecidableEq Hash] (hCodec : (∀ (w : Wave), dW (eW w) = some w) ∧ ∀ (h : Hash), dH (eH h) = some h) (events : List (Event Wave Hash)) (s : TrecState Wave Hash) : astToInbox dW dH (encConfig eW eH events s) = events

Decoding an encoded finite-set configuration gives back its inbox event list.

theorem CordialMiners.Runtime.astToState_encConfigList {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) [DecidableEq Wave] [DecidableEq Hash] (hCodec : (∀ (w : Wave), dW (eW w) = some w) ∧ ∀ (h : Hash), dH (eH h) = some h) (events : List (Event Wave Hash)) (facts : List (TrecFact Wave Hash)) : astToState dW dH (encConfigList eW eH events facts) = facts.toFinset

Decoding an encoded configuration list gives the finite set represented by its state list.

theorem CordialMiners.Runtime.astToState_encConfig {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) [DecidableEq Wave] [DecidableEq Hash] (hCodec : (∀ (w : Wave), dW (eW w) = some w) ∧ ∀ (h : Hash), dH (eH h) = some h) (events : List (Event Wave Hash)) (s : TrecState Wave Hash) : astToState dW dH (encConfig eW eH events s) = s

Decoding an encoded finite-set configuration gives back its coarse state.