| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
| |
* Fix an issue in a proof of the hashmap
* Improve scalar_decr_tac
* Improve the error message of scalar_tac and add the missing Termination.lean
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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>
|
| |
|
|\ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | |\ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This makes it possible to have `InBounds ... : Type 1` for example as
`x`.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | | | |
|
| | |/
| |/| |
|
| | |
| | |
| | |
| | | |
This reverts commit c8272aeea205ca9cb36e22757473ca2a931a4933.
|
| | |
| | |
| | |
| | | |
This reverts commit fe59d3afe131e9f83cbdf73b1c8089ad090d92fb.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |/ |
|
|/
|
|
|
|
|
|
|
|
|
|
|
| |
`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>
|
|
|
|
|
|
|
|
|
| |
`0#ty` is neutral for `max` for unsigned integers.
Without the `Fact` instances, those theorems are not as automatic as
they could be.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Situations where you have `coe (max a b) = max (coe a) (coe b)` are
often stuck during verification because of the lack of this theorem.
With this theorem, `push_cast` works as intended and normalizes even
further.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
|\
| |
| |
| | |
feat(backend/lean): Raw Lean literals can be parsed into scalars automatically
|
| |
| |
| |
| |
| |
| |
| | |
We can use coercion to go to integers, build a scalar out of an int via
unification and let the user clear up bounds or let Lean decide them.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
|/
|
|
|
|
| |
Oops, it is supposed to do something with the second argument!
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| |
|
|\ |
|
| |\ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
In the pure functional model, `swap` is mostly about borrow checking and
should simplify to the pure swap in our backends.
Other backends than Lean are not done in this commit.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
`take` in a pure functional model is the identity function and
everything related to borrow checking is handled by the forward/backward
mechanism.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| |/
|/| |
|
|/
|
|
|
|
|
| |
More than c1c33de8, actually, scalars form a linear order with a
decidable ≤ operation which is induced by the integer (Z) model.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
|
|
|
|
|
|
|
|
|
| |
Via the canonical injection, we can easily define an induced preorder on
scalars and inherit all nice properties.
It's useful to reason on specific scalar preorders w.r.t. Ordering, see
the binary search tree verification example.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| |
|
| |
|
| |
|
| |
|
| |
|
|\ |
|
| |\ |
|
| | | |
|
| | | |
|
| |/ |
|
|/ |
|
| |
|