Add some interpretations things, speed up proofs in Ed25519

After     | File Name                                                              | Before    || Change
-----------------------------------------------------------------------------------------------------------
13m02.08s | Total                                                                  | 15m13.67s || -2m11.59s
-----------------------------------------------------------------------------------------------------------
0m34.08s  | Experiments/Ed25519                                                    | 3m15.96s  || -2m41.87s
1m27.34s  | CompleteEdwardsCurve/ExtendedCoordinates                               | 1m18.08s  || +0m09.26s
0m47.66s  | ModularArithmetic/Conversion                                           | 0m40.15s  || +0m07.50s
1m37.25s  | Test/Curve25519SpecTestVectors                                         | 1m32.28s  || +0m04.96s
0m38.79s  | Spec/Ed25519                                                           | 0m34.76s  || +0m04.03s
0m30.44s  | ModularArithmetic/ModularBaseSystemProofs                              | 0m30.30s  || +0m00.14s
0m23.38s  | Experiments/MontgomeryCurve                                            | 0m23.03s  || +0m00.34s
0m22.34s  | ModularArithmetic/Pow2BaseProofs                                       | 0m22.08s  || +0m00.26s
0m22.30s  | Specific/GF25519                                                       | 0m22.27s  || +0m00.03s
0m19.90s  | Algebra                                                                | 0m20.14s  || -0m00.24s
0m17.70s  | EdDSARepChange                                                         | 0m17.18s  || +0m00.51s
0m17.18s  | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems                      | 0m16.92s  || +0m00.25s
0m13.88s  | Util/ZUtil                                                             | 0m13.76s  || +0m00.12s
0m10.20s  | Testbit                                                                | 0m09.88s  || +0m00.31s
0m09.78s  | Specific/GF25519BoundedCommon                                          | 0m09.79s  || -0m00.00s
0m08.85s  | Assembly/GF25519                                                       | 0m08.92s  || -0m00.07s
0m08.80s  | ModularArithmetic/Montgomery/ZProofs                                   | 0m08.67s  || +0m00.13s
0m08.69s  | BoundedArithmetic/ArchitectureToZLikeProofs                            | 0m08.56s  || +0m00.12s
0m08.64s  | Encoding/PointEncoding                                                 | 0m08.52s  || +0m00.12s
0m08.43s  | BoundedArithmetic/Double/Proofs/Multiply                               | 0m08.30s  || +0m00.12s
0m08.38s  | Specific/GF1305                                                        | 0m08.44s  || -0m00.05s
0m07.85s  | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate          | 0m07.80s  || +0m00.04s
0m07.74s  | Specific/GF25519Reflective/Reified/Mul                                 | 0m07.78s  || -0m00.04s
0m07.45s  | Specific/GF25519Bounded                                                | 0m07.66s  || -0m00.20s
0m07.38s  | Specific/GF25519Reflective                                             | 0m07.49s  || -0m00.11s
0m06.88s  | Specific/GF25519Reflective/Reified/Freeze                              | 0m06.87s  || +0m00.00s
0m06.79s  | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate                    | 0m06.78s  || +0m00.00s
0m06.31s  | Bedrock/Word                                                           | 0m06.10s  || +0m00.20s
0m05.98s  | BoundedArithmetic/Double/Proofs/RippleCarryAddSub                      | 0m05.40s  || +0m00.58s
0m05.52s  | Specific/SC25519                                                       | 0m05.46s  || +0m00.05s
0m05.40s  | Util/ListUtil                                                          | 0m05.42s  || -0m00.01s
0m05.38s  | Experiments/GenericFieldPow                                            | 0m05.33s  || +0m00.04s
0m04.90s  | ModularArithmetic/ModularBaseSystemListProofs                          | 0m04.80s  || +0m00.10s
0m04.85s  | WeierstrassCurve/Pre                                                   | 0m04.75s  || +0m00.09s
0m04.65s  | Reflection/Z/Interpretations                                           | 0m04.68s  || -0m00.02s
0m04.58s  | Encoding/PointEncodingPre                                              | 0m04.24s  || +0m00.33s
0m04.31s  | Reflection/LinearizeWf                                                 | 0m04.32s  || -0m00.01s
0m03.96s  | ModularArithmetic/BarrettReduction/ZHandbook                           | 0m03.92s  || +0m00.04s
0m03.92s  | BaseSystemProofs                                                       | 0m04.00s  || -0m00.08s
0m03.52s  | CompleteEdwardsCurve/Pre                                               | 0m03.52s  || +0m00.00s
0m03.46s  | ModularArithmetic/Tutorial                                             | 0m03.40s  || +0m00.06s
0m03.46s  | BoundedArithmetic/InterfaceProofs                                      | 0m03.31s  || +0m00.14s
0m03.37s  | BoundedArithmetic/Double/Proofs/Decode                                 | 0m02.84s  || +0m00.53s
0m03.33s  | Specific/GF25519Reflective/Reified/CarrySub                            | 0m03.26s  || +0m00.07s
0m03.28s  | ModularArithmetic/BarrettReduction/ZGeneralized                        | 0m03.15s  || +0m00.12s
0m02.91s  | Specific/GF25519Reflective/Reified/CarryOpp                            | 0m03.02s  || -0m00.10s
0m02.88s  | Specific/GF25519Reflective/Reified/CarryAdd                            | 0m02.88s  || +0m00.00s
0m02.86s  | ModularArithmetic/ZBoundedZ                                            | 0m02.86s  || +0m00.00s
0m02.68s  | ModularArithmetic/ModularArithmeticTheorems                            | 0m02.64s  || +0m00.04s
0m02.67s  | Assembly/State                                                         | 0m02.70s  || -0m00.03s
0m02.67s  | BoundedArithmetic/Double/Proofs/ShiftLeft                              | 0m02.60s  || +0m00.06s
0m02.62s  | BoundedArithmetic/Double/Proofs/ShiftRight                             | 0m02.50s  || +0m00.12s
0m02.38s  | ModularArithmetic/BarrettReduction/ZBounded                            | 0m02.36s  || +0m00.02s
0m02.24s  | ModularArithmetic/ModularBaseSystemOpt                                 | 0m02.20s  || +0m00.04s
0m02.17s  | Specific/FancyMachine256/Barrett                                       | 0m02.14s  || +0m00.02s
0m02.16s  | Specific/FancyMachine256/Montgomery                                    | 0m02.06s  || +0m00.10s
0m02.05s  | Reflection/WfReflective                                                | 0m01.98s  || +0m00.06s
0m02.04s  | Assembly/Evaluables                                                    | 0m01.98s  || +0m00.06s
0m02.04s  | Specific/GF25519Reflective/Reified/Unpack                              | 0m02.02s  || +0m00.02s
0m02.04s  | Specific/GF25519Reflective/Reified/Sub                                 | 0m02.01s  || +0m00.03s
0m02.02s  | Specific/GF25519Reflective/Reified/Pack                                | 0m02.00s  || +0m00.02s
0m01.93s  | Specific/FancyMachine256/Core                                          | 0m01.81s  || +0m00.11s
0m01.91s  | Reflection/WfProofs                                                    | 0m01.98s  || -0m00.07s
0m01.88s  | ModularArithmetic/Montgomery/ZBounded                                  | 0m01.86s  || +0m00.01s
0m01.74s  | Specific/GF25519Reflective/Reified/Add                                 | 0m01.72s  || +0m00.02s
0m01.72s  | Reflection/InlineWf                                                    | 0m01.71s  || +0m00.01s
0m01.67s  | Specific/GF25519Reflective/Reified/GeModulus                           | 0m01.59s  || +0m00.07s
0m01.66s  | Specific/GF25519Reflective/Reified/Opp                                 | 0m01.73s  || -0m00.07s
0m01.63s  | ModularArithmetic/BarrettReduction/Z                                   | 0m01.47s  || +0m00.15s
0m01.57s  | Reflection/InlineInterp                                                | 0m01.55s  || +0m00.02s
0m01.52s  | Assembly/WordizeUtil                                                   | 0m01.48s  || +0m00.04s
0m01.44s  | Assembly/Compile                                                       | 0m01.46s  || -0m00.02s
0m01.41s  | Util/NatUtil                                                           | 0m01.41s  || +0m00.00s
0m01.37s  | Reflection/TestCase                                                    | 0m01.42s  || -0m00.04s
0m01.32s  | Assembly/Bounds                                                        | 0m01.35s  || -0m00.03s
0m01.26s  | ModularArithmetic/PrimeFieldTheorems                                   | 0m01.29s  || -0m00.03s
0m01.25s  | BaseSystem                                                             | 0m01.18s  || +0m00.07s
0m01.18s  | BoundedArithmetic/Double/Repeated/Proofs/Decode                        | 0m01.02s  || +0m00.15s
0m01.16s  | Assembly/Conversions                                                   | 0m01.18s  || -0m00.02s
0m01.11s  | ModularArithmetic/ExtendedBaseVector                                   | 0m01.23s  || -0m00.11s
0m01.07s  | Assembly/LL                                                            | 0m00.92s  || +0m00.15s
0m01.00s  | BoundedArithmetic/Double/Proofs/LoadImmediate                          | 0m00.81s  || +0m00.18s
0m00.99s  | Util/WordUtil                                                          | 0m00.99s  || +0m00.00s
0m00.97s  | Assembly/HL                                                            | 0m01.01s  || -0m00.04s
0m00.95s  | Assembly/Pipeline                                                      | 0m00.92s  || +0m00.02s
0m00.92s  | Util/NumTheoryUtil                                                     | 0m00.90s  || +0m00.02s
0m00.92s  | BoundedArithmetic/Double/Proofs/BitwiseOr                              | 0m00.83s  || +0m00.09s
0m00.84s  | Assembly/PhoasCommon                                                   | 0m00.88s  || -0m00.04s
0m00.81s  | BoundedArithmetic/X86ToZLikeProofs                                     | 0m00.87s  || -0m00.05s
0m00.80s  | Specific/GF25519Reflective/Reified                                     | 0m00.81s  || -0m00.01s
0m00.80s  | Util/IterAssocOp                                                       | 0m00.80s  || +0m00.00s
0m00.76s  | Util/Tuple                                                             | 0m00.72s  || +0m00.04s
0m00.75s  | Assembly/QhasmEvalCommon                                               | 0m00.78s  || -0m00.03s
0m00.74s  | Util/PartiallyReifiedProp                                              | 0m00.74s  || +0m00.00s
0m00.72s  | ModularArithmetic/ExtPow2BaseMulProofs                                 | 0m00.70s  || +0m00.02s
0m00.70s  | ModularArithmetic/PseudoMersenneBaseParamProofs                        | 0m00.72s  || -0m00.02s
0m00.68s  | Specific/GF25519Reflective/Common                                      | 0m00.74s  || -0m00.05s
0m00.68s  | Encoding/ModularWordEncodingTheorems                                   | 0m00.67s  || +0m00.01s
0m00.66s  | BoundedArithmetic/Double/Repeated/Proofs/Multiply                      | 0m00.61s  || +0m00.05s
0m00.64s  | Spec/ModularWordEncoding                                               | 0m00.60s  || +0m00.04s
0m00.63s  | ModularArithmetic/ModularBaseSystem                                    | 0m00.68s  || -0m00.05s
0m00.62s  | Spec/EdDSA                                                             | 0m00.64s  || -0m00.02s
0m00.61s  | ModularArithmetic/ModularBaseSystemList                                | 0m00.68s  || -0m00.07s
0m00.61s  | Util/AdditionChainExponentiation                                       | 0m00.72s  || -0m00.10s
0m00.60s  | Encoding/ModularWordEncodingPre                                        | 0m00.68s  || -0m00.08s
0m00.58s  | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr                     | 0m00.47s  || +0m00.10s
0m00.58s  | Reflection/WfReflectiveGen                                             | 0m00.54s  || +0m00.03s
0m00.57s  | BoundedArithmetic/X86ToZLike                                           | 0m00.57s  || +0m00.00s
0m00.57s  | Reflection/LinearizeInterp                                             | 0m00.63s  || -0m00.06s
0m00.56s  | BoundedArithmetic/Interface                                            | 0m00.58s  || -0m00.01s
0m00.54s  | Reflection/InterpWfRel                                                 | 0m00.57s  || -0m00.02s
0m00.53s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.53s  || +0m00.00s
0m00.53s  | BoundedArithmetic/Double/Proofs/SelectConditional                      | 0m00.58s  || -0m00.04s
0m00.53s  | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub             | 0m00.54s  || -0m00.01s
0m00.52s  | Reflection/Z/Reify                                                     | 0m00.48s  || +0m00.04s
0m00.52s  | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional             | 0m00.48s  || +0m00.04s
0m00.51s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight                | 0m00.52s  || -0m00.01s
0m00.51s  | Assembly/StringConversion                                              | 0m00.52s  || -0m00.01s
0m00.49s  | BoundedArithmetic/Double/Core                                          | 0m00.47s  || +0m00.02s
0m00.49s  | Util/Decidable                                                         | 0m00.48s  || +0m00.01s
0m00.49s  | ModularArithmetic/PseudoMersenneBaseParams                             | 0m00.40s  || +0m00.08s
0m00.49s  | Reflection/InputSyntax                                                 | 0m00.51s  || -0m00.02s
0m00.49s  | BoundedArithmetic/Double/Repeated/Core                                 | 0m00.48s  || +0m00.01s
0m00.48s  | Reflection/Syntax                                                      | 0m00.43s  || +0m00.04s
0m00.48s  | Assembly/Qhasm                                                         | 0m00.52s  || -0m00.04s
0m00.48s  | Reflection/Z/Syntax                                                    | 0m00.47s  || +0m00.01s
0m00.47s  | ModularArithmetic/Pow2Base                                             | 0m00.48s  || -0m00.01s
0m00.47s  | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic                   | 0m00.44s  || +0m00.02s
0m00.47s  | ModularArithmetic/Pre                                                  | 0m00.54s  || -0m00.07s
0m00.47s  | BoundedArithmetic/ArchitectureToZLike                                  | 0m00.45s  || +0m00.01s
0m00.47s  | Spec/MxDH                                                              | 0m00.41s  || +0m00.06s
0m00.46s  | Reflection/InterpWf                                                    | 0m00.45s  || +0m00.01s
0m00.46s  | ModularArithmetic/ZBounded                                             | 0m00.47s  || -0m00.00s
0m00.46s  | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate                 | 0m00.50s  || -0m00.03s
0m00.46s  | Reflection/CommonSubexpressionElimination                              | 0m00.50s  || -0m00.03s
0m00.43s  | Reflection/Named/DeadCodeElimination                                   | 0m00.45s  || -0m00.02s
0m00.43s  | Reflection/InterpProofs                                                | 0m00.52s  || -0m00.09s
0m00.42s  | Spec/WeierstrassCurve                                                  | 0m00.46s  || -0m00.04s
0m00.42s  | BoundedArithmetic/StripCF                                              | 0m00.42s  || +0m00.00s
0m00.42s  | Reflection/Named/Syntax                                                | 0m00.41s  || +0m00.01s
0m00.41s  | Reflection/FilterLive                                                  | 0m00.36s  || +0m00.04s
0m00.41s  | Reflection/Conversion                                                  | 0m00.43s  || -0m00.02s
0m00.40s  | Reflection/MapInterp                                                   | 0m00.42s  || -0m00.01s
0m00.40s  | BoundedArithmetic/Eta                                                  | 0m00.46s  || -0m00.06s
0m00.39s  | Reflection/MapInterpWf                                                 | 0m00.39s  || +0m00.00s
0m00.39s  | Reflection/Inline                                                      | 0m00.40s  || -0m00.01s
0m00.38s  | Reflection/Named/EstablishLiveness                                     | 0m00.39s  || -0m00.01s
0m00.38s  | Tactics/Algebra_syntax/Nsatz                                           | 0m00.37s  || +0m00.01s
0m00.38s  | Reflection/Named/RegisterAssign                                        | 0m00.44s  || -0m00.06s
0m00.37s  | Reflection/Reify                                                       | 0m00.37s  || +0m00.00s
0m00.37s  | Reflection/WfRel                                                       | 0m00.38s  || -0m00.01s
0m00.36s  | Spec/CompleteEdwardsCurve                                              | 0m00.38s  || -0m00.02s
0m00.36s  | Assembly/QhasmUtil                                                     | 0m00.55s  || -0m00.19s
0m00.36s  | ModularArithmetic/Montgomery/Z                                         | 0m00.48s  || -0m00.12s
0m00.35s  | Reflection/Named/Compile                                               | 0m00.35s  || +0m00.00s
0m00.35s  | Reflection/Linearize                                                   | 0m00.37s  || -0m00.02s
0m00.35s  | Spec/ModularArithmetic                                                 | 0m00.35s  || +0m00.00s
0m00.34s  | Reflection/CountLets                                                   | 0m00.33s  || +0m00.01s
0m00.34s  | Reflection/Named/NameUtil                                              | 0m00.36s  || -0m00.01s
0m00.32s  | Util/Sum                                                               | 0m00.22s  || +0m00.10s
0m00.32s  | Reflection/Named/ContextOn                                             | 0m00.35s  || -0m00.02s
0m00.31s  | Assembly/QhasmCommon                                                   | 0m00.31s  || +0m00.00s
0m00.27s  | Bedrock/Nomega                                                         | 0m00.26s  || +0m00.01s
0m00.26s  | ModularArithmetic/ModularBaseSystemListZOperations                     | 0m00.26s  || +0m00.00s
0m00.19s  | Util/CaseUtil                                                          | 0m00.24s  || -0m00.04s
0m00.18s  | Experiments/ExtrHaskellNats                                            | 0m00.18s  || +0m00.00s
0m00.14s  | Util/PointedProp                                                       | 0m00.10s  || +0m00.04s
0m00.10s  | Util/Sigma                                                             | 0m00.08s  || +0m00.02s
0m00.09s  | Util/Option                                                            | 0m00.12s  || -0m00.03s
0m00.09s  | Util/Relations                                                         | 0m00.12s  || -0m00.03s
0m00.07s  | Util/Equality                                                          | 0m00.04s  || +0m00.03s
0m00.06s  | Util/Tactics                                                           | 0m00.05s  || +0m00.00s
0m00.05s  | Util/Prod                                                              | 0m00.06s  || -0m00.00s
0m00.05s  | Util/HProp                                                             | 0m00.03s  || +0m00.02s
0m00.05s  | Util/LetIn                                                             | 0m00.04s  || +0m00.01s
0m00.04s  | Util/Notations                                                         | 0m00.03s  || +0m00.01s
0m00.03s  | Tactics/VerdiTactics                                                   | 0m00.03s  || +0m00.00s
0m00.03s  | Encoding/EncodingTheorems                                              | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Unit                                                              | 0m00.04s  || -0m00.01s
0m00.03s  | Util/AutoRewrite                                                       | 0m00.02s  || +0m00.00s
0m00.03s  | Util/FixCoqMistakes                                                    | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Isomorphism                                                       | 0m00.02s  || +0m00.00s
0m00.02s  | Util/GlobalSettings                                                    | 0m00.03s  || -0m00.00s
0m00.02s  | Spec/Encoding                                                          | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Logic                                                             | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Bool                                                              | 0m00.02s  || +0m00.00s

