refactor: cleanup popcount proof

[alexkeizer]

Description:

We've cleaned up the popcount proof by:

• extending sym_aggregate to also search for memory effect hypotheses to simplify, and
• changing the semantics of add_sub_immediate to avoid pattern-matching. It turns out that pattern-matching on the result of an if (e.g., let (a, b) := if x = 0 then (foo, bar) else (bar, foo)) get's reduced to a Decidable.rec by simp only, which then gets stuck. By rephrasing it in terms of projections, we avoid this, and get clean simplified semantics.
• In the same vein, we also add existing simplification rules for AddWithCarry to the bitvec_rules simpset

Testing:

make all succeeds.

License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

[alexkeizer]

I've opened an issue upstream for the pattern-matching beheviour: leanprover/lean4#5388

[bollu]

To be rebased on top of #171

[bollu]

@alexkeizer after rebasing, for whatever reason, proofs in Sha512Prelude break due to maxRecDepth :(

I tried debugging this for a bit, then gave up:

✖ [129/135] Building Proofs.SHA512.SHA512Prelude
trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib:././.lake/packages/ELFSage/.lake/build/lib:././.lake/packages/MD4Lean/.lake/build/lib:././.lake/packages/UnicodeBasic/.lake/build/lib:././.lake/packages/BibtexQuery/.lake/build/lib:././.lake/packages/doc-gen4/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH= /Users/sidbhatz/.elan/toolchains/leanprover--lean4---nightly-2024-09-10/bin/lean ././././Proofs/SHA512/SHA512Prelude.lean -R ./././. -o ././.lake/build/lib/Proofs/SHA512/SHA512Prelude.olean -i ././.lake/build/lib/Proofs/SHA512/SHA512Prelude.ilean -c ././.lake/build/ir/Proofs/SHA512/SHA512Prelude.c --json
error: ././././Proofs/SHA512/SHA512Prelude.lean:164:0: linter Lean.Linter.constructorNameAsVariable failed: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
error: ././././Proofs/SHA512/SHA512Prelude.lean:283:0: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
error: ././././Proofs/SHA512/SHA512Prelude.lean:284:0: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
info: stderr:
PANIC at outOfBounds Init.GetElem:11:2: index out of bounds
PANIC at outOfBounds Init.GetElem:11:2: index out of bounds
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:56:21: unexpected context-free info tree node
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:56:21: unexpected context-free info tree node
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:56:21: unexpected context-free info tree node
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:56:21: unexpected context-free info tree node
error: Lean exited with code 1
Some required builds logged failures:
- Proofs.SHA512.SHA512Prelude
error: build failed
real 17.04
user 16.36
sys 0.46
make: *** [proofs] Error 1

[bollu]

@alexkeizer I think we should add an option into sym_aggregate that controls whether it tries to simplify memory as well, and to maybe gradually unroll this across the codebase?

[bollu]

Aha, let me try and just disable all linters...