ci: pilot bounded ESBMC verification

[dusterbloom]

Why

This fork-only pilot tests a narrow merge promise: when a PR changes a reviewed
state-machine core, Lucebox can select the smallest approved contract and
require deterministic bounded evidence. AI may propose repairs or missing
contracts, but it never defines or satisfies the merge gate.

The first wave targets three host-side decisions with high correctness
leverage: snapshot ownership, speculative token commitment, and KVFlash
logical-to-physical ownership.

This is intentionally one pilot PR because the three contracts, path-selection
policy, authenticated verifier images, and CI wiring form one reviewable
end-to-end safety path. Promotion is still a separate decision for each
target; this PR does not make any of the new contracts merge-blocking.

Reviewer guide

Review the production changes and their native regressions first, then review
the contract registry/manifest and workflow selection wiring. The immutable
image digests and hosted evidence establish the execution boundary; the
rollout section records the remaining maintainer decisions. Historical
bootstrap runs are retained below for auditability and are not substitutes for
the current exact-head checks.

What changed

• retains the two base-registered required inline prefix-cache targets;
• adds FullPrefixCacheState and migrates the full snapshot adapter to explicit
  key, slot, effective-boundary, and victim reservations;
• adds shared SpecCommitDecision production logic used by five model-family
  decode loops for accepted-prefix, bonus, budget, and safe token selection;
• adds KvFlashResidencyMap as the pager's authoritative CPU ownership map,
  including bounded logical growth, partial-bijection checks, protected
  eviction, rollback, masks, and epoch handling;
• adds dependency-free native regressions and CMake targets for all three;
• registers three new generated contracts as advisory, with exact
  properties, exclusions, PR/nightly bounds, protected shared harness bodies,
  and path-based selection;
• generalizes the mutation campaign to four representative defects;
• pins companion 0.3.0 verifier and repair images consistently across the
  protected registry, legacy manifest, and every workflow use site;
• adds regression checks that workflow pins cannot drift and transitive formal
  bodies cannot silently disappear from protected contract/trigger paths;
• records proof, mutation, image-acceptance, and nightly-bound evidence in
  formal/FIRST_WAVE_EVIDENCE.md.

The full-cache and KV contracts deliberately separate small model-checked
sequences from wider exact-head native lifecycle tests. GPU DMA, numerical
model behavior, HTTP orchestration, rollback/EOS emission, and whole-system
correctness remain outside these claims.

Rebase onto current main

The branch is rebased onto 2229bf6a186ce72d7c48840eb7aeeaa48eee11c6.
Conflict resolution:

• preserves main's _raw_unit_test_targets/check structure while registering
  each of the four standalone first-wave tests exactly once;
• preserves main's helper-based request-processing refactor while binding the
  effective full-snapshot boundary before reservation and cleaning up a
  rejected confirmation;
• adapts the new Qwen35-MoE invalid-decision path to main's two-argument
  recurrent-state restore API and checks its result.

GitHub reports the PR mergeable with no conflicts at exact head
326a43782cd329ccfd11630c4ae607690df6ee9f.

Trust-boundary fix and immutable images

Companion commit 8a7e1aae040a9f17a7e7513e7bb29c9495afcedb
materializes authenticated base contract snapshots ahead of head production
include paths, closing the transitive-include shadowing gap.

• 49-test companion CI;
• post-build verifier and repair smoke;
• verifier:
  ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:9321a4aa371efec1b55e33dff0c1cefbc10778aa7f38b07cb2b84cff1c9ed39e;
• repair:
  ghcr.io/dusterbloom/lucebox-esbmc-ai-repair@sha256:e33712eac4207a74562fe9d9fda9a9456ce41c175456dda3dd54e7ba7286c597.

Rebased-head validation

Local post-rebase baseline checks at dd01abd5:

• Luce registry/planner suite: 10 passed;
• the four standalone native targets built with -j4 and passed through CTest;
• the conflict-sensitive http_server.cpp and qwen35moe_backend.cpp objects
  compiled;
• generated nightly plan: 5/5 verified, KVFlash 114.25 s;
• legacy nightly manifest: 5/5 passed, KVFlash 112.49 s;
• all four mutation cases passed: each defect produced its required
  counterexample while applicable prefix-cache controls remained verified;
