From 43089352748bd6d4a9a5d452a06ae1fbebdd8260 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 18:34:02 +0000 Subject: [PATCH 01/27] WIP: P3b language width tower collapse --- src/v2/extdeps/languages/java.dag | 5 +- src/v2/extdeps/languages/lean.dag | 27 ++++++---- src/v2/extdeps/languages/primitive_width.dag | 17 +++++++ src/v2/extdeps/languages/ptx.dag | 8 +-- src/v2/extdeps/languages/rust.dag | 5 +- .../primitive_width_tower_witness_test.dag | 51 +++++++++++++++++++ 6 files changed, 89 insertions(+), 24 deletions(-) create mode 100644 src/v2/extdeps/languages/primitive_width.dag create mode 100644 src/v2/test/claim/primitive_width_tower_witness_test.dag diff --git a/src/v2/extdeps/languages/java.dag b/src/v2/extdeps/languages/java.dag index c5507fa2866..3c5842e5b05 100644 --- a/src/v2/extdeps/languages/java.dag +++ b/src/v2/extdeps/languages/java.dag @@ -1,4 +1,5 @@ module v2.extdeps.languages.java +import v2.extdeps.languages.primitive_width { OverflowAction } import v2.std.language_model { LanguageModel } import v2.std.host_transport { target_emit_host_runtime_row_unconfigured } @@ -137,10 +138,6 @@ type JavaNonIntegerPrimitiveFacts { representation: Symbol } -type OverflowAction - = PanicOnOverflow - | TwoComplementWrap - type JavaGrammarRelationRow { production: GrammarProduction emitted: Node diff --git a/src/v2/extdeps/languages/lean.dag b/src/v2/extdeps/languages/lean.dag index 4ebcc7fe342..8ee40aba3e9 100644 --- a/src/v2/extdeps/languages/lean.dag +++ b/src/v2/extdeps/languages/lean.dag @@ -1,4 +1,5 @@ module v2.extdeps.languages.lean +import v2.extdeps.languages.primitive_width { BitsWidth } import v2.std.language_model { LanguageModel } import v2.std.grammar { @@ -185,15 +186,10 @@ type LeanIntKind = Signed | Unsigned -type LeanIntWidth - = Bits8 - | Bits16 - | Bits32 - | Bits64 - | Pointer +data lean_bits_width_admissibility_note: String = "Lean fixed-precision integers admit Bits8|16|32|64 and platform word Pointer (usize); Bits128 is out of surface. Width variants are imported from v2.extdeps.languages.primitive_width.BitsWidth — not re-declared here (P3b collapse)." type LeanScalar - = IntScalar { kind: LeanIntKind, width: LeanIntWidth } + = IntScalar { kind: LeanIntKind, width: BitsWidth } | BoolScalar type LeanPrimitiveFacts { @@ -297,7 +293,18 @@ fn lean_int_kind_node(kind: LeanIntKind) -> Node { } } -fn lean_int_width_node(width: LeanIntWidth) -> Node { +fn lean_admits_bits_width(width: BitsWidth) -> Bool { + match width { + Bits8 => true + Bits16 => true + Bits32 => true + Bits64 => true + Pointer => true + Bits128 => false + } +} + +fn lean_int_width_node(width: BitsWidth) -> Node { match width { Bits8 => lean_inhabitant_atom(id: ^lean_tag_bits8) Bits16 => lean_inhabitant_atom(id: ^lean_tag_bits16) @@ -364,7 +371,7 @@ fn lean_inhabitant_int32_node() -> Node { lean_primitive_inhabitant_node(id: ^lean_inhabitant_int32, facts: lean_facts_int32) } -fn lean_int_spec_facts(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: LeanIntWidth) -> Map { +fn lean_int_spec_facts(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: BitsWidth) -> Map { Map { lookup: fn(axis) { if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { @@ -588,7 +595,7 @@ fn lean_language_model_canonical_symbols() -> Set { } } -fn lean_integer_algebra_witness_node(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: LeanIntWidth) -> Node { +fn lean_integer_algebra_witness_node(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: BitsWidth) -> Node { Node { kind: TypeNode { connective: Conj }, children: [ diff --git a/src/v2/extdeps/languages/primitive_width.dag b/src/v2/extdeps/languages/primitive_width.dag new file mode 100644 index 00000000000..2b26b84e941 --- /dev/null +++ b/src/v2/extdeps/languages/primitive_width.dag @@ -0,0 +1,17 @@ +module v2.extdeps.languages.primitive_width + +data bits_width_authority_note: String = "Single authority for the machine bit-width axis across target-language models (P3b width-tower collapse). DESIGN section 2 horizontal: Int8..UInt128 are Compose> rows — one axis, not ten types; the corpus had re-forked that axis per language as Bits8/Bits16/... variant homes. Dissolve-on: each v2.extdeps.languages.* module imports BitsWidth here and expresses language-specific surface via an admissibility relation, never a second enum carrying the same numbers." + +type BitsWidth + = Bits8 + | Bits16 + | Bits32 + | Bits64 + | Bits128 + | Pointer + +data overflow_action_homonym_note: String = "OverflowAction lifted from java.dag and rust.dag (byte-identical PanicOnOverflow | TwoComplementWrap). P3a-class self-fork homonym eliminated: one type, N language consumers." + +type OverflowAction + = PanicOnOverflow + | TwoComplementWrap diff --git a/src/v2/extdeps/languages/ptx.dag b/src/v2/extdeps/languages/ptx.dag index ae413b07484..825e69436cf 100644 --- a/src/v2/extdeps/languages/ptx.dag +++ b/src/v2/extdeps/languages/ptx.dag @@ -1,5 +1,6 @@ module v2.extdeps.languages.ptx +import v2.extdeps.languages.primitive_width { BitsWidth } import v2.std.grammar { StampClass, StampBinding, FormalProduction, ParseGrammar, GrammarExpr, GrammarProduction, GrammarRoot, GrammarSchema, GrammarSchemaProbe, GrammarSchemaProbeBinding, ModeledGrammar, Terminal, grammar_atom, grammar_empty_sync_tokens, grammar_formal_nonterminal, grammar_formal_terminal } @@ -60,12 +61,7 @@ type ThreadCoordSource | ClusterInGrid | CtaInGrid -type BitsWidth - = Bits8 - | Bits16 - | Bits32 - | Bits64 - | Bits128 +data ptx_bits_width_admissibility_note: String = "PTX register file admits Bits8|16|32|64|128 raw bit widths via imported primitive_width.BitsWidth; Pointer is not a PTX register width (category b admissibility — absent from PTX surface)." type IntegerWidth = IntBits8 diff --git a/src/v2/extdeps/languages/rust.dag b/src/v2/extdeps/languages/rust.dag index c5fd2d61103..aec16b569c3 100644 --- a/src/v2/extdeps/languages/rust.dag +++ b/src/v2/extdeps/languages/rust.dag @@ -1,4 +1,5 @@ module v2.extdeps.languages.rust +import v2.extdeps.languages.primitive_width { OverflowAction } import std.trait_derive_shape { ReprDeriveClone, ReprDeriveDebug, @@ -423,10 +424,6 @@ type RustCost { allocation_cost: Int } -type OverflowAction - = PanicOnOverflow - | TwoComplementWrap - type RustIntegerOverflowDisposition { ir_carrier: IRCarrier checked_arithmetic_debug_default: OverflowAction diff --git a/src/v2/test/claim/primitive_width_tower_witness_test.dag b/src/v2/test/claim/primitive_width_tower_witness_test.dag new file mode 100644 index 00000000000..e0106eafa49 --- /dev/null +++ b/src/v2/test/claim/primitive_width_tower_witness_test.dag @@ -0,0 +1,51 @@ +module v2.test.claim.primitive_width_tower_witness + + +import v2.extdeps.languages.lean { lean_admits_bits_width } +import v2.extdeps.languages.primitive_width { + BitsWidth, + OverflowAction, + PanicOnOverflow, + TwoComplementWrap +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data primitive_width_tower_witness_note: String = "P3b width-tower collapse receipts: canonical BitsWidth authority is singular (primitive_width.dag); lean admits Bits8|16|32|64|Pointer and refuses Bits128; OverflowAction is shared across java/rust consumers." + +test fn lean_admits_catalog_widths() -> Bool { + lean_admits_bits_width(width: Bits8) && + lean_admits_bits_width(width: Bits16) && + lean_admits_bits_width(width: Bits32) && + lean_admits_bits_width(width: Bits64) && + lean_admits_bits_width(width: Pointer) +} + +test fn lean_refuses_bits128_admissibility() -> Bool { + lean_admits_bits_width(width: Bits128) == false +} + +test fn overflow_action_shared_variants_constructible() -> Bool { + match PanicOnOverflow { + PanicOnOverflow => true + TwoComplementWrap => false + } && + match TwoComplementWrap { + PanicOnOverflow => false + TwoComplementWrap => true + } +} + +test fn overflow_action_type_is_shared_authority() -> Bool { + let debug_default: OverflowAction = PanicOnOverflow + let release_default: OverflowAction = TwoComplementWrap + match debug_default { + PanicOnOverflow => match release_default { + PanicOnOverflow => false + TwoComplementWrap => true + } + TwoComplementWrap => false + } +} From 8517fb8181bafeb5b4eda45500c787c04dd25f97 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 18:39:06 +0000 Subject: [PATCH 02/27] P3b: lift OverflowAction homonym only; hold width tower Withdraw primitive_width.dag (BitsWidth enum would mint a third width authority and canonize the wrong variant-atom shape). Cluster-7 OverflowAction moves to overflow_action.dag with java/rust imports; lean/ptx width work reverted to main pending BitWidth grounding. Co-authored-by: Cursor --- src/v2/extdeps/languages/java.dag | 2 +- src/v2/extdeps/languages/lean.dag | 27 +++++++------------ src/v2/extdeps/languages/overflow_action.dag | 7 +++++ src/v2/extdeps/languages/primitive_width.dag | 17 ------------ src/v2/extdeps/languages/ptx.dag | 8 ++++-- src/v2/extdeps/languages/rust.dag | 2 +- ... overflow_action_homonym_witness_test.dag} | 20 +++----------- 7 files changed, 28 insertions(+), 55 deletions(-) create mode 100644 src/v2/extdeps/languages/overflow_action.dag delete mode 100644 src/v2/extdeps/languages/primitive_width.dag rename src/v2/test/claim/{primitive_width_tower_witness_test.dag => overflow_action_homonym_witness_test.dag} (51%) diff --git a/src/v2/extdeps/languages/java.dag b/src/v2/extdeps/languages/java.dag index 3c5842e5b05..32875eea660 100644 --- a/src/v2/extdeps/languages/java.dag +++ b/src/v2/extdeps/languages/java.dag @@ -1,5 +1,5 @@ module v2.extdeps.languages.java -import v2.extdeps.languages.primitive_width { OverflowAction } +import v2.extdeps.languages.overflow_action { OverflowAction } import v2.std.language_model { LanguageModel } import v2.std.host_transport { target_emit_host_runtime_row_unconfigured } diff --git a/src/v2/extdeps/languages/lean.dag b/src/v2/extdeps/languages/lean.dag index 8ee40aba3e9..4ebcc7fe342 100644 --- a/src/v2/extdeps/languages/lean.dag +++ b/src/v2/extdeps/languages/lean.dag @@ -1,5 +1,4 @@ module v2.extdeps.languages.lean -import v2.extdeps.languages.primitive_width { BitsWidth } import v2.std.language_model { LanguageModel } import v2.std.grammar { @@ -186,10 +185,15 @@ type LeanIntKind = Signed | Unsigned -data lean_bits_width_admissibility_note: String = "Lean fixed-precision integers admit Bits8|16|32|64 and platform word Pointer (usize); Bits128 is out of surface. Width variants are imported from v2.extdeps.languages.primitive_width.BitsWidth — not re-declared here (P3b collapse)." +type LeanIntWidth + = Bits8 + | Bits16 + | Bits32 + | Bits64 + | Pointer type LeanScalar - = IntScalar { kind: LeanIntKind, width: BitsWidth } + = IntScalar { kind: LeanIntKind, width: LeanIntWidth } | BoolScalar type LeanPrimitiveFacts { @@ -293,18 +297,7 @@ fn lean_int_kind_node(kind: LeanIntKind) -> Node { } } -fn lean_admits_bits_width(width: BitsWidth) -> Bool { - match width { - Bits8 => true - Bits16 => true - Bits32 => true - Bits64 => true - Pointer => true - Bits128 => false - } -} - -fn lean_int_width_node(width: BitsWidth) -> Node { +fn lean_int_width_node(width: LeanIntWidth) -> Node { match width { Bits8 => lean_inhabitant_atom(id: ^lean_tag_bits8) Bits16 => lean_inhabitant_atom(id: ^lean_tag_bits16) @@ -371,7 +364,7 @@ fn lean_inhabitant_int32_node() -> Node { lean_primitive_inhabitant_node(id: ^lean_inhabitant_int32, facts: lean_facts_int32) } -fn lean_int_spec_facts(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: BitsWidth) -> Map { +fn lean_int_spec_facts(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: LeanIntWidth) -> Map { Map { lookup: fn(axis) { if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { @@ -595,7 +588,7 @@ fn lean_language_model_canonical_symbols() -> Set { } } -fn lean_integer_algebra_witness_node(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: BitsWidth) -> Node { +fn lean_integer_algebra_witness_node(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: LeanIntWidth) -> Node { Node { kind: TypeNode { connective: Conj }, children: [ diff --git a/src/v2/extdeps/languages/overflow_action.dag b/src/v2/extdeps/languages/overflow_action.dag new file mode 100644 index 00000000000..f21b3fe0e8b --- /dev/null +++ b/src/v2/extdeps/languages/overflow_action.dag @@ -0,0 +1,7 @@ +module v2.extdeps.languages.overflow_action + +data overflow_action_homonym_note: String = "OverflowAction lifted from java.dag and rust.dag (byte-identical PanicOnOverflow | TwoComplementWrap). P3a-class self-fork homonym eliminated: one type, N language consumers. No std authority covers integer overflow disposition at this grain." + +type OverflowAction + = PanicOnOverflow + | TwoComplementWrap diff --git a/src/v2/extdeps/languages/primitive_width.dag b/src/v2/extdeps/languages/primitive_width.dag deleted file mode 100644 index 2b26b84e941..00000000000 --- a/src/v2/extdeps/languages/primitive_width.dag +++ /dev/null @@ -1,17 +0,0 @@ -module v2.extdeps.languages.primitive_width - -data bits_width_authority_note: String = "Single authority for the machine bit-width axis across target-language models (P3b width-tower collapse). DESIGN section 2 horizontal: Int8..UInt128 are Compose> rows — one axis, not ten types; the corpus had re-forked that axis per language as Bits8/Bits16/... variant homes. Dissolve-on: each v2.extdeps.languages.* module imports BitsWidth here and expresses language-specific surface via an admissibility relation, never a second enum carrying the same numbers." - -type BitsWidth - = Bits8 - | Bits16 - | Bits32 - | Bits64 - | Bits128 - | Pointer - -data overflow_action_homonym_note: String = "OverflowAction lifted from java.dag and rust.dag (byte-identical PanicOnOverflow | TwoComplementWrap). P3a-class self-fork homonym eliminated: one type, N language consumers." - -type OverflowAction - = PanicOnOverflow - | TwoComplementWrap diff --git a/src/v2/extdeps/languages/ptx.dag b/src/v2/extdeps/languages/ptx.dag index 825e69436cf..ae413b07484 100644 --- a/src/v2/extdeps/languages/ptx.dag +++ b/src/v2/extdeps/languages/ptx.dag @@ -1,6 +1,5 @@ module v2.extdeps.languages.ptx -import v2.extdeps.languages.primitive_width { BitsWidth } import v2.std.grammar { StampClass, StampBinding, FormalProduction, ParseGrammar, GrammarExpr, GrammarProduction, GrammarRoot, GrammarSchema, GrammarSchemaProbe, GrammarSchemaProbeBinding, ModeledGrammar, Terminal, grammar_atom, grammar_empty_sync_tokens, grammar_formal_nonterminal, grammar_formal_terminal } @@ -61,7 +60,12 @@ type ThreadCoordSource | ClusterInGrid | CtaInGrid -data ptx_bits_width_admissibility_note: String = "PTX register file admits Bits8|16|32|64|128 raw bit widths via imported primitive_width.BitsWidth; Pointer is not a PTX register width (category b admissibility — absent from PTX surface)." +type BitsWidth + = Bits8 + | Bits16 + | Bits32 + | Bits64 + | Bits128 type IntegerWidth = IntBits8 diff --git a/src/v2/extdeps/languages/rust.dag b/src/v2/extdeps/languages/rust.dag index aec16b569c3..a56c8edabe4 100644 --- a/src/v2/extdeps/languages/rust.dag +++ b/src/v2/extdeps/languages/rust.dag @@ -1,5 +1,5 @@ module v2.extdeps.languages.rust -import v2.extdeps.languages.primitive_width { OverflowAction } +import v2.extdeps.languages.overflow_action { OverflowAction } import std.trait_derive_shape { ReprDeriveClone, ReprDeriveDebug, diff --git a/src/v2/test/claim/primitive_width_tower_witness_test.dag b/src/v2/test/claim/overflow_action_homonym_witness_test.dag similarity index 51% rename from src/v2/test/claim/primitive_width_tower_witness_test.dag rename to src/v2/test/claim/overflow_action_homonym_witness_test.dag index e0106eafa49..433d0d64903 100644 --- a/src/v2/test/claim/primitive_width_tower_witness_test.dag +++ b/src/v2/test/claim/overflow_action_homonym_witness_test.dag @@ -1,9 +1,7 @@ -module v2.test.claim.primitive_width_tower_witness +module v2.test.claim.overflow_action_homonym_witness -import v2.extdeps.languages.lean { lean_admits_bits_width } -import v2.extdeps.languages.primitive_width { - BitsWidth, +import v2.extdeps.languages.overflow_action { OverflowAction, PanicOnOverflow, TwoComplementWrap @@ -13,19 +11,7 @@ import v2.std.logic { Bool } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -data primitive_width_tower_witness_note: String = "P3b width-tower collapse receipts: canonical BitsWidth authority is singular (primitive_width.dag); lean admits Bits8|16|32|64|Pointer and refuses Bits128; OverflowAction is shared across java/rust consumers." - -test fn lean_admits_catalog_widths() -> Bool { - lean_admits_bits_width(width: Bits8) && - lean_admits_bits_width(width: Bits16) && - lean_admits_bits_width(width: Bits32) && - lean_admits_bits_width(width: Bits64) && - lean_admits_bits_width(width: Pointer) -} - -test fn lean_refuses_bits128_admissibility() -> Bool { - lean_admits_bits_width(width: Bits128) == false -} +data overflow_action_homonym_witness_note: String = "P3b cluster-7 receipt: OverflowAction is singular in v2.extdeps.languages.overflow_action; java.dag and rust.dag import it (no second declaration). Width-tower collapse deferred pending std.measure BitWidth / std.machine_constraints MachineWidth grounding column." test fn overflow_action_shared_variants_constructible() -> Bool { match PanicOnOverflow { From 16eeeed652a7cb92387686cc149ca52020acd4ef Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 18:42:15 +0000 Subject: [PATCH 03/27] Fix overflow witness parse: match on bound values only MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Bare variant atoms (match PanicOnOverflow) are not valid scrutinees in the v1 parser — use typed let bindings and a helper fn, matching enforcement_live_witness_test and wet_receipt_enrollment patterns. Co-authored-by: Cursor --- .../overflow_action_homonym_witness_test.dag | 23 ++++++++----------- 1 file changed, 10 insertions(+), 13 deletions(-) diff --git a/src/v2/test/claim/overflow_action_homonym_witness_test.dag b/src/v2/test/claim/overflow_action_homonym_witness_test.dag index 433d0d64903..b0578dac1dd 100644 --- a/src/v2/test/claim/overflow_action_homonym_witness_test.dag +++ b/src/v2/test/claim/overflow_action_homonym_witness_test.dag @@ -13,25 +13,22 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly data overflow_action_homonym_witness_note: String = "P3b cluster-7 receipt: OverflowAction is singular in v2.extdeps.languages.overflow_action; java.dag and rust.dag import it (no second declaration). Width-tower collapse deferred pending std.measure BitWidth / std.machine_constraints MachineWidth grounding column." -test fn overflow_action_shared_variants_constructible() -> Bool { - match PanicOnOverflow { +fn overflow_action_is_panic(o: OverflowAction) -> Bool { + match o { PanicOnOverflow => true TwoComplementWrap => false - } && - match TwoComplementWrap { - PanicOnOverflow => false - TwoComplementWrap => true } } +test fn overflow_action_shared_variants_constructible() -> Bool { + let panic: OverflowAction = PanicOnOverflow + let wrap: OverflowAction = TwoComplementWrap + overflow_action_is_panic(o: panic) && !overflow_action_is_panic(o: wrap) +} + test fn overflow_action_type_is_shared_authority() -> Bool { let debug_default: OverflowAction = PanicOnOverflow let release_default: OverflowAction = TwoComplementWrap - match debug_default { - PanicOnOverflow => match release_default { - PanicOnOverflow => false - TwoComplementWrap => true - } - TwoComplementWrap => false - } + overflow_action_is_panic(o: debug_default) + && !overflow_action_is_panic(o: release_default) } From d29efd684217199ebf2f83a1523b0b81d5b828b5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 18:47:39 +0000 Subject: [PATCH 04/27] P3b cluster-1: lean width tower on std.measure.BitWidth Replace LeanIntWidth enum (Bits8|...|Pointer) with std.measure.BitWidth for fixed widths and UsizeScalar for platform word. Add lean_admits_bit_width admissibility relation and witness with RED control refusing 128-bit widths. Co-authored-by: Cursor --- src/v2/extdeps/languages/lean.dag | 132 ++++++++++++++---- ...n_bit_width_admissibility_witness_test.dag | 49 +++++++ 2 files changed, 153 insertions(+), 28 deletions(-) create mode 100644 src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag diff --git a/src/v2/extdeps/languages/lean.dag b/src/v2/extdeps/languages/lean.dag index 4ebcc7fe342..4b9777f96bc 100644 --- a/src/v2/extdeps/languages/lean.dag +++ b/src/v2/extdeps/languages/lean.dag @@ -38,6 +38,7 @@ import v2.std.compilers.lexing { import v2.std.collection { Absent, List, Map, Present, Set } import v2.std.logic { Bool, bool_boolean_algebra } import std.algebra { Cons, Empty } +import std.measure { BitWidth, bit_width, bit_width_count } import v2.std.algebra { BooleanAlgebra, boolean_algebra_type_node, commutative_ring_type_node, fold_list, list_map } import v2.std.text { String } import v2.std.model_core { @@ -185,15 +186,11 @@ type LeanIntKind = Signed | Unsigned -type LeanIntWidth - = Bits8 - | Bits16 - | Bits32 - | Bits64 - | Pointer +data lean_bit_width_admissibility_note: String = "Lean fixed-precision integers admit 8/16/32/64-bit widths via std.measure.BitWidth; usize is platform word (PointerWidth axis), not a fixed BitWidth variant. P3b cluster-1 collapse: no Bits8|Bits16|... enum — admissibility is lean_admits_bit_width over BitWidth." type LeanScalar - = IntScalar { kind: LeanIntKind, width: LeanIntWidth } + = IntScalar { kind: LeanIntKind, width: BitWidth } + | UsizeScalar | BoolScalar type LeanPrimitiveFacts { @@ -204,55 +201,55 @@ type LeanPrimitiveFacts { data lean_facts_int8: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_int8, - scalar: IntScalar { kind: Signed, width: Bits8 }, + scalar: IntScalar { kind: Signed, width: bit_width(count: 8) }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_int16: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_int16, - scalar: IntScalar { kind: Signed, width: Bits16 }, + scalar: IntScalar { kind: Signed, width: bit_width(count: 16) }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_int32: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_int32, - scalar: IntScalar { kind: Signed, width: Bits32 }, + scalar: IntScalar { kind: Signed, width: bit_width(count: 32) }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_int64: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_int64, - scalar: IntScalar { kind: Signed, width: Bits64 }, + scalar: IntScalar { kind: Signed, width: bit_width(count: 64) }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_uint8: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_uint8, - scalar: IntScalar { kind: Unsigned, width: Bits8 }, + scalar: IntScalar { kind: Unsigned, width: bit_width(count: 8) }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_uint16: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_uint16, - scalar: IntScalar { kind: Unsigned, width: Bits16 }, + scalar: IntScalar { kind: Unsigned, width: bit_width(count: 16) }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_uint32: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_uint32, - scalar: IntScalar { kind: Unsigned, width: Bits32 }, + scalar: IntScalar { kind: Unsigned, width: bit_width(count: 32) }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_uint64: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_uint64, - scalar: IntScalar { kind: Unsigned, width: Bits64 }, + scalar: IntScalar { kind: Unsigned, width: bit_width(count: 64) }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_usize: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_usize, - scalar: IntScalar { kind: Unsigned, width: Pointer }, + scalar: UsizeScalar, representation: ^lean_repr_usize_platform_word } @@ -297,13 +294,25 @@ fn lean_int_kind_node(kind: LeanIntKind) -> Node { } } -fn lean_int_width_node(width: LeanIntWidth) -> Node { - match width { - Bits8 => lean_inhabitant_atom(id: ^lean_tag_bits8) - Bits16 => lean_inhabitant_atom(id: ^lean_tag_bits16) - Bits32 => lean_inhabitant_atom(id: ^lean_tag_bits32) - Bits64 => lean_inhabitant_atom(id: ^lean_tag_bits64) - Pointer => lean_inhabitant_atom(id: ^lean_tag_pointer) +fn lean_admits_bit_width(width: BitWidth) -> Bool { + let n = bit_width_count(width) + n == 8 || n == 16 || n == 32 || n == 64 +} + +fn lean_platform_word_width_node() -> Node { + lean_inhabitant_atom(id: ^lean_tag_pointer) +} + +fn lean_bit_width_node(width: BitWidth) -> Node { + let n = bit_width_count(width) + if n == 8 { + lean_inhabitant_atom(id: ^lean_tag_bits8) + } else if n == 16 { + lean_inhabitant_atom(id: ^lean_tag_bits16) + } else if n == 32 { + lean_inhabitant_atom(id: ^lean_tag_bits32) + } else { + lean_inhabitant_atom(id: ^lean_tag_bits64) } } @@ -317,7 +326,22 @@ fn lean_scalar_node(scalar: LeanScalar) -> Node { target: lean_inhabitant_atom(id: ^lean_tag_scalar_int) ), lean_named_edge(name: ^lean_scalar_field_kind, target: lean_int_kind_node(kind: kind)), - lean_named_edge(name: ^lean_scalar_field_width, target: lean_int_width_node(width: width)) + lean_named_edge(name: ^lean_scalar_field_width, target: lean_bit_width_node(width: width)) + ], + occurrence_id: SyntheticOccurrence +} + UsizeScalar => Node { + kind: TypeNode { connective: Conj }, + children: [ + lean_named_edge( + name: ^lean_scalar_field_classifier, + target: lean_inhabitant_atom(id: ^lean_tag_scalar_int) + ), + lean_named_edge(name: ^lean_scalar_field_kind, target: lean_int_kind_node(kind: Unsigned)), + lean_named_edge( + name: ^lean_scalar_field_width, + target: lean_platform_word_width_node() + ) ], occurrence_id: SyntheticOccurrence } @@ -364,13 +388,13 @@ fn lean_inhabitant_int32_node() -> Node { lean_primitive_inhabitant_node(id: ^lean_inhabitant_int32, facts: lean_facts_int32) } -fn lean_int_spec_facts(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: LeanIntWidth) -> Map { +fn lean_int_spec_facts(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: BitWidth) -> Map { Map { lookup: fn(axis) { if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.surface_spelling) } } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: lean_int_width_node(width: width) } + v2.std.optional.Present { value: lean_bit_width_node(width: width) } } else if axis == discriminant(v: ModelCoreFactAxisSignedness {}) { v2.std.optional.Present { value: lean_int_kind_node(kind: kind) } } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { @@ -382,6 +406,24 @@ fn lean_int_spec_facts(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: Lean } } +fn lean_usize_spec_facts(facts: LeanPrimitiveFacts) -> Map { + Map { + lookup: fn(axis) { + if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { + v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.surface_spelling) } + } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { + v2.std.optional.Present { value: lean_platform_word_width_node() } + } else if axis == discriminant(v: ModelCoreFactAxisSignedness {}) { + v2.std.optional.Present { value: lean_int_kind_node(kind: Unsigned) } + } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { + v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.representation) } + } else { + v2.std.optional.Absent + } + } + } +} + fn lean_bool_spec_facts(facts: LeanPrimitiveFacts) -> Map { Map { lookup: fn(axis) { @@ -402,6 +444,10 @@ fn lean_primitive_bundle_from_facts(facts: LeanPrimitiveFacts) -> PrimitiveFactB substrate_carrier: lean_primitive_facts_node(facts: facts), spec_facts: lean_int_spec_facts(facts: facts, kind: kind, width: width) } + UsizeScalar => PrimitiveFactBundle { + substrate_carrier: lean_primitive_facts_node(facts: facts), + spec_facts: lean_usize_spec_facts(facts: facts) + } BoolScalar => PrimitiveFactBundle { substrate_carrier: lean_primitive_facts_node(facts: facts), spec_facts: lean_bool_spec_facts(facts: facts) @@ -588,7 +634,7 @@ fn lean_language_model_canonical_symbols() -> Set { } } -fn lean_integer_algebra_witness_node(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: LeanIntWidth) -> Node { +fn lean_integer_algebra_witness_node(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: BitWidth) -> Node { Node { kind: TypeNode { connective: Conj }, children: [ @@ -606,7 +652,32 @@ fn lean_integer_algebra_witness_node(facts: LeanPrimitiveFacts, kind: LeanIntKin ), lean_named_edge( name: ^lean_witness_field_width, - target: lean_int_width_node(width: width) + target: lean_bit_width_node(width: width) + ) + ], + occurrence_id: SyntheticOccurrence +} +} + +fn lean_usize_algebra_witness_node(facts: LeanPrimitiveFacts) -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [ + lean_named_edge( + name: ^lean_witness_integer_commutative_ring, + target: lean_inhabitant_atom(id: ^lean_witness_integer_commutative_ring) + ), + lean_named_edge( + name: ^lean_witness_field_representation, + target: lean_inhabitant_atom(id: facts.representation) + ), + lean_named_edge( + name: ^lean_witness_field_signedness, + target: lean_int_kind_node(kind: Unsigned) + ), + lean_named_edge( + name: ^lean_witness_field_width, + target: lean_platform_word_width_node() ) ], occurrence_id: SyntheticOccurrence @@ -639,6 +710,11 @@ fn lean_scalar_algebra_inhabitance(facts: LeanPrimitiveFacts) -> AlgebraInhabita inhabitant: inhabitant, witness: lean_integer_algebra_witness_node(facts: facts, kind: kind, width: width) } + UsizeScalar => AlgebraInhabitanceDecl { + algebra: commutative_ring_type_node(inhabitant: inhabitant), + inhabitant: inhabitant, + witness: lean_usize_algebra_witness_node(facts: facts) + } BoolScalar => AlgebraInhabitanceDecl { algebra: boolean_algebra_type_node(inhabitant: inhabitant), inhabitant: inhabitant, diff --git a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag new file mode 100644 index 00000000000..6874ff902ad --- /dev/null +++ b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag @@ -0,0 +1,49 @@ +module v2.test.claim.lean_bit_width_admissibility_witness + + +import v2.extdeps.languages.lean { lean_admits_bit_width } +import std.measure { BitWidth, bit_width, bit_width_count } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data lean_bit_width_admissibility_witness_note: String = "P3b cluster-1 receipt (lean end-to-end): fixed widths ground on std.measure.BitWidth via bit_width(count); lean_admits_bit_width is the per-language admissibility relation (8/16/32/64 admitted, 128 refused). No Bits8|Bits16|... variant homes in lean.dag." + +fn bit_width_count_is_eight(width: BitWidth) -> Bool { + bit_width_count(width) == 8 +} + +fn bit_width_count_is_sixteen(width: BitWidth) -> Bool { + bit_width_count(width) == 16 +} + +fn bit_width_count_is_thirty_two(width: BitWidth) -> Bool { + bit_width_count(width) == 32 +} + +fn bit_width_count_is_sixty_four(width: BitWidth) -> Bool { + bit_width_count(width) == 64 +} + +fn bit_width_count_is_one_twenty_eight(width: BitWidth) -> Bool { + bit_width_count(width) == 128 +} + +test fn lean_admits_catalog_fixed_widths() -> Bool { + let w8: BitWidth = bit_width(count: 8) + let w16: BitWidth = bit_width(count: 16) + let w32: BitWidth = bit_width(count: 32) + let w64: BitWidth = bit_width(count: 64) + lean_admits_bit_width(width: w8) + && lean_admits_bit_width(width: w16) + && lean_admits_bit_width(width: w32) + && lean_admits_bit_width(width: w64) + && bit_width_count_is_eight(width: w8) + && bit_width_count_is_sixty_four(width: w64) +} + +test fn lean_refuses_bits128_admissibility() -> Bool { + let w128: BitWidth = bit_width(count: 128) + !lean_admits_bit_width(width: w128) && bit_width_count_is_one_twenty_eight(width: w128) +} From 3fd54b2eb331c348c8266c78910e67cd5c6da662 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 18:55:06 +0000 Subject: [PATCH 05/27] Fix lean width witness: remove orphan helper fns Witness naming hygiene requires every plain fn in *_test.dag to be reachable from a test fn; inline bit_width_count check instead. Co-authored-by: Cursor --- ...n_bit_width_admissibility_witness_test.dag | 36 +++---------------- 1 file changed, 5 insertions(+), 31 deletions(-) diff --git a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag index 6874ff902ad..68652475691 100644 --- a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag +++ b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag @@ -10,40 +10,14 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly data lean_bit_width_admissibility_witness_note: String = "P3b cluster-1 receipt (lean end-to-end): fixed widths ground on std.measure.BitWidth via bit_width(count); lean_admits_bit_width is the per-language admissibility relation (8/16/32/64 admitted, 128 refused). No Bits8|Bits16|... variant homes in lean.dag." -fn bit_width_count_is_eight(width: BitWidth) -> Bool { - bit_width_count(width) == 8 -} - -fn bit_width_count_is_sixteen(width: BitWidth) -> Bool { - bit_width_count(width) == 16 -} - -fn bit_width_count_is_thirty_two(width: BitWidth) -> Bool { - bit_width_count(width) == 32 -} - -fn bit_width_count_is_sixty_four(width: BitWidth) -> Bool { - bit_width_count(width) == 64 -} - -fn bit_width_count_is_one_twenty_eight(width: BitWidth) -> Bool { - bit_width_count(width) == 128 -} - test fn lean_admits_catalog_fixed_widths() -> Bool { - let w8: BitWidth = bit_width(count: 8) - let w16: BitWidth = bit_width(count: 16) - let w32: BitWidth = bit_width(count: 32) - let w64: BitWidth = bit_width(count: 64) - lean_admits_bit_width(width: w8) - && lean_admits_bit_width(width: w16) - && lean_admits_bit_width(width: w32) - && lean_admits_bit_width(width: w64) - && bit_width_count_is_eight(width: w8) - && bit_width_count_is_sixty_four(width: w64) + lean_admits_bit_width(width: bit_width(count: 8)) + && lean_admits_bit_width(width: bit_width(count: 16)) + && lean_admits_bit_width(width: bit_width(count: 32)) + && lean_admits_bit_width(width: bit_width(count: 64)) } test fn lean_refuses_bits128_admissibility() -> Bool { let w128: BitWidth = bit_width(count: 128) - !lean_admits_bit_width(width: w128) && bit_width_count_is_one_twenty_eight(width: w128) + !lean_admits_bit_width(width: w128) && bit_width_count(w128) == 128 } From 0ab553acc444f26f21f9b03f85d8a45075d99c48 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 19:11:10 +0000 Subject: [PATCH 06/27] Fix rust_add_emit_translate test OverflowAction imports PanicOnOverflow and TwoComplementWrap live in overflow_action.dag after the homonym lift; the manual emit test imported them from rust. Co-authored-by: Cursor --- src/v2/test/claim/manual/rust_add_emit_translate_test.dag | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/v2/test/claim/manual/rust_add_emit_translate_test.dag b/src/v2/test/claim/manual/rust_add_emit_translate_test.dag index c78aa25743e..c9fdbec72d9 100644 --- a/src/v2/test/claim/manual/rust_add_emit_translate_test.dag +++ b/src/v2/test/claim/manual/rust_add_emit_translate_test.dag @@ -20,6 +20,10 @@ import v2.compiler.translate { target_serialize_source_from_model, translate, } +import v2.extdeps.languages.overflow_action { + PanicOnOverflow, + TwoComplementWrap +} import v2.extdeps.languages.rust { rust_inhabitant_i32_node, rust_inhabitant_atom, @@ -38,9 +42,7 @@ import v2.extdeps.languages.rust { rust_fn_add_lex, rust_facts_i32, Signed, - Bits32, - PanicOnOverflow, - TwoComplementWrap + Bits32 } import v2.compiler.infer { InferredFacts, InferredTree } import extdeps.communication.medium { Lossless, Medium } From 27e0ae75b378e65cb7dbbf21acad1312f80da65c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 19:20:31 +0000 Subject: [PATCH 07/27] WIP: P3b language width tower collapse --- src/v2/extdeps/languages/overflow_action.dag | 2 +- src/v2/test/claim/overflow_action_homonym_witness_test.dag | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/v2/extdeps/languages/overflow_action.dag b/src/v2/extdeps/languages/overflow_action.dag index f21b3fe0e8b..e3479d74d12 100644 --- a/src/v2/extdeps/languages/overflow_action.dag +++ b/src/v2/extdeps/languages/overflow_action.dag @@ -1,6 +1,6 @@ module v2.extdeps.languages.overflow_action -data overflow_action_homonym_note: String = "OverflowAction lifted from java.dag and rust.dag (byte-identical PanicOnOverflow | TwoComplementWrap). P3a-class self-fork homonym eliminated: one type, N language consumers. No std authority covers integer overflow disposition at this grain." +data overflow_action_homonym_note: String = "OverflowAction homonym lift within src/v2/extdeps/languages only: java.dag and rust.dag imported this byte-identical type (PanicOnOverflow | TwoComplementWrap) instead of sharing one module. Proved here: OverflowAction is the sole type name in src/v2; variant owner count for TwoComplementWrap reduced from three declarations (dag/extdeps/languages/rust/primitives.dag IntegerOverflow, src/v2 rust, src/v2 java) to two (this module + dag primitives — file-local, unimported). Corpus-wide variant singularity is NOT claimed: the ambiguity axis is variant names, and dag/extdeps/languages/rust/primitives.dag still declares TwoComplementWrap under IntegerOverflow (three variants: TwoComplementWrap | Saturating | Trap — richer vocabulary than OverflowAction's two). Seam consolidation (OverflowAction vs IntegerOverflow nickname) is out of scope for this surface. No std authority covers integer overflow disposition at this grain." type OverflowAction = PanicOnOverflow diff --git a/src/v2/test/claim/overflow_action_homonym_witness_test.dag b/src/v2/test/claim/overflow_action_homonym_witness_test.dag index b0578dac1dd..61668737c8a 100644 --- a/src/v2/test/claim/overflow_action_homonym_witness_test.dag +++ b/src/v2/test/claim/overflow_action_homonym_witness_test.dag @@ -11,7 +11,7 @@ import v2.std.logic { Bool } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -data overflow_action_homonym_witness_note: String = "P3b cluster-7 receipt: OverflowAction is singular in v2.extdeps.languages.overflow_action; java.dag and rust.dag import it (no second declaration). Width-tower collapse deferred pending std.measure BitWidth / std.machine_constraints MachineWidth grounding column." +data overflow_action_homonym_witness_note: String = "P3b cluster-7 receipt (src/v2 scope): OverflowAction type name is singular in src/v2/extdeps/languages; java.dag and rust.dag import overflow_action (no second OverflowAction declaration in src/v2). Variant TwoComplementWrap still has a residual owner in dag/extdeps/languages/rust/primitives.dag IntegerOverflow — not exercised by this witness." fn overflow_action_is_panic(o: OverflowAction) -> Bool { match o { From fa2b115a6589291eff7c80382d403a85aa66ca09 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 19:51:38 +0000 Subject: [PATCH 08/27] Address review 45621: fail-closed width projection, coproduct witness lean_bit_width_node refuses inadmissible BitWidth via lean_tag_width_inadmissible instead of silently mapping to 64-bit; witness asserts w128 projects to the refusal node. overflow_action homonym witness drops hand-written variant predicate; uses coproduct_arm_keys and coproduct_nullary_inhabitants with discriminant() for construction checks. Co-authored-by: Cursor --- src/v2/extdeps/languages/lean.dag | 24 ++++--- ...n_bit_width_admissibility_witness_test.dag | 12 +++- .../overflow_action_homonym_witness_test.dag | 69 +++++++++++++++---- 3 files changed, 83 insertions(+), 22 deletions(-) diff --git a/src/v2/extdeps/languages/lean.dag b/src/v2/extdeps/languages/lean.dag index 4b9777f96bc..078cffa0f73 100644 --- a/src/v2/extdeps/languages/lean.dag +++ b/src/v2/extdeps/languages/lean.dag @@ -303,16 +303,24 @@ fn lean_platform_word_width_node() -> Node { lean_inhabitant_atom(id: ^lean_tag_pointer) } +fn lean_width_inadmissible_node() -> Node { + lean_inhabitant_atom(id: ^lean_tag_width_inadmissible) +} + fn lean_bit_width_node(width: BitWidth) -> Node { - let n = bit_width_count(width) - if n == 8 { - lean_inhabitant_atom(id: ^lean_tag_bits8) - } else if n == 16 { - lean_inhabitant_atom(id: ^lean_tag_bits16) - } else if n == 32 { - lean_inhabitant_atom(id: ^lean_tag_bits32) + if lean_admits_bit_width(width: width) { + let n = bit_width_count(width) + if n == 8 { + lean_inhabitant_atom(id: ^lean_tag_bits8) + } else if n == 16 { + lean_inhabitant_atom(id: ^lean_tag_bits16) + } else if n == 32 { + lean_inhabitant_atom(id: ^lean_tag_bits32) + } else { + lean_inhabitant_atom(id: ^lean_tag_bits64) + } } else { - lean_inhabitant_atom(id: ^lean_tag_bits64) + lean_width_inadmissible_node() } } diff --git a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag index 68652475691..f43376d355c 100644 --- a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag +++ b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag @@ -1,7 +1,11 @@ module v2.test.claim.lean_bit_width_admissibility_witness -import v2.extdeps.languages.lean { lean_admits_bit_width } +import v2.extdeps.languages.lean { + lean_admits_bit_width, + lean_bit_width_node, + lean_width_inadmissible_node +} import std.measure { BitWidth, bit_width, bit_width_count } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import v2.std.logic { Bool } @@ -21,3 +25,9 @@ test fn lean_refuses_bits128_admissibility() -> Bool { let w128: BitWidth = bit_width(count: 128) !lean_admits_bit_width(width: w128) && bit_width_count(w128) == 128 } + +test fn lean_inadmissible_width_projects_refusal_node() -> Bool { + let w128: BitWidth = bit_width(count: 128) + !lean_admits_bit_width(width: w128) + && lean_bit_width_node(width: w128) == lean_width_inadmissible_node() +} diff --git a/src/v2/test/claim/overflow_action_homonym_witness_test.dag b/src/v2/test/claim/overflow_action_homonym_witness_test.dag index 61668737c8a..d2dead5ad91 100644 --- a/src/v2/test/claim/overflow_action_homonym_witness_test.dag +++ b/src/v2/test/claim/overflow_action_homonym_witness_test.dag @@ -6,29 +6,72 @@ import v2.extdeps.languages.overflow_action { PanicOnOverflow, TwoComplementWrap } +import std.algebra { Empty } +import v2.std.algebra { bag_eq, fold_list, list_snoc_item } +import v2.std.collection { List } +import v2.std.diagnostic { Accepted, Rejected } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import v2.std.logic { Bool } +import v2.std.node { Symbol } +import v2.std.node_query { coproduct_arm_keys, coproduct_nullary_inhabitants } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly +data reflect_overflow_action_type: Symbol = ^OverflowAction + data overflow_action_homonym_witness_note: String = "P3b cluster-7 receipt (src/v2 scope): OverflowAction type name is singular in src/v2/extdeps/languages; java.dag and rust.dag import overflow_action (no second OverflowAction declaration in src/v2). Variant TwoComplementWrap still has a residual owner in dag/extdeps/languages/rust/primitives.dag IntegerOverflow — not exercised by this witness." -fn overflow_action_is_panic(o: OverflowAction) -> Bool { - match o { - PanicOnOverflow => true - TwoComplementWrap => false +data expected_overflow_action_arm_keys: List = [ + ^PanicOnOverflow, + ^TwoComplementWrap +] + +fn overflow_action_discriminant(value: OverflowAction) -> Symbol { + discriminant(v: value) +} + +fn symbol_eq(a: Symbol, b: Symbol) -> Bool { + a == b +} + +fn overflow_action_inhabitant_discriminants( + inhabitants: List +) -> List { + fold_list( + xs: inhabitants, + empty: Empty, + cons: fn(acc, value) { + list_snoc_item(xs: acc, item: overflow_action_discriminant(value: value)) + } + ) +} + +test fn overflow_action_coproduct_arm_keys_match_shared_authority() -> Bool { + bag_eq( + xs: coproduct_arm_keys(type_name: reflect_overflow_action_type), + ys: expected_overflow_action_arm_keys, + eq: symbol_eq + ) +} + +test fn overflow_action_nullary_inhabitants_match_arms() -> Bool { + match coproduct_nullary_inhabitants( + type_name: reflect_overflow_action_type, + discriminant_of: overflow_action_discriminant + ) { + Accepted { value: inhabitants, diagnostics: _ } => + bag_eq( + xs: overflow_action_inhabitant_discriminants(inhabitants: inhabitants), + ys: expected_overflow_action_arm_keys, + eq: symbol_eq + ) + Rejected { diagnostics: _ } => false } } -test fn overflow_action_shared_variants_constructible() -> Bool { +test fn overflow_action_variants_constructible() -> Bool { let panic: OverflowAction = PanicOnOverflow let wrap: OverflowAction = TwoComplementWrap - overflow_action_is_panic(o: panic) && !overflow_action_is_panic(o: wrap) -} - -test fn overflow_action_type_is_shared_authority() -> Bool { - let debug_default: OverflowAction = PanicOnOverflow - let release_default: OverflowAction = TwoComplementWrap - overflow_action_is_panic(o: debug_default) - && !overflow_action_is_panic(o: release_default) + overflow_action_discriminant(value: panic) == ^PanicOnOverflow + && overflow_action_discriminant(value: wrap) == ^TwoComplementWrap } From 83b35bb61e8d144c19d66e7e59899578da860d0d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 20:00:49 +0000 Subject: [PATCH 09/27] Split PR 1: lean width+signedness only; drop OverflowAction Operator ruling: OverflowAction does not land (std.integer OverflowDisposition is canonical). Revert overflow_action module; restore per-module OverflowAction in java/rust. Lean construction wall: FixedIntScalar carries LeanIntegerWidth (LeanFixedWidth+LeanAdmittedBitWidth | LeanPlatformWord), not raw BitWidth; lean_admit_bit_width returns Accepted|Refused. Signedness from std.integer (added to dag/std/integer.dag; v2 imports it). PR back to draft; overflow disposition is a separate follow-up PR. Co-authored-by: Cursor --- dag/std/integer.dag | 4 + src/v2/extdeps/languages/java.dag | 5 +- src/v2/extdeps/languages/lean.dag | 190 ++++++++---------- src/v2/extdeps/languages/overflow_action.dag | 7 - src/v2/extdeps/languages/rust.dag | 5 +- src/v2/std/integer.dag | 3 +- ...n_bit_width_admissibility_witness_test.dag | 43 ++-- .../manual/rust_add_emit_translate_test.dag | 8 +- .../overflow_action_homonym_witness_test.dag | 77 ------- 9 files changed, 120 insertions(+), 222 deletions(-) delete mode 100644 src/v2/extdeps/languages/overflow_action.dag delete mode 100644 src/v2/test/claim/overflow_action_homonym_witness_test.dag diff --git a/dag/std/integer.dag b/dag/std/integer.dag index a674412977f..fa679a13a0b 100644 --- a/dag/std/integer.dag +++ b/dag/std/integer.dag @@ -21,6 +21,10 @@ type UInt128 = Compose> type Int = AbelianGroup> type UInt = Nat +type Signedness + = Signed + | Unsigned + type IntPlatform = Compose> type UIntPlatform = Compose> diff --git a/src/v2/extdeps/languages/java.dag b/src/v2/extdeps/languages/java.dag index 32875eea660..78e65578c20 100644 --- a/src/v2/extdeps/languages/java.dag +++ b/src/v2/extdeps/languages/java.dag @@ -1,5 +1,4 @@ module v2.extdeps.languages.java -import v2.extdeps.languages.overflow_action { OverflowAction } import v2.std.language_model { LanguageModel } import v2.std.host_transport { target_emit_host_runtime_row_unconfigured } @@ -112,6 +111,10 @@ type JavaScalar | BoolScalar | VoidScalar +type OverflowAction + = PanicOnOverflow + | TwoComplementWrap + type JavaIntegerPrimitiveFacts { surface_spelling: Symbol signedness: JavaIntKind diff --git a/src/v2/extdeps/languages/lean.dag b/src/v2/extdeps/languages/lean.dag index 078cffa0f73..ba94e4f951b 100644 --- a/src/v2/extdeps/languages/lean.dag +++ b/src/v2/extdeps/languages/lean.dag @@ -38,6 +38,7 @@ import v2.std.compilers.lexing { import v2.std.collection { Absent, List, Map, Present, Set } import v2.std.logic { Bool, bool_boolean_algebra } import std.algebra { Cons, Empty } +import std.integer { Signedness } import std.measure { BitWidth, bit_width, bit_width_count } import v2.std.algebra { BooleanAlgebra, boolean_algebra_type_node, commutative_ring_type_node, fold_list, list_map } import v2.std.text { String } @@ -182,15 +183,24 @@ type LeanProofCheckSemantics { proof_irrelevance_for_propositions: Bool } -type LeanIntKind - = Signed - | Unsigned +data lean_bit_width_admissibility_note: String = "Lean fixed-precision integers: width axis is std.measure.BitWidth admitted via LeanBitWidthAdmission into LeanAdmittedBitWidth (construction wall — raw BitWidth cannot reach FixedIntScalar); platform word is LeanPlatformWord on the PointerWidth axis. Signedness is std.integer.Signedness, not LeanIntKind." -data lean_bit_width_admissibility_note: String = "Lean fixed-precision integers admit 8/16/32/64-bit widths via std.measure.BitWidth; usize is platform word (PointerWidth axis), not a fixed BitWidth variant. P3b cluster-1 collapse: no Bits8|Bits16|... enum — admissibility is lean_admits_bit_width over BitWidth." +type LeanAdmittedBitWidth + = LeanAdmitWidth8 + | LeanAdmitWidth16 + | LeanAdmitWidth32 + | LeanAdmitWidth64 + +type LeanBitWidthAdmission + = LeanBitWidthAccepted { width: LeanAdmittedBitWidth } + | LeanBitWidthRefused { width: BitWidth } + +type LeanIntegerWidth + = LeanFixedWidth { width: LeanAdmittedBitWidth } + | LeanPlatformWord type LeanScalar - = IntScalar { kind: LeanIntKind, width: BitWidth } - | UsizeScalar + = FixedIntScalar { signedness: Signedness, width: LeanIntegerWidth } | BoolScalar type LeanPrimitiveFacts { @@ -201,55 +211,55 @@ type LeanPrimitiveFacts { data lean_facts_int8: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_int8, - scalar: IntScalar { kind: Signed, width: bit_width(count: 8) }, + scalar: FixedIntScalar { signedness: Signed, width: LeanFixedWidth { width: LeanAdmitWidth8 } }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_int16: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_int16, - scalar: IntScalar { kind: Signed, width: bit_width(count: 16) }, + scalar: FixedIntScalar { signedness: Signed, width: LeanFixedWidth { width: LeanAdmitWidth16 } }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_int32: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_int32, - scalar: IntScalar { kind: Signed, width: bit_width(count: 32) }, + scalar: FixedIntScalar { signedness: Signed, width: LeanFixedWidth { width: LeanAdmitWidth32 } }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_int64: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_int64, - scalar: IntScalar { kind: Signed, width: bit_width(count: 64) }, + scalar: FixedIntScalar { signedness: Signed, width: LeanFixedWidth { width: LeanAdmitWidth64 } }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_uint8: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_uint8, - scalar: IntScalar { kind: Unsigned, width: bit_width(count: 8) }, + scalar: FixedIntScalar { signedness: Unsigned, width: LeanFixedWidth { width: LeanAdmitWidth8 } }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_uint16: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_uint16, - scalar: IntScalar { kind: Unsigned, width: bit_width(count: 16) }, + scalar: FixedIntScalar { signedness: Unsigned, width: LeanFixedWidth { width: LeanAdmitWidth16 } }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_uint32: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_uint32, - scalar: IntScalar { kind: Unsigned, width: bit_width(count: 32) }, + scalar: FixedIntScalar { signedness: Unsigned, width: LeanFixedWidth { width: LeanAdmitWidth32 } }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_uint64: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_uint64, - scalar: IntScalar { kind: Unsigned, width: bit_width(count: 64) }, + scalar: FixedIntScalar { signedness: Unsigned, width: LeanFixedWidth { width: LeanAdmitWidth64 } }, representation: ^lean_repr_fixed_precision_integer } data lean_facts_usize: LeanPrimitiveFacts = LeanPrimitiveFacts { surface_spelling: ^lean_surface_spelling_usize, - scalar: UsizeScalar, + scalar: FixedIntScalar { signedness: Unsigned, width: LeanPlatformWord }, representation: ^lean_repr_usize_platform_word } @@ -287,68 +297,64 @@ fn lean_named_edge(name: Symbol, target: Node) -> Edge { Edge { label: Named { name: name }, target: target } } -fn lean_int_kind_node(kind: LeanIntKind) -> Node { - match kind { +fn lean_signedness_node(signedness: Signedness) -> Node { + match signedness { Signed => lean_inhabitant_atom(id: ^lean_tag_signed) Unsigned => lean_inhabitant_atom(id: ^lean_tag_unsigned) } } -fn lean_admits_bit_width(width: BitWidth) -> Bool { +fn lean_admit_bit_width(width: BitWidth) -> LeanBitWidthAdmission { let n = bit_width_count(width) - n == 8 || n == 16 || n == 32 || n == 64 + if n == 8 { + LeanBitWidthAccepted { width: LeanAdmitWidth8 } + } else if n == 16 { + LeanBitWidthAccepted { width: LeanAdmitWidth16 } + } else if n == 32 { + LeanBitWidthAccepted { width: LeanAdmitWidth32 } + } else if n == 64 { + LeanBitWidthAccepted { width: LeanAdmitWidth64 } + } else { + LeanBitWidthRefused { width: width } + } } fn lean_platform_word_width_node() -> Node { lean_inhabitant_atom(id: ^lean_tag_pointer) } -fn lean_width_inadmissible_node() -> Node { - lean_inhabitant_atom(id: ^lean_tag_width_inadmissible) +fn lean_admitted_bit_width_node(width: LeanAdmittedBitWidth) -> Node { + match width { + LeanAdmitWidth8 => lean_inhabitant_atom(id: ^lean_tag_bits8) + LeanAdmitWidth16 => lean_inhabitant_atom(id: ^lean_tag_bits16) + LeanAdmitWidth32 => lean_inhabitant_atom(id: ^lean_tag_bits32) + LeanAdmitWidth64 => lean_inhabitant_atom(id: ^lean_tag_bits64) + } } -fn lean_bit_width_node(width: BitWidth) -> Node { - if lean_admits_bit_width(width: width) { - let n = bit_width_count(width) - if n == 8 { - lean_inhabitant_atom(id: ^lean_tag_bits8) - } else if n == 16 { - lean_inhabitant_atom(id: ^lean_tag_bits16) - } else if n == 32 { - lean_inhabitant_atom(id: ^lean_tag_bits32) - } else { - lean_inhabitant_atom(id: ^lean_tag_bits64) - } - } else { - lean_width_inadmissible_node() +fn lean_integer_width_node(width: LeanIntegerWidth) -> Node { + match width { + LeanFixedWidth { width: admitted } => lean_admitted_bit_width_node(width: admitted) + LeanPlatformWord => lean_platform_word_width_node() } } fn lean_scalar_node(scalar: LeanScalar) -> Node { match scalar { - IntScalar { kind, width } => Node { + FixedIntScalar { signedness, width } => Node { kind: TypeNode { connective: Conj }, children: [ lean_named_edge( name: ^lean_scalar_field_classifier, target: lean_inhabitant_atom(id: ^lean_tag_scalar_int) ), - lean_named_edge(name: ^lean_scalar_field_kind, target: lean_int_kind_node(kind: kind)), - lean_named_edge(name: ^lean_scalar_field_width, target: lean_bit_width_node(width: width)) - ], - occurrence_id: SyntheticOccurrence -} - UsizeScalar => Node { - kind: TypeNode { connective: Conj }, - children: [ lean_named_edge( - name: ^lean_scalar_field_classifier, - target: lean_inhabitant_atom(id: ^lean_tag_scalar_int) + name: ^lean_scalar_field_kind, + target: lean_signedness_node(signedness: signedness) ), - lean_named_edge(name: ^lean_scalar_field_kind, target: lean_int_kind_node(kind: Unsigned)), lean_named_edge( name: ^lean_scalar_field_width, - target: lean_platform_word_width_node() + target: lean_integer_width_node(width: width) ) ], occurrence_id: SyntheticOccurrence @@ -396,33 +402,19 @@ fn lean_inhabitant_int32_node() -> Node { lean_primitive_inhabitant_node(id: ^lean_inhabitant_int32, facts: lean_facts_int32) } -fn lean_int_spec_facts(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: BitWidth) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: lean_bit_width_node(width: width) } - } else if axis == discriminant(v: ModelCoreFactAxisSignedness {}) { - v2.std.optional.Present { value: lean_int_kind_node(kind: kind) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.representation) } - } else { - v2.std.optional.Absent - } - } - } -} - -fn lean_usize_spec_facts(facts: LeanPrimitiveFacts) -> Map { +fn lean_fixed_int_spec_facts( + facts: LeanPrimitiveFacts, + signedness: Signedness, + width: LeanIntegerWidth +) -> Map { Map { lookup: fn(axis) { if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.surface_spelling) } } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: lean_platform_word_width_node() } + v2.std.optional.Present { value: lean_integer_width_node(width: width) } } else if axis == discriminant(v: ModelCoreFactAxisSignedness {}) { - v2.std.optional.Present { value: lean_int_kind_node(kind: Unsigned) } + v2.std.optional.Present { value: lean_signedness_node(signedness: signedness) } } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.representation) } } else { @@ -448,13 +440,13 @@ fn lean_bool_spec_facts(facts: LeanPrimitiveFacts) -> Map { fn lean_primitive_bundle_from_facts(facts: LeanPrimitiveFacts) -> PrimitiveFactBundle { match facts.scalar { - IntScalar { kind, width } => PrimitiveFactBundle { + FixedIntScalar { signedness, width } => PrimitiveFactBundle { substrate_carrier: lean_primitive_facts_node(facts: facts), - spec_facts: lean_int_spec_facts(facts: facts, kind: kind, width: width) - } - UsizeScalar => PrimitiveFactBundle { - substrate_carrier: lean_primitive_facts_node(facts: facts), - spec_facts: lean_usize_spec_facts(facts: facts) + spec_facts: lean_fixed_int_spec_facts( + facts: facts, + signedness: signedness, + width: width + ) } BoolScalar => PrimitiveFactBundle { substrate_carrier: lean_primitive_facts_node(facts: facts), @@ -642,7 +634,11 @@ fn lean_language_model_canonical_symbols() -> Set { } } -fn lean_integer_algebra_witness_node(facts: LeanPrimitiveFacts, kind: LeanIntKind, width: BitWidth) -> Node { +fn lean_integer_algebra_witness_node( + facts: LeanPrimitiveFacts, + signedness: Signedness, + width: LeanIntegerWidth +) -> Node { Node { kind: TypeNode { connective: Conj }, children: [ @@ -656,36 +652,11 @@ fn lean_integer_algebra_witness_node(facts: LeanPrimitiveFacts, kind: LeanIntKin ), lean_named_edge( name: ^lean_witness_field_signedness, - target: lean_int_kind_node(kind: kind) + target: lean_signedness_node(signedness: signedness) ), lean_named_edge( name: ^lean_witness_field_width, - target: lean_bit_width_node(width: width) - ) - ], - occurrence_id: SyntheticOccurrence -} -} - -fn lean_usize_algebra_witness_node(facts: LeanPrimitiveFacts) -> Node { - Node { - kind: TypeNode { connective: Conj }, - children: [ - lean_named_edge( - name: ^lean_witness_integer_commutative_ring, - target: lean_inhabitant_atom(id: ^lean_witness_integer_commutative_ring) - ), - lean_named_edge( - name: ^lean_witness_field_representation, - target: lean_inhabitant_atom(id: facts.representation) - ), - lean_named_edge( - name: ^lean_witness_field_signedness, - target: lean_int_kind_node(kind: Unsigned) - ), - lean_named_edge( - name: ^lean_witness_field_width, - target: lean_platform_word_width_node() + target: lean_integer_width_node(width: width) ) ], occurrence_id: SyntheticOccurrence @@ -713,15 +684,14 @@ fn lean_scalar_algebra_inhabitance(facts: LeanPrimitiveFacts) -> AlgebraInhabita let inhabitant = lean_primitive_facts_node(facts: facts) match facts.scalar { - IntScalar { kind, width } => AlgebraInhabitanceDecl { + FixedIntScalar { signedness, width } => AlgebraInhabitanceDecl { algebra: commutative_ring_type_node(inhabitant: inhabitant), inhabitant: inhabitant, - witness: lean_integer_algebra_witness_node(facts: facts, kind: kind, width: width) - } - UsizeScalar => AlgebraInhabitanceDecl { - algebra: commutative_ring_type_node(inhabitant: inhabitant), - inhabitant: inhabitant, - witness: lean_usize_algebra_witness_node(facts: facts) + witness: lean_integer_algebra_witness_node( + facts: facts, + signedness: signedness, + width: width + ) } BoolScalar => AlgebraInhabitanceDecl { algebra: boolean_algebra_type_node(inhabitant: inhabitant), diff --git a/src/v2/extdeps/languages/overflow_action.dag b/src/v2/extdeps/languages/overflow_action.dag deleted file mode 100644 index e3479d74d12..00000000000 --- a/src/v2/extdeps/languages/overflow_action.dag +++ /dev/null @@ -1,7 +0,0 @@ -module v2.extdeps.languages.overflow_action - -data overflow_action_homonym_note: String = "OverflowAction homonym lift within src/v2/extdeps/languages only: java.dag and rust.dag imported this byte-identical type (PanicOnOverflow | TwoComplementWrap) instead of sharing one module. Proved here: OverflowAction is the sole type name in src/v2; variant owner count for TwoComplementWrap reduced from three declarations (dag/extdeps/languages/rust/primitives.dag IntegerOverflow, src/v2 rust, src/v2 java) to two (this module + dag primitives — file-local, unimported). Corpus-wide variant singularity is NOT claimed: the ambiguity axis is variant names, and dag/extdeps/languages/rust/primitives.dag still declares TwoComplementWrap under IntegerOverflow (three variants: TwoComplementWrap | Saturating | Trap — richer vocabulary than OverflowAction's two). Seam consolidation (OverflowAction vs IntegerOverflow nickname) is out of scope for this surface. No std authority covers integer overflow disposition at this grain." - -type OverflowAction - = PanicOnOverflow - | TwoComplementWrap diff --git a/src/v2/extdeps/languages/rust.dag b/src/v2/extdeps/languages/rust.dag index a56c8edabe4..c5fd2d61103 100644 --- a/src/v2/extdeps/languages/rust.dag +++ b/src/v2/extdeps/languages/rust.dag @@ -1,5 +1,4 @@ module v2.extdeps.languages.rust -import v2.extdeps.languages.overflow_action { OverflowAction } import std.trait_derive_shape { ReprDeriveClone, ReprDeriveDebug, @@ -424,6 +423,10 @@ type RustCost { allocation_cost: Int } +type OverflowAction + = PanicOnOverflow + | TwoComplementWrap + type RustIntegerOverflowDisposition { ir_carrier: IRCarrier checked_arithmetic_debug_default: OverflowAction diff --git a/src/v2/std/integer.dag b/src/v2/std/integer.dag index 719660a7d7a..26c08cae0c9 100644 --- a/src/v2/std/integer.dag +++ b/src/v2/std/integer.dag @@ -17,6 +17,7 @@ import v2.std.optional { import v2.std.diagnostic { Correction, Diagnostic, ExternalContractUnknown, Locus, NoCorrectionReason, Outcome, Accepted, None, Rejected, diagnostics_singleton, node_locus, outcome_accepted, outcome_rejected, port_locus, Unavailable } import v2.std.node { Atom, Conj, Edge, Named, Node, Symbol, TypeNode, SyntheticOccurrence, is_empty_conj_root } import v2.std.node_query { find_named_child } +import std.integer { Signedness } import v2.std.machine { Byte, MachineWidth, @@ -33,8 +34,6 @@ type Int = GroupCompletion type UInt = v2.std.nat.Nat type Compose -type Signedness = Signed | Unsigned - type Representation = TwosComplement | OnesComplement diff --git a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag index f43376d355c..a5410e3461b 100644 --- a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag +++ b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag @@ -1,33 +1,38 @@ module v2.test.claim.lean_bit_width_admissibility_witness -import v2.extdeps.languages.lean { - lean_admits_bit_width, - lean_bit_width_node, - lean_width_inadmissible_node -} +import v2.extdeps.languages.lean { lean_admit_bit_width } import std.measure { BitWidth, bit_width, bit_width_count } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import v2.std.logic { Bool } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -data lean_bit_width_admissibility_witness_note: String = "P3b cluster-1 receipt (lean end-to-end): fixed widths ground on std.measure.BitWidth via bit_width(count); lean_admits_bit_width is the per-language admissibility relation (8/16/32/64 admitted, 128 refused). No Bits8|Bits16|... variant homes in lean.dag." - -test fn lean_admits_catalog_fixed_widths() -> Bool { - lean_admits_bit_width(width: bit_width(count: 8)) - && lean_admits_bit_width(width: bit_width(count: 16)) - && lean_admits_bit_width(width: bit_width(count: 32)) - && lean_admits_bit_width(width: bit_width(count: 64)) -} +data lean_bit_width_admissibility_witness_note: String = "P3b cluster-1 receipt (lean end-to-end): BitWidth admission is LeanBitWidthAdmission; FixedIntScalar carries only LeanAdmittedBitWidth via LeanFixedWidth (128 cannot reach width projection). RED: lean_admit_bit_width(128) is Refused with the genuine width pinned." -test fn lean_refuses_bits128_admissibility() -> Bool { - let w128: BitWidth = bit_width(count: 128) - !lean_admits_bit_width(width: w128) && bit_width_count(w128) == 128 +test fn lean_admit_accepts_catalog_fixed_widths() -> Bool { + match lean_admit_bit_width(width: bit_width(count: 8)) { + LeanBitWidthAccepted { width: _ } => + match lean_admit_bit_width(width: bit_width(count: 16)) { + LeanBitWidthAccepted { width: _ } => + match lean_admit_bit_width(width: bit_width(count: 32)) { + LeanBitWidthAccepted { width: _ } => + match lean_admit_bit_width(width: bit_width(count: 64)) { + LeanBitWidthAccepted { width: _ } => true + LeanBitWidthRefused { width: _ } => false + } + LeanBitWidthRefused { width: _ } => false + } + LeanBitWidthRefused { width: _ } => false + } + LeanBitWidthRefused { width: _ } => false + } } -test fn lean_inadmissible_width_projects_refusal_node() -> Bool { +test fn lean_admit_refuses_bits128() -> Bool { let w128: BitWidth = bit_width(count: 128) - !lean_admits_bit_width(width: w128) - && lean_bit_width_node(width: w128) == lean_width_inadmissible_node() + match lean_admit_bit_width(width: w128) { + LeanBitWidthRefused { width: refused } => bit_width_count(refused) == 128 + LeanBitWidthAccepted { width: _ } => false + } } diff --git a/src/v2/test/claim/manual/rust_add_emit_translate_test.dag b/src/v2/test/claim/manual/rust_add_emit_translate_test.dag index c9fdbec72d9..c78aa25743e 100644 --- a/src/v2/test/claim/manual/rust_add_emit_translate_test.dag +++ b/src/v2/test/claim/manual/rust_add_emit_translate_test.dag @@ -20,10 +20,6 @@ import v2.compiler.translate { target_serialize_source_from_model, translate, } -import v2.extdeps.languages.overflow_action { - PanicOnOverflow, - TwoComplementWrap -} import v2.extdeps.languages.rust { rust_inhabitant_i32_node, rust_inhabitant_atom, @@ -42,7 +38,9 @@ import v2.extdeps.languages.rust { rust_fn_add_lex, rust_facts_i32, Signed, - Bits32 + Bits32, + PanicOnOverflow, + TwoComplementWrap } import v2.compiler.infer { InferredFacts, InferredTree } import extdeps.communication.medium { Lossless, Medium } diff --git a/src/v2/test/claim/overflow_action_homonym_witness_test.dag b/src/v2/test/claim/overflow_action_homonym_witness_test.dag deleted file mode 100644 index d2dead5ad91..00000000000 --- a/src/v2/test/claim/overflow_action_homonym_witness_test.dag +++ /dev/null @@ -1,77 +0,0 @@ -module v2.test.claim.overflow_action_homonym_witness - - -import v2.extdeps.languages.overflow_action { - OverflowAction, - PanicOnOverflow, - TwoComplementWrap -} -import std.algebra { Empty } -import v2.std.algebra { bag_eq, fold_list, list_snoc_item } -import v2.std.collection { List } -import v2.std.diagnostic { Accepted, Rejected } -import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } -import v2.std.logic { Bool } -import v2.std.node { Symbol } -import v2.std.node_query { coproduct_arm_keys, coproduct_nullary_inhabitants } - -data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly - -data reflect_overflow_action_type: Symbol = ^OverflowAction - -data overflow_action_homonym_witness_note: String = "P3b cluster-7 receipt (src/v2 scope): OverflowAction type name is singular in src/v2/extdeps/languages; java.dag and rust.dag import overflow_action (no second OverflowAction declaration in src/v2). Variant TwoComplementWrap still has a residual owner in dag/extdeps/languages/rust/primitives.dag IntegerOverflow — not exercised by this witness." - -data expected_overflow_action_arm_keys: List = [ - ^PanicOnOverflow, - ^TwoComplementWrap -] - -fn overflow_action_discriminant(value: OverflowAction) -> Symbol { - discriminant(v: value) -} - -fn symbol_eq(a: Symbol, b: Symbol) -> Bool { - a == b -} - -fn overflow_action_inhabitant_discriminants( - inhabitants: List -) -> List { - fold_list( - xs: inhabitants, - empty: Empty, - cons: fn(acc, value) { - list_snoc_item(xs: acc, item: overflow_action_discriminant(value: value)) - } - ) -} - -test fn overflow_action_coproduct_arm_keys_match_shared_authority() -> Bool { - bag_eq( - xs: coproduct_arm_keys(type_name: reflect_overflow_action_type), - ys: expected_overflow_action_arm_keys, - eq: symbol_eq - ) -} - -test fn overflow_action_nullary_inhabitants_match_arms() -> Bool { - match coproduct_nullary_inhabitants( - type_name: reflect_overflow_action_type, - discriminant_of: overflow_action_discriminant - ) { - Accepted { value: inhabitants, diagnostics: _ } => - bag_eq( - xs: overflow_action_inhabitant_discriminants(inhabitants: inhabitants), - ys: expected_overflow_action_arm_keys, - eq: symbol_eq - ) - Rejected { diagnostics: _ } => false - } -} - -test fn overflow_action_variants_constructible() -> Bool { - let panic: OverflowAction = PanicOnOverflow - let wrap: OverflowAction = TwoComplementWrap - overflow_action_discriminant(value: panic) == ^PanicOnOverflow - && overflow_action_discriminant(value: wrap) == ^TwoComplementWrap -} From 6b0f80d3180c3d43d452e62880f2f1ca0ff4e273 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 20:05:52 +0000 Subject: [PATCH 10/27] WIP: P3b language width tower collapse --- .../claim/lean_bit_width_admissibility_witness_test.dag | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag index a5410e3461b..40ea59f79f3 100644 --- a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag +++ b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag @@ -1,7 +1,11 @@ module v2.test.claim.lean_bit_width_admissibility_witness -import v2.extdeps.languages.lean { lean_admit_bit_width } +import v2.extdeps.languages.lean { + lean_admit_bit_width, + LeanBitWidthAccepted, + LeanBitWidthRefused +} import std.measure { BitWidth, bit_width, bit_width_count } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import v2.std.logic { Bool } From 0128ac7c04df808e0b99a5b6a719919b296a190b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 20:19:47 +0000 Subject: [PATCH 11/27] Drop no-op java.dag hunk: restore file to main OverflowAction relocation was zero net effect from split revert; java.dag should not appear in PR1 diff. Co-authored-by: Cursor --- src/v2/extdeps/languages/java.dag | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/v2/extdeps/languages/java.dag b/src/v2/extdeps/languages/java.dag index 78e65578c20..c5507fa2866 100644 --- a/src/v2/extdeps/languages/java.dag +++ b/src/v2/extdeps/languages/java.dag @@ -111,10 +111,6 @@ type JavaScalar | BoolScalar | VoidScalar -type OverflowAction - = PanicOnOverflow - | TwoComplementWrap - type JavaIntegerPrimitiveFacts { surface_spelling: Symbol signedness: JavaIntKind @@ -141,6 +137,10 @@ type JavaNonIntegerPrimitiveFacts { representation: Symbol } +type OverflowAction + = PanicOnOverflow + | TwoComplementWrap + type JavaGrammarRelationRow { production: GrammarProduction emitted: Node From e9954b4ee066675c98ba3456d5e2e2823a527602 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 31 Jul 2026 20:23:24 +0000 Subject: [PATCH 12/27] chore: regenerate drifted generated artifacts (ci auto-heal) --- docs/plans/fail-closed-lockdown.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/plans/fail-closed-lockdown.md b/docs/plans/fail-closed-lockdown.md index 2ff412fc41b..110e6fe7fd2 100644 --- a/docs/plans/fail-closed-lockdown.md +++ b/docs/plans/fail-closed-lockdown.md @@ -17,7 +17,7 @@ The test for "locked": (a) wired into the floor (discovered + run), (b) fail-clo | Gate | Scope | Evidence | | --- | --- | --- | | DagCompileCleanGate | whole tree (fail-fast root) | `gunbc.ci_gate` `DagCompileCleanGate`; `v2.workflow.ci_floor_plan` `gate_runnable` | -| GeneratedArtifactDriftGate | `ci.yml` / `ROADMAP.md` / `.gitignore` byte-drift + per-artifact perturb, over the committed (= generated AND not-ignored) registry | `ci_spec.dag` `GeneratedArtifactDriftGate`; `generated_artifact_gate.dag`; registry+commit-derivation `gunbc/generated_artifact.dag` | +| GeneratedArtifactDriftGate | `ci.yml` / `ROADMAP.md` / `.gitignore` byte-drift + per-artifact perturb, over the committed (= generated AND not-ignored) registry | `gunbc.ci_gate` `GeneratedArtifactDriftGate`; `tools.generated_artifact_gate` `run_generated_artifact_drift_gate`; `gunbc.generated_artifact` `committed_generated_artifacts` | These are the **structural** gates. The gap is everything *analytical* and the *bootstrap purity* gate. From 7fb10a112fb023e6760ffa4c1ac802c03c59c964 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 20:52:05 +0000 Subject: [PATCH 13/27] WIP: P3b language width tower collapse --- src/v2/extdeps/languages/verilog.dag | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/v2/extdeps/languages/verilog.dag b/src/v2/extdeps/languages/verilog.dag index a5a7934df96..5df9a78f55a 100644 --- a/src/v2/extdeps/languages/verilog.dag +++ b/src/v2/extdeps/languages/verilog.dag @@ -1,6 +1,7 @@ module v2.extdeps.languages.verilog import v2.std.nat { Nat } +import std.integer { Signedness } import v2.std.node { Symbol } import v2.std.grammar { StampClass, @@ -156,10 +157,6 @@ type NetVectoredPacking = NetUnranged | NetRanged { vectoredness: VectorednessClause, range: VectorRange } -type Signedness - = Signed - | Unsigned - type DriveStrengthClause = NoDriveStrength | DriveStrengthLexeme { lexeme: String } From d0807072d7cfa0d997e59f6967e7815b5ac33a40 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 21:13:25 +0000 Subject: [PATCH 14/27] Regenerate std_integer.rs after Signedness lands in std.integer Adding Signedness to dag/std/integer.dag requires the emitted stage0 artifact to match; regen_verify_gate_passes was failing on the drift. Co-authored-by: Cursor --- src/v1/stage0/src/std_integer.rs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/v1/stage0/src/std_integer.rs b/src/v1/stage0/src/std_integer.rs index 82baeb6f9bf..f83adb0857c 100644 --- a/src/v1/stage0/src/std_integer.rs +++ b/src/v1/stage0/src/std_integer.rs @@ -1,6 +1,7 @@ // Generated by v1 compiler -- do not edit. // Source module: std.integer +use self::Signedness::*; pub use crate::std_algebra::{AbelianGroup, GroupCompletion}; pub use crate::std_induction::int_pow_bounded; pub use crate::std_machine_constraints::{Compose, MachineWidth, PointerWidth}; @@ -47,6 +48,15 @@ pub type Int = i64; pub type UInt = i64; +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum Signedness { + Signed, + Unsigned, +} + pub type IntPlatform = crate::std_machine_constraints::Compose< i64, crate::std_machine_constraints::MachineWidth, @@ -71,3 +81,8 @@ pub fn uint8_channel_inclusive_max_value_derived() -> Option { None => None, } } + +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct Signed; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct Unsigned; From 3a90fdf0fcd25156b5ba4079e3e38f61b214fdea Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 22:22:09 +0000 Subject: [PATCH 15/27] WIP: P3b language width tower collapse --- dag/std/interface_summary.dag | 7 +++ ...ompiler-guarantee-recovery-gap-analysis.md | 44 +++++++++++++++++++ src/v1/stage0/src/cli_run.rs | 25 +++++++++++ src/v1/stage0/src/std_interface_summary.rs | 17 +++++++ src/v2/lens/cost.dag | 2 +- 5 files changed, 94 insertions(+), 1 deletion(-) diff --git a/dag/std/interface_summary.dag b/dag/std/interface_summary.dag index 317b1082c12..7b04adde381 100644 --- a/dag/std/interface_summary.dag +++ b/dag/std/interface_summary.dag @@ -111,8 +111,15 @@ fn module_key(source_hash: ContentHash, direct_import_interface_hashes: List TypedModuleKey { content_hash_tagged( +======= +data typed_module_key_v1_seed_bridge_note: String = "Seed-retained hand-Rust bridge (review 45298; receipt extended review 45554): src/v1/stage0/src/cli_run.rs typed_module_content_key is the v1 host realization of std.interface_summary.module_key and typed_module_key — reconcile-path digest strings are coerced through std.content_hash.fnv1a64_structural_hex_digest (via local structural_from_wire) before the .dag authority runs, because the v1 store boundary still carries interface hashes as digest strings. Invalid wire (wrong length, non-lowercase hex) returns Absent and typed_module_content_key refuses with panic — never unchecked structural_content_hash. DELETE SCAFFOLD — not a new digest concept; string→Fnv1a64Structural coercion the authority already requires. CENSUS SHRINK — one call site (typed_module_content_key). WITNESS — cli_run typed_module_content_key_tests fnv1a64_structural_hex_digest_refuses_invalid_wire / fnv1a64_structural_hex_digest_accepts_valid_wire (discriminating RED: uppercase and short hex → None); key-term store controls unchanged. EXPLICIT DEFERRAL — dissolves when cross-entry typed-module memo routes through emitted typed_module_key end-to-end without cli_run string wrapping; ROADMAP row 'Make native materialization the shared execution kernel' (docs/plans/witness-realization-plan.md P3/P6) and gunbc.v1_deletion_plan ^witness_realization_kernel; aligns with docs/plans/cross-entry-typed-module-memo-sketch.md Half B." + +fn typed_module_key(interface_key: ModuleKey, compiler_identity: Fnv1a64Structural) -> TypedModuleKey { + content_hash_tagged_structural( +>>>>>>> Stashed changes tag: "typed-module-compiler", payload: content_hash_combine(left: interface_key, right: compiler_identity) ) diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md index 9ae7444f14d..6ffcd8bd576 100644 --- a/docs/plans/compiler-guarantee-recovery-gap-analysis.md +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -715,6 +715,7 @@ the population **derived from the census's path axes or completeness-witnessed a them**, so a strongest-path-only reading is a red, not an oversight); `GuaranteeMeasurement` (an executed probe/witness receipt, **with a named consumer in `Accepted`**); and `GuaranteeDisposition` **derived per path, never stored** — `Unmeasured | +<<<<<<< Updated upstream BelowFloor{evidence} | FrontierAccepted{diagnostic, accepted_boundary, evidence} | OnLadder{rung, evidence} | OutsideModeledGuarantee{reason}` — folded to class state as below-floor dominates, then frontier, then unmeasured, then the **minimum rung across @@ -729,6 +730,14 @@ no stored `current_rung` column, so a transcribed rung is *unrepresentable* rath lens-caught (corrected per review 45367: an earlier draft of this stage listed `current_rung` as a carrier field, which would have reintroduced exactly the rung-inflation class §1b forbids). What survives as checks: an `OnLadder` disposition's +======= +BelowFloor{evidence} | OnLadder{rung, evidence} | OutsideModeledGuarantee{reason}` — folded +to class state as below-floor dominates, then unmeasured, then the **minimum rung across +paths**. There is no stored `current_rung` column, so a transcribed rung is +*unrepresentable* rather than lens-caught (corrected per review 45367: an earlier draft of +this stage listed `current_rung` as a carrier field, which would have reintroduced exactly +the rung-inflation class §1b forbids). What survives as checks: an `OnLadder` disposition's +>>>>>>> Stashed changes evidence refs must execute (honesty — v2's generic self-grounding is the day-one below-target disposition), and a class below its ceiling with no `next_rung_trigger` reds (stall). The five recovered fragment-vocabularies (§3's lattice, `wall @@ -743,6 +752,7 @@ IS that thread's missing claims list, not a second taxonomy beside it; and per authority is `.dag` rows projected into DESIGN.md, never hand-edited prose. Historical claims enter `Required` + `Gap` (mode-2 rule, §2). +<<<<<<< Updated upstream **Stage 1c — baseline prevalence, anchored** (split out of the old Stage 7 per the first verdict; anchored per the post-merge verdict): the whole-corpus floor rerun bucketed by ladder position, keyed to the carrier's class ids — the honest *before* picture, pinned to @@ -751,6 +761,12 @@ implementation state). Content-addressing the baseline is what makes it reproduc the in-flight branches merge — requiring every implementation node to wait on an unanchored live-tree measurement would be fragile, so the walls sequence after the baseline *node* without racing the live tree. +======= +**Stage 1c — baseline prevalence, before any wall** (split out of the old Stage 7 per the +operator's verdict): the whole-corpus floor rerun bucketed by ladder position, keyed to the +carrier's class ids — the honest *before* picture. Each wall node's roadmap edge on the +baseline node encodes that a wall landing first would pollute it. +>>>>>>> Stashed changes **Stage 2 — close the ordinary premises (wall-now set):** method/callable existence; exact call labels and counts (the §4 application-arity row); return/`data`/field/generic @@ -764,6 +780,7 @@ which dual-path resolutions are the *same* primitive — otherwise `map` resolvi registry and algebra template reds the whole corpus on day one and the wall gets reverted exactly the way the 104 preserved the exemption. +<<<<<<< Updated upstream **Stage 2 measured amendment (2026-07-31, tidy-deer-730's receipts on OPEN gunbc#7484; sequencing re-ruled by the post-merge verdict):** the open candidate carries a narrow per-receiver method-existence wall over **kernel receivers** (six REDs/positive controls, @@ -780,6 +797,25 @@ one primitive represented twice from two genuinely ambiguous candidates, so it g encode exactly that: `floor-method-ambiguity-wall ← primitive-identity-join`, while `floor-method-existence-wall` follows the anchored baseline only. The two resolution defects are §11 item 8; receiver normalization is the wall's first slice. +======= +**Stage 2 measured amendment (2026-07-31, tidy-deer-730 on gunbc#7484):** a narrow +per-receiver method-existence wall over **kernel receivers** has landed (six REDs/positive +controls, regen divergence 0). What keeps it narrow, measured: (a) two receiver-type +resolution defects — a where-refinement alias arrives as its brand, unpeeled to the base; +a pattern-destructured coproduct payload arrives typed as the *variant name* rather than +the field type — and (b) the primitive-identity fork itself: the kernel algebra profiles +disagree with interpreter dispatch (`String` and `Map` declare `length` but not `count` +while the interpreter dispatches `length`/`count`/`size`). So the Stage-5 join is a +**prerequisite of the general method wall, not a follow-on** — the roadmap edges encode +`floor-method-existence-wall ← primitive-identity-join`, correcting this section's +original order; the two resolution defects are §11 item 8. + +**Stage 3 — one cardinality vertical slice** (§4b: connect the 2026-07-04 operator +direction + the scoped lattice plan + the manual value-level fold specimens; acceptance = +the operator's scenario refusing at the seam, with the nonempty-proof positive control +compiling; the construction-wall candidate is gated on the §11 item 1a `sole_constructor` +audit — a declared roadmap edge, not prose). +>>>>>>> Stashed changes **Stage 3 — one cardinality vertical slice** (§4b: connect the 2026-07-04 operator direction + the scoped lattice plan + the manual value-level fold specimens; acceptance = @@ -808,6 +844,7 @@ target-realization completeness — NOT zero-resolution, per the Stage-2 nuance) `v2.*`/`v1.compiler.*`, classify every failure, fix, delete; the unsourced 104 is neither a blocker nor a promise). +<<<<<<< Updated upstream **Stage 6b — the acceptance-completeness door (`compiler-accepted-obligation-closure`, added per the post-merge verdict):** the terminal P0 wall making the carrier the contract rather than observability — every `Required` guarantee path has exactly one live consumer, @@ -826,3 +863,10 @@ classifier — statically-decidable / runtime-value-dependent / external-boundar resource-budget / capability-not-grounded / interpreter-defect — re-run after the declared climbs land and **diffed against the anchored baseline**, so each wall's landing is a measured before/after receipt, never an assumed win. +======= +**Stage 7 — residual prevalence, measured last** (the baseline half moved to Stage 1c per +the operator's verdict): the same bucketing classifier — statically-decidable / +runtime-value-dependent / external-boundary / resource-budget / capability-not-grounded / +interpreter-defect — re-run after the declared climbs land and **diffed against the +baseline**, so each wall's landing is a measured before/after receipt, never an assumed win. +>>>>>>> Stashed changes diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 1a35be2de97..4b5d3934a88 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -4418,6 +4418,31 @@ mod typed_module_content_key_tests { ); }); } + + /// Discriminating controls for the string→`Fnv1a64Structural` coercion on the + /// `typed_module_content_key` bridge (review 45554; authority note + /// `std.interface_summary.typed_module_key_v1_seed_bridge_note`). + #[test] + fn fnv1a64_structural_hex_digest_refuses_invalid_wire() { + use super::fnv1a64_structural_hex_digest; + assert!( + fnv1a64_structural_hex_digest("0123456789ABCDEF".to_string()).is_none(), + "uppercase hex must refuse, not fold case" + ); + assert!( + fnv1a64_structural_hex_digest("0123456789abcde".to_string()).is_none(), + "short hex must refuse" + ); + } + + #[test] + fn fnv1a64_structural_hex_digest_accepts_valid_wire() { + use super::fnv1a64_structural_hex_digest; + assert!( + fnv1a64_structural_hex_digest("0123456789abcdef".to_string()).is_some(), + "valid 16-char lowercase hex must mint" + ); + } } #[cfg(test)] diff --git a/src/v1/stage0/src/std_interface_summary.rs b/src/v1/stage0/src/std_interface_summary.rs index 65eb9aa0646..55824a93794 100644 --- a/src/v1/stage0/src/std_interface_summary.rs +++ b/src/v1/stage0/src/std_interface_summary.rs @@ -161,8 +161,25 @@ pub fn typed_module_key_note() -> NonEmptyStr { CACHED.with(|c: &NonEmptyStr| c.clone()) } +<<<<<<< Updated upstream pub fn typed_module_key(interface_key: ContentHash, compiler_identity: NonEmptyStr) -> ContentHash { content_hash_tagged( +======= +pub fn typed_module_key_v1_seed_bridge_note() -> String { + thread_local! { + static CACHED: String = { + "Seed-retained hand-Rust bridge (review 45298; receipt extended review 45554): src/v1/stage0/src/cli_run.rs typed_module_content_key is the v1 host realization of std.interface_summary.module_key and typed_module_key — reconcile-path digest strings are coerced through std.content_hash.fnv1a64_structural_hex_digest (via local structural_from_wire) before the .dag authority runs, because the v1 store boundary still carries interface hashes as digest strings. Invalid wire (wrong length, non-lowercase hex) returns Absent and typed_module_content_key refuses with panic — never unchecked structural_content_hash. DELETE SCAFFOLD — not a new digest concept; string→Fnv1a64Structural coercion the authority already requires. CENSUS SHRINK — one call site (typed_module_content_key). WITNESS — cli_run typed_module_content_key_tests fnv1a64_structural_hex_digest_refuses_invalid_wire / fnv1a64_structural_hex_digest_accepts_valid_wire (discriminating RED: uppercase and short hex → None); key-term store controls unchanged. EXPLICIT DEFERRAL — dissolves when cross-entry typed-module memo routes through emitted typed_module_key end-to-end without cli_run string wrapping; ROADMAP row 'Make native materialization the shared execution kernel' (docs/plans/witness-realization-plan.md P3/P6) and gunbc.v1_deletion_plan ^witness_realization_kernel; aligns with docs/plans/cross-entry-typed-module-memo-sketch.md Half B.".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + +pub fn typed_module_key( + interface_key: Rc, + compiler_identity: Rc, +) -> Rc { + content_hash_tagged_structural( +>>>>>>> Stashed changes "typed-module-compiler".to_string(), content_hash_combine(interface_key.clone(), compiler_identity.clone()), ) diff --git a/src/v2/lens/cost.dag b/src/v2/lens/cost.dag index 5a27e8b32f8..f2a01f8e0b6 100644 --- a/src/v2/lens/cost.dag +++ b/src/v2/lens/cost.dag @@ -285,7 +285,7 @@ fn nonzero_nat_dominates(a: NonZeroNat, b: NonZeroNat) -> Bool { } fn nat_dominates(a: v2.std.nat.Nat, b: v2.std.nat.Nat) -> Bool { - match nat_compare(a: a, b: b) { + match v2.std.nat.nat_compare(a: a, b: b) { Greater => true Equal => true _ => false From 9038b2dc284d2c2a9e30ea615e99d5cacdd1d7ec Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 22:24:47 +0000 Subject: [PATCH 16/27] Fix CI: qualify nat_compare in cost.dag; drop stash conflict markers Whole-tree compile-clean after merging main exposed ambiguous nat_compare (v2.std.nat vs std.nat) once std.integer landed in the closure. Qualify the call site in v2.lens.cost. Also revert accidental merge-conflict markers left in interface_summary.dag, std_interface_summary.rs, and the guarantee recovery doc from a botched stash pop (3a90fdf). Co-authored-by: Cursor --- dag/std/interface_summary.dag | 7 --- ...ompiler-guarantee-recovery-gap-analysis.md | 44 ------------------- src/v1/stage0/src/std_interface_summary.rs | 17 ------- src/v2/lens/cost.dag | 2 +- 4 files changed, 1 insertion(+), 69 deletions(-) diff --git a/dag/std/interface_summary.dag b/dag/std/interface_summary.dag index 7b04adde381..317b1082c12 100644 --- a/dag/std/interface_summary.dag +++ b/dag/std/interface_summary.dag @@ -111,15 +111,8 @@ fn module_key(source_hash: ContentHash, direct_import_interface_hashes: List TypedModuleKey { content_hash_tagged( -======= -data typed_module_key_v1_seed_bridge_note: String = "Seed-retained hand-Rust bridge (review 45298; receipt extended review 45554): src/v1/stage0/src/cli_run.rs typed_module_content_key is the v1 host realization of std.interface_summary.module_key and typed_module_key — reconcile-path digest strings are coerced through std.content_hash.fnv1a64_structural_hex_digest (via local structural_from_wire) before the .dag authority runs, because the v1 store boundary still carries interface hashes as digest strings. Invalid wire (wrong length, non-lowercase hex) returns Absent and typed_module_content_key refuses with panic — never unchecked structural_content_hash. DELETE SCAFFOLD — not a new digest concept; string→Fnv1a64Structural coercion the authority already requires. CENSUS SHRINK — one call site (typed_module_content_key). WITNESS — cli_run typed_module_content_key_tests fnv1a64_structural_hex_digest_refuses_invalid_wire / fnv1a64_structural_hex_digest_accepts_valid_wire (discriminating RED: uppercase and short hex → None); key-term store controls unchanged. EXPLICIT DEFERRAL — dissolves when cross-entry typed-module memo routes through emitted typed_module_key end-to-end without cli_run string wrapping; ROADMAP row 'Make native materialization the shared execution kernel' (docs/plans/witness-realization-plan.md P3/P6) and gunbc.v1_deletion_plan ^witness_realization_kernel; aligns with docs/plans/cross-entry-typed-module-memo-sketch.md Half B." - -fn typed_module_key(interface_key: ModuleKey, compiler_identity: Fnv1a64Structural) -> TypedModuleKey { - content_hash_tagged_structural( ->>>>>>> Stashed changes tag: "typed-module-compiler", payload: content_hash_combine(left: interface_key, right: compiler_identity) ) diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md index 6ffcd8bd576..9ae7444f14d 100644 --- a/docs/plans/compiler-guarantee-recovery-gap-analysis.md +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -715,7 +715,6 @@ the population **derived from the census's path axes or completeness-witnessed a them**, so a strongest-path-only reading is a red, not an oversight); `GuaranteeMeasurement` (an executed probe/witness receipt, **with a named consumer in `Accepted`**); and `GuaranteeDisposition` **derived per path, never stored** — `Unmeasured | -<<<<<<< Updated upstream BelowFloor{evidence} | FrontierAccepted{diagnostic, accepted_boundary, evidence} | OnLadder{rung, evidence} | OutsideModeledGuarantee{reason}` — folded to class state as below-floor dominates, then frontier, then unmeasured, then the **minimum rung across @@ -730,14 +729,6 @@ no stored `current_rung` column, so a transcribed rung is *unrepresentable* rath lens-caught (corrected per review 45367: an earlier draft of this stage listed `current_rung` as a carrier field, which would have reintroduced exactly the rung-inflation class §1b forbids). What survives as checks: an `OnLadder` disposition's -======= -BelowFloor{evidence} | OnLadder{rung, evidence} | OutsideModeledGuarantee{reason}` — folded -to class state as below-floor dominates, then unmeasured, then the **minimum rung across -paths**. There is no stored `current_rung` column, so a transcribed rung is -*unrepresentable* rather than lens-caught (corrected per review 45367: an earlier draft of -this stage listed `current_rung` as a carrier field, which would have reintroduced exactly -the rung-inflation class §1b forbids). What survives as checks: an `OnLadder` disposition's ->>>>>>> Stashed changes evidence refs must execute (honesty — v2's generic self-grounding is the day-one below-target disposition), and a class below its ceiling with no `next_rung_trigger` reds (stall). The five recovered fragment-vocabularies (§3's lattice, `wall @@ -752,7 +743,6 @@ IS that thread's missing claims list, not a second taxonomy beside it; and per authority is `.dag` rows projected into DESIGN.md, never hand-edited prose. Historical claims enter `Required` + `Gap` (mode-2 rule, §2). -<<<<<<< Updated upstream **Stage 1c — baseline prevalence, anchored** (split out of the old Stage 7 per the first verdict; anchored per the post-merge verdict): the whole-corpus floor rerun bucketed by ladder position, keyed to the carrier's class ids — the honest *before* picture, pinned to @@ -761,12 +751,6 @@ implementation state). Content-addressing the baseline is what makes it reproduc the in-flight branches merge — requiring every implementation node to wait on an unanchored live-tree measurement would be fragile, so the walls sequence after the baseline *node* without racing the live tree. -======= -**Stage 1c — baseline prevalence, before any wall** (split out of the old Stage 7 per the -operator's verdict): the whole-corpus floor rerun bucketed by ladder position, keyed to the -carrier's class ids — the honest *before* picture. Each wall node's roadmap edge on the -baseline node encodes that a wall landing first would pollute it. ->>>>>>> Stashed changes **Stage 2 — close the ordinary premises (wall-now set):** method/callable existence; exact call labels and counts (the §4 application-arity row); return/`data`/field/generic @@ -780,7 +764,6 @@ which dual-path resolutions are the *same* primitive — otherwise `map` resolvi registry and algebra template reds the whole corpus on day one and the wall gets reverted exactly the way the 104 preserved the exemption. -<<<<<<< Updated upstream **Stage 2 measured amendment (2026-07-31, tidy-deer-730's receipts on OPEN gunbc#7484; sequencing re-ruled by the post-merge verdict):** the open candidate carries a narrow per-receiver method-existence wall over **kernel receivers** (six REDs/positive controls, @@ -797,25 +780,6 @@ one primitive represented twice from two genuinely ambiguous candidates, so it g encode exactly that: `floor-method-ambiguity-wall ← primitive-identity-join`, while `floor-method-existence-wall` follows the anchored baseline only. The two resolution defects are §11 item 8; receiver normalization is the wall's first slice. -======= -**Stage 2 measured amendment (2026-07-31, tidy-deer-730 on gunbc#7484):** a narrow -per-receiver method-existence wall over **kernel receivers** has landed (six REDs/positive -controls, regen divergence 0). What keeps it narrow, measured: (a) two receiver-type -resolution defects — a where-refinement alias arrives as its brand, unpeeled to the base; -a pattern-destructured coproduct payload arrives typed as the *variant name* rather than -the field type — and (b) the primitive-identity fork itself: the kernel algebra profiles -disagree with interpreter dispatch (`String` and `Map` declare `length` but not `count` -while the interpreter dispatches `length`/`count`/`size`). So the Stage-5 join is a -**prerequisite of the general method wall, not a follow-on** — the roadmap edges encode -`floor-method-existence-wall ← primitive-identity-join`, correcting this section's -original order; the two resolution defects are §11 item 8. - -**Stage 3 — one cardinality vertical slice** (§4b: connect the 2026-07-04 operator -direction + the scoped lattice plan + the manual value-level fold specimens; acceptance = -the operator's scenario refusing at the seam, with the nonempty-proof positive control -compiling; the construction-wall candidate is gated on the §11 item 1a `sole_constructor` -audit — a declared roadmap edge, not prose). ->>>>>>> Stashed changes **Stage 3 — one cardinality vertical slice** (§4b: connect the 2026-07-04 operator direction + the scoped lattice plan + the manual value-level fold specimens; acceptance = @@ -844,7 +808,6 @@ target-realization completeness — NOT zero-resolution, per the Stage-2 nuance) `v2.*`/`v1.compiler.*`, classify every failure, fix, delete; the unsourced 104 is neither a blocker nor a promise). -<<<<<<< Updated upstream **Stage 6b — the acceptance-completeness door (`compiler-accepted-obligation-closure`, added per the post-merge verdict):** the terminal P0 wall making the carrier the contract rather than observability — every `Required` guarantee path has exactly one live consumer, @@ -863,10 +826,3 @@ classifier — statically-decidable / runtime-value-dependent / external-boundar resource-budget / capability-not-grounded / interpreter-defect — re-run after the declared climbs land and **diffed against the anchored baseline**, so each wall's landing is a measured before/after receipt, never an assumed win. -======= -**Stage 7 — residual prevalence, measured last** (the baseline half moved to Stage 1c per -the operator's verdict): the same bucketing classifier — statically-decidable / -runtime-value-dependent / external-boundary / resource-budget / capability-not-grounded / -interpreter-defect — re-run after the declared climbs land and **diffed against the -baseline**, so each wall's landing is a measured before/after receipt, never an assumed win. ->>>>>>> Stashed changes diff --git a/src/v1/stage0/src/std_interface_summary.rs b/src/v1/stage0/src/std_interface_summary.rs index 55824a93794..65eb9aa0646 100644 --- a/src/v1/stage0/src/std_interface_summary.rs +++ b/src/v1/stage0/src/std_interface_summary.rs @@ -161,25 +161,8 @@ pub fn typed_module_key_note() -> NonEmptyStr { CACHED.with(|c: &NonEmptyStr| c.clone()) } -<<<<<<< Updated upstream pub fn typed_module_key(interface_key: ContentHash, compiler_identity: NonEmptyStr) -> ContentHash { content_hash_tagged( -======= -pub fn typed_module_key_v1_seed_bridge_note() -> String { - thread_local! { - static CACHED: String = { - "Seed-retained hand-Rust bridge (review 45298; receipt extended review 45554): src/v1/stage0/src/cli_run.rs typed_module_content_key is the v1 host realization of std.interface_summary.module_key and typed_module_key — reconcile-path digest strings are coerced through std.content_hash.fnv1a64_structural_hex_digest (via local structural_from_wire) before the .dag authority runs, because the v1 store boundary still carries interface hashes as digest strings. Invalid wire (wrong length, non-lowercase hex) returns Absent and typed_module_content_key refuses with panic — never unchecked structural_content_hash. DELETE SCAFFOLD — not a new digest concept; string→Fnv1a64Structural coercion the authority already requires. CENSUS SHRINK — one call site (typed_module_content_key). WITNESS — cli_run typed_module_content_key_tests fnv1a64_structural_hex_digest_refuses_invalid_wire / fnv1a64_structural_hex_digest_accepts_valid_wire (discriminating RED: uppercase and short hex → None); key-term store controls unchanged. EXPLICIT DEFERRAL — dissolves when cross-entry typed-module memo routes through emitted typed_module_key end-to-end without cli_run string wrapping; ROADMAP row 'Make native materialization the shared execution kernel' (docs/plans/witness-realization-plan.md P3/P6) and gunbc.v1_deletion_plan ^witness_realization_kernel; aligns with docs/plans/cross-entry-typed-module-memo-sketch.md Half B.".to_string() - }; - } - CACHED.with(|c: &String| c.clone()) -} - -pub fn typed_module_key( - interface_key: Rc, - compiler_identity: Rc, -) -> Rc { - content_hash_tagged_structural( ->>>>>>> Stashed changes "typed-module-compiler".to_string(), content_hash_combine(interface_key.clone(), compiler_identity.clone()), ) diff --git a/src/v2/lens/cost.dag b/src/v2/lens/cost.dag index f2a01f8e0b6..27d9bf2d7b5 100644 --- a/src/v2/lens/cost.dag +++ b/src/v2/lens/cost.dag @@ -46,7 +46,7 @@ import v2.std.node { Value, fold_node } -import v2.std.nat { Nat, Succ, Zero, nat_add, nat_compare } +import v2.std.nat { Nat, Succ, Zero, nat_add } import v2.std.witness { Holds, Violates, Witness } type SizeVariable { From 121fca8f4fe57347ba5c2de1920442a90f4d1840 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 22:27:17 +0000 Subject: [PATCH 17/27] Restore out-of-lane files contaminated by shared stash pop Revert cli_run.rs (Fnv1a64Structural bridge tests from another lane) and cost.dag (nat_compare qualification) to origin/main. Re-affirm interface_summary authority files match main with zero conflict markers. Co-authored-by: Cursor --- src/v1/stage0/src/cli_run.rs | 25 ------------------------- src/v2/lens/cost.dag | 4 ++-- 2 files changed, 2 insertions(+), 27 deletions(-) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 4b5d3934a88..1a35be2de97 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -4418,31 +4418,6 @@ mod typed_module_content_key_tests { ); }); } - - /// Discriminating controls for the string→`Fnv1a64Structural` coercion on the - /// `typed_module_content_key` bridge (review 45554; authority note - /// `std.interface_summary.typed_module_key_v1_seed_bridge_note`). - #[test] - fn fnv1a64_structural_hex_digest_refuses_invalid_wire() { - use super::fnv1a64_structural_hex_digest; - assert!( - fnv1a64_structural_hex_digest("0123456789ABCDEF".to_string()).is_none(), - "uppercase hex must refuse, not fold case" - ); - assert!( - fnv1a64_structural_hex_digest("0123456789abcde".to_string()).is_none(), - "short hex must refuse" - ); - } - - #[test] - fn fnv1a64_structural_hex_digest_accepts_valid_wire() { - use super::fnv1a64_structural_hex_digest; - assert!( - fnv1a64_structural_hex_digest("0123456789abcdef".to_string()).is_some(), - "valid 16-char lowercase hex must mint" - ); - } } #[cfg(test)] diff --git a/src/v2/lens/cost.dag b/src/v2/lens/cost.dag index 27d9bf2d7b5..5a27e8b32f8 100644 --- a/src/v2/lens/cost.dag +++ b/src/v2/lens/cost.dag @@ -46,7 +46,7 @@ import v2.std.node { Value, fold_node } -import v2.std.nat { Nat, Succ, Zero, nat_add } +import v2.std.nat { Nat, Succ, Zero, nat_add, nat_compare } import v2.std.witness { Holds, Violates, Witness } type SizeVariable { @@ -285,7 +285,7 @@ fn nonzero_nat_dominates(a: NonZeroNat, b: NonZeroNat) -> Bool { } fn nat_dominates(a: v2.std.nat.Nat, b: v2.std.nat.Nat) -> Bool { - match v2.std.nat.nat_compare(a: a, b: b) { + match nat_compare(a: a, b: b) { Greater => true Equal => true _ => false From 66c35fa4d7cc841799e354534f9e222039ec86e3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 22:47:48 +0000 Subject: [PATCH 18/27] Re-export Signed/Unsigned from v2.std.integer after Signedness lift Import std.integer variant arms alongside Signedness so interval_derivation_test.dag consumers keep resolve access (review 45720). Co-authored-by: Cursor --- src/v2/std/integer.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/v2/std/integer.dag b/src/v2/std/integer.dag index 26c08cae0c9..e1136e57056 100644 --- a/src/v2/std/integer.dag +++ b/src/v2/std/integer.dag @@ -17,7 +17,7 @@ import v2.std.optional { import v2.std.diagnostic { Correction, Diagnostic, ExternalContractUnknown, Locus, NoCorrectionReason, Outcome, Accepted, None, Rejected, diagnostics_singleton, node_locus, outcome_accepted, outcome_rejected, port_locus, Unavailable } import v2.std.node { Atom, Conj, Edge, Named, Node, Symbol, TypeNode, SyntheticOccurrence, is_empty_conj_root } import v2.std.node_query { find_named_child } -import std.integer { Signedness } +import std.integer { Signedness, Signed, Unsigned } import v2.std.machine { Byte, MachineWidth, From 477db51b546e350c52f47c5e245350a9a0bd3e77 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 23:15:46 +0000 Subject: [PATCH 19/27] WIP: P3b language width tower collapse --- dag/std/integer.dag | 2 ++ src/v2/lens/cost.dag | 4 ++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/dag/std/integer.dag b/dag/std/integer.dag index fa679a13a0b..1212cd414e4 100644 --- a/dag/std/integer.dag +++ b/dag/std/integer.dag @@ -25,6 +25,8 @@ type Signedness = Signed | Unsigned +data std_integer_std_nat_fork_note: String = "PR1 Signedness lift imports std.nat here, co-resolving std.nat with v2.std.nat in whole-tree compile-clean closures. Known two-std-trees fork: std.nat.Nat = CommutativeSemiring with std.nat.nat_compare versus v2.std.nat.Nat = Zero|Succ with v2.std.nat.nat_compare — not consolidated in this PR. Dissolve-on: two-std-trees consolidation lands a single Nat authority and retires the parallel compare fns; until then ambiguous bare references must qualify by containment path (namespace-resolution-design section 13)." + type IntPlatform = Compose> type UIntPlatform = Compose> diff --git a/src/v2/lens/cost.dag b/src/v2/lens/cost.dag index 5a27e8b32f8..27d9bf2d7b5 100644 --- a/src/v2/lens/cost.dag +++ b/src/v2/lens/cost.dag @@ -46,7 +46,7 @@ import v2.std.node { Value, fold_node } -import v2.std.nat { Nat, Succ, Zero, nat_add, nat_compare } +import v2.std.nat { Nat, Succ, Zero, nat_add } import v2.std.witness { Holds, Violates, Witness } type SizeVariable { @@ -285,7 +285,7 @@ fn nonzero_nat_dominates(a: NonZeroNat, b: NonZeroNat) -> Bool { } fn nat_dominates(a: v2.std.nat.Nat, b: v2.std.nat.Nat) -> Bool { - match nat_compare(a: a, b: b) { + match v2.std.nat.nat_compare(a: a, b: b) { Greater => true Equal => true _ => false From a52f973bc315fe566cad8f2f1607290384c73fec Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 31 Jul 2026 23:18:52 +0000 Subject: [PATCH 20/27] Qualify v2.std.nat.nat_compare in cost.dag; note std.nat fork Per operator ruling msg_69df5ed6: ambiguous bare nat_compare at cost.dag:288 is under-specified once std.integer imports std.nat; qualifying by containment path is construction, not a workaround. Record two-std-trees nat_compare fork on std.integer with dissolve-on trigger; regen std_integer.rs for the carrier note. Co-authored-by: Cursor --- src/v1/stage0/src/std_integer.rs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/v1/stage0/src/std_integer.rs b/src/v1/stage0/src/std_integer.rs index f83adb0857c..9376826d79f 100644 --- a/src/v1/stage0/src/std_integer.rs +++ b/src/v1/stage0/src/std_integer.rs @@ -57,6 +57,15 @@ pub enum Signedness { Unsigned, } +pub fn std_integer_std_nat_fork_note() -> String { + thread_local! { + static CACHED: String = { + "PR1 Signedness lift imports std.nat here, co-resolving std.nat with v2.std.nat in whole-tree compile-clean closures. Known two-std-trees fork: std.nat.Nat = CommutativeSemiring with std.nat.nat_compare versus v2.std.nat.Nat = Zero|Succ with v2.std.nat.nat_compare — not consolidated in this PR. Dissolve-on: two-std-trees consolidation lands a single Nat authority and retires the parallel compare fns; until then ambiguous bare references must qualify by containment path (namespace-resolution-design section 13).".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + pub type IntPlatform = crate::std_machine_constraints::Compose< i64, crate::std_machine_constraints::MachineWidth, From a59f8a88ef3a6002d99fe616797be445ca2a3774 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 1 Aug 2026 00:07:09 +0000 Subject: [PATCH 21/27] WIP: P3b language width tower collapse --- src/v2/test/claim/bash_program_fold_support.dag | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/v2/test/claim/bash_program_fold_support.dag b/src/v2/test/claim/bash_program_fold_support.dag index 0b71852b920..107309e03de 100644 --- a/src/v2/test/claim/bash_program_fold_support.dag +++ b/src/v2/test/claim/bash_program_fold_support.dag @@ -157,7 +157,7 @@ fn bash_program_fixture_ensure_bin_specials(var_name: String, bin_name: String) produces: [BuildArtifact { path: bin_path, name: bin_name }] ) list_append( - xs: [ + left: [ bash_program_fold_tag_assign(node: bash_program_fixture_assign_root_node()), bash_program_fold_tag_assign( node: bash_build_assign( @@ -178,7 +178,7 @@ fn bash_program_fixture_ensure_bin_specials(var_name: String, bin_name: String) ) ) ], - ys: bash_program_fold_tag_if_nodes(nodes: verify_nodes) + right: bash_program_fold_tag_if_nodes(nodes: verify_nodes) ) } @@ -190,8 +190,8 @@ fn bash_program_fixture_witness_bin_specials( let root = bash_build_word_var(name: "ROOT") let invoke = bash_build_word_var(name: var_name) list_append( - xs: bash_program_fixture_ensure_bin_specials(var_name: var_name, bin_name: bin_name), - ys: [ + left: bash_program_fixture_ensure_bin_specials(var_name: var_name, bin_name: bin_name), + right: [ bash_program_fold_tag_command( node: bash_build_command_from_word_nodes(words: [ bash_build_word_lit(text: "cd"), @@ -201,8 +201,8 @@ fn bash_program_fixture_witness_bin_specials( bash_program_fold_tag_command( node: bash_build_command_from_word_nodes( words: list_append( - xs: [invoke], - ys: list_map(xs: args, f: fn(a) { bash_build_word_lit(text: a) }) + left: [invoke], + right: list_map(xs: args, f: fn(a) { bash_build_word_lit(text: a) }) ) ) ) @@ -212,8 +212,8 @@ fn bash_program_fixture_witness_bin_specials( fn bash_program_fixture_gunbc_claims_specials() -> List { list_append( - xs: bash_program_fixture_ensure_bin_specials(var_name: "GUNBC", bin_name: "gunbc"), - ys: [ + left: bash_program_fixture_ensure_bin_specials(var_name: "GUNBC", bin_name: "gunbc"), + right: [ bash_program_fold_tag_command( node: bash_build_command_from_word_nodes(words: [ bash_build_word_var(name: "GUNBC"), From dc58ff2383dfaf8ae76c3d0ef049902dd6dd702a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 1 Aug 2026 00:24:59 +0000 Subject: [PATCH 22/27] Bound std_integer_std_nat_fork_note for review 45763. Add owner/lane/interim/bound/dissolve-on fields to the two-std-trees Nat fork disposition so the Signedness lift documents tracked debt without claiming consolidation in this PR. Co-authored-by: Cursor --- dag/std/integer.dag | 2 +- src/v1/stage0/src/std_integer.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/dag/std/integer.dag b/dag/std/integer.dag index 1212cd414e4..ddf4d51ba17 100644 --- a/dag/std/integer.dag +++ b/dag/std/integer.dag @@ -25,7 +25,7 @@ type Signedness = Signed | Unsigned -data std_integer_std_nat_fork_note: String = "PR1 Signedness lift imports std.nat here, co-resolving std.nat with v2.std.nat in whole-tree compile-clean closures. Known two-std-trees fork: std.nat.Nat = CommutativeSemiring with std.nat.nat_compare versus v2.std.nat.Nat = Zero|Succ with v2.std.nat.nat_compare — not consolidated in this PR. Dissolve-on: two-std-trees consolidation lands a single Nat authority and retires the parallel compare fns; until then ambiguous bare references must qualify by containment path (namespace-resolution-design section 13)." +data std_integer_std_nat_fork_note: String = "owner: namespace-only resolution lane (docs/plans/namespace-resolution-design.md). lane: two-std-trees Nat/nat_compare co-resolution — std.integer Signedness lift imports std.nat here, so whole-tree compile-clean closures co-resolve std.nat (Nat = CommutativeSemiring, std.nat.nat_compare) with v2.std.nat (Nat = Zero|Succ, v2.std.nat.nat_compare). interim: parallel authorities stay live; ambiguous bare Nat/nat_compare references qualify by containment path (namespace-resolution-design section 13). bound: this PR does not consolidate; it qualifies only closure-surfaced bare references (v2.std.nat.nat_compare in v2.lens.cost), not a corpus-wide sweep. dissolve-on: feature:two-std-trees-nat-consolidation — single Nat authority retires both nat_compare fns and deletes this note." type IntPlatform = Compose> type UIntPlatform = Compose> diff --git a/src/v1/stage0/src/std_integer.rs b/src/v1/stage0/src/std_integer.rs index 9376826d79f..df8aa32a372 100644 --- a/src/v1/stage0/src/std_integer.rs +++ b/src/v1/stage0/src/std_integer.rs @@ -60,7 +60,7 @@ pub enum Signedness { pub fn std_integer_std_nat_fork_note() -> String { thread_local! { static CACHED: String = { - "PR1 Signedness lift imports std.nat here, co-resolving std.nat with v2.std.nat in whole-tree compile-clean closures. Known two-std-trees fork: std.nat.Nat = CommutativeSemiring with std.nat.nat_compare versus v2.std.nat.Nat = Zero|Succ with v2.std.nat.nat_compare — not consolidated in this PR. Dissolve-on: two-std-trees consolidation lands a single Nat authority and retires the parallel compare fns; until then ambiguous bare references must qualify by containment path (namespace-resolution-design section 13).".to_string() + "owner: namespace-only resolution lane (docs/plans/namespace-resolution-design.md). lane: two-std-trees Nat/nat_compare co-resolution — std.integer Signedness lift imports std.nat here, so whole-tree compile-clean closures co-resolve std.nat (Nat = CommutativeSemiring, std.nat.nat_compare) with v2.std.nat (Nat = Zero|Succ, v2.std.nat.nat_compare). interim: parallel authorities stay live; ambiguous bare Nat/nat_compare references qualify by containment path (namespace-resolution-design section 13). bound: this PR does not consolidate; it qualifies only closure-surfaced bare references (v2.std.nat.nat_compare in v2.lens.cost), not a corpus-wide sweep. dissolve-on: feature:two-std-trees-nat-consolidation — single Nat authority retires both nat_compare fns and deletes this note.".to_string() }; } CACHED.with(|c: &String| c.clone()) From 4cc930ad7ee68fbbf74c9cb9b7545c70bae6f8a5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 1 Aug 2026 00:25:57 +0000 Subject: [PATCH 23/27] Add bound-on-deferral clause to std_integer_std_nat_fork_note. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Restore fork description and dissolve-on verbatim; add operator-dispatch disposition and consumer-bound clause per review 45763 ruling. No owner named — consolidation awaits operator dispatch. Co-authored-by: Cursor --- dag/std/integer.dag | 2 +- src/v1/stage0/src/std_integer.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/dag/std/integer.dag b/dag/std/integer.dag index ddf4d51ba17..95bd1ebe7fa 100644 --- a/dag/std/integer.dag +++ b/dag/std/integer.dag @@ -25,7 +25,7 @@ type Signedness = Signed | Unsigned -data std_integer_std_nat_fork_note: String = "owner: namespace-only resolution lane (docs/plans/namespace-resolution-design.md). lane: two-std-trees Nat/nat_compare co-resolution — std.integer Signedness lift imports std.nat here, so whole-tree compile-clean closures co-resolve std.nat (Nat = CommutativeSemiring, std.nat.nat_compare) with v2.std.nat (Nat = Zero|Succ, v2.std.nat.nat_compare). interim: parallel authorities stay live; ambiguous bare Nat/nat_compare references qualify by containment path (namespace-resolution-design section 13). bound: this PR does not consolidate; it qualifies only closure-surfaced bare references (v2.std.nat.nat_compare in v2.lens.cost), not a corpus-wide sweep. dissolve-on: feature:two-std-trees-nat-consolidation — single Nat authority retires both nat_compare fns and deletes this note." +data std_integer_std_nat_fork_note: String = "PR1 Signedness lift imports std.nat here, co-resolving std.nat with v2.std.nat in whole-tree compile-clean closures. Known two-std-trees fork: std.nat.Nat = CommutativeSemiring with std.nat.nat_compare versus v2.std.nat.Nat = Zero|Succ with v2.std.nat.nat_compare — not consolidated in this PR. Dissolve-on: two-std-trees consolidation lands a single Nat authority and retires the parallel compare fns; until then ambiguous bare references must qualify by containment path (namespace-resolution-design section 13). Disposition: awaiting an operator dispatch decision — not deferred work; a corpus-wide std carrier consolidation cannot be self-assigned by the session that found it, so the trigger and acceptance condition above are fixed and what is missing is only the dispatch; naming a fabricated owner would assert an ownership fact that is not true. The bound on the deferral, which is what keeps it tracked rather than parked: 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." type IntPlatform = Compose> type UIntPlatform = Compose> diff --git a/src/v1/stage0/src/std_integer.rs b/src/v1/stage0/src/std_integer.rs index df8aa32a372..d6bdc718e96 100644 --- a/src/v1/stage0/src/std_integer.rs +++ b/src/v1/stage0/src/std_integer.rs @@ -60,7 +60,7 @@ pub enum Signedness { pub fn std_integer_std_nat_fork_note() -> String { thread_local! { static CACHED: String = { - "owner: namespace-only resolution lane (docs/plans/namespace-resolution-design.md). lane: two-std-trees Nat/nat_compare co-resolution — std.integer Signedness lift imports std.nat here, so whole-tree compile-clean closures co-resolve std.nat (Nat = CommutativeSemiring, std.nat.nat_compare) with v2.std.nat (Nat = Zero|Succ, v2.std.nat.nat_compare). interim: parallel authorities stay live; ambiguous bare Nat/nat_compare references qualify by containment path (namespace-resolution-design section 13). bound: this PR does not consolidate; it qualifies only closure-surfaced bare references (v2.std.nat.nat_compare in v2.lens.cost), not a corpus-wide sweep. dissolve-on: feature:two-std-trees-nat-consolidation — single Nat authority retires both nat_compare fns and deletes this note.".to_string() + "PR1 Signedness lift imports std.nat here, co-resolving std.nat with v2.std.nat in whole-tree compile-clean closures. Known two-std-trees fork: std.nat.Nat = CommutativeSemiring with std.nat.nat_compare versus v2.std.nat.Nat = Zero|Succ with v2.std.nat.nat_compare — not consolidated in this PR. Dissolve-on: two-std-trees consolidation lands a single Nat authority and retires the parallel compare fns; until then ambiguous bare references must qualify by containment path (namespace-resolution-design section 13). Disposition: awaiting an operator dispatch decision — not deferred work; a corpus-wide std carrier consolidation cannot be self-assigned by the session that found it, so the trigger and acceptance condition above are fixed and what is missing is only the dispatch; naming a fabricated owner would assert an ownership fact that is not true. The bound on the deferral, which is what keeps it tracked rather than parked: 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.".to_string() }; } CACHED.with(|c: &String| c.clone()) From 3af1e48121be5785bd0b741976a1e99083dbad10 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 1 Aug 2026 01:26:31 +0000 Subject: [PATCH 24/27] WIP: P3b language width tower collapse --- src/v2/extdeps/languages/lean.dag | 169 ++++++++++-------- src/v2/extdeps/languages/verilog.dag | 2 + ...n_bit_width_admissibility_witness_test.dag | 17 +- 3 files changed, 110 insertions(+), 78 deletions(-) diff --git a/src/v2/extdeps/languages/lean.dag b/src/v2/extdeps/languages/lean.dag index ba94e4f951b..1e2f54abe35 100644 --- a/src/v2/extdeps/languages/lean.dag +++ b/src/v2/extdeps/languages/lean.dag @@ -183,24 +183,22 @@ type LeanProofCheckSemantics { proof_irrelevance_for_propositions: Bool } -data lean_bit_width_admissibility_note: String = "Lean fixed-precision integers: width axis is std.measure.BitWidth admitted via LeanBitWidthAdmission into LeanAdmittedBitWidth (construction wall — raw BitWidth cannot reach FixedIntScalar); platform word is LeanPlatformWord on the PointerWidth axis. Signedness is std.integer.Signedness, not LeanIntKind." +data lean_bit_width_admissibility_note: String = "Lean fixed-precision integers: width axis is std.measure.BitWidth; lean_admit_bit_width is the admission boundary producing LeanBitWidthAccepted with LeanAdmittedBitWidth or LeanBitWidthRefused pinning the observed width. Honest rung: accepted refinement with executing refusal (witness lean_bit_width_admissibility_witness_test) — not structural impossibility; catalog fixed widths route through the admission boundary. Platform word is LeanPlatformWord on the PointerWidth axis. Signedness is std.integer.Signedness, not LeanIntKind." -type LeanAdmittedBitWidth - = LeanAdmitWidth8 - | LeanAdmitWidth16 - | LeanAdmitWidth32 - | LeanAdmitWidth64 +type LeanAdmittedBitWidth { + width: BitWidth +} type LeanBitWidthAdmission = LeanBitWidthAccepted { width: LeanAdmittedBitWidth } | LeanBitWidthRefused { width: BitWidth } type LeanIntegerWidth - = LeanFixedWidth { width: LeanAdmittedBitWidth } + = LeanFixedWidth { admission: LeanBitWidthAccepted } | LeanPlatformWord type LeanScalar - = FixedIntScalar { signedness: Signedness, width: LeanIntegerWidth } + = LeanIntegerScalar { signedness: Signedness, width: LeanIntegerWidth } | BoolScalar type LeanPrimitiveFacts { @@ -209,58 +207,84 @@ type LeanPrimitiveFacts { representation: Symbol } -data lean_facts_int8: LeanPrimitiveFacts = LeanPrimitiveFacts { - surface_spelling: ^lean_surface_spelling_int8, - scalar: FixedIntScalar { signedness: Signed, width: LeanFixedWidth { width: LeanAdmitWidth8 } }, - representation: ^lean_repr_fixed_precision_integer +fn lean_catalog_fixed_width(count: Nat) -> LeanIntegerWidth { + match lean_admit_bit_width(width: bit_width(count: count)) { + LeanBitWidthAccepted { width: admitted } => + LeanFixedWidth { admission: LeanBitWidthAccepted { width: admitted } } + LeanBitWidthRefused { width: _ } => LeanPlatformWord + } } -data lean_facts_int16: LeanPrimitiveFacts = LeanPrimitiveFacts { - surface_spelling: ^lean_surface_spelling_int16, - scalar: FixedIntScalar { signedness: Signed, width: LeanFixedWidth { width: LeanAdmitWidth16 } }, - representation: ^lean_repr_fixed_precision_integer +fn lean_facts_int8() -> LeanPrimitiveFacts { + LeanPrimitiveFacts { + surface_spelling: ^lean_surface_spelling_int8, + scalar: LeanIntegerScalar { signedness: Signed, width: lean_catalog_fixed_width(count: 8) }, + representation: ^lean_repr_fixed_precision_integer + } } -data lean_facts_int32: LeanPrimitiveFacts = LeanPrimitiveFacts { - surface_spelling: ^lean_surface_spelling_int32, - scalar: FixedIntScalar { signedness: Signed, width: LeanFixedWidth { width: LeanAdmitWidth32 } }, - representation: ^lean_repr_fixed_precision_integer +fn lean_facts_int16() -> LeanPrimitiveFacts { + LeanPrimitiveFacts { + surface_spelling: ^lean_surface_spelling_int16, + scalar: LeanIntegerScalar { signedness: Signed, width: lean_catalog_fixed_width(count: 16) }, + representation: ^lean_repr_fixed_precision_integer + } } -data lean_facts_int64: LeanPrimitiveFacts = LeanPrimitiveFacts { - surface_spelling: ^lean_surface_spelling_int64, - scalar: FixedIntScalar { signedness: Signed, width: LeanFixedWidth { width: LeanAdmitWidth64 } }, - representation: ^lean_repr_fixed_precision_integer +fn lean_facts_int32() -> LeanPrimitiveFacts { + LeanPrimitiveFacts { + surface_spelling: ^lean_surface_spelling_int32, + scalar: LeanIntegerScalar { signedness: Signed, width: lean_catalog_fixed_width(count: 32) }, + representation: ^lean_repr_fixed_precision_integer + } } -data lean_facts_uint8: LeanPrimitiveFacts = LeanPrimitiveFacts { - surface_spelling: ^lean_surface_spelling_uint8, - scalar: FixedIntScalar { signedness: Unsigned, width: LeanFixedWidth { width: LeanAdmitWidth8 } }, - representation: ^lean_repr_fixed_precision_integer +fn lean_facts_int64() -> LeanPrimitiveFacts { + LeanPrimitiveFacts { + surface_spelling: ^lean_surface_spelling_int64, + scalar: LeanIntegerScalar { signedness: Signed, width: lean_catalog_fixed_width(count: 64) }, + representation: ^lean_repr_fixed_precision_integer + } } -data lean_facts_uint16: LeanPrimitiveFacts = LeanPrimitiveFacts { - surface_spelling: ^lean_surface_spelling_uint16, - scalar: FixedIntScalar { signedness: Unsigned, width: LeanFixedWidth { width: LeanAdmitWidth16 } }, - representation: ^lean_repr_fixed_precision_integer +fn lean_facts_uint8() -> LeanPrimitiveFacts { + LeanPrimitiveFacts { + surface_spelling: ^lean_surface_spelling_uint8, + scalar: LeanIntegerScalar { signedness: Unsigned, width: lean_catalog_fixed_width(count: 8) }, + representation: ^lean_repr_fixed_precision_integer + } } -data lean_facts_uint32: LeanPrimitiveFacts = LeanPrimitiveFacts { - surface_spelling: ^lean_surface_spelling_uint32, - scalar: FixedIntScalar { signedness: Unsigned, width: LeanFixedWidth { width: LeanAdmitWidth32 } }, - representation: ^lean_repr_fixed_precision_integer +fn lean_facts_uint16() -> LeanPrimitiveFacts { + LeanPrimitiveFacts { + surface_spelling: ^lean_surface_spelling_uint16, + scalar: LeanIntegerScalar { signedness: Unsigned, width: lean_catalog_fixed_width(count: 16) }, + representation: ^lean_repr_fixed_precision_integer + } } -data lean_facts_uint64: LeanPrimitiveFacts = LeanPrimitiveFacts { - surface_spelling: ^lean_surface_spelling_uint64, - scalar: FixedIntScalar { signedness: Unsigned, width: LeanFixedWidth { width: LeanAdmitWidth64 } }, - representation: ^lean_repr_fixed_precision_integer +fn lean_facts_uint32() -> LeanPrimitiveFacts { + LeanPrimitiveFacts { + surface_spelling: ^lean_surface_spelling_uint32, + scalar: LeanIntegerScalar { signedness: Unsigned, width: lean_catalog_fixed_width(count: 32) }, + representation: ^lean_repr_fixed_precision_integer + } } -data lean_facts_usize: LeanPrimitiveFacts = LeanPrimitiveFacts { - surface_spelling: ^lean_surface_spelling_usize, - scalar: FixedIntScalar { signedness: Unsigned, width: LeanPlatformWord }, - representation: ^lean_repr_usize_platform_word +fn lean_facts_uint64() -> LeanPrimitiveFacts { + LeanPrimitiveFacts { + surface_spelling: ^lean_surface_spelling_uint64, + scalar: LeanIntegerScalar { signedness: Unsigned, width: lean_catalog_fixed_width(count: 64) }, + representation: ^lean_repr_fixed_precision_integer + } +} + +fn lean_facts_usize() -> LeanPrimitiveFacts { + LeanPrimitiveFacts { + surface_spelling: ^lean_surface_spelling_usize, + scalar: LeanIntegerScalar { signedness: Unsigned, width: LeanPlatformWord }, + representation: ^lean_repr_usize_platform_word + } } data lean_facts_bool: LeanPrimitiveFacts = LeanPrimitiveFacts { @@ -271,15 +295,15 @@ data lean_facts_bool: LeanPrimitiveFacts = LeanPrimitiveFacts { data lean_source_text: String = "def dec (n : Int32) : Int32 := n - 1\n termination_by n" data lean_primitive_facts_catalog: List = [ - lean_facts_int8, - lean_facts_int16, - lean_facts_int32, - lean_facts_int64, - lean_facts_uint8, - lean_facts_uint16, - lean_facts_uint32, - lean_facts_uint64, - lean_facts_usize, + lean_facts_int8(), + lean_facts_int16(), + lean_facts_int32(), + lean_facts_int64(), + lean_facts_uint8(), + lean_facts_uint16(), + lean_facts_uint32(), + lean_facts_uint64(), + lean_facts_usize(), lean_facts_bool ] @@ -306,14 +330,8 @@ fn lean_signedness_node(signedness: Signedness) -> Node { fn lean_admit_bit_width(width: BitWidth) -> LeanBitWidthAdmission { let n = bit_width_count(width) - if n == 8 { - LeanBitWidthAccepted { width: LeanAdmitWidth8 } - } else if n == 16 { - LeanBitWidthAccepted { width: LeanAdmitWidth16 } - } else if n == 32 { - LeanBitWidthAccepted { width: LeanAdmitWidth32 } - } else if n == 64 { - LeanBitWidthAccepted { width: LeanAdmitWidth64 } + if n == 8 || n == 16 || n == 32 || n == 64 { + LeanBitWidthAccepted { width: LeanAdmittedBitWidth { width: width } } } else { LeanBitWidthRefused { width: width } } @@ -323,25 +341,32 @@ fn lean_platform_word_width_node() -> Node { lean_inhabitant_atom(id: ^lean_tag_pointer) } -fn lean_admitted_bit_width_node(width: LeanAdmittedBitWidth) -> Node { - match width { - LeanAdmitWidth8 => lean_inhabitant_atom(id: ^lean_tag_bits8) - LeanAdmitWidth16 => lean_inhabitant_atom(id: ^lean_tag_bits16) - LeanAdmitWidth32 => lean_inhabitant_atom(id: ^lean_tag_bits32) - LeanAdmitWidth64 => lean_inhabitant_atom(id: ^lean_tag_bits64) +fn lean_admitted_bit_width_node(admitted: LeanAdmittedBitWidth) -> Node { + let n = bit_width_count(admitted.width) + if n == 8 { + lean_inhabitant_atom(id: ^lean_tag_bits8) + } else if n == 16 { + lean_inhabitant_atom(id: ^lean_tag_bits16) + } else if n == 32 { + lean_inhabitant_atom(id: ^lean_tag_bits32) + } else if n == 64 { + lean_inhabitant_atom(id: ^lean_tag_bits64) + } else { + lean_inhabitant_atom(id: ^lean_tag_width_inadmissible) } } fn lean_integer_width_node(width: LeanIntegerWidth) -> Node { match width { - LeanFixedWidth { width: admitted } => lean_admitted_bit_width_node(width: admitted) + LeanFixedWidth { admission: LeanBitWidthAccepted { width: admitted } } => + lean_admitted_bit_width_node(admitted: admitted) LeanPlatformWord => lean_platform_word_width_node() } } fn lean_scalar_node(scalar: LeanScalar) -> Node { match scalar { - FixedIntScalar { signedness, width } => Node { + LeanIntegerScalar { signedness, width } => Node { kind: TypeNode { connective: Conj }, children: [ lean_named_edge( @@ -399,7 +424,7 @@ fn lean_primitive_inhabitant_node(id: Symbol, facts: LeanPrimitiveFacts) -> Node } fn lean_inhabitant_int32_node() -> Node { - lean_primitive_inhabitant_node(id: ^lean_inhabitant_int32, facts: lean_facts_int32) + lean_primitive_inhabitant_node(id: ^lean_inhabitant_int32, facts: lean_facts_int32()) } fn lean_fixed_int_spec_facts( @@ -440,7 +465,7 @@ fn lean_bool_spec_facts(facts: LeanPrimitiveFacts) -> Map { fn lean_primitive_bundle_from_facts(facts: LeanPrimitiveFacts) -> PrimitiveFactBundle { match facts.scalar { - FixedIntScalar { signedness, width } => PrimitiveFactBundle { + LeanIntegerScalar { signedness, width } => PrimitiveFactBundle { substrate_carrier: lean_primitive_facts_node(facts: facts), spec_facts: lean_fixed_int_spec_facts( facts: facts, @@ -684,7 +709,7 @@ fn lean_scalar_algebra_inhabitance(facts: LeanPrimitiveFacts) -> AlgebraInhabita let inhabitant = lean_primitive_facts_node(facts: facts) match facts.scalar { - FixedIntScalar { signedness, width } => AlgebraInhabitanceDecl { + LeanIntegerScalar { signedness, width } => AlgebraInhabitanceDecl { algebra: commutative_ring_type_node(inhabitant: inhabitant), inhabitant: inhabitant, witness: lean_integer_algebra_witness_node( diff --git a/src/v2/extdeps/languages/verilog.dag b/src/v2/extdeps/languages/verilog.dag index 5df9a78f55a..d4c9f4b2280 100644 --- a/src/v2/extdeps/languages/verilog.dag +++ b/src/v2/extdeps/languages/verilog.dag @@ -25,6 +25,8 @@ import v2.std.compilers.lexing { WhitespaceChar } +data verilog_std_integer_signedness_migration_note: String = "Signedness consumer migration: verilog imports std.integer.Signedness. Semantic equivalence: verilog signed/unsigned on net, port, and parameter declarations is the same interpretive axis as std.integer Signed/Unsigned — whether a bit pattern is read as two's-complement signed range or unsigned modular arithmetic; no Verilog-specific signedness semantics beyond this axis are modeled on these fields." + type PortDirection = Input | Output diff --git a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag index 40ea59f79f3..8cc062a3ef8 100644 --- a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag +++ b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag @@ -4,7 +4,8 @@ module v2.test.claim.lean_bit_width_admissibility_witness import v2.extdeps.languages.lean { lean_admit_bit_width, LeanBitWidthAccepted, - LeanBitWidthRefused + LeanBitWidthRefused, + LeanAdmittedBitWidth } import std.measure { BitWidth, bit_width, bit_width_count } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } @@ -12,17 +13,21 @@ import v2.std.logic { Bool } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -data lean_bit_width_admissibility_witness_note: String = "P3b cluster-1 receipt (lean end-to-end): BitWidth admission is LeanBitWidthAdmission; FixedIntScalar carries only LeanAdmittedBitWidth via LeanFixedWidth (128 cannot reach width projection). RED: lean_admit_bit_width(128) is Refused with the genuine width pinned." +data lean_bit_width_admissibility_witness_note: String = "P3b cluster-1 receipt (lean end-to-end): LeanAdmittedBitWidth carries grounded BitWidth; lean_admit_bit_width is the admission boundary (Accepted | Refused). Honest rung: accepted refinement with executing refusal — not structural impossibility. RED: lean_admit_bit_width(128) is Refused with the genuine width pinned." test fn lean_admit_accepts_catalog_fixed_widths() -> Bool { match lean_admit_bit_width(width: bit_width(count: 8)) { - LeanBitWidthAccepted { width: _ } => + LeanBitWidthAccepted { width: w8 } => match lean_admit_bit_width(width: bit_width(count: 16)) { - LeanBitWidthAccepted { width: _ } => + LeanBitWidthAccepted { width: w16 } => match lean_admit_bit_width(width: bit_width(count: 32)) { - LeanBitWidthAccepted { width: _ } => + LeanBitWidthAccepted { width: w32 } => match lean_admit_bit_width(width: bit_width(count: 64)) { - LeanBitWidthAccepted { width: _ } => true + LeanBitWidthAccepted { width: w64 } => + bit_width_count(w8.width) == 8 && + bit_width_count(w16.width) == 16 && + bit_width_count(w32.width) == 32 && + bit_width_count(w64.width) == 64 LeanBitWidthRefused { width: _ } => false } LeanBitWidthRefused { width: _ } => false From 17f1ab6408bfc6ec920c64e0e04d646691cb3286 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 1 Aug 2026 01:27:03 +0000 Subject: [PATCH 25/27] Fix LeanFixedWidth to carry LeanAdmittedBitWidth per operator ruling. LeanBitWidthAccepted is an admission coproduct arm, not a field type. Catalog fixed widths extract LeanAdmittedBitWidth from the admission boundary; witness checks grounded BitWidth counts on accepted carriers. Co-authored-by: Cursor --- src/v2/extdeps/languages/lean.dag | 8 +++----- .../claim/lean_bit_width_admissibility_witness_test.dag | 3 +-- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/src/v2/extdeps/languages/lean.dag b/src/v2/extdeps/languages/lean.dag index 1e2f54abe35..919a0983642 100644 --- a/src/v2/extdeps/languages/lean.dag +++ b/src/v2/extdeps/languages/lean.dag @@ -194,7 +194,7 @@ type LeanBitWidthAdmission | LeanBitWidthRefused { width: BitWidth } type LeanIntegerWidth - = LeanFixedWidth { admission: LeanBitWidthAccepted } + = LeanFixedWidth { width: LeanAdmittedBitWidth } | LeanPlatformWord type LeanScalar @@ -209,8 +209,7 @@ type LeanPrimitiveFacts { fn lean_catalog_fixed_width(count: Nat) -> LeanIntegerWidth { match lean_admit_bit_width(width: bit_width(count: count)) { - LeanBitWidthAccepted { width: admitted } => - LeanFixedWidth { admission: LeanBitWidthAccepted { width: admitted } } + LeanBitWidthAccepted { width: admitted } => LeanFixedWidth { width: admitted } LeanBitWidthRefused { width: _ } => LeanPlatformWord } } @@ -358,8 +357,7 @@ fn lean_admitted_bit_width_node(admitted: LeanAdmittedBitWidth) -> Node { fn lean_integer_width_node(width: LeanIntegerWidth) -> Node { match width { - LeanFixedWidth { admission: LeanBitWidthAccepted { width: admitted } } => - lean_admitted_bit_width_node(admitted: admitted) + LeanFixedWidth { width: admitted } => lean_admitted_bit_width_node(admitted: admitted) LeanPlatformWord => lean_platform_word_width_node() } } diff --git a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag index 8cc062a3ef8..40ced02dde0 100644 --- a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag +++ b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag @@ -4,8 +4,7 @@ module v2.test.claim.lean_bit_width_admissibility_witness import v2.extdeps.languages.lean { lean_admit_bit_width, LeanBitWidthAccepted, - LeanBitWidthRefused, - LeanAdmittedBitWidth + LeanBitWidthRefused } import std.measure { BitWidth, bit_width, bit_width_count } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } From 682b6c11f7a17b0894567994a6f6392e6bc117a2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 1 Aug 2026 01:41:38 +0000 Subject: [PATCH 26/27] Refuse catalog width admission instead of widening to platform word. Add LeanFixedWidthAdmissionRefused to propagate lean_admit_bit_width refusals through lean_catalog_fixed_width; witness proves 128 is not coerced to LeanPlatformWord (review 45814). Co-authored-by: Cursor --- src/v2/extdeps/languages/lean.dag | 6 +++++- .../lean_bit_width_admissibility_witness_test.dag | 14 +++++++++++++- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/v2/extdeps/languages/lean.dag b/src/v2/extdeps/languages/lean.dag index 919a0983642..f0682d717c1 100644 --- a/src/v2/extdeps/languages/lean.dag +++ b/src/v2/extdeps/languages/lean.dag @@ -195,6 +195,7 @@ type LeanBitWidthAdmission type LeanIntegerWidth = LeanFixedWidth { width: LeanAdmittedBitWidth } + | LeanFixedWidthAdmissionRefused { width: BitWidth } | LeanPlatformWord type LeanScalar @@ -210,7 +211,8 @@ type LeanPrimitiveFacts { fn lean_catalog_fixed_width(count: Nat) -> LeanIntegerWidth { match lean_admit_bit_width(width: bit_width(count: count)) { LeanBitWidthAccepted { width: admitted } => LeanFixedWidth { width: admitted } - LeanBitWidthRefused { width: _ } => LeanPlatformWord + LeanBitWidthRefused { width: refused } => + LeanFixedWidthAdmissionRefused { width: refused } } } @@ -358,6 +360,8 @@ fn lean_admitted_bit_width_node(admitted: LeanAdmittedBitWidth) -> Node { fn lean_integer_width_node(width: LeanIntegerWidth) -> Node { match width { LeanFixedWidth { width: admitted } => lean_admitted_bit_width_node(admitted: admitted) + LeanFixedWidthAdmissionRefused { width: _ } => + lean_inhabitant_atom(id: ^lean_tag_width_inadmissible) LeanPlatformWord => lean_platform_word_width_node() } } diff --git a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag index 40ced02dde0..7b43d411b2b 100644 --- a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag +++ b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag @@ -3,8 +3,12 @@ module v2.test.claim.lean_bit_width_admissibility_witness import v2.extdeps.languages.lean { lean_admit_bit_width, + lean_catalog_fixed_width, LeanBitWidthAccepted, - LeanBitWidthRefused + LeanBitWidthRefused, + LeanFixedWidth, + LeanFixedWidthAdmissionRefused, + LeanPlatformWord } import std.measure { BitWidth, bit_width, bit_width_count } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } @@ -44,3 +48,11 @@ test fn lean_admit_refuses_bits128() -> Bool { LeanBitWidthAccepted { width: _ } => false } } + +test fn lean_catalog_refuses_bits128_not_platform_word() -> Bool { + match lean_catalog_fixed_width(count: 128) { + LeanFixedWidthAdmissionRefused { width: refused } => bit_width_count(refused) == 128 + LeanFixedWidth { width: _ } => false + LeanPlatformWord => false + } +} From 323d18e5f5a09c47da777c55949433c7f2adef0a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 1 Aug 2026 01:57:16 +0000 Subject: [PATCH 27/27] Stop width refusal at admission; seal LeanAdmittedBitWidth. Remove LeanFixedWidthAdmissionRefused from LeanIntegerWidth; catalog matches admission before building LeanIntegerScalar and uses LeanWidthAdmissionRefused scalar on refusal. Mark LeanAdmittedBitWidth sole_constructor so admitted widths are module-local to lean_admit_bit_width (review 45827). Co-authored-by: Cursor --- src/v2/extdeps/languages/lean.dag | 112 ++++++++++++------ ...n_bit_width_admissibility_witness_test.dag | 24 ++-- 2 files changed, 93 insertions(+), 43 deletions(-) diff --git a/src/v2/extdeps/languages/lean.dag b/src/v2/extdeps/languages/lean.dag index f0682d717c1..d5ab8b0a64b 100644 --- a/src/v2/extdeps/languages/lean.dag +++ b/src/v2/extdeps/languages/lean.dag @@ -183,9 +183,9 @@ type LeanProofCheckSemantics { proof_irrelevance_for_propositions: Bool } -data lean_bit_width_admissibility_note: String = "Lean fixed-precision integers: width axis is std.measure.BitWidth; lean_admit_bit_width is the admission boundary producing LeanBitWidthAccepted with LeanAdmittedBitWidth or LeanBitWidthRefused pinning the observed width. Honest rung: accepted refinement with executing refusal (witness lean_bit_width_admissibility_witness_test) — not structural impossibility; catalog fixed widths route through the admission boundary. Platform word is LeanPlatformWord on the PointerWidth axis. Signedness is std.integer.Signedness, not LeanIntKind." +data lean_bit_width_admissibility_note: String = "Lean fixed-precision integers: width axis is std.measure.BitWidth; lean_admit_bit_width is the admission boundary producing LeanBitWidthAccepted with LeanAdmittedBitWidth or LeanBitWidthRefused pinning the observed width. LeanAdmittedBitWidth is sole_constructor — cross-module forge is refused; honest rung is accepted refinement with executing refusal (witness lean_bit_width_admissibility_witness_test), not structural impossibility. Catalog fixed widths match admission Accepted before constructing LeanIntegerScalar; refusal stops at LeanWidthAdmissionRefused, not LeanIntegerWidth. Platform word is LeanPlatformWord. Signedness is std.integer.Signedness." -type LeanAdmittedBitWidth { +type LeanAdmittedBitWidth sole_constructor { width: BitWidth } @@ -195,11 +195,11 @@ type LeanBitWidthAdmission type LeanIntegerWidth = LeanFixedWidth { width: LeanAdmittedBitWidth } - | LeanFixedWidthAdmissionRefused { width: BitWidth } | LeanPlatformWord type LeanScalar = LeanIntegerScalar { signedness: Signedness, width: LeanIntegerWidth } + | LeanWidthAdmissionRefused { width: BitWidth } | BoolScalar type LeanPrimitiveFacts { @@ -208,76 +208,99 @@ type LeanPrimitiveFacts { representation: Symbol } -fn lean_catalog_fixed_width(count: Nat) -> LeanIntegerWidth { +fn lean_primitive_facts_for_catalog_width( + surface_spelling: Symbol, + signedness: Signedness, + count: Nat, + representation: Symbol +) -> LeanPrimitiveFacts { match lean_admit_bit_width(width: bit_width(count: count)) { - LeanBitWidthAccepted { width: admitted } => LeanFixedWidth { width: admitted } - LeanBitWidthRefused { width: refused } => - LeanFixedWidthAdmissionRefused { width: refused } + LeanBitWidthAccepted { width: admitted } => LeanPrimitiveFacts { + surface_spelling: surface_spelling, + scalar: LeanIntegerScalar { + signedness: signedness, + width: LeanFixedWidth { width: admitted } + }, + representation: representation + } + LeanBitWidthRefused { width: refused } => LeanPrimitiveFacts { + surface_spelling: surface_spelling, + scalar: LeanWidthAdmissionRefused { width: refused }, + representation: representation + } } } fn lean_facts_int8() -> LeanPrimitiveFacts { - LeanPrimitiveFacts { + lean_primitive_facts_for_catalog_width( surface_spelling: ^lean_surface_spelling_int8, - scalar: LeanIntegerScalar { signedness: Signed, width: lean_catalog_fixed_width(count: 8) }, + signedness: Signed, + count: 8, representation: ^lean_repr_fixed_precision_integer - } + ) } fn lean_facts_int16() -> LeanPrimitiveFacts { - LeanPrimitiveFacts { + lean_primitive_facts_for_catalog_width( surface_spelling: ^lean_surface_spelling_int16, - scalar: LeanIntegerScalar { signedness: Signed, width: lean_catalog_fixed_width(count: 16) }, + signedness: Signed, + count: 16, representation: ^lean_repr_fixed_precision_integer - } + ) } fn lean_facts_int32() -> LeanPrimitiveFacts { - LeanPrimitiveFacts { + lean_primitive_facts_for_catalog_width( surface_spelling: ^lean_surface_spelling_int32, - scalar: LeanIntegerScalar { signedness: Signed, width: lean_catalog_fixed_width(count: 32) }, + signedness: Signed, + count: 32, representation: ^lean_repr_fixed_precision_integer - } + ) } fn lean_facts_int64() -> LeanPrimitiveFacts { - LeanPrimitiveFacts { + lean_primitive_facts_for_catalog_width( surface_spelling: ^lean_surface_spelling_int64, - scalar: LeanIntegerScalar { signedness: Signed, width: lean_catalog_fixed_width(count: 64) }, + signedness: Signed, + count: 64, representation: ^lean_repr_fixed_precision_integer - } + ) } fn lean_facts_uint8() -> LeanPrimitiveFacts { - LeanPrimitiveFacts { + lean_primitive_facts_for_catalog_width( surface_spelling: ^lean_surface_spelling_uint8, - scalar: LeanIntegerScalar { signedness: Unsigned, width: lean_catalog_fixed_width(count: 8) }, + signedness: Unsigned, + count: 8, representation: ^lean_repr_fixed_precision_integer - } + ) } fn lean_facts_uint16() -> LeanPrimitiveFacts { - LeanPrimitiveFacts { + lean_primitive_facts_for_catalog_width( surface_spelling: ^lean_surface_spelling_uint16, - scalar: LeanIntegerScalar { signedness: Unsigned, width: lean_catalog_fixed_width(count: 16) }, + signedness: Unsigned, + count: 16, representation: ^lean_repr_fixed_precision_integer - } + ) } fn lean_facts_uint32() -> LeanPrimitiveFacts { - LeanPrimitiveFacts { + lean_primitive_facts_for_catalog_width( surface_spelling: ^lean_surface_spelling_uint32, - scalar: LeanIntegerScalar { signedness: Unsigned, width: lean_catalog_fixed_width(count: 32) }, + signedness: Unsigned, + count: 32, representation: ^lean_repr_fixed_precision_integer - } + ) } fn lean_facts_uint64() -> LeanPrimitiveFacts { - LeanPrimitiveFacts { + lean_primitive_facts_for_catalog_width( surface_spelling: ^lean_surface_spelling_uint64, - scalar: LeanIntegerScalar { signedness: Unsigned, width: lean_catalog_fixed_width(count: 64) }, + signedness: Unsigned, + count: 64, representation: ^lean_repr_fixed_precision_integer - } + ) } fn lean_facts_usize() -> LeanPrimitiveFacts { @@ -360,8 +383,6 @@ fn lean_admitted_bit_width_node(admitted: LeanAdmittedBitWidth) -> Node { fn lean_integer_width_node(width: LeanIntegerWidth) -> Node { match width { LeanFixedWidth { width: admitted } => lean_admitted_bit_width_node(admitted: admitted) - LeanFixedWidthAdmissionRefused { width: _ } => - lean_inhabitant_atom(id: ^lean_tag_width_inadmissible) LeanPlatformWord => lean_platform_word_width_node() } } @@ -386,6 +407,8 @@ fn lean_scalar_node(scalar: LeanScalar) -> Node { ], occurrence_id: SyntheticOccurrence } + LeanWidthAdmissionRefused { width: _ } => + lean_inhabitant_atom(id: ^lean_tag_width_inadmissible) BoolScalar => lean_inhabitant_atom(id: ^lean_tag_scalar_bool) } } @@ -465,6 +488,20 @@ fn lean_bool_spec_facts(facts: LeanPrimitiveFacts) -> Map { } } +fn lean_width_admission_refused_spec_facts(facts: LeanPrimitiveFacts) -> Map { + Map { + lookup: fn(axis) { + if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { + v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.surface_spelling) } + } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { + v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.representation) } + } else { + v2.std.optional.Absent + } + } + } +} + fn lean_primitive_bundle_from_facts(facts: LeanPrimitiveFacts) -> PrimitiveFactBundle { match facts.scalar { LeanIntegerScalar { signedness, width } => PrimitiveFactBundle { @@ -479,6 +516,10 @@ fn lean_primitive_bundle_from_facts(facts: LeanPrimitiveFacts) -> PrimitiveFactB substrate_carrier: lean_primitive_facts_node(facts: facts), spec_facts: lean_bool_spec_facts(facts: facts) } + LeanWidthAdmissionRefused { width: _ } => PrimitiveFactBundle { + substrate_carrier: lean_primitive_facts_node(facts: facts), + spec_facts: lean_width_admission_refused_spec_facts(facts: facts) + } } } @@ -725,6 +766,11 @@ fn lean_scalar_algebra_inhabitance(facts: LeanPrimitiveFacts) -> AlgebraInhabita inhabitant: inhabitant, witness: lean_bool_algebra_witness_node() } + LeanWidthAdmissionRefused { width: _ } => AlgebraInhabitanceDecl { + algebra: boolean_algebra_type_node(inhabitant: inhabitant), + inhabitant: inhabitant, + witness: lean_bool_algebra_witness_node() + } } } diff --git a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag index 7b43d411b2b..4da19b0d5d2 100644 --- a/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag +++ b/src/v2/test/claim/lean_bit_width_admissibility_witness_test.dag @@ -3,12 +3,11 @@ module v2.test.claim.lean_bit_width_admissibility_witness import v2.extdeps.languages.lean { lean_admit_bit_width, - lean_catalog_fixed_width, + lean_primitive_facts_for_catalog_width, LeanBitWidthAccepted, LeanBitWidthRefused, - LeanFixedWidth, - LeanFixedWidthAdmissionRefused, - LeanPlatformWord + LeanIntegerScalar, + LeanWidthAdmissionRefused } import std.measure { BitWidth, bit_width, bit_width_count } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } @@ -16,7 +15,7 @@ import v2.std.logic { Bool } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -data lean_bit_width_admissibility_witness_note: String = "P3b cluster-1 receipt (lean end-to-end): LeanAdmittedBitWidth carries grounded BitWidth; lean_admit_bit_width is the admission boundary (Accepted | Refused). Honest rung: accepted refinement with executing refusal — not structural impossibility. RED: lean_admit_bit_width(128) is Refused with the genuine width pinned." +data lean_bit_width_admissibility_witness_note: String = "P3b cluster-1 receipt (lean end-to-end): lean_admit_bit_width is the admission boundary; LeanAdmittedBitWidth is sole_constructor. Honest rung: accepted refinement with executing refusal — not structural impossibility. RED: width 128 refuses at admission and catalog construction yields LeanWidthAdmissionRefused, not LeanIntegerScalar." test fn lean_admit_accepts_catalog_fixed_widths() -> Bool { match lean_admit_bit_width(width: bit_width(count: 8)) { @@ -49,10 +48,15 @@ test fn lean_admit_refuses_bits128() -> Bool { } } -test fn lean_catalog_refuses_bits128_not_platform_word() -> Bool { - match lean_catalog_fixed_width(count: 128) { - LeanFixedWidthAdmissionRefused { width: refused } => bit_width_count(refused) == 128 - LeanFixedWidth { width: _ } => false - LeanPlatformWord => false +test fn lean_catalog_width_admission_refuses_bits128_not_integer_scalar() -> Bool { + match lean_primitive_facts_for_catalog_width( + surface_spelling: ^lean_surface_spelling_int32, + signedness: Signed, + count: 128, + representation: ^lean_repr_fixed_precision_integer + ).scalar { + LeanWidthAdmissionRefused { width: refused } => bit_width_count(refused) == 128 + LeanIntegerScalar { signedness: _, width: _ } => false + _ => false } }