telltale_machine/
runtime_contracts.rs

1//! Runtime admission and profile-gate contracts aligned with Lean surfaces.
2
3use std::collections::BTreeSet;
4
5use serde::{Deserialize, Serialize};
6
7use crate::determinism::DeterminismMode;
8use crate::engine::ProtocolMachineConfig;
9use crate::output_condition::OutputConditionPolicy;
10use crate::scheduler::SchedPolicy;
11
12/// ProtocolMachine admission result for advanced runtime mode checks.
13#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
14pub enum RuntimeAdmissionResult {
15    /// Runtime mode is admitted.
16    Admitted,
17    /// Runtime mode requires contracts that were not supplied.
18    RejectedMissingContracts,
19}
20
21/// Unified runtime gate result for admission + determinism profile enforcement.
22#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
23pub enum RuntimeGateResult {
24    /// Runtime mode/profile is admitted.
25    Admitted,
26    /// Runtime mode requires contracts that were not supplied.
27    RejectedMissingContracts,
28    /// Determinism profile is not supported by provided artifacts/capabilities.
29    RejectedUnsupportedDeterminismProfile,
30}
31
32/// Machine-side summary of a selected transport contract.
33///
34/// This is semantic evidence, not a transport implementation hook. Concrete
35/// transport crates translate their selected authentication, routing, and
36/// delivery mode into these fields; `telltale-machine` only checks whether the
37/// selected runtime path satisfies the theorem-pack assumptions. That keeps the
38/// machine independent of TCP, TLS, pre-shared keys, or any other concrete
39/// authentication mechanism.
40#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
41pub struct RuntimeTransportContract {
42    /// Stable transport/profile name.
43    pub transport_name: String,
44    /// Human-readable transport kind, e.g. `InMemory` or `Tcp`.
45    pub transport_type: String,
46    /// Whether messages are routed by role identity.
47    pub role_addressed_routing: bool,
48    /// Whether peer identity is authenticated at the transport boundary.
49    ///
50    /// This must be `false` for trusted-network-only transports. Theorem packs
51    /// that depend on protocol-origin integrity require this field to be true.
52    pub authenticated_peers: bool,
53    /// Whether each peer stream preserves FIFO delivery.
54    pub per_peer_fifo_delivery: bool,
55    /// Whether unknown role claims are rejected instead of admitted.
56    pub fail_closed_unknown_role: bool,
57    /// Whether the transport can synthesize messages not sent by a peer.
58    pub no_message_synthesis: bool,
59    /// Whether startup/readiness failures are surfaced explicitly.
60    pub explicit_readiness_errors: bool,
61    /// Whether the transport is deterministic enough for regression harnesses.
62    pub deterministic_for_regression: bool,
63}
64
65impl RuntimeTransportContract {
66    /// Start a semantic transport contract summary.
67    ///
68    /// All semantic fields default to `false` so callers must opt in to each
69    /// contract they can justify for the selected runtime transport.
70    #[must_use]
71    pub fn new(transport_name: impl Into<String>, transport_type: impl Into<String>) -> Self {
72        Self {
73            transport_name: transport_name.into(),
74            transport_type: transport_type.into(),
75            role_addressed_routing: false,
76            authenticated_peers: false,
77            per_peer_fifo_delivery: false,
78            fail_closed_unknown_role: false,
79            no_message_synthesis: false,
80            explicit_readiness_errors: false,
81            deterministic_for_regression: false,
82        }
83    }
84
85    /// Contract summary for the first-party in-process channel transport.
86    #[must_use]
87    pub fn first_party_in_memory() -> Self {
88        Self::new("InMemoryChannelTransport", "InMemory")
89            .with_role_addressed_routing(true)
90            .with_authenticated_peers(true)
91            .with_per_peer_fifo_delivery(true)
92            .with_fail_closed_unknown_role(true)
93            .with_no_message_synthesis(true)
94            .with_deterministic_for_regression(true)
95    }
96
97    /// Set whether messages are routed by role identity.
98    #[must_use]
99    pub fn with_role_addressed_routing(mut self, value: bool) -> Self {
100        self.role_addressed_routing = value;
101        self
102    }
103
104    /// Set whether peer identity is authenticated at the transport boundary.
105    ///
106    /// Set this to `true` only when the selected transport mode cryptographically
107    /// or otherwise operationally binds a peer to its claimed role. Plain TCP on
108    /// a trusted network should leave this `false`.
109    #[must_use]
110    pub fn with_authenticated_peers(mut self, value: bool) -> Self {
111        self.authenticated_peers = value;
112        self
113    }
114
115    /// Set whether each peer stream preserves FIFO delivery.
116    #[must_use]
117    pub fn with_per_peer_fifo_delivery(mut self, value: bool) -> Self {
118        self.per_peer_fifo_delivery = value;
119        self
120    }
121
122    /// Set whether unknown role claims are rejected instead of admitted.
123    #[must_use]
124    pub fn with_fail_closed_unknown_role(mut self, value: bool) -> Self {
125        self.fail_closed_unknown_role = value;
126        self
127    }
128
129    /// Set whether the transport can synthesize messages not sent by a peer.
130    #[must_use]
131    pub fn with_no_message_synthesis(mut self, value: bool) -> Self {
132        self.no_message_synthesis = value;
133        self
134    }
135
136    /// Set whether startup/readiness failures are surfaced explicitly.
137    #[must_use]
138    pub fn with_explicit_readiness_errors(mut self, value: bool) -> Self {
139        self.explicit_readiness_errors = value;
140        self
141    }
142
143    /// Set whether the transport is deterministic enough for regression harnesses.
144    #[must_use]
145    pub fn with_deterministic_for_regression(mut self, value: bool) -> Self {
146        self.deterministic_for_regression = value;
147        self
148    }
149}
150
151/// Transport semantics required by a theorem-pack execution profile.
152///
153/// The standard protocol-origin profile deliberately asks for authenticated
154/// peers. Without that premise, a network peer can claim a role name that the
155/// proof treats as an origin identity, invalidating the end-to-end theorem
156/// claim even if the protocol choreography is otherwise verified.
157#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
158pub struct TheoremTransportRequirements {
159    /// Whether the theorem profile depends on role-addressed routing.
160    pub role_addressed_routing: bool,
161    /// Whether the theorem profile depends on authenticated peer identity.
162    pub authenticated_peers: bool,
163    /// Whether the theorem profile depends on per-peer FIFO delivery.
164    pub per_peer_fifo_delivery: bool,
165    /// Whether unknown role claims must fail closed.
166    pub fail_closed_unknown_role: bool,
167    /// Whether the transport must not synthesize messages.
168    pub no_message_synthesis: bool,
169}
170
171impl TheoremTransportRequirements {
172    /// No transport assumptions are required.
173    #[must_use]
174    pub const fn none() -> Self {
175        Self {
176            role_addressed_routing: false,
177            authenticated_peers: false,
178            per_peer_fifo_delivery: false,
179            fail_closed_unknown_role: false,
180            no_message_synthesis: false,
181        }
182    }
183
184    /// Standard theorem-pack requirements for protocol-origin claims.
185    #[must_use]
186    pub const fn protocol_origin_integrity() -> Self {
187        Self {
188            role_addressed_routing: true,
189            authenticated_peers: true,
190            per_peer_fifo_delivery: true,
191            fail_closed_unknown_role: true,
192            no_message_synthesis: true,
193        }
194    }
195
196    /// Whether any transport premise is required.
197    #[must_use]
198    pub const fn is_empty(self) -> bool {
199        !self.role_addressed_routing
200            && !self.authenticated_peers
201            && !self.per_peer_fifo_delivery
202            && !self.fail_closed_unknown_role
203            && !self.no_message_synthesis
204    }
205}
206
207/// Transport-contract admission failure for theorem-pack claims.
208#[derive(Debug, Clone, PartialEq, Eq)]
209pub enum TransportContractGateError {
210    /// The theorem profile needs transport contracts but none were supplied.
211    MissingTransportContracts,
212    /// One selected transport does not satisfy a required semantic field.
213    UnsatisfiedTransportRequirement {
214        /// Selected transport profile name.
215        transport_name: String,
216        /// Required semantic field.
217        requirement: &'static str,
218    },
219}
220
221/// How one transported theorem family participates in shipped assurance.
222#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
223#[serde(rename_all = "snake_case")]
224pub enum TransportedTheoremUsageClass {
225    /// Executed verifier/reporting surface treats this family as a black-box premise.
226    BlackBoxPremiseOnly,
227    /// This family materially influences a shipped runtime gate/guarantee surface.
228    RuntimeCriticalInstantiatedPremise,
229    /// This family is carried for documentation or background inventory only.
230    DocumentationBackgroundOnly,
231}
232
233/// Ledger row for one transported theorem family and its admission relevance.
234#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
235pub struct TransportedTheoremBoundaryEntry {
236    /// Stable theorem-pack inventory key.
237    pub key: String,
238    /// Classification of how the family participates in shipped assurance.
239    pub usage_class: TransportedTheoremUsageClass,
240    /// Whether shipped Rust runtime admission consumes this family directly.
241    pub consumed_by_rust_runtime_admission: bool,
242    /// Whether Lean theorem-pack gate aliases consume this family directly.
243    pub consumed_by_lean_runtime_gate: bool,
244    /// Explicit assumption marker when the family is runtime-critical but not
245    /// yet instantiated in shipped Rust runtime admission.
246    pub assumption_boundary: Option<String>,
247}
248
249/// Reasons the transported-theorem ledger and runtime profile can be inconsistent.
250#[derive(Debug, Clone, PartialEq, Eq)]
251pub enum TransportedTheoremBoundaryValidationError {
252    /// Rust runtime admission consumes a theorem family that is not classified as
253    /// runtime-critical in the boundary ledger.
254    RustAdmissionKeyNotRuntimeCritical(String),
255    /// A runtime-critical theorem consumed only by Lean lost its explicit
256    /// assumption boundary marker.
257    LeanOnlyRuntimeCriticalMissingAssumptionBoundary(String),
258    /// A Rust-runtime-consumed theorem family is missing from the runtime
259    /// execution profile eligibility set.
260    RuntimeProfileMissingRustAdmissionKey(String),
261    /// A Rust-runtime-consumed theorem family is present in the runtime profile
262    /// but disabled.
263    RuntimeProfileDisablesRustAdmissionKey(String),
264    /// The runtime profile enables a theorem family that is not classified as a
265    /// Rust-runtime-consumed theorem boundary entry.
266    RuntimeProfileEnablesUnknownRustAdmissionKey(String),
267}
268
269/// Determinism artifact inventory used for runtime profile validation.
270#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
271pub struct DeterminismArtifacts {
272    /// Full determinism support.
273    pub full: bool,
274    /// Determinism modulo effect traces support.
275    pub modulo_effect_trace: bool,
276    /// Determinism modulo commutativity support.
277    pub modulo_commutativity: bool,
278    /// Replay determinism support.
279    pub replay: bool,
280}
281
282impl Default for DeterminismArtifacts {
283    fn default() -> Self {
284        Self {
285            full: true,
286            modulo_effect_trace: true,
287            modulo_commutativity: true,
288            replay: true,
289        }
290    }
291}
292
293/// Runtime capability admitted by theorem-pack/runtime contracts.
294#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
295#[serde(rename_all = "snake_case")]
296pub enum RuntimeCapability {
297    /// Live migration/runtime handoff support.
298    LiveMigration,
299    /// Autoscale repartition support.
300    AutoscaleRepartition,
301    /// Placement refinement support.
302    PlacementRefinement,
303    /// Relaxed reordering support.
304    RelaxedReordering,
305}
306
307/// Fairness assumptions carried by a proof-carrying execution profile.
308#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
309#[serde(rename_all = "snake_case")]
310pub enum ProtocolMachineFairnessAssumption {
311    /// Scheduler steps commute to the same semantic result.
312    ScheduleConfluence,
313    /// Live work is eventually scheduled.
314    StarvationFreedom,
315    /// Liveness-sensitive obligations receive fair scheduling treatment.
316    LivenessFairness,
317}
318
319/// Admissibility classes carried by a proof-carrying execution profile.
320#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
321#[serde(rename_all = "snake_case")]
322pub enum ProtocolMachineAdmissibilityClass {
323    /// Local protocol-machine envelope assumptions are admitted.
324    LocalEnvelope,
325    /// Sharded/distributed envelope assumptions are admitted.
326    ShardedEnvelope,
327    /// Protocol-envelope bridge assumptions are admitted.
328    ProtocolEnvelopeBridge,
329}
330
331/// Escalation-window classes carried by a proof-carrying execution profile.
332#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
333#[serde(rename_all = "snake_case")]
334pub enum ProtocolMachineEscalationWindowClass {
335    /// Progress contracts carry bounded escalation windows.
336    ProgressContract,
337    /// Admission complexity remains within the bounded proof envelope.
338    AdmissionComplexity,
339    /// Protocol-envelope bridge escalation windows are bounded.
340    ProtocolBridge,
341}
342
343/// Proof-carrying execution profile aligned with the Lean theorem-pack layer.
344#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
345pub struct ProtocolMachineExecutionProfile {
346    /// Fairness assumptions carried by the profile.
347    pub fairness_assumptions: BTreeSet<ProtocolMachineFairnessAssumption>,
348    /// Admissibility classes carried by the profile.
349    pub admissibility_classes: BTreeSet<ProtocolMachineAdmissibilityClass>,
350    /// Escalation-window classes carried by the profile.
351    pub escalation_window_classes: BTreeSet<ProtocolMachineEscalationWindowClass>,
352    /// Boolean theorem-pack eligibility inventory.
353    pub theorem_pack_eligibility: Vec<(String, bool)>,
354}
355
356impl ProtocolMachineExecutionProfile {
357    /// Full profile covering all currently modeled assumptions/classes.
358    #[must_use]
359    pub fn full() -> Self {
360        Self {
361            fairness_assumptions: [
362                ProtocolMachineFairnessAssumption::ScheduleConfluence,
363                ProtocolMachineFairnessAssumption::StarvationFreedom,
364                ProtocolMachineFairnessAssumption::LivenessFairness,
365            ]
366            .into_iter()
367            .collect(),
368            admissibility_classes: [
369                ProtocolMachineAdmissibilityClass::LocalEnvelope,
370                ProtocolMachineAdmissibilityClass::ShardedEnvelope,
371                ProtocolMachineAdmissibilityClass::ProtocolEnvelopeBridge,
372            ]
373            .into_iter()
374            .collect(),
375            escalation_window_classes: [
376                ProtocolMachineEscalationWindowClass::ProgressContract,
377                ProtocolMachineEscalationWindowClass::AdmissionComplexity,
378                ProtocolMachineEscalationWindowClass::ProtocolBridge,
379            ]
380            .into_iter()
381            .collect(),
382            theorem_pack_eligibility: vec![
383                ("protocol_machine_envelope_adherence".to_string(), true),
384                ("protocol_machine_envelope_admission".to_string(), true),
385                ("protocol_envelope_bridge".to_string(), true),
386            ],
387        }
388    }
389
390    fn eligibility(&self, key: &str) -> bool {
391        self.theorem_pack_eligibility
392            .iter()
393            .find(|entry| entry.0 == key)
394            .map(|entry| entry.1)
395            .unwrap_or(false)
396    }
397
398    /// Whether this profile supports protocol-machine envelope adherence.
399    #[must_use]
400    pub fn supports_protocol_machine_envelope_adherence(&self) -> bool {
401        self.eligibility("protocol_machine_envelope_adherence")
402    }
403
404    /// Whether this profile supports protocol-machine envelope admission.
405    #[must_use]
406    pub fn supports_protocol_machine_envelope_admission(&self) -> bool {
407        self.eligibility("protocol_machine_envelope_admission")
408    }
409
410    /// Whether this profile supports the protocol-envelope bridge.
411    #[must_use]
412    pub fn supports_protocol_envelope_bridge(&self) -> bool {
413        self.eligibility("protocol_envelope_bridge")
414    }
415
416    /// Transport semantics required by the enabled theorem-pack claims.
417    #[must_use]
418    pub fn transport_requirements(&self) -> TheoremTransportRequirements {
419        if self
420            .theorem_pack_eligibility
421            .iter()
422            .any(|(_, enabled)| *enabled)
423        {
424            TheoremTransportRequirements::protocol_origin_integrity()
425        } else {
426            TheoremTransportRequirements::none()
427        }
428    }
429}
430
431fn missing_transport_requirement(
432    requirements: TheoremTransportRequirements,
433    transport: &RuntimeTransportContract,
434) -> Option<&'static str> {
435    if requirements.role_addressed_routing && !transport.role_addressed_routing {
436        Some("role_addressed_routing")
437    } else if requirements.authenticated_peers && !transport.authenticated_peers {
438        Some("authenticated_peers")
439    } else if requirements.per_peer_fifo_delivery && !transport.per_peer_fifo_delivery {
440        Some("per_peer_fifo_delivery")
441    } else if requirements.fail_closed_unknown_role && !transport.fail_closed_unknown_role {
442        Some("fail_closed_unknown_role")
443    } else if requirements.no_message_synthesis && !transport.no_message_synthesis {
444        Some("no_message_synthesis")
445    } else {
446        None
447    }
448}
449
450/// Validate selected transport contracts against an execution profile's theorem claims.
451///
452/// Every selected transport must satisfy the required semantic fields because a
453/// single weaker path can invalidate origin/order assumptions used by the
454/// theorem pack.
455///
456/// # Errors
457///
458/// Returns [`TransportContractGateError`] when theorem claims require transport
459/// evidence and no selected contract is supplied, or when any selected
460/// transport lacks a required semantic field.
461pub fn validate_transport_contracts_for_execution_profile(
462    profile: &ProtocolMachineExecutionProfile,
463    transports: &[RuntimeTransportContract],
464) -> Result<(), TransportContractGateError> {
465    let requirements = profile.transport_requirements();
466    if requirements.is_empty() {
467        return Ok(());
468    }
469    if transports.is_empty() {
470        return Err(TransportContractGateError::MissingTransportContracts);
471    }
472    for transport in transports {
473        if let Some(requirement) = missing_transport_requirement(requirements, transport) {
474            return Err(
475                TransportContractGateError::UnsatisfiedTransportRequirement {
476                    transport_name: transport.transport_name.clone(),
477                    requirement,
478                },
479            );
480        }
481    }
482    Ok(())
483}
484
485/// Canonical transported-theorem boundary ledger for admission and guarantee surfaces.
486#[must_use]
487pub fn transported_theorem_boundary() -> Vec<TransportedTheoremBoundaryEntry> {
488    let mut boundary = black_box_transported_theorem_entries();
489    boundary.extend(runtime_critical_transported_theorem_entries());
490    boundary.extend(documentation_background_transported_theorem_entries());
491    boundary
492}
493
494fn boundary_entry(
495    key: &str,
496    usage_class: TransportedTheoremUsageClass,
497    consumed_by_rust_runtime_admission: bool,
498    consumed_by_lean_runtime_gate: bool,
499    assumption_boundary: Option<&str>,
500) -> TransportedTheoremBoundaryEntry {
501    TransportedTheoremBoundaryEntry {
502        key: key.to_string(),
503        usage_class,
504        consumed_by_rust_runtime_admission,
505        consumed_by_lean_runtime_gate,
506        assumption_boundary: assumption_boundary.map(str::to_string),
507    }
508}
509
510fn black_box_transported_theorem_entries() -> Vec<TransportedTheoremBoundaryEntry> {
511    use TransportedTheoremUsageClass::BlackBoxPremiseOnly;
512
513    [
514        "termination",
515        "output_condition_soundness",
516        "flp_lower_bound",
517        "flp_impossibility",
518        "cap_impossibility",
519        "quorum_geometry_safety",
520        "partial_synchrony_liveness",
521        "responsiveness",
522        "nakamoto_security",
523        "reconfiguration_safety",
524        "atomic_broadcast_ordering",
525        "accountable_safety",
526        "failure_detector_boundaries",
527        "data_availability_retrievability",
528        "coordination_characterization",
529        "crdt_envelope_and_equivalence",
530        "consensus_envelope",
531        "failure_envelope",
532        "effect_interface_bridge",
533    ]
534    .into_iter()
535    .map(|key| boundary_entry(key, BlackBoxPremiseOnly, false, false, None))
536    .collect()
537}
538
539fn runtime_critical_transported_theorem_entries() -> Vec<TransportedTheoremBoundaryEntry> {
540    use TransportedTheoremUsageClass::RuntimeCriticalInstantiatedPremise;
541
542    vec![
543        boundary_entry(
544            "byzantine_safety_characterization",
545            RuntimeCriticalInstantiatedPremise,
546            false,
547            true,
548            Some(
549                "Lean theorem-pack gate only. Rust runtime admission does not currently consume this key.",
550            ),
551        ),
552        boundary_entry(
553            "protocol_machine_envelope_adherence",
554            RuntimeCriticalInstantiatedPremise,
555            true,
556            true,
557            None,
558        ),
559        boundary_entry(
560            "protocol_machine_envelope_admission",
561            RuntimeCriticalInstantiatedPremise,
562            true,
563            true,
564            None,
565        ),
566        boundary_entry(
567            "protocol_envelope_bridge",
568            RuntimeCriticalInstantiatedPremise,
569            true,
570            true,
571            None,
572        ),
573    ]
574}
575
576fn documentation_background_transported_theorem_entries() -> Vec<TransportedTheoremBoundaryEntry> {
577    use TransportedTheoremUsageClass::DocumentationBackgroundOnly;
578
579    [
580        "classical_foster",
581        "classical_maxweight",
582        "classical_ldp",
583        "classical_mean_field",
584        "classical_heavy_traffic",
585        "classical_mixing",
586        "classical_fluid",
587        "classical_concentration",
588        "classical_littles_law",
589        "classical_functional_clt",
590        "classical_spectral_gap_termination",
591    ]
592    .into_iter()
593    .map(|key| boundary_entry(key, DocumentationBackgroundOnly, false, false, None))
594    .collect()
595}
596
597/// Runtime-critical transported theorem families.
598#[must_use]
599pub fn runtime_critical_transported_theorem_boundary() -> Vec<TransportedTheoremBoundaryEntry> {
600    transported_theorem_boundary()
601        .into_iter()
602        .filter(|entry| {
603            matches!(
604                entry.usage_class,
605                TransportedTheoremUsageClass::RuntimeCriticalInstantiatedPremise
606            )
607        })
608        .collect()
609}
610
611/// Transported-theorem keys consumed by shipped Rust runtime admission.
612#[must_use]
613pub fn rust_runtime_critical_transport_theorem_keys() -> Vec<String> {
614    runtime_critical_transported_theorem_boundary()
615        .into_iter()
616        .filter(|entry| entry.consumed_by_rust_runtime_admission)
617        .map(|entry| entry.key)
618        .collect()
619}
620
621/// Validate that the canonical transported-theorem ledger and shipped runtime
622/// execution-profile keys stay in exact correspondence.
623///
624/// # Errors
625///
626/// Returns an error when the transported-theorem ledger and runtime profile
627/// disagree about which theorem-pack keys are runtime-critical, enabled, or
628/// guarded by an explicit assumption boundary.
629pub fn validate_transported_theorem_boundary_consistency(
630    boundary: &[TransportedTheoremBoundaryEntry],
631    profile: &ProtocolMachineExecutionProfile,
632) -> Result<(), TransportedTheoremBoundaryValidationError> {
633    use TransportedTheoremBoundaryValidationError::{
634        LeanOnlyRuntimeCriticalMissingAssumptionBoundary, RuntimeProfileDisablesRustAdmissionKey,
635        RuntimeProfileEnablesUnknownRustAdmissionKey, RuntimeProfileMissingRustAdmissionKey,
636        RustAdmissionKeyNotRuntimeCritical,
637    };
638    use TransportedTheoremUsageClass::RuntimeCriticalInstantiatedPremise;
639
640    let rust_runtime_keys: BTreeSet<_> = boundary
641        .iter()
642        .filter(|entry| entry.consumed_by_rust_runtime_admission)
643        .map(|entry| entry.key.as_str())
644        .collect();
645    let enabled_profile_keys: BTreeSet<_> = profile
646        .theorem_pack_eligibility
647        .iter()
648        .filter_map(|(key, enabled)| enabled.then_some(key.as_str()))
649        .collect();
650
651    for entry in boundary {
652        if entry.consumed_by_rust_runtime_admission
653            && !matches!(entry.usage_class, RuntimeCriticalInstantiatedPremise)
654        {
655            return Err(RustAdmissionKeyNotRuntimeCritical(entry.key.clone()));
656        }
657        if matches!(entry.usage_class, RuntimeCriticalInstantiatedPremise)
658            && !entry.consumed_by_rust_runtime_admission
659            && entry.consumed_by_lean_runtime_gate
660            && entry.assumption_boundary.is_none()
661        {
662            return Err(LeanOnlyRuntimeCriticalMissingAssumptionBoundary(
663                entry.key.clone(),
664            ));
665        }
666        if entry.consumed_by_rust_runtime_admission {
667            match profile
668                .theorem_pack_eligibility
669                .iter()
670                .find(|(key, _)| key == &entry.key)
671            {
672                None => return Err(RuntimeProfileMissingRustAdmissionKey(entry.key.clone())),
673                Some((_, false)) => {
674                    return Err(RuntimeProfileDisablesRustAdmissionKey(entry.key.clone()))
675                }
676                Some((_, true)) => {}
677            }
678        }
679    }
680
681    for key in enabled_profile_keys {
682        if !rust_runtime_keys.contains(key) {
683            return Err(RuntimeProfileEnablesUnknownRustAdmissionKey(
684                key.to_string(),
685            ));
686        }
687    }
688
689    Ok(())
690}
691
692impl RuntimeCapability {
693    const ALL: [Self; 4] = [
694        Self::LiveMigration,
695        Self::AutoscaleRepartition,
696        Self::PlacementRefinement,
697        Self::RelaxedReordering,
698    ];
699
700    const fn key(self) -> &'static str {
701        match self {
702            Self::LiveMigration => "live_migration",
703            Self::AutoscaleRepartition => "autoscale_repartition",
704            Self::PlacementRefinement => "placement_refinement",
705            Self::RelaxedReordering => "relaxed_reordering",
706        }
707    }
708}
709
710/// Runtime contracts used for advanced-mode admission and capability gates.
711#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
712pub struct RuntimeContracts {
713    /// Determinism profile support artifacts.
714    pub determinism_artifacts: DeterminismArtifacts,
715    /// Whether mixed (non-full) determinism profiles are theorem-pack admitted.
716    pub can_use_mixed_determinism_profiles: bool,
717    /// Canonical capability set admitted by theorem-pack/runtime state.
718    pub capabilities: BTreeSet<RuntimeCapability>,
719    /// Proof-carrying execution profile aligned with Lean theorem-pack metadata.
720    pub execution_profile: ProtocolMachineExecutionProfile,
721    /// Transport profiles selected for theorem-backed execution.
722    pub transport_contracts: Vec<RuntimeTransportContract>,
723}
724
725impl RuntimeContracts {
726    /// Contract payload enabling all currently supported advanced runtime switches.
727    #[must_use]
728    pub fn full() -> Self {
729        Self {
730            determinism_artifacts: DeterminismArtifacts::default(),
731            can_use_mixed_determinism_profiles: true,
732            capabilities: RuntimeCapability::ALL.into_iter().collect(),
733            execution_profile: ProtocolMachineExecutionProfile::full(),
734            transport_contracts: vec![RuntimeTransportContract::first_party_in_memory()],
735        }
736    }
737
738    /// Replace selected transport contracts.
739    ///
740    /// Each selected transport contract is checked against the theorem-pack
741    /// execution profile before admission. Passing a trusted-network-only
742    /// contract intentionally rejects theorem claims that require authenticated
743    /// protocol origins.
744    #[must_use]
745    pub fn with_transport_contracts(
746        mut self,
747        contracts: impl IntoIterator<Item = RuntimeTransportContract>,
748    ) -> Self {
749        self.transport_contracts = contracts.into_iter().collect();
750        self
751    }
752}
753
754/// Build the canonical runtime execution profile for one config/contract pair.
755#[must_use]
756pub fn runtime_execution_profile(
757    cfg: &ProtocolMachineConfig,
758    contracts: Option<&RuntimeContracts>,
759) -> ProtocolMachineExecutionProfile {
760    let mut profile = ProtocolMachineExecutionProfile {
761        fairness_assumptions: [ProtocolMachineFairnessAssumption::ScheduleConfluence]
762            .into_iter()
763            .collect(),
764        admissibility_classes: [
765            ProtocolMachineAdmissibilityClass::LocalEnvelope,
766            ProtocolMachineAdmissibilityClass::ShardedEnvelope,
767        ]
768        .into_iter()
769        .collect(),
770        escalation_window_classes: [ProtocolMachineEscalationWindowClass::ProgressContract]
771            .into_iter()
772            .collect(),
773        theorem_pack_eligibility: vec![
774            ("protocol_machine_envelope_adherence".to_string(), true),
775            (
776                "protocol_machine_envelope_admission".to_string(),
777                contracts.is_some(),
778            ),
779            (
780                "protocol_envelope_bridge".to_string(),
781                !matches!(cfg.output_condition_policy, OutputConditionPolicy::Disabled),
782            ),
783        ],
784    };
785
786    if !matches!(cfg.sched_policy, SchedPolicy::Cooperative) {
787        profile
788            .fairness_assumptions
789            .insert(ProtocolMachineFairnessAssumption::StarvationFreedom);
790    }
791    if matches!(cfg.sched_policy, SchedPolicy::ProgressAware)
792        || !matches!(cfg.output_condition_policy, OutputConditionPolicy::Disabled)
793    {
794        profile
795            .fairness_assumptions
796            .insert(ProtocolMachineFairnessAssumption::LivenessFairness);
797    }
798    if contracts.is_some() {
799        profile
800            .escalation_window_classes
801            .insert(ProtocolMachineEscalationWindowClass::AdmissionComplexity);
802    }
803    if !matches!(cfg.output_condition_policy, OutputConditionPolicy::Disabled) {
804        profile
805            .admissibility_classes
806            .insert(ProtocolMachineAdmissibilityClass::ProtocolEnvelopeBridge);
807        profile
808            .escalation_window_classes
809            .insert(ProtocolMachineEscalationWindowClass::ProtocolBridge);
810    }
811
812    profile
813}
814
815/// Whether one proof-carrying execution profile supports the requested runtime config.
816#[must_use]
817pub fn execution_profile_supported(
818    profile: &ProtocolMachineExecutionProfile,
819    cfg: &ProtocolMachineConfig,
820    contracts: Option<&RuntimeContracts>,
821) -> bool {
822    let required = runtime_execution_profile(cfg, contracts);
823    let supports_adherence = required.supports_protocol_machine_envelope_adherence();
824    let supports_admission = required.supports_protocol_machine_envelope_admission();
825    let supports_bridge = required.supports_protocol_envelope_bridge();
826    required
827        .fairness_assumptions
828        .into_iter()
829        .all(|assumption| profile.fairness_assumptions.contains(&assumption))
830        && required
831            .admissibility_classes
832            .into_iter()
833            .all(|class| profile.admissibility_classes.contains(&class))
834        && required
835            .escalation_window_classes
836            .into_iter()
837            .all(|class| profile.escalation_window_classes.contains(&class))
838        && (!supports_adherence || profile.supports_protocol_machine_envelope_adherence())
839        && (!supports_admission || profile.supports_protocol_machine_envelope_admission())
840        && (!supports_bridge || profile.supports_protocol_envelope_bridge())
841}
842
843fn sched_policy_requires_contracts(policy: &SchedPolicy) -> bool {
844    !matches!(policy, SchedPolicy::Cooperative)
845}
846
847/// Whether protocol-machine config requires runtime contracts for admission.
848#[must_use]
849pub fn requires_protocol_machine_runtime_contracts(cfg: &ProtocolMachineConfig) -> bool {
850    sched_policy_requires_contracts(&cfg.sched_policy) || cfg.speculation_enabled
851}
852
853/// Protocol-machine admission gate for advanced runtime modes.
854#[must_use]
855pub fn admit_protocol_machine_runtime(
856    cfg: &ProtocolMachineConfig,
857    contracts: Option<&RuntimeContracts>,
858) -> RuntimeAdmissionResult {
859    if requires_protocol_machine_runtime_contracts(cfg) && contracts.is_none() {
860        RuntimeAdmissionResult::RejectedMissingContracts
861    } else {
862        RuntimeAdmissionResult::Admitted
863    }
864}
865
866/// Check artifact support for one determinism profile.
867#[must_use]
868pub fn determinism_profile_supported(
869    artifacts: &DeterminismArtifacts,
870    profile: DeterminismMode,
871) -> bool {
872    match profile {
873        DeterminismMode::Full => artifacts.full,
874        DeterminismMode::ModuloEffects => artifacts.modulo_effect_trace,
875        DeterminismMode::ModuloCommutativity => artifacts.modulo_commutativity,
876        DeterminismMode::Replay => artifacts.replay,
877    }
878}
879
880/// Runtime profile selection gate with mixed-profile capability checks.
881#[must_use]
882pub fn request_determinism_profile(
883    contracts: &RuntimeContracts,
884    profile: DeterminismMode,
885) -> Option<DeterminismMode> {
886    let supported = determinism_profile_supported(&contracts.determinism_artifacts, profile);
887    if !supported {
888        return None;
889    }
890    match profile {
891        DeterminismMode::Full => Some(profile),
892        DeterminismMode::ModuloEffects
893        | DeterminismMode::ModuloCommutativity
894        | DeterminismMode::Replay => contracts
895            .can_use_mixed_determinism_profiles
896            .then_some(profile),
897    }
898}
899
900/// Unified runtime gate check for advanced-mode admission and profile support.
901#[must_use]
902pub fn enforce_protocol_machine_runtime_gates(
903    cfg: &ProtocolMachineConfig,
904    contracts: Option<&RuntimeContracts>,
905) -> RuntimeGateResult {
906    match admit_protocol_machine_runtime(cfg, contracts) {
907        RuntimeAdmissionResult::RejectedMissingContracts => {
908            RuntimeGateResult::RejectedMissingContracts
909        }
910        RuntimeAdmissionResult::Admitted => match contracts {
911            Some(contracts) => {
912                if request_determinism_profile(contracts, cfg.determinism_mode).is_some() {
913                    RuntimeGateResult::Admitted
914                } else {
915                    RuntimeGateResult::RejectedUnsupportedDeterminismProfile
916                }
917            }
918            None => {
919                if matches!(cfg.determinism_mode, DeterminismMode::Full) {
920                    RuntimeGateResult::Admitted
921                } else {
922                    RuntimeGateResult::RejectedUnsupportedDeterminismProfile
923                }
924            }
925        },
926    }
927}
928
929/// Runtime capability snapshot emitted at startup.
930#[must_use]
931pub fn runtime_capability_snapshot(contracts: &RuntimeContracts) -> Vec<(String, bool)> {
932    RuntimeCapability::ALL
933        .into_iter()
934        .map(|capability| {
935            (
936                capability.key().to_string(),
937                contracts.capabilities.contains(&capability),
938            )
939        })
940        .collect()
941}
942
943#[cfg(test)]
944mod tests {
945    use super::*;
946
947    #[test]
948    fn admission_requires_contracts_for_advanced_modes() {
949        let mut cfg = ProtocolMachineConfig::default();
950        assert_eq!(
951            admit_protocol_machine_runtime(&cfg, None),
952            RuntimeAdmissionResult::Admitted
953        );
954
955        cfg.speculation_enabled = true;
956        assert_eq!(
957            admit_protocol_machine_runtime(&cfg, None),
958            RuntimeAdmissionResult::RejectedMissingContracts
959        );
960        assert_eq!(
961            admit_protocol_machine_runtime(&cfg, Some(&RuntimeContracts::full())),
962            RuntimeAdmissionResult::Admitted
963        );
964    }
965
966    #[test]
967    fn request_determinism_profile_obeys_artifacts_and_mixed_gate() {
968        let mut contracts = RuntimeContracts::full();
969        contracts.can_use_mixed_determinism_profiles = false;
970        assert_eq!(
971            request_determinism_profile(&contracts, DeterminismMode::Full),
972            Some(DeterminismMode::Full)
973        );
974        assert_eq!(
975            request_determinism_profile(&contracts, DeterminismMode::Replay),
976            None
977        );
978
979        contracts.can_use_mixed_determinism_profiles = true;
980        contracts.determinism_artifacts.replay = false;
981        assert_eq!(
982            request_determinism_profile(&contracts, DeterminismMode::Replay),
983            None
984        );
985        contracts.determinism_artifacts.replay = true;
986        assert_eq!(
987            request_determinism_profile(&contracts, DeterminismMode::Replay),
988            Some(DeterminismMode::Replay)
989        );
990    }
991
992    #[test]
993    #[allow(clippy::field_reassign_with_default)]
994    fn unified_runtime_gate_combines_admission_and_profile_checks() {
995        let mut cfg = ProtocolMachineConfig::default();
996        cfg.speculation_enabled = true;
997        assert_eq!(
998            enforce_protocol_machine_runtime_gates(&cfg, None),
999            RuntimeGateResult::RejectedMissingContracts
1000        );
1001
1002        let mut contracts = RuntimeContracts::full();
1003        contracts.determinism_artifacts.replay = false;
1004        cfg.determinism_mode = DeterminismMode::Replay;
1005        assert_eq!(
1006            enforce_protocol_machine_runtime_gates(&cfg, Some(&contracts)),
1007            RuntimeGateResult::RejectedUnsupportedDeterminismProfile
1008        );
1009
1010        contracts.determinism_artifacts.replay = true;
1011        assert_eq!(
1012            enforce_protocol_machine_runtime_gates(&cfg, Some(&contracts)),
1013            RuntimeGateResult::Admitted
1014        );
1015    }
1016
1017    #[test]
1018    fn capability_snapshot_is_derived_from_canonical_capability_set() {
1019        let mut contracts = RuntimeContracts::full();
1020        contracts
1021            .capabilities
1022            .remove(&RuntimeCapability::RelaxedReordering);
1023
1024        let snapshot = runtime_capability_snapshot(&contracts);
1025        assert_eq!(
1026            snapshot,
1027            vec![
1028                ("live_migration".to_string(), true),
1029                ("autoscale_repartition".to_string(), true),
1030                ("placement_refinement".to_string(), true),
1031                ("relaxed_reordering".to_string(), false),
1032            ]
1033        );
1034    }
1035
1036    #[test]
1037    #[allow(clippy::field_reassign_with_default)]
1038    fn runtime_execution_profile_tracks_scheduler_and_bridge_requirements() {
1039        let mut cfg = ProtocolMachineConfig::default();
1040        cfg.sched_policy = SchedPolicy::ProgressAware;
1041        cfg.output_condition_policy = OutputConditionPolicy::AllowAll;
1042
1043        let profile = runtime_execution_profile(&cfg, Some(&RuntimeContracts::full()));
1044        assert!(profile
1045            .fairness_assumptions
1046            .contains(&ProtocolMachineFairnessAssumption::LivenessFairness));
1047        assert!(profile
1048            .admissibility_classes
1049            .contains(&ProtocolMachineAdmissibilityClass::ProtocolEnvelopeBridge));
1050        assert!(profile.supports_protocol_envelope_bridge());
1051        assert!(execution_profile_supported(
1052            &ProtocolMachineExecutionProfile::full(),
1053            &cfg,
1054            Some(&RuntimeContracts::full())
1055        ));
1056    }
1057
1058    #[test]
1059    fn theorem_transport_requirements_reject_missing_contracts() {
1060        let profile = ProtocolMachineExecutionProfile::full();
1061        assert_eq!(
1062            validate_transport_contracts_for_execution_profile(&profile, &[]),
1063            Err(TransportContractGateError::MissingTransportContracts)
1064        );
1065    }
1066
1067    #[test]
1068    fn theorem_transport_requirements_accept_in_memory_profile() {
1069        let profile = ProtocolMachineExecutionProfile::full();
1070        assert_eq!(
1071            validate_transport_contracts_for_execution_profile(
1072                &profile,
1073                &[RuntimeTransportContract::first_party_in_memory()]
1074            ),
1075            Ok(())
1076        );
1077    }
1078
1079    #[test]
1080    fn theorem_transport_requirements_reject_unauthenticated_profile_for_authenticated_claims() {
1081        let profile = ProtocolMachineExecutionProfile::full();
1082        let unauthenticated = RuntimeTransportContract::new("UnauthenticatedTransport", "Network")
1083            .with_role_addressed_routing(true)
1084            .with_per_peer_fifo_delivery(true)
1085            .with_fail_closed_unknown_role(true)
1086            .with_no_message_synthesis(true)
1087            .with_explicit_readiness_errors(true);
1088        assert_eq!(
1089            validate_transport_contracts_for_execution_profile(&profile, &[unauthenticated]),
1090            Err(
1091                TransportContractGateError::UnsatisfiedTransportRequirement {
1092                    transport_name: "UnauthenticatedTransport".to_string(),
1093                    requirement: "authenticated_peers",
1094                }
1095            )
1096        );
1097    }
1098
1099    #[test]
1100    fn transported_theorem_boundary_makes_rust_runtime_subset_exact() {
1101        let boundary = transported_theorem_boundary();
1102        let rust_runtime_keys = rust_runtime_critical_transport_theorem_keys();
1103        let profile = ProtocolMachineExecutionProfile::full();
1104        let profile_keys: Vec<_> = profile
1105            .theorem_pack_eligibility
1106            .iter()
1107            .map(|(key, _)| key.clone())
1108            .collect();
1109
1110        assert_eq!(
1111            rust_runtime_keys, profile_keys,
1112            "shipped Rust runtime admission must consume exactly the classified runtime-critical theorem keys"
1113        );
1114        assert_eq!(
1115            validate_transported_theorem_boundary_consistency(&boundary, &profile),
1116            Ok(())
1117        );
1118        assert!(
1119            boundary.iter().any(|entry| {
1120                entry.key == "byzantine_safety_characterization"
1121                    && matches!(
1122                        entry.usage_class,
1123                        TransportedTheoremUsageClass::RuntimeCriticalInstantiatedPremise
1124                    )
1125                    && !entry.consumed_by_rust_runtime_admission
1126                    && entry.consumed_by_lean_runtime_gate
1127            }),
1128            "Lean-only runtime-critical theorem gates must remain explicit in the boundary ledger"
1129        );
1130    }
1131
1132    #[test]
1133    fn transported_theorem_boundary_requires_instantiation_or_assumption_boundary() {
1134        for entry in runtime_critical_transported_theorem_boundary() {
1135            assert!(
1136                entry.consumed_by_rust_runtime_admission || entry.assumption_boundary.is_some(),
1137                "runtime-critical theorem {} must have a Rust instantiation path or an explicit assumption boundary",
1138                entry.key
1139            );
1140        }
1141    }
1142
1143    #[test]
1144    fn transported_theorem_boundary_fail_closes_when_runtime_profile_key_drifts() {
1145        let boundary = transported_theorem_boundary();
1146        let mut profile = ProtocolMachineExecutionProfile::full();
1147        profile.theorem_pack_eligibility[0].0 = "protocol_machine_envelope_adherence_typo".into();
1148
1149        assert_eq!(
1150            validate_transported_theorem_boundary_consistency(&boundary, &profile),
1151            Err(
1152                TransportedTheoremBoundaryValidationError::RuntimeProfileMissingRustAdmissionKey(
1153                    "protocol_machine_envelope_adherence".into()
1154                )
1155            )
1156        );
1157    }
1158
1159    #[test]
1160    fn transported_theorem_boundary_fail_closes_when_runtime_profile_enables_unknown_key() {
1161        let boundary = transported_theorem_boundary();
1162        let mut profile = ProtocolMachineExecutionProfile::full();
1163        profile
1164            .theorem_pack_eligibility
1165            .push(("unknown_runtime_boundary".into(), true));
1166
1167        assert_eq!(
1168            validate_transported_theorem_boundary_consistency(&boundary, &profile),
1169            Err(
1170                TransportedTheoremBoundaryValidationError::RuntimeProfileEnablesUnknownRustAdmissionKey(
1171                    "unknown_runtime_boundary".into()
1172                )
1173            )
1174        );
1175    }
1176
1177    #[test]
1178    fn transported_theorem_boundary_fail_closes_when_runtime_classification_drifts() {
1179        let mut boundary = transported_theorem_boundary();
1180        let profile = ProtocolMachineExecutionProfile::full();
1181        let bridge_entry = boundary
1182            .iter_mut()
1183            .find(|entry| entry.key == "protocol_envelope_bridge")
1184            .expect("canonical boundary should classify protocol_envelope_bridge");
1185        bridge_entry.usage_class = TransportedTheoremUsageClass::BlackBoxPremiseOnly;
1186
1187        assert_eq!(
1188            validate_transported_theorem_boundary_consistency(&boundary, &profile),
1189            Err(
1190                TransportedTheoremBoundaryValidationError::RustAdmissionKeyNotRuntimeCritical(
1191                    "protocol_envelope_bridge".into()
1192                )
1193            )
1194        );
1195    }
1196
1197    #[test]
1198    fn transported_theorem_boundary_fail_closes_when_lean_only_runtime_critical_entry_loses_assumption_boundary(
1199    ) {
1200        let mut boundary = transported_theorem_boundary();
1201        let profile = ProtocolMachineExecutionProfile::full();
1202        let byzantine = boundary
1203            .iter_mut()
1204            .find(|entry| entry.key == "byzantine_safety_characterization")
1205            .expect("canonical boundary should classify byzantine_safety_characterization");
1206        byzantine.assumption_boundary = None;
1207
1208        assert_eq!(
1209            validate_transported_theorem_boundary_consistency(&boundary, &profile),
1210            Err(
1211                TransportedTheoremBoundaryValidationError::LeanOnlyRuntimeCriticalMissingAssumptionBoundary(
1212                    "byzantine_safety_characterization".into()
1213                )
1214            )
1215        );
1216    }
1217}
telltale_machine/runtime_contracts.rs

telltale_machine/
runtime_contracts.rs
