Spec purity: move the VM record into docs/

CLAUDE.md

@@ -59,12 +59,16 @@ In practice this means:
 
 1. **Spec before code.** No consensus-relevant behavior lands in
    `python/bitlisp/` without a section in `spec/` it can cite. Every PR
-   touching semantics references its spec section.
+   touching semantics references its spec section. The spec states
+   behavior only, and stays complete enough on its own to predict
+   every vector's outcome. Rationale, oracle provenance, and decision
+   records live in `docs/` (for the VM, `docs/vm-record.md`).
 2. **Vectors are the source of truth between sessions.** Sessions are
    stateless, the vector corpus is not. Any behavior worth keeping becomes
    a vector in `vectors/` the same day.
 3. **Divergence is documented, never silent.** Anywhere BitLisp differs
-   from CLVM, the divergence table in `spec/VM.md` says so and why.
+   from CLVM, the divergence table in `docs/vm-record.md` says so and
+   why.
 4. **The novel layer gets adversarial treatment first.** The matching rules
    (`spec/MATCHING.md`) have no external reference. They get
    property-based invariants and theft-bug regression vectors before any
@@ -94,7 +98,7 @@ a spec decision rather than picking a plausible reading.
   pinned in `pyproject.toml` under the `oracles` extra, and, where no
   usable wheel exists, snapshots vendored verbatim from tagged
   upstream releases (the Bitcoin Core test framework under
-  `tools/oracle/`). Provenance is recorded in `spec/VM.md`.
+  `tools/oracle/`). Provenance is recorded in `docs/vm-record.md`.
 - Chia test vectors are vendored as data into `vectors/upstream/` with
   provenance headers. CI never fetches from the network.
 - `tools/fetch-references.sh` clones upstream repos into git-ignored

README.md

@@ -13,12 +13,12 @@ The phased plan is in [docs/execution-plan.md](docs/execution-plan.md).
 
 | Path | Contents |
 | --- | --- |
-| `spec/` | The specification. `SPEC.md` (architecture), `VM.md` (evaluator + divergence table), `CONDITIONS.md` (condition vocabulary), `MATCHING.md` (tx matching rules), `COSTS.md` (cost model) |
+| `spec/` | The specification. `SPEC.md` (architecture), `VM.md` (evaluator), `CONDITIONS.md` (condition vocabulary), `MATCHING.md` (tx matching rules), `COSTS.md` (cost model) |
 | `python/bitlisp/` | Python reference implementation, the executable spec artifact |
 | `vectors/` | Test vector corpus: `vm/`, `conditions/`, `matching/`, plus `upstream/` for vendored Chia vectors |
 | `tools/` | Vector runner, corpus generators, measurement tooling |
 | `ci/` | Lint tooling with pinned versions |
-| `docs/` | Evaluation doc and essay drafts |
+| `docs/` | Evaluation doc, execution plan, the VM record (divergence table, oracle provenance, design decisions), essay drafts |
 
 ## Running the suite
 

docs/README.md

@@ -5,6 +5,9 @@
   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.
+- [vm-record.md](vm-record.md): the VM record behind spec/VM.md, the
+  divergence table, the oracle provenance, and the design decision
+  record. Cited by CLAUDE.md ground rule 3.
 - [opcode-comparison.md](opcode-comparison.md): informative side-by-side
   of the CLVM, bllsh, and BitLisp operator sets.
 - Essay drafts land here in Phase 4.

docs/execution-plan.md

@@ -43,7 +43,7 @@
 - [x] Cherry-pick from bll-consensus: CI config, vector-runner scaffolding, any generic utilities. No history fork.
 - [x] CI from day 1: pytest + vector runner + `hypothesis` property suite (empty is fine; the gate exists before the tests do).
 - [x] **Reference-material policy (no submodules, deliberately):**
