aeneas - aeneas rust verifier with a hacky Isabelle backend

	Commit message (Collapse)	Author	Age	Files	Lines
*	Add some proofs for the Lean backend (#255)	Son HO	2024-06-21	1	-11/+11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* 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>
*	Support for renaming using the rename attribute in charon (#239)	Escherichia	2024-06-18	1	-1/+1
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* 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>
*	Update the code of the hashmap	Son Ho	2024-06-17	1	-30/+31
\|
*	Update the test runner to allow the syntax [!lean] and [borrow-check]	Son Ho	2024-06-05	1	-1/+1
\|
*	tests: Rename hashmap_utils -> utils	Nadrieril	2024-05-28	1	-4/+4
\|
*	tests: Merge the hashmap test files	Nadrieril	2024-05-27	1	-1/+28
\|
*	runner: Pass options in special comments	Nadrieril	2024-05-24	1	-0/+8
\|
*	Import test suite from charon	Nadrieril	2024-05-24	1	-0/+352