Act on the codebase review: D7, harness reach, corpus strictness - #4
Merged
Merged
Conversation
Codebase review findings. README.md claimed Phase 0 while VM.md says Phase 1 in progress with two operator families landed. docs/README.md said the evaluation doc was not yet imported, it was imported in 9bf8b95. fetch-references.sh restated the superseded triage-only reading policy, which a future session would have followed. And the package docstring cited CLAUDE.md, against the rule that code comments never reference documentation files. All four now state current facts inline.
Codebase review finding, the only behavioral divergence it turned up: both oracle wheels treat max_cost = 0 as unlimited while BitLisp treats it as a real budget under which no program succeeds. The behavior was implemented but undocumented, and three independent choices (the harness budget range, the differential test, and the vector corpus) all happened to avoid budget zero, so nothing detected the difference. Verified by probe: chia-rs and the clvm package both evaluate a 1104-cost multiply successfully at max_cost 0 and reject it at max_cost 1. Section 3.3 now states the budget domain (nonnegative, unsigned 64-bit in the consensus interface, unenforced by the reference) and the zero-budget rule: uncharged check failures still report their own error class (they precede every charge and are budget-independent), every other program reports cost_exceeded, and none succeeds. The divergence table gains D7, provisional, with ratification queued as section 8 question 4. Section 2 states that deserialization input is an immutable byte string, rejected by type before reading a byte, which the implementation commit enforces. Also from review: D1's vector column cited vm/operators.json, a file that does not exist. It now cites vm/dispatch.json, and the vectors commit adds the actual BLS opcodes there.
Spec: VM.md section 2 as amended in the previous commit. Codebase review findings. A bytearray argument to deserialize sliced into bytearray atoms, which is_atom does not recognize, so the machine misclassified the input as bad_arg_list instead of refusing it, and a memoryview escaped as a bare IndexError in violation of run's documented contract that every failure is a BitLispError. deserialize now rejects any input that is not immutable bytes before reading a byte. bytes input is unaffected. Also from review: the BitLispError code guard was an assert, which vanishes under python -O and would let a typo'd code become a live error class, it now raises ValueError. The dead _MAX_LENGTH constant in serialize.py is deleted in favor of a comment on the existing fall-through guard, and the _FORMS comment now names all four tuple fields.
Codebase review finding: the envelope validator rejects unknown keys
with a stated rationale, but cases did not, so a typo'd max_cost
silently reran its vector at the default budget. The case passed
while pinning nothing, exactly the silent rot the envelope rule
exists to prevent, and 48 of the 204 cases depend on max_cost being
read. Cases are now closed (unknown keys rejected, required keys
checked) and expect must be exactly {result, cost} or {error}.
Also hoists the per-case sys.path.insert to module scope, it was
growing sys.path by one duplicate entry per vector run.
Codebase review finding: over 8000 generated programs the harness never produced wrong_arg_count, bad_arg_list, or reserved_operator, although its oracle error mappings claim all three, so those mapping rows had never once executed. The generator now emits wrong arities, improper argument tails, and the reserved empty-atom operator at low probability. Budget coverage also sharpens: 1 percent of runs use a zero budget (divergence D7, asserted as fail-closed against the unbounded outcome without consulting the oracles) and 10 percent measure the program's actual cost and rerun within a few units of it, where the charge interleaving decides the error class. The new reach immediately paid for itself twice. It caught the D7 spec text overclaiming (an uncharged check failure such as path_into_atom is budget-independent and wins over an empty budget, the spec commit in this PR states the corrected rule). And it surfaced a sixth Python-oracle library behavior: on a program that is wrong in both ways (bad arity and a pair argument) the package converts arguments to integers while iterating, before counting them, where consensus checks arity first. Both are now tolerated branches with their own counters, alongside a tolerance for the package reporting improper argument lists and f or r on an atom with a single indistinguishable message. Verified at 10k programs on seeds 99 and 4242, zero failures, every tolerance counter nonzero on both seeds.
Codebase review findings, one vectors commit for the four gaps. dispatch.json: two D7 cases (a zero budget rejects a quote with cost_exceeded, and the uncharged path_into_atom wins even at budget zero), the two actual BLS opcodes 0x1d and 0x1e as unknown operators (D1 previously cited a vector file that did not exist and no BLS opcode byte appeared anywhere in the corpus), and four section 3.2 step-ordering cases: an improper argument list beats an unknown operator, a pair operator beats the improper-list check, and both D3 and D4 rejections fire uncharged at budget 1. All six ordering and D7 outcomes are BitLisp-only semantics with no oracle, which is exactly why they need vectors. serialize.json: the strict deserializer had no vector above the two smallest length forms although D5 has no oracle at all. Non-minimal floors for the 0xe0, 0xf0, and 0xf8 forms, a declared length of 16 GiB with no body, and the empty byte string, all bad_encoding. paths.json: path_1_on_nil_env was a serialization case in disguise (env was the empty byte string, rejected before any path lookup ran) and its name promised a lookup it never performed. It moves to serialize.json as empty_env_bytes_rejected, and paths.json gains the real case: path 1 against a nil environment returns nil at cost 44, cross-checked against chia-rs. 218 cases total.
Codebase review findings. The hypothesis atom strategy tops out at 300 bytes, so only the two smallest length-prefix forms were ever property-tested although the strict deserializer has no oracle. A parametrized test now round-trips the 0xc0, 0xe0, and 0xf0 form floors byte-for-byte against the oracle serializer (the 0xf8 floor is 128 MiB, its header canonicality is pinned by rejection vectors instead). Non-bytes input rejection is pinned for bytearray and memoryview. Both oracle-importing test modules now use pytest.importorskip: a dev-only install previously failed at collection, making the split between the dev and oracles extras misleading.
Codebase review finding: the Phase 1 done-criterion is 10k randomized corpus programs with zero unexplained divergence, and CLAUDE.md tells sessions to use fresh seeds, but CI only ran the fixed-seed 300 program slice in test_differential.py. A regression that slice happens to miss would merge green. CI now runs the harness at 10k programs with the workflow run id as the seed, so every run exercises a fresh slice and no regression can hide behind a memorized one. The seed is echoed for local reproduction. The 10k run takes well under the job's 15 minute timeout.
Decision by Evan, 2026-07-26. A budget bug must reject every spend, a recoverable liveness failure, rather than hand out unlimited execution, a soundness failure. The divergence table row moves from provisional to ratified. The u64 budget-bound enforcement question in section 8 stays open.
Decision by Evan, 2026-07-26: the reference is an executable spec, not software for wide deployment, and 3.14 is the development version in actual use. requires-python moves from >=3.11 (a claim CI never exercised, flagged by the codebase review) to >=3.14, ruff targets py314, and both CI jobs install 3.14 through a hash-pinned setup-python instead of relying on the runner's default 3.12.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Acts on the findings of a full codebase review of everything that landed on
mainunreviewed (the Phase 0 and Phase 1 sessions). Stacked on #3: the base branch here istree-ops-family, and GitHub will retarget this PR tomainautomatically when #3 merges. Review #3 first.The review independently verified the consensus core (9,931 exhaustive budget-boundary comparisons against chia-rs, 600k fuzzed inputs, all five serializer length forms probed) and found no code change required for safety. What it found instead was one undocumented behavioral divergence and a set of places where the evidence trail claimed more than it covered.
What changed
max_cost = 0as unlimited. BitLisp fails closed, which is right for Bitcoin, but the behavior was undocumented and unpinned, and the harness, tests, and vectors all independently avoided budget zero. D7 is now in the divergence table (provisional, ratification queued as section 8 question 4), section 3.3 states the budget domain, vectors pin it, and 1 percent of harness runs assert it. The harness's first zero-budget runs immediately corrected my own spec draft: uncharged errors likepath_into_atomare budget-independent and win even at budget zero, so the rule is "no program succeeds", not "every program reports cost_exceeded".wrong_arg_count,bad_arg_list, orreserved_operatoralthough its mappings claim all three. It now emits wrong arities, improper tails, and the nil operator, plus cost-boundary budgets (measure, then rerun within a few units). This surfaced a sixth Python-oracle library behavior (integer conversion before arity checking), now a tolerated branch.max_costsilently reran the case at the default budget and passed while pinning nothing.path_1_on_nil_envcase moved and replaced with the lookup its name promised. 218 cases total.deserializerejects non-bytes input (a bytearray previously misclassified asbad_arg_list, a memoryview escaped as a bareIndexError), the error-code guard survivespython -O, dead_MAX_LENGTHconstant removed.__init__.py,sys.pathgrowth in the vector runner, dev-extra test collection.Spec authority
VM.md sections 2, 3.3, 6 (D7), 8 as amended in the first spec commit of this PR. All oracle claims verified by probe against
chia-rsflags 0 and theclvmpackage.Reading order
85364efhygiene: stale text and doc-referencing comments3722fd3spec: D7 and the budget domain7a26dc5implementation: input type guard and internal guards567381ctools: vector case strictnessd85bfddharness: error-path reach and budget boundaries8154d67vectors: D7, BLS opcodes, upper length forms, ordering pins5a052fctests: upper form floors, type rejection, importorskip0a0958eCI: the 10k differential gateVerify independently
Any fresh seed should report 0 failures with every tolerance counter labeled.
Flagged for your decision (not changed here)
ci/lint/requirements.txtand the oracle wheels are version-pinned but not hash-pinned. Hash-pinning (pip--require-hashes) would match the workflow's action-pinning stance.pyproject.tomldeclares >=3.11 but CI tests only ubuntu-24.04's default. A small matrix would close it.