Skip to content

Lean backend #217

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

Merged
anjapetkovic merged 21 commits into from
Apr 3, 2026
Merged

Lean backend #217

Show file tree
Hide file tree
Changes from 17 commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
ee72c0f
Initial commit
Mar 12, 2026
34d7d26
WIP: Lean backend
anjapetkovic Mar 13, 2026
69199bb
debug based on erc20 and amm examples
anjapetkovic Mar 16, 2026
aa59cfe
remove foo files
anjapetkovic Mar 17, 2026
83bced0
WIP: invariant reachable lean proof
anjapetkovic Mar 17, 2026
953c6b0
Merge branch 'main' into lean
anjapetkovic Mar 17, 2026
de5b329
prettify proofs
anjapetkovic Mar 17, 2026
390930f
fixed Actlib
anjapetkovic Mar 17, 2026
16c4f01
Merge branch 'main' into lean
anjapetkovic Mar 20, 2026
ae19582
fixed InvariantReachable proof
anjapetkovic Mar 25, 2026
5ba0ded
nit
anjapetkovic Mar 25, 2026
026dafc
lean tests
anjapetkovic Mar 25, 2026
1d9c9d0
packaged up lean ActLib + docs for Lean backend
anjapetkovic Mar 27, 2026
9003a58
fix unused vars
anjapetkovic Mar 27, 2026
c5df265
improved lean docs
anjapetkovic Mar 27, 2026
44ac5ad
updated rocq preconditions documentation
anjapetkovic Mar 27, 2026
39e17f5
cleanup
anjapetkovic Mar 27, 2026
dc2805a
Removed left-over hypotheses
lefterislazar Apr 2, 2026
5ff434a
Modified ERC and AMM specs to be compatible with LEAN, and all tests …
lefterislazar Apr 2, 2026
c6a86d4
Added automatic test for compilation of LEAN tests (no theories)
lefterislazar Apr 2, 2026
44ffd7a
Update Doc to incorporate latest changes in hypotheses
lefterislazar Apr 3, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,9 @@ src/dist/
**/RocqMakefile
**/RocqMakefile.conf
**/.RocqMakefile.d
**/CoqMakefile
**/CoqMakefile.conf
**/.CoqMakefile.d
**/.lia.cache
*.aux
**/.coqdeps.d
Expand All @@ -31,5 +34,11 @@ doc/book
# direnv
.direnv/

# lean
**/.lake/
**/lake-manifest.json

*~
*#

*.DS_Store
1 change: 1 addition & 0 deletions act.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ library
Act.Lex
Act.Parse
Act.Rocq
Act.Lean
Act.Syntax
Act.Syntax.Untyped
Act.Syntax.Typed
Expand Down
3 changes: 2 additions & 1 deletion doc/src/SUMMARY.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,8 @@
# Verification with act

- [hevm backend: Equivalence to EVM bytecode](./equiv.md)
- [Rocq backend](./rocq.md)
- [Rocq backend](./rocq.md)
- [Lean backend](./lean.md)



Expand Down
99 changes: 0 additions & 99 deletions doc/src/internals.md
View file
Open in desktop

This file was deleted.

Loading
Loading