Skip to main content

telltale_vm/
runtime_contracts.rs

1//! Runtime admission and profile-gate contracts aligned with Lean surfaces.
2
3use serde::{Deserialize, Serialize};
4
5use crate::determinism::DeterminismMode;
6use crate::scheduler::SchedPolicy;
7use crate::vm::VMConfig;
8
9/// VM admission result for advanced runtime mode checks.
10#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
11pub enum RuntimeAdmissionResult {
12    /// Runtime mode is admitted.
13    Admitted,
14    /// Runtime mode requires contracts that were not supplied.
15    RejectedMissingContracts,
16}
17
18/// Unified runtime gate result for admission + determinism profile enforcement.
19#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
20pub enum RuntimeGateResult {
21    /// Runtime mode/profile is admitted.
22    Admitted,
23    /// Runtime mode requires contracts that were not supplied.
24    RejectedMissingContracts,
25    /// Determinism profile is not supported by provided artifacts/capabilities.
26    RejectedUnsupportedDeterminismProfile,
27}
28
29/// Determinism artifact inventory used for runtime profile validation.
30#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
31pub struct DeterminismArtifacts {
32    /// Full determinism support.
33    pub full: bool,
34    /// Determinism modulo effect traces support.
35    pub modulo_effect_trace: bool,
36    /// Determinism modulo commutativity support.
37    pub modulo_commutativity: bool,
38    /// Replay determinism support.
39    pub replay: bool,
40}
41
42impl Default for DeterminismArtifacts {
43    fn default() -> Self {
44        Self {
45            full: true,
46            modulo_effect_trace: true,
47            modulo_commutativity: true,
48            replay: true,
49        }
50    }
51}
52
53/// Runtime contracts used for advanced-mode admission and capability gates.
54#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
55pub struct RuntimeContracts {
56    /// Determinism profile support artifacts.
57    pub determinism_artifacts: DeterminismArtifacts,
58    /// Whether mixed (non-full) determinism profiles are theorem-pack admitted.
59    pub can_use_mixed_determinism_profiles: bool,
60    /// Capability-gated runtime switches mirrored from theorem-pack API.
61    pub live_migration: bool,
62    /// Capability-gated runtime switches mirrored from theorem-pack API.
63    pub autoscale_repartition: bool,
64    /// Capability-gated runtime switches mirrored from theorem-pack API.
65    pub placement_refinement: bool,
66    /// Capability-gated runtime switches mirrored from theorem-pack API.
67    pub relaxed_reordering: bool,
68    /// Deterministic capability inventory emitted at startup.
69    pub capability_inventory: Vec<(String, bool)>,
70}
71
72impl RuntimeContracts {
73    /// Contract payload enabling all currently supported advanced runtime switches.
74    #[must_use]
75    pub fn full() -> Self {
76        Self {
77            determinism_artifacts: DeterminismArtifacts::default(),
78            can_use_mixed_determinism_profiles: true,
79            live_migration: true,
80            autoscale_repartition: true,
81            placement_refinement: true,
82            relaxed_reordering: true,
83            capability_inventory: vec![
84                ("live_migration".to_string(), true),
85                ("autoscale_repartition".to_string(), true),
86                ("placement_refinement".to_string(), true),
87                ("relaxed_reordering".to_string(), true),
88            ],
89        }
90    }
91}
92
93fn sched_policy_requires_contracts(policy: &SchedPolicy) -> bool {
94    !matches!(policy, SchedPolicy::Cooperative)
95}
96
97/// Whether VM config requires runtime contracts for admission.
98#[must_use]
99pub fn requires_vm_runtime_contracts(cfg: &VMConfig) -> bool {
100    sched_policy_requires_contracts(&cfg.sched_policy) || cfg.speculation_enabled
101}
102
103/// VM admission gate for advanced runtime modes.
104#[must_use]
105pub fn admit_vm_runtime(
106    cfg: &VMConfig,
107    contracts: Option<&RuntimeContracts>,
108) -> RuntimeAdmissionResult {
109    if requires_vm_runtime_contracts(cfg) && contracts.is_none() {
110        RuntimeAdmissionResult::RejectedMissingContracts
111    } else {
112        RuntimeAdmissionResult::Admitted
113    }
114}
115
116/// Check artifact support for one determinism profile.
117#[must_use]
118pub fn determinism_profile_supported(
119    artifacts: &DeterminismArtifacts,
120    profile: DeterminismMode,
121) -> bool {
122    match profile {
123        DeterminismMode::Full => artifacts.full,
124        DeterminismMode::ModuloEffects => artifacts.modulo_effect_trace,
125        DeterminismMode::ModuloCommutativity => artifacts.modulo_commutativity,
126        DeterminismMode::Replay => artifacts.replay,
127    }
128}
129
130/// Runtime profile selection gate with mixed-profile capability checks.
131#[must_use]
132pub fn request_determinism_profile(
133    contracts: &RuntimeContracts,
134    profile: DeterminismMode,
135) -> Option<DeterminismMode> {
136    let supported = determinism_profile_supported(&contracts.determinism_artifacts, profile);
137    if !supported {
138        return None;
139    }
140    match profile {
141        DeterminismMode::Full => Some(profile),
142        DeterminismMode::ModuloEffects
143        | DeterminismMode::ModuloCommutativity
144        | DeterminismMode::Replay => contracts
145            .can_use_mixed_determinism_profiles
146            .then_some(profile),
147    }
148}
149
150/// Unified runtime gate check for advanced-mode admission and profile support.
151#[must_use]
152pub fn enforce_vm_runtime_gates(
153    cfg: &VMConfig,
154    contracts: Option<&RuntimeContracts>,
155) -> RuntimeGateResult {
156    match admit_vm_runtime(cfg, contracts) {
157        RuntimeAdmissionResult::RejectedMissingContracts => {
158            RuntimeGateResult::RejectedMissingContracts
159        }
160        RuntimeAdmissionResult::Admitted => match contracts {
161            Some(contracts) => {
162                if request_determinism_profile(contracts, cfg.determinism_mode).is_some() {
163                    RuntimeGateResult::Admitted
164                } else {
165                    RuntimeGateResult::RejectedUnsupportedDeterminismProfile
166                }
167            }
168            None => {
169                if matches!(cfg.determinism_mode, DeterminismMode::Full) {
170                    RuntimeGateResult::Admitted
171                } else {
172                    RuntimeGateResult::RejectedUnsupportedDeterminismProfile
173                }
174            }
175        },
176    }
177}
178
179/// Runtime capability snapshot emitted at startup.
180#[must_use]
181pub fn runtime_capability_snapshot(contracts: &RuntimeContracts) -> Vec<(String, bool)> {
182    let mut snapshot = contracts.capability_inventory.clone();
183    snapshot.push(("live_migration".to_string(), contracts.live_migration));
184    snapshot.push((
185        "autoscale_repartition".to_string(),
186        contracts.autoscale_repartition,
187    ));
188    snapshot.push((
189        "placement_refinement".to_string(),
190        contracts.placement_refinement,
191    ));
192    snapshot.push((
193        "relaxed_reordering".to_string(),
194        contracts.relaxed_reordering,
195    ));
196    snapshot
197}
198
199#[cfg(test)]
200mod tests {
201    use super::*;
202
203    #[test]
204    fn admission_requires_contracts_for_advanced_modes() {
205        let mut cfg = VMConfig::default();
206        assert_eq!(
207            admit_vm_runtime(&cfg, None),
208            RuntimeAdmissionResult::Admitted
209        );
210
211        cfg.speculation_enabled = true;
212        assert_eq!(
213            admit_vm_runtime(&cfg, None),
214            RuntimeAdmissionResult::RejectedMissingContracts
215        );
216        assert_eq!(
217            admit_vm_runtime(&cfg, Some(&RuntimeContracts::full())),
218            RuntimeAdmissionResult::Admitted
219        );
220    }
221
222    #[test]
223    fn request_determinism_profile_obeys_artifacts_and_mixed_gate() {
224        let mut contracts = RuntimeContracts::full();
225        contracts.can_use_mixed_determinism_profiles = false;
226        assert_eq!(
227            request_determinism_profile(&contracts, DeterminismMode::Full),
228            Some(DeterminismMode::Full)
229        );
230        assert_eq!(
231            request_determinism_profile(&contracts, DeterminismMode::Replay),
232            None
233        );
234
235        contracts.can_use_mixed_determinism_profiles = true;
236        contracts.determinism_artifacts.replay = false;
237        assert_eq!(
238            request_determinism_profile(&contracts, DeterminismMode::Replay),
239            None
240        );
241        contracts.determinism_artifacts.replay = true;
242        assert_eq!(
243            request_determinism_profile(&contracts, DeterminismMode::Replay),
244            Some(DeterminismMode::Replay)
245        );
246    }
247
248    #[test]
249    #[allow(clippy::field_reassign_with_default)]
250    fn unified_runtime_gate_combines_admission_and_profile_checks() {
251        let mut cfg = VMConfig::default();
252        cfg.speculation_enabled = true;
253        assert_eq!(
254            enforce_vm_runtime_gates(&cfg, None),
255            RuntimeGateResult::RejectedMissingContracts
256        );
257
258        let mut contracts = RuntimeContracts::full();
259        contracts.determinism_artifacts.replay = false;
260        cfg.determinism_mode = DeterminismMode::Replay;
261        assert_eq!(
262            enforce_vm_runtime_gates(&cfg, Some(&contracts)),
263            RuntimeGateResult::RejectedUnsupportedDeterminismProfile
264        );
265
266        contracts.determinism_artifacts.replay = true;
267        assert_eq!(
268            enforce_vm_runtime_gates(&cfg, Some(&contracts)),
269            RuntimeGateResult::Admitted
270        );
271    }
272}