Skip to content

Generalize the Result type and implement a loop invariant inferencer #599

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

Draft
sonmarcho wants to merge 48 commits into
base: main
Choose a base branch
from
Draft

Generalize the Result type and implement a loop invariant inferencer #599

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
48 commits
Select commit Hold shift + click to select a range
81e95eb
Make the `Result` type more general to allow returns, breaks and cont…
sonmarcho Aug 15, 2025
085b486
Start implementing a invariant inferencer
sonmarcho Aug 15, 2025
c9bd198
Implement getters/setters/array values decomposition
sonmarcho Aug 15, 2025
bef1fd0
Fix a typo
sonmarcho Aug 15, 2025
da6212d
Make progress on the invariant inferencer
sonmarcho Aug 17, 2025
079ab21
Start writing some tests for Inv
sonmarcho Aug 17, 2025
e34c7b9
Make progress on the tests for inv
sonmarcho Aug 17, 2025
cfdf942
Add support for tuple expressions
sonmarcho Aug 17, 2025
13bdbac
Properly handle OfNat.ofNat
sonmarcho Aug 17, 2025
2bbc292
Improve printing
sonmarcho Aug 17, 2025
b6c2b5a
Add some tests
sonmarcho Aug 18, 2025
a666911
Update the handling of tuples
sonmarcho Aug 18, 2025
6827b4e
Properly handle matches on Prod and MProd
sonmarcho Aug 18, 2025
ab8a9c8
Make minor modifications
sonmarcho Aug 18, 2025
893ffa2
Properly handle tuple projectors and let bindings
sonmarcho Aug 18, 2025
b0d1f3a
Add support for binary arithmetic operations
sonmarcho Aug 18, 2025
d4a3ade
Improve printing
sonmarcho Aug 18, 2025
8c17e25
Start adding support for Fin
sonmarcho Aug 18, 2025
d0082e2
Improve the minimization of expressions
sonmarcho Aug 18, 2025
4cd970a
Properly support monadic binds
sonmarcho Aug 18, 2025
84b31d2
Make minor modifications
sonmarcho Aug 18, 2025
5c62b0a
Make minor modifications
sonmarcho Aug 18, 2025
8aad9e4
Add a `range` variant in `ArithExpr` and `FootprintExpr`
sonmarcho Aug 18, 2025
900b19e
Handle structure constructors in a general manner
sonmarcho Aug 18, 2025
3139f2a
Generalize the handling of projectors
sonmarcho Aug 18, 2025
b08f5d9
Fix the FootprintM monad
sonmarcho Aug 18, 2025
f796de9
Generalize the handling of `casesOn`
sonmarcho Aug 18, 2025
b383910
Nit
sonmarcho Aug 18, 2025
79bbebc
Start working on the normalization of arithmetic expressions
sonmarcho Aug 19, 2025
cdb7159
Implement a function to simplify and normalize the outputs
sonmarcho Aug 19, 2025
a95cf2a
Check the outputs of the analysis
sonmarcho Aug 20, 2025
00c2eea
Start adding extensible support for loop definitions
sonmarcho Aug 20, 2025
b55deac
Make the handling of variables more general
sonmarcho Aug 20, 2025
9180033
Remove ArithExpr and make LinArithExpr more general
sonmarcho Aug 20, 2025
c254777
Rename Inv/Inv.lean to Inv/Base.lean
sonmarcho Aug 20, 2025
f16dbab
Make the loop_inv_iter attribute work
sonmarcho Aug 20, 2025
672ded8
Start generalizing to support nested loops
sonmarcho Aug 20, 2025
b999658
Lift `analyzeFootprint` in the `MetaM` monad and fix a mistake
sonmarcho Aug 20, 2025
fef49e5
Cleanup a bit
sonmarcho Aug 20, 2025
032318a
Cleanup
sonmarcho Aug 20, 2025
0221309
Use a stack to determine the order in which to normalize the loops
sonmarcho Aug 21, 2025
0e9884c
Start applying the loop relations to their inputs
sonmarcho Aug 21, 2025
c64be8e
Make progress on supporting loops which modify counters
sonmarcho Aug 21, 2025
418c92e
Make good progress on supporting counter increments
sonmarcho Aug 21, 2025
4dd4a41
Fix a minor issue
sonmarcho Aug 21, 2025
7d36c94
Properly handle arrays updated accross nested loops
sonmarcho Aug 21, 2025
152c171
Refactor Inv/Base.lean and start working on Inv/Formula.lean
sonmarcho Aug 21, 2025
df26ced
Start implementing the lifting of pres and posts
sonmarcho Aug 22, 2025
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
1 change: 1 addition & 0 deletions backends/lean/Aeneas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import Aeneas.FCongr
import Aeneas.Fin
import Aeneas.FSimp
import Aeneas.Int
import Aeneas.Inv
import Aeneas.Let
import Aeneas.List
import Aeneas.Nat
Expand Down
2 changes: 2 additions & 0 deletions backends/lean/Aeneas/Inv.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
import Aeneas.Inv.Base
import Aeneas.Inv.Test
Loading
Loading