lean-rs-host 0.1.0

Opinionated Rust host stack for embedding Lean 4 as a theorem-prover capability: typed sessions, kernel-check evidence handles, bounded MetaM services, batching, and session pooling. Built on top of the `lean-rs` FFI primitive.
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

//! Opaque handle for kernel-checked Lean evidence.

use core::fmt;

use lean_rs_sys::lean_object;

use lean_rs::LeanRuntime;
use lean_rs::Obj;
use lean_rs::abi::traits::{LeanAbi, TryFromLean, sealed};
use lean_rs::error::LeanResult;

/// Opaque receipt for a piece of Lean evidence the kernel accepted.
///
/// Constructed only on the
/// [`crate::host::evidence::LeanKernelOutcome::Checked`] branch returned
/// by [`crate::LeanSession::kernel_check`]. The Rust handle wraps the
/// Lean-side `Evidence` value (currently a one-field structure carrying
/// a `Lean.Declaration`) opaquely — Rust does not inspect the contained
/// proof term or declaration. The two operations callers do with a
/// handle are [`crate::LeanSession::check_evidence`] (re-run the kernel
/// against it) and [`crate::LeanSession::summarize_evidence`] (project
/// it to a bounded [`crate::host::evidence::ProofSummary`]).
///
/// [`Clone`] bumps the underlying refcount; [`Drop`] releases it.
/// Neither [`Send`] nor [`Sync`]: inherited from the crate-internal
/// owned-object handle.
pub struct LeanEvidence<'lean> {
    obj: Obj<'lean>,
}

impl Clone for LeanEvidence<'_> {
    fn clone(&self) -> Self {
        Self { obj: self.obj.clone() }
    }
}

impl fmt::Debug for LeanEvidence<'_> {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        // Opaque on purpose: the Rust side has no claim on Lean's
        // structural identity. Route through a Lean-authored
        // pretty-printer export when a diagnostic string is needed.
        f.debug_struct("LeanEvidence").finish_non_exhaustive()
    }
}

impl sealed::SealedAbi for LeanEvidence<'_> {}

impl<'lean> LeanAbi<'lean> for LeanEvidence<'lean> {
    type CRepr = *mut lean_object;

    fn into_c(self, _runtime: &'lean LeanRuntime) -> *mut lean_object {
        self.obj.into_raw()
    }

    #[allow(
        clippy::not_unsafe_ptr_arg_deref,
        reason = "sealed trait — caller invariant documented on LeanAbi::from_c"
    )]
    fn from_c(c: *mut lean_object, runtime: &'lean LeanRuntime) -> LeanResult<Self> {
        // SAFETY: `c` is an owned `lean_object*` produced by the Lean
        // kernel-check capability returning an `Evidence` value; per
        // Lake's `lean_obj_res` contract it carries one reference count.
        // `runtime` witnesses `'lean`.
        #[allow(unsafe_code)]
        let obj = unsafe { Obj::from_owned_raw(runtime, c) };
        Ok(Self { obj })
    }
}

impl<'lean> TryFromLean<'lean> for LeanEvidence<'lean> {
    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
        Ok(Self { obj })
    }
}