| Commit message (Collapse) | Author | Age |
... | |
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is in preparation for dropping extra carries. What remains to be
done, after this and #106, is to finish packaging up the reified
[add_coordinates] so that it can operate on [Tuple.tuple
GF25519BoundedCommon.fe25519 4], and then to prove
```coq
forall twice_d P1 P2, Tuple.fieldwise GF25519BoundedCommon.eq
(<reflected add_coordinates> twice_d P1 P2)
(@ExtendedCoordinates.Extended.add_coordinates GF25519BoundedCommon.fe25519
GF25519Bounded.add GF25519Bounded.sub GF25519Bounded.mul twice_d
P1 P2)
```
I'm not sure how to do this, or even what the right structure for the
proof is.
|
|
|
|
| |
The lemma is currently admitted
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
Now the _correct_and_bounded lemma goes through
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
This will cancel out the timing increase of adding v8.5, v8.6.
I've never seen 8.5 and 8.5pl3 succeed, while either 8.5pl1, or 8.5pl2 failed
|
|
|
|
| |
Allow them to fail, though
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
| |
This is https://coq.inria.fr/bugs/show_bug.cgi?id=5205, Bogus "Error:
Wrong argument name: n." error message in 8.4, 8.5
|
| |
|
| |
|
|
|
|
| |
See https://coq.inria.fr/bugs/show_bug.cgi?id=5181#c3
|
| |
|
|
|
|
| |
Preparation for reflective add_coordinates
|
| |
|
|
|
|
| |
This in preparation for reifying add_coordinates
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
So I have an easy reference if I want it
Time | File Name
----------------------------------------------------------------------------------
46m09.90s | Total
----------------------------------------------------------------------------------
4m16.33s | SpecificGen/GF5211_32Reflective/Reified/Mul
3m23.12s | SpecificGen/GF5211_32Bounded
2m55.84s | SpecificGen/GF5211_32
2m25.01s | SpecificGen/GF41417_32Bounded
1m47.24s | SpecificGen/GF41417_32
1m44.75s | SpecificGen/GF5211_32BoundedCommon
1m32.33s | Test/Curve25519SpecTestVectors
1m17.22s | CompleteEdwardsCurve/ExtendedCoordinates
1m13.83s | Experiments/Ed25519
1m06.12s | SpecificGen/GF41417_32BoundedCommon
0m59.04s | SpecificGen/GF41417_32Reflective/Reified/Mul
0m40.43s | ModularArithmetic/Conversion
0m37.59s | SpecificGen/GF5211_32Reflective/CommonBinOp
0m34.60s | Spec/Ed25519
0m33.27s | SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE
0m33.24s | SpecificGen/GF5211_32Reflective/CommonUnOp
0m31.56s | ModularArithmetic/ModularBaseSystemProofs
0m30.41s | Specific/GF25519Bounded
0m30.21s | SpecificGen/GF25519_32Bounded
0m30.18s | SpecificGen/GF2519_32Bounded
0m25.95s | SpecificGen/GF41417_32Reflective/CommonBinOp
0m23.36s | Experiments/MontgomeryCurve
0m23.17s | SpecificGen/GF41417_32Reflective/CommonUnOp
0m22.94s | SpecificGen/GF2519_32
0m22.53s | SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE
0m21.95s | ModularArithmetic/Pow2BaseProofs
0m21.76s | Reflection/Z/Interpretations128/Relations
0m21.61s | Specific/GF25519
0m21.14s | SpecificGen/GF25519_32
0m20.16s | Algebra
0m19.94s | SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire
0m18.70s | SpecificGen/GF2213_32Bounded
0m18.52s | Reflection/Z/Interpretations64/Relations
0m18.14s | EdDSARepChange
0m17.27s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems
0m16.65s | SpecificGen/GF5211_32Reflective
0m14.18s | SpecificGen/GF2213_32
0m14.00s | Util/ZUtil
0m12.74s | SpecificGen/GF5211_32Reflective/Reified/PreFreeze
0m11.65s | SpecificGen/GF41417_32Reflective
0m11.27s | SpecificGen/GF25519_64Reflective
0m10.94s | SpecificGen/GF25519_64Bounded
0m10.73s | SpecificGen/GF25519_64
0m10.41s | SpecificGen/GF41417_32Reflective/Reified/PreFreeze
0m10.09s | Testbit
0m09.44s | Specific/GF25519BoundedCommon
0m09.42s | SpecificGen/GF25519_32BoundedCommon
0m09.40s | SpecificGen/GF2519_32BoundedCommon
0m09.28s | Assembly/GF25519
0m09.21s | SpecificGen/GF2519_32Reflective/Reified/Mul
0m08.90s | SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire
0m08.81s | BoundedArithmetic/ArchitectureToZLikeProofs
0m08.78s | ModularArithmetic/Montgomery/ZProofs
0m08.75s | Encoding/PointEncoding
0m08.47s | SpecificGen/GF5211_32Reflective/Reified/CarrySub
0m08.46s | Specific/GF1305
0m08.43s | BoundedArithmetic/Double/Proofs/Multiply
0m08.31s | SpecificGen/GF25519_32Reflective/Reified/Mul
0m08.12s | Specific/GF25519Reflective/Reified/Mul
0m08.00s | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate
0m07.67s | SpecificGen/GF5211_32Reflective/Reified/CarryAdd
0m07.33s | SpecificGen/GF41417_32Reflective/Reified/CarrySub
0m07.02s | MxDHRepChange
0m06.82s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate
0m06.74s | SpecificGen/GF5211_32Reflective/Reified/CarryOpp
0m06.68s | SpecificGen/GF2519_32Reflective
0m06.61s | Reflection/Z/InterpretationsGen
0m06.54s | SpecificGen/GF25519_32Reflective
0m06.36s | Specific/GF25519Reflective
0m06.34s | SpecificGen/GF41417_32Reflective/Reified/CarryAdd
0m06.09s | Bedrock/Word
0m05.85s | SpecificGen/GF41417_32Reflective/Reified/CarryOpp
0m05.80s | SpecificGen/GF2213_32BoundedCommon
0m05.70s | SpecificGen/GF2213_32Reflective/Reified/Mul
0m05.50s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub
0m05.46s | Reflection/Z/Interpretations128/RelationsCombinations
0m05.46s | Reflection/Z/Interpretations64/RelationsCombinations
0m05.41s | Experiments/GenericFieldPow
0m05.38s | Specific/SC25519
0m05.34s | Util/ListUtil
0m05.26s | SpecificGen/GF2213_32Reflective
0m05.24s | ModularArithmetic/ModularBaseSystemListProofs
0m05.06s | SpecificGen/GF5211_32Reflective/Reified/Pack
0m04.88s | SpecificGen/GF5211_32Reflective/Reified/Unpack
0m04.86s | SpecificGen/GF5211_32Reflective/Reified/Sub
0m04.82s | WeierstrassCurve/Pre
0m04.74s | SpecificGen/GF25519_32Reflective/CommonBinOp
0m04.70s | SpecificGen/GF2519_32Reflective/CommonBinOp
0m04.67s | SpecificGen/GF5211_32Reflective/Common
0m04.61s | SpecificGen/GF2519_32Reflective/Reified/PreFreeze
0m04.60s | SpecificGen/GF25519_32Reflective/Reified/PreFreeze
0m04.58s | Specific/GF25519Reflective/Reified/PreFreeze
0m04.54s | Specific/GF25519Reflective/CommonBinOp
0m04.31s | SpecificGen/GF25519_64BoundedCommon
0m04.19s | Specific/GF25519Reflective/CommonUnOp
0m04.15s | SpecificGen/GF25519_32Reflective/CommonUnOp
0m04.11s | Reflection/LinearizeWf
0m04.10s | SpecificGen/GF41417_32Reflective/Reified/Pack
0m04.10s | SpecificGen/GF2519_32Reflective/CommonUnOp
0m04.04s | SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE
0m04.01s | Specific/GF25519Reflective/CommonUnOpWireToFE
0m04.01s | SpecificGen/GF5211_32Reflective/Reified/Add
0m04.00s | SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE
0m03.98s | SpecificGen/GF41417_32Reflective/Reified/Sub
0m03.98s | ModularArithmetic/BarrettReduction/ZHandbook
0m03.94s | BaseSystemProofs
0m03.88s | SpecificGen/GF41417_32Reflective/Reified/Unpack
0m03.79s | Encoding/PointEncodingPre
0m03.70s | SpecificGen/GF2213_32Reflective/Reified/PreFreeze
0m03.57s | SpecificGen/GF5211_32Reflective/Reified/Opp
0m03.52s | CompleteEdwardsCurve/Pre
0m03.46s | SpecificGen/GF2519_32Reflective/Reified/CarrySub
0m03.45s | SpecificGen/GF25519_32Reflective/Reified/CarrySub
0m03.42s | ModularArithmetic/Tutorial
0m03.41s | SpecificGen/GF41417_32Reflective/Reified/Add
0m03.41s | BoundedArithmetic/InterfaceProofs
0m03.38s | SpecificGen/GF41417_32Reflective/Common
0m03.36s | Specific/GF25519Reflective/Reified/CarrySub
0m03.18s | ModularArithmetic/BarrettReduction/ZGeneralized
0m03.16s | SpecificGen/GF2519_32Reflective/Reified/CarryOpp
0m03.15s | ModularArithmetic/ZBoundedZ
0m03.10s | SpecificGen/GF25519_64Reflective/Reified/PreFreeze
0m03.10s | SpecificGen/GF25519_32Reflective/Reified/CarryOpp
0m03.09s | SpecificGen/GF25519_64Reflective/Reified/Mul
0m03.08s | SpecificGen/GF2519_32Reflective/Reified/CarryAdd
0m03.07s | SpecificGen/GF41417_32Reflective/Reified/Opp
0m03.06s | Specific/GF25519Reflective/Reified/CarryOpp
0m03.05s | Specific/GF25519Reflective/Reified/CarryAdd
0m03.04s | SpecificGen/GF25519_32Reflective/Reified/CarryAdd
0m02.96s | SpecificGen/GF5211_32Reflective/Reified/GeModulus
0m02.92s | SpecificGen/GF2213_32Reflective/CommonBinOp
0m02.91s | BoundedArithmetic/Double/Proofs/Decode
0m02.77s | SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire
0m02.75s | SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire
0m02.74s | SpecificGen/GF2213_32Reflective/Reified/CarrySub
0m02.72s | BoundedArithmetic/Double/Proofs/ShiftRight
0m02.71s | Specific/GF25519Reflective/CommonUnOpFEToWire
0m02.66s | ModularArithmetic/ModularArithmeticTheorems
0m02.63s | Assembly/State
0m02.62s | BoundedArithmetic/Double/Proofs/ShiftLeft
0m02.60s | SpecificGen/GF2213_32Reflective/CommonUnOp
0m02.60s | SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE
0m02.56s | SpecificGen/GF2213_32Reflective/Reified/CarryOpp
0m02.54s | SpecificGen/GF25519_64Reflective/Reified/CarrySub
0m02.54s | SpecificGen/GF41417_32Reflective/Reified/GeModulus
0m02.46s | SpecificGen/GF2213_32Reflective/Reified/CarryAdd
0m02.39s | SpecificGen/GF25519_64Reflective/Reified/CarryOpp
0m02.36s | ModularArithmetic/BarrettReduction/ZBounded
0m02.28s | ModularArithmetic/ModularBaseSystemOpt
0m02.26s | SpecificGen/GF2519_32Reflective/Reified/Unpack
0m02.25s | SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire
0m02.20s | SpecificGen/GF2519_32Reflective/Reified/Pack
0m02.19s | SpecificGen/GF25519_64Reflective/Reified/CarryAdd
0m02.16s | SpecificGen/GF25519_32Reflective/Reified/Unpack
0m02.16s | Specific/FancyMachine256/Montgomery
0m02.14s | Specific/GF25519Reflective/Reified/Pack
0m02.11s | Specific/FancyMachine256/Barrett
0m02.08s | Specific/GF25519Reflective/Reified/Unpack
0m02.08s | SpecificGen/GF25519_32Reflective/Reified/Pack
0m02.05s | SpecificGen/GF25519_32Reflective/Reified/Sub
0m02.02s | Specific/GF25519Reflective/Reified/Sub
0m02.01s | SpecificGen/GF2519_32Reflective/Reified/Sub
0m01.99s | Reflection/WfReflective
0m01.96s | SpecificGen/GF2213_32Reflective/Reified/Pack
0m01.94s | Assembly/Evaluables
0m01.93s | Reflection/WfProofs
0m01.92s | SpecificGen/GF2213_32Reflective/Reified/Unpack
0m01.87s | Specific/FancyMachine256/Core
0m01.86s | Util/WordUtil
0m01.83s | SpecificGen/GF2519_32Reflective/Reified/Opp
0m01.82s | ModularArithmetic/Montgomery/ZBounded
0m01.79s | Specific/GF25519Reflective/Reified/Add
0m01.78s | Specific/GF25519Reflective/Reified/Opp
0m01.77s | SpecificGen/GF25519_64Reflective/Reified/Pack
0m01.77s | SpecificGen/GF2213_32Reflective/Reified/Sub
0m01.77s | SpecificGen/GF2519_32Reflective/Reified/Add
0m01.76s | SpecificGen/GF25519_32Reflective/Reified/Opp
0m01.70s | SpecificGen/GF25519_64Reflective/Reified/Unpack
0m01.68s | Reflection/InlineWf
0m01.67s | SpecificGen/GF25519_32Reflective/Reified/Add
0m01.67s | SpecificGen/GF25519_32Reflective/Reified/GeModulus
0m01.65s | SpecificGen/GF25519_64Reflective/CommonBinOp
0m01.63s | Reflection/InlineInterp
0m01.63s | SpecificGen/GF2519_32Reflective/Reified/GeModulus
0m01.62s | Assembly/Compile
0m01.61s | Specific/GF25519Reflective/Reified/GeModulus
0m01.60s | Experiments/Ed25519Extraction
0m01.59s | SpecificGen/GF25519_32Reflective/Common
0m01.55s | SpecificGen/GF2213_32Reflective/Reified/Opp
0m01.54s | Specific/GF25519Reflective/Common
0m01.54s | Assembly/WordizeUtil
0m01.52s | SpecificGen/GF25519_64Reflective/Reified/GeModulus
0m01.52s | SpecificGen/GF2519_32Reflective/Common
0m01.50s | ModularArithmetic/BarrettReduction/Z
0m01.50s | SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ
0m01.48s | SpecificGen/GF2213_32Reflective/Reified/Add
0m01.46s | SpecificGen/GF25519_64Reflective/CommonUnOp
0m01.45s | SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE
0m01.42s | SpecificGen/GF2213_32Reflective/Reified/GeModulus
0m01.40s | SpecificGen/GF25519_64Reflective/Reified/Opp
0m01.40s | SpecificGen/GF25519_64Reflective/Reified/Sub
0m01.39s | Reflection/TestCase
0m01.39s | Util/NatUtil
0m01.39s | SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire
0m01.36s | ModularArithmetic/PrimeFieldTheorems
0m01.32s | Assembly/Bounds
0m01.32s | SpecificGen/GF2213_32Reflective/Common
0m01.28s | Assembly/Conversions
0m01.26s | SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ
0m01.24s | ModularArithmetic/ExtendedBaseVector
0m01.18s | BaseSystem
0m01.16s | SpecificGen/GF25519_64Reflective/Reified/Add
0m01.16s | Util/Tuple
0m01.15s | SpecificGen/GF25519_64Reflective/Common
0m01.15s | BoundedArithmetic/Double/Repeated/Proofs/Decode
0m01.09s | SpecificGen/GF5211_32Reflective/Reified
0m01.05s | SpecificGen/GF41417_32Reflective/Reified
0m01.01s | Assembly/LL
0m00.99s | Specific/GF25519Reflective/CommonUnOpFEToZ
0m00.96s | Assembly/Pipeline
0m00.94s | SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ
0m00.94s | SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ
0m00.89s | Util/NumTheoryUtil
0m00.89s | Assembly/HL
0m00.88s | BoundedArithmetic/Double/Proofs/LoadImmediate
0m00.88s | Assembly/PhoasCommon
0m00.88s | BoundedArithmetic/Double/Proofs/BitwiseOr
0m00.88s | SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ
0m00.86s | Util/IterAssocOp
0m00.84s | SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ
0m00.79s | BoundedArithmetic/X86ToZLikeProofs
0m00.77s | ModularArithmetic/ModularBaseSystem
0m00.75s | Assembly/QhasmEvalCommon
0m00.75s | SpecificGen/GF2519_32Reflective/Reified
0m00.73s | Specific/GF25519Reflective/Reified
0m00.72s | SpecificGen/GF25519_32Reflective/Reified
0m00.71s | Util/PartiallyReifiedProp
0m00.70s | SpecificGen/GF2213_32Reflective/Reified
0m00.70s | SpecificGen/GF25519_64Reflective/Reified
0m00.69s | ModularArithmetic/PseudoMersenneBaseParamProofs
0m00.68s | Reflection/Z/Syntax
0m00.66s | ModularArithmetic/ExtPow2BaseMulProofs
0m00.65s | Reflection/InterpWfRel
0m00.64s | Util/AdditionChainExponentiation
0m00.63s | BoundedArithmetic/Double/Proofs/SelectConditional
0m00.62s | Encoding/ModularWordEncodingTheorems
0m00.62s | BoundedArithmetic/Double/Repeated/Proofs/Multiply
0m00.61s | Encoding/ModularWordEncodingPre
0m00.60s | ModularArithmetic/ModularBaseSystemList
0m00.60s | Spec/EdDSA
0m00.60s | Spec/ModularWordEncoding
0m00.58s | BoundedArithmetic/Interface
0m00.58s | BoundedArithmetic/X86ToZLike
0m00.57s | Reflection/WfReflectiveGen
0m00.56s | Assembly/Qhasm
0m00.55s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub
0m00.54s | Reflection/Syntax
0m00.54s | Reflection/LinearizeInterp
0m00.54s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr
0m00.50s | BoundedArithmetic/ArchitectureToZLike
0m00.50s | Assembly/StringConversion
0m00.48s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional
0m00.48s | ModularArithmetic/Pow2Base
0m00.48s | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight
0m00.48s | Util/Decidable
0m00.48s | Reflection/Z/Reify
0m00.48s | Reflection/CommonSubexpressionElimination
0m00.47s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate
0m00.47s | BoundedArithmetic/Double/Repeated/Core
0m00.47s | Reflection/InterpProofs
0m00.47s | Reflection/Z/Interpretations128
0m00.47s | Reflection/InterpWf
0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate
0m00.46s | BoundedArithmetic/Double/Core
0m00.46s | BoundedArithmetic/StripCF
0m00.46s | Util/HList
0m00.46s | BoundedArithmetic/Eta
0m00.45s | Reflection/Z/Interpretations64
0m00.45s | ModularArithmetic/ZBounded
0m00.45s | Assembly/QhasmUtil
0m00.44s | ModularArithmetic/Pre
0m00.44s | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic
0m00.44s | Reflection/Conversion
0m00.44s | Reflection/WfRel
0m00.44s | ModularArithmetic/ModularBaseSystemListZOperationsProofs
0m00.43s | Spec/CompleteEdwardsCurve
0m00.43s | Reflection/FilterLive
0m00.42s | Reflection/MapInterpWf
0m00.42s | Reflection/Named/EstablishLiveness
0m00.42s | Reflection/InputSyntax
0m00.42s | Spec/WeierstrassCurve
0m00.42s | Reflection/Application
0m00.42s | ModularArithmetic/Montgomery/Z
0m00.41s | Spec/ModularArithmetic
0m00.40s | Reflection/Named/RegisterAssign
0m00.40s | Reflection/Named/Compile
0m00.40s | Reflection/Named/Syntax
0m00.40s | Reflection/MapInterp
0m00.39s | ModularArithmetic/ModularBaseSystemWord
0m00.39s | ModularArithmetic/ModularBaseSystemListZOperations
0m00.38s | Reflection/Linearize
0m00.38s | Tactics/Algebra_syntax/Nsatz
0m00.38s | Spec/MxDH
0m00.37s | Reflection/Inline
0m00.37s | Reflection/Reify
0m00.36s | ModularArithmetic/PseudoMersenneBaseParams
0m00.36s | Reflection/Named/DeadCodeElimination
0m00.35s | Reflection/CountLets
0m00.34s | Reflection/Named/ContextOn
0m00.33s | Reflection/Named/NameUtil
0m00.29s | Bedrock/Nomega
0m00.27s | Assembly/QhasmCommon
0m00.22s | Util/CaseUtil
0m00.22s | Util/Sum
0m00.19s | Experiments/ExtrHaskellNats
0m00.13s | Util/Relations
0m00.11s | Util/Sigma
0m00.09s | Util/Prod
0m00.09s | Util/Option
0m00.08s | Util/PointedProp
0m00.06s | Util/Equality
0m00.04s | Util/LetIn
0m00.04s | Util/HProp
0m00.04s | Util/Bool
0m00.04s | Util/IffT
0m00.04s | Util/Tactics
0m00.03s | Tactics/VerdiTactics
0m00.03s | Util/Notations
0m00.03s | Util/Unit
0m00.03s | Util/Logic
0m00.02s | Encoding/EncodingTheorems
0m00.02s | Util/Isomorphism
0m00.02s | Util/GlobalSettings
0m00.02s | Spec/Encoding
0m00.02s | Util/AutoRewrite
0m00.02s | Util/FixCoqMistakes
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
| |
I haven't found a good way to genericize the proofs of relatedness
things, mostly because Modules and functors are annoying.
|
| |
|
| |
|
| |
|