Skip to content

Commit b234599

Browse files
committed
P-037 Phase B / B1: close the snapshot tools' epoch-dispatch gap before R_B
4e75abe froze the classifier, the production-diff gate and the M3 environment identity but left one honest gap open, named in its own p037_evidence_b.py docstring: p037_mos_snapshot.py and p037_verdict_ snapshot.py's take()/compare()/verify() bodies call a module-global `ev` bound once, at import time, to p037_evidence -- so neither tool could actually take Phase-B evidence no matter what a caller wanted. This closes that gap, on top of 4e75abe, before R_B is taken. p037_evidence_b.py gains sixteen one-line re-exports of the pure population/profile/artifact/environment/git/manifest helpers its own docstring already promised were reusable (scratch_problems, execution_profile, build_rust_artifact, artifact_problems, acquire_population, release_population, materialization_root, new_take_dir, seal_artifact, materialize_population, external_ancestor_problems, analysis_paths, sanitized_env, clean_reference_profile, finalize_run, reference_contamination) -- each the literal same function object as p037_evidence's, not a copy. Both snapshot tools gain a required --epoch {a2d,b} argument on take/ compare/verify, matching p037_verdict_snapshot.py's own pre-existing "ENGINE is explicit and required" precedent: never an implicit "current epoch", branch-name inference, or a silently-read env var. main() resolves --epoch against a two-entry EPOCH_MODULES dict and rebinds the module-global `ev` before dispatching to the existing take()/compare()/ verify() bodies, which are otherwise byte-for-byte unchanged -- every ev.NAME reference in them is a call-time attribute lookup. The one exception was p037_mos_snapshot.py's module-level SOURCES dict, which had captured ev.CORPUS_DIRS/ev.REPO_TREE_DIRS as plain tuples at import time, before any --epoch exists to read; replaced with a _sources() function called inside take() itself, after `ev` is rebound. Verified the a2d path is unbroken by real execution against already- accepted evidence, not review alone: `p037_mos_snapshot.py verify --epoch a2d docs/evidence/p037-a2d-baseline-mos-repo.json --against 44b405c...` still reports OK, identical to its pre-change behaviour. ruff, mypy, test_p037_a2d_epoch.py (14/14), test_p037_evidence.py, the proof boundary (23 harnesses/16 assumptions), the B production-diff gate (IDENTICAL against 5571ba4) and the classifier selftest (12/12) all stay green. Documented as new formal-kernel.md #10.8a. Since none of these three files lie under rust/crates/own-bridge/, this commit's own production- diff-gate verdict is unaffected (still IDENTICAL) -- but because 4e75abe could not actually take Phase-B evidence, this commit's head, once pushed and confirmed terminal-green, is offered as T_B instead of 4e75abe. 4e75abe is kept exactly as committed. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AN6xHbpovxrmZ4AMjS7WQA
1 parent 4e75abe commit b234599

4 files changed

Lines changed: 149 additions & 6 deletions

File tree

