telltale-types 14.0.0

Core session types for Telltale - matching Lean definitions
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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
//! Reconfiguration and placement types for protocol role migration.

use std::collections::{BTreeMap, BTreeSet};

use serde::{Deserialize, Serialize};

/// Canonical placement kind used by reconfiguration and recovery artifacts.
#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
pub enum PlacementKind {
    /// In-process placement.
    Local,
    /// Remote endpoint placement.
    Remote,
    /// Colocated with another role.
    Colocated,
}

/// Canonical placement observation for one active role.
#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
pub struct PlacementObservation {
    /// Stable role name.
    pub role: String,
    /// Canonical placement kind.
    pub kind: PlacementKind,
    /// Optional remote endpoint for remote roles.
    pub endpoint: Option<String>,
    /// Optional region hint.
    pub region: Option<String>,
    /// Peer role for colocated placement.
    pub colocated_with: Option<String>,
}

impl PlacementObservation {
    /// Construct a local placement observation.
    #[must_use]
    pub fn local(role: impl Into<String>) -> Self {
        Self {
            role: role.into(),
            kind: PlacementKind::Local,
            endpoint: None,
            region: None,
            colocated_with: None,
        }
    }

    /// Construct a remote placement observation.
    #[must_use]
    pub fn remote(role: impl Into<String>, endpoint: impl Into<String>) -> Self {
        Self {
            role: role.into(),
            kind: PlacementKind::Remote,
            endpoint: Some(endpoint.into()),
            region: None,
            colocated_with: None,
        }
    }

    /// Construct a colocated placement observation.
    #[must_use]
    pub fn colocated(role: impl Into<String>, peer: impl Into<String>) -> Self {
        Self {
            role: role.into(),
            kind: PlacementKind::Colocated,
            endpoint: None,
            region: None,
            colocated_with: Some(peer.into()),
        }
    }

    /// Attach a canonical region hint.
    #[must_use]
    pub fn with_region(mut self, region: impl Into<String>) -> Self {
        self.region = Some(region.into());
        self
    }
}

/// Derived transport boundary kind between two active roles.
#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
pub enum TransportBoundaryKind {
    /// Both roles are in the same process without an explicit colocated hop.
    InProcess,
    /// Roles share a node through explicit colocated placement.
    SharedMemory,
    /// At least one side is remote.
    Network,
}

/// Canonical transport-observable boundary derived from placement observations.
#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
pub struct TransportBoundaryObservation {
    /// Stable lower-sorted role name.
    pub from_role: String,
    /// Stable higher-sorted role name.
    pub to_role: String,
    /// Derived boundary kind.
    pub boundary: TransportBoundaryKind,
    /// Whether the two roles resolve to different explicit regions.
    pub cross_region: bool,
}

/// Canonical phase for a transition or runtime-upgrade artifact.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum TransitionArtifactPhase {
    /// Transition is staged but not yet admitted.
    Staged,
    /// Transition passed admission and compatibility checks.
    Admitted,
    /// Transition committed a new active runtime cutover.
    CommittedCutover,
    /// Transition was rolled back after staging/admission.
    RolledBack,
    /// Transition failed before commit.
    Failed,
}

/// Pending-effect treatment required for a specialized runtime upgrade.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum PendingEffectTreatment {
    /// Pending effects are carried across the cutover.
    PreservePending,
    /// Blocked/invalidated effects must be made explicit before cutover.
    InvalidateBlocked,
}

/// Canonical publication continuity policy required for a runtime upgrade.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum CanonicalPublicationContinuity {
    /// Existing canonical publications/handles must stay valid across the cutover.
    PreserveCanonicalTruth,
    /// Canonical publications may be invalidated and re-issued.
    ReissueCanonicalTruth,
}

/// Execution-profile constraint required for a runtime upgrade.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum RuntimeUpgradeExecutionConstraint {
    /// Preserve the admitted proof-carrying bundle profile.
    PreserveBundleProfile,
    /// Requires theorem-pack/runtime support for mixed determinism profiles.
    MixedDeterminismAllowed,
}

/// Canonical compatibility contract for one specialized runtime upgrade.
#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
pub struct RuntimeUpgradeCompatibility {
    /// Execution-profile constraint for the upgrade.
    pub execution_constraint: RuntimeUpgradeExecutionConstraint,
    /// Whether ownership continuity must be preserved across the cutover.
    pub ownership_continuity_required: bool,
    /// Pending-effect treatment policy.
    pub pending_effect_treatment: PendingEffectTreatment,
    /// Canonical publication continuity policy.
    pub canonical_publication_continuity: CanonicalPublicationContinuity,
}

