summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* isabelle: more correct u32 typeisabellestuebinm2024-07-041-3/+11
| | | | | | (I'd have to figure out how to do the code equation stuff to make this type actually usable the way nat is, but it should behave correctly in proofs)
* had some fun writing an IsabelleHOL backendstuebinm2024-06-2913-132/+528
| | | | | | | (do not actually use this, most things are broken, and the primitives lib barely exists and is simply incorrect. But it is enough to create syntax-correct Isabelle code for relatively simply rust code, as long as it does not contain any uses of traits)
* Merge pull request #272 from Nadrieril/remove-llbc_nameGuillaume Boisseau2024-06-289-77/+65
|\
| * Remove redundant `llbc_name` fieldNadrieril2024-06-289-77/+65
|/ | | | It's redundant with `item_meta.name`
* Merge pull request #271 from Nadrieril/update-charon2Guillaume Boisseau2024-06-2817-32/+28
|\
| * Update charonNadrieril2024-06-2817-32/+28
|/
* Merge pull request #263 from Nadrieril/subst-predsGuillaume Boisseau2024-06-253-7/+5
|\
| * Update charonNadrieril2024-06-253-7/+5
|/
* Bump Lean to v4.9.0rc3 (#261)Son HO2024-06-256-9/+4
|
* Merge pull request #259 from Nadrieril/augmente-ta-vitesseGuillaume Boisseau2024-06-241-2/+1
|\
| * Use the self-hosted runner for the lean CI checksNadrieril2024-06-241-2/+1
|/
* Merge pull request #258 from Nadrieril/bump-charonGuillaume Boisseau2024-06-2418-105/+113
|\
| * Update charonNadrieril2024-06-2418-105/+113
|/
* Merge pull request #244 from Nadrieril/bump-charonGuillaume Boisseau2024-06-2411-13/+13
|\
| * 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
| | |
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 05:01:28 +0000