1 files changed, 14 insertions, 3 deletions

diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index 5657d8503..2ddb7079b 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -20,6 +20,10 @@ Local Coercion GF25519BoundedCommon.word64ToZ : GF25519BoundedCommon.word64 >->
 Local Coercion GF25519BoundedCommon.proj1_fe25519 : GF25519BoundedCommon.fe25519 >-> GF25519.fe25519.
 Local Set Printing Coercions.
 
+Local Notation eta x := (fst x, snd x).
+Local Notation eta3 x := (eta (fst x), snd x).
+Local Notation eta4 x := (eta3 (fst x), snd x).
+
 Context {H: forall n : nat, Word.word n -> Word.word (b + b)}.
 
 Definition feSign (f :  GF25519BoundedCommon.fe25519) : bool :=
@@ -830,13 +834,20 @@ Lemma SRepEnc_correct : forall x : ModularArithmetic.F.F l, Senc x = SRepEnc (S2
 Qed.
 
 (** TODO: How do we speed up vm_compute here?  I think it's spending most of it's time rechecking boundedness... *)
+Definition ERepB_value := Eval vm_compute in (proj1_sig (EToRep B)).
 Let ERepB : Erep.
-  let rB := (eval vm_compute in (proj1_sig (EToRep B))) in
-  exists rB. cbv [GF25519BoundedCommon.eq ModularBaseSystem.eq Pre.onCurve]. vm_decide_no_check.
+  exists (eta4 ERepB_value).
+  cbv [GF25519BoundedCommon.eq ModularBaseSystem.eq Pre.onCurve].
+  vm_decide_no_check.
 Defined.
 
+Lemma ERepB_value_correct : ERepB_value = proj1_sig (EToRep B).
+Proof. vm_cast_no_check (eq_refl ERepB_value). Qed.
+
 Let ERepB_correct : ExtendedCoordinates.Extended.eq (field:=GF25519Bounded.field25519) ERepB (EToRep B).
-  vm_decide_no_check.
+  pose proof ERepB_value_correct; destruct (EToRep B).
+  cbv [proj1_sig] in *; subst.
+  vm_decide.
 Qed.
 
 Lemma B_order_l : CompleteEdwardsCurveTheorems.E.eq