def CordialMiners.Runtime.acOpCM (l : MeTTaIL.Label) : Bool

Cordial Miners treats both state and inbox as AC collections.

Equations

• CordialMiners.Runtime.acOpCM l = (l == CordialMiners.Runtime.stateOp || l == CordialMiners.Runtime.inboxOp)

def CordialMiners.Runtime.vA (name : String) : MeTTaIL.AST

Base variable pattern.

Equations

• CordialMiners.Runtime.vA name = MeTTaIL.AST.var (MeTTaIL.DottedPath.base name)

def CordialMiners.Runtime.stateA (head rest : MeTTaIL.AST) : MeTTaIL.AST

State collection pattern or constructor.

Equations

• CordialMiners.Runtime.stateA head rest = MeTTaIL.AST.sexp CordialMiners.Runtime.stateOp [head, rest]

def CordialMiners.Runtime.inboxA (head rest : MeTTaIL.AST) : MeTTaIL.AST

Inbox collection pattern or constructor.

Equations

• CordialMiners.Runtime.inboxA head rest = MeTTaIL.AST.sexp CordialMiners.Runtime.inboxOp [head, rest]

def CordialMiners.Runtime.cmA (ib st : MeTTaIL.AST) : MeTTaIL.AST

Runtime configuration constructor.

Equations

• CordialMiners.Runtime.cmA ib st = MeTTaIL.AST.sexp CordialMiners.Runtime.cmOp [ib, st]

def CordialMiners.Runtime.proposeA (w h : MeTTaIL.AST) : MeTTaIL.AST

Equations

• CordialMiners.Runtime.proposeA w h = CordialMiners.Runtime.appA "propose" [w, h]

def CordialMiners.Runtime.qApproveA (w h : MeTTaIL.AST) : MeTTaIL.AST

Equations

• CordialMiners.Runtime.qApproveA w h = CordialMiners.Runtime.appA "q-approve" [w, h]

def CordialMiners.Runtime.certThreshA (w h : MeTTaIL.AST) : MeTTaIL.AST

Equations

• CordialMiners.Runtime.certThreshA w h = CordialMiners.Runtime.appA "cert-threshold" [w, h]

def CordialMiners.Runtime.finalA (w h : MeTTaIL.AST) : MeTTaIL.AST

Equations

• CordialMiners.Runtime.finalA w h = CordialMiners.Runtime.appA "final" [w, h]

def CordialMiners.Runtime.finalLeaderA (w h : MeTTaIL.AST) : MeTTaIL.AST

Equations

• CordialMiners.Runtime.finalLeaderA w h = CordialMiners.Runtime.appA "final-leader" [w, h]

def CordialMiners.Runtime.orderedPrefixPayloadA (payload : MeTTaIL.AST) : MeTTaIL.AST

Equations

• CordialMiners.Runtime.orderedPrefixPayloadA payload = CordialMiners.Runtime.appA "ordered-prefix" [payload]

def CordialMiners.Runtime.evProposeA (w h : MeTTaIL.AST) : MeTTaIL.AST

Equations

• CordialMiners.Runtime.evProposeA w h = CordialMiners.Runtime.appA "ev-propose" [w, h]

def CordialMiners.Runtime.evOrderPayloadA (payload : MeTTaIL.AST) : MeTTaIL.AST

Equations

• CordialMiners.Runtime.evOrderPayloadA payload = CordialMiners.Runtime.appA "ev-order" [payload]

def CordialMiners.Runtime.wVar : MeTTaIL.AST

Equations

• CordialMiners.Runtime.wVar = CordialMiners.Runtime.vA "w"

def CordialMiners.Runtime.hVar : MeTTaIL.AST

Equations

• CordialMiners.Runtime.hVar = CordialMiners.Runtime.vA "h"

def CordialMiners.Runtime.hsVar : MeTTaIL.AST

Equations

• CordialMiners.Runtime.hsVar = CordialMiners.Runtime.vA "hs"

def CordialMiners.Runtime.restVar : MeTTaIL.AST

Equations

• CordialMiners.Runtime.restVar = CordialMiners.Runtime.vA "rest"

def CordialMiners.Runtime.stVar : MeTTaIL.AST

Equations

• CordialMiners.Runtime.stVar = CordialMiners.Runtime.vA "st"

def CordialMiners.Runtime.ibVar : MeTTaIL.AST

Equations

• CordialMiners.Runtime.ibVar = CordialMiners.Runtime.vA "ib"

def CordialMiners.Runtime.ibRestVar : MeTTaIL.AST

Equations

• CordialMiners.Runtime.ibRestVar = CordialMiners.Runtime.vA "ibrest"

def CordialMiners.Runtime.baseDecl (name : String) (lhs rhs : MeTTaIL.AST) : MeTTaIL.RewriteDecl

Build a named base rewrite declaration.

Equations

• CordialMiners.Runtime.baseDecl name lhs rhs = { name := name, rw := MeTTaIL.Rewrite.base lhs rhs }

def CordialMiners.Runtime.proposeRule : MeTTaIL.RewriteDecl

Consume a proposal event and add the corresponding propose fact.

Equations

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

def CordialMiners.Runtime.qapproveRule : MeTTaIL.RewriteDecl

A proposal fact enables a quorum-approval fact.

Equations

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

def CordialMiners.Runtime.certifyRule : MeTTaIL.RewriteDecl

A quorum-approval fact enables a threshold-certificate fact.

Equations

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

def CordialMiners.Runtime.finalizeRule : MeTTaIL.RewriteDecl

A threshold-certificate fact enables a finality fact.

Equations

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

def CordialMiners.Runtime.finalLeadRule : MeTTaIL.RewriteDecl

A finality fact enables the final-leader fact.

Equations

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

def CordialMiners.Runtime.orderRule : MeTTaIL.RewriteDecl

Consume an ordering event and add an ordered-prefix fact. The event payload is one AST list term.

Equations

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

def CordialMiners.Runtime.cmPresentation : MeTTaIL.Presentation

The Cordial Miners runtime presentation. Exports, terms, equations, and references are not needed by the current engine; it reads the rewrite declarations.

Equations

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