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.

Sign up for GitHub

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

Jump to bottom

simp_mem failure with GCMGmultV8 #154

Open
shigoel opened this issue Sep 13, 2024 · 1 comment · May be fixed by #218
Open

simp_mem failure with GCMGmultV8 #154

shigoel opened this issue Sep 13, 2024 · 1 comment · May be fixed by #218
Assignees
@bollu

Comments

@shigoel
Copy link
Collaborator

shigoel commented Sep 13, 2024 •
edited
Loading

Ref.: #153

See here: simp_mem creates a malformed term under the hood, forcing the user to manually rewrite with Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'.
@shigoel shigoel changed the title simp_mem failure simp_mem failure with GCMGmultV8 Sep 30, 2024
@shigoel
Copy link
Collaborator Author

shigoel commented Sep 30, 2024

Update: note that simp_mem fails only for the proof obligation

    -- HTable is unmodified.
    sf[read_gpr 64 1#5 s0, 256] = HTable

For the more general obligation (which subsumes the above), simp_mem works fine.

  MEM_UNCHANGED_EXCEPT [(r (.GPR 0) s0, 128)] (sf, s0)

@bollu bollu linked a pull request Oct 4, 2024 that will close this issue
Draft
bollu added a commit that referenced this issue Oct 11, 2024
@bollu
feat: Switch bvOmegaBench to use MetaM
d88a9c9 
This allows us to gradually convert all our tactics to `MetaM`,
which provides the correct level to discipline to make sure
that bugs like #154 don't happen anymore.
Also, as a mild bonus, one hopes that eliminating `evalTactic` makes stuff a bit faster,
but I would not hold my breath on this.
@bollu bollu mentioned this issue Oct 11, 2024
Merged
bollu added a commit that referenced this issue Oct 11, 2024
@bollu
feat: Switch bvOmegaBench to use MetaM
475d1c4 
This allows us to gradually convert all our tactics to `MetaM`,
which provides the correct level to discipline to make sure
that bugs like #154 don't happen anymore.
Also, as a mild bonus, one hopes that eliminating `evalTactic` makes stuff a bit faster,
but I would not hold my breath on this.
bollu added a commit that referenced this issue Oct 11, 2024
@bollu
feat: Switch bvOmegaBench to use MetaM
50ab758 
This allows us to gradually convert all our tactics to `MetaM`,
which provides the correct level to discipline to make sure
that bugs like #154 don't happen anymore.
Also, as a mild bonus, one hopes that eliminating `evalTactic` makes stuff a bit faster,
but I would not hold my breath on this.
bollu added a commit that referenced this issue Oct 11, 2024
@bollu
feat: Switch bvOmegaBench to use MetaM
cd351d7 
This allows us to gradually convert all our tactics to `MetaM`,
which provides the correct level to discipline to make sure
that bugs like #154 don't happen anymore.
Also, as a mild bonus, one hopes that eliminating `evalTactic` makes stuff a bit faster,
but I would not hold my breath on this.
bollu added a commit that referenced this issue Oct 30, 2024
@bollu
feat: Switch bvOmegaBench to use MetaM
617e32b 
This allows us to gradually convert all our tactics to `MetaM`,
which provides the correct level to discipline to make sure
that bugs like #154 don't happen anymore.
Also, as a mild bonus, one hopes that eliminating `evalTactic` makes stuff a bit faster,
but I would not hold my breath on this.
shigoel pushed a commit that referenced this issue Oct 30, 2024
@bollu
feat: Switch bvOmegaBench to use MetaM [3/?] (#232)
486bd6e 
### Description:

This allows us to gradually convert all our tactics to `MetaM`,
which provides the correct level to discipline to make sure
that bugs like #154 don't
happen anymore.
Also, as a mild bonus, one hopes that eliminating `evalTactic` makes
stuff a bit faster,
but I would not hold my breath on this.

Stacked on #231 

### Testing:

What tests have been run? Did `make all` succeed for your changes? Was
conformance testing successful on an Aarch64 machine?

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@bollu bollu

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

chore: bugfixes and benchmark code for the memory based simp_mem leanprover/LNSym
2 participants
@bollu @shigoel