Rendered at 13:12:26 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
himata4113 8 hours ago [-]
talos is already in use by https://github.com/siderolabs/talos, was confused for a second when I saw talos and wasm for a second, got excited about native wasm pod support.
What is the program logic used here? The num_integer verification example seems to be hardcoding addresses in the spec; what if I want to reason about larger programs that dynamically allocate, where the addresses may not be known statically? How can I make sure these do not overlap? And since this is a shallow embedding into lean, what’s the approach for verifying properties of non-terminating programs?
mfornet 43 minutes ago [-]
> what if I want to reason about larger programs that dynamically allocate, where the addresses may not be known statically? How can I make sure these do not overlap?
We are actively working on this, as it is a pre-condition :P to reason about the simplest of useful programs. The idea is to develop an API around separation logic that allows you to reason about logic that manipulate non-overlapping regions of memory.
It won't be relevant if address are not known statically since API theorems will be parametrized over non-relevant constants such as addresses, function indices, etc...
> And since this is a shallow embedding into lean, what’s the approach for verifying properties of non-terminating programs?
To use the interpreter there is the concept of fuel, which we explicitly hide from the reasoning layer. Using fuel you can write statements of the form, this function returns out of fuel for any value of fuel passed to the interpreter, which is equivalent to prove that your program doesn't terminate.
oulipo2 20 minutes ago [-]
Interesting, have you also looked at other formal methods, like Abstract Interpretation?
lukerj00 22 hours ago [-]
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 7 hours ago [-]
What other verification targets did you consider?
mfornet 39 minutes 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.
quietusmuris 20 hours ago [-]
Interesting. Do I have to write specs in Lean against the Wasm semantics or can you annotate Rust directly?
mfornet 36 minutes ago [-]
Both.
You can write "annotate" your rust code using asserts. On the wasm side asserts are converted to trap instructions, so the Lean spec will simply be: For every input this code never traps.
Part of our focus is making sure that specs are both easy to write and read, since they are human facing. Eventually you could imagine how writing code will mostly be writing specs, and both the code and the proofs will be handled by AI agents. In this scenario it is very important that humans can easily audit and modify the specs.
sohex 1 hours ago [-]
Do people just not even search their proposed name anymore?
IshKebab 26 minutes ago [-]
It's ok for multiple different things to use the same name.
I wish these comments were banned. They come up every time someone names a project with a name that was also used by one guy for his forgotten Lisp dialect in the 70s.
CurryFurry 4 hours ago [-]
For "Lean"? LeaRn? Lean Manufacturing? Stupid one-word techbro product names.
johnsonjo 1 hours ago [-]
Lean is a programming language [1]
> Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code
We are actively working on this, as it is a pre-condition :P to reason about the simplest of useful programs. The idea is to develop an API around separation logic that allows you to reason about logic that manipulate non-overlapping regions of memory.
It won't be relevant if address are not known statically since API theorems will be parametrized over non-relevant constants such as addresses, function indices, etc...
> And since this is a shallow embedding into lean, what’s the approach for verifying properties of non-terminating programs?
To use the interpreter there is the concept of fuel, which we explicitly hide from the reasoning layer. Using fuel you can write statements of the form, this function returns out of fuel for any value of fuel passed to the interpreter, which is equivalent to prove that your program doesn't terminate.
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).
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.
You can write "annotate" your rust code using asserts. On the wasm side asserts are converted to trap instructions, so the Lean spec will simply be: For every input this code never traps.
Part of our focus is making sure that specs are both easy to write and read, since they are human facing. Eventually you could imagine how writing code will mostly be writing specs, and both the code and the proofs will be handled by AI agents. In this scenario it is very important that humans can easily audit and modify the specs.
https://en.wikipedia.org/wiki/Lynx_(disambiguation)
I wish these comments were banned. They come up every time someone names a project with a name that was also used by one guy for his forgotten Lisp dialect in the 70s.
> Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code
[1]: https://lean-lang.org/