aeneas/compiler, branch isabelle aeneas rust verifier with a hacky Isabelle backend had some fun writing an IsabelleHOL backend 2024-06-29T20:11:04+00:00 stuebinm 2024-06-29T19:31:22+00:00 59214186b817329342d9d72e23adf12f7a3b1348 (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) 
(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)
Remove redundant `llbc_name` field 2024-06-28T07:46:11+00:00 Nadrieril 2024-06-26T11:53:45+00:00 617941a779baab199aa69bf2e8578a1ee7877289 It's redundant with `item_meta.name` 
It's redundant with `item_meta.name`
Update charon 2024-06-25T11:57:52+00:00 Nadrieril 2024-06-25T11:57:52+00:00 09c02a7b56575e826c66a6c8873b290a8afb5827 






Update charon
2024-06-24T11:53:31+00:00

Nadrieril

2024-06-24T09:10:28+00:00

16aa66aabffeaaebc03c264b89387f010750dac3












Update charon
2024-06-21T14:14:58+00:00

Nadrieril

2024-06-21T13:47:56+00:00

d3f52e23ede39c4fd7845b6c5feb29d28b2a2384












`predicates` got merged into `generic_params`
2024-06-21T07:34:38+00:00

Nadrieril

2024-06-20T14:46:29+00:00

b287f234695d9013cb74c99dcac46a9b5b334f7c












Support for renaming using the rename attribute in charon (#239)
2024-06-18T20:47:35+00:00

Escherichia

2024-06-18T20:47:35+00:00

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>




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






Tiny dedup
2024-06-18T10:11:23+00:00

Nadrieril

2024-06-18T09:31:45+00:00

aa5948d7f9fd9b2d0ce18657215dae6877ebd996












Deactivate some linter options for the generated Lean files
2024-06-17T05:25:00+00:00

Son Ho

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

48b425b3b190f1d40f60ccb4cb1fdf5521753fb9












Automatically add a @[reducible] attribute to some generated functions
2024-06-17T05:14:52+00:00

Son Ho

2024-06-17T05:14:52+00:00

f4739fba4be95818ca01776837c8d610e443a45b