Struct ProtocolMachine 

pub struct ProtocolMachine<I = (), G = (), P = NoopPersistence, Nu = DefaultVerificationModel>
where
    P: PersistenceModel,
{ /* private fields */ }

The choreographic ProtocolMachine.

Manages coroutines, sessions (which own type state), and a scheduler. Multiple choreographies can be loaded into a single ProtocolMachine, each in its own session namespace — justified by separation logic.

Implementations

impl<I, G, P, Nu> ProtocolMachine<I, G, P, Nu>

where P: PersistenceModel,

pub fn new_with_models(config: ProtocolMachineConfig) -> Self

where P::PState: Default, Nu: VerificationModel + Default,

Create a ProtocolMachine for arbitrary persistence/verification model parameters.

pub fn persistent_state(&self) -> &P::PState

Borrow the persistent state tracked by the configured persistence model.

pub fn persistent_state_mut(&mut self) -> &mut P::PState

Mutably borrow persistent state.

pub fn bridge_guard_layer_for_participant<B>( &self, bridge: &B, participant: &I::ParticipantId, ) -> LayerId

where I: IdentityModel, G: GuardLayer, B: IdentityGuardBridge<I, G>,

Resolve guard-layer capability for a participant via bridge binding.

pub fn bridge_verifying_key_for_participant<B>( &self, bridge: &B, participant: &I::ParticipantId, ) -> Nu::VerifyingKey

where I: IdentityModel, Nu: VerificationModel, B: IdentityVerificationBridge<I, Nu>,

Resolve participant verification key via bridge binding.

impl ProtocolMachine

pub fn new(config: ProtocolMachineConfig) -> Self

Create a ProtocolMachine instance from configuration.

impl ProtocolMachine

pub fn step( &mut self, handler: &dyn EffectHandler, ) -> Result<StepResult, ProtocolMachineError>

Execute one scheduler step: pick a coroutine, run one instruction.

Errors

Returns a ProtocolMachineError if a coroutine faults.

pub fn step_round( &mut self, handler: &dyn EffectHandler, n: usize, ) -> Result<StepResult, ProtocolMachineError>

Execute one scheduler round through the canonical kernel API.

Errors

Returns a ProtocolMachineError if a coroutine faults.

pub fn run_concurrent( &mut self, handler: &dyn EffectHandler, max_rounds: usize, concurrency: usize, ) -> Result<RunStatus, ProtocolMachineError>

Run the ProtocolMachine until all coroutines complete or an error occurs, with concurrency N.

max_rounds prevents infinite loops.

Errors

Returns a ProtocolMachineError if any coroutine faults.

pub fn run( &mut self, handler: &dyn EffectHandler, max_steps: usize, ) -> Result<RunStatus, ProtocolMachineError>

Run the ProtocolMachine until all coroutines complete or an error occurs.

max_steps prevents infinite loops.

Errors

Returns a ProtocolMachineError if any coroutine faults.

pub fn run_replay( &mut self, fallback: &dyn EffectHandler, replay_trace: &[EffectTraceEntry], max_steps: usize, ) -> Result<RunStatus, ProtocolMachineError>

Run with replayed effect outcomes captured from a prior execution.

The fallback handler is only used for optional hooks not encoded in replay entries.

Errors

Returns a ProtocolMachineError if replay data is exhausted/mismatched or a coroutine faults.

pub fn run_replay_shared( &mut self, fallback: &dyn EffectHandler, replay_trace: Arc<[EffectTraceEntry]>, max_steps: usize, ) -> Result<RunStatus, ProtocolMachineError>

Run with replayed effect outcomes using shared trace storage.

Accepts an Arc-backed trace to avoid cloning when callers already hold shared replay buffers.

Errors

Returns a ProtocolMachineError if replay data is exhausted/mismatched or a coroutine faults.

pub fn run_concurrent_replay( &mut self, fallback: &dyn EffectHandler, replay_trace: &[EffectTraceEntry], max_rounds: usize, concurrency: usize, ) -> Result<RunStatus, ProtocolMachineError>

Run concurrently with replayed effect outcomes.

Errors

