Repository navigation
Floor cost-debt edit judgment: one lex per changed file, shared by every identity in it - #12915
Closed
gunbai-bot[bot] wants to merge 2 commits into
Closed
gunbai-bot[bot] wants to merge 2 commits into
gunbai-bot[bot] wants to merge 2 commits into
Conversation
…ery identity in it v2.workflow.floor_cost_debt_edit judged each changed cost-debt witness in its own call, and each call lexed the whole base and head file, so a file with k changed witnesses paid 2k lexes. With two changed witnesses in the 125 KB emit_test.dag, site projection ran past the floor's 90-minute cap (run 36856989404). The wet entry is now cost_debt_changed_witness_ceilings_at_base, called once per file with every changed cost-debt function in it. It lexes base and head once, reads the base resolution once, and selects each declaration from those streams. The host prints `[floor-cost-debt-edit] judgments= changed_identities=` as the control. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Consolidated into integration PR #12951 at the operator's request; this branch is merged there unchanged in its own merge commit. Closing here; the branch is kept. — sent from deep-ferret-305 |
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Oct 3, 2026
…13000's per-file sharing replaces #12915's #12915 and #13000 both share one lex per changed file across its witnesses. Two mechanisms for one fact is a fork, so main's #13000 stands whole: its floor_cost_debt_edit .dag, test and host code. #12915's plural entry, its counters and its [floor-cost-debt-edit] judgments line are dropped; with main's increments gone they would print 0. Co-Authored-By: Claude Opus 5.5 (1M context) <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
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.
Operator ruling from deep-ferret-305 (2026-10-01): a proven cost-shape defect (DESIGN §6) is always fixed.
Defect
v2.workflow.floor_cost_debt_editjudged each changed cost-debt witness in its own call. Every call lexed the whole base file and the whole head file, so a file with k changed witnesses paid 2k lexes of the same two sources. On #12905, two changed witnesses in the 125 KBdag/test/claim/live_deploy/emit_test.dagheld site projection from 12:03 past the 90-minute cancellation (run 36856989404). A green run finishes site projection in 65 s.Change
.dag:cost_debt_changed_witness_ceilings_at_basereplaces the single-function entry. It takes every changed cost-debt function of one file and returns ceilings aligned with that input.cost_debt_edits_from_sourceslexes base and head once (FileReading) and reads the base resolution once. It selects each function's declaration from those two token streams with the existingcost_debt_edit_decl_tokens; no text search.cost_debt_edit_from_sourcesthe witnesses use is now the same decision over a one-element list.required_floor_runnercalls the entry once per file, before that file's identities are classified. Each identity reads its ceiling from that per-file result.[floor-cost-debt-edit] judgments=<files> changed_identities=<n>must show judgments equal to changed files, not identities.Measured on the same subject
Locally,
claim_batch --wet, baseorigin/mainagainst head #12912 (the two changed sudoers claims), arm64 container:Both labels match the floor's own receipt:
rejudged_as_new_witness cause=edit_is_not_a_conjunct_removal.This halves the cost but does not get back near 65 s. One lex of this file is itself quadratic. That cause is located (
v1_interpretermatch_patternbuilds a native list's Cons tail eagerly) and is fixed in a follow-up PR, with parent approval.Evidence
v2.test.floor_cost_debt_edit: all 15 existing witnesses PASS locally (claim_batch --hermetic).one_lex_pair_judges_each_function_of_the_file_in_order: three functions, three different arms, judged against one lex pair and answered in input order. It passes; a misaligned answer would fail it.cargo check -p v1-compiler --libpasses (remote).🤖 Generated with Claude Code