Core.v

(*****

This file provides a generalized version of arithmetic with "mixed
radix" numerical systems. Later, parameters are entered into the
general functions, and they are partially evaluated until only runtime
basic arithmetic operations remain.

CPS
---

Fuctions are written in continuation passing style (CPS). This means
that each operation is passed a "continuation" function, which it is
expected to call on its own output (like a callback). See the end of
this comment for a motivating example explaining why we do CPS,
despite a fair amount of resulting boilerplate code for each
operation. The code block for an operation called A would look like
this:

```
Definition A_cps x y {T} f : T := ...

Definition A x y := A_cps x y id.
Lemma A_cps_id x y : forall {T} f, @A_cps x y T f = f (A x y).
Hint Opaque A : uncps.
Hint Rewrite A_cps_id : uncps.

Lemma eval_A x y : eval (A x y) = ...
Hint Rewrite eval_A : push_basesystem_eval.
```

`A_cps` is the main, CPS-style definition of the operation (`f` is the
continuation function). `A` is the non-CPS version of `A_cps`, simply
defined by passing an identity function to `A_cps`. `A_cps_id` states
that we can replace the CPS version with the non-cps version. `eval_A`
is the actual correctness lemma for the operation, stating that it has
the correct arithmetic properties. In general, the middle block
containing `A` and `A_cps_id` is boring boilerplate and can be safely
ignored.

HintDbs
-------

+ `uncps` : Converts CPS operations to their non-CPS versions.
+ `push_basesystem_eval` : Contains all the correctness lemmas for
   operations in this file, which are in terms of the `eval` function.

Positional/Associational
------------------------

We represent mixed-radix numbers in a few different ways:

+ "Positional" : a tuple of numbers and a weight function (nat->Z),
which is evaluated by multiplying the `i`th element of the tuple by
`weight i`, and then summing the products.
+ "Associational" : a list of pairs of numbers--the first is the
weight, the second is the runtime value. Evaluated by multiplying each
pair and summing the products.

The associational representation is good for basic operations like
addition and multiplication; for addition, one can simply just append
two associational lists. But the end-result code should use the
positional representation (with each digit representing a machine
word). Since converting to and fro can be easily compiled away once
the weight function is known, we use associational to write most of
the operations and liberally convert back and forth to ensure correct
output. In particular, it is important to convert before carrying.

Runtime Operations
------------------

Since some instances of e.g. Z.add or Z.mul operate on (compile-time)
weights, and some operate on runtime values, we need a way to
differentiate these cases before partial evaluation. We define a
runtime_scope to mark certain additions/multiplications as runtime
values, so they will not be unfolded during partial evaluation. For
instance, if we have:

```
Definition f (x y : Z * Z) := (fst x + fst y, (snd x + snd y)%RT).
```

then when we are partially evaluating `f`, we can easily exclude the
runtime operations (`cbv - [runtime_add]`) and prevent Coq from trying
to simplify the second addition.


Why CPS?
--------

Let's suppose we want to add corresponding elements of two `list Z`s
(so on inputs `[1,2,3]` and `[2,3,1]`, we get `[3,5,4]`). We might
write our function like this :

```
Fixpoint add_lists (p q : list Z) :=
  match p, q with
  | p0 :: p', q0 :: q' =>
    dlet sum := p0 + q0 in
    sum :: add_lists p' q'
  | _, _ => nil
  end.
```

(Note : `dlet` is a notation for `Let_In`, which is just a dumb
wrapper for `let`. This allows us to `cbv - [Let_In]` if we want to
not simplify certain `let`s.)

A CPS equivalent of `add_lists` would look like this:

```
Fixpoint add_lists_cps (p q : list Z) {T} (f:list Z->T) :=
  match p, q with
  | p0 :: p', q0 :: q' =>
    dlet sum := p0 + q0 in
    add_lists_cps p' q' (fun r => f (sum :: r))
  | _, _ => f nil
  end.
```

Now let's try some partial evaluation. The expression we'll evaluate is:

```
Definition x :=
    (fun a0 a1 a2 b0 b1 b2 =>
      let r := add_lists [a0;a1;a2] [b0;b1;b2] in
      let rr := add_lists r r in
      add_lists rr rr).
```

Or, using `add_lists_cps`:

```
Definition y :=
    (fun a0 a1 a2 b0 b1 b2 =>
      add_lists_cps [a0;a1;a2] [b0;b1;b2]
                     (fun r => add_lists_cps r r
                     (fun rr => add_lists_cps rr rr id))).
```

If we run `Eval cbv -[Z.add] in x` and `Eval cbv -[Z.add] in y`, we get
identical output:

```
fun a0 a1 a2 b0 b1 b2 : Z =>
       [a0 + b0 + (a0 + b0) + (a0 + b0 + (a0 + b0));
       a1 + b1 + (a1 + b1) + (a1 + b1 + (a1 + b1));
       a2 + b2 + (a2 + b2) + (a2 + b2 + (a2 + b2))]
```

However, there are a lot of common subexpressions here--this is what
the `dlet` we put into the functions should help us avoid. Let's try
`Eval cbv -[Let_In Z.add] in x`:

```
fun a0 a1 a2 b0 b1 b2 : Z =>
       (fix add_lists (p q : list Z) {struct p} :
        list Z :=
          match p with
          | [] => []
          | p0 :: p' =>
              match q with
              | [] => []
              | q0 :: q' =>
                  dlet sum := p0 + q0 in
                  sum :: add_lists p' q'
              end
          end)
         ((fix add_lists (p q : list Z) {struct p} :
           list Z :=
             match p with
             | [] => []
             | p0 :: p' =>
                 match q with
                 | [] => []
                 | q0 :: q' =>
                     dlet sum := p0 + q0 in
                     sum :: add_lists p' q'
                 end
             end)
            (dlet sum := a0 + b0 in
             sum
             :: (dlet sum0 := a1 + b1 in
                 sum0 :: (dlet sum1 := a2 + b2 in
                          [sum1])))
            (dlet sum := a0 + b0 in
             sum
             :: (dlet sum0 := a1 + b1 in
                 sum0 :: (dlet sum1 := a2 + b2 in
                          [sum1]))))
         ((fix add_lists (p q : list Z) {struct p} :
           list Z :=
             match p with
             | [] => []
             | p0 :: p' =>
                 match q with
                 | [] => []
                 | q0 :: q' =>
                     dlet sum := p0 + q0 in
                     sum :: add_lists p' q'
                 end
             end)
            (dlet sum := a0 + b0 in
             sum
             :: (dlet sum0 := a1 + b1 in
                 sum0 :: (dlet sum1 := a2 + b2 in
                          [sum1])))
            (dlet sum := a0 + b0 in
             sum
             :: (dlet sum0 := a1 + b1 in
                 sum0 :: (dlet sum1 := a2 + b2 in
                          [sum1]))))
```

Not so great. Because the `dlet`s are stuck in the inner terms, we
can't simplify the expression very nicely. Let's try that on the CPS
version (`Eval cbv -[Let_In Z.add] in y`):

```
fun a0 a1 a2 b0 b1 b2 : Z =>
       dlet sum := a0 + b0 in
       dlet sum0 := a1 + b1 in
       dlet sum1 := a2 + b2 in
       dlet sum2 := sum + sum in
       dlet sum3 := sum0 + sum0 in
       dlet sum4 := sum1 + sum1 in
       dlet sum5 := sum2 + sum2 in
       dlet sum6 := sum3 + sum3 in
       dlet sum7 := sum4 + sum4 in
       [sum5; sum6; sum7]
```

Isn't that lovely? Since we can push continuation functions "under"
the `dlet`s, we can end up with a nice, concise, simplified
expression.

One might suggest that we could just inline the `dlet`s and do common
subexpression elimination. But some of our terms have so many `dlet`s
that inlining them all would make a term too huge to process in
reasonable time, so this is not really an option.

*****)

