aeneas/backends/lean/Base/Progress, branch isabelle aeneas rust verifier with a hacky Isabelle backend Add some proofs for the Lean backend (#255) 2024-06-21T21:24:01+00:00 Son HO 2024-06-21T21:24:01+00:00 4d30546c809cb2c512e0c3fd8ee540fff1330eab * 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> 
* 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>
 Update Lean to v4.9.0-rc1 2024-06-13T20:04:13+00:00 Son Ho 2024-06-13T20:04:13+00:00 b3dd78ff4c8785b6ff9bce9927df90f8c78a9109 






Slightly simplify the progress tactic
2024-06-12T12:46:38+00:00

Son Ho

2024-06-12T12:46:38+00:00

f5deac2b0f42e2a87fc26da50c902729e0ed1039












Add the Simp.Config to the simp wrappers
2024-06-12T12:45:58+00:00

Son Ho

2024-06-12T12:45:58+00:00

7763a8ef8d5190fad39e9e677c5f44c536973655












Fix an issue in the progress tactic
2024-05-21T10:08:32+00:00

Son Ho

2024-05-21T10:08:32+00:00

1db6738bdbda9f306e1aedd9fd54a2017e77539c












Rename Result.ret as Result.ok in the backends
2024-04-04T14:08:32+00:00

Son Ho

2024-04-04T14:08:32+00:00

4828b77847ee981f5c6a1bbad7f8e6ed0e58eb0f












Update lean to v4.6.0-rc1 and start fixing the proofs
2024-02-02T19:48:26+00:00

Son Ho

2024-02-02T19:48:26+00:00

a68c231db4edf97c4f007724969aec7dd60941a1












Fix a minor issue with the progress tactic
2024-01-27T20:26:38+00:00

Son Ho

2024-01-27T20:26:38+00:00

c709eadb14e2ecd21c9c4a6a9def39334f27552b












Improve the Lean backend
2024-01-25T23:17:59+00:00

Son Ho

2024-01-25T23:17:59+00:00

9f0e4605e1c8816dbf5ed3e9e893b25e9a2be4a3












Start working on higher-order examples for Diverge
2023-12-11T17:34:10+00:00

Son Ho

2023-12-11T17:34:10+00:00

78367ef21c147b26040e0f6062a907fceab1f390