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
*
Add strip_subst_local
Jason Gross
2017-10-15
*
Add pow_ceil_mul_nat_divide_upperbound
Jason Gross
2017-10-13
*
Add reflective compose, notation for Z.Syntax.{Expr,Interp}
Jason Gross
2017-10-12
*
Add update_by_tac_if_not_exists
Jason Gross
2017-10-10
*
TagList: make get error, and fix bugs
Jason Gross
2017-10-10
*
Add TagList
Jason Gross
2017-10-10
*
Add notations
Jason Gross
2017-10-10
*
Add pow_ceil_mul_nat_nonneg
Jason Gross
2017-10-05
*
Add PoseTermWithName
Jason Gross
2017-10-05
*
Add some ZUtil lemmas
Jason Gross
2017-10-03
*
Add decidable equality with nil
Jason Gross
2017-08-13
*
Make some tactics a bit more powerful
Jason Gross
2017-07-08
*
More fine-grained tactics imports
Jason Gross
2017-07-08
*
More fine-grained imports
Jason Gross
2017-07-08
*
Add UnfoldArg
Jason Gross
2017-07-08
*
prove an admit in ArithmeticSynthesisTest
Andres Erbsen
2017-07-06
*
Add wrappers for subborrow and add_with_get_carry so they work when it is not...
jadep
2017-06-29
*
remove unused admit (has been moved to Tuple.v)
jadep
2017-06-26
*
Prove map2_append
Jason Gross
2017-06-25
*
write and prove Tuple.map2_cps
jadep
2017-06-25
*
Fix a typo in push_Zmod that was causing looping
Jason Gross
2017-06-22
*
Fix some minor naming bugs in sig_assoc tactics
Jason Gross
2017-06-22
*
src/Demo.v: a 200-line introduction to BaseSystem ideas
Andres Erbsen
2017-06-21
*
Prove In_to_list_left_tl, In_left_hd, to_list_left_append
Jason Gross
2017-06-21
*
Add is_bounded_by_None_repeat_In_iff_lt
Jason Gross
2017-06-20
*
Add fold_left_orb_true, fold_left_orb_pull
Jason Gross
2017-06-20
*
Add is_bounded_by_None_repeat_In_iff
Jason Gross
2017-06-20
*
[Require NatUtil] should not change [tauto]
Jason Gross
2017-06-19
*
Add ModInv
Jason Gross
2017-06-18
*
Stronger zero_bounds
Jason Gross
2017-06-18
*
Add div_nonneg to zarith
Jason Gross
2017-06-18
*
Add Z.div_nonneg
Jason Gross
2017-06-18
*
Add eq_ZToWord
Jason Gross
2017-06-17
*
Unfold Z.mul_split_at_bitwidth for reification
Jason Gross
2017-06-17
*
finish tuple-ifying Montgomery API
jadep
2017-06-16
*
CPSify Saturated API in preparation for CPSifying Montgomery (see #194)
jadep
2017-06-15
*
Don't force [Require Import String] for debug msgs
Jason Gross
2017-06-15
*
Fix a changed case in the proof in loop.v
Jason Gross
2017-06-15
*
Better for_loop induction principle
Jason Gross
2017-06-15
*
Export ZUtil.Z2Nat in ZUtil
Jason Gross
2017-06-15
*
Add ZUtil.Z2Nat
Jason Gross
2017-06-15
*
Add for_cps_unroll1
Jason Gross
2017-06-15
*
Add eq_loop_cps_large_n
Jason Gross
2017-06-15
*
move CPS notations to Util.CPSNotations
Andres Erbsen
2017-06-15
*
Loop changes, ScalarMultBase_correct with admits
Andres Erbsen
2017-06-14
*
loops WIP
Andres Erbsen
2017-06-14
*
ScalarMult: Z -> G -> G (closes #193)
Andres Erbsen
2017-06-14
*
Add mul_split_at_bitwidth, define things in terms of that
Jason Gross
2017-06-13
*
Add Z.peano_rect_strong
Jason Gross
2017-06-13
*
Add dec_eq_comparison
Jason Gross
2017-06-13
[next]