aeneas/tests/lean/Hashmap, branch isabelle

Bump Lean to v4.9.0rc3 (#261)

2024-06-25T08:34:24+00:00

Do some cleanup in the Lean backend (#257)

2024-06-22T13:07:14+00:00

Improve `scalar_tac` and `scalar_decr_tac` (#256)

2024-06-22T11:22:32+00:00

* 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)

2024-06-21T21:24:01+00:00

* 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 
Co-authored-by: Son Ho

Bump charon

2024-06-18T10:12:05+00:00

Regenerate the tests

2024-06-17T05:25:17+00:00

Update the tests

2024-06-17T05:15:26+00:00

Update Hashmap/Properties.lean

2024-06-17T04:39:16+00:00

Update the code of the hashmap

2024-06-17T04:34:07+00:00

Update the tests

2024-06-13T20:37:18+00:00