Module term_store

Expand description

Hash-consed term storage — the representation a kernel needs to be as fast as Lean’s.

Term is a Box-recursive TREE. Every walk over it is native recursion whose depth is the term’s depth, every clone copies the whole subtree, and a subterm that occurs n times is n separate trees that get checked n times. Lean’s Expr is the other thing: a maximally-shared DAG behind a structural hash, so constructing an identical subterm twice yields the SAME pointer, a == b is usually a pointer compare, and a cache keyed on that identity checks a shared subterm ONCE.

This module is that representation, built and measured STANDALONE:

TermStore::intern turns a Term into a TermId — a Copy u32 handle. Identical structure interns to an identical id, so a == b is ONE integer compare (TermStore::same) instead of a tree walk.
Every node carries its depth, its unfolded tree_size, its O(1) structural_hash, its hash-consed FREE-VARIABLE set, and the set of binder names below it. All are computed compositionally at construction, so no query re-walks the term.
IdCache is a DENSE cache keyed on node identity — Vec<Option<V>> indexed by the id, so a lookup is a bounds check and not a hash. TermStore::fold visits each DISTINCT node exactly once, which is what “checked once, not once per occurrence” is.
TermStore::instantiate is SIMULTANEOUS capture-avoiding substitution — Lean’s instantiateRev shape: a whole argument vector in one pass, not one substitution per binder. A node whose free variables do not meet the substitution’s domain is returned UNCHANGED, detected by a 64-bit mask intersection, which is what takes a deep spine from quadratic to linear.
Nothing here recurses natively. Interning, extraction, folding, substitution and normalisation are all explicit-stack loops, and the store’s own Drop is a flat Vec drop — so depth is bounded by the heap, not by 2 MiB of thread stack.

§What this module is NOT

TermStore::beta_zeta_normalize is a MEASUREMENT INSTRUMENT, not a kernel tier. It implements β and ζ and nothing else — no δ, no ι, no η, no Fix unfolding, no universe algebra. It is not a replacement for reduction::normalize. beta_delta_equivalent now uses it behind a conservative conversion gateway: checked closed monomorphic definitions are expanded, unsupported shapes are refused, and only alpha-equal results prove conversion; all other answers use the main kernel.

§The measured case for wiring this in

Four numbers, all measured on this box against the kernel as it stands.

The deep-spine corpus case used to ABORT, and no longer does — CLOSED. lean_conformance_t00_terms::a_deep_spine_costs_linearly_in_its_depth_and_not_quadratically died by SIGABRT — a stack overflow in infer_type’s own App arm — before it reached its assertion. MAX_TERM_DEPTH is 1600; BISECTED in a child process, infer_type died at 106 rungs of a Π telescope and at 52 rungs of the corpus’s own saturated dependent telescope, so the door was fifteen to thirty-one times too permissive and ADMITTED terms the kernel then killed the process on. double_check died at the SAME 52, because it calls infer_type first — so across that whole band the second kernel, whose entire job is to disagree with the first, was never consulted. deepen_stack is now wired into infer_type, is_subtype, normalize_checked_at, recheck and double_check, and a whole-crate run of 1413 tests reports zero SIGABRT/SIGSEGV: the case now FAILS AN ASSERTION, which is a verdict instead of a corpse. (The corpus case’s own prose puts the ceiling at “depth 4000”, which is wrong by 77×.)

One band is still open, and deepen_stack does not close it. The door and the sizer both measure the term they were HANDED. infer_type’s Var arm is ctx.get(name).cloned(), and Term’s Clone is derived — so it recurses over the BINDING’s type, a depth neither ever saw. MEASURED in a child process: Var("x"), one node deep, under x : Nat → … → Nat at 4000 arrows kills the process BARE and through deepen_stack, and is answered by deepen_stack_with_depth. Every arm inherits it, so the input term’s depth is a LOWER BOUND on what a kernel call descends, never the bound.

A β-step on a spine pays FOUR Θ(size) walks, and the corpus’s ratio is the square of that. ITEMISED AND COUNTED, in units a loaded box cannot move — node visits, by W_perf_extra::the_spines_four_walks_are_quadratic_in_node_visits_and_the_owned_step_is_linear:

per β-step on a spine	visits at depth 500	at depth 1500	ratio
`substitute`’s `free_vars(replacement)`	499 500	4 498 500	9.01×
`substitute`’s clone of the replacement	499 500	4 498 500	9.01×
the driver’s recursive `Drop`	501 500	4 504 500	8.98×
Brent’s `current == tortoise` (and its saves)	513 500	4 550 366	8.86×
all four	2 014 000	18 051 866	8.96×
an OWNED step that moves instead of copying	2 000	6 000	3.00×

