theorem CordialMiners.Runtime.acOpCM_state : acOpCM stateOp = true

The Cordial Miners state label is AC-enabled.

theorem CordialMiners.Runtime.acOpCM_inbox : acOpCM inboxOp = true

The Cordial Miners inbox label is AC-enabled.

theorem CordialMiners.Runtime.rewStepModAC_of_rewStep {t t' : MeTTaIL.AST} (h : MeTTaIL.RewStep cmPresentation t t') : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation t t'

A syntactic runtime step is also a modulo-AC step, using reflexive AC witnesses.

theorem CordialMiners.Runtime.acOpCM_true_ne_cmOp {l : MeTTaIL.Label} (h : acOpCM l = true) : l ≠ cmOp

AC-enabled Cordial Miners labels are collection labels, not the configuration label.

theorem CordialMiners.Runtime.acOpCM_eq_state_or_inbox {l : MeTTaIL.Label} (h : acOpCM l = true) : l = stateOp ∨ l = inboxOp

A Cordial Miners AC-enabled label is one of the two runtime collection labels.

theorem CordialMiners.Runtime.noEmbeddedConfigList_append_cons_iff {pre post : List MeTTaIL.AST} {a a' : MeTTaIL.AST} (h : NoEmbeddedConfig a ↔ NoEmbeddedConfig a') : NoEmbeddedConfigList (pre ++ a :: post) ↔ NoEmbeddedConfigList (pre ++ a' :: post)

Replacing one AC-equivalent payload preserves the no-embedded-configuration list invariant.

theorem CordialMiners.Runtime.noEmbeddedConfig_acEq_iff {source target : MeTTaIL.AST} (h : MeTTaIL.AC.ACEq acOpCM source target) : NoEmbeddedConfig source ↔ NoEmbeddedConfig target

AC-equivalence preserves the no-embedded-configuration payload invariant.

theorem CordialMiners.Runtime.runtimeConfigShape_acEq_iff {source target : MeTTaIL.AST} (h : MeTTaIL.AC.ACEq acOpCM source target) : RuntimeConfigShape source ↔ RuntimeConfigShape target

AC-equivalence preserves the top-level runtime configuration shape boundary.

theorem CordialMiners.Runtime.runtimeConfigShape_of_acEq {source target : MeTTaIL.AST} (h : MeTTaIL.AC.ACEq acOpCM source target) : RuntimeConfigShape source → RuntimeConfigShape target

Forward form of runtimeConfigShape_acEq_iff.

theorem CordialMiners.Runtime.noEmbeddedConfig_not_rewStep {source target : MeTTaIL.AST} (hclean : NoEmbeddedConfig source) : ¬MeTTaIL.RewStep cmPresentation source target

A clean payload has no Cordial Miners runtime rewrite step inside it.

theorem CordialMiners.Runtime.noEmbeddedConfig_not_rewStepModAC {source target : MeTTaIL.AST} (hclean : NoEmbeddedConfig source) : ¬MeTTaIL.AC.RewStepModAC acOpCM cmPresentation source target

A clean payload has no Cordial Miners runtime rewrite step modulo AC.

theorem CordialMiners.Runtime.runtimeConfigShape_rewStep_top {source target : MeTTaIL.AST} (hshape : RuntimeConfigShape source) (hstep : MeTTaIL.RewStep cmPresentation source target) : MeTTaIL.Reduces cmPresentation source target

Any ordinary runtime step from a shaped configuration fires at the configuration root.

theorem CordialMiners.Runtime.runtimeConfigShape_rewStepModAC_top {source target : MeTTaIL.AST} (hshape : RuntimeConfigShape source) (hstep : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation source target) : ∃ (u : MeTTaIL.AST) (u' : MeTTaIL.AST), MeTTaIL.AC.ACEq acOpCM source u ∧ RuntimeConfigShape u ∧ MeTTaIL.Reduces cmPresentation u u' ∧ MeTTaIL.AC.ACEq acOpCM u' target

A modulo-AC runtime step from a shaped configuration chooses a shaped representative and then fires at that representative's root.

theorem CordialMiners.Runtime.propose_head_modAC (w h ibrest st : MeTTaIL.AST) : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (cmA (inboxA (evProposeA w h) ibrest) st) (cmA ibrest (stateA (proposeA w h) st))

A proposal event at the head of the inbox fires the proposal rule.

theorem CordialMiners.Runtime.order_head_modAC (payload ibrest st : MeTTaIL.AST) : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (cmA (inboxA (evOrderPayloadA payload) ibrest) st) (cmA ibrest (stateA (orderedPrefixPayloadA payload) st))

An order event at the head of the inbox fires the order rule.

theorem CordialMiners.Runtime.qapprove_head_modAC (w h ib rest : MeTTaIL.AST) : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (cmA ib (stateA (proposeA w h) rest)) (cmA ib (stateA (qApproveA w h) (stateA (proposeA w h) rest)))

A proposal fact at the head of the state collection fires the quorum-approval rule.

theorem CordialMiners.Runtime.certify_head_modAC (w h ib rest : MeTTaIL.AST) : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (cmA ib (stateA (qApproveA w h) rest)) (cmA ib (stateA (certThreshA w h) (stateA (qApproveA w h) rest)))

A quorum-approval fact at the head of the state collection fires the certificate rule.

theorem CordialMiners.Runtime.finalize_head_modAC (w h ib rest : MeTTaIL.AST) : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (cmA ib (stateA (certThreshA w h) rest)) (cmA ib (stateA (finalA w h) (stateA (certThreshA w h) rest)))

A threshold-certificate fact at the head of the state collection fires the finality rule.

theorem CordialMiners.Runtime.finalLead_head_modAC (w h ib rest : MeTTaIL.AST) : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (cmA ib (stateA (finalA w h) rest)) (cmA ib (stateA (finalLeaderA w h) (stateA (finalA w h) rest)))

A finality fact at the head of the state collection fires the final-leader rule.

theorem CordialMiners.Runtime.derived_head_decodes {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {ib rest src dst : MeTTaIL.AST} {srcFact dstFact : TrecFact Wave Hash} (hsrcFlat : collectA stateOp src = [src]) (hdstFlat : collectA stateOp dst = [dst]) (hsrc : decodeFactA dW dH src = some srcFact) (hdst : decodeFactA dW dH dst = some dstFact) (step : ∀ (s : TrecState Wave Hash), srcFact ∈ s → s.Step (insert dstFact s)) : (astToState dW dH (cmA ib (stateA src rest))).Step (astToState dW dH (cmA ib (stateA dst (stateA src rest))))

Shared decoding fact for derived rules whose LHS observes one state fact and whose RHS adds one derived fact while keeping the observed fact.

inductive CordialMiners.Runtime.DerivedKind : Type

The four derived Cordial Miners rules share the same runtime shape.

• qapprove : DerivedKind
• certify : DerivedKind
• finalize : DerivedKind
• finalLead : DerivedKind

def CordialMiners.Runtime.DerivedKind.srcA : DerivedKind → MeTTaIL.AST → MeTTaIL.AST → MeTTaIL.AST

The precondition fact matched by a derived rule.

Equations

• CordialMiners.Runtime.DerivedKind.qapprove.srcA x✝¹ x✝ = CordialMiners.Runtime.proposeA x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.certify.srcA x✝¹ x✝ = CordialMiners.Runtime.qApproveA x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.finalize.srcA x✝¹ x✝ = CordialMiners.Runtime.certThreshA x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.finalLead.srcA x✝¹ x✝ = CordialMiners.Runtime.finalA x✝¹ x✝

def CordialMiners.Runtime.DerivedKind.dstA : DerivedKind → MeTTaIL.AST → MeTTaIL.AST → MeTTaIL.AST

The fact inserted by a derived rule.

Equations

• CordialMiners.Runtime.DerivedKind.qapprove.dstA x✝¹ x✝ = CordialMiners.Runtime.qApproveA x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.certify.dstA x✝¹ x✝ = CordialMiners.Runtime.certThreshA x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.finalize.dstA x✝¹ x✝ = CordialMiners.Runtime.finalA x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.finalLead.dstA x✝¹ x✝ = CordialMiners.Runtime.finalLeaderA x✝¹ x✝

def CordialMiners.Runtime.DerivedKind.srcFact {Wave : Type u_1} {Hash : Type u_2} : DerivedKind → Wave → Hash → TrecFact Wave Hash

The decoded precondition fact for a derived rule.

Equations

• CordialMiners.Runtime.DerivedKind.qapprove.srcFact x✝¹ x✝ = CordialMiners.TrecFact.propose x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.certify.srcFact x✝¹ x✝ = CordialMiners.TrecFact.qApprove x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.finalize.srcFact x✝¹ x✝ = CordialMiners.TrecFact.certThresh x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.finalLead.srcFact x✝¹ x✝ = CordialMiners.TrecFact.final x✝¹ x✝

def CordialMiners.Runtime.DerivedKind.dstFact {Wave : Type u_1} {Hash : Type u_2} : DerivedKind → Wave → Hash → TrecFact Wave Hash

The decoded inserted fact for a derived rule.

Equations

• CordialMiners.Runtime.DerivedKind.qapprove.dstFact x✝¹ x✝ = CordialMiners.TrecFact.qApprove x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.certify.dstFact x✝¹ x✝ = CordialMiners.TrecFact.certThresh x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.finalize.dstFact x✝¹ x✝ = CordialMiners.TrecFact.final x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.finalLead.dstFact x✝¹ x✝ = CordialMiners.TrecFact.finalLeader x✝¹ x✝

inductive CordialMiners.Runtime.DerivedKind.Side : Type

Select the source or destination side of a derived rule.

• src : Side
• dst : Side

def CordialMiners.Runtime.DerivedKind.sideA : Side → DerivedKind → MeTTaIL.AST → MeTTaIL.AST → MeTTaIL.AST

The AST fact on one side of a derived rule.

Equations

• CordialMiners.Runtime.DerivedKind.sideA CordialMiners.Runtime.DerivedKind.Side.src x✝² x✝¹ x✝ = x✝².srcA x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.sideA CordialMiners.Runtime.DerivedKind.Side.dst x✝² x✝¹ x✝ = x✝².dstA x✝¹ x✝

def CordialMiners.Runtime.DerivedKind.sideFact {Wave : Type u_1} {Hash : Type u_2} : Side → DerivedKind → Wave → Hash → TrecFact Wave Hash

The decoded coarse fact on one side of a derived rule.

Equations

• CordialMiners.Runtime.DerivedKind.sideFact CordialMiners.Runtime.DerivedKind.Side.src x✝² x✝¹ x✝ = x✝².srcFact x✝¹ x✝
• CordialMiners.Runtime.DerivedKind.sideFact CordialMiners.Runtime.DerivedKind.Side.dst x✝² x✝¹ x✝ = x✝².dstFact x✝¹ x✝

theorem CordialMiners.Runtime.DerivedKind.sideFlat (side : Side) (k : DerivedKind) (w h : MeTTaIL.AST) : collectA stateOp (sideA side k w h) = [sideA side k w h]

Derived-rule side ASTs are leaves of the state AC collection.

theorem CordialMiners.Runtime.DerivedKind.decodeSide {Wave : Type u_1} {Hash : Type u_2} (side : Side) (k : DerivedKind) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {w h : MeTTaIL.AST} {w' : Wave} {h' : Hash} (hw : dW w = some w') (hh : dH h = some h') : decodeFactA dW dH (sideA side k w h) = some (sideFact side k w' h')

Decoding either side AST recovers the corresponding coarse fact.

theorem CordialMiners.Runtime.DerivedKind.step {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (k : DerivedKind) (s : TrecState Wave Hash) (w : Wave) (h : Hash) (hpre : k.srcFact w h ∈ s) : s.Step (insert (k.dstFact w h) s)

The decoded coarse step for a derived rule.

theorem CordialMiners.Runtime.derivedKind_head_decodes {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (k : DerivedKind) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {w h ib rest : MeTTaIL.AST} {w' : Wave} {h' : Hash} (hw : dW w = some w') (hh : dH h = some h') : (astToState dW dH (cmA ib (stateA (k.srcA w h) rest))).Step (astToState dW dH (cmA ib (stateA (k.dstA w h) (stateA (k.srcA w h) rest))))

Any derived Cordial Miners head redex decodes to its corresponding coarse step.

theorem CordialMiners.Runtime.derived_step_of_decode {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (k : DerivedKind) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {s : TrecState Wave Hash} {w : Wave} {h : Hash} {target : MeTTaIL.AST} (hpre : k.srcFact w h ∈ s) (hdecode : astToState dW dH target = insert (k.dstFact w h) s) : s.Step (astToState dW dH target)

A decoded derived-rule target is a real coarse derived step.

theorem CordialMiners.Runtime.propose_head_decodes {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {w h ibrest st : MeTTaIL.AST} {w' : Wave} {h' : Hash} (hw : dW w = some w') (hh : dH h = some h') : (astToState dW dH (cmA (inboxA (evProposeA w h) ibrest) st)).Step (astToState dW dH (cmA ibrest (stateA (proposeA w h) st)))

A proposal head redex decodes to the coarse proposal step.

theorem CordialMiners.Runtime.order_head_decodes {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {payload ibrest st : MeTTaIL.AST} {hs : List Hash} (hp : decodeOrderedPayloadA dH [payload] = some hs) : (astToState dW dH (cmA (inboxA (evOrderPayloadA payload) ibrest) st)).Step (astToState dW dH (cmA ibrest (stateA (orderedPrefixPayloadA payload) st)))

An order head redex decodes to the coarse ordering step.

theorem CordialMiners.Runtime.decodeStateA_stateA_none {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {fact rest : MeTTaIL.AST} (hflat : collectA stateOp fact = [fact]) (hdecode : decodeFactA dW dH fact = none) : decodeStateA dW dH (stateA fact rest) = decodeStateA dW dH rest

Adding a state-collection leaf that does not decode is a decoded stutter.

theorem CordialMiners.Runtime.propose_head_backward {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (w h ibrest st : MeTTaIL.AST) : (astToState dW dH (cmA (inboxA (evProposeA w h) ibrest) st)).Step (astToState dW dH (cmA ibrest (stateA (proposeA w h) st))) ∨ astToState dW dH (cmA (inboxA (evProposeA w h) ibrest) st) = astToState dW dH (cmA ibrest (stateA (proposeA w h) st))

A proposal head redex decodes to a coarse proposal step, or stutters if the event payload is undecodable.

theorem CordialMiners.Runtime.order_head_backward {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (payload ibrest st : MeTTaIL.AST) : (astToState dW dH (cmA (inboxA (evOrderPayloadA payload) ibrest) st)).Step (astToState dW dH (cmA ibrest (stateA (orderedPrefixPayloadA payload) st))) ∨ astToState dW dH (cmA (inboxA (evOrderPayloadA payload) ibrest) st) = astToState dW dH (cmA ibrest (stateA (orderedPrefixPayloadA payload) st))

An order head redex decodes to a coarse ordering step, or stutters if the payload is undecodable.

theorem CordialMiners.Runtime.qapprove_head_decodes {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {w h ib rest : MeTTaIL.AST} {w' : Wave} {h' : Hash} (hw : dW w = some w') (hh : dH h = some h') : (astToState dW dH (cmA ib (stateA (proposeA w h) rest))).Step (astToState dW dH (cmA ib (stateA (qApproveA w h) (stateA (proposeA w h) rest))))

A quorum-approval head redex decodes to the coarse quorum-approval step.

theorem CordialMiners.Runtime.certify_head_decodes {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {w h ib rest : MeTTaIL.AST} {w' : Wave} {h' : Hash} (hw : dW w = some w') (hh : dH h = some h') : (astToState dW dH (cmA ib (stateA (qApproveA w h) rest))).Step (astToState dW dH (cmA ib (stateA (certThreshA w h) (stateA (qApproveA w h) rest))))

A certificate head redex decodes to the coarse certificate step.

theorem CordialMiners.Runtime.finalize_head_decodes {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {w h ib rest : MeTTaIL.AST} {w' : Wave} {h' : Hash} (hw : dW w = some w') (hh : dH h = some h') : (astToState dW dH (cmA ib (stateA (certThreshA w h) rest))).Step (astToState dW dH (cmA ib (stateA (finalA w h) (stateA (certThreshA w h) rest))))

A finality head redex decodes to the coarse finality step.

theorem CordialMiners.Runtime.finalLead_head_decodes {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {w h ib rest : MeTTaIL.AST} {w' : Wave} {h' : Hash} (hw : dW w = some w') (hh : dH h = some h') : (astToState dW dH (cmA ib (stateA (finalA w h) rest))).Step (astToState dW dH (cmA ib (stateA (finalLeaderA w h) (stateA (finalA w h) rest))))

A final-leader head redex decodes to the coarse final-leader step.

theorem CordialMiners.Runtime.derivedKind_head_backward {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (k : DerivedKind) (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (w h ib rest : MeTTaIL.AST) : (astToState dW dH (cmA ib (stateA (k.srcA w h) rest))).Step (astToState dW dH (cmA ib (stateA (k.dstA w h) (stateA (k.srcA w h) rest)))) ∨ astToState dW dH (cmA ib (stateA (k.srcA w h) rest)) = astToState dW dH (cmA ib (stateA (k.dstA w h) (stateA (k.srcA w h) rest)))

A derived-rule head redex decodes to a coarse derived step, or stutters if its fields are undecodable.

theorem CordialMiners.Runtime.qapprove_head_backward {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (w h ib rest : MeTTaIL.AST) : (astToState dW dH (cmA ib (stateA (proposeA w h) rest))).Step (astToState dW dH (cmA ib (stateA (qApproveA w h) (stateA (proposeA w h) rest)))) ∨ astToState dW dH (cmA ib (stateA (proposeA w h) rest)) = astToState dW dH (cmA ib (stateA (qApproveA w h) (stateA (proposeA w h) rest)))

A quorum-approval head redex is backward-sound up to decoded stutter.

theorem CordialMiners.Runtime.certify_head_backward {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (w h ib rest : MeTTaIL.AST) : (astToState dW dH (cmA ib (stateA (qApproveA w h) rest))).Step (astToState dW dH (cmA ib (stateA (certThreshA w h) (stateA (qApproveA w h) rest)))) ∨ astToState dW dH (cmA ib (stateA (qApproveA w h) rest)) = astToState dW dH (cmA ib (stateA (certThreshA w h) (stateA (qApproveA w h) rest)))

A certificate head redex is backward-sound up to decoded stutter.

theorem CordialMiners.Runtime.finalize_head_backward {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (w h ib rest : MeTTaIL.AST) : (astToState dW dH (cmA ib (stateA (certThreshA w h) rest))).Step (astToState dW dH (cmA ib (stateA (finalA w h) (stateA (certThreshA w h) rest)))) ∨ astToState dW dH (cmA ib (stateA (certThreshA w h) rest)) = astToState dW dH (cmA ib (stateA (finalA w h) (stateA (certThreshA w h) rest)))

A finality head redex is backward-sound up to decoded stutter.

theorem CordialMiners.Runtime.finalLead_head_backward {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (w h ib rest : MeTTaIL.AST) : (astToState dW dH (cmA ib (stateA (finalA w h) rest))).Step (astToState dW dH (cmA ib (stateA (finalLeaderA w h) (stateA (finalA w h) rest)))) ∨ astToState dW dH (cmA ib (stateA (finalA w h) rest)) = astToState dW dH (cmA ib (stateA (finalLeaderA w h) (stateA (finalA w h) rest)))

A final-leader head redex is backward-sound up to decoded stutter.

theorem CordialMiners.Runtime.runtime_root_step_backward {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {source target : MeTTaIL.AST} (hred : MeTTaIL.Reduces cmPresentation source target) : (astToState dW dH source).Step (astToState dW dH target) ∨ astToState dW dH source = astToState dW dH target

A direct root reduction by the Cordial Miners presentation decodes to a coarse step or to a decoded stutter.

theorem CordialMiners.Runtime.runtime_step_direct {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {source target : MeTTaIL.AST} (hshape : RuntimeConfigShape source) (hstep : MeTTaIL.RewStep cmPresentation source target) : (astToState dW dH source).Step (astToState dW dH target) ∨ astToState dW dH source = astToState dW dH target

A direct contextual runtime step from a shaped configuration decodes to a coarse step or stutter. The shape invariant rules out every strict-subterm protocol redex.

theorem CordialMiners.Runtime.runtime_step_backward_of_astToState_acEq {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hAC : ∀ {a b : MeTTaIL.AST}, MeTTaIL.AC.ACEq acOpCM a b → astToState dW dH a = astToState dW dH b) {source target : MeTTaIL.AST} (hshape : RuntimeConfigShape source) (hstep : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation source target) : (astToState dW dH source).Step (astToState dW dH target) ∨ astToState dW dH source = astToState dW dH target

A modulo-AC runtime step from a shaped configuration decodes to a coarse step or stutter whenever the selected decoder is invariant under the runtime AC equivalence.

theorem CordialMiners.Runtime.decodeListA_acEq_of_decoder_acEq {α : Type u_1} (d : MeTTaIL.AST → Option α) (hd : ∀ {a b : MeTTaIL.AST}, MeTTaIL.AC.ACEq acOpCM a b → d a = d b) {a b : MeTTaIL.AST} (h : MeTTaIL.AC.ACEq acOpCM a b) : decodeListA d a = decodeListA d b

List decoding respects runtime AC-equivalence when the element decoder does.

theorem CordialMiners.Runtime.decodeFactA_acEq_of_decoders_acEq {Wave : Type u_1} {Hash : Type u_2} (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hW : ∀ {a b : MeTTaIL.AST}, MeTTaIL.AC.ACEq acOpCM a b → dW a = dW b) (hH : ∀ {a b : MeTTaIL.AST}, MeTTaIL.AC.ACEq acOpCM a b → dH a = dH b) {a b : MeTTaIL.AST} (h : MeTTaIL.AC.ACEq acOpCM a b) : decodeFactA dW dH a = decodeFactA dW dH b

Fact decoding respects runtime AC-equivalence when both field decoders do.

theorem CordialMiners.Runtime.decodeStateA_acEq_of_decoders_acEq {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hW : ∀ {a b : MeTTaIL.AST}, MeTTaIL.AC.ACEq acOpCM a b → dW a = dW b) (hH : ∀ {a b : MeTTaIL.AST}, MeTTaIL.AC.ACEq acOpCM a b → dH a = dH b) {a b : MeTTaIL.AST} (h : MeTTaIL.AC.ACEq acOpCM a b) : decodeStateA dW dH a = decodeStateA dW dH b

State decoding respects runtime AC-equivalence when both field decoders do.

theorem CordialMiners.Runtime.astToState_acEq_of_decoders_acEq {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hW : ∀ {a b : MeTTaIL.AST}, MeTTaIL.AC.ACEq acOpCM a b → dW a = dW b) (hH : ∀ {a b : MeTTaIL.AST}, MeTTaIL.AC.ACEq acOpCM a b → dH a = dH b) {a b : MeTTaIL.AST} (h : MeTTaIL.AC.ACEq acOpCM a b) : astToState dW dH a = astToState dW dH b

Configuration decoding respects runtime AC-equivalence when both field decoders do.

theorem CordialMiners.Runtime.runtime_step_backward_of_decoders_acEq {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (hW : ∀ {a b : MeTTaIL.AST}, MeTTaIL.AC.ACEq acOpCM a b → dW a = dW b) (hH : ∀ {a b : MeTTaIL.AST}, MeTTaIL.AC.ACEq acOpCM a b → dH a = dH b) {source target : MeTTaIL.AST} (hshape : RuntimeConfigShape source) (hstep : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation source target) : (astToState dW dH source).Step (astToState dW dH target) ∨ astToState dW dH source = astToState dW dH target

A modulo-AC runtime step is backward-sound for any field decoders that respect runtime AC.

theorem CordialMiners.Runtime.collection_second_to_head (op : MeTTaIL.Label) (hac : acOpCM op = true) (first second rest : MeTTaIL.AST) : MeTTaIL.AC.ACEq acOpCM (consA op first (consA op second rest)) (consA op second (consA op first rest))

AC can move the second element of an encoded binary collection to the head.

theorem CordialMiners.Runtime.inbox_second_to_head (first second rest st : MeTTaIL.AST) : MeTTaIL.AC.ACEq acOpCM (cmA (inboxA first (inboxA second rest)) st) (cmA (inboxA second (inboxA first rest)) st)

AC can move the second inbox event to the head while preserving the rest of the configuration.

theorem CordialMiners.Runtime.state_cons_tail_fact_to_head {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (head fact : TrecFact Wave Hash) {tail : List (TrecFact Wave Hash)} {rest : MeTTaIL.AST} (hrest : MeTTaIL.AC.ACEq acOpCM (encStateList eW eH tail) (stateA (encodeFactA eW eH fact) rest)) : MeTTaIL.AC.ACEq acOpCM (stateA (encodeFactA eW eH head) (encStateList eW eH tail)) (stateA (encodeFactA eW eH fact) (stateA (encodeFactA eW eH head) rest))

If a tail fact has been moved to the state head, it can pass the cons head modulo AC.

theorem CordialMiners.Runtime.encStateList_mem_head {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) {facts : List (TrecFact Wave Hash)} {fact : TrecFact Wave Hash} (hmem : fact ∈ facts) : ∃ (rest : MeTTaIL.AST), MeTTaIL.AC.ACEq acOpCM (encStateList eW eH facts) (stateA (encodeFactA eW eH fact) rest)

Any fact in an encoded state list can be moved to the AC head.

theorem CordialMiners.Runtime.decodeStateA_stateA_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 (stateA (encodeFactA eW eH fact) rest) = insert fact (decodeStateA dW dH rest)

A presentation state node whose head is an encoded fact decodes as finite-set insertion.

theorem CordialMiners.Runtime.encStateList_mem_head_decodes {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)} {fact : TrecFact Wave Hash} (hmem : fact ∈ facts) : ∃ (rest : MeTTaIL.AST), MeTTaIL.AC.ACEq acOpCM (encStateList eW eH facts) (stateA (encodeFactA eW eH fact) rest) ∧ decodeStateA dW dH (stateA (encodeFactA eW eH fact) rest) = facts.toFinset

Moving a state-list fact to the AC head preserves the decoded finite state.

theorem CordialMiners.Runtime.encInbox_mem_head {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) {events : List (Event Wave Hash)} {event : Event Wave Hash} (hmem : event ∈ events) : ∃ (rest : MeTTaIL.AST), MeTTaIL.AC.ACEq acOpCM (encInbox eW eH events) (inboxA (encodeEventA eW eH event) rest)

Any event in an encoded inbox can be moved to the AC head.

theorem CordialMiners.Runtime.rewStepModAC_ac_left {p : MeTTaIL.Presentation} {source head target : MeTTaIL.AST} (hsource : MeTTaIL.AC.ACEq acOpCM source head) (hstep : MeTTaIL.AC.RewStepModAC acOpCM p head target) : MeTTaIL.AC.RewStepModAC acOpCM p source target

A modulo-AC step may start from any AC-equivalent left representative.

theorem CordialMiners.Runtime.DerivedKind.encodeSrc {Wave : Type u_1} {Hash : Type u_2} (k : DerivedKind) (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (w : Wave) (h : Hash) : encodeFactA eW eH (k.srcFact w h) = k.srcA (eW w) (eH h)

Encoding the source fact of a derived rule gives the source AST used by the presentation.

theorem CordialMiners.Runtime.DerivedKind.encodeDst {Wave : Type u_1} {Hash : Type u_2} (k : DerivedKind) (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (w : Wave) (h : Hash) : encodeFactA eW eH (k.dstFact w h) = k.dstA (eW w) (eH h)

Encoding the destination fact of a derived rule gives the destination AST used by the presentation.

theorem CordialMiners.Runtime.derivedKind_head_modAC (k : DerivedKind) (w h ib rest : MeTTaIL.AST) : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (cmA ib (stateA (k.srcA w h) rest)) (cmA ib (stateA (k.dstA w h) (stateA (k.srcA w h) rest)))

Any derived-rule head redex is a runtime step modulo AC.

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

The state fact inserted by an input event.

Equations

• CordialMiners.Runtime.eventStateFactA eW eH (CordialMiners.Runtime.Event.propose w h) = CordialMiners.Runtime.proposeA (eW w) (eH h)
• CordialMiners.Runtime.eventStateFactA eW eH (CordialMiners.Runtime.Event.order hs) = CordialMiners.Runtime.orderedPrefixPayloadA (CordialMiners.Runtime.encodeListA eH hs)

def CordialMiners.Runtime.eventFact {Wave : Type u_1} {Hash : Type u_2} : Event Wave Hash → TrecFact Wave Hash

The coarse fact inserted by an input event.

Equations

• CordialMiners.Runtime.eventFact (CordialMiners.Runtime.Event.propose w h) = CordialMiners.TrecFact.propose w h
• CordialMiners.Runtime.eventFact (CordialMiners.Runtime.Event.order hs) = CordialMiners.TrecFact.orderedPrefix hs

theorem CordialMiners.Runtime.eventStateFactA_eq_encodeFactA {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (event : Event Wave Hash) : eventStateFactA eW eH event = encodeFactA eW eH (eventFact event)

Event state facts are the ordinary AST encodings of their coarse facts.

theorem CordialMiners.Runtime.event_step_of_decode {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) (s : TrecState Wave Hash) (event : Event Wave Hash) {target : MeTTaIL.AST} (hdecode : astToState dW dH target = insert (eventFact event) s) : s.Step (astToState dW dH target)

A decoded input-event target is a real coarse proposal or ordering step.

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

The target configuration after an input event fires.

Equations

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

theorem CordialMiners.Runtime.event_head_modAC {Wave : Type u_1} {Hash : Type u_2} (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) (event : Event Wave Hash) (rest st : MeTTaIL.AST) : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (cmA (inboxA (encodeEventA eW eH event) rest) st) (cmA rest (stateA (eventStateFactA eW eH event) st))

An input-event head redex is a runtime step modulo AC.

theorem CordialMiners.Runtime.event_inbox_mem_modAC {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)} {event : Event Wave Hash} (hmem : event ∈ events) : ∃ (rest : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfigList eW eH events facts) (eventTargetA eW eH facts event rest)

Any input event in the encoded inbox can fire modulo AC.

theorem CordialMiners.Runtime.event_inbox_mem_forward_decode {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) {events : List (Event Wave Hash)} {facts : List (TrecFact Wave Hash)} {event : Event Wave Hash} (hmem : event ∈ events) : ∃ (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfigList eW eH events facts) target ∧ astToState dW dH target = insert (eventFact event) facts.toFinset

Any input event in the encoded inbox has a runtime step whose target decodes to the inserted fact.

theorem CordialMiners.Runtime.event_inbox_mem_forward_step {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) {events : List (Event Wave Hash)} {facts : List (TrecFact Wave Hash)} {event : Event Wave Hash} (hmem : event ∈ events) : ∃ (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfigList eW eH events facts) target ∧ TrecState.Step facts.toFinset (astToState dW dH target)

Any input event in the encoded inbox decodes to a genuine coarse protocol step.

theorem CordialMiners.Runtime.runtime_step_stutter_of_inserted_fact_mem {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (dW : MeTTaIL.AST → Option Wave) (dH : MeTTaIL.AST → Option Hash) {source target : MeTTaIL.AST} {facts : List (TrecFact Wave Hash)} {fact : TrecFact Wave Hash} (hrel : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation source target) (hdecode : astToState dW dH target = insert fact facts.toFinset) (hfact : fact ∈ facts) : ∃ (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation source target ∧ astToState dW dH target = facts.toFinset

If a runtime witness decodes to insertion of an already-present fact, it is a decoded stutter.

theorem CordialMiners.Runtime.event_inbox_mem_forward_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) {events : List (Event Wave Hash)} {facts : List (TrecFact Wave Hash)} {event : Event Wave Hash} (hmem : event ∈ events) (hfact : eventFact event ∈ facts) : ∃ (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfigList eW eH events facts) target ∧ astToState dW dH target = facts.toFinset

If an input event adds a fact already decoded in the state, the runtime step is a decoded stutter.

theorem CordialMiners.Runtime.propose_inbox_mem_modAC {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)} {w : Wave} {h : Hash} (hmem : Event.propose w h ∈ events) : ∃ (rest : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfigList eW eH events facts) (cmA rest (stateA (proposeA (eW w) (eH h)) (encStateList eW eH facts)))

A proposal event anywhere in the encoded inbox can fire modulo AC.

theorem CordialMiners.Runtime.order_inbox_mem_modAC {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)} {hs : List Hash} (hmem : Event.order hs ∈ events) : ∃ (rest : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfigList eW eH events facts) (cmA rest (stateA (orderedPrefixPayloadA (encodeListA eH hs)) (encStateList eW eH facts)))

An order event anywhere in the encoded inbox can fire modulo AC.

theorem CordialMiners.Runtime.derived_state_head_modAC {Wave : Type u_1} {Hash : Type u_2} (k : DerivedKind) (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) {events : List (Event Wave Hash)} {facts : List (TrecFact Wave Hash)} {w : Wave} {h : Hash} {rest : MeTTaIL.AST} (hstate : MeTTaIL.AC.ACEq acOpCM (encStateList eW eH facts) (stateA (k.srcA (eW w) (eH h)) rest)) : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfigList eW eH events facts) (cmA (encInbox eW eH events) (stateA (k.dstA (eW w) (eH h)) (stateA (k.srcA (eW w) (eH h)) rest)))

A headed derived-rule source fact gives the matching runtime step.

theorem CordialMiners.Runtime.derived_state_mem_modAC {Wave : Type u_1} {Hash : Type u_2} (k : DerivedKind) (eW : Wave → MeTTaIL.AST) (eH : Hash → MeTTaIL.AST) {events : List (Event Wave Hash)} {facts : List (TrecFact Wave Hash)} {w : Wave} {h : Hash} (hmem : k.srcFact w h ∈ facts) : ∃ (rest : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfigList eW eH events facts) (cmA (encInbox eW eH events) (stateA (k.dstA (eW w) (eH h)) (stateA (k.srcA (eW w) (eH h)) rest)))

A derived fact anywhere in the encoded state can fire its derived rule modulo AC.

theorem CordialMiners.Runtime.derived_state_mem_forward_decode {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (k : DerivedKind) (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)} {facts : List (TrecFact Wave Hash)} {w : Wave} {h : Hash} (hmem : k.srcFact w h ∈ facts) : ∃ (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfigList eW eH events facts) target ∧ astToState dW dH target = insert (k.dstFact w h) facts.toFinset

A derived fact anywhere in the encoded state has a runtime step whose target decodes to the inserted derived fact.

theorem CordialMiners.Runtime.derived_state_mem_forward_step {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (k : DerivedKind) (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)} {facts : List (TrecFact Wave Hash)} {w : Wave} {h : Hash} (hmem : k.srcFact w h ∈ facts) : ∃ (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfigList eW eH events facts) target ∧ TrecState.Step facts.toFinset (astToState dW dH target)

Any derived-rule precondition in the encoded state decodes to a genuine coarse protocol step.

theorem CordialMiners.Runtime.derived_state_mem_forward_stutter {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (k : DerivedKind) (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)} {facts : List (TrecFact Wave Hash)} {w : Wave} {h : Hash} (hsrc : k.srcFact w h ∈ facts) (hdst : k.dstFact w h ∈ facts) : ∃ (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfigList eW eH events facts) target ∧ astToState dW dH target = facts.toFinset

If a derived rule adds a fact already decoded in the state, the runtime step is a decoded stutter.

theorem CordialMiners.Runtime.event_forward_decode {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) (s : TrecState Wave Hash) (event : Event Wave Hash) : ∃ (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfig eW eH [event] s) target ∧ astToState dW dH target = insert (eventFact event) s

A single input event supplied in the inbox has a runtime step whose target decodes to the inserted coarse fact.

theorem CordialMiners.Runtime.event_forward_step {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) (s : TrecState Wave Hash) (event : Event Wave Hash) : ∃ (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfig eW eH [event] s) target ∧ s.Step (astToState dW dH target)

A single input event supplied in the inbox has a runtime step that decodes to a coarse protocol step.

theorem CordialMiners.Runtime.event_forward_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) {s : TrecState Wave Hash} {event : Event Wave Hash} (hfact : eventFact event ∈ s) : ∃ (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfig eW eH [event] s) target ∧ astToState dW dH target = s

A single input event that adds an already-present fact is a decoded stutter.

theorem CordialMiners.Runtime.derived_step_forward_decode {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (k : DerivedKind) (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) {s : TrecState Wave Hash} {w : Wave} {h : Hash} (hpre : k.srcFact w h ∈ s) : ∃ (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfig eW eH [] s) target ∧ astToState dW dH target = insert (k.dstFact w h) s

A derived-rule precondition in a finite state has a runtime step whose target decodes to the corresponding inserted fact.

theorem CordialMiners.Runtime.derived_step_forward_step {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (k : DerivedKind) (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) {s : TrecState Wave Hash} {w : Wave} {h : Hash} (hpre : k.srcFact w h ∈ s) : ∃ (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfig eW eH [] s) target ∧ s.Step (astToState dW dH target)

A derived-rule precondition in a finite state has a runtime step that decodes to a coarse protocol step.

theorem CordialMiners.Runtime.derived_step_forward_stutter {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (k : DerivedKind) (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) {s : TrecState Wave Hash} {w : Wave} {h : Hash} (hsrc : k.srcFact w h ∈ s) (hdst : k.dstFact w h ∈ s) : ∃ (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfig eW eH [] s) target ∧ astToState dW dH target = s

A derived rule that adds an already-present fact is a decoded stutter.

def CordialMiners.Runtime.RuntimeStepDecodesTo {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) (events : List (Event Wave Hash)) (s targetState : TrecState Wave Hash) : Prop

A runtime step witness whose target decodes to a chosen coarse state.

Equations

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

def CordialMiners.Runtime.RuntimeStepIsCoarseStep {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) (events : List (Event Wave Hash)) (s : TrecState Wave Hash) : Prop

A runtime step witness whose decoded target is a coarse protocol successor.

Equations

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

def CordialMiners.Runtime.RuntimeForwardComplete {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) : Prop

Every coarse protocol step has a runtime witness that decodes to its target.

Equations

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

def CordialMiners.Runtime.RuntimeEventSound {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) : Prop

One supplied input event runs to a decoded coarse protocol successor.

Equations

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

def CordialMiners.Runtime.RuntimeDerivedSound {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) : Prop

One derived-rule precondition fact runs to a decoded coarse protocol successor.

Equations

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

def CordialMiners.Runtime.RuntimeEventStutterSound {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) : Prop

A duplicate input event runs to a decoded stutter.

Equations

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

def CordialMiners.Runtime.RuntimeDerivedStutterSound {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) : Prop

A derived rule whose output fact is already present runs to a decoded stutter.

Equations

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

def CordialMiners.Runtime.RuntimeScopedBridge {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) : Prop

The scoped runtime bridge surface currently proved for the Cordial Miners presentation.

Equations

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

theorem CordialMiners.Runtime.trec_step_forward_decode {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) {s s' : TrecState Wave Hash} (hstep : s.Step s') : ∃ (events : List (Event Wave Hash)) (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfig eW eH events s) target ∧ astToState dW dH target = s'

Every coarse TrecState.Step has a matching runtime step whose target decodes to the coarse target. The theorem is stated through astToState because runtime collections are multisets while TrecState is a Finset. Re-adding an existing fact duplicates an AST leaf but decodes to the same finite set.

theorem CordialMiners.Runtime.trec_step_forward_reachable {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) {s s' : TrecState Wave Hash} (hreach : Relation.ReflTransGen TrecState.Step ∅ s) (hstep : s.Step s') : ∃ (events : List (Event Wave Hash)) (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfig eW eH events s) target ∧ astToState dW dH target = s' ∧ Relation.ReflTransGen TrecState.Step ∅ (astToState dW dH target)

If the coarse source is reachable, the decoded target produced by the runtime forward witness is reachable too. The proved forward bridge gives this reachability transfer.

theorem CordialMiners.Runtime.trec_step_forward_wf {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) {s s' : TrecState Wave Hash} (hreach : Relation.ReflTransGen TrecState.Step ∅ s) (hstep : s.Step s') : ∃ (events : List (Event Wave Hash)) (target : MeTTaIL.AST), MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (encConfig eW eH events s) target ∧ astToState dW dH target = s' ∧ TrecWF (astToState dW dH target)

Coarse well-formedness transfers to the decoded target of the runtime witness produced by the forward bridge, provided the source state was coarse-reachable.

theorem CordialMiners.Runtime.scoped_runtime_bridge {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) : RuntimeScopedBridge eW eH dW dH

The proved scoped bridge for the declared Cordial Miners runtime fragments.

The first component is forward completeness for every coarse TrecState.Step. The next two components are decoded soundness facts for the input-event and derived-rule fragments. The last two components are decoded stutter facts for duplicate input events and duplicate derived facts. The theorem is not the full arbitrary-RewStepModAC backward theorem.

theorem CordialMiners.Runtime.propose_second_inbox_modAC (first w h ibrest st : MeTTaIL.AST) : MeTTaIL.AC.RewStepModAC acOpCM cmPresentation (cmA (inboxA first (inboxA (evProposeA w h) ibrest)) st) (cmA (inboxA first ibrest) (stateA (proposeA w h) st))

A proposal event in the second inbox position can fire modulo AC, leaving the first event pending.