lean_rs_host/host/
progress.rs

1//! Structured progress reporting for host-session operations.
2//!
3//! Progress is host policy layered over the L1 `lean-rs` callback
4//! registry. Public callers provide a borrowed [`LeanProgressSink`];
5//! this module hides the temporary callback handle, ABI status byte,
6//! and panic/stale-handle mapping needed by Lean progress shims.
7
8// SAFETY DOC: this module has two narrow unsafe operations: turning a
9// synchronous callback handle back into its stack-owned context pointer,
10// and reading the scalar-tail `UInt8` from an `Except UInt8 _` error
11// constructor after validating the constructor tag. Each block carries
12// the local invariant.
13#![allow(unsafe_code)]
14
15use std::panic::{AssertUnwindSafe, catch_unwind};
16use std::time::{Duration, Instant};
17
18use lean_rs::abi::structure::{ctor_tag, take_ctor_objects};
19use lean_rs::abi::traits::{TryFromLean, conversion_error};
20use lean_rs::{LeanCallbackFlow, LeanCallbackHandle, LeanCallbackStatus, LeanProgressTick, LeanResult, Obj};
21
22/// One structured progress observation from a `LeanSession` operation.
23///
24/// Events are delivered synchronously on the Lean-bound worker thread.
25/// `current` is phase-local and monotonically non-decreasing within one
26/// `phase`. `total = None` means the operation can report a phase-local
27/// counter but does not know the final bound cheaply.
28#[derive(Clone, Copy, Debug, Eq, PartialEq)]
29pub struct LeanProgressEvent {
30    /// Stable phase label for the current operation.
31    pub phase: &'static str,
32    /// Phase-local progress counter.
33    pub current: u64,
34    /// Optional phase-local total.
35    pub total: Option<u64>,
36    /// Time elapsed since this phase started.
37    pub elapsed: Duration,
38}
39
40/// Sink for structured host progress events.
41///
42/// A sink is a one-way callback. It runs synchronously on the thread
43/// currently executing the `LeanSession` method and must not call back
44/// into the same session or re-enter the same Lean call stack. Expensive
45/// work should be queued elsewhere by the sink because progress may be
46/// reported many times for bulk operations.
47///
48/// Rust panics from sinks invoked through Lean progress shims are
49/// contained by the L1 callback trampoline and returned as a host
50/// internal error. Panics from host-side progress checkpoints are caught
51/// before they escape the session method.
52pub trait LeanProgressSink: Send + Sync {
53    /// Receive one progress event.
54    fn report(&self, event: LeanProgressEvent);
55}
56
57pub(crate) struct ProgressBridge<'a> {
58    handle: LeanCallbackHandle<LeanProgressTick>,
59    #[allow(dead_code, reason = "keeps the callback context alive until after handle drop")]
60    context: Box<ProgressContext<'a>>,
61}
62
63struct ProgressContext<'a> {
64    sink: &'a dyn LeanProgressSink,
65    phase: &'static str,
66    started: Instant,
67    total: Option<u64>,
68}
69
70impl<'a> ProgressBridge<'a> {
71    pub(crate) fn new(sink: &'a dyn LeanProgressSink, phase: &'static str, total: Option<u64>) -> LeanResult<Self> {
72        let context = Box::new(ProgressContext {
73            sink,
74            phase,
75            started: Instant::now(),
76            total,
77        });
78        let context_ptr: *const ProgressContext<'a> = &raw const *context;
79        let context_addr = context_ptr as usize;
80        let handle = LeanCallbackHandle::<LeanProgressTick>::register(move |event| {
81            // SAFETY: `context_addr` points at the `ProgressContext`
82            // boxed inside the owning `ProgressBridge`. The bridge keeps
83            // the callback handle live only for one synchronous Lean call
84            // and drops the handle before the context. Host progress
85            // shims do not store callback handles for later use.
86            let context = unsafe { &*(context_addr as *const ProgressContext<'_>) };
87            context.sink.report(LeanProgressEvent {
88                phase: context.phase,
89                current: event.current,
90                total: context.total,
91                elapsed: context.started.elapsed(),
92            });
93            LeanCallbackFlow::Continue
94        })?;
95        Ok(Self { handle, context })
96    }
97
98    pub(crate) fn abi_parts(&self) -> (usize, usize) {
99        self.handle.abi_parts()
100    }
101
102    pub(crate) fn decode<'lean, T>(&self, obj: Obj<'lean>) -> LeanResult<T>
103    where
104        T: TryFromLean<'lean>,
105    {
106        decode_progress_result(obj, &self.handle)
107    }
108}
109
110pub(crate) fn report_progress(
111    sink: Option<&dyn LeanProgressSink>,
112    phase: &'static str,
113    current: u64,
114    total: Option<u64>,
115    started: Instant,
116) -> LeanResult<()> {
117    let Some(sink) = sink else {
118        return Ok(());
119    };
120    let event = LeanProgressEvent {
121        phase,
122        current,
123        total,
124        elapsed: started.elapsed(),
125    };
126    catch_unwind(AssertUnwindSafe(|| sink.report(event)))
127        .map_err(|payload| lean_rs::__host_internals::host_callback_panic(payload.as_ref()))
128}
129
130fn decode_progress_result<'lean, T>(obj: Obj<'lean>, handle: &LeanCallbackHandle<LeanProgressTick>) -> LeanResult<T>
131where
132    T: TryFromLean<'lean>,
133{
134    match ctor_tag(&obj)? {
135        1 => {
136            let [value] = take_ctor_objects::<1>(obj, 1, "Except.ok")?;
137            T::try_from_lean(value)
138        }
139        0 => {
140            let [status_obj] = take_ctor_objects::<1>(obj, 0, "Except.error")?;
141            let status = u8::try_from_lean(status_obj)?;
142            progress_status_to_result(status, handle)?;
143            Err(lean_rs::__host_internals::host_internal(
144                "progress shim returned Except.error with successful callback status",
145            ))
146        }
147        other => Err(conversion_error(format!(
148            "expected Lean Except ctor from progress shim (tag 0 = error, 1 = ok), found tag {other}"
149        ))),
150    }
151}
152
153fn progress_status_to_result(status: u8, handle: &LeanCallbackHandle<LeanProgressTick>) -> LeanResult<()> {
154    match LeanCallbackStatus::from_abi(status) {
155        Some(LeanCallbackStatus::Ok) => Ok(()),
156        Some(LeanCallbackStatus::StaleHandle) => Err(lean_rs::__host_internals::host_internal(
157            "Lean progress shim called a stale callback handle",
158        )),
159        Some(LeanCallbackStatus::WrongPayload) => Err(lean_rs::__host_internals::host_internal(
160            "Lean progress shim called a callback handle through the wrong payload trampoline",
161        )),
162        Some(LeanCallbackStatus::Stopped) => Err(lean_rs::__host_internals::host_internal(
163            "progress sink asked Lean to stop, but host progress does not define stop semantics",
164        )),
165        Some(LeanCallbackStatus::Panic) => Err(handle.last_error().unwrap_or_else(|| {
166            lean_rs::__host_internals::host_internal("progress sink panicked without recording a callback error")
167        })),
168        None => Err(conversion_error(format!(
169            "Lean progress shim returned unknown callback status byte {status}"
170        ))),
171    }
172}
lean_rs_host/host/progress.rs

lean_rs_host/host/
progress.rs
