ticket #000035: fold dav1d 2026-05-11 §3.4 review into spec text + impl

dav1d returned the §3.4 φ_PRG anchor-map review with a decision set:
HMAC-SHA-512 / 32-byte seed / uint32-be counter from 0 / SHALL-replace
all LOCKED; manifest field renamed; float-map prose corrected; two
ADDs (exhaustion guard + seed-independence rule); M1-policy separation.

Spec text (#000035 §3.4):
- Folded dav1d's full corrected §9.10 wording (RESPONSE_1 §1).
- Manifest field phi_prg_seed → anchor_prg_seed (purpose-scoped, not
  implementation-scoped; phi_prg_seed kept only as a code-local alias;
  phi_seed / m1_anchor_seed rejected as too vague / too policy-tied).
- Float map 2·(u32/2^32)−1 unchanged (KAT compat) but the prose now
  says "uniform over a 2^32-point grid in [-1, 1) with negligible
  finite-grid mean −2^−32" — NOT "unbiased". -1.0 reachable, +1.0
  not. If exact zero-mean is ever needed → midpoint map x =
  2·((u32+0.5)/2^32)−1 with a PHI_PRG_VERSION bump + new KATs, never
  a silent change.
- Added dim_h ≤ 16·2^32 exhaustion guard (4-byte counter ceiling).
- Added seed-independence + single-purpose-seed requirements (seed
  must be generated independently of model/data, not adversary-
  selected, not reused for other PRG domains — no domain-separation
  tag in v1).
- Added §9.10.1: M1 enablement is a mitigation-selection-policy
  decision (e.g. skippable under #000034 NO_ALIGNMENT), not a §9.10
  function-definition question; "MUST NOT claim M1 while still using
  embed_hard_to_vec" prevents fake-M1 deployments.
- Added an endianness-confirmation note: big-endian is pinned to the
  impl + KATs; flip only if v7 TLV convention turns out little-endian
  (would need a PHI_PRG_VERSION bump).
- SHALL-replace wording kept (RFC-2119 strong mandate inside M1).

Implementation (arborist/substrate/anchor_prg.py):
- New dim_h > 16·2^32 → ValueError guard (clean message naming the
  ceiling rather than overflowing the counter deep in _expand).
- bool dim_h now rejected explicitly (isinstance(True, int) is True).
- Module + function docstrings updated: manifest field is
  anchor_prg_seed; seed-independence / single-purpose rules; corrected
  float-map distribution wording (negligible mean −2^−32, not exactly
  zero); endianness note.

Tests (tests/test_anchor_prg.py, 27 → 30):
- test_phi_prg_rejects_bool_dim_h (True/False params).
- test_phi_prg_rejects_dim_h_above_counter_ceiling.

Doc cross-refs: soft-hash-channel-analysis.md §9.2 + §11 status note
the dav1d-reviewed §9.10 wording + anchor_prg_seed field name.
#000035 ticket status + TICKETS.md row updated. AUTOCOUNT markers
for test_anchor_prg.py bumped 27 → 30 across 5 doc files.

Full suite: 2291 passed, 28 skipped.

docs/tickets/ticket-000006-bench-emergent-findings.md

@@ -731,7 +731,7 @@ Two cryptographic-primitive Phase 1 deliverables landed
   `bench/fixtures/phi-alignment/synthetic-checkpoints.jsonl`.
 - **#000035 Phase 1** (earlier today): φ_PRG reference impl at
   `arborist/substrate/anchor_prg.py` (HMAC-SHA-512 counter-mode
-  KDF) + <!--AUTOCOUNT:tests:tests/test_anchor_prg.py-->27<!--/AUTOCOUNT--> tests (was 20; +7 from `de997f7` 2026-05-10 pattern
+  KDF) + <!--AUTOCOUNT:tests:tests/test_anchor_prg.py-->30<!--/AUTOCOUNT--> tests (was 20; +7 from `de997f7` 2026-05-10 pattern
   backfill — prefix-extension closure invariant, hand-computed
   HMAC-SHA-512 first-block formula, parametrized invalid-input
   cones) + <!--AUTOCOUNT:fixture-rows:bench/fixtures/phi-prg/known-answer-tests.jsonl-->10<!--/AUTOCOUNT-->-vector KAT fixture at

docs/tickets/ticket-000035-prg-choice-phi-prg.md

@@ -1,6 +1,6 @@
 # Ticket #000035 — PRG choice for φ_PRG
 
-**Status:** in progress · Phase 1 landed 2026-05-10; v7 §9.10 spec amendment text pinned in §3.4 below, awaits v7 spec maintainer review
+**Status:** in progress · Phase 1 landed 2026-05-10; **§9.10 spec amendment text dav1d-reviewed final 2026-05-11** (§3.4 below holds the folded version). Review decisions applied: manifest field renamed `phi_prg_seed → anchor_prg_seed` (purpose-scoped; `phi_prg_seed` kept as a code-local alias); float-map prose corrected ("uniform over a 2^32-point grid in [-1, 1) with negligible mean −2^−32", not "unbiased" — formula unchanged for KAT compat); `dim_h ≤ 16·2^32` exhaustion guard added to `arborist/substrate/anchor_prg.py` (+ bool-`dim_h` reject); seed-independence / single-purpose-seed rule added; M1-enablement-policy separation (§9.10.1: skipping M1 governed by mitigation-selection policy, e.g. NO_ALIGNMENT per #000034, not by §9.10). HMAC-SHA-512 / 32-byte seed / uint32-be counter / `SHALL`-replace all LOCKED. Remaining: confirm v7's canonical integer endianness (big-endian assumed) before the §9.10 text freezes into the v7 spec; the actual landing-into-v7-spec step still parks on v7 plastic-training gaining a deployment target.
 **Opened:** 2026-05-09
 **Scope:** Pin a specific cryptographic PRG construction for the
 M1 mitigation (PRG-based anchor map) proposed in #000018 §5.2 +
@@ -192,23 +192,85 @@ regression coverage. Generated once, pinned.
 
 ### 3.4 Spec amendment
 
-v7 § 9.10 amendment text:
+v7 § 9.10 amendment text — **dav1d-reviewed final (2026-05-11)**.
+Decision set (`RESPONSE` 2026-05-11): HMAC-SHA-512 — LOCK; manifest
+field `anchor_prg_seed` (purpose-scoped, not implementation-scoped
+— `phi_prg_seed` is an acceptable code-local alias only); seed
+size 32 bytes — LOCK; counter `uint32` big-endian from 0 — LOCK
+(flip to little-endian only if v7's TLV convention already is);
+float map `2·(u32/2^32)−1` kept for KAT compatibility but the
+prose must say "uniform over a 2^32-point grid in [-1, 1) with
+negligible finite-grid mean −2^−32", **not** "unbiased"; `SHALL`
+replace `embed_hard_to_vec` when M1 is enabled (whether M1 itself
+is mandatory is a separate mitigation-selection-policy question).
+Plus an explicit `dim_h ≤ 16·2^32` exhaustion guard and a
+seed-independence requirement.
 
 ```
-The anchor map φ_PRG(C(M), dim_h) is defined as follows:
-  Let SEED be the v7 boot manifest's `phi_prg_seed` field
-  (32-byte committed value).
-  Let counter range over big-endian 4-byte integers from 0.
-  Output := concatenate HMAC-SHA-512(SEED, C(M) ‖ counter)
-            until ≥ dim_h * 4 bytes; truncate.
-  Convert each successive 4 bytes to a float via
-            2 * (uint32_be / 2^32) - 1.
-  The dim_h-vector is the resulting list.
+§ 9.10  Anchor PRG map φ_PRG
 
-φ_PRG SHALL replace the v7 reference linear projection
-embed_hard_to_vec when the M1 mitigation is enabled.
+When M1 is enabled, the v7 anchor map φ_PRG(C(M), dim_h) is defined
+as follows.
+
+Let anchor_prg_seed be the v7 boot manifest's dedicated 32-byte PRG
+seed. The seed MUST be generated independently of the model
+checkpoint and training data, and MUST NOT be adversary-selected.
+The seed MAY be public once committed, but it MUST be committed
+before the corresponding anchor map is evaluated. anchor_prg_seed
+is single-purpose — it MUST NOT be reused for any other PRG domain.
+
+Let C(M) be the fixed-length committed model digest. Let counter
+range over unsigned 4-byte big-endian integers starting at 0.
+
+For counter = 0, 1, 2, … compute:
+
+    block_counter = HMAC-SHA-512(anchor_prg_seed, C(M) ‖ counter_be32)
+
+Concatenate successive blocks until at least dim_h · 4 bytes are
+available; truncate to exactly dim_h · 4 bytes. A 4-byte counter
+admits 2^32 HMAC-SHA-512 blocks of 64 bytes each, so dim_h MUST
+satisfy dim_h ≤ 16 · 2^32; a request beyond that is an error.
+
+Partition the byte stream into dim_h successive 4-byte words.
+Interpret each word as an unsigned big-endian integer u32. Map
+each u32 to a float by:
+
+    x = 2 · (u32 / 2^32) − 1
+
+The resulting dim_h-vector is φ_PRG(C(M), dim_h).
+
+This maps uniformly onto a 2^32-point grid in [-1, 1). The value
+-1.0 is reachable; +1.0 is not. The finite-grid mean is −2^−32,
+which is negligible for the anchor-map use case. If exact
+zero-mean sampling is ever required, the formula MUST be
+version-bumped (e.g. to the midpoint map x = 2·((u32+0.5)/2^32)−1)
+rather than silently changed, and new KAT vectors emitted.
+
+When M1 is enabled, φ_PRG SHALL replace the v7 reference linear
+projection embed_hard_to_vec for the hard-anchor-to-vector map.
+An operator MUST NOT claim M1 while continuing to use
+embed_hard_to_vec.
+
+§ 9.10.1  M1 enablement policy (non-normative pointer)
+
+Whether a given deployment MUST enable M1 is decided by the
+mitigation-selection policy, not by this section. M1 enablement
+MAY be skipped only under an explicit policy rule — for example
+when a current #000034 φ/Hessian alignment probe returns
+NO_ALIGNMENT and the deployment policy accepts the residual risk.
+Once M1 is enabled, § 9.10 above applies in full.
 ```
 
+**Note on counter endianness.** §3.4 currently fixes big-endian.
+Before the §9.10 amendment freezes into the v7 spec, confirm v7's
+canonical integer-byte-order convention: if v7 TLV uses
+little-endian, flip §3.4 to match; if v7 has no established
+convention, big-endian as specified here becomes the canonical
+choice for this PRG. The reference implementation
+(`arborist/substrate/anchor_prg.py`) and the 10 KAT vectors are
+pinned to big-endian; a flip would require a `PHI_PRG_VERSION`
+bump + regenerated KATs.
+
 ## 4. Out of scope
 
 - v7 spec full revision; this ticket lands the §9.10 amendment
@@ -271,7 +333,7 @@ the moment v7 needs it.
   from any version number. Acceptance-criteria §5 item 1 reads
   through to "or equivalent location" so the move doesn't
   invalidate the original criterion.
-- ``tests/test_anchor_prg.py`` — <!--AUTOCOUNT:tests:tests/test_anchor_prg.py-->27<!--/AUTOCOUNT--> tests covering determinism,
+- ``tests/test_anchor_prg.py`` — <!--AUTOCOUNT:tests:tests/test_anchor_prg.py-->30<!--/AUTOCOUNT--> tests covering determinism,
   range invariants, chi² loose-uniformity sanity, dim_h boundary
   (1, 16384), seed-bit-flip avalanche, hash-bit-flip avalanche,
   hand-computed HMAC-SHA-512 first-block formula, prefix-extension

docs/tickets/ticket-000044-autocount-doc-drift-discipline.md

@@ -82,7 +82,7 @@ because the prose IS the inside-of-tag content.
 ### 3.1 `tests`
 
 ```markdown
-<!--AUTOCOUNT:tests:tests/test_anchor_prg.py-->27<!--/AUTOCOUNT-->
+<!--AUTOCOUNT:tests:tests/test_anchor_prg.py-->30<!--/AUTOCOUNT-->
 ```
 
 Live value: `pytest --collect-only -q <path>` count, with