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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
//! Fuzzing entry points (feature `fuzzing`, not semver-stable).
//!
//! The in-tree `crates/lean-rs/fuzz/` cargo-fuzz crate drives the
//! `pub(crate) abi` decoders with `Arbitrary`-generated Lean-shaped
//! inputs constructed via `lean-rs-sys` public helpers. Those decoders
//! are `pub(crate)`, so this module is the *only* place that exposes
//! them for an external test harness — and only when the `fuzzing`
//! feature is enabled.
//!
//! Per `docs/architecture/01-safety-model.md`'s "fuzz arbitrary raw
//! pointers" non-goal, every entry point takes a `*mut lean_object`
//! that the caller must have produced from a real `lean-rs-sys`
//! allocator. The wrappers do not validate provenance; they only
//! observe that decoders return either `Ok(_)` or
//! `Err(LeanError::Host(stage = Conversion))`.
//!
//! The `Drop` of every wrapped `Obj<'lean>` runs `lean_dec`, so the
//! caller transfers exactly one refcount per call.
use lean_object;
use crateTryFromLean;
use crate;
use crateLeanResult;
use crateLeanRuntime;
use crateObj;
/// Wrap a raw owned Lean pointer (one refcount transferred from the
/// caller) and decode it as a Rust `String`.
///
/// # Errors
///
/// Returns `LeanError::Host { stage: Conversion, .. }` if the input is
/// not a Lean `String` (wrong tag, scalar, malformed UTF-8).
///
/// # Safety
///
/// `raw` must be a non-null pointer produced by a `lean-rs-sys`
/// allocator, owning exactly one Lean reference count.
pub unsafe
/// Decode a raw owned pointer as a `Vec<u8>` interpreted as a
/// `ByteArray`.
///
/// # Errors
///
/// Returns `LeanError::Host { stage: Conversion, .. }` if the input is
/// not a packed-byte scalar array (wrong tag, wrong elem size).
///
/// # Safety
///
/// Same as [`decode_string`].
pub unsafe
/// Decode a raw owned pointer as a `Vec<u64>` interpreted as
/// `Array UInt64`.
///
/// # Errors
///
/// Returns `LeanError::Host { stage: Conversion, .. }` if the input is
/// not an array of polymorphic-boxed `u64` values.
///
/// # Safety
///
/// Same as [`decode_string`]; additionally the array's element type
/// must be polymorphic-boxed `u64` (Lake's `Array UInt64` encoding).
pub unsafe
/// Decode a raw owned pointer as an `Option<u64>` interpreted as
/// `Option UInt64`.
///
/// # Errors
///
/// Returns `LeanError::Host { stage: Conversion, .. }` if the input
/// does not match Lean's mixed-arity `Option` encoding (`None` =
/// `lean_box(0)`, `Some x` = ctor tag 1 with one field).
///
/// # Safety
///
/// Same as [`decode_string`].
pub unsafe
/// Decode a raw owned pointer as a `Result<u64, String>` interpreted
/// as `Except String UInt64`.
///
/// # Errors
///
/// Returns `LeanError::Host { stage: Conversion, .. }` if the input
/// is not an `Except` ctor (tag 0 = `error`, tag 1 = `ok`), or if
/// either branch's payload fails its own decode.
///
/// # Safety
///
/// Same as [`decode_string`].
pub unsafe
/// Decode a raw owned pointer as a `u64` interpreted as a Lean `Nat`
/// (scalar fast path; bignum branch surfaces a typed `Conversion`
/// error).
///
/// # Errors
///
/// Returns `LeanError::Host { stage: Conversion, .. }` if the input
/// is not a scalar-tagged `Nat` that fits a `u64` (bignum / wrong tag).
///
/// # Safety
///
/// Same as [`decode_string`].
pub unsafe
/// Read the tag of a constructor, surfacing a typed `Conversion` error
/// when the input is not a constructor at all.
///
/// # Errors
///
/// Returns `LeanError::Host { stage: Conversion, .. }` if the input is
/// a scalar or non-constructor heap object.
///
/// # Safety
///
/// Same as [`decode_string`].
pub unsafe
// Re-export the public error type so fuzz harnesses can pattern-match
// on `LeanError::Host` without crossing through `lean_rs::error`.
pub use crateLeanError;