Files
BFM-decomp/phase-ends/current/logs/T2.md
T

5.7 KiB
Raw Blame History

T2 log — cast and lying gate instruments, reinterpret-macro set (Phase 3.39)

Expert: expert-fable (Fable 5.1, effort high). Start commit 0830f6374d.

Timeline

  1. Read card slice, plan Context/Interfaces/Cookbook/Research, T2 entry, tasks/T1.md. Read include/common.h (3.4 KB), docs/gen3-standards.md (11 KB), cookbook/C0507.md.
  2. Finding against plan Context: the legacy reinterpret macros LOBU/LOH/HIH/LOHU/HIHU/LOW/LOWU DO exist, include/common.h:55-61 (Phase 37 T3), unused in src (grep: only the defines). The retriever note "none in include/" was wrong.
  3. Finding: .run/P37/restruct/ledger.jsonl holds 0 rung-S rows and 0 KEPT( sites (173,459 rows: D 173,185, L 274). No existing kept site is ledgered; byte proofs had to use raw sites chosen by cause class.
  4. Three retriever-code questions (no reports written; answers inline): type_census internals (forms :133-140, find_sites :275, selftest :1767, main :1879, TOOL_STAMP :55 keys the walk cache, lazy import restruct :1853); restruct ledger schema (rung-S row: tu, unit=fn, verdict S2/KEPT-ALL, sites[] {form,line,base ":",off,width,sign,access,type,field,verdict "KEPT()"}, pass_hint classes :563-591 incl. SCHED-ALIAS/ALIGNMENT/WIDTH, no SIGN/NON-STRUCT; macro_probe() :4245 proves LOBU..LOWU only under --selftest --real); lever_census internals (no pass/instrument parse exists; --strict :1190-1204 fails on every A/B site regardless of marker, pt>0, direct GTE; selftest is an ok flag, not a checks list).
  5. Hook blocked sed on tools/*.py ("learn a tool from --help, never its source"); source facts came from retriever-code instead.
  6. Picked byte-proof sites with a scratch filter over .run/P39/census/sites.jsonl (scratchpad pick.py, not kept): SIGN ov_SC01_000_after.c:2682 (same base+off read s16 and u16 in func_801523F4), WIDTH ov_SC01_000_jr_801734BC.c:2582 (two widths at param_1+8 in func_801749C8), MISALIGNED ov_SC01_000_jr_8012ACE0.c:2624 (*(int *)(param_1 + 6)), NON-STRUCT ov_SC01_000_jr_8012ACE0.c:795 (bclass other), SCHED-ALIAS ov_SC05_010_jr_80180F84.c:3006 (func_801814AC +0x34 store, cookbook §458 exemplar).
  7. Coder c1 (common.h ONE edit + 5 proofs + R22) and c2 (lever_census --residue) in parallel; c3 (type_census --check-casts) after c1's commit.
  8. Expert edit: docs/gen3-standards.md §2 rule 5 + definition-of-done clause (one file, ~15 lines).
  9. Verify (two calls, > 285 s together): .run/logs/t2_verify_a.log (selftests + check-structs, rc 0), .run/logs/t2_verify_b.log (check-casts, rc 1 as required). kit-corpus + tools-health: .run/logs/t2_kit.log.

Decisions (judgment items)

  • Raw = forms P/I/X/M (M2C_FIELD stays raw). Backed = a site spelled by a registered macro whose restruct.ledger_latest[("S", tu, fn)] row has verdict KEPT/S2/KEPT-ALL and a sites[] entry KEPT(<class>) matching off + ":" (REINTERP: line). One filter, R100.
  • Cause classes: SCHED-ALIAS, SIGN, WIDTH (overlap loser), MISALIGNED, NON-STRUCT, plus REINTERP for the legacy lvalue set. Macro names CAST_ALIAS/CAST_SIGN/CAST_WIDTH/CAST_MISALIGNED/CAST_NONSTRUCT, all (T, p, k) → (*(T *)((p) + (k))).
  • Legacy LOBU..LOWU: reinstated as the set's sixth class rather than retired (a form-I lvalue reinterpretation has no other honest spelling); byte proof = restruct's macro_probe (selftest --real 82/82 at b5e18e5f83, T1), no new site proof.
  • Definition lines of registered macros in include/common.h (incl. M2C_FIELD:43) are not sites: M reads 19,542 (T1 19,543 − common.h's own define); P stays 408,974 despite five new *(T *)( define lines.
  • Byte-proof sites were restored after IDENTICAL (tree keeps 0 macro sites, unbacked 0): keeping them would have left 5 unledgered macro sites for the next task; the proof lines live in logs/T2.c1.md.
  • Reading A: --residue rows excluded from --strict failures only, counted in every total; residue-unused rows printed (stale rows visible).

Coder briefs

  • T2.c1 → 247422bb83 (logs/T2.c1.md): common.h:62-78; proofs make check BINARY=ov_SC01_000 → BYTE-IDENTICAL sha1 9052dc0e…, make check BINARY=ov_SC05_010 → BYTE-IDENTICAL sha1 9b5a70f9…; R22 make clean && make extract-all JOBS=16 && make check-all JOBS=16 → 218 passed 0 failed (.run/logs/t2_r22.log). Deviation: 4 src files restored, not 3; discussions/INDEX.md (pre-modified) auto-staged into the commit.
  • T2.c2 → 313ee50403 (logs/T2.c2.md): lever_census.py load_residue, strict_failures() :1109-1148, selftest controls i-iv :1194-1209, --residue :1219, main :1249-1265; config/lever_residue.tsv header. Live: pins 1868, asm 1411, gte-levers 450, direct GTE 6717, per-TU asm macro defs 314, …, residue 0, residue-unused 0 — FAIL rc 1 (.run/logs/t2c2_strict.log). Deviation: per-TU asm macro defs not matchable by residue (mdefs_all local to run_census) → one synthetic asm-macro fail entry while pt>0.
  • T2.c3 → 7845da8f03 (logs/T2.c3.md): type_census.py KEPT_MACROS/FORM_K :141-147, form-K pass :374-394, defline drop :612-620, check_casts_inputs/check_casts_verdict, --check-casts; selftest 32 → 50 checks; config/lying_exceptions.tsv header. Live: check-casts: raw P=408974 I=60666 X=13800 M=19542; macros none (unbacked 0); lying=229 (ledgered 0) rc 1 (.run/logs/t2c3_casts.log). Caches: .run/P37/census/cache/walk_cache.json and .run/P39/census/cache removed; rebuilt under the new TOOL_STAMP.

Hypotheses rejected

  • "Legacy LOBU..LOWU absent from include/" (plan Context) — false, present at common.h:55-61.
  • "Existing kept sites in the ledger can serve as proofs" — ledger has no rung-S rows; proofs used class-picked raw sites.

Commands (.run/logs)

t2_proof_sc01, t2_proof_sc05, t2_r22 (c1); t2c2_strict (c2); t2c3_structs, t2c3_casts (c3); t2_verify_a, t2_verify_b, t2_kit (expert).