From b87fbe5731094edf69cb45548492ad8aba573303 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 29 Sep 2026 19:53:17 +0000 Subject: [PATCH 1/2] TCB: compile the assembly only on little-endian targets with the ABI's pointer width Each target's functions were compiled under `target_arch` alone, which also holds on aarch64_be (and armeb), where the little-endian ISA models are wrong, and on x32 (and aarch64 ILP32), where pointers are narrower than the 64-bit calling convention the contracts assume (#242): the crate built for aarch64_be and returned a wrong SHA-256. `Rust.cfg` adds `target_endian = "little"` and the pointer width of the target's `Abi.ptrBits` to its `rustCfg` in the generated `src/asm/mod.rs`, and src/lib.rs fails to compile, with a message saying why, on any configuration of the four architectures that excludes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017k2Cxdn15GPq2CYjNJDRh1 --- lean/VerifiedGarbage/TCB/Artifact.lean | 4 +++- lean/VerifiedGarbage/TCB/Rust.lean | 15 ++++++++++++-- src/asm/mod.rs | 8 ++++---- src/lib.rs | 27 ++++++++++++++++++++++++++ 4 files changed, 47 insertions(+), 7 deletions(-) diff --git a/lean/VerifiedGarbage/TCB/Artifact.lean b/lean/VerifiedGarbage/TCB/Artifact.lean index 41498ae2c..8fcf2a6bf 100644 --- a/lean/VerifiedGarbage/TCB/Artifact.lean +++ b/lean/VerifiedGarbage/TCB/Artifact.lean @@ -43,7 +43,9 @@ 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 naming this target's architecture (e.g. + `target_arch = "x86_64"`). Its functions are compiled where it holds on a + little-endian target with the pointer width of `abi` (`Rust.cfg`). -/ rustCfg : String /-- The Rust ABI string of the generated functions (e.g. `sysv64`). -/ rustAbi : String diff --git a/lean/VerifiedGarbage/TCB/Rust.lean b/lean/VerifiedGarbage/TCB/Rust.lean index a656f64a5..a82930316 100644 --- a/lean/VerifiedGarbage/TCB/Rust.lean +++ b/lean/VerifiedGarbage/TCB/Rust.lean @@ -20,7 +20,11 @@ A naked function has no compiler-generated prologue or epilogue, so the machine code that runs is exactly the code that was verified (plus the final `ret` from the printer). The functions of each target are collected in `src/asm//`, one file per `module`, compiled only under the -target's `cfg`. +target's `cfg` (`Target.rustCfg`), and only where memory is little-endian, as +every ISA model's is (`TCB/Mem.lean`), and pointers have the width of the +target's calling convention (`Abi.ptrBits`), which its contracts assume +(`cfg`): not on, say, `aarch64_be` or x32, whose `target_arch` is also +`aarch64` or `x86_64`. A call (`Code.call name body`) is a call instruction whose operand is the symbol of the Rust function `name` (a `sym` operand). The model runs `body` @@ -205,6 +209,13 @@ def checkUnique (as : List Artifact) : Except String Unit := unless (as.filter fun b => b.target.name == a.target.name && b.name == a.name).length == 1 do throw s!"{a.target.name}: {a.name} is defined more than once" +/-- The Rust `cfg` predicate under which the functions of target `T` are +compiled: its `rustCfg`, on a little-endian target (as the ISA models are) +whose pointers have the width its calling convention and so its contracts +assume (`Abi.ptrBits`). -/ +def cfg (T : Target) : String := + s!"all({T.rustCfg}, target_endian = \"little\", target_pointer_width = \"{T.abi.ptrBits}\")" + /-- `mod` declarations for generated child modules (never reformatted by rustfmt). -/ def modDecls (ms : List String) (cfg : String → Option String) : String := String.join (ms.map fun m => @@ -216,7 +227,7 @@ def modDecls (ms : List String) (cfg : String → Option String) : String := /-- The generated files, given the module of each function each artifact calls. -/ def render (as : List Artifact) (moduleOf : Artifact → String → String) : List (String × String) := let targets := distinct as (·.target.name) - let cfgOf (t : String) : Option String := (as.find? (·.target.name == t)).map (·.target.rustCfg) + let cfgOf (t : String) : Option String := (as.find? (·.target.name == t)).map (cfg ·.target) let root := header ++ "//! Formally verified assembly, emitted from Lean. See `lean/README.md`.\n" ++ diff --git a/src/asm/mod.rs b/src/asm/mod.rs index 5ea4dfd54..8cc9b4ec6 100644 --- a/src/asm/mod.rs +++ b/src/asm/mod.rs @@ -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"))] #[rustfmt::skip] pub(crate) mod aarch64; -#[cfg(target_arch = "x86_64")] +#[cfg(all(target_arch = "x86_64", target_endian = "little", target_pointer_width = "64"))] #[rustfmt::skip] pub(crate) mod x86_64; -#[cfg(target_arch = "arm")] +#[cfg(all(target_arch = "arm", target_endian = "little", target_pointer_width = "32"))] #[rustfmt::skip] pub(crate) mod arm; -#[cfg(target_arch = "x86")] +#[cfg(all(target_arch = "x86", target_endian = "little", target_pointer_width = "32"))] #[rustfmt::skip] pub(crate) mod x86; diff --git a/src/lib.rs b/src/lib.rs index d11d0dc00..75d331276 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -32,6 +32,33 @@ 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 (`Rust.cfg`, in +// `lean/VerifiedGarbage/TCB/Rust.lean`), not on, say, aarch64_be or x32. +#[cfg(any( + all( + any( + target_arch = "aarch64", + target_arch = "arm", + target_arch = "x86", + target_arch = "x86_64" + ), + target_endian = "big" + ), + all( + any(target_arch = "aarch64", target_arch = "x86_64"), + not(target_pointer_width = "64") + ), + all( + any(target_arch = "arm", target_arch = "x86"), + not(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. From 8ac58bbdb12939850601b120e071f8057e52d358 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 29 Sep 2026 20:55:11 +0000 Subject: [PATCH 2/2] Only the cfg conditions each architecture needs Review: `target_endian` and `target_pointer_width` are only ambiguous on some architectures. Each target's `rustCfg` now says exactly what its architecture needs, instead of `Rust.cfg` adding both to all four: aarch64 its endianness (aarch64_be) and pointer width (ILP32), x86_64 its pointer width (x32), arm its endianness (armeb), and x86 nothing. The `compile_error!` in src/lib.rs covers the same configurations. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017k2Cxdn15GPq2CYjNJDRh1 --- lean/VerifiedGarbage/TCB/AArch64/Target.lean | 5 ++++- lean/VerifiedGarbage/TCB/Arm/Target.lean | 3 ++- lean/VerifiedGarbage/TCB/Artifact.lean | 8 +++++--- lean/VerifiedGarbage/TCB/Rust.lean | 15 ++------------- lean/VerifiedGarbage/TCB/X86_64/Target.lean | 3 ++- src/asm/mod.rs | 6 +++--- src/lib.rs | 18 +++++------------- 7 files changed, 23 insertions(+), 35 deletions(-) diff --git a/lean/VerifiedGarbage/TCB/AArch64/Target.lean b/lean/VerifiedGarbage/TCB/AArch64/Target.lean index d02c420bb..dd1ab4de9 100644 --- a/lean/VerifiedGarbage/TCB/AArch64/Target.lean +++ b/lean/VerifiedGarbage/TCB/AArch64/Target.lean @@ -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 diff --git a/lean/VerifiedGarbage/TCB/Arm/Target.lean b/lean/VerifiedGarbage/TCB/Arm/Target.lean index bf381c2f8..f9665701b 100644 --- a/lean/VerifiedGarbage/TCB/Arm/Target.lean +++ b/lean/VerifiedGarbage/TCB/Arm/Target.lean @@ -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 diff --git a/lean/VerifiedGarbage/TCB/Artifact.lean b/lean/VerifiedGarbage/TCB/Artifact.lean index 8fcf2a6bf..d871652a5 100644 --- a/lean/VerifiedGarbage/TCB/Artifact.lean +++ b/lean/VerifiedGarbage/TCB/Artifact.lean @@ -43,9 +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 naming this target's architecture (e.g. - `target_arch = "x86_64"`). Its functions are compiled where it holds on a - little-endian target with the pointer width of `abi` (`Rust.cfg`). -/ + /-- 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 diff --git a/lean/VerifiedGarbage/TCB/Rust.lean b/lean/VerifiedGarbage/TCB/Rust.lean index a82930316..a656f64a5 100644 --- a/lean/VerifiedGarbage/TCB/Rust.lean +++ b/lean/VerifiedGarbage/TCB/Rust.lean @@ -20,11 +20,7 @@ A naked function has no compiler-generated prologue or epilogue, so the machine code that runs is exactly the code that was verified (plus the final `ret` from the printer). The functions of each target are collected in `src/asm//`, one file per `module`, compiled only under the -target's `cfg` (`Target.rustCfg`), and only where memory is little-endian, as -every ISA model's is (`TCB/Mem.lean`), and pointers have the width of the -target's calling convention (`Abi.ptrBits`), which its contracts assume -(`cfg`): not on, say, `aarch64_be` or x32, whose `target_arch` is also -`aarch64` or `x86_64`. +target's `cfg`. A call (`Code.call name body`) is a call instruction whose operand is the symbol of the Rust function `name` (a `sym` operand). The model runs `body` @@ -209,13 +205,6 @@ def checkUnique (as : List Artifact) : Except String Unit := unless (as.filter fun b => b.target.name == a.target.name && b.name == a.name).length == 1 do throw s!"{a.target.name}: {a.name} is defined more than once" -/-- The Rust `cfg` predicate under which the functions of target `T` are -compiled: its `rustCfg`, on a little-endian target (as the ISA models are) -whose pointers have the width its calling convention and so its contracts -assume (`Abi.ptrBits`). -/ -def cfg (T : Target) : String := - s!"all({T.rustCfg}, target_endian = \"little\", target_pointer_width = \"{T.abi.ptrBits}\")" - /-- `mod` declarations for generated child modules (never reformatted by rustfmt). -/ def modDecls (ms : List String) (cfg : String → Option String) : String := String.join (ms.map fun m => @@ -227,7 +216,7 @@ def modDecls (ms : List String) (cfg : String → Option String) : String := /-- The generated files, given the module of each function each artifact calls. -/ def render (as : List Artifact) (moduleOf : Artifact → String → String) : List (String × String) := let targets := distinct as (·.target.name) - let cfgOf (t : String) : Option String := (as.find? (·.target.name == t)).map (cfg ·.target) + let cfgOf (t : String) : Option String := (as.find? (·.target.name == t)).map (·.target.rustCfg) let root := header ++ "//! Formally verified assembly, emitted from Lean. See `lean/README.md`.\n" ++ diff --git a/lean/VerifiedGarbage/TCB/X86_64/Target.lean b/lean/VerifiedGarbage/TCB/X86_64/Target.lean index b25434294..ce11cb0a5 100644 --- a/lean/VerifiedGarbage/TCB/X86_64/Target.lean +++ b/lean/VerifiedGarbage/TCB/X86_64/Target.lean @@ -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 diff --git a/src/asm/mod.rs b/src/asm/mod.rs index da6564e1f..2ff1de918 100644 --- a/src/asm/mod.rs +++ b/src/asm/mod.rs @@ -9,14 +9,14 @@ #[rustfmt::skip] pub(crate) mod aarch64; -#[cfg(all(target_arch = "arm", target_endian = "little", target_pointer_width = "32"))] +#[cfg(all(target_arch = "arm", target_endian = "little"))] #[rustfmt::skip] pub(crate) mod arm; -#[cfg(all(target_arch = "x86", target_endian = "little", target_pointer_width = "32"))] +#[cfg(target_arch = "x86")] #[rustfmt::skip] pub(crate) mod x86; -#[cfg(all(target_arch = "x86_64", target_endian = "little", target_pointer_width = "64"))] +#[cfg(all(target_arch = "x86_64", target_pointer_width = "64"))] #[rustfmt::skip] pub(crate) mod x86_64; diff --git a/src/lib.rs b/src/lib.rs index 69eff5290..6b3991786 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -34,25 +34,17 @@ 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 (`Rust.cfg`, in -// `lean/VerifiedGarbage/TCB/Rust.lean`), not on, say, aarch64_be or x32. +// compiled only where both hold (each target's `rustCfg`, in +// `lean/VerifiedGarbage/TCB//Target.lean`), not on aarch64_be, armeb +// or x32. #[cfg(any( all( - any( - target_arch = "aarch64", - target_arch = "arm", - target_arch = "x86", - target_arch = "x86_64" - ), + any(target_arch = "aarch64", target_arch = "arm"), target_endian = "big" ), all( any(target_arch = "aarch64", target_arch = "x86_64"), - not(target_pointer_width = "64") - ), - all( - any(target_arch = "arm", target_arch = "x86"), - not(target_pointer_width = "32") + target_pointer_width = "32" ), ))] compile_error!(