The corpus case asks for ≤ 5.00× at 3× the depth, and the kernel’s own wall clock on this box reads 6.9× to 12.3× across repeated runs of one binary (40–94 ms at depth 500, 428 ms to 1.16 s at depth 1500). Each of the four is quadratic ON ITS OWN, so removing any three leaves the ratio where it was — which is the measurement that says no constant factor reaches it. Three of the four can go inside type_checker.rs and reduction.rs: free_vars(replacement) is only needed when a BINDER in the body could capture, and on a spine the body is Var("x") and has none; the clone and the Drop both go if the reducer OWNS its term instead of borrowing it. The fourth cannot. Brent’s cycle detection needs an equality test on the WHOLE term, and a Box-recursive tree has no O(1) one — every cheap surrogate (a bounded prefix compare, a depth-limited compare, a periodic compare) is either unsound or useless on exactly this shape, because two spines of different lengths agree for every rung of the shorter. A hash-consed store has both: same is a u32 compare and structural_hash is computed at construction. That is the measured case for stage 2 below, and this store already reduces the same spine at 2.77× (1.64 ms → 4.55 ms, interning included).

Nat has no literal fast path. try_primitive_reduce matches Literal::Int and Literal::BigInt only, because term::lit_bigint returns None for Literal::Nat, so natLe peels one Succ per unit. The two slowest tests in the kernel crate are both this, at 61.7 s and 52.4 s of a 66 s suite against a median under 0.3 s. That fix lives in reduction.rs, not here; W_perf_extra’s a_nat_order_fast_path_must_agree_with_the_unary_unfolding is the specification it has to satisfy.
The main kernel has no whnf and no cache of any kind. is_subtype normalises BOTH sides to a FULL normal form and then compares, with one alpha_eq tree walk as its only shortcut, on every conversion. Lean’s isDefEq is whnf-driven over a hash-consed Expr with a whnf cache and an isDefEq cache. MEASURED: one convertible-but-not-α-equal pair costs 6.55 ms once and 6.62 ms per call a hundred times over — a FLAT per-call cost, which is what “no cache anywhere” looks like from outside. That is the largest remaining algorithmic gap after (3), and TermStore::alpha_id, IdCache, TypeCache and DefEqCache::scoped are the four pieces it needs — the last two carrying the lifetime and the environment key that make a kernel cache SOUND rather than merely fast.

§The wiring plan

Three routes, and only one is open.

Change Term’s children from Box to Rc. Hundreds of Box::new Term-child sites sit in FROZEN test files. Closed by rule.
Add a Term::Shared(Rc<Term>) variant. Seven frozen kernel test files match Term exhaustively and wildcard-free, deliberately — lean_conformance_t00_terms.rs says so in a doc comment (“a new variant has to answer here”). Closed by rule.
Keep Term as the BOUNDARY type and make the store the kernel’s internal representation. This is the recommendation. Every frozen test builds a Term, calls a kernel entry point, and compares a Term; none of them can observe what happens in between. The boundary is EIGHT public functions taking &Term: type_checker::{infer_type, is_subtype, substitute}, reduction::{normalize, normalize_at, normalize_checked} (plus normalize_checked_at), and recheck::{recheck, double_check}. Intern once on the way in, extract once on the way out. The entry points already pay an O(size) term.clone() before their first step — normalize_checked_at pays two — so interning replaces a cost rather than adding one.

Four stages, each independently green.

Stage 1 — conversion, type_checker.rs only. Five alpha_eq call sites become alpha_same, and is_subtype gains the cache it has never had: HashMap<(TermId, TermId), bool>. The walk is replaced by a walk of the same order that MEMOISES, so the second conversion mentioning a subterm is O(1) instead of O(size). Hold the store thread-local behind the existing INSIDE_KERNEL door, so the outermost entry creates it and DoorGuard drops it — a cache with the lifetime of one kernel call cannot grow without bound or leak across a Context change.
Stage 2 — the reducer, reduction.rs. normalize_checked_at interns once and runs its fixpoint and Brent cycle detection on TermIds: (2) above goes away outright. The 54 reduce_step_at arms port one at a time with recheck_reduction_differential.rs as the oracle. Depth stops binding, because the traversal is this file’s explicit stack.
Stage 3 — infer_type, type_checker.rs. Its 33 recursive self-calls become one fold over an IdCache of types — which IS a_shared_subterm_is_checked_once_and_not_once_per_occurrence, by construction rather than by a special case — and the 16 KB frame that aborts the process disappears with the recursion.
Stage 4 — the second kernel, recheck.rs. It gets its OWN TermStore. Do not share one between the two kernels: six soundness bugs this campaign were miscounted identically in both, so double_check agreed with the bug throughout. A shared store is a shared bug.

