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

Make a massive revamp of the Lean backend #444

Draft
wants to merge 86 commits into
base: main
Choose a base branch
from
+12,086 −4,843
Draft

Make a massive revamp of the Lean backend #444

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
86 commits
Select commit Hold shift + click to select a range
af0c52c
Add some arithmetic facts
sonmarcho Feb 3, 2025
6bef6be
Add more arithmetic facts
sonmarcho Feb 3, 2025
2a93da0
Start updating the Scalar definition to use bit vectors
sonmarcho Feb 4, 2025
8efe8f5
Update scalar_tac
sonmarcho Feb 4, 2025
0fbc6f3
Make progress on updating the scalar defs and proofs
sonmarcho Feb 7, 2025
8058ba7
Add the lemmas about division
sonmarcho Feb 7, 2025
d3677d4
Make progress on the lemmas about remainder
sonmarcho Feb 10, 2025
b1154db
Add the theorems about the remainder operation
sonmarcho Feb 10, 2025
6b3947e
Add the definitions for checked operations
sonmarcho Feb 10, 2025
9bd6204
Update the theorems about the division
sonmarcho Feb 10, 2025
2585304
Add specs for the checkeds operations
sonmarcho Feb 10, 2025
ec4beab
Add lemmas to reason about the casts
sonmarcho Feb 10, 2025
12c8a6b
Cleanup a bit and add models for leading_zeros
sonmarcho Feb 10, 2025
194d7e1
Add the missing scalar definitions and theorems
sonmarcho Feb 10, 2025
c9888fc
Update the bound definitions in ScalarCore.lean
sonmarcho Feb 11, 2025
67d494d
Update the definitions of Array, Slice and Vec
sonmarcho Feb 11, 2025
f67b924
Update ScalarNotations.lean
sonmarcho Feb 14, 2025
6a5f7e3
Update CoreConvertNum.lean
sonmarcho Feb 14, 2025
18732ba
Update Progress/Progress.lean
sonmarcho Feb 14, 2025
19e032f
Add simp lemmas in ScalarCore.lean
sonmarcho Feb 14, 2025
e0007b9
Update overflowing_add
sonmarcho Feb 14, 2025
c3f86c6
Update the extraction
sonmarcho Feb 14, 2025
7d27a94
Merge remote-tracking branch 'origin/main' into son/lean
sonmarcho Feb 14, 2025
917068a
Regenerate the tests
sonmarcho Feb 14, 2025
2c861ca
Fix the extraction of casts
sonmarcho Feb 14, 2025
46c0767
Add a micro-pass and use ok and fail instead of Result.{ok,fail}
sonmarcho Feb 14, 2025
6b49eba
Regenerate the tests
sonmarcho Feb 14, 2025
c9694f9
Do not inline all the primitive operations
sonmarcho Feb 14, 2025
351fe2f
Add the builtin information directly in the pure declarations
sonmarcho Feb 14, 2025
28d55ce
Add a micro-pass to lift pure function calls to monadic function calls
sonmarcho Feb 17, 2025
f968bdc
Attempt to write a first version of progress_pure
sonmarcho Feb 18, 2025
16ee948
Write a first working version of the lifting function for progress_pure
sonmarcho Feb 19, 2025
68a3928
Start cleaning up the liftThm function for progress_pure
sonmarcho Feb 19, 2025
09479d0
Finish cleaning up Progress.Core.lean
sonmarcho Feb 19, 2025
e681709
Fix a minor issue in Progress.Core.lean
sonmarcho Feb 19, 2025
b22c8c5
Fix some issues in Progress/Core.lean
sonmarcho Feb 19, 2025
9b22edd
Add a progress_pure_def attribute
sonmarcho Feb 19, 2025
2a99d8c
Use progress_pure and progress_pure_def in Scalar.lean
sonmarcho Feb 19, 2025
303afbc
Add lemmas and improve some tactics
sonmarcho Feb 20, 2025
ce00eb1
Add annotations to the generated code in the presence of coercions
sonmarcho Feb 20, 2025
0e5f988
Update the tutorial
sonmarcho Feb 20, 2025
4843b46
Cleanup the tutorial a bit
sonmarcho Feb 20, 2025
ea37a61
Replace the ScalarTac.nonLin option with a config field
sonmarcho Feb 20, 2025
6bd398c
Add some forgotten progress annotations
sonmarcho Feb 20, 2025
5fdbe68
Implement minimize_goal and improve extract_goal
sonmarcho Feb 20, 2025
974ce9b
Make minor modifications
sonmarcho Feb 20, 2025
a3bcafe
Implement the scalar_tac_simp attribute
sonmarcho Feb 20, 2025
46e0729
Add simp lemmas for scalar_tac
sonmarcho Feb 20, 2025
c4a6897
Make minor modifications
sonmarcho Feb 20, 2025
a911914
Make more simplifications to scalar_tac
sonmarcho Feb 20, 2025
034ccb9
Merge int_tac and scalar_tac
sonmarcho Feb 20, 2025
6cff3d7
Add an expensive minimal exemple in progress
sonmarcho Feb 20, 2025
741b744
Add a simpAll option to scalar_tac and save some profiling results
sonmarcho Feb 21, 2025
00d8bff
Allow the syntax `progress with term`
sonmarcho Feb 21, 2025
ea3563a
Fix an issue and improve the extract_goal tactic
sonmarcho Feb 21, 2025
fc252de
Fix the proofs about the AVL tree
sonmarcho Feb 21, 2025
d000d04
Implement the local progress attribute
sonmarcho Feb 21, 2025
4e9ec83
Implement a progress_simp attribute
sonmarcho Feb 21, 2025
705b1d6
Improve extract_goal to rename the shadowed variables
sonmarcho Feb 21, 2025
df4ca98
Fix the proof of the hashmap
sonmarcho Feb 21, 2025
f9cb0bd
Make most of the scalar constant definitions reducible
sonmarcho Feb 21, 2025
7256852
Fix a minor issue
sonmarcho Feb 21, 2025
8f24e4a
Reactivate the use of simpAll by default in scalar_tac
sonmarcho Feb 21, 2025
99cf0c1
Always use simp_all in the preprocessing step of scalar_tac
sonmarcho Feb 24, 2025
c4ccf2b
Introduce fsimp and fsimp_all
sonmarcho Feb 24, 2025
6590d4a
Use fsimp instead of simp in the proofs of the hashmap and the AVL tree
sonmarcho Feb 24, 2025
02cf81d
Make minor modifications
sonmarcho Feb 24, 2025
d68fc19
Make a minor modification
sonmarcho Feb 24, 2025
3e5af2b
Improve extract_goal and make progress use `saturareFast` in `scalar_…
sonmarcho Feb 24, 2025
a1ac863
Add a comment
sonmarcho Feb 24, 2025
b8801a8
Add a comment
sonmarcho Feb 24, 2025
920d018
Make a minor modification
sonmarcho Feb 24, 2025
fc44471
Add some arithmetic lemmas
sonmarcho Feb 25, 2025
b422e97
Implement the natify tactic
sonmarcho Feb 25, 2025
0a7e3ef
Implement the bvify tactic
sonmarcho Feb 25, 2025
d5d9d95
Implement bv_tac
sonmarcho Feb 25, 2025
32bf650
Add some range definitions
sonmarcho Feb 25, 2025
36f3533
Improve `progress with` to allow hovering over the theorem name
sonmarcho Feb 25, 2025
15a17a7
Merge remote-tracking branch 'origin/main' into son/lean
sonmarcho Feb 25, 2025
d4ad011
Update the way we compute which functions should be reducible
sonmarcho Feb 25, 2025
1bca2a4
Make a nit
sonmarcho Feb 25, 2025
9b3b634
Fix a naming issue at extraction and add `Box::as_mut`
sonmarcho Feb 25, 2025
c7d7c7f
Remove the splitGoal option of scalar_tac
sonmarcho Feb 25, 2025
fcd5bf0
Make a minor modification of the proofs of the hashmap
sonmarcho Feb 26, 2025
e1e2a13
Use getElem! and List.set instead of List.index and List.update
sonmarcho Feb 27, 2025
9252e81
Use #guard_msgs in Diverge/Elab.lean
sonmarcho Feb 27, 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
12 changes: 9 additions & 3 deletions backends/lean/Aeneas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,17 @@
import Aeneas.Arith
import Aeneas.Bvify
import Aeneas.BvTac
import Aeneas.Diverge
import Aeneas.FSimp
import Aeneas.List
import Aeneas.Std
import Aeneas.Natify
import Aeneas.Progress
import Aeneas.SimpLemmas
import Aeneas.Utils
import Aeneas.Range
import Aeneas.Saturate
import Aeneas.ScalarNF
import Aeneas.ScalarTac
import Aeneas.SimpLemmas
import Aeneas.Std
import Aeneas.Utils
import Aeneas.Termination
import Aeneas.Zify
Loading
Loading