Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
alex merged 4 commits into from
Sep 29, 2026
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
b87fbe5
TCB: compile the assembly only on little-endian targets with the ABI'…
claude Sep 29, 2026
01817b2
Merge remote-tracking branch 'origin/main' into claude/gifted-johnson…
claude Sep 29, 2026
d059682
Merge remote-tracking branch 'origin/main' into claude/gifted-johnson…
claude Sep 29, 2026
8ac58bb
Only the cfg conditions each architecture needs
claude Sep 29, 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
5 changes: 4 additions & 1 deletion lean/VerifiedGarbage/TCB/AArch64/Target.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,10 @@ abbrev target : Target where
isa := isa
printer := printer
abiPreserved := abiPreserved
rustCfg := "target_arch = \"aarch64\""
-- `aarch64_be` targets are big-endian, and ILP32 ones (`aarch64-unknown-linux-gnu_ilp32`)
-- have 32-bit pointers.
rustCfg := "all(target_arch = \"aarch64\", target_endian = \"little\", \
target_pointer_width = \"64\")"
rustAbi := "C"
abi := abi

Expand Down
3 changes: 2 additions & 1 deletion lean/VerifiedGarbage/TCB/Arm/Target.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,8 @@ abbrev target : Target where
isa := isa
printer := printer
abiPreserved := abiPreserved
rustCfg := "target_arch = \"arm\""
-- `armeb` targets are big-endian.
rustCfg := "all(target_arch = \"arm\", target_endian = \"little\")"
rustAbi := "C"
abi := abi

Expand Down
6 changes: 5 additions & 1 deletion lean/VerifiedGarbage/TCB/Artifact.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,11 @@ structure Target where
returns, relating the entry state to the exit state (callee-saved
registers and the stack pointer restored, return address intact). -/
abiPreserved : isa.State → isa.State → Prop
/-- The Rust `cfg` predicate under which this target's functions are compiled. -/
/-- The Rust `cfg` predicate under which this target's functions are
compiled. It must exclude every configuration of the architecture that the
model does not describe: memory is little-endian in every ISA model
(`TCB/Mem.lean`), and pointers have `abi`'s width (`Abi.ptrBits`), which
the contracts assume. -/
rustCfg : String
/-- The Rust ABI string of the generated functions (e.g. `sysv64`). -/
rustAbi : String
Expand Down
3 changes: 2 additions & 1 deletion lean/VerifiedGarbage/TCB/X86_64/Target.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,8 @@ abbrev target : Target where
isa := isa
printer := printer
abiPreserved := abiPreserved
rustCfg := "target_arch = \"x86_64\""
-- x32 targets (`x86_64-unknown-linux-gnux32`) have 32-bit pointers.
rustCfg := "all(target_arch = \"x86_64\", target_pointer_width = \"64\")"
rustAbi := "sysv64"
abi := abi

Expand Down
6 changes: 3 additions & 3 deletions src/asm/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,18 +5,18 @@
//! whose machine code has been proven correct, memory safe and constant time
//! against its contract.

#[cfg(target_arch = "aarch64")]
#[cfg(all(target_arch = "aarch64", target_endian = "little", target_pointer_width = "64"))]

@alex alex Sep 29, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@alex alex Sep 29, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

#[rustfmt::skip]
pub(crate) mod aarch64;

#[cfg(target_arch = "arm")]
#[cfg(all(target_arch = "arm", target_endian = "little"))]
#[rustfmt::skip]
pub(crate) mod arm;

#[cfg(target_arch = "x86")]
#[rustfmt::skip]
pub(crate) mod x86;

@alex alex Sep 29, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 alex Sep 29, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 alex Sep 29, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

hi, this still needs action

@alex alex Sep 29, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


#[cfg(target_arch = "x86_64")]
#[cfg(all(target_arch = "x86_64", target_pointer_width = "64"))]
#[rustfmt::skip]
pub(crate) mod x86_64;
19 changes: 19 additions & 0 deletions src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,25 @@ use asm::x86 as arch;
#[cfg(target_arch = "x86_64")]
use asm::x86_64 as arch;

// The ISA models are little-endian, and the contracts assume the pointer
// width of each architecture's calling convention: the verified assembly is
// compiled only where both hold (each target's `rustCfg`, in
// `lean/VerifiedGarbage/TCB/<Target>/Target.lean`), not on aarch64_be, armeb
// or x32.
#[cfg(any(
all(
any(target_arch = "aarch64", target_arch = "arm"),
target_endian = "big"
),
all(
any(target_arch = "aarch64", target_arch = "x86_64"),
target_pointer_width = "32"
),
))]
compile_error!(
"the verified assembly needs a little-endian target with its architecture's usual pointer width (not, e.g., aarch64_be or x32)"
);

// The 32-bit x86 model's baseline is i686 with SSE2 (see
// `lean/VerifiedGarbage/TCB/X86/Isa.lean`): older CPUs' `mul` is not constant
// time.
Expand Down
Loading