Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Address review comments | Nadrieril | 2024-04-18 | 18 | -2/+20 |
| | |||||
* | Ensure we regenerate files properly in CI | Nadrieril | 2024-04-18 | 27 | -32/+9 |
| | | | | | Files that weren't regenerated were marked as not automatically-generated. | ||||
* | Merge pull request #145 from RaitoBezarius/no-flakes | Guillaume Boisseau | 2024-04-18 | 4 | -1/+50 |
|\ | |||||
| * | feat(nix): support non-Flakes users | Ryan Lahfa | 2024-04-17 | 4 | -1/+50 |
| | | | | | | | | | | | | | | | | Not all Nix users can make use of Flakes. This adds the compatibility for non-Flakes users. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | ||||
* | | Merge pull request #130 from AeneasVerif/fast-tests-outside-of-ci | Son HO | 2024-04-18 | 2 | -8/+4 |
|\ \ | | | | | | | Run sanity checks in CI only | ||||
| * | | Run sanity checks in CI only | Nadrieril | 2024-04-16 | 2 | -8/+4 |
| | | | |||||
* | | | Merge pull request #147 from AeneasVerif/binops-simplification | Son HO | 2024-04-18 | 4 | -478/+171 |
|\ \ \ | |_|/ |/| | | Bump charon | ||||
| * | | Bump charon | Nadrieril | 2024-04-17 | 4 | -478/+171 |
|/ / | |||||
* | | 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 |
| | | | | | |