summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* some isabelle/hol verificationHEADmainstuebinm2024-06-297-24/+341
| | | | | | | | doesn't do much, just proves that the find function won't cause an error. also removes all uses of rust traits, since these are currently broken on the aeneas side.
* feat: make `find` a better specificationRaito Bezarius2024-04-232-10/+19
| | | | | | | | | | 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>
* Merge pull request #3 from RaitoBezarius/bst-findRyan Lahfa2024-04-2311-202/+376
|\ | | | | feat: `find` and `insert` reinforced proofs
| * feat: close `find` / `insert` proofsRaito Bezarius2024-04-2311-215/+347
| | | | | | | | | | | | | | | | 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` proofRaito Bezarius2024-04-181-0/+42
|/ | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: extract `find`Raito Bezarius2024-04-181-2/+28
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: make `find` extractableRaito Bezarius2024-04-181-1/+1
| | | | | | I was not borrowing `&self`! Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* chore: nixify the projectRaito Bezarius2024-04-185-0/+89
| | | | | | So that I stop doing `nix run` one-offs! Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: factor everything in `OrdSpecRel`Raito Bezarius2024-04-172-6/+2
| | | | | | Now, we speak only about equivalence. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: add functional correctness of elements contained in the resulting treeRaito Bezarius2024-04-176-86/+95
| | | | | | | We revamp the typeclass mechanisms and we add an equality hypothesis now. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: add `find` functionRaito Bezarius2024-04-162-13/+36
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: init lake lockRaito Bezarius2024-04-121-0/+77
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: upgrade to lean v4.7Raito Bezarius2024-04-122-9/+2
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: note on extraction for inductiveRaito Bezarius2024-04-121-0/+2
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* fixup! feat: cleanup more the gitignoreRaito Bezarius2024-04-121-0/+1
|
* feat: commit Rust alternativesRaito Bezarius2024-04-122-0/+106
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: cleanup more the gitignoreRaito Bezarius2024-04-121-0/+1
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: init notesRaito Bezarius2024-04-121-0/+114
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: cleanup the MainRaito Bezarius2024-04-121-33/+1
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* Merge pull request #2 from RaitoBezarius/refactor-theoryRyan Lahfa2024-04-127-116/+433
|\ | | | | refactor: generalize the theory and perform some lifts
| * feat: upgrade and close all proofs except Preorder on U32Raito Bezarius2024-04-125-81/+138
| | | | | | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
| * feat: close the BST proof modulo unbundlingRaito Bezarius2024-04-052-1/+60
| | | | | | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
| * feat: close key theorem for any result on binary search treesRaito Bezarius2024-04-041-25/+26
| | | | | | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
| * feat: lift Rust "totality" to total ordersRaito Bezarius2024-04-041-15/+30
| | | | | | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
| * refactor: define some projectors for ForallNodeRaito Bezarius2024-04-041-0/+6
| | | | | | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
| * refactor: generalize the theory and perform some liftsRaito Bezarius2024-03-286-107/+286
|/ | | | | | Move forward the "HSpec" idea, move around files, construct the hierarchy of trees, etc. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* feat: first property "set of values post = {a} \cup set of values pre"Raito Bezarius2024-03-261-25/+62
| | | | | | This is a first property which is generic of all BSTs. Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* Initial extractionRaito Bezarius2024-03-256-9/+208
| | | | Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
* Initial commitRaito Bezarius2024-03-255-0/+122
Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 05:51:15 +0000