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

chore: remove old versions of the sym tactic, and rename the new sym1_n tactic to sym_n #94

Merged
merged 65 commits into from
Aug 20, 2024
Merged

chore: remove old versions of the sym tactic, and rename the new sym1_n tactic to sym_n #94

merged 65 commits into from
Aug 20, 2024

Conversation

alexkeizer
Copy link
Collaborator

Depends on #92

Description:

Relatively minor cleanup that removes the old versions of symbolic simulation in favor of the new sym1_n tactic, which I subsequently renamed to the more intuitive sym_n, now that this name is available.

Testing:

make all ran locally

License:

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

@alexkeizer
chore: add testcase for popcount32_program.stepi_0x4005c0
fd3729d 
This particular instruction's semantics are not being reduced properly,
so the test case is currently failing, but it has the desired
theorem statement
@alexkeizer
fix: use simprocs in step-theorem generation
467b749
@alexkeizer
fix: AbsVCG proof that broke with the new stepi theorem
ff8b501
@alexkeizer
remove note about test failing
32d246c
@alexkeizer
fix: change SHA512 test expectation to reflect more powerful reduction
4b284a6
@alexkeizer
refactor: extract programHypType function
abb7ee3
@alexkeizer
refactor: ProgramInfo namespace
1a56280
@alexkeizer
refactor: store Name as part of ProgramInfo
cbd6e5d
@alexkeizer
refactor: move fetch_inst_eq_of_prgram_eq_of_map_find lemma
acb11bc
@alexkeizer
refactor: move type definitions of expected hyps to Common
a258b9f
@alexkeizer
feat: expand the range of bitvector that can be reflected
f3271f8
@alexkeizer
feat: bitvec to hex utility function
948f453
@alexkeizer
refactor: ProgramInfo tracing, make sure to instantiate mvars, and …
1542ccf 
…allow a definition expr to be passed to `lookupOrGenerate`
@alexkeizer
refactor fetch theorem generation to use ProgramInfo, and to direct…
9de997f 
…ly construct a proof (without simp)
@alexkeizer
refactor: move let-bindings into a more narrow scope for better rea…
b1c1739 
…dability
@alexkeizer
refactor: extract h_pc_type
1c59e02
@alexkeizer
feat: reduceDecodeInst utility to reduce decoded instructions
436bc51
@alexkeizer
refactor: make h_err_type non-monadic
9cc5e45
@alexkeizer
refactor: restate h_pc_type in terms of r, rather than read_pc
982db67
@alexkeizer
feat: yoink #time command from Mathlib
62eeeb4
@alexkeizer
fix: h_pc_type docstring
ec80934
@alexkeizer
feat: ProgramInfo utilities
a161dce
@alexkeizer
feat: stepi_eq_of_fetch_inst_of_decode_raw_inst helper lemma
d207187
@alexkeizer
feat: alternative generation of step theorems
b849e94
@alexkeizer
refactor: remove programHypType
654a73c
@alexkeizer
Merge branch 'main' into better-fetch-theorem-gen
68ef5b8
@alexkeizer
refactor: use the new stepi_eq lemmas in sym1_n
79387c9
@alexkeizer
feat: ProgramInfoT state monad transformer
09559da
@alexkeizer
preparation for caching more instruction info
642f0d5
@alexkeizer
feat: add argument to ProgramInfoT.run that controls whether to per…
c3bc3d4 
…sists the state to the environment afterwards
alexkeizer and others added 20 commits August 16, 2024 15:02
@alexkeizer
add copyright blurb
d3e22f4
@alexkeizer
refactor: add InstInfo.ofRawInst
4a84c51
@alexkeizer
delete old sym tactics
6c222c8
@alexkeizer
Merge branch 'better-fetch-theorem-gen' into nuke-old-sym-tactics
aabbf10
@alexkeizer
refactor: remove old versions of the sym tactic, and rename the new…
4ef25be 
… `sym1_n` tactic to `sym_n`
@alexkeizer
refactor: move around definitions
2f5ede1
@alexkeizer
track an expr for the final state, remove SymContext.default now th…
74bdcb0 
…at it is no longer needed for the old tactics
@alexkeizer
feat: make sym_n change the types of the hypotheses it found to be …
6f5b449 
…exactly of the expected shape (removing the need to `simp` before calling `sym_n`)
@alexkeizer
refactor: use r in stepi_eq_of_fetch_inst_of_decode_raw_inst
f7aa9a2
@alexkeizer @shigoel
Update Tactics/Reflect/ProgramInfo.lean
4487d25 
Co-authored-by: Shilpi Goel <[email protected]>
@alexkeizer
improve docstring for instSemantics?
be96715
@alexkeizer
Merge branch 'better-fetch-theorem-gen' of https://github.com/alexkei…
5ffeeea 
…zer/LNSym into better-fetch-theorem-gen
@alexkeizer
Merge branch 'main' into better-fetch-theorem-gen
a007c3c
@alexkeizer
move toHexWithoutLeadingZeroes to Arm/BitVec kitchen sink file
48c3674
@alexkeizer @shigoel
Apply suggestions from code review
2e3dbbf 
Co-authored-by: Shilpi Goel <[email protected]>
@alexkeizer @shigoel
Update Tactics/StepThms.lean
1d55329 
Co-authored-by: Shilpi Goel <[email protected]>
@alexkeizer
chore: add comment about when you might need canonicalizeBitVec
41a5916
@alexkeizer
fix: actually remove 0x prefix from toHexWithoutLeadingZeroes
e59e004
@alexkeizer
Merge branch 'better-fetch-theorem-gen' into nuke-old-sym-tactics
be904b0
@alexkeizer
Merge branch 'main' into nuke-old-sym-tactics
a15ac64
@alexkeizer alexkeizer marked this pull request as ready for review August 19, 2024 21:33
shigoel
shigoel reviewed Aug 20, 2024
View reviewed changes
Tactics/Sym.lean Show resolved Hide resolved
Tests/Tactics/Sym.lean Show resolved Hide resolved
Tests/Tactics/Sym.lean Show resolved Hide resolved
Tactics/SymContext.lean Outdated Show resolved Hide resolved
@alexkeizer
Copy link
Collaborator Author

@shigoel, this should be ready to merge now

shigoel
shigoel reviewed Aug 20, 2024
View reviewed changes
Tactics/Sym.lean Outdated Show resolved Hide resolved
shigoel
shigoel approved these changes Aug 20, 2024
View reviewed changes
Copy link
Collaborator

@shigoel shigoel left a comment

Choose a reason for hiding this comment

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

Thanks!

@shigoel shigoel merged commit 3f29251 into leanprover:main Aug 20, 2024
2 checks passed
@alexkeizer alexkeizer deleted the nuke-old-sym-tactics branch August 20, 2024 20:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@shigoel shigoel shigoel approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@alexkeizer @shigoel