diff --git a/docs/spec/01-lottery-hash.md b/docs/spec/01-lottery-hash.md
index 63744afe4..adfebacbf 100644
--- a/docs/spec/01-lottery-hash.md
+++ b/docs/spec/01-lottery-hash.md
@@ -223,10 +223,27 @@ The program is interpreted for `ACCEPT_UNITS = 64` units of 32 lanes, `ACCEPT_HA
 |---|---|
 | Base nonces | the first 64 values of SplitMix64 seeded with `FNV-1a-64("igneum-accept/" || seed words as little-endian bytes)`, each `low32(next()) AND NOT 31`; unit `u` runs lanes `base_u + 0 .. base_u + 31` |
 | Init words `I` | the program's eight seed words (section 1.6) |
-| Dataset | `dataset_elem(idx, S[0], S[1])` of `verify.rs` (the closed form of the version 0.1 packs; `S[0]`, `S[1]` are seed words 0 and 1) at `ACCEPT_DATASET_LOG2 = 28`, 2^28 words, `MASK = 0x0fffffff`, whatever the live dataset size |
+| Dataset | the closed form `dataset_elem(idx, S[0], S[1])` below (the version 0.1 packs' stand-in; `S[0]`, `S[1]` are seed words 0 and 1) at `ACCEPT_DATASET_LOG2 = 28`, 2^28 words, `MASK = 0x0fffffff`, whatever the live dataset size |
 | Address of a load with source value `x` | without an era `idx = x AND MASK`; under an era the form of 1.13.1 at `D = 28`: `k = min(k_off, 2)`, `y = rotl(x * M, R)`, `idx = ((y AND (MASK >> k)) OR ((o AND (2^k - 1)) << (28 - k))) AND MASK` |
 | Execution | section 1.7 exactly, the shadow block included under class v4: after instruction 63 of every iteration the 256 shadow instructions run 27 times with that iteration's `sel` (sub-version 3, AP-F8-3; until it, the test ran the base instructions alone and judged a program the chain never hashes) |
 
+The closed form, 32-bit wrapping arithmetic throughout (`verify.rs`, `dataset_elem`; the rule's only dataset, never the chain's):
+
+```
+dataset_elem(i, S0, S1):
+    x = i XOR S0
+    x = x * 0x9E3779B1
+    x = x XOR (x >> 15)
+    x = x + S1
+    x = x * 0x85EBCA77
+    x = x XOR (x >> 13)
+    x = x * 0xC2B2AE3D
+    x = x XOR (x >> 16)
+    return x
+```
+
+A load reads `dataset_elem(idx, S[0], S[1])` and XORs it into `dst`, as 1.4.1 reads `dataset[idx]`. Test vectors, pinned by `igneum-pow/tests/spec_readback.rs`: `dataset_elem(0x00000fed, 0x9E3779B9, 0x7F4A7C15) = 0x5c7dabd2`; `dataset_elem(0x0fffffff, 0x00000000, 0x00000000) = 0x7662c1ec`. The register initialisation is section 1.6 with `I` the seed words; `sel`, the instruction semantics and the output fold are section 1.7.
+
 During the run: a `load` whose 32 lanes compute one address in any unit rejects the program (`LaneConstantSite`, checked at every load of every iteration and unit, the shadow block has none). After the run, over the 2,048 final register states and 2,048 outputs, in this order:
 
 | Check | Limit | Reject |
diff --git a/igneum-pow/tests/spec_readback.rs b/igneum-pow/tests/spec_readback.rs
index 8f2a1725b..61b1bb0df 100644
--- a/igneum-pow/tests/spec_readback.rs
+++ b/igneum-pow/tests/spec_readback.rs
@@ -6,6 +6,7 @@
 //! row's generator (3 for "class v3", 5 for "generator 5", else 4) equals the id, and, for a class v4 row, that the
 //! chain's own draw with the era seed (the same bytes unless the Note names another) accepts at that attempt.
 //! The constants half is `tools/ci/spec-constants-check.mjs` (the pre-push gate; no build).
+use igneum_pow::verify::dataset_elem;
 use igneum_pow::generator::{attempt_words, generate_from_seed_bytes_program_class, program_id, ProgramClass, GENERATOR_VERSION_V3, GENERATOR_VERSION_V4};
 use std::path::PathBuf;
 
@@ -113,3 +114,30 @@ fn the_chain_draw_accepts_each_class_v4_row_at_its_attempt() {
     }
     assert!(drawn >= 1, "no class v4 row to draw");
 }
+
+/// The closed-form dataset of 1.4.6.4: every `dataset_elem(a, b, c) = d` vector the spec prints is the crate's value.
+#[test]
+fn the_closed_form_vectors_of_the_spec_are_the_crates() {
+    let path = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join(SPEC);
+    let text = std::fs::read_to_string(&path).unwrap();
+    let mut n = 0;
+    for (k, line) in text.lines().enumerate() {
+        let mut rest = line;
+        while let Some(i) = rest.find("dataset_elem(0x") {
+            let tail = &rest[i + "dataset_elem(".len()..];
+            let Some(close) = tail.find(')') else { break };
+            let args: Vec<u32> = tail[..close].split(',').map(|a| u32::from_str_radix(a.trim().trim_start_matches("0x"), 16).unwrap_or_else(|_| panic!("{}:{}: bad vector argument {:?}", SPEC, k + 1, a))).collect();
+            let after = &tail[close + 1..];
+            if args.len() == 3 && after.trim_start().starts_with('=') {
+                let eq = after.find('=').unwrap();
+                let hex: String = after[eq + 1..].trim_start().trim_start_matches("0x").chars().take_while(|c| c.is_ascii_hexdigit()).collect();
+                let want = u32::from_str_radix(&hex, 16).unwrap_or_else(|_| panic!("{}:{}: bad vector value", SPEC, k + 1));
+                let got = dataset_elem(args[0], args[1], args[2]);
+                assert_eq!(got, want, "{}:{}: dataset_elem({:#010x}, {:#010x}, {:#010x}) is {:#010x} in the crate, {:#010x} in the spec", SPEC, k + 1, args[0], args[1], args[2], got, want);
+                n += 1;
+            }
+            rest = &rest[i + 1..];
+        }
+    }
+    assert!(n >= 2, "the spec prints {n} closed-form vectors; two are expected");
+}