Skip to content

verify-1.6.0-done: the parity verdict judges every owed cell, not one; ledger sync keeps a gone scope with open findings (L-R23) (stacked on #918) #950

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
MattJackson merged 1 commit into from
Oct 15, 2026
Merged

verify-1.6.0-done: the parity verdict judges every owed cell, not one; ledger sync keeps a gone scope with open findings (L-R23) (stacked on #918) #950

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
84 changes: 70 additions & 14 deletions scripts/verify-1.6.0-done.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -582,6 +582,18 @@ print(d)
' "$1" "$2"
}

# How many cells a cells.json carries (its `cells` array). Non-zero rc when it cannot be read.
json_cell_count() { # $1 = cells.json
command -v python3 >/dev/null 2>&1 || { echo "python3 is not on PATH" >&2; return 2; }
python3 -c '
import json, sys
try:
print(len(json.load(open(sys.argv[1]))["cells"]))
except Exception as e:
sys.stderr.write("unreadable cells.json %s: %s\n" % (sys.argv[1], e)); sys.exit(2)
' "$1"
}

# The path the build named must be a real, executable, NON-SYMLINK file. The symlink arm is not
# tidiness: a stray link at the recorder's path is exactly how a foreign build got in front of this
# instrument on this checkout, and it is the one shape that satisfies `-x` while pointing at another
Expand Down Expand Up @@ -644,8 +656,8 @@ assert_golden_is_pinned() { # $1 = golden recording dir ; $2 = the committed di

# The verdict, taken from the report the differ wrote rather than from its exit status, and printed
# with the scope attached so a green can never be read as more than it is.
assert_parity_verdict() { # $1 = report dir
local rep="${1:-}" owed diverging accepted unbaselined scope
assert_parity_verdict() { # $1 = report dir ; $2 = owed-baseline.txt ; $3 = cells.json
local rep="${1:-}" base="${2:-}" cells="${3:-}" owed diverging accepted unbaselined scope want_owed want_scope
if ! owed="$(json_field "$rep/report.json" totals.owed 2>/dev/null)"; then
echo "no readable report at $rep/report.json — the replay left no verdict to read, so there is none"; return 1
fi
Expand All @@ -655,12 +667,42 @@ assert_parity_verdict() { # $1 = report dir
scope="$(json_field "$rep/report.json" totals.cells_in_scope 2>/dev/null)" || return 1
case "$owed" in ''|*[!0-9]*) echo "totals.owed is not a count ('$owed')"; return 1 ;; esac
case "$diverging" in ''|*[!0-9]*) echo "totals.diverging is not a count ('$diverging')"; return 1 ;; esac
case "$unbaselined" in ''|*[!0-9]*) echo "totals.unbaselined is not a count ('$unbaselined')"; return 1 ;; esac
case "$scope" in ''|*[!0-9]*) echo "totals.cells_in_scope is not a count ('$scope')"; return 1 ;; esac
echo "compared $owed owed cell(s) of a $scope-cell corpus: $diverging diverging, $accepted accepted, $unbaselined unbaselined"
if [ "$owed" -eq 0 ]; then
echo "the replay compared ZERO cells. A run that measured nothing and a run that found nothing"
echo "print the same zero; this one measured nothing — refusing"
return 1
fi
# THE DENOMINATOR IS EVERY OWED CELL, NOT ONE (TODO l.2750 item 7). Refusing only a zero left the
# floor at ONE: a replay whose id filter kept 1 owed cell of 1,015 printed green. The owed count
# must EQUAL the golden's PASS set (owed-baseline.txt, which assert_golden_bookkeeping holds to the
# golden), the scope must equal the committed corpus (cells.json), and the engine's own partition
# must close (owed + unbaselined = scope; busbar-release run.rs splits the selected cells exactly
# so). Any owed cell the replay did not judge is a refusal.
if [ -z "$base" ] || [ -z "$cells" ]; then
echo "no owed-baseline / cells.json was named, so the owed denominator cannot be checked — refusing"; return 1
fi
if ! want_owed="$(grep -cv -e '^[[:space:]]*$' -e '^[[:space:]]*#' "$base" 2>/dev/null)"; then
echo "the owed baseline $base is unreadable or empty — refusing"; return 1
fi
if ! want_scope="$(json_cell_count "$cells")"; then
echo "the corpus $cells is unreadable — refusing"; return 1
fi
if [ "$owed" -ne "$want_owed" ]; then
echo "the replay judged $owed owed cell(s), but the golden owes $want_owed ($base):"
echo "$((want_owed - owed)) owed cell(s) went unjudged — a partial replay is not a parity verdict — refusing"
return 1
fi
if [ "$scope" -ne "$want_scope" ]; then
echo "the replay's scope is $scope cell(s), but the committed corpus holds $want_scope ($cells) — refusing"
return 1
fi
if [ $((owed + unbaselined)) -ne "$scope" ]; then
echo "owed $owed + unbaselined $unbaselined != scope $scope: the report does not account for every cell — refusing"
return 1
fi
if [ "$diverging" -ne 0 ]; then
echo "$diverging unaccepted divergence(s) over $owed owed cell(s) — see $rep/diverging.txt"
return 1
Expand Down Expand Up @@ -970,10 +1012,17 @@ if [ "$SELFTEST" -eq 1 ]; then
printf '{"binary_sha256":"%s","recorded":3}\n' "$st_sha" > "$st_tmp/rec-good/meta.json"
printf '{"binary_sha256":"%s","recorded":3}\n' "$st_other" > "$st_tmp/rec-wrong/meta.json"
printf '# version\tasset\tsha256\n%s\tbusbar-selftest\t%s\n' "$PARITY_BASELINE_VERSION" "$st_sha" > "$st_tmp/digests.tsv"
mkdir -p "$st_tmp/rep-green" "$st_tmp/rep-diverging" "$st_tmp/rep-nothing"
printf '{"totals":{"owed":913,"diverging":0,"accepted":289,"unbaselined":1405,"cells_in_scope":2318}}\n' > "$st_tmp/rep-green/report.json"
printf '{"totals":{"owed":913,"diverging":8,"accepted":289,"unbaselined":1405,"cells_in_scope":2318}}\n' > "$st_tmp/rep-diverging/report.json"
printf '{"totals":{"owed":0,"diverging":0,"accepted":0,"unbaselined":0,"cells_in_scope":0}}\n' > "$st_tmp/rep-nothing/report.json"
mkdir -p "$st_tmp/rep-green" "$st_tmp/rep-diverging" "$st_tmp/rep-nothing" "$st_tmp/rep-one" "$st_tmp/rep-short" "$st_tmp/rep-scope" "$st_tmp/rep-open"
# A five-cell corpus, three owed (the golden's PASS set) and two unbaselined.
printf '# owed\na|1\nb|2\n\nc|3\n' > "$st_tmp/par-base.txt"
printf '{"cells":[{"id":"a|1"},{"id":"b|2"},{"id":"c|3"},{"id":"d|4"},{"id":"e|5"}]}\n' > "$st_tmp/par-cells.json"
printf '{"totals":{"owed":3,"diverging":0,"accepted":1,"unbaselined":2,"cells_in_scope":5}}\n' > "$st_tmp/rep-green/report.json"
printf '{"totals":{"owed":3,"diverging":2,"accepted":1,"unbaselined":2,"cells_in_scope":5}}\n' > "$st_tmp/rep-diverging/report.json"
printf '{"totals":{"owed":0,"diverging":0,"accepted":0,"unbaselined":0,"cells_in_scope":0}}\n' > "$st_tmp/rep-nothing/report.json"
printf '{"totals":{"owed":1,"diverging":0,"accepted":0,"unbaselined":0,"cells_in_scope":1}}\n' > "$st_tmp/rep-one/report.json"
printf '{"totals":{"owed":2,"diverging":0,"accepted":0,"unbaselined":3,"cells_in_scope":5}}\n' > "$st_tmp/rep-short/report.json"
printf '{"totals":{"owed":3,"diverging":0,"accepted":0,"unbaselined":1,"cells_in_scope":4}}\n' > "$st_tmp/rep-scope/report.json"
printf '{"totals":{"owed":3,"diverging":0,"accepted":0,"unbaselined":1,"cells_in_scope":5}}\n' > "$st_tmp/rep-open/report.json"
st_expect accept "a real, unlinked, executable artefact is the subject" assert_candidate_bin_sane "$st_tmp/busbar"
st_expect refuse "a SYMLINK standing where the candidate binary should be" assert_candidate_bin_sane "$st_tmp/busbar-link"
st_expect refuse "a candidate path that does not exist" assert_candidate_bin_sane "$st_tmp/absent"
Expand All @@ -986,10 +1035,16 @@ if [ "$SELFTEST" -eq 1 ]; then
st_expect accept "a golden whose digest this repository commits" assert_golden_is_pinned "$st_tmp/rec-good" "$st_tmp/digests.tsv" "$PARITY_BASELINE_VERSION"
st_expect refuse "a golden whose digest this repository does not commit" assert_golden_is_pinned "$st_tmp/rec-wrong" "$st_tmp/digests.tsv" "$PARITY_BASELINE_VERSION"
st_expect refuse "a golden checked against a digest table that is not there" assert_golden_is_pinned "$st_tmp/rec-good" "$st_tmp/no-such.tsv" "$PARITY_BASELINE_VERSION"
st_expect accept "a report with cells compared and none diverging" assert_parity_verdict "$st_tmp/rep-green"
st_expect refuse "a report carrying unaccepted divergences" assert_parity_verdict "$st_tmp/rep-diverging"
st_expect refuse "a report that compared ZERO cells (the zero that is not one)" assert_parity_verdict "$st_tmp/rep-nothing"
st_expect refuse "no report at all" assert_parity_verdict "$st_tmp/rep-missing"
st_pv() { assert_parity_verdict "$1" "$st_tmp/par-base.txt" "$st_tmp/par-cells.json"; }
st_expect accept "a report that judged every owed cell and none diverging" st_pv "$st_tmp/rep-green"
st_expect refuse "a report carrying unaccepted divergences" st_pv "$st_tmp/rep-diverging"
st_expect refuse "a report that compared ZERO cells (the zero that is not one)" st_pv "$st_tmp/rep-nothing"
st_expect refuse "no report at all" st_pv "$st_tmp/rep-missing"
st_expect refuse "a replay that judged ONE owed cell (the floor of one, item 7)" st_pv "$st_tmp/rep-one"
st_expect refuse "a replay that judged all but one owed cell" st_pv "$st_tmp/rep-short"
st_expect refuse "a replay over a corpus short of the committed cells.json" st_pv "$st_tmp/rep-scope"
st_expect refuse "a report whose owed + unbaselined does not close the scope" st_pv "$st_tmp/rep-open"
st_expect refuse "a verdict asked with no owed baseline to hold the count to" assert_parity_verdict "$st_tmp/rep-green"

# ── PARITY RECORDS BOTH LEGS (item 38) ────────────────────────────────────────────────────────
st_legs_named() { case " $PARITY_LEGS " in *" default "*) ;; *) return 1 ;; esac
Expand Down Expand Up @@ -1521,7 +1576,7 @@ elif [ -x bin/oracle ]; then
# ...and the same two facts re-derived from the report the differ wrote, so the claim does not
# rest on one flag in one pinned engine. A green is a statement about the OWED cells only.
step "[$PARITY_LEG] the report's own numbers: cells were compared, and none diverged" \
assert_parity_verdict "$REPORT"
assert_parity_verdict "$REPORT" testing/shadow-oracle/owed-baseline.txt testing/shadow-oracle/cells.json
else
absent_step "[$PARITY_LEG] the parity recording and its verdict" \
"a candidate binary this run can prove it built — nothing was recorded, so nothing is proven; the release build above is where to start"
Expand Down Expand Up @@ -1562,14 +1617,15 @@ if [ -f qa/audit-ledger.json ]; then
# The `audit-ledger` GATE was deleted with the old register; what survives, and what
# judges a restored register, is `cargo xtask ledger`. Its rules' own RED proofs are its unit
# tests, declared by count so a filter that drifts off them is RED rather than vacuously green.
# 27 = the 11 audit rule tests (xtask/src/audit.rs) + the 11 audit_cmd tests (hygiene_tests 4,
# move_tests 7) + the five pinned-scope tests (xtask/src/audit_pinned/pinned_tests.rs: a moved pin
# 28 = the 11 audit rule tests (xtask/src/audit.rs) + the 12 audit_cmd tests (hygiene_tests 4,
# move_tests 8, the eighth L-R23's: `sync --write` keeps a gone scope with an open HIGH/MEDIUM
# unless `--drop` names it) + the five pinned-scope tests (xtask/src/audit_pinned/pinned_tests.rs: a moved pin
# reads stale, a byte-identical pin carries the record, an unproducible pin is RED naming it, a
# twin / non-plugin git dep is not mounted, the tree wins). THE FILTER NAMES THE THREE MODULES, not
# the bare substring `audit`: that substring also selected q128's two `an_audit_of_*` tests and the
# construction gate's two `no_response_escapes_audit_tests`, so the run passed 31 against a declared
# 29 and this step was RED on tests that are not the ledger's rules (they run in TEST).
step "audit ledger rules (xtask audit + audit_cmd + audit_pinned tests)" filtered_cargo_test 27 cargo test -p xtask --lib -- audit:: audit_cmd:: audit_pinned::
step "audit ledger rules (xtask audit + audit_cmd + audit_pinned tests)" filtered_cargo_test 28 cargo test -p xtask --lib -- audit:: audit_cmd:: audit_pinned::
step "audit-ledger --check" cargo xtask ledger --check
else
absent_step "audit ledger" "qa/audit-ledger.json"
Expand Down
129 changes: 125 additions & 4 deletions xtask/src/audit_cmd.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,8 @@ use crate::json_lite::{self, Json, Obj};

