leanprover / LNSym

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

chore: split out simp_mem to Arm/Memory/Common [1/?] #230

Closed bollu closed 1 week ago

bollu commented 4 weeks ago

Description:

This will be used in the next paper to build mem_omega, which will be a finishing tactic that will use the full power of omega. simp_mem will be restricted in power to only perform rewriting, allowing us to better control omega.

Testing:

conformance succeeds

License:

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