summaryrefslogtreecommitdiff
path: root/backends/fstar (unfollow)
Commit message (Expand)AuthorFilesLines
2023-11-09Update the failing proofsSon Ho1-1/+17
2023-10-27Regenerate some of the F* test filesSon Ho1-2/+19
2023-10-26Update Primitives.fstSon Ho1-48/+318
2023-10-22Add more support for numeric operations, xor, rotateJonathan Protzenko1-1/+22
2023-10-13Update Primitives.fstSon Ho1-0/+3
2023-09-07Fix some issuesSon Ho1-10/+37
2023-08-04Fix issues with the extraction and extend the primitive libraries for Coq and F*Son Ho1-0/+75
2023-02-03Do not unfold the monadic lets for the generated F* codeSon Ho1-1/+3
2022-11-16Make minor modifications to the extractionSon Ho1-10/+14
2022-11-14Add a `-use-fuel` optionSon Ho1-0/+3
2022-11-14Make [Result::Failure] type an [Error] parameterSon Ho2-14/+65
2022-11-11Move the fstar files to the new backends directorySon Ho1-0/+287