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 #96 from RaitoBezarius/bump-lean
Son HO
2024-03-25
2
-2
/
+2
|
\
|
*
backend(/tests)/lean: 4.6.0-rc1 → 4.6.1
Ryan Lahfa
2024-03-25
2
-2
/
+2
|
/
*
Merge pull request #93 from AeneasVerif/son/examples
Son HO
2024-03-20
45
-711
/
+846
|
\
|
*
Merge remote-tracking branch 'origin/main' into son/examples
Son Ho
2024-03-20
1
-3
/
+7
|
|
\
|
|
/
|
/
|
*
|
Merge pull request #90 from AeneasVerif/son/makefile
Son HO
2024-03-20
2
-9
/
+13
|
\
\
|
*
|
Change the tests target to test
Son Ho
2024-03-11
2
-6
/
+6
|
*
|
Update the Makefile to automatically reformat the code
Son Ho
2024-03-11
1
-3
/
+7
|
|
*
Update the Makefile
Son Ho
2024-03-20
2
-8
/
+8
|
|
*
Update the flake.lock
Son Ho
2024-03-20
1
-15
/
+15
|
|
*
Regenerate the code
Son Ho
2024-03-20
29
-454
/
+431
|
|
*
Improve the generation of pretty name and the micro passes
Son Ho
2024-03-20
8
-30
/
+144
|
|
*
Regenerate the tests
Son Ho
2024-03-19
22
-188
/
+80
|
|
*
Improve the pure micro passes
Son Ho
2024-03-19
2
-8
/
+64
|
|
*
Update the demo
Son Ho
2024-03-19
4
-30
/
+126
|
|
/
|
/
|
*
|
Merge pull request #92 from AeneasVerif/son/globals
Son HO
2024-03-18
18
-462
/
+506
|
\
\
|
*
|
Update the flake.nix and the flake.lock
Son Ho
2024-03-18
2
-367
/
+4
|
*
|
Fix a minor issue
Son Ho
2024-03-18
1
-1
/
+3
|
*
|
Regenerate the test files
Son Ho
2024-03-18
6
-66
/
+297
|
*
|
Update extract_trait_impl
Son Ho
2024-03-18
1
-7
/
+23
|
*
|
Fix the extraction of trait constants
Son Ho
2024-03-18
2
-35
/
+22
|
*
|
Regenerate the constants tests and update Primitives/Base.lean
Son Ho
2024-03-18
4
-55
/
+101
|
*
|
Make good progress on adding generics to global constants
Son Ho
2024-03-18
8
-47
/
+172
|
/
/
*
|
Merge pull request #91 from AeneasVerif/son/hax
Son HO
2024-03-17
16
-101
/
+75
|
\
\
|
|
/
|
/
|
|
*
Update the flake.lock
Son Ho
2024-03-17
1
-21
/
+21
|
*
Fix a minor issue
Son Ho
2024-03-17
1
-1
/
+1
|
*
Make minor updates
Son Ho
2024-03-17
3
-7
/
+14
|
*
Fix a small issue ollowing updates in Charon
Son Ho
2024-03-17
1
-3
/
+8
|
*
Update following changes in Charon
Son Ho
2024-03-17
11
-72
/
+34
|
/
*
Merge pull request #88 from AeneasVerif/son/clashes
Son HO
2024-03-11
37
-703
/
+825
|
\
|
*
Update the flake.lock
Son Ho
2024-03-11
1
-12
/
+12
|
*
Regenerate the test files
Son Ho
2024-03-11
14
-244
/
+227
|
*
Simplify the generated names
Son Ho
2024-03-11
1
-14
/
+25
|
*
Update the generated files
Son Ho
2024-03-11
15
-380
/
+389
|
*
Update tests/Makefile
Son Ho
2024-03-11
1
-1
/
+1
|
*
Update the generation of names
Son Ho
2024-03-11
7
-39
/
+57
|
*
Update a builtin name
Son Ho
2024-03-11
1
-1
/
+1
|
*
Update the builtin name patterns
Son Ho
2024-03-10
1
-23
/
+66
|
*
Update the name generation and add CLI to print external pat names
Son Ho
2024-03-10
7
-48
/
+106
|
/
*
Merge pull request #85 from AeneasVerif/son/fix_loops3
Son HO
2024-03-09
28
-350
/
+1185
|
\
|
*
Update the flake.lock
Son Ho
2024-03-09
1
-24
/
+24
|
*
Regenerate the test files
Son Ho
2024-03-09
10
-0
/
+420
|
*
Fix an issue with the divergent encoding
Son Ho
2024-03-09
1
-3
/
+27
|
*
Fix some issues
Son Ho
2024-03-08
2
-9
/
+10
|
*
Add some comments
Son Ho
2024-03-08
2
-9
/
+12
|
*
Fix an issue in PureMicroPasses.filter_loop_inputs
Son Ho
2024-03-08
1
-13
/
+43
|
*
Simplify the contexts before symbolically evaluating loops
Son Ho
2024-03-08
4
-2
/
+137
|
*
Fix a last issue
Son Ho
2024-03-08
2
-51
/
+110
|
*
Fix an issue with the loops
Son Ho
2024-03-08
1
-1
/
+7
|
*
Make progress on fixing the loops
Son Ho
2024-03-08
8
-31
/
+70
|
*
Fix a small issue with the loops
Son Ho
2024-03-08
2
-7
/
+19
[next]