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
...
*
Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtil
Jason Gross
2018-08-23
*
Add more absint proofs
Jason Gross
2018-08-21
*
Add more operation-specific proofs
Jason Gross
2018-08-21
*
Do most of abs-int interp proofs
Jason Gross
2018-08-21
*
Revert "Revert "Add more instances for type.related""
Jason Gross
2018-08-20
*
Revert "Add more instances for type.related"
Jason Gross
2018-08-17
*
Be more judicious about an instance
Jason Gross
2018-08-17
*
Add and_eqv_for_each_lhs_of_arrow_not_higher_order
Jason Gross
2018-08-16
*
Add andb_each_lhs_of_arrow
Jason Gross
2018-08-16
*
Add more instances for type.related
Jason Gross
2018-08-16
*
Fix bounds on n_corners_and_zero
Jason Gross
2018-08-16
*
Prove monotonicity properties about zrange
Jason Gross
2018-08-15
*
Fix another proof broken by wrong behavior of cbn
Jason Gross
2018-08-14
*
Fix a proof broken by wrong behavior of cbn
Jason Gross
2018-08-14
*
Add more zutil morphisms
Jason Gross
2018-08-13
*
Fix some bounds analysis
Jason Gross
2018-08-13
*
Add some Z.le Proper hints to zarith
Jason Gross
2018-08-13
*
Fix previous commit
Jason Gross
2018-08-13
*
Move a lemma
Jason Gross
2018-08-13
*
Fix a wrong bound computation (on negatives), fix a proof
Jason Gross
2018-08-13
*
Add the file proving split_bounds correct
Jason Gross
2018-08-13
*
Fix split_bounds, prove it correct
Jason Gross
2018-08-13
*
Factor through is_tighter_than_bool, add is_bounded_by_bool_Proper_if_sumbool...
Jason Gross
2018-08-13
*
Add some util lemmas
Jason Gross
2018-08-13
*
Finish and enable rule-specific rewriter wf proofs
Jason Gross
2018-08-13
*
Finish rule-specific rewriter wf proofs
Jason Gross
2018-08-13
*
Improvements in rewrite-rule-specific proofs
Jason Gross
2018-08-13
*
Split up rewrite rules proofs into multiple files
Jason Gross
2018-08-13
*
Prove rewrite-rule-independent parts of rewrite Wf
Jason Gross
2018-08-13
*
Don't guarantee anything about casting outside of range
Jason Gross
2018-08-10
*
Add related_hetero_iff_app_curried
Jason Gross
2018-08-10
*
Add ListUtil.map_nth_default_seq
Jason Gross
2018-08-10
*
Make Prod.eta_expand also work in the context
Jason Gross
2018-08-10
*
Better transport lemmas in LanguageInversion
Jason Gross
2018-08-09
*
Add ListUtil.{combine_repeat,combine_rev_rev_samelength}
Jason Gross
2018-08-09
*
Improve the power of split_andb
Jason Gross
2018-08-09
*
Don't fuse annotations
Jason Gross
2018-08-09
*
Add more interp lemmas
Jason Gross
2018-08-09
*
Push back admits in interp lemmas
Jason Gross
2018-08-08
*
Add Wf_of_Wf3
Jason Gross
2018-08-08
*
Reserve 'n notation in Notations.v
Jason Gross
2018-08-08
*
Add some partial interp proofs for abs-int
Jason Gross
2018-08-08
*
Add lemmas about type.and_for_each_lhs_of_arrow
Jason Gross
2018-08-07
*
Finish relax interp proofs
Jason Gross
2018-08-07
*
Add another GeneralizeVar pass to add support for using Wf3
Jason Gross
2018-08-07
*
Fix an issue with the previous commit
Jason Gross
2018-08-07
*
Add Proof using to arithmetic proofs
Jason Gross
2018-08-07
*
Add type.related_hetero3
Jason Gross
2018-08-06
*
Start setting up abs-int interp proofs
Jason Gross
2018-08-06
*
Add gen_interp_Proper
Jason Gross
2018-08-06
[prev]
[next]