# API reference Lean doc comments provide hover documentation in the editor. `Tutorial/Guide.lean` is a compiled tutorial. `Tests/PublicAPI.lean` checks the declaration-level interface below, while `Tests/ModuleImport.lean` and `Tests/Import.lean` check module and ordinary source-file consumers. The library exports the following small interfaces. | Module | Responsibility | | --- | --- | | `waterfall` / `waterfall.Tactic` | `waterfall`, `waterfall?`, `Mode`, `Options` | | `waterfall.Core` | `run` and engine transitions | | `waterfall.Protocol` | `Config`, `Stats`, `Move`, `Candidate`, `Job`, `Node`, `Space`, `SearchPolicy`, `Hooks` | | `waterfall.Execution` | Metered move execution and final root validation | | `waterfall.Critics` | Guarded blocked-premise moves and bounded search guidance | | `waterfall.Choices` | Generic lazy selection, filtering, collection and commitment | | `waterfall.Parallel` | Isolated concurrent trials, shared work accounting and cancellation | | `waterfall.Committed` | ACL2-inspired callbacks over the shared engine | | `waterfall.Suggestions` | Checked standalone scripts and editor hints from retained paths | | `waterfall.Observe` | Optional timing, control middleware, action recording and replay | | `waterfall.Canonical` | Optional canonical goal encoding for replay checks | The [proof architecture walkthrough](IMPLEMENTATION.md) maps these interfaces to the named proof-stage generators and explains how their child obligations form one compatible proof continuation. Generator helpers are private; extensions use `movesFor`, `operations`, and `Hooks`. ## Tactic interface `Options` extends engine `Config` with `mode : Mode := .search` and `cpus : Nat := 1`. Standard Lean configuration syntax accepts individual fields or `(config := { ... })`. The adapter passes `mode.hooks` and `Options.toConfig` to `Parallel.run`; one CPU calls `run` directly. Custom callback functions are configured through `run`, preserving the arbitrary typed policy state interface. It adds no proof-search algorithm. `run (cfg : Config) (rules : Array (TSyntax term) := #[]) (hooks : Hooks := {})` runs in `TacticM` and returns `Stats` after closing all original goals. Failure restores Lean's original proof state. Effort and external observer effects are not rolled back. `Stats.choices` contains retained labels in reverse proof order. `waterfall?` installs `Suggestions.run` inside each worker. It records only accepted steps and gives the winning proof a checked editor replacement. `Suggestions.compile` accepts the input checkpoint, original goals, retained path, rules and optional hooks; it returns `Script` (`tactic`, `text`, `usedTerm`) while restoring the completed proof. It reparses the printed text and requires all original obligations to close with error recovery disabled. The inference operations and accepted-step hook contract are unchanged. `Move.subject` identifies the expression acted upon; `Move.command?` optionally shares a command an adapter already constructs. These are presentation metadata, independent of dispatch, cost and policy selection. A command proposal is always checked as printed text. ## Search and checkpoints `Choices α = (α → TacticM Bool) → TacticM Bool` is effectful lazy enumeration. Returning `true` from a visitor stops it. `Choices.first` commits to the first emitted choice even if its downstream continuation fails; `filter` retains a subsequence; `collect` eagerly materializes all emitted choices and pays their cost. A `Node σ` contains a saved Lean proof state, all pending `Job`s, typed policy state and the retained plan. Each job has its own remaining structural allowance and ancestry. Never combine jobs from one checkpoint with Lean state from another. A `SearchPolicy` supplies its state type, initial state and `choose : Space State → Choices (Node State)`. `Space.expand` enumerates metered transitions for a selected goal and operation batches. `Space.restart` restores a compatible checkpoint, installs new policy state and charges an attempt. Already funded frontier entries remain selectable at attempt exhaustion; new expansion and restart are refused. Ambient limits still constrain traversal. ## Hooks - `charge`: reserve one operation before dispatch, including checkpoint restarts. Exceptions stop the run; reservations and external effects are not rolled back. - `policy`: choose transitions, agenda order and traversal. - `prelude`: infer bounded depth/strength trials from the original goals. Each request has its own attempt cap and the engine also limits all such work to one quarter of public effort. The ordinary `trials` schedule remains intact. - `trials`: finite batches of depth/positive-strength pairs by round. - `batches`: lazy structural groups; each original group must occur exactly once. - `order`: a permutation of candidate selectors within a batch; validated. - `cost`: effective path cost under the goal's context and rollback. Structural costs must respect the engine's positive intrinsic floor. - `extraMoves`: append general operations without renumbering the originals. - `around`: polymorphic middleware around a span and continuation. - `accepted`: observe only the retained complete proof's selections, in reverse order. `Move.preparation` distinguishes one-binder introduction, bulk introduction, pointwise equality, normalization and target splitting. Policies should use this typed field rather than diagnostic labels. `Critics.hooks` composes with an arbitrary existing policy: it appends guarded case-split proposals and places them first without dropping any candidate. Search mode enables its early goal-directed prelude; committed mode shares the moves and ordering only. An observer calls its continuation once and leaves proof state alone. Resource control middleware can reduce allowances or abort spans. The engine owns proof acceptance and rollback. Ordering and cost callbacks see temporary state; external IO side effects remain the callback author's responsibility. ## Progress and extension operations `Move.checkLocalChange` defaults to `false`. A structural extension may assign a shared witness, change another obligation, or update local values while leaving the selected target and assumption types unchanged. The engine accepts such a transition and charges its positive structural cost. Final root validation is unchanged; accepting a transition is not accepting a complete proof. Built-in generators set `checkLocalChange := true` to preserve their existing local stutter pruning. An extension can opt into this heuristic explicitly, or implement its own progress checks in `Move.run`. The heuristic compares the single child's target and assumption types with the input; it is deliberately not a general test of proof-state equality. The engine's positive cost floor and global attempt allowance still bound steps that leave a goal unchanged. ## Observation and replay Import `waterfall.Observe` explicitly. `capture` returns a `Report` with success, error, optional timing rows and an optional `Plan`. Timing rows distinguish inclusive and exclusive wall-clock nanoseconds and raw heartbeats. A `Control` can supply smaller per-span slices and a cooperative deadline. Deadlines are checked between spans; a process timeout belongs to the calling harness. Plans store versioned action selectors, goal/agenda encodings, selected focus, strength, costs and generated-child counts. Replay validates these against the same operations and supplied rules; it does not search for another route. Pass a stable source/theory key and retain the exact source version. Changed operations, selector order, costs or unrecorded provider state can invalidate a plan. Final root validation and Lean's kernel remain authoritative. See `Tests/SearchPolicy.lean` for a FIFO frontier, scored successors, commitment, sibling dependencies and charged checkpoint recovery; see `Tests/Observe.lean` for timing and replay examples. ## Parallel execution `Parallel.run cpus cfg rules withHooks` runs the same engine in isolated workers. `withHooks` receives a continuation accepting `Hooks`; call it once. Allocate mutable observers inside this function so each worker owns separate IO references: ```lean import waterfall import waterfall.Observe open Lean Elab Tactic waterfall example (P : Prop) (h : P) : P := by run_tac discard <| Parallel.run 2 {} #[] fun use => do let recorder ← Observe.Recorder.create use (recorder.hooks {} Mode.search.hooks) ``` Round `i` of `Hooks.trials` belongs to worker `i % cpus`; bounded prelude trials belong to worker zero. No trial is duplicated, and all callbacks otherwise describe one policy. The first observed complete proof wins; ordering among simultaneous completions is unspecified. This parallelizes iterative deepening, not sibling proof obligations or branches inside a single trial. Committed mode retains its local commitment semantics. A mutex reserves attempts across workers, including restarts. Each worker has its own engine counters and elaboration state. The enclosing remaining heartbeat allowance is divided equally; unused shares are currently not redistributed. Each worker records its spent heartbeats in a `finally` block, independently of whether it returns a proof result or an interrupt. The parent always cancels, joins, and reads these costs before adopting the winner. Actual child heartbeats, including failed and cancelled work, are charged to the parent's thread counter before acceptance. Aggregate overruns reject the result. Workers use dedicated threads so a caller running inside Lean's elaboration pool cannot starve them. Operating-system CPU affinity can impose lower CPU concurrency than `cpus`; zero is rejected. No process or CPU affinity is created by the tactic itself. The limit is per invocation, not a global limit on concurrent theorem elaboration. Parent cancellation and a completed proof signal cancellation to workers, which are always joined. Cancellation remains cooperative inside Lean operations. Increasing both work and heartbeat limits keeps every trial eventually available when the underlying schedule is fair. A fixed total budget can produce different coverage from sequential execution: speculation competes for the same resources. Custom callbacks must not share mutable IO references unless synchronized; use `withHooks` for per-worker recorders and other local state. Observer callbacks in an unsuccessful worker may already have run and are not undone by cancellation. `Stats.attempts` and `nodes` are aggregate counts; depth, strength and choices identify the winning worker. `Observe.capture` remains a sequential convenience API; use the initializer above for parallel observation.