diff --git a/src/v4/extdeps/cpp_abi.dag b/src/v4/extdeps/cpp_abi.dag index 371e25e8d8e..dc8733a1d60 100644 --- a/src/v4/extdeps/cpp_abi.dag +++ b/src/v4/extdeps/cpp_abi.dag @@ -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 } @@ -29,12 +25,8 @@ type CppIntegerWidth // 🟒 pretty-much-done β€” core integer-width bundle includes wchar_t width; testcase: test/claim/manual/cpp_scalar_grounding_anchor.dag. type CppCoreIntegerWidthModel -<<<<<<< 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 } @@ -42,7 +34,6 @@ type CppPlainCharSignedness 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 @@ -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 } @@ -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 } diff --git a/src/v4/extdeps/languages/cpp.dag b/src/v4/extdeps/languages/cpp.dag index 9689aa145ea..08b3db2051d 100644 --- a/src/v4/extdeps/languages/cpp.dag +++ b/src/v4/extdeps/languages/cpp.dag @@ -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 @@ -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 @@ -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 diff --git a/src/v4/extdeps/languages/rust.dag b/src/v4/extdeps/languages/rust.dag index 2391f9d64e8..818be0063d3 100644 --- a/src/v4/extdeps/languages/rust.dag +++ b/src/v4/extdeps/languages/rust.dag @@ -80,6 +80,7 @@ type OverflowDisposition = 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_boolean_algebra diff --git a/src/v4/extdeps/languages/typescript.dag b/src/v4/extdeps/languages/typescript.dag index 504604dc1c6..21eec7cc68e 100644 --- a/src/v4/extdeps/languages/typescript.dag +++ b/src/v4/extdeps/languages/typescript.dag @@ -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_boolean_algebra diff --git a/src/v4/test/claim/manual/rust_primitive_grounding_anchor.dag b/src/v4/test/claim/manual/rust_primitive_grounding_anchor.dag new file mode 100644 index 00000000000..e12b52107d9 --- /dev/null +++ b/src/v4/test/claim/manual/rust_primitive_grounding_anchor.dag @@ -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 = rust_bool_grounding +data rust_anchor_bool_std_authority: BooleanAlgebra = 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 +type rust_anchor_i64_kind_axis = RustIntKind +type rust_anchor_i64_width_axis = RustIntWidth +type rust_anchor_i64_std_coincidence_target = Int64