summaryrefslogtreecommitdiff
path: root/tests/fstar/rename_attribute/Primitives.fst (unfollow)
Commit message (Collapse)AuthorFilesLines
2024-06-18Support for renaming using the rename attribute in charon (#239)Escherichia1-0/+0
* support for renaming using the rename attribute in charon * support for global decl * add support for renaming field * applied suggested changes and began adding support for variant * finished support for renaming variant * applied suggested changes * add tests * fixed variant and field renaming * update charon-pin * update flake.lock * Update the charon pin * Fix an issue with renaming trait method implementations * Fix an issue with the renaming of trait implementations * Fix an issue when renaming enumerations * Update the Charon pin * Fix the F* tests * Fix an issue with the spans for the loops * Fix the tests * Update a comment * Use fuel in the coq tests * Generate the template decreases clauses by default --------- Co-authored-by: Escherichia <escherichia@charlotte> Co-authored-by: Son Ho <hosonmarc@gmail.com>
2024-04-25Update the backend and ExtractBuiltin.mlSon Ho1-0/+6
2024-04-25Update the tests for ExternalSon Ho1-0/+75
2024-04-04Rename Result.ret as Result.ok in the backendsSon Ho1-28/+28
2024-03-08Update the Makefile and remove the split files for F*Son Ho1-0/+0
2023-12-22Fix minor issuesSon Ho1-1/+20
2023-12-22Fix the models for core::mem::replaceSon Ho1-1/+1
2023-12-22Update the library for F*Son Ho1-83/+28
2023-12-13Update the extraction to handle casts between integers/boolsSon Ho1-0/+4
2023-11-29Add support for more bitwise operations and update the extractionSon Ho1-8/+159
2023-11-21Update more namesSon Ho1-16/+16
2023-11-21Update the standard librariesSon Ho1-28/+28
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 Ho1-14/+18
2022-11-11Move the fstar files to the new backends directorySon Ho1-0/+0
2022-11-11Make the Nix build workSon Ho1-0/+0
2022-11-10Make a minor cleanupSon Ho1-3/+4
2022-10-27Reorganize a bit the projectSon Ho1-0/+0
2022-09-22Update fstar/Primitives.fstSon HO1-1/+1
2022-06-30Traduct globals body separately (WIP)Sidney Congard1-0/+3
2022-05-15Add a pass to cleanup the deconstructed ADTs and fix a small issueSon Ho1-1/+1
2022-05-15Treat integer casts in a general mannerSon Ho1-0/+4
2022-02-11Make good progress on the proofs of hashmapSon Ho1-14/+14
2022-02-10Make progress on the proofs of HashMapSon Ho1-4/+4
2022-02-10Update Primitives.fstSon Ho1-1/+10
2022-02-09Add definitions to Primitives.fst and start on improving/fixing theSon Ho1-0/+49
generated F* file
2022-02-07Make more minor modificationsSon Ho1-1/+3
2022-02-07Make minor modifications to Primitives.fstSon Ho1-1/+2
2022-02-04Work on decomposition of monadic let-bindings for F*Son Ho1-0/+10
2022-02-03Make mor modificationsSon Ho1-0/+3
2022-02-03Make minor modificationsSon Ho1-1/+1
2022-02-03Rename Assumed.fst to Primitives.fst and make progress on thatSon Ho1-0/+205
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-15 04:20:16 +0000