§What this file hands the kernel TODAY, with no representation change

The four stages above all move the kernel onto TermId. These work against the Box-recursive Term the kernel already has, and each is one line at a call site. The first three are WIRED IN — type_checker::{infer_type, is_subtype}, reduction::normalize_checked_at, recheck::{recheck, double_check} and reduction::reduce_step_opt’s Term::Let arm all call into this file now:

deepen_stack — the kernel takes its own stack, sized from the term it was handed, so the door’s advertised limit becomes the real one and no admitted term can abort the process. One line at the top of each public entry, with no re-indentation of its body.
zeta_or_share_opt — the whole occurrence-gated ζ rule, as one call, in the Option<Term> shape reduce_step_opt has. Both kernels used to ζ-substitute UNCONDITIONALLY, so a value bound once and used n times was written and checked n times, which is a_shared_subterm_is_checked_once_and_not_once_per_occurrence exactly: 329 nodes against a ceiling of 97, and 92 under this rule — the case is green. occurrences_in_term is the gate underneath it and zeta_expand_head_term is what conversion owes in return. All three are iterative, so none has the ceiling type_checker::body_stats does.
kernel_stack_bytes — recheck.rs’s stack budget was a hard-coded 1 MiB that assumed a 2 MiB thread. Derived from this instead, the second kernel stops answering Unsupported on a deep term the first kernel now checks happily.
deepen_stack_with_depth — NOT yet wired, and it closes a hole the other three do not. The door and deepen_stack both measure the term they were HANDED; infer_type’s Var arm walks the CONTEXT’s type instead. MEASURED in a child process: a one-node term Var("x") under a binding of depth 4000 kills the process both bare AND through deepen_stack, and is answered when the sizer is told the context’s depth.
TypeCache + TermStore::env_for — inferType memoised on (environment, term), which is a_shared_subterm_is_checked_once_and_not_once_per_occurrence on the CHECKING side. The environment is in the key because Term names its variables and Context::extend shadows; Lean’s Expr is de Bruijn and does not need it, which is exactly why porting its inferType cache across unchanged is unsound here.

Two things not to do. Do not put the store in Context — Context is cloned on every extend and would copy the store with it. And do not key a CACHE on a term’s identity alone: Term names its variables and Context::extend SHADOWS, so one TermId has one type per scope. TypeCache carries the EnvId that makes the key sound, and KernelCall gives it a lifetime it cannot escape.

The float question is SETTLED. Literal’s PartialEq is hand-written in term.rs and compares f64::to_bits(), so it is total and reflexive and the store’s interning key is the kernel’s own equality. literal_identity_eq is the INDEPENDENT second implementation of that rule, locked against term.rs’s over an adversarial grid, and eq_faithful is the conservative guard that was correct under the old rule and stays correct under the new one.

§Example

use logicaffeine_kernel::term_store::TermStore;
use logicaffeine_kernel::Term;

let mut store = TermStore::new();
let x = Term::Var("x".to_string());
let twice = Term::App(Box::new(x.clone()), Box::new(x.clone()));

// The two occurrences of `x` are ONE node.
let id = store.intern(&twice);
assert_eq!(store.dag_size(id), 2);      // the App and the one shared Var
assert_eq!(store.tree_size(id), 3);     // what a tree walk would count

// Interning identical structure yields the identical handle: equality is O(1).
assert_eq!(store.intern(&twice), id);
assert_eq!(store.extract(id), twice);

Structs§

