theorem CordialMiners.Runtime.dNat_acEq {a b : MeTTaIL.AST} (h : MeTTaIL.AC.ACEq acOpCM a b) : dNat a = dNat b

The executable Nat decoder ignores every runtime AC rearrangement.

theorem CordialMiners.Runtime.decodeListA_dNat_acEq {a b : MeTTaIL.AST} (h : MeTTaIL.AC.ACEq acOpCM a b) : decodeListA dNat a = decodeListA dNat b

Runtime AC rearrangement does not change executable Nat-list decoding.

theorem CordialMiners.Runtime.decodeFactA_dNat_acEq {a b : MeTTaIL.AST} (h : MeTTaIL.AC.ACEq acOpCM a b) : decodeFactA dNat dNat a = decodeFactA dNat dNat b

Executable Nat fact decoding ignores every runtime AC rearrangement.

theorem CordialMiners.Runtime.decodeStateA_dNat_acEq {a b : MeTTaIL.AST} (h : MeTTaIL.AC.ACEq acOpCM a b) : decodeStateA dNat dNat a = decodeStateA dNat dNat b

Executable Nat state decoding ignores every runtime AC rearrangement.

theorem CordialMiners.Runtime.astToState_dNat_acEq {a b : MeTTaIL.AST} (h : MeTTaIL.AC.ACEq acOpCM a b) : astToState dNat dNat a = astToState dNat dNat b

Executable Nat configuration decoding factors through runtime AC equivalence.

theorem CordialMiners.Runtime.runtime_step_backward_nat {source target : MeTTaIL.AST} (hshape : RuntimeConfigShape source) (hstep : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation source target) : (astToState dNat dNat source).Step (astToState dNat dNat target) ∨ astToState dNat dNat source = astToState dNat dNat target

The executable Nat/Nat runtime never takes a modulo-AC step outside the coarse protocol, up to decoded stutter.

def CordialMiners.Runtime.buriedProposalStart : MeTTaIL.AST

A proposal event buried after an order event. One runtime step must find it modulo AC.

Equations

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

def CordialMiners.Runtime.afterBuriedProposal : MeTTaIL.AST

The expected result after consuming the buried proposal event.

Equations

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

theorem CordialMiners.Runtime.buriedProposal_modAC : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation buriedProposalStart afterBuriedProposal

The buried proposal run is also a genuine runtime step modulo AC.

