GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.
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
Use sep-algebra instead of ad-hoc separation logic framework.
Pack pretty much all rules added to simpset in bundles.
Fix existing proofs.
More reproving of lemmas with grouped lemmas.
Progress on HoareTripleForInstruction.thy cleanup.
More cleanup / breakage.
Only a few [simp] left to remove.
No more superfluous [simp] in HoareTripleInstructions
Start looking at Storage lemmas.
More cleaning up.
More triple storage cleanup.
Finally got storage triple working.
More cleanup of storage and update next lemma too.
Start inst 2 cleanup.
Progress on inst2
More inst2 cleanup.
progress on swap cleanup.
stalling on swap :/
Fall back to bundles instead of modifying all the proofs.
LogGasCall partially checks.
More of log gas call triples with bundles.
Fix more of loggascall.
quick refactoring of loggascall.
Speeding up memory_range proofs.
More speed up/fix of loggascall.
Speedup some of inst2 lemmas, finish loggascall and start simple wallet.
Add missing lemmas moved from loggascall to inst.
More proof speedup and SimpleWallet update.
Progress on fixing SimpleWallet.
Speed up proof slightly.
Thanks a lot!