Returns a ProtocolMachineError if replay data is exhausted/mismatched or a coroutine faults.

pub fn run_concurrent_replay_shared( &mut self, fallback: &dyn EffectHandler, replay_trace: Arc<[EffectTraceEntry]>, max_rounds: usize, concurrency: usize, ) -> Result<RunStatus, ProtocolMachineError>

Run concurrently with replayed outcomes using shared trace storage.

Errors

Returns a ProtocolMachineError if replay data is exhausted/mismatched or a coroutine faults.

pub fn trace(&self) -> &[ObsEvent]

Get the observable trace.

pub fn reap_closed_sessions(&mut self) -> Vec<ClosedSessionSummary>

Reap closed sessions once all associated coroutines are terminal.

pub fn obs_trace(&self) -> &[ObsEvent]

Lean-aligned observable trace accessor.

pub fn role_symbol_count(&self) -> usize

Number of interned role symbols.

pub fn label_symbol_count(&self) -> usize

Number of interned label symbols.

pub fn handler_symbol_count(&self) -> usize

Number of interned handler symbols.

pub fn edge_symbol_count(&self) -> usize

Number of interned edge symbols.

pub fn config(&self) -> &ProtocolMachineConfig

Access ProtocolMachine configuration.

pub fn last_sched_step(&self) -> Option<&SchedStepDebug>

Last scheduler-dispatched step metadata, if any coroutine ran.

pub fn scheduler_step_count(&self) -> usize

Scheduler-dispatched step counter.

pub fn coroutine_count(&self) -> usize

Number of coroutine records in the ProtocolMachine.

pub fn next_session_id(&self) -> SessionId

Next session identifier reserved for allocation.

pub fn session_count(&self) -> usize

Number of active sessions in the ProtocolMachine.

pub fn live_session_count(&self) -> usize

Number of sessions still resident in the ProtocolMachine, including closed ones.

impl ProtocolMachine

pub fn refinement_slice( &self, ) -> Result<ProtocolMachineRefinementSlice, RefinementSliceError>

Export the concrete runtime slice used for exact Rust/Lean refinement checks.

Errors

Returns an error when the exported counts do not fit the bridge-safe u64 schema.

pub fn last_pre_dispatch_refinement_slice( &self, ) -> Option<ProtocolMachineRefinementSlice>

Export the most recent normalized pre-dispatch refinement slice.

This snapshot is captured after ingress, timeout pruning, receiver unblocking, and ready-eligibility normalization, but before runnable coroutine selection.

pub fn transition_refinement_summary( &self, ) -> Result<TransitionRefinementSummary, RefinementSliceError>

Export the most recent scheduler-transition summary used for exact Rust↔Lean step-state checks.

Errors

Returns an error when exported counts do not fit the bridge-safe u64 schema.

pub fn claimed_runtime_core_bundle( &self, ) -> Result<ClaimedRuntimeCoreBundle, RefinementSliceError>

Export the current claim-critical runtime refinement core bundle.

Errors

Returns an error when exported counts do not fit the bridge-safe u64 schema.

pub fn runtime_observation_bundle( &self, ) -> Result<RuntimeObservationBundle, RefinementSliceError>

Export the broader runtime observation bundle used by operational suites.

Errors

Returns an error when exported counts do not fit the bridge-safe u64 schema.

pub fn memory_usage(&self) -> ProtocolMachineMemoryUsage

Approximate retained state for the protocol-machine runtime.

pub fn output_condition_checks(&self) -> &[OutputConditionCheck]

Get recorded output-condition verification checks.

pub fn effect_trace(&self) -> &[EffectTraceEntry]

Get recorded effect-trace entries.

pub fn effect_exchanges(&self) -> &[EffectExchangeRecord]

Get canonical typed effect request/outcome exchanges.

pub fn operation_instances(&self) -> &[OperationInstance]

Get canonical operation instances tracked as runtime state.

pub fn outstanding_effects(&self) -> &[OutstandingEffect]

Get canonical outstanding effects tracked as runtime state.

pub fn progress_contracts(&self) -> &[ProgressContract]