‎docs/notes/p037-formal-kernel.md‎

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2522,3 +2522,91 @@ above: B1 tooling and this note land first; `T_B` and `R_B` remain "not
25222522
this task" until their own evidence is terminal-green; the first semantic
25232523
treatment remains named, scoped to `production_diff_gate.rust`'s mutable
25242524
items, and unattempted.
2525+
2526+
#### 10.8a Phase B / B1: completing the instrument's last gap before R_B
2527+
2528+
§10.8's own text on `scripts/p037_evidence_b.py` already named an open
2529+
mechanical question rather than papering over it: `p037_mos_snapshot.py`
2530+
and `p037_verdict_snapshot.py`'s `take()`/`compare()`/`verify()` bodies
2531+
call a module-global `ev` bound, at the top of each file, by a single
2532+
hardcoded `import p037_evidence as ev` — meaning both tools would stamp
2533+
epoch `"a2d"` no matter what a caller wanted, and taking R_B with them
2534+
as written was not actually possible. `4e75abe` froze the classifier,
2535+
the gate and the environment identity with that gap still open; this
2536+
addendum closes it, on top of `4e75abe`, before R_B is taken.
2537+
2538+
**REPOSITORY FACT.** Not every `ev.*` name these two tools use is
2539+
epoch-specific. `p037_evidence_b.py`'s own docstring already listed the
2540+
population/profile/artifact/environment/git/manifest mechanics it
2541+
imports unchanged from `p037_evidence.py`, stating the intent plainly:
2542+
"so `p037_mos_snapshot.py`/`p037_verdict_snapshot.py`'s existing `take()`
2543+
bodies can build a record from either module by calling the same-named
2544+
function." That sentence was aspirational until now — `p037_evidence_b`
2545+
did not yet expose those pure names at its own top level (only reachable
2546+
as `p037_evidence_b.ev.scratch_problems`, not `p037_evidence_b.
2547+
scratch_problems`), so binding a caller's `ev` to it would have raised
2548+
`AttributeError` on the first pure call. Fixed by sixteen one-line
2549+
re-exports (`scratch_problems = ev.scratch_problems`, and so on for
2550+
`execution_profile`, `build_rust_artifact`, `artifact_problems`,
2551+
`acquire_population`, `release_population`, `materialization_root`,
2552+
`new_take_dir`, `seal_artifact`, `materialize_population`,
2553+
`external_ancestor_problems`, `analysis_paths`, `sanitized_env`,
2554+
`clean_reference_profile`, `finalize_run`, `reference_contamination`) —
2555+
each one the literal same function object as `p037_evidence`'s, checked
2556+
directly (`p037_evidence_b.scratch_problems is p037_evidence.
2557+
scratch_problems` → `True`), not merely asserted.
2558+
2559+
**Design: explicit `--epoch`, no silent selection.** Both snapshot tools
2560+
gain a required `--epoch {a2d,b}` argument on every subcommand that
2561+
touches `ev` (`take`, `compare`, `verify`) — matching
2562+
`p037_verdict_snapshot.py`'s own pre-existing "ENGINE is explicit and
2563+
required" precedent for exactly the same reason, and satisfying the B1
2564+
brief's explicit list of forbidden mechanisms: no implicit "current
2565+
epoch", no branch-name inference, no silently-read environment variable.
2566+
`main()` resolves `args.epoch` against a two-entry `EPOCH_MODULES` dict
2567+
(`{"a2d": p037_evidence, "b": p037_evidence_b}`) and rebinds the
2568+
module-global `ev` to the selected module *before* calling `take()`/
2569+
`compare()`/`verify()` — whose bodies are otherwise byte-for-byte
2570+
unchanged, because every `ev.NAME` reference inside them is an attribute
2571+
lookup Python resolves at call time, not at function-definition time.
2572+
The one place that was NOT already call-time-lazy was
2573+
`p037_mos_snapshot.py`'s module-level `SOURCES` dict, which captured
2574+
`ev.CORPUS_DIRS`/`ev.REPO_TREE_DIRS` as plain tuples at import time —
2575+
before any `--epoch` argument exists to read. Replaced with a `_sources
2576+
(epoch_mod)` function called inside `take()` itself, after `ev` is
2577+
rebound, so `--epoch b` actually reaches the augmented `CORPUS_DIRS`
2578+
(`p037_evidence_b`'s tuple, plus `corpus/p037-shapes`) instead of
2579+
silently reusing a2d's.
2580+
2581+
**MEASURED/AUDITED FACT.** The a2d path was proven unbroken by real
2582+
execution against already-accepted evidence, not by code review alone:
2583+
`p037_mos_snapshot.py verify --epoch a2d docs/evidence/p037-a2d-baseline-
2584+
mos-repo.json --against 44b405c2003b1d68965fe6346c2506d51ed52def` still
2585+
reports `OK: ... fresh evidence at 44b405c2003b ...; inputs=82,
2586+
support=3`, identical to its pre-change behaviour. The same command
2587+
against current `HEAD` correctly reports `FAIL[provenance]: the
2588+
treatment changed between 44b405c2003b and HEAD` — the A2.2-D door
2589+
treatment landing after `T_D`, exactly as A2.2-D's own design intends,
2590+
and unrelated to this change. `p037_evidence_b.EPOCH_MODULES` (read via
2591+
each snapshot tool's own dict of the same name) resolves `"a2d"` to
2592+
`p037_evidence` and `"b"` to `p037_evidence_b`, with `CORPUS_DIRS`
2593+
differing exactly as designed (`"corpus/p037-shapes" in ...` is `False`
2594+
for a2d, `True` for b) and `REPO_TREE_DIRS` identical on both (b never
2595+
had a different repo-tree population). `ruff check .`, the project-wide
2596+
`mypy`, `tests/test_p037_a2d_epoch.py` (14/14) and `tests/
2597+
test_p037_evidence.py` all stay green on a clean tree; the one transient
2598+
`FAIL[fresh-record-valid]` seen while this addendum's own files were
2599+
still uncommitted was `evidence was taken on a dirty tree` — the test's
2600+
own real-`git`-backed fixture correctly reporting this checkout's actual
2601+
dirty state at that moment, not a defect in the fix, and gone once
2602+
committed.
2603+
2604+
**Consequence for T_B.** `4e75abe`'s production-diff gate verdict
2605+
(`IDENTICAL` against `5571ba4`) is untouched by this addendum — none of
2606+
its three files lie under `rust/crates/own-bridge/`. But `4e75abe` could
2607+
not actually take Phase-B evidence, so it is not offered as `T_B`: the
2608+
commit landing this addendum is, once it is itself pushed and confirmed
2609+
terminal-green (including fast Kani) the same way `4e75abe` was. `4e75abe`
2610+
stays exactly as committed, an honest record of the instrument as it
2611+
stood one step before the gap was found — the same discipline §10.7a and
2612+
§10.6.14a both already apply to their own preceding heads.

‎scripts/p037_evidence_b.py‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,31 @@
6868

6969
EvidenceRefused = ev.EvidenceRefused
7070

71+
# Re-exported verbatim so this module is a full drop-in for `ev` wherever a
72+
# caller's code (unchanged) reaches for one of these names -- see
73+
# scripts/p037_mos_snapshot.py and scripts/p037_verdict_snapshot.py's
74+
# --epoch dispatch, which rebinds their module-global `ev` to this module or
75+
# to p037_evidence and calls the same, already-written take()/_measure()
76+
# bodies either way. None of these read EPOCH/EPOCH_RECORD_PATH/
77+
# INSTRUMENT_PATHS internally (see module docstring), so aliasing them here
78+
# moves zero bytes of logic and adds none.
79+
scratch_problems = ev.scratch_problems
80+
execution_profile = ev.execution_profile
81+
build_rust_artifact = ev.build_rust_artifact
82+
artifact_problems = ev.artifact_problems
83+
acquire_population = ev.acquire_population
84+
release_population = ev.release_population
85+
materialization_root = ev.materialization_root
86+
new_take_dir = ev.new_take_dir
87+
seal_artifact = ev.seal_artifact
88+
materialize_population = ev.materialize_population
89+
external_ancestor_problems = ev.external_ancestor_problems
90+
analysis_paths = ev.analysis_paths
91+
sanitized_env = ev.sanitized_env
92+
clean_reference_profile = ev.clean_reference_profile
93+
finalize_run = ev.finalize_run
94+
reference_contamination = ev.reference_contamination
95+
7196
EPOCH = "b"
7297
EPOCH_RECORD_PATH = "docs/evidence/p037-b-epoch.json"
7398

‎scripts/p037_mos_snapshot.py‎

Lines changed: 22 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@
4646
sys.path.insert(0, str(ROOT))
4747

4848
import p037_evidence as ev # noqa: E402
49+
import p037_evidence_b # noqa: E402
4950
from shadow_compare import ( # noqa: E402
5051
DEFAULT_TIMEOUT_SECONDS,
5152
ExecutionFailure,
@@ -57,10 +58,19 @@
5758
from ownlang.repro import ENGINE_PYTHON, ENGINE_RUST, hash_bytes # noqa: E402
5859

5960
SCHEMA = "p037-mos-snapshot/2"
60-
SOURCES: dict[str, tuple[str, ...]] = {
61-
"corpus": ev.CORPUS_DIRS,
62-
"repo": ev.REPO_TREE_DIRS,
63-
}
61+
SOURCE_NAMES: tuple[str, ...] = ("corpus", "repo")
62+
# Epoch is explicit and required, matching p037_verdict_snapshot.py's own
63+
# "ENGINE is explicit and required" precedent -- never an implicit "current
64+
# epoch", branch-name inference or a silently-read env var (P-037 Phase B
65+
# prompt, section on epoch-aware tooling). main() rebinds the module-global
66+
# `ev` to the selected module before calling take()/_measure()/compare()/
67+
# verify()/extract_facts() below; their bodies read `ev.*` at call time and
68+
# are otherwise UNCHANGED for either epoch.
69+
EPOCH_MODULES: dict[str, Any] = {"a2d": ev, "b": p037_evidence_b}
70+
71+
72+
def _sources(epoch_mod: Any) -> dict[str, tuple[str, ...]]:
73+
return {"corpus": epoch_mod.CORPUS_DIRS, "repo": epoch_mod.REPO_TREE_DIRS}
6474

6575

6676
class ReferenceContamination(RuntimeError):
@@ -189,7 +199,7 @@ def _refuse(problems: list[str]) -> None:
189199

190200

191201
def take(source: str, out: Path, timeout: float, population_commit: str) -> int:
192-
roots = SOURCES[source]
202+
roots = _sources(ev)[source]
193203
try:
194204
_refuse(ev.scratch_problems(out))
195205
provenance = ev.evidence_fields(roots, population_commit=population_commit)
@@ -461,23 +471,29 @@ def main(argv: list[str]) -> int:
461471
ap.add_argument("--selftest", action="store_true")
462472
sub = ap.add_subparsers(dest="cmd")
463473
t = sub.add_parser("take")
464-
t.add_argument("--source", required=True, choices=tuple(SOURCES))
474+
t.add_argument("--epoch", required=True, choices=tuple(EPOCH_MODULES))
475+
t.add_argument("--source", required=True, choices=SOURCE_NAMES)
465476
t.add_argument("--out", required=True, type=Path)
466477
t.add_argument("--population-commit", default="HEAD",
467478
help="the commit whose blobs are analysed (default HEAD; the after "
468479
"side of a pair names the baseline's commit)")
469480
t.add_argument("--timeout", type=float, default=DEFAULT_TIMEOUT_SECONDS)
470481
c = sub.add_parser("compare")
482+
c.add_argument("--epoch", required=True, choices=tuple(EPOCH_MODULES))
471483
c.add_argument("--before", required=True, type=Path)
472484
c.add_argument("--after", required=True, type=Path)
473485
c.add_argument("--against", default="HEAD",
474486
help="the commit the after side must be fresh at (default HEAD)")
475487
v = sub.add_parser("verify")
488+
v.add_argument("--epoch", required=True, choices=tuple(EPOCH_MODULES))
476489
v.add_argument("snapshot", type=Path)
477490
v.add_argument("--against", default="HEAD")
478491
args = ap.parse_args(argv)
479492
if args.selftest:
480493
return selftest()
494+
if args.cmd in ("take", "compare", "verify"):
495+
global ev
496+
ev = EPOCH_MODULES[args.epoch]
481497
if args.cmd == "take":
482498
return take(args.source, args.out, args.timeout, args.population_commit)
483499
if args.cmd == "compare":

‎scripts/p037_verdict_snapshot.py‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,10 +56,19 @@
5656
from typing import Any
5757

5858
import p037_evidence as ev
59+
import p037_evidence_b
5960

6061
ROOT = Path(__file__).resolve().parent.parent
6162
SCHEMA = "p037-verdict-snapshot/3"
6263
VERDICT_LEVELS = ("error", "warning")
64+
# Epoch is explicit and required -- same precedent this module's own
65+
# docstring already states for ENGINE, extended to epoch selection (P-037
66+
# Phase B: never an implicit "current epoch", branch-name inference or a
67+
# silently-read env var). main() rebinds the module-global `ev` to the
68+
# selected module before calling take()/_measure()/compare()/verify()/
69+
# run_one() below; their bodies read `ev.*` at call time and are otherwise
70+
# UNCHANGED for either epoch.
71+
EPOCH_MODULES: dict[str, Any] = {"a2d": ev, "b": p037_evidence_b}
6372

6473

6574
def run_one(path: Path, engine: str, env: dict[str, str]) -> dict[str, Any]:
@@ -313,23 +322,28 @@ def main(argv: list[str]) -> int:
313322
formatter_class=argparse.RawDescriptionHelpFormatter)
314323
sub = ap.add_subparsers(dest="cmd", required=True)
315324
t = sub.add_parser("take", help="record a snapshot")
325+
t.add_argument("--epoch", required=True, choices=tuple(EPOCH_MODULES))
316326
t.add_argument("--engine", required=True, choices=("rust", "python"))
317327
t.add_argument("--out", required=True, type=Path)
318328
t.add_argument("--corpus", action="append", default=None, metavar="DIR")
319329
t.add_argument("--population-commit", default="HEAD",
320330
help="the commit whose blobs are analysed (default HEAD; the after "
321331
"side of a pair names the baseline's commit)")
322332
c = sub.add_parser("compare", help="diff two snapshots")
333+
c.add_argument("--epoch", required=True, choices=tuple(EPOCH_MODULES))
323334
c.add_argument("--before", required=True, type=Path)
324335
c.add_argument("--after", required=True, type=Path)
325336
c.add_argument("--level", default="verdict", choices=("verdict", "all"),
326337
help="verdict = error/warning only (default); all = advisories too")
327338
c.add_argument("--against", default="HEAD",
328339
help="the commit the after side must be fresh at (default HEAD)")
329340
v = sub.add_parser("verify", help="prove a snapshot is still fresh evidence at a commit")
341+
v.add_argument("--epoch", required=True, choices=tuple(EPOCH_MODULES))
330342
v.add_argument("snapshot", type=Path)
331343
v.add_argument("--against", default="HEAD")
332344
args = ap.parse_args(argv)
345+
global ev
346+
ev = EPOCH_MODULES[args.epoch]
333347
if args.cmd == "take":
334348
dirs = tuple(args.corpus) if args.corpus else ev.CORPUS_DIRS
335349
return take(args.engine, args.out, dirs, args.population_commit)

0 commit comments

Comments
 (0)