Switch to fully uncurried form for reflection

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.

1 files changed, 43 insertions, 11 deletions

diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index 1a1bc9490..c7e9d173c 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -845,11 +845,11 @@ Local Ltac prove_bounded_by :=
            => apply bounded_by_from_is_bounded
          | [ |- GF25519BoundedCommon.is_bounded
                   (GF25519BoundedCommon.fe25519WToZ
-                     (GF25519Bounded.mulW _ _)) = true ]
+                     (GF25519Bounded.mulW (_, _))) = true ]
            => apply GF25519Bounded.mulW_correct_and_bounded
          | [ |- GF25519BoundedCommon.is_bounded
                   (GF25519BoundedCommon.fe25519WToZ
-                     (GF25519Bounded.mulW_noinline _ _)) = true ]
+                     (GF25519Bounded.mulW_noinline (_, _))) = true ]
            => apply GF25519Bounded.mulW_correct_and_bounded
          | [ |- GF25519BoundedCommon.is_bounded
                   (GF25519BoundedCommon.fe25519WToZ
@@ -882,17 +882,49 @@ Proof.
   rewrite ModularBaseSystemProofs.encode_rep.
   symmetry.
   eapply @ModularBaseSystemProofs.sqrt_5mod8_correct;
-    eauto using GF25519.freezePreconditions25519, ModularBaseSystemProofs.encode_rep, bounded_by_freeze, bounded_by_encode_freeze; prove_bounded_by; eauto using GF25519BoundedCommon.is_bounded_proj1_fe25519; [ reflexivity |
-  lazymatch goal with
+    eauto using GF25519.freezePreconditions25519, ModularBaseSystemProofs.encode_rep, bounded_by_freeze, bounded_by_encode_freeze; prove_bounded_by; eauto using GF25519BoundedCommon.is_bounded_proj1_fe25519;
+      cbv [HList.hlistP HList.hlistP'] in *;
+      repeat apply conj;
+      [ reflexivity |
+        try lazymatch goal with
     | |- appcontext[GF25519Bounded.powW ?a ?ch] =>
       let A := fresh "H" in
       destruct (GF25519Bounded.powW_correct_and_bounded ch a) as [A ?];
-        [ rewrite GF25519BoundedCommon.fe25519WToZ_ZToW;
+      [ rewrite GF25519BoundedCommon.fe25519WToZ_ZToW;
+        hnf;
           solve [eauto using GF25519BoundedCommon.is_bounded_proj1_fe25519]
-        | rewrite A;
+        | cbv [Tuple.map List.map Tuple.on_tuple Tuple.from_list' Tuple.from_list Tuple.to_list Tuple.to_list'] in *;
+          rewrite A;
           rewrite GF25519.pow_correct, ModularBaseSystemOpt.pow_opt_correct
             by reflexivity]
-    end..];
+      end..].
+  (*{ lazymatch goal with
+    | |- appcontext[GF25519Bounded.powW ?a ?ch] =>
+      let A := fresh "H" in
+      destruct (GF25519Bounded.powW_correct_and_bounded ch a) as [A ?];
+        [ rewrite GF25519BoundedCommon.fe25519WToZ_ZToW;
+          hnf;
+          solve [eauto using GF25519BoundedCommon.is_bounded_proj1_fe25519]
+        | cbv [Tuple.map List.map Tuple.on_tuple Tuple.from_list' Tuple.from_list Tuple.to_list Tuple.to_list'] in *;
+          move A at bottom;
+          rewrite A, !GF25519.pow_correct
+            by reflexivity(*
+          rewrite GF25519.pow_correct, ModularBaseSystemOpt.pow_opt_correct
+            by reflexivity*)]
+    end.
+    About GF25519.pow_correct.
+
+    cbv [GF25519BoundedCommon.is_bounded fst snd GF25519BoundedCommon.is_bounded_gen].
+
+    cbv [Tuple.map2 Tuple.on_tuple2 Tuple.to_list GF25519.length_fe25519 Tuple.to_list' map2 GF25519BoundedCommon.bounds].
+    rewrite ModularBaseSystemOpt.pow_opt_correct.
+    rewrite GF25519.pow_correct.
+    rewrite H.
+    .
+    SearchAbout GF25519Bounded.mulW.
+    Set Printing Coercions.
+    rewrite H.
+
     [ rewrite GF25519BoundedCommon.fe25519WToZ_ZToW by (eapply GF25519BoundedCommon.is_bounded_proj1_fe25519); reflexivity | ].
   unfold GF25519Bounded.mulW_noinline.
   match goal with
@@ -908,8 +940,8 @@ Proof.
   rewrite ModularBaseSystemProofs.carry_mul_rep by reflexivity.
   rewrite ModularBaseSystemProofs.mul_rep by reflexivity.
   apply f_equal2;
-  rewrite ModularBaseSystemOpt.pow_opt_correct; reflexivity.
-Qed.
+  rewrite ModularBaseSystemOpt.pow_opt_correct; reflexivity.*)
+Admitted.
 
 (* TODO : move to GF25519BoundedCommon *)
 Module GF25519BoundedCommon.
@@ -1003,7 +1035,7 @@ Let verify_correct :
       (* Ahomom := *) Ahomom
       (* ERepEnc := *) ERepEnc
       (* ERepEnc_correct := *) ERepEnc_correct
-      (* Proper_ERepEnc := *) Proper_ERepEnc 
+      (* Proper_ERepEnc := *) Proper_ERepEnc
       (* ERepDec := *) ERepDec
       (* ERepDec_correct := *) ERepDec_correct
       (* SRep := *) SRep (*(Tuple.tuple (Word.word 32) 8)*)
@@ -1019,7 +1051,7 @@ Let verify_correct :
       (* SRepDec_correct := *) SRepDec_correct
 .
 
-(* TODO : make a new file for the stuff below *) 
+(* TODO : make a new file for the stuff below *)
 
 Lemma Fhomom_inv_zero :
   GF25519BoundedCommon.eq