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
...
|
*
|
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
|
/
/
|
*
backends/lean: introduce `HasIntPred` automation
Ryan Lahfa
2024-06-12
2
-8
/
+38
|
/
*
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
|
/
/
*
|
Propagated changes to statement from Charon (#223)
Escherichia
2024-06-04
4
-5
/
+6
*
|
Merge pull request #228 from AeneasVerif/son/loops2
Son HO
2024-06-04
31
-1149
/
+2143
|
\
\
|
*
\
Merge branch 'main' into son/loops2
Son Ho
2024-06-04
188
-5984
/
+2764
|
|
\
\
|
|
/
/
|
/
|
|
*
|
|
Merge pull request #230 from W95Psp/follow-up-charon-pr-209
Guillaume Boisseau
2024-06-04
7
-6
/
+12
|
\
\
\
|
*
|
|
Fix the CI pin check
Nadrieril
2024-06-04
1
-0
/
+2
|
*
|
|
Update charon pin
Nadrieril
2024-06-04
2
-4
/
+4
|
*
|
|
feat: basic handling for `RValue::Len`, following AeneasVerif/charon#209
Lucas Franceschino
2024-06-03
4
-2
/
+6
|
/
/
/
|
*
|
Improve collapse_ctx
Son Ho
2024-06-04
1
-1
/
+42
|
*
|
Do more cleanup
Son Ho
2024-06-04
1
-40
/
+44
|
*
|
Factor out the code in collapse_ctx
Son Ho
2024-06-04
2
-153
/
+56
|
*
|
Start factoring out the code of reduce_ctx and collapse_ctx
Son Ho
2024-06-04
1
-91
/
+162
|
*
|
Improve merge_abstractions by splitting the markers before merging
Son Ho
2024-06-04
1
-0
/
+75
|
*
|
Cleanup merge_abstractions
Son Ho
2024-06-04
1
-96
/
+183
|
*
|
Add a test
Son Ho
2024-06-03
4
-103
/
+123
|
*
|
Fix an issue with the type of the values given back by loops
Son Ho
2024-06-03
3
-157
/
+237
|
*
|
Fix a bug when composing the continuations in eval_statement
Son Ho
2024-06-03
4
-122
/
+131
|
*
|
Change the order in which we merge abstractions
Son Ho
2024-06-03
5
-105
/
+99
|
*
|
Cleanup a bit
Son Ho
2024-06-03
3
-44
/
+53
|
*
|
Factor out some code and update some comments
Son Ho
2024-06-03
4
-166
/
+173
[prev]
[next]