telltale_bridge/
invariants.rs

1//! Typed invariant-claims schema for proof-oriented protocol bundles.
2
3use std::collections::BTreeMap;
4use std::sync::Arc;
5
6use serde::{Deserialize, Serialize};
7use serde_json::Value;
8use telltale_machine::composition::{CompositionCertificate, ReconfigurationPolicy};
9use telltale_machine::runtime::loader::CodeImage;
10use telltale_machine::ProtocolBundle as MachineProtocolBundle;
11use telltale_types::{FixedQ32, GlobalType, LocalTypeR};
12
13use crate::export::{global_to_json, local_to_json};
14use crate::import::{json_to_global, json_to_local};
15
16/// Schema version for protocol-bundle payloads.
17pub const PROTOCOL_BUNDLE_SCHEMA_VERSION: &str = "protocol_bundle.v1";
18
19#[must_use]
20pub fn canonical_protocol_bundle_schema_version() -> String {
21    PROTOCOL_BUNDLE_SCHEMA_VERSION.to_string()
22}
23
24fn deserialize_protocol_bundle_schema_version<'de, D>(deserializer: D) -> Result<String, D::Error>
25where
26    D: serde::Deserializer<'de>,
27{
28    let version = String::deserialize(deserializer)?;
29    if version == PROTOCOL_BUNDLE_SCHEMA_VERSION {
30        Ok(version)
31    } else {
32        Err(serde::de::Error::custom(format!(
33            "unsupported schema_version '{version}'; expected '{PROTOCOL_BUNDLE_SCHEMA_VERSION}'"
34        )))
35    }
36}
37
38#[derive(Clone, Debug, Default, Serialize, Deserialize)]
39pub enum SchedulerKind {
40    #[default]
41    Cooperative,
42    RoundRobin,
43    Priority,
44    ProgressAware,
45}
46
47#[derive(Clone, Debug, Default, Serialize, Deserialize)]
48pub enum FaultModel {
49    #[default]
50    Crash,
51    Byzantine,
52    Hybrid,
53}
54
55#[derive(Clone, Debug, Default, Serialize, Deserialize)]
56pub enum TimingModel {
57    #[default]
58    Asynchronous,
59    PartialSynchrony,
60    Synchronous,
61}
62
63#[derive(Clone, Debug, Default, Serialize, Deserialize)]
64pub enum ConsistencyLevel {
65    #[default]
66    Linearizable,
67    Sequential,
68    Eventual,
69}
70
71#[derive(Clone, Debug, Default, Serialize, Deserialize)]
72pub enum AvailabilityLevel {
73    #[default]
74    Total,
75    BoundedDegradation,
76    BestEffort,
77}
78
79#[derive(Clone, Debug, Default, Serialize, Deserialize)]
80pub enum PartitionModel {
81    #[default]
82    None,
83    CrashOnly,
84    NetworkSplit,
85}
86
87#[derive(Clone, Debug, Default, Serialize, Deserialize)]
88pub enum QuorumSystemKind {
89    #[default]
90    Majority,
91    Weighted,
92    Flexible,
93}
94
95#[derive(Clone, Debug, Default, Serialize, Deserialize)]
96pub struct LivenessConfig {
97    pub scheduler: SchedulerKind,
98    pub fairness_k: Option<usize>,
99    pub progress_required: bool,
100}
101
102#[derive(Clone, Debug, Default, Serialize, Deserialize)]
103pub struct FLPConfig {
104    pub crash_bound: usize,
105    pub requires_determinism: bool,
106}
107
108#[derive(Clone, Debug, Default, Serialize, Deserialize)]
109pub struct CAPConfig {
110    pub consistency: ConsistencyLevel,
111    pub availability: AvailabilityLevel,
112    pub partition_model: PartitionModel,
113}
114
115#[derive(Clone, Debug, Default, Serialize, Deserialize)]
116pub struct QuorumGeometryConfig {
117    pub quorum_system: QuorumSystemKind,
118    pub n: usize,
119    pub quorum_size: usize,
120    pub intersection_size: usize,
121}
122
123#[derive(Clone, Debug, Default, Serialize, Deserialize)]
124pub struct PartialSynchronyConfig {
125    pub timing: TimingModel,
126    pub delta_bound: Option<usize>,
127}
128
129#[derive(Clone, Debug, Default, Serialize, Deserialize)]
130pub struct ResponsivenessConfig {
131    pub leader_based: bool,
132    pub requires_stable_period: bool,
133}
134
135#[derive(Clone, Debug, Default, Serialize, Deserialize)]
136pub struct NakamotoConfig {
137    pub honest_fraction: FixedQ32,
138    pub finality_depth: usize,
139}
140
141#[derive(Clone, Debug, Default, Serialize, Deserialize)]
142pub struct ReconfigurationConfig {
143    pub dynamic_membership: bool,
144    pub overlap_required: bool,
145}
146
147#[derive(Clone, Debug, Default, Serialize, Deserialize)]
148pub struct AtomicBroadcastConfig {
149    pub total_order: bool,
150    pub valid_delivery: bool,
151}
152
153#[derive(Clone, Debug, Default, Serialize, Deserialize)]
154pub struct AccountableSafetyConfig {
155    pub enabled: bool,
156}
157
158#[derive(Clone, Debug, Default, Serialize, Deserialize)]
159pub struct FailureDetectorsConfig {
160    pub enabled: bool,
161}
162
163#[derive(Clone, Debug, Default, Serialize, Deserialize)]
164pub struct DataAvailabilityConfig {
165    pub enabled: bool,
166}
167
168#[derive(Clone, Debug, Default, Serialize, Deserialize)]
169pub struct CoordinationConfig {
170    pub enabled: bool,
171}
172
173#[derive(Clone, Debug, Default, Serialize, Deserialize)]
174pub struct CRDTConfig {
175    pub enabled: bool,
176}
177
178#[derive(Clone, Debug, Default, Serialize, Deserialize)]
179pub struct ByzantineSafetyConfig {
180    pub enabled: bool,
181}
182
183#[derive(Clone, Debug, Default, Serialize, Deserialize)]
184pub struct ConsensusEnvelopeConfig {
185    pub enabled: bool,
186}
187
188#[derive(Clone, Debug, Default, Serialize, Deserialize)]
189pub struct FailureEnvelopeConfig {
190    pub enabled: bool,
191}
192
193#[derive(Clone, Debug, Default, Serialize, Deserialize)]
194pub struct ProtocolMachineEnvelopeAdherenceConfig {
195    pub enabled: bool,
196}
197
198#[derive(Clone, Debug, Default, Serialize, Deserialize)]
199pub struct ProtocolMachineEnvelopeAdmissionConfig {
200    pub enabled: bool,
201}
202
203#[derive(Clone, Debug, Default, Serialize, Deserialize)]
204pub struct ProtocolEnvelopeBridgeConfig {
205    pub enabled: bool,
206}
207
208#[derive(Clone, Debug, Default, Serialize, Deserialize)]
209pub struct DistributedClaims {
210    #[serde(default)]
211    pub fault_model: FaultModel,
212    pub flp: Option<FLPConfig>,
213    pub cap: Option<CAPConfig>,
214    pub quorum_geometry: Option<QuorumGeometryConfig>,
215    pub partial_synchrony: Option<PartialSynchronyConfig>,
216    pub responsiveness: Option<ResponsivenessConfig>,
217    pub nakamoto: Option<NakamotoConfig>,
218    pub reconfiguration: Option<ReconfigurationConfig>,
219    pub atomic_broadcast: Option<AtomicBroadcastConfig>,
220    pub accountable_safety: Option<AccountableSafetyConfig>,
221    pub failure_detectors: Option<FailureDetectorsConfig>,
222    pub data_availability: Option<DataAvailabilityConfig>,
223    pub coordination: Option<CoordinationConfig>,
224    pub crdt: Option<CRDTConfig>,
225    pub byzantine_safety: Option<ByzantineSafetyConfig>,
226    pub consensus_envelope: Option<ConsensusEnvelopeConfig>,
227    pub failure_envelope: Option<FailureEnvelopeConfig>,
228    pub protocol_machine_envelope_adherence: Option<ProtocolMachineEnvelopeAdherenceConfig>,
229    pub protocol_machine_envelope_admission: Option<ProtocolMachineEnvelopeAdmissionConfig>,
230    pub protocol_envelope_bridge: Option<ProtocolEnvelopeBridgeConfig>,
231}
232
233#[derive(Clone, Debug, Default, Serialize, Deserialize)]
234pub struct FosterConfig {
235    pub enabled: bool,
236}
237
238#[derive(Clone, Debug, Default, Serialize, Deserialize)]
239pub struct MaxWeightConfig {
240    pub enabled: bool,
241    pub slack: Option<FixedQ32>,
242}
243
244#[derive(Clone, Debug, Default, Serialize, Deserialize)]
245pub struct LDPConfig {
246    pub enabled: bool,
247}
248
249#[derive(Clone, Debug, Default, Serialize, Deserialize)]
250pub struct MeanFieldConfig {
251    pub enabled: bool,
252    pub population_size: Option<usize>,
253}
254
255#[derive(Clone, Debug, Default, Serialize, Deserialize)]
256pub struct HeavyTrafficConfig {
257    pub enabled: bool,
258}
259
260#[derive(Clone, Debug, Default, Serialize, Deserialize)]
261pub struct MixingConfig {
262    pub enabled: bool,
263    pub mixing_time_bound: Option<usize>,
264}
265
266#[derive(Clone, Debug, Default, Serialize, Deserialize)]
267pub struct FluidConfig {
268    pub enabled: bool,
269}
270
271#[derive(Clone, Debug, Default, Serialize, Deserialize)]
272pub struct ConcentrationConfig {
273    pub enabled: bool,
274}
275
276#[derive(Clone, Debug, Default, Serialize, Deserialize)]
277pub struct LittlesLawConfig {
278    pub enabled: bool,
279}
280
281#[derive(Clone, Debug, Default, Serialize, Deserialize)]
282pub struct FunctionalCLTConfig {
283    pub enabled: bool,
284}
285
286#[derive(Clone, Debug, Default, Serialize, Deserialize)]
287pub struct SpectralGapTerminationConfig {
288    pub enabled: bool,
289}
290
291#[derive(Clone, Debug, Default, Serialize, Deserialize)]
292pub struct ClassicalClaims {
293    pub foster: Option<FosterConfig>,
294    pub max_weight: Option<MaxWeightConfig>,
295    pub ldp: Option<LDPConfig>,
296    pub mean_field: Option<MeanFieldConfig>,
297    pub heavy_traffic: Option<HeavyTrafficConfig>,
298    pub mixing: Option<MixingConfig>,
299    pub fluid: Option<FluidConfig>,
300    pub concentration: Option<ConcentrationConfig>,
301    pub littles_law: Option<LittlesLawConfig>,
302    pub functional_clt: Option<FunctionalCLTConfig>,
303    pub spectral_gap_termination: Option<SpectralGapTerminationConfig>,
304}
305
306#[derive(Clone, Debug, Serialize, Deserialize)]
307pub struct InvariantClaims {
308    #[serde(deserialize_with = "crate::schema::deserialize_schema_version")]
309    pub schema_version: String,
310    pub liveness: Option<LivenessConfig>,
311    #[serde(default)]
312    pub distributed: DistributedClaims,
313    #[serde(default)]
314    pub classical: ClassicalClaims,
315}
316
317impl Default for InvariantClaims {
318    fn default() -> Self {
319        Self {
320            schema_version: crate::schema::canonical_schema_version(),
321            liveness: None,
322            distributed: DistributedClaims::default(),
323            classical: ClassicalClaims::default(),
324        }
325    }
326}
327
328#[derive(Clone, Debug, Serialize, Deserialize)]
329pub struct ProtocolBundle {
330    #[serde(deserialize_with = "deserialize_protocol_bundle_schema_version")]
331    pub schema_version: String,
332    pub global_type: Value,
333    pub local_types: BTreeMap<String, Value>,
334    pub claims: InvariantClaims,
335}
336
337/// Errors that can occur while converting an exported bridge bundle into a machine bundle.
338#[derive(Debug, thiserror::Error)]
339pub enum MachineBundleConversionError {
340    /// Global type JSON could not be parsed back into a Rust type.
341    #[error("failed to import global type from bridge bundle: {0}")]
342    GlobalImport(#[from] crate::ImportError),
343    /// One of the local type JSON payloads could not be parsed.
344    #[error("failed to import local type for role `{role}` from bridge bundle: {source}")]
345    LocalImport {
346        /// Role whose local type failed to import.
347        role: String,
348        /// Underlying import error.
349        source: crate::ImportError,
350    },
351}
352
353impl ProtocolBundle {
354    /// Reconfiguration claim carried by the bridge bundle, if any.
355    #[must_use]
356    pub fn reconfiguration_policy(&self) -> Option<ReconfigurationPolicy> {
357        self.claims
358            .distributed
359            .reconfiguration
360            .as_ref()
361            .map(|reconfiguration| ReconfigurationPolicy {
362                dynamic_membership: reconfiguration.dynamic_membership,
363                overlap_required: reconfiguration.overlap_required,
364            })
365    }
366
367    /// Convert this exported bundle into a machine bundle with the provided admission certificate.
368    ///
369    /// # Errors
370    ///
371    /// Returns `MachineBundleConversionError` when the exported global/local types cannot be
372    /// imported back into Rust machine artifacts.
373    pub fn to_machine_bundle(
374        &self,
375        certificate: CompositionCertificate,
376    ) -> Result<MachineProtocolBundle, MachineBundleConversionError> {
377        let global = json_to_global(&self.global_type)?;
378        let mut local_types = BTreeMap::new();
379        for (role, local) in &self.local_types {
380            let local_type = json_to_local(local).map_err(|source| {
381                MachineBundleConversionError::LocalImport {
382                    role: role.clone(),
383                    source,
384                }
385            })?;
386            local_types.insert(role.clone(), local_type);
387        }
388        let code = Arc::new(CodeImage::from_local_types(&local_types, &global));
389        let bundle = MachineProtocolBundle::new(code, certificate);
390        Ok(match self.reconfiguration_policy() {
391            Some(policy) => bundle.with_reconfiguration_policy(policy),
392            None => bundle,
393        })
394    }
395}
396
397/// Export a typed protocol bundle for Lean-side verification entrypoints.
398#[must_use]
399pub fn export_protocol_bundle(
400    global: &GlobalType,
401    local_types: &BTreeMap<String, LocalTypeR>,
402    claims: InvariantClaims,
403) -> ProtocolBundle {
404    let local_types = local_types
405        .iter()
406        .map(|(role, local)| (role.clone(), local_to_json(local)))
407        .collect();
408
409    ProtocolBundle {
410        schema_version: canonical_protocol_bundle_schema_version(),
411        global_type: global_to_json(global),
412        local_types,
413        claims,
414    }
415}
416
417#[cfg(test)]
418mod tests {
419    use super::*;
420    use telltale_types::{GlobalType, Label};
421
422    #[test]
423    fn test_export_protocol_bundle_includes_schema_and_claims() {
424        let global = GlobalType::send("A", "B", Label::new("msg"), GlobalType::End);
425        let mut locals = BTreeMap::new();
426        locals.insert(
427            "A".to_string(),
428            LocalTypeR::send("B", Label::new("msg"), LocalTypeR::End),
429        );
430        locals.insert(
431            "B".to_string(),
432            LocalTypeR::recv("A", Label::new("msg"), LocalTypeR::End),
433        );
434
435        let claims = InvariantClaims {
436            schema_version: crate::schema::canonical_schema_version(),
437            liveness: Some(LivenessConfig {
438                scheduler: SchedulerKind::RoundRobin,
439                fairness_k: Some(2),
440                progress_required: true,
441            }),
442            distributed: DistributedClaims {
443                flp: Some(FLPConfig {
444                    crash_bound: 1,
445                    requires_determinism: true,
446                }),
447                accountable_safety: Some(AccountableSafetyConfig { enabled: true }),
448                byzantine_safety: Some(ByzantineSafetyConfig { enabled: true }),
449                protocol_envelope_bridge: Some(ProtocolEnvelopeBridgeConfig { enabled: true }),
450                ..DistributedClaims::default()
451            },
452            classical: ClassicalClaims {
453                foster: Some(FosterConfig { enabled: true }),
454                ..ClassicalClaims::default()
455            },
456        };
457
458        let bundle = export_protocol_bundle(&global, &locals, claims);
459        assert_eq!(bundle.schema_version, PROTOCOL_BUNDLE_SCHEMA_VERSION);
460        assert_eq!(
461            bundle.claims.schema_version,
462            crate::schema::LEAN_BRIDGE_SCHEMA_VERSION
463        );
464        assert!(bundle.local_types.contains_key("A"));
465        assert!(bundle.local_types.contains_key("B"));
466    }
467}
telltale_bridge/invariants.rs

telltale_bridge/
invariants.rs
