Act on the codebase review: D7, harness reach, corpus strictness

.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"
@@ -53,3 +59,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 <printed 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}"

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
 

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.

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"]

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

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

python/bitlisp/serialize.py

@@ -12,17 +12,17 @@
 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),
     (0xE0, 0x0F, 2, 0x2000),
     (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]

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
 

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"

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. Ratified, see section 8. | `vm/dispatch.json` |
 
 ## 7. Oracle provenance
 
@@ -275,3 +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 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).