search

leanprover / LNSym

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

refactor: extract out `MemoryEffects` structure #222

Closed alexkeizer closed 4 weeks ago

alexkeizer commented 1 month ago

Description:

Extracted from #179, stacked on #220.

We extract out memory-effects related code from AxEffects into a new MemoryEffects structure. This PR is purely a non-functional change, but will serve as the starting point of integrating simp_mem with sym_n.

The current simplification is effectively a no-op, since the proof state is not massaged to the way simp_mem wants it to be. Subsequent PRs will focus on massaging the goal state to be as simp_mem likes, and then trying to symbolically simplify the memory expression we see.

Testing:

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

License:

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

Co-authored-by @bollusiddu.druid@gmail.com

alexkeizer commented 1 month ago

This extracts the purely non-functional refactor from #179. I've stacked this PR on top of #220 to make use of the common tracing methods we've already added at some point in that stack, so this version of the change resolves all comment that were made on the previous PR, and is ready to merge from my perspective.

alexkeizer commented 4 weeks ago

@shigoel All comment address, this should be ready to merge