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.
Doesn't that put the Rust compiler (and its assert lowering) in the trusted base? How do you know the asserts you wrote are the traps you're reasoning about?
> Doesn't that put the Rust compiler (and its assert lowering) in the trusted base?
Yes, but I would argue the are already in the trusted base before this project, we are not removing that. We want instead remove "your code" from the trusted base, and just keep the compiler and the specs.
> How do you know the asserts you wrote are the traps you're reasoning about?
You just do. The asserts and the specs have a similar role, they are both consumer facing, and consumers need to make sure they are correct and cover what it is intended.
How do you actually prove it though? I understand if it's fully automated SMT-style proof, but doesn't Lean require tediously explicit proofs? If it doesn't prove automatically do you have to write out Lean helper proofs about the compiled WASM?
AI has been great so far filling in most of the proofs, and I'm trying to avoid SMT-style proofs early on, to make sure we have a solid API that can be scaled to arbitrary complex code without increasing too much the cost of the verification. I'm sure nonetheless that SMT solvers will play a role going forward in filling up some proofs.
The reason AI has been so good at filling most of the proofs in my opinion, is that proofs are actually "simple", but very tedious and long. Part of our work right now is make sure that the tedious part can be solved mechanically as easy and efficient as possible, so both human or AI can focus on the interesting parts.
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.
Doesn't that put the Rust compiler (and its assert lowering) in the trusted base? How do you know the asserts you wrote are the traps you're reasoning about?
> Doesn't that put the Rust compiler (and its assert lowering) in the trusted base?
Yes, but I would argue the are already in the trusted base before this project, we are not removing that. We want instead remove "your code" from the trusted base, and just keep the compiler and the specs.
> How do you know the asserts you wrote are the traps you're reasoning about?
You just do. The asserts and the specs have a similar role, they are both consumer facing, and consumers need to make sure they are correct and cover what it is intended.
How do you actually prove it though? I understand if it's fully automated SMT-style proof, but doesn't Lean require tediously explicit proofs? If it doesn't prove automatically do you have to write out Lean helper proofs about the compiled WASM?
AI has been great so far filling in most of the proofs, and I'm trying to avoid SMT-style proofs early on, to make sure we have a solid API that can be scaled to arbitrary complex code without increasing too much the cost of the verification. I'm sure nonetheless that SMT solvers will play a role going forward in filling up some proofs.
The reason AI has been so good at filling most of the proofs in my opinion, is that proofs are actually "simple", but very tedious and long. Part of our work right now is make sure that the tedious part can be solved mechanically as easy and efficient as possible, so both human or AI can focus on the interesting parts.