summaryrefslogtreecommitdiff
path: root/backends (unfollow)
Commit message (Expand)AuthorFilesLines
2023-12-08Update the progress tactic to use discrimination treesSon Ho3-272/+175
2023-12-07Start working on a version of Diverge.FixI more suited to higher-order functionsSon Ho3-67/+510
2023-12-07Reorganize a bitSon Ho3-65/+94
2023-11-29Add support for more bitwise operations and update the extractionSon Ho3-10/+275
2023-11-21Update more namesSon Ho3-48/+48
2023-11-21Update the standard librariesSon Ho5-78/+85
2023-11-09Update the failing proofsSon Ho3-6/+40
2023-10-27Regenerate the Coq test filesSon Ho1-1/+1
2023-10-27Update Primitives.vSon Ho1-60/+342
2023-10-27Regenerate some of the F* test filesSon Ho1-2/+19
2023-10-26Update Primitives.fstSon Ho1-48/+318
2023-10-26Make progress on fixing the extractionSon Ho1-64/+64
2023-10-26Make progress on fixing the extraction for LeanSon Ho1-114/+50
2023-10-25Make the hashmap files typecheck again in LeanSon Ho4-33/+107
2023-10-25Fix some issues at extraction and add builtinsSon Ho7-23/+206
2023-10-24Handle properly the builtin, non fallible functionsSon Ho1-2/+2
2023-10-24Fix minor issuesSon Ho1-2/+2
2023-10-24Add definitions in for the Lean Primitives librarySon Ho3-0/+57
2023-10-22Add more support for numeric operations, xor, rotateJonathan Protzenko1-1/+22
2023-10-17Refold the scalar types when applying progressSon Ho4-16/+91
2023-10-17Implement tactics for termination proofs which involve arithmeticSon Ho4-21/+37
2023-10-16Improve formatting of scalars in LeanSon Ho1-0/+15
2023-10-13Update Primitives.fstSon Ho1-0/+3
2023-10-13Add supSon Ho3-1/+68
2023-09-18Prove that Vec is inhabitedSon Ho1-0/+4
2023-09-18Simplify some lemmas and prove that the scalars and Vec are inhabitedSon Ho2-9/+10
2023-09-18Add notations for the Isize.ofInt, etc.Son Ho1-0/+16
2023-09-18Add arithmetic lemmas in Scalar.leanSon Ho1-12/+179
2023-09-18Improve scalar_tacSon Ho3-56/+36
2023-09-18Fix an issue when loading the saved theorem maps for the progress tacticSon Ho2-3/+68
2023-09-14Fix the hashmap proofs in LeanSon Ho2-7/+8
2023-09-14Fix panic issues with the progress tacticSon Ho1-3/+5
2023-09-14Update to Lean 4.0.0 and fix some broken proofsSon Ho7-38/+50
2023-09-07Fix some issuesSon Ho5-34/+221
2023-09-07Map some globals like u32::MAX to standard definitionsSon Ho1-0/+42
2023-08-04Update the Makefile and regenerate the test filesSon Ho1-1/+0
2023-08-04Fix issues with the extraction and extend the primitive libraries for Coq and F*Son Ho3-20/+139
2023-08-04Make minor modificationsSon Ho1-4/+4
2023-08-04Add SliceLen as a primitive function and make minor adjustmentsSon Ho1-42/+38
2023-08-04Add the UtilsBase.lean fileSon Ho1-0/+10
2023-08-04Start adding support for Arrays/Slices in the Lean librarySon Ho8-39/+680
2023-07-26Update some of the Vec function specsSon Ho2-9/+21
2023-07-26Update the syntax of the progress tacticSon Ho4-25/+32
2023-07-25Make progress on the proofs of the hashmapSon Ho1-4/+43
2023-07-25Make progress on the proofs of the hashmapSon Ho6-30/+104
2023-07-25Make progress on the hashmap propertiesSon Ho7-29/+49
2023-07-25Improve int_tac and scalar_tacSon Ho5-32/+87
2023-07-25Add the possibility of using "_" as ident for progressSon Ho2-18/+26
2023-07-25Improve the syntax of progress: `as ⟨ x, y .. ⟩`Son Ho2-44/+94
2023-07-20Fix a naming issue with progressSon Ho1-4/+4
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 19:47:18 +0000