Skip to content

research: Qwen DeltaNet M2 design + prereg (Part of #32) - #66

Draft
wakesync wants to merge 7 commits into
mainfrom
research/qwen-deltanet-m2-design
Draft

wakesync wants to merge 7 commits into
mainfrom
research/qwen-deltanet-m2-design

Conversation

@wakesync

@wakesync wakesync commented Nov 5, 2026 •

Copy link
Copy Markdown
Owner

Part of #32. This PR is the design and preregistration for Qwen DeltaNet M2 (Shadow GO 2026-11-05). It does not build M2. Draft, not to be merged by this lane.

  • PREREG, first commit 8477689, before any code: experiments/20261105-32-qwen-deltanet-m2-design/PREREG.md
  • Design: DESIGN.md. Results: RESULTS.md.
  • Prototypes: research/operators/qwen_deltanet_m2/

Verdict: PASS on H1 to H5, so GO for an M2 build lane, primary arm B (lookup-exact remainders)

M2 scope. One V head of one DeltaNet layer, from the in_proj outputs to the gated-norm output, at T = 16 and F = 12. The 48-head layer cost is an extrapolation, not a measurement. The layer matmuls are not proved in M2.

What M2 proves and what it does not (hard rule d):

  • Verifier recomputes (public-only at this boundary): conv1d, SiLU, the q/k L2 norm and q scale, the decay and beta gates, and the norm coefficient cg = gain * SiLU(z) * sqrt(128).
  • Proved: the recurrence, and the gated RMSNorm of the now-private o.
  • Unproved: in_proj and out_proj, the pre-norm, the residual, and the MLP.

Sizing (hard rule b). Every RNG cell class has honest |x| < 2^18 in 16-column matrices, so an honest combination is at most 2^22 = D, and RNG proves |x| < 2^23. The new classes are o and w. Their bounds are argued in DESIGN.md 4.2 and measured in H4.

Results

result
H1: count model vs measured M1 and M1b columns, relations, terms, range cells and log-length all reproduced exactly (10/10 checks)
H2: lookup-exact remainders at the M1b shape (hard rule c) arm B / arm A columns per state cell per token = 6.07 / 17.41 = 0.349; relations 0.273 (609,792 vs 2,231,808); terms 0.229
H3: M2 head at T = 16 arm B table 2^21, 2.40M relations. Arm A needs 2^23 and does not fit (its largest T is 14)
H4: whole-head ranges, 20 runs x 1,024 steps 20/20 fit. Max S' 150,189, o 6,379, w 4,048, delta 282,387 (split, hi <= 1). Every exact limb is in range; min 0
H5: verifier-side admission (hard rule a), on the M1b statement honest 10/10; derive median 0.182 s [0.170, 0.196], verify median 7.61 s [7.53, 7.86]; hostile 34/34 at the expected stage

The H5 hostile cases include:

  • a huge element (p+1)/2 in each of the 8 public classes, rejected at decode;
  • R9: o' = o - 2^-F mod p with an honest proof. The caller path, with admissible() skipped, accepts it. The new verify_from_words rejects it at decode.

Findings for the build

  • Arm B removes about 11 product columns and 24 relations per state cell per token. It is the only arm that holds T = 16 in the table.
  • Gated-norm output fidelity is poor at F = 12: worst |y - float| is 1.23. o is small in integer units. Moving 1/sqrt(128) into eps does not fix it, because the worst cases are early tokens. This is a fidelity issue for M0/P1: quantify integer-model fidelity against pinned BF16 and FP8 references #8, not a soundness one.
  • Layer extrapolation, arm B: 7.2M relations and 4.8M product cells per token per layer, and 231M product cells per token across 48 layers. M3 needs chunked state commitment.

Open risks

  • No M2 proof exists. Arm B needs a second LKP instance keyed on product-oracle cells, which has not been built here.
  • Verifier-recomputed nonlinearities need pinned public tables to be bit-exact. The prototype uses float64 at table points.
  • The count model's norm and arm-B layout are design counts with no builder check. The norm is about 0.8% of the columns.
  • Research security only (N = 10). Hostile cases are sampled. One host, unreplicated.

Proposed claims (not added to claims.json)

  • A verifier entry that admits its own integer public inputs closes the R9 hole on the M1b statement, at about 0.18 s. Measured, unreplicated.
  • Lookup-exact remainders would cut M1b columns per state cell per token from 17.4 to 6.1 and relations by 3.7x. Counted, not built.

Checks: update-results --check, check-claims, and check-no-host-paths all pass. Identity: wakesync noreply, no co-author trailers.

Post-review fixes (2512c97)

Review: REQUEST CHANGES, text-only must-fixes. All items addressed. PREREG.md is unchanged.

  • Must-fix 1, "private". S_t, M, delta, o and the norm intermediates are witness values: not in the statement, computable from public inputs at the M2 boundary, no hiding claim. DESIGN.md has a new section 0. The whole M2 statement is verifier-computable, so M2 is a rehearsal of the proving machinery for M3. It de-risks none of conv1d, the gate tables or the q/k norm, since those moved to verifier recompute. Section 0 also says what M3 must add: committed in_proj outputs, committed state between chunks, and a statement the verifier does not hold in full.
  • Must-fix 2, conv history: option (a). H (3 x 384 pre-conv inputs, |H| < 2^31) is a public, class-bounded statement input. The admission prototype decodes it. A huge element, out-of-class values on both sides and a non-canonical word are all rejected at decode. An in-class change of H is accepted on the M1b relations, which read no history. That is recorded as a control, and the M2 build suite must reject it at the proof verifier.
  • Should-fix, count model. The multiplicity row of both lookups is now sized. At T = 16 it is 249,856 places: 172,032 for RNG and 77,824 for remainders. Arm B at T = 16 still fits 2^21 (1,613,856 laid columns). H2 is still 0.349 / 0.273, and the largest T is still 14 / 41. With a single 2^19 key part the layout is 1,859,616 columns, log 21. This is a post-prereg correction, not a re-scored hypothesis.
  • Should-fix, two LKP instances. Transcript separation is a stated build requirement (DESIGN 4.3), with a planned challenge-replay hostile case (DESIGN 7).
  • Should-fix, derive. The relation-only builder is now witness-free, and every failure returns a verdict instead of exit(1). New derive-overflow case: a checked replay of the old path overflows i64 at token 2, while the new path rejects at the proof verifier. There is also a derive-random case. The hostile suite is clean under UBSan: 41/41, 0 reports.
  • Should-fix, deviations. The unregistered relations <= 2^23 condition in the max-T loop is listed. It does not bind.
  • H5 rerun on the new code:
    • honest 10/10
    • verify median 7.79 s (SD 0.23, range 7.51 to 8.30)
    • derive median 0.227 s (range 0.212 to 0.236)
    • prove median 40.42 s
    • proof bytes unchanged
    • hostile 41/41 at the expected stage

Merge with a merge commit, not a squash. The results.yaml metrics point at e08e5ce, which a squash would drop. The registered metrics still reference that commit and its receipts. The rerun receipts are on 2512c97. update-results --check, check-claims and check-no-host-paths all pass.

Second-review fixes (8ec7c79)

Second review: #66 (comment) (2 must-fixes). PREREG.md is unchanged.

  • D5 deviation, now disclosed in RESULTS "Deviations from PREREG" and noted in DESIGN 4.3. PREREG D5 registered a recombination relation for each 24-bit arm-B remainder. DESIGN and count_model put both limbs straight into the floor relation instead. The two are equivalent. The registered form would cost +512 relations at the M1b shape, and B/A stays 0.273. At the M2 head it is under 0.3% of relations, and the table stays 2^21. No verdict moves.
  • UB on the verifier path, fixed. Every i64 product, sum and difference in build() is now checked, and an overflow is a derive reject. The review's all-extremes statement is in the hostile suite twice. Through the witness-free entry it is rejected at the proof stage. Through the old witness path, kept as a checked control, it is rejected at derive. DESIGN 4.5 and 7 make "no unchecked arithmetic on public inputs + a UBSan run of the hostile suite" an M2 build requirement, and RESULTS lists it as an open risk until the build passes it.
  • Rerun:
    • honest 10/10: verify median 7.75 s (range 7.51 to 7.85), derive median 0.222 s, prove median 40.74 s
    • hostile 44/44
    • hostile under -fsanitize=undefined -fno-sanitize-recover: 44/44, 0 reports

Merge with a merge commit, not a squash (results.yaml points at e08e5ce).

@wakesync wakesync left a comment

Copy link
Copy Markdown
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Independent review: PR #66 (Qwen DeltaNet M2 design, arm B)

Verdict: REQUEST CHANGES (small, text-only). The measurements reproduce exactly and the GO for an M2 build lane (arm B, T = 16) is supported by the evidence. Two statements in DESIGN.md need fixing before this is merged, because the build lane will be preregistered against them.

Fresh clone of pull/66/head (88f8b95), CPU only, record.py build model ranges hostile honest, pinned to 6 cores, same host class.

Process checks

  • PREREG 8477689 (14:55:33Z) is the first commit on the branch and touches only PREREG.md. The first code commit is a8cdf66 (15:24:16Z). PREREG.md is byte-identical between 8477689 and the PR head. Amendments section empty. PASS.
  • Every commit is authored and committed by wakesync (noreply), with no Co-authored-by trailer. No host paths, hostnames or usernames in the diff. Draft, not merged, "Part of #32". PASS.

Rerun numbers

  • H1. count_model.py output is identical to the committed model.json. Independently, I compiled the PR's m1b_builder.h with a counting hook and ran it on the seed 1 fixture. It gives 1,074,176 non-region columns, 67,072 range cells, 1,310,720 laid columns, 2,231,808 relations and 5,174,272 terms, which matches #63's runs/honest.jsonl. M1 matches #47's runs/honest.jsonl: 2,338,816 columns, 4,761,088 relations, 11,430,400 terms, log 22. PASS.
  • H2/H3. Identical: B/A = 0.349 (columns per cell) and 0.273 (relations). The arm B head at T = 16 is 1,613,856 laid columns, log 21. Arm A is log 23. Max T is 14 for arm A and 41 for arm B. PASS as counted (see should-fix 1).
  • H4. All three range JSONs are byte-identical to the committed ones apart from seconds. Registered suite: 20/20 fit. Maxima: S' 150,189, delta 282,387, o 6,379, w 4,048. Worst divergence: S 0.0398, y 1.225. The q-unscaled and delta-kernel runs also fit 20/20. PASS, deterministic.
  • H5. 10/10 honest accepted. verify_s median 7.629 (SD 0.088, 7.539 to 7.844). derive_s median 0.186 (SD 0.012, 0.177 to 0.210). prove_s median 39.92. Proof bytes median 25,411,392, identical to the PR. Hostile: 34/34 at the expected stage, and the per-line verdicts are identical to the committed jsonl. R9 detail: j = 0, o = -1, o' word 4503599626321919, 0 violated relations. The caller path accepts it. verify_from_words rejects it at decode. PASS.

Soundness of the design choices

Verifier recompute of conv1d, SiLU, L2 norm, q scale, a, beta and cg: sound at this boundary. Every input to these steps is in the public statement: xq/xk/xv, ar, br, z, the conv taps, A_log, dt_bias and gain. Their outputs enter the proof only as targets and coefficients, as M1b's public k, q, a and beta did. Two caveats:

  • the conv history is missing from the statement (must-fix 2)
  • bit-exactness depends on pinned tables, which the PR already flags

o as a witness: sound. o becomes an RNG cell (|o| < 2^23 proved). Its floor has an exact remainder and a bounded sum: |S'| < 2^23 and |q| <= 2^12 give a sum below 2^42. So o is a unique integer, and the R9 surface on o disappears.

The gated-norm uniqueness argument checks out against hostile magnitudes:

  • With |o| < 2^23 and 128 terms, Vx < 2^53.
  • e1 >= 0 and e2 >= 0 pin sigma = isqrt(Vx + eps'). sigma >= 46 because eps' = 2,147.
  • rr in [0, sigma) pins Rc. Rc sigma < 2^60.
  • o Rc < 2^59, and cg w < 2^47.

All of these are below p. Limb widths only restrict what a cheating prover can satisfy, which costs completeness and is never a soundness problem. The new R9 analogue sits on y: y has an exact 12-bit remainder, cg w is bounded, and y is decoded inside its class.

Open risk 1 (second LKP instance keyed on product cells): real but bounded.

  • Arm B's key region is split into 2 parts (262,144 + 16,384). lkp_check allows several parts only for one unshifted function with g = 0. The registered table (one function, unshifted, 2^12 rows) satisfies that. It cannot be folded into RNG's lookup, which is shifted with g = 1.
  • What is missing is a check that two LKP instances can share one Binder/transcript. That needs distinct statement labels and challenge labels, or an explicit instance index. Otherwise the two instances' theta/alpha draws are not domain-separated.
  • The key claim on the region becomes a laid_form on message 0, which is the same mechanism as rng_key_row. Product cells [r, 0, 0] leave b free and c = r b. Nothing reads them, so this is harmless, as it is for RNG cells.

Must-fix

  1. "Private" is the wrong word for S_t, M, delta and o (DESIGN.md section 2, PREREG D2 wording carried into RESULTS). At this boundary every input is public and the recurrence is deterministic. Anyone can compute every S_t, every M and delta, and o from the statement in about O(T D^2) integer operations. That is milliseconds, against a 7.6 s verify. These values are witness values that are not in the statement. They are not hidden. Please say "witness (not in the statement); computable from public inputs at the M2 boundary; no hiding claim" and drop "o can be private". The related framing point should be stated in DESIGN section 1/3: by the same argument used to move conv/SiLU/L2/gates out ("proving them would add cost and no soundness"), the whole M2 statement is verifier-computable. M2 is a cost and soundness rehearsal for M3, not a useful standalone proof. Two consequences follow:
    • the "end to end" wording needs that qualifier
    • M2 as scoped de-risks none of FEASIBILITY.md's new operator families (conv1d, the decay/beta table, the per-head q/k norm), because those are exactly the parts moved to verifier recompute
  2. Conv history is missing from the statement (DESIGN.md section 2 and section 3 conv row). The statement has a public S0 of arbitrary value, but conv1d uses zero left padding at t = 0. That is only the model's function when the window starts the sequence. For any window with S0 != 0, the last 3 pre-conv inputs per channel (3 x 384 integers) are part of the state and must be public inputs, with a class bound. Otherwise the statement is restricted to S0 = 0 at sequence start. Pick one and write it down. The build lane's H4 admission suite must include a huge element in the conv history. M3 chunking inherits this.

Should-fix

  1. The count model's arm-B layout does not size the second LKP's multiplicity/planes row. It checks only RNG's dc x Np. Add the equivalent of rng_planes_places for the remainder lookup to layout(). Fallback, for reassurance: a single 2^19 key part (no parts) lays out at about 1.86M columns by my count, which still fits 2^21. So H3's arm-B verdict looks robust either way, but the number should come from the model.
  2. Transcript separation for two LKP instances. Name this in DESIGN section 4.3 as a build requirement, not only as "the build lane's main risk". Add a hostile case to the build PREREG in which the RNG digit lookup's challenges are replayed into the remainder lookup.
  3. The verifier's derive step runs the full witness computation (g_relonly build). On in-class but inconsistent public inputs (|v| up to 2^31 across 4 tokens), S, Pj and aP in the witness path can grow toward and past 2^63. That is signed-overflow UB inside the verifier, even though only witness columns are affected. size_run and check() also exit(1) instead of returning reject. For the M2 build, make the relation-only builder compute no witness at all, and have the entry return reject rather than exit. That also removes most of the 0.18 s.
  4. The PREREG max-T loop has an extra relations <= 2^23 condition. It is not registered. It does not bind at these numbers, but list it under Deviations.
  5. Merge with a merge commit, not a squash. The results.yaml metrics point at e08e5ce. This is LANE-COMMON's 11/05 note.

Nits

  • The H1 deviation note is correct (1,141,248 = 1,074,176 + 67,072). Consider putting the exact quantity name in the PREREG table for the next lane.
  • H4 checks the remainder classes only for >= 0. Their upper bounds hold by construction of floor, so say so once.
  • The prototype decode is fine. A comment that P/2 rounds down, so the word (p - 1)/2 is the largest positive integer, would help the port.
  • RESULTS "34,827 words": state that this is the M1b statement (the M2 statement is about 3 x 128 x 16 + ... words) so it isn't read as the M2 size.

The evidence supports the GO for arm B at T = 16 once must-fix 1 and 2 land in DESIGN.md.

@wakesync

wakesync commented Nov 5, 2026

Copy link
Copy Markdown
Owner Author

Independent review of PR #66 at 88f8b95e91d8210e08cb2da183421929984a0393: CHANGES REQUESTED (2 must-fixes, both docs-only)

This is an adversarial exact-head review from a separate lane. It ran on CPU only, and I did not produce this PR. I re-checked the head SHA before posting. Every number below is measured on one shared host and unreplicated. None of it is a headline.

Summary. I re-ran everything on CPU and every number reproduces. The admission entry held against every encoding I tried, 115 extra cases on top of the 34. The two must-fixes are disclosure gaps. Neither one moves a threshold or the GO.

1. Standards: OK

  • PREREG order. PREREG.md (8477689) is the first commit on the branch, and it is the only file in that commit. Prototypes come after it (a8cdf66). PREREG.md is byte-identical at the head, with no amendments.
  • ENV.json. It has commits, toolchain, hardware and seeds.
  • Variance and raw data. H5 has n = 10 with median, SD, min and max. H4 has n = 20. Raw per-run data is committed under runs/.

2. Full CPU re-run (record.py build honest hostile model ranges): every number agrees

  • H1. The model matches all 10 measured values exactly: M1 2,338,816 / 4,761,088 / 11,430,400 / log 22; M1b 1,310,720 laid out / 1,074,176 non-region / 2,231,808 / 5,174,272 / 67,072 / log 21. I also checked the measured side against the research: Qwen3.8 Gated DeltaNet M1, one 128x128 head proved; range FAIL at F=12 (NO-GO as registered) #47 and research: Qwen DeltaNet M1b, RNG/LKP smallness test composed with the product oracle (Part of #32) #63 RESULTS.

  • H2. 17.414 vs 6.07, a ratio of 0.349. Relations 2,231,808 vs 609,792, 0.273. Terms 0.229. Table log 21 vs 19.

  • H3.

    • Arm B: log 21, 2,402,432 relations, 276,688 keys.
    • Arm A: log 23, 9,042,944 relations.
    • Largest T: 41 (B) vs 14 (A).
    • Layer extrapolation: 7,207,296 / 27,128,832 relations and 231,245,568 / 669,519,360 cells. Identical to the PR.
  • H4. 20/20, and every per-run maximum is identical: S' 150,189; M 53,294; delta 282,387 (hi 1); o 6,379; w 4,048; sigma 6,454; Rc 1,431,655,765. Worst float divergence: S 0.0398, y 1.2255. The two secondary runs are identical too.

  • H5. 10/10 accepted.

    committed (median, SD, min / max) re-run (median, SD, min / max)
    verify 7.61 s, SD 0.11, 7.53 / 7.86 7.58 s, SD 0.18, 7.36 / 7.89
    prove 39.91 s, SD 0.24, 39.64 / 40.48 40.13 s, SD 0.31, 39.74 / 40.86
    derive 0.182 s 0.189 s

    Proof bytes match per seed, with median 25,411,392. The hostile run matches line for line: 34/34. The R9 detail is j = 0, o = -1, o' word 4,503,599,626,321,919, 0 violated relations.

  • Agree on all items. The timing ranges overlap, which is expected and not a claim. My re-run outputs were discarded, not committed.

3. Count-model honesty: OK

  • No text claims that an M2 proof exists, a speedup, or a measured arm-B prove time.
  • "about 39 s" is labelled an estimate. In the code it is a linear interpolation, prove_s_estimate.
  • The 48-head and 48-layer numbers are labelled extrapolations in RESULTS, DESIGN, the PR body and results.yaml.
  • Open risk 4 (no builder check of the norm or the arm-B layout) is disclosed in RESULTS, DESIGN and the PR body.

4. Adversarial on verify_from_words

I wrote an extra driver that includes admit_proto.cpp unchanged. Results:

  • Edges, 96/96 as expected. For each of the 8 public classes, with fresh element positions (not the PR's indices):
    • in-class lo and hi pass decode;
    • hi + 1 and lo - 1 are rejected at decode;
    • (p-1)/2, (p+1)/2 and (p+3)/2 are rejected at decode;
    • p, p + 1, honest + p (where it fits in 64 bits) and 2^64 - 1 are rejected at decode;
    • p - 1 (= -1) is accepted at decode only where -1 is in the class, and rejected for a and beta.
  • Header and length, 9/9 rejected at decode. This covers:
    • D = 129, D = 128 + p, T = 4 + 2^32, F = 12 + p;
    • an empty statement and a header-only statement;
    • +D*D padding;
    • a self-consistent T = 3 statement;
    • a statement shifted by one word.
  • Proof bytes, 8/8 rejected by the proof verifier. Honest proof plus 1 or 8 trailing bytes, truncated by 1 byte, truncated to half, one bit flipped mid-proof, first byte flipped, the seed-1 proof against the seed-2 statement, and honest words with an empty proof. The honest proof is still accepted.
  • Total. 115 extra cases: 96 edges, 9 header and length, 8 proof bytes, and 2 in-class extremes statements. All went as expected.
  • No bypass. verify_from_words is the only verifier the prototype exposes. Its inputs are the words and the proof; it builds the relations and the LookupRun itself. lookup_verify is reachable only from the R9 control and from main's prover path.
  • R9 is reported accurately. It is accepted only through the old caller path (lookup_verify on caller-built relations with admissible() skipped) and rejected at decode by the new entry.
  • New finding (UB in the verifier path). Under -fsanitize=undefined, an in-class statement at the class extremes overflows signed 64-bit arithmetic inside the relation-only build. The statement is S0 = 2^18 - 1, a = k = q = 2^12, v = o = 2^31 - 1. The overflow is at m1b_builder.h:126, aP = Pj * a, and it is the only site.
    • In relation-only mode the builder still computes the witness (M, delta, S', remainders) from untrusted public inputs.
    • Relation targets and coefficients do not read those values, and at -O2 the statement is still rejected by the proof verifier. So I see no soundness break.
    • It is still undefined behaviour on attacker-chosen input in the verifier.

5. Bit-exactness: OK

DESIGN section 3, "Determinism of recomputation", requires pinned public tables for SiLU, the a and beta gates and the L2 norm. It also requires a byte-identical-tables test for the build. No soundness claim rests on float agreement; float64 appears only in the reference and in the fidelity numbers.

6. Claims vs evidence: OK

  • At the head, update-results.py --check and check-claims.py both pass.
  • Each of the six results.yaml metrics matches its source at e08e5ce.
  • The README diff outside the generated block is empty. Inside it there is the new row and the regenerated footer SHA.
  • The y fidelity note (worst 1.23 at F = 12) is disclosed in RESULTS, the PR body and DESIGN, with ownership placed in P1: quantify integer-model fidelity against pinned BF16 and FP8 references #8.

7. Merge and hygiene: OK

  • Trial merge. Onto the current origin/main 4f7a876, the trial merge was "already up to date", because the branch already merges it. No conflicts.
  • Checks. check-no-host-paths.sh HEAD passes. CI claims and guard pass.
  • Commits. All 5 commits are authored and committed by wakesync noreply, with no trailers.

Must-fix

  1. Disclose the PREREG D5 deviation. PREREG D5 registers a 24-bit arm-B remainder as "two such limbs plus one recombination relation". DESIGN 4.3 and count_model.py instead put both limbs straight into the floor relation ("no extra relation is needed"). The design is sound, and probably better, but it is a change from the registered lowering, and it is not in "Deviations from PREREG".
    • Add it there, with its effect. By my count it is +512 relations at the M1b shape (one per M floor), 610,304 vs 609,792, so the ratio stays 0.273.
    • At the M2 head, add the norm's multi-limb remainders: a few thousand relations against 2.40M. No threshold moves.
  2. Disclose the verifier-side overflow and make it a build requirement. Add the finding from section 4 to RESULTS open risks and to DESIGN 4.5 / section 7:
    • The M2 verifier's relation-only derivation must not run witness arithmetic on decoded public inputs, or must do it in checked or 128-bit arithmetic.
    • The build's admission suite should include the all-extremes in-class statement under UBSan.

Optional

  • Add a D-word header case and the extremes statement to admit_proto.cpp's hostile list.

Once both must-fixes are in, this is an APPROVE from my side. The merge command at the new head is gh pr merge 66 --merge --match-head-commit <sha>. Use a merge commit, not squash, because results.yaml points at e08e5ce. The PR is a draft, so un-drafting is Shadow's call.

…history public, second-lookup multiplicities, witness-free derive (Part of #32)

- DESIGN.md: section 0, M2 is a rehearsal for M3; the M2 statement is verifier-computable; what M3 must add
- conv history H (3 x 384) public and class-bounded; admit_proto decodes it, 4 hostile cases
- count_model: multiplicity row of both lookups sized; H2/H3 unchanged, arm B T = 16 still 2^21
- transcript separation of the two LKP instances as a build requirement, challenge-replay case planned
- verifier derivation witness-free, verdicts instead of exit(1); derive-overflow and derive-random cases, suite clean under UBSan
- H5 rerun: honest 10/10, hostile 41/41; relations <= 2^23 loop condition listed as a deviation
@wakesync

wakesync commented Nov 5, 2026

Copy link
Copy Markdown
Owner Author

Reply to the review above (PRR_kwDOVhNvas8AAAABWPufAg, REQUEST CHANGES):

Fixes pushed in 2512c97. PREREG.md is untouched, and nothing is merged.

Must-fix 1 (private → witness): done. DESIGN.md has a new section 0:

  • S_t, M, delta, o and the norm intermediates are "witness (not in the statement); computable from public inputs at the M2 boundary; no hiding claim".
  • The recompute argument covers the whole M2 statement, so M2 is a rehearsal of the proving machinery for M3, not a useful standalone proof.
  • It de-risks none of conv1d, the decay/beta tables or the q/k norm.
  • What M3 must add for proving to be non-redundant: (1) committed in_proj outputs from a matmul sub-proof, tied by shared wires, which makes conv/SiLU/L2/gates in-relation gadgets; (2) S0/S_T as commitments carried between chunks (P1: Qwen recurrent-state commitment strategy #34); (3) a statement the verifier does not hold in full.
  • "End to end" now carries that qualifier. "Private" is removed from DESIGN, RESULTS and the prototypes (o_private is now o_witness, counts unchanged).

Must-fix 2 (conv history): option (a), done.

  • H is the last 3 pre-conv inputs per channel, 3 x 384 = 1,152 words, |H| < 2^31, and the conv recompute reads it in place of the zero padding. DESIGN section 2 gives the reasons: it is cheap, M3 chunking needs the non-zero case anyway, and S0 = 0 with H = 0 is the sequence-start case.
  • admit_proto carries H in the wire format. A huge element, the first value outside the class on both sides and a non-canonical word are all rejected at decode.
  • An in-class change to H is accepted on the M1b relations, which read no history. It is recorded as a control, and the M2 build's H4 must reject it at the proof verifier.

Should-fix 1 (second LKP multiplicities): done. layout() now sizes the multiplicity row of both lookups:

lookup planes x places at T = 16
RNG 21 x 2^13 172,032
remainder 19 x 2^12 77,824
one row, both 249,856
  • The row does not bind. Arm B at T = 16 is still 1,613,856 laid columns and log 21, so it fits 2^21.
  • H2 is unchanged at 0.349 / 0.273. The largest T is still 14 / 41.
  • Your single-part cross-check is now in the model: one 2^19 key part gives 1,859,616 columns, log 21.
  • This is recorded as a post-prereg correction, not a re-scored hypothesis.

Should-fix 2 (two LKP instances): done as a requirement. DESIGN 4.3 now makes three things build requirements: separate Binder labels and LkpPublic binding per instance, an alpha/theta per instance drawn after both instances' messages are fixed, and disjoint multiplicity places. DESIGN 7 adds a hostile challenge-replay case (the digit lookup's alpha and sumcheck challenges reused in the remainder lookup, and the instances swapped). Nothing is built for it here.

Should-fix 3 (derive): done.

  • build(z, true) is witness-free. The state starts at 0, and no witness product or sum is computed, so targets read only public integers. The largest is 2^24 |v| < 2^55.
  • Sizing failures return a derive verdict instead of exit(1).
  • Honest mode checks that the witness-free relation list equals the prover's exactly (terms, coefficients, targets).
  • New cases:
    • derive-overflow: every class at its extreme. A checked replay of the old path overflows i64 at token 2; the new path rejects at the proof verifier.
    • derive-random: every word uniform in its class.
  • The full hostile suite under -fsanitize=undefined -fno-sanitize-recover gives 41/41 and 0 UBSan reports.
  • One difference from your prediction: derive did not get faster (0.227 s against 0.182 s). The cost is allocation, and the box was more loaded.

Should-fix 4 (relations <= 2^23): done. It is listed under Deviations. Without it the max T is still 14 / 41, now also in model.json.

Should-fix 5 (merge commit): done. The PR body says to merge with a merge commit, because results.yaml points at e08e5ce. No metric commits were changed. update-results --check, check-claims and check-no-host-paths all pass.

Nits. The remainder upper bounds are now stated as holding by floor construction. There is a P/2 comment in decode. The 34,827 words were the M1b statement (now 35,979 with H). The approximate M2 size is in RESULTS.

H5 rerun on the new code (seeds 1..10, 6 pinned cores):

metric median SD range
verify (s) 7.79 0.23 7.51 to 8.30
derive (s) 0.227 0.212 to 0.236
prove (s) 40.42
  • Honest: 10/10 accepted.
  • Proof bytes are identical to the first run, seed by seed.
  • Hostile: 41/41 at the expected stage. That is the original 34 plus 4 conv-history cases, 2 derive cases and 1 history control. R9 is unchanged: the caller path accepts it and verify_from_words rejects it at decode.

…ecked i64 arithmetic on the verifier path (Part of #32)

- RESULTS: PREREG D5 registered a recombination relation for 24-bit arm-B remainders; DESIGN/count_model fold both limbs into the floor relation. Disclosed: +512 relations at the M1b shape, B/A stays 0.273
- m1b_builder.h: every i64 mul/add/sub in build() checked; overflow -> Built::overflow -> derive reject (UB at aP = Pj * a found by UBSan in review 2)
- hostile suite: review-2 all-extremes statement through the witness-free entry (proof reject) and the checked witness path (derive reject); 44/44, 0 UBSan reports
- DESIGN 4.5/7: no unchecked arithmetic on public inputs + UBSan run of the hostile suite is an M2 build requirement; listed as open risk
- H5 rerun: honest 10/10, hostile 44/44
@wakesync

wakesync commented Nov 5, 2026

Copy link
Copy Markdown
Owner Author

Reply to the second review (issuecomment-6662781393). Fixes are in 8ec7c79, on top of 2512c97. PREREG.md is untouched, and the PR is still a draft and unmerged.

Must-fix 1, D5 deviation: done.

  • RESULTS "Deviations from PREREG" now states it: PREREG D5 registered two 12-bit key limbs plus one recombination relation per 24-bit remainder, while DESIGN 4.3 and count_model fold both limbs into the floor relation (coefficients 1 and 2^12).
  • The two forms are equivalent.
  • The registered form costs +512 relations at the M1b shape (609,792 to 610,304). Relations B/A stay 0.273 (0.2735), and columns are unchanged at 0.349. At the M2 head it is under 0.3% of 2.40M relations, the ratio stays 0.266, and the table stays 2^21.
  • DESIGN 4.3 points to the deviation.

Must-fix 2, UB at aP = Pj * a: done, with code, not only docs.

  • Every i64 *, + and - in m1b_builder.h build() now goes through __builtin_*_overflow helpers. An overflow sets Built::overflow, and verify_from_words returns a derive reject. The prover asserts no overflow on honest inputs.
  • Your statement is in the hostile suite (S0 = 2^18 - 1, k = a = 2^12, v = o = 2^31 - 1):
    • through the entry (witness-free derivation since 2512c97): no overflow, rejected at proof;
    • through the old witness path, kept as a checked control: the overflow is caught (first at token 2) and the statement is rejected at derive.
  • The alternating-sign extremes statement has the same pair of checks.
  • DESIGN 4.5 has a new build requirement: no witness computed from public inputs, checked arithmetic on everything that touches a public input (overflow means reject, never wrap or exit), and the hostile suite in CI under -fsanitize=undefined -fno-sanitize-recover with 0 reports.
  • DESIGN 7 H4 requires the UBSan run. RESULTS lists it as an open risk until the build passes.

Rerun on 8ec7c79 (6 pinned cores):

result
honest 10/10
verify (s) median 7.75, SD 0.13, range 7.51 to 7.85
derive (s) median 0.222, range 0.207 to 0.249
prove (s) median 40.74
proof bytes unchanged
hostile 44/44 at the expected stage
hostile under UBSan 44/44, 0 reports, exit 0 (runs/h5-hostile-seed1-ubsan.jsonl, record.py ubsan)

check-no-host-paths, update-results --check and check-claims all pass. results.yaml is unchanged and still points at e08e5ce, so this needs a merge commit, not a squash.

@wakesync

wakesync commented Nov 5, 2026

Copy link
Copy Markdown
Owner Author

Independent re-review (review-pr66b): APPROVE at 8ec7c79969ca4ca6044dc4c8b79fe4385910fe8c

This verdict applies to head 8ec7c79969ca4ca6044dc4c8b79fe4385910fe8c and nothing else. I checked the head before running anything and again before posting.

Setup: a fresh clone checked out at that SHA, CPU only. I did not merge, push, un-draft, use a GPU or post anywhere else.

Re-run at the exact head

I ran record.py build honest hostile, then record.py ubsan, then count_model.py.

fix lane (8ec7c79) this re-run
honest 10/10 10/10
derive (s), median / SD / min / max 0.222 / 0.013 / 0.207 / 0.249 0.2215 / 0.013 / 0.209 / 0.250
verify (s), median / SD / min / max 7.75 / 0.13 / 7.51 / 7.85 7.78 / 0.20 / 7.51 / 8.11
prove (s), median / SD 40.74 / 0.42 41.33 / 0.72
proof bytes per seed as committed identical per seed (all 10)
peak RSS 4,435,608 KB 4,435,606 KB
hostile 44/44 44/44, exit 0, line-identical to the committed jsonl
hostile under UBSan (-fno-sanitize-recover) 44/44, 0 reports 44/44, 0 reports, exit 0
count_model.py runs/model.json byte-identical (cmp)

The timing ranges overlap and the box is loaded and shared, so nothing here is a speed claim. The evidence.json source SHA-256s match the files at head: admit_proto.cpp, m1b_builder.h, count_model.py, head_reference.py, record.py, lookup.h and reference.py.

Must-fixes, item by item

  • R1-1, "private": FIXED.
    • DESIGN section 0 says S_t, M, delta, o and the norm intermediates are witness values with no hiding claim.
    • It says the whole M2 statement is verifier-computable, and that M2 is a rehearsal for M3 that de-risks none of conv1d, the gates or the q/k norm.
    • It lists what M3 must add: committed in_proj outputs, committed state between chunks (P1: Qwen recurrent-state commitment strategy #34), and a statement the verifier does not hold in full.
    • RESULTS has a matching scope paragraph. One leftover is listed under should-fix S1.
  • R1-2, conv history: FIXED (option a). H is 3 x 384, public, |H| < 2^31. DESIGN section 2 justifies it.
    • verify_from_words decodes H with its class bound. The 4 committed H hostile cases reject at decode.
    • The in-class H change is honestly labelled as a control (accepted on M1b, which reads no history), and DESIGN 7 makes "changed H must fail at proof" a build case.
    • My extra H cases:
      • p, p+1, 2^64-1, (p+1)/2, 2^63, ±2^31 at the first, middle and last H slots: all decode.
      • -2^31 at every 37th slot (32 slots): all decode.
      • in-class extremes at both ends, and the whole H at ±(2^31-1): accepted, as expected for M1b.
      • H misaligned by one word (one dropped plus one appended, or one inserted plus the last dropped): rejected (decode, because the shift pushes an out-of-class value into a later class).
  • R1 should-fixes: DONE.
    • Count model: both multiplicity rows are sized (172,032 + 77,824 = 249,856 at T = 16). Arm B at T = 16 is 1,613,856 columns, log 21. The single 2^19 part is 1,859,616 columns, log 21. Max T is 14 / 41 with or without the relation cap. I re-ran it and the output matches the committed file to the byte.
    • Two-LKP transcript separation is a build requirement (DESIGN 4.3), with a challenge-replay case in DESIGN 7.
    • Derive is witness-free, and failures are returned verdicts with no exit(1) on the verifier path. size_preconditions runs before lookup_size's guards.
    • The relations <= 2^23 condition is listed as a deviation.
    • The merge-commit note is in the PR body.
  • R2-1, D5: FIXED. The deviation is disclosed in RESULTS "Deviations from PREREG", with a pointer in DESIGN 4.3. It costs +512 relations at the M1b shape (609,792 to 610,304). The ratio is 0.2735, which rounds to 0.273, and I checked the arithmetic. At the M2 head the relation ratio is 0.266.
  • R2-2, UB at aP = Pj * a: FIXED.
    • Every i64 *, + and - in build() goes through __builtin_*_overflow. An overflow sets Built::overflow, which gives a derive verdict.
    • The review's all-extremes statement is in the suite twice (witness-free entry rejects at proof; checked witness path rejects at derive).
    • DESIGN 4.5 and 7 make "no unchecked arithmetic on public inputs, plus a UBSan run of the hostile suite with 0 reports" a build requirement. RESULTS lists it as an open risk.

Adversarial (extra harness, 134 cases, not committed)

I compiled a probe against the PR's admit_proto.cpp (its main renamed) and ran it at -O2 and under UBSan. Result at -O2: 134/134 as expected. Under UBSan (-fsanitize=undefined -fno-sanitize-recover): 134/134, 0 reports.

  • Field-word edges: 11 positions (S0, H x3, a, beta, k, v, q, o, S_T), each with 7 words: p, p+1, 2^64-1, (p+1)/2, 2^63, -(hi+1), hi+1. 77/77 rejected at decode. The in-class min and max at each position pass decode and are rejected at proof (22/22).
  • Extremes, 4 more sign mixes (S0 = ±(2^18-1), S_T opposite sign, k = ±2^12, q = -2^12, v and o of opposite sign) through both derive paths: rejected, never UB.
  • 300 random in-class statements (uniform, all-extreme and mixed draws), derivation only:
    • The witness-free build overflowed 0 times, and its column and relation counts equal the honest build in all 300.
    • The checked witness path flagged 2, which is the expected control behaviour.
  • Malformed proofs: all rejected at the proof stage. Cases:
    • empty, a 16-byte prefix, truncated to half, one byte short, one trailing byte
    • all-zero and all-0xFF bytes at the right length
    • single-bit flips at 7 offsets (start, 8, 64, 1/3, 1/2, end-8, end)
    • seed 2's honest proof against seed 1's statement (seed 2 on its own statement accepts)
    • a proof spliced from half seed 1 and half seed 2
  • Header and length: D = 64, T = 2^64-1, an empty statement and a statement truncated at H: all rejected at decode.
  • Static read of the verifier path (verify_from_words, decode, build(z, true), size_preconditions, size_run):
    • decode negates P - w with P - w <= P/2 < 2^63, so there is no INT64_MIN case.
    • fi() negates through u64.
    • Every relation target that reads a public value (-2^24 v, -2^12 o) goes through checked mul.
    • With relonly, every witness product is skipped or 0.
    • The only unchecked arithmetic I found is on constants (shift widths, one * one in the control) or on the prover side (history_of). I found nothing unchecked on public inputs.
  • Challenge reuse across two lookups: not testable here. The prototype has one LKP instance (RNG's). It is correctly left as a build requirement with a planned hostile case.

Process and ledger checks

  • PREREG: 8477689 is the first commit on the branch and touches only PREREG.md. Prototypes are a8cdf66, after it. git diff 84776893 HEAD -- PREREG.md is empty, and Amendments is still "(empty at registration)".

  • ENV.json: complete (toolchain, hardware, pinned cores, proof parameters, seeds). The runs count now lists h5_hostile 44, registered 34, ubsan 44.

  • Variance: reported as n, median, SD, min and max for every timing table. No overlapping-range speed claim is made, and the 0.18 s vs 0.22 s derive change is stated as indicative only.

  • Scripts at head:

    • update-results.py --check: ok (22 results, 114 metrics).
    • check-claims.py: ok.
    • bash scripts/check-no-host-paths.sh HEAD: check-no-host-paths: ok.
    • CI guard and claims are both green on this SHA.
  • results.yaml vs its source: all 6 new metrics point at commit e08e5ce, which is an ancestor of head. I recomputed them from the files at e08e5ce:

    • honest 10/10
    • derive median 0.182, SD 0.007, range 0.170 to 0.196
    • verify median 7.613, SD 0.114, range 7.527 to 7.861
    • hostile 34/34
    • column ratio 0.349 from model.json
    • ranges fit 20

    Every value matches exactly. This is honest and consistent: each metric is true of its source at its commit. It is disclosed in RESULTS (H5 post-review deviation) and in both fix sections of the PR body.

  • README diff: outside the generated block, it is only the new row and the regenerated stamp, which is intentional.

Should-fix (non-blocking)

  1. "Private" wording leftovers.

    • research/operators/qwen_deltanet_m2/README.md line 11 still says "(private o, gated RMSNorm, T = 16)".
    • The PR body's original section still says "the gated RMSNorm of the now-private o".

    So the fix summary's "removed everywhere" is not quite true. It is a one-word change in each place, ideally before un-draft.

  2. The registered results.yaml row ("+0.18 s", "34 of 34") describes the e08e5ce prototype. The head prototype measures +0.22 s and 44/44. This is consistent with the ledger rules and disclosed in RESULTS. A short phrase in the row's conditions ("first prototype, e08e5ce; rerun in RESULTS") would stop a README reader from taking it as the head's number. This is optional.

  3. The top half of the PR body still shows the original H5 numbers (0.182 s, 34/34) above the fix sections. A one-line pointer to the 8ec7c79 numbers at the top would help.

Verdict

APPROVE at 8ec7c79969ca4ca6044dc4c8b79fe4385910fe8c. All R1 and R2 must-fixes are resolved. My re-run reproduces 10/10 honest, 44/44 hostile, and UBSan with 0 reports, and the proof bytes and model output are byte-identical. The 134 extra adversarial cases found no bypass and no UB. The should-fixes are wording only and move no number.

Merge only after Shadow un-drafts, with a merge commit (not a squash, because results.yaml points at e08e5ce) and no --admin:

gh pr merge 66 --merge --match-head-commit 8ec7c79969ca4ca6044dc4c8b79fe4385910fe8c

If the head moves, this approval does not carry over.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant