TCB: compile the assembly only on little-endian targets with the ABI's pointer width

[alex]

Addresses the last finding of #242 ("Endianness and pointer width are assumed and not enforced").

Each target's functions were compiled under target_arch = "…" alone. That also holds on:

• big-endian aarch64_be and armeb, where the ISA models, which are little-endian (TCB/Mem.lean), are wrong;
• x32 and aarch64 ILP32, whose pointers are narrower than the 64-bit calling convention the contracts assume (Abi.ptrBits).

On main the crate builds for aarch64_be, where, per the issue, it returns a wrong SHA-256 for "abc".

⚠️ Trust change

This changes three target definitions, and the doc of Target.rustCfg in TCB/Artifact.lean. It changes no model, contract or Verified.

Each rustCfg now excludes exactly the configurations its architecture has that the model doesn't describe:

target	rustCfg
aarch64	all(target_arch = "aarch64", target_endian = "little", target_pointer_width = "64")
x86_64	all(target_arch = "x86_64", target_pointer_width = "64")
arm	all(target_arch = "arm", target_endian = "little")
x86	target_arch = "x86" (unchanged)

TCB/Artifact.lean documents that a rustCfg must exclude any configuration whose endianness or pointer width differs from the model's.

src/lib.rs has a compile_error! for the same configurations (big-endian aarch64 or arm, 32-bit aarch64 or x86_64), next to the existing one for x86 without SSE2. Otherwise the build would fail with a confusing unresolved import asm::….

Validation

• lake build and lake env lean --run Emit.lean --check: the only change to src/asm/ is the three cfgs in mod.rs.
• These now fail with the compile_error! message: x86_64-unknown-linux-gnux32, and, with nightly -Zbuild-std=core,alloc, aarch64_be-unknown-none-softfloat and armebv7r-none-eabi.
• These still build: x86_64-unknown-linux-gnu, aarch64-unknown-linux-gnu, i686-unknown-linux-gnu, aarch64-unknown-none-softfloat and armv7r-none-eabi.
• cargo test, cargo fmt --check, cargo clippy --all-targets -- -D warnings and ci/check_arch_gates.py pass.

🤖 Generated with Claude Code

https://claude.ai/code/session_017k2Cxdn15GPq2CYjNJDRh1

[alex]

these are too many checks -- it's only arm that has multiple endianesses, and I don't think target_pointer_width is ambigious anywhere at all...

[alex]

Both conditions do exclude real targets. I checked each against main:

• Endianness beyond arm: target_arch = "aarch64" also holds on aarch64_be-unknown-linux-gnu and aarch64_be-unknown-none-softfloat. On main, cargo +nightly check -Zbuild-std=core,alloc --target aarch64_be-unknown-none-softfloat succeeds, and it fails on this branch. That's the issue's wrong-SHA-256 case.
• Pointer width: x86_64-unknown-linux-gnux32 (tier 2, with std) has target_arch = "x86_64" and target_pointer_width = "32", and so does aarch64-unknown-linux-gnu_ilp32. cargo check --target x86_64-unknown-linux-gnux32 succeeds on main, so usize and pointers are 32-bit while the model and contracts assume 64-bit.

You're right that some conditions are redundant: x86 is always little-endian and 32-bit, arm is always 32-bit, and x86_64 is always little-endian. The emitted cfg is uniform because Rust.cfg derives it from Abi.ptrBits rather than listing targets. That way a new target is covered without anyone remembering to add it (e.g. powerpc64 in #108 covers both endiannesses). If you'd rather have minimal cfgs, I can instead put the exact predicate in each target's rustCfg: aarch64 gets endian and width, x86_64 width, arm endian, x86 nothing. I'd also trim the compile_error! in lib.rs to match. Which do you prefer?

---

Generated by Claude Code

[alex]

hi, this still needs action

[alex]

Done in 8ac58bb: each target's rustCfg now has only the conditions its architecture needs.

• aarch64: target_endian = "little" and target_pointer_width = "64" (for aarch64_be and ILP32)
• x86_64: target_pointer_width = "64" (for x32)
• arm: target_endian = "little" (for armeb)
• x86: target_arch = "x86", unchanged

Rust.cfg is gone. lib.rs's compile_error! covers the same configurations: big-endian aarch64 or arm, and 32-bit aarch64 or x86_64. aarch64_be-unknown-none-softfloat, armebv7r-none-eabi and x86_64-unknown-linux-gnux32 fail with its message. aarch64, armv7r, i686 and x86_64 still build.

---

Generated by Claude Code

[alex]

merge conflicts

[alex]

wat, how you can have aarch64 that doesn't have target_poitner_width of 64???

[alex]

rustc has three (all tier 3), from rustc +nightly -Z unstable-options --print target-spec-json --target …:

• aarch64-unknown-linux-gnu_ilp32: "arch": "aarch64", "target-pointer-width": 32
• aarch64_be-unknown-linux-gnu_ilp32: the same, big-endian
• arm64_32-apple-watchos: "arch": "aarch64", "target-pointer-width": 32 (Apple Watch)

All three are AArch64 instructions with a 32-bit data model (ILP32). Pointers and usize are 32 bits in memory and in x registers, whose upper halves the calling convention leaves unspecified. The AArch64 model and contracts assume 64-bit usize and pointers, so without the width check the crate would compile for these targets against the wrong contracts.

---

Generated by Claude Code