BugZoo: tokenizer/import boundary

Tokenization usually happens outside the tensor graph, which makes it easy for a model import to silently disagree about vocabulary size, padding, EOS, or special-token IDs. LLM inference-engine bug studies include tokenizer/config mismatch classes among real production failures:

https://arxiv.org/abs/2506.09713

TorchLean's current contract is focused: once tokens enter the verified fragment, token IDs can be represented as Fin vocabularySize, making out-of-vocabulary IDs unrepresentable. Bounds alone do not establish that two tokenizers assign the same token to the same ID, or that padding and end-of-sequence metadata matches the model. Importers must check those agreements.

structure NN.Examples.BugZoo.TokenizerBoundary.TokenizerContract : Type

The tokenizer metadata that must agree with the model's embedding table.

• vocabularySize : Nat
• paddingTokenId : Fin self.vocabularySize
• endOfSequenceTokenId : Fin self.vocabularySize

structure NN.Examples.BugZoo.TokenizerBoundary.TokenSequence (vocabularySize sequenceLength : Nat) : Type

A token sequence whose IDs are statically bounded by the vocabulary size.

• tokenAt : Fin sequenceLength → Fin vocabularySize

theorem NN.Examples.BugZoo.TokenizerBoundary.paddingTokenId_isValid (contract : TokenizerContract) : ↑contract.paddingTokenId < contract.vocabularySize

The padding token is in range by construction.

theorem NN.Examples.BugZoo.TokenizerBoundary.tokenId_isValid {vocabularySize sequenceLength : Nat} (sequence : TokenSequence vocabularySize sequenceLength) (position : Fin sequenceLength) : ↑(sequence.tokenAt position) < vocabularySize

Every imported token ID is in range by construction.