const USAGE: &str = "\
usage:
cargo xtask ledger sync [--write] derive the scope list from the tree
cargo xtask ledger sync [--write] [--drop ID,..] derive the scope list from the tree; a gone
scope with an open HIGH/MEDIUM is kept unless --drop names it
cargo xtask ledger status print the table and write qa/evidence/AUDIT-STATUS.md
cargo xtask ledger next the worklist, worst first
cargo xtask ledger record --scope S --round N --result R --report P --auditor A [--counts ..] [--at REV]
Expand Down Expand Up @@ -57,7 +58,8 @@ const MOVE_SUB: &str = "move";
/// auditor believed they had named the commit they read, and the record would claim a tree nobody
/// looked at. An unexpected positional has always been an error; a misspelt flag is the same
/// mistake.
const OPTIONS: [&str; 10] = [
const OPTIONS: [&str; 11] = [
"drop",
"ledger",
"report-md",
"scope",
Expand Down Expand Up @@ -136,7 +138,12 @@ pub fn main(root: &std::path::Path, args: &[String]) -> i32 {
}

match a.sub.as_deref() {
Some("sync") => cmd_sync(&git, &register, a.flags.iter().any(|f| f == "write")),
Some("sync") => cmd_sync(
&git,
&register,
a.flags.iter().any(|f| f == "write"),
a.map.get("drop").map(String::as_str),
),
Some("status") => cmd_status(&git, &register, &report),
Some("next") => cmd_next(&git, &register),
Some("record") => cmd_record(&git, &register, &a),
Expand Down Expand Up @@ -170,7 +177,32 @@ fn ids(scopes: &[Json]) -> Vec<String> {
.collect()
}

fn cmd_sync(git: &Git, register: &std::path::Path, write: bool) -> i32 {
/// The scopes `sync` would drop (their path is gone) that still carry an OPEN HIGH or MEDIUM finding,
/// each with the counts that hold it open. L-R23: `sync --write` used to drop them with the record
/// and exit 0, so a finding nobody fixed left the register by deleting the directory it was in.
fn dropped_open(existing: &[Json], removed: &[&String]) -> Vec<(String, String)> {
existing
.iter()
.filter_map(|sc| {
let id = sc.get("id").as_str()?;
if !removed.iter().any(|r| r.as_str() == id) {
return None;
}
let found = audit::open_findings(sc, None)?;
let counts = found.get("counts");
let held: Vec<String> = ["HIGH", "MEDIUM"]
.iter()
.filter_map(|k| {
let n = counts.get(k).as_i64().unwrap_or(0);
(n > 0).then(|| format!("{k} {n}"))
})
.collect();
(!held.is_empty()).then(|| (id.to_string(), held.join(", ")))
})
.collect()
}

fn cmd_sync(git: &Git, register: &std::path::Path, write: bool, drop: Option<&str>) -> i32 {
let mounted = match git.mounted_at("HEAD") {
Ok(m) => m,
Err(e) => return die(e),
Expand All @@ -196,6 +228,42 @@ fn cmd_sync(git: &Git, register: &std::path::Path, write: bool) -> i32 {
println!("- {sid} (path gone from the tree; its audit record goes with it)");
}

// A GONE SCOPE THAT STILL HOLDS AN OPEN HIGH/MEDIUM IS NOT DROPPED IN SILENCE. It goes only when
// `--drop` names it — the declaration that the finding left with the code, reviewed in the
// diff that carries it. A named id that is not such a scope is refused too: a declaration that
// covers nothing is a standing excuse.
let open = dropped_open(&existing, &removed);
let declared: Vec<&str> = drop
.unwrap_or_default()
.split(',')
.map(str::trim)
.filter(|d| !d.is_empty())
.collect();
let undeclared: Vec<&(String, String)> = open
.iter()
.filter(|(id, _)| !declared.contains(&id.as_str()))
.collect();
let idle: Vec<&&str> = declared
.iter()
.filter(|d| !open.iter().any(|(id, _)| id == **d))
.collect();
if !undeclared.is_empty() || !idle.is_empty() {
for (id, held) in &undeclared {
eprintln!(
"sync: REFUSED -- {id} is gone from the tree with open findings ({held}); fix and \
record them, `ledger move` the record to where the code went, or name the scope \
in --drop"
);
}
for d in &idle {
eprintln!(
"sync: REFUSED -- --drop names {d}, which is not a gone scope with open findings"
);
}
eprintln!("sync: nothing written");
return 1;
}

let merged = audit::merge(&derived, &existing);
if added.is_empty() && removed.is_empty() {
println!(
Expand Down Expand Up @@ -2026,6 +2094,59 @@ mod move_tests {
assert!(super::round_from_record(&never_read).is_none());
}

/// L-R23 RED: a scope whose path is gone while it holds an open HIGH finding is NOT dropped by
/// `sync --write` (exit 1, register untouched); `--drop` naming it is the one way through, and a
/// `--drop` naming nothing open is refused too.
#[test]
fn sync_keeps_a_gone_scope_with_open_findings_unless_drop_names_it() {
let s = scratch("drop-open");
s.crate_at("keep", "pub fn k() {}\n");
s.crate_at("gone", "pub fn g() {}\n");
s.commit("base");
assert_eq!(s.xtask(&["sync", "--write"]), 0);
assert_eq!(
s.xtask(&[
"record",
"--scope",
"crates/gone/src",
"--round",
"1",
"--result",
"findings",
"--report",
"a path admits an unmetered call",
"--auditor",
"alice",
"--counts",
"HIGH=1",
]),
0
);
s.run(&["rm", "-rq", "crates/gone"]);
s.commit("delete the crate the finding was in");
let before = s.raw();

assert_eq!(
s.xtask(&["sync", "--write"]),
1,
"an open HIGH is not dropped"
);
assert_eq!(s.raw(), before, "a refused sync writes nothing");
assert_eq!(
s.xtask(&["sync", "--write", "--drop", "crates/keep/src"]),
1,
"a --drop naming a scope with nothing open is refused"
);
assert_eq!(s.raw(), before);

assert_eq!(
s.xtask(&["sync", "--write", "--drop", "crates/gone/src"]),
0
);
assert!(s.scope("crates/gone/src").is_none(), "named, it goes");
assert!(s.scope("crates/keep/src").is_some());
}

/// THE LAUNDERING, AND THE REPAIR, IN ONE TEST — because a tool whose reason for existing is
/// undocumented is a tool the next reader deletes.
///
Expand Down