Re:AlphaProof Code
by ane on Tuesday November 10, 2026 @08:07AM
(#50439778)
How is guaranteed that whatever the compiled Rust code running on a Lean model of a processor is doing matches what a real processor is doing? How do we know that the Lean spec that it wrote based on the specification matches what the Rust code that implements Signal does?
[ Parent
| on HN ]
It's not and we don't. We can however run some lean in rust with things like https://github.com/conao3/lean-rs
Or you can use verus instead which does automatic mapping from the rust code to the proof where possible.
Re:AlphaProof Code
by Paracompact on Tuesday November 10, 2026 @08:49AM
(#50440323)
Not sure why you're responding with information that would imply they modeled Rust in Lean or vice versa. As I explained, their target was the compiled ELF binary, not Rust source. This way, they avoid including the entire Rust compiler and its as-yet formally undefined semantics into the trusted computing base.
[delayed]
Re:AlphaProof Code
by Paracompact on Tuesday November 10, 2026 @08:36AM
(#50440131)
Rust need not apply, since the proof is about the libsignal-cli ELF binary, compiled under reasonable assumptions (single-threaded, statically linked, etc). The Lean semantics of the some-hundred instructions were tested to adhere to Arm-provided ASL spec, as compared to two independent emulators.