Finitely Verifiable Segmentation: the derivation archive

This is the evidence behind Finitely Verifiable Segmentation: Decidability for Every Tokenizer with a Finite-State Verifier. It is deposited on its own so that the archive has an identifier independent of the manuscript, and every count the paper quotes can be checked from it: three instances against their archived records, the library instance, the certificate-transfer study and the WordPiece instance, every other by regenerating it here, and the three too once their inputs are supplied: the pinned build of the library, and the two published vocabularies the tokenizer instances read. What changed in v2. This version accompanies the manuscript's second arXiv version. bpe_transfer_study.py prints the derived lines the manuscript now quotes beside its stored records, the shares of boundaries transferred at the deepest extensions and the cost totals including the one-time build, and the gate holds them; the archive adds the modules the gate now imports, under explorations/certification/modulo/ and certified_gap_window.py. The stored records themselves are unchanged. The programs, their comments and their messages use American spelling throughout, which renames a few internal identifiers (among them the class Materializer and the functions _normalize and minimized_size) and changes no decision; DEPOSIT.md says "licenses" where it said "licences". What is here. The archive keeps the layout of the tree it was cut from, so the relative paths the modules use resolve as they do there. explorations/certification/ holds the modules that implement the four decisions and the two independence decisions, the calculus, the transfer laws and the weighted theory and print the counts the manuscript quotes: the modules scripts/check-paper5.sh runs and what they import, which includes the modules of the companion paper on certified splitting, the generators of the five reference fixtures the library instance is held to, data/library-verifier.txt, the record of that instance, and under data/ the records and witness files of the transfer study and of the WordPiece instance at its prefix and at full depth. Beside them the directory carries local-vocab.txt, the vocabulary the training module writes and the others read, and THIRD_PARTY_NOTICES.md. paper-drafts/certified-recovery/checker/ is the reference model of maximal-munch scanning the modules import. scripts/check-paper5.sh is the gate the author runs in the repository, shipped for reference, and verify-all.sh at the root runs those of its stages that need no manuscript. Verifying it. One ledger covers every file here except itself. To check the bytes: sha256sum -c manifest.txt To rerun the claims, sh verify-all.sh at the root. It needs python3, sha256sum, curl and a writable temporary directory. It checks the ledger, fetches the one benchmark corpus the modules read, runs the modules the claims gate names, and holds their output to the lines that back the counts the manuscript quotes. Whatever it cannot run it names with its reason. What is not here. The benchmark corpus is twitter.json, byte-identical to jsonexamples/twitter.json at simdjson's release v3.10.1. It is third-party content and is not redistributed; verify-all.sh fetches it from that pinned release and holds it to its SHA-256, 30721e49... The library instance is the munch lexer library at release v2.3.0, commit fa3f20d, which is not redistributed here. explorations/certification/library_instance.py names the commit and, given a build of the library at it, regenerates the five fixtures, of the four decisions, of cut and chunk independence, of the merge tower and of the trie chain, holds each byte for byte to the library's copy, runs the library's verifier, merge-tower and trie-chain tests and its supply probe, and rewrites data/library-verifier.txt; without a build it reports the stored record and names the regeneration as not run. The certificate-transfer study, explorations/certification/bpe_transfer_study.py, reads the GPT-2 merge list, gpt2-merges.txt, byte-identical to vocab.bpe of the original GPT-2 distribution, which some mirrors, Hugging Face among them, name merges.txt, of SHA-256 1ce1664773c50f3e0cc8842619a93edc4624525b728b188a9e0be33b7726adc5, fetched from <https://openaipublic.blob.core.windows.net/gpt-2/encodings/main/vocab.bpe>; the WordPiece instance, explorations/certification/wordpiece_instance.py, reads the BERT-Base, Uncased vocabulary, bert-vocab.txt (vocab.txt of the 2018-10-18 uncased_L-12_H-768_A-12 archive), of SHA-256 07eced375cec144d27c900241f3e339478dec958f92fddbc551f295c992038a3, the same bytes as vocab.txt of google-bert/bert-base-uncased on Hugging Face at revision 86b5e0934494bd15c9632b12f734a8a67f723594, <https://huggingface.co/google-bert/bert-base-uncased/resolve/86b5e0934494bd15c9632b12f734a8a67f723594/vocab.txt>. Neither is redistributed. Run bare, each module reports its stored records and names the rerun as not run; with BPE_TRANSFER_RERUN=1 or WORDPIECE_INSTANCE_RERUN=1 set and the file in place under the llm-vocabs directory beside the archive, each refuses an input whose digest differs and reruns in full, about one hundred and about forty minutes. A rerun writes its records and witness files to a fresh temporary directory, never over the stored ones, and holds them to the stored records: every line must be equal once the elapsed times, the memory figures and the worker count are set aside, a count that shares its line with a timing still compared, and the witness files byte for byte; the module then prints the stored records, so that the gate holds the same lines after a rerun as without one. The stored records are the archived observations, taken with the worker counts they print on a machine they do not otherwise describe, so the manifest and the timings the paper quotes from them hold on any machine. The WordPiece instance builds its full-depth verifier with explorations/certification/wordpiece_trie_verifier.py, which ships because the instance imports it. Its own study, the trie construction validated against the tabulated verifier at the 4,096 prefix and scaled to the full lexical inventory, is recorded in data/wordpiece-trie-verifier.txt and lies outside the default gate: run bare, the module prints that record, and WORDPIECE_TRIE_RERUN=1 reruns it and holds the fresh record to the stored one in the same way. The correspondence the full-depth construction relies on, no transition in disagreement at the prefix, is also printed by the WordPiece instance itself, and the gate holds it there. explorations/certification/splice_theorem.py adapts material from two OpenAI repositories: the pre-tokenizer patterns of GPT-2, from openai/gpt-2 under its Modified MIT License, and of cl100k_base, from openai/tiktoken under the MIT License, together with GPT-2's byte-to-unicode map and a reimplementation of its merge loop. explorations/certification/THIRD_PARTY_NOTICES.md carries both licences in full and names what each covers. That material stays under those licences. Everything else in this deposit is the author's own work and is released under CC BY 4.0.