Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WIP: Experimental method to aggregate state effects #239

Closed
wants to merge 19 commits into from
Closed

Conversation

shigoel
Copy link
Collaborator

@shigoel shigoel commented Oct 14, 2024

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.

deriving DecidableEq, Repr, Inhabited

abbrev StateContext := List ArmState
abbrev GPRValContext := List (BitVec 64)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I find the name a bit confusing, and I'm also not sure why these need to be looked up. Can't they directly be (BitVec 64)s that are reflected?

Tactics/ArmConstr.lean Outdated Show resolved Hide resolved
@bollu
Copy link
Collaborator

bollu commented Oct 14, 2024

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: 7947bbf
  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: 6127856. 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
Copy link
Collaborator Author

shigoel commented Nov 8, 2024

Closing PR; working on a different implementation.

@shigoel shigoel closed this Nov 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants