search

leanprover / LNSym

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

WIP: Experimental method to aggregate state effects #239

Closed shigoel closed 4 hours ago

shigoel commented 3 weeks ago

Description:

Experimental method, inspired by simp_arith, to aggregate state effects.

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.

bollu commented 3 weeks ago

I experimented with this a bit, and here's what I found:

  1. It seems like we can cleanup at least some of the impl by using stdlib constructs like foldl. I did this in this commit: https://github.com/leanprover/LNSym/commit/7947bbfc4828a4ae34e740790d490fe75298f70b
  2. Switching to Std.HashMap means that we can't straight up talk about the hashmaps being defeq (because they need not be structurally equal, only extensionally equal). Defining extensional equality and trying to switch to it also does not work, because we seem to lose defeqs: https://github.com/leanprover/LNSym/commit/612785659b7838edee41cca532a4691fc459daa4. I'm not sure why we lose defeq, maybe @alexkeizer can chime in. Best guess: something in HashMap uses well-founded recursion, not structural recursion, which breaks defeq :(
shigoel commented 4 hours ago

Closing PR; working on a different implementation.