theorem CordialMiners.Runtime.buriedProposal_eval_modAC : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation buriedProposalStart (MeTTaIL.AC.evalAC' acOpCM cmPresentation 1 buriedProposalStart)

The executable buried-proposal step has a runtime relation witness.

def CordialMiners.Runtime.orderStart : MeTTaIL.AST

A multi-hash order event. The payload uses the runtime AST list codec.

Equations

• CordialMiners.Runtime.orderStart = CordialMiners.Runtime.encConfigList CordialMiners.Runtime.eNat CordialMiners.Runtime.eNat [CordialMiners.Runtime.Event.order [1, 2, 3]] []

def CordialMiners.Runtime.afterOrder : MeTTaIL.AST

The expected result after consuming the order event.

Equations

• CordialMiners.Runtime.afterOrder = CordialMiners.Runtime.encConfigList CordialMiners.Runtime.eNat CordialMiners.Runtime.eNat [] [CordialMiners.TrecFact.orderedPrefix [1, 2, 3]]

def CordialMiners.Runtime.runtimeFactList : MeTTaIL.AST → List (TrecFact ℕ ℕ)

Decode the state facts from a Nat/Nat runtime configuration.

Equations

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

theorem CordialMiners.Runtime.runtimeFactList_encStateList (facts : List (TrecFact ℕ ℕ)) : List.filterMap (decodeFactA dNat dNat) (collectA stateOp (encStateList eNat eNat facts)) = facts

Decoding an executable Nat/Nat state list returns the fact list used to build it.

theorem CordialMiners.Runtime.runtimeFactList_encConfigList (events : List (Event ℕ ℕ)) (facts : List (TrecFact ℕ ℕ)) : runtimeFactList (encConfigList eNat eNat events facts) = facts

Decoding an executable Nat/Nat configuration returns its encoded fact list.

theorem CordialMiners.Runtime.order_modAC : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation orderStart afterOrder

The order run is also a genuine runtime step modulo AC.

theorem CordialMiners.Runtime.order_eval_modAC : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation orderStart (MeTTaIL.AC.evalAC' acOpCM cmPresentation 1 orderStart)

The executable order step has a runtime relation witness.

def CordialMiners.Runtime.finalityStart : MeTTaIL.AST

A one-block finality scenario driven entirely by runtime rewrite rules.

Equations

• CordialMiners.Runtime.finalityStart = CordialMiners.Runtime.encConfigList CordialMiners.Runtime.eNat CordialMiners.Runtime.eNat [CordialMiners.Runtime.Event.propose 1 10] []

def CordialMiners.Runtime.finalityAfterPropose : MeTTaIL.AST

The finality scenario after the proposal input has been consumed.

Equations

• CordialMiners.Runtime.finalityAfterPropose = CordialMiners.Runtime.encConfigList CordialMiners.Runtime.eNat CordialMiners.Runtime.eNat [] [CordialMiners.TrecFact.propose 1 10]

def CordialMiners.Runtime.finalityAfterQApprove : MeTTaIL.AST

The finality scenario after quorum approval.

Equations

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

def CordialMiners.Runtime.finalityAfterCert : MeTTaIL.AST

The finality scenario after threshold certification.

Equations

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

def CordialMiners.Runtime.finalityAfterFinal : MeTTaIL.AST

The finality scenario after finality.

Equations

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

def CordialMiners.Runtime.finalityExpectedConfig : MeTTaIL.AST

The expected AST after proposal, approval, certificate, finality, and final-leader derivation.

Equations

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

def CordialMiners.Runtime.finalityExpectedFacts : List (TrecFact ℕ ℕ)

The decoded coarse facts expected from the finality run.

Equations

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

def CordialMiners.Runtime.finalityExpectedState : TrecState ℕ ℕ

The decoded coarse state expected from the finality run.

Equations

• CordialMiners.Runtime.finalityExpectedState = CordialMiners.Runtime.finalityExpectedFacts.toFinset

theorem CordialMiners.Runtime.finality_run_modAC : Relation.ReflTransGen (MeTTaIL.AC.RewStepModAC acOpCM cmPresentation) finalityStart finalityExpectedConfig

The five-step finality run is reachable in the runtime relation modulo AC.

theorem CordialMiners.Runtime.finality_eval_run_modAC : Relation.ReflTransGen (MeTTaIL.AC.RewStepModAC acOpCM cmPresentation) finalityStart (MeTTaIL.AC.evalAC' acOpCM cmPresentation 5 finalityStart)

The executable finality run has a runtime relation witness.

theorem CordialMiners.Runtime.finality_runtime_state_decodes : astToState dNat dNat (MeTTaIL.AC.evalAC' acOpCM cmPresentation 5 finalityStart) = finalityExpectedState

The executable finality run decodes to the expected coarse state.

theorem CordialMiners.Runtime.finality_trec_reachable : Relation.ReflTransGen TrecState.Step ∅ finalityExpectedState

The decoded coarse state of the finality run is reachable in T_rec.

theorem CordialMiners.Runtime.finality_runtime_trec_reachable : Relation.ReflTransGen TrecState.Step ∅ (astToState dNat dNat (MeTTaIL.AC.evalAC' acOpCM cmPresentation 5 finalityStart))

The decoded result of the executable finality run is coarse-reachable.

theorem CordialMiners.Runtime.finality_runtime_wf : TrecWF (astToState dNat dNat (MeTTaIL.AC.evalAC' acOpCM cmPresentation 5 finalityStart))

The decoded result of the executable finality run satisfies the coarse well-formedness invariant.

theorem CordialMiners.Runtime.finality_runtime_final_needs_propose : TrecFact.propose 1 10 ∈ astToState dNat dNat (MeTTaIL.AC.evalAC' acOpCM cmPresentation 5 finalityStart)

The final fact in the executable runtime result is backed by the matching proposal fact.