|
Everett
|
I use this small Lean model to check the laws behind Everett's composable updates and persistent representations. We can execute its admission and ownership operations, and Lean checks the accompanying theorems. I keep this model separate from the C++ implementation: a proof about these definitions does not by itself verify the codecs, memory accesses or disk operations in include/everett/.
The design, per-key categories and implementation ledger give the surrounding context. The first theorem connecting composition to publication is Everett.adopt_adjacent_merge: replacing two adjacent changes by their composite preserves the adopted root's full arrow meaning. We establish that equality from the category laws, without treating equal fingerprints as equal states.
I pin this project to Lean 4.19.0, release commit 6caaee842e94, through lean-toolchain. The official release contains the toolchain. With Lean's elan toolchain manager installed, Lake uses that file to select the version. No mathlib or external package download is required after the toolchain is available.
From this directory:
The default build checks every model module, the theorem-based examples and the axiom audit. The interpreted executable prints the outcomes of disjoint updates, an invalid reversal of same-key updates, and a retained snapshot whose current owner has adopted a different exact index/target pair. It also shows a sampled search whose native match lies before the routed window and is recovered through a false borrow, then runs the succinct-navigation boundary examples.
I use by decide only where Lean can reduce a concrete proposition in the kernel; these examples do not use native_decide as a proof shortcut. Executing the compiled examples also depends on the compiler and runtime. The theorem checks and the executable output are separate forms of verification.
| Module | Definitions and checked properties |
|---|---|
| Category | An explicit category policy; source/target-indexed histories; composition of concatenated histories; adjacent contraction in an arbitrary chronological context; binary-tree reassociation with the same ordered leaves |
| Updates | A dependent family of state types and categories; componentwise world arrows; the typed disjoint-coordinate square; exact-source-checked single-key admission; target correctness; commutation of two valid updates at distinct keys |
| Fingerprint | Integer state potentials; endpoint-delta composition; history telescoping; adjacent-merge contribution preservation; the sum of per-key deltas over Fin n |
| Snapshots | Exact pair/target identities; immutable catalog extension; owner-rooted reachability; snapshot retention and read preservation; complete-target readiness; eligible reclamation; independent adoption with an explicit semantic premise |
| Allocation | A monotone allocation watermark, fresh installation and non-reuse of issued IDs across allocation/reclamation sequences |
| Adoption | Discharges the semantic adoption premise for chronological adjacent merges, using the actual history-composition theorem |
| Fractional | Stable tagged merging; exact every-Kth samples; sampled predecessor windows; endpoint-rank projections; local/global predecessor equivalence; false-borrow recovery for unique native keys; a list-level index builder and exact-target retention |
| DualRoute | Three-origin rank windows share one entry budget; independent main/secondary predecessors and optional cut-LCP repairs; terminal-secondary traversal visits at most twice the main height |
| Prefix | Finite-string lexicographic order, prefix interval convexity and the exact LCP minimum for three ordered strings |
| Framing | Retained prefixes and reconstructed key lengths stay within physical stream extents; admitted extent bounds imply bounded conversion to bits |
| Frontier | Merge-head ordering from carried LCP lengths, suffix-only comparison at equal lengths, and exact new frontier lengths |
| Transfer | Content-mismatch transfers, the literal-position invariant, composition and associative ordered summaries |
| RetainedFloor | Constructed retained-prefix caps; exact canceled-owner literal aliases; arbitrary fragment-gather preservation; extra literal growth charged to canceled FC payloads |
| NativeMerge | Executable two-way merging of strictly ordered native runs; unique sorted output; optional pointwise lookup composition; chronological reassociation and disjoint-support commutation |
| CarriedChain | Bottom-up coherent chain builder; exact target/next-parent correspondence; carried aligned windows and explicit empty-node traversal; one answer per node |
| CarriedRoute | Concrete parent/sample builder; carried parent windows through stored rank checkpoints and one sample lookup; exact target-window search for one edge |
| Navigation | Constructed unary Elias–Fano selection; strict high positions; common-stride and EOF recovery; grouped population/checkpoint rank equals fractional rank, with bounded local scans and no stored endpoint total |
| Examples | Heterogeneous keys, valid and stale sources, noncommutative histories, changed index/target versions, and an old target that cannot be reclaimed while a snapshot retains it |
| FractionalExamples | K=3 and K=15, equal keys across several cuts, empty native projections, false-borrow recovery, empty targets, before-first queries, short tails and stored-index routing |
| Audit | Rejects unexpected axioms in every kernel-safe Everett declaration and its transitive dependencies |
The checked fixture assigns a natural-number state to one key and a Boolean state to another. We can prove equality of the resulting worlds, not merely equality of their hashes:
Both changes are valid against initial. Their distinct keys make either intermediate world a valid source for the other change. If we instead reverse increment and next, which act on the same key, the second ordering fails its source check. Examples.lean checks both outcomes.
For histories, I retain the arrow itself. word_category has one object and lists of natural numbers as arrows; composition concatenates the lists. Its arrows [1] and [2] do not commute, although every arrow has the same source and target. Reassociation of a fixed chronological sequence is proved separately from permutation. This example also gives a nonidentity arrow with zero endpoint delta, so fingerprint equality cannot silently stand in for arrow equality.
In the snapshot fixture, current owner 0 and snapshot owner 1 initially name root 1, whose exact target is 0. The current owner adopts new root 3, whose target is 2. Roots 1 and 3 share a native identity but have different index identities. old_target_retained proves that the snapshot still pins target 0; a proposed reclamation list containing 0 therefore fails the eligibility condition.
The sampling design starts from two ordered streams. We merge their occurrences, retaining the origin tag and label even when keys are equal. Native occurrences precede borrowed occurrences at the same key. augment_preserves_occurrences proves a permutation of the complete input records; augment_filter and augment_filter_right recover each source in its original order. The labels are supplied by the caller. We preserve them without assuming that arbitrary input labels are distinct.
samples xs K records positions \(0,K,2K,\ldots\) that exist in xs, together with the exact target occurrence at each position. Let \(\ell\) be the last sampled position whose key is at most the query, or zero if no sample qualifies. The search window is
\[ [\ell,\min(\ell+K,|xs|)). \]
predecessor_bracket places the global rightmost qualifying occurrence inside that window. routed_predecessor_correct goes further: searching the actual window and translating its result back to an absolute ordinal gives exactly the same Option Nat as a full search. This includes equality runs, the short last group, an empty target and queries before the first key. The local spacing theorem needs only \(K>0\); the storage policy's restriction to \(K=2^n-1\geq3\) is a separate codec choice.
Rank projects the virtual half-open window into a native interval and a borrowed interval. project_window proves that each interval is exactly the corresponding origin-filtered window, in order. projected_lengths_sum says their lengths sum to the virtual length, so the two ranges share one budget of at most \(K\) occurrences.
There is an equality boundary worth keeping visible. A long run of borrowed copies of a key may carry the route beyond its matching native occurrence. Searching just the projected native interval would then miss the key. For a pair with unique native keys, false_borrow_recovery proves that the matching native occurrence is at
\[ \mathrm{rank}_{\mathrm{native}}(j)-1 \]
in the native stream, where \(j\) is a borrowed occurrence of that key. The rank is positive, so the subtraction is safe. false_borrow_flag constructs the semantic flag by checking for a native match, and false_borrow_flag_correct proves its exact meaning. native_match_candidates combines the ordinary projected hit with this extra probe.
For example, the K=3 fixture has one native 5 at virtual position 2 and eight borrowed copies spanning several cuts. A query for 5 routes to position 9, finds its augmented predecessor at 10, and has an empty native projection. Native rank is 2, so the extra probe retrieves native ordinal 1. These outcomes are checked by reduction and by the general theorems. Native uniqueness is a per-blob invariant; matching keys in different blobs remain separate history segments. The more general merge and predecessor theorems preserve multiplicity without that invariant, but equality recovery requires it.
The mathematical rank function is defined at every position. The concrete rank_groups<K> API stores boundary ranks. rank_inside_route connects the two: a finer rank is the boundary rank plus the native count in a local prefix of fewer than \(K\) occurrences. No arbitrary-position constant-time rank API is assumed or proved.
Finally, build_index stores a target ID and its sampled target occurrences. build_index_matches establishes exact correspondence from the builder's output. index_route reads those stored samples, and indexed_predecessor_correct proves that the resulting target-window search agrees with a full search of that exact target. Catalog extension and eligible reclamation preserve the certificate by preserving the target record. A source pair's target_samples follows its literal stored target edge; adding a merged target does not redirect that edge.
This builder produces mathematical lists. Its entries retain the destination's occurrence labels and tags; constructing a source's borrowed stream requires source-local labels and borrowed tags. The one-edge CarriedRoute builder below now constructs those borrowed tags and exact target ordinals. Encoded-file decoding, independent dual-target routing and the full three-origin cascade remain separate refinement obligations; CarriedChain below composes the narrower one-origin model. The searches here enumerate finite lists, so these theorems establish the window's entry bound and lookup meaning, not the running time of binary search, compressed rank or key reconstruction.
I model the dual-target topology separately in DualRoute.lean. Three origin predicates project a virtual window into native, main-borrowed and secondary-borrowed intervals. Their lengths sum exactly to the original window length, hence share its \(K\)-entry budget. The two children retain independent predecessor answers, including missing answers and equality runs.
Each optional borrowed predecessor has its own exact cut LCP. repair_both uses the ordered-string law to recover both comparisons from the same incoming boundary state. An absent predecessor stays absent; an existing empty key is not confused with absence. The required stored-cut equalities are explicit content assumptions, not inferred from counts or hashes.
The executable chain recurses only through main catalogs; a secondary contains native entries and no child. search_correct agrees with full list searches, and visits_bound gives at most \(2h\) catalog visits for main height \(h\), including a synthetic root if present. These visits are not instruction or byte costs. The traversal computes exact samples and an independent route in each catalog; it does not yet derive the next window from a carried parent result. The CarriedRoute model below proves that handoff for one constructed edge. Connecting it into this three-origin chain, with stored dual-target samples, false-borrow probes, immutable file identities and C++ decoding, remains separate. No scheduler, visibility deadline or space theorem is claimed.
The comparison-state design separates two obligations for ordinary front coding. The forward candidate is between its physical predecessor and the incoming boundary. The borrowed predecessor needed for the next hop can instead precede the boundary, and needs additional information.
Prefix.lean works with actual finite strings and lexicographic order. For ordered strings \(C\le B\le Q\), the exact identity is
\[ \mathrm{lcp}(C,Q)= \min\bigl(\mathrm{lcp}(C,B),\mathrm{lcp}(B,Q)\bigr). \]
This lets an exact cut-LCP scalar repair the preceding borrowed key's comparison state. Equality and proper-prefix cases are included. The statement needs the ordering hypotheses; arbitrary triples only satisfy the usual lower bound. The theorem does not certify that a stored index contains the right scalar.
frontier_recovery_without_length sharpens the endpoint test: because \(C\le Q\), equality holds exactly when the recovered LCP equals \(|Q|\). The preceding key's full length is unnecessary for this comparison. This includes an empty query and proper-prefix cases.
merge_retained_le and merge_literal_suffix justify forwarding a slice of an input literal into the merge output. If the input predecessor precedes the last output key, the output retains at least as much prefix as the input frame. Skipping output keys can break that premise; the cursor's retained key context then supplies any prefix material needed by the next emitted key.
adjacent_min_eq_endpoints extends this law to any nondecreasing finite walk: the minimum of its exact adjacent LCPs is the LCP of the first and last keys. accumulated_lcp_min proves the actual left-fold update with an existing cap; walk_min_eq_endpoints initializes it to the first key's length. The empty-walk convention is zero, and a singleton's result is its self-LCP. Repeated keys and proper prefixes are included. This supports a sampler's comparison argument across several occurrences, without asserting that its C++ cursor implements the mathematical walk.
Frontier.lean applies the same string law during a sorted merge. If both heads follow the preceding output, the head sharing the longer prefix with that output sorts first. Their mutual LCP is then the smaller carried length. When the lengths agree, dropping that shared prefix preserves strict order; adding it back to the suffix LCP recovers the exact new frontier. Equality, empty strings and proper prefixes are included. These laws justify the comparison shortcut independently of the cursor implementation. They do not prove cursor state maintenance, decoding, or its running time.
Transfer.lean models a content mismatch as a position with its direction, or infinity. A record retaining \(r\) units preserves an incoming mismatch before \(r\); otherwise it substitutes the literal mismatch \(e\). Valid summaries require \(e\ge r\). Their composition represents applying the earlier record followed by the later one, preserves validity, and is associative. The selected mismatch retains its direction.
These summaries describe content mismatches. Infinity does not mean that two complete keys are equal: endpoints and full lengths remain separate. The module does not prove that a particular SIMD comparison produces the correct summary.
The missing bridge is from the origin-filtered cut to these string hypotheses, then from the encoded length/LCP metadata and literal comparisons to the abstract state. Complete cascade composition, block access bounds and the C++ implementation remain separate refinements.
Deleting a record does not erase its contribution to a later key's inherited prefix. In RetainedFloor, I give the replacing tombstone enough literal material to stand in for its exact canceled record. Let \(r\) be that record's stored retained-prefix position and \(n\) the tombstone's ordinary retained position. I construct the tombstone with
\[ t=\min(n,r), \qquad \Delta=n-t=\max(0,n-r). \]
target_literal_covered proves that the tombstone's literal suffix contains the entire target literal suffix. For an owned key position \(j\ge r\), alias_lookup proves that the replacement address is exactly \(j-t\); alias_in_bounds proves that address is in bounds whenever the original key position is. No omitted prefix is reconstructed by these definitions.
literal_growth proves that \(\Delta\) is exactly the increase in literal units. extra_le_target_literal bounds it by \(|k|-r\), the canceled record's existing literal payload. batch_charge sums this bound over admitted certificates. Charging each physical record once additionally requires distinct target identities; admitted_once states that obligation. These are literal-unit bounds, excluding count controls, values, indexes, allocation and I/O costs.
One tombstone need not contain every inherited fragment exposed by a run of deletions. fragments_covered instead proves that any supplied finite gather schedule returns the same units after each original owner is redirected to its own certificate. The adjacent-owner example obtains separate fragments from two tombstones. A GPU implementation still has to find those owners and split copies at ownership boundaries; a machine-word boundary alone is insufficient.
The certificate names a file, record ordinal and exact stored retention. changed_retention_rejected shows why an equivalent re-encoding cannot silently replace that target. Source immutability, identity non-reuse, pin lifetime and same-key admission remain obligations of the surrounding catalog and codec. The construction receives the known complete target key; a fingerprint does not stand in for that knowledge.
No survivor mask is assumed by the coverage theorem, so adjacent deletions do not invalidate it. Its caller must establish that each requested fragment really belongs to that original owner, and that its extent is valid. The module does not prove the owner-tree algorithm, deletion visibility, shader accesses or a complete parallel merge. It also does not implement or verify the tighter single-bridge encoding that depends on a frozen survivor mask.
I model a native run as a finite list of natural-number keys with arbitrary values. native_merge.merge is the actual two-way recursive algorithm: it emits the smaller head, and combines equal heads with compose key older newer. The callback produces a value at the same key. merge_ordered proves strict output order, and merge_unique proves that no key occurs twice. Neither result needs an algebraic law for the callback.
lookup_merge gives the per-key meaning of the algorithm. A key present in only one input keeps its value; a key in both inputs gets the callback result in older/newer order. Missing bindings act as identities in Option Value, without requiring an identity element in Value itself. Strict input order is essential: these theorems do not grant arbitrary duplicate keys within one native run.
We can then reason about different merge trees. If the callback is associative at each key, lookup_merge_assoc proves the same lookup in either parenthesization of three chronological inputs. ordered_ext establishes that strictly ordered runs are canonical for their lookups, so merge_assoc strengthens this to equality of the complete output lists. It changes parenthesization while keeping the same ordered leaves. For disjoint supports, merge_disjoint proves that the two inputs commute without any callback law.
The checked concatenation examples make the distinction concrete: equal-key values [30] followed by [31] produce [30, 31]; reversing them produces [31, 30]. Concatenation is associative, and concat_assoc applies the general merge theorem to it, but concat_not_commutative proves that swapping overlapping inputs changes the result.
This module uses a total value callback. I keep typed arrow admissibility in the category modules; the native-merge theorem does not itself validate an arrow's source, choose a merge schedule, handle exceptions, or elide deletion markers. It also does not refine the C++ builder, front-coded streams, allocation or disk publication. Those layers must preserve this ordered callback semantics before we can transfer the abstract result to them.
I expose category laws as fields of category: identity and associativity are requirements on a policy, not axioms asserting Everett's desired result. The replacement and noncommutative word policies supply concrete proofs of those laws. Histories have typed endpoints, so a chain cannot contain an arrow whose source differs from the preceding arrow's target.
mutation.apply is an executable endpoint-state projection. It checks the exact old state and installs the target of an admissible arrow. It does not retain the arrow or evaluate a compact diff. world_category, history, and the adoption theorem describe full arrow semantics separately. I have not yet proved an executor refinement connecting those two layers, or arbitrary partition-batch replay and duplicate-delivery suppression.
world_category supports a category depending on the full key. This first model uses ordinary dependent function worlds; it does not yet construct the restricted product of worlds with finite support relative to a baseline. The fingerprint sum explicitly enumerates Fin n, so each key in that finite universe occurs once. Potentials take values in exact integers:
\[ \Delta(x,y)=\phi(y)-\phi(x),\qquad \Delta(x,z)=\Delta(x,y)+\Delta(y,z). \]
No injectivity, randomness or collision bound is assumed. Generalizing the integer proof to a parameterized additive group is a separate extension.
The catalog is an immutable function from natural-number IDs to optional blob records. Each record stores its exact native ID, index ID, target blob ID and an abstract payload. The target edge is followed literally. Native/index IDs are uninterpreted identities here; the model does not open files or calculate content addresses. storage adds a monotone watermark so the allocation API cannot reuse an issued ID after reclamation. Calling the lower-level catalog.install directly requires its separate freshness proof; it is not a complete allocator.
catalog.observe reads a root's stored abstract payload. It does not decode or compose the target graph. Consequently, independent adoption requires concrete readable old/new records and equal payloads. adopt_adjacent_merge supplies that equality for an actual typed merge. adopt_ready separately requires a complete new target graph, while reclamation theorems require a proof that no deleted ID is reachable from an owner. These are explicit interface obligations. I am not assuming that an unverified external index satisfies them.
CarriedRoute supplies a concrete one-edge connection that DualRoute.search does not yet make. build_edge stable-merges native entries with the child's exact every- \(K\)th samples, retaining their target ordinals and equal-key multiplicity. We prove both origin filtering and parent sortedness from the actual builder. The stored edge also retains the exact child and constructs its origin-population classes and checkpoints.
The public semantic query transfer_at_group receives this stored edge, an existing group boundary and an incoming parent window. It reads the stored rank directory, searches only that window, adds the local borrowed population to the boundary rank, and reads the last passed sample by ordinal. It does not reconstruct the samples, scan the whole parent prefix, or compare the query against a fresh child sample search. descend_at_group follows the retained target and searches the resulting window of at most \(K\) entries.
descend_at_group_correct proves that this complete path returns the child's exact global predecessor. The theorem requires sorted native and child inputs and a valid incoming bracket containing the parent's predecessor when one exists. It derives the parent cut, sample correspondence and stored-rank correctness; those are not supplied as conclusions or opaque builder axioms. The preceding edge's bracket theorem provides the form of invariant needed for composition. Queries before the first key, equality runs crossing several cuts, empty targets, short final groups and rejected one-past-end parent groups have checked examples. The outer Option reports an invalid stored group; the inner Option reports an absent predecessor. An empty parent has no stored group, so transfer_at_group rejects it. Zero passed samples use carry's zero bootstrap; neither case invents a rank endpoint.
The incoming parent window's size remains a caller obligation. The local origin scan stays within it, and the outgoing child window has at most \(K\) entries. These are entry-count bounds; list indexing, dropping prefixes and predecessor search are executable mathematical definitions, not instruction-count proofs. This module has one native and one borrowed origin. It does not yet build the full three-origin main/secondary chain or refine immutable lists to encoded file identities and parser operations. The finite one-origin chain below proves the recursive connection for this narrower topology.
CarriedChain composes those edges into a finite chain. build_chain constructs the chain from the bottom up, sampling exactly the next node's immutable entries. build_chain_coherent proves that every stored edge came from the concrete builder and retains exactly that next parent. The correspondence is equality of complete entries, not equality of lengths or fingerprints; a same-length retargeting fixture fails coherence.
walk receives only the stored chain and an incoming window. At each nonempty link it reads the stored directory, transfers through the last passed sample, and passes the resulting window to the next node. The invariant proves that its lower bound is a multiple of \(K\) and names an existing group. An empty node has a separate path: the builder proves that its target is empty too, and the walk passes \([0,0)\) without attempting rank at group zero. Empty nodes still contribute their missing answers to the result.
walk_correct proves the complete result equals the list of global predecessors. search_built discharges coherence through construction, requiring only sorted input layers and positive \(K\). The root begins with its complete source window; every generated recursive window has at most \(K\) entries. A three-node example carries sample position 3 into the middle node, then position 6 into its child, returning predecessor ordinals [1, 4, 6]. Other examples check before-first and after-last queries, empty chains and incoherent targets. answer_count proves that every node contributes exactly one answer.
These are bounds on the windows selected, not on Lean list operations or machine instructions. The reference walk performs two local predecessor scans at a nonempty link and a local origin count; it does not claim one fused scan. This chain has one borrowed origin, uniform sampling spacing and exact list-valued target correspondence. The full three-origin main/secondary topology, physical file identities, false-borrow native probes and encoded decoding still need a separate refinement.
Navigation connects ordinal navigation to the list semantics used above. I model the actual unary high-bit vector and uncompressed low fields; I do not assume a correct select operation as a premise.
For nondecreasing offsets \(v_i\) and a positive base \(B=2^w\), encode stores the low remainder \(v_i\bmod B\) and emits unary quotient gaps. select_one walks those bits. unary_high_select proves that its \(i\)th selected bit is at \(\lfloor v_i/B\rfloor+i\), and high_positions_strict proves that these positions are strictly increasing even when offsets repeat. decode_encode then recovers every input offset. These are executable list definitions, not assertions about an external selector. The theorem holds for every positive base, so choosing the width does not affect correctness. low_bit_field_bound proves that every low remainder fits its \(w\)-bit field, including the zero-width case. encoded_high_population proves that the unary vector contains exactly one set bit per offset. For a nonempty sequence ending at \(U\), encoded_high_length proves its logical length is exactly \(\lfloor U/B\rfloor+N\); an empty vector has length zero. These counts precede word padding and select-accelerator storage.
A profile owner subtracts the common value width times the record ordinal before encoding its boundary offsets. stride_fits rules out truncated subtraction; stride_ordered states that physical growth covers those fixed-width values. We derive monotone residuals from those two conditions. physical_select_correct proves exact recovery after adding the stride back. owner_boundaries generates regular block ordinals and appends one real EOF entry; owner_select proves the full \(\min(jW,N)\) ordinal convention, and owner_eof selects the final entry using the actual record count. For 17 records with codec block size \(W=15\), EOF adds 17 strides, not 30. The codec block spacing \(W\) is independent of the sampling group size \(K\) used for rank below. An empty owner still appends its one EOF value; a generic empty EF sequence contains no implicit sentinel.
For grouped rank, classes constructs each population by filtering a real \(K\)-entry window, including its short tail. population_window_bound proves that a population cannot exceed either \(K\) or the remaining entries. Thus class_field_bound proves that \(K=2^b-1\) classes fit in \(b\) bits, including the full-population code \(K\). checkpoints records a prefix sum only for each existing checkpoint group. grouped_rank_correct proves that a checkpoint plus the intervening classes equals fractional.rank at a valid stored group boundary. directory_scan_budget bounds that scan by fewer than \(C\) classes (128 in the implementation). fine_rank combines this boundary rank with the local origin scan, of fewer than \(K\) entries. The executable boundary API rejects a one-past-end group. grouped_total_correct derives the total from the last valid boundary plus its population; no extra total is stored. These bounds count selected classes or entries, not Lean list traversal or machine instructions.
The model uses natural numbers and lists. It does not yet verify packed low fields or population words, sparse/dense select accelerators, machine overflow, SIMD instructions, or the C++ parser. The byte-level implementation must refine these concrete construction and navigation contracts.
Audit.lean visits every kernel-safe declaration in the Everett namespace, collects its transitive axiom dependencies, and fails the build if it finds anything outside Lean's standard propext, Quot.sound and Classical.choice foundations. The build reports the declaration count and the actual dependencies. This slice uses all three, including Classical.choice through Std's list theorems. The audit also catches a theorem placeholder hidden behind another declaration. Compiler-generated unsafe execution artifacts are outside that logical audit; no model source declares an unsafe definition or an additional axiom.
I have deliberately not claimed:
The next useful connection is a precise interpretation from encoded immutable pairs to these abstract sequences and catalog records. The list-level builder and local lookup theorems give that refinement a concrete contract to meet.
Contributions and bug reports are welcome through the Everett issue tracker. I can also be reached at ekmet.nosp@m.t@gm.nosp@m.ail.c.nosp@m.om.
This proof layer uses the same dual license as Everett: BSD-2-Clause or Apache-2.0, at the recipient's choice.
-Edward Kmett
1.9.8