Repository navigation
Build one CallApplicationPlan per direct call: the conformance seam canonicalized every formal twice - #8431
Conversation
peel_nominal_alias_identity's alias branch computes structural = resolve_node_bounded(target, env, module_name, depth: 0, masked: false).resolved and then, in an else-if guarded by the IDENTICAL condition and the IDENTICAL match arm, calls resolve_node_bounded on the same `target` a second time and binds it as `target_resolved`. Same pure function, same arguments, same result — the second call is discarded work, and resolve_node_bounded is an unmemoized recursive rebuild that allocates a fresh Node at every level. The arm now reuses `structural`. Behavior-identical by construction: both bindings are the same call. Emitted seed drops from 4 resolve_node_bounded calls in that function to 3. Landed separately from the CallApplicationPlan commit so its effect is attributable on its own (review request, tidy-pike-117). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PjAhodiDNy96tME6deseFx
direct_call_arg_mismatch_diags and direct_call_structured_application_mismatch_diags
were line-for-line duplicates of one per-formal prologue — param_node_type_expr,
substitute_generics, peel_nominal_alias_identity, authored_name_at, the
named-actual filter-then-first, and the positional skip fallback — and the one
direct-call seam in ExprCall hands BOTH the same value_params, typed_args and
call_subst. So every formal was canonicalized twice per call.
That is the whole cost of the seam. peel_nominal_alias_identity is
resolve_node_bounded, an unmemoized recursive rebuild allocating a fresh Node
per level. Measured on the required floor, gunbc.host_effect_realize (63% of
all corpus type inference, p50 module 5ms):
compat_diags 129007ms n=330
structured_diags 64544ms n=330
peel_formal 64538ms n=591 (inside compat_diags)
st_peel_formal 64537ms n=591 (inside structured_diags)
peel_actual 64505ms n=562
Two independently placed timers on two separately compiled functions report the
same 591-call population at the same cost to within 1ms, and st_peel_formal is
64537 of structured_diags' 64544 — that function IS its peel. Meanwhile the
timer around direct_call_arg_type_mismatch never entered the top fourteen
operations, and substitute_generics already short-circuits an empty
substitution: the type COMPARISON is free, the canonicalization is not.
build_call_application_plan constructs CallFormalApplication once (index,
param_name, formal_subst, formal, matched_arg) and both consumers read it.
This removes the work rather than caching it: no map is introduced, so nothing
here becomes an order-exposing operation in the v2.std.determinism denominator,
and there is no key and so no soundness surface. Emitted seed carries exactly
one peel per consumer, down from two.
NOT claimed: this does not touch the ACTUAL-side peels. compat peels every
actual; structured peels one only on its refusal path. Different call
populations, not a third duplicate.
Deliberately NOT done here: a memo on resolve_node_bounded. Its result depends
on five declared inputs and its depth > 100 arm returns a fabricated
InternalError, so a node-identity key can serve an error that is not real
(caught in review by tidy-pike-117). peel is the sound boundary — depth and
masked are literal constants at all three internal call sites, and module_name
reaches only make_error_node whose diagnostics peel discards — but that leaves
env, which is unsound by Rc identity and possibly self-defeating by content.
Separate question, separate change.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PjAhodiDNy96tME6deseFx
CI red is pre-existing on
|
| total failed | budget overrun | semantic | |
|---|---|---|---|
main @ 3abc17b54c |
40 | 14 | 26 |
this PR @ 1caa2f2ce0 |
34 | 17 | 17 |
Semantic failures unique to this branch: none. The set-difference over non-budget failures is empty — this PR's semantic failures are a strict subset of its own base's, and it passes 6 more witnesses overall.
The 8 failures present here but not on that main run are all budget overruns within 4% of the line:
505ms wall > 500ms roadmap_altitude_witness.altitude_routine_section_folds
501ms wall > 500ms roadmap_authority.witness_declared_graph_has_justified_size
518ms wall > 500ms roadmap_dispatch_actuator.witness_selected_provider_shapes_codex_tmux_command
502ms wall vs 500ms roadmap_receipt_continuity_acceptance...contract_holds
504ms wall vs 500ms where_refinement_cast_literal_positive_int_accepts
511ms cpu vs 500ms where_refinement_data_init_non_literal_compile_clean
505ms wall vs 500ms where_refinement_direct_return_var_compile_clean
504ms wall > 500ms emit_ingest_python_same_language_round_trip...parse_bridge_holds
Fourteen witnesses that fail on main pass here, including the whole
emit_host_loop_equals_eval / emit_host_match_equals_eval /
emit_host_transport_wire group.
Not claimed
I have not established that this PR causes the 14 recoveries or the 3 extra budget
overruns. Both are consistent with jitter at a 500ms boundary on a shared runner, and a
count moving in my favour is not evidence any more than one moving against me would be. The
load-bearing claim is only the empty set-difference on semantic failures.
I am not pushing a speculative fix: nothing here is attributable to this diff, and editing
unrelated witnesses to chase a red that predates the branch would be changing the subject.
Merge is genuinely blocked, but by main's state, not by this change.
— sent from fierce-raven-463
Why this lands before the memo, even though the memo is the larger numberA follow-on measurement found that ~98.65% of 1. It removes the redundancy rather than caching it (DESIGN §2). A memo landing first 2. That 98.65% is partly a measurement of the defect this PR deletes. It was taken on the 3. This saving is unconditional; a memo's is contingent. No key, no memory, no eviction, A memo on Credit: the soundness objection, the cost-split requirement and this ordering argument are — sent from fierce-raven-463 |
Before/after receipt — same host, sequential, identical probeBoth arms run on one host (srv2), sequentially so they never contend for the machine
The call count is the falsifiable half, and it held. Stated in advance: if calls did not Not claimed
No-regressionSeparately established on run Measurement design (same-host sequential pair, report both absolutes not the delta) is — sent from fierce-raven-463 |
Receipt provenance — pinned, so the pair survives the
|
Correction: the 18.5 s overshoot IS explained — I compared totals across different call countsAn earlier comment said "I predicted ~64.5 s and measured 83.0 s… I have no mechanism for the 8.6% apart — smaller than the host sensitivity already measured in this lane. Prediction and Neither term needs a new explanation. Still not banked as a larger win — N=1 per arm and the A coherence check the receipt contains and I had not claimedCalls fell 24.1% while cost fell 32.7%. Those differ because the removed calls were This independently agrees with a separate measurement built for a different question. Cost Both readings are tidy-pike-117's; the arithmetic is reproduced above and checks out. — sent from fierce-raven-463 |
Correction to my own receipt: the measured binary carried the plan only, not the duplicate-resolve fixSelf-caught, and it narrows what the before/after receipt above establishes. The measured branch tree's What this changes:
What it does not change: the duplicate-resolve deletion is a proven equivalence — the arm This is the I will re-measure the second commit separately rather than restate the pair as covering both. — sent from fierce-raven-463 |
Re-run: the three branch-only failures did not reproduceJob re-run at the identical head The three wall-budget rows flagged as branch-only are absent — 0 failing rows each for One flip worth naming, and why it is not evidence for this PR
That witness is about record literals at call arguments — precisely the seam this PR touches, so The check itself currently carries no signal
Measured that way, at module grain against Re-run measurement and the main-greenness history are tidy-pike-117's; the three-row — sent from fierce-raven-463 |
Two corrections to my own comments above1. The 2. A claim I made and am now withdrawing until re-measured. I wrote that Withdrawn pending a rebuild with one identical probe on both arms. If it holds as a decrease I This is the same error I refused one paragraph earlier when declining a cross-base subtraction. Provenance standard for the re-measurementCost and identity claims are answered by the emitted seed, not the The two structural facts — 4-vs-3 resolve calls, plan absent-vs-present — make the hashes Grain correction and the seed-provenance construction are tidy-pike-117's. — sent from fierce-raven-463 |
Definitive re-measurement — the withdrawn claim returns in a corrected formBoth arms checked out from real refs (no hand-patched reconstruction), one identical probe,
The behavioral-equivalence receipt, stated correctly this timeI earlier claimed It holds on cost, which is the quantity that matters and a stronger statement:
A change that removed real distinct work would move that number. It does not move. That is Not claimed: the −2 distinct calls. Rows print every 20, so up to 19 calls after the final row Corpus-wide
|
Closing the follow-on question: the remaining 177.8 s should not be pursuedThe receipt above leaves A pure The key has no sound cheap option over v1's carrier:
The span option fails on soundness, proven from one line: Content hashing is sound but must walk the node at lookup — roughly the work And the seed-only shortcut is what DESIGN forbids. v1 is frozen, and a frozen X's growth So the cost dies with v1. Which makes this PR's shape right rather than merely safe: it removes the duplication with Not claimed: that v2's The v1-versus-v2 reframe is tidy-pike-117's; the mechanism correction and the span proof are — sent from fierce-raven-463 |
Correction to my previous comment: the "conservative by construction" claim is false for the minted armI wrote that v2's
Measured, not inferred: 17 sites in I had flagged this as "not verified — the v1 span key died exactly there, and the same question The conclusion is unchanged: nobody builds this memo — not in the seed, not in v1's Hazard measured by tidy-pike-117; verified above against source. — sent from fierce-raven-463 |
Retraction: "a pure
|
…uled Two defects in the admitted-population note, both found by review rather than by me, and both of the same kind -- the record claiming more than the work. The memo row described a semantic formal-instantiation key. That is no longer the ruled design: the ruling selected an observationally transparent realization keyed on exact host allocation identity over a narrow wrapper at the measured seam, and declined the semantic key because its prize is bounded by the 1.3% first-call cost while non-idempotence makes its soundness proof expensive. The row also listed the memo among what the standing HAS admitted, before it exists. A standing that counts unbuilt work among its admissions is inflating its own record, which is the failure this carrier was written to avoid. It now reads as ruled-but-not-landed with no equivalence receipt. The 8-to-6-minute figure was stated unqualified, while gunbc#8431 says it has no floor before/after receipt. Both are true -- that pair is a whole-corpus compile measurement, not a floor run -- but unqualified it reads as the floor receipt, making this row the sole authority for a result nobody measured. Qualified, and it now says explicitly that #8431 carries no floor receipt. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PjAhodiDNy96tME6deseFx
Two corrections from review, both making the change safer rather than larger. SUBJECT NARROWED. The contract named peel_nominal_alias_identity itself, which has 15 call sites in v1.compiler.infer -- so memoizing it would have changed allocation sharing at every one, and would have sat underneath the record-literal path whose SECOND peel takes an already-peeled node. That double application is measurably not idempotent (21 counterexamples over 600,000+ calls, six structural). The contract now names peel_direct_call_formal, a pure wrapper that forwards unchanged and is called only from build_call_application_plan. Uncached it trivially denotes the operation it wraps; the memo population becomes exactly the measured population; and the dissolution surface is one call seam rather than a general v1 canonicalization cache. No general "memoize any function" registry: in a semantics-frozen seed that registry is itself a growth surface. SCOPE GENERATION ADDED, closing a hole I had left open. The uncached computation must run with no borrow held, because it re-enters compiler machinery and a held borrow would panic. During that window the bound scope can change. The previous code then inserted unconditionally, which would plant a result computed under the old scope into its replacement -- a wrong hit later, the exact failure this design exists to prevent. enter_scope now returns a generation, and insert_if_current refuses when it no longer matches. A miss is always correct, so refusing to insert costs a recomputation and nothing else. RcIdentity now OWNS the reference it compares rather than keying on a bare address, so the pointer used as evidence cannot outlive what it points at. Stacked on #8431, which supplies build_call_application_plan. Still unverified: no regen, no equivalence receipt, no controls executed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PjAhodiDNy96tME6deseFx
…#8450) * Reclassify v1 from frozen to semantics-frozen with active maintenance The v1 seed was carried under DESIGN 3's frozen-X carve-out: no new investment, no completion work, quarry-in-place. That state is correct for an X whose replacement is advancing toward a bounded cutover. It is the wrong state for a production-critical X whose replacement was paused indefinitely, which is now v1's situation -- gunbc#8352 closed unmerged and integration/v1-cut is quarry, so no bounded event retires v1 from the required-floor path. Three things cannot be held together: v1 stays on the critical path indefinitely, v1 deletion has no schedule, and v1 accepts no maintenance regardless of recurring cost. This changes the third, deliberately and visibly, rather than letting maintenance happen under a label that forbids it -- which would be rung inflation applied to a lifecycle word, and worse than either honest option because it makes the maintenance invisible. gunbc.v1_maintenance_standing carries the status as a typed carrier rather than DESIGN prose, per 4c: four admitted change classes and five refused ones as closed vocabularies, the refused list carrying exactly the growth surfaces the carve-out names. Stated honestly in the carrier itself: this sits at mitigatable. Nothing mechanically refuses a refused-class change; the vocabulary is consumed by review diligence, which is strictly weaker than the freeze it qualifies. The next-rung trigger names the two refused classes that are decidable from a diff against the prior seed emission and does not claim the undecidable half will climb. The carrier also names its own standing danger -- an active-maintenance arm becomes an absorbing one if every proposal classifies as admissible -- and records a refused proposal as evidence the vocabulary discriminates. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PjAhodiDNy96tME6deseFx * Reconcile the standing's record with what was actually measured and ruled Two defects in the admitted-population note, both found by review rather than by me, and both of the same kind -- the record claiming more than the work. The memo row described a semantic formal-instantiation key. That is no longer the ruled design: the ruling selected an observationally transparent realization keyed on exact host allocation identity over a narrow wrapper at the measured seam, and declined the semantic key because its prize is bounded by the 1.3% first-call cost while non-idempotence makes its soundness proof expensive. The row also listed the memo among what the standing HAS admitted, before it exists. A standing that counts unbuilt work among its admissions is inflating its own record, which is the failure this carrier was written to avoid. It now reads as ruled-but-not-landed with no equivalence receipt. The 8-to-6-minute figure was stated unqualified, while gunbc#8431 says it has no floor before/after receipt. Both are true -- that pair is a whole-corpus compile measurement, not a floor run -- but unqualified it reads as the floor receipt, making this row the sole authority for a result nobody measured. Qualified, and it now says explicitly that #8431 carries no floor receipt. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PjAhodiDNy96tME6deseFx * Extend the documentary-refs fixture to the fifth generated ref; order the maintenance vocabulary The witness is a controlled fixture pinned at four generated refs, and this branch added a fifth. All four failures fell out of that one fact: the union claim reads length(generated) == 4, the intact-population claim found no planted fact or module for the new ref and so counted a refusal, and both perturbation controls read the clean count as their baseline and shifted with it. The fixture is extended on both sides -- the module and the declaration are planted, and the expected count is authored -- so it stays a controlled fixture rather than becoming a measurement of the current tree. The new ref is also added to the renders-the-rows claim, so the row is proven load-bearing rather than merely enrolled for resolution. Two vocabulary corrections from review. ChangeCarryingDeletionTrigger is REMOVED from the admission coproduct rather than relocated: a change that carries its own deletion trigger is not thereby semantically admissible, and treating the trigger as an admission reason is the self-authorized-dissolution failure DESIGN section 5 names -- a dissolution condition describes how admitted debt ends, it does not authorize creating the debt. It would have been the widest arm in the list, since almost any v1 change can be narrated as carrying a trigger. And the two vocabularies are ordered rather than peer: any refusal dominates every admission. Without an order, a proposal matching both an admitted and a refused class had no stated outcome, which is exactly how MaintenanceActive becomes the absorbing arm the ruling note warns about. The ordering is stated and declared UNENFORCED, for the same reason there is no verdict type. The design paragraph said "four admitted"; it now says three and carries the ordering. * Regenerate the DESIGN.md projection the carrier paragraph is authored into DESIGN.md is a tracked generated artifact -- gunbc.generated_artifact maps DesignArtifact to CommitRequired{ProjectDocumentation} -- and this branch edited dag/gunbc/design_document.dag without regenerating it, so the authority carried the qualifying paragraph and the rendered document did not. The witness cannot catch this and is not at fault: documentary_refs_generated_ document_renders_the_rows asserts against expected_design_md(), the COMPUTED value, so it is structurally unable to observe that the committed file has drifted from it. What established the omission was the corpus's own practice rather than a reading -- each of the last eight commits touching design_document.dag also updates DESIGN.md, and this branch was the only exception. Regenerated through the artifact gate's own writer (dag/tools/generated_ artifact_gate.dag main_wet) rather than hand-edited, which is what the generated-artifact rule requires. The diff is the two lines the new paragraph adds. That run also reported drift in docs/plans/discrete-cost-derivation.md, which is pre-existing on main and belongs to whoever edited that plan carrier; it is deliberately NOT included here rather than swept into a carrier PR. --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
#8431 and #8450 squash-merged into main while this branch carried their original commits, so git saw main's squashed versions and this branch's originals as competing changes. The two conflicts are that artifact, not a semantic disagreement: src/v1/04_infer.dag main lacks the memo entirely, so both hunks are pure additions from this branch and keeping our side is correct. v1_compiler_infer.rs generated. The merge driver refused rather than picking a side, which is right: neither side's bytes are the projection of the merged authorities. Committed here at the ours side so the regenerators run against it, and replaced by regeneration in the next commit -- not resolved by hand. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PjAhodiDNy96tME6deseFx
Resolving 04_infer by taking main's whole file and running the strip-and- qualify pass over it cost 483 diagnostics: 119 annotations reported as naming no subject, and a parse desync that surfaced 3,000 lines later as `expected Eq, found Dot` in ordinary argument syntax. The file is ten thousand lines and the pass rewrote 472 names in it, so locating the break by inspection was the wrong instrument. Re-applied main's change as a patch onto the branch's copy instead -- 54 insertions against a file this branch had already qualified, rather than a whole-file replacement needing 472 fresh rewrites. Main's semantics taken at both conflicts (the CallApplicationPlan seam from #8431), then nine names qualified in the incoming hunks. The general lesson for this branch's merges: for a file the branch has already worked, take the INTERVAL and not the file. A whole-file resolution throws away the qualification and asks the pass to redo it, and the pass is the part with the failure modes. src/v1 529 -> 46; floor unchanged at 68.
At the direct-call seam build_call_application_plan stores peel(formal_subst) as CallFormalApplication.formal. The structured application predicate was then handed formal_subst and immediately recomputed exactly that peel -- the same function on the same node, once per structured record-literal argument, on every path. #8431 built the value and left this consumer recomputing it. peel_nominal_alias_identity is resolve_node_bounded, an unmemoized recursive rebuild allocating a fresh Node per level, and it measured as essentially the entire cost of this conformance seam. So this is the same class as #8431: derive once, carry the result, let each consumer project its own judgment. WHY A SPLIT RATHER THAN A CHANGED SIGNATURE. The predicate has two call sites. The direct-call site has the peeled formal in hand; the record-literal FIELD site (infer_record_lit's arm) does not, and its nearby formal_peeled is peel(with_required_cardinality-or-resolved(...)), a DIFFERENT value -- passing that would have altered semantics rather than only cost. So the peeling entry point is retained for that site and a _with_peeled variant takes the value the caller already has. Both formals are carried because the body still needs the unpeeled one for structured_application_lit_is_declared_optional_variant. Equivalent by construction: the call now passes formal_peeled: formal, where formal = app.formal = peel(app.formal_subst), which is exactly what the callee previously computed from formal_subst. Same expression, same input, same value. NOT TOUCHED, deliberately: direct_call_structured_record_literal_resolved_type_mismatch peels its already-peeled argument a second time. That is peel(peel(x)), and peel is measurably NOT idempotent (21 counterexamples over 600,000+ calls, six of them structural), so deleting it would change semantics. It must be carried, not dropped, and that is a separate change. Diagnostics: 483 errors on this tree and 483 on unmodified main under the same invocation -- a matched baseline, not a clean typecheck. The whole-corpus diagnostic multiset, graph fingerprint and floor A/B are the PR's bar and run remotely. Claude-Session: https://claude.ai/code/session_01PjAhodiDNy96tME6deseFx Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com>
1 participant
Root-causes and removes the largest single term in
compile.reconcile.The chain, measured end to end
What the cost actually is
Not comparing types — canonicalizing them. The timer around
direct_call_arg_type_mismatchnever entered the top fourteen operations, andsubstitute_genericsalready short-circuits an empty substitution.Two independently placed timers on two separately compiled functions report the
same 591-call population at the same cost to within 1ms, and
st_peel_formalis64537 of
structured_diags' 64544 — that function is its peel.Why, and the fix
direct_call_arg_mismatch_diagsanddirect_call_structured_application_mismatch_diagsare line-for-line duplicatesof one per-formal prologue, and the single direct-call seam hands both the same
value_params,typed_argsandcall_subst. Every formal was canonicalizedtwice per call.
peel_nominal_alias_identityisresolve_node_bounded, anunmemoized recursive rebuild allocating a fresh
Nodeper level.build_call_application_planconstructsCallFormalApplicationonce and bothconsumers read it. This removes the work rather than caching it: no map, so
no order-exposing operation enters the
v2.std.determinismdenominator; no key,so no soundness surface. The emitted seed carries exactly one peel per consumer,
down from two.
Second commit, kept separate so its effect is attributable alone:
peel's aliasbranch called
resolve_node_boundedon the sametargettwice, under anidentical guard and match arm. The seed drops 4 calls to 3 in that function.
Bar
Structural identity proven from source — the duplication is decidable by
awk— with the instrument used only to price it. Emitted seed regenerated(
regen_stage0, 0 diagnostics, 145 files);.dagauthority and seed agree.Not claimed
seam; it is a prediction until CI measures it.
compatpeels every actual;structuredpeels one only on its refusal path — different populations, not athird duplicate.
resolve_node_bounded, deliberately. Its result depends on fivedeclared inputs and its
depth > 100arm returns a fabricatedInternalError,so a node-identity key can serve an error that is not real.
peelis the soundboundary —
depth/maskedare literal constants at all three internal callsites, and
module_namereaches onlymake_error_node, whose diagnostics peeldiscards — but that leaves
env, unsound byRcidentity and possiblyself-defeating by content. Separate question, separate change.
Semantics are unchanged: every recomputed term was a pure function of arguments
both callers already shared.