-  - Oracles = released artifacts: `clvm` + `chia_rs` wheels pinned in the lockfile (dev deps only); upstream commit hashes recorded in `VM.md` provenance. Hardened phase: intersection diffing stays at the vector and corpus level through the Python harness and the pinned wheels, `clvm_rs` consulted as source only.
+  - Oracles = released artifacts: `clvm` + `chia_rs` wheels pinned in the lockfile (dev deps only); upstream commit hashes recorded in the VM record's provenance (`docs/vm-record.md`). Hardened phase: intersection diffing stays at the vector and corpus level through the Python harness and the pinned wheels, `clvm_rs` consulted as source only.
   - Chia's official test vectors vendored as **data** into `vectors/upstream/` with provenance headers (repo, commit, license). CI never fetches from the network.
   - `tools/fetch-references.sh` clones clvm/clvm_rs/chia_rs into git-ignored `references/`.
   - **Upstream sync is a governance event, never a float:** on each upstream clvm/chia_rs release, triage the changelog — *adopt* (semantics we want: spec amendment + vectors + pin bump in one reviewed commit), *take* (oracle-only bug fix: pin bump), or *decline* (Chia-specific: rationale recorded in the divergence table). Every pin bump is a commit with reasons; oracle drift is never ambient.
@@ -67,15 +67,15 @@
 **Goal:** a minimal Python evaluator whose shared core is bit-for-bit CLVM-equivalent, with divergences enumerated.
 
 - [x] Implement the evaluator in `python/bitlisp/` — own code, not a wrapper (it is the spec artifact), small and boring: cons cells, serialization, operator dispatch, cost accounting.
-- [x] Define operator set in `VM.md`: CLVM core **minus** BLS operators, **plus** `secp_verify` (BIP340, assertive semantics deferred to condition layer). Divergence table with rationale per row. Amended after the Phase 1 close: `sha256tree` adopted 2026-07-29 (decision by Evan, VM.md divergence D9).
+- [x] Define operator set in `VM.md`: CLVM core **minus** BLS operators, **plus** `secp_verify` (BIP340, assertive semantics deferred to condition layer). Divergence table with rationale per row. Amended after the Phase 1 close: `sha256tree` adopted 2026-07-29 (decision by Evan, divergence D9 in `docs/vm-record.md`).
 - [x] Inherit the CLVM cost table (`COSTS.md`); weight-mapping section stubbed for Phase 3 data.
 - [x] **Differential harness v1** (`tools/diff_clvm.py`): run every intersection program through bitlisp-python AND `clvm`/`chia_rs`; assert identical (result, cost) or identical error class.
 - [x] Import Chia's official CLVM test vectors for the intersection; generate randomized program corpus (Claude Code task: corpus generator with size/depth knobs).
