Module coroutine 

Coroutine: lightweight execution unit within the ProtocolMachine.

Each role in a choreography runs as a coroutine with its own PC, register file, and status. Matches the Lean Coroutine structure.

Structs

Coroutine

A single coroutine executing a role’s local protocol.

EffectCtx

Effect context for coroutine execution, aligned with the Lean ProtocolMachine model.

KnowledgeFact

Knowledge fact for ownership checks.

ProgressToken

Progress-token representation aligned with the Lean ProtocolMachine model.

SpeculationState

Speculation state for a coroutine.

Enums

BlockReason

Why a coroutine is blocked.

CoroStatus

Coroutine execution status.

Fault

Runtime fault.

Value

Runtime value stored in registers and buffers.

Type Aliases

CoroutineState

Lean-aligned coroutine state alias.

KnowledgeSet

Lean-aligned knowledge set type.

RegFile

Register-file representation aligned with the Lean ProtocolMachine model.