summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Update charonNadrieril2024-06-2411-13/+13
|
* Do some cleanup in the Lean backend (#257)Son HO2024-06-228-78/+89
|
* Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO2024-06-228-126/+179
| | | | | | | * 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
* Add some proofs for the Lean backend (#255)Son HO2024-06-2118-165/+1163
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * 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>
* Merge pull request #254 from Nadrieril/declarationgroup-mixedGuillaume Boisseau2024-06-218-10/+19
|\
| * Update charonNadrieril2024-06-218-10/+19
|/
* Merge pull request #253 from Nadrieril/merge-preds-into-paramsGuillaume Boisseau2024-06-2110-77/+67
|\
| * `predicates` got merged into `generic_params`Nadrieril2024-06-2110-77/+67
|/
* Support for renaming using the rename attribute in charon (#239)Escherichia2024-06-1827-301/+2797
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * 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>
* Merge pull request #251 from Nadrieril/bump-charon2Guillaume Boisseau2024-06-1822-89/+73
|\
| * Revert "Switch to GitHub CI runners" againNadrieril2024-06-181-12/+4
| | | | | | | | This was botched by a confusing merge in https://github.com/AeneasVerif/aeneas/pull/246
| * Bump charonNadrieril2024-06-1818-64/+64
| |
| * Tiny dedupNadrieril2024-06-183-13/+5
|/
* Merge pull request #246 from AeneasVerif/son/cleanupSon HO2024-06-1842-508/+694
|\ | | | | Do some cleanup in the test files and the Lean backend
| * Merge branch 'main' into son/cleanupSon HO2024-06-1717-22/+22
| |\ | |/ |/|
* | Merge pull request #240 from RaitoBezarius/has-int-predSon HO2024-06-172-9/+41
|\ \ | | | | | | backends/lean: introduce `HasIntPred` automation
| * \ Merge branch 'main' into has-int-predSon Ho2024-06-1717-22/+22
| |\ \ | |/ / |/| |
* | | Merge pull request #245 from AeneasVerif/son/update-leanSon HO2024-06-176-14/+14
|\ \ \ | | | | | | | | Bump Lean to 4.9.0-rc2
| * \ \ Merge branch 'main' into son/update-leanSon Ho2024-06-171-12/+4
| |\ \ \ | |/ / / |/| | |
* | | | Merge pull request #249 from Nadrieril/github-ciGuillaume Boisseau2024-06-171-12/+4
|\ \ \ \
| * | | | Revert "Switch to GitHub CI runners"Nadrieril2024-06-171-12/+4
|/ / / / | | | | | | | | | | | | This reverts commit dc8278e8bfd5d903ba472f6c91bd67510b23cbc4.
| * | | Merge branch 'main' into son/update-leanSon Ho2024-06-171-4/+12
| |\ \ \ | |/ / / |/| | |
* | | | Merge pull request #248 from Nadrieril/bump-charon2Guillaume Boisseau2024-06-1717-22/+22
|\ \ \ \
| * | | | Update charonNadrieril2024-06-1717-22/+22
|/ / / /
| * | | Regenerate the testsSon Ho2024-06-1715-18/+18
| | | |
| * | | Update the Charon pinSon Ho2024-06-172-4/+4
| | | |
| | | * Merge branch 'main' into son/cleanupGuillaume Boisseau2024-06-171-4/+12
| | | |\ | |_|_|/ |/| | |
* | | | Merge pull request #247 from Nadrieril/github-ciGuillaume Boisseau2024-06-171-4/+12
|\ \ \ \
| * | | | Switch to GitHub CI runnersNadrieril2024-06-171-4/+12
|/ / / /
| | | * Regenerate the testsSon Ho2024-06-1726-2/+77
| | | |
| | | * Deactivate some linter options for the generated Lean filesSon Ho2024-06-171-0/+9
| | | |
| | | * Update the testsSon Ho2024-06-176-4/+31
| | | |
| | | * Automatically add a @[reducible] attribute to some generated functionsSon Ho2024-06-174-3/+66
| | | |
| | | * Update Hashmap/Properties.leanSon Ho2024-06-171-36/+34
| | | |
| | | * Update the code of the hashmapSon Ho2024-06-1712-459/+465
| | |/
| | * Make a minor cleanupSon Ho2024-06-171-9/+11
| | |
| | * Merge branch 'son/update-lean' into has-int-predSon Ho2024-06-1724-321/+458
| | |\ | | |/ | |/|
| * | Update the Lean dependenciesSon Ho2024-06-172-8/+8
| | |
| * | Update the testsSon Ho2024-06-142-4/+4
| | |
| * | Start updating Lean to 4.9.0-rc2Son Ho2024-06-142-4/+4
|/ /
* | Merge pull request #243 from AeneasVerif/son/update-leanSon HO2024-06-1318-168/+196
|\ \ | | | | | | Update Lean to v4.9.0-rc1
| * | Update the testsSon Ho2024-06-134-34/+29
| | |
| * | Update Lean to v4.9.0-rc1Son Ho2024-06-1315-139/+172
|/ /
* | Merge pull request #242 from AeneasVerif/son/scalars2Son HO2024-06-139-114/+150
|\ \ | | | | | | Update the scalar notations for the Lean backend
| * | Fix more issues with the scalar notationsSon Ho2024-06-131-15/+29
| | |
| * | Fix more issuesSon Ho2024-06-133-16/+22
| | |
| * | Fix a proofSon Ho2024-06-131-1/+1
| | |
| * | Merge branch 'main' into son/scalars2Son HO2024-06-131-1/+1
| |\ \ | |/ / |/| |
* | | Merge pull request #238 from RaitoBezarius/prop-has-imp-sortSon HO2024-06-131-1/+1
|\ \ \ | | | | | | | | feat: `PropHasImp` can have `Sort u` as premisses
| * \ \ Merge branch 'main' into prop-has-imp-sortSon HO2024-06-125-45/+118
| |\ \ \ | |/ / / |/| | |
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 03:05:32 +0000