Require Import Coq.ZArith.ZArith Coq.micromega.Psatz Coq.omega.Omega.
Require Import Coq.ZArith.BinIntDef.
Local Open Scope Z_scope.

Require Import Crypto.Algebra.Nsatz.
Require Import Crypto.Util.Decidable Crypto.Util.LetIn.
Require Import Crypto.Util.ListUtil Crypto.Util.Sigma.
Require Import Crypto.Util.CPSUtil Crypto.Util.Prod.
Require Import Crypto.Util.ZUtil.Modulo.PullPush.
Require Import Crypto.Util.ZUtil.Zselect.
Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Util.ZUtil.Definitions.
Require Import Crypto.Util.ZUtil.CPS.
Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.UniquePose.
Require Import Crypto.Util.Tactics.VM.
Require Import Crypto.Util.IdfunWithAlt.
Require Import Crypto.Util.Notations.

Require Import Coq.Lists.List. Import ListNotations.
Require Crypto.Util.Tuple. Local Notation tuple := Tuple.tuple.

Local Ltac prove_id :=
  repeat match goal with
         | _ => progress intros
         | _ => progress simpl
         | _ => progress cbv [Let_In]
         | _ => progress (autorewrite with uncps push_id in * )
         | _ => break_innermost_match_step
         | _ => contradiction
         | _ => reflexivity
         | _ => nsatz
         | _ => solve [auto]
         end.

Create HintDb push_basesystem_eval discriminated.
Local Ltac prove_eval :=
  repeat match goal with
         | _ => progress intros
         | _ => progress simpl
         | _ => progress cbv [Let_In]
         | _ => progress Z.ltb_to_lt
         | _ => progress (autorewrite with push_basesystem_eval uncps push_id cancel_pair in * )
         | _ => break_innermost_match_step
         | _ => split
         | H : _ /\ _ |- _ => destruct H
         | H : Some _ = Some _ |- _ => progress (inversion H; subst)
         | _ => discriminate
         | _ => reflexivity
         | _ => nsatz
         end.

Definition mod_eq (m:positive) a b := a mod m = b mod m.
Global Instance mod_eq_equiv m : RelationClasses.Equivalence (mod_eq m).
Proof. constructor; congruence. Qed.
Definition mod_eq_dec m a b : {mod_eq m a b} + {~ mod_eq m a b}
  := Z.eq_dec _ _.
Lemma mod_eq_Z2F_iff m a b :
  mod_eq m a b <-> Logic.eq (F.of_Z m a) (F.of_Z m b).
Proof. rewrite <-F.eq_of_Z_iff; reflexivity. Qed.

Delimit Scope runtime_scope with RT.

Definition runtime_mul := Z.mul.
Global Notation "a * b" := (runtime_mul a%RT b%RT) : runtime_scope.
Definition runtime_add := Z.add.
Global Notation "a + b" := (runtime_add a%RT b%RT) : runtime_scope.
Definition runtime_opp := Z.opp.
Global Notation "- a" := (runtime_opp a%RT) : runtime_scope.
Definition runtime_and := Z.land.
Global Notation "a &' b" := (runtime_and a%RT b%RT) : runtime_scope.
Definition runtime_shr := Z.shiftr.
Global Notation "a >> b" := (runtime_shr a%RT b%RT) : runtime_scope.
Definition runtime_lor := Z.lor.
Global Arguments runtime_lor (_ _)%RT.

Ltac cbv_runtime := cbv beta delta [runtime_add runtime_and runtime_lor runtime_mul runtime_opp runtime_shr].

