aeneas - aeneas rust verifier with a hacky Isabelle backend

	Commit message (Collapse)	Author	Age	Files	Lines
*	backends/lean: introduce `HasIntPred` automation	Ryan Lahfa	2024-06-12	1	-5/+33
\| \| \| \| \| \| \| \| \| \| \| \| \|	`HasIntPred` enable generation of facts based on specific terms in the context rather than their types, e.g. if the "length of a list" occurs in the context, generate the fact 0 ≤ length of that list, which can be further used for `scalar_tac` automation to discharge bounds goals. The aim is to use it to simplify various height related computations, e.g. whenever "height of a (left ; right) tree" is encountered, generate "height left < height of a (left ; right) tree", etc. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
*	Update scalar_tac to use omega instead of linarith	Son Ho	2024-05-24	1	-97/+65
\|
*	Update the lean toolchain and fix the proofs	Son Ho	2024-04-05	1	-1/+0
\|
*	Refold the scalar types when applying progress	Son Ho	2023-10-17	1	-2/+2
\|
*	Implement tactics for termination proofs which involve arithmetic	Son Ho	2023-10-17	1	-0/+11
\|
*	Improve scalar_tac	Son Ho	2023-09-18	1	-3/+5
\|
*	Update to Lean 4.0.0 and fix some broken proofs	Son Ho	2023-09-14	1	-1/+1
\|
*	Start adding support for Arrays/Slices in the Lean library	Son Ho	2023-08-04	1	-10/+21
\|
*	Update the syntax of the progress tactic	Son Ho	2023-07-26	1	-1/+1
\|
*	Make progress on the proofs of the hashmap	Son Ho	2023-07-25	1	-0/+1
\|
*	Make progress on the hashmap properties	Son Ho	2023-07-25	1	-0/+2
\|
*	Improve int_tac and scalar_tac	Son Ho	2023-07-25	1	-7/+56
\|
*	Make some proofs in Hashmap/Properties.lean and improve progress	Son Ho	2023-07-20	1	-1/+1
\|
*	Improve progress	Son Ho	2023-07-19	1	-8/+0
\|
*	Reorganize the Lean backend	Son Ho	2023-07-17	1	-0/+236