feat: add base-locked per-PR contract plans

Draft
DU
3mo ago
+5905-186

Why

The generated-plan verifier authenticated the base template itself, but a
template could include a shared contract body that was then resolved from the
PR/head workspace. A PR could weaken that transitive body while retaining a
base-approved wrapper. That breaks the central promise that the contract comes
from protected base policy.

What changed

  • materializes every authenticated contract_paths snapshot into an isolated
    per-target include tree;
  • supplies both repository-relative and declared include-root-relative snapshot
    views ahead of all head production include paths;
  • shadows only declared contract paths, so undeclared production headers still
    resolve from the exact head revision;
  • keeps the immutable base-native regression compiled against exact head
    production code;
  • adds an adversarial preprocessor regression where the head weakens a
    transitive body and changes production to agree with it; verification must
    still use the base body and report a counterexample;
  • updates the drift and contract-portfolio documentation to distinguish branch
    source, published images, registry policy, model-checked scope, native
    regression scope, and branch-protection promotion.

Validation and publication

  • CI run 30538756694
    passed all 49 tests, including the adversarial transitive-contract
    regression;
  • exact source commit
    8a7e1aae040a9f17a7e7513e7bb29c9495afcedb was built and both image variants
    passed their ESBMC smoke checks in
    release run 30541259801;
  • verifier:
    ghcr.io/dusterbloom/lucebox-esbmc-ai-verifier@sha256:9321a4aa371efec1b55e33dff0c1cefbc10778aa7f38b07cb2b84cff1c9ed39e;
  • repair:
    ghcr.io/dusterbloom/lucebox-esbmc-ai-repair@sha256:e33712eac4207a74562fe9d9fda9a9456ce41c175456dda3dd54e7ba7286c597;
  • the current Luce first-wave registry is accepted by this planner;
  • git diff --check passed.

Rollout

The Lucebox draft pins both post-smoke digests consistently across policy and
workflows. After rebasing onto current main, its exact base=head bootstrap
verified all five generated contracts and the legacy shadow in
run 30548178937.
The current Lucebox exact head, including its post-rebase CI integration fix,
also verified all five contracts in both lanes in
run 30555414224.
The updated verifier also supports a separate authenticated nightly timeout;
Lucebox’s five-block nightly passed both lanes with approximately 58.5 seconds
of KVFlash margin in
run 30561396096.

This remains a draft until the companion source and Lucebox pin changes are
reviewed and merged into their protected base branches. The three new Lucebox
targets remain advisory and require separate per-target promotion after soak
and maintainer approval.

Lucebox first-wave integration:
https://github.com/dusterbloom/lucebox-hub/pull/9