Get canonical progress contracts tracked as runtime state.

pub fn progress_transitions(&self) -> &[ProgressTransition]

Get replay-visible progress transitions tracked as runtime state.

pub fn delegation_audit_log(&self) -> &[DelegationAuditRecord]

Get recorded delegation audit records.

pub fn authority_audit_log(&self) -> &[AuthorityAuditRecord]

Get recorded authority witness audit records.

pub fn semantic_audit_log(&self) -> Vec<SemanticAuditRecord>

Get canonical semantic audit records derived from authority, delegation, failure, and effect/interface traces.

pub fn capability_lifecycle_audit_log( &self, ) -> Vec<ProtocolCriticalCapabilityLifecycleRecord>

Get canonical capability/evidence lifecycle audit records.

pub fn semantic_objects(&self) -> ProtocolMachineSemanticObjects

Get canonical semantic objects derived from authority, handoff, effect, and output-condition surfaces.

pub fn publication_events(&self) -> Vec<PublicationEvent>

Get canonical semantic publication events.

pub fn prestate_bindings(&self) -> Vec<PrestateBinding>

Get canonical prestate bindings.

pub fn agreement_profiles(&self) -> Vec<AgreementProfile>

Get canonical named agreement profiles.

pub fn agreement_contracts(&self) -> Vec<AgreementContract>

Get canonical agreement contracts.

pub fn agreement_evidence(&self) -> Vec<AgreementEvidence>

Get canonical agreement evidence objects.

pub fn agreement_states(&self) -> Vec<AgreementState>

Get canonical agreement states.

pub fn require_authoritative_read( &self, read_id: &str, ) -> Result<AuthoritativeRead, ProtocolMachineError>

Require that one semantic-path read be authoritative.

Errors

Returns a contract violation when the requested read is observational or unknown.

pub fn require_canonical_handle( &self, handle_id: &str, ) -> Result<CanonicalHandle, ProtocolMachineError>

Require that one parity-critical path use a canonical handle.

Errors

Returns a contract violation when the requested handle is missing.

pub fn communication_replay_root(&self) -> Hash

Deterministic communication replay-state root.

pub fn communication_consumption_artifacts( &self, ) -> &[CommunicationConsumptionArtifact]

Receive-boundary replay-consumption artifacts.

pub fn drain_obs_trace(&mut self) -> Vec<ObsEvent>

Drain retained observable events in canonical insertion order.

pub fn drain_effect_trace(&mut self) -> Vec<EffectTraceEntry>

Drain retained effect-trace entries in canonical insertion order.

pub fn drain_output_condition_checks(&mut self) -> Vec<OutputConditionCheck>

Drain retained output-condition diagnostics in canonical insertion order.

pub fn drain_delegation_audit_log(&mut self) -> Vec<DelegationAuditRecord>

Drain retained delegation audit records in canonical insertion order.

pub fn drain_authority_audit_log(&mut self) -> Vec<AuthorityAuditRecord>

Drain retained authority witness audit records in canonical insertion order.

pub fn drain_communication_consumption_artifacts( &mut self, ) -> Vec<CommunicationConsumptionArtifact>

Drain retained communication replay-consumption artifacts in canonical insertion order.

pub fn canonical_replay_fragment(&self) -> CanonicalReplayFragmentV1

Canonical replay/state fragment for deterministic diffing and snapshots.

pub fn crashed_sites(&self) -> &BTreeSet<String>

Crashed sites currently active in topology state.

pub fn partitioned_edges(&self) -> &BTreeSet<(String, String)>

Partitioned site-links currently active in topology state.

pub fn corrupted_edges(&self) -> &BTreeMap<(String, String), CorruptionType>

Corrupted directed edges currently active in topology state.

pub fn timed_out_sites(&self) -> BTreeMap<String, u64>

Active site timeouts.

pub fn timeout_witnesses(&self) -> &BTreeMap<String, TimeoutWitness>

Active timeout witnesses keyed by site.

impl ProtocolMachine

pub fn clock(&self) -> &SimClock

Access the simulation clock.

pub fn all_done(&self) -> bool

