feat(#778): WCET phase 4 — bounded self-recursion via a verified depth-hint#813
Merged
Conversation
Convert the phase-3 `recursion` decline for exactly the shape synth can prove sound: a SINGLE-self-call chain whose controlling value is entry-independently bounded by a mask (`m = param & K ∈ [0,K]`), decreasing by a const step toward a base guard on the SAME masked quantity. synth DERIVES its own max depth (never the raw hint) via the loop trip machinery seeded at `init = mask`; a `--wcet-hints` `recursion_depth` entry only gates consumption. The composer folds the certified self-edge as `(max_depth+1) × frame_cost` instead of declining. Soundness legs (all enforced, else decline): - single self-call, multiplier 1 (tree/fib recursion → reject: exponential frames) - self-call arg = (same masked quantity) − const step (range containment) - base guard control-dependence: self-call unreachable when the guard fires - exit_index-derived depth (wrap/divisibility-safe), frame_count = depth+1 Decline-honesty MOVED not deleted: uncapped countdown (runtime-unbounded param), mutual/indirect recursion, multi-self-call → still LOUD-decline `recursion` with `hint-unverifiable-recursion` / `hint-below-derived-depth` machine reasons. Evidence: masked md bounded (derived depth 15, 16 frames, 752 cyc); unicorn cross-check md(0xFFFFFFFF)=267 insns across all frames <= 752 (entry-independent); fib/countdown/too-low-hint reject with specific reasons. .text byte-identical. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ursion - wcet_bound_gate.rs: 5 phase-4 fixtures (masked accept w/ derived depth 15 / 752 cyc EXACT literal, unhinted-still-declines non-vacuity, too-low-hint rejected RED-FIRST, fib tree-recursion + uncapped-countdown + mutual all reject with specific machine reasons) + assert_hint_rejection helper. - wcet_compose.rs: 3 pure-composer unit tests (certified self folds depth frames, folds non-self callee per-frame, distinct mutual cycle STILL declines). - scripts/repro/wcet_phase4_49_recursion_soundness.py: unicorn cross-check — md(0xFFFFFFFF)=267 insns across all 16 frames <= 752 (entry-independent). - ci.yml: wcet_bound_gate step comment extended to phase 4. - claims.yaml: pin the (max_depth+1) frame-count fold (SYNTH-WCET-CYCLE-MODEL); claim_check green 25/25. - verified-codegen-roadmap.yaml: VCR-WCET-002 sys-verification, links verifies VCR-001 + refines VCR-WCET-001; rivet validate NON_XREF=0. - CLAUDE.md Track D: document phase 4. Frozen 10/10 unchanged (WCET is a byte-invisible sidecar). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ndness)
Advisor-caught unsound acceptances in the phase-4 recursion checker:
1. CONDITIONAL DECREMENT: the checker's linear walk applied the arg computation
(the decrement) unconditionally, but only proved the self-call control-
dependent on the base guard — NOT that the guard→self-call region is
straight-line. A decrement gated on a SECOND guard (e.g. `param > 100`) was
modeled as `m-step` while a runtime path skipping it recurses UNBOUNDED. Fix:
enforce the region `(guard, self-call]` is (a) branch-free and (b) single-entry
(no branch targets into it) — the linear-body analog of the loop analyzer's
branch discipline. Adversarial fixture (would emit a finite bound on an
infinite recursion) now declines `recursion` + hint-unverifiable-recursion.
2. COUNT-UP UNDER-ESTIMATE: depth was seeded at init=mask only; for a count-up
(step>0) the worst-case init is 0, so seeding mask under-estimates. Fix:
evaluate exit_index at BOTH endpoints {0, mask}, require both terminate, take
the max (entry-independent worst case regardless of direction). Eq/Ne base
guards restricted to step ±1 (interior inits could otherwise miss the target
residue class while endpoints land).
Gate + repro harness: add the conditional-decrement adversarial case (both
assert declined). masked accept unchanged (depth 15 / 752 cyc). 34 gate tests +
11 compose units green; clippy/fmt clean; claims 25/25; rivet NON_XREF=0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
v0.49 Lane 3. Converts the
recursionWCET decline for the BOUNDABLE case: an untrusted recursion-depth hint (extends the--wcet-hintsscry seam) is SOUNDLY CHECKED — the bounddepth × per-frameis admissible only if synth verifies the recursion cannot exceed the hinted depth (straight-line single-entry const-decrement); otherwise the hint is REJECTED with a machine reason and the function still declines.Soundness gates (red-first, verified from scratch):
wcet_bound_gate34/34 incl.wrong_hint_below_real_trip_is_rejected_red_first.scripts/repro/wcet_phase4_49_recursion_soundness.py: bounded self-recursion under a correct hint → bounded (bound ≥ actual); a too-low hint (3<15) → declinedhint-below-derived-depth; a conditional-decrement / count-up recursion → declinedhint-unverifiable-recursion(a soundness fix — the arg region isn't straight-line single-entry)..textbyte-invisible (WCET sidecar): frozen 10/10 (control_step 0x00210A55). claims 25/25 (new depth-frame constant pinned). rivet clean (new sys-verification carries averifieslink). L7's async gate re-verified green on the merged tree.Note: the authoring agent hit an API stall after committing; this PR was salvaged by re-verifying every gate from scratch on the rebased tree (commit-per-step preserved all 3 commits).
🤖 Generated with Claude Code