index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
*
Merge pull request #242 from AeneasVerif/son/scalars2
Son HO
2024-06-13
9
-114
/
+150
|
\
|
*
Fix more issues with the scalar notations
Son Ho
2024-06-13
1
-15
/
+29
|
*
Fix more issues
Son Ho
2024-06-13
3
-16
/
+22
|
*
Fix a proof
Son Ho
2024-06-13
1
-1
/
+1
|
*
Merge branch 'main' into son/scalars2
Son HO
2024-06-13
1
-1
/
+1
|
|
\
|
|
/
|
/
|
*
|
Merge pull request #238 from RaitoBezarius/prop-has-imp-sort
Son HO
2024-06-13
1
-1
/
+1
|
\
\
|
*
\
Merge branch 'main' into prop-has-imp-sort
Son HO
2024-06-12
5
-45
/
+118
|
|
\
\
|
|
/
/
|
/
|
|
|
*
|
feat: `PropHasImp` can have `Sort u` as premisses
Ryan Lahfa
2024-06-11
1
-1
/
+1
|
|
*
Merge branch 'main' into son/scalars2
Son HO
2024-06-12
0
-0
/
+0
|
|
|
\
|
|
_
|
/
|
/
|
|
*
|
|
Merge pull request #241 from AeneasVerif/son/tactics
Son HO
2024-06-12
5
-45
/
+118
|
\
\
\
|
|
/
/
|
/
|
|
|
|
*
Add an example
Son Ho
2024-06-12
1
-0
/
+3
|
|
*
Update the code extraction and regenerate the tests
Son Ho
2024-06-12
3
-9
/
+15
|
|
*
Update the scalar notations in Lean
Son Ho
2024-06-12
3
-102
/
+109
|
|
/
|
*
Revert "Update the scalar notation for the Lean backend"
Son Ho
2024-06-12
2
-26
/
+26
|
*
Revert "Regenerate the tests"
Son Ho
2024-06-12
12
-333
/
+338
|
*
Revert "Update CoreConvertNum.lean"
Son Ho
2024-06-12
1
-22
/
+22
|
*
Revert "Fix some mistakes"
Son Ho
2024-06-12
4
-17
/
+15
|
*
Fix some mistakes
Son Ho
2024-06-12
4
-15
/
+17
|
*
Update CoreConvertNum.lean
Son Ho
2024-06-12
1
-22
/
+22
|
*
Regenerate the tests
Son Ho
2024-06-12
12
-338
/
+333
|
*
Update the scalar notation for the Lean backend
Son Ho
2024-06-12
2
-26
/
+26
|
*
Deactivate the coercion from Nat to Scalar
Son Ho
2024-06-12
2
-0
/
+17
|
*
Slightly simplify the progress tactic
Son Ho
2024-06-12
1
-8
/
+4
|
*
Add wrappers around the rewriter
Son Ho
2024-06-12
1
-0
/
+61
|
*
Add the Simp.Config to the simp wrappers
Son Ho
2024-06-12
4
-37
/
+36
|
/
*
Merge pull request #237 from AeneasVerif/son/tuples
Son HO
2024-06-11
6
-28
/
+96
|
\
|
*
Deactivate the use of tuple projectors in the Lean backend
Son Ho
2024-06-11
3
-7
/
+12
|
*
Update the tests for tuples
Son Ho
2024-06-11
4
-22
/
+85
|
/
*
Merge pull request #232 from Nadrieril/type-alias
Guillaume Boisseau
2024-06-06
7
-12
/
+56
|
\
|
*
Filter out type aliases
Nadrieril
2024-06-06
7
-12
/
+56
|
/
*
Merge pull request #233 from AeneasVerif/son/borrow-check
Son HO
2024-06-06
45
-759
/
+1500
|
\
|
*
Regenerate the Coq and Lean betrees
Son Ho
2024-06-05
2
-178
/
+423
|
*
Fix a minor issue
Son Ho
2024-06-05
1
-0
/
+1
|
*
Update the F* betree
Son Ho
2024-06-05
3
-144
/
+280
|
*
Fix a minor issue
Son Ho
2024-06-05
1
-0
/
+1
|
*
Update the betree
Son Ho
2024-06-05
1
-99
/
+98
|
*
Regenerate some tests
Son Ho
2024-06-05
1
-14
/
+2
|
*
Add some negative tests for the borrow checker
Son Ho
2024-06-05
2
-0
/
+105
|
*
Update an error message
Son Ho
2024-06-05
1
-6
/
+10
|
*
Add more tests
Son Ho
2024-06-05
5
-0
/
+79
|
*
Update the test runner
Son Ho
2024-06-05
1
-1
/
+4
|
*
Relax more checks for borrow-checking
Son Ho
2024-06-05
1
-1
/
+2
|
*
Relax some constraints in the symbolic execution when borrow-checking
Son Ho
2024-06-05
4
-16
/
+54
|
*
Update the test runner to allow the syntax [!lean] and [borrow-check]
Son Ho
2024-06-05
14
-34
/
+65
|
*
Implement a BorrowCheck.borrow_check_crate
Son Ho
2024-06-05
6
-10
/
+54
|
*
Add an option to run Aeneas as a borrow checker
Son Ho
2024-06-05
10
-276
/
+342
|
/
*
Merge pull request #227 from AeneasVerif/son/clean-synthesis
Son HO
2024-06-05
15
-423
/
+345
|
\
|
*
Merge branch 'main' into son/clean-synthesis
Son Ho
2024-06-05
62
-1437
/
+2425
|
|
\
|
|
/
|
/
|
*
|
Merge pull request #231 from Nadrieril/bump-hax
Guillaume Boisseau
2024-06-05
29
-291
/
+282
|
\
\
|
*
|
Update charon
Nadrieril
2024-06-05
29
-291
/
+282
|
/
/
[next]