From 9d026e1ab6937987b7e03fba75ecc2bb5603813e Mon Sep 17 00:00:00 2001 From: Swung0x48 Date: Wed, 23 Sep 2026 18:51:47 -0400 Subject: [PATCH] [tools] (P7): gate 3 runs the monolith x3 and 60-reduce.py judges a case whose same-session monolith is not bit-identical by the ID-P7-62 distributional check --- .../tools/30-gate3-selftest.sh | 144 +++++++ .../p7/device-window-2/tools/30-gate3.sh | 24 +- .../tools/60-reduce-selftest.py | 217 +++++++++- .../p7/device-window-2/tools/60-reduce.py | 393 +++++++++++++++--- .../notes/p7/device-window-2/tools/window.sh | 2 +- 5 files changed, 698 insertions(+), 82 deletions(-) create mode 100755 docs/Disaggregated/notes/p7/device-window-2/tools/30-gate3-selftest.sh mode change 100755 => 100644 docs/Disaggregated/notes/p7/device-window-2/tools/30-gate3.sh mode change 100755 => 100644 docs/Disaggregated/notes/p7/device-window-2/tools/window.sh diff --git a/docs/Disaggregated/notes/p7/device-window-2/tools/30-gate3-selftest.sh b/docs/Disaggregated/notes/p7/device-window-2/tools/30-gate3-selftest.sh new file mode 100755 index 00000000..da20bcc6 --- /dev/null +++ b/docs/Disaggregated/notes/p7/device-window-2/tools/30-gate3-selftest.sh @@ -0,0 +1,144 @@ +#!/usr/bin/env bash +# 30-gate3-selftest.sh [--script PATH] (host only: no phone, no adb server, no device lock) +# +# Runs 30-gate3.sh (or PATH: red-once of an older driver) against a stub adb and a stub runner in a +# temp dir and checks its repeat bookkeeping (ID-P7-62: the monolith arm runs x --repeat, recorded +# as arms.txt monolith_repeat=) and its resume semantics: +# fresh --cases a,b: arms.txt says repeat=3 monolith_repeat=3; the runner is asked for the +# monolith x3; every monolith pair archives 3 repeats and writes its .done; exit 0 +# resume one monolith .done deleted: only that pair re-runs, again x3 +# incomplete a monolith repeat without its PNG: no .done, progress.tsv INCOMPLETE, exit 3; the +# same command again completes it +# frozen an arms.txt with monolith_repeat=3, resumed with --repeat 1: every arm keeps 3 +# old-format an arms.txt without monolith_repeat= (a run the pre-ID-P7-62 script started): a +# resume keeps that run's monolith x1 +# Exit 0 when every check holds. +set -uo pipefail +HERE=$(CDPATH= cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd) +SCRIPT="$HERE/30-gate3.sh" +[ "${1:-}" = --script ] && SCRIPT=$2 +TMP=$(mktemp -d "${TMPDIR:-/tmp}/w2-gate3-selftest-XXXXXX") +trap 'rm -rf "$TMP"' EXIT +BOOT=11111111-2222-3333-4444-555555555555 + +# The driver under test beside this tree's lib.sh (it sources "$(dirname "$0")/lib.sh"). +mkdir -p "$TMP/under-test" "$TMP/bin" "$TMP/tree/tools/trace_replay" "$TMP/tree/tools/device_bench" "$TMP/logs" +cp "$SCRIPT" "$TMP/under-test/30-gate3.sh" +cp "$HERE/lib.sh" "$TMP/under-test/lib.sh" +cat > "$TMP/bin/adb" <<'EOF' +#!/usr/bin/env bash +[ "${1:-}" = -s ] && shift 2 +case "$*" in + get-state) echo device;; + "shell cat /proc/sys/kernel/random/boot_id") echo "$FAKE_BOOT";; +esac +exit 0 +EOF +chmod +x "$TMP/bin/adb" +printf '#!/usr/bin/env bash\necho " VERDICT: PINNED"\n' > "$TMP/tree/tools/device_bench/pin_device.sh" +cat > "$TMP/tree/tools/trace_replay/run_android_retrace_local.py" <<'EOF' +# Stub runner (lib.sh looks for: def bash_executable / def clear_repeat_outputs). +import argparse, json, os, pathlib +ap = argparse.ArgumentParser() +for flag in ("--case", "--backend", "--transport", "--archive-dir"): + ap.add_argument(flag) +ap.add_argument("--repeat", type=int, default=1) +ap.add_argument("--env", action="append", default=[]) +ap.add_argument("--use-pbuffer", action="store_true") +a = ap.parse_args() +with open(os.environ["FAKE_RUNLOG"], "a") as log: + log.write("transport=%s repeat=%d case=%s env=%s\n" % (a.transport, a.repeat, a.case, ",".join(a.env))) +drop = os.environ.get("FAKE_DROP", "") # :: archived without its PNG +arm = pathlib.Path(a.archive_dir) / (a.case + "-DirectVulkan") +for i in range(1, a.repeat + 1): + rep = arm / ("repeat-%02d" % i) + rep.mkdir(parents=True, exist_ok=True) + (rep / "result.json").write_text(json.dumps({"passed": True, "ssim": 0.998})) + if drop != "%s:%s:%d" % (a.transport, a.case, i): + (rep / (a.case + "-DirectVulkan-actual.png")).write_bytes(b"png") + print('"passed": true') +(pathlib.Path(a.archive_dir) / "run.json").write_text("{}") +EOF +: > "$TMP/fake.apk" +export PATH="$TMP/bin:$PATH" FAKE_BOOT=$BOOT FAKE_RUNLOG="$TMP/runner.log" W2_LOGROOT="$TMP/logs" W2_SHARED_LOCK= \ + W2_LOCK="$TMP/w2.lock" W2_TOOLS_OVERRIDE="$TMP/tree" W2_APK_OVERRIDE="$TMP/fake.apk" W2_SERIAL=stub0000 +: > "$FAKE_RUNLOG" +# Never the real adb (it would reach the Windows adb server, or start one in WSL). +[ "$(command -v adb)" = "$TMP/bin/adb" ] || { echo "the stub adb is not first on PATH: $(command -v adb)" >&2; exit 2; } + +TOTAL=0; FAILED=() +expect() { # [detail] + TOTAL=$((TOTAL + 1)) + if [ "$2" -eq 0 ]; then echo " ok $1"; else echo " FAIL $1 <-- ${3:-}"; FAILED+=("$1"); fi +} +gate() { # [args...] -> the driver's exit status; its log in $TMP/..log + local stamp=$1; shift + mkdir -p "$W2_LOGROOT/$stamp/session" + echo "$BOOT" > "$W2_LOGROOT/$stamp/session/boot-id.txt" + RUNS=$((RUNS + 1)) + bash "$TMP/under-test/30-gate3.sh" "$stamp" "$@" > "$TMP/$stamp.$RUNS.log" 2>&1 +} +calls() { grep -c -- "$1" "$FAKE_RUNLOG" || true; } +reps() { find "$W2_LOGROOT/$1/gate3/archive/$2/$3-DirectVulkan" -maxdepth 1 -name 'repeat-*' 2>/dev/null | wc -l; } +RUNS=0 +echo "30-gate3 self-test: driver $SCRIPT, stubs in $TMP" + +echo "[fresh] a new run records monolith_repeat and runs the monolith x --repeat" +gate fresh --cases case-a,case-b; rc=$? +G="$W2_LOGROOT/fresh/gate3" +expect "exit 0" $rc "rc=$rc; $(tail -3 "$TMP/fresh.$RUNS.log")" +grep -qx 'monolith_repeat=3' "$G/arms.txt" && grep -qx 'repeat=3' "$G/arms.txt" +expect "arms.txt: repeat=3 and monolith_repeat=3" $? "$(cat "$G/arms.txt")" +[ "$(calls 'transport=monolith repeat=3 ')" = 2 ] && [ "$(calls 'transport=monolith repeat=1 ')" = 0 ] +expect "the runner is asked for the monolith x3 on both cases" $? "$(grep monolith "$FAKE_RUNLOG")" +[ "$(reps fresh monolith case-a)" = 3 ] && [ "$(reps fresh monolith case-b)" = 3 ] +expect "each monolith pair archives 3 repeats" $? "$(reps fresh monolith case-a)/$(reps fresh monolith case-b)" +[ "$(ls "$G"/state/*/*.done | wc -l)" = 8 ] && [ -f "$G/state/monolith/case-a.done" ] +expect "every (arm, case) pair has its .done (8)" $? "$(ls "$G"/state/*/)" +[ "$(calls 'transport=inproc repeat=3 ')" = 2 ] && [ "$(calls 'transport=spawn repeat=3 ')" = 2 ] \ + && [ "$(calls 'transport=inproc repeat=1 case=case-.* env=MOBILEGL_IPC_RUN_AHEAD=0')" = 2 ] +expect "the split arms keep x3 and ra0 x1" $? "$(cat "$FAKE_RUNLOG")" + +echo "[resume] a deleted monolith .done re-runs that one pair, x3" +: > "$FAKE_RUNLOG"; rm "$G/state/monolith/case-a.done" +gate fresh; rc=$? +[ $rc -eq 0 ] && [ "$(wc -l < "$FAKE_RUNLOG")" = 1 ] && [ "$(calls 'transport=monolith repeat=3 case=case-a ')" = 1 ] \ + && [ -f "$G/state/monolith/case-a.done" ] && [ "$(reps fresh monolith case-a)" = 3 ] +expect "only monolith case-a re-ran, x3, and wrote its .done" $? "rc=$rc; $(cat "$FAKE_RUNLOG")" + +echo "[incomplete] a monolith repeat without its PNG leaves the pair open" +: > "$FAKE_RUNLOG" +FAKE_DROP=monolith:case-b:2 gate incomplete --cases case-a,case-b; rc=$? +G="$W2_LOGROOT/incomplete/gate3" +[ $rc -eq 3 ] && [ ! -f "$G/state/monolith/case-b.done" ] && [ -f "$G/state/monolith/case-a.done" ] \ + && grep -q "^monolith case-b .* INCOMPLETE$" "$G/progress.tsv" +expect "monolith case-b repeat-02 without a PNG -> no .done, progress INCOMPLETE, exit 3" $? "rc=$rc; $(cat "$G/progress.tsv" 2>/dev/null)" +: > "$FAKE_RUNLOG" +gate incomplete; rc=$? +[ $rc -eq 0 ] && [ -f "$G/state/monolith/case-b.done" ] && [ "$(wc -l < "$FAKE_RUNLOG")" = 1 ] \ + && [ "$(calls 'transport=monolith repeat=3 case=case-b ')" = 1 ] +expect "...the same command again re-runs that pair only (x3) and completes, exit 0" $? "rc=$rc; $(cat "$FAKE_RUNLOG")" + +echo "[frozen] a resume keeps the first run's counts, whatever --repeat it is given" +G="$W2_LOGROOT/frozen/gate3"; mkdir -p "$G" +printf 'case-a\n' > "$G/cases.txt" +printf 'arms=monolith inproc spawn inproc-ra0\nrepeat=3\nmonolith_repeat=3\n' > "$G/arms.txt" +: > "$FAKE_RUNLOG" +gate frozen --repeat 1; rc=$? +[ $rc -eq 0 ] && [ "$(calls 'transport=monolith repeat=3 ')" = 1 ] && [ "$(calls 'transport=inproc repeat=3 ')" = 1 ] \ + && [ "$(calls 'transport=spawn repeat=3 ')" = 1 ] +expect "arms.txt repeat=3 monolith_repeat=3 resumed with --repeat 1 -> monolith, inproc, spawn x3" $? "rc=$rc; $(cat "$FAKE_RUNLOG")" + +echo "[old-format] an arms.txt the pre-ID-P7-62 script froze (no monolith_repeat=) keeps its monolith x1" +G="$W2_LOGROOT/old/gate3"; mkdir -p "$G" +printf 'case-a\n' > "$G/cases.txt" +printf 'arms=monolith inproc spawn inproc-ra0\nrepeat=3\napk=x\ntools=y\n' > "$G/arms.txt" +: > "$FAKE_RUNLOG" +gate old; rc=$? +[ $rc -eq 0 ] && [ "$(calls 'transport=monolith repeat=1 ')" = 1 ] && [ "$(reps old monolith case-a)" = 1 ] \ + && [ -f "$G/state/monolith/case-a.done" ] && [ "$(calls 'transport=inproc repeat=3 ')" = 1 ] \ + && grep -q 'monolith repeat frozen at 1' "$TMP/old.$RUNS.log" +expect "monolith x1 with its .done, the split arms x3, and the log says why" $? "rc=$rc; $(cat "$FAKE_RUNLOG")" + +echo "30-gate3 self-test: $((TOTAL - ${#FAILED[@]}))/$TOTAL checks passed${FAILED:+; FAILED: ${FAILED[*]}}" +[ ${#FAILED[@]} -eq 0 ] diff --git a/docs/Disaggregated/notes/p7/device-window-2/tools/30-gate3.sh b/docs/Disaggregated/notes/p7/device-window-2/tools/30-gate3.sh old mode 100755 new mode 100644 index e174eb08..60756ad4 --- a/docs/Disaggregated/notes/p7/device-window-2/tools/30-gate3.sh +++ b/docs/Disaggregated/notes/p7/device-window-2/tools/30-gate3.sh @@ -2,7 +2,10 @@ # 30-gate3.sh [--cases a,b,...] [--repeat N] [--arms monolith,inproc,spawn,inproc-ra0] # # CONTRACT-P7 7.1/7.2 exit gate 3, one reboot-clean session, DirectVulkan x --use-pbuffer: -# monolith x1 the same-session control every split reading is scored against +# monolith xN the same-session control every split reading is scored against; xN (ID-P7-62) +# so the session itself shows whether the monolith is bit-reproducible - a case +# whose monolith is not (the Iris sundial-lite / bliss / derivative packs on Adreno +# 830) is judged by 60-reduce.py's distributional check instead of bit-identity # inproc xN (N = --repeat, default 3) must be bit-identical across passes # spawn xN same, server role in a second process # inproc-ra0 x1 MOBILEGL_IPC_RUN_AHEAD=0 lockstep control, recorded only @@ -69,26 +72,35 @@ PY fi mapfile -t CASES < "$OUT/cases.txt" [ ${#CASES[@]} -gt 0 ] || die "empty case list" -[ -f "$OUT/arms.txt" ] || printf 'arms=%s\nrepeat=%s\napk=%s\ntools=%s\n' "$ARMS" "$REPEAT" "$W2_APK" "$W2_TOOLS" > "$OUT/arms.txt" -# The repeat count is frozen with the case list: a resume started without the first run's --repeat +[ -f "$OUT/arms.txt" ] || printf 'arms=%s\nrepeat=%s\nmonolith_repeat=%s\napk=%s\ntools=%s\n' \ + "$ARMS" "$REPEAT" "$REPEAT" "$W2_APK" "$W2_TOOLS" > "$OUT/arms.txt" +# The repeat counts are frozen with the case list: a resume started without the first run's --repeat # (RUNBOOK: "30-gate3.sh ") must not re-run a pair with another count than its siblings'. FROZEN_REPEAT=$(sed -n 's/^repeat=//p' "$OUT/arms.txt") if [ -n "$FROZEN_REPEAT" ] && [ "$FROZEN_REPEAT" != "$REPEAT" ]; then log "repeat frozen at $FROZEN_REPEAT by $OUT/arms.txt (asked: $REPEAT)" REPEAT=$FROZEN_REPEAT fi -log "gate3 stamp=$STAMP cases=${#CASES[@]} arms=[$ARMS] repeat=$REPEAT apk=$W2_APK tools=$W2_TOOLS" +# The monolith runs x the same repeat from ID-P7-62 on (arms.txt monolith_repeat=). An arms.txt +# without the key was frozen by the earlier script, whose monolith pairs ran x1: a resume of that +# run keeps x1, so its monolith pairs all have one count (60-reduce.py reads the same key). +MONO_REPEAT=$(sed -n 's/^monolith_repeat=//p' "$OUT/arms.txt") +if [ -z "$MONO_REPEAT" ]; then + MONO_REPEAT=1 + log "monolith repeat frozen at 1 by $OUT/arms.txt (no monolith_repeat=: started by the pre-ID-P7-62 script)" +fi +log "gate3 stamp=$STAMP cases=${#CASES[@]} arms=[$ARMS] repeat=$REPEAT monolith_repeat=$MONO_REPEAT apk=$W2_APK tools=$W2_TOOLS" arm_args() { # -> runner arguments case "$1" in - monolith) echo "--transport monolith --repeat 1";; + monolith) echo "--transport monolith --repeat $MONO_REPEAT";; inproc) echo "--transport inproc --repeat $REPEAT";; spawn) echo "--transport spawn --repeat $REPEAT";; inproc-ra0) echo "--transport inproc --repeat 1 --env MOBILEGL_IPC_RUN_AHEAD=0";; *) die "unknown arm $1";; esac } -arm_repeats() { case "$1" in inproc|spawn) echo "$REPEAT";; *) echo 1;; esac; } +arm_repeats() { case "$1" in inproc|spawn) echo "$REPEAT";; monolith) echo "$MONO_REPEAT";; *) echo 1;; esac; } # -> the repeats (of 1..n) that lack result.json or an actual PNG; empty = complete missing_repeats() { diff --git a/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce-selftest.py b/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce-selftest.py index 0957edc2..70a4cafa 100644 --- a/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce-selftest.py +++ b/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce-selftest.py @@ -6,8 +6,8 @@ reducer on each exactly as window.sh does (a subprocess, --logroot --too the printed verdict, verdict.json and the exit status. Gate 3 is canned at the gate's own denominator - the canonical 36, derived here as 30-gate3.sh derives gate3/cases.txt (the tree's trace_cases.json CI split DirectVulkan cases minus CONTRACT-P7 7.1's three exclusions) - with -monolith / inproc x3 / spawn x3 / ra0, one boot_id, reboot-clean, unless a scenario says -otherwise. The scenarios: +monolith x3 (ID-P7-62) / inproc x3 / spawn x3 / ra0, one boot_id, reboot-clean, unless a scenario +says otherwise. The scenarios: control gate 3 and all five CTS blocks equal to $BASE -> GATE3 PASS, CTS PASS, exit 0 missing-block ssbo never finished, dsa's report is empty, texture's has no results; and a @@ -33,6 +33,18 @@ otherwise. The scenarios: NEEDS-ADJUDICATION naming it; one case differing, adjudicated (+ a stale line) -> PASS; one inproc repeat differs from its siblings -> FAIL (within-arm identity) unfinished a pair without .done; a repeat without an actual PNG -> GATE3 INCOMPLETE + monolith-determinism ID-P7-62, on synthetic 8x8 pictures (base grey 128, the first n px at + another level): a bit-identical monolith x3 + a nondeterministic inproc -> FAIL + (strict clause); a nondeterministic monolith (3 distinct / 3 passes, 10 px / delta + 4 apart) + split pictures inside 1.25x (10 px / delta 5) -> PASS, exit 0, no + adjudication line needed, the numbers printed; the same with the stdlib decoder + (W2_REDUCE_PNG_DECODER=pure) -> the same numbers; split beyond 1.25x in delta + (6 > 5) or in pixels (13 > 12.5) -> FAIL; one split ssim 0.0005+ from ONE + monolith reading -> FAIL; the pre-ID-P7-62 monolith x1 + a nondeterministic + split -> FAIL naming the >= 3 passes it lacks; a finished monolith pair short of + arms.txt's monolith_repeat -> FAIL; --extra-monolith DIR@BOOT adding two passes + to that x1 archive -> the rule applies, GATE3 PASS-WITH-EXTRA-READINGS (exit 1), + without @BOOT or with another boot -> INVALID-SESSION rate-gate the gate rate alone decides (no crash anywhere): k $BASE-Pass dsa cases turn Fail. k=1: 367/370, -0.270 pp -> PASS, exit 0; k=2: -0.541 pp -> FAIL on the rate; k=4: 364/6/0/1/0, -1.081 pp -> FAIL, CTS FAIL @@ -102,7 +114,10 @@ CASES, A, B = (), None, None OPENRA = "OpenRA" REPEAT = 3 GONE = "/nonexistent/p7w7-tree-deadbeef/tools/cts/caselists/p7-%s-gl46.txt" -ARMS = (("monolith", 1), ("inproc", REPEAT), ("spawn", REPEAT), ("inproc-ra0", 1)) +ARMS = (("monolith", REPEAT), ("inproc", REPEAT), ("spawn", REPEAT), ("inproc-ra0", 1)) +# The pre-ID-P7-62 30-gate3.sh: monolith x1, and no monolith_repeat= in gate3/arms.txt. +ARMS_MONO1 = (("monolith", 1),) + ARMS[1:] +ARMS_TXT_MONO1 = "arms=monolith inproc spawn inproc-ra0\nrepeat=3\n" DSA_STORAGE = "KHR-GL46.direct_state_access.renderbuffers_storage" SI_INCOMPLETE = "KHR-GL46.shader_image_load_store.incomplete_textures" CODEX_RULING = "ruling: integrator 2026-09-23 after codex closeout review" @@ -128,6 +143,14 @@ def write(path, data): path.write_text(data, encoding="utf-8") +def lookup(table, arm, case, repeat, default): + """A canned per-repeat value: (arm, case, repeat), else (arm, case), else arm, else default.""" + for key in ((arm, case, repeat), (arm, case), arm): + if key in table: + return table[key] + return default + + def read_list(path): if not path.is_file(): return [] @@ -163,21 +186,31 @@ class Canned: self.root, self.tree, self.ca = root, tree, ca def png(self, value): + """value: a grey level (a solid 8x8 picture), or (n, level): grey 128 with its first n pixels + (row-major) at `level` - the synthetic 'speckle' the ID-P7-62 scenarios move around.""" + if isinstance(value, tuple): + n, level = value + rgba = bytearray(self.ca._solid(8, 8, 128)) + for i in range(n): + rgba[i * 4:i * 4 + 3] = bytes([level] * 3) + return self.ca._png_bytes(8, 8, bytes(rgba)) return self.ca._png_bytes(8, 8, self.ca._solid(8, 8, value)) def gate3(self, out, picture=None, boot=BOOT, cases=None, reboot_clean=True, arms=ARMS, arms_txt=None, - excluded=EXCLUDED): - """30-gate3.sh's output. picture: {arm or (arm, case): grey value} (default 128 everywhere); - arms: ((arm, repeats), ...) actually run; arms_txt: gate3/arms.txt's text (default: what - 30-gate3.sh writes for `arms`).""" - picture = picture or {} + excluded=EXCLUDED, ssim=None): + """30-gate3.sh's output. picture: {arm, (arm, case) or (arm, case, repeat): Canned.png value} + (default 128 everywhere); ssim: the same keys -> result.json's ssim (default 0.998, OpenRA + 1.0); arms: ((arm, repeats), ...) actually run; arms_txt: gate3/arms.txt's text (default: + what 30-gate3.sh writes for `arms`).""" + picture, ssim = picture or {}, ssim or {} cases = CASES if cases is None else cases g = out / "gate3" write(g / "cases.txt", "\n".join(cases) + "\n") write(g / "excluded.txt", "\n".join(excluded) + "\n") repeat = max([n for a, n in arms if a in ("inproc", "spawn")] or [REPEAT]) write(g / "arms.txt", arms_txt if arms_txt is not None - else "arms=%s\nrepeat=%d\n" % (" ".join(a for a, _ in arms), repeat)) + else "arms=%s\nrepeat=%d\nmonolith_repeat=%d\n" % (" ".join(a for a, _ in arms), repeat, + dict(arms).get("monolith", repeat))) write(out / "session/boot-id.txt", boot + "\n") write(out / "session/reboot-clean.txt", ("reboot-clean: 00000000-0000-0000-0000-000000000000 -> %s\n" % boot) if reboot_clean @@ -189,10 +222,11 @@ class Canned: for i in range(1, n + 1): rep = g / "archive" / arm / name / ("repeat-%02d" % i) write(rep / "result.json", json.dumps({ - "passed": True, "statusCode": 0, "backend": "DirectVulkan", "ssim": 1.0 if openra else 0.998, + "passed": True, "statusCode": 0, "backend": "DirectVulkan", + "ssim": lookup(ssim, arm, case, i, 1.0 if openra else 0.998), "ssimThreshold": 0.99, "mismatchPixels": 0 if openra else 17, "matchedGoldenPath": "/in/golden.png", "cropX": 0, "cropY": 0, "cropWidth": 0, "cropHeight": 0})) - write(rep / (name + "-actual.png"), self.png(picture.get((arm, case), picture.get(arm, 128)))) + write(rep / (name + "-actual.png"), self.png(lookup(picture, arm, case, i, 128))) write(rep / "logcat.txt", "canned logcat %s %s repeat %d\n" % (arm, case, i)) write(rep / "mobilegl.log", LOGS[arm]) if arm in ("inproc", "spawn"): @@ -203,6 +237,23 @@ class Canned: "finished=2026-09-23T12:00:00-04:00\n" % (n, boot, boot)) return g + def extra_monolith(self, d, case, pictures, boot=None): + """A run_android_retrace_local.py --archive-dir tree of monolith passes outside gate3/ (the + g3det E1-mono shape): one repeat per `pictures` value; boot: stamp repeat-NN/boot_id.txt.""" + name = case + "-DirectVulkan" + for i, value in enumerate(pictures, 1): + rep = d / name / ("repeat-%02d" % i) + write(rep / "result.json", json.dumps({ + "passed": True, "statusCode": 0, "backend": "DirectVulkan", "ssim": 0.998, "ssimThreshold": 0.99, + "mismatchPixels": 17, "matchedGoldenPath": "/in/golden.png", "cropX": 0, "cropY": 0, + "cropWidth": 0, "cropHeight": 0})) + write(rep / (name + "-actual.png"), self.png(value)) + write(rep / "logcat.txt", "canned extra logcat %s repeat %d\n" % (case, i)) + write(rep / "mobilegl.log", LOGS["monolith"]) + if boot: + write(rep / "boot_id.txt", "boot_id=%s boot_id_before=%s\n" % (boot, boot)) + return d + def base(self, b): return dict(json.loads((self.tree / CTS_BASE_REL / ("report-%s.json" % b)).read_text(encoding="utf-8"))["results"]) @@ -269,11 +320,14 @@ class Canned: return out -def run_reducer(logroot, stamp, tree, json_out=None): +def run_reducer(logroot, stamp, tree, json_out=None, extra=(), env=None): cmd = [sys.executable, str(REDUCER), stamp, "--logroot", str(logroot), "--tools", str(tree)] if json_out: cmd += ["--json", str(json_out)] - p = subprocess.run(cmd, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, universal_newlines=True) + for spec in extra: + cmd += ["--extra-monolith", str(spec)] + p = subprocess.run(cmd, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, universal_newlines=True, + env=dict(os.environ, **(env or {}))) vpath = Path(json_out) if json_out else Path(logroot) / stamp / "verdict.json" verdict = json.loads(vpath.read_text(encoding="utf-8")) if vpath.is_file() else {} return p.returncode, p.stdout, verdict @@ -420,7 +474,7 @@ def scenario_monolith_arm(k, cn, tree): e.get("verdict") == "FAIL" and overall(v) == "FAIL" and rc != 0 and any("NOT proven monolith" in r for r in e.get("reasons", [])), e) k.expect("the other case still PASS", case(v, B).get("verdict") == "PASS") - k.expect("arm identity line counts 35/36 monolith", "monolith 35/36 repeat(s)" in text, text) + k.expect("arm identity line counts 107/108 monolith passes (x3)", "monolith 107/108 repeat(s)" in text, text) out = cn.window("mono-nolog") (out / "gate3/archive/monolith" / (B + "-DirectVulkan") / "repeat-01" / "mobilegl.log").unlink() @@ -493,7 +547,8 @@ def scenario_arms(k, cn, tree): k.expect("a run started without spawn -> GATE3 FAIL-ARMS", overall(v) == "FAIL-ARMS" and rc != 0 and any("arm spawn has no archive" in p for p in contract(v, "arms")), overall(v)) - cn.window("ra0-planned", gate3_args={"arms": three, "arms_txt": "arms=monolith inproc spawn inproc-ra0\nrepeat=3\n"}) + cn.window("ra0-planned", gate3_args={"arms": three, "arms_txt": "arms=monolith inproc spawn inproc-ra0\nrepeat=3\n" + "monolith_repeat=3\n"}) rc, text, v = run_reducer(cn.root, "ra0-planned", tree) k.expect("inproc-ra0 named in arms.txt but not reached yet -> GATE3 INCOMPLETE (not PASS), exit != 0", overall(v) == "INCOMPLETE" and rc != 0 and contract(v, "arms") == [] @@ -556,10 +611,10 @@ def scenario_cross_arm(k, cn, tree): and g3(v, "cross_arm_unadjudicated") == list(CASES)) x = case(v, B).get("cross_arm", {}) k.expect("the list carries the archived px!=golden and the direct px counts (8x8: 64 between 128 and 129)", - x.get("px_vs_golden") == {"monolith": 17, "inproc": [17, 17, 17], "spawn": [17, 17, 17]} + x.get("px_vs_golden") == {"monolith": [17, 17, 17], "inproc": [17, 17, 17], "spawn": [17, 17, 17]} and x.get("px_direct") == {"inproc-monolith": 0, "spawn-monolith": 64, "inproc-spawn": 64} - and "px!=golden (archived mismatchPixels) monolith 17, inproc 17..17, spawn 17..17; px between the arms' " - "first repeats: inproc-monolith 0, spawn-monolith 64, inproc-spawn 64" in text, x) + and "px!=golden (archived mismatchPixels) monolith 17..17, inproc 17..17, spawn 17..17; px between the " + "arms' first repeats: inproc-monolith 0, spawn-monolith 64, inproc-spawn 64" in text, x) k.expect("both rulings are named", "ruling: integrator 2026-09-23;" in text and CODEX_RULING in text) out = cn.window("cross-adj", gate3_args={"picture": {"spawn": 129}}) @@ -614,6 +669,131 @@ def scenario_unfinished(k, cn, tree): and any("no *-actual.png" in r for r in e.get("reasons", [])), e) +def scenario_determinism(k, cn, tree): + print("[monolith-determinism] ID-P7-62: a monolith not bit-identical over >= 3 passes swaps the split arms' " + "bit-identity clause for the distributional check") + # A nondeterministic monolith: 3 distinct pictures, pairwise 10 px apart, largest delta 4 -> the + # split bound is 12.5 px / delta 5.0. + mono = {("monolith", A, 1): (10, 128), ("monolith", A, 2): (10, 132), ("monolith", A, 3): (10, 130)} + inside = {("inproc", A, 1): (10, 129), ("inproc", A, 2): (10, 131), ("inproc", A, 3): (10, 133), + ("spawn", A, 1): (10, 130), ("spawn", A, 2): (10, 132), ("spawn", A, 3): (10, 128)} + rule_line = "nondeterministic monolith (3 distinct / 3 passes) -> distributional check (ID-P7-62)" + numbers = {"passes": 3, "distinct": 3, "rule": "distributional", "mono_pairs": 3, "mono_px_max": 10, + "mono_delta_max": 4, "split_pairs": 18, "split_px_max": 10, "split_delta_max": 5, "within": True} + + def det(v): + return case(v, A).get("monolith_determinism", {}) + + def has(v, needle): + return any(needle in r for r in case(v, A).get("reasons", [])) + + # (a) the strict clause stands when the monolith is bit-identical over its 3 passes. + cn.window("det-strict", gate3_args={"picture": {("inproc", A, 2): (10, 131)}}) + rc, text, v = run_reducer(cn.root, "det-strict", tree) + k.expect("bit-identical monolith x3 + a nondeterministic inproc -> %s FAIL (strict clause), GATE3 FAIL" % A, + case(v, A).get("verdict") == "FAIL" and overall(v) == "FAIL" and rc != 0 and det(v).get("rule") == "strict" + and has(v, "inproc repeats NOT bit-identical (2 distinct pictures); the same-session monolith is " + "bit-identical over 3 passes") and case(v, B).get("verdict") == "PASS", + (case(v, A).get("reasons"), det(v))) + + # (b) a nondeterministic monolith, the split pictures inside its spread -> PASS, no adjudication. + cn.window("det-inside", gate3_args={"picture": {**mono, **inside}}) + rc, text, v = run_reducer(cn.root, "det-inside", tree) + k.expect("nondeterministic monolith (3 distinct / 3 passes) + split inside 1.25x -> %s PASS, GATE3 PASS, exit 0" % A, + case(v, A).get("verdict") == "PASS" and overall(v) == "PASS" and rc == 0 + and "GATE3 PASS: 36/36 cases PASS\n" in text, (case(v, A).get("reasons"), overall(v), text[-400:])) + k.expect("...the rule line and the numbers: 10 px / delta 4 over 3 monolith pairs, 10 px / delta 5 over 18 " + "split pairs, bound 12.50 px / 5.00", + {key: det(v).get(key) for key in numbers} == numbers and rule_line in text + and "monolith-vs-monolith max 10 px / delta 4 (3 pairs); split-vs-monolith max 10 px / delta 5 (18 pairs); " + "bound 1.25x = 12.50 px / 5.00: within" in text + and g3(v, "determinism", {}).get("distributional") == [A], (det(v), text[:1500])) + k.expect("...its cross-arm difference needs no gate3/adjudication.tsv line (decided by the rule)", + case(v, A).get("cross_arm", {}).get("identical") is False + and case(v, A).get("cross_arm", {}).get("distributional") is True + and g3(v, "cross_arm_unadjudicated") == [] and "compared by the ID-P7-62 distributional check" in text, + case(v, A).get("cross_arm")) + decoder = det(v).get("decoder", "") + rc, text, v = run_reducer(cn.root, "det-inside", tree, env={"W2_REDUCE_PNG_DECODER": "pure"}) + k.expect("...the stdlib PNG decoder (W2_REDUCE_PNG_DECODER=pure) gives the same numbers (default decoder: %s)" + % decoder, {key: det(v).get(key) for key in numbers} == numbers + and det(v).get("decoder", "").startswith("pure-python") and rc == 0, det(v)) + + # (c) beyond 1.25x: in the per-channel delta, then in the pixel count. + cn.window("det-delta", gate3_args={"picture": {**mono, **inside, ("inproc", A, 3): (10, 134)}}) + rc, text, v = run_reducer(cn.root, "det-delta", tree) + k.expect("...one split picture at delta 6 > 1.25 x 4 -> %s FAIL, GATE3 FAIL" % A, + case(v, A).get("verdict") == "FAIL" and overall(v) == "FAIL" and rc != 0 + and det(v).get("split_delta_max") == 6 and det(v).get("within") is False + and has(v, "split-vs-monolith max per-channel delta 6 > 1.25 x the monolith-vs-monolith max 4 (= 5.00)") + and not has(v, "differing px"), case(v, A).get("reasons")) + cn.window("det-px", gate3_args={"picture": {**mono, **inside, ("inproc", A, 3): (13, 131)}}) + rc, text, v = run_reducer(cn.root, "det-px", tree) + k.expect("...one split picture 13 px off > 1.25 x 10 (delta inside) -> %s FAIL" % A, + case(v, A).get("verdict") == "FAIL" and rc != 0 and det(v).get("split_px_max") == 13 + and det(v).get("split_delta_max") == 4 + and has(v, "split-vs-monolith max 13 differing px > 1.25 x the monolith-vs-monolith max 10 (= 12.50)") + and not has(v, "per-channel delta"), (det(v), case(v, A).get("reasons"))) + + # (d) clause (1) holds against EVERY monolith reading, not one of them. + ssim = {("monolith", A, 1): 0.9978, ("monolith", A, 2): 0.998, ("monolith", A, 3): 0.9982, ("spawn", A, 2): 0.99831} + cn.window("det-ssim", gate3_args={"picture": {**mono, **inside}, "ssim": ssim}) + rc, text, v = run_reducer(cn.root, "det-ssim", tree) + k.expect("...a spawn ssim 0.00051 from ONE monolith reading (0.00011 from another) -> %s FAIL" % A, + case(v, A).get("verdict") == "FAIL" and rc != 0 and det(v).get("within") is True + and case(v, A).get("reasons") == ["spawn rep2 |ssim-monolith|=0.000510 > 0.0005 (max over 3 monolith readings)"], + case(v, A).get("reasons")) + + # (e) the pre-ID-P7-62 archives (monolith x1, no monolith_repeat= in arms.txt): the rule cannot apply. + cn.window("det-mono1", gate3_args={"arms": ARMS_MONO1, "arms_txt": ARMS_TXT_MONO1, "picture": inside}) + rc, text, v = run_reducer(cn.root, "det-mono1", tree) + k.expect("monolith x1 (the earlier 30-gate3.sh) + a nondeterministic split -> %s FAIL naming the >= 3 monolith " + "passes the rule needs" % A, + case(v, A).get("verdict") == "FAIL" and overall(v) == "FAIL" and rc != 0 and g3(v, "monolith_repeat") == 1 + and det(v).get("rule") == "strict (< 3 monolith passes)" + and has(v, "inproc repeats NOT bit-identical (3 distinct pictures); the ID-P7-62 nondeterministic-monolith " + "rule needs >= 3 same-session monolith passes, this session has 1") + and case(v, B).get("verdict") == "PASS", (det(v), case(v, A).get("reasons"))) + + # (f) the monolith pair's own bookkeeping: arms.txt monolith_repeat=3 holds a finished pair to 3. + out = cn.window("det-short") + shutil.rmtree(out / "gate3/archive/monolith" / (A + "-DirectVulkan") / "repeat-03") + rc, text, v = run_reducer(cn.root, "det-short", tree) + k.expect("a finished monolith pair with 2 of arms.txt's monolith_repeat=3 -> %s FAIL" % A, + case(v, A).get("verdict") == "FAIL" and rc != 0 + and has(v, "monolith: 2 repeat(s) in a finished pair < gate3/arms.txt monolith_repeat=3"), case(v, A)) + (out / "gate3/state/monolith" / (A + ".done")).unlink() + rc, text, v = run_reducer(cn.root, "det-short", tree) + k.expect("...the same pair without its .done -> INCOMPLETE (a resume re-runs it)", + case(v, A).get("verdict") == "INCOMPLETE" and overall(v) == "INCOMPLETE" + and "monolith: 2/3 repeats" in case(v, A).get("reasons", []), case(v, A).get("reasons")) + + # (g) --extra-monolith: the g3det E1-mono re-reduction shape (x1 archive + passes outside gate3/). + cn.window("det-extra", gate3_args={"arms": ARMS_MONO1, "arms_txt": ARMS_TXT_MONO1, "picture": inside}) + extra = cn.extra_monolith(cn.root / "extra-unstamped", A, [(10, 132), (10, 130)]) + rc, text, v = run_reducer(cn.root, "det-extra", tree, extra=["%s@%s" % (extra, BOOT)]) + k.expect("x1 archive + 2 extra monolith passes attested @session boot -> the rule applies (3 distinct / 3), " + "%s PASS, GATE3 PASS-WITH-EXTRA-READINGS, exit 1" % A, + case(v, A).get("verdict") == "PASS" and det(v).get("rule") == "distributional" + and overall(v) == "PASS-WITH-EXTRA-READINGS" and rc == 1 + and "GATE3 PASS-WITH-EXTRA-READINGS: 36/36 cases PASS" in text and "NOT a gate verdict" in text + and "monolith 38/38 repeat(s) (2 of them --extra-monolith)" in text, + (overall(v), case(v, A).get("reasons"), det(v), text[-600:])) + rc, text, v = run_reducer(cn.root, "det-extra", tree, extra=[extra]) + s = g3(v, "session", {}) + k.expect("...the same extra passes with no boot_id.txt and no @BOOT_ID -> GATE3 INVALID-SESSION", + overall(v) == "INVALID-SESSION" and rc != 0 + and any("carry no boot_id" in p and "--extra-monolith" in p for p in s.get("problems", [])), s) + rc, text, v = run_reducer(cn.root, "det-extra", tree, extra=["%s@%s" % (extra, OTHER_BOOT)]) + k.expect("...attested @another boot -> GATE3 INVALID-SESSION naming it", + overall(v) == "INVALID-SESSION" and rc != 0 + and any(OTHER_BOOT in p for p in g3(v, "session", {}).get("problems", [])), g3(v, "session")) + stamped = cn.extra_monolith(cn.root / "extra-stamped", A, [(10, 132), (10, 130)], boot=BOOT) + rc, text, v = run_reducer(cn.root, "det-extra", tree, extra=[stamped]) + k.expect("...extra passes whose own boot_id.txt is the session's (no @BOOT_ID) -> PASS-WITH-EXTRA-READINGS", + overall(v) == "PASS-WITH-EXTRA-READINGS" and rc == 1 and case(v, A).get("verdict") == "PASS", overall(v)) + + def pass_cases(cn, b): """$BASE-Pass cases of block b's caselist (not skipped), in caselist order.""" base = cn.base(b) @@ -954,6 +1134,7 @@ def main(): scenario_case_set(k, cn, tree) scenario_cross_arm(k, cn, tree) scenario_unfinished(k, cn, tree) + scenario_determinism(k, cn, tree) scenario_rate_gate(k, cn, tree) scenario_cts_lost(k, cn, tree) scenario_vacuous(k, cn, tree) diff --git a/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce.py b/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce.py index b2a4a462..31cd3834 100644 --- a/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce.py +++ b/docs/Disaggregated/notes/p7/device-window-2/tools/60-reduce.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -"""60-reduce.py [--logroot DIR] [--tools TREE] [--json OUT] +"""60-reduce.py [--logroot DIR] [--tools TREE] [--json OUT] [--extra-monolith DIR[@BOOT_ID] ...] 60-reduce.py --check-block RUN_DIR REPORT_JSON Device window 2 verdicts, read from the window's own output directory (/). @@ -24,13 +24,35 @@ GATE 3 (CONTRACT-P7 7.1/7.2), per case of gate3/cases.txt: every arm, carries one boot_id, equal to session/boot-id.txt. A second boot_id, a record that carries none, or no session/boot-id.txt makes the whole gate GATE3 INVALID-SESSION, whatever the pictures say (the gate is a same-session reading); - * monolith x1 is the same-session control: it must itself pass, and its role logs must show no - 'Config: IPC' / MOBILEGL_TRANSPORT line (the arm really was the monolith); + * the monolith arm (x gate3/arms.txt's monolith_repeat: 3 from ID-P7-62 on; an arms.txt without + the key is the earlier script's x1) is the same-session control: every pass must itself pass, + and its role logs must show no 'Config: IPC' / MOBILEGL_TRANSPORT line (the arm really was the + monolith); a finished monolith pair with fewer passes than monolith_repeat is that case FAIL; * inproc and spawn: the pair finished (state .done), every expected repeat present and error-free, each repeat's arm proof (transport-proof.json passed), the device's own pass verdict (ssim >= case threshold), ALL repeats OF THE ARM bit-identical (actual PNG SHA-256; - within-arm identity is the gate), and |ssim - monolith ssim| <= 0.0005 on every repeat; a - repeat whose logcat is byte-identical to the previous repeat's is flagged STALE; + within-arm identity is the gate), and |ssim - m| <= 0.0005 on every repeat for EVERY monolith + reading m of the session; a repeat whose logcat is byte-identical to the previous repeat's is + flagged STALE; + * NONDETERMINISTIC MONOLITH (ID-P7-62, g3det VERDICT.md section 2): the bit-identity clause + presupposes a bit-reproducible reference. A case whose same-session monolith pictures are NOT + all bit-identical over >= 3 passes has none, so for it the split arms' bit-identity clause is + replaced by the distributional check: (1) the |ssim - m| clause above, for every monolith + reading m; (2) over every split-vs-monolith picture pair (inproc and spawn repeats x monolith + passes) the maximum differing-pixel count (any RGBA channel differs) and the maximum + per-channel delta are each <= 1.25 x the monolith-vs-monolith maximum. The pixels are read + from the archived actual PNGs (numpy + PIL; without them, or with W2_REDUCE_PNG_DECODER=pure, + compare_actuals' stdlib decoder - the same numbers, slower). Such a case prints + 'nondeterministic monolith (N distinct / M passes) -> distributional check' and its numbers, + and its cross-arm difference is decided by (2), not by gate3/adjudication.tsv. A case whose + monolith is bit-identical, or that has fewer than 3 monolith passes (the pre-ID-P7-62 x1 + archives), keeps the strict clause; + * --extra-monolith DIR[@BOOT_ID] (repeatable; an adjudication re-reduction, never the gate): + adds the passes under DIR/-DirectVulkan/repeat-NN (a run_android_retrace_local.py + --archive-dir tree) to the case's monolith readings. Each must be the session's: a repeat's + boot_id.txt, else the BOOT_ID the operator attests for DIR from the run's own boot_id checks; + none, or another boot, is INVALID-SESSION. A reading that uses one is at best + GATE3 PASS-WITH-EXTRA-READINGS, never PASS; * OpenRA: 1.000000 and mismatch 0 on every repeat of both split arms AND on monolith; * cross-arm picture identity (inproc vs spawn vs monolith) is not a per-case gate (ruling: integrator 2026-09-23, ID-P7-59): a mismatch prints a WARN line and leaves the case's verdict @@ -42,8 +64,9 @@ GATE 3 (CONTRACT-P7 7.1/7.2), per case of gate3/cases.txt: * inproc-ra0 (RUN_AHEAD=0): required on every case (one archived repeat with its .done) and its role log must prove run-ahead=0 (else that case FAIL: it is not the control arm); its picture and ssim are recorded, never gating; - * a reading that passes but is not the gate's - a proper subset of the canonical 36, or a - session that is not reboot-clean - is GATE3 PASS-SUBSET / PASS-NOT-REBOOT-CLEAN, never PASS. + * a reading that passes but is not the gate's - a proper subset of the canonical 36, a session + that is not reboot-clean, or one that used --extra-monolith - is GATE3 PASS-SUBSET / + PASS-NOT-REBOOT-CLEAN / PASS-WITH-EXTRA-READINGS, never PASS. BSL STATS: per arm, maps-line / VmRSS / VmHWM peaks and the wbuf[] gauges (information). CTS AFTER (CONTRACT-P7 7.3), per block vs device-window-1/CTS-base/report-.json, over the cases the AFTER run was asked to run (so a --limit subset is compared like for like): @@ -79,15 +102,16 @@ CTS AFTER (CONTRACT-P7 7.3), per block vs device-window-1/CTS-base/report-= 3 repeats, four arms, reboot-clean, one session, every cross-arm mismatch adjudicated) and CTS is PASS (five full blocks); 1 otherwise -(a section that did not run, a PASS-SUBSET / PASS-NOT-REBOOT-CLEAN / PASS-NEEDS-ADJUDICATION -reading, INCOMPLETE / INVALID-SESSION, FAIL-REPEATS / FAIL-ARMS / FAIL-CASESET, or FAIL); 2 on -bad input. +(a section that did not run, a PASS-SUBSET / PASS-NOT-REBOOT-CLEAN / PASS-NEEDS-ADJUDICATION / +PASS-WITH-EXTRA-READINGS reading, INCOMPLETE / INVALID-SESSION, FAIL-REPEATS / FAIL-ARMS / +FAIL-CASESET, or FAIL); 2 on bad input. --check-block RUN_DIR REPORT_JSON: the completeness test 50-cts-after.sh applies before it writes a block's .done (the same code the verdict uses): exit 0 when the report has a result for every non-skipped case of the run's caselist and unrun.txt is empty, 3 when not (the reason is printed). """ import argparse import hashlib +import itertools import json import os import re @@ -96,6 +120,13 @@ from collections import Counter from pathlib import Path TOL = 0.0005 +# ID-P7-62 (g3det VERDICT.md section 2): a case whose same-session monolith is not bit-identical +# over >= MONOLITH_RULE_PASSES passes is judged by the distributional check, whose pixel bound is +# SPREAD_FACTOR x the monolith's own spread. +MONOLITH_RULE_PASSES = 3 +SPREAD_FACTOR = 1.25 +RULING_62 = "ID-P7-62" +UUID = re.compile(r"^(.+)@([0-9a-f]{8}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{12})$") # CONTRACT-P7 7.1/7.2's constants: the gate is held to these, never to what gate3/arms.txt, # gate3/cases.txt or gate3/excluded.txt record about the run (ruling: integrator 2026-09-23 after # codex closeout review). @@ -182,8 +213,9 @@ def read_adjudication(path): # ------------------------------------------------------------------------------------------------ # gate 3 # ------------------------------------------------------------------------------------------------ -def gate3_session(out, g): - """One boot session for every record of every arm (ruling c).""" +def gate3_session(out, g, extras=()): + """One boot session for every record of every arm (ruling c), and of every --extra-monolith + reading (its repeat's boot_id.txt, else the BOOT_ID attested for its directory).""" want = first_line(out / "session" / "boot-id.txt") problems, seen, unstamped = [], {}, [] @@ -210,6 +242,13 @@ def gate3_session(out, g): note(rec.get("boot_id"), where) if "boot_id_before" in rec: note(rec["boot_id_before"], where + " (boot_id_before)") + for extra in extras: + for row in extra["rows"]: + where = "--extra-monolith %s/%s/repeat-%02d" % (extra["dir"], row["arm"], row["repeat"]) + rec = read_record(Path(row["dir"]) / "boot_id.txt") or {} + note(rec.get("boot_id") or extra["boot"], where) + if "boot_id_before" in rec: + note(rec["boot_id_before"], where + " (boot_id_before)") if not want: problems.append("no session/boot-id.txt: 21-preflight.sh records the session's boot_id there") if unstamped: @@ -276,7 +315,108 @@ def px_between(ca, left, right): return "n/a (%s)" % error -def gate3(out, ca): +# ---- ID-P7-62: the pixel spread of a nondeterministic monolith, and the split arms' against it ---- +class NumpyPictures: + """Archived actual PNGs as int16 RGBA arrays (numpy + PIL).""" + name = "numpy+PIL" + + def __init__(self): + import numpy # noqa: F401 - both imported here so a missing one selects the fallback + from PIL import Image + self.np, self.image = numpy, Image + + def load(self, path): + with self.image.open(path) as picture: + return self.np.asarray(picture.convert("RGBA"), dtype=self.np.int16) + + def diff(self, a, b): + """-> (pixels where any RGBA channel differs, the largest per-channel delta).""" + if a.shape != b.shape: + raise ValueError("picture sizes differ: %s vs %s" % (a.shape, b.shape)) + d = self.np.abs(a - b) + return int((d.max(axis=2) > 0).sum()), int(d.max()) + + +class PurePictures: + """The same numbers with compare_actuals' stdlib PNG decoder (no numpy / PIL).""" + name = "pure-python (compare_actuals.read_png_rgba)" + + def __init__(self, ca): + self.ca = ca + + def load(self, path): + return self.ca.read_png_rgba(path) + + def diff(self, a, b): + if (a.width, a.height) != (b.width, b.height): + raise ValueError("picture sizes differ: %dx%d vs %dx%d" % (a.width, a.height, b.width, b.height)) + stride, px, delta = a.width * 4, 0, 0 + for y in range(a.height): + ra, rb = a.pixels[y * stride:(y + 1) * stride], b.pixels[y * stride:(y + 1) * stride] + if ra == rb: + continue + for i in range(0, stride, 4): + if ra[i:i + 4] != rb[i:i + 4]: + px += 1 + delta = max(delta, max(abs(ra[i + c] - rb[i + c]) for c in range(4))) + return px, delta + + +def picture_reader(ca): + """numpy + PIL when importable (and W2_REDUCE_PNG_DECODER != pure), else the stdlib decoder.""" + if os.environ.get("W2_REDUCE_PNG_DECODER", "") != "pure": + try: + return NumpyPictures() + except ImportError: + pass + return PurePictures(ca) + + +def spread(reader, mono, split): + """ID-P7-62 clause (2). mono, split: [(sha, path)] over every reading (a picture repeated in + several readings is decoded and compared once; an identical pair counts as 0 px / delta 0). + -> {mono_pairs, mono_px_max, mono_delta_max, split_pairs, split_px_max, split_delta_max}.""" + cache, memo = {}, {} + + def load(sha, path): + if sha not in cache: + cache[sha] = reader.load(path) + return cache[sha] + + def worst(pairs): + px = delta = 0 + for (sa, pa), (sb, pb) in pairs: + if sa == sb: + continue + key = (sa, sb) if sa < sb else (sb, sa) + if key not in memo: + memo[key] = reader.diff(load(sa, pa), load(sb, pb)) + px, delta = max(px, memo[key][0]), max(delta, memo[key][1]) + return px, delta + mono_pairs = list(itertools.combinations(mono, 2)) + split_pairs = list(itertools.product(split, mono)) + mono_px, mono_delta = worst(mono_pairs) + split_px, split_delta = worst(split_pairs) + return {"mono_pairs": len(mono_pairs), "mono_px_max": mono_px, "mono_delta_max": mono_delta, + "split_pairs": len(split_pairs), "split_px_max": split_px, "split_delta_max": split_delta} + + +def extra_monolith(ca, specs): + """--extra-monolith DIR[@BOOT_ID] -> [{dir, boot, rows}] (rows: compare_actuals.summarize rows, + arm = -DirectVulkan), or raises ValueError on a directory that is not an archive.""" + extras = [] + for spec in specs or []: + m = UUID.match(spec) + path, boot = (m.group(1), m.group(2)) if m else (spec, None) + d = Path(path).expanduser() + if not d.is_dir(): + raise ValueError("--extra-monolith %s: not a directory" % path) + rows = ca.summarize(d)["rows"] + extras.append({"dir": str(d), "boot": boot, "rows": rows}) + return extras + + +def gate3(out, ca, extras=()): g = out / "gate3" cases_file = g / "cases.txt" if not cases_file.is_file(): @@ -289,12 +429,24 @@ def gate3(out, ca): repeat = int(meta.get("repeat", str(CONTRACT_REPEATS))) except ValueError: repeat = 0 + # 30-gate3.sh records monolith_repeat= from ID-P7-62 on (the monolith runs x --repeat); an + # arms.txt without the key was written by the earlier script, which ran the monolith x1. + try: + mono_repeat = int(meta.get("monolith_repeat", "1")) + except ValueError: + mono_repeat = 0 planned = meta.get("arms", "").split() arms_present = [a for a in REQUIRED_ARMS if (g / "archive" / a).is_dir()] summaries = {a: ca.summarize(g / "archive" / a) for a in arms_present} - session = gate3_session(out, g) - identity = {"monolith_repeats": 0, "monolith_proven": 0, "split_repeats": 0, "split_proofs_passed": 0} + session = gate3_session(out, g, extras) + identity = {"monolith_repeats": 0, "monolith_proven": 0, "monolith_extra": 0, "split_repeats": 0, + "split_proofs_passed": 0} adjudicated, adjudication_problems = read_adjudication(g / "adjudication.tsv") + reader = None # the PNG reader of the distributional check, made on first use + extra_rows = {} + for extra in extras: + for row in extra["rows"]: + extra_rows.setdefault(row["arm"], []).append(dict(row, extra=extra["dir"])) # ---- the contract's constants (ruling: integrator 2026-09-23 after codex closeout review) ---- contract = {"repeats": [], "arms": [], "cases": []} @@ -362,26 +514,57 @@ def gate3(out, ca): for case in cases: reasons, incomplete = [], [] entry = {"case": case, "arms": {}} - mono = rows("monolith", case) - mono_row = mono_ssim = mono_sha = None + # The monolith readings: the gate's own x monolith_repeat, then any --extra-monolith pass. + gate_mono = rows("monolith", case) + extra_mono = extra_rows.get(case + "-DirectVulkan", []) if "monolith" in summaries and not finished("monolith", case): incomplete.append("monolith: no state .done (pair unfinished; 30-gate3.sh retries it)") - if len(mono) != 1 or mono[0].get("error"): - incomplete.append("monolith: %s" % mono[0].get("error") if mono else not_run("monolith")) - else: - m = mono_row = mono[0] - mono_ssim, mono_sha = m.get("ssim_vs_golden"), m.get("actual_sha256") + if not gate_mono: + incomplete.append(not_run("monolith")) + elif len(gate_mono) != mono_repeat: + if finished("monolith", case) and len(gate_mono) < mono_repeat: + reasons.append("monolith: %d repeat(s) in a finished pair < gate3/arms.txt monolith_repeat=%d" + % (len(gate_mono), mono_repeat)) + else: + incomplete.append("monolith: %d/%d repeats" % (len(gate_mono), mono_repeat)) + mono_rows, not_monolith = [], [] + for m in gate_mono + extra_mono: + where = "monolith rep%d" % m["repeat"] if not m.get("extra") else \ + "monolith (--extra-monolith %s) rep%d" % (m["extra"], m["repeat"]) + if m.get("error"): + incomplete.append("%s: %s" % (where, m["error"])) + continue + mono_rows.append(m) not_mono = monolith_identity(m) + if not_mono: + not_monolith.append("%s: %s" % (where, not_mono)) identity["monolith_repeats"] += 1 identity["monolith_proven"] += not_mono is None - entry["arms"]["monolith"] = {"ssim": mono_ssim, "sha": mono_sha, "identity": not_mono or "monolith", - "mismatch": m.get("mismatch_pixels_vs_golden"), "passed": m.get("passed")} + identity["monolith_extra"] += bool(m.get("extra")) + m_ssim = m.get("ssim_vs_golden") if not_mono: - reasons.append("monolith arm is NOT proven monolith (%s)" % not_mono) + reasons.append("%s is NOT proven monolith (%s)" % (where, not_mono)) if m.get("passed") is not True: - reasons.append("monolith control did not pass (ssim %s)" % mono_ssim) - if case == OPENRA and not (m.get("mismatch_pixels_vs_golden") == 0 and (mono_ssim or 0) >= 0.9999995): - reasons.append("OpenRA monolith not 1.000000/0 (%s/%s)" % (mono_ssim, m.get("mismatch_pixels_vs_golden"))) + reasons.append("%s: the monolith control did not pass (ssim %s)" % (where, m_ssim)) + if case == OPENRA and not (m.get("mismatch_pixels_vs_golden") == 0 and (m_ssim or 0) >= 0.9999995): + reasons.append("OpenRA %s not 1.000000/0 (%s/%s)" % (where, m_ssim, m.get("mismatch_pixels_vs_golden"))) + mono_row = mono_rows[0] if mono_rows else None + mono_ssims = [m["ssim_vs_golden"] for m in mono_rows if isinstance(m.get("ssim_vs_golden"), (int, float))] + mono_shas = [m["actual_sha256"] for m in mono_rows if m.get("actual_sha256")] + if mono_rows: + entry["arms"]["monolith"] = { + "repeats": len(gate_mono), "extra": len(extra_mono), "ssim": [m.get("ssim_vs_golden") for m in mono_rows], + "sha": sorted(set(mono_shas)), "mismatch": [m.get("mismatch_pixels_vs_golden") for m in mono_rows], + "passed": all(m.get("passed") is True for m in mono_rows), "identity": not_monolith or "monolith"} + # ID-P7-62: is the same-session reference itself bit-reproducible? + det = entry["monolith_determinism"] = {"passes": len(mono_shas), "distinct": len(set(mono_shas))} + distributional = det["passes"] >= MONOLITH_RULE_PASSES and det["distinct"] > 1 + if distributional: + det["rule"] = "distributional" + elif det["passes"] >= MONOLITH_RULE_PASSES: + det["rule"] = "strict" + else: + det["rule"] = "strict (< %d monolith passes)" % MONOLITH_RULE_PASSES split_rows = {} for arm in SPLIT_ARMS: rs = split_rows[arm] = rows(arm, case) @@ -412,19 +595,54 @@ def gate3(out, ca): else: a["proofs_passed"] += 1 identity["split_proofs_passed"] += 1 - if mono_ssim is not None and r.get("ssim_vs_golden") is not None: - d = abs(r["ssim_vs_golden"] - mono_ssim) + if mono_ssims and r.get("ssim_vs_golden") is not None: + # Against EVERY monolith reading of the session (ID-P7-62 clause (1)); with one + # reading, or a bit-identical monolith, this is the contract's single difference. + d = max(abs(r["ssim_vs_golden"] - m) for m in mono_ssims) if d > TOL: - reasons.append("%s rep%d |ssim-monolith|=%.6f > %.4f" % (arm, r["repeat"], d, TOL)) + reasons.append("%s rep%d |ssim-monolith|=%.6f > %.4f%s" % ( + arm, r["repeat"], d, TOL, + "" if len(set(mono_ssims)) == 1 else " (max over %d monolith readings)" % len(mono_ssims))) if case == OPENRA and not (r.get("mismatch_pixels_vs_golden") == 0 and (r.get("ssim_vs_golden") or 0) >= 0.9999995): reasons.append("OpenRA %s rep%d not 1.000000/0 (%s/%s)" % (arm, r["repeat"], r.get("ssim_vs_golden"), r.get("mismatch_pixels_vs_golden"))) shas = [r.get("actual_sha256") for r in rs if r.get("actual_sha256")] - if len(set(shas)) > 1: - reasons.append("%s repeats NOT bit-identical (%d distinct pictures)" % (arm, len(set(shas)))) + if len(set(shas)) > 1 and not distributional: + # The strict clause; under ID-P7-62 the distributional check below replaces it. + if det["passes"] >= MONOLITH_RULE_PASSES: + why = "; the same-session monolith is bit-identical over %d passes" % det["passes"] + else: + why = ("; the %s nondeterministic-monolith rule needs >= %d same-session monolith passes, this " + "session has %d" % (RULING_62, MONOLITH_RULE_PASSES, det["passes"])) + reasons.append("%s repeats NOT bit-identical (%d distinct pictures)%s" % (arm, len(set(shas)), why)) lc = [logcat_sha(r) for r in rs] for i in range(1, len(lc)): if lc[i] and lc[i] == lc[i - 1]: reasons.append("%s rep%d STALE (logcat identical to rep%d)" % (arm, rs[i]["repeat"], rs[i - 1]["repeat"])) + if distributional: + # ID-P7-62 clause (2): the split pictures lie inside the monolith's own spread. + split_valid = [r for arm in SPLIT_ARMS for r in split_rows[arm] if not r.get("error") and r.get("actual")] + split_ssims = [r["ssim_vs_golden"] for r in split_valid if isinstance(r.get("ssim_vs_golden"), (int, float))] + det["max_dssim"] = max((abs(s - m) for s in split_ssims for m in mono_ssims), default=None) + reader = reader or picture_reader(ca) + det["decoder"] = reader.name + try: + det.update(spread(reader, [(m["actual_sha256"], picture(m)) for m in mono_rows if m.get("actual")], + [(r["actual_sha256"], picture(r)) for r in split_valid])) + except Exception as error: # an unreadable / mis-sized picture: no measurement, no pass + det["error"] = "%s: %s" % (type(error).__name__, error) + reasons.append("%s distributional check cannot be measured (%s)" % (RULING_62, det["error"])) + else: + det["px_bound"] = SPREAD_FACTOR * det["mono_px_max"] + det["delta_bound"] = SPREAD_FACTOR * det["mono_delta_max"] + det["within"] = det["split_px_max"] <= det["px_bound"] and det["split_delta_max"] <= det["delta_bound"] + if det["split_px_max"] > det["px_bound"]: + reasons.append("%s: split-vs-monolith max %d differing px > %.2f x the monolith-vs-monolith max %d " + "(= %.2f)" % (RULING_62, det["split_px_max"], SPREAD_FACTOR, det["mono_px_max"], + det["px_bound"])) + if det["split_delta_max"] > det["delta_bound"]: + reasons.append("%s: split-vs-monolith max per-channel delta %d > %.2f x the monolith-vs-monolith " + "max %d (= %.2f)" % (RULING_62, det["split_delta_max"], SPREAD_FACTOR, + det["mono_delta_max"], det["delta_bound"])) # The RUN_AHEAD=0 control arm: required on every case (CONTRACT-P7 7.2 "RUN_AHEAD=0 对照臂一遍 # 记录"), and it must be that arm; its picture is recorded, never gating. ra0 = rows("inproc-ra0", case) @@ -440,16 +658,20 @@ def gate3(out, ca): incomplete.append("inproc-ra0 rep%d: %s" % (r["repeat"], r["error"])) elif entry["arms"]["inproc-ra0"]["proof"] != "run-ahead=0": reasons.append("inproc-ra0 is not proven the RUN_AHEAD=0 arm (%s)" % entry["arms"]["inproc-ra0"]["proof"]) - # Cross-arm identity: not a per-case gate (ruling d), but every mismatch needs an adjudication. + # Cross-arm identity: not a per-case gate (ruling d), but every mismatch needs an adjudication - + # except under ID-P7-62, where the monolith has no one picture to be identical to and clause + # (2) above is the cross-arm judgment. ip = set(entry["arms"].get("inproc", {}).get("sha", [])) sp = set(entry["arms"].get("spawn", {}).get("sha", [])) + mp = set(mono_shas) entry["inproc_eq_spawn"] = bool(ip) and ip == sp - entry["split_eq_monolith"] = bool(ip) and ip == sp == {mono_sha} - x = entry["cross_arm"] = {"monolith": mono_sha, "inproc": sorted(ip), "spawn": sorted(sp), - "identical": (entry["split_eq_monolith"] if (ip and sp and mono_sha) else None)} - if x["identical"] is False: + entry["split_eq_monolith"] = bool(ip) and ip == sp == mp + x = entry["cross_arm"] = {"monolith": sorted(mp), "inproc": sorted(ip), "spawn": sorted(sp), + "identical": (entry["split_eq_monolith"] if (ip and sp and mp) else None), + "distributional": distributional} + if x["identical"] is False and not distributional: first = {arm: picture(split_rows[arm][0]) if split_rows[arm] else None for arm in SPLIT_ARMS} - x["px_vs_golden"] = {"monolith": mono_row.get("mismatch_pixels_vs_golden") if mono_row else None, + x["px_vs_golden"] = {"monolith": [m.get("mismatch_pixels_vs_golden") for m in mono_rows], "inproc": [r.get("mismatch_pixels_vs_golden") for r in split_rows["inproc"]], "spawn": [r.get("mismatch_pixels_vs_golden") for r in split_rows["spawn"]]} x["px_direct"] = {"inproc-monolith": px_between(ca, first["inproc"], picture(mono_row)), @@ -463,7 +685,8 @@ def gate3(out, ca): contract["repeats"].append("%d finished inproc/spawn pair(s) archived fewer than CONTRACT-P7 7.2's %d repeats " "(arms.txt repeat=%s): %s%s" % (len(short), CONTRACT_REPEATS, meta.get("repeat", "?"), ", ".join(short[:4]), ", ..." if len(short) > 4 else "")) - mismatched = [e["case"] for e in results if e["cross_arm"]["identical"] is False] + mismatched = [e["case"] for e in results if e["cross_arm"]["identical"] is False + and not e["cross_arm"]["distributional"]] unadjudicated = [c for c in mismatched if c not in adjudicated] stale = sorted(c for c in adjudicated if c not in set(mismatched)) verdicts = [e["verdict"] for e in results] @@ -479,6 +702,10 @@ def gate3(out, ca): if unadjudicated: not_a_gate.append("%d cross-arm mismatch(es) without a gate3/adjudication.tsv line (%s): %s%s" % ( len(unadjudicated), CODEX_RULING, ", ".join(unadjudicated[:3]), ", ..." if len(unadjudicated) > 3 else "")) + if extras: + not_a_gate.append("%d extra monolith reading(s) from outside gate3/archive (--extra-monolith %s): an " + "adjudication re-reduction, NOT a gate verdict" % ( + sum(len(x["rows"]) for x in extras), ", ".join(x["dir"] for x in extras))) if not session["valid"]: overall = "INVALID-SESSION" elif contract["repeats"]: @@ -495,11 +722,20 @@ def gate3(out, ca): overall = "PASS-NOT-REBOOT-CLEAN" elif unadjudicated: overall = "PASS-NEEDS-ADJUDICATION" + elif extras: + overall = "PASS-WITH-EXTRA-READINGS" elif "FAIL" in verdicts: overall = "FAIL" else: overall = "INCOMPLETE" - return {"cases": results, "excluded": excluded, "repeat": repeat, "denominator": len(cases), + rule_of = [(e["case"], e["monolith_determinism"]["rule"]) for e in results] + return {"cases": results, "excluded": excluded, "repeat": repeat, "monolith_repeat": mono_repeat, + "determinism": {"distributional": [c for c, r in rule_of if r == "distributional"], + "strict": [c for c, r in rule_of if r == "strict"], + "strict_under_3_passes": [c for c, r in rule_of if r.startswith("strict (")]}, + "extra_monolith": [{"dir": x["dir"], "boot_attested": x["boot"], "repeats": len(x["rows"]), + "cases": sorted({r["arm"] for r in x["rows"]})} for x in extras], + "denominator": len(cases), "overall": overall, "not_a_gate": not_a_gate, "arms_present": arms_present, "arms_planned": planned, "contract": contract, "canonical": canonical, "canonical_problems": canonical_problems, "cross_arm_mismatched": mismatched, "cross_arm_unadjudicated": unadjudicated, @@ -509,11 +745,15 @@ def gate3(out, ca): def print_gate3(g3): - print("== GATE 3 (DirectVulkan x pbuffer; split repeat=%d, contract >= %d; tol |ssim-monolith| <= %.4f) ==" - % (g3["repeat"], CONTRACT_REPEATS, TOL)) + print("== GATE 3 (DirectVulkan x pbuffer; split repeat=%d, contract >= %d; monolith repeat=%d; " + "tol |ssim-monolith| <= %.4f) ==" % (g3["repeat"], CONTRACT_REPEATS, g3["monolith_repeat"], TOL)) s = g3["session"] print("-- session: boot_id %s; %d record(s) stamped; %s" % (s["session_boot_id"] or "?", s["records"], s["reboot_clean"] or "no session/reboot-clean.txt")) + for x in g3["extra_monolith"]: + print("-- extra monolith readings (--extra-monolith, NOT the gate's own archive): %s: %d repeat(s) over %d " + "case(s); unstamped repeats attested boot_id %s" % (x["dir"], x["repeats"], len(x["cases"]), + x["boot_attested"] or "(none)")) for problem in s["problems"]: print(" ! INVALID-SESSION: " + problem) c = g3["contract"] @@ -529,7 +769,8 @@ def print_gate3(g3): print("WARN gate3/excluded.txt [%s] is not CONTRACT-P7 7.1's [%s] (the case set above is held to the contract's)" % (" ".join(g3["excluded"]), " ".join(CONTRACT_EXCLUDED))) w = max([len(e["case"]) for e in g3["cases"]] + [4]) - print("%-*s %-10s %-11s %-24s %-24s %-11s %s" % (w, "case", "verdict", "monolith", "inproc(min..max) #sha", "spawn(min..max) #sha", "ra0", "i==s==m")) + print("%-*s %-10s %-24s %-24s %-24s %-11s %s" % (w, "case", "verdict", "monolith(min..max) #sha", + "inproc(min..max) #sha", "spawn(min..max) #sha", "ra0", "i==s==m")) for e in g3["cases"]: def cell(arm): a = e["arms"].get(arm) @@ -539,39 +780,63 @@ def print_gate3(g3): if not vals: return "err" return "%.6f..%.6f #%d" % (min(vals), max(vals), len(a["sha"])) - mono = e["arms"].get("monolith", {}).get("ssim") ra0 = e["arms"].get("inproc-ra0", {}).get("ssim") - print("%-*s %-10s %-11s %-24s %-24s %-11s %s" % ( - w, e["case"], e["verdict"], "%.6f" % mono if isinstance(mono, (int, float)) else "-", + print("%-*s %-10s %-24s %-24s %-24s %-11s %s" % ( + w, e["case"], e["verdict"], cell("monolith"), cell("inproc"), cell("spawn"), "%.6f" % ra0 if isinstance(ra0, (int, float)) else "-", "yes" if e["split_eq_monolith"] else ("i==s" if e["inproc_eq_spawn"] else "no"))) + det = e["monolith_determinism"] + if det["rule"] == "distributional": + print("%-*s nondeterministic monolith (%d distinct / %d passes) -> distributional check (%s)" % ( + w, "", det["distinct"], det["passes"], RULING_62)) + if "error" not in det: + print("%-*s monolith-vs-monolith max %d px / delta %d (%d pairs); split-vs-monolith max %d px / " + "delta %d (%d pairs); bound %.2fx = %.2f px / %.2f: %s; max |ssim - monolith| %s; decoder %s" % ( + w, "", det["mono_px_max"], det["mono_delta_max"], det["mono_pairs"], det["split_px_max"], + det["split_delta_max"], det["split_pairs"], SPREAD_FACTOR, det["px_bound"], + det["delta_bound"], "within" if det["within"] else "OUTSIDE", + "-" if det["max_dssim"] is None else "%.1e" % det["max_dssim"], det["decoder"])) for reason in e["reasons"]: print("%-*s ! %s" % (w, "", reason)) + dt = g3["determinism"] + print("-- monolith determinism (%s; same-session monolith passes): %d case(s) bit-identical over >= %d passes " + "(strict clause), %d nondeterministic -> distributional check%s, %d with < %d passes (strict clause; the " + "rule cannot apply)" % (RULING_62, len(dt["strict"]), MONOLITH_RULE_PASSES, len(dt["distributional"]), + " (%s)" % ", ".join(dt["distributional"]) if dt["distributional"] else "", + len(dt["strict_under_3_passes"]), MONOLITH_RULE_PASSES)) ra0s = [(e["case"], e["arms"]["inproc-ra0"]) for e in g3["cases"] if "inproc-ra0" in e["arms"]] print("-- RUN_AHEAD=0 control (required on every case, picture recorded, not gating): %d/%d case(s); proofs: %s" % ( len(ra0s), len(g3["cases"]), ", ".join(sorted({r["proof"] for _, r in ra0s})) or "-")) i = g3["identity"] - print("-- arm identity: monolith %d/%d repeat(s) with no Config: IPC / MOBILEGL_TRANSPORT line; " - "inproc+spawn transport-proof passed %d/%d" % (i["monolith_proven"], i["monolith_repeats"], - i["split_proofs_passed"], i["split_repeats"])) + print("-- arm identity: monolith %d/%d repeat(s)%s with no Config: IPC / MOBILEGL_TRANSPORT line; " + "inproc+spawn transport-proof passed %d/%d" % ( + i["monolith_proven"], i["monolith_repeats"], + " (%d of them --extra-monolith)" % i["monolith_extra"] if i["monolith_extra"] else "", + i["split_proofs_passed"], i["split_repeats"])) judged = [e for e in g3["cases"] if e["cross_arm"]["identical"] is not None] adj = g3["adjudication"] + distributional = [e for e in judged if e["cross_arm"]["distributional"] and not e["cross_arm"]["identical"]] print("-- cross-arm picture identity (NOT a per-case gate, %s; every mismatch needs a gate3/adjudication.tsv " - "line, %s): %d/%d case(s) inproc==spawn==monolith; %d mismatch(es), %d unadjudicated" % ( + "line, %s): %d/%d case(s) inproc==spawn==monolith; %d mismatch(es), %d unadjudicated; %d nondeterministic-" + "monolith case(s) compared by the %s distributional check instead" % ( RULING, CODEX_RULING, sum(e["cross_arm"]["identical"] for e in judged), len(judged), - len(g3["cross_arm_mismatched"]), len(g3["cross_arm_unadjudicated"]))) + len(g3["cross_arm_mismatched"]), len(g3["cross_arm_unadjudicated"]), len(distributional), RULING_62)) def px(v): if isinstance(v, list): nums = [n for n in v if isinstance(n, int)] return "%d..%d" % (min(nums), max(nums)) if nums else "-" return "-" if v is None else str(v) + for e in distributional: + print(" note: cross-arm %s: nondeterministic monolith (%d distinct pictures): the arms are compared by the " + "%s distributional check above, not by gate3/adjudication.tsv" % ( + e["case"], e["monolith_determinism"]["distinct"], RULING_62)) for e in judged: - if not e["cross_arm"]["identical"]: + if not e["cross_arm"]["identical"] and not e["cross_arm"]["distributional"]: x = e["cross_arm"] g, d = x["px_vs_golden"], x["px_direct"] print("WARN cross-arm %s: monolith %s | inproc %s | spawn %s" % ( - e["case"], (x["monolith"] or "-")[:12], ",".join(v[:12] for v in x["inproc"]) or "-", + e["case"], ",".join(v[:12] for v in x["monolith"]) or "-", ",".join(v[:12] for v in x["inproc"]) or "-", ",".join(v[:12] for v in x["spawn"]) or "-")) print(" px!=golden (archived mismatchPixels) monolith %s, inproc %s, spawn %s; px between the arms' " "first repeats: inproc-monolith %s, spawn-monolith %s, inproc-spawn %s" % ( @@ -581,9 +846,14 @@ def print_gate3(g3): else "UNADJUDICATED: no gate3/adjudication.tsv line")) for problem in adj["problems"]: print("WARN " + problem) - if adj["stale"]: + by_rule = set(g3["determinism"]["distributional"]) + agree = [c for c in adj["stale"] if c not in by_rule] + if agree: print(" note: gate3/adjudication.tsv names case(s) whose arms agree (nothing to adjudicate): " - + ", ".join(adj["stale"])) + + ", ".join(agree)) + if len(agree) != len(adj["stale"]): + print(" note: gate3/adjudication.tsv names nondeterministic-monolith case(s) the %s distributional check " + "decides (the line is not used): %s" % (RULING_62, ", ".join(c for c in adj["stale"] if c in by_rule))) print("-- excluded (red on monolith, CONTRACT-P7 7.1): " + (", ".join(g3["excluded"]) or "none")) n = len(g3["cases"]) npass = sum(e["verdict"] == "PASS" for e in g3["cases"]) @@ -922,6 +1192,10 @@ def main(): ap.add_argument("--json", help="write every section as JSON here (default /verdict.json)") ap.add_argument("--check-block", nargs=2, metavar=("RUN_DIR", "REPORT_JSON"), help="only test one block's completeness (50-cts-after.sh, before it writes .done)") + ap.add_argument("--extra-monolith", action="append", metavar="DIR[@BOOT_ID]", + help="add DIR/-DirectVulkan/repeat-NN as extra same-session monolith readings (%s " + "adjudication re-reduction; never PASS); @BOOT_ID attests the session of the repeats that " + "carry no boot_id.txt" % RULING_62) args = ap.parse_args() if args.check_block: return check_block(Path(args.check_block[0]), Path(args.check_block[1])) @@ -941,7 +1215,12 @@ def main(): import compare_actuals as ca base_dir = Path(tools) / "docs/Disaggregated/notes/p7/device-window-1/CTS-base" report = {"stamp": args.stamp, "out": str(out)} - g3 = gate3(out, ca) + try: + extras = extra_monolith(ca, args.extra_monolith) + except ValueError as error: # (compare_actuals.ImageError is one) + print(str(error), file=sys.stderr) + return 2 + g3 = gate3(out, ca, extras) if g3: print_gate3(g3) else: diff --git a/docs/Disaggregated/notes/p7/device-window-2/tools/window.sh b/docs/Disaggregated/notes/p7/device-window-2/tools/window.sh old mode 100755 new mode 100644 index a7bf6e83..2f8489c9 --- a/docs/Disaggregated/notes/p7/device-window-2/tools/window.sh +++ b/docs/Disaggregated/notes/p7/device-window-2/tools/window.sh @@ -5,7 +5,7 @@ # 10-build.sh APK + host artefacts, stamp (default p7w7-) host only # 21-preflight.sh record found state, reboot-clean (unless --no-reboot), stay-on, pin # 20-install.sh adb install -r, on-device base.apk sha256 == built APK, dex2oat idle -# 30-gate3.sh 36 cases x {monolith x1, inproc x3, spawn x3, inproc RUN_AHEAD=0 x1} +# 30-gate3.sh 36 cases x {monolith x3, inproc x3, spawn x3, inproc RUN_AHEAD=0 x1} # 40-bsl-stats.sh bsl-esc-menu x {inproc, spawn} with MOBILEGL_PIPE_STATS + maps sampler # 50-cts-after.sh five KHR-GL46 blocks, inproc x DirectVulkan, AFTER lib deployed to mgcts # 60-reduce.py gate-3 verdict per case, bsl peaks, CTS delta table + new-crash list