aeneas
aeneas copied to clipboard
AeneasVerif
A verification toolchain for Rust programs
When running ``` cargo check && nix run github:aeneasverif/aeneas#charon -L -- --hide-marker-traits --remove-associated-types='*' && nix run github:aeneasverif/aeneas -L -- -backend lean sha3.llbc ``` on [a project](https://github.com/ayhon/sha3.rs/tree/f186e6fbd2a1424617166efe11d3daa682583324), I encountered the following...
`scalar_tac` calls `simp_all` in its preprocessing phase to "normalize" the terms, leading to loops when we have assumptions of the shape: `x = f x` in the context. This can...
It should be possible to benefit from more parallelism when building the Lean backend
Aeneas translates trait methods that have a default body because in the future we may want to refer to them. These methods are named `Trait::method`, which in Lean causes a...
# Use Aesop We should use Aesop's `saturate` tactic to saturate the context forward, as it would allow quite expressive patterns in `scalar_tac` like: ```lean @[scalar_tac a < b, c...
Lean now defines types like `UInt8`, `Int8`, etc. We should use those, or at least define the scalars in terms of `BitVec` as it is a more natural representation of...
divergent def fib (n : U32) : Result U32 := match n with | 0#scalar => Result.ok 1#u32 | 1#scalar => Result.ok 1#u32 | _ => do let i ←...
Opaque functions are translated to axioms if we don't use `--split-files`, which can lead to issues because axioms are `noncomputable` in Lean, and all definitions using a non-computable definition should...
First reported on the Zulip: https://aeneas-verif.zulipchat.com/#narrow/channel/349819-general/topic/Bugs.3A.20SHA1.20in.20Aeneas/near/493428308 This can lead to issues with external, non-builtin definitions, like here: ```lean axiom alloc.vec.Vec.extend_from_slice {T : Type} {A : Type} (corecloneCloneInst : core.clone.Clone T)...