Measure rebuild/search cost; make the @UF clear opt-in - #44

Closed

oflatt-claude wants to merge 118 commits into

saulshanabrook:mainfrom

oflatt-claude:worktree-uf-clear

Commits on Jul 27, 2026

Add an occurrence-index catalog; post each row once per distinct value

oflatt
and
claude
committed
150f145
Add occurrence atoms to the free-join query language

oflatt
and
claude
committed
8feaa93
Expose occurrence atoms through the bridge

oflatt
and
claude
committed
cdf3ad1
Add the (index name function (any cols...)) command

oflatt
and
claude
committed
b1cf686
Rebuild the encoding's eq-sort columns through a declared index

oflatt
and
claude
committed
c642dee
Document the index-driven rebuild; tidy the diff's comments

oflatt
and
claude
committed
d0370dc

Commits on Jul 28, 2026

Fix the defects two reviews found in the occurrence-index work

oflatt
and
claude
committed
30d871a
Test the silent defects; refuse the plan shapes an index cannot serve

oflatt
and
claude
committed
083ce8d
Tell get_index which question a probe asks, rather than infer it

oflatt
and
claude
committed
6f9e989
Test that an occurrence atom overrides the requested plan strategy

oflatt
and
claude
committed
b561863
Tidy the comments added by the review fixes

oflatt
and
claude
committed
15bbe04
Order a rule proof's substitution by first occurrence in the body

oflatt
and
claude
committed
39fbc88
Enumerate a rule head's conclusion sites in one place

oflatt
and
claude
committed
8104d89
Turn off the CSE prepass while the proof encoding is reworked

oflatt
and
claude
committed
5ddb853
Record the integer_math cross-treatment failure as a bug, not an artifact

oflatt
and
claude
committed
6fe4274
Write down the proof-encoding rework plan

oflatt
and
claude
committed
a1edaa0
Check that a rule's conclusion can be rebuilt from its premises

oflatt
and
claude
committed
0ca6723
Make the encoding's set-if-empty read its own batch's pending inserts

oflatt
and
claude
committed
87dfd0b
Record the check_shadowing clone as deferred, not taken

oflatt
and
claude
committed
17628ab
Split phase 2 into indexing and deletion

oflatt
and
claude
committed
2a7303c
Stamp each rule proof with the head site it concludes at

oflatt
and
claude
committed
9670cc3
Make unchanged view row counts an explicit gate

oflatt
and
claude
committed
9a6c61a
Record why a rule head's skeleton is not reconstructible from a site

oflatt
and
claude
committed
09e4391
Give encoder temporaries their own fresh-name counter

oflatt
and
claude
committed
14670be
Record how the canonicalization bridge is carried

oflatt
and
claude
committed
4db5308
Synthesize a rule head's proof skeleton instead of emitting it

oflatt
and
claude
committed
40f2b14
Read a deep proof without a deep call stack

oflatt
and
claude
committed
4502d04
Write the sequenced plan down, and correct the Fiat note

oflatt
and
claude
committed
75e7202
Read each table once per extraction, not once per node

oflatt
and
claude
committed
fa5918a
Apply the proof simplifier's reflexive identities before minting

oflatt
and
claude
committed
283e289
Record the premises-inline-then-chain design

oflatt
and
claude
committed
f2f74b0
Collapse the last reflexive composites, and stop reading a proof nobody uses

oflatt
and
claude
committed
ea9082f

Commits on Jul 29, 2026

Carry a rule's premises inline, and chain its later sites

oflatt
and
claude
committed
403473d
Stop storing a rule proof's terms, since nothing reads them

oflatt
and
claude
committed
c65362a
Record the refactor, two bugs, and correct the term-mode note

oflatt
and
claude
committed
611c2d0
Cover the indexed rebuild rule in unsafe_seminaive_matches_naive

oflatt
and
claude
committed
06b786d
Make correctness at every phase an invariant, not a hope

oflatt
and
claude
committed
365f068
Drop the dd endpoints from the nightly for now

oflatt
and
claude
committed
7fc8053
Pack a rebuild firing into one raw proof node

oflatt
and
claude
committed
720065e
Stop re-minting the container anchor the rebuild primitive already wrote

oflatt
and
claude
committed
4c197d6
Stop minting the body Fiat triples nothing reads

oflatt
and
claude
committed
d5c9d24
Pack a rebuild firing's congruence steps into one row

oflatt
and
claude
committed
7015b3a
Fold a rebuild firing's e-class move into its packed row

oflatt
and
claude
committed
a932b22
Defer the skeleton composites, so a head that reads none writes none

oflatt
and
claude
committed
9fa84f6
Narrow the row-count nondeterminism to merge-function invocations

oflatt
and
claude
committed
d5868f4
Prototype the head-traversal unification over a sink

oflatt
and
claude
committed
b7b3028
Revert the sink, keeping the congruence it made redundant

oflatt
and
claude
committed
34fcda2
Require a rule's premises to cover its body facts

oflatt
and
claude
committed
b0f8fbb
Let the nightly run be tried locally without publishing

oflatt
and
claude
committed
7ffbfbd
Let the local nightly publish, since nothing is published

oflatt
and
claude
committed
ef231f1
Pack a merge collision's displaced edge into one proof row

oflatt
and
claude
committed
70479df
Restore the harness node count, and say how to count it

oflatt
and
claude
committed
3912365
Merge upstream main for the nightly uv and rustup bootstrap

oflatt
and
claude
committed
0feb461
Stage a rule head's rows as a batch rather than one at a time

oflatt
and
claude
committed
9be2172
Record the follow-ups this PR is not doing

