Proj aware join - #149
Open
Adam-Vandervorst wants to merge 9 commits into
Open
Conversation
A body variable that no template reads and that the body mentions once is invisible downstream: every value past the first re-derives an answer byte-for-byte, which the trie then dedups. Both engines stop at the first witness. space.rs computes the mask once per transform and marks a variable only inside its conjunct's TRAILING run -- anything after it in the same conjunct draws its values from the subtrie the choice selects, so cutting there would drop answers rather than duplicates. The walk is allocation-free and does not read the templates at all unless the body leaves a candidate a template could disqualify. Only the plain `,` -> `,` write form cuts. The cut drops DUPLICATE answers, which is invisible only to a sink idempotent in them, and the `O` form and the source/sink transforms can carry Count, Sum, And, Head/Tail and the float reductions, whose result is a function of how many answers arrive. Leapfrog takes the cut on its own path, chosen once per level before any loop, so fill_lead_candidates and consume_lead keep the exact code they had; if the single witness does not match, the level re-runs as a full enumeration, so the cut can only drop a duplicate. The ProductZipper descends the first complete subterm instead of enumerating every variable, size class and arity below the position; on a factor's trailing variable that descent also crosses the factor boundary, force-enrolling the next factor. Every other query entry keeps its signature and passes a zero mask. Replayed onto main rather than rebased commit-by-commit: main has since merged #146, which already moved the subterm walk into mork-expr (so this uses upstream's subterm_parse_step rather than adding another), deleted first_subterm, and rewrote Bindings and the candidate handling underneath consume_lead. Thirteen compounding merges would have been far more error-prone than re-applying the net change to the current shapes. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The decomposition, crafting, LTS and process-calculus programs were committed with their generated fact data -- 78k lines. generate.py now produces all of them, carrying only the rule text, and the directory is 32K. Numbers move on this base: with #146 merged the naive process calculus runs 4.7x faster than it did pre-rebase, so the incrementalization uplift on an 800-long cascade reads 4.4x (delta) and 7.0x (consuming) rather than 19.7x and 30.2x. The transforms still remove the same quadratic; the baseline they are removing it from got faster. The other families are unchanged: cyc 26x/28x, craft 6.7x/14.6x, clq 0.9x/7.1x. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
walking every expression twice `byte_item` masks an arity, a symbol size and a variable index with 0b0011_1111, so all three are already below 64. Testing `r < 64` before using a VarRef, or clamping an arity with `.min(64)`, cost a branch and -- much worse -- read as though a larger value were possible. Those guards are gone; where the bound matters it is a debug_assert naming the reason. The variable cap is handled once rather than per access: the encoding caps a routable body at 63 variables and a mask cannot name what it cannot index, so a body past the cap opts out entirely and returns a zero mask. That is conservative -- a zero mask is the unchanged enumeration -- and it replaces a bounds check on every NewVar. The test pins both halves: past the cap nothing is marked, at the cap marking is normal. `span()` is itself a full walk of the expression, so calling it and then walking the bytes did the work twice, once for the body and once per template. Both walks now run straight off the pointer and stop when the subterm parse closes. And the ground stamps do the rest: a template carrying a nonzero stamp is ground by the stamp's contract, so it holds no variable and is skipped without being walked at all. That needs the templates as ExprEnv rather than Expr, which is what the call site already had -- it was flattening them to Expr and discarding the stamps. Together these take the analysis to parity with not running it. counter_machine, median of four alignment-varied rounds: 206ms with the analysis stubbed out, 216ms before this change, 205ms after. bfc, transitive and tile_puzzle_states are unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
`vs!` is the only place the walk learns a candidate is non-ground, and the cut goes around it: descend_first_subterm took the leftmost path and passed var_facts through untouched. A leftmost subterm can very well carry a variable -- an arity byte sorts below a symbol byte, so a compound like `(f $z)` is exactly what gets picked -- and the leaf then read that fact as ground and handed it to stamp_ground, whose SAFETY note is explicit that a false stamp makes consumers settle by memcmp and skip variable hunts over the span. descend_first_subterm now ORs in the bit of every factor it finds a variable in, at item heads only so a symbol's payload cannot be read as a tag. The invariant is self-checking from now on: in debug builds the leaf re-derives groundness by walking the fact's span before stamping, and panics if the bit disagreed. That discriminates -- with the tracking removed it fires on differential/corpus/programs/projection_cut.mm2, which had been reaching the bug all along without the wrong stamp changing any visible answer. Both runners could compare stale output. Neither cleared its target nor checked the exit status, so a crashed or timed-out run left the PREVIOUS run's space in place and the comparison passed on it. Both now remove the file first and require a zero exit; the fuzzer reports a cut build that fails rather than crediting it with the speed-up. And the explanations at the places called out were too long, and in one case wrong: the mask's doc claimed every bound in it was structural, when the variable cap is a real bound with a real early exit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The harness ran the baseline then the variant for every pair. Over a benchmark that takes tens of seconds, drift across the pair is monotonic, so whichever runs second is charged for it -- a systematic bias, not noise that averages out. Each program is now timed twice, on either side of the other, and the best of each is kept. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A self-join over one relation needs BOTH deltas: new receivers against every message, and every receiver against new messages. The lowering had only the second, so a communication that derives a RECEIVER never reacted with a message already in the soup -- it was incomplete, not just slower. The cascade I measured hid it: every body it derives is a message, so the missing arm never had anything to do. A soup where receiving yields a receiver shows it at once -- the monotone rule derives (! deep ok) and the one-armed delta does not. Both arms now run, alternated by the same IC controller process_calculus_bench uses for its own two rules, and the corpus program carries a soup that catches the difference. Getting it to catch took three tries, which is worth recording: the delta only loses an answer when the message has already been RETIRED from the worklist, so the shape needs an early consumer to retire (! r1 q1) in the first round and a late-derived receiver that then has to find it in the full relation. Seeded-and-never-matched, or derived-while-still-pending, and the one-armed version passes by luck. Verified by removing arm 0: pD loses exactly (! deep ok). Also: `min(...) if (bn1 or bn2) else None` in the bench harness read a genuine 0 ms as failure. Only None is failure. And `mork test` gains projection_cut_variables, covering what the cut must take (a trailing don't-care with fan-out, a schematic witness) and what it must refuse (a non-trailing one, the same nested, and a repeated variable that is a join variable). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
It was a hardcoded `pub static ACT_PATH = "/dev/shm/"`, so every ACT test failed off Linux: macOS has no /dev/shm, and `mork test` died at the first backup_tree with a bare NotFound. `act_path()` now reads the ACT_PATH environment variable, and otherwise takes the best temporary location the platform offers: /dev/shm on Linux when it is mounted, since a tmpfs keeps an ACT out of the disk, and the OS temp directory elsewhere -- TMPDIR on macOS, which launchd always sets per-user, and TEMP/TMP on Windows. The separator is appended if missing and the directory is created if absent, so pointing ACT_PATH at a fresh path just works. Verified on macOS three ways: the default writes to $TMPDIR (/var/folders/../T/two_bipolar_equal_crossed.act), an explicit ACT_PATH is honoured, and a non-existent one is created. This does not make `mork test` pass here. It now reaches a hash assertion that expects (result XoicVnQv2bk) and gets (result -Egab4rQ3Nc). That failure is main's, not this branch's: main with its constant repointed at a real directory fails at the same test with the same two values. Left alone. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The expectation predated #146, which made the hasher compile: the constants came from whatever was silently used while the `gxhash` cfg never matched. With gxhash 3.x running, `(myexpr ..)` hashes to -Egab4rQ3Nc and ru8oOBGFlq0. Portable, contrary to what I said last round: gxhash documents its hashes as stable across every supported platform for a given major version, so this is not pinned to this machine's ISA. It is pinned to gxhash 3.x, and a major bump will move it again. With this, `mork test` passes end to end on both engines -- and the same constant makes main pass too, which is how I know the value is the hasher's and not this branch's. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The query-side rule -- mentioned once, unread, trailing -- says nothing about the DATA sharing a variable across the columns it names. Facts like (f $x A $x) tie the don't-care column to the column a template reads, so the audit asked whether $a still iterates over A and B under (, (f $a $a $_)). It does, on both engines, and the reason is structural rather than lucky: the discriminating information lives in the REPEATED column, which is a trie prefix of the don't-care column, so it is enumerated before the cut ever applies. More generally a bare fresh singleton is an unconstrained position: the binding it takes is read by nothing and constrains nothing else, so the choice cannot propagate. What could still discriminate is a later query position drawing from the subtrie the choice selected, and that is precisely what the trailing condition excludes. Eight aliasing shapes are pinned, expected generated from a NO-CUT build so the cut is measured against the semantics it must preserve -- including the middle-position case, which must not be cut at all. Non-vacuous, checked by the unifications counter: over 400 facts sharing an aliased prefix and differing at the don't-care column, the cut takes 400 unifications to 1 with the same single answer; over 400 facts differing at the REPEATED column it takes 400 to 400, collapsing nothing, which is the audited case at scale. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
|
(Unsound as currently presented by 590b08c ) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Skip trie subtrees when no mentions in then are needed.