lion_core/step/
plugin_internal.rs

1// Copyright (C) 2026 HaiyangLi
2// SPDX-License-Identifier: AGPL-3.0-or-later
3//! Lion Step Plugin Internal
4//!
5//! Corresponds to: Lion/Step/PluginInternal.lean
6//!
7//! Plugin-internal computation (sandboxed, untrusted).
8
9use crate::state::State;
10use crate::types::{MemAddr, PluginId, Size};
11
12use super::{PluginPrecondition, StepError};
13
14/// Plugin internal computation descriptor
15///
16/// Corresponds to Lean: `structure PluginInternal`
17///
18/// Describes what a plugin's internal WASM computation does:
19/// - Memory regions read
20/// - Memory regions written
21/// - Whether to consume from mailbox
22#[derive(Debug, Clone, Default)]
23pub struct PluginInternal {
24    /// Memory regions read
25    ///
26    /// Corresponds to Lean: `reads : List (MemAddr x Size)`
27    pub reads: Vec<(MemAddr, Size)>,
28
29    /// Memory regions written
30    ///
31    /// Corresponds to Lean: `writes : List (MemAddr x Size)`
32    pub writes: Vec<(MemAddr, Size)>,
33
34    /// Whether to consume from mailbox
35    ///
36    /// Corresponds to Lean: `consume_mailbox : Bool`
37    pub consume_mailbox: bool,
38}
39
40impl PluginInternal {
41    /// Create a new plugin internal computation descriptor
42    pub fn new(
43        reads: Vec<(MemAddr, Size)>,
44        writes: Vec<(MemAddr, Size)>,
45        consume_mailbox: bool,
46    ) -> Self {
47        PluginInternal {
48            reads,
49            writes,
50            consume_mailbox,
51        }
52    }
53
54    /// Create a computation that just computes (no I/O)
55    pub fn compute() -> Self {
56        PluginInternal {
57            reads: Vec::new(),
58            writes: Vec::new(),
59            consume_mailbox: false,
60        }
61    }
62
63    /// Create a computation that reads memory
64    pub fn with_reads(reads: Vec<(MemAddr, Size)>) -> Self {
65        PluginInternal {
66            reads,
67            writes: Vec::new(),
68            consume_mailbox: false,
69        }
70    }
71
72    /// Create a computation that writes memory
73    pub fn with_writes(writes: Vec<(MemAddr, Size)>) -> Self {
74        PluginInternal {
75            reads: Vec::new(),
76            writes,
77            consume_mailbox: false,
78        }
79    }
80
81    /// Check preconditions for plugin internal execution
82    ///
83    /// Corresponds to Lean: `def plugin_internal_pre`
84    ///
85    /// Preconditions:
86    /// 1. Plugin is not blocked on another actor
87    /// 2. Read regions are in bounds
88    /// 3. Write regions are in bounds
89    /// 4. If consuming mailbox, mailbox must not be empty
90    ///
91    /// # Errors
92    ///
93    /// Returns `StepError::PluginNotFound` if the plugin does not exist.
94    /// Returns `StepError::PluginPreconditionFailed` if the plugin's actor is blocked.
95    /// Returns `StepError::PluginPreconditionFailed` if a read region is out of bounds.
96    /// Returns `StepError::PluginPreconditionFailed` if a write region is out of bounds.
97    /// Returns `StepError::PluginPreconditionFailed` if consuming mailbox but the mailbox is empty.
98    pub fn check_preconditions(&self, state: &State, pid: PluginId) -> Result<(), StepError> {
99        // Check plugin exists
100        let plugin = state
101            .get_plugin(pid)
102            .ok_or(StepError::PluginNotFound(pid))?;
103
104        // Check not blocked
105        if let Some(actor) = state.get_actor(pid) {
106            if actor.is_blocked() {
107                return Err(StepError::PluginPreconditionFailed(
108                    PluginPrecondition::Blocked {
109                        pid,
110                        blocked_on: actor.blocked_on(),
111                    },
112                ));
113            }
114        }
115
116        // Check read regions in bounds
117        if let Some(err) = self.find_oob_read(plugin) {
118            return Err(err);
119        }
120
121        // Check write regions in bounds
122        if let Some(err) = self.find_oob_write(plugin) {
123            return Err(err);
124        }
125
126        // Check mailbox if consuming
127        if self.consume_mailbox {
128            if let Some(actor) = state.get_actor(pid) {
129                if !actor.can_receive() {
130                    return Err(StepError::PluginPreconditionFailed(
131                        PluginPrecondition::MailboxEmpty,
132                    ));
133                }
134            }
135        }
136
137        Ok(())
138    }
139
140    /// Helper: find first out-of-bounds read region
141    fn find_oob_read(&self, plugin: &crate::state::PluginState) -> Option<StepError> {
142        self.reads.iter().find_map(|&(addr, size)| {
143            if plugin.memory().addr_in_bounds(addr, size) {
144                None
145            } else {
146                Some(StepError::PluginPreconditionFailed(
147                    PluginPrecondition::ReadOutOfBounds {
148                        addr,
149                        size,
150                        bounds: plugin.memory_bounds(),
151                    },
152                ))
153            }
154        })
155    }
156
157    /// Helper: find first out-of-bounds write region
158    fn find_oob_write(&self, plugin: &crate::state::PluginState) -> Option<StepError> {
159        self.writes.iter().find_map(|&(addr, size)| {
160            if plugin.memory().addr_in_bounds(addr, size) {
161                None
162            } else {
163                Some(StepError::PluginPreconditionFailed(
164                    PluginPrecondition::WriteOutOfBounds {
165                        addr,
166                        size,
167                        bounds: plugin.memory_bounds(),
168                    },
169                ))
170            }
171        })
172    }
173}
174
175// ============== FRAME THEOREMS ==============
176//
177// These correspond to Lean's comprehensive frame theorem:
178// plugin_internal_comprehensive_frame
179//
180// Plugin internal execution (WASM sandbox) only affects:
181// - The executing plugin's memory contents
182// - The executing plugin's local state
183//
184// It CANNOT modify:
185// - Other plugins' state
186// - Kernel state
187// - Actor state (except mailbox consumption)
188// - Resources
189// - Workflows
190// - Ghost state
191// - Time
192// - Security-critical fields (level, heldCaps, memory.bounds)
193
194#[cfg(test)]
195mod tests {
196    use super::*;
197    use crate::state::{ActorRuntime, Message, PluginState};
198    use crate::types::SecurityLevel;
199
200    #[test]
201    fn test_plugin_internal_default() {
202        let pi = PluginInternal::default();
203        assert!(pi.reads.is_empty());
204        assert!(pi.writes.is_empty());
205        assert!(!pi.consume_mailbox);
206    }
207
208    #[test]
209    fn test_plugin_internal_compute() {
210        let pi = PluginInternal::compute();
211        assert!(pi.reads.is_empty());
212        assert!(pi.writes.is_empty());
213        assert!(!pi.consume_mailbox);
214    }
215
216    #[test]
217    fn test_plugin_internal_with_reads() {
218        let pi = PluginInternal::with_reads(vec![(0, 100), (200, 50)]);
219        assert_eq!(pi.reads.len(), 2);
220        assert!(pi.writes.is_empty());
221    }
222
223    #[test]
224    fn test_plugin_internal_with_writes() {
225        let pi = PluginInternal::with_writes(vec![(0, 100)]);
226        assert!(pi.reads.is_empty());
227        assert_eq!(pi.writes.len(), 1);
228    }
229
230    #[test]
231    fn test_check_preconditions_plugin_not_found() {
232        let state = State::empty();
233        let pi = PluginInternal::compute();
234
235        let result = pi.check_preconditions(&state, 1);
236        assert!(matches!(result, Err(StepError::PluginNotFound(1))));
237    }
238
239    #[test]
240    fn test_check_preconditions_blocked() {
241        let mut state = State::empty();
242        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Public, 1024));
243
244        let mut actor = ActorRuntime::empty(10);
245        actor.set_blocked_mut(42);
246        state.insert_actor(1, actor).unwrap();
247
248        let pi = PluginInternal::compute();
249        let result = pi.check_preconditions(&state, 1);
250
251        assert!(matches!(
252            result,
253            Err(StepError::PluginPreconditionFailed(_))
254        ));
255    }
256
257    #[test]
258    fn test_check_preconditions_read_out_of_bounds() {
259        let mut state = State::empty();
260        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Public, 100));
261
262        // Read region beyond memory bounds
263        let pi = PluginInternal::with_reads(vec![(0, 200)]);
264        let result = pi.check_preconditions(&state, 1);
265
266        assert!(matches!(
267            result,
268            Err(StepError::PluginPreconditionFailed(_))
269        ));
270    }
271
272    #[test]
273    fn test_check_preconditions_write_out_of_bounds() {
274        let mut state = State::empty();
275        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Public, 100));
276
277        // Write region beyond memory bounds
278        let pi = PluginInternal::with_writes(vec![(50, 100)]);
279        let result = pi.check_preconditions(&state, 1);
280
281        assert!(matches!(
282            result,
283            Err(StepError::PluginPreconditionFailed(_))
284        ));
285    }
286
287    #[test]
288    fn test_check_preconditions_consume_empty_mailbox() {
289        let mut state = State::empty();
290        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Public, 1024));
291        let _ = state.insert_actor(1, ActorRuntime::empty(10));
292
293        let pi = PluginInternal {
294            reads: Vec::new(),
295            writes: Vec::new(),
296            consume_mailbox: true,
297        };
298        let result = pi.check_preconditions(&state, 1);
299
300        assert!(matches!(
301            result,
302            Err(StepError::PluginPreconditionFailed(_))
303        ));
304    }
305
306    #[test]
307    fn test_check_preconditions_success() {
308        let mut state = State::empty();
309        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Public, 1024));
310        let _ = state.insert_actor(1, ActorRuntime::empty(10));
311
312        let pi = PluginInternal::with_reads(vec![(0, 100), (500, 200)]);
313        let result = pi.check_preconditions(&state, 1);
314
315        assert!(result.is_ok());
316    }
317
318    #[test]
319    fn test_check_preconditions_consume_non_empty_mailbox() {
320        let mut state = State::empty();
321        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Public, 1024));
322
323        let mut actor = ActorRuntime::empty(10);
324        let msg = Message::new(1, 2, 1, SecurityLevel::Public, vec![]);
325        actor.enqueue_pending_mut(msg);
326        let _ = actor.deliver_mut();
327        state.insert_actor(1, actor).unwrap();
328
329        let pi = PluginInternal {
330            reads: Vec::new(),
331            writes: Vec::new(),
332            consume_mailbox: true,
333        };
334        let result = pi.check_preconditions(&state, 1);
335
336        assert!(result.is_ok());
337    }
338
339    // ============== FRAME PROPERTY TESTS ==============
340
341    #[test]
342    fn test_frame_other_plugins_unchanged() {
343        // Corresponds to Lean: plugin_internal_frame
344        // Other plugins should be unchanged after plugin internal execution
345        let mut state = State::empty();
346        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Public, 1024));
347        let _ = state.insert_plugin(2, PluginState::empty(SecurityLevel::Secret, 2048));
348        let _ = state.insert_actor(1, ActorRuntime::empty(10));
349
350        let initial_plugin2 = state.get_plugin(2).cloned();
351
352        // Execute plugin 1 internal
353        let step = super::super::Step::PluginInternal {
354            pid: 1,
355            pi: PluginInternal::compute(),
356        };
357        let new_state = step.execute(&state).expect("should succeed");
358
359        // Plugin 2 should be unchanged
360        assert_eq!(new_state.get_plugin(2), initial_plugin2.as_ref());
361    }
362
363    #[test]
364    fn test_frame_kernel_unchanged() {
365        // Corresponds to Lean: plugin_internal_kernel_unchanged
366        let mut state = State::empty();
367        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Public, 1024));
368        let _ = state.insert_actor(1, ActorRuntime::empty(10));
369
370        let initial_kernel_now = state.kernel().now();
371
372        let step = super::super::Step::PluginInternal {
373            pid: 1,
374            pi: PluginInternal::compute(),
375        };
376        let new_state = step.execute(&state).expect("should succeed");
377
378        // Kernel time should be unchanged
379        assert_eq!(new_state.kernel().now(), initial_kernel_now);
380    }
381
382    #[test]
383    fn test_frame_time_unchanged() {
384        // Corresponds to Lean: plugin_internal_time_unchanged
385        let mut state = State::empty();
386        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Public, 1024));
387        let _ = state.insert_actor(1, ActorRuntime::empty(10));
388
389        let initial_time = state.time();
390
391        let step = super::super::Step::PluginInternal {
392            pid: 1,
393            pi: PluginInternal::compute(),
394        };
395        let new_state = step.execute(&state).expect("should succeed");
396
397        // Time should be unchanged
398        assert_eq!(new_state.time(), initial_time);
399    }
400
401    #[test]
402    fn test_security_invariant_level_preserved() {
403        // Corresponds to Lean: plugin_internal_level_preserved
404        let mut state = State::empty();
405        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Confidential, 1024));
406        let _ = state.insert_actor(1, ActorRuntime::empty(10));
407
408        let step = super::super::Step::PluginInternal {
409            pid: 1,
410            pi: PluginInternal::with_writes(vec![(0, 100)]),
411        };
412        let new_state = step.execute(&state).expect("should succeed");
413
414        // Security level should be preserved
415        assert_eq!(new_state.plugin_level(1), Some(SecurityLevel::Confidential));
416    }
417
418    #[test]
419    fn test_security_invariant_caps_preserved() {
420        // Corresponds to Lean: plugin_internal_caps_preserved
421        let mut state = State::empty();
422        let mut ps = PluginState::empty(SecurityLevel::Public, 1024);
423        ps.grant_cap_mut(42);
424        ps.grant_cap_mut(43);
425        state.insert_plugin(1, ps).unwrap();
426        let _ = state.insert_actor(1, ActorRuntime::empty(10));
427
428        let step = super::super::Step::PluginInternal {
429            pid: 1,
430            pi: PluginInternal::compute(),
431        };
432        let new_state = step.execute(&state).expect("should succeed");
433
434        // Held caps should be preserved
435        assert!(new_state.plugin_holds(1, 42));
436        assert!(new_state.plugin_holds(1, 43));
437    }
438
439    #[test]
440    fn test_security_invariant_bounds_preserved() {
441        // Corresponds to Lean: plugin_internal_bounds_preserved
442        let mut state = State::empty();
443        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Public, 1024));
444        let _ = state.insert_actor(1, ActorRuntime::empty(10));
445
446        let step = super::super::Step::PluginInternal {
447            pid: 1,
448            pi: PluginInternal::with_writes(vec![(0, 100)]),
449        };
450        let new_state = step.execute(&state).expect("should succeed");
451
452        // Memory bounds should be preserved
453        assert_eq!(
454            new_state.get_plugin(1).map(|p| p.memory_bounds()),
455            Some(1024)
456        );
457    }
458}
lion_core/step/plugin_internal.rs

lion_core/step/
plugin_internal.rs
