mirror of
https://github.com/Druthulu/BFM-decomp
synced 2026-09-26 21:36:06 -04:00
chore(phase-33): A5 prep — tools/verify_contract.sh (the recorded contract run: per-step logs ending EXIT=rc, abort on first red, contract-line asserts, SUMMARY.md), .run/P33/verify/ allowlisted, audit_frontier's denominator lines DERIVED (1,258 stubs = main's LINKED regions, 0 game-code; disc UNCLAIMED from the ledger; the typed '39 modules / missing oracle' caveat was stale since P30/P31)
This commit is contained in:
Drew T
+10
@@ -328,6 +328,16 @@ unsloth_compiled_cache/
|
||||
/.run/P32/t4d/bank/*
|
||||
!/.run/P32/t4d/bank/*.c
|
||||
# P32 T4c hand pass (S85, 2026-09-06): the two main rows' variants, rtu logs, notes, reproducers, bank bodies, slates, gate/R22 logs (not dumps_*/ or rtu/)
|
||||
# P33 A5 (S87, 2026-09-06): THE recorded contract run — tools/verify_contract.sh's per-step logs, the two link
|
||||
# maps of the with/without-SDK dual and SUMMARY.md (quoted by docs/verification.md). Evidence, tracked.
|
||||
!/.run/P33/
|
||||
/.run/P33/*
|
||||
!/.run/P33/verify/
|
||||
/.run/P33/verify/*
|
||||
!/.run/P33/verify/*.log
|
||||
!/.run/P33/verify/*.map
|
||||
!/.run/P33/verify/*.md
|
||||
!/.run/P33/verify/*.txt
|
||||
!/.run/P32/t4e/
|
||||
/.run/P32/t4e/*
|
||||
!/.run/P32/t4e/*.c
|
||||
|
||||
+14
-5
@@ -43,6 +43,7 @@ import collections
|
||||
import glob
|
||||
import json
|
||||
import os
|
||||
import re
|
||||
import sys
|
||||
|
||||
REPO = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
|
||||
@@ -186,11 +187,19 @@ def main():
|
||||
else:
|
||||
print("All views agree with the corpus oracle.")
|
||||
print()
|
||||
print("SCOPE CAVEAT (R34/R36, printed deliberately): agreement here does NOT mean the")
|
||||
print("denominator is complete. Every view above — and the byte-gate itself — is blind to code")
|
||||
print("that was never onboarded. Open: the 39 un-onboarded type-1 modules")
|
||||
print("(docs/disc-completeness.md) and main's missing independent boundary oracle")
|
||||
print("(docs/second-oracle.md). No 100% claim is meaningful until those resolve.")
|
||||
# The denominator facts, DERIVED (P33 A5, S87): this used to be a typed caveat naming "the 39 un-onboarded
|
||||
# modules" and "main's missing oracle" — both resolved in P30/P31 while the text stayed. R51.
|
||||
linked = {f"src/{seg}.c" for seg in progress._main_linked_segs_from_makefile()}
|
||||
n_linked_stubs = sum(1 for b, st in ref.items() if b == "main" for x in st if getattr(x, "path", "") in linked)
|
||||
n_total = total_open
|
||||
print(f"DENOMINATOR (R34/R36): agreement above says nothing about code never onboarded, so:")
|
||||
print(f" stubs {n_total} total, {n_linked_stubs} inside main's LINKED (Sony-object) regions by design, "
|
||||
f"{n_total - n_linked_stubs} game-code stubs open")
|
||||
ledger = os.path.join(REPO, "docs/disc-ledger.md")
|
||||
m = re.search(r"## Code payloads — (\d+) UNCLAIMED of (\d+)", open(ledger, encoding="utf-8").read()) if os.path.exists(ledger) else None
|
||||
print(f" disc: {m.group(1) + ' UNCLAIMED of ' + m.group(2) + ' code payloads (docs/disc-ledger.md, from make audit-disc)' if m else 'docs/disc-ledger.md ABSENT — run make audit-disc'}")
|
||||
sig_main = os.path.join(REPO, ".run/sig.main.jsonl")
|
||||
print(f" main's build-derived boundary sig: {'present' if os.path.exists(sig_main) else 'ABSENT — run make sig-main'} (.run/sig.main.jsonl; the Ghidra sig is the second, independent oracle)")
|
||||
return 1 if (problems and a.strict) else 0
|
||||
|
||||
|
||||
|
||||
@@ -0,0 +1,104 @@
|
||||
#!/usr/bin/env bash
|
||||
# tools/verify_contract.sh — THE recorded verification run of the byte-identity contract (P33 A5).
|
||||
#
|
||||
# tools/verify_contract.sh # runs every step on the COMMITTED tree -> .run/P33/verify/
|
||||
#
|
||||
# One log per step, NN_<name>.log, each ending in "EXIT=<rc>" + a UTC timestamp (the P32 r22_check.log shape);
|
||||
# the run ABORTS on the first non-zero exit (R53: a later green step must never paper over an earlier red one),
|
||||
# and every step is also asserted by the contract line it must print — a zero exit without the line is a FAIL
|
||||
# (R49). SUMMARY.md is generated from the logs at the end and is what docs/verification.md §2 quotes.
|
||||
#
|
||||
# Steps: 00 tree (HEAD + porcelain: only the R23 ghidra/ churn may be dirty) · 01 make check-env · 02 the family map
|
||||
# regen · 03 the R22 clean fleet (make clean && extract-all && check-all) · 04 make sdk-dual (needs the SDK objects;
|
||||
# SKIPPED with a recorded line without them — a public clone's default build IS the without leg) · 05 make
|
||||
# tools-health · 06 make audit-frontier · 07 make audit-disc (needs the 4-track disc in disks/) · 08 make report.
|
||||
# Wall: ≈1 h (the fleet rebuild dominates). Nothing here needs Ghidra.
|
||||
set -uo pipefail
|
||||
REPO="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
|
||||
cd "$REPO"
|
||||
OUT="$REPO/.run/P33/verify"; mkdir -p "$OUT"
|
||||
JOBS="${JOBS:-16}"
|
||||
NPROC="$(nproc)"
|
||||
say() { printf 'verify_contract: %s\n' "$*"; }
|
||||
|
||||
# run_step NN name expected-regex command... (expected-regex may be "" = exit code only)
|
||||
run_step() {
|
||||
local nn="$1" name="$2" expect="$3"; shift 3
|
||||
local log="$OUT/${nn}_${name}.log"
|
||||
say "step $nn $name: $*"
|
||||
{ printf '# %s\n# cmd: %s\n# started: %s\n' "$name" "$*" "$(date -u +%Y-%m-%dT%H:%M:%SZ)"; } > "$log"
|
||||
local t0=$SECONDS
|
||||
"$@" >> "$log" 2>&1
|
||||
local rc=$?
|
||||
printf 'EXIT=%s wall=%ss finished: %s\n' "$rc" "$((SECONDS - t0))" "$(date -u +%Y-%m-%dT%H:%M:%SZ)" >> "$log"
|
||||
if [ "$rc" != 0 ]; then say "step $nn $name FAILED (rc=$rc) — see $log; aborting (R53)"; summary "ABORTED at $nn"; exit 1; fi
|
||||
if [ -n "$expect" ] && ! grep -qE -- "$expect" "$log"; then
|
||||
say "step $nn $name exited 0 but did not print /$expect/ — FAIL (R49); aborting"; summary "ABORTED at $nn (missing contract line)"; exit 1
|
||||
fi
|
||||
say "step $nn $name OK (rc=0, $((SECONDS - t0)) s)"
|
||||
}
|
||||
|
||||
summary() {
|
||||
local verdict="$1" s="$OUT/SUMMARY.md"
|
||||
{
|
||||
echo "# .run/P33/verify/SUMMARY.md — the recorded contract run (generated by tools/verify_contract.sh; never edit)"
|
||||
echo
|
||||
echo "- **Tree:** \`$(git rev-parse HEAD)\` ($(git log -1 --format=%cs)) · **Host:** $(uname -sr), $NPROC CPUs, JOBS=$JOBS · **Run:** $(date -u +%Y-%m-%dT%H:%M:%SZ)"
|
||||
echo "- **Verdict:** $verdict"
|
||||
echo
|
||||
echo "| # | Step | EXIT | wall | contract line |"
|
||||
echo "|---|---|---|---|---|"
|
||||
for f in "$OUT"/[0-9][0-9]_*.log; do
|
||||
[ -f "$f" ] || continue
|
||||
local b; b="$(basename "$f" .log)"
|
||||
local ex; ex="$(grep -oE '^EXIT=[0-9]+' "$f" | tail -1 | cut -d= -f2)"
|
||||
local w; w="$(grep -oE 'wall=[0-9]+s' "$f" | tail -1 | cut -d= -f2)"
|
||||
local line; line="$(grep -E "${LINES[${b#*_}]:-__none__}" "$f" | tail -1 | sed 's/|/\\|/g' | cut -c1-140)"
|
||||
echo "| ${b%%_*} | \`${b#*_}\` | ${ex:-?} | ${w:-?} | ${line:-—} |"
|
||||
done
|
||||
} > "$s"
|
||||
say "SUMMARY written: $s"
|
||||
}
|
||||
|
||||
# the contract line each step must print (also used by summary to quote it)
|
||||
declare -A LINES=(
|
||||
[tree]='^HEAD '
|
||||
[check-env]='check-env: OK'
|
||||
[family-hseq]='family_hseq'
|
||||
[r22-clean-fleet]='check-all: 218 passed, 0 failed of 218'
|
||||
[sdk-dual]='sdk-dual: (OK|SKIPPED)'
|
||||
[tools-health]='tools-health: OK'
|
||||
[audit-frontier]='audit-frontier|frontier'
|
||||
[audit-disc]='UNCLAIMED code payloads: 0'
|
||||
[report]='FLEET distinct-code\(uniq\): .* = 100\.0%'
|
||||
)
|
||||
|
||||
step_tree() {
|
||||
echo "HEAD $(git rev-parse HEAD) $(git log -1 --format='%cs %s' | cut -c1-100)"
|
||||
local dirty; dirty="$(git status --porcelain | grep -v ' ghidra/' || true)"
|
||||
if [ -n "$dirty" ]; then echo "DIRTY (beyond the R23 ghidra/ churn):"; echo "$dirty"; return 1; fi
|
||||
echo "porcelain clean apart from ghidra/ ($(git status --porcelain | grep -c ' ghidra/' || true) churn lines)"
|
||||
}
|
||||
step_family() { .venv/bin/python tools/family_hseq.py && echo "family_hseq regenerated: $(.venv/bin/python -c 'import json;d=json.load(open(".run/family_hseq.json"));print(len(d.get("binaries",[])),"binaries scanned,",d.get("open_instances"),"open instances")')"; }
|
||||
step_fleet() { make clean && make -j"$NPROC" extract-all JOBS="$JOBS" && make -j"$NPROC" check-all JOBS="$JOBS"; }
|
||||
step_sdk_dual() {
|
||||
local d1 d2; d1="$(make -s print-LIBCD_ELF)"; d2="$(make -s print-LIBPAD_ELF)"
|
||||
if [ -d "$d1" ] && [ -d "$d2" ]; then make -j"$NPROC" sdk-dual; else echo "sdk-dual: SKIPPED — no SDK objects on this machine ($d1 / $d2); the default build IS the without-SDK leg"; fi
|
||||
}
|
||||
step_tools_health() { make -j"$NPROC" tools-health && ! grep -q '\[warn\]' "$OUT/05_tools-health.log"; }
|
||||
step_report() { make report && cat docs/progress.fleet.md | head -12; }
|
||||
|
||||
say "recorded run -> $OUT (HEAD $(git rev-parse --short HEAD))"
|
||||
run_step 00 tree "${LINES[tree]}" step_tree
|
||||
run_step 01 check-env "${LINES[check-env]}" make check-env
|
||||
run_step 02 family-hseq "${LINES[family-hseq]}" step_family
|
||||
run_step 03 r22-clean-fleet "${LINES[r22-clean-fleet]}" step_fleet
|
||||
run_step 04 sdk-dual "${LINES[sdk-dual]}" step_sdk_dual
|
||||
run_step 05 tools-health "${LINES[tools-health]}" step_tools_health
|
||||
run_step 06 audit-frontier "${LINES[audit-frontier]}" make audit-frontier
|
||||
run_step 07 audit-disc "${LINES[audit-disc]}" make audit-disc
|
||||
run_step 08 report "${LINES[report]}" step_report
|
||||
# the report must also say 0 stubs and 0 open near-misses
|
||||
grep -qE 'INCLUDE_ASM stubs *: *0' "$OUT/08_report.log" || { say "report: INCLUDE_ASM stubs line is not 0 — FAIL"; summary "FAILED at 08 (stubs)"; exit 1; }
|
||||
summary "PASS — every step EXIT=0 with its contract line"
|
||||
say "PASS"
|
||||
Reference in New Issue
Block a user