Quentin Garchery

Performance slowdown with version 2.1.0

6

Hi everyone, trying to port my lambdapi programs to version 2.2.0, I noticed a slowdown in the verification. It seems like the issue appeared between version 2.0.0 and 2.1.0. Making...

Rewriting a pattern containing an abstraction

1

Hi again ! Rewriting a pattern that contains an abstraction does not seem to work anymore. For example, running lambdapi version 2.2.0 on the content of [rew_abs.txt](https://github.com/Deducteam/lambdapi/files/8505622/ra.txt) fails with `Uncaught...

Allow rewrite tactic on hypotheses

3

Rewriting on an hypothesis that is defined earlier than the equality to rewrite is cumbersome. ``` require open Stdlib.Set Stdlib.Prop Stdlib.Eq Stdlib.Nat; symbol test_rew_hyp (a b : ℕ) f :...

Parsing fails with bytes32 and address

2

### Component Forge ### Have you ensured that all of these are up to date? - [X] Foundry - [X] Foundryup ### What version of Foundry are you on? forge...

List all the additional steps we could follow to improve the formal verification work: - [x] **update to main**, notably taking into account the storage refactor (done in #373) -...

In Compound it is actually possible to borrow the reserves, in which case utilization > 100%. The computation of the p2p rate of the Compound Lens reverts if utilization >...

When the Lens computes the virtual rate that you would get from entering a position, the p2p amount is not updated. This leads to a rare case where there is...

Formal verification wish list

1

Here is a list of properties that we can try to verify using Certora: - [x] there is a tree of roles: owner > curator > allocator, and owner >...