6.4. Storage strategy🔗

setup_benchmark fib n => 2 ^ n auto-generates two top-level defs:

• fib._leanBench_complexity : Nat → Nat

• fib._leanBench_runChecked : Nat → IO (Option UInt64)

The macro stores Names pointing at these defs (not Syntax, not Expr) in the env extension. Names are trivially serializable; the defs themselves are normal Lean code and ship in the user's .olean.

runChecked is uniformly Nat → IO (Option UInt64): returns some hash when the function's return type has a Hashable instance, else none after forcing the result. Uniform type avoids type-level branching leaking through the design.