index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
Add a couple more identifiers to support eager rec
Jason Gross
2019-03-07
*
Add some Proper lemmas to ListUtil
Jason Gross
2019-03-07
*
Only write to .c files on success
Jason Gross
2019-03-07
*
Update .out files
Jason Gross
2019-03-07
*
Reify most rewrite rules
Jason Gross
2019-03-07
*
Fix reification of interpreted idents
Jason Gross
2019-03-06
*
Add support for reifying fancy identifiers
Jason Gross
2019-03-06
*
Add reserved notations for \in
Jason Gross
2019-03-05
*
Allow reifying Z.cast2
Jason Gross
2019-03-05
*
Fix unfolding of pattern.base.lookup_default
Jason Gross
2019-03-05
*
Actually fix reification of literals
Jason Gross
2019-03-05
*
Revert "Fix reification of literals"
Jason Gross
2019-03-05
*
Fix reification of literals
Jason Gross
2019-03-05
*
Add UnderLets.flat_map
Jason Gross
2019-03-05
*
Fix another instance of reduction
Jason Gross
2019-03-04
*
Fix reduction
Jason Gross
2019-03-04
*
Fix an issue with a proof from the previous commit
Jason Gross
2019-03-04
*
Add some things to GENERATED rewriter file
Jason Gross
2019-03-04
*
Allow reifying cast and literals
Jason Gross
2019-03-04
*
Add some minor reflect things
Jason Gross
2019-03-04
*
Add back build status indicator to README.md
Jason Gross
2019-03-04
*
Make [reflect] a typeclass and add a bunch of lemmas
Jason Gross
2019-03-04
*
Update a proof to work with previous commit
Jason Gross
2019-02-27
*
Add UnderLets.map
Jason Gross
2019-02-27
*
finish porting barrett and montgomery code to new glue style
jadep
2019-02-21
*
adapt barrett to new glue code
jadep
2019-02-21
*
Make Qed not take forever
jadep
2019-02-21
*
start adapting Montgomery to new glue code
jadep
2019-02-21
*
Add base.{base_,}interp_beq
Jason Gross
2019-02-20
*
Update .out files
Jason Gross
2019-02-18
*
Add support for reifying `zrange` and `option`
Jason Gross
2019-02-18
*
fix cast admits in Fancy
jadep
2019-02-15
*
Fix missing "= true" in a tactic so [Admitted] is unneccesary.
jadep
2019-02-15
*
Add Option.{lift,map,combine}, List.Option.lift
Jason Gross
2019-02-11
*
Insert casts before literals during bounds analysis
Jason Gross
2019-02-11
*
Rename p484_64.c to p434_64.c (fix typo)
Daniel Hirche
2019-02-11
*
clean up and factor out cast-admit so that [Print Assumptions] is more fine-g...
jadep
2019-02-08
*
cleanup
jadep
2019-02-08
*
remove some TODOs -- actually, the final proof does not rely on the unused va...
jadep
2019-02-08
*
fix Montgomery proof and clean up a little
jadep
2019-02-08
*
remove 2: syntax so 8.7 builds
jadep
2019-02-07
*
Fix instruction-order admit; still neads cleanup
jadep
2019-02-07
*
Use Preconditions: Postconditions:, rather than /\ and ->
Jason Gross
2019-02-02
*
More minor improvements in docstrings
Jason Gross
2019-02-02
*
Rename docstring generator based on Andres' suggestion
Jason Gross
2019-02-02
*
Update with davidben's and Andres' suggestions
Jason Gross
2019-02-02
*
Drop `map λ` bits in docstrings
Jason Gross
2019-02-02
*
Address code review comments to improve docstrings
Jason Gross
2019-02-02
*
Add autogenerated docstrings to synthesized code
Jason Gross
2019-02-02
*
Add zrange_rect{,_Proper,_Proper_dep}
Jason Gross
2019-02-02
[prev]
[next]