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
...
|
*
|
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
|
*
Fix some issues with the loops
Son Ho
2024-03-08
3
-140
/
+206
|
*
Do not fail in end_abstraction_aux if the abs disappeared
Son Ho
2024-03-08
2
-64
/
+80
|
*
Add logging information
Son Ho
2024-03-08
3
-0
/
+24
|
*
Update Print.ml
Son Ho
2024-03-08
1
-8
/
+8
|
/
*
Merge pull request #83 from AeneasVerif/son/backs
Son HO
2024-03-08
76
-18929
/
+705
|
\
|
*
Update the workers
Son Ho
2024-03-08
1
-1
/
+0
|
*
Update the flake.nix
Son Ho
2024-03-08
1
-14
/
+5
|
*
Remove the split test files for F*
Son Ho
2024-03-08
55
-16239
/
+0
|
*
Update the Makefile and remove the split files for F*
Son Ho
2024-03-08
5
-952
/
+4
|
*
Make progress on propagating the changes
Son Ho
2024-03-08
14
-949
/
+259
|
*
Remove the option to split fwd/back functions and update SymbolicToPure
Son Ho
2024-03-08
5
-776
/
+439
|
/
*
Merge pull request #82 from AeneasVerif/son/switch
Son HO
2024-03-08
20
-173
/
+352
|
\
|
*
Update the code generated for tuple projectors
Son Ho
2024-03-08
4
-19
/
+48
|
*
Fix tuple indexing for Lean backend
Zyad Hassan
2024-03-08
3
-6
/
+35
|
*
Update the generation of constant bodies for Lean
Son Ho
2024-03-08
6
-28
/
+26
|
*
Update the tuples syntax
Son Ho
2024-03-08
1
-1
/
+3
[prev]
[next]