make fsatz recurse when proving nonzero-ness, undo Weierstrass workaround

After     | File Name                                                              | Before    || Change
-----------------------------------------------------------------------------------------------------------
29m00.03s | Total                                                                  | 33m00.88s || -4m00.84s
-----------------------------------------------------------------------------------------------------------
11m48.99s | WeierstrassCurve/WeierstrassCurveTheorems                              | 16m37.07s || -4m00.08s
1m46.82s  | Test/Curve25519SpecTestVectors                                         | 1m47.06s  || -0m00.24s
1m18.46s  | Spec/MontgomeryCurve                                                   | 0m43.03s  || +0m00.43s
0m50.03s  | Specific/GF25519Reflective/Reified/LadderStep                          | 0m50.00s  || +0m00.03s
0m43.21s  | Spec/Ed25519                                                           | 0m42.48s  || +0m00.73s
0m37.78s  | ModularArithmetic/Conversion                                           | 0m40.14s  || -0m00.35s
0m34.92s  | Specific/GF25519Reflective/Reified/AddCoordinates                      | 0m36.07s  || -0m00.14s
0m32.14s  | Specific/GF25519Bounded                                                | 0m31.64s  || +0m00.50s
0m29.53s  | ModularArithmetic/ModularBaseSystemProofs                              | 0m29.72s  || -0m00.18s
0m24.83s  | Reflection/Z/Interpretations128/Relations                              | 0m23.35s  || +0m00.47s
0m23.51s  | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems                      | 0m23.57s  || -0m00.05s
0m20.51s  | ModularArithmetic/Pow2BaseProofs                                       | 0m22.19s  || -0m00.67s
0m20.13s  | Specific/GF25519                                                       | 0m22.72s  || -0m00.58s
0m19.08s  | Reflection/Named/MapCastWf                                             | 0m19.60s  || -0m00.52s
0m18.74s  | CompleteEdwardsCurve/ExtendedCoordinates                               | 0m17.30s  || +0m00.43s
0m18.47s  | Reflection/Z/Interpretations64/Relations                               | 0m19.28s  || -0m00.81s
0m18.12s  | EdDSARepChange                                                         | 0m18.55s  || -0m00.42s
0m14.69s  | Util/ZUtil                                                             | 0m15.19s  || -0m00.50s
0m13.86s  | Reflection/Named/ContextProperties/SmartMap                            | 0m14.23s  || -0m00.37s
0m13.65s  | Reflection/Named/ContextProperties/NameUtil                            | 0m15.92s  || -0m00.26s
0m11.98s  | Specific/GF25519Reflective/Reified/Mul                                 | 0m12.53s  || -0m00.54s
0m11.84s  | Experiments/Ed25519                                                    | 0m11.87s  || -0m00.02s
0m11.64s  | Specific/NewBaseSystemTest                                             | 0m11.70s  || -0m00.05s
0m11.28s  | Algebra/Field                                                          | 0m11.55s  || -0m00.27s
0m09.04s  | Reflection/Named/MapCastInterp                                         | 0m09.25s  || -0m00.21s
0m09.02s  | Assembly/GF25519                                                       | 0m09.52s  || -0m00.50s
0m08.92s  | Specific/GF25519BoundedCommon                                          | 0m08.75s  || +0m00.16s
0m08.88s  | Testbit                                                                | 0m10.14s  || -0m00.25s
0m08.25s  | BoundedArithmetic/Double/Proofs/Multiply                               | 0m08.14s  || +0m00.10s
0m08.16s  | ModularArithmetic/Montgomery/ZProofs                                   | 0m08.50s  || -0m00.33s
0m08.02s  | BoundedArithmetic/ArchitectureToZLikeProofs                            | 0m08.18s  || -0m00.16s
0m07.94s  | Reflection/InlineWf                                                    | 0m08.34s  || -0m00.39s
0m07.48s  | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate                    | 0m06.54s  || +0m00.94s
0m07.47s  | Algebra/Ring                                                           | 0m07.50s  || -0m00.03s
0m07.41s  | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate          | 0m07.65s  || -0m00.24s
0m07.10s  | MxDHRepChange                                                          | 0m07.48s  || -0m00.38s
0m06.48s  | Specific/GF1305                                                        | 0m06.40s  || +0m00.08s
0m06.33s  | BoundedArithmetic/Double/Proofs/RippleCarryAddSub                      | 0m05.14s  || +0m00.19s
0m06.27s  | Reflection/Z/InterpretationsGen                                        | 0m06.42s  || -0m00.15s
0m06.01s  | Specific/GF25519Reflective/Reified/PreFreeze                           | 0m05.91s  || +0m00.09s
0m05.96s  | Bedrock/Word                                                           | 0m05.77s  || +0m00.19s
0m05.90s  | NewBaseSystem                                                          | 0m06.06s  || -0m00.15s
0m05.76s  | Util/FixedWordSizesEquality                                            | 0m05.98s  || -0m00.22s
0m05.49s  | Specific/GF25519Reflective/Reified/CarrySub                            | 0m05.42s  || +0m00.07s
0m05.38s  | CompleteEdwardsCurve/Pre                                               | 0m04.22s  || +0m00.16s
0m05.17s  | Specific/SC25519                                                       | 0m05.31s  || -0m00.13s
0m05.08s  | Util/ListUtil                                                          | 0m05.16s  || -0m00.08s
0m05.04s  | Experiments/GenericFieldPow                                            | 0m05.20s  || -0m00.16s
0m05.01s  | Specific/GF25519Reflective/Reified/CarryAdd                            | 0m05.04s  || -0m00.03s
0m04.98s  | Specific/GF25519Reflective/CommonBinOp                                 | 0m05.18s  || -0m00.19s
0m04.75s  | ModularArithmetic/ModularBaseSystemListProofs                          | 0m04.81s  || -0m00.05s
0m04.59s  | Algebra/Field_test                                                     | 0m12.12s  || -0m00.52s
0m04.48s  | Reflection/InlineCastWf                                                | 0m04.72s  || -0m00.23s
0m03.97s  | Specific/GF25519Reflective/CommonUnOp                                  | 0m04.16s  || -0m00.18s
0m03.97s  | Specific/GF25519Reflective/Common9_4Op                                 | 0m04.11s  || -0m00.14s
0m03.96s  | Specific/GF25519Reflective/CommonUnOpWireToFE                          | 0m03.91s  || +0m00.04s
0m03.70s  | Specific/GF25519Reflective/Reified/CarryOpp                            | 0m03.73s  || -0m00.02s
0m03.53s  | ModularArithmetic/BarrettReduction/ZHandbook                           | 0m03.71s  || -0m00.18s
0m03.51s  | BaseSystemProofs                                                       | 0m03.52s  || -0m00.01s
0m03.39s  | Reflection/EtaWf                                                       | 0m03.45s  || -0m00.06s
0m03.37s  | Reflection/Named/CompileWf                                             | 0m03.81s  || -0m00.43s
0m03.34s  | Specific/GF25519Reflective/Reified/Sub                                 | 0m03.47s  || -0m00.13s
0m03.16s  | BoundedArithmetic/InterfaceProofs                                      | 0m03.14s  || +0m00.02s
0m02.99s  | Reflection/LinearizeWf                                                 | 0m03.09s  || -0m00.09s
0m02.90s  | Specific/GF25519Reflective/Reified/Add                                 | 0m03.02s  || -0m00.12s
0m02.84s  | ModularArithmetic/BarrettReduction/ZGeneralized                        | 0m02.88s  || -0m00.04s
0m02.79s  | Specific/FancyMachine256/Montgomery                                    | 0m02.77s  || +0m00.02s
0m02.77s  | ModularArithmetic/ZBoundedZ                                            | 0m02.91s  || -0m00.14s
0m02.74s  | Reflection/Named/CompileInterp                                         | 0m03.65s  || -0m00.90s
0m02.68s  | BoundedArithmetic/Double/Proofs/Decode                                 | 0m02.62s  || +0m00.06s
0m02.68s  | Specific/GF25519Reflective/CommonUnOpFEToWire                          | 0m02.72s  || -0m00.04s
0m02.63s  | ModularArithmetic/ModularArithmeticTheorems                            | 0m02.65s  || -0m00.02s
0m02.62s  | Specific/FancyMachine256/Barrett                                       | 0m02.58s  || +0m00.04s
0m02.58s  | Specific/GF25519Reflective/Reified/Pack                                | 0m02.56s  || +0m00.02s
0m02.54s  | Reflection/InlineInterp                                                | 0m02.53s  || +0m00.01s
0m02.46s  | BoundedArithmetic/Double/Proofs/ShiftRight                             | 0m02.52s  || -0m00.06s
0m02.42s  | Specific/GF25519Reflective/Reified/Unpack                              | 0m02.42s  || +0m00.00s
0m02.40s  | Specific/GF25519ReflectiveAddCoordinates                               | 0m02.33s  || +0m00.06s
0m02.39s  | Reflection/Named/ContextProperties                                     | 0m02.42s  || -0m00.02s
0m02.38s  | BoundedArithmetic/Double/Proofs/ShiftLeft                              | 0m02.40s  || -0m00.02s
0m02.34s  | Assembly/State                                                         | 0m02.44s  || -0m00.10s
0m02.22s  | Specific/GF25519Reflective/Reified/Opp                                 | 0m02.23s  || -0m00.00s
0m02.22s  | Reflection/Named/NameUtilProperties                                    | 0m02.31s  || -0m00.08s
0m02.18s  | ModularArithmetic/ModularBaseSystemOpt                                 | 0m02.19s  || -0m00.00s
0m02.16s  | Reflection/WfProofs                                                    | 0m02.15s  || +0m00.01s
0m02.14s  | ModularArithmetic/BarrettReduction/ZBounded                            | 0m02.19s  || -0m00.04s
0m02.12s  | Reflection/TestCase                                                    | 0m02.23s  || -0m00.10s
0m01.99s  | Specific/GF25519Reflective/Reified/GeModulus                           | 0m01.96s  || +0m00.03s
0m01.90s  | WeierstrassCurve/Pre                                                   | 0m01.55s  || +0m00.34s
0m01.87s  | Reflection/WfReflective                                                | 0m01.83s  || +0m00.04s
0m01.79s  | Util/WordUtil                                                          | 0m01.82s  || -0m00.03s
0m01.76s  | Specific/FancyMachine256/Core                                          | 0m01.75s  || +0m00.01s
0m01.71s  | SaturatedBaseSystem                                                    | 0m01.92s  || -0m00.20s
0m01.68s  | Algebra/Group                                                          | 0m01.72s  || -0m00.04s
0m01.67s  | ModularArithmetic/Montgomery/ZBounded                                  | 0m01.68s  || -0m00.01s
0m01.63s  | Assembly/Evaluables                                                    | 0m01.68s  || -0m00.05s
0m01.45s  | Specific/GF25519Reflective/Common                                      | 0m01.39s  || +0m00.06s
0m01.43s  | Reflection/Z/Interpretations128/RelationsCombinations                  | 0m01.16s  || +0m00.27s
0m01.42s  | Reflection/Named/InterpretToPHOASWf                                    | 0m01.51s  || -0m00.09s
0m01.32s  | Util/NatUtil                                                           | 0m01.32s  || +0m00.00s
0m01.30s  | Util/Tuple                                                             | 0m01.30s  || +0m00.00s
0m01.30s  | ModularArithmetic/PrimeFieldTheorems                                   | 0m01.29s  || +0m00.01s
0m01.30s  | Assembly/WordizeUtil                                                   | 0m01.46s  || -0m00.15s
0m01.30s  | ModularArithmetic/BarrettReduction/Z                                   | 0m01.34s  || -0m00.04s
0m01.30s  | Reflection/MapCastInterp                                               | 0m01.30s  || +0m00.00s
0m01.26s  | Specific/GF25519Reflective                                             | 0m01.30s  || -0m00.04s
0m01.22s  | Assembly/Compile                                                       | 0m01.26s  || -0m00.04s
0m01.21s  | Reflection/Z/Interpretations64/RelationsCombinations                   | 0m01.19s  || +0m00.02s
0m01.20s  | Reflection/Z/Syntax/Equality                                           | 0m01.17s  || +0m00.03s
0m01.18s  | Assembly/Bounds                                                        | 0m01.35s  || -0m00.17s
0m01.06s  | BaseSystem                                                             | 0m01.05s  || +0m00.01s
0m01.01s  | Experiments/Ed25519Extraction                                          | 0m00.98s  || +0m00.03s
0m01.00s  | Reflection/SmartBoundInterp                                            | 0m01.02s  || -0m00.02s
0m00.99s  | BoundedArithmetic/Double/Repeated/Proofs/Decode                        | 0m01.02s  || -0m00.03s
0m00.99s  | Reflection/Relations                                                   | 0m00.96s  || +0m00.03s
0m00.96s  | ModularArithmetic/ExtendedBaseVector                                   | 0m01.03s  || -0m00.07s
0m00.89s  | Assembly/Conversions                                                   | 0m00.89s  || +0m00.00s
0m00.89s  | Reflection/Named/InterpretToPHOASInterp                                | 0m00.92s  || -0m00.03s
0m00.88s  | Reflection/SmartCastWf                                                 | 0m00.89s  || -0m00.01s
0m00.84s  | Algebra/IntegralDomain                                                 | 0m00.86s  || -0m00.02s
0m00.84s  | Reflection/InlineCastInterp                                            | 0m00.89s  || -0m00.05s
0m00.80s  | Specific/GF25519Reflective/CommonUnOpFEToZ                             | 0m00.87s  || -0m00.06s
0m00.79s  | Util/NumTheoryUtil                                                     | 0m00.94s  || -0m00.14s
0m00.78s  | BoundedArithmetic/Double/Proofs/BitwiseOr                              | 0m00.76s  || +0m00.02s
0m00.76s  | Reflection/MapCastByDeBruijnInterp                                     | 0m00.72s  || +0m00.04s
0m00.75s  | BoundedArithmetic/Double/Proofs/LoadImmediate                          | 0m00.76s  || -0m00.01s
0m00.74s  | BoundedArithmetic/X86ToZLikeProofs                                     | 0m00.73s  || +0m00.01s
0m00.74s  | Reflection/WfInversion                                                 | 0m00.78s  || -0m00.04s
0m00.73s  | Reflection/Named/CompileProperties                                     | 0m00.77s  || -0m00.04s
0m00.71s  | Assembly/LL                                                            | 0m00.73s  || -0m00.02s
0m00.69s  | Assembly/Pipeline                                                      | 0m00.69s  || +0m00.00s
0m00.69s  | Util/IterAssocOp                                                       | 0m00.74s  || -0m00.05s
0m00.68s  | Assembly/HL                                                            | 0m00.70s  || -0m00.01s
0m00.68s  | Util/PartiallyReifiedProp                                              | 0m00.70s  || -0m00.01s
0m00.67s  | Karatsuba                                                              | 0m00.71s  || -0m00.03s
0m00.67s  | Assembly/QhasmEvalCommon                                               | 0m00.67s  || +0m00.00s
0m00.66s  | Specific/GF25519BoundedAddCoordinates                                  | 0m00.63s  || +0m00.03s
0m00.65s  | Assembly/PhoasCommon                                                   | 0m00.62s  || +0m00.03s
0m00.62s  | Specific/GF25519Reflective/Reified                                     | 0m00.62s  || +0m00.00s
0m00.62s  | Reflection/MultiSizeTest                                               | 0m00.65s  || -0m00.03s
0m00.58s  | ModularArithmetic/PseudoMersenneBaseParamProofs                        | 0m00.58s  || +0m00.00s
0m00.58s  | Reflection/MapCastByDeBruijnWf                                         | 0m00.57s  || +0m00.01s
0m00.58s  | Spec/WeierstrassCurve                                                  | 0m00.48s  || +0m00.09s
0m00.55s  | Encoding/ModularWordEncodingTheorems                                   | 0m00.58s  || -0m00.02s
0m00.54s  | ModularArithmetic/ExtPow2BaseMulProofs                                 | 0m00.53s  || +0m00.01s
0m00.53s  | Spec/EdDSA                                                             | 0m00.53s  || +0m00.00s
0m00.53s  | Util/AdditionChainExponentiation                                       | 0m00.56s  || -0m00.03s
0m00.53s  | BoundedArithmetic/Double/Repeated/Proofs/Multiply                      | 0m00.53s  || +0m00.00s
0m00.52s  | Reflection/InterpByIsoProofs                                           | 0m00.53s  || -0m00.01s
0m00.52s  | Reflection/Named/WfInterp                                              | 0m00.52s  || +0m00.00s
0m00.51s  | ModularArithmetic/ModularBaseSystemList                                | 0m00.51s  || +0m00.00s
0m00.51s  | BoundedArithmetic/Interface                                            | 0m00.51s  || +0m00.00s
0m00.51s  | BoundedArithmetic/X86ToZLike                                           | 0m00.53s  || -0m00.02s
0m00.51s  | Encoding/ModularWordEncodingPre                                        | 0m00.53s  || -0m00.02s
0m00.51s  | Reflection/WfReflectiveGen                                             | 0m00.48s  || +0m00.03s
0m00.50s  | ModularArithmetic/ModularBaseSystem                                    | 0m00.54s  || -0m00.04s
0m00.50s  | Reflection/Named/FMapContext                                           | 0m00.52s  || -0m00.02s
0m00.49s  | BoundedArithmetic/Double/Proofs/SelectConditional                      | 0m00.48s  || +0m00.01s
0m00.48s  | Spec/ModularWordEncoding                                               | 0m00.50s  || -0m00.02s
0m00.47s  | Spec/CompleteEdwardsCurve                                              | 0m00.48s  || -0m00.01s
0m00.47s  | Assembly/StringConversion                                              | 0m00.42s  || +0m00.04s
0m00.47s  | Reflection/InterpWfRel                                                 | 0m00.47s  || +0m00.00s
0m00.47s  | Reflection/BoundByCastInterp                                           | 0m00.45s  || +0m00.01s
0m00.46s  | Util/CPSUtil                                                           | 0m00.51s  || -0m00.04s
0m00.45s  | Algebra/ScalarMult                                                     | 0m00.47s  || -0m00.01s
0m00.44s  | Util/Decidable                                                         | 0m00.43s  || +0m00.01s
0m00.44s  | BoundedArithmetic/Double/Core                                          | 0m00.41s  || +0m00.03s
0m00.44s  | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub             | 0m00.42s  || +0m00.02s
0m00.44s  | Reflection/SmartBoundWf                                                | 0m00.45s  || -0m00.01s
0m00.43s  | BoundedArithmetic/Double/Repeated/Core                                 | 0m00.43s  || +0m00.00s
0m00.43s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight                | 0m00.44s  || -0m00.01s
0m00.43s  | Util/HList                                                             | 0m00.43s  || +0m00.00s
0m00.43s  | Reflection/InputSyntax                                                 | 0m00.42s  || +0m00.01s
0m00.42s  | Algebra/Monoid                                                         | 0m00.46s  || -0m00.04s
0m00.42s  | Assembly/Qhasm                                                         | 0m00.43s  || -0m00.01s
0m00.42s  | Util/NUtil                                                             | 0m00.43s  || -0m00.01s
0m00.41s  | ModularArithmetic/ZBounded                                             | 0m00.40s  || +0m00.00s
0m00.41s  | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate                 | 0m00.39s  || +0m00.01s
0m00.41s  | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional             | 0m00.41s  || +0m00.00s
0m00.41s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.42s  || -0m00.01s
0m00.41s  | Reflection/Named/PositiveContext/DefaultsProperties                    | 0m00.36s  || +0m00.04s
0m00.40s  | ModularArithmetic/Pre                                                  | 0m00.43s  || -0m00.02s
0m00.40s  | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr                     | 0m00.44s  || -0m00.03s
0m00.40s  | Reflection/Z/Interpretations64                                         | 0m00.40s  || +0m00.00s
0m00.40s  | Reflection/Z/Reify                                                     | 0m00.40s  || +0m00.00s
0m00.40s  | Reflection/InterpWf                                                    | 0m00.41s  || -0m00.00s
0m00.39s  | BoundedArithmetic/ArchitectureToZLike                                  | 0m00.41s  || -0m00.01s
0m00.39s  | BoundedArithmetic/StripCF                                              | 0m00.41s  || -0m00.01s
0m00.39s  | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic                   | 0m00.39s  || +0m00.00s
0m00.39s  | Reflection/Z/BoundsInterpretations                                     | 0m00.38s  || +0m00.01s
0m00.39s  | Reflection/Z/Interpretations128                                        | 0m00.41s  || -0m00.01s
0m00.38s  | Algebra                                                                | 0m00.35s  || +0m00.03s
0m00.38s  | Reflection/Z/Syntax                                                    | 0m00.37s  || +0m00.01s
0m00.38s  | Reflection/Z/Syntax/Util                                               | 0m00.35s  || +0m00.03s
0m00.36s  | Reflection/MapCastByDeBruijn                                           | 0m00.35s  || +0m00.01s
0m00.35s  | ModularArithmetic/ModularBaseSystemListZOperations                     | 0m00.33s  || +0m00.01s
0m00.35s  | ModularArithmetic/ModularBaseSystemListZOperationsProofs               | 0m00.34s  || +0m00.00s
0m00.35s  | Reflection/Z/HexNotationConstants                                      | 0m00.35s  || +0m00.00s
0m00.34s  | Spec/MxDH                                                              | 0m00.34s  || +0m00.00s
0m00.34s  | ModularArithmetic/Pow2Base                                             | 0m00.39s  || -0m00.04s
0m00.34s  | Assembly/QhasmUtil                                                     | 0m00.36s  || -0m00.01s
0m00.34s  | ModularArithmetic/PseudoMersenneBaseParams                             | 0m00.42s  || -0m00.07s
0m00.34s  | ModularArithmetic/Montgomery/Z                                         | 0m00.33s  || +0m00.01s
0m00.34s  | Reflection/Named/PositiveContext/Defaults                              | 0m00.33s  || +0m00.01s
0m00.34s  | Reflection/Named/RegisterAssign                                        | 0m00.36s  || -0m00.01s
0m00.34s  | Reflection/Named/DeadCodeElimination                                   | 0m00.35s  || -0m00.00s
0m00.33s  | BoundedArithmetic/Eta                                                  | 0m00.37s  || -0m00.03s
0m00.33s  | Reflection/Tuple                                                       | 0m00.33s  || +0m00.00s
0m00.33s  | ModularArithmetic/ModularBaseSystemWord                                | 0m00.32s  || +0m00.01s
0m00.33s  | Reflection/Named/Syntax                                                | 0m00.35s  || -0m00.01s
0m00.33s  | Reflection/Z/CNotations                                                | 0m00.34s  || -0m00.01s
0m00.32s  | Tactics/Algebra_syntax/Nsatz                                           | 0m00.34s  || -0m00.02s
0m00.32s  | Reflection/Reify                                                       | 0m00.34s  || -0m00.02s
0m00.32s  | Reflection/Named/MapCast                                               | 0m00.32s  || +0m00.00s
0m00.32s  | Reflection/Named/Wf                                                    | 0m00.30s  || +0m00.02s
0m00.32s  | Reflection/Named/Compile                                               | 0m00.30s  || +0m00.02s
0m00.32s  | Reflection/Named/PositiveContext                                       | 0m00.33s  || -0m00.01s
0m00.32s  | Reflection/Named/ContextProperties/Tactics                             | 0m00.30s  || +0m00.02s
0m00.32s  | Reflection/Named/IdContext                                             | 0m00.31s  || +0m00.01s
0m00.32s  | Reflection/Z/BinaryNotationConstants                                   | 0m00.31s  || +0m00.01s
0m00.32s  | Reflection/Z/FoldTypes                                                 | 0m00.34s  || -0m00.02s
0m00.32s  | Reflection/Z/JavaNotations                                             | 0m00.32s  || +0m00.00s
0m00.31s  | Util/Factorize                                                         | 0m00.32s  || -0m00.01s
0m00.31s  | Reflection/Named/EstablishLiveness                                     | 0m00.32s  || -0m00.01s
0m00.31s  | Reflection/Named/SmartMap                                              | 0m00.32s  || -0m00.01s
0m00.30s  | Reflection/Named/InterpretToPHOAS                                      | 0m00.29s  || +0m00.01s
0m00.29s  | Spec/ModularArithmetic                                                 | 0m00.34s  || -0m00.05s
0m00.29s  | Reflection/FilterLive                                                  | 0m00.29s  || +0m00.00s
0m00.29s  | Reflection/Named/ContextDefinitions                                    | 0m00.33s  || -0m00.04s
0m00.29s  | Reflection/MultiSizeTest2                                              | 0m00.30s  || -0m00.01s
0m00.28s  | Reflection/Named/ContextOn                                             | 0m00.31s  || -0m00.02s
0m00.27s  | Bedrock/Nomega                                                         | 0m00.26s  || +0m00.01s
0m00.27s  | Util/FixedWordSizes                                                    | 0m00.28s  || -0m00.01s
0m00.27s  | Reflection/Z/OpInversion                                               | 0m00.31s  || -0m00.03s
0m00.26s  | Reflection/MapCastWf                                                   | 0m00.29s  || -0m00.02s
0m00.25s  | Reflection/ExprInversion                                               | 0m00.26s  || -0m00.01s
0m00.24s  | Assembly/QhasmCommon                                                   | 0m00.26s  || -0m00.02s
0m00.23s  | Reflection/Equality                                                    | 0m00.23s  || +0m00.00s
0m00.22s  | Util/Sum                                                               | 0m00.22s  || +0m00.00s
0m00.21s  | Reflection/SmartMap                                                    | 0m00.23s  || -0m00.02s
0m00.19s  | Util/CaseUtil                                                          | 0m00.18s  || +0m00.01s
0m00.19s  | Reflection/LinearizeInterp                                             | 0m00.22s  || -0m00.03s
0m00.18s  | Util/LetInMonad                                                        | 0m00.16s  || +0m00.01s
0m00.17s  | Reflection/EtaInterp                                                   | 0m00.17s  || +0m00.00s
0m00.17s  | Reflection/CommonSubexpressionElimination                              | 0m00.16s  || +0m00.01s
0m00.16s  | Reflection/InterpProofs                                                | 0m00.17s  || -0m00.01s
0m00.16s  | Experiments/ExtrHaskellNats                                            | 0m00.16s  || +0m00.00s
0m00.13s  | Reflection/Wf                                                          | 0m00.11s  || +0m00.02s
0m00.11s  | Reflection/BoundByCastWf                                               | 0m00.11s  || +0m00.00s
0m00.11s  | Reflection/Named/NameUtil                                              | 0m00.10s  || +0m00.00s
0m00.10s  | Util/Option                                                            | 0m00.12s  || -0m00.01s
0m00.09s  | Util/Sigma                                                             | 0m00.08s  || +0m00.00s
0m00.09s  | Util/Relations                                                         | 0m00.09s  || +0m00.00s
0m00.08s  | Reflection/Conversion                                                  | 0m00.09s  || -0m00.00s
0m00.08s  | Util/PointedProp                                                       | 0m00.08s  || +0m00.00s
0m00.07s  | Util/Prod                                                              | 0m00.07s  || +0m00.00s
0m00.07s  | Reflection/TypeInversion                                               | 0m00.08s  || -0m00.00s
0m00.06s  | Util/Equality                                                          | 0m00.06s  || +0m00.00s
0m00.05s  | Util/Tactics                                                           | 0m00.04s  || +0m00.01s
0m00.05s  | Reflection/Inline                                                      | 0m00.06s  || -0m00.00s
0m00.05s  | Reflection/SmartBound                                                  | 0m00.07s  || -0m00.02s
0m00.05s  | Reflection/MapCast                                                     | 0m00.05s  || +0m00.00s
0m00.05s  | Reflection/BoundByCast                                                 | 0m00.05s  || +0m00.00s
0m00.04s  | Util/HProp                                                             | 0m00.03s  || +0m00.01s
0m00.04s  | Util/Tactics/DestructHyps                                              | 0m00.01s  || +0m00.03s
0m00.04s  | Util/Bool                                                              | 0m00.04s  || +0m00.00s
0m00.04s  | Util/LetIn                                                             | 0m00.04s  || +0m00.00s
0m00.04s  | Reflection/Syntax                                                      | 0m00.04s  || +0m00.00s
0m00.04s  | Reflection/Eta                                                         | 0m00.06s  || -0m00.01s
0m00.04s  | Reflection/Linearize                                                   | 0m00.03s  || +0m00.01s
0m00.04s  | Reflection/InlineCast                                                  | 0m00.06s  || -0m00.01s
0m00.04s  | Reflection/SmartCastInterp                                             | 0m00.04s  || +0m00.00s
0m00.04s  | Reflection/CountLets                                                   | 0m00.03s  || +0m00.01s
0m00.04s  | Reflection/FoldTypes                                                   | 0m00.04s  || +0m00.00s
0m00.04s  | Reflection/InterpByIso                                                 | 0m00.04s  || +0m00.00s
0m00.03s  | Util/GlobalSettings                                                    | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Tactics/DoWithHyp                                                 | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Tactics/SpecializeBy                                              | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/UniquePose                                                | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Logic                                                             | 0m00.03s  || +0m00.00s
0m00.03s  | Util/IffT                                                              | 0m00.04s  || -0m00.01s
0m00.03s  | Reflection/Map                                                         | 0m00.02s  || +0m00.00s
0m00.03s  | Reflection/TypeUtil                                                    | 0m00.03s  || +0m00.00s
0m00.03s  | Reflection/SmartCast                                                   | 0m00.04s  || -0m00.01s
0m00.03s  | Util/Sumbool                                                           | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Unit                                                              | 0m00.03s  || +0m00.00s
0m00.02s  | Util/FixCoqMistakes                                                    | 0m00.01s  || +0m00.01s
0m00.02s  | Util/Isomorphism                                                       | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/Head                                                      | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/BreakMatch                                                | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Tactics/RewriteHyp                                                | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/SplitInContext                                            | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/VM                                                        | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Notations                                                         | 0m00.03s  || -0m00.00s
0m00.02s  | Tactics/VerdiTactics                                                   | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Tower                                                             | 0m00.04s  || -0m00.02s
0m00.02s  | Util/AutoRewrite                                                       | 0m00.02s  || +0m00.00s
0m00.02s  | Spec/Encoding                                                          | 0m00.02s  || +0m00.00s
0m00.02s  | Encoding/EncodingTheorems                                              | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Curry                                                             | 0m00.01s  || +0m00.01s
0m00.01s  | Util/Tactics/DestructHead                                              | 0m00.02s  || -0m00.01s

