# Algorithm and correctness contract

## Single-path sampling

The draft token must be sampled from exactly the distribution q recorded in
the proposal. `SimulationRound.draft_uniforms` and the replay APIs now supply
independent draft draws. Accept with min(1, p(x)/q(x)); on rejection sample
normalize(max(p-q, 0)). Proposal rows and target rows must have equal vocabulary
size, finite nonnegative entries, and unit mass. All random inputs are finite
and in [0,1). Inputs after the first rejection are validated too.

The verifier stops after the accepted path or its first replacement. It does
not implement the optional extra target token after accepting the entire path.
This is a distribution-preserving round boundary, but produces at most gamma
tokens per round rather than Algorithm 1's gamma+1.

Reference: [Leviathan et al., ICML 2023, Algorithm 1](https://proceedings.mlr.press/v202/leviathan23a/leviathan23a.pdf).

## Deterministic tree candidates and residual verification

Tree construction chooses ordered, distinct sibling candidates using top-k.
`build_from_model` queries each actual parent prefix separately; the older
`build(depth_logits)` input is only a context-independent fixture interface.
The adaptive builder chooses width from each parent's entropy.

A fixed candidate x is a point-mass proposal, not a random sample from the
builder's full softmax row. Therefore `evaluate_tree` accepts x with probability
r(x), where r starts as the target distribution p. On rejection it removes x
and normalizes the remaining mass before trying the next sibling. If every
candidate fails it samples the residual, emits that replacement, and ends the
round. On acceptance it follows only that branch. At a leaf the round ends.

For the first candidate x, output mass is p(x). Conditional on rejecting x,
the remaining distribution is p(y)/(1-p(x)), so for every y != x its
unconditional mass is (1-p(x))*p(y)/(1-p(x)) = p(y). Applying this identity
recursively across siblings preserves p. Applying it at every accepted prefix
preserves the autoregressive joint law when decoding continues across rounds.
This requires independent acceptance/fallback draws and a target provider
whose logits depend only on the supplied context. A deterministic PRNG is a
reproducibility tool; it is not a mathematical source of independent entropy.

This is deterministic-candidate residual sampling, not a claim to reproduce
SpecInfer's full serving system or its particular multi-draft sampling scheme.
The old deepest-path tie-break heuristic has been removed.

## Target position and batching

A query associated with node x contains the prompt and ancestors, EXCLUDING x.
Its returned next-token distribution scores x. Siblings share one query and
must share the same target row. Nodes must be parent-before-child; duplicate
sibling token ids, inconsistent vocabulary sizes, and inconsistent sibling
scores are rejected.

`score_tree_from_model` is a sequential reference adapter.
`score_tree_from_batch_model` sends all unique parent contexts in one callback;
`score_tree_layers_from_batch_model` sends one callback per depth. Both validate
that returned rows stay in context order before scores are aligned to node IDs.
No tensor tree-attention mask, GPU kernel, trained weights, tokenizer, or real
KV tensors are present.

`decode_adaptive_tree_from_batch_models` uses `AdaptiveTreePolicy` end to end:
the width is derived from every parent's normalized draft entropy, and the next
round's depth is adjusted from accepted-path tokens divided by the proposed
depth. The final round caps its depth to the remaining output budget, so it
does not score discarded suffix tokens.

## Experiments

`compare_tree_decoding` runs both baseline and tree decoding with the same
target callback, prompt, seed, and exact new-token budget. Both providers must
be pure functions of context; stateful providers must be reset by their owner.
Sampled sequences need not match because the algorithms consume different
numbers of random draws. Compare output distributions, not identical strings.

Reports distinguish actual target/draft queries from hypothetical batches.
They measure no wall-clock speedup. The legacy `DecodeMetrics.target_calls`
name was replaced with `target_batches`. Imported experiment records require
matching target-model identifiers, prompts, and continuation lengths.

## Evidence

`correctness_wbtest.mbt` includes Cartesian grids over independent draws:
a binary single-path example yields 2500/10000 occurrences for probability 0.25;
a two-level tree yields joint counts [2000,500,3000,4500] matching its
conditional target distributions. Tests also cover absent-tree fallback tokens,
invalid probabilities/random inputs, query positions, ordering, independent
snapshot state, and actual callback counts. These are reference correctness
checks, not real-model throughput benchmarks.