Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
73 commits
Select commit Hold shift + click to select a range
e3725a5
WIP: valiant-ibex-312
briansrls May 5, 2026
f87de65
fix(v3): close nested-optional cardinality codegen bypass (Path B ren…
briansrls May 5, 2026
195377e
fix(v3): refresh bootstrap generated snapshots via regen_bootstrap
briansrls May 5, 2026
31cab64
ci: empty-commit retrigger for #1803 self_host_ratchet runner-budget …
briansrls May 6, 2026
cdd9778
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
a9dadaa
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
273aefc
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
384217e
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
d400a92
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
ce25cb6
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
eaf36c0
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
81cb31f
WIP: valiant-ibex-312
briansrls May 6, 2026
d47b122
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
9ccfe16
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
3e3c320
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
25a6cf4
fix(measure): typed scale_exponent authority + constrained-inhabitanc…
briansrls May 6, 2026
4e4859d
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
b38f007
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
919681b
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
8058d29
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
724fcdc
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
819e0ef
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
ac62e02
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
90b991e
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
c0cf5ef
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
cddc251
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
e7c97f9
WIP: valiant-ibex-312
briansrls May 6, 2026
2eb2632
WIP: valiant-ibex-312
briansrls May 6, 2026
01df58e
test(r3-l6): wire cross_target_coverage carrier ratchet through SG-0
briansrls May 6, 2026
da1ada8
fix(r3-l6): four-pattern dissolution receipt for ShapeATarget 🟢 TERMINAL
briansrls May 6, 2026
b179018
ci: re-trigger after PR body SG-0 hand-path delta line restoration
briansrls May 6, 2026
2dd990b
WIP: valiant-ibex-312
briansrls May 6, 2026
103ef13
test(r3-l6): tighten ratchet to assert exact variant labels + record …
briansrls May 6, 2026
bcbb856
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
06bad65
docs(sg0-census): correct PR-number cite (this is #1842, precedent #1…
briansrls May 6, 2026
62d3e67
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
2c9de32
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
989ad70
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
2f26cd3
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
bae5f01
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
3e8e833
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
7d91345
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
0b4686a
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
f53b8aa
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
fad2902
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
2e5274a
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
8b64aeb
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
4ded97f
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
5243bcd
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
207980d
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
002ea5e
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
037548f
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
d3a153a
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
a17db56
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
e7ba022
feat(v3): widen IntervalInt::ExactInterval host repr to BigInt (R3 Ph…
briansrls May 6, 2026
bc5ea81
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 6, 2026
3e6c821
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 7, 2026
0bc89da
docs(v3): refresh module-level doc to match BigInt host repr
briansrls May 7, 2026
652ad27
WIP: valiant-ibex-312
briansrls May 7, 2026
078b5e8
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 7, 2026
5951150
feat(v3): add u128 IntegerPrimitive row to rust_pilot_primitives (R3 …
briansrls May 7, 2026
f994e1f
feat(v3): add u128 TypeRealization + inhabitance row to spec/rust.dag…
briansrls May 7, 2026
b6989ec
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 7, 2026
272db6c
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 7, 2026
cf1ea78
docs(v3): align EXPECTED_INTEGER_ROWS comment with live state (10 rows)
briansrls May 7, 2026
05b84bb
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 7, 2026
48806f1
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 7, 2026
9dc2017
docs(rust-primitives): refresh PILOT SCOPE / Slice B2 header to live …
briansrls May 7, 2026
9a28fbe
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 7, 2026
be8e4b2
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 7, 2026
7c64505
WIP: valiant-ibex-312
briansrls May 7, 2026
f4b31e6
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 7, 2026
4844bbb
Merge remote-tracking branch 'origin/main' into session/valiant-ibex-312
briansrls May 7, 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
32 changes: 32 additions & 0 deletions dsl/std/integer.dag
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ module std.integer
import std.algebra { OrderedRing, Semiring, AbelianGroup, GroupCompletion }
import std.bit { Byte, Word16, Word32, Word64, Word128 }
import std.nat { Nat }
import std.machine_constraints { Compose, MachineWidth, PointerWidth }

// Signed integers: ordered rings (add + negate + mul + compare)
type Int8 = OrderedRing<Byte>
Expand Down Expand Up @@ -110,6 +111,37 @@ type UInt128 = Semiring<Word128>
type Int = AbelianGroup<GroupCompletion<Nat>>
type UInt = Nat

// IntPlatform / UIntPlatform — pointer-width-sized integer substrate concepts.
//
// Per Director Q1+Q2+Q3+Q4 RATIFIED at gunbc#1739 #issuecomment-4393248961
// (2026-05-07) + inner-token rename `Platform` → `PointerWidth` RATIFIED
// at gunbc#828 #issuecomment-4393616097. Outer carrier names
// `IntPlatform`/`UIntPlatform` stay verbatim (Q1 RATIFIED). Inner substrate
// token is `PointerWidth` to avoid collision with pre-existing
// `Platform = Linux | Macos | Windows` (OS-identity axis) at
// `dsl/std/types.dag:356`; per `feedback_reason_not_label`, pointer-width
// is the structural reason and OS-identity vs pointer-width are
// orthogonal axes (32-bit Linux vs 64-bit Linux are different pointer
// widths but same OS).
//
// Composition per Q-MachineConstraint-Carrier sub-decision 3
// (gunbc#828 #issuecomment-4385530115) extended with substrate token
// `PointerWidth` per Q3 ratification (substrate-concept layer, NOT target-
// only) — `MachineWidth<PointerWidth>` resolves at Grounding-emit time
// per target spec; substrate stays target-agnostic.
//
// Direct-consumer site: `src/v3/spec/rust.dag` `TargetIntegerTypeInhabitance`
// rows for `isize` (kernel_integer = IntPlatform) and `usize`
// (kernel_integer = UIntPlatform) with `bound: PlatformDependentFact`.
// Targets without native pointer-sized integers (Python's arbitrary-
// precision `int`, etc.) handle ground-time projection via target-
// conditioned **lowering** — substrate stays clean (Grounding-lane work).
//
// Practice 4: N/A — type aliases over existing `Compose<...>` carrier;
// no new sum types or coproducts introduced here.
type IntPlatform = Compose<Int, MachineWidth<PointerWidth>>
type UIntPlatform = Compose<UInt, MachineWidth<PointerWidth>>

// Nat-alignment refinements (S9 Slice 2 / Slice 2.5 / Phase-4).
//
// NonNegativeInt formerly lived in dsl/std/types.dag refining Int with a
Expand Down
49 changes: 49 additions & 0 deletions dsl/std/machine_constraints.dag
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,55 @@ module std.machine_constraints
// `Nat` carrier — then delete this block and re-measure consumers.
type MachineWidth<bits>

// ----------------------------------------------------------------------------
// PointerWidth — substrate token for target-resolved pointer-width axis.
// ----------------------------------------------------------------------------
//
// Per Director Q1+Q2+Q3+Q4 RATIFIED at gunbc#1739 #issuecomment-4393248961
// (2026-05-07) + inner-token rename `Platform` → `PointerWidth` RATIFIED at
// gunbc#828 #issuecomment-4393616097 (per `feedback_reason_not_label` —
// pointer-width is the structural reason; the original brief framing
// collided with pre-existing `Platform = Linux | Macos | Windows` at
// `dsl/std/types.dag:356`, which is the OS-identity axis, NOT the pointer-
// width axis; conflating them would lose orthogonality).
//
// `PointerWidth` names the target-resolved pointer-width axis at substrate-
// concept layer (NOT target-only) per `feedback_target_agnostic_ir`:
// multiple targets carry pointer-sized integers (Rust `isize`/`usize`, Go
// `int`/`uint`, C `intptr_t`, …); modeling at substrate-concept layer keeps
// substrate target-agnostic and lets Grounding project to specific widths
// at emit time.
//
// **Shape: opaque token** (Option β per worker-DFS at dispatch). Sibling to
// the phantom-`bits` parameter on `MachineWidth<bits>`: where `bits = 32`
// resolves at substrate-load time (literal `Nat` index), `bits = PointerWidth`
// resolves at Grounding-emit time (target-conditioned width). No payload at
// the substrate-concept layer — Grounding consumers project `PointerWidth`
// to the per-target width (Rust pointer-width 32/64, Go `int` width, etc.).
//
// Practice 4 dissolution ledger (nominal opaque carrier; no coproduct variants):
// - Pattern 1 (fact placement): fails — `PointerWidth` centralizes the
// "target-resolved pointer-width" axis; one slot per use, not multiple
// competing slots.
// - Pattern 2 (variant-is-data): n/a — no variants.
// - Pattern 3 (algebraic form): fails — `PointerWidth` is a target-
// resolution tag, not an algebraic operation over widths.
// - Pattern 4 (dimensional): fails — target-resolved pointer-width is an
// irreducible substrate fact at this layer; per-target enumeration is
// Grounding's job (concrete width 32 / 64 etc. lands at emit time).
// Verdict: terminal at substrate-concept layer.
//
// CONSTRAINED-INHABITANCE GAP (mirrors `MachineWidth<bits>`'s P2/P5 scaffold):
// Same parser-parallel constraint posture — `PointerWidth` is consumed as
// a `MachineWidth<PointerWidth>` argument; mechanical width-projection
// is Grounding's enforcement. No structural `PointerWidth : Nat` bound
// at parse time (substrate grammar gap).
//
// **Dissolution trigger:** when substrate grammar admits bounded type-
// level parameters (the same trigger named on `MachineWidth<bits>` above),
// tighten `PointerWidth`'s constraint surface alongside.
type PointerWidth

// ----------------------------------------------------------------------------
// Compose<Algebra, MachineConstraint> — type-level phantom composition (ratified interaction shape).
// ----------------------------------------------------------------------------
Expand Down
Loading
Loading