# Laws, proofs, and the runtime boundary Use **Bend 2.0.26**. Start with `bend guide`; check with `bend version`. CI downloads that release and verifies its SHA-256. Versioned archives are at . `BEND=/path/to/bend` selects the executable for the proof gate. ```sh bend PROOF.bend --check-only # all 19 laws, no open claims bun run check:proofs # safety audit + proofs + byte-for-byte regeneration bun run proofs:generate # intentional update: prove, compile, write artifacts bun run proofs:artifact # compiler-free source/bridge/artifact receipt check bun run check:fast # proof gate + types + affected tests, no full suite ``` `LAWS.bend` contains the independently reviewed specifications. Change the implementation or proof, not the claim, when a proof fails. No holes, axioms, unsafe definitions, or sampled inputs establish these proofs. Normal checks never rewrite artifacts; only `proofs:generate` does. Development remains buildless for the extension, and installed Fovea needs no Bend executable. ## Coverage ledger | Laws | Production connection | | --- | --- | | 6 disclosure laws | Executed compiled `disclosure` export, consumed by the renderer. | | 5 accounting laws | Executed compiled `shownCount` / `remainingCount` exports, consumed by both renderers. | | 4 heat-basis laws | Executed compiled `basisStep` export, interpreted by basis extension. | | 4 rational heat-algebra laws | Model only; not a proof of the Float64 solver. | **15 production-linked laws, four model-only laws.** Linking a law does not prove every caller, codec, compiler transformation, or numerical operation. ## From proofs to executed code This follows Pi Fabric's compiler-to-library pattern: 1. `LAWS.bend` names the actual exports in `proofs/kernel.bend`, not independent lookalikes. `PROOF.bend` proves those claims with `--check-only`. 2. `scripts/compile-bend.mjs` invokes Bend's JS backend on that same kernel. It checks export names and compiled arities against `proofs/kernel-abi.json`, parses the JS, and accepts only the pinned CLI footer before removing its two invocation statements. It exposes the existing definitions through Bend's own `run_lib` trampoline. No algorithm is translated into handwritten JS. 3. Esbuild eliminates unused CLI/IO code. Remaining imports and known host-effect primitives are rejected. The pure library and ABI declarations are committed as `src/verified/generated/kernel.js` and `kernel.d.ts`. 4. `src/core/disclosure.ts` and `src/verified/policy.ts` are small, fail-closed Boolean/tag and number/BigInt codecs. `render.ts` and `heat.ts` execute their returned decisions and commands; there is no optional assertion or fallback implementation beside the verified path. 5. `manifest.json` binds the transitive proof sources, bridge, ABI, codecs, toolchain versions, and artifact bytes using SHA-256. `check:proofs` proves and reproduces everything byte-for-byte. `proofs:artifact` checks the receipt with development dependencies but **without invoking Bend**. It is a freshness receipt, not a cryptographic certificate or replacement for proof checking. `build:cli` checks the receipt before bundling and rejects remaining imports except Node built-ins. `prepack` additionally runs the full proof gate, not the test suite. `bun run check:package` packs with Bun, extracts outside the checkout, checks shipped receipt hashes, entry points and licenses, and runs the CLI and compiled kernel with no installed dependencies or Bend. Pass an existing tarball to check that exact archive before `bun publish path/to/package.tgz`. CI checks proofs, generation, and negative bridge fixtures. Published packages include the proof sources, receipt, and [Bend runtime notice](../THIRD_PARTY_NOTICES.md). No loader, generation step, or analysis import is added to idle extension startup. The trusted boundary includes Bend's checker, compiler and safe Base primitives, the library extraction/tree-shaking tools, ABI declarations and codecs, the host command interpreter, and the JS engine. Byte parity establishes freshness, not formal correctness of those components. `tests/verified-kernels.test.ts` checks numeric/tag boundaries and spies on real renderer/heat consumers to catch bypasses. `tests/proofs.test.ts` mutates exported wrappers, the ABI, compiler footer, source receipts and generated bytes: the gate must reject drift, not bless a parallel model. ### Runtime numeric domain The pinned backend supports immediate naturals through **2^48 - 1**, stricter than JavaScript's `MAX_SAFE_INTEGER`. The codecs reject negative, fractional, nonfinite or out-of-range counts before execution and reject invalid results. Bend laws quantify over unbounded naturals; runtime claims apply within this checked domain. Kernel intermediates stay in range: subtraction saturates, comparison selects an input, and basis indices reconstruct or decrease `have`. Natural array counts/order requests in production are well within the bound. Bend emits a recursive `Nat.min`, unsuitable for large counts. The compiled accounting implementation instead compares and selects. `counts-proof.bend` proves that implementation equal to the structural `Nat.min` specification for **all naturals**, then transports the original five laws through the equality. No handwritten JS optimization replaces the proven implementation. ABI tests exercise counts at zero, 100,000, 2^32 and the backend maximum. ## Safe Bend only `check:proofs` is authoritative; plain `bend` does not enforce our extra policy. The gate walks the complete local import closure of laws, proofs and kernel, rejecting: - every `@unsafe`, even an unused helper in a transitive import; - references to unsafe Base primitives `Array.fork` and `Array.join`; - foreign C/JS imports, remote packages, and unrecognized import forms; - paths or symlinks escaping the repository. Local imports use `import ./file.bend as Alias` (parent paths inside the repo are allowed); the only nonlocal import is `import Base`. Comments and quoted literals are not code. Proof-module `main` is never executed; the compiler's kernel CLI is stripped and likewise never executed. Bend 2.0.26's Base **contains two unsafe array-sharing definitions; we do not use them**. Each proof gate audits `bend base`: those must be the only unsafe definitions, and their names may appear only at their declarations, excluding indirect use through other helpers. Changes fail closed for a new audit. Importing Base is not a claim that its entire library is unsafe-free. This is not a sandbox for a malicious compiler or concurrent edits. Negative fixtures exercise unsafe paths without adding unsafe code to actual proofs. ## What is proved? ### Executed: disclosure decisions `proofs/disclosure.bend`, exported as `kernel.disclosure`, supplies the renderer's candidate-admission decision. The laws cover all five-Boolean input combinations: | Law | Guarantee | | --- | --- | | `scope_wins` | Out-of-scope nodes are dropped, including repeated nuclei. | | `exclusion_wins` | Exclusion wins over disclosure and nucleus exceptions. | | `fresh_revealed` | An eligible unseen node is admitted. | | `seen_suppressed` | A seen node is suppressed when repetition is disabled. | | `periphery_suppressed` | A seen non-nucleus cannot repeat. | | `nucleus_repeated` | Repetition admits an eligible nucleus, seen or not. | `Reveal` means admit a candidate, not necessarily fit it within the output budget. `Suppress` increments the disclosure count; `Drop` does not. The previous finite lookup table has been replaced by the compiled function. Three ABI probes cover all result tags and distinguish all five argument positions, rather than re-enumerating the proved truth table. Host set membership, nucleus classification, suppression bookkeeping, sorting and formatting remain tested. ### Executed: prefix accounting `proofs/counts.bend` specifies `shown = min(total, requested)` and `remaining = total - shown`. The compiled equivalent supplies both renderers' prefix caps, omission counts and returned `shown` metadata. The five laws prove: - shown never exceeds total or requested; - shown plus remaining equals total; - a full prefix omits nothing; - applying the same cap twice is idempotent. `revealGroups` now reports the actual fitted prefix rather than all candidates as `shown`, matching its omission footer. Integration tests check that contract. These laws do **not** prove token estimation, UTF-16 lengths, formatting, header fallbacks, or binary-search safety/maximality. ### Executed: heat-basis extension commands `proofs/basis.bend`, exported as `kernel.basisStep`, directs `extendChebyshevVectors` in `src/core/heat.ts`. Given existing vector count `have` and desired maximum order, the compiled result is the only admission decision: | Law | Guarantee | | --- | --- | | `basis_empty_refused` | An empty basis yields `Empty`, never a recurrence. | | `basis_complete_retained` | A basis already beyond the target order yields `Done`. | | `basis_first_order` | A one-vector basis with requested order >= 1 yields `First`. | | `basis_next_exact` | A missing order >= 2 yields exactly `Next(have, have-1, have-2)`. | The host refuses `Empty`, returns on `Done`, computes the first multiplication on `First`, and reads/writes the indices from `Next`. Existing basis vectors are reused. This is a structural bridge, **not** a proof of the Float64 recurrence, array dimensions/aliasing, cache generation, Bessel coefficients or heat accuracy. ### Model only: exact heat-transport conservation `proofs/heat.bend` models nonnegative rational matrix-vector transport with integer numerators. `nat-proof.bend` proves arithmetic by induction, without algebraic axioms or conservation assumptions. Each source column has mass numerator a[j] and weights w[i,j]. `Normalized` requires a **proof** that every column sums to the same strictly positive denominator D. Then: ``` out[i] = sum_j w[i,j] * a[j] sum_i out[i] = D * sum_j a[j] ``` Input mass has denominator Q; output has denominator D*Q, so this is exact conservation of rational mass. Any finite nonnegative rational column-stochastic matrix admits such a common denominator. `Nat` establishes nonnegativity; lists are zero-padded and an empty list is the zero vector, not a fixed-point simulation. | Law | Guarantee | | --- | --- | | `heat_vector_add_mass` | Vector addition adds total masses. | | `heat_scale_mass` | Scaling scales total mass. | | `heat_transport_mass` | Normalized transport conserves rational mass. | | `heat_singleton_mass` | A probability-one self-transition retains arbitrary mass. | This targets algebra beneath `forwardHeat`: its exact walk is P = W D_degree^-1, with identity on isolated nodes. The premise is checked normalization evidence, not conservation assumed as an axiom. Negative tests reject a mass-dropping implementation and a forged normalization witness. The singleton gives a concrete, nonempty valid witness. **Boundary:** this model is not compiled into the heat solver. We have not proved that `buildCsr` establishes its premises, degree conjugation refines this walk, or the Chebyshev polynomial equals the exponential. Extending conservation from one step through powers to the infinite Poisson mixture `exp(-t) sum_k t^k/k! P^k` still needs an iteration/limit development. IEEE-754 rounding, Bessel/gamma evaluation, pruning and truncation need error bounds. Changing real arithmetic to naturals does not discharge these obligations. ### Not a law: monotonically growing lit sets The old “dwell monotonicity” test covered one fixture. The universal claim is false even for exact symmetric heat: relative thresholding can lose nodes as heat spreads. With edges `(0,1,1e-6)` and `(0,2,1)`, seed `[0,1,0]`, the 2%-of-maximum lit set has size **3 at t=8** but **2 at t=64**. Both Chebyshev and the independent scaled-Taylor reference witness this in `tests/heat.test.ts`. The fixture test is named for what it asserts, not a universal invariant. ## Test-retirement ledger Retired the products that repeated executed Bend laws; keep small witnesses for unproved compiler/codec boundaries in `tests/verified-kernels.test.ts`: | Retired coverage | Proof replacement | Remaining runtime probes | | --- | --- | --- | | 32-case disclosure truth table | Six exhaustive disclosure laws | Three cases covering all tags and distinct Boolean patterns for every argument position. | | 6 × 6 count-pair matrix against `Math.min` | Five accounting laws plus `shown_equiv` | Five selected pairs: zero in either argument, asymmetric counts, 2^32, and the backend maximum (also catches recursive lowering). | | Repeated basis-order samples / duplicate `Done` case | Four basis-command laws | Every command tag and `Next` indices at the minimum and backend maximum; real heat-interpreter wiring. | Invalid-input rejection, unsafe/import guards, artifact/ABI mutations and actual consumer-call tests remain: Bend does not prove the host bridge or safety gate. **No existing integration or numerical tests are retired.** | Coverage | Remaining obligation | | --- | --- | | Disclosure suppression/repeated nuclei | Actual IDs, set membership, edge classification and bookkeeping. | | Scope/exclusion before overflow | Cap ordering and full artifact contents. | | Budgets, group rendering, overflow, ops | Strings, footers, fallback paths, caller clamps and fitting. | | `conserved-heat.test.ts`: conservation/singletons | Float64 degree correction, isolated-node dispatch and tolerances. | | Stationary mass / analytic star | Spectral mixing, exponential, focus conjugation and excess subtraction. | | `heat.test.ts`: Bessel/Taylor/positivity | Approximation, coefficients, pruning and rounding errors. | | Recurrence-prefix parity / cache isolation | Float64 interpreter, mutable arrays, aliasing and graph invalidation beyond the proved index commands. | | Lit-set widening | Fixture only; the counterexample protects against a universal misstatement. | | Nuclei/startup/filesystem/extraction/sync/provenance | Seed assembly, imports, IO, parsers, races and attribution. | Sample-by-sample tests of the pure disclosure predicate would be redundant; keep ABI/generation and integration witnesses. Retiring budget examples would require a production-executed fit kernel proving both safety and prefix maximality under actual string costs and fallback rules. In particular, appending is not universally byte-monotone: the omission footer disappears at the full prefix, its decimal count can shrink, and a header alone can exceed a tiny budget. The full-prefix fast path handles one discontinuity, not a proof of binary search.