Skip to main content

protocol/lib

Reference for mo:core/protocol/lib in the core library.

Import​

mo:core/protocol/lib

Status​

  • Protocol schema module
  • Runtime builders plus pure quorum helpers

Purpose​

protocol/lib defines the shared schema used to describe protocol participants, endpoints, state bindings, call bindings, and temporal properties. It is a declaration layer: it structures protocol metadata for extraction and analysis, but it does not prove the temporal properties by itself.

Use this module when you want protocol metadata to be machine-readable by the Sector9 analysis pipeline instead of leaving roles and call surfaces as comments.

The source module is named ProtocolCore, but users import it by path:

import Protocol "mo:core/protocol/lib";

Public API​

Types​

  • Property<State, Handle, PropertyId> - A named temporal property plus the handles it refers to.
  • ProtocolSpec<State, Participant, Handle, PropertyId> - Protocol name, participants, and properties.
  • TrustClass - #trusted_canister, #untrusted_canister, or #untrusted_offchain.
  • RoleSpec<Role> - Role metadata with trust class and multiplicity.
  • Temporal<State> - Temporal property shape: #always, #eventually, #until, or #leads_to.
  • Endpoint<Role, Handle> - Role, verification flag, and endpoint handle.
  • EndpointSchedule - #top_level or #callee_only.
  • EndpointMode<Role, Handle> - Endpoint scheduling metadata.
  • CallBinding<Role, Handle> - Caller/callee role and handle binding.
  • CompanionBinding<Role, Handle> - Companion role and handle binding.
  • StateBinding<Role> - Runtime state field binding, optionally from a source root.
  • SurfaceExclusion<Role> - Method exclusion metadata for a role.
  • BindingWitness<EndpointBinding> - Witness record for endpoint bindings.
  • BoundSpec<Spec, RuntimeBindings, EndpointBinding> - Protocol spec bundled with runtime bindings and witness data.

Builder Functions​

  • endpoint<Role, Handle>(role : Role, verified_call : Bool, handle : Handle) : Endpoint<Role, Handle>
  • callBinding<Role, Handle>(callerRole : Role, callerHandle : Handle, receiverParam : Nat, calleeRole : Role, calleeHandle : Handle) : CallBinding<Role, Handle>
  • endpointMode<Role, Handle>(role : Role, handle : Handle, schedule : EndpointSchedule) : EndpointMode<Role, Handle>
  • companionBinding<Role, Handle, Companion>(role : Role, handle : Handle, _companion : Companion) : CompanionBinding<Role, Handle>
  • stateBinding<Role>(field : Text, role : Role) : StateBinding<Role>
  • stateBindingFrom<Role>(field : Text, source_root : Text, role : Role) : StateBinding<Role>
  • surfaceExclude<Role>(role : Role, method_name : Text) : SurfaceExclusion<Role>
  • roleSpec<Role>(role : Role, trust : TrustClass, many : Bool) : RoleSpec<Role>
  • property<State, Handle, PropertyId>(id : PropertyId, temporal : Temporal<State>, handles : [Handle]) : Property<State, Handle, PropertyId>
  • bindingWitness<EndpointBinding>(endpoints : [EndpointBinding]) : BindingWitness<EndpointBinding>
  • boundSpec<Spec, RuntimeBindings, EndpointBinding>(spec : Spec, runtime : RuntimeBindings, witness : BindingWitness<EndpointBinding>) : BoundSpec<Spec, RuntimeBindings, EndpointBinding>
  • autoSpec<State, Participant, Handle, PropertyId>(name : Text, participants : [Participant], properties : [Property<State, Handle, PropertyId>]) : ProtocolSpec<State, Participant, Handle, PropertyId>

Pure Quorum Helpers​

  • majorityThreshold(participantCount : Nat) : Nat - Returns 0 for zero participants, otherwise participantCount / 2 + 1.
  • hasMajority(observed : Nat, participantCount : Nat) : Bool - Checks whether observed reaches the majority threshold.
  • hasUnanimity(observed : Nat, participantCount : Nat) : Bool - Checks whether all participants are observed.
  • quorumsIntersect(leftQuorum : Nat, rightQuorum : Nat, participantCount : Nat) : Bool - Checks whether two quorums must overlap.

Summary​

  • Use protocol/lib to declare protocol metadata in a structured, typed form.
  • Use the builder functions instead of constructing records directly when you want stable extraction shapes.
  • Temporal properties are represented as data; proving them remains the responsibility of the verification and protocol-analysis workflow.