search

leanprover / LNSym

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

feat: attempt to preserve stack alignment proof in AxEffect update #209

Closed alexkeizer closed 1 month ago

alexkeizer commented 1 month ago

Description:

Stacked on #207.

When an write to memory or a write to a register that is not SP is made, we update the proof of stack alignment. When a write to SP is made, we create a new mvar with the proof obligation that the new value is aligned, and store that mvar in a new sideConditions field.

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.

alexkeizer commented 1 month ago

@shigoel rebased on main and addressed comments!