Module B.
  Definition limb := (Z*Z)%type. (* position coefficient and run-time value *)
  Module Associational.
    Definition eval (p:list limb) : Z :=
      List.fold_right Z.add 0%Z (List.map (fun t => fst t * snd t) p).

    Lemma eval_nil : eval nil = 0. Proof. reflexivity. Qed.
    Lemma eval_cons p q : eval (p::q) = (fst p) * (snd p) + eval q. Proof. reflexivity. Qed.
    Lemma eval_app p q: eval (p++q) = eval p + eval q.
    Proof. induction p; simpl eval; rewrite ?eval_nil, ?eval_cons; nsatz. Qed.
    Hint Rewrite eval_nil eval_cons eval_app : push_basesystem_eval.

    Definition multerm (t t' : limb) : limb :=
      (fst t * fst t', (snd t * snd t')%RT).
    Lemma eval_map_multerm (a:limb) (q:list limb)
      : eval (List.map (multerm a) q) = fst a * snd a * eval q.
    Proof.
      induction q; cbv [multerm]; simpl List.map;
        autorewrite with push_basesystem_eval cancel_pair; nsatz.
    Qed. Hint Rewrite eval_map_multerm : push_basesystem_eval.

    Definition mul_cps (p q:list limb) {T} (f : list limb->T) :=
      flat_map_cps (fun t => @map_cps _ _ (multerm t) q) p f.

    Definition mul (p q:list limb) := mul_cps p q id.
    Lemma mul_cps_id p q: forall {T} f, @mul_cps p q T f = f (mul p q).
    Proof. cbv [mul_cps mul]; prove_id. Qed.
    Hint Opaque mul : uncps.
    Hint Rewrite mul_cps_id : uncps.

    Lemma eval_mul p q: eval (mul p q) = eval p * eval q.
    Proof. cbv [mul mul_cps]; induction p; prove_eval. Qed.
    Hint Rewrite eval_mul : push_basesystem_eval.

    Section split_cps.
      Context (s:Z) {T : Type}.

      Fixpoint split_cps (xs:list limb)
               (f :list limb*list limb->T) :=
        match xs with
        | nil => f (nil, nil)
        | cons x xs' =>
          split_cps xs'
                (fun sxs' =>
          Z.eqb_cps (fst x mod s) 0
                    (fun b =>
          if b
          then f (fst sxs',          cons (fst x / s, snd x) (snd sxs'))
          else f (cons x (fst sxs'), snd sxs')))
        end.
    End split_cps.

    Definition split s xs := split_cps s xs id.
    Lemma split_cps_id s p: forall {T} f,
        @split_cps s T p f = f (split s p).
    Proof.
      induction p as [|?? IHp];
        repeat match goal with
               | _ => rewrite IHp
               | _ => progress (cbv [split]; prove_id)
               end.
    Qed.
    Hint Opaque split : uncps.
    Hint Rewrite split_cps_id : uncps.

    Lemma eval_split s p (s_nonzero:s<>0):
      eval (fst (split s p)) + s*eval (snd (split s p)) = eval p.
    Proof.
      cbv [split];  induction p; prove_eval.
      match goal with
        H:_ |- _ =>
        unique pose proof (Z_div_exact_full_2 _ _ s_nonzero H)
        end; nsatz.
    Qed. Hint Rewrite @eval_split using auto : push_basesystem_eval.

    Definition reduce_cps (s:Z) (c:list limb) (p:list limb)
               {T} (f : list limb->T) :=
      split_cps s p
                (fun ab => mul_cps c (snd ab)
                                  (fun rr =>f (fst ab ++ rr))).

    Definition reduce s c p := reduce_cps s c p id.
    Lemma reduce_cps_id s c p {T} f:
      @reduce_cps s c p T f = f (reduce s c p).
    Proof. cbv [reduce_cps reduce]; prove_id. Qed.
    Hint Opaque reduce : uncps.
    Hint Rewrite reduce_cps_id : uncps.

    Lemma reduction_rule a b s c m (m_eq:Z.pos m = s - c):
      (a + s * b) mod m = (a + c * b) mod m.
    Proof.
      rewrite m_eq. pose proof (Pos2Z.is_pos m).
      replace (a + s * b) with ((a + c*b) + b*(s-c)) by ring.
      rewrite Z.add_mod, Z_mod_mult, Z.add_0_r, Z.mod_mod by omega.
      trivial.
    Qed.
    Lemma eval_reduce s c p (s_nonzero:s<>0) m (m_eq : Z.pos m = s - eval c) :
      mod_eq m (eval (reduce s c p)) (eval p).
    Proof.
      cbv [reduce reduce_cps mod_eq]; prove_eval.
        erewrite <-reduction_rule by eauto; prove_eval.
    Qed.
    Hint Rewrite eval_reduce using (omega || assumption) : push_basesystem_eval.
    (* Why TF does this hint get picked up outside the section (while other eval_ hints do not?) *)


    Definition negate_snd_cps (p:list limb) {T} (f:list limb ->T) :=
      map_cps (fun cx => (fst cx, (-snd cx)%RT)) p f.

    Definition negate_snd p := negate_snd_cps p id.
    Lemma negate_snd_id p {T} f : @negate_snd_cps p T f = f (negate_snd p).
    Proof. cbv [negate_snd_cps negate_snd]; prove_id. Qed.
    Hint Opaque negate_snd : uncps.
    Hint Rewrite negate_snd_id : uncps.

    Lemma eval_negate_snd p : eval (negate_snd p) = - eval p.
    Proof.
      cbv [negate_snd_cps negate_snd]; induction p; prove_eval.
    Qed. Hint Rewrite eval_negate_snd : push_basesystem_eval.

    Section Carries.
      Context {modulo_cps div_cps:forall {R},Z->Z->(Z->R)->R}.
      Let modulo x y := modulo_cps _ x y id.
      Let div x y := div_cps _ x y id.
      Context {modulo_cps_id : forall R x y f, modulo_cps R x y f = f (modulo x y)}
              {div_cps_id : forall R x y f, div_cps R x y f = f (div x y)}.
      Context {div_mod : forall a b:Z, b <> 0 ->
                                       a = b * (div a b) + modulo a b}.
      Hint Rewrite modulo_cps_id div_cps_id : uncps.

      Definition carryterm_cps (w fw:Z) (t:limb) {T} (f:list limb->T) :=
        Z.eqb_cps (fst t) w (fun eqb =>
        if eqb
        then dlet t2 := snd t in
             div_cps _ t2 fw (fun d2 =>
             modulo_cps _ t2 fw (fun m2 =>
             dlet d2 := d2 in
             dlet m2 := m2 in
             f ((w*fw, d2) :: (w, m2) :: @nil limb)))
        else f [t]).

      Definition carryterm w fw t := carryterm_cps w fw t id.
      Lemma carryterm_cps_id w fw t {T} f :
        @carryterm_cps w fw t T f
        = f (@carryterm w fw t).
      Proof using div_cps_id modulo_cps_id.
        cbv [carryterm_cps carryterm Let_In]; prove_id.
      Qed.
      Hint Opaque carryterm : uncps.
      Hint Rewrite carryterm_cps_id : uncps.


      Lemma eval_carryterm w fw (t:limb) (fw_nonzero:fw<>0):
        eval (carryterm w fw t) = eval [t].
      Proof using Type*.
        cbv [carryterm_cps carryterm Let_In]; prove_eval.
        specialize (div_mod (snd t) fw fw_nonzero).
        nsatz.
      Qed. Hint Rewrite eval_carryterm using auto : push_basesystem_eval.

      Definition carry_cps (w fw:Z) (p:list limb) {T} (f:list limb->T) :=
        flat_map_cps (carryterm_cps w fw) p f.

      Definition carry w fw p := carry_cps w fw p id.
      Lemma carry_cps_id w fw p {T} f:
        @carry_cps w fw p T f = f (carry w fw p).
      Proof using div_cps_id modulo_cps_id.
        cbv [carry_cps carry]; prove_id.
      Qed.
      Hint Opaque carry : uncps.
      Hint Rewrite carry_cps_id : uncps.

      Lemma eval_carry w fw p (fw_nonzero:fw<>0):
        eval (carry w fw p) = eval p.
      Proof using Type*. cbv [carry_cps carry]; induction p; prove_eval. Qed.
      Hint Rewrite eval_carry using auto : push_basesystem_eval.
    End Carries.

  End Associational.

  Ltac div_mod_cps_t :=
    intros; autorewrite with uncps push_id; try reflexivity.

  Hint Rewrite
      @Associational.reduce_cps_id
      @Associational.split_cps_id
      @Associational.mul_cps_id : uncps.
  Hint Rewrite
       @Associational.carry_cps_id
       @Associational.carryterm_cps_id
       using div_mod_cps_t : uncps.


  Module Positional.
    Section Positional.
      Import Associational.
      Context (weight : nat -> Z) (* [weight i] is the weight of position [i] *)
              (weight_0 : weight 0%nat = 1%Z)
              (weight_nonzero : forall i, weight i <> 0).

      (** Converting from positional to associational *)
      Definition to_associational_cps {n:nat} (xs:tuple Z n)
                 {T} (f:list limb->T) :=
        map_cps weight (seq 0 n)
                (fun r =>
                   to_list_cps n xs (fun rr => combine_cps r rr f)).

      Definition to_associational {n} xs :=
        @to_associational_cps n xs _ id.
      Lemma to_associational_cps_id {n} x {T} f:
        @to_associational_cps n x T f = f (to_associational x).
      Proof using Type. cbv [to_associational_cps to_associational]; prove_id. Qed.
      Hint Opaque to_associational : uncps.
      Hint Rewrite @to_associational_cps_id : uncps.

      Definition eval {n} x :=
        @to_associational_cps n x _ Associational.eval.

      Lemma eval_single (x:Z) : eval (n:=1) x = weight 0%nat * x.
      Proof. cbv - [Z.mul Z.add]. ring. Qed.

      Lemma eval_unit : eval (n:=0) tt = 0.
      Proof. reflexivity. Qed.
      Hint Rewrite eval_unit eval_single : push_basesystem_eval.

      Lemma eval_to_associational {n} x :
        Associational.eval (@to_associational n x) = eval x.
      Proof using Type.
        cbv [to_associational_cps eval to_associational]; prove_eval.
      Qed. Hint Rewrite @eval_to_associational : push_basesystem_eval.

      (** (modular) equality that tolerates redundancy **)
      Definition eq {sz} m (a b : tuple Z sz) : Prop :=
        mod_eq m (eval a) (eval b).

      (** Converting from associational to positional *)

      Definition zeros n : tuple Z n := Tuple.repeat 0 n.
      Lemma eval_zeros n : eval (zeros n) = 0.
      Proof using Type.
        cbv [eval Associational.eval to_associational_cps zeros].
        pose proof (seq_length n 0). generalize dependent (seq 0 n).
        intro xs; revert n; induction xs as [|?? IHxs]; intros n H;
          [autorewrite with uncps; reflexivity|].
        destruct n as [|n]; [distr_length|].
        specialize (IHxs n). autorewrite with uncps in *.
        rewrite !@Tuple.to_list_repeat in *.
        simpl List.repeat. rewrite map_cons, combine_cons, map_cons.
        simpl fold_right.  rewrite IHxs by distr_length. ring.
      Qed. Hint Rewrite eval_zeros : push_basesystem_eval.

      Definition add_to_nth_cps {n} i x t {T} (f:tuple Z n->T) :=
        @on_tuple_cps _ _ 0 (update_nth_cps i (runtime_add x)) n n t _ f.

      Definition add_to_nth {n} i x t := @add_to_nth_cps n i x t _ id.
      Lemma add_to_nth_cps_id {n} i x xs {T} f:
        @add_to_nth_cps n i x xs T f = f (add_to_nth i x xs).
      Proof using weight.
        cbv [add_to_nth_cps add_to_nth]; erewrite !on_tuple_cps_correct
          by (intros; autorewrite with uncps; reflexivity); prove_id.
        Unshelve.
        intros; subst. autorewrite with uncps push_id. distr_length.
      Qed.
      Hint Opaque add_to_nth : uncps.
      Hint Rewrite @add_to_nth_cps_id : uncps.

      Lemma eval_add_to_nth {n} (i:nat) (x:Z) (H:(i<n)%nat) (xs:tuple Z n):
        eval (@add_to_nth n i x xs) = weight i * x + eval xs.
      Proof using Type.
        cbv [eval to_associational_cps add_to_nth add_to_nth_cps runtime_add].
        erewrite on_tuple_cps_correct by (intros; autorewrite with uncps; reflexivity).
        prove_eval.
        cbv [Tuple.on_tuple].
        rewrite !Tuple.to_list_from_list.
        autorewrite with uncps push_id.
        rewrite ListUtil.combine_update_nth_r at 1.
        rewrite <-(update_nth_id i (List.combine _ _)) at 2.
        rewrite <-!(ListUtil.splice_nth_equiv_update_nth_update _ _ (weight 0, 0)); cbv [ListUtil.splice_nth id];
          repeat match goal with
                 | _ => progress (apply Zminus_eq; ring_simplify)
                 | _ => progress autorewrite with push_basesystem_eval cancel_pair distr_length
                 | _ => progress rewrite <-?ListUtil.map_nth_default_always, ?map_fst_combine, ?List.firstn_all2, ?ListUtil.map_nth_default_always, ?nth_default_seq_inbouns, ?plus_O_n
                 end; trivial; lia.
        Unshelve.
        intros; subst. autorewrite with uncps push_id. distr_length.
      Qed. Hint Rewrite @eval_add_to_nth using omega : push_basesystem_eval.

      Section place_cps.
        Context {T : Type}.

        Fixpoint place_cps (t:limb) (i:nat) (f:nat * Z->T) :=
          Z.eqb_cps (fst t mod weight i) 0 (fun eqb =>
          if eqb
          then f (i, let c := fst t / weight i in (c * snd t)%RT)
          else match i with S i' => place_cps t i' f | O => f (O, fst t * snd t)%RT end).
      End place_cps.

      Definition place t i := place_cps t i id.
      Lemma place_cps_id t i {T} f :
        @place_cps T t i f = f (place t i).
      Proof using Type. cbv [place]; induction i; prove_id. Qed.
      Hint Opaque place : uncps.
      Hint Rewrite place_cps_id : uncps.

      Lemma place_cps_in_range (t:limb) (n:nat)
        : (fst (place_cps t n id) < S n)%nat.
      Proof using Type. induction n; simpl; cbv [Z.eqb_cps]; break_match; simpl; omega. Qed.
      Lemma weight_place_cps t i
        : weight (fst (place_cps t i id)) * snd (place_cps t i id)
          = fst t * snd t.
      Proof using Type*.
        induction i; cbv [id]; simpl place_cps; cbv [Z.eqb_cps]; break_match;
          Z.ltb_to_lt;
          autorewrite with cancel_pair;
          try match goal with [H:_|-_] => apply Z_div_exact_full_2 in H end;
          nsatz || auto.
      Qed.

      Definition from_associational_cps n (p:list limb)
                 {T} (f:tuple Z n->T):=
        fold_right_cps2
          (fun t st T' f' =>
             place_cps t (pred n)
                       (fun p=> add_to_nth_cps (fst p) (snd p) st f'))
          (zeros n) p f.

      Definition from_associational n p := from_associational_cps n p id.
      Lemma from_associational_cps_id {n} p {T} f:
        @from_associational_cps n p T f = f (from_associational n p).
      Proof using Type.
        cbv [from_associational_cps from_associational]; prove_id.
      Qed.
      Hint Opaque from_associational : uncps.
      Hint Rewrite @from_associational_cps_id : uncps.

      Lemma eval_from_associational {n} p (n_nonzero:n<>O):
        eval (from_associational n p) = Associational.eval p.
      Proof using Type*.
        cbv [from_associational_cps from_associational]; induction p;
          [|pose proof (place_cps_in_range a (pred n))]; prove_eval.
        cbv [place]; rewrite weight_place_cps. nsatz.
      Qed.
      Hint Rewrite @eval_from_associational using omega
        : push_basesystem_eval.


      Section Wrappers.
        (* Simple wrappers for Associational definitions; convert to
        associational, do the operation, convert back. *)

        Definition add_cps {n} (p q : tuple Z n) {T} (f:tuple Z n->T) :=
          to_associational_cps p
            (fun P => to_associational_cps q
              (fun Q => from_associational_cps n (P++Q) f)).

        Definition mul_cps {n m} (p q : tuple Z n) {T} (f:tuple Z m->T) :=
          to_associational_cps p
            (fun P => to_associational_cps q
              (fun Q => Associational.mul_cps P Q
                (fun PQ => from_associational_cps m PQ f))).

        Definition reduce_cps {m n} (s:Z) (c:list B.limb) (p : tuple Z m)
                   {T} (f:tuple Z n->T) :=
          to_associational_cps p
            (fun P => Associational.reduce_cps s c P
               (fun R => from_associational_cps n R f)).

        Definition negate_snd_cps {n} (p : tuple Z n)
                   {T} (f:tuple Z n->T) :=
          to_associational_cps p
            (fun P => Associational.negate_snd_cps P
              (fun R => from_associational_cps n R f)).

        Definition split_cps {n m1 m2} (s:Z) (p : tuple Z n)
                    {T} (f:(tuple Z m1 * tuple Z m2) -> T) :=
          to_associational_cps p
            (fun P => Associational.split_cps s P
            (fun split_P =>
               from_associational_cps m1 (fst split_P)
                 (fun m1_P =>
               from_associational_cps m2 (snd split_P)
                 (fun m2_P =>
                    f (m1_P, m2_P))))).

        Definition scmul_cps {n} (x : Z) (p: tuple Z n)
                    {T} (f:tuple Z n->T) :=
          to_associational_cps p
            (fun P => Associational.mul_cps P [(1, x)]
            (fun R => from_associational_cps n R f)).

        (* This version of sub does not add balance; bounds must be
        carefully handled. *)
        Definition unbalanced_sub_cps {n} (p q: tuple Z n)
                    {T} (f:tuple Z n->T) :=
          to_associational_cps p
            (fun P => to_associational_cps q
            (fun Q => Associational.negate_snd_cps Q
            (fun negQ => from_associational_cps n (P ++ negQ) f))).

      End Wrappers.
      Hint Unfold
           Positional.add_cps
           Positional.mul_cps
           Positional.reduce_cps
           Positional.negate_snd_cps
           Positional.split_cps
           Positional.scmul_cps
           Positional.unbalanced_sub_cps
      .

      Section Carries.
        Context {modulo_cps div_cps:forall {R},Z->Z->(Z->R)->R}.
        Let modulo x y := modulo_cps _ x y id.
        Let div x y := div_cps _ x y id.
        Context {modulo_cps_id : forall R x y f, modulo_cps R x y f = f (modulo x y)}
                {div_cps_id : forall R x y f, div_cps R x y f = f (div x y)}.
        Context {div_mod : forall a b:Z, b <> 0 ->
                                         a = b * (div a b) + modulo a b}.
        Hint Rewrite modulo_cps_id div_cps_id : uncps.

        Definition carry_cps {n m} (index:nat) (p:tuple Z n)
                   {T} (f:tuple Z m->T) :=
          to_associational_cps p
            (fun P =>  @Associational.carry_cps
                         modulo_cps div_cps
                         (weight index)
                         (weight (S index) / weight index)
                         P T
             (fun R => from_associational_cps m R f)).

        Definition carry {n m} i p := @carry_cps n m i p _ id.
        Lemma carry_cps_id {n m} i p {T} f:
          @carry_cps n m i p T f = f (carry i p).
        Proof.
          cbv [carry_cps carry]; prove_id; rewrite carry_cps_id; reflexivity.
        Qed.
        Hint Opaque carry : uncps. Hint Rewrite @carry_cps_id : uncps.

        Lemma eval_carry {n m} i p: (n <> 0%nat) -> (m <> 0%nat) ->
                                  weight (S i) / weight i <> 0 ->
          eval (carry (n:=n) (m:=m) i p) = eval p.
        Proof.
          cbv [carry_cps carry]; intros. prove_eval.
          rewrite @eval_carry by eauto.
          apply eval_to_associational.
        Qed.
        Hint Rewrite @eval_carry : push_basesystem_eval.

        Definition carry_reduce_cps {n}
                   (s:Z) (c:list limb) (p : tuple Z n)
                   {T} (f: tuple Z n ->T) :=
          carry_cps (n:=n) (m:=S n) (pred n) p
            (fun r => reduce_cps (m:=S n) (n:=n) s c r f).
        Hint Unfold carry_reduce_cps.

        (* N.B. It is important to reverse [idxs] here. Like
        [fold_right], [fold_right_cps2] is written such that the first
        terms in the list are actually used last in the computation. For
        example, running:

        `Eval cbv - [Z.add] in (fun a b c d => fold_right Z.add d [a;b;c]).`

        will produce [fun a b c d => (a + (b + (c + d)))].*)
        Definition chained_carries_cps {n} (p:tuple Z n) (idxs : list nat)
                   {T} (f:tuple Z n->T) :=
          fold_right_cps2 carry_cps p (rev idxs) f.

        Definition chained_carries {n} p idxs := @chained_carries_cps n p idxs _ id.
        Lemma chained_carries_id {n} p idxs : forall {T} f,
            @chained_carries_cps n p idxs T f = f (chained_carries p idxs).
        Proof using modulo_cps_id div_cps_id.
          cbv [chained_carries_cps chained_carries]; prove_id.
        Qed.
        Hint Opaque chained_carries : uncps.
        Hint Rewrite @chained_carries_id : uncps.

        Lemma eval_chained_carries {n} (p:tuple Z n) idxs :
          (forall i, In i idxs -> weight (S i) / weight i <> 0) ->
          eval (chained_carries p idxs) = eval p.
        Proof using Type*.
          cbv [chained_carries chained_carries_cps]; intros;
            autorewrite with uncps push_id.
          apply fold_right_invariant; [|intro; rewrite <-in_rev];
            destruct n; prove_eval; auto.
        Qed. Hint Rewrite @eval_chained_carries : push_basesystem_eval.

        Definition chained_carries_reduce_cps_step {n} (s:Z) (c:list limb) {T}
                   (chained_carries_reduce_cps : forall (p:tuple Z n) (carry_chains : list (list nat)) (f : tuple Z n -> T), T)
                   (p : tuple Z n) (carry_chains : list (list nat))
                   (f : tuple Z n -> T)
          : T
          := match carry_chains with
             | nil => f p
             | carry_chain :: nil
               => chained_carries_cps
                    (n:=n) p carry_chain f
             | carry_chain :: carry_chains
               => chained_carries_cps
                    (n:=n) p carry_chain
                    (fun r => carry_reduce_cps (n:=n) s c r
                    (fun r' => chained_carries_reduce_cps r' carry_chains f))
             end.
        Section chained_carries_reduce_cps.
          Context {n:nat} (s:Z) (c:list limb) {T:Type}.

          Fixpoint chained_carries_reduce_cps
                   (p : tuple Z n) (carry_chains : list (list nat))
                   (f : tuple Z n -> T)
            : T
            := @chained_carries_reduce_cps_step
                 n s c T
                 chained_carries_reduce_cps p carry_chains f.
        End chained_carries_reduce_cps.

        Lemma step_chained_carries_reduce_cps {n} (s:Z) (c:list limb) {T} p carry_chain carry_chains (f : tuple Z n -> T)
          : chained_carries_reduce_cps s c p (carry_chain :: carry_chains) f
            = match length carry_chains with
              | O => chained_carries_cps
                       (n:=n) p carry_chain f
              | S _
                => chained_carries_cps
                     (n:=n) p carry_chain
                     (fun r => carry_reduce_cps (n:=n) s c r
                     (fun r' => chained_carries_reduce_cps s c r' carry_chains f))
              end.
        Proof.
          destruct carry_chains; reflexivity.
        Qed.

        Definition chained_carries_reduce {n} (s:Z) (c:list limb) (p:tuple Z n) (carry_chains : list (list nat))
          : tuple Z n
          := chained_carries_reduce_cps s c p carry_chains id.

        Lemma chained_carries_reduce_id {n} s c {T} p carry_chains f
          : @chained_carries_reduce_cps n s c T p carry_chains f
            = f (@chained_carries_reduce n s c p carry_chains).
        Proof.
          destruct carry_chains as [|carry_chain carry_chains]; [ reflexivity | ].
          cbv [chained_carries_reduce].
          revert p carry_chain; induction carry_chains as [|? carry_chains IHcarry_chains]; intros.
          { simpl; repeat autounfold; autorewrite with uncps. reflexivity. }
          { rewrite !step_chained_carries_reduce_cps.
            simpl @length; cbv iota beta.
            repeat autounfold; autorewrite with uncps.
            rewrite !IHcarry_chains.
            reflexivity. }
        Qed.
        Hint Opaque chained_carries_reduce : uncps.
        Hint Rewrite @chained_carries_reduce_id : uncps.

        Lemma eval_chained_carries_reduce {n} (s:Z) (c:list limb) (p:tuple Z n) carry_chains
              (Hn : n <> 0%nat)
              (s_nonzero:s<>0) m (m_eq : Z.pos m = s - Associational.eval c)
              (Hwt : weight (S (Init.Nat.pred n)) / weight (Init.Nat.pred n) <> 0)
          : (List.fold_right
               and
               True
               (List.map
                  (fun idxs
                   => forall i, In i idxs -> weight (S i) / weight i <> 0)
                  carry_chains)) ->
            mod_eq m (eval (chained_carries_reduce s c p carry_chains)) (eval p).
        Proof using Type*.
          destruct carry_chains as [|carry_chain carry_chains]; [ reflexivity | ].
          cbv [chained_carries_reduce].
          revert p carry_chain; induction carry_chains as [|? carry_chains IHcarry_chains]; intros.
          { cbn in *; prove_eval; auto. }
          { rewrite !step_chained_carries_reduce_cps.
            simpl @length; cbv iota beta.
            repeat autounfold; autorewrite with uncps push_id push_basesystem_eval.
            cbv [chained_carries_reduce].
            rewrite !IHcarry_chains by (cbn in *; tauto); clear IHcarry_chains.
            cbn in * |- .
            prove_eval; auto. }
        Qed.
        Hint Rewrite @eval_chained_carries_reduce using (omega || assumption) : push_basesystem_eval.

        (* Reverse of [eval]; translate from Z to basesystem by putting
        everything in first digit and then carrying. This function, like
        [eval], is not defined using CPS. *)
        Definition encode {n} (x : Z) : tuple Z n :=
          chained_carries (from_associational n [(1,x)]) (seq 0 n).
        Lemma eval_encode {n} x : (n <> 0%nat) ->
          (forall i, In i (seq 0 n) -> weight (S i) / weight i <> 0) ->
          eval (@encode n x) = x.
        Proof using Type*. cbv [encode]; intros; prove_eval; auto. Qed.
        Hint Rewrite @eval_encode : push_basesystem_eval.

      End Carries.
      Hint Unfold carry_reduce_cps.

      Section Subtraction.
        Context {m n} {coef : tuple Z n}
                {coef_mod : mod_eq m (eval coef) 0}.

        Definition sub_cps (p q : tuple Z n) {T} (f:tuple Z n->T):=
          add_cps coef p
            (fun cp => negate_snd_cps q
              (fun _q => add_cps cp _q f)).

        Definition sub p q := sub_cps p q id.
        Lemma sub_id p q {T} f : @sub_cps p q T f = f (sub p q).
        Proof using Type. cbv [sub_cps sub]; autounfold; prove_id. Qed.
        Hint Opaque sub : uncps.
        Hint Rewrite sub_id : uncps.

        Lemma eval_sub p q : mod_eq m (eval (sub p q)) (eval p - eval q).
        Proof using Type*.
          cbv [sub sub_cps]; autounfold; destruct n; prove_eval.
          transitivity (eval coef + (eval p - eval q)).
          { apply f_equal2; ring. }
          { cbv [mod_eq] in *; rewrite Z.add_mod_full, coef_mod, Z.add_0_l, Zmod_mod. reflexivity. }
        Qed.

        Definition opp_cps (p : tuple Z n) {T} (f:tuple Z n->T):=
          sub_cps (zeros n) p f.
      End Subtraction.

      (* Lemmas about converting to/from F. Will be useful in proving
      that basesystem is isomorphic to F.commutative_ring_modulo.*)
      Section F.
        Context {sz:nat} {sz_nonzero : sz<>0%nat} {m :positive}.
        Context (weight_divides : forall i : nat, weight (S i) / weight i <> 0).
        Context {modulo_cps div_cps:forall {R},Z->Z->(Z->R)->R}.
        Let modulo x y := modulo_cps _ x y id.
        Let div x y := div_cps _ x y id.
        Context {modulo_cps_id : forall R x y f, modulo_cps R x y f = f (modulo x y)}
                {div_cps_id : forall R x y f, div_cps R x y f = f (div x y)}.
        Context {div_mod : forall a b:Z, b <> 0 ->
                                         a = b * (div a b) + modulo a b}.
        Hint Rewrite modulo_cps_id div_cps_id : uncps.

        Definition Fencode (x : F m) : tuple Z sz :=
          encode (div_cps:=div_cps) (modulo_cps:=modulo_cps) (F.to_Z x).

        Definition Fdecode (x : tuple Z sz) : F m := F.of_Z m (eval x).

        Lemma Fdecode_Fencode_id x : Fdecode (Fencode x) = x.
        Proof using div_mod sz_nonzero weight_0 weight_divides weight_nonzero div_cps_id modulo_cps_id.
          cbv [Fdecode Fencode]; rewrite @eval_encode by eauto.
          apply F.of_Z_to_Z.
        Qed.

        Lemma eq_Feq_iff a b :
          Logic.eq (Fdecode a) (Fdecode b) <-> eq m a b.
        Proof using Type. cbv [Fdecode]; rewrite <-F.eq_of_Z_iff; reflexivity. Qed.
      End F.


    End Positional.
    Hint Rewrite eval_unit eval_single : push_basesystem_eval.

    (* Helper lemmas and definitions for [eval] that to be in a
    separate section so the weight function can change. *)
    Section EvalHelpers.
      Lemma eval_step {n} (x:tuple Z n) : forall wt z,
        eval wt (Tuple.append z x) = wt 0%nat * z + eval (fun i => wt (S i)) x.
      Proof.
        destruct n; [reflexivity|].
        intros; cbv [eval to_associational_cps].
        autorewrite with uncps. rewrite map_S_seq. reflexivity.
      Qed.

      Lemma eval_left_append {n} : forall wt x xs,
          eval wt (Tuple.left_append (n:=n) x xs)
          = wt n * x + eval wt xs.
      Proof.
        induction n as [|n IHn]; intros wt x xs; try destruct xs;
          unfold Tuple.left_append; fold @Tuple.left_append;
            autorewrite with push_basesystem_eval; [ring|].
        rewrite (Tuple.subst_append xs), Tuple.hd_append, Tuple.tl_append.
        rewrite !eval_step, IHn. ring.
      Qed.
      Hint Rewrite @eval_left_append : push_basesystem_eval.

      Lemma eval_wt_equiv {n} :forall wta wtb (x:tuple Z n),
          (forall i, wta i = wtb i) -> eval wta x = eval wtb x.
      Proof.
        destruct n as [|n]; [reflexivity|].
        induction n as [|n IHn]; intros wta wtb x H; [rewrite !eval_single, H; reflexivity|].
        simpl tuple in *; destruct x.
        change (t, z) with (Tuple.append (n:=S n) z t).
        rewrite !eval_step. rewrite (H 0%nat). apply Group.cancel_left.
        apply IHn; auto.
      Qed.

      Definition eval_from {n} weight (offset:nat) (x : tuple Z n) : Z :=
        eval (fun i => weight (i+offset)%nat) x.

      Lemma eval_from_0 {n} wt x : @eval_from n wt 0 x = eval wt x.
      Proof. cbv [eval_from]. auto using eval_wt_equiv. Qed.
    End EvalHelpers.

    Section Select.
      Context {weight : nat -> Z}.

      Definition select_cps {n} (mask cond:Z) (p:tuple Z n)
                 {T} (f:tuple Z n->T) :=
        dlet t := Z.zselect cond 0 mask in Tuple.map_cps (runtime_and t) p f.

      Definition select {n} mask cond p := @select_cps n mask cond p _ id.
      Lemma select_id {n} mask cond p T f :
        @select_cps n mask cond p T f = f (select mask cond p).
      Proof.
        cbv [select select_cps Let_In]; autorewrite with uncps push_id;
          reflexivity.
      Qed.
      Hint Opaque select : uncps.

      Lemma map_and_0 {n} (p:tuple Z n) : Tuple.map (Z.land 0) p = zeros n.
      Proof.
        induction n as [|n IHn]; [destruct p; reflexivity | ].
        rewrite (Tuple.subst_append p), Tuple.map_append, Z.land_0_l, IHn.
        reflexivity.
      Qed.

      Lemma eval_select {n} mask cond x (H:Tuple.map (Z.land mask) x = x) :
        B.Positional.eval weight (@select n mask cond x) =
        if dec (cond = 0) then 0 else  B.Positional.eval weight x.
      Proof.
        cbv [select select_cps Let_In].
        autorewrite with uncps push_id.
        rewrite Z.zselect_correct; break_match.
        { rewrite map_and_0. apply B.Positional.eval_zeros. }
        {  change runtime_and with Z.land. rewrite H; reflexivity. }
      Qed.

    End Select.

  End Positional.

  Hint Unfold
      Positional.add_cps
      Positional.mul_cps
      Positional.reduce_cps
      Positional.carry_reduce_cps
      Positional.negate_snd_cps
      Positional.split_cps
      Positional.scmul_cps
      Positional.unbalanced_sub_cps
      Positional.opp_cps
  .
  Hint Rewrite
      @Associational.reduce_cps_id
      @Associational.split_cps_id
      @Associational.mul_cps_id
      @Positional.from_associational_cps_id
      @Positional.place_cps_id
      @Positional.add_to_nth_cps_id
      @Positional.to_associational_cps_id
      @Positional.sub_id
      @Positional.select_id
    : uncps.
  Hint Rewrite
       @Associational.carry_cps_id
       @Associational.carryterm_cps_id
       @Positional.carry_cps_id
       @Positional.chained_carries_id
       @Positional.chained_carries_reduce_id
       using div_mod_cps_t : uncps.
  Hint Rewrite
       @Associational.eval_mul
       @Positional.eval_single
       @Positional.eval_unit
       @Positional.eval_to_associational
       @Positional.eval_left_append
       @Associational.eval_carry
       @Associational.eval_carryterm
       @Associational.eval_reduce
       @Associational.eval_split
       @Positional.eval_zeros
       @Positional.eval_carry
       @Positional.eval_from_associational
       @Positional.eval_add_to_nth
       @Positional.eval_chained_carries
       @Positional.eval_chained_carries_reduce
       @Positional.eval_sub
       @Positional.eval_select
       using (assumption || (div_mod_cps_t; auto) || vm_decide) : push_basesystem_eval.
End B.

(* Modulo and div that do shifts if possible, otherwise normal mod/div *)
Section DivMod.
  Definition modulo_cps {T} (a b : Z) (f : Z -> T) : T :=
    Z.eqb_cps (2 ^ (Z.log2 b)) b (fun eqb =>
    if eqb
    then let x := (Z.ones (Z.log2 b)) in f (a &' x)%RT
    else f (Z.modulo a b)).

  Definition div_cps {T} (a b : Z) (f : Z -> T) : T :=
    Z.eqb_cps (2 ^ (Z.log2 b)) b (fun eqb =>
    if eqb
    then let x := Z.log2 b in f ((a >> x)%RT)
    else f (Z.div a b)).

  Definition modulo (a b : Z) : Z := modulo_cps a b id.
  Definition div (a b : Z) : Z := div_cps a b id.

  Lemma modulo_id {T} a b f
    : @modulo_cps T a b f = f (modulo a b).
  Proof. cbv [modulo_cps modulo]; autorewrite with uncps; break_match; reflexivity. Qed.
  Hint Opaque modulo : uncps.
  Hint Rewrite @modulo_id : uncps.

  Lemma div_id {T} a b f
    : @div_cps T a b f = f (div a b).
  Proof. cbv [div_cps div]; autorewrite with uncps; break_match; reflexivity. Qed.
  Hint Opaque div : uncps.
  Hint Rewrite @div_id : uncps.

  Lemma div_cps_correct {T} a b f : @div_cps T a b f = f (Z.div a b).
  Proof.
    cbv [div_cps Z.eqb_cps]; intros. break_match; try reflexivity.
    rewrite Z.shiftr_div_pow2 by apply Z.log2_nonneg.
    Z.ltb_to_lt; congruence.
  Qed.

  Lemma modulo_cps_correct {T} a b f : @modulo_cps T a b f = f (Z.modulo a b).
  Proof.
    cbv [modulo_cps Z.eqb_cps]; intros. break_match; try reflexivity.
    rewrite Z.land_ones by apply Z.log2_nonneg.
    Z.ltb_to_lt; congruence.
  Qed.

  Definition div_correct a b : div a b = Z.div a b := div_cps_correct a b id.
  Definition modulo_correct a b : modulo a b = Z.modulo a b := modulo_cps_correct a b id.

  Lemma div_mod a b (H:b <> 0) : a = b * div a b + modulo a b.
  Proof.
    rewrite div_correct, modulo_correct; auto using Z.div_mod.
  Qed.
End DivMod.

Hint Opaque div modulo : uncps.
Hint Rewrite @div_id @modulo_id : uncps.

Import B.

Create HintDb basesystem_partial_evaluation_unfolder.

Hint Unfold
     id
     Associational.eval
     Associational.multerm
     Associational.mul_cps
     Associational.mul
     Associational.split_cps
     Associational.split
     Associational.reduce_cps
     Associational.reduce
     Associational.negate_snd_cps
     Associational.negate_snd
     Associational.carryterm_cps
     Associational.carryterm
     Associational.carry_cps
     Associational.carry
     Positional.to_associational_cps
     Positional.to_associational
     Positional.eval
     Positional.zeros
     Positional.add_to_nth_cps
     Positional.add_to_nth
     Positional.place_cps
     Positional.place
     Positional.from_associational_cps
     Positional.from_associational
     Positional.carry_cps
     Positional.carry
     Positional.chained_carries_cps
     Positional.chained_carries
     Positional.chained_carries_reduce_cps_step
     Positional.chained_carries_reduce_cps
     Positional.chained_carries_reduce
     Positional.encode
     Positional.add_cps
     Positional.mul_cps
     Positional.reduce_cps
     Positional.carry_reduce_cps
     Positional.negate_snd_cps
     Positional.split_cps
     Positional.scmul_cps
     Positional.unbalanced_sub_cps
     Positional.sub_cps
     Positional.sub
     Positional.opp_cps
     Positional.Fencode
     Positional.Fdecode
     Positional.eval_from
     Positional.select_cps
     Positional.select
     modulo div modulo_cps div_cps
     id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps'
     Z.add_get_carry_full Z.add_get_carry_full_cps
  : basesystem_partial_evaluation_unfolder.

Hint Unfold
     B.limb ListUtil.sum ListUtil.sum_firstn
     CPSUtil.Tuple.mapi_with_cps CPSUtil.Tuple.mapi_with'_cps CPSUtil.flat_map_cps CPSUtil.on_tuple_cps CPSUtil.fold_right_cps2
     Decidable.dec Decidable.dec_eq_Z
     id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps'
     Z.add_get_carry_full Z.add_get_carry_full_cps Z.mul_split Z.mul_split_cps Z.mul_split_cps'
  : basesystem_partial_evaluation_unfolder.


Ltac basesystem_partial_evaluation_unfolder t :=
  eval
    cbv
    delta [
      (* this list must contain all definitions referenced by t that reference [Let_In], [runtime_add], [runtime_opp], [runtime_mul], [runtime_shr], or [runtime_and] *)
      id
        Positional.to_associational_cps Positional.to_associational
        Positional.eval Positional.zeros Positional.add_to_nth_cps
        Positional.add_to_nth Positional.place_cps Positional.place
        Positional.from_associational_cps Positional.from_associational
        Positional.carry_cps Positional.carry
        Positional.chained_carries_cps Positional.chained_carries
        Positional.chained_carries_reduce_cps
        Positional.chained_carries_reduce
        Positional.chained_carries_reduce_cps_step
        Positional.sub_cps Positional.sub Positional.split_cps
        Positional.scmul_cps Positional.unbalanced_sub_cps
        Positional.negate_snd_cps Positional.add_cps Positional.opp_cps
        Associational.eval Associational.multerm Associational.mul_cps
        Associational.mul Associational.split_cps Associational.split
        Associational.reduce_cps Associational.reduce
        Associational.carryterm_cps Associational.carryterm
        Associational.carry_cps Associational.carry
        Associational.negate_snd_cps Associational.negate_snd div modulo
        id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps'
        Z.add_get_carry_full Z.add_get_carry_full_cps
    ] in t.

Ltac pattern_strip t :=
  let t := (eval pattern @Let_In,
            @runtime_mul, @runtime_add, @runtime_opp, @runtime_shr, @runtime_and, @runtime_lor,
            @id_with_alt,
            @Z.add_get_carry, @Z.zselect
             in t) in
  let t := match t with ?t _ _ _ _ _ _ _ _ _ _ => t end in
  t.

Ltac apply_patterned t1 :=
  constr:(t1
            (@Let_In)
            (@runtime_mul)
            (@runtime_add)
            (@runtime_opp)
            (@runtime_shr)
            (@runtime_and)
            (@runtime_lor)
            (@id_with_alt)
            (@Z.add_get_carry)
            (@Z.zselect)).

Ltac pattern_strip_full t :=
  let t := (eval pattern
                 (@Let_In Z (fun _ => Z)),
            @Z.add_get_carry_cps, @Z.mul_split_at_bitwidth_cps,
            (@Z.eq_dec_cps), (@Z.eqb_cps),
            @runtime_mul, @runtime_add, @runtime_opp, @runtime_shr, @runtime_and, @runtime_lor,
            (@id_with_alt Z),
            @Z.add_get_carry, @Z.zselect, @Z.mul_split_at_bitwidth,
            Z.mul, Z.add, Z.opp, Z.shiftr, Z.shiftl, Z.land, Z.lor,
            Z.modulo, Z.div, Z.log2, Z.pow, Z.ones,
            Z.eq_dec, Z.eqb,
            (@ModularArithmetic.F.to_Z), (@ModularArithmetic.F.of_Z),
            2%Z, 1%Z, 0%Z
             in t) in
  let t := match t with ?t
                         _
                         _ _
                         _ _
                         _ _ _ _ _ _
                         _
                         _ _ _
                         _ _ _ _ _ _ _
                         _ _ _ _ _
                         _ _
                         _ _
                         _ _ _ => t end in
  let t := (eval pattern Z, (@Let_In), (@id_with_alt) in t) in
  let t := match t with ?t _ _ _ => t end in
  t.

Ltac apply_patterned_full t1 :=
  constr:(t1
            Z
            (@Let_In) (@id_with_alt)
            (@Let_In Z (fun _ => Z))
            (@Z.add_get_carry_cps) (@Z.mul_split_at_bitwidth_cps)
            (@Z.eq_dec_cps) (@Z.eqb_cps)
            (@runtime_mul) (@runtime_add) (@runtime_opp) (@runtime_shr) (@runtime_and) (@runtime_lor)
            (@id_with_alt Z)
            (@Z.add_get_carry) (@Z.zselect) (@Z.mul_split_at_bitwidth)
            Z.mul Z.add Z.opp Z.shiftr Z.shiftl Z.land Z.lor
            Z.modulo Z.div Z.log2 Z.pow Z.ones
            Z.eq_dec Z.eqb
            (@ModularArithmetic.F.to_Z) (@ModularArithmetic.F.of_Z)
            2%Z 1%Z 0%Z).

Ltac basesystem_partial_evaluation_gen unfold_tac t t1 :=
  let t := unfold_tac t in
  let t := pattern_strip t in
  let dummy := match goal with _ => pose t as t1 end in
  let t1' := apply_patterned t1 in
  t1'.

Ltac basesystem_partial_evaluation_RHS_gen unfold_tac :=
  let t := match goal with |- _ _ ?t => t end in
  let t1 := fresh "t1" in
  let t1' := basesystem_partial_evaluation_gen unfold_tac t t1 in
  transitivity t1';
  [replace_with_vm_compute t1; clear t1|reflexivity].

Ltac basesystem_partial_evaluation_default_unfolder t :=
  basesystem_partial_evaluation_unfolder t.

Ltac basesystem_partial_evaluation_RHS :=
  basesystem_partial_evaluation_RHS_gen basesystem_partial_evaluation_default_unfolder.
Ltac basesystem_partial_evaluation :=
  basesystem_partial_evaluation_gen basesystem_partial_evaluation_default_unfolder.


(** This block of tactic code works around bug #5434
    (https://coq.inria.fr/bugs/show_bug.cgi?id=5434), that
    [vm_compute] breaks an invariant in pretyping/constr_matching.ml.
    So we refresh all of the names in match statements in the goal by
    crawling it.

    In particular, [replace_with_vm_compute] creates a [vm_compute]d
    term which has anonymous binders where pretyping expects there to
    be named binders.  This shows up when you try to match on the
    function (the branch statement of the match) with an Ltac pattern
    like [(fun x : ?T => ?C)] rather than [(fun x : ?T => @?C x)]; we
    use the former in reification to save the cost of many extra
    invocations of [cbv beta].  Luckily, patterns like [(fun x : ?T =>
    @?C x)] don't trigger this anomaly, so we can walk the term,
    fixing all match statements whose branches are functions whose
    binder names were eaten by [vm_compute] (note that in a match,
    every branch where the corresponding constructor takes arguments
    is represented internally as a function (lambda term)).  We fix
    the match statements by pulling out the branch with the [@?]
    pattern that doesn't trigger the anomaly, and then recreating the
    match with a destructuring [let] that hasn't been through
    [vm_compute], and therefore has name information that
    constr_matching is happy with. *)
Ltac replace_match_with_destructuring_match T :=
  match T with
  | ?F ?X
    => let F' := replace_match_with_destructuring_match F in
       let X' := replace_match_with_destructuring_match X in
       constr:(F' X')
  (* we must use [@?f a b] here and not [?f], or else we get an anomaly *)
  | match ?d with pair a b => @?f a b end
    => let d' := replace_match_with_destructuring_match d in
       let T' := fresh in
       constr:(let '(a, b) := d' in
               match f a b with
               | T' => ltac:(let v := (eval cbv beta delta [T'] in T') in
                             let v := replace_match_with_destructuring_match v in
                             exact v)
               end)
  | (fun a : ?A => @?f a)
    => let T' := fresh in
       let T' := fresh T' in
       let T' := fresh T' in
       constr:(fun a : A
               => match f a with
                  | T' => ltac:(let v := (eval cbv beta delta [T'] in T') in
                                let v := replace_match_with_destructuring_match v in
                                exact v)
                  end)
  | ?x => x
  end.
