Merge spec-accept-23 de952ba3 into master (gate: green on de952ba3, recorded by tools/ci/pre-push.sh; landed on the box mirror)
This commit is contained in:
commit
360eb15228
2 changed files with 47 additions and 2 deletions
|
|
@ -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 |
|
||||
|
|
@ -245,7 +262,7 @@ A load site is a load's ordinal within the iteration, 0 to 15, in instruction or
|
|||
|
||||
(c'') The distinct-index ratio. The one test that runs past the 64 units: `ACCEPT_UNITS_DISTINCT_V4 = 4,096` units, the first 4,096 base nonces of the same stream (the 64 of (c) are its first 64), so every site is evaluated `N = 2^20` times. For each site `s`, `d_s` is the number of distinct `idx` values it computed over those evaluations, `W_s = 2^28 >> min(k_off_s, 2)` is its window in words, and the expectation of a uniform source on that window is `E_s = N - N^2 / (2 W_s)` (an integer at these constants: 2^20 - 2^11, 2^20 - 2^12, 2^20 - 2^13). The site's ratio `d_s / E_s` must reach `MIN_DISTINCT_RATIO_V4 = 0.98`; the first site under it, in order, rejects the program (`LowEntropySite`). The implementation compares in f64; the integer comparison `50 d_s >= 49 E_s` gives the same verdict for every value of `d_s` at these constants (the margin is at least 0.32 of a count; adv-accept-3 section 6.1), and an implementation MAY use it. The floor sits in a measured gap: the accepted population's minimum is 0.983 to 0.989 and the rejected population's maximum 0.966 over 20,275 draws of two lanes, so a floor anywhere in 0.967 to 0.988 gives the same verdicts on every program seen (adv-accept-3 section 6.4). `MAX_SOURCE_REPEAT_V4 = 8` exists in the file and is not part of the rule.
|
||||
|
||||
What the parts catch: (a) the empty-list fallback of 1.4.3; (b) registers that saturate to all ones (2.4 percent of class v2 candidates); (c) zero-absorbing register sets, lane-constant load sites, output bias and value-level address repeats (2.1 percent); (a') the cross-hash hot set of a load fed by `or`, `mul` or `mulhi` through the iteration boundary (AP-F8-1); (c') the same set delivered any other way; (c'') a low-entropy index band the lineage rules cannot see (F8's p23, p18, p19, p15, p56). Why (c) uses the closed form: the test is a pure function of the program (no cache, no day), costs about 3 ms on one core for the 64 units and 2.8 s with (c'') on the chosen candidate, and the census checked on 100,000 class v2 programs that its verdict agrees with the memory-hard dataset's on all but 39 threshold-edge cases (section 7.3). Not in the rule, and why: a contraction as the last write (80 percent of programs) and the `or` count are too common and (c) already catches the cases that matter; the load critical path is a hash-rate question, not a weakness; a 2^24 stage of (c'') does not separate the open F8 tail (p4, p8, p10, p34 read the clean seeds' values there; ledger AP-F8-1).
|
||||
What the parts catch: (a) the empty-list fallback of 1.4.3; (b) registers that saturate to all ones (2.4 percent of class v2 candidates, the class v2 census); (c) zero-absorbing register sets, lane-constant load sites, output bias and value-level address repeats (2.1 percent of class v2 candidates); (a') the cross-hash hot set of a load fed by `or`, `mul` or `mulhi` through the iteration boundary (AP-F8-1); (c') the same set delivered any other way; (c'') a low-entropy index band the lineage rules cannot see (F8's p23, p18, p19, p15, p56). Under the shipped rule, measured on 20,000 seeds (adv-accept's attempts census on sub-version 3, 42,711 rejected candidates, 8 October 2026): 68.1 percent of candidates are rejected, flat across attempts; of the rejections (a') takes 83.5 percent, (a) 11.6, (b) 3.0, (c'') 1.1, (c) constant bits 0.4, (c) saturated finals 0.3, (c') 0.05 and (c) the distinct sum 0.04; the accepted attempt is 2.1 on average and 28 at most, 0 seeds of 20,000 reached the cap, and 256 consecutive rejections have probability about 2 x 10^-43. Why (c) uses the closed form: the test is a pure function of the program (no cache, no day), costs about 3 ms on one core for the 64 units and 2.8 s with (c'') on the chosen candidate, and the census checked on 100,000 class v2 programs that its verdict agrees with the memory-hard dataset's on all but 39 threshold-edge cases (section 7.3). Not in the rule, and why: a contraction as the last write (80 percent of programs) and the `or` count are too common and (c) already catches the cases that matter; the load critical path is a hash-rate question, not a weakness; a 2^24 stage of (c'') does not separate the open F8 tail (p4, p8, p10, p34 read the clean seeds' values there; ledger AP-F8-1).
|
||||
|
||||
#### 1.4.6.6 Attempts, the cap, the last resort and the program id
|
||||
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue