Skip to content

T-4: canonical-B per-primitive grounding exemplar (unblocks Phase-3 ts/py) #3421

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
briansrls wants to merge 1 commit into from
Closed

T-4: canonical-B per-primitive grounding exemplar (unblocks Phase-3 ts/py) #3421

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 0 additions & 16 deletions src/v4/extdeps/cpp_abi.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,12 +14,8 @@ type CppMachineWidth16
type CppMachineWidth32
type CppMachineWidth64

<<<<<<< HEAD
// 🟢 pretty-much-done — closed ABI integer-width atoms; testcase: test/claim/manual/cpp_scalar_grounding_anchor.dag.
// 🟢 coproduct dissolution — DECISIONS.md T29-ABI.
=======
// 🟢 coproduct dissolution — T29-ABI.
>>>>>>> origin/main
type CppIntegerWidth
= CppWidth8 { width: CppMachineWidth8 }
| CppWidth16 { width: CppMachineWidth16 }
Expand All @@ -29,20 +25,15 @@ type CppIntegerWidth
// 🟢 pretty-much-done — core integer-width bundle includes wchar_t width; testcase: test/claim/manual/cpp_scalar_grounding_anchor.dag.
type CppCoreIntegerWidthModel<char_width, short_width, int_width, long_width, long_long_width, pointer_width, wchar_t_width>

<<<<<<< HEAD
// 🟢 pretty-much-done — implementation-defined plain-char signedness coordinate; testcase: test/claim/manual/cpp_scalar_grounding_anchor.dag.
// 🟢 coproduct dissolution — DECISIONS.md T29-ABI.
=======
// 🟢 coproduct dissolution — T29-ABI.
>>>>>>> origin/main
type CppPlainCharSignedness
= PlainCharSigned { tag: CppPlainCharSigned }
| PlainCharUnsigned { tag: CppPlainCharUnsigned }

type CppPlainCharSigned
type CppPlainCharUnsigned

<<<<<<< HEAD
// 🟢 pretty-much-done — implementation-defined wchar_t signedness coordinate; testcase: test/claim/manual/cpp_scalar_grounding_anchor.dag.
// 🟢 coproduct dissolution — DECISIONS.md T29-ABI.
type CppWcharTSignedness
Expand All @@ -54,9 +45,6 @@ type CppWcharTUnsigned

// 🟢 pretty-much-done — standard data-model family names; testcase: test/claim/manual/cpp_scalar_grounding_anchor.dag.
// 🟢 coproduct dissolution — DECISIONS.md T29-ABI.
=======
// 🟢 coproduct dissolution — T29-ABI.
>>>>>>> origin/main
type CppDataModelFamily
= ILP32 { tag: CppDataModelFamilyILP32 }
| LP64 { tag: CppDataModelFamilyLP64 }
Expand All @@ -68,12 +56,8 @@ type CppDataModelFamilyLP64
type CppDataModelFamilyLLP64
type CppDataModelFamilyILP64

<<<<<<< HEAD
// 🟢 pretty-much-done — ABI model selector; testcase: test/claim/manual/cpp_scalar_grounding_anchor.dag.
// 🟢 coproduct dissolution — DECISIONS.md T29-ABI.
=======
// 🟢 coproduct dissolution — T29-ABI.
>>>>>>> origin/main
type CppAbiModel
= ItaniumCxxAbi186 { tag: CppAbiModelItaniumCxxAbi186 }
| PlatformCxxAbi { tag: CppAbiModelPlatformCxxAbi }
Expand Down
14 changes: 0 additions & 14 deletions src/v4/extdeps/languages/cpp.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,16 +1,9 @@
// src/v4/extdeps/languages/cpp.dag
<<<<<<< HEAD
// Scope: C++ language primitive fact bundles.
// Owns: CppSignedIntegerSurfaceSpelling, CppUnsignedIntegerSurfaceSpelling, CppPlainCharSurfaceSpelling, CppWcharTSurfaceSpelling, CppFixedUnsignedCodeUnitIntegerSurfaceSpelling, CppSignedIntegerWidthSelection, CppUnsignedIntegerWidthSelection, CppPlainCharWidthSelection, CppWcharTWidthSelection, CppFixedUnsignedCodeUnitIntegerWidthSelection, CppTwosComplement, CppRepresentableResultRequired, CppUnsignedModuloArithmetic, CppScalar, cpp_bool_grounding.
// Consumes: v4.std.logic.Bool, bool_boolean_algebra; v4.std.algebra.BooleanAlgebra; v4.extdeps.cpp_abi.CppTargetProfile.
// Status: D2-REV/T29 forward reconcile; C++ integer facts are ABI-width-parametric, bool canonical-B decl-ref grounding stays 🟡 E-6(b) staging; scaffold:T-4-cpp-slice / 🟡 feature:t4-cpp-scalar-ladder bounds this file to carrier scaffolding until generated per-spelling CppTargetProfile selection rows consume it (INVARIANTS P5).
// Anchor: ISO/IEC 14882:2020 (C++20) [basic.fundamental], [expr.pre]; upstream mirror https://eel.is/c++draft/basic.fundamental.
=======
// Scope: C++ language primitive resolver facts.
// Owns: CppIntegerOverflowDisposition, cpp_bool_grounding.
// Consumes: v4.std.logic.Bool, bool_boolean_algebra; v4.std.algebra.BooleanAlgebra; CppTargetProfile/CppTargetDataModel via T29-ABI follow-up rows.
// Status: D2-REV resolver slice; bool canonical-B decl-ref grounding — 🟡 E-6(b) staging (scaffold at decl; ledger modeling-discipline.md Non-bool C++ scalar ladder still 🟡 feature:t4-cpp-scalar-ladder — P4-3208 + T29-ABI.
>>>>>>> origin/main

