search

leanprover / LNSym

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

feat: make sym_n search for h_err and h_sp, or introduce new goals if they are not present #75

Closed alexkeizer closed 2 months ago

alexkeizer commented 2 months ago

Description:

Expands upon #69 to include context search for h_err and h_sp. These assumptions are not strictly required, since we don't reflect information from them, so if they are not present we introduce a new goal for them (in contrast to the other hypotheses, for which we simply throw an error).

Testing:

make all succeeds, including conformance testing

License:

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

alexkeizer commented 2 months ago

This PR depends on #69

alexkeizer commented 2 months ago

I've pulled in main after the dependecy got merged, so this is now ready for review: @bollu @shigoel