diff --git a/artifacts/design.yaml b/artifacts/design.yaml index 0e64ad6..9ea88cf 100644 --- a/artifacts/design.yaml +++ b/artifacts/design.yaml @@ -664,3 +664,125 @@ 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. + 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: > + 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 + 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));