aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Collapse)AuthorAge
* Add ap_transport to Equality.vGravatar Jason Gross2017-04-02
|
* Coalesce Tuple.pointwise2 and Tuple.fieldwiseGravatar Jason Gross2017-04-02
| | | | | | We don't need both of them. We keep the definition of pointwise2 because it's needed for reification to work, and we keep the name of fieldwise because it's used in more places. This closes #137.
* Fix definition of BoundedWordGravatar Jason Gross2017-04-01
| | | | | | | We need to take log2, because wordT takes lg(wordsize). We need to pass None rather than Some, because None means "the original output type of the function we're reifying is a tuple of Z" (as opposed to a tuple of words), which is the situation we're in.
* Split off BoundedWord.v from IntegrationTest.vGravatar Jason Gross2017-04-01
|
* Split out Tactics.SubstLetGravatar Jason Gross2017-04-01
|
* Add Tuple.etaGravatar Jason Gross2017-04-01
|
* Add Z.log2_up_le_pow2_fullGravatar Jason Gross2017-03-31
|
* Add is_tighter_than_bool to zrangeGravatar Jason Gross2017-03-31
|
* More compatibility for etransitivityGravatar Jason Gross2017-03-31
|
* Add [change_with_curried] to Curry.vGravatar Jason Gross2017-03-31
|
* Add [etransitivity y], [etransitivity_rev] tacticsGravatar Jason Gross2017-03-31
|
* Add wordToZ{_gen,}_rangeGravatar Jason Gross2017-03-30
|
* added tuple [repeat]Gravatar jadep2017-03-30
|
* Use r[_ ~> _] for range rather than b[_ ~> _]Gravatar Jason Gross2017-03-30
|
* Rename Bounds to ZRange, use Prop, not boolGravatar Jason Gross2017-03-30
| | | | | | As per @andres-erbsen's comments at https://github.com/mit-plv/fiat-crypto/commit/ba864554da71ebe20b2494b1e8adf04779cd904b#commitcomment-21565223, https://github.com/mit-plv/fiat-crypto/commit/ba864554da71ebe20b2494b1e8adf04779cd904b#commitcomment-21565200
* Get rid of list-based Tuple.mapGravatar Jason Gross2017-03-30
|
* Add a file dedicated to the definition of Z boundsGravatar Jason Gross2017-03-30
|
* Add Tuple.pointwise2, Tuple.map_fixGravatar Jason Gross2017-03-30
| | | | These are for definining boundedness and lining up judgmentally with reflective things
* remove commented-out lemma and add CPS version of mapi_withGravatar jadep2017-03-29
|
* change map_with to mapi_with, a version that handles the index explicitlyGravatar jadep2017-03-29
|
* Add Z.one_succ Z.two_succ to zsimplify_const dbGravatar Jason Gross2017-03-28
|
* Don't reserve '(max_bitwidth'Gravatar Jason Gross2017-03-28
|
* Add a notation for printingGravatar Jason Gross2017-03-28
|
* Add lemmas needed for saturated arithmetic [compact]Gravatar jadep2017-03-24
|
* Split off extra power of ltb_to_lt, split_andbGravatar Jason Gross2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This should make the build faster. After | File Name | Before || Change ----------------------------------------------------------------------------------------------------------- 12m23.36s | Total | 19m19.28s || -6m55.91s ----------------------------------------------------------------------------------------------------------- 0m30.37s | Specific/GF25519Bounded | 4m13.77s || -3m43.40s 0m05.10s | Specific/GF25519Reflective/CommonBinOp | 1m03.15s || -0m58.04s 0m04.12s | Specific/GF25519Reflective/CommonUnOp | 0m41.26s || -0m37.14s 0m03.87s | Specific/GF25519Reflective/CommonUnOpWireToFE | 0m36.38s || -0m32.51s 0m02.84s | Specific/GF25519Reflective/CommonUnOpFEToWire | 0m28.09s || -0m25.25s 0m07.65s | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m17.70s || -0m10.04s 0m22.28s | Reflection/Z/Interpretations128/Relations | 0m31.68s || -0m09.39s 0m18.82s | Reflection/Z/Interpretations64/Relations | 0m27.99s || -0m09.16s 0m02.55s | BoundedArithmetic/Double/Proofs/ShiftLeft | 0m06.03s || -0m03.48s 0m06.86s | Reflection/Z/InterpretationsGen | 0m08.87s || -0m02.00s 0m02.55s | BoundedArithmetic/Double/Proofs/ShiftRight | 0m04.69s || -0m02.14s 0m30.47s | ModularArithmetic/ModularBaseSystemProofs | 0m31.67s || -0m01.20s 0m08.77s | Specific/GF25519BoundedCommon | 0m10.43s || -0m01.66s 0m03.07s | ModularArithmetic/ZBoundedZ | 0m04.16s || -0m01.09s 1m29.26s | Test/Curve25519SpecTestVectors | 1m29.49s || -0m00.22s 0m47.87s | Specific/GF25519Reflective/Reified/LadderStep | 0m47.14s || +0m00.72s 0m38.92s | ModularArithmetic/Conversion | 0m39.24s || -0m00.32s 0m36.94s | Spec/Ed25519 | 0m36.07s || +0m00.86s 0m34.26s | Specific/GF25519Reflective/Reified/AddCoordinates | 0m34.09s || +0m00.16s 0m21.21s | ModularArithmetic/Pow2BaseProofs | 0m21.29s || -0m00.07s 0m19.58s | Specific/GF25519 | 0m19.52s || +0m00.05s 0m18.22s | EdDSARepChange | 0m18.44s || -0m00.22s 0m14.71s | Util/ZUtil | 0m14.78s || -0m00.06s 0m14.22s | Reflection/Named/MapCastWf | 0m14.17s || +0m00.05s 0m11.62s | Specific/NewBaseSystemTest | 0m11.50s || +0m00.11s 0m11.13s | Specific/GF25519Reflective/Reified/Mul | 0m11.02s || +0m00.11s 0m11.07s | Experiments/Ed25519 | 0m10.75s || +0m00.32s 0m09.92s | Testbit | 0m09.85s || +0m00.07s 0m08.73s | Reflection/Named/MapCastInterp | 0m08.68s || +0m00.05s 0m08.70s | Assembly/GF25519 | 0m08.70s || +0m00.00s 0m08.67s | ModularArithmetic/Montgomery/ZProofs | 0m09.23s || -0m00.56s 0m08.38s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.50s || -0m00.11s 0m08.18s | BoundedArithmetic/Double/Proofs/Multiply | 0m08.24s || -0m00.06s 0m06.64s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate | 0m06.82s || -0m00.18s 0m06.34s | Specific/GF1305 | 0m06.34s || +0m00.00s 0m06.08s | NewBaseSystem | 0m06.13s || -0m00.04s 0m05.96s | Util/FixedWordSizesEquality | 0m05.87s || +0m00.08s 0m05.72s | Specific/GF25519Reflective/Reified/PreFreeze | 0m05.73s || -0m00.01s 0m05.47s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub | 0m05.42s || +0m00.04s 0m05.22s | Specific/GF25519Reflective/Reified/CarrySub | 0m05.42s || -0m00.20s 0m04.94s | Specific/GF25519Reflective/Reified/CarryAdd | 0m04.90s || +0m00.04s 0m04.91s | Specific/SC25519 | 0m04.95s || -0m00.04s 0m04.88s | ModularArithmetic/ModularBaseSystemListProofs | 0m04.95s || -0m00.07s 0m04.20s | Specific/GF25519Reflective/Common9_4Op | 0m04.10s || +0m00.10s 0m03.89s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.97s || -0m00.08s 0m03.79s | BaseSystemProofs | 0m03.81s || -0m00.02s 0m03.73s | Specific/GF25519Reflective/Reified/CarryOpp | 0m03.80s || -0m00.06s 0m03.51s | Specific/GF25519Reflective/Reified/Sub | 0m03.56s || -0m00.05s 0m03.39s | BoundedArithmetic/InterfaceProofs | 0m03.53s || -0m00.13s 0m03.12s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m03.19s || -0m00.06s 0m02.97s | Specific/GF25519Reflective/Reified/Add | 0m03.16s || -0m00.18s 0m02.94s | ModularArithmetic/ModularArithmeticTheorems | 0m02.86s || +0m00.08s 0m02.78s | Specific/FancyMachine256/Barrett | 0m02.72s || +0m00.05s 0m02.77s | Specific/GF25519ReflectiveAddCoordinates | 0m02.80s || -0m00.02s 0m02.77s | Specific/FancyMachine256/Montgomery | 0m02.86s || -0m00.08s 0m02.75s | Specific/GF25519Reflective/Reified/Pack | 0m02.67s || +0m00.08s 0m02.67s | BoundedArithmetic/Double/Proofs/Decode | 0m02.66s || +0m00.00s 0m02.54s | Specific/GF25519Reflective/Reified/Unpack | 0m02.44s || +0m00.10s 0m02.38s | Specific/GF25519Reflective/Reified/Opp | 0m02.36s || +0m00.02s 0m02.38s | ModularArithmetic/ModularBaseSystemOpt | 0m02.18s || +0m00.19s 0m02.27s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.35s || -0m00.08s 0m02.20s | Reflection/TestCase | 0m02.33s || -0m00.12s 0m02.15s | Specific/GF25519Reflective/Reified/GeModulus | 0m02.05s || +0m00.10s 0m01.98s | Util/WordUtil | 0m02.02s || -0m00.04s 0m01.96s | Assembly/Evaluables | 0m01.96s || +0m00.00s 0m01.88s | Specific/FancyMachine256/Core | 0m01.88s || +0m00.00s 0m01.77s | ModularArithmetic/Montgomery/ZBounded | 0m01.83s || -0m00.06s 0m01.58s | Specific/GF25519Reflective | 0m01.45s || +0m00.13s 0m01.54s | Specific/GF25519Reflective/Common | 0m01.50s || +0m00.04s 0m01.51s | ModularArithmetic/PrimeFieldTheorems | 0m01.44s || +0m00.07s 0m01.50s | Assembly/Compile | 0m01.50s || +0m00.00s 0m01.45s | ModularArithmetic/BarrettReduction/Z | 0m01.48s || -0m00.03s 0m01.28s | Reflection/Z/Syntax/Equality | 0m01.28s || +0m00.00s 0m01.26s | Experiments/Ed25519Extraction | 0m01.28s || -0m00.02s 0m01.24s | Assembly/Conversions | 0m01.12s || +0m00.11s 0m01.22s | Reflection/Z/Interpretations64/RelationsCombinations | 0m01.20s || +0m00.02s 0m01.21s | ModularArithmetic/ExtendedBaseVector | 0m01.15s || +0m00.06s 0m01.21s | Reflection/Z/Interpretations128/RelationsCombinations | 0m01.32s || -0m00.11s 0m01.20s | BaseSystem | 0m01.27s || -0m00.07s 0m01.12s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.03s || +0m00.09s 0m01.10s | Specific/GF25519Reflective/CommonUnOpFEToZ | 0m01.11s || -0m00.01s 0m00.99s | Util/NumTheoryUtil | 0m01.03s || -0m00.04s 0m00.98s | Assembly/HL | 0m00.94s || +0m00.04s 0m00.96s | Assembly/LL | 0m01.00s || -0m00.04s 0m00.94s | Assembly/Pipeline | 0m00.90s || +0m00.03s 0m00.92s | BoundedArithmetic/Double/Proofs/LoadImmediate | 0m00.92s || +0m00.00s 0m00.88s | Specific/GF25519Reflective/Reified | 0m00.72s || +0m00.16s 0m00.83s | Karatsuba | 0m00.94s || -0m00.10s 0m00.82s | Util/IterAssocOp | 0m00.84s || -0m00.02s 0m00.82s | BoundedArithmetic/Double/Proofs/BitwiseOr | 0m00.99s || -0m00.17s 0m00.80s | BoundedArithmetic/X86ToZLikeProofs | 0m00.83s || -0m00.02s 0m00.79s | Assembly/PhoasCommon | 0m00.93s || -0m00.14s 0m00.76s | Specific/GF25519BoundedAddCoordinates | 0m00.79s || -0m00.03s 0m00.75s | ModularArithmetic/ModularBaseSystemList | 0m00.64s || +0m00.10s 0m00.72s | Encoding/ModularWordEncodingTheorems | 0m00.67s || +0m00.04s 0m00.72s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.67s || +0m00.04s 0m00.70s | Reflection/MapCastByDeBruijnInterp | 0m00.64s || +0m00.05s 0m00.68s | ModularArithmetic/ModularBaseSystem | 0m00.67s || +0m00.01s 0m00.67s | BoundedArithmetic/Interface | 0m00.64s || +0m00.03s 0m00.67s | Spec/EdDSA | 0m00.68s || -0m00.01s 0m00.65s | BoundedArithmetic/X86ToZLike | 0m00.55s || +0m00.09s 0m00.63s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.70s || -0m00.06s 0m00.61s | Encoding/ModularWordEncodingPre | 0m00.74s || -0m00.13s 0m00.61s | BoundedArithmetic/Double/Proofs/SelectConditional | 0m00.60s || +0m00.01s 0m00.60s | BoundedArithmetic/Double/Repeated/Proofs/Multiply | 0m00.68s || -0m00.08s 0m00.59s | Spec/ModularWordEncoding | 0m00.58s || +0m00.01s 0m00.56s | Util/NUtil | 0m00.58s || -0m00.01s 0m00.56s | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight | 0m00.48s || +0m00.08s 0m00.54s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.45s || +0m00.09s 0m00.53s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.46s || +0m00.07s 0m00.53s | Reflection/MapCastByDeBruijnWf | 0m00.53s || +0m00.00s 0m00.50s | BoundedArithmetic/ArchitectureToZLike | 0m00.41s || +0m00.09s 0m00.50s | BoundedArithmetic/Double/Repeated/Core | 0m00.47s || +0m00.03s 0m00.50s | BoundedArithmetic/Eta | 0m00.44s || +0m00.06s 0m00.49s | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.52s || -0m00.03s 0m00.49s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.56s || -0m00.07s 0m00.48s | BoundedArithmetic/Double/Core | 0m00.49s || -0m00.01s 0m00.48s | Reflection/Z/Interpretations128 | 0m00.45s || +0m00.02s 0m00.47s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.50s || -0m00.03s 0m00.47s | ModularArithmetic/ModularBaseSystemListZOperationsProofs | 0m00.37s || +0m00.09s 0m00.46s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.38s || +0m00.08s 0m00.46s | BoundedArithmetic/StripCF | 0m00.44s || +0m00.02s 0m00.46s | ModularArithmetic/Pre | 0m00.47s || -0m00.00s 0m00.46s | ModularArithmetic/ZBounded | 0m00.55s || -0m00.09s 0m00.45s | Reflection/Z/Reify | 0m00.48s || -0m00.02s 0m00.44s | ModularArithmetic/Montgomery/Z | 0m00.38s || +0m00.06s 0m00.42s | Reflection/Z/Interpretations64 | 0m00.42s || +0m00.00s 0m00.40s | ModularArithmetic/Pow2Base | 0m00.40s || +0m00.00s 0m00.40s | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic | 0m00.44s || -0m00.03s 0m00.39s | Reflection/Z/Syntax/Util | 0m00.38s || +0m00.01s 0m00.33s | Spec/ModularArithmetic | 0m00.43s || -0m00.09s 0m00.18s | Reflection/CommonSubexpressionElimination | 0m00.15s || +0m00.03s 0m00.05s | Util/Bool | 0m00.04s || +0m00.01s
* Remove a line I forgot to remove in the previous commitGravatar Jason Gross2017-03-21
|
* Split off the extra power of rewrite_mod_small into rewrite_mod_mod_smallGravatar Jason Gross2017-03-21
|
* Make Z.rewrite_mod_small a bit more powerfulGravatar Jason Gross2017-03-21
| | | | | Now it can handle things like ((x mod 4) mod 2) when we have (x mod 4 < 2) as a hypothesis.
* Make Bool.split_andb a bit more powerfulGravatar Jason Gross2017-03-21
|
* Make Z.ltb_to_lt a bit strongerGravatar Jason Gross2017-03-21
| | | | | | | | Now it works not just at top-level, but also in, e.g., arguments to hypotheses. We had to change some proofs because it no longer moves the hypotheses it changes to the bottom.
* Add {firstn,skipn}_seqGravatar Jason Gross2017-03-19
|
* generalize In_firstn_skipn_splitGravatar Jason Gross2017-03-19
|
* Add In_firstn_skipn_splitGravatar Jason Gross2017-03-19
|
* Add firstn_firstn_minGravatar Jason Gross2017-03-19
|
* Add dec_eq_positiveGravatar Jason Gross2017-03-17
|
* Fix a name clashGravatar Jason Gross2017-03-14
|
* Add firstn_skipnGravatar Jason Gross2017-03-14
|
* Add split_prodGravatar Jason Gross2017-03-14
|
* Add skipn_skipnGravatar Jason Gross2017-03-14
|
* Move find_if_eq to Decidable.v, use Decidable in NamedGravatar Jason Gross2017-03-14
|
* Add faster versions of destruct_head_*Gravatar Jason Gross2017-03-14
| | | | Sometimes, it's a performance bottleneck
* address some code review commentsGravatar Andres Erbsen2017-03-02
|
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
|
* Add η principles for sigma typesGravatar Jason Gross2017-03-01
|
* Add dlet_nd notationGravatar Jason Gross2017-03-01
| | | | This is for non-dependent [dlet]s, to help Coq's type inference
* Add strip_eta_tuple lemmasGravatar Jason Gross2017-02-28
|
* Better tuple_eta argumentsGravatar Jason Gross2017-02-28
|
* Add eta_tuple functionsGravatar Jason Gross2017-02-28
| | | | | These are for getting nicely reduced forms of, e.g., Tuple.map, without knowing exactly what the tuple is
* Added operation (including creating )Gravatar jadep2017-02-27
|
* added Positional wrappers for Associational operations, added correctness ↵Gravatar jadep2017-02-27
| | | | proof of
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 15:44:20 +0000