summaryrefslogtreecommitdiff
path: root/tests/lean (unfollow)
Commit message (Collapse)AuthorFilesLines
2024-06-28Update charonNadrieril5-7/+7
2024-06-25Bump Lean to v4.9.0rc3 (#261)Son HO3-5/+2
2024-06-24Update charonNadrieril3-3/+3
2024-06-22Do some cleanup in the Lean backend (#257)Son HO1-56/+20
2024-06-22Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO1-76/+24
* Fix an issue in a proof of the hashmap * Improve scalar_decr_tac * Improve the error message of scalar_tac and add the missing Termination.lean
2024-06-21Add some proofs for the Lean backend (#255)Son HO3-67/+941
* Make progress on the proofs of the hashmap * Make a minor modification to the hashmap * Make progress on the hashmap * Make progress on the proofs * Make progress on the proofs * Make progress on the proof of the hashmap * Progress on the proofs of the hashmap * Update a proof * Update the Charon pin * Make minor modifications to the hashmap * Regenerate the tests * Regenerate the hashmap * Add lemmas to the Lean backend * Make progress on the proofs of the hashmap * Make a minor fix * Finish the proof about the hashmap * Update scalar_tac * Make a minor modification in the hashmap * Update the proofs of the hashmap --------- Co-authored-by: Son Ho <sonho@Sons-MacBook-Pro.local> Co-authored-by: Son Ho <sonho@Sons-MBP.lan>
2024-06-18Support for renaming using the rename attribute in charon (#239)Escherichia1-0/+92
* 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-06-18Bump charonNadrieril4-15/+15
2024-06-17Regenerate the testsSon Ho5-6/+6
2024-06-17Update charonNadrieril5-6/+6
2024-06-17Regenerate the testsSon Ho25-0/+75
2024-06-17Update the testsSon Ho6-4/+31
2024-06-17Update Hashmap/Properties.leanSon Ho1-36/+34
2024-06-17Update the code of the hashmapSon Ho3-130/+135
2024-06-17Update the Lean dependenciesSon Ho1-4/+4
2024-06-14Update the testsSon Ho2-4/+4
2024-06-13Update the testsSon Ho3-29/+29
2024-06-12Update the code extraction and regenerate the testsSon Ho1-2/+2
2024-06-12Revert "Regenerate the tests"Son Ho12-333/+338
This reverts commit cd5542fc82edee11181a43e3a342a2567c929e7e.
2024-06-12Revert "Fix some mistakes"Son Ho3-15/+15
This reverts commit f05a0faf14fdd558039da52624d57028eb64f9fd.
2024-06-12Fix some mistakesSon Ho3-15/+15
2024-06-12Regenerate the testsSon Ho12-338/+333
2024-06-11Deactivate the use of tuple projectors in the Lean backendSon Ho1-2/+4
2024-06-11Update the tests for tuplesSon Ho1-7/+24
2024-06-05Regenerate the Coq and Lean betreesSon Ho1-89/+202
2024-06-05Update charonNadrieril9-117/+117
2024-06-03Add a testSon Ho1-34/+39
2024-05-31Regenerate testsAymeric Fromherz2-2/+2
2024-05-31Regenerate test outputAymeric Fromherz5-36/+719
2024-05-30Implement two phases of loops join + collapseAymeric Fromherz5-719/+36
2024-05-28Reactivate the infinite-loop.rs testSon Ho1-0/+25
2024-05-28tests: Rename hashmap_utils -> utilsNadrieril3-11/+10
2024-05-28Add some testsNadrieril2-0/+51
2024-05-28tests: Rename betree_main -> betreeNadrieril8-75/+74
2024-05-27tests: Merge the hashmap test filesNadrieril13-575/+81
2024-05-27runner: Support negative testsNadrieril1-0/+6
2024-05-24Update output filesNadrieril8-177/+177
2024-05-24Update test outputsNadrieril15-391/+391
2024-05-24Tweak a pathNadrieril15-391/+391
2024-05-23Regenerate Lean files for betreeAymeric Fromherz1-0/+4
2024-05-23Regenerate Lean files for betree following extraction changesAymeric Fromherz2-47/+46
2024-05-23Bump charon versionNadrieril5-7/+7
2024-04-30Update charonNadrieril2-1/+2
2024-04-25Regenerate and fix the testsSon Ho1-9/+9
2024-04-25Update the tests for ExternalSon Ho6-83/+66
2024-04-24Fix a couple of testsZyad Hassan4-13/+4
2024-04-24Update testsZyad Hassan2-12/+0
2024-04-24compiler: map `core::mem::swap` to the pure swapRyan Lahfa1-6/+0
In the pure functional model, `swap` is mostly about borrow checking and should simplify to the pure swap in our backends. Other backends than Lean are not done in this commit. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
2024-04-18Ensure we regenerate files properly in CINadrieril2-2/+0
Files that weren't regenerated were marked as not automatically-generated.
2024-04-17Bump charonNadrieril1-159/+56