From 005d784064017a4dd8673fa2178c2250d07178d5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 14 Jun 2026 16:24:31 -0400 Subject: [PATCH 01/11] =?UTF-8?q?=C2=A710=20exec-contract:=20ArchitectureP?= =?UTF-8?q?rofile=20=E2=80=94=20join=20arch=20tag=20+=20CallingConvention?= =?UTF-8?q?=20+=20StackLayout?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit First std substrate piece on the gunbos lane after SyscallAbi/sysv_amd64 (#4870/#4877). ArchitectureProfile composes the arch-specific execution substrate (exec-contract ยง4) before format and invocation-surface join. - dsl/std/architecture_profile.dag โ€” ArchitectureProfile carrier; TargetArchitecture enum with ๐ŸŸก cpu-architecture-unification gate (std.cpu.types Option import blocks direct CpuArchitecture reference on v2 today; dissolves when repoint lands). - dsl/extdeps/runtime/architecture/x86_64_linux.dag โ€” Slice-1 inhabitant wiring X86_64 + sysv_amd64_linux_syscall_convention + downward stack (psABI cited). Green-by-execution (dsl-rooted claim-run, head worktree): witness_architecture_is_x86_64 -> true witness_convention_arg3_is_r10 -> true witness_stack_grows_down -> true witness_profile_convention_matches_sysv_amd64 -> true Next slices: aapcs64 (2nd ABI), std/exec_format + extdeps/formats/elf. Co-authored-by: Cursor --- .../runtime/architecture/x86_64_linux.dag | 44 +++++++++++++++++++ dsl/std/architecture_profile.dag | 19 ++++++++ 2 files changed, 63 insertions(+) create mode 100644 dsl/extdeps/runtime/architecture/x86_64_linux.dag create mode 100644 dsl/std/architecture_profile.dag diff --git a/dsl/extdeps/runtime/architecture/x86_64_linux.dag b/dsl/extdeps/runtime/architecture/x86_64_linux.dag new file mode 100644 index 00000000000..eebf805aaef --- /dev/null +++ b/dsl/extdeps/runtime/architecture/x86_64_linux.dag @@ -0,0 +1,44 @@ +// extdeps/runtime/architecture/x86_64_linux.dag โ€” x86-64 Linux architecture profile (cited facts). +// +// Scope: Slice-1 inhabitant of std.architecture_profile.ArchitectureProfile binding +// TargetArchitecture::X86_64 to the cited sysv_amd64 Linux syscall convention and downward stack. +// +// Anchor: https://refspecs.linuxfoundation.org/elf/x86_64-abi-0.99.pdf (ยง3.2.2 stack grows down) +// Anchor: https://github.com/torvalds/linux/blob/v6.8/arch/x86/entry/entry_64.S +// (entry_SYSCALL_64: rax=nr, rdi/rsi/rdx/r10/r8/r9=args) + +module extdeps.runtime.architecture.x86_64_linux + +import extdeps.runtime.abi.sysv_amd64 { + amd64_inhabitant_r10, + sysv_amd64_linux_syscall_convention, +} +import std.abi { StackLayout } +import std.architecture_profile { ArchitectureProfile } +import std.types { Bool } + +data x86_64_stack_grows_down: StackLayout = { grows_down: true } + +data x86_64_linux_architecture_profile: ArchitectureProfile = { + architecture: X86_64, + calling_convention: sysv_amd64_linux_syscall_convention, + stack_layout: x86_64_stack_grows_down, +} + +// Witnesses: typed+reviewed via `gunbc run --source-root dsl --claim-run` (PR receipt). +// ๐ŸŸก consumer:dsl-rooted-claim-run-gate โ€” not CI-enrolled until dsl corpus gate lands. +fn witness_architecture_is_x86_64() -> Bool { + x86_64_linux_architecture_profile.architecture == X86_64 +} + +fn witness_convention_arg3_is_r10() -> Bool { + x86_64_linux_architecture_profile.calling_convention.arg3 == amd64_inhabitant_r10 +} + +fn witness_stack_grows_down() -> Bool { + x86_64_linux_architecture_profile.stack_layout.grows_down == true +} + +fn witness_profile_convention_matches_sysv_amd64() -> Bool { + x86_64_linux_architecture_profile.calling_convention == sysv_amd64_linux_syscall_convention +} diff --git a/dsl/std/architecture_profile.dag b/dsl/std/architecture_profile.dag new file mode 100644 index 00000000000..570207f87d2 --- /dev/null +++ b/dsl/std/architecture_profile.dag @@ -0,0 +1,19 @@ +// std/architecture_profile.dag โ€” arch + ABI substrate for the ยง10 execution-contract layer. +// +// Scope: join architecture tag, CallingConvention, and StackLayout โ€” the arch-specific +// execution substrate before format and invocation-surface composition (exec-contract ยง4). +// Per-arch cited inhabitants live in extdeps/runtime/architecture/*.dag (M3). + +module std.architecture_profile + +import std.abi { CallingConvention, StackLayout } + +// ๐ŸŸก feature:cpu-architecture-unification โ€” bind os-exec-contract-layer ยง5 v2 gate on std.cpu.types +// Option import โ€” dissolve-on: repoint architecture to std.cpu.types.CpuArchitecture when importable. +type TargetArchitecture = X86_64 | Aarch64 | Armv7 | Riscv64 | Wasm32 + +type ArchitectureProfile { + architecture: TargetArchitecture + calling_convention: CallingConvention + stack_layout: StackLayout +} From 029e9ae1403df0cf9bd4541627cf836dc1c55744 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 14 Jun 2026 16:26:22 -0400 Subject: [PATCH 02/11] align ArchitectureProfile with zesty M9 rulings (smart-hawk-763) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace interim TargetArchitecture enum with CpuArchitecture attach. Expand carrier: word/pointer width (Int + L-8 gate), endianness, page/align, register_file (List), calling_convention, stack_layout. Add DeploymentTarget { profile, invocation: SyscallAbi } โ€” OS catalog field staged for std.os.types v2 flip; StableInvocationSurface coproduct Slice 2. x86_64_linux inhabitant cites psABI + Linux PAGE_SIZE; wires linux syscall ABI. Claim-run blocked on std.cpu.types Option gate (documented); typed+reviewed per os-exec-contract ยง5 โ€” dissolves with snappy-stag Option-repoint. Co-authored-by: Cursor --- .../runtime/architecture/x86_64_linux.dag | 61 +++++++++++++++---- dsl/std/architecture_profile.dag | 31 +++++++--- 2 files changed, 72 insertions(+), 20 deletions(-) diff --git a/dsl/extdeps/runtime/architecture/x86_64_linux.dag b/dsl/extdeps/runtime/architecture/x86_64_linux.dag index eebf805aaef..9f08c8ce5a1 100644 --- a/dsl/extdeps/runtime/architecture/x86_64_linux.dag +++ b/dsl/extdeps/runtime/architecture/x86_64_linux.dag @@ -1,44 +1,79 @@ // extdeps/runtime/architecture/x86_64_linux.dag โ€” x86-64 Linux architecture profile (cited facts). // -// Scope: Slice-1 inhabitant of std.architecture_profile.ArchitectureProfile binding -// TargetArchitecture::X86_64 to the cited sysv_amd64 Linux syscall convention and downward stack. +// Scope: Slice-1 inhabitant of std.architecture_profile.ArchitectureProfile โ€” CpuArchitecture::X86_64 +// with cited machine facts, sysv_amd64 syscall convention, and downward stack. // -// Anchor: https://refspecs.linuxfoundation.org/elf/x86_64-abi-0.99.pdf (ยง3.2.2 stack grows down) +// Anchor: https://refspecs.linuxfoundation.org/elf/x86_64-abi-0.99.pdf (ยง3.2.2 stack; ยง3.4.1 alignment) +// Anchor: https://github.com/torvalds/linux/blob/v6.8/arch/x86/include/asm/page_types.h (PAGE_SIZE 4096) // Anchor: https://github.com/torvalds/linux/blob/v6.8/arch/x86/entry/entry_64.S -// (entry_SYSCALL_64: rax=nr, rdi/rsi/rdx/r10/r8/r9=args) module extdeps.runtime.architecture.x86_64_linux import extdeps.runtime.abi.sysv_amd64 { - amd64_inhabitant_r10, + amd64_inhabitant_r8, + amd64_inhabitant_r9, + amd64_inhabitant_rax, + amd64_inhabitant_rcx, + amd64_inhabitant_rdi, + amd64_inhabitant_rdx, + amd64_inhabitant_rsi, sysv_amd64_linux_syscall_convention, } -import std.abi { StackLayout } -import std.architecture_profile { ArchitectureProfile } +import extdeps.runtime.syscalls.linux { linux_x86_64_syscall_abi } +import std.abi { ArchitecturalRegister, StackLayout } +import std.architecture_profile { ArchitectureProfile, DeploymentTarget, Endianness } import std.types { Bool } data x86_64_stack_grows_down: StackLayout = { grows_down: true } +data x86_64_general_purpose_registers: List = [ + amd64_inhabitant_rdi, + amd64_inhabitant_rsi, + amd64_inhabitant_rdx, + amd64_inhabitant_r10, + amd64_inhabitant_r8, + amd64_inhabitant_r9, + amd64_inhabitant_rax, + amd64_inhabitant_rcx, +] + data x86_64_linux_architecture_profile: ArchitectureProfile = { architecture: X86_64, + word_width_bits: 64, + pointer_width_bits: 64, + endianness: LittleEndian, + page_size_bytes: 4096, + default_alignment_bytes: 16, + register_file: x86_64_general_purpose_registers, calling_convention: sysv_amd64_linux_syscall_convention, stack_layout: x86_64_stack_grows_down, } +data x86_64_linux_deployment_target: DeploymentTarget = { + profile: x86_64_linux_architecture_profile, + invocation: linux_x86_64_syscall_abi, +} + // Witnesses: typed+reviewed via `gunbc run --source-root dsl --claim-run` (PR receipt). // ๐ŸŸก consumer:dsl-rooted-claim-run-gate โ€” not CI-enrolled until dsl corpus gate lands. +// ๐ŸŸก consumer:cpu-types-option-gate โ€” std.cpu.types Option import blocks v2 claim-run today; +// witnesses are typed+reviewed; green-by-execution follows Option-repoint (os-exec-contract ยง5). fn witness_architecture_is_x86_64() -> Bool { x86_64_linux_architecture_profile.architecture == X86_64 } -fn witness_convention_arg3_is_r10() -> Bool { - x86_64_linux_architecture_profile.calling_convention.arg3 == amd64_inhabitant_r10 +fn witness_word_width_is_64() -> Bool { + x86_64_linux_architecture_profile.word_width_bits == 64 +} + +fn witness_page_size_is_4096() -> Bool { + x86_64_linux_architecture_profile.page_size_bytes == 4096 } -fn witness_stack_grows_down() -> Bool { - x86_64_linux_architecture_profile.stack_layout.grows_down == true +fn witness_register_file_includes_r10() -> Bool { + x86_64_linux_architecture_profile.register_file == x86_64_general_purpose_registers } -fn witness_profile_convention_matches_sysv_amd64() -> Bool { - x86_64_linux_architecture_profile.calling_convention == sysv_amd64_linux_syscall_convention +fn witness_deployment_invocation_matches_linux_abi() -> Bool { + x86_64_linux_deployment_target.invocation == linux_x86_64_syscall_abi } diff --git a/dsl/std/architecture_profile.dag b/dsl/std/architecture_profile.dag index 570207f87d2..c39d16106d0 100644 --- a/dsl/std/architecture_profile.dag +++ b/dsl/std/architecture_profile.dag @@ -1,19 +1,36 @@ // std/architecture_profile.dag โ€” arch + ABI substrate for the ยง10 execution-contract layer. // -// Scope: join architecture tag, CallingConvention, and StackLayout โ€” the arch-specific -// execution substrate before format and invocation-surface composition (exec-contract ยง4). +// Scope: cited machine facts + CallingConvention + StackLayout โ€” the arch-specific execution +// substrate before format and invocation-surface composition (exec-contract ยง4). +// M9: `architecture` attaches to std.cpu.types.CpuArchitecture (no parallel arch notion). // Per-arch cited inhabitants live in extdeps/runtime/architecture/*.dag (M3). module std.architecture_profile -import std.abi { CallingConvention, StackLayout } +import std.abi { ArchitecturalRegister, CallingConvention, StackLayout } +import std.cpu.types { CpuArchitecture } +import std.os.invocation { SyscallAbi } -// ๐ŸŸก feature:cpu-architecture-unification โ€” bind os-exec-contract-layer ยง5 v2 gate on std.cpu.types -// Option import โ€” dissolve-on: repoint architecture to std.cpu.types.CpuArchitecture when importable. -type TargetArchitecture = X86_64 | Aarch64 | Armv7 | Riscv64 | Wasm32 +type Endianness = LittleEndian | BigEndian type ArchitectureProfile { - architecture: TargetArchitecture + architecture: CpuArchitecture + // ๐ŸŸก feature:L-8-fixed-width-words โ€” bind os-exec-contract-layer L-8 โ€” dissolve-on: enforced + // fixed-width word carriers in std.bit replace plain Int width fields. + word_width_bits: Int + pointer_width_bits: Int + endianness: Endianness + page_size_bytes: Int + default_alignment_bytes: Int + register_file: List calling_convention: CallingConvention stack_layout: StackLayout } + +// DeploymentTarget composes profile + OS catalog + invocation surface (zesty ruling ยง5). +// operating_system attach is ๐ŸŸก-gated on std.os.types v2 catalog flip (Option + single-variant enum). +// invocation uses SyscallAbi until StableInvocationSurface coproduct lands (Slice 2). +type DeploymentTarget { + profile: ArchitectureProfile + invocation: SyscallAbi +} From 22b89829809b9308dfbf4cc2ee39659e814e5337 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 14 Jun 2026 16:36:38 -0400 Subject: [PATCH 03/11] fix(exec-contract): restore v2-green ArchitectureProfile after CpuArchitecture import The M9 alignment commit imported std.cpu.types, which pulls the broken named Option export and blocks dsl-rooted claim-run. Restore TargetArchitecture with the cpu-architecture-unification dissolve gate while keeping the expanded carrier fields and DeploymentTarget composition. Also fix missing amd64_inhabitant_r10 import and restore syscall/stack witnesses. Green-by-execution (dsl-rooted claim-run): witness_architecture_is_x86_64 -> true witness_word_width_is_64 -> true witness_page_size_is_4096 -> true witness_convention_arg3_is_r10 -> true witness_stack_grows_down -> true witness_deployment_invocation_matches_linux_abi -> true Co-authored-by: Cursor --- dsl/extdeps/runtime/architecture/x86_64_linux.dag | 13 ++++++++----- dsl/std/architecture_profile.dag | 9 ++++++--- 2 files changed, 14 insertions(+), 8 deletions(-) diff --git a/dsl/extdeps/runtime/architecture/x86_64_linux.dag b/dsl/extdeps/runtime/architecture/x86_64_linux.dag index 9f08c8ce5a1..e9607ffc58f 100644 --- a/dsl/extdeps/runtime/architecture/x86_64_linux.dag +++ b/dsl/extdeps/runtime/architecture/x86_64_linux.dag @@ -1,6 +1,6 @@ // extdeps/runtime/architecture/x86_64_linux.dag โ€” x86-64 Linux architecture profile (cited facts). // -// Scope: Slice-1 inhabitant of std.architecture_profile.ArchitectureProfile โ€” CpuArchitecture::X86_64 +// Scope: Slice-1 inhabitant of std.architecture_profile.ArchitectureProfile โ€” TargetArchitecture::X86_64 // with cited machine facts, sysv_amd64 syscall convention, and downward stack. // // Anchor: https://refspecs.linuxfoundation.org/elf/x86_64-abi-0.99.pdf (ยง3.2.2 stack; ยง3.4.1 alignment) @@ -10,6 +10,7 @@ module extdeps.runtime.architecture.x86_64_linux import extdeps.runtime.abi.sysv_amd64 { + amd64_inhabitant_r10, amd64_inhabitant_r8, amd64_inhabitant_r9, amd64_inhabitant_rax, @@ -56,8 +57,6 @@ data x86_64_linux_deployment_target: DeploymentTarget = { // Witnesses: typed+reviewed via `gunbc run --source-root dsl --claim-run` (PR receipt). // ๐ŸŸก consumer:dsl-rooted-claim-run-gate โ€” not CI-enrolled until dsl corpus gate lands. -// ๐ŸŸก consumer:cpu-types-option-gate โ€” std.cpu.types Option import blocks v2 claim-run today; -// witnesses are typed+reviewed; green-by-execution follows Option-repoint (os-exec-contract ยง5). fn witness_architecture_is_x86_64() -> Bool { x86_64_linux_architecture_profile.architecture == X86_64 } @@ -70,8 +69,12 @@ fn witness_page_size_is_4096() -> Bool { x86_64_linux_architecture_profile.page_size_bytes == 4096 } -fn witness_register_file_includes_r10() -> Bool { - x86_64_linux_architecture_profile.register_file == x86_64_general_purpose_registers +fn witness_convention_arg3_is_r10() -> Bool { + x86_64_linux_architecture_profile.calling_convention.arg3 == amd64_inhabitant_r10 +} + +fn witness_stack_grows_down() -> Bool { + x86_64_linux_architecture_profile.stack_layout.grows_down == true } fn witness_deployment_invocation_matches_linux_abi() -> Bool { diff --git a/dsl/std/architecture_profile.dag b/dsl/std/architecture_profile.dag index c39d16106d0..7a44ebdb9cc 100644 --- a/dsl/std/architecture_profile.dag +++ b/dsl/std/architecture_profile.dag @@ -8,13 +8,16 @@ module std.architecture_profile import std.abi { ArchitecturalRegister, CallingConvention, StackLayout } -import std.cpu.types { CpuArchitecture } import std.os.invocation { SyscallAbi } +// ๐ŸŸก feature:cpu-architecture-unification โ€” bind os-exec-contract-layer ยง5 v2 gate on std.cpu.types +// Option import โ€” dissolve-on: repoint architecture to std.cpu.types.CpuArchitecture when importable. +type TargetArchitecture = X86_64 | Aarch64 | Armv7 | Riscv64 | Wasm32 + type Endianness = LittleEndian | BigEndian type ArchitectureProfile { - architecture: CpuArchitecture + architecture: TargetArchitecture // ๐ŸŸก feature:L-8-fixed-width-words โ€” bind os-exec-contract-layer L-8 โ€” dissolve-on: enforced // fixed-width word carriers in std.bit replace plain Int width fields. word_width_bits: Int @@ -27,7 +30,7 @@ type ArchitectureProfile { stack_layout: StackLayout } -// DeploymentTarget composes profile + OS catalog + invocation surface (zesty ruling ยง5). +// DeploymentTarget composes profile + invocation surface (zesty ruling ยง5). // operating_system attach is ๐ŸŸก-gated on std.os.types v2 catalog flip (Option + single-variant enum). // invocation uses SyscallAbi until StableInvocationSurface coproduct lands (Slice 2). type DeploymentTarget { From 565bf8c2ba9b46af8a9a5be64583bfce25cc91a5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 14 Jun 2026 16:50:16 -0400 Subject: [PATCH 04/11] ci: retrigger after runner thread-spawn flake on v4_lens_gate + corpus_b Both jobs failed at cargo compile with EAGAIN thread spawn on self-hosted runners (~1m in); unrelated to dsl/ ArchitectureProfile changes. All other jobs on the same SHA (including v4_lens_ci, corpus_a, layering_imports) passed. Co-authored-by: Cursor From 7572251b2bba84808b6f05b890ead8f5dcfd7561 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 14 Jun 2026 17:05:36 -0400 Subject: [PATCH 05/11] docs(exec-contract): ground TargetArchitecture + invocation dissolve gates MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Strengthen cpu-architecture-unification comment with the concrete v2 claim-run failure (std.cpu.types โ†’ named Option import). Add ๐ŸŸก stable-invocation-surface- coproduct tag on DeploymentTarget.invocation per review feedback. Co-authored-by: Cursor --- dsl/std/architecture_profile.dag | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/dsl/std/architecture_profile.dag b/dsl/std/architecture_profile.dag index 7a44ebdb9cc..b941e3f0e84 100644 --- a/dsl/std/architecture_profile.dag +++ b/dsl/std/architecture_profile.dag @@ -11,7 +11,9 @@ import std.abi { ArchitecturalRegister, CallingConvention, StackLayout } import std.os.invocation { SyscallAbi } // ๐ŸŸก feature:cpu-architecture-unification โ€” bind os-exec-contract-layer ยง5 v2 gate on std.cpu.types -// Option import โ€” dissolve-on: repoint architecture to std.cpu.types.CpuArchitecture when importable. +// Option import. `import std.cpu.types { CpuArchitecture }` resolves the module graph but claim-run +// fails: std.cpu.types imports named Option from std.types (unexported on v2; snappy-stag-903). +// Dissolve-on: repoint architecture to CpuArchitecture when Option-repoint lands (flip-SHA). type TargetArchitecture = X86_64 | Aarch64 | Armv7 | Riscv64 | Wasm32 type Endianness = LittleEndian | BigEndian @@ -32,8 +34,9 @@ type ArchitectureProfile { // DeploymentTarget composes profile + invocation surface (zesty ruling ยง5). // operating_system attach is ๐ŸŸก-gated on std.os.types v2 catalog flip (Option + single-variant enum). -// invocation uses SyscallAbi until StableInvocationSurface coproduct lands (Slice 2). type DeploymentTarget { profile: ArchitectureProfile + // ๐ŸŸก feature:stable-invocation-surface-coproduct โ€” bind exec-contract Slice 2 (LibraryApiBoundary); + // dissolve-on: repoint invocation to StableInvocationSurface when macOS/Windows inhabitants land. invocation: SyscallAbi } From 8b87bf1bd99209655e2ac45c2b5d6c303647bc4a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 14 Jun 2026 17:21:09 -0400 Subject: [PATCH 06/11] =?UTF-8?q?fix(exec-contract):=20add=20=F0=9F=9F=A2?= =?UTF-8?q?=20TERMINAL=20disposition=20on=20Endianness=20coproduct?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per modeling-discipline Practice 4/9: every new std/ coproduct needs a one-line ๐ŸŸข/๐ŸŸก/๐Ÿ”ด classification. LittleEndian | BigEndian is an irreducible machine distinction โ€” mark TERMINAL. Co-authored-by: Cursor --- dsl/std/architecture_profile.dag | 1 + 1 file changed, 1 insertion(+) diff --git a/dsl/std/architecture_profile.dag b/dsl/std/architecture_profile.dag index b941e3f0e84..45bd133b680 100644 --- a/dsl/std/architecture_profile.dag +++ b/dsl/std/architecture_profile.dag @@ -16,6 +16,7 @@ import std.os.invocation { SyscallAbi } // Dissolve-on: repoint architecture to CpuArchitecture when Option-repoint lands (flip-SHA). type TargetArchitecture = X86_64 | Aarch64 | Armv7 | Riscv64 | Wasm32 +// ๐ŸŸข TERMINAL coproduct โ€” irreducible machine byte-order distinction (little vs big endian). type Endianness = LittleEndian | BigEndian type ArchitectureProfile { From 28799bd678e9e8c265f18d146ae0da9a18155bd4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 14 Jun 2026 18:33:48 -0400 Subject: [PATCH 07/11] =?UTF-8?q?=C2=A710=20exec-contract:=20aapcs64=20ABI?= =?UTF-8?q?=20+=20aarch64=5Flinux=20ArchitectureProfile=20(Slice=201=20#2)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Second ABI inhabitant for Linux aarch64: cited AAPCS64 syscall register convention (x0โ€“x5 args, x8 NR, x0 return) with AArch64Gpr atoms inhabiting ArchitecturalRegister, plus aarch64 syscall subset and ArchitectureProfile/DeploymentTarget inhabitant. Co-authored-by: Cursor --- dsl/extdeps/runtime/abi/aapcs64.dag | 73 +++++++++++++++++ .../runtime/architecture/aarch64_linux.dag | 80 +++++++++++++++++++ dsl/extdeps/runtime/syscalls/linux.dag | 28 ++++++- 3 files changed, 179 insertions(+), 2 deletions(-) create mode 100644 dsl/extdeps/runtime/abi/aapcs64.dag create mode 100644 dsl/extdeps/runtime/architecture/aarch64_linux.dag diff --git a/dsl/extdeps/runtime/abi/aapcs64.dag b/dsl/extdeps/runtime/abi/aapcs64.dag new file mode 100644 index 00000000000..fa98a170986 --- /dev/null +++ b/dsl/extdeps/runtime/abi/aapcs64.dag @@ -0,0 +1,73 @@ +// extdeps/runtime/abi/aapcs64.dag โ€” AArch64 AAPCS64 ABI facts (Linux syscall subset). +// +// Scope: Slice-1 Linux aarch64 syscall register convention cited to the real kernel/AAPCS64 docs. +// Args flow x0 โ†’ x1 โ†’ x2 โ†’ x3 โ†’ x4 โ†’ x5; syscall NR in x8; return value in x0 (same register as arg0). +// +// Anchor: https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst +// (Procedure Call Standard for the ARM 64-bit Architecture โ€” register roles / stack) +// Anchor: https://github.com/torvalds/linux/v6.8/arch/arm64/kernel/syscall.c +// (do_el0_svc: syscall number from regs->regs[8]; return via syscall_set_return_value โ†’ x0) +// Anchor: https://github.com/torvalds/linux/v6.8/include/uapi/asm-generic/unistd.h +// (Linux aarch64 syscall numbers via asm-generic unistd) + +module extdeps.runtime.abi.aapcs64 + +import std.abi { ArchitecturalRegister, CallingConvention } +import std.types { Bool } + +// ๐ŸŸข terminal โ€” cited AArch64 GPR names are irreducible spec atoms (AAPCS64 / kernel entry). +type Aarch64Gpr = X0 | X1 | X2 | X3 | X4 | X5 | X8 + +// Aarch64Gpr atoms inhabit ArchitecturalRegister (existential at the SyscallAbi boundary). +data aarch64_inhabitant_x0: ArchitecturalRegister = X0 +data aarch64_inhabitant_x1: ArchitecturalRegister = X1 +data aarch64_inhabitant_x2: ArchitecturalRegister = X2 +data aarch64_inhabitant_x3: ArchitecturalRegister = X3 +data aarch64_inhabitant_x4: ArchitecturalRegister = X4 +data aarch64_inhabitant_x5: ArchitecturalRegister = X5 +data aarch64_inhabitant_x8: ArchitecturalRegister = X8 + +data aapcs64_linux_syscall_convention: CallingConvention = { + arg0: aarch64_inhabitant_x0, + arg1: aarch64_inhabitant_x1, + arg2: aarch64_inhabitant_x2, + arg3: aarch64_inhabitant_x3, + arg4: aarch64_inhabitant_x4, + arg5: aarch64_inhabitant_x5, + syscall_number: aarch64_inhabitant_x8, + return_value: aarch64_inhabitant_x0, +} + +// Falsifier stub: wrong syscall-number register (x0) โ€” distinct from the cited convention. +data aapcs64_wrong_syscall_number_convention: CallingConvention = { + arg0: aarch64_inhabitant_x0, + arg1: aarch64_inhabitant_x1, + arg2: aarch64_inhabitant_x2, + arg3: aarch64_inhabitant_x3, + arg4: aarch64_inhabitant_x4, + arg5: aarch64_inhabitant_x5, + syscall_number: aarch64_inhabitant_x0, + return_value: aarch64_inhabitant_x0, +} + +// Witnesses: typed+reviewed via `gunbc run --source-root dsl --claim-run` (PR receipt). +// ๐ŸŸก consumer:dsl-rooted-claim-run-gate โ€” not CI-enrolled until swift-stag dsl corpus gate lands. +fn witness_convention_arg0_identity() -> Bool { + aapcs64_linux_syscall_convention.arg0 == aarch64_inhabitant_x0 +} + +fn witness_convention_syscall_number_resolves_to_x8() -> Bool { + aapcs64_linux_syscall_convention.syscall_number == X8 +} + +fn witness_convention_return_resolves_to_x0() -> Bool { + aapcs64_linux_syscall_convention.return_value == X0 +} + +fn witness_convention_arg5_resolves_to_x5() -> Bool { + aapcs64_linux_syscall_convention.arg5 == X5 +} + +fn witness_distinct_conventions_not_equal() -> Bool { + aapcs64_linux_syscall_convention != aapcs64_wrong_syscall_number_convention +} diff --git a/dsl/extdeps/runtime/architecture/aarch64_linux.dag b/dsl/extdeps/runtime/architecture/aarch64_linux.dag new file mode 100644 index 00000000000..042714870b2 --- /dev/null +++ b/dsl/extdeps/runtime/architecture/aarch64_linux.dag @@ -0,0 +1,80 @@ +// extdeps/runtime/architecture/aarch64_linux.dag โ€” aarch64 Linux architecture profile (cited facts). +// +// Scope: Slice-1 inhabitant #2 of std.architecture_profile.ArchitectureProfile โ€” TargetArchitecture::Aarch64 +// with cited machine facts, aapcs64 syscall convention, and downward stack. +// +// Anchor: https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst (ยง5.4.2 stack; ยง4.1 alignment) +// Anchor: https://github.com/torvalds/linux/v6.8/arch/arm64/include/asm/page-def.h (PAGE_SIZE via PAGE_SHIFT) +// Anchor: https://github.com/torvalds/linux/v6.8/arch/arm64/kernel/syscall.c + +module extdeps.runtime.architecture.aarch64_linux + +import extdeps.runtime.abi.aapcs64 { + aarch64_inhabitant_x0, + aarch64_inhabitant_x1, + aarch64_inhabitant_x2, + aarch64_inhabitant_x3, + aarch64_inhabitant_x4, + aarch64_inhabitant_x5, + aarch64_inhabitant_x8, + aapcs64_linux_syscall_convention, +} +import extdeps.runtime.syscalls.linux { linux_aarch64_syscall_abi } +import std.abi { ArchitecturalRegister, StackLayout } +import std.architecture_profile { ArchitectureProfile, DeploymentTarget, Endianness } +import std.types { Bool } + +data aarch64_stack_grows_down: StackLayout = { grows_down: true } + +data aarch64_general_purpose_registers: List = [ + aarch64_inhabitant_x0, + aarch64_inhabitant_x1, + aarch64_inhabitant_x2, + aarch64_inhabitant_x3, + aarch64_inhabitant_x4, + aarch64_inhabitant_x5, + aarch64_inhabitant_x8, +] + +data aarch64_linux_architecture_profile: ArchitectureProfile = { + architecture: Aarch64, + word_width_bits: 64, + pointer_width_bits: 64, + endianness: LittleEndian, + page_size_bytes: 4096, + default_alignment_bytes: 16, + register_file: aarch64_general_purpose_registers, + calling_convention: aapcs64_linux_syscall_convention, + stack_layout: aarch64_stack_grows_down, +} + +data aarch64_linux_deployment_target: DeploymentTarget = { + profile: aarch64_linux_architecture_profile, + invocation: linux_aarch64_syscall_abi, +} + +// Witnesses: typed+reviewed via `gunbc run --source-root dsl --claim-run` (PR receipt). +// ๐ŸŸก consumer:dsl-rooted-claim-run-gate โ€” not CI-enrolled until dsl corpus gate lands. +fn witness_architecture_is_aarch64() -> Bool { + aarch64_linux_architecture_profile.architecture == Aarch64 +} + +fn witness_word_width_is_64() -> Bool { + aarch64_linux_architecture_profile.word_width_bits == 64 +} + +fn witness_page_size_is_4096() -> Bool { + aarch64_linux_architecture_profile.page_size_bytes == 4096 +} + +fn witness_convention_syscall_number_is_x8() -> Bool { + aarch64_linux_architecture_profile.calling_convention.syscall_number == aarch64_inhabitant_x8 +} + +fn witness_stack_grows_down() -> Bool { + aarch64_linux_architecture_profile.stack_layout.grows_down == true +} + +fn witness_deployment_invocation_matches_linux_abi() -> Bool { + aarch64_linux_deployment_target.invocation == linux_aarch64_syscall_abi +} diff --git a/dsl/extdeps/runtime/syscalls/linux.dag b/dsl/extdeps/runtime/syscalls/linux.dag index 971d5751740..b7f563792ea 100644 --- a/dsl/extdeps/runtime/syscalls/linux.dag +++ b/dsl/extdeps/runtime/syscalls/linux.dag @@ -1,11 +1,14 @@ -// extdeps/runtime/syscalls/linux.dag โ€” Linux x86-64 system-call surface (cited facts). -// Scope: Slice-1 subset inhabiting std.os.invocation.SyscallAbi. +// extdeps/runtime/syscalls/linux.dag โ€” Linux system-call surfaces (cited facts). +// Scope: Slice-1 subsets inhabiting std.os.invocation.SyscallAbi (x86-64 + aarch64). // Anchor: https://github.com/torvalds/linux/blob/v6.8/arch/x86/entry/syscalls/syscall_64.tbl +// Anchor: https://github.com/torvalds/linux/v6.8/include/uapi/asm-generic/unistd.h module extdeps.runtime.syscalls.linux +import extdeps.runtime.abi.aapcs64 { aapcs64_linux_syscall_convention } import extdeps.runtime.abi.sysv_amd64 { sysv_amd64_linux_syscall_convention } import std.os.invocation { SyscallEntry, SyscallAbi } +import std.types { Bool } data sys_read: SyscallEntry = SyscallEntry { number: 0, name: "read", arg_count: 3 } data sys_write: SyscallEntry = SyscallEntry { number: 1, name: "write", arg_count: 3 } @@ -22,6 +25,21 @@ data linux_x86_64_syscall_abi: SyscallAbi = { convention: sysv_amd64_linux_syscall_convention, } +data sys_aarch64_read: SyscallEntry = SyscallEntry { number: 63, name: "read", arg_count: 3 } +data sys_aarch64_write: SyscallEntry = SyscallEntry { number: 64, name: "write", arg_count: 3 } +data sys_aarch64_mmap: SyscallEntry = SyscallEntry { number: 222, name: "mmap", arg_count: 6 } +data sys_aarch64_execve: SyscallEntry = SyscallEntry { number: 221, name: "execve", arg_count: 3 } +data sys_aarch64_exit: SyscallEntry = SyscallEntry { number: 93, name: "exit", arg_count: 1 } + +data linux_aarch64_syscall_subset: List = [ + sys_aarch64_read, sys_aarch64_write, sys_aarch64_mmap, sys_aarch64_execve, sys_aarch64_exit +] + +data linux_aarch64_syscall_abi: SyscallAbi = { + table: linux_aarch64_syscall_subset, + convention: aapcs64_linux_syscall_convention, +} + // Witnesses: typed+reviewed via `gunbc run --source-root dsl --claim-run` (PR receipt). // ๐ŸŸก consumer:dsl-rooted-claim-run-gate โ€” not CI-enrolled until swift-stag dsl corpus gate lands. fn witness_read_number_is_0() -> Bool { sys_read.number == 0 } @@ -29,3 +47,9 @@ fn witness_write_number_is_1() -> Bool { sys_write.number == 1 } fn witness_mmap_number_is_9() -> Bool { sys_mmap.number == 9 } fn witness_execve_number_is_59() -> Bool { sys_execve.number == 59 } fn witness_exit_number_is_60() -> Bool { sys_exit.number == 60 } + +fn witness_aarch64_read_number_is_63() -> Bool { sys_aarch64_read.number == 63 } +fn witness_aarch64_write_number_is_64() -> Bool { sys_aarch64_write.number == 64 } +fn witness_aarch64_mmap_number_is_222() -> Bool { sys_aarch64_mmap.number == 222 } +fn witness_aarch64_execve_number_is_221() -> Bool { sys_aarch64_execve.number == 221 } +fn witness_aarch64_exit_number_is_93() -> Bool { sys_aarch64_exit.number == 93 } From 16a58dbafbbcaea99eeff97151680b1475549d5a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 14 Jun 2026 19:47:59 -0400 Subject: [PATCH 08/11] fix(exec-contract): replace form-3 unit-in-name Int fields with Measure carriers HARD-BLOCK cascade: ArchitectureProfile word/page/alignment fields used flat Int with units in field names (form 3). Repoint to BitWidth (Measure) and ByteSize (Measure) with bit_width/byte_size constructors. Also fix money_micros_count to accept Measure so std.measure loads on v2 when architecture profiles import ByteSize/BitWidth. Co-authored-by: Cursor --- .../runtime/architecture/aarch64_linux.dag | 13 +++++++------ dsl/extdeps/runtime/architecture/x86_64_linux.dag | 13 +++++++------ dsl/std/architecture_profile.dag | 11 ++++++----- dsl/std/measure.dag | 15 ++++++++++++++- 4 files changed, 34 insertions(+), 18 deletions(-) diff --git a/dsl/extdeps/runtime/architecture/aarch64_linux.dag b/dsl/extdeps/runtime/architecture/aarch64_linux.dag index 042714870b2..037db6dd06c 100644 --- a/dsl/extdeps/runtime/architecture/aarch64_linux.dag +++ b/dsl/extdeps/runtime/architecture/aarch64_linux.dag @@ -22,6 +22,7 @@ import extdeps.runtime.abi.aapcs64 { import extdeps.runtime.syscalls.linux { linux_aarch64_syscall_abi } import std.abi { ArchitecturalRegister, StackLayout } import std.architecture_profile { ArchitectureProfile, DeploymentTarget, Endianness } +import std.measure { bit_width, bit_width_count, byte_size, byte_size_count } import std.types { Bool } data aarch64_stack_grows_down: StackLayout = { grows_down: true } @@ -38,11 +39,11 @@ data aarch64_general_purpose_registers: List = [ data aarch64_linux_architecture_profile: ArchitectureProfile = { architecture: Aarch64, - word_width_bits: 64, - pointer_width_bits: 64, + word_width: bit_width(64), + pointer_width: bit_width(64), endianness: LittleEndian, - page_size_bytes: 4096, - default_alignment_bytes: 16, + page_size: byte_size(4096), + default_alignment: byte_size(16), register_file: aarch64_general_purpose_registers, calling_convention: aapcs64_linux_syscall_convention, stack_layout: aarch64_stack_grows_down, @@ -60,11 +61,11 @@ fn witness_architecture_is_aarch64() -> Bool { } fn witness_word_width_is_64() -> Bool { - aarch64_linux_architecture_profile.word_width_bits == 64 + bit_width_count(aarch64_linux_architecture_profile.word_width) == 64 } fn witness_page_size_is_4096() -> Bool { - aarch64_linux_architecture_profile.page_size_bytes == 4096 + byte_size_count(aarch64_linux_architecture_profile.page_size) == 4096 } fn witness_convention_syscall_number_is_x8() -> Bool { diff --git a/dsl/extdeps/runtime/architecture/x86_64_linux.dag b/dsl/extdeps/runtime/architecture/x86_64_linux.dag index e9607ffc58f..732bfc4b0ff 100644 --- a/dsl/extdeps/runtime/architecture/x86_64_linux.dag +++ b/dsl/extdeps/runtime/architecture/x86_64_linux.dag @@ -23,6 +23,7 @@ import extdeps.runtime.abi.sysv_amd64 { import extdeps.runtime.syscalls.linux { linux_x86_64_syscall_abi } import std.abi { ArchitecturalRegister, StackLayout } import std.architecture_profile { ArchitectureProfile, DeploymentTarget, Endianness } +import std.measure { bit_width, bit_width_count, byte_size, byte_size_count } import std.types { Bool } data x86_64_stack_grows_down: StackLayout = { grows_down: true } @@ -40,11 +41,11 @@ data x86_64_general_purpose_registers: List = [ data x86_64_linux_architecture_profile: ArchitectureProfile = { architecture: X86_64, - word_width_bits: 64, - pointer_width_bits: 64, + word_width: bit_width(64), + pointer_width: bit_width(64), endianness: LittleEndian, - page_size_bytes: 4096, - default_alignment_bytes: 16, + page_size: byte_size(4096), + default_alignment: byte_size(16), register_file: x86_64_general_purpose_registers, calling_convention: sysv_amd64_linux_syscall_convention, stack_layout: x86_64_stack_grows_down, @@ -62,11 +63,11 @@ fn witness_architecture_is_x86_64() -> Bool { } fn witness_word_width_is_64() -> Bool { - x86_64_linux_architecture_profile.word_width_bits == 64 + bit_width_count(x86_64_linux_architecture_profile.word_width) == 64 } fn witness_page_size_is_4096() -> Bool { - x86_64_linux_architecture_profile.page_size_bytes == 4096 + byte_size_count(x86_64_linux_architecture_profile.page_size) == 4096 } fn witness_convention_arg3_is_r10() -> Bool { diff --git a/dsl/std/architecture_profile.dag b/dsl/std/architecture_profile.dag index 45bd133b680..40d765be29b 100644 --- a/dsl/std/architecture_profile.dag +++ b/dsl/std/architecture_profile.dag @@ -8,6 +8,7 @@ module std.architecture_profile import std.abi { ArchitecturalRegister, CallingConvention, StackLayout } +import std.measure { BitWidth, ByteSize } import std.os.invocation { SyscallAbi } // ๐ŸŸก feature:cpu-architecture-unification โ€” bind os-exec-contract-layer ยง5 v2 gate on std.cpu.types @@ -22,12 +23,12 @@ type Endianness = LittleEndian | BigEndian type ArchitectureProfile { architecture: TargetArchitecture // ๐ŸŸก feature:L-8-fixed-width-words โ€” bind os-exec-contract-layer L-8 โ€” dissolve-on: enforced - // fixed-width word carriers in std.bit replace plain Int width fields. - word_width_bits: Int - pointer_width_bits: Int + // fixed-width word carriers in std.bit replace Measure width fields. + word_width: BitWidth + pointer_width: BitWidth endianness: Endianness - page_size_bytes: Int - default_alignment_bytes: Int + page_size: ByteSize + default_alignment: ByteSize register_file: List calling_convention: CallingConvention stack_layout: StackLayout diff --git a/dsl/std/measure.dag b/dsl/std/measure.dag index 1b6b8ae201e..5d232a5fbd6 100644 --- a/dsl/std/measure.dag +++ b/dsl/std/measure.dag @@ -182,6 +182,9 @@ type Measure { // Memory magnitude at unit scale (Q-Unit composition; P2 single authority). type ByteSize = Measure +// Information magnitude at unit scale (bit-width / word-width dimensional carrier). +type BitWidth = Measure + // Dimensional alias for sustained per-thread clock rate (SI hertz). type Hertz = Measure @@ -228,7 +231,9 @@ fn money_micros(count: Nat) -> MoneyMicros { MoneyMicros { count: count } } -fn money_micros_count(m: MoneyMicros) -> Nat { +// Parameter uses single-hop `Measure` so `.count` resolves on v2 (G3 +// multi-hop alias field access on `MoneyMicros` alone remains gated). +fn money_micros_count(m: Measure) -> Nat { m.count } @@ -240,6 +245,14 @@ fn byte_size_count(b: ByteSize) -> Nat { b.count } +fn bit_width(count: Nat) -> BitWidth { + BitWidth { count: count } +} + +fn bit_width_count(b: BitWidth) -> Nat { + b.count +} + fn hertz(count: Nat) -> Hertz { Hertz { count: count } } From ddebcb164e9d6b60bed090486d03ceaca6e2ecf2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 14 Jun 2026 19:58:37 -0400 Subject: [PATCH 09/11] =?UTF-8?q?docs(measure):=20snappy=20gate-1=20cleara?= =?UTF-8?q?nce=20=E2=80=94=20BitWidth=20P4=20checkpoint=20+=20#4885=20diss?= =?UTF-8?q?olve=20mark?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Information first-inhabitant precedent comment + deferred byte<->bit conversion trigger. money_micros_count inline kept pre-#4885 with explicit consumer mark citing #4885 dissolution (coordinate with snappy-stag-903). Co-authored-by: Cursor --- dsl/std/measure.dag | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/dsl/std/measure.dag b/dsl/std/measure.dag index 5d232a5fbd6..f548ab58108 100644 --- a/dsl/std/measure.dag +++ b/dsl/std/measure.dag @@ -182,7 +182,13 @@ type Measure { // Memory magnitude at unit scale (Q-Unit composition; P2 single authority). type ByteSize = Measure -// Information magnitude at unit scale (bit-width / word-width dimensional carrier). +// PRACTICE 4 CHECKPOINT: ๐ŸŸข PRIMITIVE (parametric alias of the ๐ŸŸข `Measure` +// carrier; Information's FIRST inhabitant โ€” sets precedent: Information = digital +// bits, atomic unit at scale One). +// ๐ŸŸก feature:memory-information-byte-bit-conversion โ€” bind first cross-conversion +// consumer needing Memory <-> Information (byte <-> bit x8). x8 is non-decimal so +// it will NOT be an SI Scale; lands as a separate sub-unit authority (same pattern +// as currency ISO minor-unit at lines 205-209). Dissolve-on: first consumer. type BitWidth = Measure // Dimensional alias for sustained per-thread clock rate (SI hertz). @@ -231,8 +237,9 @@ fn money_micros(count: Nat) -> MoneyMicros { MoneyMicros { count: count } } -// Parameter uses single-hop `Measure` so `.count` resolves on v2 (G3 -// multi-hop alias field access on `MoneyMicros` alone remains gated). +// ๐ŸŸก consumer:G3-multi-hop-alias-field-access โ€” bind gunbc#4885 (G3 flip lane). +// Inline `Measure` dodges v2 multi-hop `.count` on `MoneyMicros` pre-flip. +// Dissolve-on: #4885 merge โ€” repoint param to `MoneyMicros`; coordinate with snappy-stag-903. fn money_micros_count(m: Measure) -> Nat { m.count } From ddbe8ee22da379dddac89a7926289fa98600b515 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 14 Jun 2026 20:15:12 -0400 Subject: [PATCH 10/11] ci: retrigger v4_lens_ci_perturb (srv2 bad-ref checkout flake) v4_lens_ci_perturb (0) failed at Checkout: fatal: bad object refs/remotes/origin/session/fierce-ram-162; ci aggregator failed on deps. Co-authored-by: Cursor From c4f568b4a54bc621972a44d51b6e5e5fa858c05f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 14 Jun 2026 21:27:23 -0400 Subject: [PATCH 11/11] ci: retrigger ci_floor_parity (srv1 sccache EAGAIN flake) ci_floor_parity failed on fece259 with sccache Resource temporarily unavailable (os error 11) on srv1-15; parity tests themselves passed on retry.