Repository navigation
C1: SizeExpr/CostExpr authority in v2.lens.cost - #7879
Merged
Merged
Conversation
This reverts commit 613ecd3.
Deliver the lane-brief design note with promoted type shapes, SymbolicCost projection rules, countable CostRefused causes, and the blocking-wall witness roster. Revert the premature expr.dag carrier until C0(b) merges. Co-authored-by: Cursor <cursoragent@cursor.com>
Record 22/22 PASS claim_batch baseline for the blocking cost wall roster, interim SizeVariable grounding with dissolution trigger, C2 Certainty constraint, and accurate execution-environment finding (/usr/local/bin/gunbc parse failure on clean main; worktree claim_batch green). Co-authored-by: Cursor <cursoragent@cursor.com>
|
Bugbot is not enabled for your account, so this pull request was not reviewed. Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs. |
gunbai-bot
Bot
force-pushed
the
session/quick-koi-569
branch
from
August 6, 2026 01:14
0d819a0 to
ba62cec
Compare
8 of 9 tasks
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 6, 2026
Add v2.lens.cost.expr with grounded SizeExpr/CostExpr coproducts, normalize_cost_expr_to_symbolic projection, closed CostExprRefusalCause, and bounded_summation_test witnesses. Sync design note post-carrier. cost_lens/symbolic_cost_fold unchanged. Stacked on main after #7879 design note merge. Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 6, 2026
Add v2.lens.cost.expr with grounded SizeExpr/CostExpr coproducts, normalize_cost_expr_to_symbolic projection, closed CostExprRefusalCause, and bounded_summation_test witnesses. Sync design note post-carrier. cost_lens/symbolic_cost_fold unchanged. Stacked on main after #7879 design note merge. Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 6, 2026
Add v2.lens.cost.expr with grounded SizeExpr/CostExpr coproducts, normalize_cost_expr_to_symbolic projection, closed CostExprRefusalCause, and bounded_summation_test witnesses. Sync design note post-carrier. cost_lens/symbolic_cost_fold unchanged. Stacked on main after #7879 design note merge. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 6, 2026
* WIP: C1: SizeExpr/CostExpr authority in v2.lens.cost * C1: SizeExpr/CostExpr carrier and discriminating witnesses Add v2.lens.cost.expr with grounded SizeExpr/CostExpr coproducts, normalize_cost_expr_to_symbolic projection, closed CostExprRefusalCause, and bounded_summation_test witnesses. Sync design note post-carrier. cost_lens/symbolic_cost_fold unchanged. Stacked on main after #7879 design note merge. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: C1: SizeExpr/CostExpr authority in v2.lens.cost * WIP: C1: SizeExpr/CostExpr authority in v2.lens.cost * C1: refuse degenerate log bases; drop uninhabited EffectModelAbsent Add InvalidLogBase to CostExprRefusalCause (bases 0 and 1 fail-closed); valid base 2 still projects to LogCost. Delete EffectModelAbsent — only UnmodeledEffect is produced. Add expr_refusal_test witnesses. Sync design note to symbol-based candidate/delivered status. Co-authored-by: Cursor <cursoragent@cursor.com> * C1: record post-carrier 22/22 baseline receipt on final head Re-executed blocking-wall roster plus carrier witnesses at 9c15327; fix budget_roster entry path in the design note table. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: C1: SizeExpr/CostExpr authority in v2.lens.cost * C1: inline degenerate log-base check via nat_lte Drop hand-rolled log_base_is_degenerate; refuse bases 0 and 1 with v2.std.nat.nat_lte against Succ{Zero} per review 49372. Co-authored-by: Cursor <cursoragent@cursor.com> * C1: roster cost_loop_expr non-fold residue site non_fold_residue_no_unrostered_or_stale failed with unrostered=1 stale=0 at src/v2/lens/cost/expr.dag::cost_loop_expr (zero-body CostExpr fold). Co-authored-by: Cursor <cursoragent@cursor.com> * Fix NFR reason string: avoid brace interpolation on Zero nfr_reason_cost_loop_zero_body_fold used CostConst{Zero} in prose; frontier re-eval treats braces as interpolation and failed with undefined variable Zero. Co-authored-by: Cursor <cursoragent@cursor.com> * C1: route log/effect refusals through CostRefused wrapper Align normalize_cost_expr_to_symbolic with design §4: degenerate log bases, ungrounded log arguments, and CostEffect delegate to the CostRefused arm instead of emitting UnknownCost directly. Co-authored-by: Cursor <cursoragent@cursor.com> * C1: cite CI floor acceptance instead of stale local receipt The design note no longer claims post-carrier baseline at a pre-final commit or "CI floor pending"; acceptance is the green PR ci check on the merge head, with local claim_batch runs labelled authoring history. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.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.
Summary
C1 design deliverable (no carrier until C0(b) lands and operator signals): grounded
SizeExpr/CostExprauthority design with executed baseline receipt.Design:
docs/plans/c1-cost-expr-authority-design.mdExecuted baseline (22/22 PASS)
./target/release/claim_batchon worktree atc71592487— all blocking-wall witnesses green:src/v2/lens/cost/*modules (22 functions including copied_port suite)budget_roster_completeness_test(BoundConsumerWitness)Key decisions
SizeVariable; dissolves whenCostSubject.input: ValueIdentitylandsCostRefused { cause: CostExprRefusalCause }closed coproduct (countable, not free text)Certaintyconstraint recorded: must reconcileDescentEvidence+Measured, never a third vocabularycost_lens/symbolic_cost_foldunchanged in C1llvm_instruction_coststays registered underv2.lens.costExecution environment finding
/usr/local/bin/gunbc run --claim-runfails on clean main withexpected RBrace, found Dotatcost.dag:69— PATH install cannot parse current.dagsyntax. Worktreeclaim_batchpasses. Not a tree defect.Test plan
claim_batchbaseline roster: 22/22 PASS (documented in design §6)