I'm trying to build a web app in Rust using axum, and am thinking whether I can export that Rust code to Lean4 so that I can verify business logic or security properties.
I first tried Aeneas, but it can only work for restricted grammer and structurs that are hard to review (it even doesnt look like Rust).
let mut i = 0;
while i < ps.len() {
if ps[i].id == id {
return Some(ps[i].clone());
}
i += 1;
}
None
}
```
Is there anybody who have addressed this kind of problem??
For anyone interested, the experiment source and examples are at https://github.com/h5i-dev/i5h. I've ported parts of a few real web apps (e.g., Kellnr, Atuin, Wastebin, Conduit), and their core logic can now be verified to some extent. Ofcourse, that does assume the rest is correct, like axum/hyper for HTTP and PostgreSQL plus the engine for storage.
I first tried Aeneas, but it can only work for restricted grammer and structurs that are hard to review (it even doesnt look like Rust).
For example, when I want to write:
``` fn find_post(ps: &[Post], id: u64) -> Option<&Post> {
}```
I have to write:
``` pub fn find_post(ps: &Vec<Post>, id: u64) -> Option<Post> {
}```
Is there anybody who have addressed this kind of problem??
For anyone interested, the experiment source and examples are at https://github.com/h5i-dev/i5h. I've ported parts of a few real web apps (e.g., Kellnr, Atuin, Wastebin, Conduit), and their core logic can now be verified to some extent. Ofcourse, that does assume the rest is correct, like axum/hyper for HTTP and PostgreSQL plus the engine for storage.