0005 the proof standard and the oracle each family is frozen from - CyrilB1531/lodestar GitHub Wiki
0005 โ The proof standard and the oracle each family is frozen from
Status: accepted ยท Date: 2026-09-20
Context
Twelve records decided one thing between them: what this repository accepts as a proof
of behaviour, and which reference each family of members is held to. They were written
where the question arose โ 0007 at Metaphone, 0013 and 0014 at SentencePiece,
0017, 0034 and 0127 at BPE, 0036 at a metric with no reference, 0075 at Double
Metaphone, 0077 at the keyword extractors, 0143 at the conformal quantile, 0144 and
its amendment 0146 at vocab.txt โ so a reader asking "how is this proven, and against
what" had to find twelve files to learn one answer. This record is that answer, and the
twelve are removed with it.
Python is a development dependency and never a runtime one. Every corpus under
tests/oracles/ is generated by tools/generate_oracles.py against libraries pinned by
hash in tools/requirements.lock.txt โ and in tools/requirements-nodeps.txt for the two
that cannot be resolved normally โ and each corpus's metadata names the library and the
version it was frozen from, so a later divergence is traceable to a release rather than to
"the reference". The Oracles are reproducible job regenerates and compares numbers, not
bytes (tools/compare_oracles.py).
Decision
(a) What counts as proof here
The standard is a value frozen from the canonical reference into tests/oracles/*.json
and replayed against the C#, compared at 1e-9 for floats and exactly for strings. Not a
hand-written expectation, and not a second implementation of the same idea: the corpus is
the reference's own output, captured once and committed. A row in docs/equivalence.md
lands in the same commit as the member it maps.
Where no seed can be frozen, a distributional comparison is admissible (0034). Over
many encodes of a fixture, the set of reachable outputs and their frequencies are a property
of the algorithm, and a corpus can hold them. It is the weaker instrument โ it proves a
distribution rather than a behaviour, and it wants a large sample for a tight bound โ but it
is an instrument, and it is this repository's standing answer for any reference that cannot be
pinned. The consequence is the point of stating it: "no deterministic implementation
reproduces it" describes such a behaviour, it does not excuse refusing it. BPE dropout
is measured to have no seed at all (tokenizers draws from Rust's thread_rng, which
random.seed does not reach) and is refused anyway โ for want of a user, zero of 23
surveyed models declaring one, not for want of a proof. A single file that declares it
reopens the question.
A member may ship with no oracle only when all three of these hold, and it must carry all
three (0036):
- No reference exists to freeze. The canonical library does not implement it โ not that the reference is inconvenient, or the corpus would be large. If one appears later, the exception is retired and the member joins the corpus.
- Its definition is pinned by tests that state each choice. A member without a reference has variants, and the variant chosen is a decision; each clause of the definition gets a test, so a later change fails rather than drifts.
- The documentation says it is not verified against a reference โ on the member's
reference page, and in its
docs/equivalence.mdrow, whose Python column reads "no counterpart" rather than a function name. A reader learns this from the documentation, never from a surprise.
ReciprocalRank is the only member shipping under that exception, and the count is the
measure: a second citation is the moment to ask whether the rule became a habit. 0075
declined to spend it on Double Metaphone once two independent implementations were measured
to agree on 401 of 401 primaries โ an exception is worth less every time it is spent loosely.
(b) The reference each family is frozen from
Versions are today's, read from tools/requirements.lock.txt.
| family | reference, pinned version | the scope of the parity, and what is deliberately outside it | record |
|---|---|---|---|
| SentencePiece / Unigram | sentencepiece 0.2.2 |
Frozen over XLM-R's real 250 002-piece vocabulary, re-emitted by tools/fetch_xlmr_vocab.py into tests/oracles/xlmr_fairseq.model at the ids HuggingFace gives them and keeping the stock nmt_nfkc map. Outside: the unknown-piece penalty is floored at min(0, min_score) - 10, which binds only for a hand-built vocabulary whose scores are all positive, and is the safe direction. |
0013, 0014 |
| The precompiled normalizer | sentencepiece 0.2.2, plus tests/oracles/custom_norm.model's three hand-written rules |
The precompiled_charsmap blob is interpreted โ darts-clone trie, same longest-match walk โ rather than reimplemented on string.Normalize(FormKC): measured over all 149 251 assigned code points, the map and NFKC differ on 181, of which 136 were assigned to Unicode after the map was compiled, so that gap grows with every Unicode release and differs per runtime. Outside: a normalizer named without a map, a map that will not parse, and NFKC in a tokenizer.json are refused rather than partly applied. |
0014 |
| BPE, byte-level and classic | tokenizers 0.23.2 |
End-to-end, token for token, over GPT-2's vendored 50 257-entry vocabulary and merge table, and over a small classic model for the code-point lineage; both directions, CJK and emoji included. Outside: Llama-3 and Qwen2 are proven at the split level only, their Split regexes replayed from two ungated mirrors, with no vendored vocabulary; byte_fallback is refused, so Llama-2 and Mistral v0.1 have no class here and the guide says so; a non-zero dropout is refused per (a); and astral letters and digits split differently, because .NET's \p{L}/\p{N} test one UTF-16 code unit at a time where Rust's regex matches by code point. |
0017, 0034 |
| BPE encode speed | Microsoft.ML.Tokenizers 2.0.0's CodeGenTokenizer โ a .NET incumbent, not a Python oracle |
The bar is the incumbent computing the same ids: both sides read tokenizer_30k_bpe.json and return identical ids over the corpus, and Lodestar.Embeddings must not be slower on that row. BpeBenchmarks keeps Unigram as its baseline as a record for the nightly series, no longer as a 2ร acceptance bar โ the two benchmarks do not do the same work. |
0127 |
WordPiece from a vocab.txt |
tokenizers 0.23.2 |
VocabTxtLoader sets BasicTokenization, so the route documented for stock BERT runs BertNormalizer and BertPreTokenizer without a flag; vocab_txt.json replays it on a cased and an uncased model. The normalizer drops NUL, U+FFFD and the Cc, Cf, Cs and Co characters but tab, newline and return, and keeps unassigned (Cn) code points โ is_control tests a control in the narrow sense, not a category beginning with C, so dropping them lost text that BERT reads as [UNK]. Cs stays on the list and has no upstream counterpart: a Rust char cannot hold a surrogate and a .NET string can. Outside: TokenizerJsonLoader leaves the flag off and still refuses a full BertNormalizer. |
0144, amended by 0146 |
| Soundex, NYSIIS, Metaphone, match rating | jellyfish 1.2.1 |
Soundex and NYSIIS take the shared random corpus phonetics.json, 402 inputs, at 100 %. Metaphone is validated on real words โ metaphone.json, ~120 English names and words chosen to cover the rules. Outside: jellyfish's behaviour on degenerate letter sequences ("ghhh", "xhdzhumzj") is its C implementation's, of no value to reproduce, and is not. |
0007 |
| Double Metaphone | doublemetaphone 1.2 |
A second phonetics oracle because jellyfish 1.2.1 exports no Double Metaphone at all. Chosen on a 401-word comparison: metaphone 0.6 agrees on every primary but emits a trailing space and has not shipped since 2016, phonetics 1.0.5 drops characters from keys, abydos is GPLv3 and excluded by decision 0002. The secondary is normalised to "" for "no alternate" on the way into the corpus. |
0075 |
| RAKE | rake-nltk 1.0.6 |
The stop-word list is passed in, never downloaded: RakeOptions.StopWords defaults to the assembly's own StopWords.English and the generator hands rake_nltk.Rake that same list, which is what makes the corpus a parity claim rather than a comparison of two lists wearing one name. |
0077 |
| TextRank | summa 1.2.0, hash-pinned in tools/requirements-nodeps.txt |
Numerical parity at the same 1e-9: summa solves the eigenproblem through scipy.linalg.eig, the shipped graph reaches the same ranking by power iteration. summa reads eigenvector column 0 unconditionally, which is not reproducibly the dominant one โ with eigenvalue 0.85 at multiplicity 3 the column order is the BLAS build's โ so the generator patches summa.keywords._pagerank for the span of each call and selects the dominant left eigenvector by index, asserting dominance and vแตM โ ฮปvแต before returning. Outside: Words past the graph's size returns every node there is where summa raises IndexError. |
0077 |
| MMR | keybert 0.9.0, hash-pinned in tools/requirements-nodeps.txt and installed --no-deps |
mmr.json stores the selected index set and no scores, and the test compares sets. Outside: keybert parameterises diversity = 1 - ฮป where Mmr.Select takes the literature's ฮป; it rounds every similarity to four decimals before comparing, which decides near ties on the fifth digit; and it re-sorts its picks by relevance, discarding the selection order Mmr.Select promises. None of the three is reproduced. |
0077 |
| Split conformal | mapie 1.5.0 |
ConformalQuantileRule.Ceiling โ k = ceil((n + 1)(1 - alpha)) โ is the zero value and what the two-argument overload keeps, and it is what SplitConformalRegressor does. SplitConformalClassifier does not: ConformalQuantileRule.MapieClassification reads numpy's higher quantile at MAPIE's level so a prediction set matches predict_set, and past level 1 it returns double.PositiveInfinity. The corpus carries two cases where the two rules disagree and freezes both. |
0143 |
| every other family โ metrics, decomposition, cluster, preprocessing, stats, regression, time series, survival, distances, stemmers, BM25, near duplicates, pooling and kNN | scikit-learn 1.9.0, scipy 1.18.1, statsmodels 0.15.0, lifelines 0.30.3, rapidfuzz 3.14.6, jellyfish 1.2.1, textdistance 4.6.3, difflib (standard library), nltk 3.10.3 and snowballstemmer 3.1.1, rank_bm25 0.2.2, datasketch 2.0.0, simhash 2.1.2, numpy 2.5.3 |
The scope of each is its row in docs/equivalence.md, and each corpus's metadata names the library it was frozen from. |
their own records |
Consequences
- The twelve records this replaces are deleted. Cite this one with its section โ "0152 (b), the BPE row" โ rather than a number that no longer resolves.
- The version column is read from the lock file, not from memory. Two figures have moved
since the records that quoted them:
0034measureddropoutontokenizers0.23.1, and the lock pins 0.23.2 today, which is the version0144and0146measured BERT's pipeline on.0007,0013and0017named no version at all; today's arejellyfish1.2.1,sentencepiece0.2.2 andtokenizers0.23.2.summaandkeybertare pinned intools/requirements-nodeps.txtrather than the lock, which is why0077's versions are not found there. - Adding an oracle library is a decision and not a convenience: it is pinned by hash,
attributed in
THIRD-PARTY-NOTICES.mdin the same change, and refused outright if it is copyleft (decision 0002) โ the rule that removedpython-Levenshteinand excludedabydosandscikit-survival. - The three traps CLAUDE.md records still apply to every regeneration: run the generator from
a working directory that is not an ancestor of the checkout, read the generator's own exit
code and never a pipeline's, and believe a red
Oracles are reproducibleโ it compares numbers, so a failure means a corpus moved by more than an assertion tolerates. - A divergence found against a reference is aligned in code where it can be. What lands here
is what cannot be: a behaviour that is the reference's own defect, an implementation detail
of its indexing, or a difference in the platform's Unicode tables. Each such row is one line
in the table above and one row in
docs/equivalence.md.