From 5a0c4eb34708d2c85d91e6cb2c708ed16249e06d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 6 Jul 2016 11:29:16 -0400 Subject: stuck trying to figure out dependently typed continuation passing style --- src/Specific/GF1305.v | 29 ++++++++++++++++++++++++----- 1 file changed, 24 insertions(+), 5 deletions(-) (limited to 'src/Specific') 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 : -- cgit v1.2.3