/// Canonical serialized artifact for one runtime-upgrade transition phase.
#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
pub struct RuntimeUpgradeArtifact {
    /// Stable upgrade identifier.
    pub upgrade_id: String,
    /// Phase represented by this artifact.
    pub phase: TransitionArtifactPhase,
    /// Canonical sorted members before this phase.
    pub previous_members: Vec<String>,
    /// Canonical sorted members after this phase.
    pub next_members: Vec<String>,
    /// Compatibility contract admitted for this upgrade.
    pub compatibility: RuntimeUpgradeCompatibility,
    /// Canonical publication ids carried into the new runtime.
    pub carried_publication_ids: Vec<String>,
    /// Canonical publication ids invalidated by the cutover.
    pub invalidated_publication_ids: Vec<String>,
    /// Stable obligation ids carried into the new runtime.
    pub carried_obligation_ids: Vec<String>,
    /// Stable obligation ids invalidated by the cutover.
    pub invalidated_obligation_ids: Vec<String>,
    /// Optional failure/rollback reason.
    pub reason: Option<String>,
}

#[derive(Debug, Clone)]
struct ResolvedPlacement {
    node_key: String,
    region: Option<String>,
    uses_colocation: bool,
    remote: bool,
}

fn normalize_placement_observations(
    observations: &[PlacementObservation],
) -> Result<Vec<PlacementObservation>, String> {
    let mut normalized = observations.to_vec();
    normalized.sort_by(|left, right| left.role.cmp(&right.role));

    let mut seen_roles = BTreeSet::new();
    for observation in &normalized {
        if !seen_roles.insert(observation.role.clone()) {
            return Err(format!(
                "duplicate placement observation for role {}",
                observation.role
            ));
        }
        match observation.kind {
            PlacementKind::Local => {
                if observation.endpoint.is_some() {
                    return Err(format!(
                        "local role {} must not carry a remote endpoint",
                        observation.role
                    ));
                }
                if observation.colocated_with.is_some() {
                    return Err(format!(
                        "local role {} must not carry colocated_with metadata",
                        observation.role
                    ));
                }
            }
            PlacementKind::Remote => {
                if observation.endpoint.is_none() {
                    return Err(format!(
                        "remote role {} must carry an endpoint",
                        observation.role
                    ));
                }
                if observation.colocated_with.is_some() {
                    return Err(format!(
                        "remote role {} must not carry colocated_with metadata",
                        observation.role
                    ));
                }
            }
            PlacementKind::Colocated => {
                let Some(peer) = observation.colocated_with.as_ref() else {
                    return Err(format!(
                        "colocated role {} must name its colocated peer",
                        observation.role
                    ));
                };
                if peer == &observation.role {
                    return Err(format!(
                        "role {} may not be colocated with itself",
                        observation.role
                    ));
                }
                if observation.endpoint.is_some() {
                    return Err(format!(
                        "colocated role {} must not carry a direct endpoint",
                        observation.role
                    ));
                }
            }
        }
    }

    Ok(normalized)
}

fn resolve_placement(
    role: &str,
    placements: &BTreeMap<String, PlacementObservation>,
    visiting: &mut BTreeSet<String>,
) -> Result<ResolvedPlacement, String> {
    if !visiting.insert(role.to_string()) {
        return Err(format!("cyclic colocated placement involving role {role}"));
    }

    let resolved = match placements.get(role) {
        Some(PlacementObservation {
            kind: PlacementKind::Local,
            region,
            ..
        }) => Ok(ResolvedPlacement {
            node_key: "local".to_string(),
            region: region.clone(),
            uses_colocation: false,
            remote: false,
        }),
        Some(PlacementObservation {
            kind: PlacementKind::Remote,
            endpoint,
            region,
            ..
        }) => Ok(ResolvedPlacement {
            node_key: format!("remote:{}", endpoint.clone().unwrap_or_default()),
            region: region.clone(),
            uses_colocation: false,
            remote: true,
        }),
        Some(PlacementObservation {
            kind: PlacementKind::Colocated,
            role,
            colocated_with,
            region,
            ..
        }) => {
            let peer = colocated_with
                .as_ref()
                .expect("normalized colocated observation should name its peer");
            let inherited = resolve_placement(peer, placements, visiting)?;
            if let (Some(explicit), Some(inherited_region)) =
                (region.as_ref(), inherited.region.as_ref())
            {
                if explicit != inherited_region {
                    return Err(format!(
                        "role {role} declares region {explicit} but colocated peer resolves to {inherited_region}"
                    ));
                }
            }
            Ok(ResolvedPlacement {
                node_key: inherited.node_key,
                region: region.clone().or(inherited.region),
                uses_colocation: true,
                remote: inherited.remote,
            })
        }
        None => Err(format!("placement observation is missing role {role}")),
    };

    visiting.remove(role);
    resolved
}

