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.

2 files changed, 20 insertions, 12 deletions

diff --git a/src/Specific/FancyMachine256/Barrett.v b/src/Specific/FancyMachine256/Barrett.v
index 93a9432aa..a43becf68 100644
--- a/src/Specific/FancyMachine256/Barrett.v
+++ b/src/Specific/FancyMachine256/Barrett.v
@@ -63,9 +63,11 @@ End expression.
 
 Section reflected.
   Context (ops : fancy_machine.instructions (2 * 128)).
-  Definition rexpression : Syntax.Expr base_type op (Arrow TZ (Arrow TZ (Arrow TW (Arrow TW (Tbase TW))))).
+  Local Notation tZ := (Tbase TZ).
+  Local Notation tW := (Tbase TW).
+  Definition rexpression : Syntax.Expr base_type op (Arrow (tZ * tZ * tW * tW) tW).
   Proof.
-    let v := (eval cbv beta delta [expression] in (fun m μ x y => expression ops m μ (x, y))) in
+    let v := (eval cbv beta delta [expression] in (fun mμxy => let '(mv, μv, xv, yv) := mμxy in expression ops mv μv (xv, yv))) in
     let v := Reify v in
     exact v.
   Defined.
@@ -85,8 +87,8 @@ Section reflected.
   Context (m μ : Z)
           (props : fancy_machine.arithmetic ops).
 
-  Let result (v : Tuple.tuple fancy_machine.W 2) := Syntax.Interp interp_op rexpression_simple m μ (fst v) (snd v).
-  Let assembled_result (v : Tuple.tuple fancy_machine.W 2) : fancy_machine.W := Core.Interp compiled_syntax m μ (fst v) (snd v).
+  Let result (v : Tuple.tuple fancy_machine.W 2) := Syntax.Interp (@interp_op _) rexpression_simple (m, μ, fst v, snd v).
+  Let assembled_result (v : Tuple.tuple fancy_machine.W 2) : fancy_machine.W := Core.Interp compiled_syntax (m, μ, fst v, snd v).
 
   Theorem sanity : result = expression ops m μ.
   Proof.
@@ -126,7 +128,7 @@ End reflected.
 Print compiled_syntax.
 (* compiled_syntax =
 fun ops : fancy_machine.instructions (2 * 128) =>
-λn RegMod RegMuLow x xHigh,
+λn (RegMod, RegMuLow, x, xHigh),
 slet RegMod := RegMod in
 slet RegMuLow := RegMuLow in
 slet RegZero := ldi 0 in
@@ -148,5 +150,6 @@ c.Sub(tmp, x, tmp),
 c.Addm(q, tmp, RegZero),
 c.Addm(out, q, RegZero),
 Return out
-     : forall ops : fancy_machine.instructions (2 * 128), expr base_type op Register (TZ -> TZ -> TW -> TW -> Tbase TW)
+     : forall ops : fancy_machine.instructions (2 * 128),
+       expr base_type op Register (Tbase TZ * Tbase TZ * Tbase TW * Tbase TW -> Tbase TW)
 *)
diff --git a/src/Specific/FancyMachine256/Montgomery.v b/src/Specific/FancyMachine256/Montgomery.v
index f0ca09119..fd0d9a57f 100644
--- a/src/Specific/FancyMachine256/Montgomery.v
+++ b/src/Specific/FancyMachine256/Montgomery.v
@@ -53,9 +53,13 @@ End expression.
 
 Section reflected.
   Context (ops : fancy_machine.instructions (2 * 128)).
-  Definition rexpression : Syntax.Expr base_type op (Arrow TZ (Arrow TZ (Arrow TW (Arrow TW (Tbase TW))))).
+  Local Notation tZ := (Tbase TZ).
+  Local Notation tW := (Tbase TW).
+  Definition rexpression : Syntax.Expr base_type op (Arrow (tZ * tZ * tW * tW) tW).
   Proof.
-    let v := (eval cbv beta delta [expression] in (fun modulus m' x y => expression ops modulus m' (x, y))) in
+    let v := (eval cbv beta delta [expression] in
+                 (fun modulus_m'_x_y => let '(modulusv, m'v, xv, yv) := modulus_m'_x_y in
+                                        expression ops modulusv m'v (xv, yv))) in
     let v := Reify v in
     exact v.
   Defined.
@@ -76,9 +80,9 @@ Section reflected.
   Context (modulus m' : Z)
           (props : fancy_machine.arithmetic ops).
 
-  Let result (v : Tuple.tuple fancy_machine.W 2) := Syntax.Interp interp_op rexpression_simple modulus m' (fst v) (snd v).
+  Let result (v : Tuple.tuple fancy_machine.W 2) := Syntax.Interp interp_op rexpression_simple (modulus, m', fst v, snd v).
 
-  Let assembled_result (v : Tuple.tuple fancy_machine.W 2) : fancy_machine.W := Core.Interp compiled_syntax modulus m' (fst v) (snd v).
+  Let assembled_result (v : Tuple.tuple fancy_machine.W 2) : fancy_machine.W := Core.Interp compiled_syntax (modulus, m', fst v, snd v).
 
   Theorem sanity : result = expression ops modulus m'.
   Proof.
@@ -124,7 +128,7 @@ End reflected.
 Print compiled_syntax.
 (* compiled_syntax =
 fun ops : fancy_machine.instructions (2 * 128) =>
-λn RegMod RegPInv lo hi,
+λn (RegMod, RegPInv, lo, hi),
 slet RegMod := RegMod in
 slet RegPInv := RegPInv in
 slet RegZero := ldi 0 in
@@ -147,5 +151,6 @@ c.Selc(y, RegMod, RegZero),
 c.Sub(lo, hi, y),
 c.Addm(lo, lo, RegZero),
 Return lo
-     : forall ops : fancy_machine.instructions (2 * 128), expr base_type op Register (TZ -> TZ -> TW -> TW -> Tbase TW)
+     : forall ops : fancy_machine.instructions (2 * 128),
+       expr base_type op Register (Tbase TZ * Tbase TZ * Tbase TW * Tbase TW -> Tbase TW)
 *)