Ltac do_replace_match_with_destructuring_match_in_goal :=
  let G := get_goal in
  let G' := replace_match_with_destructuring_match G in
  change G'.

(* TODO : move *)
Lemma F_of_Z_opp {m} x : F.of_Z m (- x) = F.opp (F.of_Z m x).
Proof.
  cbv [F.opp]; intros. rewrite F.to_Z_of_Z, <-Z.sub_0_l.
  etransitivity; rewrite F.of_Z_mod;
    [rewrite Z.opp_mod_mod|]; reflexivity.
Qed.

Hint Rewrite <-@F.of_Z_add : pull_FofZ.
Hint Rewrite <-@F.of_Z_mul : pull_FofZ.
Hint Rewrite <-@F.of_Z_sub : pull_FofZ.
Hint Rewrite <-@F_of_Z_opp : pull_FofZ.

Ltac F_mod_eq :=
  cbv [Positional.Fdecode]; autorewrite with pull_FofZ;
  apply mod_eq_Z2F_iff.

Ltac presolve_op_mod_eq wt x :=
  transitivity (Positional.eval wt x); repeat autounfold;
  [ cbv [mod_eq]; apply f_equal2; [|reflexivity];
    apply f_equal
  | autorewrite with uncps push_id push_basesystem_eval ].

Ltac solve_op_mod_eq wt x :=
  presolve_op_mod_eq wt x;
  [ basesystem_partial_evaluation_RHS;
    do_replace_match_with_destructuring_match_in_goal
  | reflexivity ].

Ltac solve_op_F wt x := F_mod_eq; solve_op_mod_eq wt x.
Ltac presolve_op_F wt x := F_mod_eq; presolve_op_mod_eq wt x.