module v4.extdeps.languages.cpp

Expand All @@ -27,7 +20,6 @@ type CppSignedIntegerSurfaceSpelling
| LongInt
| LongLongInt

<<<<<<< HEAD
// 🟢 pretty-much-done — closed unsigned integer spelling family; testcase: test/claim/manual/cpp_scalar_grounding_anchor.dag.
// 🟢 coproduct dissolution — DECISIONS.md T29-CPP-SCALAR-FORWARD.
type CppUnsignedIntegerSurfaceSpelling
Expand All @@ -36,12 +28,6 @@ type CppUnsignedIntegerSurfaceSpelling
| UnsignedInt
| UnsignedLongInt
| UnsignedLongLongInt
=======
// 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL.
type CppIntegerOverflowDisposition
= RepresentableResultRequired
| UnsignedModuloArithmetic
>>>>>>> origin/main

// 🟢 pretty-much-done — singleton plain-char spelling; testcase: test/claim/manual/cpp_scalar_grounding_anchor.dag.
type CppPlainCharSurfaceSpelling
Expand Down
1 change: 1 addition & 0 deletions src/v4/extdeps/languages/rust.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,7 @@ type OverflowDisposition<IRCarrier>
= MustPanicOnOverflow
| MayPanicOrTwoComplementWrap

// Anchor: https://doc.rust-lang.org/reference/types/boolean.html
// 🟡 canonical-B decl-ref · E-6(b) bounded-exception · scaffold feature:canonical-b-grounding-consumer · dissolve-on: B1-CANON+zip-fold consume (ledger: B1·T-9/C1 · grounding-worked-examples.md §0)
data rust_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra

Expand Down
1 change: 1 addition & 0 deletions src/v4/extdeps/languages/typescript.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,4 +23,5 @@ type TsEcma262PrimitiveOperationSemantics
| TsNumberBitwiseInt32Uint32Semantics
| TsBigIntExactUnboundedSemantics

// 🟡 canonical-B decl-ref · E-6(b) bounded-exception · scaffold feature:canonical-b-grounding-consumer · dissolve-on: B1-CANON+zip-fold consume (ledger: B1·T-9/C1 · grounding-worked-examples.md §0)
data ts_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra
37 changes: 37 additions & 0 deletions src/v4/test/claim/manual/rust_primitive_grounding_anchor.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
// src/v4/test/claim/manual/rust_primitive_grounding_anchor.dag
// Scope: Canonical-B per-primitive grounding/coincidence compile exemplar (operator A-vs-B=B).
// Owns: rust_anchor_* type/data aliases for bool decl-ref, never primitive coincidence, i64 fact-bundle vs std Int64.
// Consumes: extdeps/languages/rust.dag, std/logic, std/cardinality, std/integer, std/algebra.
// Status: compile-only groundedness testcase — depth bar for T-4 Phase-3 typescript/python slices.
// Anchor: docs/modeling/grounding-worked-examples.md §0; INVARIANTS P1 hollow-alias / coincidence bar.

module v4.test.claim.manual.rust_primitive_grounding_anchor

import v4.extdeps.languages.rust {
rust_bool_grounding,
RustNever,
RustIntKind,
RustIntWidth,
RustScalar
}
import v4.std.algebra { BooleanAlgebra }
import v4.std.cardinality { Never }
import v4.std.integer { Int64 }
import v4.std.logic { Bool, bool_boolean_algebra }

// §0 base case — canonical-B decl-ref: language bool → single std authority (not GroundingMap spelling).
data rust_anchor_bool_grounding: BooleanAlgebra<Bool> = rust_bool_grounding
data rust_anchor_bool_std_authority: BooleanAlgebra<Bool> = bool_boolean_algebra

// §0 degenerate case — primitive coincidence: Rust `!` is std `Never` (no build-up above the primitive).
type rust_anchor_never_coincidence = RustNever
type rust_anchor_never_std = Never

// §0 classifier vs coincidence — `RustScalar.NeverScalar` classifies surface `!`; `RustNever` is the grounding target.
type rust_anchor_never_scalar_classifier = RustScalar

// §B refinement case — `RustScalar.IntScalar` fact-bundle (kind×width) vs std `Int64` coincidence target (fold-discharge, not alias).
type rust_anchor_i64_scalar_classifier = RustScalar

@briansrls briansrls May 20, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: The i64 exemplar names the whole RustScalar classifier instead of a concrete Rust i64 fact bundle, so it does not anchor the Rust Reference facts or the Int64 coincidence required by INVARIANTS P1 / modeling-discipline Practice 8.

type rust_anchor_i64_kind_axis = RustIntKind
type rust_anchor_i64_width_axis = RustIntWidth
type rust_anchor_i64_std_coincidence_target = Int64
Loading