aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/GF25519Reflective/Reified
Commit message (Collapse)AuthorAge
* fix src/Specific/GF25519Reflective/Reified/AddCoordinates.vGravatar 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.
* Rename Interp lemmasGravatar Jason Gross2017-02-21
| | | | | | ```bash $ git grep --name-only 'Interp_InlineCast\|Interp_InlineConst\|Interp_Linearize' | xargs sed s'/Interp_/Interp/g' -i ```
* Add some display logsGravatar Jason Gross2017-02-15
|
* Add some display logsGravatar Jason Gross2017-02-15
|
* Add rudimentary Java and C notation files, displayGravatar Jason Gross2017-02-15
|
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
| | | | Also split off some bits of Util.Tactics
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We instead use the [Op] constructor for constants. This allows [exprf] to not depend on the interpretation function; this means we don't need to map over it to change the interpretation function. This saves us about 300 lines of code and about 30s of build time, total. After | File Name | Before || Change ----------------------------------------------------------------------------------------------------------- 18m11.34s | Total | 18m46.86s || -0m35.52s ----------------------------------------------------------------------------------------------------------- 0m19.99s | Specific/GF25519ReflectiveAddCoordinates | 0m31.78s || -0m11.79s 1m53.69s | Specific/GF25519Reflective/Reified/LadderStep | 2m01.32s || -0m07.62s 1m27.74s | Specific/GF25519Reflective/Reified/AddCoordinates | 1m34.03s || -0m06.29s 0m01.45s | Specific/GF25519Reflective | 0m06.31s || -0m04.85s 0m04.62s | Reflection/InlineInterp | 0m01.52s || +0m03.10s 1m19.68s | CompleteEdwardsCurve/ExtendedCoordinates | 1m21.19s || -0m01.50s 0m02.90s | Reflection/InlineWf | 0m01.80s || +0m01.09s N/A | Reflection/MapWithInterpInfo | 0m01.70s || -0m01.70s 1m32.32s | Test/Curve25519SpecTestVectors | 1m32.25s || +0m00.06s 1m12.79s | Experiments/Ed25519 | 1m13.17s || -0m00.38s 0m40.52s | ModularArithmetic/Conversion | 0m40.44s || +0m00.08s 0m34.57s | Spec/Ed25519 | 0m34.53s || +0m00.03s 0m30.82s | ModularArithmetic/ModularBaseSystemProofs | 0m30.89s || -0m00.07s 0m30.11s | Specific/GF25519Bounded | 0m30.21s || -0m00.10s 0m23.20s | Experiments/MontgomeryCurve | 0m23.26s || -0m00.06s 0m22.16s | Reflection/Z/Interpretations128/Relations | 0m21.72s || +0m00.44s 0m21.69s | ModularArithmetic/Pow2BaseProofs | 0m21.58s || +0m00.11s 0m20.25s | Algebra | 0m20.27s || -0m00.01s 0m19.81s | Specific/GF25519 | 0m19.83s || -0m00.01s 0m18.82s | Reflection/Z/Interpretations64/Relations | 0m18.50s || +0m00.32s 0m18.19s | EdDSARepChange | 0m18.26s || -0m00.07s 0m17.08s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m17.16s || -0m00.08s 0m14.10s | Util/ZUtil | 0m14.03s || +0m00.07s 0m10.05s | Testbit | 0m10.02s || +0m00.03s 0m08.95s | Specific/GF25519BoundedCommon | 0m08.90s || +0m00.04s 0m08.87s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.81s || +0m00.05s 0m08.80s | Assembly/GF25519 | 0m08.82s || -0m00.01s 0m08.80s | ModularArithmetic/Montgomery/ZProofs | 0m08.87s || -0m00.06s 0m08.51s | Encoding/PointEncoding | 0m08.53s || -0m00.01s 0m08.37s | BoundedArithmetic/Double/Proofs/Multiply | 0m08.39s || -0m00.02s 0m08.34s | Specific/GF1305 | 0m08.31s || +0m00.02s 0m07.85s | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m07.86s || -0m00.01s 0m07.60s | Specific/GF25519Reflective/Reified/Mul | 0m07.52s || +0m00.08s 0m07.13s | MxDHRepChange | 0m07.08s || +0m00.04s 0m06.85s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate | 0m06.77s || +0m00.08s 0m06.62s | Reflection/Z/InterpretationsGen | 0m06.62s || +0m00.00s 0m05.69s | Reflection/Z/Interpretations64/RelationsCombinations | 0m05.60s || +0m00.09s 0m05.68s | Reflection/Z/Interpretations128/RelationsCombinations | 0m05.67s || +0m00.00s 0m05.48s | Specific/SC25519 | 0m05.38s || +0m00.10s 0m05.40s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub | 0m05.36s || +0m00.04s 0m04.93s | ModularArithmetic/ModularBaseSystemListProofs | 0m04.96s || -0m00.03s 0m04.87s | WeierstrassCurve/Pre | 0m04.83s || +0m00.04s 0m04.45s | Specific/GF25519Reflective/Reified/PreFreeze | 0m04.56s || -0m00.10s 0m04.33s | Specific/GF25519Reflective/CommonBinOp | 0m04.55s || -0m00.21s 0m03.95s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.98s || -0m00.02s 0m03.87s | Specific/GF25519Reflective/CommonUnOp | 0m04.08s || -0m00.20s 0m03.86s | Encoding/PointEncodingPre | 0m03.88s || -0m00.02s 0m03.84s | BaseSystemProofs | 0m03.88s || -0m00.04s 0m03.75s | Specific/GF25519Reflective/CommonUnOpWireToFE | 0m03.96s || -0m00.20s 0m03.64s | CompleteEdwardsCurve/Pre | 0m03.60s || +0m00.04s 0m03.51s | BoundedArithmetic/InterfaceProofs | 0m03.42s || +0m00.08s 0m03.41s | ModularArithmetic/Tutorial | 0m03.38s || +0m00.03s 0m03.30s | Reflection/LinearizeWf | 0m04.24s || -0m00.94s 0m03.20s | Specific/GF25519Reflective/Reified/CarrySub | 0m03.28s || -0m00.07s 0m03.14s | ModularArithmetic/ZBoundedZ | 0m03.14s || +0m00.00s 0m03.14s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m03.14s || +0m00.00s 0m02.95s | Specific/GF25519Reflective/Reified/CarryAdd | 0m02.93s || +0m00.02s 0m02.92s | Specific/GF25519Reflective/Common9_4Op | 0m02.89s || +0m00.02s 0m02.82s | Specific/GF25519Reflective/Reified/CarryOpp | 0m02.95s || -0m00.13s 0m02.82s | BoundedArithmetic/Double/Proofs/Decode | 0m02.90s || -0m00.08s 0m02.69s | BoundedArithmetic/Double/Proofs/ShiftRight | 0m02.69s || +0m00.00s 0m02.66s | ModularArithmetic/ModularArithmeticTheorems | 0m02.67s || -0m00.00s 0m02.63s | Specific/FancyMachine256/Montgomery | 0m02.24s || +0m00.38s 0m02.61s | Specific/GF25519Reflective/CommonUnOpFEToWire | 0m02.76s || -0m00.14s 0m02.58s | BoundedArithmetic/Double/Proofs/ShiftLeft | 0m02.58s || +0m00.00s 0m02.56s | Specific/GF25519Reflective/Common | 0m02.60s || -0m00.04s 0m02.52s | Specific/FancyMachine256/Barrett | 0m02.20s || +0m00.31s 0m02.50s | Specific/GF25519BoundedAddCoordinates | 0m02.60s || -0m00.10s 0m02.39s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.31s || +0m00.08s 0m02.34s | ModularArithmetic/ModularBaseSystemOpt | 0m02.31s || +0m00.02s 0m02.02s | Specific/GF25519Reflective/Reified/Sub | 0m02.01s || +0m00.01s 0m01.98s | Reflection/WfReflective | 0m02.54s || -0m00.56s 0m01.94s | Specific/GF25519Reflective/Reified/Pack | 0m02.07s || -0m00.12s 0m01.93s | Assembly/Evaluables | 0m01.93s || +0m00.00s 0m01.92s | Specific/GF25519Reflective/Reified/Unpack | 0m02.04s || -0m00.12s 0m01.90s | Specific/FancyMachine256/Core | 0m01.79s || +0m00.10s 0m01.79s | ModularArithmetic/Montgomery/ZBounded | 0m01.86s || -0m00.07s 0m01.77s | Specific/GF25519ExtendedAddCoordinates | 0m01.76s || +0m00.01s 0m01.68s | Specific/GF25519Reflective/Reified/Add | 0m01.69s || -0m00.01s 0m01.67s | Specific/GF25519BoundedExtendedAddCoordinates | 0m01.79s || -0m00.12s 0m01.63s | Experiments/Ed25519Extraction | 0m01.66s || -0m00.03s 0m01.62s | Specific/GF25519Reflective/Reified/Opp | 0m01.72s || -0m00.09s 0m01.54s | Specific/GF25519Reflective/Reified/GeModulus | 0m01.59s || -0m00.05s 0m01.50s | Reflection/TestCase | 0m01.42s || +0m00.08s 0m01.47s | ModularArithmetic/BarrettReduction/Z | 0m01.47s || +0m00.00s 0m01.43s | Assembly/Compile | 0m01.46s || -0m00.03s 0m01.33s | Reflection/WfProofs | 0m01.95s || -0m00.61s 0m01.26s | ModularArithmetic/PrimeFieldTheorems | 0m01.28s || -0m00.02s 0m01.20s | Assembly/Conversions | 0m01.19s || +0m00.01s 0m01.16s | ModularArithmetic/ExtendedBaseVector | 0m01.22s || -0m00.06s 0m01.16s | BaseSystem | 0m01.15s || +0m00.01s 0m01.09s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.11s || -0m00.02s 0m00.99s | Util/NumTheoryUtil | 0m00.96s || +0m00.03s 0m00.96s | Assembly/HL | 0m00.96s || +0m00.00s 0m00.94s | Assembly/LL | 0m00.99s || -0m00.05s 0m00.94s | Assembly/Pipeline | 0m00.92s || +0m00.01s 0m00.88s | Reflection/WfInversion | 0m01.21s || -0m00.32s 0m00.86s | Assembly/PhoasCommon | 0m00.91s || -0m00.05s 0m00.86s | Specific/GF25519Reflective/CommonUnOpFEToZ | 0m01.02s || -0m00.16s 0m00.85s | BoundedArithmetic/Double/Proofs/LoadImmediate | 0m00.86s || -0m00.01s 0m00.84s | BoundedArithmetic/Double/Proofs/BitwiseOr | 0m00.91s || -0m00.07s 0m00.82s | BoundedArithmetic/X86ToZLikeProofs | 0m00.85s || -0m00.03s 0m00.79s | Util/IterAssocOp | 0m00.82s || -0m00.02s 0m00.75s | Reflection/Z/Syntax | 0m00.67s || +0m00.07s 0m00.73s | Util/PartiallyReifiedProp | 0m00.73s || +0m00.00s 0m00.70s | Encoding/ModularWordEncodingTheorems | 0m00.76s || -0m00.06s 0m00.70s | Specific/GF25519Reflective/Reified | 0m00.72s || -0m00.02s 0m00.66s | BoundedArithmetic/Double/Repeated/Proofs/Multiply | 0m00.62s || +0m00.04s 0m00.66s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.66s || +0m00.00s 0m00.64s | Encoding/ModularWordEncodingPre | 0m00.63s || +0m00.01s 0m00.61s | ModularArithmetic/ModularBaseSystem | 0m00.66s || -0m00.05s 0m00.61s | Util/AdditionChainExponentiation | 0m00.64s || -0m00.03s 0m00.60s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.64s || -0m00.04s 0m00.60s | Reflection/MultiSizeTest2 | 0m00.71s || -0m00.10s 0m00.60s | Spec/EdDSA | 0m00.65s || -0m00.05s 0m00.59s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.51s || +0m00.07s 0m00.58s | BoundedArithmetic/Interface | 0m00.60s || -0m00.02s 0m00.58s | ModularArithmetic/ModularBaseSystemList | 0m00.61s || -0m00.03s 0m00.55s | Spec/ModularWordEncoding | 0m00.63s || -0m00.07s 0m00.55s | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight | 0m00.50s || +0m00.05s 0m00.55s | Reflection/InterpWfRel | 0m00.58s || -0m00.02s 0m00.54s | BoundedArithmetic/X86ToZLike | 0m00.55s || -0m00.01s 0m00.54s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.53s || +0m00.01s 0m00.54s | BoundedArithmetic/Double/Proofs/SelectConditional | 0m00.62s || -0m00.07s 0m00.54s | Reflection/WfReflectiveGen | 0m00.58s || -0m00.03s 0m00.52s | BoundedArithmetic/ArchitectureToZLike | 0m00.41s || +0m00.11s 0m00.51s | BoundedArithmetic/Double/Core | 0m00.48s || +0m00.03s 0m00.50s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.51s || -0m00.01s 0m00.49s | Spec/WeierstrassCurve | 0m00.42s || +0m00.07s 0m00.48s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.54s || -0m00.06s 0m00.47s | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.58s || -0m00.10s 0m00.47s | Reflection/InterpWf | 0m00.50s || -0m00.03s 0m00.47s | ModularArithmetic/Pre | 0m00.48s || -0m00.01s 0m00.47s | BoundedArithmetic/Double/Repeated/Core | 0m00.46s || +0m00.00s 0m00.46s | Reflection/Z/Interpretations64 | 0m00.49s || -0m00.02s 0m00.45s | Reflection/InputSyntax | 0m00.42s || +0m00.03s N/A | Reflection/MapInterpWf | 0m00.44s || -0m00.44s 0m00.44s | Spec/CompleteEdwardsCurve | 0m00.39s || +0m00.04s 0m00.44s | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic | 0m00.42s || +0m00.02s 0m00.44s | Reflection/Z/Interpretations128 | 0m00.52s || -0m00.08s 0m00.44s | ModularArithmetic/ZBounded | 0m00.45s || -0m00.01s 0m00.42s | BoundedArithmetic/StripCF | 0m00.42s || +0m00.00s 0m00.42s | Reflection/Z/Reify | 0m00.43s || -0m00.01s 0m00.42s | ModularArithmetic/ModularBaseSystemListZOperationsProofs | 0m00.47s || -0m00.04s 0m00.41s | Reflection/Named/DeadCodeElimination | 0m00.43s || -0m00.02s 0m00.41s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.38s || +0m00.02s 0m00.41s | Spec/ModularArithmetic | 0m00.34s || +0m00.06s 0m00.41s | Reflection/Named/RegisterAssign | 0m00.37s || +0m00.03s 0m00.41s | Reflection/Reify | 0m00.39s || +0m00.01s 0m00.40s | ModularArithmetic/Pow2Base | 0m00.42s || -0m00.01s 0m00.40s | Reflection/Named/EstablishLiveness | 0m00.33s || +0m00.07s 0m00.40s | Reflection/ExprInversion | 0m00.57s || -0m00.16s 0m00.40s | Reflection/Named/Syntax | 0m00.40s || +0m00.00s 0m00.38s | Reflection/Named/Compile | 0m00.34s || +0m00.03s N/A | Reflection/MapInterp | 0m00.38s || -0m00.38s 0m00.38s | ModularArithmetic/Montgomery/Z | 0m00.39s || -0m00.01s 0m00.38s | ModularArithmetic/ModularBaseSystemWord | 0m00.36s || +0m00.02s N/A | Reflection/WfRel | 0m00.38s || -0m00.38s 0m00.38s | Reflection/Tuple | N/A || +0m00.38s 0m00.37s | Spec/MxDH | 0m00.39s || -0m00.02s 0m00.37s | BoundedArithmetic/Eta | 0m00.36s || +0m00.01s 0m00.36s | Reflection/Named/ContextOn | 0m00.37s || -0m00.01s 0m00.34s | Reflection/FilterLive | 0m00.34s || +0m00.00s 0m00.34s | Reflection/LinearizeInterp | 0m00.53s || -0m00.19s 0m00.33s | Reflection/Relations | N/A || +0m00.33s 0m00.32s | Reflection/Equality | 0m00.41s || -0m00.08s 0m00.30s | Reflection/Syntax | 0m00.52s || -0m00.22s 0m00.30s | Reflection/InterpProofs | 0m00.47s || -0m00.17s 0m00.30s | Reflection/ApplicationLemmas | 0m00.43s || -0m00.13s 0m00.30s | Reflection/CommonSubexpressionElimination | 0m00.50s || -0m00.20s 0m00.28s | Reflection/Inline | 0m00.37s || -0m00.08s 0m00.28s | Reflection/Conversion | 0m00.44s || -0m00.15s 0m00.27s | Reflection/MapCastWithCastOp | 0m00.38s || -0m00.10s 0m00.26s | Reflection/MapCast | 0m00.40s || -0m00.14s 0m00.26s | Reflection/ApplicationRelations | 0m00.35s || -0m00.08s 0m00.24s | Reflection/Application | 0m00.38s || -0m00.14s 0m00.23s | Reflection/Linearize | 0m00.35s || -0m00.11s 0m00.20s | Reflection/CountLets | 0m00.33s || -0m00.13s 0m00.20s | Reflection/Named/NameUtil | 0m00.36s || -0m00.15s 0m00.09s | Util/PointedProp | 0m00.08s || +0m00.00s 0m00.05s | Util/LetIn | 0m00.06s || -0m00.00s 0m00.03s | Util/Notations | 0m00.03s || +0m00.00s 0m00.03s | Util/AutoRewrite | 0m00.03s || +0m00.00s
* Add reified LadderStep without carriesGravatar Jason Gross2017-01-07
|
* Fix some problems with previous commitGravatar Jason Gross2016-11-17
|
* Remove admits, fill templates, copy boundsGravatar Jason Gross2016-11-17
|
* Update AddCoordinatesGravatar Jason Gross2016-11-17
| | | | Now the _correct_and_bounded lemma goes through
* Minor change in AddCoordinatesGravatar Jason Gross2016-11-17
|
* Move util definitions to util folderGravatar Jason Gross2016-11-17
|
* Add reified mostly-bounds-checked add_coordinatesGravatar Jason Gross2016-11-17
|
* Remove dead code in rebuild-reified.pyGravatar Jason Gross2016-11-11
|
* Begin filling in @JasonGross's stubsGravatar jadep2016-11-11
|
* Freeze stubsGravatar Jason Gross2016-11-11
|
* Split up GF25519Reflective.Common: faster+parallelGravatar Jason Gross2016-11-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change -------------------------------------------------------------------------------- 2m53.12s | Total | 2m52.26s || +0m00.85s -------------------------------------------------------------------------------- 0m01.38s | Specific/GF25519Reflective/Common | 0m43.51s || -0m42.12s 0m14.82s | Specific/GF25519Reflective/CommonBinOp | N/A || +0m14.82s 0m10.91s | Specific/GF25519Reflective/CommonUnOp | N/A || +0m10.91s 0m10.44s | Specific/GF25519Reflective/CommonUnOpWireToFE | N/A || +0m10.43s 0m06.42s | Specific/GF25519Reflective/CommonUnOpFEToWire | N/A || +0m06.41s 1m18.24s | Experiments/Ed25519 | 1m18.57s || -0m00.32s 0m07.97s | Specific/GF25519Reflective/Reified/Mul | 0m08.45s || -0m00.47s 0m07.89s | Specific/GF25519Reflective/Reified/Freeze | 0m07.84s || +0m00.04s 0m06.87s | Specific/GF25519Reflective | 0m06.92s || -0m00.04s 0m03.53s | Specific/GF25519Reflective/Reified/CarrySub | 0m03.63s || -0m00.10s 0m03.27s | Specific/GF25519Reflective/Reified/CarryAdd | 0m03.28s || -0m00.00s 0m03.18s | Specific/GF25519Reflective/Reified/CarryOpp | 0m03.15s || +0m00.03s 0m02.24s | Specific/GF25519Reflective/Reified/Unpack | 0m02.21s || +0m00.03s 0m02.19s | Specific/GF25519Reflective/Reified/Pack | 0m02.28s || -0m00.08s 0m02.16s | Specific/GF25519Reflective/Reified/Sub | 0m02.15s || +0m00.01s 0m02.14s | Specific/GF25519Bounded | 0m02.07s || +0m00.07s 0m02.07s | Experiments/Ed25519Extraction | 0m02.16s || -0m00.09s 0m01.99s | Specific/GF25519Reflective/Reified/Add | 0m01.81s || +0m00.17s 0m01.82s | Specific/GF25519Reflective/Reified/Opp | 0m01.78s || +0m00.04s 0m01.76s | Specific/GF25519Reflective/Reified/GeModulus | 0m01.71s || +0m00.05s 0m00.97s | Specific/GF25519Reflective/CommonUnOpFEToZ | N/A || +0m00.97s 0m00.86s | Specific/GF25519Reflective/Reified | 0m00.75s || +0m00.10s
* Plug in boundedness proofsGravatar Jason Gross2016-11-05
| | | | | We no longer admit the boundedness proofs (other than freeze); a significant chunk of the boundedness proofs now line up nicely.
* Add better bounded lemmas to reified thingsGravatar Jason Gross2016-11-05
|
* Add code for overflow check (disabled bc freeze)Gravatar Jason Gross2016-11-05
| | | | | | | Currently freeze overflows; Jade says this is because the carry chain got reversed, and that she'll work on fixing this. We should enable the sanity checks at some point after this is fixed, to fail early if things overflow.
* Print out the computed bounds on the various opsGravatar Jason Gross2016-11-01
| | | | | | | | | Apparently some of them overflow (carry_opp, opp, sub, carry_sub) Also the bounds on ge_modulus are probably wrong, given that it's claiming that the function always returns 0. cc @andres-erbsen @jadep
* Also construct relatedness proofs in reifiedGravatar Jason Gross2016-10-30
|
* Add reification of various operationsGravatar Jason Gross2016-10-30
We split the reification up into separate files, one operation per file, so that we can run all the reification in parallel when building.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 08:34:49 +0000