From c5224b3b5028414802323ff6bf6e8e43a56fb768 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 27 Apr 2026 21:16:11 -0400 Subject: [PATCH 1/4] WIP: lively-wolf-462 --- dsl/extdeps/languages/python/primitives.dag | 233 ++++++++++++++++++++ 1 file changed, 233 insertions(+) create mode 100644 dsl/extdeps/languages/python/primitives.dag diff --git a/dsl/extdeps/languages/python/primitives.dag b/dsl/extdeps/languages/python/primitives.dag new file mode 100644 index 00000000000..839fbbbe92d --- /dev/null +++ b/dsl/extdeps/languages/python/primitives.dag @@ -0,0 +1,233 @@ +// extdeps/languages/python/primitives.dag — Structural target-primitive +// declarations for the Python target (T-Ground-Python tranche 1 / spec authority). +// +// TRANCHE 1 (this file): Python language-reference built-in types whose +// value domain is fixed by the language spec — `int` (arbitrary precision), +// `bool`, `str` (immutable Unicode code-point sequence), and `None` (the +// single inhabitant of `NoneType`). See Python Language Reference §"The +// standard type hierarchy" (docs.python.org/3/reference/datamodel.html) and +// §"Numeric Types — int, float, complex" +// (docs.python.org/3/library/stdtypes.html#numeric-types-int-float-complex). +// +// `float` and `complex` are intentionally omitted from this tranche: the +// language reference states "Floating point numbers are usually implemented +// using double in C" and explicitly flags float/complex precision as +// "implementation dependent". Declaring a fixed IEEE-754 carrier here would +// repeat the same no-lying-about-width discipline violation Go's omission of +// `int` / `uint` / `uintptr` calls out — defer until a CPython-tagged +// implementation-width story lands alongside DB-11 / cardinality substrate. +// `bytes` / `bytearray` (built-in byte-sequence types) are also deferred to +// the next tranche; they're language-level but not part of the +// numeric/bool/str tranche-1 scope per dispatch brief. +// +// TWO-AUTHORITY DISCIPLINE (ROADMAP §Post-R1 Grounding lanes): +// (a) THIS FILE — Python language reference (docs.python.org/3/reference). +// (b) stdlib carriers and product-specific rows (e.g. `dict` for Json, +// `bytes` for Bytes payloads consumed via stdlib paths) stay in +// python/types.dag + emit tables until a dedicated stdlib-authority +// slice lands; do not cite stdlib paths here. +// +// CONSUMER BOUNDARY: same Path-2 honest state as rust/primitives.dag and +// go/primitives.dag — the top-level `python_spec_predeclared_primitives` +// list and `python_dag_unit_target_primitive` lower as `ValueBody::Unparsed` +// until R2 T-Substrate's top-level aggregate sub-lane lands; type-structure +// (`PythonPrimitive = …`) is walkable for Engine / future loaders. +// +// LESSON 5 (grounding-pilot-receipt.md): subset-only axes are structurally +// partitioned — string algebra/carrier tags live only on PythonStringPrimitive; +// integer carrier discipline lives only on PythonIntegerPrimitive; the +// terminal sentinel pair lives only on PythonUnitPrimitive. +// +// STRING (language ref §"Text Sequence Type — str", +// docs.python.org/3/library/stdtypes.html#textseq): a `str` value is an +// immutable sequence of Unicode code points (free monoid over Unicode code +// points). Source-text encoding (UTF-8 / UTF-16 / etc.) is NOT a second +// carrier/algebra authority on the spec `str` row — it is encode/decode +// surface and belongs in operator or stdlib slices, not parallel sum arms +// on `PythonStringPrimitive`. (Same discipline as Go's spec-string row +// declining a UTF-8 parallel authority on `GoStringPrimitive`.) +// +// SUBSTRATE-GAP FLAGS: +// 1. Python `int` is arbitrary precision — no fixed-width carrier and no +// modular-wrap overflow. Tranche-1 models this with the +// `PythonUnboundedIntegerCarrier` sentinel (no `range_min/max`, +// no `overflow` field) so consumers cannot read a false fixed width. +// Post-DB-11 / cardinality substrate this becomes +// `OrderedRing` with countably-infinite +// cardinality; today the sentinel carrier is the honest declaration. +// 2. `bool` is a subclass of `int` per the Python data model +// (True == 1, False == 0). Tranche-1 routes `bool` through +// `PythonBooleanPrimitive` with the canonical two-element Boolean +// algebra value-domain (Bit-carrier sentinel) and does not yet model +// the int-coercion edge — that lives in coercion / operator slices, +// not on the predeclared primitive row. +// 3. Algebra and carrier identity is still carried by structural tags +// (`PythonIntegerAlgebra` / `PythonNonIntegerAlgebra` / +// `PythonTargetCarrier` / `PythonSpecString*Tag`), same bridge pattern +// as rust/primitives.dag and go/primitives.dag, until the .dag +// substrate exposes type expressions as data values. + +module extdeps.languages.python.primitives + +// ========================================================================= +// Algebra tags, partitioned by integer / non-integer / string class. +// +// Practice 4 (docs/modeling-discipline.md) ledger annotations follow the +// post-#1046 Go file style: each closed coproduct names its GREEN +// (terminal / consumed) and YELLOW (parse-scaffold reserved) arms. +// Single-arm `type X = Tag` declarations leave `Tag` unresolved in the +// v2 bootstrap compiler — every coproduct below has ≥2 arms by +// construction, with reserved arms named for their dissolution trigger. +// ========================================================================= + +// Python `int` is the only spec-predeclared integer; it inhabits the +// (unbounded, signed) ordered ring. The reserved arm exists solely so the +// v2 bootstrap loader resolves `PythonIntegerAlgebra` as a sum, not a unary +// alias. +// +// Practice 4: **🟢 GREEN** — `PythonOrderedRingAlgebra` is the terminal +// algebra-tag for Python's spec integer. +// **🟡 YELLOW (scaffold)** — `PythonIntegerAlgebraReserved` exists only for +// the v2 "≥2 sum arms" tag-resolution constraint; named trigger: +// bootstrap / loader closes single-arm sums, OR a future stdlib-authority +// slice lands a second integer algebra row (e.g., a Semiring inhabitant +// from numerics packages — would still NOT belong on this language-spec +// row; reserved arm dissolves regardless). +type PythonIntegerAlgebra + = PythonOrderedRingAlgebra + | PythonIntegerAlgebraReserved + +// Bool + None share one closed algebra-tag sum (mirrors rust +// `NonIntegerAlgebra` and go `GoSpecDiscreteAlgebra` grouping). String is +// separate — its value-domain is a sequence monoid, not a discrete scalar. +// +// Practice 4: **🟢 GREEN (terminal coproduct).** Both arms are spec-realized +// and consumed: `PythonCanonicalTwoElementBooleanAlgebra` is the value-domain +// of `bool`; `PythonTerminalAlgebra` is the single-inhabitant algebra of +// `NoneType`. Each arm has a matching `PythonPrimitive` row in +// `python_spec_predeclared_primitives` / `python_dag_unit_target_primitive`. +type PythonNonIntegerAlgebra + = PythonCanonicalTwoElementBooleanAlgebra + | PythonTerminalAlgebra + + +// ========================================================================= +// Target carrier tags (value-domain witnesses; not CPython object layout). +// +// `PythonUnboundedIntegerCarrier` is the honest declaration that Python's +// spec `int` is arbitrary-precision — there is no fixed bit-width and no +// modular-wrap field on `PythonIntegerPrimitive`. Substrate-gap flag #1 +// names DB-11 / cardinality dissolution. +// +// `PythonBitCarrier` and `PythonTerminalCarrier` mirror the Rust/Go +// convention of declaring the algebra value-domain witness (per +// `dsl/std/integer.dag:4` "Int is a CARRIER (Word64) with EVIDENCE…"), +// not CPython object representation (CPython stores both `True`/`False` +// as singleton PyBool objects; that is target-codegen / runtime, not +// algebra value-domain). +// +// Practice 4: **🟢 GREEN (terminal coproduct).** All three arms are +// consumed by tranche-1 rows: integer (UnboundedInteger), bool (Bit), and +// None (Terminal). No reserved scaffolds — three arms is already ≥2. +// ========================================================================= + +type PythonTargetCarrier + = PythonUnboundedIntegerCarrier + | PythonBitCarrier + | PythonTerminalCarrier + + +// String value = immutable Unicode code-point sequence (monoid + Unicode +// code-point carrier). Reserved arms are v2 parse scaffolding only (never +// used in data) — same single-arm-resolution issue as `PythonIntegerAlgebra`; +// do **not** add a UTF-8 / UTF-16 / encoding parallel authority here +// (header §STRING). +// +// Practice 4: **🟢 GREEN** — first arms are the terminal string-value +// witnesses (algebra: immutable codepoint-sequence monoid; carrier: +// Unicode code-point sequence). **🟡 YELLOW (scaffold)** — reserved arms +// exist only for the v2 "≥2 sum arms" tag-resolution constraint; named +// trigger: bootstrap / loader closes single-arm sums. +type PythonSpecStringAlgebraTag + = PythonImmutableUnicodeCodePointSequenceMonoidAlgebra + | PythonSpecStringAlgebraParseReserved + +type PythonSpecStringCarrierTag + = PythonUnicodeCodePointSequenceCarrier + | PythonSpecStringCarrierParseReserved + + +// ========================================================================= +// Sum-typed Python spec primitive (Lesson 5 partition). +// +// Sum-typed so each spec primitive's structurally-meaningful axes attach +// only where they have meaning: integer carrier discipline only on +// `PythonIntegerPrimitive`; string algebra/carrier tags only on +// `PythonStringPrimitive`. State-space modeling discipline — no +// `bool: PythonUnboundedIntegerCarrier`, no `int: PythonUnicodeCodePointSequenceCarrier`. +// +// No `range_min/max` and no `overflow` field on `PythonIntegerPrimitive`: +// substrate-gap flag #1 — Python's spec `int` is unbounded, so a +// fixed-range / fixed-overflow row would be a lie. Consumers needing +// concrete-width integer routing should consult target-specific lanes +// (Rust / Go `*_integer_range` rows) rather than synthesizing a width here. +// ========================================================================= + +type PythonPrimitive + = PythonIntegerPrimitive { + target_name: String + algebra: PythonIntegerAlgebra + carrier: PythonTargetCarrier + } + | PythonStringPrimitive { + target_name: String + algebra: PythonSpecStringAlgebraTag + carrier: PythonSpecStringCarrierTag + } + | PythonBooleanPrimitive { + target_name: String + algebra: PythonNonIntegerAlgebra + carrier: PythonTargetCarrier + } + | PythonUnitPrimitive { + target_name: String + algebra: PythonNonIntegerAlgebra + carrier: PythonTargetCarrier + } + + +// Predeclared spec primitives: int, bool, str. +// (None / NoneType is split into a separate top-level row below — same +// pattern as Go's `go_dag_unit_target_primitive` — because `None` is the +// canonical DAG `Unit` realization in `python/types.dag`, not a numeric +// or sequence primitive.) +// +// `float` / `complex` deferred (header §implementation-defined width). +// `bytes` / `bytearray` deferred to next tranche. +data python_spec_predeclared_primitives: List = [ + PythonIntegerPrimitive { target_name: "int", + algebra: PythonOrderedRingAlgebra, + carrier: PythonUnboundedIntegerCarrier }, + + PythonBooleanPrimitive { target_name: "bool", + algebra: PythonCanonicalTwoElementBooleanAlgebra, + carrier: PythonBitCarrier }, + + PythonStringPrimitive { target_name: "str", + algebra: PythonImmutableUnicodeCodePointSequenceMonoidAlgebra, + carrier: PythonUnicodeCodePointSequenceCarrier } +] + +// DAG Unit → Python: `None` (the sole inhabitant of `NoneType`) is the +// target spelling for DagName `Unit` in `python/types.dag`. Split out from +// the predeclared list (same pattern as `go_dag_unit_target_primitive`) +// because `None` is a value, not a type name in the spec's predeclared-type +// list — `NoneType` is the type and is not a builtin identifier in the +// scope a user can name without `types.NoneType`. The target-name string +// here records the value spelling consumers emit ("None"), aligning with +// `python_type_checkpoints` in `python/types.dag`. +data python_dag_unit_target_primitive: PythonPrimitive = PythonUnitPrimitive { + target_name: "None", + algebra: PythonTerminalAlgebra, + carrier: PythonTerminalCarrier +} From 8cfdaa5b8801d2b3a76a6fc4329b59b1dc33da15 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 28 Apr 2026 01:51:56 +0000 Subject: [PATCH 2/4] T-Ground-Python tranche 1: per-variant witness tags + PythonPrimitive ledger Address codex review on PR #1080 (sha f417bcef): 1. Split shared `PythonNonIntegerAlgebra` / `PythonTargetCarrier` into per-variant witness-tag pairs so each `PythonPrimitive` variant admits only its spec-valid (algebra, carrier) pair. Boolean cannot carry a terminal-algebra; integer cannot carry a Bit-carrier; etc. Illegal-states-unrepresentable enforced structurally. 2. Add Practice 4 GREEN/YELLOW ledger to the top-level `PythonPrimitive` coproduct (terminal four-arm partition; row mapping + dissolution trigger named). CI: ci_full_dsl bootstrap loads all 134 sources clean. Co-Authored-By: Claude Opus 4.7 (1M context) --- dsl/extdeps/languages/python/primitives.dag | 229 +++++++++++--------- 1 file changed, 127 insertions(+), 102 deletions(-) diff --git a/dsl/extdeps/languages/python/primitives.dag b/dsl/extdeps/languages/python/primitives.dag index 839fbbbe92d..2f236fd7d3d 100644 --- a/dsl/extdeps/languages/python/primitives.dag +++ b/dsl/extdeps/languages/python/primitives.dag @@ -34,9 +34,11 @@ // (`PythonPrimitive = …`) is walkable for Engine / future loaders. // // LESSON 5 (grounding-pilot-receipt.md): subset-only axes are structurally -// partitioned — string algebra/carrier tags live only on PythonStringPrimitive; -// integer carrier discipline lives only on PythonIntegerPrimitive; the -// terminal sentinel pair lives only on PythonUnitPrimitive. +// partitioned — every `PythonPrimitive` variant carries its own per-variant +// algebra-tag and carrier-tag witness types, so any algebra/carrier pair +// other than the spec-valid one is unrepresentable by construction (no +// `PythonBooleanPrimitive { algebra: TerminalAlgebra }`, +// no `PythonIntegerPrimitive { carrier: BitCarrier }`). // // STRING (language ref §"Text Sequence Type — str", // docs.python.org/3/library/stdtypes.html#textseq): a `str` value is an @@ -50,7 +52,7 @@ // SUBSTRATE-GAP FLAGS: // 1. Python `int` is arbitrary precision — no fixed-width carrier and no // modular-wrap overflow. Tranche-1 models this with the -// `PythonUnboundedIntegerCarrier` sentinel (no `range_min/max`, +// `PythonIntUnboundedCarrier` sentinel (no `range_min/max`, // no `overflow` field) so consumers cannot read a false fixed width. // Post-DB-11 / cardinality substrate this becomes // `OrderedRing` with countably-infinite @@ -62,137 +64,160 @@ // the int-coercion edge — that lives in coercion / operator slices, // not on the predeclared primitive row. // 3. Algebra and carrier identity is still carried by structural tags -// (`PythonIntegerAlgebra` / `PythonNonIntegerAlgebra` / -// `PythonTargetCarrier` / `PythonSpecString*Tag`), same bridge pattern -// as rust/primitives.dag and go/primitives.dag, until the .dag -// substrate exposes type expressions as data values. +// (per-variant `PythonSpecAlgebraTag` / +// `PythonSpecCarrierTag`), same bridge pattern as +// rust/primitives.dag and go/primitives.dag, until the .dag substrate +// exposes type expressions as data values. module extdeps.languages.python.primitives // ========================================================================= -// Algebra tags, partitioned by integer / non-integer / string class. +// Per-variant algebra / carrier witness tags. +// +// State-space modeling discipline: each `PythonPrimitive` variant gets its +// own dedicated algebra-tag and carrier-tag sum, so the spec-valid +// (algebra, carrier) pair is the *only* representable assignment for that +// row. Sharing a broad `PythonNonIntegerAlgebra` across Boolean and Unit +// (or a broad `PythonTargetCarrier` across Integer / Boolean / Unit) would +// admit nonsense rows like `PythonBooleanPrimitive { algebra: TerminalAlgebra }` +// — illegal-states-unrepresentable forbids that. // // Practice 4 (docs/modeling-discipline.md) ledger annotations follow the -// post-#1046 Go file style: each closed coproduct names its GREEN -// (terminal / consumed) and YELLOW (parse-scaffold reserved) arms. -// Single-arm `type X = Tag` declarations leave `Tag` unresolved in the -// v2 bootstrap compiler — every coproduct below has ≥2 arms by -// construction, with reserved arms named for their dissolution trigger. +// post-#1046 Go file style: each closed coproduct names its **🟢 GREEN** +// (terminal / consumed) arm and its **🟡 YELLOW** (parse-scaffold reserved) +// arm. Every coproduct below has ≥2 arms by construction (v2 bootstrap +// loader rejects unary `type X = Tag` aliases), with reserved arms named +// for their dissolution trigger: bootstrap / loader closes single-arm sums, +// at which point the reserved arms (and these per-variant tag types +// entirely) collapse into direct algebra/carrier references — see +// substrate-gap flag #3. // ========================================================================= -// Python `int` is the only spec-predeclared integer; it inhabits the -// (unbounded, signed) ordered ring. The reserved arm exists solely so the -// v2 bootstrap loader resolves `PythonIntegerAlgebra` as a sum, not a unary -// alias. -// -// Practice 4: **🟢 GREEN** — `PythonOrderedRingAlgebra` is the terminal -// algebra-tag for Python's spec integer. -// **🟡 YELLOW (scaffold)** — `PythonIntegerAlgebraReserved` exists only for -// the v2 "≥2 sum arms" tag-resolution constraint; named trigger: -// bootstrap / loader closes single-arm sums, OR a future stdlib-authority -// slice lands a second integer algebra row (e.g., a Semiring inhabitant -// from numerics packages — would still NOT belong on this language-spec -// row; reserved arm dissolves regardless). -type PythonIntegerAlgebra - = PythonOrderedRingAlgebra - | PythonIntegerAlgebraReserved - -// Bool + None share one closed algebra-tag sum (mirrors rust -// `NonIntegerAlgebra` and go `GoSpecDiscreteAlgebra` grouping). String is -// separate — its value-domain is a sequence monoid, not a discrete scalar. -// -// Practice 4: **🟢 GREEN (terminal coproduct).** Both arms are spec-realized -// and consumed: `PythonCanonicalTwoElementBooleanAlgebra` is the value-domain -// of `bool`; `PythonTerminalAlgebra` is the single-inhabitant algebra of -// `NoneType`. Each arm has a matching `PythonPrimitive` row in -// `python_spec_predeclared_primitives` / `python_dag_unit_target_primitive`. -type PythonNonIntegerAlgebra - = PythonCanonicalTwoElementBooleanAlgebra - | PythonTerminalAlgebra +// --- Integer primitive witness tags --- +// +// Practice 4: **🟢 GREEN** — `PythonIntOrderedRingAlgebra` is the terminal +// algebra-tag for Python's spec integer (signed, additive inverse exists). +// **🟡 YELLOW (scaffold)** — `PythonIntegerSpecAlgebraReserved`. +type PythonIntegerSpecAlgebraTag + = PythonIntOrderedRingAlgebra + | PythonIntegerSpecAlgebraReserved +// Practice 4: **🟢 GREEN** — `PythonIntUnboundedCarrier` is the honest +// declaration that Python `int` is arbitrary-precision (substrate-gap +// flag #1; DB-11 will refine to a countably-infinite cardinality witness). +// **🟡 YELLOW (scaffold)** — `PythonIntegerSpecCarrierReserved`. +type PythonIntegerSpecCarrierTag + = PythonIntUnboundedCarrier + | PythonIntegerSpecCarrierReserved -// ========================================================================= -// Target carrier tags (value-domain witnesses; not CPython object layout). -// -// `PythonUnboundedIntegerCarrier` is the honest declaration that Python's -// spec `int` is arbitrary-precision — there is no fixed bit-width and no -// modular-wrap field on `PythonIntegerPrimitive`. Substrate-gap flag #1 -// names DB-11 / cardinality dissolution. -// -// `PythonBitCarrier` and `PythonTerminalCarrier` mirror the Rust/Go -// convention of declaring the algebra value-domain witness (per -// `dsl/std/integer.dag:4` "Int is a CARRIER (Word64) with EVIDENCE…"), -// not CPython object representation (CPython stores both `True`/`False` -// as singleton PyBool objects; that is target-codegen / runtime, not -// algebra value-domain). -// -// Practice 4: **🟢 GREEN (terminal coproduct).** All three arms are -// consumed by tranche-1 rows: integer (UnboundedInteger), bool (Bit), and -// None (Terminal). No reserved scaffolds — three arms is already ≥2. -// ========================================================================= -type PythonTargetCarrier - = PythonUnboundedIntegerCarrier - | PythonBitCarrier - | PythonTerminalCarrier +// --- Boolean primitive witness tags --- +// +// Practice 4: **🟢 GREEN** — `PythonBoolCanonicalTwoElementBooleanAlgebra` +// is the terminal algebra-tag for Python's spec `bool`. +// **🟡 YELLOW (scaffold)** — `PythonBooleanSpecAlgebraReserved`. +type PythonBooleanSpecAlgebraTag + = PythonBoolCanonicalTwoElementBooleanAlgebra + | PythonBooleanSpecAlgebraReserved + +// Practice 4: **🟢 GREEN** — `PythonBoolBitCarrier` is the algebra +// value-domain witness for `bool` (per `dsl/std/integer.dag:4` carrier-vs- +// evidence convention; not CPython object representation). +// **🟡 YELLOW (scaffold)** — `PythonBooleanSpecCarrierReserved`. +type PythonBooleanSpecCarrierTag + = PythonBoolBitCarrier + | PythonBooleanSpecCarrierReserved -// String value = immutable Unicode code-point sequence (monoid + Unicode -// code-point carrier). Reserved arms are v2 parse scaffolding only (never -// used in data) — same single-arm-resolution issue as `PythonIntegerAlgebra`; -// do **not** add a UTF-8 / UTF-16 / encoding parallel authority here -// (header §STRING). +// --- String primitive witness tags --- // -// Practice 4: **🟢 GREEN** — first arms are the terminal string-value -// witnesses (algebra: immutable codepoint-sequence monoid; carrier: -// Unicode code-point sequence). **🟡 YELLOW (scaffold)** — reserved arms -// exist only for the v2 "≥2 sum arms" tag-resolution constraint; named -// trigger: bootstrap / loader closes single-arm sums. -type PythonSpecStringAlgebraTag - = PythonImmutableUnicodeCodePointSequenceMonoidAlgebra - | PythonSpecStringAlgebraParseReserved +// Practice 4: **🟢 GREEN** — +// `PythonStrImmutableUnicodeCodePointSequenceMonoidAlgebra` is the +// terminal algebra-tag for Python `str` (header §STRING). +// **🟡 YELLOW (scaffold)** — `PythonStringSpecAlgebraReserved`. Encoding +// (UTF-8 / UTF-16) is NOT a second arm here. +type PythonStringSpecAlgebraTag + = PythonStrImmutableUnicodeCodePointSequenceMonoidAlgebra + | PythonStringSpecAlgebraReserved -type PythonSpecStringCarrierTag - = PythonUnicodeCodePointSequenceCarrier - | PythonSpecStringCarrierParseReserved +// Practice 4: **🟢 GREEN** — `PythonStrUnicodeCodePointSequenceCarrier` is +// the terminal carrier-tag for Python `str`. +// **🟡 YELLOW (scaffold)** — `PythonStringSpecCarrierReserved`. +type PythonStringSpecCarrierTag + = PythonStrUnicodeCodePointSequenceCarrier + | PythonStringSpecCarrierReserved + + +// --- Unit (None / NoneType) primitive witness tags --- +// +// Practice 4: **🟢 GREEN** — `PythonUnitTerminalAlgebra` is the +// single-inhabitant algebra of `NoneType`. +// **🟡 YELLOW (scaffold)** — `PythonUnitSpecAlgebraReserved`. +type PythonUnitSpecAlgebraTag + = PythonUnitTerminalAlgebra + | PythonUnitSpecAlgebraReserved + +// Practice 4: **🟢 GREEN** — `PythonUnitTerminalCarrier` is the +// single-inhabitant carrier sentinel for `None` (DB-11 will refine to +// `Cardinality`). +// **🟡 YELLOW (scaffold)** — `PythonUnitSpecCarrierReserved`. +type PythonUnitSpecCarrierTag + = PythonUnitTerminalCarrier + | PythonUnitSpecCarrierReserved // ========================================================================= // Sum-typed Python spec primitive (Lesson 5 partition). // // Sum-typed so each spec primitive's structurally-meaningful axes attach -// only where they have meaning: integer carrier discipline only on -// `PythonIntegerPrimitive`; string algebra/carrier tags only on -// `PythonStringPrimitive`. State-space modeling discipline — no -// `bool: PythonUnboundedIntegerCarrier`, no `int: PythonUnicodeCodePointSequenceCarrier`. +// only where they have meaning, AND each variant's algebra/carrier fields +// are typed by per-variant singleton-tag pairs (see witness-tag block +// above) — illegal-states-unrepresentable: a `PythonBooleanPrimitive` can +// only carry `PythonBoolCanonicalTwoElementBooleanAlgebra` and +// `PythonBoolBitCarrier`; a `PythonIntegerPrimitive` can only carry +// `PythonIntOrderedRingAlgebra` and `PythonIntUnboundedCarrier`; etc. // // No `range_min/max` and no `overflow` field on `PythonIntegerPrimitive`: // substrate-gap flag #1 — Python's spec `int` is unbounded, so a // fixed-range / fixed-overflow row would be a lie. Consumers needing // concrete-width integer routing should consult target-specific lanes // (Rust / Go `*_integer_range` rows) rather than synthesizing a width here. +// +// Practice 4 (docs/modeling-discipline.md): **🟢 GREEN (terminal coproduct).** +// Ledger — all four arms are spec-realized and consumed; each has a +// matching row in `python_spec_predeclared_primitives` / +// `python_dag_unit_target_primitive`: +// - `PythonIntegerPrimitive` ↔ row `int` (spec §"Numeric Types" — int). +// - `PythonBooleanPrimitive` ↔ row `bool` (spec §"Boolean Type — bool"). +// - `PythonStringPrimitive` ↔ row `str` (spec §"Text Sequence — str"). +// - `PythonUnitPrimitive` ↔ row `None` (spec §"The Null Object — None"). +// No reserved scaffold arm needed (already ≥2 arms by construction). +// Dissolution trigger for the partition itself: when DB-11 / cardinality +// substrate lets algebra+carrier be referenced as data, all four variants +// collapse into a single record-shaped row with refinement-typed fields, +// and `PythonPrimitive` retires alongside the per-variant witness tags. // ========================================================================= type PythonPrimitive = PythonIntegerPrimitive { target_name: String - algebra: PythonIntegerAlgebra - carrier: PythonTargetCarrier + algebra: PythonIntegerSpecAlgebraTag + carrier: PythonIntegerSpecCarrierTag } | PythonStringPrimitive { target_name: String - algebra: PythonSpecStringAlgebraTag - carrier: PythonSpecStringCarrierTag + algebra: PythonStringSpecAlgebraTag + carrier: PythonStringSpecCarrierTag } | PythonBooleanPrimitive { target_name: String - algebra: PythonNonIntegerAlgebra - carrier: PythonTargetCarrier + algebra: PythonBooleanSpecAlgebraTag + carrier: PythonBooleanSpecCarrierTag } | PythonUnitPrimitive { target_name: String - algebra: PythonNonIntegerAlgebra - carrier: PythonTargetCarrier + algebra: PythonUnitSpecAlgebraTag + carrier: PythonUnitSpecCarrierTag } @@ -206,16 +231,16 @@ type PythonPrimitive // `bytes` / `bytearray` deferred to next tranche. data python_spec_predeclared_primitives: List = [ PythonIntegerPrimitive { target_name: "int", - algebra: PythonOrderedRingAlgebra, - carrier: PythonUnboundedIntegerCarrier }, + algebra: PythonIntOrderedRingAlgebra, + carrier: PythonIntUnboundedCarrier }, PythonBooleanPrimitive { target_name: "bool", - algebra: PythonCanonicalTwoElementBooleanAlgebra, - carrier: PythonBitCarrier }, + algebra: PythonBoolCanonicalTwoElementBooleanAlgebra, + carrier: PythonBoolBitCarrier }, PythonStringPrimitive { target_name: "str", - algebra: PythonImmutableUnicodeCodePointSequenceMonoidAlgebra, - carrier: PythonUnicodeCodePointSequenceCarrier } + algebra: PythonStrImmutableUnicodeCodePointSequenceMonoidAlgebra, + carrier: PythonStrUnicodeCodePointSequenceCarrier } ] // DAG Unit → Python: `None` (the sole inhabitant of `NoneType`) is the @@ -228,6 +253,6 @@ data python_spec_predeclared_primitives: List = [ // `python_type_checkpoints` in `python/types.dag`. data python_dag_unit_target_primitive: PythonPrimitive = PythonUnitPrimitive { target_name: "None", - algebra: PythonTerminalAlgebra, - carrier: PythonTerminalCarrier + algebra: PythonUnitTerminalAlgebra, + carrier: PythonUnitTerminalCarrier } From 7d841b93c47561f010b3366529208a5c98b7b02e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 28 Apr 2026 02:34:44 +0000 Subject: [PATCH 3/4] T-Ground-Python: fix stale ValueBody::Unparsed live-state claim MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Address codex NON-BLOCKING (P1 Documentation Describes Live State) on PR #1080 sha f4d6d09a: header claimed top-level rows lower as `ValueBody::Unparsed` until aggregate sub-lane lands. That is stale — `rust_pilot_primitives` already lowers as `ValueBody::List` per `src/v3/grounding_engine/src/lib.rs:7` (registered via `src/v3/std/extdeps_bootstrap_fixtures.dag:23`). Narrow the claim: aggregate lowering is live; what's not yet live for this file is fixture registration + a Python-grounding engine consumer. Path-2 staging language preserved but qualified to the fixture-registration sense, not the lowering sense. Co-Authored-By: Claude Opus 4.7 (1M context) --- dsl/extdeps/languages/python/primitives.dag | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/dsl/extdeps/languages/python/primitives.dag b/dsl/extdeps/languages/python/primitives.dag index 2f236fd7d3d..ec6094a9a5d 100644 --- a/dsl/extdeps/languages/python/primitives.dag +++ b/dsl/extdeps/languages/python/primitives.dag @@ -27,11 +27,16 @@ // python/types.dag + emit tables until a dedicated stdlib-authority // slice lands; do not cite stdlib paths here. // -// CONSUMER BOUNDARY: same Path-2 honest state as rust/primitives.dag and -// go/primitives.dag — the top-level `python_spec_predeclared_primitives` -// list and `python_dag_unit_target_primitive` lower as `ValueBody::Unparsed` -// until R2 T-Substrate's top-level aggregate sub-lane lands; type-structure -// (`PythonPrimitive = …`) is walkable for Engine / future loaders. +// CONSUMER BOUNDARY: top-level list / record `ValueBody` aggregates lower +// structurally today (rust_pilot_primitives is loaded as `ValueBody::List` +// by `src/v3/grounding_engine/src/lib.rs:7`, registered via +// `src/v3/std/extdeps_bootstrap_fixtures.dag:23`). What is *not* yet live +// for this file: no `ExtdepsBootstrapFixture` row has been registered for +// `python_spec_predeclared_primitives` or `python_dag_unit_target_primitive`, +// and there is no Python-grounding engine consumer in-tree yet — so today +// these rows are loaded but unconsumed (Path-2 staging in the +// fixture-registration sense, not in the lowering sense). Type-structure +// (`PythonPrimitive = …`) is walkable for the future engine consumer. // // LESSON 5 (grounding-pilot-receipt.md): subset-only axes are structurally // partitioned — every `PythonPrimitive` variant carries its own per-variant From 8bab3867310f5bdd981d60e43093636b5f87d2bf Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 28 Apr 2026 02:35:39 +0000 Subject: [PATCH 4/4] =?UTF-8?q?T-Ground-Python:=20relabel=20PythonPrimitiv?= =?UTF-8?q?e=20partition=20GREEN=20=E2=86=92=20YELLOW?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Address codex non-blocking on PR #1080 sha f4d6d09a: the partition was labeled GREEN while the same comment named a DB-11/cardinality dissolution trigger — that's YELLOW (scheduled scaffold), not GREEN (terminal). Arms remain individually populated; only the partition-level classification changes. Co-Authored-By: Claude Opus 4.7 (1M context) --- dsl/extdeps/languages/python/primitives.dag | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/dsl/extdeps/languages/python/primitives.dag b/dsl/extdeps/languages/python/primitives.dag index ec6094a9a5d..7b5709e848a 100644 --- a/dsl/extdeps/languages/python/primitives.dag +++ b/dsl/extdeps/languages/python/primitives.dag @@ -188,19 +188,20 @@ type PythonUnitSpecCarrierTag // concrete-width integer routing should consult target-specific lanes // (Rust / Go `*_integer_range` rows) rather than synthesizing a width here. // -// Practice 4 (docs/modeling-discipline.md): **🟢 GREEN (terminal coproduct).** -// Ledger — all four arms are spec-realized and consumed; each has a -// matching row in `python_spec_predeclared_primitives` / -// `python_dag_unit_target_primitive`: +// Practice 4 (docs/modeling-discipline.md): **🟡 YELLOW (scheduled +// scaffold).** All four arms are spec-realized and consumed today (each +// has a matching row in `python_spec_predeclared_primitives` / +// `python_dag_unit_target_primitive`): // - `PythonIntegerPrimitive` ↔ row `int` (spec §"Numeric Types" — int). // - `PythonBooleanPrimitive` ↔ row `bool` (spec §"Boolean Type — bool"). // - `PythonStringPrimitive` ↔ row `str` (spec §"Text Sequence — str"). // - `PythonUnitPrimitive` ↔ row `None` (spec §"The Null Object — None"). -// No reserved scaffold arm needed (already ≥2 arms by construction). -// Dissolution trigger for the partition itself: when DB-11 / cardinality +// The partition itself is YELLOW (not GREEN) because its end-state is +// dissolution, not steady-state coexistence: when DB-11 / cardinality // substrate lets algebra+carrier be referenced as data, all four variants // collapse into a single record-shaped row with refinement-typed fields, // and `PythonPrimitive` retires alongside the per-variant witness tags. +// Dissolution trigger: DB-11 / cardinality substrate (named). // ========================================================================= type PythonPrimitive