stuck trying to figure out dependently typed continuation passing style

1 files changed, 24 insertions, 5 deletions

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 :