Repository navigation
Integer interval decode reads the module's data rows; the 2^n ladder and digit primitives are carried tables (stage 1 of #11741's rewire program) - #11784
Conversation
…riving the 2^n ladder per candidate integer_standard_integer_type_interval_spec called integer_machine_interval_spec on every demand, a second way to compute a bound beside the int8..uint128 data rows that already carry each spec once per frame; the node decoder folded it over all ten standard types per decode, so one integer-node decode re-derived 2^127 and its siblings. On the required floor with the eval-frame memo retired (run 35466872753) integer_pow2_magnitude was the top within-claim recurrence: 22,715 repeats across 44 claims. The projection now matches the type to its row (std.materialization_ladder rule 1: one computation identity, carried), and the decoder compares against a once-per-frame table of (type, interval node). Same value by construction -- each row's body is integer_machine_interval_spec with the literal signedness and width the matches produced -- and by execution: interval_derivation_matches_all_legacy_spelled_bounds still holds against hand-spelled bounds, from_node_round_trips_all_standard_types still holds. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Ledger-Repair-Judged: docs/design-rung-drops.md Ledger-Rows-Repaired: docs/design-rung-drops.md namespace_wave_admission_wall_removed Heal-Candidate-Run: 35486408641
… the pow2 ladder; digit primitives as tables - integer_standard_integer_type_interval_nodes is list_map over integer_standard_integer_type_roster: one enumeration of the closed set. - The annotation names the instrument (the floor's demand census) and transcribes no figure. - integer_pow2_magnitude reads a once-per-frame ladder table for exponents up to 128 (built by the same doubling the recursion performs) so the ten widths share one chain's prefix instead of ten ladders. - decimal_digit_of_units and nonzero_decimal_digit_of_positive_units are direct tables instead of roster scans; decimal_digit_double is its own twenty-row truth table. Same values: pow2_digit_shapes_hold and the hand-spelled legacy bounds still hold on both realizations. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Reply to review 68856 (REQUEST_CHANGES), both findings verified and fixed in b4e9aa8: the annotation now names the instrument (the floor's demand census, within-claim repeats = evals − claims) and carries no transcribed figure; the decode table is |
…to session/merry-fox-260-stage1
|
Reply to review 68885 (REQUEST_CHANGES), which reviewed the auto-heal head |
…git primitives stay as they were The carried ladder is read by walking its Cons chain -- the nth Cons is 2^n by construction, running off the end continues doubling from the last carried power -- so there is no indexed lookup and no miss arm inside the carried range to absorb a deficit. The hand-authored digit tables (decimal_digit_of_units, nonzero_decimal_digit_of_positive_units, decimal_digit_double) are reverted: they re-minted the digit<->value authority as a second table beside decimal_digit_value, and their siblings still derived from it. One digit<->value row set with both directions derived is its own change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Reply to review 68908 (REQUEST_CHANGES), all three findings verified and fixed in f5ca0df. (1)+(2) The digit primitives are reverted to main's derivations: the twenty-row doubling table and the hand-written inverses re-minted the digit↔value authority beside |
…-stage1 # Conflicts: # docs/design-rung-drops.md
What
Stage 1 of the rewire program behind #11741 (option-A ruling): the top within-claim recurrence on the required floor with the eval-frame memo retired.
integer_standard_integer_type_interval_speccalledinteger_machine_interval_specon every demand — a second way to compute a bound beside theint8_interval_spec … uint128_interval_specdatarows that already carry each spec once per frame (their own annotation says the fn "remains the single derivation authority; these rows are its applications" — the fn had never been pointed at them).integer_standard_integer_type_from_nodefolded that fn over all ten standard types per decode, so one integer-node decode re-derived 2^127 and its nine siblings (a 127-step decimal-doubling ladder each).std.materialization_ladderrule 1: one computation identity, carried, never re-derived.Now: the projection matches the type to its row; the decoder compares against a once-per-frame table of (type, interval node) derived by
list_mapfrom the one roster.integer_machine_interval_specstays the single derivation authority; nothing new computes a bound.One more carry in the same ladder, found by re-measuring after the first:
integer_pow2_magnitudewalks a once-per-frame ladder of 2^0..2^128 (built by the same doubling the recursion performs; index n IS 2^n by construction) so the ten widths share one chain's prefix instead of climbing ten ladders. The walk is structural — the nth Cons is 2^n, running off the end continues doubling from the last carried power — so there is no indexed lookup and no miss arm inside the carried range (review 68908). The digit primitives (decimal_digit_valueand its inverse,decimal_digit_double) are deliberately untouched: making the inverse direction a second hand-authored table was refused as a §3 re-mint, and the right shape — one digit↔value row set with both directions derived — is its own change.Semantics-preserving on its face
Same value by construction — each row's body is
integer_machine_interval_spec(signedness: S, width_bits: W)with the literalS/Wthe two total matches produce for that type — and by execution:interval_derivation_matches_all_legacy_spelled_bounds(all ten types against hand-spelled bounds, an oracle independent of both the old and the new route) andfrom_node_round_trips_all_standard_typeshold on the memo-on and the memo-retired binary. A direct old-vs-new equality claim was written, measured at 1.87M eval steps (it re-runs the ladder it exists to retire), and not enrolled: the legacy-bounds claim is the independent receipt. Memo-on cost of the first-touching claim per frame rises slightly (41k → 49k steps) because the ladder table is built to 2^128 once regardless of which widths a frame demands; every other claim falls.Matched before/after on the claims it names
claim_batch --claim-run, same three modules, same session host; "before" isorigin/mainatdfa4644000, "after" is this head; measured under both realizations (memo-on = today's floor; memo-retired = the #11741 head).interval_derivation_matches_all_legacy_spelled_boundsderivation_discriminates_planted_off_by_onepow2_digit_shapes_holdinterval_min_not_above_max_for_all_standard_typesfrom_node_round_trips_all_standard_typeswell_formed_unbounded_carrier_still_decodesdecode_refusals_carry_distinct_reason_symbolsproducer_fault_refusals_retain_the_lookup_causecross_language_compile_python_to_typescript_round_trip_holdstranslate_refuses_underived_conj_holdstranslate_refuses_underived_disj_holdstranslate_refuses_underived_value_holdstranslate_refuses_underived_bodied_arrow_holdstranslate_refuses_underived_grammar_match_holdstranslate_refuses_mixed_derived_root_underived_child_holdstranslate_refuses_absent_parent_underived_child_holdstranslate_refuses_bodyless_emission_root_with_poison_child_holdstranslate_refuses_bodied_arrow_shortcut_underived_descendant_holdstranslate_refuses_projection_absent_fold_bodied_arrow_underived_descendant_holdstranslate_accepts_synthetic_empty_facts_tree_holdstranslate_accepts_derived_corpus_module_holdstranslate_derived_emit_byte_identical_to_before_holdsrust_binop_vep_emit_core_catalog_holdsrust_binop_vep_emit_discriminates_from_addrust_binop_vep_emit_wrong_token_discriminatesrust_binop_vep_emit_missing_catalog_rejectsrust_binop_producer_emit_sub_holdsrust_binop_producer_emit_sub_discriminates_from_addrust_binop_producer_emit_mul_holdsrust_binop_producer_emit_eq_holdsTerminal results: 30/30 PASS before and after under both realizations — floor population unchanged, no claim moved its verdict. The
translate_*/rust_binop_*rows are unchanged by design: their memo-retired cost has a different root (theformal_production_*grammar lookup family, ranks 2–10 of the floor census), which is stage 2.Instrument for re-derivation:
required_floor_cross_claim_demand.tsvof the run, within-claim repeats =evals − claimsper producer row; the ranking is on #11741.Generated-artifact side effects
The two non-
.daghunks (.gitattributes,docs/design-rung-drops.md) are the CI auto-heal regenerating projections that were stale on this branch's merge base. The removal of thePOSTSCRIPT, 2026-09-20line indocs/design-rung-drops.mdis not this PR dropping operator text: that line was a hand-edit to the generated file (never in the.dagrow), main itself removed it in #11789, andorigin/maincarries zero occurrences today; this PR's file is byte-identical to main's.🤖 Generated with Claude Code