lion_core/step/
kernel_op.rs

1// Copyright (C) 2026 HaiyangLi
2// SPDX-License-Identifier: AGPL-3.0-or-later
3//! Lion Step Kernel Operations
4//!
5//! Corresponds to: Lion/Step/KernelOp.lean
6//!
7//! Kernel-internal operations (trusted TCB).
8
9use crate::state::State;
10use crate::types::{ActorId, ThreadId, WorkflowId};
11
12use super::{KernelOpError, StepError};
13
14/// Kernel-internal operations (no external trigger)
15///
16/// Corresponds to Lean: `inductive KernelOp`
17#[derive(Debug, Clone, PartialEq, Eq)]
18#[must_use = "kernel operations must be executed"]
19pub enum KernelOp {
20    /// Deliver one message to actor
21    ///
22    /// Corresponds to Lean: `| route_one (dst : ActorId)`
23    RouteOne {
24        /// Destination actor to receive the message
25        dst: ActorId,
26    },
27
28    /// Advance workflow
29    ///
30    /// Corresponds to Lean: `| workflow_tick (w : WorkflowId)`
31    WorkflowTick {
32        /// Workflow to advance
33        wid: WorkflowId,
34    },
35
36    /// Increment global time
37    ///
38    /// Corresponds to Lean: `| time_tick`
39    TimeTick,
40
41    /// Unblock actor waiting to send
42    ///
43    /// Corresponds to Lean: `| unblock_send (dst : ActorId)`
44    UnblockSend {
45        /// Destination actor to unblock
46        dst: ActorId,
47    },
48
49    /// Context switch between threads
50    ///
51    /// Corresponds to Lean: `| thread_switch (from_ to_ : ThreadId)`
52    ThreadSwitch {
53        /// Thread to switch from
54        from: ThreadId,
55        /// Thread to switch to
56        to: ThreadId,
57    },
58}
59
60impl KernelOp {
61    /// Execute the kernel operation
62    ///
63    /// Corresponds to Lean: `def KernelExecInternal`
64    ///
65    /// Each operation modifies only its designated state component:
66    /// - route_one: moves message from pending to mailbox
67    /// - time_tick: increments global time
68    /// - workflow_tick: advances workflow state
69    /// - unblock_send: clears blockedOn for actor
70    ///
71    /// # Errors
72    ///
73    /// Returns `StepError::ActorNotFound` if the destination actor does not exist (RouteOne, UnblockSend).
74    /// Returns `StepError::KernelOpFailed` if the actor has no pending messages or its mailbox is full (RouteOne).
75    /// Returns `StepError::KernelOpFailed` if the workflow is not found or is not running (WorkflowTick).
76    pub fn execute(&self, state: &State) -> Result<State, StepError> {
77        match self {
78            KernelOp::RouteOne { dst } => execute_route_one(state, *dst),
79            KernelOp::WorkflowTick { wid } => execute_workflow_tick(state, *wid),
80            KernelOp::TimeTick => execute_time_tick(state),
81            KernelOp::UnblockSend { dst } => execute_unblock_send(state, *dst),
82            KernelOp::ThreadSwitch { from, to } => execute_thread_switch(state, *from, *to),
83        }
84    }
85
86    /// Execute the kernel operation (mutating version).
87    ///
88    /// Same validation as `execute` but modifies `&mut State` in place.
89    pub fn execute_mut(&self, state: &mut State) -> Result<(), StepError> {
90        match self {
91            KernelOp::RouteOne { dst } => execute_route_one_mut(state, *dst),
92            KernelOp::WorkflowTick { wid } => execute_workflow_tick_mut(state, *wid),
93            KernelOp::TimeTick => execute_time_tick_mut(state),
94            KernelOp::UnblockSend { dst } => execute_unblock_send_mut(state, *dst),
95            KernelOp::ThreadSwitch { from, to } => execute_thread_switch_mut(state, *from, *to),
96        }
97    }
98}
99
100/// Execute route_one
101///
102/// Move first message from pending to mailbox (if pending non-empty).
103/// Scheduler ensures mailbox doesn't exceed capacity.
104///
105/// Corresponds to Lean: `KernelExecInternal .route_one`
106fn execute_route_one(state: &State, dst: ActorId) -> Result<State, StepError> {
107    let actor = state.get_actor(dst).ok_or(StepError::ActorNotFound(dst))?;
108
109    // Check pending queue has messages
110    if actor.pending_len() == 0 {
111        return Err(StepError::KernelOpFailed(
112            KernelOpError::NoPendingMessages { dst },
113        ));
114    }
115
116    // Check mailbox has space
117    if actor.mailbox_len() >= actor.capacity() {
118        return Err(StepError::KernelOpFailed(
119            KernelOpError::MailboxAtCapacity { dst },
120        ));
121    }
122
123    // Deliver message
124    let mut new_state = state.clone();
125    if let Some(actor) = new_state.get_actor_mut(dst) {
126        let _ = actor.deliver_mut();
127    }
128
129    Ok(new_state)
130}
131
132/// Execute workflow_tick
133///
134/// Advance workflow state (must preserve has-work invariant).
135///
136/// Corresponds to Lean: `KernelExecInternal .workflow_tick`
137///
138/// PERF NOTE: Currently a no-op that validates preconditions and clones state.
139/// The actual workflow advancement is abstracted in the formal model. A concrete
140/// implementation would advance node states based on dependencies and avoid the
141/// identity clone. The clone is retained for API uniformity with other kernel ops.
142fn execute_workflow_tick(state: &State, wid: WorkflowId) -> Result<State, StepError> {
143    let workflow = state.get_workflow(wid).ok_or(StepError::KernelOpFailed(
144        KernelOpError::WorkflowNotFound { wid },
145    ))?;
146
147    // Check workflow is running
148    if !workflow.is_running() {
149        return Err(StepError::KernelOpFailed(
150            KernelOpError::WorkflowNotRunning { wid },
151        ));
152    }
153
154    // Abstract tick: validates preconditions, returns state unchanged.
155    // A concrete implementation would advance node states based on dependencies.
156    Ok(state.clone())
157}
158
159/// Execute time_tick
160///
161/// Increment time and kernel time.
162///
163/// Corresponds to Lean: `KernelExecInternal .time_tick`
164fn execute_time_tick(state: &State) -> Result<State, StepError> {
165    let mut new_state = state.clone();
166    new_state
167        .tick()
168        .map_err(|e| StepError::KernelOpFailed(KernelOpError::CounterOverflow(e.to_string())))?;
169    Ok(new_state)
170}
171
172/// Execute unblock_send
173///
174/// Clear blockedOn for the destination actor.
175///
176/// Corresponds to Lean: `KernelExecInternal .unblock_send`
177fn execute_unblock_send(state: &State, dst: ActorId) -> Result<State, StepError> {
178    let _actor = state.get_actor(dst).ok_or(StepError::ActorNotFound(dst))?;
179
180    let mut new_state = state.clone();
181    if let Some(actor) = new_state.get_actor_mut(dst) {
182        actor.unblock_mut();
183    }
184
185    Ok(new_state)
186}
187
188/// Execute thread_switch
189///
190/// Context switch between threads: save `from` registers, restore `to` and
191/// make it running. Requires threads/scheduler in State (Phase 3).
192///
193/// Corresponds to Lean: `KernelExecInternal (.thread_switch from_ to_)`
194///
195/// NOTE: State does not yet include threads/scheduler fields (Phase 3 extension).
196/// This stub returns an error until the State type is extended.
197fn execute_thread_switch(
198    _state: &State,
199    _from: ThreadId,
200    _to: ThreadId,
201) -> Result<State, StepError> {
202    Err(StepError::KernelOpFailed(KernelOpError::NotImplemented {
203        operation: "thread_switch",
204    }))
205}
206
207// ============== MUTATING VARIANTS ==============
208
209fn execute_route_one_mut(state: &mut State, dst: ActorId) -> Result<(), StepError> {
210    let actor = state.get_actor(dst).ok_or(StepError::ActorNotFound(dst))?;
211
212    if actor.pending_len() == 0 {
213        return Err(StepError::KernelOpFailed(
214            KernelOpError::NoPendingMessages { dst },
215        ));
216    }
217
218    if actor.mailbox_len() >= actor.capacity() {
219        return Err(StepError::KernelOpFailed(
220            KernelOpError::MailboxAtCapacity { dst },
221        ));
222    }
223
224    if let Some(actor) = state.get_actor_mut(dst) {
225        let _ = actor.deliver_mut();
226    }
227
228    Ok(())
229}
230
231fn execute_workflow_tick_mut(state: &mut State, wid: WorkflowId) -> Result<(), StepError> {
232    let workflow = state.get_workflow(wid).ok_or(StepError::KernelOpFailed(
233        KernelOpError::WorkflowNotFound { wid },
234    ))?;
235
236    if !workflow.is_running() {
237        return Err(StepError::KernelOpFailed(
238            KernelOpError::WorkflowNotRunning { wid },
239        ));
240    }
241
242    // Abstract tick: validates preconditions, state unchanged.
243    Ok(())
244}
245
246fn execute_time_tick_mut(state: &mut State) -> Result<(), StepError> {
247    state
248        .tick()
249        .map_err(|e| StepError::KernelOpFailed(KernelOpError::CounterOverflow(e.to_string())))?;
250    Ok(())
251}
252
253fn execute_unblock_send_mut(state: &mut State, dst: ActorId) -> Result<(), StepError> {
254    let _actor = state.get_actor(dst).ok_or(StepError::ActorNotFound(dst))?;
255
256    if let Some(actor) = state.get_actor_mut(dst) {
257        actor.unblock_mut();
258    }
259
260    Ok(())
261}
262
263fn execute_thread_switch_mut(
264    _state: &mut State,
265    _from: ThreadId,
266    _to: ThreadId,
267) -> Result<(), StepError> {
268    Err(StepError::KernelOpFailed(KernelOpError::NotImplemented {
269        operation: "thread_switch",
270    }))
271}
272
273// ============== FRAME THEOREMS ==============
274//
275// These correspond to Lean's comprehensive frame theorems.
276// In Rust, we verify these properties through tests.
277
278#[cfg(test)]
279mod tests {
280    use super::*;
281    use crate::state::{ActorRuntime, Message, PluginState, WorkflowInstance};
282    use crate::types::SecurityLevel;
283
284    fn make_test_message(id: u128) -> Message {
285        Message::new(id, 1, 2, SecurityLevel::Public, vec![1, 2, 3])
286    }
287
288    #[test]
289    fn test_time_tick_increments_time() {
290        let state = State::empty();
291        assert_eq!(state.time(), 0);
292
293        let op = KernelOp::TimeTick;
294        let new_state = op.execute(&state).expect("time_tick should succeed");
295
296        assert_eq!(new_state.time(), 1);
297    }
298
299    #[test]
300    fn test_time_tick_preserves_plugins() {
301        // Corresponds to Lean: time_tick_comprehensive_frame (plugins unchanged)
302        let mut state = State::empty();
303        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Public, 100));
304
305        let op = KernelOp::TimeTick;
306        let new_state = op.execute(&state).expect("time_tick should succeed");
307
308        // Plugins should be unchanged
309        assert!(new_state.get_plugin(1).is_some());
310        assert_eq!(
311            new_state.get_plugin(1).map(|p| p.memory_bounds()),
312            Some(100)
313        );
314    }
315
316    #[test]
317    fn test_time_tick_preserves_actors() {
318        // Corresponds to Lean: time_tick_comprehensive_frame (actors unchanged)
319        let mut state = State::empty();
320        let _ = state.insert_actor(1, ActorRuntime::empty(10));
321
322        let op = KernelOp::TimeTick;
323        let new_state = op.execute(&state).expect("time_tick should succeed");
324
325        // Actors should be unchanged
326        assert!(new_state.get_actor(1).is_some());
327        assert_eq!(new_state.get_actor(1).map(|a| a.capacity()), Some(10));
328    }
329
330    #[test]
331    fn test_route_one_moves_message() {
332        let mut state = State::empty();
333        let mut actor = ActorRuntime::empty(10);
334        actor.enqueue_pending_mut(make_test_message(42));
335        state.insert_actor(1, actor).unwrap();
336
337        assert_eq!(state.get_actor(1).map(|a| a.pending_len()), Some(1));
338        assert_eq!(state.get_actor(1).map(|a| a.mailbox_len()), Some(0));
339
340        let op = KernelOp::RouteOne { dst: 1 };
341        let new_state = op.execute(&state).expect("route_one should succeed");
342
343        assert_eq!(new_state.get_actor(1).map(|a| a.pending_len()), Some(0));
344        assert_eq!(new_state.get_actor(1).map(|a| a.mailbox_len()), Some(1));
345    }
346
347    #[test]
348    fn test_route_one_preserves_other_actors() {
349        // Corresponds to Lean: route_one_comprehensive_frame (other actors unchanged)
350        let mut state = State::empty();
351
352        let mut actor1 = ActorRuntime::empty(10);
353        actor1.enqueue_pending_mut(make_test_message(1));
354        state.insert_actor(1, actor1).unwrap();
355
356        let actor2 = ActorRuntime::empty(5);
357        state.insert_actor(2, actor2).unwrap();
358
359        let op = KernelOp::RouteOne { dst: 1 };
360        let new_state = op.execute(&state).expect("route_one should succeed");
361
362        // Actor 2 should be unchanged
363        assert_eq!(new_state.get_actor(2).map(|a| a.capacity()), Some(5));
364        assert_eq!(new_state.get_actor(2).map(|a| a.pending_len()), Some(0));
365    }
366
367    #[test]
368    fn test_route_one_preserves_plugins() {
369        // Corresponds to Lean: route_one_memory_unchanged
370        let mut state = State::empty();
371
372        let mut actor = ActorRuntime::empty(10);
373        actor.enqueue_pending_mut(make_test_message(1));
374        state.insert_actor(1, actor).unwrap();
375
376        let _ = state.insert_plugin(1, PluginState::empty(SecurityLevel::Secret, 1024));
377
378        let op = KernelOp::RouteOne { dst: 1 };
379        let new_state = op.execute(&state).expect("route_one should succeed");
380
381        // Plugin should be unchanged
382        assert_eq!(new_state.plugin_level(1), Some(SecurityLevel::Secret));
383    }
384
385    #[test]
386    fn test_route_one_no_pending_fails() {
387        let mut state = State::empty();
388        let _ = state.insert_actor(1, ActorRuntime::empty(10));
389
390        let op = KernelOp::RouteOne { dst: 1 };
391        let result = op.execute(&state);
392
393        assert!(matches!(result, Err(StepError::KernelOpFailed(_))));
394    }
395
396    #[test]
397    fn test_route_one_mailbox_full_fails() {
398        let mut state = State::empty();
399
400        // Create actor with capacity 1, full mailbox
401        let mut actor = ActorRuntime::empty(1);
402        actor.enqueue_pending_mut(make_test_message(1));
403        let _ = actor.deliver_mut(); // Fill mailbox
404        actor.enqueue_pending_mut(make_test_message(2)); // Add another pending
405        state.insert_actor(1, actor).unwrap();
406
407        let op = KernelOp::RouteOne { dst: 1 };
408        let result = op.execute(&state);
409
410        assert!(matches!(result, Err(StepError::KernelOpFailed(_))));
411    }
412
413    #[test]
414    fn test_unblock_send_clears_blocked() {
415        let mut state = State::empty();
416        let mut actor = ActorRuntime::empty(10);
417        actor.set_blocked_mut(42);
418        state.insert_actor(1, actor).unwrap();
419
420        assert!(state.get_actor(1).map(|a| a.is_blocked()).unwrap_or(false));
421
422        let op = KernelOp::UnblockSend { dst: 1 };
423        let new_state = op.execute(&state).expect("unblock_send should succeed");
424
425        assert!(!new_state
426            .get_actor(1)
427            .map(|a| a.is_blocked())
428            .unwrap_or(true));
429    }
430
431    #[test]
432    fn test_unblock_send_preserves_mailbox() {
433        // Corresponds to Lean: unblock_send_comprehensive_frame
434        let mut state = State::empty();
435        let mut actor = ActorRuntime::empty(10);
436        actor.enqueue_pending_mut(make_test_message(1));
437        let _ = actor.deliver_mut();
438        actor.set_blocked_mut(42);
439        state.insert_actor(1, actor).unwrap();
440
441        let initial_mailbox_len = state.get_actor(1).map(|a| a.mailbox_len()).unwrap_or(0);
442
443        let op = KernelOp::UnblockSend { dst: 1 };
444        let new_state = op.execute(&state).expect("unblock_send should succeed");
445
446        let final_mailbox_len = new_state.get_actor(1).map(|a| a.mailbox_len()).unwrap_or(0);
447        assert_eq!(initial_mailbox_len, final_mailbox_len);
448    }
449
450    #[test]
451    fn test_workflow_tick_not_found() {
452        let state = State::empty();
453
454        let op = KernelOp::WorkflowTick { wid: 999 };
455        let result = op.execute(&state);
456
457        assert!(matches!(result, Err(StepError::KernelOpFailed(_))));
458    }
459
460    #[test]
461    fn test_workflow_tick_preserves_other_workflows() {
462        // Corresponds to Lean: workflow_tick_comprehensive_frame
463        let mut state = State::empty();
464
465        let _ = state.insert_workflow(1, WorkflowInstance::running(100));
466        let _ = state.insert_workflow(2, WorkflowInstance::running(200));
467
468        let op = KernelOp::WorkflowTick { wid: 1 };
469        let new_state = op.execute(&state).expect("workflow_tick should succeed");
470
471        // Workflow 2 should be unchanged
472        assert!(new_state
473            .get_workflow(2)
474            .map(|w| w.is_running())
475            .unwrap_or(false));
476    }
477}
lion_core/step/kernel_op.rs

lion_core/step/
kernel_op.rs
