studio/proxy
2
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

docs(lean4): add Rust cross-references to formal specs

Browse Source 
Add documentation comments linking Lean 4 specifications to their
corresponding Rust implementations (tree_predict, mlp_predict_32,
PackedNode). Reference TorchLean arXiv ID for future axiom replacement.

Signed-off-by: Sienna Meridian Satterwhite <sienna@sunbeam.pt>
This commit is contained in:
Sienna Meridian Satterwhite
2026-03-10 23:38:22 +00:00
parent 97e58b5a42
commit 3628424f43
3 changed files with 19 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
lean4/Sunbeam/Model/DecisionTree.lean
View File

@@ -2,13 +2,23 @@ import Sunbeam.Model.Basic
namespace Sunbeam
/-- A decision tree node (inductive = automatic termination for structural recursion). -/
/-- A decision tree node (inductive = automatic termination for structural recursion).
This is an abstract specification of the Rust packed-array representation:
`type PackedNode = (u8, f32, u16, u16)` — `(feature_index, threshold, left, right)`
Leaf nodes in Rust use `feature_index = 255`; the threshold encodes the decision:
`< 0.25` → Allow, `> 0.75` → Block, otherwise → Defer.
Here we use an inductive type so that structural recursion gives automatic termination. -/
inductive TreeNode where
| leaf (decision : Decision) : TreeNode
| split (featureIdx : Nat) (threshold : Float) (left right : TreeNode) : TreeNode
deriving Repr
/-- Tree prediction by structural recursion (termination is automatic). -/
/-- Tree prediction by structural recursion (termination is automatic).
Corresponds to `ensemble::tree::tree_predict` in Rust, which loops over a flat
packed-node array. The semantic behavior is identical: split nodes compare
`input[featureIdx]` against `threshold` and branch left/right. -/
def treePredictAux {n : Nat} (input : Fin n → Float) : TreeNode → Decision
| .leaf d => d
| .split idx thr left right =>

6
lean4/Sunbeam/Model/MLP.lean
View File

@@ -4,7 +4,11 @@ import Sunbeam.Model.ReLU
namespace Sunbeam
/-- Weights for a 2-layer MLP (input → hidden → scalar output). -/
/-- Weights for a 2-layer MLP (input → hidden → scalar output).
Corresponds to `ensemble::mlp::mlp_predict_32` in Rust, which uses const generic
`INPUT` and a fixed hidden dimension of 32. Here `hiddenDim` is a parameter so
structural properties can be proved generically. -/
structure MLPWeights (inputDim hiddenDim : Nat) where
w1 : Fin hiddenDim → FloatVec inputDim
b1 : FloatVec hiddenDim

4
lean4/Sunbeam/Model/Sigmoid.lean
View File

@@ -13,8 +13,8 @@ float inputs. They cannot be proved inside Lean because `Float` operations are
`@[extern]` (opaque to the kernel). The axioms form a documented trust boundary:
we trust the C runtime's `exp` implementation.
When TorchLean ships its verified Float32 kernel, these axioms can be replaced
with proofs against that kernel.
When TorchLean (arXiv:2602.22631) ships its verified Float32 kernel, these
axioms can be replaced with proofs against that kernel.
-/
/-- Sigmoid output is always positive: exp(-x) ≥ 0 ⟹ 1+exp(-x) ≥ 1 ⟹ 1/(1+exp(-x)) > 0. -/