avl-verification/AvlVerification, branch main Isabelle fork of https://github.com/RaitoBezarius/avl-verification 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>
feat: outline of `find` proof 2024-04-18T13:38:36+00:00 Raito Bezarius 2024-04-18T13:38:36+00:00 2ff68510aabc63e250f98264e0642557015de4e2 Signed-off-by: Raito Bezarius <masterancpp@gmail.com> 
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
feat: factor everything in `OrdSpecRel` 2024-04-17T14:50:16+00:00 Raito Bezarius 2024-04-17T14:50:16+00:00 fb9a1e93c2163b170979523f9a0cae90b472a16c Now, we speak only about equivalence. Signed-off-by: Raito Bezarius <masterancpp@gmail.com> 
Now, we speak only about equivalence.

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
feat: add functional correctness of elements contained in the resulting tree 2024-04-17T13:08:07+00:00 Raito Bezarius 2024-04-17T13:08:07+00:00 945c630ec18e282bd0db731fb3f0b521e99de059 We revamp the typeclass mechanisms and we add an equality hypothesis now. Signed-off-by: Raito Bezarius <masterancpp@gmail.com> 
We revamp the typeclass mechanisms and we add an equality hypothesis
now.

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
feat: upgrade and close all proofs except Preorder on U32 2024-04-12T17:11:16+00:00 Raito Bezarius 2024-04-12T17:11:16+00:00 3577c7dc9d3013d401c45a7628b0ff4b6fd0ec67 Signed-off-by: Raito Bezarius <masterancpp@gmail.com> 
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
feat: close the BST proof modulo unbundling 2024-04-05T16:33:47+00:00 Raito Bezarius 2024-04-04T15:31:19+00:00 50be416e22a39eaf59f7edba81b919e1f114a0ae Signed-off-by: Raito Bezarius <masterancpp@gmail.com> 
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
feat: close key theorem for any result on binary search trees 2024-04-04T15:30:46+00:00 Raito Bezarius 2024-04-04T15:30:46+00:00 22a499f5d4d231bef3193405983f9ade6da116db Signed-off-by: Raito Bezarius <masterancpp@gmail.com> 
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
feat: lift Rust "totality" to total orders 2024-04-04T15:30:22+00:00 Raito Bezarius 2024-04-04T15:30:22+00:00 7064a237805d5cac48d2f5aa7e4691ea7695b8af Signed-off-by: Raito Bezarius <masterancpp@gmail.com> 
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
refactor: define some projectors for ForallNode 2024-04-04T15:29:44+00:00 Raito Bezarius 2024-04-04T15:29:44+00:00 9da83df6319b806d584da9ae5c6da260fcae56a8 Signed-off-by: Raito Bezarius <masterancpp@gmail.com> 
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
refactor: generalize the theory and perform some lifts 2024-03-28T19:30:56+00:00 Raito Bezarius 2024-03-28T16:59:35+00:00 5e35e3875884ca4be63f253d9e8d7f2fc71b3527 Move forward the "HSpec" idea, move around files, construct the hierarchy of trees, etc. Signed-off-by: Raito Bezarius <masterancpp@gmail.com> 
Move forward the "HSpec" idea, move around files, construct the hierarchy of trees, etc.

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