aeneas rust verifier with a hacky Isabelle backend https://stuebinm.eu/git/aeneas/atom/charon-pin?h=isabelle 2024-06-28T06:18:47Z 2024-06-28T06:18:47Z Nadrieril 2024-06-26T14:24:27Z urn:sha1:c00d337f48cbaf56a5b81f396c2f18ae811aee5a 2024-06-25T11:57:52Z Nadrieril 2024-06-25T11:57:52Z urn:sha1:09c02a7b56575e826c66a6c8873b290a8afb5827 2024-06-24T11:53:31Z Nadrieril 2024-06-24T09:10:28Z urn:sha1:16aa66aabffeaaebc03c264b89387f010750dac3 2024-06-24T08:37:32Z Nadrieril 2024-06-24T08:37:32Z urn:sha1:ba2111ff8f4281e0be345380775cb7a43afa22e8 2024-06-21T14:14:58Z Nadrieril 2024-06-21T13:47:56Z urn:sha1:d3f52e23ede39c4fd7845b6c5feb29d28b2a2384 2024-06-21T07:34:38Z Nadrieril 2024-06-20T14:46:29Z urn:sha1:b287f234695d9013cb74c99dcac46a9b5b334f7c 2024-06-18T20:47:35Z Escherichia 2024-06-18T20:47:35Z urn:sha1:aa8e74197687ecc6d8f925babc8ba3cd6c739990 * 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> 2024-06-18T10:12:05Z Nadrieril 2024-06-18T10:12:05Z urn:sha1:082661f0d9d1bb1196ef8e1d57b3f2b4922b3d8e 2024-06-17T18:06:19Z Son Ho 2024-06-17T18:06:19Z urn:sha1:8eacc8bc308ba6b703d46137262de37a69f2ecab 2024-06-06T07:36:36Z Nadrieril 2024-06-05T08:08:56Z urn:sha1:7f2b8bf304f9c21f34c4be44a087cc15c56d6b07