/// Canonicalize and validate placement observations.
///
/// # Errors
///
/// Returns a descriptive error when the observation set is internally inconsistent.
pub fn canonicalize_placement_observations(
    observations: &[PlacementObservation],
) -> Result<Vec<PlacementObservation>, String> {
    let normalized = normalize_placement_observations(observations)?;
    let placements = normalized
        .iter()
        .cloned()
        .map(|observation| (observation.role.clone(), observation))
        .collect::<BTreeMap<_, _>>();
    for role in placements.keys() {
        resolve_placement(role, &placements, &mut BTreeSet::new())?;
    }
    Ok(normalized)
}

/// Derive canonical transport-observable boundaries for a placement set.
///
/// # Errors
///
/// Returns a descriptive error when the observation set is internally inconsistent.
pub fn canonical_transport_boundaries(
    observations: &[PlacementObservation],
) -> Result<Vec<TransportBoundaryObservation>, String> {
    let normalized = canonicalize_placement_observations(observations)?;
    let placements = normalized
        .iter()
        .cloned()
        .map(|observation| (observation.role.clone(), observation))
        .collect::<BTreeMap<_, _>>();
    let mut resolved = BTreeMap::new();
    for role in placements.keys() {
        resolved.insert(
            role.clone(),
            resolve_placement(role, &placements, &mut BTreeSet::new())?,
        );
    }

    let roles = normalized
        .iter()
        .map(|observation| observation.role.clone())
        .collect::<Vec<_>>();
    let mut boundaries = Vec::new();
    for (index, left_role) in roles.iter().enumerate() {
        for right_role in roles.iter().skip(index + 1) {
            let left_resolved = resolved
                .get(left_role)
                .expect("resolved placements should exist for every role");
            let right_resolved = resolved
                .get(right_role)
                .expect("resolved placements should exist for every role");
            let boundary = if left_resolved.remote || right_resolved.remote {
                TransportBoundaryKind::Network
            } else if left_resolved.uses_colocation || right_resolved.uses_colocation {
                TransportBoundaryKind::SharedMemory
            } else {
                TransportBoundaryKind::InProcess
            };
            let cross_region = match (&left_resolved.region, &right_resolved.region) {
                (Some(left), Some(right)) => left != right,
                _ => false,
            };
            boundaries.push(TransportBoundaryObservation {
                from_role: left_role.clone(),
                to_role: right_role.clone(),
                boundary,
                cross_region,
            });
        }
    }
    Ok(boundaries)
}

#[cfg(test)]
mod tests {
    use super::{canonical_transport_boundaries, PlacementObservation, TransportBoundaryKind};

    #[test]
    fn remote_and_colocated_boundaries_are_canonical() {
        let boundaries = canonical_transport_boundaries(&[
            PlacementObservation::local("Alice").with_region("eu_central_1"),
            PlacementObservation::remote("Bob", "127.0.0.1:19801").with_region("eu_west_1"),
            PlacementObservation::colocated("Carol", "Alice").with_region("eu_central_1"),
        ])
        .expect("valid placement observations");

        assert_eq!(
            boundaries,
            vec![
                super::TransportBoundaryObservation {
                    from_role: "Alice".to_string(),
                    to_role: "Bob".to_string(),
                    boundary: TransportBoundaryKind::Network,
                    cross_region: true,
                },
                super::TransportBoundaryObservation {
                    from_role: "Alice".to_string(),
                    to_role: "Carol".to_string(),
                    boundary: TransportBoundaryKind::SharedMemory,
                    cross_region: false,
                },
                super::TransportBoundaryObservation {
                    from_role: "Bob".to_string(),
                    to_role: "Carol".to_string(),
                    boundary: TransportBoundaryKind::Network,
                    cross_region: true,
                },
            ]
        );
    }

    #[test]
    fn conflicting_colocated_regions_reject() {
        let error = canonical_transport_boundaries(&[
            PlacementObservation::local("Alice").with_region("eu_central_1"),
            PlacementObservation::colocated("Bob", "Alice").with_region("us_east_1"),
        ])
        .expect_err("conflicting colocated regions must reject");

        assert!(
            error.contains("declares region"),
            "expected explicit colocated-region conflict, got {error}"
        );
    }
}