aeneas
aeneas copied to clipboard
AeneasVerif
A verification toolchain for Rust programs
Forgive me if this is naive: I was trying out aeneas on some rust code, and hit internal errors. I've managed to minimize the example to the following: ```use std::convert::TryFrom;...
This is related to https://github.com/AeneasVerif/aeneas/pull/563
This is an alternative version of https://github.com/AeneasVerif/aeneas/pull/559 which also improves the performance of `progress*`. As the performance gain was disappointing and as it lead to an significant increase in the...
Currently, at least in the Lean backend, functions and traits are generated with extra fields/arguments for the trait bounds they have, except for the implicit `Sized` bound. In order to...
This PR introduces an issue: https://github.com/AeneasVerif/aeneas/pull/543 Generating several *theorems* at once with a macro like `uscalar` breaks the goto definition. See for instance: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Factoring.20out.20declarations.20with.20a.20macro/with/523917818
Because of this, patterns for `scalar_tac` don't always work in the expected manner (because the pattern may be valid *before* simplification, meaning it doesn't get triggered afterwards).
This is not completely a MWE, but shows the issue: ```lean import Aeneas.Std import Aeneas.ScalarTac axiom List.toBits(ls: List (Aeneas.Std.UScalar ty)): List Bool @[scalar_tac_simps, scalar_tac ls.toBits] axiom List.length_toBits(ls: List (Aeneas.Std.UScalar ty))...
`scalar_tac_preprocess` leaves the following goal unchanged: ```lean @[reducible] def n8 : ℕ := 8 example : n8 * n8 = 64 := by scalar_tac_preprocess sorry ``` There seems to be...