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
*
Finish rule-specific rewriter wf proofs
Jason Gross
2018-08-13
*
Improvements in rewrite-rule-specific proofs
Jason Gross
2018-08-13
*
Split up new-pipeline more
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
*
README: note remake_curves.sh is in Specific/CurveParameters
George Tankersley
2018-08-09
*
Improve the power of split_andb
Jason Gross
2018-08-09
*
[travis] Only run git diff on failure
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
*
Add app_curried_Proper_gen as an instance
Jason Gross
2018-08-06
*
Add related_iff_app_curried
Jason Gross
2018-08-06
*
Remove fastpath for Zcast in absint
Jason Gross
2018-08-06
*
Remove thunking from abstract interpretation
Jason Gross
2018-08-06
*
Generalize interp flat lemmas
Jason Gross
2018-08-06
*
Generalize wf_interp_Proper
Jason Gross
2018-08-06
*
Finish AbsInt Wf proofs
Jason Gross
2018-08-04
*
Move new-pipeline to its own stage
Jason Gross
2018-08-04
*
Backwards compatible fix for some issues from https://github.com/coq/coq/pull...
Jason Gross
2018-08-04
*
Add wf for DefaultValue
Jason Gross
2018-08-03
*
Add wf_splice_list, wf_splice_list_no_order
Jason Gross
2018-08-03
*
Fix typo in previous commit
Jason Gross
2018-08-03
*
Add eq_ident_Decidable
Jason Gross
2018-08-03
*
Add reflect_list_cps_id
Jason Gross
2018-08-03
*
Better rewrite_type_transport_correct
Jason Gross
2018-08-02
*
Adjust GENERATEDIdentifiersWithoutTypesProofs.v, add eta_ident_cps_correct
Jason Gross
2018-08-02
*
Add GENERATEDIdentifiersWithoutTypesProofs.v
Jason Gross
2018-08-02
*
Also generate decidable equality for pattern.ident
Jason Gross
2018-08-02
*
Make wf_safe_t a bit stronger
Jason Gross
2018-08-02
*
Make ERROR_BAD_REWRITE_RULE Opaque, not Qed'ed
Jason Gross
2018-08-02
*
Generalize option_eq to support heterogenous relations
Jason Gross
2018-08-02
*
Add nth_error_combine
Jason Gross
2018-08-01
[next]