telltale_vm/
loader.rs

1//! Dynamic choreography loading.
2//!
3//! Matches `CodeImage`, `UntrustedImage`, `loadTrusted`, `loadUntrusted`
4//! from `runtime.md §10`.
5
6use std::collections::BTreeMap;
7
8use telltale_types::{GlobalType, LocalTypeR};
9
10use crate::instr::Instr;
11
12/// A verified code image: program + global type + local types.
13///
14/// In the Lean spec, this carries well-formedness and projection correctness
15/// proofs. In Rust, the proofs are replaced by runtime validation that was
16/// performed before constructing the image.
17#[derive(Debug, Clone)]
18pub struct CodeImage {
19    /// Bytecode programs per role.
20    pub programs: BTreeMap<String, Vec<Instr>>,
21    /// The global type this image was derived from.
22    pub global_type: GlobalType,
23    /// Projected local types per role.
24    pub local_types: BTreeMap<String, LocalTypeR>,
25}
26
27/// An unverified code image: program + global type, no validation proof.
28///
29/// Must be validated before execution via `validate`.
30#[derive(Debug, Clone)]
31pub struct UntrustedImage {
32    /// Bytecode programs per role.
33    pub programs: BTreeMap<String, Vec<Instr>>,
34    /// The global type this image was derived from.
35    pub global_type: GlobalType,
36    /// Projected local types per role (claimed, not yet verified).
37    pub local_types: BTreeMap<String, LocalTypeR>,
38}
39
40/// Result of loading a code image.
41#[derive(Debug)]
42pub enum LoadResult {
43    /// Image loaded successfully.
44    Ok,
45    /// Validation failed.
46    ValidationFailed {
47        /// Description of the validation failure.
48        reason: String,
49    },
50}
51
52impl CodeImage {
53    /// Create a code image from projected local types by compiling each to bytecode.
54    #[must_use]
55    pub fn from_local_types(
56        local_types: &BTreeMap<String, LocalTypeR>,
57        global_type: &GlobalType,
58    ) -> Self {
59        let programs = local_types
60            .iter()
61            .map(|(role, lt)| (role.clone(), crate::compiler::compile(lt)))
62            .collect();
63
64        Self {
65            programs,
66            global_type: global_type.clone(),
67            local_types: local_types.clone(),
68        }
69    }
70
71    /// Role names in this image.
72    #[must_use]
73    pub fn roles(&self) -> Vec<String> {
74        self.programs.keys().cloned().collect()
75    }
76}
77
78impl UntrustedImage {
79    /// Create an untrusted image from projected local types.
80    #[must_use]
81    pub fn from_local_types(
82        local_types: &BTreeMap<String, LocalTypeR>,
83        global_type: &GlobalType,
84    ) -> Self {
85        let programs = local_types
86            .iter()
87            .map(|(role, lt)| (role.clone(), crate::compiler::compile(lt)))
88            .collect();
89
90        Self {
91            programs,
92            global_type: global_type.clone(),
93            local_types: local_types.clone(),
94        }
95    }
96
97    /// Validate the image: check well-formedness and projection correctness.
98    ///
99    /// 1. Checks that the global type is well-formed.
100    /// 2. Re-projects the global type onto each role.
101    /// 3. Verifies that the claimed local types match the re-projected types.
102    /// 4. Recompiles from the verified local types (ignoring claimed bytecode).
103    ///
104    /// # Errors
105    ///
106    /// Returns `LoadResult::ValidationFailed` if any check fails.
107    pub fn validate(self) -> Result<CodeImage, LoadResult> {
108        if !self.global_type.well_formed() {
109            return Err(LoadResult::ValidationFailed {
110                reason: "global type is not well-formed".into(),
111            });
112        }
113
114        // Re-project global type onto all roles.
115        let projected =
116            telltale_theory::projection::project_all(&self.global_type).map_err(|e| {
117                LoadResult::ValidationFailed {
118                    reason: format!("projection failed: {e}"),
119                }
120            })?;
121
122        let projected_map: BTreeMap<String, LocalTypeR> = projected.into_iter().collect();
123
124        // Verify claimed roles match projected roles.
125        if self.local_types.keys().collect::<Vec<_>>() != projected_map.keys().collect::<Vec<_>>() {
126            return Err(LoadResult::ValidationFailed {
127                reason: format!(
128                    "role mismatch: claimed {:?}, projected {:?}",
129                    self.local_types.keys().collect::<Vec<_>>(),
130                    projected_map.keys().collect::<Vec<_>>(),
131                ),
132            });
133        }
134
135        // Verify each claimed local type matches the re-projected type.
136        for (role, claimed) in &self.local_types {
137            let expected = &projected_map[role];
138            if claimed != expected {
139                return Err(LoadResult::ValidationFailed {
140                    reason: format!(
141                        "local type mismatch for role {role}: claimed {claimed:?}, expected {expected:?}"
142                    ),
143                });
144            }
145        }
146
147        // Recompile from verified local types (ignore claimed bytecode).
148        Ok(CodeImage::from_local_types(
149            &projected_map,
150            &self.global_type,
151        ))
152    }
153}
154
155#[cfg(test)]
156mod tests {
157    use super::*;
158    use telltale_types::Label;
159
160    fn simple_global() -> GlobalType {
161        GlobalType::mu(
162            "step",
163            GlobalType::send(
164                "A",
165                "B",
166                Label::new("msg"),
167                GlobalType::send("B", "A", Label::new("msg"), GlobalType::var("step")),
168            ),
169        )
170    }
171
172    #[test]
173    fn test_untrusted_validate_correct() {
174        let global = simple_global();
175        let projected: BTreeMap<_, _> = telltale_theory::projection::project_all(&global)
176            .unwrap()
177            .into_iter()
178            .collect();
179        let image = UntrustedImage::from_local_types(&projected, &global);
180        let verified = image.validate();
181        assert!(verified.is_ok());
182    }
183
184    #[test]
185    fn test_untrusted_validate_bad_local_type() {
186        let global = simple_global();
187        let mut locals = BTreeMap::new();
188        // Claim A has End instead of correct projection.
189        locals.insert("A".to_string(), LocalTypeR::End);
190        locals.insert(
191            "B".to_string(),
192            LocalTypeR::mu(
193                "step",
194                LocalTypeR::Recv {
195                    partner: "A".into(),
196                    branches: vec![(
197                        Label::new("msg"),
198                        None,
199                        LocalTypeR::Send {
200                            partner: "A".into(),
201                            branches: vec![(Label::new("msg"), None, LocalTypeR::var("step"))],
202                        },
203                    )],
204                },
205            ),
206        );
207        let image = UntrustedImage::from_local_types(&locals, &global);
208        let result = image.validate();
209        assert!(result.is_err());
210    }
211
212    #[test]
213    fn test_untrusted_validate_bad_global_type() {
214        // Self-communication is not well-formed.
215        let global = GlobalType::send("A", "A", Label::new("msg"), GlobalType::End);
216        let mut locals = BTreeMap::new();
217        locals.insert("A".to_string(), LocalTypeR::End);
218        let image = UntrustedImage::from_local_types(&locals, &global);
219        let result = image.validate();
220        assert!(result.is_err());
221    }
222
223    #[test]
224    fn test_trusted_and_untrusted_validated_images_match() {
225        let global = simple_global();
226        let projected: BTreeMap<_, _> = telltale_theory::projection::project_all(&global)
227            .unwrap()
228            .into_iter()
229            .collect();
230
231        let trusted = CodeImage::from_local_types(&projected, &global);
232        let validated = UntrustedImage::from_local_types(&projected, &global)
233            .validate()
234            .expect("untrusted image should validate");
235
236        assert_eq!(trusted.global_type, validated.global_type);
237        assert_eq!(trusted.local_types, validated.local_types);
238        assert_eq!(trusted.programs, validated.programs);
239    }
240
241    #[test]
242    fn test_validate_ignores_untrusted_program_payload_and_recompiles() {
243        let global = simple_global();
244        let projected: BTreeMap<_, _> = telltale_theory::projection::project_all(&global)
245            .unwrap()
246            .into_iter()
247            .collect();
248
249        let mut untrusted = UntrustedImage::from_local_types(&projected, &global);
250        untrusted
251            .programs
252            .insert("A".to_string(), vec![Instr::Halt, Instr::Halt]);
253        untrusted
254            .programs
255            .insert("B".to_string(), vec![Instr::Yield]);
256
257        let validated = untrusted
258            .validate()
259            .expect("validation should reproject and recompile");
260        let trusted = CodeImage::from_local_types(&projected, &global);
261
262        assert_eq!(validated.local_types, trusted.local_types);
263        assert_eq!(validated.programs, trusted.programs);
264    }
265}
telltale_vm/loader.rs

telltale_vm/
loader.rs