oflatt
and
claude
committed
f948fe3
Move the follow-ups out of the tree and into an issue

oflatt
and
claude
committed
88586eb
Drop the rework plan from the tree

oflatt
and
claude
committed
1da0392
Remove the CSE prepass

oflatt
and
claude
committed
4d2e861
Fold a firing's five types into one

oflatt
and
claude
committed
bf881be
Number a head's sites with a cursor instead of a shadow tree

oflatt
and
claude
committed
e24024d
Give a head one lowering description instead of two

oflatt
and
claude
committed
1b00670
Stop offering a connector that is never absent

oflatt
and
claude
committed
2815b8b
Retire the reconstruction experiment

oflatt
and
claude
committed
b8aa71f
Name the head module after what is left in it

oflatt
and
claude
committed
fbed16d
Change-log the rework, and drop the entry for the removed prepass

oflatt
and
claude
committed
eeae874
Check the site a rule proof names, not just that the head concludes it

oflatt
and
claude
committed
037d26b
Give rustup's shims PATH priority, not just PATH membership

oflatt
and
claude
committed
e3462f3
Read a chained rule proof's name off the row that carries it

oflatt
and
claude
committed
c78b4a1
Fix the role a canonical-reflexive proof names

oflatt
and
claude
committed
4a17c3c
Let a frame's stages branch directly instead of through a verdict type

oflatt
and
claude
committed
c135d84
Describe the rule-head lowering the encoder emits

oflatt
and
claude
committed
53b5ec8

Commits on Jul 30, 2026

Pin the preconditions the proof lowering relies on

oflatt
and
claude
committed
59b371b
Say what the nightly measures, and reject a non-positive round count

oflatt
and
claude
committed
6cf0fad
Trim this branch's doc comments to the contract

oflatt
and
claude
committed
ee2247a
Say which globals add a premise, and point at the test for it

oflatt
and
claude
committed
441dc59
Read a site's composition off the head, not off a re-encoding of it

oflatt
and
claude
committed
37afe30
Name a rule proof's conclusion with one integer

oflatt
and
claude
committed
1e739d7
Compose a head's proofs in one place, whichever side is asking

oflatt
and
claude
committed
53751a9
Keep the conclusion site out of the checker

oflatt
and
claude
committed
f42b6ed
Name a rule head's proofs by position, not by a role at a site

oflatt
and
claude
committed
ca6c83a
Return a built term's two ids from the recursion, not through a map

oflatt
and
claude
committed
47cde85
Tell the encoding doc as the proof it specifies, then the skeleton it writes

oflatt
and
claude
committed
8198f74
Ask for the value-rebuild rule you want, not for a tag

oflatt
and
claude
committed
e82ec30
Split a union's union-find edge by what justifies it

oflatt
and
claude
committed
8acefd1
Check a head's columns against the walk that fills them

oflatt
and
claude
committed
d7a45c4
Say out loud the shapes that would otherwise mint a wrong proof

oflatt
and
claude
committed
7fe510c
Make a stale doc link fail the build

oflatt
and
claude
committed
ee809b6
Ask one thing which of the two layers is in force

oflatt
and
claude
committed
0dacb3e
Say that layer 1 is an algebra with two interpretations

oflatt
and
claude
committed
bf0653f
Lay a head's columns out once, and check both walks against it

oflatt
and
claude
committed
bbefa37
Say what layer 1 does, not how obvious it is

oflatt
and
claude
committed
64fa634
Walk a nested term through layer 1, level by level

oflatt
and
claude
committed
9216c4a
Trim this branch's new docs to the contract

oflatt
and
claude
committed
2e898d6
Say why the natural node stays unseeded, and stop there

oflatt
and
claude
committed
579d119
Ship a packed row's composition with the row

oflatt
and
claude
committed
1da17fb

Commits on Jul 31, 2026

Write a layer-1 composition as one row, not one per step

oflatt
and
claude
committed
e8eccfb
Carry a packed row's skeleton in the row, not in its name

oflatt
and
claude
committed
e1e00ec
Hold a deferred group as its statements, nothing else

oflatt
and
claude
committed
7fcf5ce
Hold both kinds of deferred proof in one map

oflatt
and
claude
committed
83f1f08
Walk a rule head once per firing, not once per proof read out of it

oflatt
and
claude
committed
a7c690d
Take a row's bridges one at a time, rather than by position

oflatt
and
claude
committed
91d8908
Chain every rule proof row of a head, not only the composing ones

oflatt
and
claude
committed
8ecac21
Lay a head out once, with its plan, not once per proof read out of it

oflatt
and
claude
committed
1422480
Check the invariants three comments claim and nothing enforced

oflatt
and
claude
committed
a32cad1
Reflexivize a premise through the shared builders, not around them

oflatt
and
claude
committed
9eec432
Stop reserving a head column nothing ever fills

oflatt
and
claude
committed
1e48126
State a rebuild row's shape once, so the test round-trips the encoder's

oflatt
and
claude
committed
230920e
Hold a composition and its layout in one tree, not two

oflatt
and
claude
committed
e4aa665
Describe each proof constructor once, for both readers of it

oflatt
and
claude
committed
95e08a8
Delete what nothing reads, and dedupe what two places matched

oflatt
and
claude
committed
aaca9ae
Say each of the new docs' facts in one place

oflatt
and
claude
committed
75251d4
Say what proof mode costs a user, not how it is built

oflatt
and
claude
committed
5cc4dc1
Clear every @UF table at the end of each maintenance run

oflatt
and
claude
committed
e15c13b
Measure the encoding's rebuild and search cost; make the @UF clear opt-in

oflatt
and
claude
committed
f498e73

Commits on Aug 1, 2026