avl-verification/Verification, branch main Isabelle fork of https://github.com/RaitoBezarius/avl-verification feat: make `find` a better specification 2024-04-23T14:34:55+00:00 Raito Bezarius 2024-04-23T14:34:06+00:00 69e7653d313773304939de58c575595ece3aa034 Previously, find := true was matching this spec. It needed to be in PRE/POST style and be an equivalence wrt to the location return value. Alternatively, we import the Order. Signed-off-by: Raito Bezarius <masterancpp@gmail.com> 
Previously, find := true was matching this spec.
It needed to be in PRE/POST style and be an equivalence wrt to the
location return value.

Alternatively, we import the Order.

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
feat: close `find` / `insert` proofs 2024-04-23T12:24:04+00:00 Raito Bezarius 2024-04-23T12:24:04+00:00 b650710ad3f8c14b713bdf52f684f472115dce2f After a complete 180 with the Order theory, we close the goals of find and insert and we give an example of U32 order that we will upstream to Aeneas directly. Signed-off-by: Raito Bezarius <masterancpp@gmail.com> 
After a complete 180 with the Order theory, we close the goals of find
and insert and we give an example of U32 order that we will upstream to
Aeneas directly.

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>