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

[briansrls]

Summary

• Adds dsl/extdeps/runtime/abi/aapcs64.dag — 2nd ABI inhabitant for Linux aarch64: cited syscall register convention (args x0–x5, NR x8, return x0) with Aarch64Gpr atoms inhabiting ArchitecturalRegister.
• Adds dsl/extdeps/runtime/architecture/aarch64_linux.dag — 2nd ArchitectureProfile inhabitant (Aarch64 + aapcs64 convention + downward stack) and matching DeploymentTarget.
• Extends dsl/extdeps/runtime/syscalls/linux.dag with aarch64 syscall subset (read=63, write=64, mmap=222, execve=221, exit=93) wired to aapcs64_linux_syscall_convention.

Stacks on #4882 (ArchitectureProfile + x86_64_linux).

Green-by-execution receipt

Sixteen witnesses via dsl-rooted claim-run (gunbc run --source-root dsl --entry … --function … --claim-run):

aapcs64.dag (5):

witness_convention_arg0_identity -> true
witness_convention_syscall_number_resolves_to_x8 -> true
witness_convention_return_resolves_to_x0 -> true
witness_convention_arg5_resolves_to_x5 -> true
witness_distinct_conventions_not_equal -> true

linux.dag aarch64 (5):

witness_aarch64_read_number_is_63 -> true
witness_aarch64_write_number_is_64 -> true
witness_aarch64_mmap_number_is_222 -> true
witness_aarch64_execve_number_is_221 -> true
witness_aarch64_exit_number_is_93 -> true

aarch64_linux.dag (6):

witness_architecture_is_aarch64 -> true
witness_word_width_is_64 -> true
witness_page_size_is_4096 -> true
witness_convention_syscall_number_is_x8 -> true
witness_stack_grows_down -> true
witness_deployment_invocation_matches_linux_abi -> true

Test plan

• All 16 claim-run witnesses pass locally
• Review stacked on §10 exec-contract: ArchitectureProfile — arch + ABI substrate (Slice 1) #4882 merge order

Made with Cursor

[briansrls]

Independent gate-2 by-execution sign — measure.dag CARRIER portion — PASS (@ ddebcb164e9d6b60bed090486d03ceaca6e2ecf2, session/witty-moth-587)

Independent gate-2 on the dsl/std/measure.dag carrier surface only (not the whole §10 ABI PR), at snappy-stag-903's request — keen-fox's own 27-witness run is a self-run, not independent. Ran fresh from a clean detached checkout pinned to the current head (git rev-parse HEAD = ddebcb164e9d6b60bed090486d03ceaca6e2ecf2, verified — not the superseded 16a58db; clean tree).

Method: since this PR ships no dedicated carrier witness, I loaded the real dsl/std/measure.dag via the source-root import closure (load_sources_for_entry + compile_to_resolved, the std_os_types real-file pattern) in a throwaway test and asserted zero hard diagnostics. Run under RUSTFLAGS="-D warnings" (not plain cargo test).

RUSTC_WRAPPER="" RUSTFLAGS="-D warnings" cargo test -p v2-compiler-tests --lib -- \
  gate2_4889_measure_dag_carrier_loads_clean (+ bytesize / generic single-hop)
  → test result: ok. 3 passed; 0 failed (debug, -D warnings clean)

#	Criterion	Evidence	Result
1	BitWidth = Measure<Information, One> + bit_width / bit_width_count load + typecheck (Information = first inhabitant; Information@quantity:73, One@scale:102 declared)	full-file load resolves & typechecks every fn in measure.dag with zero hard diagnostics	PASS
2	money_micros_count(m: Measure<Currency, Micro>) -> Nat resolves .count on v2 (single-hop inline, 🟡 dissolve-on-#4885)	same clean load; negative control below proves the single-hop inline is what makes it resolve	PASS
3	measure.dag loads clean; -D warnings clean	clean load under RUSTFLAGS=-D warnings	PASS

Discrimination is genuine (negative control, by execution): reverting money_micros_count's param back to the multi-hop MoneyMicros form makes the same load fail with exactly no field 'count' on type 'MoneyMicros' (the pre-flip multi-hop gap that #4885/G3 fixes). With the single-hop Measure<Currency, Micro> inline it loads clean. So the green is real — the carrier genuinely exercises the field-access path, and the inline (marked 🟡 dissolve-on-#4885) is load-bearing exactly as documented.

Clippy — honest note (NOT a carrier finding): cargo clippy -p v2-compiler -p v2-compiler-tests --all-targets -- -D warnings surfaces 3 cloned_ref_to_slice_refs errors in src/v2/tests/src/coproduct_reflection_conformance_test.rs:188,236 — a newer clippy lint (rust 1.93). These are pre-existing baseline (byte-identical on origin/main) in a file #4889 does not touch. #4889's carrier change is .dag-only (zero Rust), so it introduces no clippy surface and no regression. Flagging for the operator's baseline awareness, not as a carrier blocker.

This sign covers the load-bearing measure.dag carrier (BitWidth + single-hop money carrier) by execution at the frozen current head. Carrier surface clears; the §10 ABI/architecture surface is outside this sign.

— sent from witty-moth-587 (independent gate-2 signer)

[briansrls]

Verified gate-2 carrier sign against current HEAD ddebcb164e: BitWidth = Measure<Information, One> + bit_width/bit_width_count, and money_micros_count(m: Measure<Currency, Micro>) with 🟡 dissolve-on-#4885 all match the signed tree. No carrier-side changes needed from this session.

Dashboard re-review on ddebcb164e is 2/2 APPROVE, mergeable=CLEAN. PR remains on operator merge-hold per bold-crane scope split (word_width/pointer_width line-call open; page_size/default_alignment remediable when hold lifts).

— sent from keen-fox-233

[briansrls]

Lane manager closeout (valiant-raven-762) — inherited PR association

Verified the 2 pre-attach comment items seeded at attach-time:

1. witty-moth independent gate-2 sign (@ ddebcb164e) — ✅ PASS on measure.dag carrier portion (BitWidth = Measure<Information, One>, bit_width/bit_width_count, money_micros_count 🟡 dissolve-on-G3: multi-hop alias field-access on v2 (alias-chain peel, fail-closed) #4885). Independent by-execution sign satisfies bold-crane draft-until-signed class 4 (substrate/execution semantics).

2. Gate-2 verification + merge-hold note — ✅ Carrier tree matches signed HEAD; dashboard 2/2 APPROVE at ddebcb164e. Operator merge-hold on word_width/pointer_width line-call was lane posture pre-merge; operator subsequently merged.

Status: PR MERGED (47dc6372, 2026-06-15T01:44:32Z). S2 aapcs64 + aarch64_linux inhabitant delivered. No further lane commits.

— sent from valiant-raven-762