RFC: a fixpoint that settles

@thomasklemm

Current state (updated Oct 10)

rubys gave the go-ahead to stage the work, and dai199 confirmed that S2 fits harvest_return.rs; their suggestions shaped this plan. S2a to S3 are commits on the staged branch, with S2b to S3 behind flags that are off by default. A follow-up branch adds shuffled-order canaries, an error census and two fixes to the sharing. Milestone 2 has the staged measurements. The research is open in #669, where anyone can take on a problem, and records what came after, including the merged #674 (the receiver-side rows the proposal below calls a follow-up), #705 and #724.

S0 Opt-in canaries show whether the whole-program fixpoint settled #657
S1 A cloned type shares its children instead of copying them #656, then each distinct piece stored once and visited once
S2a Why each untyped exists: pending, gradual or unresolved
S2b Joins instead of overwrites
S2c Recursive types by origin
S3 Re-type only what changed; dependency order comes after the any-order gate
S4 Precision and typed recursion in generated code (prototype)

Gates in roundhouse's terms, for S3 with every flag on against main 194f26cf at milestone 2 (first update, second); the October 10 re-measurement follows the table:

Gate	Status	Where it stands
Flags off changes nothing	✅	Emission identical on 105 fixture × target pairs; suite and typing ceilings as main
Every loop settles	✅	On all five public apps and the large app
Same answer every run	✅	Every digest agrees across runs
Same answer in any order	❌	The ivar and parameter slot joins on main now satisfy the lattice laws (#705, #724), but the structure the fixpoint works over still depends on the schedule
No new errors	⚠️	None new, but 10 of Discourse's 13 fewer are hidden, not fixed
`check` time	⚠️	Faster on the public apps; on the large app 3% slower, or 18% faster with the type-identity prototype
Precision	❌	Fully typed −0.19 points; fewer oracle rejections than main; at least one gain is unsound

October 10, on main c210f226 with #705 and #724 merged. The research corpus re-measured S3 on the five public apps. Each point names its fact in facts.md, and each fact links its receipts in the lab.

Settling isn't quiescence yet. S3 reports every loop settled, but an extra verification round still moves values on four apps (F22, F24).
Any order passes on none of the five (F24). A new structure dump shows writers and routes differing between schedules on all five apps, and slots on four. A plain repeat keeps slots and writers but still changes routes on four, so route differences can't be pinned on the schedule alone (F31).
Same answer every run holds for value digests on all five apps, but for the structure digest on only two (F24).
Precision: 69.81% of expressions are fully typed, against 70.16% for the main-compatible base (F23).
Errors: one error only S3 reports, and fifteen only the base reports; nine of those fifteen are hidden by unknown receivers rather than fixed (F27).
Soundness: the first traces from a public app's own tests. Across 127 values recorded by three Discourse tests, main accepts all 127 and S3 rejects 36. Every acceptance involves an uncertain or unsupported type, so this is witnessed coverage, not a soundness proof (F29).
Incremental: warm replay matches a cold check on all six edits; computing input fingerprints takes most of its time (F30).

Corrections to the original proposal

The three large-app runs differ only in the final expansion, which walked HashMaps in hash order. The loop's own state is identical across hash seeds, and S2c now walks in sorted order. Order-dependent rules do remain, but they show only in shuffled order, not run to run.
The history-only limit holds in principle: a cut that sees only a slot's history can't tell recursion from a long chain. But on main, A recursive method's harvested return stops unrolling; a gap cause is the same on every run #528's cut leaves short chains alone, as dai199's six-method chains show.
⊥ for pending values is the join's identity during the loop. It is not Ty::Bottom, which means "never returns" and prints as never, ! or bot. Pending values left at the end go through the entry-point policy, which settles them as gradual untyped.
Ty already keeps Var, Untyped and Bottom apart; the operations merge them (is_unknown, strip_unknown, the harvest fallback). S2a puts provenance on Ty, which reverses Stabilize harvested returns that oscillate on Untyped/Var #505's choice to keep it off, and its commit message says why.
Precision is reported as the share of expressions fully typed, with no untyped or Var at any depth, next to the share holding untyped and the runtime oracle's rejections. A count alone rewards rules that drop arms a value really has; the oracle catches those.

Links: staged branch · follow-up branch · lab · research: #669 · related: #630 (class/instance dispatch, merged)

Original proposal (frozen)

Kept exactly as posted on Oct 8, so the comments below keep pointing at the right sections. The current plan and corrections are in "Current state" above.

Roundhouse's type analysis copies recursive types one level deeper each round, until the round cap or #584's size bound cuts them off. Stored as cycles instead, and computed by rules that never retract a conclusion when they learn more, those types stop growing, and the analysis settles on its own.

Measure	Without the proposal	With the proposal (prototypes)
Large app from #518: production and absorb loops	run to the 12-round cap	settle in 6 and 3 rounds; one more round changes none of 1,235,386 expression types
Public apps whose loops settle	2 of 5	5 of 5
Large app's biggest type carried between rounds	24.1M tree nodes, only 127 of them distinct	each distinct piece stored once
Large app checked with no size bound	killed at the 40 GiB memory limit	completes at 3.06 GiB
A 64-method chain with no cycle (reproduction)	unfinished at the round cap	settles with 2 typings per method
13 small reproductions: expressions typed as bare `untyped`	14.1%	1.3%

A loop settles when a round changes no signature before the 12-round cap. Roundhouse runs three loops in turn: production; views and tests; and absorb, which re-runs production when views or tests moved one of its signatures.

Main fits in memory today because #584's bound cuts large carried types to untyped. With each distinct piece stored once, no size bound is needed.

The combined prototype is still slower on the large app: about 41 s, or 46–47 s with S1's sharing, against 31 s for the same base with a size bound. More of its expressions also contain untyped somewhere: 24.4% against 23.0%. On its own, the ordered worklist took about half the time (0.53× and 0.61× in two paired runs), though not yet with identical answers; bringing that speed into the combination is the next step.

Baselines: the first two rows are main after #584 (4be26816 for the large app, 07ce8255 for the public apps); everything else is b28b17b6, from before #584, where the prototypes were built. In the proposal column, the memory rows are S1 alone, the chain row is S3 alone, and the rest are the combined prototype: S2 and S3 together, whose results S1's sharing doesn't change. Re-measurement on current main is under way. Each prototype is a patch in the lab, which reproduces every public number; the combined one is phase-c2.diff, research probes included. Conditions are listed at the end.

How it works

Take the JSON-style normalizer from #518 (reproduction). Its true return type is recursive:

type j = Hash[String, j] | Array[j] | Integer | String | nil

Each round re-types the method with the previous round's answer pasted in, so after k rounds the type is unfolded k levels deep. thomasklemm logged its parameter type growing 9, 15, 33, … 332k nodes until the run was killed at 4 GiB; this shape escapes #528's recursion cut. Since #584, a size bound stops the growth, and whatever it cuts becomes untyped.

Stored instead as a cycle, with a reference back to where the value came from (its origin), the same type is finite, and the loop can arrive at it.

Some rules, though, retract conclusions when they learn more:

a block parameter is typed from a union's first arm only (reproduction);
in method dispatch, untyped swallows the whole union, while parameter unification drops it.

With rules like these, a loop can flip forever while nothing grows. As thomasklemm found in #518, such flips are what hold Mastodon and Discourse at their caps. When every rule is monotone, never retracting a conclusion when it learns more, and the loop starts from nothing known yet, it can only gain facts, and it stops, in any order of evaluation.

Each half fails without the other. Monotone rules without cycles keep climbing; cycles with rules that retract keep flipping. Together they settle on the least solution, the most precise answer the rules allow, in any order of evaluation. That is machine-checked in Lean 4 for a core calculus; the Rust prototype demonstrates settling, but not yet that its answer is the least one.

The approach isn't new. Research type checkers for unannotated Scheme programs used it in the 1990s to infer and print recursive types, and TypeProf takes a similar approach for Ruby; citations are in the credits. The staged plan also answers three concerns on record: an accumulating row contaminated by an early placeholder (68f4d828), the "larger typing-provenance change" #505 anticipated, and "a new Ty variant that every emitter handles" (#518).

Proposed stages

Stage	Change	Evidence
S0. Canaries	checks that a settled loop really settled: an inventory of state carried between rounds, plus same-seed and shuffled-order runs	partly in place via #589
S1. Shared types	each distinct piece of a type stored once, with operations that visit each piece once	with no size bound, the large app completes at 3.06 GiB instead of being killed at 40 GiB; generated code is byte-identical
S2. Monotone rules and recursive types	rules that never retract a conclusion, starting from nothing known yet; recursive types stored as references to their origin	with S3 also on, all 5 public apps and the large app settle
S3. Ordered rounds	a method is re-typed only when something it read changed, in dependency order	chains of 32–128 methods take 2 typings per method; capped rounds spend 25 and still don't finish
S4. Precision and printing	separate results per argument shape where the return depends on it; recursive types printed as RBS aliases, behind a flag	modeled only

How the stages land:

S1 is designed to preserve behaviour, so it can land first.
S2's rules and recursive types land together.
S3 follows S2: first in a shadow mode that only checks that skipped methods wouldn't have changed, then as the default.

Each stage ships as small PRs; anything that changes results stays behind a flag until it passes the decision gates under Details. Emitting recursive types in generated code, new or raised caps, and inference state persisted between builds are out of scope.

Questions for the maintainers

S1: is sharing types a good first step, and how should its migration be split and timed? Its first part touches 108 files.
Provenance: today's untyped can mean not computed yet, opted out or unresolved. Is splitting those three, with an explicit policy for entry points and for methods whose callers are never seen, acceptable as the "larger typing-provenance change" Stabilize harvested returns that oscillate on Untyped/Var #505 anticipated?
Recursive types: should they be analysis-only references, a Ty::Rec that emitters print as untyped? The alternative, folding each slot's history where a round hands types to the next, needs no Ty change, but it reads only history, so by finding 2 below it can't be exact on every acyclic chain; it is offered only as a fallback.
Scheduling: should S3 share a design with thomasklemm's change-driven scheduling for Spinel, RFC/spike: evaluate change-driven fixpoint scheduling within one fresh whole-program analysis matz/spinel#7237?
Where things live: should the Lean proof, the pinned public-app corpus and the runtime oracle, which checks inferred types against values recorded while the code runs, move into this repository, or stay in the lab?

Details

Why the loops don't settle: four findings

Growth (#518) and oscillation share a root: the loop has nothing to settle to. Oscillation is on record twice: rubys noted Mastodon methods that "flip between two types each round" (ccbafad6), and thomasklemm named it "the next convergence item" (#518). Today a cap, a bound (#584) and a stabilize rule (#521) make the loop stop anyway, and each hides the others' symptoms.

1. The memory is copies, not information (measured). A carried type is one that a round hands to the next: a method's return, a parameter row, an instance variable or a constant. On b28b17b6 with no size bound, the large app's largest carried type, a method return, has 24,052,607 tree nodes but only 127 distinct subtrees. The sampled signature state has 54.0M nodes and 17,663 distinct subtrees. As the largest type grows, its tree roughly triples each round, while its distinct subtrees grow by about nine.

2. The answer is a cycle, not a finite tree (proved for the calculus). Each return, parameter row, instance variable and constant is a slot with one type for all calling contexts, so the rules are set constraints: each slot stands for a set of possible values, constrained by the code. With finitely many constructors and program sites, no negated constraints, and conditions restricted to sites that can build a value, their least solution is a regular tree language (Heintze–Jaffar): a set of trees that a finite grammar describes. On recursive data, that grammar has a cycle. A loop over finite trees holds depth k after round k, much as listing x, xx, xxx, … one at a time never arrives at x*.

The cycle must point to where a value came from, not to what it resembles. #528's cut and #584's bound see only a slot's own history, and a cutoff like that provably can't tell recursion from a long chain. Suppose it stops the recursive slot X = Integer | Array[X] at round k, and what it cuts stays cut. On a chain of k methods, each wrapping the next one's result in an Array, the first slot has exactly the recursive slot's history for k rounds, so the cutoff fires there too and over-approximates forever. A recorded origin tells them apart: the chain has no back edge, no reference back to an earlier slot.

3. Some rules aren't monotone, and some state is hidden (measured, with public reproductions). A rule is monotone if learning more about its inputs never retracts a conclusion about its output.

First-arm block binding. A block parameter takes its type only from the first concrete arm of the receiver's union. In the reproduction, one round turns the parameter row Hash into Hash | Array[Integer], and the next turns it back into Hash: more input gives less output, so the row flips forever.
untyped wins in dispatch, then is dropped. Dispatch on a union that contains untyped returns bare untyped, discarding the other arms' results; parameter unification then drops that untyped. In the prototype's first configuration, this pair caused the last oscillation in Mastodon's absorb loop.
History-dependent stabilize. When a return keeps changing between variants that share a concrete core but differ in their untyped or Var arms, Stabilize harvested returns that oscillate on Untyped/Var #521's stabilize keeps the first variant written. On Forem, global rounds and an ordered schedule both reach a state that one more full round leaves unchanged, yet 18 entries differ between them, each only in those arms: two different fixpoints of the same rules.
State outside the compared tables. The type an earlier round stamped on an empty literal (reproduction), parameter-default stamps and controller bindings all carry over between rounds, but the signature check that ends a loop doesn't compare them.

4. Rounds repeat work (measured). On the large app, depending on the loop and round, 74–98% of method-body re-typings produce the same output as before. Only re-typings whose inputs didn't change can be skipped safely, so this is an upper bound on avoidable work. Long chains need many rounds: the cap went from 4 to 12 when lobsters needed 9 (be964432). In the measured visit order, a generated 64-method chain advances one method per round and exhausts the cap, despite #524's dirty set, which narrows production rounds to what the call graph says changed.

Why accumulation can work now, after two failed attempts

Accumulating, joining each round's result into what earlier rounds found instead of recomputing it, was tried twice, and the two attempts failed differently:

68f4d828 (rubys) found the accumulating parameter table "monotonic in the wrong direction" and made it rebuild every round: "Round 1 … records Untyped; round 2 sees Str; unify fuses them into Str | Untyped, which is untyped with extra steps." An early placeholder had contaminated the row.
In Spinel, matz tried the rule "UNKNOWN must not downgrade an established return" and found that it froze a return that had genuinely become wrong (933266361). So Spinel resets and re-derives, by design (convergence notes).

Both point to the same lesson: accumulation is only safe when the analysis keeps the kinds of unknown apart.

Today one value carries two meanings that pull in opposite directions. Not computed yet (call it pending) is no evidence: it sits below every type, and the next round may replace it. The author opted out (call it gradual) is every value at once, and no round may remove it. Every rule that meets untyped must either keep it or drop it, and each choice is wrong for one meaning:

keeping a pending Untyped is 68f4d828's contamination;
dropping a gradual untyped is how Stabilize harvested returns that oscillate on Untyped/Var #521's stabilize can strip a genuine arm, and a short public reproduction types an Integer as String;
keeping it in dispatch and dropping it in unification is the Mastodon flip.

S2 separates the meanings. Pending becomes ⊥ ("bottom"): joining ⊥ with any type T gives T. Gradual stays untyped. Unresolved external or unsupported inputs become a third kind. With monotone rules and ⊥ as the starting value, every state the loop passes through lies below the final answer, so no round retracts what an earlier round concluded (the standard fixed-point theorems of Kleene and Knaster–Tarski). Operations that do narrow or retract, namely branch refinement, checks against declared types and retraction after source deletions, stay separate from this loop.

Accumulation alone isn't enough. For a non-monotone rule F, the iteration X ↦ X ∪ F(X), which only ever adds facts, can stop at a state where F(X) ⊆ X but F(X) ≠ X: some facts survive only because an earlier round produced them. Leastness and order independence don't follow.

Pieces are already in place: 16e1ead2 makes union_of a law-abiding join, with exhaustive tests of its laws, and #565 makes pending parameter joins commutative. Neither certifies the whole analyzer. #505 called the split "a larger typing-provenance change", and it is one: S2 needs the split at the producers, plus an explicit policy for entry points and unseen callers.

Stages in detail

S0: canaries and counters (no behaviour change). Part of this already exists:

Fixpoint bound follow-ups: record the Rust gap, pin that the fixpoint settles #589's fixpoint_rounds();
the determinism tests of Make a module parameter's call-site join order-independent (#209) #565, A recursive method's harvested return stops unrolling; a gap cause is the same on every run #528 and 16e1ead2;
Spinel's inference canary, requested by rubys in Proposal: add one or more "real applications" to the Spinel CI pipeline matz/spinel#4113.

S0 adds:

A carried-state inventory: a list of every value one round reads from an earlier one, with a check that one more full round changes none of them. A cache left off the list must be shown to depend only on listed state, and to be invalidated whenever that state changes.
Separate reporting: changes to signatures, to IR and to other carried state are counted separately, along with every cap hit and every frozen unit.
Order controls: on whole apps, repeat runs with the same seed, and runs in shuffled order.
Cyclic-type tests: adversarial tests for comparing cyclic types.
A growth estimate per dependency component, a group of slots or bodies that depend on each other in a cycle. Computed from type sizes, it predicts ×2.000 per round for the two-method cycle and ×1.645 for the normalizer, against ×2.00 and ×1.63 observed.

S1: shared types with DAG-aware operations (intended to preserve behaviour). ccbafad6 (rubys) shared the constant registry instead of copying it and took Mastodon's check from 12.9 to 4.6 s; #171 (tobi) shared constant scopes. S1 extends sharing to the types themselves.

Storing the 127 distinct subtrees once isn't enough on its own: comparisons, hashes, substitutions and rewrites still walk the 24-million-node tree they stand for. Two rules fix that:

memoize every structural operation on node identity, the standard technique behind hash-consing (Filliâtre–Conchon) and binary decision diagrams (Bryant);
a rewrite that changes nothing returns the node it was given.

Measured on b28b17b6 with no size bound; #528's cut and the round caps still apply:

sharing alone, without these two rules, reaches 16.4 GiB and is stopped at the 600 s deadline;
with them, the run completes at 3.06 GiB in 46.9 s;
generated code is byte-identical across 7 fixtures × 14 targets, the default suite passes (4,261 tests), and the three untyped-count ceiling tests hold at 0, 304 and 523.

The first step of the change touches 108 files. S1 hasn't been measured together with #584's bound; that measurement comes first.

S2: monotone rules from ⊥, landed together with recursive types by origin.

Recursive references. Inside a dependency component, a type refers to another slot's type by a (slot, program position) pair instead of embedding a copy. This is the classic set-based technique of one variable per program site; TypeProf v2 does something similar for container element types (related work). Ty gains an analysis-only Ty::Rec, which takes nine mechanical exhaustive-match updates, including fallbacks in eight emitter type renderers and the IDE. Emitters print untyped where a reference remains. That narrows thomasklemm's concern, "a new Ty variant that every emitter handles", to small fallback changes now, with typed recursive emission as later work.

A fallback needs no Ty change: where a round hands its types to the next, fold each slot's history into a recursive type kept in a side table, and let the typer see only a depth-limited unfolding of it, with untyped below. It reads only the slot's history, so by finding 2 it can't be exact on every acyclic chain; it is offered only as a fallback.

Monotone rules from ⊥:

block parameters join over every arm that answers;
unification joins instead of dropping;
pending values join commutatively;
the carried state from finding 3 becomes explicit slots;
the pending, gradual and unresolved split happens at the producers.

Why the halves land together (measured on the five public apps unless noted):

The rule repairs alone, with no recursive references and no bound. Two repairs act in this run: block binding over all arms, and visiting the classes that include a concern in name order. (In this prototype, the pending join has no effect without recursive references.) Discourse's node count stays within about 0.1% of the base's, but parameter rows still grow by a fixed amount each round (+11 nodes per round on Discourse, +8 on Chatwoot), Mastodon still oscillates, and the loops still run to their caps.
An earlier variant that also stopped untyped from swallowing the other arms in dispatch grows Discourse's final state 28× (1.09M → 30.9M nodes, 5.1 GiB). Removing one non-monotone rule can uncover growth that the old oscillation was holding in check.
Recursive references with today's non-monotone rules leave Mastodon's flipping row at the cap.
A partial port of the rules onto main 07ce8255, which includes A type the fixpoint carries between rounds stays bounded (#518) #584, leaves Mastodon and Discourse at their caps and adds 32 errors on Mastodon. On the large app, A type the fixpoint carries between rounds stays bounded (#518) #584's bound fires 5,243 times instead of 2,036.

S2's earlier prototype, fold2, without the ordered worklist, on the large app: 3.58 GiB and 78.2 s, against 34.5 s for the historical bounded control. The tests and absorb loops settle; production still runs to the cap.

S3: ordered rounds, after S2.

The change:

record each method body's read set, everything its typing read;
re-type a body only when something it read changed;
process bodies in dependency order (Bourdoncle's weak topological order, a standard ordering that iterates each cycle as a unit; see related work).

Read sets must include every semantic input; a changed input may still produce unchanged output.

Why after S2. The least-solution theorem for dependency-ordered solving assumes a monotone system with complete dependencies, so it applies once S2 holds.

In Spinel:

RFC/spike: evaluate change-driven fixpoint scheduling within one fresh whole-program analysis matz/spinel#7237 (thomasklemm) proposes change-driven scheduling for Spinel's deliberately non-monotone pipeline. Its obligation is different: preserve the existing semantics and validate pass order.
Proposal: opt-in compiler phase and fixpoint timing records for reproducible compile-time measurements matz/spinel#7236 (thomasklemm) proposes opt-in compiler-phase and fixpoint timing records.
FrancescoK's A method whose value moved has its callers' values derived again in the same pass matz/spinel#7697 and A call forwarding its method's parameters is bound again when they move matz/spinel#7699 shorten chains by re-deriving dependent values within the same pass.

Measured alone (S3 without S1 or S2), on b28b17b6 with the historical bounded control's size bound:

generated return chains of 32, 64 and 128 methods take 2.00 typings per method; capped rounds spend 25 typings per method and still don't finish;
on the large app, two back-to-back pairs of runs took 0.53× and 0.61× the bounded control's wall time.

The answers differ, so this is not a like-for-like speedup. The scheduler freezes 139 units (the bodies it types) after 12 changes each within a phase, an extra full round still moves 68 slots after production and 118 after absorb, and errors rise by 8. Inside the combined prototype, no unit freezes. On the large app, one dependency component holds 17,284 of 21,495 units (80%), so the gain comes from selective re-typing within components, not from small components.

S4: precision and printing.

Per-argument-shape summaries (modeled). Today a method gets one summary for all its calls. In a finite model of the normalizer, typing the body separately for Hash, Array and other arguments (three body rows instead of one) removes the 8 spurious receiver arms at its two merge calls. The complete shell, the smallest refinement that makes the analysis exact for these operations (Giacobazzi–Ranzato–Scozzari), shows that two summaries suffice for those calls: one for Hash arguments and one for everything else. Splitting has a cost: Endoh's commit e68384616 removed union-argument expansion, turning a 27-overload example into one union signature. So the number of summaries per method must be measured. Separate class-side and instance-side parameter rows remain a follow-up named in #551.

Printing. Before export, resolve alias cycles that pass through no type constructor (type a = b | nil with type b = a), then validate with rbs; version 3.10.0 accepts the JSON alias from How it works. Roundhouse's reader currently rejects multiple overloads and leaves cyclic aliases unread (src/rbs.rs), so the reader comes first. The Rust-target gaps #589 records for methods that walk recursive data, serde_json::Value lacking transform_values and case value when Hash / when Array rendering as a type-blind match, need the operations and branch tests lowered too, not just a type.

What the combined prototype shows, and what it doesn't

The combined prototype is S2's recursive references and monotone rules with S3's worklist, on b28b17b6, with no size bound; adding S1's sharing changes no result, only memory and time. Its whole diff, sharing included, is phase-c2.diff, run with the flags of phase-c2a in configurations.json.

Large app. Each configuration has two timing runs, back to back with no other benchmark running; separate instrumented runs check the result, three without sharing and one with it.

Production stops after 6 rounds and absorb after 3.
An extra round changes none of the recorded signature, IR (0 of 1,235,386 expressions) or recursive-table fingerprints.
Without sharing, the two runs take 40.8 and 41.1 s at 3.82 and 3.79 GiB. With sharing, they take 46.9 and 46.0 s at 3.08 GiB. The historical bounded control takes 31.4 and 31.5 s at about 3.78 GiB.
Errors are 3,335 against the control's 3,336: dispatch goes 253 → 254 and ivar 67 → 65.

Public apps:

the five apps take 25.3 s in total, against 32.4 s for the control (0.78×; Forem is slightly slower);
in all five, one more full round after the absorb loop changes nothing recorded; one more round after the production loop still changes 3 expressions on Forem and 1 on Mastodon;
errors match by kind on four apps and fall by 12 on Discourse;
generated code is byte-identical across 7 fixtures × 15 targets (this harness has one more target than S1's).

Three integration fixes made the difference:

the worklist tracks reads of the recursive-reference table;
pending values join commutatively (without this, one Mastodon slot flipped 701,502 times);
back edges propagate in ordered sweeps.

The evidence supports three claims, of decreasing strength:

The prototype reaches a stable state, observed as quiescence: one more round changes nothing the instrumentation records. The fingerprint omits some carried fields, for example controller bindings, so S0's inventory is required before saying "fixpoint" without qualification.
The least solution is proved for the calculus under its hypotheses, but not established for the Rust result. The three verification runs on the large app agree on the recursive-reference table, but their signature and IR digests differ (300,632, 300,615 and 300,611 expressions containing untyped), because order-dependent rules remain.
Soundness for Ruby execution has known failures, found by the runtime oracle, which checks inferred types against values recorded while the program runs. On the normalizer, the inferred recursive type rejects 28 of 32 sampled runtime values, because block and argument flows (sort.to_h) aren't propagated. Traces from the other 12 small reproductions are accepted.

Precision. On the large app, 24.39% of the 1,232,382 expressions that carry a type contain untyped at some depth in the combined prototype, against 23.02% in the historical bounded control; on the five public apps, 14.45% against 14.18%. Counted by cause, most of the remaining untyped comes from parameters that no caller gives a type, from failed dispatch, and from pending placeholders that are never replaced; the untyped printed where a reference remains doesn't explain the gap on its own.

What is mechanized (Lean 4)

The fixed-point results are classical textbook theorems: Kleene and Knaster–Tarski fixed points, set-based analysis, and chaotic iteration. Several have been mechanized before, in Isabelle and Coq. The new part is a Lean 4 proof for a small model of the analysis with finitely many program sites, plus a proof that this model agrees with a relational statement of its rules (Equiv.pt_iff). Nothing proves that the Rust analyzer implements the model.

The build has no unproved steps (sorry, admit), no trusted evaluation (native_decide) and only the standard axioms. It proves:

Bounded rounds. Re-evaluating everything each round (naive) or only what new facts touch (semi-naive) needs at most |slots| × |sites| rounds; the productivity-refined solver needs at most |slots| × |sites| + |sites|. Worklist iteration terminates by a decreasing measure.
Leastness. The result is the least fixpoint. Semi-naive equals naive. Worklist solvers agree with them for any queue order that never drops pending work. Dependency-ranked layers solved to local least fixpoints give the global least solution.
Warm starts and edits. Starting from a state X other than ⊥ still gives the exact answer if X lies below the least fixpoint and one round only adds to it (X ⊆ F(X)). Rules added within the schema restart exactly from the old solution. Deleted rules can leave self-supporting stale facts, so deletion needs invalidation.
Meaning. The result is the least regular-tree solution once conditions are restricted to sites that can build a value. Soundness holds for a small language with records, arrays and recursion.
The history-only limit from finding 2.

Counterexamples show why the hypotheses can't be dropped:

the first-arm transfer has no fixpoint;
a seed fact that nothing derives, like a self-justifying Var, reaches a fixpoint that isn't least;
an untracked carried stamp defeats a table-only convergence test.

A starting state proven to lie below the answer may replace ⊥, and derived caches are allowed with correct invalidation.

Not proposed, decision gates and ownership

Not proposed:

typed recursive emission in any backend (emitters print untyped where a reference remains);
a new or raised cap or bound (existing caps stay, as canaries that should not fire);
inference state persisted across builds, or changes to Spinel (RFC/spike: evaluate change-driven fixpoint scheduling within one fresh whole-program analysis matz/spinel#7237 is a counterpart, not a dependency);
a change of diagnostics policy (errors that untyped used to hide are reported, and counted separately).

Decision gates:

S1 needs byte-identical generated code for every fixture and target, a green default suite, and a measurement paired with A type the fixpoint carries between rounds stays bounded (#518) #584.
S2 needs:
- the public apps to settle with errors by kind no higher than main on the same base;
- the large app re-measured on current main;
- no run-to-run difference under the carried-state inventory and order controls;
- the share of expressions holding untyped back at main's level.
S3 first runs as a shadow schedule that asserts a skipped body would not have changed, as RFC/spike: evaluate change-driven fixpoint scheduling within one fresh whole-program analysis matz/spinel#7237 stages it. It becomes the default after S2.
S4 waits for S2 and S3, and must report context and grammar sizes.

Ownership:

S2 touches harvest_return.rs (A recursive method's harvested return stops unrolling; a gap cause is the same on every run #528, A call through x.class does not feed the instance method of that name #551; dai199) and the parameter join (Make a module parameter's call-site join order-independent (#209) #565; eddygarcas).
S3 touches dirty_retype.rs and the scheduling thomasklemm deferred in Stabilize harvested returns that oscillate on Untyped/Var #521 and began in Narrow production typing rounds with a call-graph dirty set #524.

Each stage is offered as small PRs against that work, not around it.

Conditions and reproduction

Bases:

Prototype base: b28b17b6 unless a commit is named.
Historical bounded control: b28b17b6 with an experimental depth-8, 256-node bound. It is not A type the fixpoint carries between rounds stays bounded (#518) #584, whose depth-16, 512-node bound applies where types are stored.
Post-A type the fixpoint carries between rounds stays bounded (#518) #584 main, as measured: 4be26816 for the large app and 07ce8255 for the public apps; live main has moved on since.
Re-measurement: every staged PR is re-measured, paired, on its own target base.

Evidence labels:

measured: run in the real analyzer on a named base;
modeled: shown in an executable Python model only;
proved: machine-checked in Lean 4 for a core calculus.

Inputs:

Public apps: Campfire, Mastodon, Chatwoot v4.18.0, Discourse v2026.9.0 and Forem, at pinned commits.
Large app: a private Rails app of about 1,380 Ruby files, the one from Analysis grows without bound on a helper that returns a recursive array (since #477) #518, reported as aggregates only.

The lab: bunnykong/roundhouse-fixpoint-lab holds the recipes, manifests, patches with their flags, runtime oracle and Lean project. Each result names its base, flags and command. Wall times depend on the host.

Credits

Upstream:

@thomasklemm: A type the fixpoint carries between rounds stays bounded (#518) #584's bound and Fixpoint bound follow-ups: record the Rust gap, pin that the fixpoint settles #589's loop reporting, with the census of carried types across seven public apps; Stabilize harvested returns that oscillate on Untyped/Var #521's stabilize and Narrow production typing rounds with a call-graph dirty set #524's dirty set; Proposal: opt-in compiler phase and fixpoint timing records for reproducible compile-time measurements matz/spinel#7236 and RFC/spike: evaluate change-driven fixpoint scheduling within one fresh whole-program analysis matz/spinel#7237 for Spinel;
@dai199: A recursive method's harvested return stops unrolling; a gap cause is the same on every run #528's recursion cut and A call through x.class does not feed the instance method of that name #551's x.class filtering;
@eddygarcas: Make a module parameter's call-site join order-independent (#209) #565's order-independent parameter joins;
@rubys: 16e1ead2's law-abiding join, ccbafad6's shared constant registry and 68f4d828's rebuilt parameter table;
@matz: Spinel's convergence rules and inference canary;
@tobi: Make roundhouse check fast on large apps #171's shared constant scopes and Meta PR 2: fixes from running roundhouse over a large internal Rails codebase #503's fixes from a large Rails codebase;
@FrancescoK: A method whose value moved has its callers' values derived again in the same pass matz/spinel#7697 and A call forwarding its method's parameters is bound again when they move matz/spinel#7699, which re-derive dependent values within a pass.

Precedent:

set-based analysis (Heintze; Heintze–Jaffar);
Soft Scheme and MrSpidey, research type checkers for Scheme that printed inferred recursive types for unannotated programs, in published results from a few thousand lines up to 17,661 lines (Wright–Cartwright; Flanagan–Felleisen);
TypeProf (Endoh);
Bourdoncle's chaotic iteration strategies;
hash-consing (Filliâtre–Conchon);
complete shells (Giacobazzi–Ranzato–Scozzari).

The full list, with links, is in RELATED-WORK.md.

@thomasklemm

A few specific questions for the people whose work this builds on:

@thomasklemm: S2 and S3 build on A type the fixpoint carries between rounds stays bounded (#518) #584 and Fixpoint bound follow-ups: record the Rust gap, pin that the fixpoint settles #589, and on Stabilize harvested returns that oscillate on Untyped/Var #521 and Narrow production typing rounds with a call-graph dirty set #524. Does finding 3 under Details, the non-monotone rules, match the oscillation you traced on Mastodon and Discourse? And should S3 share a design with RFC/spike: evaluate change-driven fixpoint scheduling within one fresh whole-program analysis matz/spinel#7237 (question 4)?
@dai199: S2 changes harvest_return.rs, where A recursive method's harvested return stops unrolling; a gap cause is the same on every run #528's cut lives. Where recursion is certified, it would store a recursive reference instead of cutting to untyped. Does that fit your plans for that file?
@eddygarcas: S2 needs every pending join to be commutative, as Make a module parameter's call-site join order-independent (#209) #565 made the module parameter join. Does extending that to all pending values look right to you?
@tobi: S1 extends Make roundhouse check fast on large apps #171's sharing from constant scopes to the types themselves. On the large app from Analysis grows without bound on a helper that returns a recursive array (since #477) #518, the prototype completes the check at 3.06 GiB with no size bound, which may help on codebases like the one behind Meta PR 2: fixes from running roundhouse over a large internal Rails codebase #503.
@rubys: questions 1, 2 and 5: how to stage S1's migration, whether to split untyped into pending, gradual and unresolved, and where the proof and corpus should live.
@matz: question 4. S3 and RFC/spike: evaluate change-driven fixpoint scheduling within one fresh whole-program analysis matz/spinel#7237 face the same scheduling problem from opposite sides: a monotone analysis here, and Spinel's deliberately non-monotone pipeline there. S2's case for accumulation starts from the failure matz/spinel@9332663616 records.

A staged diff on current main, one commit per stage, follows in this thread when it's ready.

Thanks for this. It's a careful piece of work, and the diagnosis matches what I saw on Mastodon: when ccbafad made rounds cheap, the flipping was still there, and my attempts at a "no downgrade to untyped" rule and a "no new facts" stopping rule didn't settle it either. Your explanation of why each half fails without the other is the clearest account of that I've read.

On the questions you put to me:

S1 staging, and splitting untyped: you've got this. You know the migration's shape better than I do. Splitting pending, gradual and unresolved is the lesson I took from 68f4d82, and I'm glad to see it made explicit. Sequence it however works best for you. The gates you've written (byte-identical output, a green suite, a paired measurement against #584) are the right ones.

Where the proof, corpus and oracle live: your call too. Whatever a CI gate depends on probably wants to be in this repo eventually, but there's no rush.

A few things I'd be curious whether you've considered:

Identical results run to run as the first gate. The three large-app runs giving different digests stood out to me more than the precision or timing numbers. Have you considered making "same answer every time, in any order" the bar S2 has to clear before anything else is weighed?
Measuring each stage in roundhouse's terms. Settling and least solutions are the analysis's own yardsticks. Have you considered also reporting each stage by error counts, check time on Mastodon and Discourse, and untyped in the generated code? Those are what tell us more of Rails transpiles.
Where recursive types would pay off. Generated code is byte-identical and typed recursive emission is out of scope, so the payoff for the transpiled output is deferred. Have you considered naming one concrete target, say typed recursion in the Rust or Crystal output where Fixpoint bound follow-ups: record the Rust gap, pin that the fixpoint settles #589 recorded gaps, as the reason the later stages are worth it?
S3 earlier. On its own the ordered worklist took about half the time on the large app, and that's the piece that speaks most directly to Mastodon's cost. With the shadow mode you describe (checking that every skipped method really wouldn't have changed), have you considered whether it could come before S2 rather than after?
The untyped split as its own step. Have you considered landing the three kinds first as a tag that changes no behavior, with byte-identical output, and changing the join rules afterward behind a flag?

Looking forward to the staged diffs.

Thanks, that's generous, and so is the latitude on S1 and on where the proof, corpus and oracle live.

Both rules you tried fail for reasons the RFC predicts:

"No downgrade to untyped" freezes an answer once it looks informative, so when a value genuinely changes, the stale answer stays. matz found the same in Spinel: the rule "froze a return that had genuinely become wrong" (matz/spinel@9332663616).
"No new facts" stops when a round adds nothing. But a rule that isn't monotone can also stop producing a fact it produced before, and that fact stays stored, stale. So "no new facts" means settled only when every rule is monotone (learning more never withdraws a conclusion) and the loop starts from nothing known yet. The Details block "Why accumulation can work now, after two failed attempts" works this through.

Each of your five suggestions changes the plan, and two come with a caution:

Same answer every time, in any order, as the first gate. Adopted, with a correction to the RFC first.
- Run to run, the large app's digests differ after the loop, not inside it. Under two different hash seeds, the state the loop settles on is identical; only the final expansion differs. That step unfolds recursive references into ordinary types for the emitters, and it walks HashMaps in hash order. A sorted walk is the planned fix.
- In shuffled order, every difference traced so far on the public apps comes through one of two rules. decide_harvested_return (from Stabilize harvested returns that oscillate on Untyped/Var #521) chooses between a method's stored return and its newly harvested one, and several of its branches keep whichever was written first, or last. unify_param_ty, when both values are pending, keeps the later one, so HashMap iteration order can decide the result.
- The plan: each rule gets an order-independent replacement, a join that gives the same answer whichever value arrives first. Repeated and shuffled-order runs check it before precision or timing is weighed. Main's own output already varies by a few lines between runs, as thomasklemm noted in #518, so the same replacements should help main too.
Each stage in roundhouse's terms. Adopted, with one caution. Every staged diff will report, next to the analysis's own measures, errors by kind, check time on Mastodon and Discourse, and untyped in the generated code, counted in the .rbs sidecars Spinel reads. The caution: both counts can mislead when a rule drops an untyped arm that a value really has. The sidecar prints String | untyped as plain untyped, so dropping the arm improves the count while making the type wrong. Errors mislead the same way: in the RFC's join_untyped reproduction, current main reports no known method `bit_length` on String for a call that succeeds at runtime, because the dropped arm left only String. So each report will pair the counts with the runtime oracle, which checks inferred types against values recorded while the program runs.
A concrete payoff. Adopted. The target is the normalizer from Analysis grows without bound on a helper that returns a recursive array (since #477) #518, transpiled with a real recursive type, so the generated code compiles and prints what Ruby prints. In Rust, where Fixpoint bound follow-ups: record the Rust gap, pin that the fixpoint settles #589 recorded the gap, that means an enum, with case value when Hash / when Array lowered to a match on its variants. In Crystal, a recursive alias expresses the type directly.

There is also a nearer payoff, found today. Main's test a_result_merged_back_into_its_own_parameter_settles_bounded (in recursive_type_bound) settles only because main drops the |k, v| block flow in sort.to_h. Restoring that flow on main, a fix that only adds information, makes the test fail: its loops run to the cap. The prototype, given the same fix, settles the program. On main, a sounder type and a settling loop exclude each other here; the new fixpoint gives both.
S3 earlier. Yes, with S3 split in two:
- The first half keeps today's round order and skips re-typing a method when nothing it read has changed since its last typing. A typing depends only on what it reads, so the same inputs give the same output, and skipping should change no answer, even under today's rules. Shadow mode re-types every skipped method anyway and checks that claim. This half can follow S1.
- The second half visits methods in dependency order. Under today's order-dependent rules that changes answers, so it waits for the replacements in (1).
One caution: the "about half the time" came from the full worklist, which also reordered, and so changed answers. How much of that gain the first half keeps isn't measured yet.
The untyped split as its own step. Adopted. The three kinds land first as a tag that changes no output, so byte-identical output is the whole review. The join rules and recursive references follow, each behind its own flag, switched on together, since each half fails without the other.

The staged diffs will follow in this thread, each measured as in (2).

@bunnykong

@bunnykong Thanks for laying out how this touches #528.

Short answer: yes, it fits. #528's cut was a stopgap for one symptom, chatwoot's sanitize_mailbox_value doubling every round. It decides "recursive" from the slot's own history, and a recorded origin is a better witness. I have nothing in flight on harvest_return.rs that this would collide with.

I built phase-c2.diff on b28b17b6 next to current main and tried a few small shapes. Below are three suggestions, plus one finding that the RFC doesn't cause.

1. One merge decision per slot. decide_harvested_return is currently the one place that says what a write to a harvested return does. In the prototype, fold::join_rets joins on top of it afterwards. So a reference-mode slot goes through #521's history-dependent stabilize first and the monotone join second. I'd rather S2 replace those rules inside decide_harvested_return than add a pass after it.

2. The Campfire case in the module header. It records that a full lattice join was tried and rejected, because Untyped followed by Nil collapsed Campfire's URI helpers to bare Nil. That is the pending/gradual confusion again. The split should fix it, but only if those helpers' Untyped is classified as gradual or unresolved rather than pending. It would make a good regression test for the producer-side split.

3. Gates for this file. The insert_recursive_return_* tests pin the cut. Under the fold they need SCC-keyed equivalents (the sanitize, flattened-union and record shapes). Chatwoot's check --continue time and memory should be a gate too, since that was the hang #528 fixed (over 20 minutes and 30 GB before). For scheduling, a work-count check in the style of Spinel's make scale-test could help: generate the chain at two sizes and compare typings, not seconds. Your chain-64 runs in about 0.04 s here. On the prototype it settles with 128 typings (2 per method); main leaves 39 of the 64 returns untyped. A count like that doesn't depend on the machine and is cheap enough for the default cargo test job, next to tests/recursive_type_bound.rs, which already guards time and memory for the cycle shapes.

On the cut outside certified components: on current main I couldn't make it misfire on a plain chain. I tried six methods each wrapping the next in an Array, defined in either order, on the class side and the instance side, and every one was typed exactly. So I don't mind when the cut goes; reporting harvest_untie_cut per stage would show it becoming unused.

A class/instance finding the RFC doesn't cause. I checked whether def self.call(*a) = new(*a).call would read as a self-call and put call into reference mode, since the call-graph edges are keyed by (class, method). It doesn't: the prototype reports rec_methods: 0 for that shape. But the same shape already failed earlier, on both b28b17b6 and main. Dispatch checked class_methods before instance_methods on the shared Ty::Class, so Greeter.new(x).call resolved to the class-side call, whose body then resolved to itself and stayed untyped. Forem writes this service-object shape in 107 files. #630 fixes it: across the seven public apps, warnings drop by 614 and chatwoot loses 19 errors; the 30 errors it adds are existing gaps that a return type now reaches, detailed there. The side ambiguity lives in Ty itself, not only in the params and slot keys that #551's follow-up and S4 mention, so it's worth knowing before S2's join meets those slots.

Thanks for building phase-c2.diff and trying shapes against it, and for confirming that S2's change fits your plans for harvest_return.rs. All three suggestions are adopted.

1. One merge decision per slot. Agreed. S2's order-independent join will replace the rules inside decide_harvested_return, and the separate fold::join_rets pass goes away. The function is central to rubys's first gate, the same answer in any order: every shuffled-order difference traced to a method on the public apps passes through it, because several of its branches depend on the order of writes. But the join alone won't meet the gate. In a first trial of the order-independent joins, Campfire gives the same answer in any order, while Chatwoot, Mastodon and Discourse still don't: some rules for typing method bodies aren't monotone yet, and which slots become references can depend on the order. The staged diffs will report each source.

2. The Campfire case. Agreed on the diagnosis, and it becomes a regression test for the untyped split. Your caveat held: a trial that treated every unknown return as not computed yet, failed method lookups included, brought the collapse to Nil back. The test fails under that trial, and passes on main and when only genuinely pending returns are treated that way. Telling those apart needs the provenance tag, which is why the tag lands first.

3. Gates for this file. All four go into the plan:

SCC-keyed versions of the insert_recursive_return_* tests, for the sanitize, flattened-union and record shapes;
Chatwoot's check --continue time and memory at every stage, since that was the hang A recursive method's harvested return stops unrolling; a gap cause is the same on every run #528 fixed, alongside Mastodon and Discourse;
a work-count test in the default cargo test job, next to tests/recursive_type_bound.rs: the chain at two sizes, compared by typings rather than seconds, with the RFC's chain-64 as the first case;
harvest_untie_cut, reported per stage.

On the cut outside certified components. Your six-method chains show that on main the cut leaves short chains alone. The RFC's finding 2 is a limit in principle: a rule that sees only a slot's own history can't tell a recursion from a long enough chain whose history grows the same way, one level per round. A recorded origin can. The per-stage counter will show whether the cut stops firing, and so far it hasn't: on the prototype it still fires on four of the five public apps, and a first trial of the order-independent joins makes it fire more often. The staged diffs will explain why.

On the class/instance finding. Thanks for tracing it and for #630. The side lives in Ty itself, not only in the parameter rows that the RFC's S4 note mentions. Once #630 lands, the def self.call(*a) = new(*a).call shape becomes one of S2's tests, checking both sides' returns and that neither call enters reference mode.

All of this goes into the staged diffs.

Join what one round hands the next instead of replacing it (opt-in)

The staged diffs are up: six commits on main 194f26cf, one per stage, with the untyped tag as its own step, so S2 is three commits. With every flag off, each commit gives main's output: emission is byte-identical on all 105 fixture × target pairs, the library tests pass at every commit, and the default suite passes at the tip. The PRs will be rebased onto current main.

Each stage in roundhouse's terms on Mastodon · Discourse · Chatwoot, against main at 194f26cf. Errors were identical across three runs; times are medians of three interleaved runs.

Stage	Errors	`check` s	Loops
main	1,583 · 3,136 · 958	9.1 · 20.9 · 4.3	production at the cap on all three; absorb too, except on Chatwoot
S0. Canaries, opt-in	as main	as main	as main
S1. Shared types	as main	8.5 · 19.7 · 4.0; peaks 13–16% lower	as main
S2a. The `untyped` tag	as main	9.1 · 20.2 · 3.9	as main
S2b. Joins, alone	+11 · −4 · +1	8.7 · 21.5 · 5.8	every loop at the cap
S2c. Recursive references	+1 · −5 · as main	9.2 · 18.9 · 5.0	Mastodon and Discourse settle; Chatwoot's production doesn't
S3. Dependency-ordered worklist	as main · −13 · as main	5.5 · 16.9 · 3.0	every loop settles, on all five public apps

S2b is measured alone only because the split asks for it; it ships switched on with S2c. Its 11 extra errors on Mastodon are 7 dispatch and 4 binop. S3's 13 fewer on Discourse are 10 dispatch and 3 binop.

untyped in the generated code, the share of signature positions in the Spinel sidecars, pooled over the five public apps: 40.89% of signature positions hold untyped on main, S1 and S2a; 41.19% at S2b alone; 40.99% at S2c and S3.

Precision, fully typed with the runtime oracle beside it: 69.02% of expressions are fully typed on main and 68.83% at S3, pooled over the five apps, and the share holding untyped goes from 14.34% to 14.55%. Beside that, of 17,820 values recorded at runtime across 53 traces, S3's types reject 6,699 and main's 9,224. Most of the difference is in the recursive reproductions; the settling reproduction below still needs the flow fix (8 rejected at S3, 6 on main).

On S3 earlier: the S3 commit is the whole worklist, so its times include the reordering. The first half, skipping unchanged methods in today's order with a shadow check, isn't on the branch yet, and how much of the gain it keeps isn't measured.

The large app from #518 (aggregates only), at S3: production settles in 6 rounds and absorb in 3, and two runs agree in every digest. Errors are 3,598 against main's 3,675, 1.47 points more expressions hold untyped (24.66% against 23.19%), and peak memory is 3.0 GiB against main's 4.0, mostly from S1. It is still slower: 47 and 66 s on a loaded host, against 39 s for S2a, which gives main's answers with S1's sharing, in the same series.

The same answer every time:

Run to run, it holds. Two runs at S3 agree in every digest on all five public apps and on the large app; S2c now walks the final expansion in sorted order.
In shuffled order, the branch can't check it yet; S0's shuffled-order control comes next. On the RFC's prototype, a trial with the one merge described below removes the order dependence in merges and shows what remains. None of it is a merge. What remains includes body rules that settle differently depending on order (on Chatwoot, chunk ends as Array[Int] in one order and Array[untyped] in another), and the choice of which slots become references.

The two payoffs from the earlier reply, now public reproductions:

On main, a sounder type costs settling; S2 and S3 with the fix give both. Main settles but rejects 6 of 12 values recorded at runtime, because it drops the |k, v| flow in sort.to_h. Restoring the flow on main runs production and absorb to the cap. S2 and S3 alone settle but reject 8 of 12. With the corrected flow rules on top (branch fixpoint-sound, behind RH_FOLD), every loop settles within 3 rounds and none of the 12 are rejected.
Typed recursion in generated code. On the RFC's prototype, behind a flag, a recursive reference prints as a Rust enum (with case … when Hash / when Array lowered to a match on its variants) and as a Crystal alias. For three of the four shapes Fixpoint bound follow-ups: record the Rust gap, pin that the fixpoint settles #589 recorded, cargo check goes from 3–5 errors to none, crystal build passes, and each program renders what CRuby renders, byte for byte. The class-method cycle isn't covered yet, and the emitter handles only these walk idioms.

dai199's suggestions:

One merge decision per slot isn't on the branch yet: S2b still joins after decide_harvested_return. A trial that makes it the one merge settles and repeats run to run. But it adds dispatch errors on Chatwoot, Forem, Mastodon, Discourse and the large app, on calls that T | untyped used to absorb, so it waits until the error report counts those apart.
The Campfire case has been a test since S2b, and it caught a real bug. S2b's join dropped a gradual untyped from a nil-only core, which turned the URI helper into a method that always returns nil. S2b now keeps that untyped, and the test passes at every stage.

dai199's gates for harvest_return.rs

The shapes the insert_recursive_return_* tests pin settle by reference under S2c, and the cut never fires on them.
tests/chain_typing_count.rs, in the default cargo test job, settles chains of 32 and 64 methods with two typings per method, every link typed. Main leaves 7 of 32 and 39 of 64 returns untyped.
harvest_untie_cut, Mastodon · Discourse · Chatwoot, falls from 44 · 195 · 83 on main to 18 · 58 · 46 at S3. It no longer fires on the recursive walkers it was written for (Chatwoot's sanitize_mailbox_value, Discourse's map_json and others). The cuts that remain aren't recursion: most withdraw a known return when an untyped arm joins it, and the rest cut a pending placeholder. The provenance tag tells both apart from recursion, so the next step is to cut only strict nesting of an informative return.
Chatwoot completes in under 8 s and 0.6 GiB at every stage.

Still open:

the large app's speed under S2 and S3;
the same answer in shuffled order;
the name_collision reproduction, where a class method and an instance method of one name share a parameter row. It needs rows keyed by side, the follow-up named in A call through x.class does not feed the instance method of that name #551.

Next: S0 and S1 as the first PRs, with S1 split into shared payloads and the single walk over each shared node, each rebased and measured on current main. Corrections to the original proposal are listed at the top of the issue.

Since the last update, the first two PRs are open, a prototype addresses the large app's speed under S2 and S3, and errors are now matched call site by call site, which corrects how the last update read Discourse's 13 fewer errors. Two results are setbacks: at least one precision gain is unsound, and freezing part of the structure changed answers.

The PRs. #657 adds S0's opt-in canaries. #656 is the first half of S1: a copied type shares its pieces instead of duplicating them. Both pass CI.

The large app's speed, left open last time. A profile of S3 on the large app finds joins in 17% of the analyzer's samples, resolving recursive references in 15% and comparing types in 8% (the shares overlap). A prototype behind RH_ARENA gives each type two identities:

an exact one, which keeps record field order and the untyped tag;
a semantic one, which agrees with Ty::eq.

The prototype remembers each union by its ordered pair of exact identities, so a repeated join is a lookup, and it resolves references by semantic identity. No typing rule changes.

With every S2 and S3 flag on, the large app's check takes 34.0 s with the prototype, against 43.0 s without it and 41.7 s on main 194f26cf. Last time's comparison was with S2a; this one includes main. These are medians of three interleaved runs on a loaded host, and in every run the prototype beat both. On Mastodon and Discourse it takes another 6% and 8% off S3's time (Chatwoot wasn't in this series). Peak memory on the large app is 3.1 GiB, 2% above S3 alone and still well below main's 4.0, mostly thanks to S1.

All ten S0 digests, the errors by kind and the diagnostic content are identical with and without the prototype on the five public apps and the large app, and the default suite passes. With the S2 and S3 flags off, the union memo alone still takes 3–5% off check time on Mastodon, Discourse and the large app, so it can follow S1 as a PR of its own; resolving references by semantic identity goes with S2c.

A bug in the staged branch's sharing, found by the prototype and fixed

S1's interner reuses any live value that is equal apart from the untyped tag, so a value could come back carrying another value's tag. The join memo, which lasts for a single join, compares the same way. No typing rule reads the tag yet, and with the interner's fix every S0 digest, error count and loop outcome is unchanged on the five public apps and the large app (the digests, like Ty::eq, ignore the tag). The tags themselves change on all six: on Mastodon, the untyped leaves tagged gradual at the end of the run fall from 12,902 to 5,370, and the difference is now tagged unresolved. The join memo's fix passes its own tests; its run on the apps comes next. The narrower cut proposed last time will read the tag, so both fixes ship with S2a, where the tag first appears. #656 has neither the interner nor the memo, so it isn't affected.

Errors by kind, classified. A census now matches each failing call site between main and S3:

S3 adds no error on any of the five public apps.
Of Discourse's 13 fewer errors, 3 are binary operations whose operands gained an arm that makes them compatible; whether that arm occurs at runtime isn't checked yet.
The other 10 are dispatch errors whose receiver now includes untyped, which hides them rather than fixes them.

So the top section's "as main or fewer" holds only for the count; the section now says so, and the gate counts hidden errors on their own line from now on. The census needs name-level output, so it runs on the public apps only; the large app's dispatch +10 and unsupported −85 remain counts by kind.

Precision, expression by expression. Last time S3 was 0.19 points below main in fully typed expressions. Matching every expression between the two, about a million on the five public apps, shows S3 losing precision on 4,823 and gaining it on 2,334. About half of the losses already hold untyped before recursive references are expanded, a quarter pick it up during expansion, and the rest hold an unresolved type variable. Switching rules off one at a time puts roughly a third each on the worklist's order, on S2c's reference slots, and on S2b's joins and all-arms binding, counting a loss that several switches recover only once.

Some causes are specific and have small fixes. Two are prototyped behind flags but not yet measured on the apps:

a class test that succeeds but still lets untyped into the branch;
Array(…) applied to a recursive reference, which treats the reference as a single value: in a focused test, an array of strings comes out as Array[Array[String]], a wrong type rather than a vague one.

A third, the class-versus-instance dispatch, is already fixed on main by #630, which the staged branch predates.

At least one gain is unsound. In Discourse's app/jobs/base.rb, S3 types @data as a hash of Integer values after both a String and an Integer are stored in it, because the join over its []= writes loses the earlier contents. Only a sample of gains was checked, and no runtime trace covers the apps, so the oracle couldn't catch this. The fix is to keep the prior contents in that join, and traces of app code would let the oracle catch the next one.

The same answer in shuffled order. It can now be checked. On a follow-up branch, S0's canaries gain a seeded shuffle of the worklist and a digest of the structure the fixpoint works over, meaning which slots exist, who writes each one, and which become recursive references. At S3 today, that structure differs between schedules on four of the five public apps and changes during the run on all five. So there is no single fixpoint for the order to reach, and repairing the rules alone can't give the same answer in any order. This is also where the analyzer departs from the lab's Lean model, whose slots and constraints come from the program before solving.

A first attempt at fixing the structure changed answers. It builds part of the structure before typing: which methods are recursive, and the call graph between them. On the four public apps measured so far, that part now stays the same from start to end and across schedules. The rest is still created while typing, and it still differs between schedules on three of those four apps. Freezing only part of it also changed answers: errors appear on all four apps (on Forem, dispatch errors rise from 177 at S3 to 219), and some are hidden on Chatwoot and Mastodon. So this step stays local until the rest is declared too.

Still open: the same answer in shuffled order, and the name_collision reproduction, which waits for parameter rows keyed by side, the follow-up named in #551.

Next:

the second half of S1 once A cloned type shares its children instead of copying them #656 lands, then the union memo as its own PR;
S2a as a PR, with both fixes for the tag;
the unsound []= join fixed, and the precision fixes measured on the apps;
the staged branch rebased onto a main that includes A call on an instance answers the instance method of its name #630;
dai199's one merge per slot, run through the census;
the rest of the structure declared before typing.

@dai199

The research behind this RFC is now public in #669, a draft not proposed for merge in this form: six open problems, a check for each, the established facts with their commits, and every attempt so far, dead ends included. The problems are hard and still open, and progress will be faster with more people working on them. Anyone is welcome to take one on: the README shows how to pick a problem, run its check on the pinned public apps, and report back here.

@dai199, your suggestion of a single merge decision per slot has now been through the census, as the last update planned. The trial is on fixpoint-onemerge, behind RH_DET, off by default. It bundles the one merge in decide_harvested_return with normalized joins, so its effects aren't the merge's alone:

It settles, gives the same answer every run, and raises the pooled share of fully typed expressions from S3's 68.83% to 70.77% on the five public apps, above main's 69.02%.
Against S3, it also adds 107 errors and removes 20. A review against the source judged 80 of the 84 new dispatch errors impossible and four unclear; none is confirmed real.
In 59 of them, the receiver is nil alone where the source builds an object. At S3, 53 of those receivers held an unresolved type variable and 6 an untyped arm. The cause at the producer isn't traced yet, but because those receivers now count as fully typed, part of the gain is unsound.
In 9 more, Mastodon's can? surfaced once its receiver lost an untyped arm. User delegates can? to its role, and the analyzer doesn't model that delegation; untyped used to hide the gap.
The other 16 dispatch errors have mixed causes, and the 23 errors of other kinds weren't reviewed.

One question, where a link to the lines would be enough: at S3, most of those receivers held a pending value beside nil, and in the trial only nil is left. Is there a place in decide_harvested_return, or in the join, where a pending arm next to nil can be dropped, and should it be kept as unresolved instead? It resembles the Campfire case you raised, with a pending value where Campfire had a gradual one.

Your recent PRs already appear in the research. #630 removed one of the causes of lost precision, and #634 changed main's to_h pair reading, which the lab's settling reproduction depends on; re-checked on current main, that reproduction still holds.

@bunnykong

@bunnykong, on your question. Short answer: yes, but commutativity is not enough on its own. Every join that feeds a carried slot needs to be a real join-semilattice: commutative, associative and idempotent, with one operator per slot and with pending as its identity. On main, several joins fall short of that in ways #565 didn't touch. And as your structure digest already shows, the join laws give a schedule-independent answer only when the transfer rules are monotone and the slot set is fixed before solving. So I'd treat the joins as necessary, not sufficient.

What #565 did, and how far it carries. It made unify_param_ty symmetric by ordering Var < Untyped < concrete, checking Var on both sides before Untyped. It also sorted the includers by class id before folding, but that sort only gives the same answer run to run. It does nothing for a shuffled worklist, so it can't stand in for a commutative join. The ordering part does generalize, and it's cheap, because union_of already canonicalizes. One caveat about our own change: absorbing Untyped below a concrete type is right for pending and unresolved values, and wrong for gradual ones. It drops a real arm, the same failure as your join_untyped reproduction. Once S2a's tag exists, the rule should read: pending and unresolved are identities, and gradual stays as an arm. Campfire's start_new_session_for(user) would still get User, because that untyped is a registry gap (unresolved), not a dynamic value.

Joins on main that aren't semilattice joins (at d4f4076; each one confirmed with a scratch unit test):

unify_param_ty with two pending values keeps the later one: unify(Var(1), Var(2)) = Var(2), but unify(Var(2), Var(1)) = Var(1) (mod.rs#L6876-L6881). This is the case you traced.
unify_param_ty isn't associative across union_of. It absorbs a bare Untyped but not an Untyped arm inside a union, so unify(Int, Str | untyped) = Int | Str | untyped while unify(unify(Int, Str), untyped) = Int | Str. The answer depends on whether a producer joined first. The fix is to define the join on the flattened arm set and classify each arm (mod.rs#L6865-L6908).
union_of and unify_param_ty disagree about Var. union_of keeps it as an ordinary arm, while unify_param_ty and widen_hash_ivar_value treat it as bottom. So widen_hash_ivar_value gives Hash[Str, Int | Str] when the {} seed comes first, and Hash[Str | Var, Int | Str | Var] when a []= write comes before it (mod.rs#L7796-L7821, body/mod.rs#L2665).
widen_hash_ivar_value ignores a []= write when the ivar is Hash | Nil, or anything else that isn't a bare Hash (mod.rs#L7806). A nullable hash keeps Hash[Str, Str] | Nil after an Int write. That is not an ordering bug but a lost write, close to the unsound @data case on your soundness frontier.
Record order breaks canonical unions. Row.fields is an IndexMap, so == ignores field order, but cmp_row compares in insertion order (ty.rs#L550-L563). union_of({a: Int, b: Int}, {a: Str, b: Int}) and union_of({a: Str, b: Int}, {b: Int, a: Int}) come out as unions with different variant order, and the two aren't ==. push_union_variants also keeps whichever field order arrived first (body/mod.rs#L2762). Records also join as separate arms rather than field by field, unlike Hash and Array. That keeps the laws, but it is worth deciding on before S2c's record shapes.
The size bound runs after every pairwise join (bound(unify(slot, obs)) at mod.rs#L5203 and #L5417, the ivar merges at L7611/L7624/L7643, and harvest_return.rs#L156). bound doesn't distribute over the join. With a 10-deep Array and two 300-class Hash values, one grouping ends as untyped and the other keeps the deep array. The fix is to bound once per slot per round, after the whole fold, or to treat the bound as a widening applied at one fixed point in the schedule. With S2c's references it should almost never fire, but a backstop that fires in an order-dependent way breaks the gate whenever it does.
decide_harvested_return is replacement, not a join (harvest_return.rs#L115-L142). It keeps the last write when the cores differ. For example, Str | untyped then Int gives Int, and the reverse order gives Str | untyped. It also has an untie step that depends on history. You and @dai199 already have this one in fixpoint-onemerge. The only thing I'd add is that switching it from replacement to accumulation is safe only once pending and unresolved are identities, or stale arms from early, less-informed rounds stick for good. On main, strip_unknown maps Var to Untyped (ty.rs#L447-L460), so stabilize_untyped_return_oscillation turns a pending arm beside nil into a gradual Nil | untyped (harvest_return.rs#L42-L55). That may bear on your question to @dai199 about pending arms next to nil.

union_of itself is fine: its lattice-law tests (body/mod.rs#L3873-L3968) hold, apart from the record field order above.

Cost. Sorting fold inputs costs O(n log n) per fold and is negligible, but it only buys determinism from run to run. Normalizing on the arm set costs about what union_of's canonicalization already costs, and your union memo covers the repeats. Comparing record rows with keys in sorted order adds a sort per comparison, unless rows are canonicalized when they're built. If emitted field order matters for a target, the canonical form should keep a stable source order rather than arrival order.

Offer. I can take items 1 to 6 as one PR against main, outside decide_harvested_return, which stays with fixpoint-onemerge. The PR would contain:

a single join for parameter slots, defined over the classified arm set;
consistent Var handling in union_of and widen_hash_ivar_value;
records compared without regard to field order;
the bound applied once after each slot's fold;
generated lattice-law tests (commutative, associative, idempotent, pending as identity) over every carried-slot join, next to union_of's tests and tests/concern_param_determinism.rs.

Before S2a's tag lands, it would use today's Var and Untyped and leave gradual absorption alone. After S2a, it would switch to the tag. I'd report it with the any-order check and the census on the five pinned apps. If that works for you, I'll claim it under "Any order".

Add background notes, and a first claim on the any-order frontier

@eddygarcas

@eddygarcas, thanks. "Necessary, not sufficient" is the right framing, and the seven joins are exactly what the any-order brief was missing. They're now in it, linked back here, and the claim is recorded.

Points of contact for the PR:

Overlap. A cloned type shares its children instead of copying them #656 changes how Ty payloads are shared, mostly mechanically across many files. The staged S2b and S2c commits touch unify_param_ty, the ivar merges and the harvest. Main comes first: whichever of A cloned type shares its children instead of copying them #656 and your PR lands second rebases, and the staged branch rebases onto both.
Running the checks. The canaries aren't on main until Opt-in canaries show whether the whole-program fixpoint settled #657 merges, so build the change on top of fixpoint-next to run the any-order check. There, PROBE_BASE=1 gives main's behavior in the same binary, and RH_PRECISION_CENSUS=1 adds the precision shares.
Item 4 may explain the unsound @data case in Discourse's app/jobs/base.rb (facts F8): an ivar seeded with {}, then written through []=. It would make a good regression test.
Item 5. The staged sharing (the second half of S1) reuses a payload only when it is equal including record field order, because some targets emit fields in that order. Comparing rows regardless of order works as long as the stored form keeps source order, as you suggest.
Item 7. The strip_unknown path, which turns a pending arm beside nil into a gradual Nil | untyped, looks like the missing link for the question to @dai199. It's noted in the soundness brief.

@bunnykong

@bunnykong On fixpoint-onemerge it's dropped in the join itself, not in the old harvest rules.

In det.rs, norm_opt removes a Var arm of a top-level union as ⊥ (L512). Below the top it becomes pending_untyped; at the top nothing is kept. So Nil | Var normalizes to Nil.
Every harvested return goes through it under RH_DET: lat_norm on the first write (harvest_return.rs L197) and lat_join in decide_harvested_return (L144-L148). The rules eddygarcas pointed at (stabilize_untyped_return_oscillation via strip_unknown) aren't reached in the trial. On main they turn the same pair into Nil | untyped, not Nil.

Should it be kept as unresolved? I think so, because a Var beside nil is often not pending. The body typer returns the same Var(0) (unknown()) when dispatch finds nothing, and nothing refines it later:

a modeled class whose walk misses the method (send.rs L1585);
a Time or Date method that isn't modeled (L1882-L1883);
a union whose arms all miss (L1921).

Reading those as ⊥ removes a real "unknown" and leaves nil, which would explain receivers that are nil alone where the source builds an object. I haven't traced the 59 sites to confirm it.

Until S2a's tag can tell the producers apart, a safe rule is to drop a Var arm only while the slot can still change, and keep any that survives to quiescence as unresolved, counted as not fully typed. With the tag, those dispatch fallbacks would produce unresolved directly, and only the placeholder seeded before a slot is first computed would be ⊥.

Separately, I'll take the name_collision follow-up: parameter rows keyed by receiver side, the follow-up named in #551. It's a change on main, outside the staged branch; I'll report it here with the checks.

@bunnykong

@bunnykong Thanks for the trace. It also corrects my examples: the fallbacks are in the class walk and on unmodeled receivers, not the Time/Date path. Agreed that the precision has to come back by modeling those methods.

@eddygarcas The row shape is settled: rows are keyed (ClassId, Symbol, MethodReceiver) (ParamKey in src/analyze/mod.rs), and apply_param_sites and the concern fold still join with unify_param_ty per row, so items 1 and 2 can build on that. The (class, name) view App::inferred_method_params publishes stays as it is too: the one review comment on it doesn't hold, because the controller's class-side helper clones are the helper_method instance methods themselves, whose view calls feed the instance row. CI is green; I'll note here when #674 lands.

Make modeling the fallback methods precision's next step

@eddygarcas

@eddygarcas #674 is merged (c19524c). Two review fixes went in with it: the owner walk now looks for a def on the call's side first, so Child.fetch reaches Grand.fetch past a Base#fetch, and the S0 canaries' fingerprint reads rows by side (Class.name / Class#name). The row key is ParamKey = (ClassId, Symbol, MethodReceiver) as described above.

@bunnykong

Items 3 to 6 are up as #705, against main. All emitted output is unchanged on all 12 targets, and there is a generated lattice-law harness and a regression test for the @data shape. On fixpoint-next the pooled fully-typed share moves 68.83% → 68.99% (S3) and 69.02% → 69.20% with PROBE_BASE=1.

Items 1 and 2 are built on #674's rows, but one choice is yours before they go up. @bunnykong @dai199, once unify_param_ty treats an untyped arm inside a union like a bare one (item 2's associativity fix), Nil | untyped joins to Nil. On our runtime probe that types Relation#order_key_of's record as Nil, and +2 sites lose their type. It is the same nil-only case as S2b on Campfire. Three options:

(a) Only a non-nil concrete type absorbs untyped, so unify(Nil, untyped) stays Nil | untyped. This keeps the laws, never narrows to bare Nil, and is my preference until S2a lands.
(b) Keep untyped arms inside unions as they are. The result then still depends on grouping, so item 2 isn't really fixed.
(c) Hold items 1 and 2 until S2a's tag, then absorb only pending and unresolved values.

Would you rather have (a) now, or wait for (c)?

@eddygarcas

@eddygarcas, thanks for #705. (a) now, please. It keeps the laws and never narrows to bare Nil.

I'd keep (a)'s rule after S2a too, because (c) as written would likely bring the nil-only receivers back. In the RH_DET trial, 52 of its 59 nil-only receivers came from permanent dispatch fallbacks, 49 of them registry gaps (28 missing methods, 21 unmodeled receivers), and none from a pending value (F18). Keeping every surviving Var as unresolved removed all 59, but fully typed fell to 64.01%, against 68.83% on S3. (a)'s rule is narrower: it keeps the arm only when no non-nil type sits beside it.

So unresolved would stop being an identity: pending is the identity, unresolved is absorbed only by a non-nil concrete type, and gradual stays an arm. start_new_session_for(user) still gets User. If the tags share one untyped arm, gradual has to win when they merge, or grouping matters again.

Record rubys#705 and split the any-order claim

analyze: keep `[]=` writes made before the Hash seed (rubys#617)

analyze: make the ivar-slot join treat a pending Var as identity (#617)

analyze: keep `[]=` writes to a nullable Hash ivar (#617)

ty: order record rows regardless of field order (#617)

analyze: bound each ivar slot once, after its writes (#617)

Merge pull request #705 from eddygarcas/any-order-ivar

analyze: make the parameter-slot join a lattice join (#617)

analyze: bound each parameter row once, after its fold (#617)

Merge pull request #724 from eddygarcas/any-order-params

Navigation Menu

Repository navigation

RFC: a fixpoint that settles #617

Current state (updated Oct 10)

Original proposal (frozen)

How it works

Proposed stages

Questions for the maintainers

Details

Credits

4 remaining items

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

RFC: a fixpoint that settles #617

Description

Current state (updated Oct 10)

Original proposal (frozen)

How it works

Proposed stages

Questions for the maintainers

Details

Credits

Activity

bunnykong commented on Oct 8, 2026

rubys commented on Oct 8, 2026

bunnykong commented on Oct 8, 2026

dai199 commented on Oct 8, 2026

bunnykong commented on Oct 8, 2026

bunnykong commented on Oct 8, 2026

bunnykong commented on Oct 9, 2026

bunnykong commented on Oct 9, 2026

eddygarcas commented on Oct 9, 2026

bunnykong commented on Oct 9, 2026

dai199 commented on Oct 9, 2026

4 remaining items

dai199 commented on Oct 9, 2026

dai199 commented on Oct 9, 2026

eddygarcas commented on Oct 9, 2026

bunnykong commented on Oct 9, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions