Ask HN: Can we translate normal Rust (axum) to Lean 4 without restrictions?

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).

For example, when I want to write:

``` fn find_post(ps: &[Post], id: u64) -> Option<&Post> {

    ps.iter().find(|p| p.id == id)

}

```

I have to write:

``` pub fn find_post(ps: &Vec<Post>, id: u64) -> Option<Post> {

  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.