aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments
Commit message (Collapse)AuthorAge
* Loops (trying again) (#259)Gravatar Andres Erbsen2017-12-11
| | | | * clean up src/Experiments/Loops.v, add While and For
* [demo] Add reification in src/Experiments/SimplyTypedArithmetic.v (#275)Gravatar Jason Gross2017-11-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * [demo] Add reification in src/Experiments/SimplyTypedArithmetic.v It's rather verbose, unfortunately. The reification also doesn't have any of the nice debugging features of the version of reification in Compilers, because that's even more boilerplate. Not sure if I should add that back in, at the moment. Also, for some strange reason, places where `constr`s fail to typecheck seem to induce backtracking where I don't think they should, and I'm not sure what's going on... * [demo] Add more namespacing * Update llet notation, update is_known_const name As per code review suggestions * Namespace var_context, add some coqbug references * Rename is_type_arg to is_template_parameter As per https://github.com/mit-plv/fiat-crypto/pull/275#discussion_r153036059 * Simplify the logic around delayed arguments a bit We no longer pass around dummy markers in the tuple of arguments. * [demo] More informative reification error messages This time without exponential slowdown in failure cases and without needing to manually think up all of the possible errors and write them out. Possible thanks to Hugo's comment at https://github.com/coq/coq/issues/6252#issuecomment-347041995 * [demo] respond to code review, add comments * Update documentation with suggestions from Andres
* [demo] Replace (max (length a) (length b)) with explicit nat argGravatar Jason Gross2017-11-24
|
* [Demo] Define [place] in terms of nat_rectGravatar Jason Gross2017-11-24
| | | | This will make it easier to reify
* [demo] Use [List.repeat] rather than [List.map]Gravatar Jason Gross2017-11-24
| | | | | As per https://github.com/mit-plv/fiat-crypto/pull/271/commits/76634efa66aa9085a1e410c04f930dd5645126df#r152719891
* [demo] Pass in a [nat] for list lengthGravatar Jason Gross2017-11-24
| | | | | | | As per https://github.com/mit-plv/fiat-crypto/pull/271/commits/76634efa66aa9085a1e410c04f930dd5645126df#r152720364 and https://github.com/mit-plv/fiat-crypto/pull/271/commits/76634efa66aa9085a1e410c04f930dd5645126df#r152720444
* Remove tuple from src/DemoWithReification.vGravatar Jason Gross2017-11-24
|
* Move DemoWithReification.v => Experiments/SimplyTypedArithmetic.vGravatar Jason Gross2017-11-24
| | | | | As per https://github.com/mit-plv/fiat-crypto/pull/271#discussion_r152720545
* automate some proofs; also remove trace-based reasoning in favor of ↵Gravatar jadep2017-10-26
| | | | induction on fuel
* invariants don't need to know the fuelGravatar jadep2017-10-26
|
* WIP: loopsGravatar jadep2017-10-26
|
* remove unused filesGravatar Andres Erbsen2017-04-06
|
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
| | | | | | | | This closes #146 and makes `make quick` faster. The changes were generated by adding [Global Set Suggest Proof Using.] to GlobalSettings.v, and then following [the instructions for a script I wrote](https://github.com/JasonGross/coq-tools#proof-using-helper).
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Most files no longer import Crypto.Util.Tactics. We remove an unused lemma depending on classical axioms; closes #143. After | File Name | Before || Change ----------------------------------------------------------------------------------------------------------- 28m38.18s | Total | 29m04.51s || -0m26.32s ----------------------------------------------------------------------------------------------------------- 0m41.70s | ModularArithmetic/ModularBaseSystemProofs | 0m32.66s || +0m09.04s 1m39.88s | MontgomeryX | 1m46.07s || -0m06.18s 1m56.52s | WeierstrassCurve/Projective | 2m00.76s || -0m04.23s 10m36.85s | WeierstrassCurve/WeierstrassCurveTheorems | 10m40.14s || -0m03.28s 0m21.35s | ModularArithmetic/Pow2BaseProofs | 0m22.54s || -0m01.18s 0m20.24s | Reflection/Named/MapCastWf | 0m21.41s || -0m01.17s 1m30.28s | Test/Curve25519SpecTestVectors | 1m31.19s || -0m00.90s 0m49.53s | Specific/IntegrationTest | 0m50.01s || -0m00.47s 0m42.19s | MontgomeryCurveTheorems | 0m42.18s || +0m00.00s 0m41.08s | ModularArithmetic/Conversion | 0m41.84s || -0m00.76s 0m36.62s | Spec/Ed25519 | 0m37.13s || -0m00.51s 0m23.64s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m24.44s || -0m00.80s 0m19.94s | Specific/GF25519 | 0m20.12s || -0m00.17s 0m19.59s | CompleteEdwardsCurve/ExtendedCoordinates | 0m19.83s || -0m00.23s 0m19.14s | Reflection/Z/Bounds/InterpretationLemmas | 0m19.90s || -0m00.75s 0m18.65s | EdDSARepChange | 0m18.74s || -0m00.08s 0m16.24s | Reflection/Z/ArithmeticSimplifierWf | 0m17.11s || -0m00.87s 0m15.03s | Util/ZUtil | 0m15.93s || -0m00.90s 0m14.74s | Reflection/Named/ContextProperties/NameUtil | 0m15.11s || -0m00.36s 0m14.62s | Reflection/Named/ContextProperties/SmartMap | 0m14.93s || -0m00.31s 0m12.96s | Specific/NewBaseSystemTest | 0m13.24s || -0m00.27s 0m11.84s | Algebra/Field | 0m12.49s || -0m00.65s 0m10.21s | Testbit | 0m09.86s || +0m00.35s 0m09.86s | Reflection/Z/ArithmeticSimplifierInterp | 0m10.69s || -0m00.83s 0m09.44s | Reflection/Named/MapCastInterp | 0m09.82s || -0m00.38s 0m08.81s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m09.37s || -0m00.55s 0m08.60s | Assembly/GF25519 | 0m08.66s || -0m00.06s 0m08.58s | ModularArithmetic/Montgomery/ZProofs | 0m08.77s || -0m00.18s 0m08.53s | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m08.34s || +0m00.18s 0m08.41s | BoundedArithmetic/Double/Proofs/Multiply | 0m08.77s || -0m00.35s 0m08.26s | Reflection/InlineWf | 0m08.59s || -0m00.33s 0m07.54s | Algebra/Ring | 0m08.04s || -0m00.49s 0m07.43s | MxDHRepChange | 0m07.10s || +0m00.33s 0m07.15s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate | 0m07.09s || +0m00.06s 0m07.00s | NewBaseSystem | 0m07.16s || -0m00.16s 0m06.51s | Specific/GF1305 | 0m06.52s || -0m00.00s 0m06.09s | Util/FixedWordSizesEquality | 0m06.37s || -0m00.28s 0m05.56s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub | 0m05.51s || +0m00.04s 0m05.38s | CompleteEdwardsCurve/Pre | 0m05.38s || +0m00.00s 0m05.28s | ModularArithmetic/ModularBaseSystemListProofs | 0m05.15s || +0m00.12s 0m05.24s | Experiments/GenericFieldPow | 0m05.54s || -0m00.29s 0m05.01s | Specific/SC25519 | 0m05.38s || -0m00.37s 0m04.93s | Algebra/Field_test | 0m04.81s || +0m00.12s 0m04.78s | Reflection/InlineCastWf | 0m04.94s || -0m00.16s 0m04.10s | Reflection/Z/Syntax/Equality | 0m04.28s || -0m00.18s 0m03.92s | BaseSystemProofs | 0m03.90s || +0m00.02s 0m03.75s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.94s || -0m00.18s 0m03.72s | CompleteEdwardsCurve/EdwardsMontgomery | 0m03.69s || +0m00.03s 0m03.72s | Reflection/EtaWf | 0m03.71s || +0m00.01s 0m03.60s | Reflection/Named/CompileWf | 0m04.01s || -0m00.40s 0m03.58s | SaturatedBaseSystem | 0m03.76s || -0m00.17s 0m03.33s | BoundedArithmetic/InterfaceProofs | 0m03.72s || -0m00.39s 0m03.16s | Reflection/LinearizeWf | 0m03.26s || -0m00.09s 0m03.08s | ModularArithmetic/ZBoundedZ | 0m03.16s || -0m00.08s 0m03.01s | Specific/FancyMachine256/Montgomery | 0m03.16s || -0m00.15s 0m02.99s | Reflection/Named/CompileInterp | 0m03.24s || -0m00.25s 0m02.92s | ModularArithmetic/ModularArithmeticTheorems | 0m03.06s || -0m00.14s 0m02.92s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m03.15s || -0m00.23s 0m02.90s | Specific/FancyMachine256/Barrett | 0m03.18s || -0m00.28s 0m02.80s | Spec/MontgomeryCurve | 0m03.05s || -0m00.25s 0m02.77s | BoundedArithmetic/Double/Proofs/ShiftRight | 0m02.75s || +0m00.02s 0m02.75s | BoundedArithmetic/Double/Proofs/Decode | 0m02.81s || -0m00.06s 0m02.64s | BoundedArithmetic/Double/Proofs/ShiftLeft | 0m02.62s || +0m00.02s 0m02.54s | Reflection/InlineInterp | 0m02.60s || -0m00.06s 0m02.48s | Reflection/Named/ContextProperties | 0m02.58s || -0m00.10s 0m02.47s | ModularArithmetic/ModularBaseSystemOpt | 0m02.39s || +0m00.08s 0m02.40s | Reflection/TestCase | 0m02.60s || -0m00.20s 0m02.35s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.40s || -0m00.04s 0m02.35s | Reflection/Z/Bounds/Relax | 0m02.46s || -0m00.10s 0m02.33s | Reflection/Named/NameUtilProperties | 0m02.40s || -0m00.06s 0m02.15s | Reflection/WfProofs | 0m02.26s || -0m00.10s 0m02.00s | Reflection/WfReflective | 0m02.04s || -0m00.04s 0m01.97s | ModularArithmetic/Montgomery/ZBounded | 0m02.14s || -0m00.17s 0m01.90s | Specific/FancyMachine256/Core | 0m01.98s || -0m00.08s 0m01.89s | Util/WordUtil | 0m01.96s || -0m00.07s 0m01.88s | Assembly/Evaluables | 0m01.82s || +0m00.05s 0m01.62s | WeierstrassCurve/Pre | 0m01.64s || -0m00.01s 0m01.56s | Reflection/Named/InterpretToPHOASWf | 0m01.61s || -0m00.05s 0m01.46s | Assembly/Compile | 0m01.51s || -0m00.05s 0m01.44s | ModularArithmetic/PrimeFieldTheorems | 0m01.43s || +0m00.01s 0m01.44s | ModularArithmetic/BarrettReduction/Z | 0m01.57s || -0m00.13s 0m01.41s | Algebra/Group | 0m01.87s || -0m00.46s 0m01.40s | Util/Tuple | 0m01.46s || -0m00.06s 0m01.38s | Reflection/MapCastInterp | 0m01.38s || +0m00.00s 0m01.31s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.05s || +0m00.26s 0m01.26s | ModularArithmetic/ExtendedBaseVector | 0m01.28s || -0m00.02s 0m01.16s | Assembly/Conversions | 0m01.13s || +0m00.03s 0m01.14s | Reflection/Z/Bounds/Pipeline/Definition | 0m01.15s || -0m00.01s 0m01.13s | BaseSystem | 0m01.14s || -0m00.01s 0m01.06s | Reflection/SmartBoundInterp | 0m01.07s || -0m00.01s 0m01.04s | Reflection/Named/InterpretToPHOASInterp | 0m00.99s || +0m00.05s 0m01.01s | Reflection/SmartCastWf | 0m00.94s || +0m00.07s 0m01.01s | Assembly/Pipeline | 0m01.02s || -0m00.01s 0m01.01s | Reflection/Relations | 0m01.06s || -0m00.05s 0m00.97s | Assembly/HL | 0m00.99s || -0m00.02s 0m00.96s | Algebra/IntegralDomain | 0m01.00s || -0m00.04s 0m00.94s | Assembly/LL | 0m01.02s || -0m00.08s 0m00.92s | BoundedArithmetic/Double/Proofs/BitwiseOr | 0m00.91s || +0m00.01s 0m00.90s | Assembly/PhoasCommon | 0m00.87s || +0m00.03s 0m00.89s | Util/NumTheoryUtil | 0m00.92s || -0m00.03s 0m00.87s | BoundedArithmetic/Double/Proofs/LoadImmediate | 0m00.96s || -0m00.08s 0m00.84s | Reflection/WfInversion | 0m00.88s || -0m00.04s 0m00.83s | Reflection/InlineCastInterp | 0m00.85s || -0m00.02s 0m00.81s | Reflection/Named/CompileProperties | 0m00.87s || -0m00.05s 0m00.80s | BoundedArithmetic/X86ToZLikeProofs | 0m00.86s || -0m00.05s 0m00.78s | Karatsuba | 0m00.84s || -0m00.05s 0m00.72s | Util/PartiallyReifiedProp | 0m00.73s || -0m00.01s 0m00.72s | Reflection/MultiSizeTest | 0m00.72s || +0m00.00s 0m00.69s | ModularArithmetic/ModularBaseSystem | 0m00.72s || -0m00.03s 0m00.68s | BoundedArithmetic/Double/Repeated/Proofs/Multiply | 0m00.61s || +0m00.07s 0m00.68s | Reflection/MapCastByDeBruijnInterp | 0m00.76s || -0m00.07s 0m00.68s | Encoding/ModularWordEncodingTheorems | 0m00.80s || -0m00.12s 0m00.68s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.72s || -0m00.03s 0m00.67s | Spec/EdDSA | 0m00.66s || +0m00.01s 0m00.67s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.74s || -0m00.06s 0m00.66s | Reflection/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.62s || +0m00.04s 0m00.66s | Util/IterAssocOp | 0m00.94s || -0m00.27s 0m00.64s | Encoding/ModularWordEncodingPre | 0m00.73s || -0m00.08s 0m00.63s | ModularArithmetic/ModularBaseSystemList | 0m00.77s || -0m00.14s 0m00.62s | Spec/ModularWordEncoding | 0m00.66s || -0m00.04s 0m00.61s | Reflection/MapCastByDeBruijnWf | 0m00.61s || +0m00.00s 0m00.58s | BoundedArithmetic/X86ToZLike | 0m00.57s || +0m00.01s 0m00.58s | Reflection/Z/CNotations | 0m00.56s || +0m00.01s 0m00.57s | Spec/WeierstrassCurve | 0m00.57s || +0m00.00s 0m00.56s | Spec/CompleteEdwardsCurve | 0m00.59s || -0m00.02s 0m00.56s | BoundedArithmetic/Double/Proofs/SelectConditional | 0m00.58s || -0m00.01s 0m00.56s | Reflection/InterpByIsoProofs | 0m00.60s || -0m00.03s 0m00.55s | Reflection/Named/WfInterp | 0m00.57s || -0m00.01s 0m00.55s | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight | 0m00.57s || -0m00.01s 0m00.54s | Reflection/Named/FMapContext | 0m00.70s || -0m00.15s 0m00.54s | Util/AdditionChainExponentiation | 0m00.62s || -0m00.07s 0m00.54s | Reflection/SmartBoundWf | 0m00.55s || -0m00.01s 0m00.54s | Reflection/WfReflectiveGen | 0m00.54s || +0m00.00s 0m00.54s | BoundedArithmetic/Interface | 0m00.56s || -0m00.02s 0m00.52s | BoundedArithmetic/ArchitectureToZLike | 0m00.46s || +0m00.06s 0m00.52s | Reflection/Z/JavaNotations | 0m00.58s || -0m00.05s 0m00.52s | Reflection/Z/Syntax/Util | 0m00.53s || -0m00.01s 0m00.52s | Util/CPSUtil | 0m00.57s || -0m00.04s 0m00.51s | Reflection/BoundByCastInterp | 0m00.51s || +0m00.00s 0m00.50s | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.53s || -0m00.03s 0m00.50s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.57s || -0m00.06s 0m00.50s | Reflection/InterpWfRel | 0m00.54s || -0m00.04s 0m00.49s | Reflection/Z/InlineInterp | 0m00.37s || +0m00.12s 0m00.49s | Reflection/InputSyntax | 0m00.55s || -0m00.06s 0m00.49s | Util/Decidable | 0m00.48s || +0m00.01s 0m00.48s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.39s || +0m00.08s 0m00.48s | BoundedArithmetic/Double/Repeated/Core | 0m00.48s || +0m00.00s 0m00.47s | BoundedArithmetic/Double/Core | 0m00.50s || -0m00.03s 0m00.47s | Reflection/Z/Bounds/Pipeline | 0m00.46s || +0m00.00s 0m00.47s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.54s || -0m00.07s 0m00.47s | ModularArithmetic/ModularBaseSystemListZOperationsProofs | 0m00.42s || +0m00.04s 0m00.47s | Util/NUtil | 0m00.50s || -0m00.03s 0m00.47s | Reflection/Z/Bounds/Interpretation | 0m00.42s || +0m00.04s 0m00.47s | Reflection/Z/Reify | 0m00.49s || -0m00.02s 0m00.46s | BoundedArithmetic/StripCF | 0m00.44s || +0m00.02s 0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.51s || -0m00.04s 0m00.46s | Reflection/Z/MapCastByDeBruijn | 0m00.50s || -0m00.03s 0m00.46s | Reflection/Z/Bounds/MapCastByDeBruijnWf | 0m00.42s || +0m00.04s 0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.55s || -0m00.09s 0m00.45s | Util/HList | 0m00.50s || -0m00.04s 0m00.44s | Reflection/Z/Inline | 0m00.39s || +0m00.04s 0m00.44s | Reflection/InterpWf | 0m00.55s || -0m00.11s 0m00.44s | Reflection/Z/Syntax | 0m00.46s || -0m00.02s 0m00.44s | Reflection/Z/ArithmeticSimplifier | 0m00.47s || -0m00.02s 0m00.44s | Reflection/Named/DeadCodeElimination | 0m00.36s || +0m00.08s 0m00.44s | ModularArithmetic/ZBounded | 0m00.49s || -0m00.04s 0m00.43s | ModularArithmetic/Pre | 0m00.44s || -0m00.01s 0m00.42s | ModularArithmetic/Montgomery/Z | 0m00.39s || +0m00.02s 0m00.42s | Reflection/Z/Bounds/MapCastByDeBruijnInterp | 0m00.43s || -0m00.01s 0m00.42s | Util/ZRange | 0m00.42s || +0m00.00s 0m00.42s | Reflection/Z/MapCastByDeBruijnInterp | 0m00.46s || -0m00.04s 0m00.41s | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic | 0m00.45s || -0m00.04s 0m00.41s | Reflection/Z/Bounds/MapCastByDeBruijn | 0m00.50s || -0m00.09s 0m00.40s | Reflection/Z/MapCastByDeBruijnWf | 0m00.50s || -0m00.09s 0m00.40s | Reflection/Z/InlineWf | 0m00.42s || -0m00.01s 0m00.40s | Reflection/Z/Bounds/Pipeline/OutputType | 0m00.38s || +0m00.02s 0m00.40s | ModularArithmetic/Pow2Base | 0m00.43s || -0m00.02s 0m00.40s | Reflection/Named/PositiveContext/DefaultsProperties | 0m00.52s || -0m00.12s 0m00.40s | Reflection/MapCastByDeBruijn | 0m00.39s || +0m00.01s 0m00.39s | Reflection/Z/Bounds/Pipeline/Glue | 0m00.46s || -0m00.07s 0m00.39s | Reflection/Named/PositiveContext/Defaults | 0m00.40s || -0m00.01s 0m00.39s | Reflection/Named/ContextDefinitions | 0m00.37s || +0m00.02s 0m00.38s | Reflection/Z/FoldTypes | 0m00.38s || +0m00.00s 0m00.38s | Reflection/Z/HexNotationConstants | 0m00.42s || -0m00.03s 0m00.38s | Reflection/Z/OpInversion | 0m00.37s || +0m00.01s 0m00.38s | ModularArithmetic/ModularBaseSystemListZOperations | 0m00.41s || -0m00.02s 0m00.38s | Reflection/Named/EstablishLiveness | 0m00.38s || +0m00.00s 0m00.38s | Reflection/Named/RegisterAssign | 0m00.38s || +0m00.00s 0m00.38s | Reflection/Reify | 0m00.40s || -0m00.02s 0m00.37s | ModularArithmetic/ModularBaseSystemWord | 0m00.38s || -0m00.01s 0m00.36s | Reflection/Named/InterpretToPHOAS | 0m00.45s || -0m00.09s 0m00.36s | Reflection/Named/Syntax | 0m00.35s || +0m00.01s 0m00.36s | BoundedArithmetic/Eta | 0m00.42s || -0m00.06s 0m00.35s | Reflection/Named/Compile | 0m00.34s || +0m00.00s 0m00.35s | Reflection/MapCastWf | 0m00.31s || +0m00.03s 0m00.35s | Reflection/Named/SmartMap | 0m00.36s || -0m00.01s 0m00.35s | Util/BoundedWord | 0m00.40s || -0m00.05s 0m00.35s | Spec/ModularArithmetic | 0m00.36s || -0m00.01s 0m00.34s | Reflection/Named/ContextOn | 0m00.34s || +0m00.00s 0m00.34s | Reflection/FilterLive | 0m00.32s || +0m00.02s 0m00.34s | Reflection/Named/MapCast | 0m00.37s || -0m00.02s 0m00.33s | Reflection/Named/PositiveContext | 0m00.39s || -0m00.06s 0m00.33s | Algebra/ScalarMult | 0m00.56s || -0m00.23s 0m00.32s | Reflection/Z/BinaryNotationConstants | 0m00.35s || -0m00.02s 0m00.32s | Reflection/Tuple | 0m00.38s || -0m00.06s 0m00.32s | Reflection/Named/ContextProperties/Tactics | 0m00.48s || -0m00.15s 0m00.32s | Reflection/Named/IdContext | 0m00.33s || -0m00.01s 0m00.31s | Reflection/Named/Wf | 0m00.38s || -0m00.07s 0m00.30s | Reflection/MultiSizeTest2 | 0m00.34s || -0m00.04s 0m00.29s | Reflection/ExprInversion | 0m00.26s || +0m00.02s 0m00.29s | Spec/MxDH | 0m00.43s || -0m00.14s 0m00.26s | Algebra/Monoid | 0m00.51s || -0m00.25s 0m00.26s | Util/Sum | 0m00.34s || -0m00.08s 0m00.24s | Algebra | 0m00.43s || -0m00.19s 0m00.23s | Reflection/Equality | 0m00.25s || -0m00.01s 0m00.22s | Reflection/CommonSubexpressionElimination | 0m00.17s || +0m00.04s 0m00.21s | Reflection/SmartMap | 0m00.23s || -0m00.02s 0m00.20s | Reflection/EtaInterp | 0m00.22s || -0m00.01s 0m00.20s | Reflection/BoundByCastWf | 0m00.12s || +0m00.08s 0m00.20s | Reflection/LinearizeInterp | 0m00.23s || -0m00.03s 0m00.18s | Util/LetInMonad | 0m00.19s || -0m00.01s 0m00.16s | Reflection/InterpProofs | 0m00.18s || -0m00.01s 0m00.13s | Util/Option | 0m00.14s || -0m00.01s 0m00.13s | Reflection/Wf | 0m00.12s || +0m00.01s 0m00.12s | Reflection/RewriterWf | 0m00.19s || -0m00.07s 0m00.08s | Reflection/Conversion | 0m00.08s || +0m00.00s 0m00.08s | Reflection/Named/NameUtil | 0m00.12s || -0m00.03s 0m00.07s | Reflection/Inline | 0m00.04s || +0m00.03s 0m00.06s | Reflection/TypeInversion | 0m00.08s || -0m00.02s 0m00.06s | Reflection/SmartBound | 0m00.06s || +0m00.00s 0m00.06s | Reflection/InlineCast | 0m00.06s || +0m00.00s 0m00.06s | Util/Tactics | 0m00.07s || -0m00.01s 0m00.06s | Reflection/RewriterInterp | 0m00.05s || +0m00.00s 0m00.06s | Reflection/MapCast | 0m00.06s || +0m00.00s 0m00.05s | Reflection/TypeUtil | 0m00.04s || +0m00.01s 0m00.04s | Reflection/Syntax | 0m00.09s || -0m00.05s 0m00.04s | Reflection/FoldTypes | 0m00.05s || -0m00.01s 0m00.04s | Reflection/Linearize | 0m00.04s || +0m00.00s 0m00.04s | Reflection/Rewriter | 0m00.03s || +0m00.01s 0m00.04s | Reflection/Map | 0m00.04s || +0m00.00s 0m00.04s | Util/Tactics/OnSubterms | N/A || +0m00.04s 0m00.04s | Reflection/CountLets | 0m00.04s || +0m00.00s 0m00.04s | Reflection/SmartCast | 0m00.04s || +0m00.00s 0m00.04s | Util/LetIn | 0m00.07s || -0m00.03s 0m00.04s | Reflection/Eta | 0m00.05s || -0m00.01s 0m00.04s | Reflection/BoundByCast | 0m00.06s || -0m00.01s 0m00.03s | Reflection/SmartCastInterp | 0m00.05s || -0m00.02s 0m00.03s | Util/Tactics/SubstEvars | N/A || +0m00.03s 0m00.03s | Reflection/InterpByIso | 0m00.04s || -0m00.01s 0m00.03s | Util/Tactics/Forward | N/A || +0m00.03s 0m00.03s | Util/Tactics/BreakMatch | 0m00.02s || +0m00.00s 0m00.03s | Reflection/RenameBinders | 0m00.03s || +0m00.00s 0m00.03s | Util/Tactics/ConvoyDestruct | N/A || +0m00.03s 0m00.02s | Util/Tactics/SideConditionsBeforeToAfter | N/A || +0m00.02s 0m00.02s | Util/Tactics/Revert | N/A || +0m00.02s 0m00.02s | Util/Tactics/Test | N/A || +0m00.02s 0m00.02s | Util/Tactics/SetEvars | N/A || +0m00.02s 0m00.02s | Util/Tactics/SetoidSubst | N/A || +0m00.02s 0m00.02s | Util/Tactics/DestructTrivial | N/A || +0m00.02s 0m00.02s | Util/Tactics/ESpecialize | N/A || +0m00.02s 0m00.02s | Util/Tactics/SimplifyProjections | N/A || +0m00.02s 0m00.02s | Util/Tactics/Not | N/A || +0m00.02s 0m00.02s | Util/Tactics/Contains | N/A || +0m00.02s 0m00.02s | Util/Tactics/SimplifyRepeatedIfs | N/A || +0m00.02s 0m00.02s | Util/Tactics/ClearDuplicates | N/A || +0m00.02s 0m00.02s | Util/Tactics/DebugPrint | N/A || +0m00.02s 0m00.01s | Util/Tactics/GetGoal | N/A || +0m00.01s
* Remove everything after the individual reified opsGravatar Jason Gross2017-04-03
| | | | | This includes extraction and associated targets. I've left the .hs files lying around, currently unused.
* remove undeclared lines from Ed25519Extraction.vGravatar Andres Erbsen2017-03-02
|
* move large non-building chunks of Ed25519.vGravatar Andres Erbsen2017-03-02
|
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
|
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
| | | | | | | | | | | This will eventually make a number of proofs easier. Unfortunately, the correctness lemmas for AddCoordinates and LadderStep no longer work (because of different arities), and there's a proof in Experiments/Ed25519 that I've admitted. The correctness lemmas will be easy to re-add when we have a more general version that handle arbitrary type shapes.
* Removed code that will be completely replaced in the future; replaced some ↵Gravatar jadep2017-02-22
| | | | pointencoding things with axioms pending pointencoding rewrite by Andres
* move lemmas from Ed25519 to WordUtilGravatar jadep2017-02-22
|
* move some lemmas from Ed25519 to ZUtilGravatar jadep2017-02-22
|
* moved more stuff to NUtilGravatar jadep2017-02-22
|
* Moved N lemmas from Ed25519 and IterAssocOp into new NUtil fileGravatar jadep2017-02-22
|
* categorize the rest of the stuff in Ed25519Gravatar jadep2017-02-22
|
* categorize some of the stuff in Ed25519Gravatar jadep2017-02-22
|
* Fix changed namesGravatar Jason Gross2017-02-03
|
* Generalize add_coordinatesGravatar Jason Gross2016-11-17
| | | | | | | | | | | | | | | | | | 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.
* Support for 128-bit wordsGravatar Jason Gross2016-11-14
| | | | | I haven't found a good way to genericize the proofs of relatedness things, mostly because Modules and functors are annoying.
* extraction: inline field operations into group operationsGravatar Andres Erbsen2016-11-14
|
* Add mulW_noinlineGravatar Jason Gross2016-11-14
|
* Proper_sqrtGravatar Andres Erbsen2016-11-13
|
* Remove extra admitted lemmas in 8.4Gravatar Jason Gross2016-11-12
|
* GF25519: add ErepAddGravatar Andres Erbsen2016-11-11
|
* [cbn] is 8.5 onlyGravatar Jason Gross2016-11-11
|
* Fix proofs broken by stronger preconditionsGravatar Jason Gross2016-11-11
|
* Most of the admits in Ed25519.vGravatar Rob Sloan2016-11-11
|
* extraction less slowGravatar Andres Erbsen2016-11-11
|
* Work around looping in 8.4Gravatar Jason Gross2016-11-10
| | | | This fixes #96
* Rewrite cast_word so that it's extracted betterGravatar Jason Gross2016-11-09
| | | | | | | | It will now be extracted as the identity function automatically, so we don't need to manually extract it as the empty string. This should also fix #93. (I think the issue was that this was an instance of https://coq.inria.fr/bugs/show_bug.cgi?id=4243.)
* implement X25519Gravatar Andres Erbsen2016-11-06
|
* move B_order_l and prime_qGravatar Andres Erbsen2016-11-06
|
* Connect [is_bounded] to [bounded_by]Gravatar Jason Gross2016-11-06
| | | | | This hooks up the boundedness constraints on [freeze] in GF25519Bounded to those in Ed25519.
* Work around a bug in 8.4 vm_computeGravatar Jason Gross2016-11-05
|
* put EdDSA encoding sign bit at the MSBGravatar Andres Erbsen2016-11-04
|
* fix extraction directives -- tested enc((l+1)B)=enc(B)Gravatar Andres Erbsen2016-11-03
|
* separate Ed25519Extraction.v, add extraction to MakefileGravatar Andres Erbsen2016-11-03
| | | | | @JasonGross: src/Specific/GF25519Bounded.v has another constant that I think needs a extraction-friendly version, I added a comment
* fix Word64 constants for extraction, check in more extraction directivesGravatar Andres Erbsen2016-11-03
|
* Make [freeze] proofs consider machine integer width and hard input bounds ↵Gravatar jadep2016-11-03
| | | | separately
* fix and prove ERepDec_correctGravatar Andres Erbsen2016-11-02
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 13:49:02 +0000