• independent conflict-resolution review and git diff --check passed.

Current exact-head CI integration checks at f1e9e0cd:

• repository-wide Ruff: passed;
• Luce registry/planner suite: 10 passed;
• server unit plus all four first-wave native tests: 5/5 passed;
• independent adversarial review and git diff --check: passed;
• standard CI run 30555368450:
  uv workspace, Windows build/smoke, Linux build/CTest, and both megakernel
  architecture imports passed. The RTX 3090 job remains pending because
  this fork currently has no registered self-hosted runners; it is not a test
  failure.

Hosted post-rebase mode=all bootstrap at dd01abd5:

• generated protected plan: 5/5 verified in 3m28;
• legacy-manifest shadow: 5/5 passed in 5m01;
• generated KVFlash: 109.89 s; legacy KVFlash: 175.53 s;
• plan SHA-256:
  3b44025140576c0e3e49458c61d386e74057fb4fbfab36b1c3aa71dbad526ea3;
• generated report SHA-256:
  b6ca2e50cf85520375d13967c77d5e104f1f082b161dc6e9b4d23221cd022782;
• legacy report SHA-256:
  f7090943e6946fd0bbc3eef551578953432d1ddb1c620dfded65b97d66848cb1;
• run 30548178937.

Hosted current exact-head mode=all validation at 326a4378:

• generated protected plan: 5/5 verified in 3m56;
• legacy-manifest shadow: 5/5 passed in 3m55;
• generated KVFlash: 131.46 s; legacy KVFlash: 137.47 s;
• plan SHA-256:
  7c0add83702426ed3bd3b30278fa53a1b955864459525c75e0bffead69fc5fce;
• generated report SHA-256:
  a0f28f68a77c293b35a54acda7c7f7b3b9e8fe9326966327a3b16000b2f81e5d;
• legacy report SHA-256:
  92967bc6803f133bcb990af06e1e6b616aa8b47b7d03df32cea4db16efd64e5c;
• run 30555414224.

Hosted exact-head mode=nightly bootstrap:

• generated protected plan: 5/5 verified in 4m38;
• legacy-manifest shadow: 5/5 passed in 4m36;
• generated five-block KVFlash: 173.76/180 s;
• legacy five-block KVFlash: 172.14/180 s;
• plan SHA-256:
  abab0e72619f6dd9c9718858c514cce2211719c7b31d7963270d58c64e8cdd31;
• generated report SHA-256:
  96c9924ee08c50e2ac98f75098afc06a6d65437dd1f25a4844a3ef38abd9a002;
• legacy report SHA-256:
  95631d7d6743cd86375b887f38fa3f629d6ea0804c614f1aeb5c933a1b3c0f74;
• run 30548927583.

The earlier nightly run had only 6–8 seconds of hosted margin. The separate
nightly timeout now provides approximately 58.5 seconds of margin in the
slower lane. The earlier six-block calibration timed out in both lanes in
run 30543897953.

Hosted exact-head mode=nightly with the separate KVFlash timeout:

• generated protected plan: 5/5 verified in 4m36;
• legacy-manifest shadow: 5/5 passed in 4m53;
• generated KVFlash: 167.92/240 s;
• legacy KVFlash: 181.48/240 s;
• plan SHA-256:
  d50d74575fae0871a6ac0eb94b2a36946edd4dcf4e6f7ca3f919ded5f5fec6f9;
• generated report SHA-256:
  f045a24c6c8619091d375c488ae9b7295f5cc1ed197f795c23723fcc606b302e;
• legacy report SHA-256:
  23a526ceb8f28279be848ef3548919d9247d9e185f715d9b10f515b22e7f1744;
• run 30561396096.

Trust and rollout

This PR intentionally keeps prefix-cache-full-lifecycle,
spec-commit-exactness, and kvflash-residency-map advisory. The image-pin
transition and target enforcement are separate review decisions.

Remaining gates:

1. review and merge companion PR Add Discord community link to README #1 and this pin/source transition into their
   protected base branches;
2. collect repeat hosted nightlies with the new meaningful KVFlash runtime margin;
3. review and promote each new target separately, including its protected
   contract, bounds, latency budget, and maintainer ownership.

This draft does not alter branch protection.

Companion implementation:
dusterbloom/lucebox-esbmc-ai#1