index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Util
Commit message (
Expand
)
Author
Age
*
reorganized lemmas; moved several to ListUtil and ZUtil.
Jade Philipoom
2015-11-24
*
Added base_succ precondition to BaseSystem to help prove carrying.
Jade Philipoom
2015-11-19
*
ModularBaseSystem: carry_rep has boring modular arithmetic proofs
Andres Erbsen
2015-11-17
*
ModularBaseSystem.carry: implement, state lemmas, some progress on proofs
Andres Erbsen
2015-11-17
*
BaseSystem: more boring
Andres Erbsen
2015-11-10
*
ModularBaseSystem: finished most admits for addition and multiplication, move...
Jade Philipoom
2015-11-09
*
ModularBaseSystem: prove some admits in mase system extension
Andres Erbsen
2015-11-07
*
ModularBaseSystem: continuing to prove base_good.
Jade Philipoom
2015-11-07
*
Merge remote-tracking branch 'jadep/master'
Andres Erbsen
2015-11-06
|
\
*
|
instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19)
Andres Erbsen
2015-11-06
|
*
Added lemmas to ListUtil and BaseSystem to help in ModularBaseSystem.
Jade Philipoom
2015-11-05
|
*
Relocated boring tactic to ListUtil and added combine_truncate lemma.
Jade Philipoom
2015-11-04
|
/
*
set_nth_splice case coverage
Andres Erbsen
2015-11-03
*
more set_nth
Andres Erbsen
2015-11-03
*
set_nth
Andres Erbsen
2015-11-01
*
BaseSystem to Util.ListUtil: separate out generic list lemmas
Andres Erbsen
2015-10-29