From 85364ef5f53a0e1e01ef138464cb2a544c2a7e8c Mon Sep 17 00:00:00 2001 From: Evan Date: Sun, 26 Jul 2026 19:18:23 -0700 Subject: [PATCH 01/10] Fix stale status text and doc-referencing comments 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. --- README.md | 6 ++++-- docs/README.md | 8 ++++---- python/bitlisp/__init__.py | 6 +++--- tools/fetch-references.sh | 9 +++------ 4 files changed, 14 insertions(+), 15 deletions(-) diff --git a/README.md b/README.md index 9f0abc7..2d16a49 100644 --- a/README.md +++ b/README.md @@ -4,8 +4,10 @@ An executable specification for a Bitcoin Script successor: a CLVM-derived predicate VM plus a condition vocabulary and transaction-matching layer, committed under a new taproot leaf version. -Status: Phase 0 (bootstrap). Nothing here is consensus-ready. The phased -plan is in [docs/execution-plan.md](docs/execution-plan.md). +Status: Phase 1 (VM core via CLVM intersection) in progress. The +evaluator core, the tree ops family, and the arithmetic family are +implemented and pinned by vectors. Nothing here is consensus-ready. +The phased plan is in [docs/execution-plan.md](docs/execution-plan.md). ## Layout diff --git a/docs/README.md b/docs/README.md index 90a192f..bcab08b 100644 --- a/docs/README.md +++ b/docs/README.md @@ -1,8 +1,8 @@ # docs - [execution-plan.md](execution-plan.md): the phased working plan. -- `bitcoin-script-successor-evaluation.md`: the evaluation doc this repo - executes against. Not yet imported, it currently lives outside the - repo. Drop it in here so the section 7 design obligations and the - section 8 confidence table are citable from spec and CLAUDE.md. +- [bitcoin-script-successor-evaluation.md](bitcoin-script-successor-evaluation.md): + the evaluation doc this repo executes against. The section 7 design + obligations and the section 8 confidence table are citable from spec + and CLAUDE.md. - Essay drafts land here in Phase 4. diff --git a/python/bitlisp/__init__.py b/python/bitlisp/__init__.py index c253794..387cc89 100644 --- a/python/bitlisp/__init__.py +++ b/python/bitlisp/__init__.py @@ -1,8 +1,8 @@ """BitLisp reference implementation. -This package is the executable specification. Every consensus-relevant -behavior implemented here cites a section of spec/ (ground rule 1 in -CLAUDE.md). +This package is the executable specification: small, boring, and +readable whole. Behavior is pinned by the vector corpus and by +differential testing against the consensus oracle. """ from .errors import CODES, BitLispError diff --git a/tools/fetch-references.sh b/tools/fetch-references.sh index 75ff1d9..7093f5a 100755 --- a/tools/fetch-references.sh +++ b/tools/fetch-references.sh @@ -1,11 +1,8 @@ #!/usr/bin/env bash # Clones upstream reference repos into git-ignored references/ for -# HUMAN BROWSING ONLY. -# -# Policy (CLAUDE.md): references/ is opened only in divergence-triage -# sessions, never implementation sessions. Code is never copied from -# it. Oracles used by tests are the released wheels pinned in -# pyproject.toml, not these checkouts. +# reading. Code is never copied from these checkouts, and they are +# not a build input: the oracles used by tests are the released +# wheels pinned in pyproject.toml. set -o errexit -o nounset -o pipefail cd "$(git rev-parse --show-toplevel)" From 3722fd3f91daed15c41dc474cbf630b69d154af3 Mon Sep 17 00:00:00 2001 From: Evan Date: Sun, 26 Jul 2026 19:26:17 -0700 Subject: [PATCH 02/10] Record divergence D7: a zero cost budget fails closed 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 | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) diff --git a/spec/VM.md b/spec/VM.md index a41730e..042c11e 100644 --- a/spec/VM.md +++ b/spec/VM.md @@ -47,6 +47,11 @@ rules on input (divergence D5). One node serializes as follows. nil is `0x80` (the zero-length case of the second row). +Deserialization operates on an immutable byte string. The reference +implementation rejects any other input type with `bad_encoding` +before reading a byte, so type coercion can never produce a +differently shaped tree. + The deserializer rejects, with error `bad_encoding`: 1. Truncated input, and input with trailing bytes after the root node. @@ -133,6 +138,18 @@ at every charge. The budget is inclusive: a program whose total cost equals `max_cost` exactly succeeds. Exceeding it raises `cost_exceeded`. +`max_cost` is a nonnegative integer. In the consensus interface it is +an unsigned 64-bit quantity, derived from transaction weight in the +Phase 3 mapping. The Python reference accepts any nonnegative Python +integer and does not enforce the 64-bit bound, the hardened +implementation will. A budget of zero is a real budget: every program +charges at least once before completing, so no program succeeds under +a zero budget. A program whose uncharged checks fail first (a path +walk into an atom, an improper argument list, an unknown operator) +reports that error, every other program reports `cost_exceeded`. Both +CLVM oracles instead treat a zero `max_cost` as unlimited (divergence +D7). + ## 4. Operator table Implemented so far: the core specials, the tree ops family, and the @@ -237,12 +254,13 @@ pin it. No divergence exists outside this table. "Both oracles" means | # | Area | CLVM behavior | BitLisp behavior | Rationale | Vectors | | --- | --- | --- | --- | --- | --- | -| D1 | BLS operators | `point_add`, `pubkey_for_exp`, BLS extension ops present | absent, `unknown_operator` | Bitcoin has no BLS. Removing them removes their entire attack and cost surface. | `vm/operators.json` | +| D1 | BLS operators | `point_add`, `pubkey_for_exp`, BLS extension ops present | absent, `unknown_operator` | Bitcoin has no BLS. Removing them removes their entire attack and cost surface. | `vm/dispatch.json` | | D2 | secp256k1 | `secp256k1_verify` post-hardfork op | `secp_verify`, BIP340 Schnorr (crypto family session) | Native curve, native signature scheme. | TODO Phase 1 crypto session | | D3 | Unknown operators | Both oracles accept unknown opcodes, cost derived from the opcode bytes, result nil | `unknown_operator` error | The operator set is closed by design. Bitcoin soft-forks at the tapleaf-version level, not through unknown-opcode acceptance. PROVISIONAL, see section 8. | `vm/dispatch.json` | | D4 | Pair in operator position | `clvm` rejects. `chia-rs` accepts via a legacy apply-style rule (observed: `((A . B) . rest)` dispatches on `A` with arity errors reported for `A`'s operator) | `operator_not_atom` error | The oracles disagree with each other. Strict rejection is the smaller, reviewable surface. PROVISIONAL, see section 8. | `vm/dispatch.json` | | D5 | Deserialization strictness | Both oracles accept non-minimal length encodings, trailing bytes, and (chia-rs) `0xfe` back-references | `bad_encoding` for all three (section 2) | Witness bytes must have exactly one accepted spelling per program. Malleability of the serialized form is a consensus hazard in the Bitcoin context. | `vm/serialize.json` | | D6 | `/` with negative operands | Consensus (`chia-rs`): floor division. The `clvm` package injects a policy error ("deprecated") that is not consensus | Floor division, matching consensus | Intersection parity targets the consensus oracle. The Python package's rejection is library policy, the diff harness treats it as an expected divergence. OPEN QUESTION, see section 8. | `vm/arith.json` | +| D7 | Zero cost budget | Both oracles treat `max_cost = 0` as unlimited | A zero budget is a real budget, no program succeeds under it (section 3.3) | A zero sentinel meaning unlimited is a library convenience, not consensus behavior. In the Bitcoin context the budget derives from transaction weight and is never legitimately zero, and an accidental zero must fail closed rather than open. PROVISIONAL, see section 8. | `vm/dispatch.json` | ## 7. Oracle provenance @@ -275,3 +293,10 @@ these is a spec amendment plus vector update in one reviewed commit. floor semantics, reject negative operands in consensus, or drop `/` entirely and keep only `divmod`. Needs a decision before the operator set freezes. +4. **D7 (zero budget).** Fail-closed implemented: a zero `max_cost` + rejects every program where the oracles treat it as unlimited. + Found by the codebase review, previously undocumented. Confirm + fail-closed, and decide whether the reference should also enforce + the unsigned 64-bit budget bound the hardened implementation will + have (section 3.3 currently records the bound without enforcing + it). From 7a26dc5827cbd24bac7ec5eb5b240b5cf5ed5dfb Mon Sep 17 00:00:00 2001 From: Evan Date: Sun, 26 Jul 2026 19:26:17 -0700 Subject: [PATCH 03/10] Reject non-bytes deserialization input, harden two internal guards 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. --- python/bitlisp/errors.py | 5 ++++- python/bitlisp/serialize.py | 17 +++++++++++++---- 2 files changed, 17 insertions(+), 5 deletions(-) diff --git a/python/bitlisp/errors.py b/python/bitlisp/errors.py index c63775c..5206c34 100644 --- a/python/bitlisp/errors.py +++ b/python/bitlisp/errors.py @@ -32,6 +32,9 @@ class BitLispError(Exception): """ def __init__(self, code, message): - assert code in CODES, code + # A typo'd code must fail loudly even under python -O, where + # an assert would vanish and let it become a live error class. + if code not in CODES: + raise ValueError(f"unknown error code {code!r}") super().__init__(message) self.code = code diff --git a/python/bitlisp/serialize.py b/python/bitlisp/serialize.py index 98279f4..f62e0f7 100644 --- a/python/bitlisp/serialize.py +++ b/python/bitlisp/serialize.py @@ -12,9 +12,10 @@ from .errors import BitLispError from .sexp import is_atom -# Length prefix forms: (leading byte low-bit mask, extra length bytes, -# smallest length that requires this form). An encoding is canonical -# only if the length could not fit a shorter form. +# Length prefix forms: (prefix byte, mask selecting the length bits +# inside the prefix byte, count of extra length bytes, smallest length +# that requires this form). An encoding is canonical only if the +# length could not fit a shorter form. _FORMS = ( (0x80, 0x3F, 0, 0), (0xC0, 0x1F, 1, 0x40), @@ -22,7 +23,6 @@ (0xF0, 0x07, 3, 0x100000), (0xF8, 0x03, 4, 0x8000000), ) -_MAX_LENGTH = 0x400000000 - 1 # 34-bit length field _PARSE, _CONS = 0, 1 @@ -54,11 +54,20 @@ def _write_atom(out, atom): out += low_bits.to_bytes(extra, "big") if extra else b"" out += atom return + # The forms cover every length below 2**34. Longer atoms have no + # encoding in the wire format. raise BitLispError("bad_encoding", "atom too long to serialize") def deserialize(data): """Parses exactly one node from all of data, strictly.""" + # Only immutable bytes may enter. A bytearray would slice into + # bytearray atoms, which the machine would not recognize as atoms, + # and a memoryview can escape as a bare IndexError. Rejecting the + # type before reading a byte keeps every failure inside the error + # taxonomy. + if type(data) is not bytes: + raise BitLispError("bad_encoding", "input must be bytes") pos = 0 values = [] tasks = [_PARSE] From 567381c120b7e2bd73205d9fb308e32c6ed4d948 Mon Sep 17 00:00:00 2001 From: Evan Date: Sun, 26 Jul 2026 19:26:17 -0700 Subject: [PATCH 04/10] Close the vector case shape like the envelope 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. --- tools/run_vectors.py | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/tools/run_vectors.py b/tools/run_vectors.py index 5ff147a..387d480 100755 --- a/tools/run_vectors.py +++ b/tools/run_vectors.py @@ -28,6 +28,7 @@ REPO_ROOT = Path(__file__).resolve().parent.parent VECTOR_ROOT = REPO_ROOT / "vectors" +sys.path.insert(0, str(REPO_ROOT / "python")) SCHEMA = "bitlisp-vector-v0" SUITES = ("vm", "conditions", "matching") @@ -76,7 +77,9 @@ def discover(root=VECTOR_ROOT): def run_vm_case(case): """One vm case: run serialized (program, env) under a budget. - Case shape: + Case shape, closed like the envelope (unknown keys rejected, a + typo'd max_cost would otherwise silently rerun the case at the + default budget and pass while pinning nothing): { "name": "", "program": "", @@ -86,14 +89,27 @@ def run_vm_case(case): or {"error": ""} } """ - sys.path.insert(0, str(REPO_ROOT / "python")) from bitlisp import BitLispError, run_serialized from bitlisp.errors import CODES + required = {"name", "program", "env", "expect"} + keys = set(case) + if missing := required - keys: + raise VectorError(f"missing keys {sorted(missing)}") + if extra := keys - required - {"max_cost"}: + raise VectorError(f"unknown keys {sorted(extra)}") + expect = case["expect"] + if not isinstance(expect, dict) or set(expect) not in ( + {"result", "cost"}, + {"error"}, + ): + raise VectorError( + "expect must be exactly {result, cost} or {error}, " + f"got {sorted(expect) if isinstance(expect, dict) else expect!r}" + ) program = bytes.fromhex(case["program"]) env = bytes.fromhex(case["env"]) max_cost = case.get("max_cost", 11_000_000_000) - expect = case["expect"] try: cost, result = run_serialized(program, env, max_cost) outcome = {"result": result.hex(), "cost": cost} From d85bfdd70b5a96f159230f8e03e65ef2543f91f2 Mon Sep 17 00:00:00 2001 From: Evan Date: Sun, 26 Jul 2026 19:27:39 -0700 Subject: [PATCH 05/10] Reach the unexercised error paths and budget boundaries 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. --- tools/diff_clvm.py | 107 ++++++++++++++++++++++++++++++++++++++------- 1 file changed, 92 insertions(+), 15 deletions(-) diff --git a/tools/diff_clvm.py b/tools/diff_clvm.py index 4a37817..d4f5302 100644 --- a/tools/diff_clvm.py +++ b/tools/diff_clvm.py @@ -9,21 +9,31 @@ - clvm (Python package), the secondary oracle Success requires identical (cost, result bytes) or an identical error -class. Four disagreements with the Python oracle are tolerated and +class. Six disagreements with the Python oracle are tolerated and counted, all library behavior rather than consensus: its policy rejection of negative division operands (consensus does floor division), its budget check running only after an operator completes, its immediate check of apply's cost where consensus defers the check -to the applied program's first charge, and its lack of the consensus -operand size limits. The two budget-timing tolerances are verified -per case, not assumed: the tolerating branch re-runs an +to the applied program's first charge, its lack of the consensus +operand size limits, its single message for both an improper argument +list and f or r on an atom, and its integer conversion running before +the arity check where consensus checks arity first. The two budget-timing tolerances +are verified per case, not assumed: the tolerating branch re-runs an implementation without the tight budget and requires it to reproduce the other side's outcome exactly, so neither can absorb an unrelated -divergence. The generator never emits the recorded BitLisp -divergences: unknown operators, pairs in operator position, and -non-canonical serializations cannot arise because programs are -emitted by bitlisp's own canonical serializer over the implemented -opcode set. Anything else is a finding and fails the run. +divergence. + +The generator never emits three of the recorded BitLisp divergences: +unknown operators, pairs in operator position, and non-canonical +serializations cannot arise because programs are emitted by bitlisp's +own canonical serializer over the implemented opcode set. It does +emit zero budgets, which exercise divergence D7 (the oracles treat a +zero budget as unlimited): those runs assert bitlisp's fail-closed +outcome and skip the oracles. It also emits wrong arities, improper +argument tails, and the reserved empty-atom operator, and a share of +runs use a budget within a few units of the program's measured cost, +where the charge interleaving decides the error class. Anything else +is a finding and fails the run. Usage: python3 tools/diff_clvm.py --count 10000 --seed 1 @@ -147,9 +157,10 @@ def run_py(program, env, max_cost): class Generator: """Random programs over the implemented operator set.""" - # opcode -> arity, None for variadic (0 to 4 arguments). The - # generator always emits a valid arity: wrong_arg_count paths are - # pinned by hand-written vectors instead. + # opcode -> arity, None for variadic (0 to 4 arguments). Wrong + # arities, improper argument tails, and the reserved empty-atom + # operator are emitted at low probability so the wrong_arg_count, + # bad_arg_list, and reserved_operator paths stay exercised. ARITIES = { b"\x03": 3, # i b"\x04": 2, # c @@ -217,8 +228,17 @@ def program(self, depth): return (b"\x08", b"") # (x) opcode = r.choice(self.OPCODES) arity = self.ARITIES[opcode] - arg_count = r.randint(0, 4) if arity is None else arity + if arity is None: + arg_count = r.randint(0, 4) + elif r.random() < 0.06: + arg_count = max(0, arity + r.choice((-1, 1))) + else: + arg_count = arity + if r.random() < 0.03: + opcode = b"" # reserved operator, arguments still evaluate args = b"" + if r.random() < 0.03: + args = int_to_atom(r.randint(1, 127)) # improper tail for _ in range(arg_count): args = (self.program(depth - 1), args) return (opcode, args) @@ -237,10 +257,13 @@ def main(): stats = { "ok": 0, "err_agree": 0, + "d7_zero_budget": 0, "policy_div": 0, "py_budget_timing": 0, "py_apply_cost_timing": 0, "py_no_operand_limit": 0, + "py_improper_list_ambiguity": 0, + "py_arity_check_order": 0, } failures = 0 @@ -249,9 +272,45 @@ def main(): env_node = gen.value_tree(3) program = serialize(program_node) env = serialize(env_node) - max_cost = MAX_COST if rng.random() < 0.9 else rng.randint(1, 5000) + roll = rng.random() + if roll < 0.84: + max_cost = MAX_COST + elif roll < 0.85: + max_cost = 0 # divergence D7, asserted below + elif roll < 0.90: + max_cost = rng.randint(1, 5000) + else: + # Boundary budgets: measure the program's actual cost, + # then rerun within a few units of it, where the charge + # interleaving decides which error class is reported. + probe = run_bitlisp(program, env, MAX_COST) + if probe[0] == "ok": + max_cost = max(1, probe[1] + rng.randint(-3, 1)) + else: + max_cost = rng.randint(1, 5000) bl = run_bitlisp(program, env, max_cost) + + # Recorded divergence D7: the oracles treat a zero budget as + # unlimited, bitlisp fails closed. No program may succeed. An + # uncharged check failure wins over the empty budget and is + # budget-independent, so it must match the unbounded outcome, + # everything else must be cost_exceeded. The oracles are not + # consulted. + if max_cost == 0: + zero_ok = bl == ("err", "cost_exceeded") or ( + bl[0] == "err" and bl == run_bitlisp(program, env, MAX_COST) + ) + if zero_ok: + stats["d7_zero_budget"] += 1 + else: + failures += 1 + print(f"MISMATCH d7 #{i}: prog={program.hex()} env={env.hex()}") + print(f" max_cost=0 bitlisp={bl}, expected a failure") + if failures >= args.max_fails: + break + continue + rs = run_rs(program, env, max_cost) py = run_py(program, env, max_cost) @@ -300,6 +359,21 @@ def main(): # consensus reports the applied program's error. py_agrees = True stats["py_apply_cost_timing"] += 1 + elif bl == ("err", "bad_arg_list") and py == ("err", "arg_not_pair"): + # The Python oracle reports an improper argument list + # with the same message as f or r on an atom, so the two + # classes are indistinguishable in its output. The + # consensus comparison above already matched the class + # exactly. + py_agrees = True + stats["py_improper_list_ambiguity"] += 1 + elif bl == ("err", "wrong_arg_count") and py == ("err", "arg_not_atom"): + # On a program that is wrong in both ways (bad arity and + # a pair argument), consensus checks arity first while + # the Python oracle converts arguments to integers while + # iterating, before counting them. + py_agrees = True + stats["py_arity_check_order"] += 1 if not py_agrees: failures += 1 @@ -311,14 +385,17 @@ def main(): stats["ok" if bl[0] == "ok" else "err_agree"] += 1 - total = stats["ok"] + stats["err_agree"] + total = stats["ok"] + stats["err_agree"] + stats["d7_zero_budget"] print( f"diff_clvm: {total} compared, {stats['ok']} ok, " f"{stats['err_agree']} errors agreed, " + f"{stats['d7_zero_budget']} d7 zero-budget, " f"{stats['policy_div']} tolerated py policy-div, " f"{stats['py_budget_timing']} tolerated py budget-timing, " f"{stats['py_apply_cost_timing']} tolerated py apply-cost-timing, " f"{stats['py_no_operand_limit']} tolerated py no-operand-limit, " + f"{stats['py_improper_list_ambiguity']} tolerated py improper-list, " + f"{stats['py_arity_check_order']} tolerated py arity-order, " f"{failures} failures" ) return 1 if failures else 0 From 8154d67d1f4af9536b22cdd73babe383f2dfdf91 Mon Sep 17 00:00:00 2001 From: Evan Date: Sun, 26 Jul 2026 19:29:02 -0700 Subject: [PATCH 06/10] Pin the review-found gaps: D7, BLS opcodes, upper length forms 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. --- vectors/vm/dispatch.json | 68 +++++++++++++++++++++++++++++++++++++++ vectors/vm/paths.json | 17 +++++----- vectors/vm/serialize.json | 48 +++++++++++++++++++++++++++ 3 files changed, 125 insertions(+), 8 deletions(-) diff --git a/vectors/vm/dispatch.json b/vectors/vm/dispatch.json index 5886b98..9280c4e 100644 --- a/vectors/vm/dispatch.json +++ b/vectors/vm/dispatch.json @@ -320,6 +320,74 @@ "expect": { "error": "cost_exceeded" } + }, + { + "name": "zero_budget_rejects_quote", + "program": "ff0101", + "env": "80", + "max_cost": 0, + "expect": { + "error": "cost_exceeded" + } + }, + { + "name": "zero_budget_uncharged_error_wins", + "program": "07", + "env": "65", + "max_cost": 0, + "expect": { + "error": "path_into_atom" + } + }, + { + "name": "unknown_operator_bls_point_add", + "program": "ff1d80", + "env": "80", + "expect": { + "error": "unknown_operator" + } + }, + { + "name": "unknown_operator_bls_pubkey_for_exp", + "program": "ff1e80", + "env": "80", + "expect": { + "error": "unknown_operator" + } + }, + { + "name": "bad_arg_list_beats_unknown_operator", + "program": "ff2f05", + "env": "80", + "expect": { + "error": "bad_arg_list" + } + }, + { + "name": "pair_operator_beats_bad_arg_list", + "program": "ffff010105", + "env": "80", + "expect": { + "error": "operator_not_atom" + } + }, + { + "name": "unknown_operator_uncharged_budget_1", + "program": "ff2f80", + "env": "80", + "max_cost": 1, + "expect": { + "error": "unknown_operator" + } + }, + { + "name": "pair_operator_uncharged_budget_1", + "program": "ffff0101ffff010280", + "env": "80", + "max_cost": 1, + "expect": { + "error": "operator_not_atom" + } } ] } diff --git a/vectors/vm/paths.json b/vectors/vm/paths.json index 86b44dc..ba97dc3 100644 --- a/vectors/vm/paths.json +++ b/vectors/vm/paths.json @@ -118,14 +118,6 @@ "error": "path_into_atom" } }, - { - "name": "path_1_on_nil_env", - "program": "01", - "env": "", - "expect": { - "error": "bad_encoding" - } - }, { "name": "walk_precedes_charge_path_error_at_budget_1", "program": "04", @@ -153,6 +145,15 @@ "result": "ff0a14", "cost": 48 } + }, + { + "name": "path_1_on_nil_env", + "program": "01", + "env": "80", + "expect": { + "result": "80", + "cost": 44 + } } ] } diff --git a/vectors/vm/serialize.json b/vectors/vm/serialize.json index d9d8e5a..9e52bcb 100644 --- a/vectors/vm/serialize.json +++ b/vectors/vm/serialize.json @@ -178,6 +178,54 @@ "result": "ffff0102ffff807fff0102", "cost": 20 } + }, + { + "name": "empty_env_bytes_rejected", + "program": "01", + "env": "", + "expect": { + "error": "bad_encoding" + } + }, + { + "name": "non_minimal_e0_form", + "program": "e0000141", + "env": "80", + "expect": { + "error": "bad_encoding" + } + }, + { + "name": "non_minimal_f0_form", + "program": "f000000141", + "env": "80", + "expect": { + "error": "bad_encoding" + } + }, + { + "name": "non_minimal_f8_form", + "program": "f80000000141", + "env": "80", + "expect": { + "error": "bad_encoding" + } + }, + { + "name": "declared_length_exceeds_input", + "program": "fbffffffff", + "env": "80", + "expect": { + "error": "bad_encoding" + } + }, + { + "name": "empty_program_bytes_rejected", + "program": "", + "env": "80", + "expect": { + "error": "bad_encoding" + } } ] } From 5a052fc6bd665ac41c914b5dc611da5549f2eec9 Mon Sep 17 00:00:00 2001 From: Evan Date: Sun, 26 Jul 2026 19:29:48 -0700 Subject: [PATCH 07/10] Cover the upper length forms, type rejection, and the dev extra 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. --- python/tests/test_differential.py | 5 +++++ python/tests/test_serialize.py | 35 +++++++++++++++++++++++++++++-- 2 files changed, 38 insertions(+), 2 deletions(-) diff --git a/python/tests/test_differential.py b/python/tests/test_differential.py index f59701c..68ea6c9 100644 --- a/python/tests/test_differential.py +++ b/python/tests/test_differential.py @@ -10,9 +10,14 @@ import sys from pathlib import Path +import pytest + REPO_ROOT = Path(__file__).resolve().parent.parent.parent sys.path.insert(0, str(REPO_ROOT / "tools")) +# The oracle wheels are the `oracles` extra, not `dev`: skip cleanly +# instead of failing collection when only `dev` is installed. +pytest.importorskip("chia_rs") import diff_clvm # noqa: E402 from diff_clvm import Generator, run_bitlisp, run_rs # noqa: E402 diff --git a/python/tests/test_serialize.py b/python/tests/test_serialize.py index 47c350d..22f70c4 100644 --- a/python/tests/test_serialize.py +++ b/python/tests/test_serialize.py @@ -5,11 +5,15 @@ from pathlib import Path import pytest -from clvm import SExp -from clvm.serialize import sexp_to_stream from hypothesis import given from hypothesis import strategies as st +# The oracle wheels are the `oracles` extra, not `dev`: skip cleanly +# instead of failing collection when only `dev` is installed. +clvm = pytest.importorskip("clvm") +from clvm import SExp # noqa: E402 +from clvm.serialize import sexp_to_stream # noqa: E402 + REPO_ROOT = Path(__file__).resolve().parent.parent.parent sys.path.insert(0, str(REPO_ROOT / "python")) @@ -71,3 +75,30 @@ def test_int_codec_negative_power_boundaries(): assert int_to_atom(-32768) == b"\x80\x00" assert int_to_atom(128) == b"\x00\x80" assert int_to_atom(0) == b"" + + +# The hypothesis strategy tops out in the 0xc0 form. The upper length +# forms are covered here deterministically: each length is the floor +# of its form (the smallest length the form may canonically encode), +# checked byte-for-byte against the oracle and round-tripped. The +# 0xf8 floor (128 MiB) is exercised for header canonicality by the +# rejection vectors instead of materializing the atom. +@pytest.mark.parametrize( + ("length", "prefix"), + [(0x40, 0xC0), (0x2000, 0xE0), (0x100000, 0xF0)], +) +def test_length_form_floors_roundtrip_and_match_oracle(length, prefix): + atom = b"\xaa" * length + encoded = serialize(atom) + assert encoded[0] & prefix == prefix + assert deserialize(encoded) == atom + buf = io.BytesIO() + sexp_to_stream(SExp.to(atom), buf) + assert encoded == buf.getvalue() + + +@pytest.mark.parametrize("bad_input", [bytearray(b"\x80"), memoryview(b"\x80")]) +def test_non_bytes_input_rejected(bad_input): + with pytest.raises(BitLispError) as excinfo: + deserialize(bad_input) + assert excinfo.value.code == "bad_encoding" From 0a0958eaa97a59042c79273336a8047be6120d0a Mon Sep 17 00:00:00 2001 From: Evan Date: Sun, 26 Jul 2026 19:30:22 -0700 Subject: [PATCH 08/10] Gate CI on the 10k differential run the plan requires 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. --- .github/workflows/ci.yml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 675d167..ea513c6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -53,3 +53,14 @@ jobs: - name: Vector corpus run: | "${RUNNER_TEMP}/venv/bin/python" tools/run_vectors.py + - name: Differential harness, 10k programs + # The Phase 1 done-criterion gate. The seed varies per run so + # regressions cannot hide behind one fixed slice, and it is + # printed so any failure reproduces locally with + # tools/diff_clvm.py --count 10000 --seed . + env: + DIFF_SEED: ${{ github.run_id }} + run: | + echo "diff harness seed: ${DIFF_SEED}" + "${RUNNER_TEMP}/venv/bin/python" tools/diff_clvm.py \ + --count 10000 --seed "${DIFF_SEED}" From c99af7214b66455ea35932256e494118afe9179a Mon Sep 17 00:00:00 2001 From: Evan Date: Sun, 26 Jul 2026 20:34:32 -0700 Subject: [PATCH 09/10] Ratify D7: the zero cost budget fails closed 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. --- spec/VM.md | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/spec/VM.md b/spec/VM.md index 042c11e..4e28491 100644 --- a/spec/VM.md +++ b/spec/VM.md @@ -260,7 +260,7 @@ pin it. No divergence exists outside this table. "Both oracles" means | D4 | Pair in operator position | `clvm` rejects. `chia-rs` accepts via a legacy apply-style rule (observed: `((A . B) . rest)` dispatches on `A` with arity errors reported for `A`'s operator) | `operator_not_atom` error | The oracles disagree with each other. Strict rejection is the smaller, reviewable surface. PROVISIONAL, see section 8. | `vm/dispatch.json` | | D5 | Deserialization strictness | Both oracles accept non-minimal length encodings, trailing bytes, and (chia-rs) `0xfe` back-references | `bad_encoding` for all three (section 2) | Witness bytes must have exactly one accepted spelling per program. Malleability of the serialized form is a consensus hazard in the Bitcoin context. | `vm/serialize.json` | | D6 | `/` with negative operands | Consensus (`chia-rs`): floor division. The `clvm` package injects a policy error ("deprecated") that is not consensus | Floor division, matching consensus | Intersection parity targets the consensus oracle. The Python package's rejection is library policy, the diff harness treats it as an expected divergence. OPEN QUESTION, see section 8. | `vm/arith.json` | -| D7 | Zero cost budget | Both oracles treat `max_cost = 0` as unlimited | A zero budget is a real budget, no program succeeds under it (section 3.3) | A zero sentinel meaning unlimited is a library convenience, not consensus behavior. In the Bitcoin context the budget derives from transaction weight and is never legitimately zero, and an accidental zero must fail closed rather than open. PROVISIONAL, see section 8. | `vm/dispatch.json` | +| D7 | Zero cost budget | Both oracles treat `max_cost = 0` as unlimited | A zero budget is a real budget, no program succeeds under it (section 3.3) | A zero sentinel meaning unlimited is a library convenience, not consensus behavior. In the Bitcoin context the budget derives from transaction weight and is never legitimately zero, and an accidental zero must fail closed rather than open. Ratified, see section 8. | `vm/dispatch.json` | ## 7. Oracle provenance @@ -293,10 +293,11 @@ these is a spec amendment plus vector update in one reviewed commit. floor semantics, reject negative operands in consensus, or drop `/` entirely and keep only `divmod`. Needs a decision before the operator set freezes. -4. **D7 (zero budget).** Fail-closed implemented: a zero `max_cost` - rejects every program where the oracles treat it as unlimited. - Found by the codebase review, previously undocumented. Confirm - fail-closed, and decide whether the reference should also enforce - the unsigned 64-bit budget bound the hardened implementation will - have (section 3.3 currently records the bound without enforcing - it). +4. **D7 (zero budget).** Fail-closed RATIFIED (decision by Evan, + 2026-07-26): a zero `max_cost` rejects every program where the + oracles treat it as unlimited. A budget bug must reject every + spend, a recoverable liveness failure, rather than hand out + unlimited execution, a soundness failure. Still open: whether the + reference should also enforce the unsigned 64-bit budget bound the + hardened implementation will have (section 3.3 currently records + the bound without enforcing it). From 98a3ba15af182ece1ab8aec9723ad951aea4bd4e Mon Sep 17 00:00:00 2001 From: Evan Date: Sun, 26 Jul 2026 20:34:32 -0700 Subject: [PATCH 10/10] Require Python 3.14 and test exactly that in CI 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. --- .github/workflows/ci.yml | 6 ++++++ pyproject.toml | 4 ++-- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ea513c6..c6b6b58 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -30,6 +30,9 @@ jobs: timeout-minutes: 10 steps: - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5.0.1 + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0 + with: + python-version: "3.14" - name: Install pinned lint tools run: | python3 -m venv "${RUNNER_TEMP}/lint-venv" @@ -43,6 +46,9 @@ jobs: timeout-minutes: 15 steps: - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5.0.1 + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0 + with: + python-version: "3.14" - name: Install package with dev and oracle pins run: | python3 -m venv "${RUNNER_TEMP}/venv" diff --git a/pyproject.toml b/pyproject.toml index b741c14..9f743ea 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -8,7 +8,7 @@ version = "0.0.1" description = "Executable specification for a CLVM-derived Bitcoin predicate VM and matching layer" readme = "README.md" license = "Apache-2.0" -requires-python = ">=3.11" +requires-python = ">=3.14" # Runtime dependencies stay empty on purpose. The reference # implementation is the spec artifact and must be self-contained. @@ -35,7 +35,7 @@ testpaths = ["python/tests"] [tool.ruff] line-length = 88 -target-version = "py311" +target-version = "py314" [tool.ruff.lint] select = ["E", "F", "W", "I", "B", "UP"]