dryz

Is llama.cpp's DRY sampler correct? An exhaustive verification of its hand-rolled reverse Z-algorithm suffix-match length against an independent suffix-repeat oracle.

The DRY ("don't repeat yourself") sampler penalizes a candidate next token by multiplier * base^(L - allowed_length), where L is the length of the longest suffix of the recent token history that emitting that token would extend into a repeat. L is computed by a hand-rolled reverse Z-algorithm over the last-n tokens, with a window cap and sequence-breaker restart logic (src/llama-sampler.cpp, Steps 1-4). Hand-rolled string matchers of exactly this kind produced earlier findings in this project's llama.cpp audits, so this repo checks whether DRY's match length is ever wrong.

Result

It is not. Over the searched space the shipped DRY match length is exactly correct.

The penalty is made exactly invertible: with multiplier = 1, base = 2, allowed_length = 1, the logit delta applied to candidate z is exactly 2^(L_z - 1) for L_z >= 1 and 0 otherwise, so L_z is recovered by exact float equality, L_z = 1 + log2(delta). That inverted length is compared to a clean-room suffix-repeat oracle, cross-checked by two genuinely different formulations that must agree first: one keys on the earlier positions where the token appears and matches backward, the other appends the token, forms the extended string, and finds the longest recurring suffix that includes it. They are different algorithms computing the same quantity, so a mistake in one does not replicate in the other; they agree on every one of the 797,157 base cases (0 self-disagreements). The library is then compared to this reference across three configurations:

• Base (no window cap, no breaker): 797,157 cases, 0 mismatches.
• Window cap (penalty_last_n = 4): 797,157 cases, 0 mismatches.
• Single-token sequence breaker: 797,157 cases, 0 mismatches.

Total 2,391,471 differential cases over all token histories of length 1..11 on a 3-symbol alphabet (plus a separate 1,048,560-case run on a 4-symbol alphabet up to length 8, also 0 mismatches). The library's reverse-Z match length, including the window-cap truncation and the single-token-breaker rep_limit logic, equals the independent oracle on every case. This is, as far as I know, the first exhaustive verification of this kernel; it ships as a correctness certificate for the DRY suffix-match at build 9760, commit 6ee0f65793.

Why the certificate is trustworthy

• Real subject. The harness links the shipped llama_sampler_init_dry / accept / apply from libllama (Homebrew build 9760, commit 6ee0f65793) and drives the real sampler on synthetic token histories. Harness-eval is production-eval; nothing is transcribed. The vocabulary is loaded vocab_only (no tensors, no decode, no Metal), needed only for the sampler's const llama_vocab * argument.
• Exact, self-consistent oracle. L_z is an integer recovered by exact float equality, not a timing or a probability. The reference is computed by two genuinely different algorithms (position-keyed backward matching and extended-string suffix matching) that must agree before either is compared to the library (0 disagreements over the whole search), and is validated against the algorithm's own worked example.
• Positive controls fire. A periodic history has a known closed-form match length that both the library and the oracle reproduce; a non-vacuity injection compares the library against a deliberately off-by-one reference and flags 3,276 cases, proving exact-equality can see a wrong length; and the negative control multiplier = 0 yields zero deltas, proving the harness reads the DRY signal and not noise.
• A false positive in the oracle was caught, not shipped. An early version of the oracle did not model that DRY deliberately does not penalize a single-token sequence breaker (Step 4, L3121); this produced 3,368 apparent "mismatches" that were the oracle's error, not the library's. Reading the source and modeling the exclusion removed them, and the result is exact. This is the same discipline that separates a real bug from a reference-model mistake.

Scope

Fully CPU, deterministic, exact; no decode, no model tensors, no GPU. The certificate covers the base, window-cap, and single-token-breaker configurations over the searched history family; the audited quantity is the integer match length L_z, which fully determines the penalty. Multi-token restart sequences carry a limitation that the shipped code itself documents (a fully-contained restart sequence can fail to suppress a longer one), so they are a known, disclosed edge and are out of scope here. The exact floating-point penalty for base != 2 and interactions with other samplers are also out of scope.

Run

./run.sh /path/to/any-model.gguf

Needs the Homebrew llama.cpp at /opt/homebrew and any local GGUF (for the vocab-only load). Fully CPU, deterministic; the whole 2.4-million-case sweep runs in a few seconds.

Files

• dryz.cpp — links the shipped DRY sampler; inverts the penalty to L_z, the two clean-room oracles and the window-cap/breaker model, the exhaustive enumeration, and the three controls.
• PREREG.md — the pre-registration.
• results/main.json — machine-checked output.

License

MIT.