search

leanprover / LNSym

Armv8 Native Code Symbolic Simulator in Lean
Apache License 2.0
62 stars 18 forks source link

BLOCKED: feat: intermediate state aggregation through a persistent AxEffects object #210

Open alexkeizer opened 1 month ago

alexkeizer commented 1 month ago

Description:

Stacked on

This PR changes sym_n to keep a single AxEffects object which is updated (rather than replaced) each step.

Currently, this significantly slows down symbolic simulation, causing timeouts when simulation more than ~60 steps of SHA512, and thus breaking a lot of proofs.

Testing:

What tests have been run? Did make all succeed for your changes? Was conformance testing successful on an Aarch64 machine?

License:

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

alexkeizer commented 3 weeks ago

This is currently blocked, waiting on a diagnosis of https://github.com/leanprover/lean4/issues/5610