<feed xmlns='http://www.w3.org/2005/Atom'>
<title>aeneas/backends/lean, branch isabelle</title>
<subtitle>aeneas rust verifier with a hacky Isabelle backend</subtitle>
<id>https://stuebinm.eu/git/aeneas/atom/backends/lean?h=isabelle</id>
<link rel='self' href='https://stuebinm.eu/git/aeneas/atom/backends/lean?h=isabelle'/>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/'/>
<updated>2024-06-25T08:34:24Z</updated>
<entry>
<title>Bump Lean to v4.9.0rc3 (#261)</title>
<updated>2024-06-25T08:34:24Z</updated>
<author>
<name>Son HO</name>
</author>
<published>2024-06-25T08:34:24Z</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=59ee1eb89d7c1018858250832ff1a92af0cbeab6'/>
<id>urn:sha1:59ee1eb89d7c1018858250832ff1a92af0cbeab6</id>
<content type='text'>
</content>
</entry>
<entry>
<title>Do some cleanup in the Lean backend (#257)</title>
<updated>2024-06-22T13:07:14Z</updated>
<author>
<name>Son HO</name>
</author>
<published>2024-06-22T13:07:14Z</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=8719c17f1a363c0463d74b90e558b2aaa24645d6'/>
<id>urn:sha1:8719c17f1a363c0463d74b90e558b2aaa24645d6</id>
<content type='text'>
</content>
</entry>
<entry>
<title>Improve `scalar_tac` and `scalar_decr_tac` (#256)</title>
<updated>2024-06-22T11:22:32Z</updated>
<author>
<name>Son HO</name>
</author>
<published>2024-06-22T11:22:32Z</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=8144c39f4d37aa1fa14a8a061eb7ed60e153fb4c'/>
<id>urn:sha1:8144c39f4d37aa1fa14a8a061eb7ed60e153fb4c</id>
<content type='text'>
* 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</content>
</entry>
<entry>
<title>Add some proofs for the Lean backend (#255)</title>
<updated>2024-06-21T21:24:01Z</updated>
<author>
<name>Son HO</name>
</author>
<published>2024-06-21T21:24:01Z</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=4d30546c809cb2c512e0c3fd8ee540fff1330eab'/>
<id>urn:sha1:4d30546c809cb2c512e0c3fd8ee540fff1330eab</id>
<content type='text'>
* 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 &lt;sonho@Sons-MacBook-Pro.local&gt;
Co-authored-by: Son Ho &lt;sonho@Sons-MBP.lan&gt;</content>
</entry>
<entry>
<title>Make a minor cleanup</title>
<updated>2024-06-17T04:26:43Z</updated>
<author>
<name>Son Ho</name>
</author>
<published>2024-06-17T04:26:43Z</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=007c9024c0c3b549049a55243b391ae2337ad616'/>
<id>urn:sha1:007c9024c0c3b549049a55243b391ae2337ad616</id>
<content type='text'>
</content>
</entry>
<entry>
<title>Merge branch 'son/update-lean' into has-int-pred</title>
<updated>2024-06-17T04:16:43Z</updated>
<author>
<name>Son Ho</name>
</author>
<published>2024-06-17T04:16:43Z</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=e57e6f08e5cc34bf4e9237650f5ecbab440b9ea2'/>
<id>urn:sha1:e57e6f08e5cc34bf4e9237650f5ecbab440b9ea2</id>
<content type='text'>
</content>
</entry>
<entry>
<title>Update the Lean dependencies</title>
<updated>2024-06-17T04:14:06Z</updated>
<author>
<name>Son Ho</name>
</author>
<published>2024-06-17T04:14:06Z</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=85098d7caf5e3196c2e8f92411efd2814bfed1ea'/>
<id>urn:sha1:85098d7caf5e3196c2e8f92411efd2814bfed1ea</id>
<content type='text'>
</content>
</entry>
<entry>
<title>Start updating Lean to 4.9.0-rc2</title>
<updated>2024-06-14T11:55:30Z</updated>
<author>
<name>Son Ho</name>
</author>
<published>2024-06-14T11:55:30Z</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=e3bde786750009becf4f828370f2e0d242ccf39d'/>
<id>urn:sha1:e3bde786750009becf4f828370f2e0d242ccf39d</id>
<content type='text'>
</content>
</entry>
<entry>
<title>Update the tests</title>
<updated>2024-06-13T20:37:18Z</updated>
<author>
<name>Son Ho</name>
</author>
<published>2024-06-13T20:37:18Z</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=d5cf75a0f8209298ad85f46249f14d5c3a24faf6'/>
<id>urn:sha1:d5cf75a0f8209298ad85f46249f14d5c3a24faf6</id>
<content type='text'>
</content>
</entry>
<entry>
<title>Update Lean to v4.9.0-rc1</title>
<updated>2024-06-13T20:04:13Z</updated>
<author>
<name>Son Ho</name>
</author>
<published>2024-06-13T20:04:13Z</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=b3dd78ff4c8785b6ff9bce9927df90f8c78a9109'/>
<id>urn:sha1:b3dd78ff4c8785b6ff9bce9927df90f8c78a9109</id>
<content type='text'>
</content>
</entry>
</feed>
