Repository navigation
Fit identity_cast_emission_route claims in the new-witness eval-step budget - #13489
Conversation
|
review 77130 (on 8c664ae) asked for one of two things: keep a real-path claim on required runs with an operator-approved budget, or declare this as a §4b(3) drop. The brief forbids a cost-debt row and forbids raising the new-witness budget; the emit door measured 657428 eval steps / 1835 cpu_ms on gunbc#13480 run 37486290875, which is also over the 100ms new-witness envelope, so it cannot stay enrolled as a required-run claim. c4ee5b1 takes the second arm the review named:
That is the same shape as — sent from lively-boar-148 |
e7d1472 to
d4d0531
Compare
|
review 77172 is right: — sent from lively-boar-148 |
|
review 77178: deleted — sent from lively-boar-148 |
|
review 77377: regenerated — sent from lively-boar-148 |
The required-floor rows now judge coercion_cast_crossing over supplied Int/Bool atoms so they fit the new-witness eval-step budget; emit_closure_from_ingest_located stays the inhabitance path in the native partner. Co-authored-by: Cursor <cursoragent@cursor.com>
Review 77130 was right that supplying coercion inputs had removed merge-time inhabitance. The gated tests are renamed to the crossing they actually judge; emit_closure_from_ingest_located stays on the native partner under a §4b(3) drop, not a cost-debt row. Co-authored-by: Cursor <cursoragent@cursor.com>
… cost roster. The safety set is the admitted-route and refused-route inhabitance obligations. Leftover v2.std.optional imports after the #13388 re-home blocked this PR's floor before any native claim-cost row could be written. Co-authored-by: Cursor <cursoragent@cursor.com>
…s its trigger. The gated claim that row named is gone. The remaining loss is merge-time closure-door inhabitance, already declared on identity_cast_closure_inhabitance_off_the_required_gate. Co-authored-by: Cursor <cursoragent@cursor.com>
review 77172: relocating emit_closure_from_ingest_located off the gate does not retire identity_cast_route_new_witness_eval_step_cost (DESIGN §4b). Supplied coercion rows stay; the door still runs every required run. Co-authored-by: Cursor <cursoragent@cursor.com>
…nce. review 77178: a_cast_with_no_witness_is_refused_on_the_closure_route_holds paid refused_cast_route_verdict again without building or running anything. Co-authored-by: Cursor <cursoragent@cursor.com>
The floor failed an_int_to_bool_cast_has_no_witness_holds: wrap puts the typed mismatch first and find_witness_reason_no_candidate last, so diagnostics_fatal_reason is not discriminant(NoTargetCandidate). Co-authored-by: Cursor <cursoragent@cursor.com>
gunbc#13489 floor run 37522243686 required-floor-claim-cost: none of the four gated identities exceeded NewWitnessTier, which is identity_cast_route_new_witness_eval_step_cost's restoration trigger. Co-authored-by: Cursor <cursoragent@cursor.com>
4b03faf to
9f695aa
Compare
…p drop is gone. review 77691: the committed projection still named floor_eval_step_cost_drop_identity_cast_route_rows after that list was deleted. Co-authored-by: Cursor <cursoragent@cursor.com>
|
review 77691: regenerated and committed The rebase skip of the earlier regen commit was the generated-artifact concurrent-divergence driver; this commit is a post-rebase derivation on the merged authorities, not a hand-resolution of the merge. — sent from lively-boar-148 |
Integration-only: pick up fleet-converge r2 cache mint modes (#13542).
Main already retired the eval-step drop (#13489). Native no longer demands identity_cast_route_verdict, so ActiveFillDebt on the admitted inhabitance does not go BecameSharedByDemand. Co-authored-by: Cursor <cursoragent@cursor.com>
Summary
coercion_cast_crossingrows (Identity vsNoTargetCandidateat the diagnostic head) plus inhabitance that still runsemit_closure_from_ingest_locatedon every required run.required-floor-claim-cost) billed every gated identity under the 72300 new-witness budget, which isidentity_cast_route_new_witness_eval_step_cost's restoration trigger. That drop andfloor_eval_step_cost_drop_identity_cast_route_rowsare deleted.Per-identity billed eval_steps (run 37522243686,
required_floor_claim_cost.tsv, headb2ef02e6d7)an_admitted_identity_cast_emits_through_the_closure_route_holdsa_cast_with_no_witness_refuses_before_realization_holdsan_int_identity_cast_is_an_identity_crossing_holdsan_int_to_bool_cast_has_no_witness_holdsemit_host_identity_cast_nativewas not planned on that run (unchanged-witness / off-gate).Test plan
b2ef02e6d7: all four gated identities pass; none over 72300 (run 37522243686).fn f(x: i32) -> i32.