1 files changed, 41 insertions, 7 deletions

diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v
index 2717f6bbc..cff35104c 100644
--- a/src/Spec/MontgomeryCurve.v
+++ b/src/Spec/MontgomeryCurve.v
@@ -60,6 +60,8 @@ Module M.
             end.
     Next Obligation. Proof. t. Qed.
 
+    Program Definition zero : point := ∞.
+
     Program Definition opp (P:point) : point :=
       match P return F*F+∞ with
       | (x, y) => (x, -y)
@@ -73,23 +75,55 @@ Module M.
     Local Notation "27" := (3*9).
     Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
 
-    Let WeierstrassA := ((3-a^2)/(3*b^2)).
-    Let WeierstrassB := ((2*a^3-9*a)/(27*b^3)).
+    Local Notation WeierstrassA := ((3-a^2)/(3*b^2)).
+    Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)).
     Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB).
     Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB).
 
+    Program Definition to_Weierstrass (P:point) : Wpoint :=
+      match coordinates P return F*F+∞ with
+      | (x, y) => ((x + a/3)/b, y/b)
+      | _ => ∞
+      end.
+    Next Obligation.
+    Proof. clear char_ge_3; destruct P; t. Qed.
+
     Program Definition of_Weierstrass (P:Wpoint) : point :=
       match W.coordinates P return F*F+∞ with
       | (x,y) => (b*x-a/3, b*y)
       | _ => ∞
       end.
     Next Obligation.
