Tobias Grosser

This was suggested by @math-fehr on today's meeting.

chore: update to lean4:v4.11.0-rc2

8

Lean is now actively complaining about variable definitions that change theorem statements by only being references in proofs. Hence, we drop some widereaching variable definitions and inline them into the...

AliveStatements: a * allOnes w = -a

1

There is a relatively simple statements in bitvec_152 that remains unsolved: a * allOnes w = -a

This lets us say the following: > We accurately model all semantics in LLVM. For operations that are side-effectful (divisions and remainders), we mark them as such in our framework,...

Lean is complaining about `motive not type correct`. @bollu and I debugged for an hour and could not figure out what's wrong.

llvm: BitVec.xor_neg_one will enable ring_nf to be more powerful

3

The pattern `a ^^^ (-1#w) = (-1#w) - a` arises several times in AliveStatements. Proofing it will in certain cases enable ring to close goals, but it also breaks certain...