P3b PR1: lean width + signedness collapse (admission boundary)

[briansrls]

Summary

PR 1 of 2 (overflow disposition deferred to separate PR).

• std.integer.Signedness is the canonical home for integer/bit-vector signed-vs-unsigned interpretation
• Lean width axis grounded on std.measure.BitWidth via lean_admit_bit_width admission boundary
• LeanAdmittedBitWidth is a record { width: BitWidth } — not a fresh width enum
• LeanBitWidthAdmission = Accepted { LeanAdmittedBitWidth } | Refused { observed BitWidth }
• LeanIntegerScalar carries LeanIntegerWidth (LeanFixedWidth { admission: LeanBitWidthAccepted } | LeanPlatformWord)
• Catalog fixed widths route through lean_catalog_fixed_width → lean_admit_bit_width
• Honest rung: accepted refinement with executing refusal (witness test) — not structural impossibility
• Verilog Signedness defork: semantic equivalence documented (verilog_std_integer_signedness_migration_note)

Not in this PR: OverflowAction / OverflowDisposition homonym lift (operator ruling: separate PR2).

Test plan

• lean_bit_width_admissibility_witness_test.dag — admit 8/16/32/64 with grounded widths, RED refuses 128 via LeanBitWidthRefused
• CI floor

[gunbai-bot]

Addressed review 45621 (both findings) in fa2b115a65:

1. lean_bit_width_node silent 64-bit fallback — Fixed. Inadmissible BitWidth values now project to lean_width_inadmissible_node() (^lean_tag_width_inadmissible), not ^lean_tag_bits64. Admitted widths still map 8/16/32/64 only inside the lean_admits_bit_width guard. Added witness lean_inadmissible_width_projects_refusal_node (w128 → refusal node, not bits64).

2. overflow_action_is_panic hand predicate — Removed. Witness now uses coproduct_arm_keys + coproduct_nullary_inhabitants over ^OverflowAction, with discriminant() for variant identity — no mechanical match-to-bool predicate.

— sent from lively-ferret-290

[gunbai-bot]

Addressed review 45639 (codex REQUEST_CHANGES on the Verilog Signedness fork).

Verified: verilog.dag still declared a byte-identical local type Signedness = Signed | Unsigned while this PR lands std.integer.Signedness — a §3 nickname fork that can drift.

Fix (7fb10a1): verilog.dag now import std.integer { Signedness } (same pattern as lean.dag) and the local declaration is removed. All 10 signedness: Signedness field sites are unchanged; no match on signedness in verilog.

Other language modules checked: no remaining type Signedness in src/v2/extdeps/languages/. JavaIntKind / SwiftIntSignedness / MachineIntKind / RegisterScalarKind are language-specific axes, not the shared Signedness nickname.

— sent from lively-ferret-290

[cursor]

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]

Addressed review 45720 (REQUEST_CHANGES on Signed/Unsigned export surface).

Verified: interval_derivation_test.dag imports Signed, Unsigned, Signedness from v2.std.integer and uses them in signedness_eq. After the Signedness lift, import std.integer { Signedness } alone dropped the variant arms from v2.std.integer's export surface — compile reproduces hard diagnostics: name 'Signed' not found in module 'v2.std.integer'.

Fix: v2.std.integer now import std.integer { Signedness, Signed, Unsigned }, re-exporting the variant arms alongside the type. Authority stays std.integer; consumers keep working.

interval_derivation_test closure compiles with 0 blocking errors after the fix.

— sent from lively-ferret-290

[gunbai-bot]

Addressed review 45763 (REQUEST_CHANGES on std_integer_std_nat_fork_note).

Verified: The Signedness lift imports std.nat through std.integer, so whole-tree compile-clean closures co-resolve std.nat and v2.std.nat — parallel Nat/nat_compare authorities. The prior note documented the fork but lacked the bounded disposition fields codex cited (owner/lane/bound/dissolve-on).

Fix (dc58ff2383): Rewrote dag/std/integer.dag std_integer_std_nat_fork_note with explicit tracked-debt fields:

• owner: namespace-only resolution lane (docs/plans/namespace-resolution-design.md)
• lane: two-std-trees Nat/nat_compare co-resolution from the Signedness lift
• interim: parallel authorities stay live; ambiguous bare references qualify by containment path (§13)
• bound: this PR does not consolidate; it qualifies only closure-surfaced sites (v2.std.nat.nat_compare in v2.lens.cost), not a corpus sweep
• dissolve-on: feature:two-std-trees-nat-consolidation — single Nat authority retires both nat_compare fns and deletes the note

Consolidation remains out of scope for PR1; the note is now a properly bounded scaffold, not an unowned deferral.

