§10 exec-contract: aapcs64 ABI + aarch64_linux ArchitectureProfile (Slice 1 #2)

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
+}

dsl/extdeps/runtime/architecture/aarch64_linux.dag

@@ -0,0 +1,81 @@
+// 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.measure { bit_width, bit_width_count, byte_size, byte_size_count }
+import std.types { Bool }
+
+data aarch64_stack_grows_down: StackLayout = { grows_down: true }
+
+data aarch64_general_purpose_registers: List<ArchitecturalRegister> = [
+  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: bit_width(64),
+  pointer_width: bit_width(64),
+  endianness: LittleEndian,
+  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,
+}
+
+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 {
+  bit_width_count(aarch64_linux_architecture_profile.word_width) == 64
+}
+
+fn witness_page_size_is_4096() -> Bool {
+  byte_size_count(aarch64_linux_architecture_profile.page_size) == 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
+}

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<ArchitecturalRegister> = [
 
 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 {

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,10 +25,31 @@ 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<SyscallEntry> = [
+  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 }
 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 }

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<Information, One> 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<ArchitecturalRegister>
   calling_convention: CallingConvention
   stack_layout: StackLayout

dsl/std/measure.dag

@@ -182,6 +182,15 @@ type Measure<Q, S> {
 // Memory magnitude at unit scale (Q-Unit composition; P2 single authority).
 type ByteSize = Measure<Memory, One>
 
+// 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<Information, One>
+
 // Dimensional alias for sustained per-thread clock rate (SI hertz).
 type Hertz = Measure<Frequency, One>
 
@@ -228,7 +237,10 @@ fn money_micros(count: Nat) -> MoneyMicros {
   MoneyMicros { count: count }
 }
 
-fn money_micros_count(m: MoneyMicros) -> Nat {
+// 🟡 consumer:G3-multi-hop-alias-field-access — bind gunbc#4885 (G3 flip lane).
+// Inline `Measure<Currency, Micro>` 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<Currency, Micro>) -> Nat {
   m.count
 }
 
@@ -240,6 +252,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 }
 }