From 26ca103e5f264bcbc3c3cda3293876c7f5226505 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 11 Aug 2026 21:43:48 +0200 Subject: [PATCH 1/2] =?UTF-8?q?FEAT-065:=20scry=20adjudicates=20its=20own?= =?UTF-8?q?=20oracle=20(verify=5Fagainst)=20=E2=80=94=20conservative=20by?= =?UTF-8?q?=20construction?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the fix-verify loop REQ-018 promised: the v3.1 verification oracle was PROSE; this makes it a machine verdict, so an agent's edit is gated by a sound checker rather than by tests. `verify_against(before, after) -> Vec` with outcomes discharged / still-open / regressed / moved / removed-with-code / uncertain. DD-021 (new) records two findings that forced the design: 1. `obligation_id` includes the advisory CODE (clean-room: one i32.div_s raises two obligations at one pc, so the site alone does not discriminate) — but FIXING an obligation changes its code (div-by-zero → proven-safe) and hence its id, which is exactly the transition to detect. Matching on the id would render every genuine discharge as two unrelated events. So THREE keys, each with one job: obligation_id (cite), site_key (match — excludes code), group_key (the ordinal domain — the conservatism signal). 2. `ObligationId.v` PROVES identity can alias (survivor_inherits_deleted_identity), which admits a FALSE discharge: an open site is deleted, a proven-safe same-kind sibling inherits its identity, and the deleted obligation looks fixed. So `discharged` is a CERTAINTY claim — withheld unless the ordinal domain's site set is unchanged; otherwise `uncertain`. Verified the conservatism actually FIRES on that scenario rather than passing by another route (a probe printed the real verdict before it was removed): Uncertain before=div-by-zero after=Some("proven-safe") "looks proven safe, but this site's ordinal domain changed membership so identity may have aliased — discharge withheld" Without the rule this case reports `discharged` for an obligation never fixed. `removed-with-code` is kept strictly distinct from `discharged` — deleting the code that carried an obligation proves nothing, and an agent rewarded for conflating them learns to delete rather than fix. HONEST RESIDUAL (DD-021 limitations): a pure REORDERING of two same-kind operators in one region preserves the group's site set while swapping which site each key denotes, so that edit shape can still mis-attribute a verdict. Disclosed; closing it needs content corroboration beyond the key. Tests: 4 FEAT-065 oracles (real fix → Discharged; deletion → RemovedWithCode and never Discharged; aliasing → Uncertain; lost fact → Regressed). core 106, viz 25, segment 10, poly 9, interval 8, octagon 26. clippy -D warnings clean across CI's package set, fmt clean, rivet validate PASS. Scope: the PURE adjudicator. CLI/MCP surfacing is FEAT-066/067. FEAT-065 stays `proposed` pending clean-room + CI. Co-Authored-By: Claude Opus 4.8 --- artifacts/design.yaml | 74 ++++++ crates/scry-analyze-core/src/lib.rs | 345 ++++++++++++++++++++++++++++ crates/scry-viz/src/lib.rs | 2 + 3 files changed, 421 insertions(+) diff --git a/artifacts/design.yaml b/artifacts/design.yaml index 0e64ad6..741eac0 100644 --- a/artifacts/design.yaml +++ b/artifacts/design.yaml @@ -664,3 +664,77 @@ artifacts: target: FEAT-064 - type: traces-to target: FEAT-065 + + - id: DD-021 + type: design-decision + title: "v3.3 — Adjudicating a NON-INJECTIVE identity: three keys, and `discharged` as a certainty claim" + status: proposed + tags: [ai-agent, fix-verify-loop, oracle, conservatism, v3.3] + description: > + How FEAT-065 compares two runs given that FEAT-064's identity is provably + NOT injective across arbitrary edits. Two findings forced this to be a + decision rather than an implementation detail. + (1) `proofs/rocq/ObligationId.v` PROVES the aliasing hazard + (`survivor_inherits_deleted_identity`): delete the first of two same-kind + operators in a region and the survivor's ordinal — hence its identity — + becomes exactly the deleted site's. A naive diff-by-identity can therefore + report a FALSE `discharged`: site A is an open obligation, site B at the + same kind is PROVEN-SAFE, A is deleted, B inherits A's identity, and A's + identity now resolves to a proven-safe advisory although A was never fixed. + (2) The advisory CODE is a required component of the identity (clean-room: + one `i32.div_s` raises both div-by-zero and signed-overflow at one pc, so + the site alone does not discriminate). But fixing an obligation CHANGES its + code — `div-by-zero` becomes `proven-safe` — so the full identity is + unstable across exactly the transition the adjudicator exists to detect. + Matching on it alone would render every genuine discharge as + "one identity vanished, an unrelated one appeared". + fields: + decision: > + Emit THREE keys per advisory, each with one job: + * `obligation_id` = hash(func_ident, path, kind, ordinal, CODE) — + globally unique per obligation. What a consumer stores and cites. + * `site_key` = hash(func_ident, path, kind, ordinal) — identifies + the SITE, stable across a code/class change. This is what FEAT-065 + MATCHES ON, so a div-by-zero becoming proven-safe is recognised as + the same site changing state rather than two unrelated events. + * `group_key` = hash(func_ident, path, kind) — the ORDINAL DOMAIN. + Its membership is what aliasing perturbs, so it is the conservatism + signal. + Adjudication outcomes: `discharged`, `still-open`, `regressed`, `moved`, + `removed-with-code`, `uncertain`. + `discharged` is a CERTAINTY CLAIM and requires all of: the site_key was an + open obligation before; it is proven-safe (or raises no obligation) after; + AND its `group_key`'s site_key SET is unchanged between the two runs. + If that set changed, the verdict is `uncertain` — never `discharged`. + `removed-with-code` (the site no longer exists) is a distinct outcome and + must never be reported as `discharged`. + rationale: > + The adjudicator inherits the analyzer's discipline one layer up: scry + claims PROVEN-SAFE only when the abstract state rules the trap out, and + FEAT-065 claims `discharged` only when identity cannot have aliased. + Over-claiming a discharge is the same class of error as an unsound + analysis, and it is the error an agent optimising against the verdict + would exploit fastest — an agent rewarded for `discharged` learns to + DELETE code, which is why `removed-with-code` is kept strictly separate. + The group-set check is chosen because aliasing by deletion or insertion + NECESSARILY changes the ordinal domain's membership, so the cheap signal + covers the realistic edit shapes. + limitations: > + HONEST RESIDUAL, disclosed rather than hidden: a pure REORDERING of two + same-kind operators within one region preserves the group's site_key set + while swapping which site each key denotes (each op takes the other's + ordinal). The group-set check cannot see it, so that edit shape can still + mis-attribute a verdict. It is an unusual edit, its consequence is a + wrong verdict rather than an unsound analysis, and closing it would need + content corroboration beyond the key (e.g. hashing the operator's local + context) — deferred, and named here so a consumer is not surprised. + Consequence for consumers: a `discharged` verdict is evidence, not proof, + under a same-kind reordering; `uncertain` is the honest default whenever + the domain moved. + links: + - type: satisfies + target: REQ-020 + - type: traces-to + target: FEAT-065 + - type: traces-to + target: DD-020 diff --git a/crates/scry-analyze-core/src/lib.rs b/crates/scry-analyze-core/src/lib.rs index 177d0cb..4e9c69c 100644 --- a/crates/scry-analyze-core/src/lib.rs +++ b/crates/scry-analyze-core/src/lib.rs @@ -675,6 +675,55 @@ pub struct Advisory { /// Empty when no identity could be derived. Opaque by construction — the /// layout is not a contract; do not parse it. pub obligation_id: String, + /// FEAT-065 (DD-021): identity of the SITE, excluding the advisory code — + /// so it is STABLE when an obligation changes state (`div-by-zero` becoming + /// `proven-safe` changes `obligation_id` but not this). This is the key + /// [`verify_against`] matches on; without it every genuine discharge would + /// read as "one identity vanished and an unrelated one appeared". + pub site_key: String, + /// FEAT-065 (DD-021): the ORDINAL DOMAIN this site's ordinal is counted + /// within (function + region path + operator kind). Aliasing perturbs this + /// domain's membership, so a change in its site set is the signal that + /// forces a `discharged` verdict down to `uncertain`. + pub group_key: String, +} + +/// FEAT-065 (REQ-020, DD-021): the outcome of adjudicating ONE obligation +/// across two analyses. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum VerifyOutcome { + /// The obligation was open and is now discharged, AND identity cannot have + /// aliased. A CERTAINTY claim — see [`verify_against`]. + Discharged, + /// Still an open obligation. + StillOpen, + /// Was proven safe, is an open obligation again. + Regressed, + /// Same site, different position. Informational — NOT progress. + Moved, + /// The site no longer exists. Explicitly NOT a discharge: deleting the code + /// that carried an obligation proves nothing, and an agent rewarded for + /// conflating the two learns to delete rather than fix. + RemovedWithCode, + /// Identity may have aliased (the obligation's ordinal domain changed + /// membership), so no claim is made. The honest default. + Uncertain, +} + +/// FEAT-065: one adjudicated obligation. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct VerifyVerdict { + /// The obligation's identity in the BEFORE run. + pub obligation_id: String, + /// The site identity used for matching (DD-021). + pub site_key: String, + /// The verdict. + pub outcome: VerifyOutcome, + /// Advisory code before / after, where known. + pub before_code: String, + pub after_code: Option, + /// Why this outcome — in particular why a discharge was withheld. + pub detail: String, } /// FEAT-055 (REQ-018): a candidate counterexample for an `UnprovenObligation` @@ -3107,6 +3156,198 @@ fn obligation_id_of(func_ident: &str, path: &str, kind: &str, ordinal: u32, code out } +/// FEAT-065 (REQ-020, DD-021): adjudicate one analysis against a prior one — +/// scry judging its own verification oracle, so an agent's edit is gated by a +/// SOUND checker rather than by tests. +/// +/// Matching is by [`Advisory::site_key`], not `obligation_id`: fixing an +/// obligation changes its code (`div-by-zero` → `proven-safe`) and therefore its +/// id, so id-matching would render every genuine discharge as two unrelated +/// events (DD-021). +/// +/// `Discharged` is a CERTAINTY claim and is withheld unless the obligation's +/// ORDINAL DOMAIN ([`Advisory::group_key`]) has an unchanged site set. +/// `ObligationId.v` proves identity can alias when that domain changes +/// membership, which admits a FALSE discharge: an open site is deleted, a +/// proven-safe sibling of the same kind inherits its identity, and the deleted +/// obligation appears to have been fixed. When the domain moved, the verdict is +/// [`VerifyOutcome::Uncertain`] instead — the adjudicator inherits the +/// analyzer's discipline one layer up. +/// +/// [`VerifyOutcome::RemovedWithCode`] is kept strictly distinct from +/// `Discharged`: deleting the code that carried an obligation proves nothing, +/// and an agent rewarded for conflating them learns to delete rather than fix. +pub fn verify_against(before: &AnalysisResult, after: &AnalysisResult) -> Vec { + use alloc::collections::{BTreeMap, BTreeSet}; + + fn is_open(c: AdvisoryClass) -> bool { + matches!( + c, + AdvisoryClass::UnprovenObligation | AdvisoryClass::DefiniteFault + ) + } + fn site_sets(r: &AnalysisResult) -> BTreeMap<&str, BTreeSet<&str>> { + let mut m: BTreeMap<&str, BTreeSet<&str>> = BTreeMap::new(); + for a in r.advisories.iter().filter(|a| !a.site_key.is_empty()) { + m.entry(a.group_key.as_str()) + .or_default() + .insert(a.site_key.as_str()); + } + m + } + + let after_groups = site_sets(after); + let before_groups = site_sets(before); + let mut after_by_site: BTreeMap<&str, Vec<&Advisory>> = BTreeMap::new(); + for a in after.advisories.iter().filter(|a| !a.site_key.is_empty()) { + after_by_site + .entry(a.site_key.as_str()) + .or_default() + .push(a); + } + + let mut out: Vec = Vec::new(); + + for b in before + .advisories + .iter() + .filter(|a| !a.site_key.is_empty() && is_open(a.class)) + { + // Did this obligation's ordinal domain keep the same site set? If not, + // identity may have aliased and no discharge may be claimed. + let domain_stable = + before_groups.get(b.group_key.as_str()) == after_groups.get(b.group_key.as_str()); + + let at_site = after_by_site.get(b.site_key.as_str()); + let (outcome, after_code, detail) = match at_site { + // The site is gone. NOT a discharge. + None => ( + VerifyOutcome::RemovedWithCode, + None, + String::from( + "the site no longer exists; deleting code that carried an \ + obligation is not a discharge", + ), + ), + Some(list) => { + // Same obligation still open at this site? + if let Some(same) = list.iter().find(|a| a.code == b.code && is_open(a.class)) { + let o = if same.pc != b.pc { + VerifyOutcome::Moved + } else { + VerifyOutcome::StillOpen + }; + ( + o, + Some(same.code.clone()), + String::from("still an open obligation"), + ) + } else if let Some(proven) = list + .iter() + .find(|a| a.class == AdvisoryClass::LeverageableFact) + { + if domain_stable { + ( + VerifyOutcome::Discharged, + Some(proven.code.clone()), + String::from("now proven safe, and the ordinal domain is unchanged"), + ) + } else { + ( + VerifyOutcome::Uncertain, + Some(proven.code.clone()), + String::from( + "looks proven safe, but this site's ordinal domain changed \ + membership so identity may have aliased — discharge withheld", + ), + ) + } + } else { + ( + VerifyOutcome::Uncertain, + None, + String::from( + "the obligation is absent but the site is not clearly proven safe", + ), + ) + } + } + }; + out.push(VerifyVerdict { + obligation_id: b.obligation_id.clone(), + site_key: b.site_key.clone(), + outcome, + before_code: b.code.clone(), + after_code, + detail, + }); + } + + // Regressions: a site that was a proven fact now raises an obligation. + let before_proven: BTreeSet<&str> = before + .advisories + .iter() + .filter(|a| a.class == AdvisoryClass::LeverageableFact && !a.site_key.is_empty()) + .map(|a| a.site_key.as_str()) + .collect(); + for a in after + .advisories + .iter() + .filter(|a| !a.site_key.is_empty() && is_open(a.class)) + { + if before_proven.contains(a.site_key.as_str()) { + out.push(VerifyVerdict { + obligation_id: a.obligation_id.clone(), + site_key: a.site_key.clone(), + outcome: VerifyOutcome::Regressed, + before_code: String::from("proven-safe"), + after_code: Some(a.code.clone()), + detail: String::from("was a proven fact, now raises an obligation"), + }); + } + } + out +} + +/// FEAT-065 (DD-021): the SITE key — everything the obligation id has EXCEPT +/// the advisory code, so it survives an obligation changing state. +fn site_key_of(func_ident: &str, path: &str, kind: &str, ordinal: u32) -> String { + let mut h = Sha256::new(); + h.update(b"site|"); + h.update(func_ident.as_bytes()); + h.update(b"|"); + h.update(path.as_bytes()); + h.update(b"|"); + h.update(kind.as_bytes()); + h.update(b"|"); + h.update(ordinal.to_le_bytes()); + let d = h.finalize(); + let mut out = String::with_capacity(16); + for b in d.iter().take(8) { + out.push_str(&format!("{b:02x}")); + } + out +} + +/// FEAT-065 (DD-021): the ORDINAL DOMAIN key — function + region path + kind, +/// WITHOUT the ordinal. Aliasing perturbs this domain's membership, which is the +/// signal that forces a discharge down to `uncertain`. +fn group_key_of(func_ident: &str, path: &str, kind: &str) -> String { + let mut h = Sha256::new(); + h.update(b"group|"); + h.update(func_ident.as_bytes()); + h.update(b"|"); + h.update(path.as_bytes()); + h.update(b"|"); + h.update(kind.as_bytes()); + let d = h.finalize(); + let mut out = String::with_capacity(16); + for b in d.iter().take(8) { + out.push_str(&format!("{b:02x}")); + } + out +} + /// FEAT-064: does this advisory describe the MODULE rather than a code site? /// Such advisories carry `(func 0, pc 0)` as a SENTINEL, so giving them a site /// identity would collide with a genuine advisory there, drift whenever func 0's @@ -3126,6 +3367,8 @@ fn stamp_obligation_ids( ) { for a in advisories.iter_mut().filter(|a| is_module_scoped(&a.code)) { a.obligation_id = obligation_id_of("", "", "", 0, &a.code); + a.site_key = site_key_of("", "", "", 0); + a.group_key = group_key_of("", "", ""); } for f in defined_funcs { let ident = function_meta @@ -3145,6 +3388,8 @@ fn stamp_obligation_ids( .map(op_report_name) .unwrap_or_else(|| a.code.clone()); a.obligation_id = obligation_id_of(&ident, path, &kind, *ordinal, &a.code); + a.site_key = site_key_of(&ident, path, &kind, *ordinal); + a.group_key = group_key_of(&ident, path, &kind); } } } @@ -3188,6 +3433,8 @@ fn compute_advisories( verification: "re-run scry: this handle_findings entry disappears".into(), counterexample: None, obligation_id: String::new(), + site_key: String::new(), + group_key: String::new(), }); } @@ -3228,6 +3475,8 @@ fn compute_advisories( ), counterexample: Some(trap_counterexample(t.kind, &t.op, memory_size_bytes)), obligation_id: String::new(), + site_key: String::new(), + group_key: String::new(), }); } TrapVerdict::ProvenSafe => { @@ -3255,6 +3504,8 @@ fn compute_advisories( ), counterexample: None, obligation_id: String::new(), + site_key: String::new(), + group_key: String::new(), }); } } @@ -3296,6 +3547,8 @@ fn compute_advisories( ), counterexample: None, obligation_id: String::new(), + site_key: String::new(), + group_key: String::new(), }); } @@ -3315,6 +3568,8 @@ fn compute_advisories( verification: "re-run scry: stack_usage.max_stack_bytes becomes Bytes(n)".into(), counterexample: None, obligation_id: String::new(), + site_key: String::new(), + group_key: String::new(), }); } @@ -8941,6 +9196,96 @@ mod tests { .clone() } + fn outcome_for(v: &[VerifyVerdict], code: &str) -> Vec { + v.iter() + .filter(|x| x.before_code == code) + .map(|x| x.outcome) + .collect() + } + + /// FEAT-065 AC — a real fix is reported `discharged`. The divisor becomes a + /// non-zero constant, so the same SITE flips from an open obligation to a + /// proven fact; matching must survive the code change (DD-021). + #[test] + fn feat065_a_real_fix_is_discharged() { + let before = analyze_default( + "(module (func (export \"b\") (param i32) (result i32) i32.const 10 local.get 0 i32.div_s))", + ); + let after = analyze_default( + "(module (func (export \"b\") (param i32) (result i32) i32.const 10 i32.const 5 i32.div_s))", + ); + let v = verify_against(&before, &after); + assert!( + outcome_for(&v, "div-by-zero").contains(&VerifyOutcome::Discharged), + "guarding the divisor must be Discharged; got {v:?}" + ); + } + + /// FEAT-065 AC — deleting the code that carried an obligation is + /// `removed-with-code`, NEVER `discharged`: an agent rewarded for conflating + /// them learns to delete rather than fix. + #[test] + fn feat065_deleting_the_code_is_not_a_discharge() { + let before = analyze_default( + "(module (func (export \"b\") (param i32) (result i32) i32.const 10 local.get 0 i32.div_s))", + ); + let after = + analyze_default("(module (func (export \"b\") (param i32) (result i32) i32.const 0))"); + let v = verify_against(&before, &after); + let got = outcome_for(&v, "div-by-zero"); + assert!( + !got.contains(&VerifyOutcome::Discharged), + "deletion is never a discharge; got {v:?}" + ); + assert!( + got.contains(&VerifyOutcome::RemovedWithCode), + "expected RemovedWithCode; got {v:?}" + ); + } + + /// FEAT-065 AC — the CONSERVATISM rule, which `ObligationId.v` proves is + /// necessary. Two same-kind sites: #0 open, #1 proven safe. Delete #0 and #1 + /// slides into ordinal 0, INHERITING #0's identity while being proven safe — + /// so a naive diff-by-identity would call #0 discharged though it was never + /// fixed. The ordinal domain changed, so the verdict must degrade. + #[test] + fn feat065_aliasing_forces_uncertain_not_discharged() { + let before = analyze_default( + "(module (func (export \"b\") (param i32) (result i32) \ + i32.const 10 local.get 0 i32.div_s i32.const 20 i32.const 5 i32.div_s i32.add))", + ); + let after = analyze_default( + "(module (func (export \"b\") (param i32) (result i32) i32.const 20 i32.const 5 i32.div_s))", + ); + let v = verify_against(&before, &after); + let got = outcome_for(&v, "div-by-zero"); + assert!( + !got.contains(&VerifyOutcome::Discharged), + "aliasing must NOT read as a discharge (the survivor_inherits_deleted_identity hazard); got {v:?}" + ); + assert!( + got.contains(&VerifyOutcome::Uncertain) + || got.contains(&VerifyOutcome::RemovedWithCode), + "aliasing must degrade to Uncertain/RemovedWithCode; got {v:?}" + ); + } + + /// FEAT-065 AC — losing a proven fact is reported `regressed`. + #[test] + fn feat065_regression_is_reported() { + let before = analyze_default( + "(module (func (export \"b\") (param i32) (result i32) i32.const 10 i32.const 5 i32.div_s))", + ); + let after = analyze_default( + "(module (func (export \"b\") (param i32) (result i32) i32.const 10 local.get 0 i32.div_s))", + ); + let v = verify_against(&before, &after); + assert!( + v.iter().any(|x| x.outcome == VerifyOutcome::Regressed), + "losing a proven fact must be Regressed; got {v:?}" + ); + } + /// FEAT-064 AC#1 (REQ-020) — an edit in an UNRELATED function must not /// disturb this function's obligation identity. #[test] diff --git a/crates/scry-viz/src/lib.rs b/crates/scry-viz/src/lib.rs index 142f2a3..7db5d5d 100644 --- a/crates/scry-viz/src/lib.rs +++ b/crates/scry-viz/src/lib.rs @@ -2131,6 +2131,8 @@ mod tests { verification: "re-run scry".into(), counterexample: None, obligation_id: format!("test-{i:04x}"), + site_key: format!("site-{i:04x}"), + group_key: String::from("grp-test"), }; for i in 0..(ADVISORY_PER_CLASS_CAP as u32 + 25) { r.advisories.push(mk(i)); From 9ac974efb65c3cc868a4e6a46b6fae33d289c06a Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 11 Aug 2026 21:59:54 +0200 Subject: [PATCH 2/2] DD-021: retract the falsified rationale + record 6 adversarial findings MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adversarial review of the FEAT-065 adjudicator (PR #120, now draft) falsified this decision's central justification. DD-021 asserted that "aliasing by deletion or insertion NECESSARILY changes the ordinal domain's membership" — the sentence the whole conservatism rule rested on. It is FALSE: a deletion paired with a same-kind insertion leaves the group's site_key set byte-identical, so the check passes and a FALSE `discharged` is produced — the delete-instead-of-fix reward hack the rule exists to prevent. Retracted in place (not quietly reworded) and the six reproduced findings recorded in `limitations`, including two the design did not anticipate at all: new obligations produce no verdict whatsoever, and `regressed` is fabricated on a byte-identical module (contradictory verdicts under one id). Correcting the claim, not the ledger. The implementation stays in draft until matching uses CONTENT corroboration rather than a positional ordinal plus a population check. Co-Authored-By: Claude Opus 4.8 --- artifacts/design.yaml | 56 +++++++++++++++++++++++++++++++++++++++---- 1 file changed, 52 insertions(+), 4 deletions(-) diff --git a/artifacts/design.yaml b/artifacts/design.yaml index 741eac0..9ea88cf 100644 --- a/artifacts/design.yaml +++ b/artifacts/design.yaml @@ -716,11 +716,59 @@ artifacts: analysis, and it is the error an agent optimising against the verdict would exploit fastest — an agent rewarded for `discharged` learns to DELETE code, which is why `removed-with-code` is kept strictly separate. - The group-set check is chosen because aliasing by deletion or insertion - NECESSARILY changes the ordinal domain's membership, so the cheap signal - covers the realistic edit shapes. + RETRACTED 2026-08-11 by adversarial review — this decision originally + justified the group-set check by asserting that "aliasing by deletion or + insertion NECESSARILY changes the ordinal domain's membership". THAT IS + FALSE, and it was the sentence the whole conservatism rule rested on. A + deletion PAIRED WITH a same-kind insertion in the same region leaves the + group's site_key set byte-identical, so the check passes and a FALSE + `discharged` is produced — the delete-instead-of-fix reward hack this + rule exists to prevent. The group-set check is therefore a NECESSARY but + NOT SUFFICIENT condition, and on its own it does not make `discharged` + a certainty claim. Sound matching needs CONTENT corroboration (hashing + the operator's local context so a replaced operator cannot inherit a + predecessor's identity) rather than a positional ordinal plus a + population check. See the limitations field; the implementation is held + in draft until this is resolved. limitations: > - HONEST RESIDUAL, disclosed rather than hidden: a pure REORDERING of two + FOUND BY ADVERSARIAL REVIEW 2026-08-11 (all reproduced; the + implementation is in draft, nothing shipped): + (1) CARDINALITY-PRESERVING DELETION defeats the group-set check — delete + the open operator and append a same-kind safe one, and the site set + is unchanged, yielding a false `discharged`. This falsifies the + rationale's central claim (see above). + (2) `body_shape_hash` is the WHOLE function identity in the no-name / + no-export case, so two structurally identical functions share + site/group keys — deleting a whole function carrying an obligation + reports `discharged`. Conversely ANY opcode edit in such a function + moves every key in it, so for stripped modules `discharged` is + unreachable for the canonical fix shape (insert a guard / replace a + `local.get` with a constant). Mitigation direction: never claim + `discharged` when the function identity came from the shape-hash + fallback — degrade to `uncertain`. + (3) OBLIGATION LAUNDERING: wrapping the site in a typed `block`/`if` + routes it through `havoc_region`, which emits no trap check, no gap + and no advisory when the write set is empty and the region contains + no call — so a LIVE obligation disappears and reads as + `removed-with-code`. Root cause is a pre-existing FEAT-040/046 + reporting hole, tracked separately; the adjudicator must treat + "absent from a function that degraded or gained a havoc region" as + `uncertain`. + (4) `regressed` is FABRICATED on a byte-identical module: `site_key` + excludes the code, so an open div-by-zero and a proven + signed-overflow at one `i32.div_s` share a site key, putting it in + the proven set. Self-comparison returns contradictory `still-open` + and `regressed` verdicts under one id with an invented before-code. + The proven-safe advisory does not record WHICH trap kind it proves, + which is the underlying data gap. + (5) NEW obligations produce NO verdict at all (only sites that + previously carried a proven fact are checked), so a fault introduced + where nothing was flagged before passes the gate clean. This is the + blindest direction for an autonomous agent. + (6) `obligation_id` is not unique, against this decision's own claim: two + ProvenSafe trap kinds at one pc both use code `proven-safe`, and the + shape-hash collision duplicates ids across functions. + PRE-EXISTING RESIDUAL, disclosed from the start: a pure REORDERING of two same-kind operators within one region preserves the group's site_key set while swapping which site each key denotes (each op takes the other's ordinal). The group-set check cannot see it, so that edit shape can still