docs: search plumbing for agent autoresearch loops

CHANGELOG.md

@@ -4,6 +4,13 @@
 
 ### Added
 
+- **Docs: autoresearch / search-plumbing guide.** New mdBook chapter
+  [`search-plumbing.md`](docs/mdbook/src/search-plumbing.md) ties budgets,
+  batch APIs, compact `DerivedResult` envelopes, claim graphs, and certificate
+  coverage together; Sphinx gains [`api/workload.rst`](docs/sphinx/api/workload.rst)
+  plus `DerivedResult.to_dict` / `BudgetExceededError` entries. Cross-links from
+  getting-started, intro, README, claim-graphs, batch, and budgets.
+
 - **Budgets, cooperative cancellation, and a determinism seed** (P1 search
   plumbing item 4): `alkahest.Budget(wall_ms=..., max_steps=..., seed=...)`
   and `alkahest.context(budget=...)` push a wall-clock/step budget into a

README.md

@@ -228,9 +228,21 @@ Most transforming operations (`diff`, `simplify`, `integrate`, `sum_*`, …) ret
 - `.value` — the result expression
 - `.steps` — derivation log (list of rewrite rules applied)
 - `.certificate` — Lean 4 proof term, when available
+- `.to_dict()` / `.to_json()` — versioned machine-parseable envelope; use `mode="compact"` in agent loops
 
 Exceptions: `limit` returns a bare `Expr`, and `series` returns a `Series` (with its own `.polynomial` / `.order` fields). Use `.value` only on `DerivedResult`.
 
