Strata
Lossless compression of bootable ISO collections and nested file streams
The full 100-page manuscript, Lean source, Linux executable, experimental readers, corpus provenance and measured results are supplied in the companion ZIP. This text describes the principal results and evidence.
Archive contract
A collection is an ordered finite sequence of triples $(c_i,n_i,x_i)$ of category, basename label and finite byte string. A repeated label or byte value remains a distinct occurrence. An archive decoder restores every original byte string in its original order, with the indexed labels. In particular, packing a bootable ISO retains its system area, optical descriptors, boot catalog, image sectors and internal compressed files. Materialization returns the exact original ISO including material outside the visible directory tree.
STC1 groups same-category inputs physically, stores an indexed sequence of independent compressed blocks, and refers to each file by an ordered list of extents. It finds potential equal blocks by SHA-256 and compares the full bytes before sharing. The block portfolio contains raw, gzip, xz and zstd and accepts trusted local filter pairs. A candidate whose inverse fails to recover its decoded block cannot replace the incumbent. The index remains available when a payload codec is unavailable.
Nested operations and coherence
Use a finitary typed signature whose input ports are ordered. Its polynomial endofunctor on families of sets is $(PX)_c=\coprod_{o:t(o)=c}\prod_j X_{s_j(o)}$. The initial algebra consists of finite typed trees of raw leaves, ordered sequences and certified wrapper operations. A wrapper exposes its immediate child wire representations and a recipe for the original parent wire representation. Decoding a compressed stream and re-encoding it canonically need not return the input stream. A reversible opening includes whatever residual is needed to reconstruct the original wire bytes.
The terms and their one-hole typed contexts form a category under substitution. Its simplices are chains of actual nesting layers. Adding compatible storage presentations and resource embeddings gives a category $P$. The simplicial groupoids $\operatorname{core}(\operatorname{Fun}([n],P))$ give the Rezk classifying diagram, with presentation isomorphisms comparing chains. The Segal comparison is an equivalence because endpoint isomorphisms can be transported to turn a weakly matched sequence into a strict chain. A laminar set of proper intervals in a fixed chain specifies a partial parenthesization. The reverse-inclusion poset of such sets has the empty set as terminal object, so its nerve is contractible. All those evaluation plans compute the same composite of certified recipes. For independent sibling operations, product evaluation gives commuting cubes.
On the directed acyclic resource graph, the opens are the dependency-closed subsets. The presheaf assigning validated byte tuples to an open is a sheaf. Compatible local assignments glue by assigning each vertex the value given by a covering open. Its dependencies lie in that same open, so the joined assignment satisfies every local reconstruction rule. For a read, the required open is the closure of the blocks intersecting the requested interval. In STC1 every block is independently decodable.
Range reconstruction and minimum size
For an entry, the logical intervals of its extents partition the original byte range. Intersecting these intervals with the requested range gives a partition of the requested bytes. Each intersection translates to a subinterval of the corresponding decoded block. Concatenating the subintervals in extent order therefore returns the original range. ISO cuts are sector-aligned, so a complete optical sector lies in one decoded block.
For a fixed layout and exact-sharing dictionary, the variable serialized cost of a candidate $(c,w)$ is the stored length plus the length of its codec ID, the length of the decimal stored-length field and two terminators. The remaining index fields and fixed-width footer do not depend on that codec choice. For independent choices, minimizing each block's cost minimizes their sum. The executable also compares whole archives under a finite layout portfolio. A broader problem that lets candidates add shared support resources is NP-hard by a reduction from set cover. One unit-cost resource represents each set and each element chooses a candidate requiring any set containing it. The manuscript distinguishes this finite optimum from unrestricted compression, which cannot shrink every input by injectivity.
Lean and experimental evidence
The Lean kernel checks the framing round trip over every finite ordered sequence of finite byte strings, the byte-array adapter, composition with any codec having a left inverse, and a theorem for a locally checked codec candidate. The executable streams blocks and uses the verified framing functions for the index. Byte-range correctness follows from the extent invariant and is exercised in cross-reader tests. External codecs, filesystem operations and firmware are tested interfaces.
The public corpus consists of Core 16.1, Core 16.2 and TinyCore 16.1 x86 ISOs, with verified input lengths and recorded SHA-256 digests. The original total was 63,989,760 bytes. The fixed 2 MiB full-portfolio archive occupied 62,271,978 bytes. Sector-aligned content-defined cuts occupied 38,848,049 bytes, a 39.29% reduction from the original subtotal. The latter profile had 119 logical extents and 74 physical blocks. Every tested profile recovered every image byte-for-byte. The best tested solid USTAR baseline occupied 62,274,180 bytes. The advantage is corpus-specific and mainly reflects reuse across matching sector ranges.
A separate dual-mode El Torito fixture booted under SeaBIOS and OVMF in QEMU 8.2.2 from the original ISO, the restored ISO, and a read-only archive-backed NBD optical drive. Each path reached its firmware-specific marker. The virtual-media result is conditional on the adapter's device interface and concerns the fixture and named virtual firmware. The package specifies the remaining bootloader and kernel-handoff obligations for bare-metal use.
The nested test built PDFs with distinct Flate streams encoding the same inner archive. Both PDFs, their attachments and the nested payloads were recovered exactly. The companion resolves dotted archive addresses and searches primary ISO directory names via indexed ranges. A filesystem frontend can build on these typed views, retain provenance, and pin each request to an immutable archive version.
Selected references
- Kock, Polynomial functors and trees. arXiv
- Rezk, A model for the homotopy theory of homotopy theory. arXiv
- Gálvez-Carrillo, Kock and Tonks, Decomposition spaces and incidence algebras. arXiv
- Mac Lane and Moerdijk, Sheaves in Geometry and Logic. Springer
- Muthitacharoen, Chen and Mazières, A low-bandwidth network file system. Authors' paper
- Xia et al., FastCDC. USENIX
- ECMA-119 optical volume and file structure. Ecma International
- El Torito bootable CD-ROM format. Specification
- UEFI media access protocols. UEFI Forum
- ISO 32000-2, PDF 2.0. PDF Association
- de Moura and Ullrich, The Lean 4 theorem prover and programming language. Springer
Authorship and automation
The manuscript is prepared for anonymous editorial handling. An AI drafting system assisted with the exposition, implementation and experiment orchestration. The proof statements, source and observed results are available for review and reproduction.