DefEqCache: A cache of decided conversions, keyed on a PAIR of node identities.
EnvId: Identity of a hash-consed LOCAL TYPING ENVIRONMENT — the fragment of a Context that decides a term’s type, and therefore half of the key an inferType cache must have.
IdCache: A cache keyed on node identity, dense: Vec<Option<V>> indexed by the id, so a lookup is a bounds check and NOT a hash.
KernelCall: A token that lives exactly as long as ONE outermost kernel call, and that a cache BORROWS.
LevelId: Identity of an interned universe level.
LitId: Identity of an interned literal.
NameSetId: Identity of a hash-consed, sorted set of names.
ScopedDefEqCache: DefEqCache branded with the lifetime of ONE outermost kernel call. See DefEqCache::scoped.
ShapeMask: The set of NodeShapes occurring anywhere in a subterm — one u16, computed once at interning time and answered in O(1) thereafter.
SubstId: Identity of a hash-consed simultaneous substitution.
TermId: Identity of an interned term — a Copy handle whose equality IS structural equality.
TermStore: A hash-consed term store: maximal structural sharing, O(1) equality, O(1) annotations.
TooLarge: A DAG whose unfolding is too large to materialise as a Term.
TypeCache: inferType, memoised on (environment, term) — the cache Lean has and we do not, with the half Lean does not need because its Expr is de Bruijn.

Enums§

LevelView: A borrowed view of one interned universe level.
Node: One term node with its children replaced by handles — the flat shape that makes the store a DAG rather than a tree.
NodeShape: Which Node kind a subterm is — one per Node variant, and wildcard-free everywhere it is matched for the same reason Node is.
Occurrences: How often a name occurs — the only distinction an occurrence-gated ζ rule needs.
StoreNormalForm: The result of TermStore::beta_zeta_normalize — honest about a budget it did not finish inside, the way reduction::normalize_checked is.

Constants§

BASE_STACK_BYTES: The floor under any stack the kernel sizes for itself, whatever the term’s depth — room for the non-recursive part of a kernel call, and for a panic to unwind and format its message.
BYTES_PER_RUNG: Stack reserved per rung of nesting past INLINE_DEPTH.
INLINE_DEPTH: The deepest term the kernel will walk on a stack it did not size.

Functions§

beta_zeta_normal_form: THE PURE β/ζ DOOR. The Term-level entry point a tree reducer wires in so a β-heavy reduction stops being quadratic — and the only one it needs, because it answers None for every term it is not certain about.
beta_zeta_normal_form_in_context: beta_zeta_normal_form with every policy question answered from the Context — the form a reducer wires in, with nothing left for the caller to get wrong.
deepen_stack: Run f on a stack sized for term — or report that this call is already on one.
deepen_stack_all: deepen_stack for an entry point that takes more than one term — is_subtype and def_eq compare two, and the stack has to hold the DEEPER of them.
deepen_stack_all_with_depth: deepen_stack_all told about depth the TERMS DO NOT SHOW — and it is not a refinement, it is a hole in the door that this is the only way to close.
deepen_stack_with_depth: deepen_stack told about depth the term does not show — see deepen_stack_all_with_depth for the defect this closes.
kernel_stack_bytes: How much stack the kernel call on this thread is entitled to use.
kernel_stack_rungs: The rungs (BYTES_PER_RUNG each) of the stack this thread runs on, by the kernel’s own sizing rule: at least INLINE_DEPTH, at most the kernel’s term-depth door.
literal_identity_eq: THE ONE RULE. Total, reflexive literal equality — bit-exact on floats — offered as a FUNCTION so term.rs and this store cannot hold two different opinions about it.
occurrence_count_in_term: How many FREE occurrences of name a Term has, saturating at u32::MAX.
occurrences_in_term: occurrence_count_in_term, classified — everything an occurrence-gated ζ rule needs, and strictly CHEAPER than the count, because it stops at the second occurrence.
occurs_free_in_term: Whether name occurs free in body at all — stops at the first occurrence.
stack_bytes_for_depth: How many bytes of stack a term of this depth is given.
term_depth: The nesting depth of a Term, counted in EDGES: a leaf is 0.
within_kernel_depth: Whether syntax is within the kernel’s existing term-depth limit.
zeta_expand_head_term: ζ-expand a Let at the head, whatever its occurrence count — the step a conversion check must be able to take on demand once zeta_or_share lets a Let survive into a normal form. None for anything that is not Let-headed.
zeta_or_share: ONE ζ step, OCCURRENCE-GATED, against a reducer that always returns a Term.
zeta_or_share_in_place: zeta_or_share_opt on a Let the caller owns, stepping its parts where they lie: the same rule, in the same order, with the same answer, but a part that a step leaves alone is never copied and nothing is rebuilt around the one that moved. step_in_place must be the in-place twin of step (reduce_step_in_place of reduce_step_opt), which reduction::owned_normalize_controls pins shape by shape. false for anything not Let.
zeta_or_share_opt: zeta_or_share against a reducer that reports PROGRESS: step answers None when there is no redex. reduction.rs’s reduce_step_opt calls it for every Term::Let.