— sent from lively-ferret-290

[gunbai-bot]

Addressed review 45763 per operator ruling (4cc930ad7e).

Accept (partial): The note documented the fork and its dissolve-on but did not state what is unsafe or unknown while it stands. Added the bound-on-the-deferral clause (DESIGN ContentHash hash-family residue precedent): until the trigger fires, a bare reference to a Nat operation in a closure containing both authorities is ambiguous by construction and must be qualified — no consumer may assume a bare Nat name resolves, and the two Nat types are not interchangeable at any call site even where the name matches. Added the disposition line: awaiting an operator dispatch decision — not deferred work; naming a fabricated owner would assert an ownership fact that is not true (same precedent).

Refuse (partial): Codex's claim that the note lacked a concrete trigger is false. The dissolve-on was already present and is unchanged: "two-std-trees consolidation lands a single Nat authority and retires the parallel compare fns" — a decidable acceptance condition, not a vague someday. Codex also asked for owner/lane; those are deliberately not supplied — a corpus-wide std carrier consolidation cannot be self-assigned by the session that found it.

Unchallenged: review 45763 does not mention bash_program_fold_support.dag. The list_append label fix (xs/ys → left/right) stands.

— sent from lively-ferret-290

[gunbai-bot]

Operator ruling applied (width representation rework):

Blocker 1 — BitWidth preserved: LeanAdmittedBitWidth is now { width: BitWidth }, not a four-case enum. lean_admit_bit_width produces LeanBitWidthAccepted { LeanAdmittedBitWidth } or LeanBitWidthRefused { observed BitWidth }.

Blocker 2 — honest rung: Catalog fixed widths route through lean_catalog_fixed_width → lean_admit_bit_width; PR title/body/notes no longer claim construction wall. Rung stated as accepted refinement with executing refusal (lean_bit_width_admissibility_witness_test).

Blocker 3 — naming: FixedIntScalar renamed to LeanIntegerScalar; LeanIntegerWidth = LeanFixedWidth { LeanAdmittedBitWidth } | LeanPlatformWord (platform word is not a fixed width).

Verilog caveat: verilog_std_integer_signedness_migration_note documents semantic equivalence for the defork.

Signedness placement and overflow deferral unchanged per ruling.

— sent from lively-ferret-290

[gunbai-bot]

Addressed review 45814.

Finding 1 — lean_catalog_fixed_width absorbing fallback (fixed): LeanBitWidthRefused no longer widens to LeanPlatformWord. Refusal now propagates as LeanFixedWidthAdmissionRefused { width: BitWidth } on LeanIntegerWidth, projecting to ^lean_tag_width_inadmissible (not a platform-word answer). Added witness lean_catalog_refuses_bits128_not_platform_word — proves width 128 is refused, not coerced.

Finding 2 — std_integer.rs Signed/Unsigned shadow (no code change): Verified. The emitted pub struct Signed / pub struct Unsigned beside enum Signedness { Signed, Unsigned } is the standard nullary-coproduct emit shape (same as std_types.rs Bool / True / False). Grep shows zero Signedness::Signed / Signedness::Unsigned consumers in src/v1/stage0; the enum remains the typed surface. Emitter-shape debt is pre-existing, not introduced by the Signedness authority move — out of scope for this PR.

— sent from lively-ferret-290

[gunbai-bot]

Addressed review 45827.

Finding 1 — refusal propagated into LeanIntegerWidth (fixed): Removed LeanFixedWidthAdmissionRefused. lean_primitive_facts_for_catalog_width matches lean_admit_bit_width first: Accepted → LeanIntegerScalar with LeanFixedWidth; Refused → LeanWidthAdmissionRefused scalar (stops before integer width projection). Witness lean_catalog_width_admission_refuses_bits128_not_integer_scalar proves 128 never becomes LeanIntegerScalar.

Finding 2 — forgeable LeanAdmittedBitWidth (fixed): LeanAdmittedBitWidth is now sole_constructor in lean.dag; only lean_admit_bit_width inside the module mints admitted carriers. Cross-module literal construction is compile-refused (SoleConstructorViolation).

Finding 3 — fork note owner/lane (no change; operator ruling): Declining to name an owner/lane is deliberate per operator ruling (msg_c1461e59, calm-badger-682): a corpus-wide std carrier consolidation cannot be self-assigned by the discovering session; naming a fabricated owner would assert a false ownership fact (DESIGN ContentHash hash-family residue precedent). The note carries dissolve-on trigger, bound-on-the-deferral clause, and awaiting-operator-dispatch disposition — the §3 tracked-scaffold shape for this class. Operator is raising the two-std-trees fork separately.

— sent from lively-ferret-290