summaryrefslogtreecommitdiff
path: root/tests/coq (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Update charonNadrieril2024-06-285-7/+7
|
* Update charonNadrieril2024-06-243-3/+3
|
* Add some proofs for the Lean backend (#255)Son HO2024-06-212-20/+49
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * 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>
* Support for renaming using the rename attribute in charon (#239)Escherichia2024-06-182-0/+1084
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * 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>
* Bump charonNadrieril2024-06-184-15/+15
|
* Merge branch 'main' into son/cleanupSon HO2024-06-175-6/+6
|\
| * Update charonNadrieril2024-06-175-6/+6
| |
* | Update the code of the hashmapSon Ho2024-06-173-136/+136
|/
* Update the tests for tuplesSon Ho2024-06-111-7/+26
|
* Regenerate the Coq and Lean betreesSon Ho2024-06-051-89/+221
|
* Update charonNadrieril2024-06-059-86/+86
|
* Merge branch 'main' into son/loops2Son Ho2024-06-0432-2144/+586
|\
| * Fix an issue with some names being ignored when generating unique variable namesSon Ho2024-05-281-2/+2
| |
| * Reactivate the infinite-loop.rs testSon Ho2024-05-281-0/+27
| |
| * tests: Rename hashmap_utils -> utilsNadrieril2024-05-283-11/+10
| |
| * Add some testsNadrieril2024-05-281-0/+54
| |
| * tests: Rename betree_main -> betreeNadrieril2024-05-287-84/+84
| |
| * tests: Merge the hashmap test filesNadrieril2024-05-2713-1734/+96
| |
| * Rename some subdirectories for consistencyNadrieril2024-05-249-0/+0
| |
| * Update output filesNadrieril2024-05-248-177/+177
| |
| * Update test outputsNadrieril2024-05-2415-391/+391
| |
* | Add a testSon Ho2024-06-031-34/+39
| |
* | Regenerate testsAymeric Fromherz2024-05-319-31/+31
| |
* | Regenerate test outputAymeric Fromherz2024-05-315-36/+908
| |
* | Implement two phases of loops join + collapseAymeric Fromherz2024-05-305-908/+36
|/
* Tweak a pathNadrieril2024-05-2415-391/+391
|
* Bump charon versionNadrieril2024-05-235-7/+7
|
* Update charonNadrieril2024-04-301-1/+1
|
* Regenerate and fix the testsSon Ho2024-04-259-19/+60
|
* Merge branch 'main' into core-option-unwrapSon Ho2024-04-2513-85/+584
|\
| * Regenerate the Primitives filesSon Ho2024-04-256-0/+450
| |
| * Update the tests for ExternalSon Ho2024-04-257-92/+134
| |
* | Update testsZyad Hassan2024-04-242-14/+0
|/
* Ensure we regenerate files properly in CINadrieril2024-04-186-6/+0
| | | | | Files that weren't regenerated were marked as not automatically-generated.
* Bump charonNadrieril2024-04-171-159/+56
|
* Fix a Coq fileSon Ho2024-04-111-1/+1
|
* Regenerate the test filesSon Ho2024-04-0420-535/+501
|
* Regenerate the test filesSon Ho2024-04-042-12/+12
|
* Regenerate the test filesSon Ho2024-04-0413-99/+104
|
* Regenerate the codeSon Ho2024-03-209-126/+119
|
* Regenerate the testsSon Ho2024-03-199-64/+26
|
* Update the demoSon Ho2024-03-191-10/+38
|
* Regenerate the test filesSon Ho2024-03-182-22/+114
|
* Regenerate the constants tests and update Primitives/Base.leanSon Ho2024-03-181-18/+35
|
* Regenerate the test filesSon Ho2024-03-113-83/+78
|
* Update the generated filesSon Ho2024-03-115-128/+134
|
* Regenerate the test filesSon Ho2024-03-092-0/+133
|
* Add some missing filesSon Ho2024-02-092-0/+30
|
* Add some demo filesSon Ho2024-02-092-0/+1066
|
* Rename and regenerate some filesSon Ho2024-02-025-119/+119
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 16:03:22 +0000