lean-rs-worker-protocol 0.1.19

Wire protocol and shared value types for the lean-rs worker process boundary.
Documentation 
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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131

//! Hidden closed worker capability export shapes.
//!
//! The worker protocol lets downstream callers choose export names, but not
//! ABI shapes. This module is the shared source of truth for the small set of
//! worker operation signatures that may cross the child process boundary.
//! It is public only because parent, child, and harness live in separate
//! crates; it is not downstream extensibility for arbitrary worker exports.

use lean_toolchain::{
    LeanExportAbiRepr, LeanExportArgAbi, LeanExportOwnership, LeanExportResultConvention, LeanExportReturnAbi,
    LeanExportSignature,
};

/// Worker operation shape used for checked capability dispatch.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum WorkerExportOperation {
    Metadata,
    Doctor,
    JsonCommand,
    StreamingCommand,
    FixtureMul,
    FixturePanic,
}

impl WorkerExportOperation {
    /// Stable diagnostic label for the operation shape.
    #[must_use]
    pub const fn as_str(self) -> &'static str {
        match self {
            Self::Metadata => "metadata String -> IO String",
            Self::Doctor => "doctor String -> IO String",
            Self::JsonCommand => "json command String -> IO String",
            Self::StreamingCommand => "streaming command String, USize, USize -> IO UInt8",
            Self::FixtureMul => "fixture multiplication UInt64, UInt64 -> UInt64",
            Self::FixturePanic => "fixture panic UInt8 -> Unit",
        }
    }
}

/// Trusted manifest signature for a metadata export.
#[must_use]
pub fn metadata_signature(symbol: impl Into<String>) -> LeanExportSignature {
    string_io_signature(symbol)
}

/// Trusted manifest signature for a doctor export.
#[must_use]
pub fn doctor_signature(symbol: impl Into<String>) -> LeanExportSignature {
    string_io_signature(symbol)
}

/// Trusted manifest signature for a JSON command export.
#[must_use]
pub fn json_command_signature(symbol: impl Into<String>) -> LeanExportSignature {
    string_io_signature(symbol)
}

/// Trusted manifest signature for a streaming command export.
#[must_use]
pub fn streaming_command_signature(symbol: impl Into<String>) -> LeanExportSignature {
    LeanExportSignature::function(
        symbol,
        vec![
            owned_object_arg(),
            scalar_arg(LeanExportAbiRepr::USize),
            scalar_arg(LeanExportAbiRepr::USize),
        ],
        io_return(LeanExportAbiRepr::LeanObject),
    )
}

/// Trusted manifest signature for the private fixture multiplication export.
#[must_use]
pub fn fixture_mul_signature(symbol: impl Into<String>) -> LeanExportSignature {
    LeanExportSignature::function(
        symbol,
        vec![scalar_arg(LeanExportAbiRepr::U64), scalar_arg(LeanExportAbiRepr::U64)],
        pure_return(LeanExportAbiRepr::U64),
    )
}

/// Trusted manifest signature for the private fixture panic export.
#[must_use]
pub fn fixture_panic_signature(symbol: impl Into<String>) -> LeanExportSignature {
    LeanExportSignature::function(
        symbol,
        vec![scalar_arg(LeanExportAbiRepr::U8)],
        pure_return(LeanExportAbiRepr::LeanObject),
    )
}

fn string_io_signature(symbol: impl Into<String>) -> LeanExportSignature {
    LeanExportSignature::function(
        symbol,
        vec![owned_object_arg()],
        io_return(LeanExportAbiRepr::LeanObject),
    )
}

const fn owned_object_arg() -> LeanExportArgAbi {
    LeanExportArgAbi::new(LeanExportAbiRepr::LeanObject, LeanExportOwnership::Owned)
}

const fn scalar_arg(repr: LeanExportAbiRepr) -> LeanExportArgAbi {
    LeanExportArgAbi::new(repr, LeanExportOwnership::None)
}

const fn pure_return(repr: LeanExportAbiRepr) -> LeanExportReturnAbi {
    LeanExportReturnAbi::new(repr, return_ownership(repr), LeanExportResultConvention::Pure)
}

const fn io_return(repr: LeanExportAbiRepr) -> LeanExportReturnAbi {
    LeanExportReturnAbi::new(repr, return_ownership(repr), LeanExportResultConvention::IoResult)
}

const fn return_ownership(repr: LeanExportAbiRepr) -> LeanExportOwnership {
    match repr {
        LeanExportAbiRepr::LeanObject => LeanExportOwnership::Owned,
        LeanExportAbiRepr::U8
        | LeanExportAbiRepr::U16
        | LeanExportAbiRepr::U32
        | LeanExportAbiRepr::U64
        | LeanExportAbiRepr::USize
        | LeanExportAbiRepr::I8
        | LeanExportAbiRepr::I16
        | LeanExportAbiRepr::I32
        | LeanExportAbiRepr::I64
        | LeanExportAbiRepr::ISize
        | LeanExportAbiRepr::F64 => LeanExportOwnership::None,
    }
}