Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
73df0cc
WIP: v4 T-4 combined #3200 merged-main reclass-PR (comment-only, no-u…
briansrls May 16, 2026
ee9a051
v4 T-4 #3200 reclass: llvm_ir.dag (7) + go.dag (4) widths πŸŸ’β†’πŸŸ‘ (commen…
briansrls May 16, 2026
83afba8
v4 T-4 #3200 reclass: add ledger-header flip + rust.dag widths
briansrls May 16, 2026
62d8d3d
Merge remote-tracking branch 'origin/main' into session/snappy-otter-…
briansrls May 17, 2026
9531d4e
WIP: v4 T-4 combined #3200 merged-main reclass-PR (comment-only, no-u…
briansrls May 17, 2026
69392ed
v4 T-4 #3215 fix: BLOCKING β€” rewrite ConversionOpcode/AtomicRmwOp/Bin…
briansrls May 17, 2026
45434d1
Merge remote-tracking branch 'origin/main' into session/snappy-otter-…
briansrls May 17, 2026
18d0b80
WIP: v4 T-4 combined #3200 merged-main reclass-PR (comment-only, no-u…
briansrls May 17, 2026
d46499f
v4 T-4 #3215 fix: BLOCKING β€” split landed-ontology from per-op-witnes…
briansrls May 17, 2026
8db67bd
v4 T-4 #3215 precision: tighten landed-witness inventory to FIVE (was…
briansrls May 17, 2026
0b40c53
Merge remote-tracking branch 'origin/main' into session/snappy-otter-…
briansrls May 17, 2026
82c9921
v4 T-4 #3215 fix: BLOCKING β€” ConversionOpcode keep shape only; fptoui…
briansrls May 17, 2026
74c3f79
v4 T-4 #3215 re-point: ConversionOpcode deferral owner = TBD per extd…
briansrls May 17, 2026
0be3260
Merge remote-tracking branch 'origin/main' into session/snappy-otter-…
briansrls May 17, 2026
017f8ca
Merge remote-tracking branch 'origin/main' into session/snappy-otter-…
briansrls May 17, 2026
c8ff7aa
Merge remote-tracking branch 'origin/main' into session/snappy-otter-…
briansrls May 17, 2026
c49f6ba
Merge remote-tracking branch 'origin/main' into session/snappy-otter-…
briansrls May 17, 2026
e6bfce1
Merge remote-tracking branch 'origin/main' into session/snappy-otter-…
briansrls May 17, 2026
ac3fa7d
Merge remote-tracking branch 'origin/main' into session/snappy-otter-…
briansrls May 17, 2026
0f89536
v4 T-4 #3215 fix: BLOCKING β€” ConversionOpcode std/ptr.dag phantom-aut…
briansrls May 17, 2026
d0914c5
Merge remote-tracking branch 'origin/main' into session/snappy-otter-…
briansrls May 17, 2026
60a2759
Merge remote-tracking branch 'origin/main' into session/snappy-otter-…
briansrls May 17, 2026
e803c21
Merge remote-tracking branch 'origin/main' into session/snappy-otter-…
briansrls May 17, 2026
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
111 changes: 107 additions & 4 deletions src/v4/extdeps/languages/go.dag
Original file line number Diff line number Diff line change
Expand Up @@ -539,7 +539,10 @@ import v4.std.node { Symbol }
// an edit to THIS declaration under the L-2 pin discipline.
//
// Coproduct dissolution (Practice 4 / modeling-discipline.md Β§4) β€”
// 🟒 GREEN (terminal). Ledger β€” five patterns attempted:
// 🟑 YELLOW (deferred-on-consumer; re-scoped under #3200 rule-change
// 2026-05-16 β€” namable richer source exists per standing width-enum
// precedent; see #3200 RE-SCOPE footer before the type declaration
// below). Ledger β€” five patterns attempted:
// 1. Fact placement β€” FAILS: every signed-integer-scalar consumer
// (emission of `int32` vs `int64`; per-target cost-realization
// sizes; the eventual std/integer.dag inhabitance + D2a(3)
Expand Down Expand Up @@ -577,6 +580,29 @@ import v4.std.node { Symbol }
// not all `F<bit-count: Int>`.
// Terminal: the closed five-way Go signed-integer-width classifier
// for the pinned Go Specification.
//
// #3200 RE-SCOPE (rule-change 2026-05-16, docs/modeling-discipline.md
// merged on origin/main): under the pre-#3200 consumer-DEPENDENT GREEN
// rule this width classifier was correctly GREEN. Under the post-#3200
// consumer-INDEPENDENT rule this is 🟑 YELLOW per the standing
// width-enum-family precedent (operator ruling 2026-05-16 per T-4 mgr
// msg_5c6cbb48: "yellow please" β€” any width-enum across the lane flips
// 🟑 per Practice-7-projection-over-Nat richer-source):
// Richer source: bit-counts project from Nat β€” SignedBits8/16/32/64
// are F<bit-count: Nat> over the spec's stabilized signed widths;
// SignedPlatformInt is a `PlatformDependent` discriminant cell on
// the same axis. A future std/integer.dag width carrier would name
// this Nat-projection authoritatively.
// Trigger: first consumer of width MEANING (cost-realization sizes /
// std/integer.dag bounded-Int inhabitance / D2a(3) silent-wrap
// resolver β€” D2 pathway).
// Obligation: the first meaning-consumer owes the (bit-count |
// platform-dependent) decomposition AT that consumer (a lens
// read), NOT a local match-over-width lookup in this carrier; the
// Go spec keyword (`int8` / `int`) stays the parse/emit-side
// authority. Per the cited operator ruling, do NOT fold this 🟑
// into a fresh push; track for the next review-tail commit on any
// touching PR.
type SignedIntWidth
= SignedBits8
| SignedBits16
Expand Down Expand Up @@ -633,7 +659,10 @@ type SignedIntWidth
// P1 modeling-faithfulness requires.
//
// Coproduct dissolution (Practice 4 / modeling-discipline.md Β§4) β€”
// 🟒 GREEN (terminal). Ledger β€” five patterns attempted:
// 🟑 YELLOW (deferred-on-consumer; re-scoped under #3200 rule-change
// 2026-05-16 β€” namable richer source exists per standing width-enum
// precedent; see #3200 RE-SCOPE footer before the type declaration
// below). Ledger β€” five patterns attempted:
// 1. Fact placement β€” FAILS: every unsigned-integer-scalar consumer
// reads the width to size representations (emission of `uint32`
// vs `uint64` vs `uintptr`; per-target cost-realization sizes);
Expand All @@ -659,6 +688,29 @@ type SignedIntWidth
// each other per spec) β€” they are not all `F<bit-count: Int>`.
// Terminal: the closed six-way Go unsigned-integer-width classifier
// for the pinned Go Specification.
//
// #3200 RE-SCOPE (rule-change 2026-05-16, docs/modeling-discipline.md
// merged on origin/main): under the pre-#3200 consumer-DEPENDENT GREEN
// rule this width classifier was correctly GREEN. Under the post-#3200
// consumer-INDEPENDENT rule this is 🟑 YELLOW per the standing
// width-enum-family precedent (operator ruling 2026-05-16 per T-4 mgr
// msg_5c6cbb48):
// Richer source: bit-counts project from Nat β€” UnsignedBits8/16/32/
// 64 are F<bit-count: Nat>; UnsignedPlatformInt and Unsigned-
// PointerSized are two distinct `PlatformDependent` discriminant
// cells on the same axis (the asymmetry vs Signed is captured by
// a second platform-dependent cell, not a different axis). A
// future std/integer.dag width carrier would name this Nat-
// projection authoritatively.
// Trigger: first consumer of width MEANING (cost-realization sizes /
// std/integer.dag bounded-UInt inhabitance β€” D2 pathway).
// Obligation: the first meaning-consumer owes the (bit-count |
// platform-dependent-cell) decomposition AT that consumer (a lens
// read), NOT a local match-over-width lookup in this carrier; the
// Go spec keyword (`uint16` / `uintptr`) stays the parse/emit-side
// authority. Per the cited operator ruling, do NOT fold this 🟑
// into a fresh push; track for the next review-tail commit on any
// touching PR.
type UnsignedIntWidth
= UnsignedBits8
| UnsignedBits16
Expand All @@ -683,7 +735,10 @@ type UnsignedIntWidth
// the L-2 pin discipline.
//
// Coproduct dissolution (Practice 4 / modeling-discipline.md Β§4) β€”
// 🟒 GREEN (terminal). Ledger β€” five patterns attempted:
// 🟑 YELLOW (deferred-on-consumer; re-scoped under #3200 rule-change
// 2026-05-16 β€” namable richer source exists per standing width-enum
// precedent; see #3200 RE-SCOPE footer before the type declaration
// below). Ledger β€” five patterns attempted:
// 1. Fact placement β€” FAILS: every float-scalar consumer reads the
// width to size representations (emission of `float32` vs
// `float64`; cost-realization for floating-point ops); shared
Expand Down Expand Up @@ -713,6 +768,27 @@ type UnsignedIntWidth
// Go stabilizes" is the partition discriminant, not a
// parameterization of a richer source set.
// Terminal: the closed two-way Go stable-float-width classifier.
//
// #3200 RE-SCOPE (rule-change 2026-05-16, docs/modeling-discipline.md
// merged on origin/main): under the pre-#3200 consumer-DEPENDENT GREEN
// rule this width classifier was correctly GREEN. Under the post-#3200
// consumer-INDEPENDENT rule this is 🟑 YELLOW per the standing
// width-enum-family precedent (operator ruling 2026-05-16 per T-4 mgr
// msg_5c6cbb48):
// Richer source: bit-counts project from Nat (and from the IEEE-754
// binaryN universe `{16, 32, 64, 128, …}`) β€” Bits32 / Bits64 are
// F<bit-count: Nat> selecting the Go-stabilized subset. A future
// std/float.dag width carrier (the ApproximateField partition
// across IEEE-754 binaryN) would name this projection
// authoritatively.
// Trigger: first consumer of float-width MEANING (cost-realization
// sizes / std/float.dag ApproximateField instance β€” D2 pathway).
// Obligation: the first meaning-consumer owes the bit-count
// decomposition AT that consumer (a lens read), NOT a local
// match-over-width lookup; the Go spec keyword (`float32` /
// `float64`) stays the parse/emit-side authority. Per the cited
// operator ruling, do NOT fold this 🟑 into a fresh push; track
// for the next review-tail commit on any touching PR.
type GoFloatWidth
= Bits32
| Bits64
Expand Down Expand Up @@ -748,7 +824,10 @@ type GoFloatWidth
// `num-complex`, which are programs per L-2, NOT primitives).
//
// Coproduct dissolution (Practice 4 / modeling-discipline.md Β§4) β€”
// 🟒 GREEN (terminal). Ledger β€” five patterns attempted:
// 🟑 YELLOW (deferred-on-consumer; re-scoped under #3200 rule-change
// 2026-05-16 β€” namable richer source exists per standing width-enum
// precedent; see #3200 RE-SCOPE footer before the type declaration
// below). Ledger β€” five patterns attempted:
// 1. Fact placement β€” FAILS: every complex-scalar consumer reads
// the width to size representations (emission of `complex64`
// vs `complex128`; cost-realization for complex ops which
Expand Down Expand Up @@ -779,6 +858,30 @@ type GoFloatWidth
// projection is observed in commentary, not encoded as a
// Practice 7 collapse.
// Terminal: the closed two-way Go stable-complex-width classifier.
//
// #3200 RE-SCOPE (rule-change 2026-05-16, docs/modeling-discipline.md
// merged on origin/main): under the pre-#3200 consumer-DEPENDENT GREEN
// rule this width classifier was correctly GREEN (pattern 5 already
// noted the PARTIAL projection from GoFloatWidth). Under the post-
// #3200 consumer-INDEPENDENT rule this is 🟑 YELLOW per the standing
// width-enum-family precedent (operator ruling 2026-05-16 per T-4 mgr
// msg_5c6cbb48):
// Richer source: bit-counts project from Nat AND from GoFloatWidth
// (Bits64 = complex-of-Bits32, Bits128 = complex-of-Bits64) β€”
// `F<X> = complex-of-float-width-X` is the namable projection
// pattern-5 already identified as INCIDENTAL but real. A future
// std/complex.dag (the ApproximateField-of-Conj-of-two-same-width-
// floats partition) would name this Nat/GoFloatWidth projection
// authoritatively.
// Trigger: first consumer of complex-width MEANING (cost-realization
// sizes β€” decomposed into per-component float ops; std/complex
// ApproximateField instance β€” D2 pathway).
// Obligation: the first meaning-consumer owes the (component-float-
// width) decomposition AT that consumer (a lens read), NOT a local
// match-over-width lookup; the Go spec keyword (`complex64` /
// `complex128`) stays the parse/emit-side authority. Per the cited
// operator ruling, do NOT fold this 🟑 into a fresh push; track
// for the next review-tail commit on any touching PR.
type GoComplexWidth
= Bits64
| Bits128
Expand Down
Loading
Loading