3 ms·

I’m on the Cajal team - not OP, but happy to answer questions. The core bet is that Wasm is a good verification target (close to compiled artifacts, many langu

I’m on the Cajal team - not OP, but happy to answer questions. The core bet is that Wasm is a good verification target (close to compiled artifacts, many languages target it), and Lean is the right place to do verification. Super interested in hearing from people working with Lean, compilers or other Wasm verification frameworks (eg Iris-Wasm).

kdavis 4mo ago
What other verification targets did you consider?
- mfornet 4mo ago
  Initially we considered formalizing rust code, aeneas is a very promising project that would unlock a lot of features right way by transpiling to lean. However, we didn't want to lock ourselves to rust, so we decided to use a lower level target such that we could verify code from "any" language. We considered LLVM-IR, and RISC-V. Ultimately WASM felt like the right decisions. More importantly WASM spec is very well done in details, and it is written with formal verification in mind early on, and there are are plans from to include Lean as one of the targets for generating the spec automatically from SpecTec. Once this exist, we will formalize that our interpreter is correct under the definition generated from the official Wasm-Lean-Spec so we remove it from the Trusted-Base going forward.
- lukerj00 4mo ago
  More on this - LLVM-IR has no official formal semantics and it's riddled with UB. RISC-V has a formal model in Sail, but it's an ISA so you throw away the structured control flow and types which we want for proving. Wasm has different levels we can validate against - starting with W3C test suite, then later full verification against the SpecTec-generated Lean semantics so that we can drop our interpreter from the trusted base.
jsmorph 4mo ago
Cool. I've been working on a compiler for a subset of Lean that targets WASM. The compiler is implemented in Lean. https://github.com/jsmorph/leanexe https://github.com/jsmorph/leanexe I think I managed to use Talos to prove the WAT generated from an example LeanExe program is correct. ? https://gist.github.com/jsmorph/275a15dc21af037e1d02a1b433bef81f https://gist.github.com/jsmorph/275a15dc21af037e1d02a1b433be... Fun.

kdavis 4mo ago

What other verification targets did you consider?

mfornet 4mo ago
Initially we considered formalizing rust code, aeneas is a very promising project that would unlock a lot of features right way by transpiling to lean. However, we didn't want to lock ourselves to rust, so we decided to use a lower level target such that we could verify code from "any" language. We considered LLVM-IR, and RISC-V. Ultimately WASM felt like the right decisions. More importantly WASM spec is very well done in details, and it is written with formal verification in mind early on, and there are are plans from to include Lean as one of the targets for generating the spec automatically from SpecTec. Once this exist, we will formalize that our interpreter is correct under the definition generated from the official Wasm-Lean-Spec so we remove it from the Trusted-Base going forward.
lukerj00 4mo ago
More on this - LLVM-IR has no official formal semantics and it's riddled with UB. RISC-V has a formal model in Sail, but it's an ISA so you throw away the structured control flow and types which we want for proving. Wasm has different levels we can validate against - starting with W3C test suite, then later full verification against the SpecTec-generated Lean semantics so that we can drop our interpreter from the trusted base.

jsmorph 4mo ago

Cool. I've been working on a compiler for a subset of Lean that targets WASM. The compiler is implemented in Lean. https://github.com/jsmorph/leanexe https://github.com/jsmorph/leanexe I think I managed to use Talos to prove the WAT generated from an example LeanExe program is correct. ? https://gist.github.com/jsmorph/275a15dc21af037e1d02a1b433bef81f https://gist.github.com/jsmorph/275a15dc21af037e1d02a1b433be... Fun.