-    Proof. clear char_ge_3; subst WeierstrassA; subst WeierstrassB; destruct P; t. Qed.
+    Proof. clear char_ge_3; destruct P; t. Qed.
 
-    Lemma of_Weierstrass_add P1 P2 :
-      eq (of_Weierstrass (W.add P1 P2))
-         (add (of_Weierstrass P1) (of_Weierstrass P2)).
-    Proof. cbv [WeierstrassA WeierstrassB eq of_Weierstrass W.add add coordinates W.coordinates proj1_sig] in *; clear char_ge_3; t. Qed.
+    (* TODO: move *)
+    Program Definition Wopp (P:Wpoint) : Wpoint :=
+      match P return F*F+∞ with
+      | (x, y) => (x, -y)
+      | ∞ => ∞
+      end.
+    Next Obligation. destruct P; t. Qed.
+
+    Axiom Wgroup : @Algebra.group Wpoint (@W.eq F Feq Fadd Fmul WeierstrassA WeierstrassB)
+         Wadd (@W.zero F Feq Fadd Fmul WeierstrassA WeierstrassB) Wopp.
+    Program Definition _MW : _ /\ _ /\ _ :=
+      @Group.group_from_redundant_representation
+        Wpoint W.eq Wadd W.zero Wopp
+        Wgroup
+        point eq add zero opp
+        of_Weierstrass
+        to_Weierstrass
+        _ _ _ _ _
+        .
+    Next Obligation. cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add coordinates W.coordinates proj1_sig] in *; t. Qed.
+    Next Obligation. cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add coordinates W.coordinates proj1_sig] in *. clear char_ge_3. t. 2:intuition idtac. 2:intuition idtac. 2:intuition idtac.
+                     { repeat split; destruct_head' and; t. } Qed.
+    Next Obligation.
+      (* addition case, same issue as in Weierstrass associativity *) 
+      cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add coordinates W.coordinates proj1_sig] in *.
+      clear char_ge_3. t. Qed.
+    Next Obligation. cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add Wopp opp coordinates W.coordinates proj1_sig] in *. clear char_ge_3. t. Qed.
+    Next Obligation. cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add Wopp opp coordinates W.coordinates proj1_sig] in *. clear char_ge_3. t. Qed.
     
     Section AddX.
       Lemma homogeneous_x_differential_addition_releations P1 P2 :