Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | compiler: map `core::mem::swap` to the pure swap | Ryan Lahfa | 2024-04-24 | 3 | -6/+4 |
| | | | | | | | | | 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> | ||||
* | compiler: map `core::option::Option::take` to identity function | Ryan Lahfa | 2024-04-17 | 2 | -0/+6 |
| | | | | | | | | `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> | ||||
* | Merge pull request #126 from RaitoBezarius/scalar-preorders | Son HO | 2024-04-15 | 1 | -0/+10 |
|\ | | | | | lean: scalars form a preorder | ||||
| * | lean: scalars form a preorder | Ryan Lahfa | 2024-04-12 | 1 | -0/+10 |
| | | | | | | | | | | | | | | | | | | | | 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> | ||||
* | | Merge pull request #127 from AeneasVerif/fix-ci | Son HO | 2024-04-15 | 2 | -2/+5 |
|\ \ | |/ |/| | Fix CI | ||||
| * | Fix CI | Nadrieril | 2024-04-15 | 2 | -2/+5 |
|/ | |||||
* | Merge pull request #124 from AeneasVerif/son/lean1 | Son HO | 2024-04-12 | 11 | -60/+674 |
|\ | | | | | Add more definitions to the Lean library | ||||
| * | Add more definitions to the Lean library | Son Ho | 2024-04-12 | 5 | -0/+200 |
| | | |||||
| * | Reorganize the files in the Lean backend a bit | Son Ho | 2024-04-12 | 5 | -241/+266 |
| | | |||||
| * | Start adding integer functions to the Lean library | Son Ho | 2024-04-12 | 7 | -58/+447 |
|/ | |||||
* | Merge pull request #110 from zhassan-aws/checked-ops | Son HO | 2024-04-12 | 2 | -21/+279 |
|\ | | | | | Add builtins for some checked ops for the Lean backend | ||||
| * | Update the bindings for the extraction | Son Ho | 2024-04-12 | 1 | -14/+11 |
| | | |||||
| * | Merge branch 'main' into checked-ops | Son Ho | 2024-04-12 | 0 | -0/+0 |
| |\ | |/ |/| | |||||
* | | Merge pull request #123 from AeneasVerif/son/clean | Son HO | 2024-04-11 | 80 | -1997/+1989 |
|\ \ | | | | | | | Cleanup the code in preparation of the nested loops | ||||
| | * | Fix a proof | Son Ho | 2024-04-12 | 1 | -1/+0 |
| | | | |||||
| | * | Update the core.num.checked_* definitions | Son Ho | 2024-04-12 | 1 | -31/+233 |
| | | | |||||
| | * | Merge branch 'son/clean' into checked-ops | Son Ho | 2024-04-11 | 117 | -2327/+2546 |
| | |\ | | |/ | |/| | |||||
| * | | Update a Lean file | Son Ho | 2024-04-11 | 1 | -1/+1 |
| | | | |||||
| * | | Update some Lean proofs | Son Ho | 2024-04-11 | 3 | -24/+24 |
| | | | |||||
| * | | Update a comment | Son Ho | 2024-04-11 | 1 | -2/+2 |
| | | | |||||
| * | | Fix a Coq file | Son Ho | 2024-04-11 | 1 | -1/+1 |
| | | | |||||
| * | | Fix some F* proofs | Son Ho | 2024-04-11 | 1 | -4/+4 |
| | | | |||||
| * | | Merge remote-tracking branch 'origin/main' into son/clean | Son Ho | 2024-04-11 | 40 | -130/+310 |
| |\ \ | |/ / |/| | | |||||
* | | | Merge pull request #121 from AeneasVerif/son/format | Son HO | 2024-04-11 | 1 | -9/+6 |
|\ \ \ | | | | | | | | | Reformat the code | ||||
| * | | | Reformat the code | Son Ho | 2024-04-11 | 1 | -9/+6 |
|/ / / | |||||
* | | | Merge pull request #119 from AeneasVerif/generic-copy | Guillaume Boisseau | 2024-04-11 | 4 | -11/+11 |
|\ \ \ | |||||
| * | | | Use charon main | Nadrieril | 2024-04-11 | 2 | -5/+4 |
| | | | | |||||
| * | | | Update a comment | Son HO | 2024-04-11 | 1 | -1/+1 |
| | | | | |||||
| * | | | Trust rustc regarding `Copy` bounds | Nadrieril | 2024-04-10 | 5 | -11/+12 |
|/ / / | |||||
* | | | Merge pull request #115 from AeneasVerif/nix | Son HO | 2024-04-10 | 1 | -0/+7 |
|\ \ \ | | | | | | | | | Update flake.nix | ||||
| * | | | Update flake.nix | Nadrieril | 2024-04-08 | 1 | -0/+7 |
|/ / / | | | | | | | | | | | | | It was missing some dependencies, and while we're at it we can disable sanity checks in tests. | ||||
* | | | Merge pull request #113 from AeneasVerif/escherichia/error_catching_translate | Son HO | 2024-04-07 | 15 | -66/+186 |
|\ \ \ | | | | | | | | | Error catching should tell when code couldn't be generated | ||||
| * | | | Improve the error messages further | Son Ho | 2024-04-07 | 3 | -1/+44 |
| | | | | |||||
| * | | | Cleanup a bit and improve the error messages | Son Ho | 2024-04-07 | 12 | -82/+91 |
| | | | | |||||
| * | | | Resolved comments and added the name of the not translated element | Escherichia | 2024-04-05 | 2 | -7/+18 |
| | | | | |||||
| * | | | resolved comments | Escherichia | 2024-04-05 | 3 | -99/+113 |
| | | | | |||||
| * | | | error catching should now be able to tell when code couldn't be generated | Escherichia | 2024-04-05 | 3 | -101/+144 |
| | | | | |||||
* | | | | Merge pull request #114 from AeneasVerif/son/lean-version | Son HO | 2024-04-05 | 12 | -36/+36 |
|\ \ \ \ | |/ / / |/| | | | Bump the version of Lean to 4.7.0 | ||||
| * | | | Update the lean toolchain and fix the proofs | Son Ho | 2024-04-05 | 12 | -36/+36 |
| | | | | |||||
* | | | | Merge pull request #106 from AeneasVerif/escherichia/error_catching | Son HO | 2024-04-04 | 13 | -9/+54 |
|\ \ \ \ | | | | | | | | | | | Added Error and EError to expressions and propagated related changes | ||||
| * | | | | Fix a minor issue | Son Ho | 2024-04-04 | 1 | -1/+1 |
| | | | | | |||||
| * | | | | Merge remote-tracking branch 'origin/main' into escherichia/error_catching | Son Ho | 2024-04-04 | 45 | -396/+446 |
| |\ \ \ \ | |||||
| * | | | | | Update the way errors are reported | Son Ho | 2024-04-04 | 2 | -10/+7 |
| | | | | | | |||||
| * | | | | | Update the nix flake | Son Ho | 2024-04-04 | 1 | -3/+3 |
| | | | | | | |||||
| * | | | | | Now prints all errors in the error_list | Escherichia | 2024-04-04 | 2 | -3/+11 |
| | | | | | | |||||
| * | | | | | Merge remote-tracking branch 'origin/main' into escherichia/error_catching | Escherichia | 2024-04-04 | 3 | -5/+2 |
| |\ \ \ \ \ | |||||
| * | | | | | | resolved requested changes | Escherichia | 2024-04-03 | 1 | -1/+0 |
| | | | | | | | |||||
| * | | | | | | resolved requested changes | Escherichia | 2024-04-03 | 3 | -6/+4 |
| | | | | | | | |||||
| * | | | | | | added extract_ty_errors and extract_texpression_errors to deal with the ↵ | Escherichia | 2024-04-03 | 2 | -3/+10 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | error case in their respective types | ||||
| * | | | | | | added Error and EError to expressions and propagated related changes | Escherichia | 2024-04-03 | 12 | -5/+41 |
| | | | | | | |