BugZoo: RoPE position accounting #
LLM inference-engine bug studies report cache, RoPE, tokenizer/config, batching, and resource boundary bugs across real serving stacks:
https://arxiv.org/abs/2506.09713
TorchLean does not model every production RoPE kernel. It can make the position schedule explicit. A KV-cache or decode importer should not infer positions from ambient mutable state; it should hand over a schedule that Lean can inspect.
def
NN.Examples.BugZoo.RoPEPosition.append
{seqLen : ℕ}
(schedule : TorchLean.Tensor ℕ [seqLen])
(position : ℕ := seqLen)
:
TorchLean.Tensor ℕ [seqLen + 1]
Append one position to the tensor schedule supplied to rotary or absolute position embeddings.
The default is the old sequence length, matching the zero-based, unshifted convention.
An offset or sliding-window schedule can supply position explicitly. No rotation kernel is
evaluated or verified by this function.