1.2. Optional per-param setup🔗

If your benchmarked function operates on a structure that's expensive to build (a sorted array, a tree, a hashmap), declaring it as Nat → α will fold the build cost into every timed iteration and ruin the verdict — a log n search behind a O(n) setup looks linear in the report. Use the optional with prep := <ident> clause to hoist the setup out of the timing loop:

def mkArr (n : Nat) : Array Nat := (Array.range n).map (· * 7)

def prepInput (n : Nat) : Array Nat × Nat :=
  (mkArr n, (n.max 1 - 1) * 7 / 2)

partial def bsearch (a : Array Nat) (target : Nat) : Option Nat := Id.run do
  let mut lo := 0
  let mut hi := a.size
  while lo < hi do
    let mid := (lo + hi) / 2
    if a[mid]! < target then lo := mid + 1
    else hi := mid
  if lo < a.size && a[lo]! == target then some lo else none

def runBinary (input : Array Nat × Nat) : Nat :=
  (bsearch input.1 input.2).getD 0

setup_benchmark runBinary n => Nat.log2 (n + 1)
  with prep := prepInput

Type contract: prep : Nat → σ and the benchmarked function has type σ → α. The prep's return type σ must be Hashable (Array Nat × Nat derives it automatically); the macro hashes the prep result before timing starts so its construction cost is fully paid up front. Prep then runs once per child-process spawn — not once per autotuner probe — and the inner loop calls the function with the prepared value.