summaryrefslogtreecommitdiff
path: root/tests (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04WIPJonathan Protzenko6-40/+206
2023-06-04Fix runaway indentationJonathan Protzenko1-451/+440
2023-06-04Fill out more of the primitives file, attempt at type classes for scalar_castJonathan Protzenko2-4/+28
2023-06-04Remove last sorry in PrimitivesJonathan Protzenko1-4/+2
2023-06-04Fill out Primitives.leanJonathan Protzenko2-10/+110
2023-06-04Don't need extra variables for the decreases clausesJonathan Protzenko1-11/+15
2023-06-04WIP printing proper clausesJonathan Protzenko1-35/+49
2023-06-04Fix some printing bits, proper syntax for terminates and decreases clausesJonathan Protzenko2-446/+481
2023-06-04WIP lots of stuffJonathan Protzenko4-24/+73
2023-06-04Fixup one primitive that is not assumed to be monadicJonathan Protzenko1-4/+4
2023-06-04Fix a syntax errorJonathan Protzenko1-10/+5
2023-06-04Custom syntax support for structures in LeanJonathan Protzenko1-22/+71
2023-06-04More cosmetic improvementsJonathan Protzenko2-89/+85
2023-06-04Fix a couple bugs here and there, improve Lean code-gen, still WIPJonathan Protzenko2-266/+310
2023-06-04New directory structure and corresponding extraction, + misc fixes, for LeanJonathan Protzenko8-132/+138
2023-06-04Write a tactic to discharge integer literal proof obligationsJonathan Protzenko2-8/+27
2023-06-04Add a sample test to illustrate potential project structureJonathan Protzenko9-0/+751
2023-06-04Initial Lean backend, WIPJonathan Protzenko1-3/+4
2023-02-03Do not unfold the monadic lets for the generated F* codeSon Ho15-3632/+1667
2023-02-03Update the hashmap and regenerateSon Ho9-62/+37
2023-02-03Improve the pretty names generation for loopsSon Ho6-47/+47
2023-02-03Make modifications to the MakefilesSon Ho2-6/+18
2023-02-03Implement a pass to filter the unused input arguments in the loop functionsSon Ho4-31/+22
2023-02-03Fix an issue with the names of the loop decreases clausesSon Ho10-142/+149
2023-02-03Improve the order of the loop input parametersSon Ho13-62/+62
2023-02-03Improve the heuristic to find pretty names for the variables in the loopsSon Ho9-377/+387
2023-02-03Improve PureMicroPasses.filter_useless and regenerate the betree codeSon Ho3-85/+56
2023-02-03Regenerate the hashmap code and update the proofsSon Ho10-380/+681
2023-02-03Fix some issues with the values given back by loop backward translationsSon Ho4-0/+160
2023-02-03Fix an issue with the translation of loops::clearSon Ho2-16/+6
2023-02-03Add more loop examples and fix issuesSon Ho4-0/+312
2023-02-03Implement support for nested borrows in loops, and add loop testsSon Ho4-18/+820
2023-02-03Regenerate the testsSon Ho4-0/+394
2023-02-03Improve the loops' numberingSon Ho2-19/+18
2023-02-03Make another loop example workSon Ho4-0/+44
2023-02-03Regenerate the filesSon Ho19-863/+245
2023-02-03Make minor modifications and generate code for loopsSon Ho6-0/+176
2022-11-16Add a nix derivation for the Coq proofsSon Ho2-2/+7
2022-11-16Do not introduce match on the fuel for non-recursive functionsSon Ho3-667/+477
2022-11-16Automatically generate the Makefile and _CoqProject files in the tests subdir...Son Ho16-15/+51
2022-11-16Add the aeneas-verify-fstar derivationSon Ho5-5/+10
2022-11-16Generate record field projectors for CoqSon Ho10-695/+612
2022-11-16Change the name of the generated Coq modulesSon Ho11-42/+42
2022-11-16Improve formattingSon Ho17-583/+587
2022-11-16Remove some comments from Hashmap.Properties.fstSon Ho1-60/+0
2022-11-16Make minor modifications to the extractionSon Ho9-58/+70
2022-11-14Extract the Polonius examples in CoqSon Ho8-1/+2105
2022-11-14Generate Coq code for `hashmap` and `hashmap_on_disk`Son Ho11-0/+2264
2022-11-14Add a `-use-fuel` optionSon Ho7-3/+56
2022-11-14Regenerate the files and fix the proofsSon Ho21-1088/+1159
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 22:39:43 +0000