WCET phase 5 (#778): data-dependent masked-ceiling loop certificates

[avrabe]

What

Extends the --wcet-hints scry seam (untrusted oracle + sound synth-side checker) past const-trip / const-depth to a DATA-DEPENDENT loop whose exit bound is a masked value i REL (x & K). This is the named richer-certificate follow-up to WCET phase 4 (bounded recursion), applying the same untrusted-hint + sound-checker pattern to data-dependent loop shapes — no scry dependency, a synth-side seam.

Refs #778, #242 (Track D schedulability).

The certificate design (what synth verifies)

The witness is an entry-independent masked ceiling, not merely a decreasing measure. A decreasing measure proves termination; a finite WCET number additionally needs an entry-independent upper bound on the measure's initial value. That discriminator is the mask:

• x & K ∈ [0, K] for ANY runtime x when K's sign bit is clear (Sym::Masked { mask }, tracked from And rd, _, #K). Base identity is irrelevant — x & K ≤ K regardless of what x holds (simpler and more robust than recursion's masked chain, which needs the base identity for its decrement).
• The real per-iteration loop bound lies somewhere in [0, K], so synth DERIVES the worst-case trip as the MAX over both endpoints (rhs = K and rhs = 0), requiring both to terminate. A single endpoint is unsound for a count-DOWN loop — the fatal class (see below). The both-endpoints max is pinned in claims.yaml under SYNTH-WCET-CYCLE-MODEL.
• Eq/Ne masked exits are restricted to |step| == 1 (else an interior bound value can be missed — the divisibility-divergence trap), carried over from the recursion module.
• Hint-gated + derive-not-trust, mirroring the equality-exit and recursion-depth seams: unhinted → still declines loop; a --wcet-hints loop_bounds entry only gates consumption; the emitted trip is synth's DERIVED ceiling (new source mask-ceiling), never the raw hint.

bound ≥ actual evidence (unicorn Thumb-2 cross-check)

scripts/repro/wcet_phase5_778_masked_loop_soundness.py executes the compiled loops and asserts bound ≥ executed insns for the worst-case input + entry-independence across the masked domain:

• count-up maskloop(0xFFFFFFFF) = r0 21: 138 insns ≤ 262 cyc; maskloop(0): 19 ≤ 262.
• count-down cd(0) = r0 10 (10 iterations — the rhs=0 worst case): 180 insns ≤ 339 cyc. A naive single-endpoint seed (rhs=7) would have derived trip 3 → a bound below the real 10-iteration execution. The both-endpoints max derives 10 — this is the load-bearing soundness case.

invalid-cert-rejected evidence (red-first)

• too-low hint (3 < derived 7) → REJECTED hint-below-derived-trip, function stays declined.
• UNMASKED i < param (no entry-independent ceiling) → still declines loop + hint-unverifiable-induction even WITH a hint. param is Sym::Top, never Sym::Masked, so eval_pred returns None — the mask is the sole discriminator. This is the existing data_dependent_hint_is_rejected_unverifiable test staying green: proof the decline moved onto the masked shape, not widened to every runtime bound.
• unhinted masked loop → still declines loop (opt-in gate).

before → after decline matrix

shape	before	after
masked loop i < (x&K), no hint	loop decline	loop decline (opt-in)
masked loop, correct hint ≥ K	loop decline	BOUNDED (mask-ceiling, derived trip)
masked loop, hint < derived	loop decline	loop decline + hint-below-derived-trip
unmasked i < param, any hint	loop + hint-unverifiable-induction	unchanged (decline moved, not widened)

Gates

• crates/synth-cli/tests/wcet_bound_gate.rs: 5 new phase-5 fixtures (count-up accept, count-down both-endpoints, unhinted decline, too-low reject, unmasked reject). 39/39 gate tests pass.
• claims.yaml: pins the both-endpoints max (let (hi, lo) = (at(ceiling)?, at(0)?);) — a single-endpoint regression reddens claim-check. 25/25 claims hold.
• .github/workflows/ci.yml: phase-5 note on the existing WCET gate step.
• No regression: phase-2/3/4 unicorn harnesses + all 21 wcet unit tests pass.

Frozen + claim status

• Frozen-safe: WCET reads the already-final instruction stream and never mutates it; the ELF .text is byte-identical with or without --wcet-hints (verified). The sidecar is additive metadata.
• claims: 25/25 hold; status.json unchanged (new evidence under the existing SYNTH-WCET-CYCLE-MODEL id).

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L