stuck trying to figure out dependently typed continuation passing style

5 files changed, 57 insertions, 30 deletions

diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v
index c0b6be25b..0f02000d0 100644
--- a/src/Experiments/DerivationsOptionRectLetInEncoding.v
+++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v
@@ -18,16 +18,6 @@ Local Open Scope equiv_scope.
 Generalizable All Variables.
 
 
-Local Ltac set_evars :=
-  repeat match goal with
-         | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E)
-         end.
-
-Local Ltac subst_evars :=
-  repeat match goal with
-         | [ e := ?E |- _ ] => is_evar E; subst e
-         end.
-
 Definition path_sig {A P} {RA:relation A} {Rsig:relation (@sig A P)}
            {HP:Proper (RA==>Basics.impl) P}
            (H:forall (x y:A) (px:P x) (py:P y), RA x y -> Rsig (exist _ x px) (exist _ y py))
diff --git a/src/ModularArithmetic/ModularBaseSystemInterface.v b/src/ModularArithmetic/ModularBaseSystemInterface.v
index b0cfffe8b..be7f2f257 100644
--- a/src/ModularArithmetic/ModularBaseSystemInterface.v
+++ b/src/ModularArithmetic/ModularBaseSystemInterface.v
@@ -11,20 +11,26 @@ Generalizable All Variables.
 Section s.
   Context `{prm:PseudoMersenneBaseParams m} {sc : SubtractionCoefficient m prm}.
 
-  Definition frep := tuple Z (length PseudoMersenneBaseParamProofs.base).
+  Definition fe := tuple Z (length PseudoMersenneBaseParamProofs.base).
 
-  Definition mul : frep -> frep -> frep.
-    refine (on_tuple2 (mul_opt k c) _).
-    abstract (intros; rewrite mul_opt_correct; auto using length_mul).
-  Defined.
+  About from_list.
+
+  Lemma carry_mul_on_tuple x y :
+    length (carry_mul (to_list (length base) x) (to_list (length base) y)) = length base.
+  Admitted.
 
-  Definition add : frep -> frep -> frep.
+  Definition mul {k_ c_} (pfk : k = k_) (pfc:c = c_) (x y:fe) : fe.
+    refine (carry_mul_opt_cps (fun xs => from_list _ xs) (to_list _ x) (to_list _ y) _).
+    abstract (apply carry_mul_on_tuple).
+  Defined.
+  
+  Definition add : fe -> fe -> fe.
     refine (on_tuple2 add_opt _).
     abstract (intros; rewrite add_opt_correct, add_length_exact; case_max; omega).
   Defined.
 
-  Definition sub : frep -> frep -> frep.
+  Definition sub : fe -> fe -> fe.
     refine (on_tuple2 sub_opt _).
     abstract (intros; rewrite sub_opt_correct; apply length_sub; rewrite ?coeff_length; auto).
   Defined.
-End S.
\ No newline at end of file
+End s.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index abbb0e573..e11186cfb 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -486,21 +486,23 @@ Section Multiplication.
     : mul_opt us vs = mul us vs
     := proj2_sig (mul_opt_sig us vs).
 
-  Definition carry_mul_opt_sig (us vs : digits) : { b : digits | b = carry_mul us vs }.
+  Definition carry_mul_opt_sig {T:digits->Type} (f:forall d:digits, T d) (us vs : digits) : { x | x = f (carry_mul us vs) }.
   Proof.
     eexists.
     cbv [carry_mul].
-    erewrite <-carry_full_opt_correct by eauto.
+    (* FIXME
+    erewrite <-carry_full_opt_cps_correct by eauto.
     erewrite <-mul_opt_correct.
     reflexivity.
+   *)
   Defined.
 
-  Definition carry_mul_opt (us vs : digits) : digits
-    := Eval cbv [proj1_sig carry_mul_opt_sig] in proj1_sig (carry_mul_opt_sig us vs).
+  Definition carry_mul_opt_cps {T} (f:forall d:digits, T d) (us vs : digits) : T (carry_mul us vs)
+    := Eval cbv [proj1_sig carry_mul_opt_sig] in proj1_sig (carry_mul_opt_sig f us vs).
 
-  Definition carry_mul_opt_correct us vs
-    : carry_mul_opt us vs = carry_mul us vs
-    := proj2_sig (carry_mul_opt_sig us vs).
+  Definition carry_mul_opt_cps_correct {T} (f:forall d:digits, T d) (us vs : digits)
+    : carry_mul_opt_cps f us vs = f (carry_mul us vs)
+    := proj2_sig (carry_mul_opt_sig f us vs).
 End Multiplication.
 
 Record freezePreconditions {modulus} (prm : PseudoMersenneBaseParams modulus) int_width :=
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index 02ef714d9..edb122ac2 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -2,14 +2,18 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystem.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseRep.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemInterface.
 Require Import Coq.Lists.List Crypto.Util.ListUtil.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.BaseSystem.
+Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Notations.
 Import ListNotations.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
 Local Open Scope Z.
+Local Infix "<<" := Z.shiftr.
+Local Infix "&" := Z.land.
 
 (* BEGIN PseudoMersenneBaseParams instance construction. *)
 
@@ -37,12 +41,27 @@ Defined.
 (* Precompute k and c *)
 Definition k_ := Eval compute in k.
 Definition c_ := Eval compute in c.
+Definition k_subst : k = k_ := eq_refl k_.
 Definition c_subst : c = c_ := eq_refl c_.
 
-(* Makes Qed not take forever *)
-Opaque Z.shiftr Pos.iter Z.div2 Pos.div2 Pos.div2_up Pos.succ Z.land
-  Z.of_N Pos.land N.ldiff Pos.pred_N Pos.pred_double Z.opp Z.mul Pos.mul
-  Let_In digits Z.add Pos.add Z.pos_sub andb Z.eqb Z.ltb.
+Definition fe1305 : Type := Eval cbv in fe.
+
+Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In.
+
+Definition mul (f g:fe1305) : { fg | fg = ModularBaseSystemInterface.mul k_subst c_subst f g }.
+  (* NOTE: beautiful example of reduction slowness: stack overflow if [f] [g] are not destructed first *)
+  cbv [fe1305] in *.
+  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
+  eexists. 
+  cbv.
+  autorewrite with zsimplify.
+  reflexivity.
+Defined.
+
+(*
+Local Transparent Let_In.
+Eval cbv iota beta delta [proj1_sig mul Let_In] in (fun f0 f1 f2 f3 f4  g0 g1 g2 g3 g4 => proj1_sig (mul (f4,f3,f2,f1,f0) (g4,g3,g2,g1,g0))).
+*)
 
 Local Open Scope nat_scope.
 Lemma GF1305Base26_mul_reduce_formula :
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 304ae3c20..ab98bb7f2 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -40,6 +40,16 @@ Tactic Notation "unique" "assert" constr(T) "by" tactic3(tac) :=
   | _ => assert T by tac
   end.
 
+Ltac set_evars :=
+  repeat match goal with
+         | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E)
+         end.
+
+Ltac subst_evars :=
+  repeat match goal with
+         | [ e := ?E |- _ ] => is_evar E; subst e
+         end.
+
 (** destruct discriminees of [match]es in the goal *)
 (* Prioritize breaking apart things in the context, then things which
    don't need equations, then simple matches (which can be displayed