Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Fix an issue with the extraction of aggregated arrays | Son Ho | 2023-08-03 | 10 | -180/+320 |
| | |||||
* | Make a minor formatting modification for Lean | Son Ho | 2023-08-03 | 15 | -1/+15 |
| | |||||
* | Update the Makefile to add the array test | Son Ho | 2023-08-03 | 1 | -1/+16 |
| | |||||
* | Fix issues | Son Ho | 2023-08-03 | 11 | -57/+140 |
| | |||||
* | Make minor modifications | Son Ho | 2023-08-02 | 3 | -16/+29 |
| | |||||
* | Add the function signatures in Assumed.ml | Son Ho | 2023-08-02 | 1 | -0/+143 |
| | |||||
* | Make more progress | Son Ho | 2023-08-02 | 2 | -75/+186 |
| | |||||
* | Make progress | Son Ho | 2023-08-02 | 5 | -53/+80 |
| | |||||
* | Make progress | Son Ho | 2023-08-02 | 14 | -76/+178 |
| | |||||
* | Make progress | Son Ho | 2023-08-02 | 7 | -164/+232 |
| | |||||
* | Make progress proapagating the changes | Son Ho | 2023-08-02 | 25 | -273/+407 |
| | |||||
* | Start adding support for const generics | Son Ho | 2023-08-01 | 11 | -226/+246 |
| | |||||
* | Merge pull request #31 from AeneasVerif/son_lean_backend | Son HO | 2023-07-31 | 160 | -10464/+11401 |
|\ | | | | | Improve the Lean backend | ||||
| * | Make minor modifications | Son Ho | 2023-07-31 | 1 | -0/+9 |
| | | |||||
| * | Make minor modifications | Son Ho | 2023-07-26 | 1 | -3/+2 |
| | | |||||
| * | Make a minor modification to a hashmap proof | Son Ho | 2023-07-26 | 1 | -5/+9 |
| | | |||||
| * | Update some of the Vec function specs | Son Ho | 2023-07-26 | 3 | -25/+40 |
| | | |||||
| * | Update the syntax of the progress tactic | Son Ho | 2023-07-26 | 5 | -111/+117 |
| | | |||||
| * | Fix a proof for the hashmap | Son Ho | 2023-07-26 | 1 | -5/+12 |
| | | |||||
| * | Make progress on the proofs of the hashmap | Son Ho | 2023-07-25 | 2 | -22/+83 |
| | | |||||
| * | Make progress on the proofs of the hashmap | Son Ho | 2023-07-25 | 7 | -34/+216 |
| | | |||||
| * | Make progress on the hashmap properties | Son Ho | 2023-07-25 | 8 | -29/+141 |
| | | |||||
| * | Improve int_tac and scalar_tac | Son Ho | 2023-07-25 | 5 | -32/+87 |
| | | |||||
| * | Add the possibility of using "_" as ident for progress | Son Ho | 2023-07-25 | 2 | -18/+26 |
| | | |||||
| * | Improve the syntax of progress: `as ⟨ x, y .. ⟩` | Son Ho | 2023-07-25 | 3 | -74/+98 |
| | | |||||
| * | Improve the interactivity of some hashmap proofs | Son Ho | 2023-07-20 | 1 | -75/+34 |
| | | |||||
| * | Fix a naming issue with progress | Son Ho | 2023-07-20 | 1 | -4/+4 |
| | | |||||
| * | Make progress on some of the hashmap proofs | Son Ho | 2023-07-20 | 2 | -48/+149 |
| | | |||||
| * | Make some proofs in Hashmap/Properties.lean and improve progress | Son Ho | 2023-07-20 | 5 | -74/+129 |
| | | |||||
| * | Improve progress further and move some lemmas | Son Ho | 2023-07-20 | 3 | -105/+109 |
| | | |||||
| * | Add fine-grained lemmas for the arithmetic operations | Son Ho | 2023-07-20 | 2 | -8/+131 |
| | | |||||
| * | Improve progress further | Son Ho | 2023-07-20 | 2 | -72/+142 |
| | | |||||
| * | Fix a small issue with the persistent state of progress | Son Ho | 2023-07-19 | 2 | -5/+13 |
| | | |||||
| * | Add some utilities for progress | Son Ho | 2023-07-19 | 2 | -5/+35 |
| | | |||||
| * | Add arithmetic spec lemmas | Son Ho | 2023-07-19 | 1 | -6/+161 |
| | | |||||
| * | Start implementing support for some type classes for progress | Son Ho | 2023-07-19 | 2 | -25/+117 |
| | | |||||
| * | Cleanup more | Son Ho | 2023-07-19 | 1 | -3/+0 |
| | | |||||
| * | Cleanup a bit | Son Ho | 2023-07-19 | 1 | -2/+0 |
| | | |||||
| * | Improve progress | Son Ho | 2023-07-19 | 4 | -45/+131 |
| | | |||||
| * | Move an arithmetic lemma | Son Ho | 2023-07-18 | 2 | -10/+10 |
| | | |||||
| * | Make modifications to Vec.lean | Son Ho | 2023-07-18 | 1 | -3/+5 |
| | | |||||
| * | Improve progress | Son Ho | 2023-07-18 | 4 | -18/+32 |
| | | |||||
| * | Make minor modifications | Son Ho | 2023-07-17 | 1 | -25/+0 |
| | | |||||
| * | Start proving theorems for primitive definitions | Son Ho | 2023-07-17 | 6 | -50/+116 |
| | | |||||
| * | Reorganize the Lean backend | Son Ho | 2023-07-17 | 11 | -1171/+1184 |
| | | |||||
| * | With @sonmarcho, some Lean proofs for hashmaps + comments about possible ↵ | Aymeric Fromherz | 2023-07-17 | 2 | -0/+196 |
| | | | | | | | | improvements | ||||
| * | Move a definition | Son Ho | 2023-07-17 | 2 | -3/+3 |
| | | |||||
| * | Update the lean dependencies and update IList | Son Ho | 2023-07-17 | 7 | -14/+17 |
| | | |||||
| * | Update a comment | Son Ho | 2023-07-13 | 1 | -2/+1 |
| | | |||||
| * | Add IList.lean | Son Ho | 2023-07-13 | 4 | -64/+242 |
| | |