Whether all coroutines are terminal (done or faulted).

pub fn coroutine(&self, id: usize) -> Option<&Coroutine>

Get a coroutine by ID.

pub fn coroutine_program_len(&self, id: usize) -> Option<usize>

Program length for a coroutine by id.

pub fn unique_program_count(&self) -> usize

Number of unique immutable programs retained by the ProtocolMachine.

pub fn coroutine_mut(&mut self, id: usize) -> Option<&mut Coroutine>

Get a mutable coroutine by ID.

pub fn session_coroutines(&self, sid: SessionId) -> Vec<&Coroutine>

Get all coroutines for a session.

pub fn sessions(&self) -> &SessionStore

Access the session store.

pub fn validate_post_decode(&self) -> Result<(), String>

Validate structural invariants after deserializing a persisted machine.

This is intentionally conservative: it checks the decoded state against configuration limits and internal ID consistency before the machine is resumed.

Errors

Returns a deterministic reason when decoded state violates runtime invariants.

pub fn wf_vm_state(&self) -> Result<(), String>

Runtime well-formedness predicate used by debug assertions.

Errors

Returns a description of the invariant violation if the ProtocolMachine state is invalid.

pub fn inject_message( &mut self, sid: SessionId, from: &str, to: &str, value: Value, ) -> Result<EnqueueResult, ProtocolMachineError>

Inject a message directly into a session buffer.

Used by simulation middleware (network/fault injection) to deliver in-flight messages without executing a ProtocolMachine send instruction.

Errors

Returns an error if the session does not exist.

pub fn coroutines(&self) -> &[Coroutine]

Access all coroutines.

pub fn pause_role(&mut self, role: &str)

Pause execution for all coroutines of a role.

pub fn resume_role(&mut self, role: &str)

Resume execution for all coroutines of a role.

pub fn set_paused_roles(&mut self, roles: &BTreeSet<String>)

Replace the paused role set.

pub fn paused_roles(&self) -> &BTreeSet<String>

Access paused roles.

impl ProtocolMachine

pub fn mark_owner_died( &mut self, sid: SessionId, owner_id: &str, ) -> Result<CancellationWitness, OwnershipError>

Fault a session because the current owner died.

Errors

Returns an OwnershipError if the live owner no longer matches.

pub fn cancel_abandoned_transfer( &mut self, receipt: &OwnershipReceipt, ) -> Result<CancellationWitness, OwnershipError>

Cancel a session because a staged transfer was abandoned.

Errors

Returns an OwnershipError if the receipt no longer matches the staged transfer.

pub fn fault_failed_transfer_commit( &mut self, receipt: &OwnershipReceipt, reason: impl Into<String>, ) -> Result<(), OwnershipError>

Fault a session because a staged transfer could not commit.

Errors

Returns an OwnershipError if the receipt no longer matches the staged transfer.

impl ProtocolMachine

pub fn load_choreography_owned( &mut self, image: &CodeImage, owner_id: impl Into<String>, ) -> Result<OwnedSession, ProtocolMachineError>

Preferred choreography open path that immediately claims session ownership.

Third-party host integrations use this owned helper so subsequent session-local mutation flows through an explicit ownership capability.

Errors

Returns a ProtocolMachineError if the choreography cannot be loaded or the initial ownership claim fails.

Trait Implementations

impl<I: Debug, G: Debug, P, Nu: Debug> Debug for ProtocolMachine<I, G, P, Nu>

where P: PersistenceModel + Debug, P::PState: Debug,

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de, I, G, P, Nu> Deserialize<'de> for ProtocolMachine<I, G, P, Nu>

where P: PersistenceModel, Nu: Deserialize<'de>, P::PState: Deserialize<'de>,

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl KernelMachine for ProtocolMachine

fn kernel_step_round( &mut self, handler: &dyn EffectHandler, n: usize, ) -> Result<StepResult, ProtocolMachineError>

Execute one scheduler round in the machine’s native state.

impl<I, G, P, Nu> Serialize for ProtocolMachine<I, G, P, Nu>

where P: PersistenceModel, Nu: Serialize, P::PState: Serialize,

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.