summaryrefslogtreecommitdiff
path: root/tests/lean/Hashmap (unfollow)
Commit message (Collapse)AuthorFilesLines
2024-06-25Bump Lean to v4.9.0rc3 (#261)Son HO1-3/+0
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-18Bump charonNadrieril1-1/+1
2024-06-17Regenerate the testsSon Ho4-0/+12
2024-06-17Update the testsSon Ho2-2/+9
2024-06-17Update Hashmap/Properties.leanSon Ho1-36/+34
2024-06-17Update the code of the hashmapSon Ho3-130/+135
2024-06-13Update the testsSon Ho1-15/+15
2024-06-12Revert "Regenerate the tests"Son Ho1-31/+31
This reverts commit cd5542fc82edee11181a43e3a342a2567c929e7e.
2024-06-12Regenerate the testsSon Ho1-31/+31
2024-06-05Update charonNadrieril1-18/+18
2024-05-31Regenerate testsAymeric Fromherz1-1/+1
2024-05-31Regenerate test outputAymeric Fromherz1-8/+140
2024-05-30Implement two phases of loops join + collapseAymeric Fromherz1-140/+8
2024-05-28tests: Rename hashmap_utils -> utilsNadrieril3-11/+10
2024-05-27tests: Merge the hashmap test filesNadrieril6-32/+95
2024-05-24Update test outputsNadrieril2-32/+32
2024-05-24Tweak a pathNadrieril2-32/+32
2024-04-11Update some Lean proofsSon Ho1-7/+7
2024-04-05Update the lean toolchain and fix the proofsSon Ho1-6/+14
2024-04-04Regenerate the test filesSon Ho1-31/+31
2024-04-04Regenerate the test filesSon Ho1-6/+6
2024-04-04Regenerate the test filesSon Ho1-8/+8
2024-03-20Regenerate the codeSon Ho1-17/+12
2024-03-19Regenerate the testsSon Ho1-3/+1
2024-03-08Regenerate the test filesSon Ho1-6/+6
2023-12-23Regenerate the filesSon Ho1-6/+3
2023-12-23Update the proof of the hashmap in LeanSon Ho1-100/+44
2023-12-22Regenerate the test files and add the fstar-split testsSon Ho1-336/+246
2023-11-24Regenerate the filesSon Ho1-21/+19
2023-11-21Regenerate the filesSon Ho2-40/+80
2023-11-21Regenerate most of the test filesSon Ho1-66/+64
2023-11-09Update the failing proofsSon Ho1-5/+6
2023-10-25Regenerate the hashmap filesSon Ho2-86/+133
2023-09-14Fix the hashmap proofs in LeanSon Ho1-7/+2
2023-09-13Make minor modificationsSon Ho1-5/+3
2023-09-07Regenerate the test files and fix a proofSon Ho1-5/+1
2023-08-09Update the nix flake and regenerate the codeSon Ho1-1/+1
2023-08-04Fix a heart beat issue in a Lean proofSon Ho1-0/+4
2023-08-04Make minor modificationsSon Ho1-2/+2
2023-08-03Make a minor formatting modification for LeanSon Ho2-0/+2
2023-07-31Make minor modificationsSon Ho1-0/+9
2023-07-26Make minor modificationsSon Ho1-3/+2
2023-07-26Make a minor modification to a hashmap proofSon Ho1-5/+9
2023-07-26Update some of the Vec function specsSon Ho1-16/+19
2023-07-26Update the syntax of the progress tacticSon Ho1-86/+85
2023-07-26Fix a proof for the hashmapSon Ho1-5/+12
2023-07-25Make progress on the proofs of the hashmapSon Ho1-18/+40
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-08 23:33:31 +0000