-- [x] Divergent operators tested against their own oracles (`secp_verify` → BIP340 official vectors + Bitcoin Core's test-framework implementation, vendored). The original `coincurve` plan was dropped for lack of a usable wheel, decision recorded in VM.md section 7.
+- [x] Divergent operators tested against their own oracles (`secp_verify` → BIP340 official vectors + Bitcoin Core's test-framework implementation, vendored). The original `coincurve` plan was dropped for lack of a usable wheel, decision recorded in the VM record's oracle provenance (`docs/vm-record.md`).
 
 **Done when:** 100% pass on intersection vectors + 10k randomized corpus programs with zero unexplained divergence; divergence table complete.
 
-**Done 2026-07-29.** All divergence decisions ratified or explicitly assigned to Phase 3 (VM.md section 8). Verified fresh: 76 unit tests, 460 vector cases, the 832-case vendored upstream corpus, `diff_clvm.py --count 10000 --seed 20260729`, and `diff_secp.py --seed 20260729` with three verifiers, all zero failures. Cost-table audit clean in both directions after adding the raise-operator charge-order statement.
+**Done 2026-07-29.** All divergence decisions ratified or explicitly assigned to Phase 3 (the design decision record, `docs/vm-record.md`). Verified fresh: 76 unit tests, 460 vector cases, the 832-case vendored upstream corpus, `diff_clvm.py --count 10000 --seed 20260729`, and `diff_secp.py --seed 20260729` with three verifiers, all zero failures. Cost-table audit clean in both directions after adding the raise-operator charge-order statement.
 
 **Claude Code fit:** excellent — mechanical, oracle-checked, test-first. Ideal sessions: one operator family per session (arith, bytes/strings, tree ops, crypto), each ending with vectors committed.
 
@@ -105,7 +105,7 @@
 **Reference material for this phase (recorded 2026-07-29, per Evan):**
 
 - **Condition costing has five years of deployed CLVM learnings: read them before designing ours.** Chia's deployed per-condition costs are the baseline, and CHIP-0049 (the Chia 3.0 hard fork, in review) revises them: a base cost of 500 per condition beyond the first 100 of each coin spend, announcement conditions always priced, and the hard 1,024-announcement cap removed in favor of pricing. That direction is consistent with obligation 2's pricing approach, applied by the team with production data. Two decisions to make deliberately rather than inherit: whether a per-spend free tier (their first-100 carve-out) is acceptable or a cliff we reject, and which precedent prices our tx-scoped SEND/RECV_MESSAGE conditions. Ours port Chia's SEND_MESSAGE and RECEIVE_MESSAGE (CHIP-0025), the announcements' successors, and CHIP-0049's always-priced exception enumerates only the four announcement codes, leaving Chia's own message conditions on the free tier, so the precedent is split and must be chosen, not assumed.
-- **Taproot output construction: out of the VM (ratified), the condition-layer form open (decide in CONDITIONS.md).** bllsh ships `secp256k1_muladd`, a general EC linear-combination operator, largely so programs can verify taproot tweaks in-language. BitLisp will meet the same need when covenant recursion constructs a successor coin whose scriptPubKey is taproot(internal key, tree). The conditions-architecture candidate is a condition form that commits to the taproot components and lets the one hardened validator compute the tweak natively, keeping EC arithmetic out of the consensus VM. Decide the form when CONDITIONS.md v0 is drafted, and record the muladd decline rationale next to it (VM.md section 8, D2 entry, already records the v0 decline).
+- **Taproot output construction: out of the VM (ratified), the condition-layer form open (decide in CONDITIONS.md).** bllsh ships `secp256k1_muladd`, a general EC linear-combination operator, largely so programs can verify taproot tweaks in-language. BitLisp will meet the same need when covenant recursion constructs a successor coin whose scriptPubKey is taproot(internal key, tree). The conditions-architecture candidate is a condition form that commits to the taproot components and lets the one hardened validator compute the tweak natively, keeping EC arithmetic out of the consensus VM. Decide the form when CONDITIONS.md v0 is drafted, and record the muladd decline rationale next to it (the D2 entry in `docs/vm-record.md` already records the v0 decline).
 
 **Done when:** invariant suite green over large generated corpora; adversarial corpus ≥ 50 hand-designed vectors each citing a MATCHING.md rule; a reviewer can read MATCHING.md alone and predict every vector's outcome.
 

docs/opcode-comparison.md

@@ -9,7 +9,7 @@ Sources, as read on 2026-07-29:
 
 - **CLVM**: the consensus operator set as dispatched by the pinned
   consensus oracle `chia-rs` 0.46.0 (upstream commit `7d487907`,
-  provenance in spec/VM.md section 7), cross-read against the
+  provenance in [vm-record.md](vm-record.md)), cross-read against the
   `clvm_rs` dispatch table in `references/`. Flag-gated and
   guard-only operators are marked.
 - **bllsh**: Anthony Towns' bll implementation,
@@ -154,8 +154,8 @@ In BitLisp that surface belongs to
   sits on 0x3f with upstream's own opcode, semantics, and cost
   constants, adopted while the operator is still flag-gated there so
   the two converge when Chia's 3.0 fork activates. Every removal and
-  addition has a rationale row in the divergence table, spec/VM.md
-  section 6.
+  addition has a rationale row in the divergence table in
+  [vm-record.md](vm-record.md).
 - **bllsh relative to CLVM** reworks the core rather than curating
   it: division is gone, the two shifts collapse into one operator,
   bitwise moves from integers to byte strings, list construction
@@ -165,7 +165,8 @@ In BitLisp that surface belongs to
   verification over secp256k1. BitLisp's `secp_verify` follows
   bllsh's `bip340_verify` precedent for tri-state semantics (empty
   signature returns nil, invalid signature raises), a debt recorded
-  in the D2 decision record. CLVM is the outlier with raise-only
+  in the D2 entry of [vm-record.md](vm-record.md). CLVM is the
+  outlier with raise-only
   ECDSA.
 - **What only BitLisp has** is mostly not visible in an opcode
   table: the closed operator set, strict canonical deserialization,