corgi backend: runtime parity (executable, capability fallbacks, worker guard) - #811
Merged
frankmcsherry merged 8 commits intoJul 30, 2026
Conversation
…pile Backend::join gated its projection nowhere: a program with Case/List/Unary/ Hash inside a join's projection panicked on corgi and worked on vec — the one place capability (not just speed) depended on the lowering's coverage. The join now takes the same shape as linear's gate: when the projection is not compilable, join with the identity projection (Var(0); (Var(1), Var(2)) — compilable by construction) and apply the original terms as a row-wise Project, rebased from the join env [/bin/zsh=key, =lv, =rv] onto the row env [/bin/zsh=key, =(lv, rv)]. The join_fallback gate program puts a unary negation reading both sides in a join projection (verified to drive the fallback path) and asserts agreement with the vec backend; the gate grows to seven programs. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Neg is corgi's wrapping negate on the raw bits (exactly -as_int()); Not compares scalars against zero and constant-folds non-Int truthiness to 1 (the cross-shape Eq precedent); Len is the static shape arity for tuples and an acc+1 Fold along each row's list. compilable admits the three; the fallback list shrinks to Case/Inject/IsTag, List intro, and Hash — the last now documented as the one true kernel gap (splitmix64 parity needs lane-wise xor and integer rem corgi does not yet have). The new scalar_ops gate program tripped a pre-existing divergence: ordered compares ran unsigned over raw two's-complement bits, so any negative operand disagreed with vec's signed semantics. Lt/Le/Gt/Ge now route both operands through ToSigned (the order-preserving signed encoding); Eq/Ne stay raw (bit-equality is sign-safe). The non-negative-int assumption narrows to order-sensitive contexts (Min, structural sort order). scalar_ops runs verified fallback-free; join_fallback moves to hash (still unlowerable) so it keeps driving the join fallback. Gate: nine programs... eight — reach/scc/stable/unnest/adt/binders/join_fallback/scalar_ops. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Inject with a literal tag is Op::Inject (lane t of a t+1-lane sum, the below-t lanes uncommitted); a data-driven tag has no static lane count and stays row-wise. IsTag on a sum maps every committed lane to its constant answer and unwraps (uncommitted lanes need no arm); on any other shape it folds to the constant 0, matching eval's non-Variant-is-never-the-tag. infer_term_shape learns Inject's sum shape so downstream cross-shape Eq folds stay correct. NB Term::Inject's fields are (tag, payload) — the first draft had them swapped, which the shape-free gate demoted to a silent fallback rather than a miscompile; the instrumented fallback-free check is what caught it. The sum_ops gate program covers intro, committed- and uncommitted-lane tag tests, and istag-on-tuple, verified fallback-free. Gate: nine programs. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
frankmcsherry
force-pushed
the
corgi-runtime-parity
branch
from
July 30, 2026 17:42
87cf2d1 to
36bb671
Compare
compile becomes Option-returning — the gate at the moment of full information. apply_ops attempts each projection/predicate with the container's shapes and falls back to rows only when the lowering declines; the syntactic compilable check remains solely the join-INLINE gate (a declined join projection defers to a linear stage, where the shape-aware gate lowers it — deferral composes, so nothing stays row-wise for gating reasons). Out-of-range env references decline rather than panic: closed bodies truncate the environment by design. Case lowers as CapSum (distribute the environment into each committed lane), MapSum (each arm a closed body over Prod([ctx, payload]) — arms see the outer env plus the payload as top binder; a default runs WITHOUT the binder, matching eval), and Unwrap (arm result shapes joined ⊥-tolerantly; genuine conflicts defer to rows). A local shape_join stands in until corgi exports its own. Fold bodies now carry aligned [init, elem] shapes, and infer_term_shape learns Bound, Case, and joined If shapes — If must OVER- approximate sum lanes lest a downstream Case leave runtime rows unmapped. One engine caveat: Select over sums that commit different lanes trips an offset bug in the pinned rev's lane merge, so sum-shaped If results defer to rows until the next corgi pin bump. The case_ops gate program covers the compiled arm+default path (verified), the shape-clash decline (verified, via a filter so the program stays vec-valid), and dead compile_term_single is removed. Gate: ten programs. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
render_tree_rows is the corgi substrate's row-boundary entry point: imports convert to corgi containers (ToCorgi), the tree renders columnar, exports convert back (FromCorgi) — signature-compatible with vec::render_tree, so a row-speaking driver switches backends by switching one call. evaluate now routes through it (the conversion dance lived there twice). ddir_vec becomes ddir with --backend=vec|corgi (default vec): the corgi backend is now runnable on every program the vec runtime runs — file inputs, synthesized rounds, --explain, --diag — not only the test gate. Smoke: scc 1k/2k, 100 update rounds on both backends. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The corgi arrange is Pipeline (no key exchange), so multi-worker execution would mis-place keys — silently wrong, not slow; the vec backend's arrange_by_key exchanges and has no such constraint. Assert one worker until a columnar exchange (radix partition by key hash) exists — that work pairs naturally with the stored-hash-column direction. Verified to fire under -w2. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
frankmcsherry
marked this pull request as ready for review
July 30, 2026 18:11
The per-feature programs (join_fallback, scalar_ops, sum_ops, case_ops) are test fixtures, not examples — contrived shapes whose comments discuss fallback routing — and now live under tests/programs/ beside the gate that owns them. The algorithm programs stay in examples/, where they honestly double as demos. tour.ddp is the complement, not a replacement: one program composing the constructs — scalars, sums with case/istag, lists with fold/len and the flatmap/collect round trip, all four reducers, iteration with concat — as the grammar's worked example and the gate's integration check. The pinned- path fixtures localize failures and keep verifiable fallback counts (a mixed term tree rows atomically, so a tour alone would silently shift coverage to the row path); the tour covers what they deliberately avoid, construct INTERACTIONS. Gate: eleven programs. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
frankmcsherry
force-pushed
the
corgi-runtime-parity
branch
from
July 30, 2026 18:37
b9d4c2d to
0b95eb0
Compare
Tuple keys ((group, index) and friends) previously took the structural last-resort: a symmetric compare_at walk of BOTH sides, every unit — per-row structural dispatch, cost tracking the trace rather than the delta, and the super-linear round times the 250k scc-compound measurement showed. But neither dumbness is forced by tuple-ness: only the resumable-block bookmark truly needs a single-u64 key. advance_lanes pulls every key lane as u64 buffers and walks them with lexicographic machine compares, with the single-lane path's two regimes: a much smaller side drives and the other is probed wholesale (find_ranges with a gather_lanes-built tuple needle column — shape-generic), or comparable sides merge symmetrically. Ordinal group tokens, one block (the bookmark question defers to a digest scheme; the walk, not the blocking, is what scales). The structural walk remains only for keys that do not flatten to integer lanes at all (sums/lists in the key) — and fires zero times across the gate. The pair_keys fixture (composite keys with overlap, fanout, and one-sided keys) pins the path — verified routed to advance_lanes. Gate: twelve. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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
1 participant
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.
Follow-on to #795, closing the gaps between "a corgi backend" and "a corgi runtime as capable as vec" — from the pre-merge completeness audit. All items landed:
80897fd1):Backend::joincompiled its projection ungated — aCase/List/Unary/Hashin a join projection panicked on corgi, worked on vec. Non-compilable projections now defer: identity join + a followingProject, terms rebased onto the row env. Verified to drive the fallback path.1d8a90a6,36bb6710,6c010ce2):Neg/Not/Len; literal-tagInjectandIsTag;CaseviaCapSum/MapSum/Unwrapwitheval's exact binder discipline.compileis nowOption-returning — the shape-aware gate at the moment of full information — withcompilablesurviving only as the join-inline gate (deferral composes). Bonus fix the new gate programs flushed out: ordered compares ran unsigned over two's-complement bits;Lt/Le/Gt/Genow route throughToSignedand agree with vec on negatives.90706ea1):ddir_vecbecomesddir --backend=vec|corgi— the corgi backend runs every program the vec runtime runs (file inputs, rounds,--explain,--diag).render_tree_rowsis the row-boundary corgi render, signature-compatible withvec::render_tree.d5b5a920): corgi's arrange isPipeline(no exchange), so multi-worker would mis-place keys silently; asserted single-worker until a columnar exchange exists.Gate: ten programs (was six), all verified for compiled-vs-fallback path routing, green in debug (harness asserts live) and release.
Deferred, recorded:
Listintro andHashneed corgi-side kernels (ListIntro; lane-wise xor + integer rem for splitmix parity); the pinned engine'sSelect-over-sums lane merge has an offset bug, so sum-shapedIfresults defer to rows until a pin bump. The server's trace registry stays vec-typed — making it backend-generic is its own follow-up.🤖 Generated with Claude Code