+### Search plumbing (agent loops)
+
+| Need | Entry point |
+|---|---|
+| Bound one candidate | `Budget` + `context(budget=…)` → `BudgetExceededError` (`E-BUDGET-*`) |
+| Fan out without aborting | `batch_map` / `integrate_many` / `simplify_many` / `diff_many` |
+| Compact logs | `DerivedResult.to_dict(mode="compact")` |
+| Session provenance | `alkahest.research` claim graphs |
+
+Docs: [Autoresearch / agent loops](https://alkahest-cas.github.io/alkahest/search-plumbing.html).
+
 ---
 
 ## Reinforcement learning

docs/mdbook/src/SUMMARY.md

@@ -18,10 +18,11 @@
 - [Interoperability](./interop.md)
 - [Reinforcement learning](./rl.md)
 - [Derivation logs](./derivations.md)
-- [Batch and streaming evaluation](./batch.md)
 - [Claim graphs](./claim-graphs.md)
 - [Lean certificates](./lean-certs.md)
   - [Certificate coverage](./certificate-coverage.md)
 - [Error handling](./errors.md)
-- [Budgets, cancellation, and determinism](./budgets.md)
+- [Autoresearch / agent loops](./search-plumbing.md)
+  - [Budgets, cancellation, and determinism](./budgets.md)
+  - [Batch and streaming evaluation](./batch.md)
 - [Stability policy](./stability.md)

docs/mdbook/src/batch.md

@@ -119,3 +119,22 @@ failed = [(o.index, o.error) for o in outs if not o.ok]
 `KeyboardInterrupt` or `SystemExit` still propagates and stops the batch, since
 swallowing those would make the process unkillable. Everything else — including every
 Alkahest `E-*` error and any exception your own `fn` raises — is captured.
+
+## Combining with budgets
+
+Wrap the batch in `context(budget=…)` so each candidate inherits the same
+cooperative wall/step limit (and optional seed). A trip surfaces as
+`BatchItem(ok=False, error={"code": "E-BUDGET-00x", …})` rather than aborting
+the rest of the batch — see [Budgets](./budgets.md).
+
+```python
+with ak.context(pool=pool, budget=ak.Budget(wall_ms=50, max_steps=10_000, seed=7)):
+    outs = ak.integrate_many(candidates, x, parallel=True)
+```
+
+## See also
+
+- [Autoresearch / agent loops](./search-plumbing.md)
+- [Budgets, cancellation, and determinism](./budgets.md)
+- [Derivation logs — compact envelopes](./derivations.md#machine-parseable-output-to_dict--to_json)
+- [Error handling](./errors.md)

docs/mdbook/src/budgets.md

@@ -164,3 +164,11 @@ except ak.IntegrationError as e:
 
 On the Rust side (`alkahest_core::budget`): `Budget`, `enter`, `BudgetGuard`, `check`,
 `seed`, `is_active`, `request_cancel`, `clear_cancel`, `is_cancelled`, `BudgetError`.
+
+## See also
+
+- [Autoresearch / agent loops](./search-plumbing.md)
+- [Batch and streaming evaluation](./batch.md) — budgets compose with `*_many` /
+  `batch_map`; a trip becomes one failed `BatchItem`, not a killed process
+- [Error handling](./errors.md) — `E-BUDGET-*` in the exception hierarchy
+- [Claim graphs](./claim-graphs.md) — session-level provenance around budgeted calls

docs/mdbook/src/claim-graphs.md

@@ -212,3 +212,12 @@ print(report.to_markdown())
 runs the full experimental-mathematics loop — high-precision quadrature, `guess_relation`
 for the integer relation, a recorded conjecture, symbolic proof, Lean certificate, JSON
 round trip, and re-verification — and prints the rendered document.
+
+## See also
+
+- [Autoresearch / agent loops](./search-plumbing.md) — how claim graphs fit next to
+  budgets, batch APIs, and compact result envelopes
+- [Budgets](./budgets.md) — bound one candidate so a hard instance cannot stall the session
+- [Batch](./batch.md) — fan out many `DerivedResult` producers without aborting on one failure
+- [Derivation logs](./derivations.md#machine-parseable-output-to_dict--to_json) —
+  `to_dict(mode="compact")` for token-efficient claim payloads

docs/mdbook/src/derivations.md

@@ -212,3 +212,10 @@ An invalid `mode` (anything other than `"full"`/`"compact"`) raises
 `DerivedResult` is per-call. To accumulate many results into a citable, serialisable,
 re-verifiable artifact — a DAG of claims with stable IDs, hypotheses, and certificate
 status — see [claim graphs](./claim-graphs.md).
+
+## See also
+
+- [Autoresearch / agent loops](./search-plumbing.md)
+- [Batch](./batch.md) — produce many `DerivedResult`s without aborting on one failure
+- [Budgets](./budgets.md) — bound the call that produced the derivation
+- [Certificate coverage](./certificate-coverage.md) — `certificate_status` in the envelope

docs/mdbook/src/getting-started.md

@@ -259,6 +259,29 @@ with alkahest.context(pool=pool, simplify=True):
     expr = z**2 + alkahest.sin(z)
 ```
 
+### Agent / autoresearch loops
+
+For a fan-out of candidates under a wall-clock or step budget, with results that
+survive context compaction:
+
+```python
+import alkahest as ak
+
+pool = ak.ExprPool()
+x = pool.symbol("x")
+
+with ak.context(pool=pool, budget=ak.Budget(wall_ms=100, seed=1)):
+    outs = ak.integrate_many([x**2, ak.sin(x)], x)
+    for item in outs:
+        if item.ok:
+            print(item.value.to_dict(mode="compact")["verification"]["status"])
+        else:
+            print(item.error["code"])  # e.g. E-INT-001 or E-BUDGET-001
+```
+
+Full picture: [Autoresearch / agent loops](./search-plumbing.md),
+[Budgets](./budgets.md), [Batch](./batch.md), [Claim graphs](./claim-graphs.md).
+
 ## Running the examples
 
 The `examples/` directory in the Git repository has runnable end-to-end scripts. With `alkahest` installed (`pip install alkahest` or `maturin develop` as above), from the repository root run:

docs/mdbook/src/intro.md

@@ -14,11 +14,13 @@ A general-purpose symbolic math library designed around three axes:
 
 **Ergonomics.** The Python API uses operator overloading for natural expression construction. Results are rich objects with `.value`, `.steps`, and `.certificate` attributes. Error messages carry structured codes, location information, and suggested remediations.
 
+**Agent loops.** Budgets and cancellation, batch APIs that never abort on one bad candidate, versioned compact result envelopes, and session-level [claim graphs](./claim-graphs.md) are first-class — see [Autoresearch / agent loops](./search-plumbing.md).
+
 ## Design principles
 
 **Explicit representations.** The type system distinguishes `UniPoly` (FLINT-backed univariate polynomial), `MultiPoly` (sparse multivariate), `RationalFunction`, and the generic `Expr` tree. Converting between them is an explicit call. There are no silent representation changes hiding performance cliffs.
 
-**Stateless by design.** No global assumption contexts. No hidden caches that change behavior. All context (domains, simplification policy, precision) is passed explicitly or bundled into expression structure. This makes results deterministic and parallelism safe.
+**Stateless by design.** No global assumption contexts. No hidden caches that change behavior. All context (domains, simplification policy, precision, budgets) is passed explicitly or scoped through `context(...)`. This makes results deterministic and parallelism safe.
 
 **Composable transformations.** `trace`, `grad`, `jit`, and `certify` operate on a shared traced representation and stack freely: `jit(grad(f))` compiles a derivative, `jit(grad(grad(f)))` compiles a second derivative.
 

docs/mdbook/src/python-api.md

@@ -4,4 +4,14 @@ The Sphinx-generated Python API is published alongside this guide:
 
 **[Open the Python API documentation](https://alkahest-cas.github.io/alkahest/api/)**
 
-It includes `ExprPool`, simplification, calculus, polynomials, numerics, transforms, matrices, ODE/DAE, solvers, codegen, and error types.
+It includes `ExprPool`, simplification, calculus, polynomials, numerics, transforms, matrices, ODE/DAE, solvers, codegen, error types, and the [search / workload](https://alkahest-cas.github.io/alkahest/api/api/workload.html) surface (`Budget`, `batch_map`, `DerivedResult.to_dict`, …).
+
+Conceptual chapters for agent-facing plumbing:
+
+| Topic | Guide |
+|---|---|
+| Budgets, cancellation, seeds | [Budgets](./budgets.md) |
+| Batch / streaming fan-out | [Batch](./batch.md) |
+| Compact machine-parseable results | [Derivation logs](./derivations.md#machine-parseable-output-to_dict--to_json) |
+| Session provenance | [Claim graphs](./claim-graphs.md) |
+| Overview | [Autoresearch / agent loops](./search-plumbing.md) |

docs/mdbook/src/search-plumbing.md

@@ -0,0 +1,48 @@
+# Autoresearch / agent loops
+
+Alkahest is useful inside unsupervised or lightly-supervised math search loops
+because it is designed to be called **many times under a budget**, with results
+that stay auditable. The pieces below are the *search plumbing* that sits next
+to the mathematics:
+
+| Need | API | Guide |
+|---|---|---|
+| Bound one candidate so a hard instance cannot stall the sweep | `Budget`, `context(budget=…)`, `request_cancel` | [Budgets](./budgets.md) |
+| Fan out many candidates without one failure aborting the batch | `batch_map`, `integrate_many`, … | [Batch](./batch.md) |
+| Cheap, versioned payloads for logs / LLM context | `DerivedResult.to_dict(mode="compact")` | [Derivation logs](./derivations.md#machine-parseable-output-to_dict--to_json) |
+| Accumulate claims across iterations | `alkahest.research` claim graph | [Claim graphs](./claim-graphs.md) |
+| Ask “will this call certify?” before spending compute | `certifiable`, `require_certificate` | [Certificate coverage](./certificate-coverage.md) |
+
+A minimal loop shape:
+
+```python
+import alkahest as ak
+
+pool = ak.ExprPool()
+x = pool.symbol("x")
+candidates = [x**2, ak.sin(x), ak.log(ak.log(x))]
+
+with ak.research.session(title="Sweep", pool=pool, capture=True) as s:
+    with ak.context(pool=pool, budget=ak.Budget(wall_ms=200, max_steps=50_000, seed=7)):
+        for item in ak.integrate_many(candidates, x, parallel=True):
+            if not item.ok:
+                # E-BUDGET-* → deprioritize; E-INT-* → record and move on
+                continue
+            # Token-cheap record for the next iteration / a human referee
+            _ = item.value.to_dict(mode="compact")
+
+print(s.graph.to_markdown())
+```
+
+Honesty rules that matter in a loop:
+
+- A **budget trip is a fine answer**, not a crash — catch `BudgetExceededError`
+  (`E-BUDGET-*`) and deprioritize that candidate.
+- A **batch never drops a slot** — failures become `BatchItem(ok=False, error=…)`.
+- **Compact mode never hides verification status** — `verification["status"]`
+  stays readable; Lean source is omitted on purpose.
+- **Certificates are withheld rather than lied about** — see
+  [certificate coverage](./certificate-coverage.md).
+
+See also the runnable experimental-mathematics demo
+[`examples/pslq_research_loop.py`](https://github.com/alkahest-cas/alkahest/blob/main/examples/pslq_research_loop.py).

docs/sphinx/api/core.rst

@@ -132,27 +132,56 @@ DerivedResult
       with ``status == "certificate_available"`` has generated Lean source but
       has not been checked by Lean in this execution.
 
+   .. method:: to_dict(mode: str = "full") -> dict
+
+      Versioned machine-parseable envelope combining ``value``,
+      ``verification``, ``certificate_status``, and ``steps``.
+
+      :param mode: ``"full"`` (default) or ``"compact"``. Compact mode drops
+         ``before``/``after`` step text and uses short step keys (``r``/``s``),
+         but **never** renames or drops ``verification["status"]`` and never
+         includes Lean certificate source. See the
+         `derivation logs <../derivations.html#machine-parseable-output-to_dict--to_json>`_
+         chapter.
+
+   .. method:: to_json(mode: str = "full") -> str
+
+      ``json.dumps(self.to_dict(mode=mode))``.
+
+   .. attribute:: SCHEMA_VERSION
+   .. attribute:: STEPS_SCHEMA_VERSION
+
+      Class-level integers matching ``alkahest.RESULT_SCHEMA_VERSION`` and
+      ``alkahest.STEPS_SCHEMA_VERSION``.
+
    Example::
 
       dr = diff(sin(x**2), x)
       print(dr.value)   # 2*x*cos(x^2)
       for step in dr.steps:
           print(step['rule'], step['before'], "→", step['after'])
+      print(dr.to_dict(mode="compact")["verification"]["status"])
 
 Context manager
 ---------------
 
-.. function:: context(pool=None, domain="real", simplify=False)
+.. function:: context(pool=None, domain="real", simplify=False, assumptions=None, require_certificate=None, budget=None, **extra)
 
-   Context manager that sets a default pool and configuration.
+   Context manager that sets thread-local defaults for a block.
 
    Inside the context, :func:`symbol` creates symbols in the active pool
-   without passing it explicitly::
+   without passing it explicitly. Optional ``budget=`` pushes a
+   :class:`Budget` for the block (see the
+   `workload API <workload.html>`_ and the
+   `budgets guide <../budgets.html>`_)::
 
       with alkahest.context(pool=pool, simplify=True):
           z = alkahest.symbol("z")
           expr = z**2 + alkahest.sin(z)
 
+      with alkahest.context(pool=pool, budget=alkahest.Budget(wall_ms=50, seed=7)):
+          alkahest.integrate(z**2, z)
+
 .. function:: symbol(name: str, domain: str = "real") -> Expr
 
    Create a symbol in the active context pool. Raises ``RuntimeError``

docs/sphinx/api/errors.rst

@@ -169,6 +169,32 @@ Exception subclasses
           ak.diff(ak.sin(x), x)            # fine — certifies
           ak.integrate(ak.log(x), x)       # raises E-CERT-001
 
+.. exception:: BudgetExceededError
+
+   Code prefix ``E-BUDGET-*``. A cooperative budget or cancellation trip —
+   not a mathematical failure. Raised when an active
+   :class:`~alkahest.Budget` is exceeded (or :func:`~alkahest.request_cancel`
+   was called) at a checkpoint inside an engine that honors budgets
+   (notably :func:`~alkahest.integrate`). See the
+   `budgets guide <../budgets.html>`_ and the
+   `workload API <workload.html>`_.
+
+   - ``E-BUDGET-001`` — wall-clock limit elapsed
+   - ``E-BUDGET-002`` — step limit exceeded
+   - ``E-BUDGET-003`` — cancellation requested
+
+   Example::
+
+      import alkahest as ak
+
+      pool = ak.ExprPool()
+      x = pool.symbol("x")
+      try:
+          with ak.context(pool=pool, budget=ak.Budget(max_steps=0)):
+              ak.integrate(x**2, x)
+      except ak.BudgetExceededError as e:
+          print(e.code)  # E-BUDGET-002
+
 Catching errors by subsystem
 ----------------------------