index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Collapse
)
Author
Age
Files
Lines
*
Prove hash_map_insert_fwd_back_spec
Son Ho
2023-06-04
1
-1
/
+59
|
*
Make progress on the proofs of the hash map
Son Ho
2023-06-04
6
-6
/
+799
|
*
Make good progress on the proofs of the hashmap in HOL4
Son Ho
2023-06-04
7
-64
/
+841
|
*
Start working on the proofs of the hash map
Son Ho
2023-06-04
1
-0
/
+543
|
*
Make the theorems used by the progress tactic persistent
Son Ho
2023-06-04
8
-186
/
+285
|
*
Update tests/Makefile
Son Ho
2023-06-04
1
-1
/
+1
|
*
Add the generated HOL4 files
Son Ho
2023-06-04
44
-4
/
+13223
|
*
Commit saveThmsLib.sig
Son Ho
2023-06-04
1
-0
/
+46
|
*
Improve the parsing for divDefLib
Son Ho
2023-06-04
1
-1
/
+91
|
*
Fix some minor issues
Son Ho
2023-06-04
2
-41
/
+49
|
*
Make progress on the HOL4 backend
Son Ho
2023-06-04
4
-81
/
+378
|
*
Make progress on extracting the HOL4 files
Son Ho
2023-06-04
5
-18
/
+319
|
*
Make the unfolding theorems collection from evalLib persistent
Son Ho
2023-06-04
10
-251
/
+235
|
*
Make minor modifications
Son Ho
2023-06-04
1
-5
/
+11
|
*
Start working on saveThmsLib
Son Ho
2023-06-04
1
-0
/
+190
|
*
Commit evalLib
Son Ho
2023-06-04
2
-0
/
+170
|
*
Update the definitions of mk_vec and vec_insert_back
Son Ho
2023-06-04
2
-21
/
+71
|
*
Cleanup a bit the HOL4 backend and implement eval_conv
Son Ho
2023-06-04
14
-56
/
+238
|
*
Make good progress on generating code for HOL4
Son Ho
2023-06-04
22
-719
/
+2101
|
*
Make a minor modification
Son Ho
2023-06-04
1
-3
/
+5
|
*
Introduce fix_exec, an executable version of fix
Son Ho
2023-06-04
5
-13
/
+90
|
*
Make minor modifications
Son Ho
2023-06-04
2
-8
/
+35
|
*
Make minor modifications to divDefLib
Son Ho
2023-06-04
2
-60
/
+65
|
*
Fix minor issues
Son Ho
2023-06-04
3
-12
/
+508
|
*
Fix minor issues
Son Ho
2023-06-04
2
-6
/
+17
|
*
Do more cleanup
Son Ho
2023-06-04
2
-1222
/
+0
|
*
Cleanup the files of the HOL4 backend
Son Ho
2023-06-04
16
-3080
/
+2938
|
*
Reimplement DefineDiv with the new fixed point operator
Son Ho
2023-06-04
3
-2
/
+1249
|
*
Write some tests for divDefProto2Script.sml
Son Ho
2023-06-04
2
-84
/
+214
|
*
Update divDefProto2Script.sml
Son Ho
2023-06-04
1
-55
/
+16
|
*
Write a prototype definition using the general fixed-point combinator
Son Ho
2023-06-04
2
-510
/
+417
|
*
Start working on more general fixed-point combinators
Son Ho
2023-06-04
3
-0
/
+904
|
*
Cleanup divDefProtoScript
Son Ho
2023-06-04
2
-523
/
+12
|
*
Improve the performance of dependent rewrites by using nets
Son Ho
2023-06-04
2
-58
/
+120
|
*
Make more proofs about the hashmap proto
Son Ho
2023-06-04
5
-4
/
+225
|
*
Update the hashmap proofs and fix some tactics
Son Ho
2023-06-04
5
-46
/
+300
|
*
Start working on a version of divDefLib which uses fixed point combinators
Son Ho
2023-06-04
2
-0
/
+983
|
*
Cleanup a bit and reorganize
Son Ho
2023-06-04
6
-90
/
+577
|
*
Make minor modifications
Son Ho
2023-06-04
1
-0
/
+26
|
*
Fix minor bugs in divDefLib.sml
Son Ho
2023-06-04
1
-28
/
+134
|
*
Fix a small issue
Son Ho
2023-06-04
1
-3
/
+32
|
*
Cleanup a bit
Son Ho
2023-06-04
1
-220
/
+136
|
*
Finish a first working version of divDefLib.sml
Son Ho
2023-06-04
1
-29
/
+347
|
*
Start working on divDefLib for diverging definitions
Son Ho
2023-06-04
9
-111
/
+995
|
*
Add a .sig file
Son Ho
2023-06-04
1
-0
/
+202
|
*
Reorganize the HOL4 files and fix some issues with the arithmetic proofs
Son Ho
2023-06-04
4
-763
/
+568
|
*
Make progress on the standard library for HOL4
Son Ho
2023-06-04
9
-91
/
+1041
|
*
Cleanup a bit
Son Ho
2023-06-04
3
-191
/
+17
|
*
Make progress on primitivesScript
Son Ho
2023-06-04
6
-211
/
+333
|
*
Make more progress on primitivesScript.sml
Son Ho
2023-06-04
2
-209
/
+191
|
[next]