telltale-machine 17.0.0

Protocol machine for choreographic session type protocols
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103

//! Runtime architecture contract.
//!
//! This module defines the canonical semantic engine and the role of each
//! runtime surface.

/// Runtime engine role classification during migration.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum EngineRole {
    /// Canonical semantic owner.
    Canonical,
    /// Adapter/runtime surface that must not redefine semantics.
    AdapterOnly,
}

/// Semantic ownership contract for runtime execution surfaces.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct EngineOwnership {
    /// Runtime surface name.
    pub engine: &'static str,
    /// Canonical/adaptor role.
    pub role: EngineRole,
    /// Who owns instruction semantics.
    pub instruction_semantics_owner: &'static str,
    /// Who owns scheduler policy interpretation.
    pub scheduler_policy_owner: &'static str,
    /// Who owns observable trace emission semantics.
    pub trace_semantics_owner: &'static str,
}

/// Canonical semantic owner for ProtocolMachine execution.
pub const CANONICAL_ENGINE: &str = "ProtocolMachineKernel";

/// Cross-target semantic contract.
///
/// Native single-threaded, native threaded, and wasm cooperative runtimes
/// must agree on canonical ProtocolMachine observables, modulo effect-policy differences.
pub const CROSS_TARGET_CONTRACT: &str =
    "NativeThreaded ~= NativeSingleThreaded ~= WasmCooperative (modulo effects)";

/// Equivalence surfaces checked by cross-target validation.
pub const EQUIVALENCE_SURFACES: &[&str] = &[
    "normalized_vm_observable_trace",
    "normalized_scheduler_step_trace",
    "effect_trace",
];

/// Declared runtime ownership for all ProtocolMachine execution surfaces.
pub const ENGINE_OWNERSHIP: &[EngineOwnership] = &[
    EngineOwnership {
        engine: "ProtocolMachineKernel",
        role: EngineRole::Canonical,
        instruction_semantics_owner: "ProtocolMachineKernel + exec::*",
        scheduler_policy_owner: "ProtocolMachineKernel + scheduler::Scheduler",
        trace_semantics_owner: "ProtocolMachineKernel commit path",
    },
    EngineOwnership {
        engine: "ProtocolMachine",
        role: EngineRole::AdapterOnly,
        instruction_semantics_owner: "ProtocolMachineKernel + exec::*",
        scheduler_policy_owner: "ProtocolMachineKernel + scheduler::Scheduler",
        trace_semantics_owner: "ProtocolMachineKernel commit path",
    },
    EngineOwnership {
        engine: "ThreadedProtocolMachine",
        role: EngineRole::AdapterOnly,
        instruction_semantics_owner: "ProtocolMachineKernel + exec::*",
        scheduler_policy_owner: "ProtocolMachineKernel + scheduler::Scheduler",
        trace_semantics_owner: "ProtocolMachineKernel commit path",
    },
    EngineOwnership {
        engine: "WasmCooperativeDriver",
        role: EngineRole::AdapterOnly,
        instruction_semantics_owner: "ProtocolMachineKernel + exec::*",
        scheduler_policy_owner: "ProtocolMachineKernel + scheduler::Scheduler",
        trace_semantics_owner: "ProtocolMachineKernel commit path",
    },
];

#[cfg(test)]
mod tests {
    use super::{
        EngineRole, CANONICAL_ENGINE, CROSS_TARGET_CONTRACT, ENGINE_OWNERSHIP, EQUIVALENCE_SURFACES,
    };

    #[test]
    fn canonical_engine_is_declared_once() {
        let canon = ENGINE_OWNERSHIP
            .iter()
            .filter(|o| o.role == EngineRole::Canonical)
            .collect::<Vec<_>>();
        assert_eq!(canon.len(), 1);
        assert_eq!(canon[0].engine, CANONICAL_ENGINE);
    }

    #[test]
    fn cross_target_contract_declares_required_surfaces() {
        assert!(CROSS_TARGET_CONTRACT.contains("modulo effects"));
        assert_eq!(EQUIVALENCE_SURFACES.len(), 3);
        assert!(EQUIVALENCE_SURFACES.contains(&"normalized_vm_observable_trace"));
        assert!(EQUIVALENCE_SURFACES.contains(&"normalized_scheduler_step_trace"));
        assert!(EQUIVALENCE_SURFACES.contains(&"effect_trace"));
    }
}