From 3e6b93d54ee5c0c9cb0fad888bbbdec7668750f0 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 22 Jul 2026 15:52:47 +0200 Subject: [PATCH 1/4] feat(#778): WCET phase-5 data-dependent masked-ceiling loop certificates MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extend the --wcet-hints scry seam past const-trip/const-depth to a DATA-DEPENDENT masked bound (`i REL (x & K)`). The masked value is entry-independently bounded to [0, K] for ANY runtime x (x & K in [0,K]), so synth DERIVES the worst-case trip as the MAX over both endpoints of the bound domain (rhs=K and rhs=0, both required to terminate) — a single endpoint is unsound for count-down shapes. Hint-gated + derived-not-trusted, mirroring the equality-exit and recursion-depth seams: - new Sym::Masked{mask} tracked from `And rd,_,#K` (K>=0, sign-bit clear so x&K stays non-negative); base identity irrelevant (x&K<=K for any x) - eval_pred accepts (Slot, Masked) -> Pred{rhs:K, masked_ceiling:Some(K)}, surviving the SetCond->cmp#0 indirection via Sym::Bool - masked_exit_index: both-endpoints max + Eq/Ne |step|==1 restriction; always hint-gated - new WcetLoopBoundSource::MaskCeiling so the sidecar states the extra data-dependent-ceiling assumption (distinct from HintVerified) Decline moved not deleted: unhinted masked loop still declines `loop`; unmasked `i < param` still rejects `hint-unverifiable-induction` (param is Sym::Top, never Masked); too-low hint rejects `hint-below-derived-trip`. Frozen-safe: WCET reads the final stream, .text byte-identical w/ or w/o hints. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend/src/wcet_loops.rs | 130 +++++++++++++++++++-- crates/synth-backend/src/wcet_recursion.rs | 1 + crates/synth-core/src/wcet.rs | 11 ++ 3 files changed, 133 insertions(+), 9 deletions(-) diff --git a/crates/synth-backend/src/wcet_loops.rs b/crates/synth-backend/src/wcet_loops.rs index adeb2e88..a285813a 100644 --- a/crates/synth-backend/src/wcet_loops.rs +++ b/crates/synth-backend/src/wcet_loops.rs @@ -147,6 +147,15 @@ pub(crate) struct Pred { pub(crate) add: i64, pub(crate) rel: Rel, pub(crate) rhs: i32, + /// (#778 phase 5) The DATA-DEPENDENT masked bound: when the compare RHS is a + /// masked value `x & K` (`K = masked_ceiling ≥ 0`), the real per-iteration + /// bound lies in `[0, K]` for ANY runtime input (`x & K ∈ [0,K]`). `rhs` is + /// then the ceiling `K` (the entry-independent worst case). The trip count is + /// derived as the MAX over both endpoints of the bound domain (`rhs = K` and + /// `rhs = 0`) — a single endpoint is unsound for count-DOWN shapes — and the + /// result is always HINT-GATED (opt-in, mirroring the equality-exit gate). + /// `None` for a normal const bound (unchanged phase-2 behavior). + pub(crate) masked_ceiling: Option, } impl Pred { @@ -169,6 +178,13 @@ enum Sym { Slot { off: i64, add: i64 }, /// A 0/1 boolean holding `pred`. Bool(Pred), + /// (#778 phase 5) A masked value `x & K` (`mask = K ≥ 0`), for ANY `x`. The + /// value is entry-independently bounded to `[0, K]` — the base identity is + /// irrelevant (`x & K ≤ K` regardless of what `x` holds), unlike the + /// recursion module's masked chain which needs the base identity for the + /// decrement. Used ONLY as a data-dependent loop-bound ceiling (the compare + /// RHS); the trip count it yields is always hint-gated. + Masked { mask: i32 }, } /// Walk state: symbolic registers, slot writes since walk start, tainted slots @@ -260,8 +276,22 @@ fn eval_pred(cond: Condition, flags: &Option<(Sym, Sym)>) -> Option { add: *add, rel: Rel::of(cond), rhs: *c, + masked_ceiling: None, }), - // `cmp , #0` — the eqz / br_if lowering shape. + // (#778 phase 5) `cmp , ` — the counter is + // compared against a DATA-DEPENDENT masked bound `x & K ∈ [0, K]`. The + // ceiling `K` is the entry-independent worst case (`rhs = K`); the trip + // this yields is derived at BOTH endpoints of `[0, K]` and hint-gated. + (Sym::Slot { off, add }, Sym::Masked { mask }) => Some(Pred { + off: *off, + add: *add, + rel: Rel::of(cond), + rhs: *mask, + masked_ceiling: Some(*mask), + }), + // `cmp , #0` — the eqz / br_if lowering shape. The bool carries the + // ORIGINAL predicate (including any masked_ceiling), so a masked bound + // survives the SetCond→cmp#0 indirection. (Sym::Bool(p), Sym::Const(0)) => match cond { Condition::EQ => Some(p.negate()), Condition::NE => Some(*p), @@ -304,6 +334,10 @@ struct Region { init: Option, /// Proven trip count (body executions) + whether it is hint-gated. trip: Option<(u64, bool)>, + /// (#778 phase 5) True when the exit bound is a DATA-DEPENDENT masked ceiling + /// (`x & K`) rather than a literal const — the accepted bound then carries + /// the `MaskCeiling` source so the sidecar states the extra assumption. + masked_bound: bool, /// Per-iteration execution-count factor for instructions in this region. factor: u128, } @@ -370,6 +404,7 @@ pub(crate) fn analyze_loops( proof: None, init: None, trip: None, + masked_bound: false, factor: 1, }); } @@ -514,12 +549,15 @@ pub(crate) fn analyze_loops( r.trip = None; continue; }; + r.masked_bound = match shape { + ExitShape::HeadTest(p) | ExitShape::BottomTest(p) => p.masked_ceiling.is_some(), + }; r.trip = match shape { - ExitShape::HeadTest(p) => exit_index(init, step, &p), + ExitShape::HeadTest(p) => masked_exit_index(init, step, &p), ExitShape::BottomTest(p) => { // Body n (n ≥ 1) enters with v = init + (n−1)·step and repeats // while `pred` holds. K = 1 + (first m ≥ 0 where ¬pred fires). - exit_index(init, step, &p.negate()) + masked_exit_index(init, step, &p.negate()) .and_then(|(m, h)| m.checked_add(1).map(|k| (k, h))) } }; @@ -551,12 +589,22 @@ pub(crate) fn analyze_loops( } (Some(k), WcetLoopBoundSource::Static) } - // Equality-exit (hint-gated): unhinted → keep the decline. + // Hint-gated shape (equality-exit OR data-dependent masked ceiling, + // #778 phase 5): unhinted → keep the `loop` decline. A bound resting + // on either assumption is opt-in. (Some((_, true)), None) => (None, WcetLoopBoundSource::Static), - // Equality-exit with a hint: consume ONLY if derived ≤ hint. + // Hint-gated shape WITH a hint: consume ONLY if derived ≤ hint. The + // accepted source distinguishes a masked ceiling from an equality + // exit so the sidecar states which assumption the bound rests on. The + // emitted trip is always synth's DERIVED value, never the raw hint. (Some((k, true)), Some(h)) => { if k <= h { - (Some(k), WcetLoopBoundSource::HintVerified) + let source = if r.masked_bound { + WcetLoopBoundSource::MaskCeiling + } else { + WcetLoopBoundSource::HintVerified + }; + (Some(k), source) } else { rejections.push(rejection( idx, @@ -593,7 +641,9 @@ pub(crate) fn analyze_loops( region_instr_count: r.closer - r.head + 1, source, hint: match source { - WcetLoopBoundSource::HintVerified => hint, + WcetLoopBoundSource::HintVerified | WcetLoopBoundSource::MaskCeiling => { + hint + } WcetLoopBoundSource::Static => None, }, }); @@ -897,9 +947,21 @@ fn sym_step(op: &ArmOp, st: &mut WalkState, store_events: &mut Vec<(i64, Sym)>) st.kill_all_regs(); st.flags = None; } + // (#778 phase 5) `And rd, _, #K` with a NON-NEGATIVE const mask yields a + // value in `[0, K]` for ANY input (`x & K ≤ K`, and `≥ 0` because K's + // sign bit is clear). A masked value with K's sign bit SET (`K < 0`, + // e.g. 0xFFFFFFFF) can be negative — the ceiling reasoning collapses — + // so only a non-negative mask is tracked; everything else kills rd. + And { rd, op2, .. } => { + let v = match st.op2(op2) { + Sym::Const(mask) if mask >= 0 => Sym::Masked { mask }, + _ => Sym::Top, + }; + st.set_reg(*rd, v); + st.flags = None; + } // Single-register-destination ALU ops: kill exactly rd. - And { rd, .. } - | Orr { rd, .. } + Orr { rd, .. } | Eor { rd, .. } | Rsb { rd, .. } | Mvn { rd, .. } @@ -1147,6 +1209,55 @@ fn shift_slots(st: &mut WalkState, delta: i64) { /// with STATIC no-overflow checks over the whole counter walk in the /// predicate's signedness domain. Returns `(n, requires_hint)`; equality exits /// set `requires_hint` (consumed only under a verified `--wcet-hints` entry). +/// (#778 phase 5) Trip count for an exit predicate that may carry a +/// DATA-DEPENDENT masked bound. For a normal const bound (`masked_ceiling == +/// None`) this is exactly [`exit_index`]. For a masked bound `x & K ∈ [0, K]` +/// the real per-iteration bound is somewhere in `[0, K]` for ANY runtime input, +/// so the sound trip is the MAXIMUM over the whole bound domain: +/// +/// - A single endpoint is UNSOUND. For a count-UP loop (`i < bound`) the worst +/// case is the LARGEST bound (`K`); for a count-DOWN loop (`i > bound`) the +/// worst case is the SMALLEST bound (`0`). Seeding only `rhs = K` would emit a +/// bound BELOW a real count-down execution — the fatal class. +/// - We evaluate `exit_index` at BOTH endpoints (`rhs = K` and `rhs = 0`), +/// require BOTH to terminate (else the loop is not guaranteed-terminating for +/// every masked value), and take the MAX trip. Because the trip is monotone in +/// the bound for a threshold relation, the max over the two endpoints bounds +/// the max over the whole `[0, K]` interval (and per-iteration-varying bounds, +/// each `m_j ≤ K`, are covered too: a count-up exits by `counter = K`, a +/// count-down's worst case is the `rhs = 0` endpoint). +/// - For an Eq/Ne exit, an interior bound value can be MISSED by a step that does +/// not divide the distance (the divisibility-divergence trap), so endpoint +/// reasoning holds only when EVERY value in `[0, K]` is reachable — i.e. +/// `|step| == 1`. A larger step with an Eq/Ne masked bound is declined. +/// +/// The masked trip is ALWAYS hint-gated (the returned bool is forced true): a +/// bound resting on a data-dependent ceiling is opt-in, mirroring the +/// equality-exit gate. `None` propagates (unproven) whenever either endpoint +/// fails to terminate or wraps. +fn masked_exit_index(init: i32, step: i64, p: &Pred) -> Option<(u64, bool)> { + let Some(ceiling) = p.masked_ceiling else { + return exit_index(init, step, p); + }; + debug_assert!(ceiling >= 0); + // Eq/Ne masked bound: only |step| == 1 keeps every interior value reachable. + if matches!(p.rel, Rel::Eq | Rel::Ne) && step.abs() != 1 { + return None; + } + let at = |rhs: i32| -> Option { + let pr = Pred { + rhs, + masked_ceiling: None, + ..*p + }; + exit_index(init, step, &pr).map(|(k, _)| k) + }; + let (hi, lo) = (at(ceiling)?, at(0)?); + // Force hint-gated: a data-dependent ceiling is only ever consumed under a + // verified --wcet-hints entry. + Some((hi.max(lo), true)) +} + /// `None` = exit not statically guaranteed (or a possible wrap) → unproven. pub(crate) fn exit_index(init: i32, step: i64, p: &Pred) -> Option<(u64, bool)> { let s = step; @@ -1256,6 +1367,7 @@ mod tests { add, rel, rhs, + masked_ceiling: None, } } diff --git a/crates/synth-backend/src/wcet_recursion.rs b/crates/synth-backend/src/wcet_recursion.rs index 2f731ff6..f9a2d75d 100644 --- a/crates/synth-backend/src/wcet_recursion.rs +++ b/crates/synth-backend/src/wcet_recursion.rs @@ -239,6 +239,7 @@ pub(crate) fn analyze_recursion( add: base_pred.add, rel: base_pred.rel, rhs: base_pred.rhs, + masked_ceiling: None, // recursion derives its own depth via exit_index directly }; // Endpoint reasoning is sound only when `exit_index` is MONOTONE in init over // `[0, mask]`. For a threshold predicate (<, <=, >, >=) it is. For an diff --git a/crates/synth-core/src/wcet.rs b/crates/synth-core/src/wcet.rs index effeb04f..6258eb3d 100644 --- a/crates/synth-core/src/wcet.rs +++ b/crates/synth-core/src/wcet.rs @@ -175,6 +175,17 @@ pub enum WcetLoopBoundSource { /// trip count (divisibility + monotonicity + derived ≤ hint) before use. The /// emitted trip count is still synth's DERIVED value, never the raw hint. HintVerified, + /// (#778 phase 5) The loop's exit bound is a DATA-DEPENDENT masked ceiling + /// (`i REL (x & K)` for a runtime `x`): the real per-iteration bound lies in + /// `[0, K]` for ANY input (`x & K ∈ [0,K]`), so synth DERIVES the worst-case + /// trip as the MAX over both endpoints of that interval (`rhs = K` and + /// `rhs = 0`, both required to terminate) — an entry-independent ceiling. + /// Like [`HintVerified`] this is HINT-GATED: the derived trip is consumed + /// only under an explicit `--wcet-hints` entry the derived count respects + /// (`derived ≤ hint`); the emitted trip is synth's DERIVED value, never the + /// raw hint. A distinct source (not `HintVerified`) so the sidecar states the + /// extra data-dependent-ceiling assumption the bound rests on. + MaskCeiling, } /// One proven-bounded loop inside a bounded function (#778 phase 2). Loops are From c1f06a166dc7af751c8dc5f71847f6cae25b4e81 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 22 Jul 2026 15:54:10 +0200 Subject: [PATCH 2/4] test(#778): phase-5 masked-loop unicorn soundness cross-check Execute compiled masked-ceiling loops under unicorn (Thumb-2): bound >= actual for the worst-case input, entry-independence across the masked domain, and the count-DOWN case whose worst case is the rhs=0 endpoint (proves both-endpoints max is not the naive single-endpoint undercount). Plus decline-honesty: unhinted masked stays declined, too-low hint rejected, UNMASKED i Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../wcet_phase5_778_masked_loop_soundness.py | 210 ++++++++++++++++++ 1 file changed, 210 insertions(+) create mode 100755 scripts/repro/wcet_phase5_778_masked_loop_soundness.py diff --git a/scripts/repro/wcet_phase5_778_masked_loop_soundness.py b/scripts/repro/wcet_phase5_778_masked_loop_soundness.py new file mode 100755 index 00000000..e4d22ac0 --- /dev/null +++ b/scripts/repro/wcet_phase5_778_masked_loop_soundness.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python3 +"""#778 phase 5 masked-ceiling loop-bound soundness cross-check: execute a +compiled BOUNDED data-dependent loop under unicorn (Thumb-2) and confirm the +derived masked-ceiling bound is a sound upper bound on the ACTUAL executed cost +for the WORST-CASE runtime input over the whole masked domain. + +The masked-ceiling accept shape bounds its loop counter against a DATA-DEPENDENT +value `x & K ∈ [0, K]` for ANY runtime input `x`. synth derives the worst-case +trip as the MAX over both endpoints of that interval (`rhs = K` and `rhs = 0`) — +an entry-independent ceiling — and consumes it only under a verified +`--wcet-hints` `loop_bounds` entry. We drive the input that MAXIMIZES the real +trip and check: + + 1. functional result (r0) matches the WASM ground truth; + 2. bound_cycles >= total executed machine instructions (every machine insn + costs >= 1 cycle) — the masked-ceiling bound is a sound ceiling; + 3. ENTRY-INDEPENDENCE: several inputs (including the OTHER endpoint) all run + within the SAME bound — the count-up worst case is `x&K == K`, the + count-DOWN worst case is `x&K == 0`, and the both-endpoints max covers both. + +The load-bearing red half (the decline moved, not deleted): + - an UNMASKED data-dependent loop (`i < param`) STAYS declined `loop` even + WITH a hint (`hint-unverifiable-induction`) — the mask is the discriminator; + - a too-low hint (< derived) is REJECTED `hint-below-derived-trip`; + - unhinted, the masked loop STAYS declined `loop` (opt-in gate). + +This is execution-side evidence the cargo gate (wcet_bound_gate.rs) cannot +produce in-CI (no unicorn dep there); the gate pins the same fixtures +analytically (derived trip, source mask-ceiling, bound >= trip x region, and the +reject matrix). + +Usage: + SYNTH=/path/to/synth python3 scripts/repro/wcet_phase5_778_masked_loop_soundness.py +Requires: pip install unicorn pyelftools +""" +import json +import os +import subprocess +import sys + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +from wcet_phase2_778_unicorn_soundness import ( # noqa: E402 + load_elf, run_func, sidecar_entry, +) + +SYNTH = os.environ.get("SYNTH", "synth") +TMP = "/tmp/wcet_phase5" + +# COUNT-UP masked bound: counter i from 0, exit when i < (param & 7) is false. +# Real trips = param & 7 (<= 7). Worst case param & 7 == 7 → 7 trips. Sum 0..i. +UP_WAT = r""" +(module + (func (export "maskloop") (param i32) (result i32) + (local i32 i32) + (block + (loop + local.get 1 local.get 0 i32.const 7 i32.and i32.lt_s i32.eqz br_if 1 + local.get 2 local.get 1 i32.add local.set 2 + local.get 1 i32.const 1 i32.add local.set 1 + br 0)) + local.get 2)) +""" + +# COUNT-DOWN masked bound: counter starts at 10, decrements, exit when +# counter > (param & 7) is false. Real trips = 10 - (param & 7). WORST case is +# param & 7 == 0 → 10 trips. A NAIVE single-endpoint seed (rhs=7) would derive +# 3 → an UNSOUND bound below the real 10-iteration execution. The both-endpoints +# max derives 10. +DOWN_WAT = r""" +(module + (func (export "cd") (param i32) (result i32) + (local i32 i32) + (local.set 1 (i32.const 10)) + (block + (loop + local.get 1 local.get 0 i32.const 7 i32.and i32.gt_s i32.eqz br_if 1 + local.get 2 i32.const 1 i32.add local.set 2 + local.get 1 i32.const 1 i32.sub local.set 1 + br 0)) + local.get 2)) +""" + +# UNMASKED data-dependent bound (`i < param`): the discriminator negative. No +# mask → no entry-independent ceiling → STAYS declined even with a hint. +UNMASKED_WAT = r""" +(module + (func (export "spin") (param i32) (result i32) + (local i32) + (block + (loop + local.get 1 local.get 0 i32.lt_s i32.eqz br_if 1 + local.get 1 i32.const 1 i32.add local.set 1 + br 0)) + local.get 1)) +""" + + +def wat_file(name, wat): + p = os.path.join(TMP, name + ".wat") + open(p, "w").write(wat) + return p, os.path.join(TMP, name + ".elf") + + +def write_hints(name, fn, bounds): + p = os.path.join(TMP, name + ".hints.json") + json.dump({"schema": "synth-wcet-hints-v1", + "functions": {fn: {"loop_bounds": bounds}}}, open(p, "w")) + return p + + +def compile_wat(wat_path, elf_path, hints=None): + cmd = [SYNTH, "compile", wat_path, "-o", elf_path, "-t", "cortex-m4", "--emit-wcet"] + if hints: + cmd += ["--wcet-hints", hints] + r = subprocess.run(cmd, capture_output=True, text=True, timeout=120) + assert r.returncode == 0, r.stderr + return json.load(open(elf_path + ".wcet.json")) + + +def up_ref(param): + m = param & 7 + return sum(range(m)) # 0+1+..+(m-1) + + +def down_ref(param): + m = param & 7 + return max(0, 10 - m) # counter 10 down to m, counting iterations + + +def loop_src(f): + return f.get("loops", [{}])[0].get("source") + + +def main(): + os.makedirs(TMP, exist_ok=True) + + print("== count-UP masked ceiling: bound >= actual for worst-case input ==") + p, e = wat_file("up", UP_WAT) + hints = write_hints("up", "maskloop", [7]) # ceiling K = 7 + rep = compile_wat(p, e, hints=hints) + f = sidecar_entry(rep, "maskloop") + assert f["status"] == "bounded", f"maskloop: expected bounded, got {f}" + assert loop_src(f) == "mask-ceiling", f"expected mask-ceiling source: {f}" + assert f["loops"][0]["trip_count"] == 7, f"derived trip != 7: {f['loops']}" + bound = f["cycles"] + text, text_addr, syms = load_elf(e) + # WORST case is param & 7 == 7 (max trips). Entry-independence: every input, + # including the OTHER endpoint (param&7==0 → 0 trips), runs within the bound. + for arg in (7, 0xFFFFFFFF, 0x7FFFFFFF, 0, 3, 8): + r0, n = run_func(text, text_addr, syms["maskloop"], (arg,)) + assert r0 == up_ref(arg) & 0xFFFFFFFF, f"maskloop({arg:#x}): r0={r0} != {up_ref(arg)}" + assert bound >= n, ( + f"maskloop({arg:#x}): UNSOUND — masked bound {bound} cyc < {n} executed insns") + print(f" OK maskloop({arg:#x})=r0 {r0}: {n} insns <= bound {bound} cyc") + + print("== count-DOWN masked ceiling: worst case is the OTHER endpoint (rhs=0) ==") + p, e = wat_file("down", DOWN_WAT) + hints = write_hints("down", "cd", [10]) # derived 10 (the rhs=0 endpoint) + rep = compile_wat(p, e, hints=hints) + f = sidecar_entry(rep, "cd") + assert f["status"] == "bounded", f"cd: expected bounded, got {f}" + assert loop_src(f) == "mask-ceiling", f + assert f["loops"][0]["trip_count"] == 10, ( + f"UNSOUND single-endpoint: count-down trip must be 10 (rhs=0), got " + f"{f['loops'][0]['trip_count']} — a naive rhs=7 seed would give 3") + bound = f["cycles"] + text, text_addr, syms = load_elf(e) + for arg in (0, 8, 0xFFFFFFF8, 7, 0xFFFFFFFF, 3): + r0, n = run_func(text, text_addr, syms["cd"], (arg,)) + assert r0 == down_ref(arg) & 0xFFFFFFFF, f"cd({arg:#x}): r0={r0} != {down_ref(arg)}" + assert bound >= n, ( + f"cd({arg:#x}): UNSOUND — masked bound {bound} cyc < {n} executed insns " + f"(count-down worst case is param&7==0 → 10 trips)") + print(f" OK cd({arg:#x})=r0 {r0}: {n} insns <= bound {bound} cyc") + + print("== decline-honesty: the decline MOVED, not deleted ==") + # Unhinted masked loop STAYS declined `loop` (opt-in gate). + p, e = wat_file("up", UP_WAT) + rep = compile_wat(p, e, hints=None) + f = sidecar_entry(rep, "maskloop") + assert f["status"] == "declined" and f["reason"] == "loop", f + print(" OK maskloop unhinted: declined `loop` (masked bound is opt-in)") + + # Too-low hint (< derived 7) REJECTED below-derived. + hints = write_hints("up_low", "maskloop", [3]) + rep = compile_wat(p, e, hints=hints) + f = sidecar_entry(rep, "maskloop") + assert f["status"] == "declined" and f["reason"] == "loop", f + reasons = [r["reason"] for r in f.get("hint_rejections", [])] + assert "hint-below-derived-trip" in reasons, f + print(" OK maskloop + too-low hint(3<7): declined `loop` + hint-below-derived-trip") + + # UNMASKED data-dependent loop STAYS declined even WITH a hint — the mask is + # the discriminator (param is symbolic Top, never Masked). + p, e = wat_file("unmasked", UNMASKED_WAT) + hints = write_hints("unmasked", "spin", [100]) + rep = compile_wat(p, e, hints=hints) + f = sidecar_entry(rep, "spin") + assert f["status"] == "declined" and f["reason"] == "loop", \ + f"UNSOUND — unmasked `i < param` was BOUNDED (no entry-independent ceiling): {f}" + reasons = [r["reason"] for r in f.get("hint_rejections", [])] + assert "hint-unverifiable-induction" in reasons, f + print(" OK spin (unmasked i Date: Wed, 22 Jul 2026 15:57:29 +0200 Subject: [PATCH 3/4] test(#778): phase-5 masked-ceiling gate fixtures + claim pin + CI note MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit wcet_bound_gate.rs: 5 phase-5 fixtures (red-first) — unhinted masked declines `loop`; count-up correct hint bounds (trip 7, source mask-ceiling, 262 cyc); count-DOWN uses both-endpoints (trip 10 not the naive 3, 339 cyc); too-low hint rejected hint-below-derived-trip; UNMASKED i Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 13 ++- claims.yaml | 11 ++ crates/synth-cli/tests/wcet_bound_gate.rs | 124 ++++++++++++++++++++++ 3 files changed, 144 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1cc665e9..8e86ae59 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -51,7 +51,7 @@ jobs: # disk-exhaustion workaround) is gone. The z3-solver feature path is # covered by the dedicated `Z3 Verification` differential job below. run: cargo test --workspace - - name: WCET bound gate (#778 — sound static WCET incl. phase-3/4 recursion) + - name: WCET bound gate (#778 — sound static WCET incl. phase-3/4/5) # The soundness gate for --emit-wcet: bound >= actual on loop-free + # const-loop fixtures, EXACT-literal composed bounds over the direct call # graph (leaf->mid->root; a callee in a proven loop counted trip×), and the @@ -61,9 +61,14 @@ jobs: # single-self-call chain with a VERIFIED depth hint is BOUNDED (derived # depth 15, frame_count 16, 752 cyc); a too-low hint / tree (fib) / uncapped # countdown / mutual recursion STAY declined with the specific machine - # reason (hint-below-derived-depth / hint-unverifiable-recursion). Covered - # by `cargo test --workspace` above; run explicitly so a WCET-soundness - # regression is unmissable in the log. + # reason (hint-below-derived-depth / hint-unverifiable-recursion). Phase 5 + # (#778): a DATA-DEPENDENT masked-ceiling loop bound (`i REL (x & K)`) with a + # VERIFIED loop_bounds hint is BOUNDED (derived trip = both-endpoints max, + # source `mask-ceiling`); the count-DOWN case's worst case is the rhs=0 + # endpoint (a single-endpoint seed would undercount); unhinted / too-low / + # UNMASKED `i < param` STAY declined (`loop` + hint-below-derived-trip / + # hint-unverifiable-induction). Covered by `cargo test --workspace` above; + # run explicitly so a WCET-soundness regression is unmissable in the log. run: cargo test -p synth-cli --test wcet_bound_gate - name: Space-consistency invariant (#77 — execution+memory space) # The #77 checked property: an inconsistent execution/memory-space diff --git a/claims.yaml b/claims.yaml index 33b3ebb0..d3e70105 100644 --- a/claims.yaml +++ b/claims.yaml @@ -639,3 +639,14 @@ claims: pattern: 'let frames = \(cert\.max_depth as u128\)\.saturating_add\(1\);' glob: ['crates/synth-backend/src/wcet_compose.rs'] expect: 1 + # #778 phase 5 — the SOUND-critical masked-ceiling BOTH-ENDPOINTS MAX. For a + # data-dependent masked loop bound `x & K ∈ [0, K]`, the worst-case trip is + # at the `rhs = K` endpoint for a count-UP loop and the `rhs = 0` endpoint + # for a count-DOWN loop. Seeding only ONE endpoint emits a bound BELOW a real + # count-down execution (the fatal class). synth evaluates BOTH endpoints, + # requires BOTH to terminate (the `?` operators), and takes the MAX. Pinning + # this guards against a silent single-endpoint regression that would undercount. + - kind: count-eq + pattern: 'let \(hi, lo\) = \(at\(ceiling\)\?, at\(0\)\?\);' + glob: ['crates/synth-backend/src/wcet_loops.rs'] + expect: 1 diff --git a/crates/synth-cli/tests/wcet_bound_gate.rs b/crates/synth-cli/tests/wcet_bound_gate.rs index 356b6686..cb4c972d 100644 --- a/crates/synth-cli/tests/wcet_bound_gate.rs +++ b/crates/synth-cli/tests/wcet_bound_gate.rs @@ -1126,6 +1126,130 @@ fn conditional_decrement_recursion_rejected_unverifiable() { assert_hint_rejection(&report, "f", "hint-unverifiable-recursion", 15); } +// --------------------------------------------------------------------------- +// #778 phase 5 — DATA-DEPENDENT masked-ceiling loop certificates. +// +// The `loop` decline is CONVERTED for a data-dependent loop whose exit bound is +// a MASKED value `x & K ∈ [0, K]` (entry-independent for ANY runtime `x`). synth +// DERIVES the worst-case trip as the MAX over both endpoints of `[0, K]` +// (`rhs = K` and `rhs = 0`, both required to terminate) — a single endpoint is +// unsound for count-DOWN shapes. Like the equality-exit and recursion-depth +// seams it is HINT-GATED (unhinted → still declines `loop`) and DERIVE-not-trust +// (emitted trip is synth's derived ceiling, source `mask-ceiling`). RED-FIRST: +// the wrong/unmasked rejections are asserted alongside the conversion, and the +// UNMASKED `i < param` shape STILL declines (decline MOVED, not deleted). +// --------------------------------------------------------------------------- + +/// COUNT-UP masked bound: `for i in 0.. while i < (param & 7)`. Real trips = +/// `param & 7 ≤ 7`; worst case (any `x` with `x&7==7`) is 7. Head-test. +const MASK_UP_WAT: &str = r#" + (module + (func (export "maskloop") (param i32) (result i32) + (local i32 i32) + (block + (loop + local.get 1 local.get 0 i32.const 7 i32.and i32.lt_s i32.eqz br_if 1 + local.get 2 local.get 1 i32.add local.set 2 + local.get 1 i32.const 1 i32.add local.set 1 + br 0)) + local.get 2)) +"#; + +/// COUNT-DOWN masked bound: counter 10 decrements while `counter > (param & 7)`. +/// Real trips = `10 - (param & 7)`; WORST case is `param&7 == 0` → 10 trips. The +/// load-bearing soundness fixture: a naive single-endpoint seed (`rhs = 7`) would +/// derive 3 — a bound BELOW the real 10-iteration execution (the fatal class). +/// The both-endpoints max derives 10. +const MASK_DOWN_WAT: &str = r#" + (module + (func (export "cd") (param i32) (result i32) + (local i32 i32) + (local.set 1 (i32.const 10)) + (block + (loop + local.get 1 local.get 0 i32.const 7 i32.and i32.gt_s i32.eqz br_if 1 + local.get 2 i32.const 1 i32.add local.set 2 + local.get 1 i32.const 1 i32.sub local.set 1 + br 0)) + local.get 2)) +"#; + +/// Unhinted, the masked-ceiling shape STAYS declined `loop` — the decline the +/// hint seam converts (asserted so the conversion below is non-vacuous). A bound +/// resting on a data-dependent ceiling is opt-in (mirroring the equality-exit and +/// recursion-depth gates). +#[test] +fn masked_ceiling_loop_unhinted_still_declines() { + let report = compile_wcet(MASK_UP_WAT, "cortex-m4"); + assert_declined(&report, "maskloop", "loop"); +} + +/// GREEN (count-up): a correct hint (7 ≥ synth's DERIVED ceiling 7) converts the +/// `loop` decline into a bound. The emitted trip is synth's DERIVED value (7) +/// with source `mask-ceiling` — never the raw hint. The exact bound literal (262) +/// is pinned; a lowering change fails loud. unicorn ground truth +/// (`wcet_phase5_778_masked_loop_soundness.py`): maskloop(0xFFFFFFFF)=r0 21, 138 +/// executed machine insns ≤ 262 (entry-independent). +#[test] +fn masked_ceiling_count_up_correct_hint_bounds() { + let hints = r#"{"schema":"synth-wcet-hints-v1","functions":{"maskloop":{"loop_bounds":[7]}}}"#; + let report = compile_wcet_hinted(MASK_UP_WAT, "cortex-m4", Some(hints)); + assert_bounded(&report, "maskloop", 262); + assert_loop(&report, "maskloop", 0, 7, "mask-ceiling"); + assert_trip_floor(&report, "maskloop"); +} + +/// GREEN (count-down): the both-endpoints soundness case. The worst-case trip is +/// at the `rhs = 0` endpoint (10 iterations), NOT the naive `rhs = K` endpoint +/// (3). synth derives 10; a single-endpoint seed would have emitted a bound below +/// a real execution. The pinned trip 10 (not 3) is the direct guard against that +/// fatal class. unicorn: cd(0)=r0 10, 180 insns ≤ 339. +#[test] +fn masked_ceiling_count_down_uses_both_endpoints() { + let hints = r#"{"schema":"synth-wcet-hints-v1","functions":{"cd":{"loop_bounds":[10]}}}"#; + let report = compile_wcet_hinted(MASK_DOWN_WAT, "cortex-m4", Some(hints)); + assert_bounded(&report, "cd", 339); + assert_loop(&report, "cd", 0, 10, "mask-ceiling"); + assert_trip_floor(&report, "cd"); +} + +/// RED: a too-LOW hint (3 < synth's derived ceiling 7) is REJECTED +/// `hint-below-derived-trip` and the function STAYS declined — a wrong oracle +/// claim never becomes a bound. +#[test] +fn masked_ceiling_too_low_hint_rejected_red_first() { + let hints = r#"{"schema":"synth-wcet-hints-v1","functions":{"maskloop":{"loop_bounds":[3]}}}"#; + let report = compile_wcet_hinted(MASK_UP_WAT, "cortex-m4", Some(hints)); + assert_declined(&report, "maskloop", "loop"); + assert_hint_rejection(&report, "maskloop", "hint-below-derived-trip", 3); +} + +/// DECLINE-HONESTY (the decline MOVED, not deleted): an UNMASKED data-dependent +/// bound (`i < param`, no mask) has NO entry-independent ceiling. Even WITH a +/// hint it STAYS declined `loop` with `hint-unverifiable-induction`. The mask is +/// the sole discriminator (`param` is symbolic Top, never a masked ceiling); this +/// is exactly `data_dependent_hint_is_rejected_unverifiable` above — asserting it +/// here proves phase 5 MOVED the decline onto the masked shape rather than +/// WIDENING acceptance to every runtime bound. +#[test] +fn unmasked_data_dependent_loop_stays_declined_with_hint() { + let wat = r#" + (module + (func (export "spin") (param i32) (result i32) + (local i32) + (block + (loop + local.get 1 local.get 0 i32.lt_s i32.eqz br_if 1 + local.get 1 i32.const 1 i32.add local.set 1 + br 0)) + local.get 1)) + "#; + let hints = r#"{"schema":"synth-wcet-hints-v1","functions":{"spin":{"loop_bounds":[100]}}}"#; + let report = compile_wcet_hinted(wat, "cortex-m4", Some(hints)); + assert_declined(&report, "spin", "loop"); + assert_hint_rejection(&report, "spin", "hint-unverifiable-induction", 100); +} + /// Assert `name` carries a hint rejection with EXACTLY `reason` and `hint`. fn assert_hint_rejection(report: &Value, name: &str, reason: &str, hint: u64) { let f = func(report, name); From 61837139270931dd730851444022f987073b5e22 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 22 Jul 2026 15:58:50 +0200 Subject: [PATCH 4/4] docs(#778): CLAUDE.md Track D + CHANGELOG phase-5 masked-ceiling loops Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CHANGELOG.md | 16 ++++++++++++++++ CLAUDE.md | 20 ++++++++++++++++++-- 2 files changed, 34 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0d19e5c6..a2b11016 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,22 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +### Added + +- **WCET phase 5 (#778) — data-dependent masked-ceiling loop certificates.** The + `--wcet-hints` scry seam now bounds a DATA-DEPENDENT loop whose exit bound is a + masked value `i REL (x & K)`. Because `x & K ∈ [0, K]` for ANY runtime `x` + (`Sym::Masked`, mask sign-bit clear), synth DERIVES the worst-case trip as the + MAX over both endpoints of `[0, K]` — a single endpoint would undercount a + count-DOWN loop (the fatal class). Hint-gated + derive-not-trust like the + equality-exit and recursion-depth seams (new source `mask-ceiling`). The decline + MOVED, not deleted: an unhinted masked loop still declines `loop`; a too-low hint + rejects `hint-below-derived-trip`; an UNMASKED `i < param` still declines + `hint-unverifiable-induction` (the mask is the sole discriminator). Frozen-safe + (WCET reads the final stream; `.text` byte-identical). New unicorn cross-check + `wcet_phase5_778_masked_loop_soundness.py` (count-down `cd(0)`: 180 insns ≤ 339 + cyc); the both-endpoints max is pinned in `claims.yaml`. + ## [0.49.0] - 2026-07-17 **"Phase-2 frontier + falcon to zero" — the verified allocation validator went diff --git a/CLAUDE.md b/CLAUDE.md index 3c4c0473..0aebbee1 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -222,8 +222,24 @@ frozen and oracle-gated every step: exact-literal chain + recursion/indirect decline honesty + masked-recursion accept/reject) and the `wcet_phase4_49_recursion_soundness.py` unicorn cross- check (`md(0xFFFFFFFF)` executes 267 insns across all 16 frames ≤ 752 cyc, - entry-independent). Richer recursion certificates (clamp-bounded controlling - values, data-dependent depths, scry) are a named follow-up. + entry-independent). Phase 5 (#778): DATA-DEPENDENT masked-ceiling LOOP + certificates (`wcet_loops.rs`) — the scry seam extended past const-trip to a + loop whose exit bound is a MASKED value `i REL (x & K)`. `x & K ∈ [0, K]` for + ANY runtime `x` (`Sym::Masked`, mask sign-bit clear; base identity irrelevant), + so synth DERIVES the worst-case trip as the MAX over BOTH endpoints of `[0, K]` + (`rhs = K` and `rhs = 0`, both required to terminate — a single endpoint would + undercount a count-DOWN loop, the fatal class; the both-endpoints max is pinned + in `claims.yaml`). Like the equality-exit and recursion-depth seams it is + HINT-GATED (unhinted masked loop still declines `loop`) and DERIVE-not-trust + (emitted trip is synth's derived ceiling, source `mask-ceiling`); a too-low hint + → `hint-below-derived-trip`; an UNMASKED `i < param` (no entry-independent + ceiling) still LOUD-DECLINES `loop` + `hint-unverifiable-induction` (the mask is + the sole discriminator — the decline MOVED onto the masked shape, not widened to + every runtime bound). Gated by `wcet_bound_gate.rs` (count-up/-down accept + + unhinted/too-low/unmasked reject) and the `wcet_phase5_778_masked_loop_soundness.py` + unicorn cross-check (count-down `cd(0)` executes 180 insns ≤ 339 cyc). Richer + certificates (clamp-bounded controlling values, data-dependent recursion depths, + scry) are a named follow-up. - **Gate `VCR-VER-001`:** DEMONSTRATED (implemented, evidence in `scripts/repro/vcr_ver_001_gate.md`) — the v0.11.20 reciprocal-mult cost-gate was deleted outright (PR #322, differential bit-identical); the