Skip to main content

Module witness

Module witness 

Source
Expand description

Sparse solve witness — per-entry residual audit for SubLinear orchestrator outputs.

ADR-001 open question #3:

Does solve_on_change need a witness? Probably yes — a caller wants to verify the delta-solve’s output equals the full-solve’s output up to ε. Cheap to compute; one extra A·x.

This module closes that gap, but with an important refinement: a full A · x matvec costs O(nnz(A)), which would dominate the SubLinear orchestrator’s own cost and defeat the architectural win. Instead, we verify only the entries the orchestrator returned — the closure rows.

Restricted residual: for each (i, x_i) entry, compute r_i = b[i] - Σ_j A[i,j] · x[j] using a sparse x map. The audit succeeds iff max_i |r_i| ≤ tolerance · max(1, ‖b‖_∞). Cost is O(|entries| · avg_row_nnz) — same complexity class as the orchestrator. Independent of n for sparse DD matrices.

§When to use

  • Audit mode during development: run the SubLinear orchestrator, then witness the output. A failed witness is a real bug in the solver, not just a tolerance miss — by construction the sparse-Neumann path can only over-iterate, never produce a wrong answer on a strict-DD matrix.
  • Trust-but-verify in production: gate downstream agent actions on witness success. The cost is the same complexity class as the solve, so the verification is essentially free relative to the solve cost.
  • Regression guards: a property test that fuzzes deltas and asserts witness success on every output is a strong correctness signal for the SubLinear stack.

Structs§

VerifySparseSolutionOp
Op marker for verify_sparse_solution. SubLinear in n.
WitnessReport
Result of a witness check.

Functions§

verify_sparse_solution
Verify a sparse solution returned by one of the SubLinear orchestrators against the matrix + RHS.