index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
Commit message (
Expand
)
Author
Age
...
*
Improve rewriter speed
Jason Gross
2018-07-25
*
Add option sequencing/return
Jason Gross
2018-07-25
*
Reserve ;;;, fix level of prefix # to not clash with infix #
Jason Gross
2018-07-25
*
Revert "Improve rewriter speed"
Jason Gross
2018-07-24
*
Improve rewriter speed
Jason Gross
2018-07-24
*
Add ListUtil.{take,drop}_while
Jason Gross
2018-07-24
*
Montgomery reduction in new pipeline
Jason Gross
2018-07-21
*
Support reification of firstn, skipn
Jason Gross
2018-07-18
*
Make Z.modinv run on wf proofs
Jason Gross
2018-07-18
*
vm_compute in peel_interp_app
Jason Gross
2018-07-18
*
Thunk nat_rect for better perf, list_{rect=>case}
Jason Gross
2018-07-17
*
Handle Z.pow in push_Zmod tactic
Jason Gross
2018-07-17
*
Remove a lemma that's been moved to NatUtil
Jason Gross
2018-07-17
*
Handle Z.pow in {push,pull}_Zmod
Jason Gross
2018-07-17
*
Add minor lemmas to util
Jason Gross
2018-07-17
*
Allow reification of nat_rect (fun _ => _ -> _)
Jason Gross
2018-07-15
*
Add a stronger version of eval_reduce
Jason Gross
2018-07-14
*
Partial adaptation to https://github.com/coq/coq/pull/8063
Jason Gross
2018-07-14
*
Better error message printing
Jason Gross
2018-07-12
*
Remove useless dependency
Jason Gross
2018-07-12
*
Make Z.div_mod_to_quot_rem stronger
Jason Gross
2018-07-10
*
Allow printing more easily readable code in errors
Jason Gross
2018-07-09
*
Prove that to_bytesmod partitions
Jason Gross
2018-07-08
*
Shuffle some ZUtil lemmas around
Jason Gross
2018-07-08
*
Fix an infinite loop in Z.peel_le
Jason Gross
2018-07-06
*
Factor eval_reduce_square_exact a bit differently
Jason Gross
2018-07-03
*
Remove nested proofs
Jason Gross
2018-07-03
*
Fix hints, hopefully
Jason Gross
2018-07-03
*
clean
Jason Gross
2018-07-03
*
Finish reduce_square proof
Jason Gross
2018-07-03
*
Try to fix square again
Jason Gross
2018-07-03
*
Fix a typo, start on proof
Jason Gross
2018-07-03
*
Fix a reification issue
Jason Gross
2018-07-03
*
Try a different reduce_square
Jason Gross
2018-07-03
*
WIP better square
Jason Gross
2018-07-03
*
Fix missing arg
Jason Gross
2018-07-03
*
Add missing space
Jason Gross
2018-07-03
*
Add support for annotating generated C functions with comments
Jason Gross
2018-07-03
*
Synthesize selectznz
Jason Gross
2018-07-03
*
Correctly reify match on prod
Jason Gross
2018-07-03
*
Add select
Jason Gross
2018-07-03
*
Comment out some code that's too slow
Jason Gross
2018-07-03
*
Allow passing functions to synthesize on the command line, and scmul for 25519
Jason Gross
2018-07-03
*
Pull out *2 in square, don't turn *2 into <<1
Jason Gross
2018-07-03
*
No subst01 in mulmod
Jason Gross
2018-07-03
*
Start with a better template for carry_square
Jason Gross
2018-07-03
*
Don't subst01 in square
Jason Gross
2018-07-03
*
synthesize square
Jason Gross
2018-07-03
*
static in c
Jason Gross
2018-07-03
*
static void
Jason Gross
2018-07-03
[prev]
[next]