1 files changed, 0 insertions, 229 deletions
diff --git a/src/Specific/Framework/ReificationTypes.v b/src/Specific/Framework/ReificationTypes.v
deleted file mode 100644
index 47542d1c4..000000000
--- a/src/Specific/Framework/ReificationTypes.v
+++ /dev/null
@@ -1,229 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
-Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.ZRange Crypto.Util.BoundedWord.
-Require Import Crypto.Util.Tactics.DestructHead.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.Decidable.
-
-Require Import Crypto.Util.Tactics.PoseTermWithName.
-Require Import Crypto.Util.Tactics.CacheTerm.
-
-Ltac pose_local_limb_widths wt sz limb_widths :=
-  pose_term_with
-    ltac:(fun _ => (eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz))))
-           limb_widths.
-
-Ltac get_b_of upper_bound_of_exponent :=
-  constr:(fun exp => {| lower := 0 ; upper := upper_bound_of_exponent exp |}%Z). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
-
-(* The definition [bounds_exp] is a tuple-version of the limb-widths,
-   which are the [exp] argument in [b_of] above, i.e., the approximate
-   base-2 exponent of the bounds on the limb in that position. *)
-Ltac pose_local_bounds_exp sz limb_widths bounds_exp :=
-  pose_term_with_type
-    (Tuple.tuple Z sz)
-    ltac:(fun _ => eval compute in
-               (Tuple.from_list sz limb_widths eq_refl))
-           bounds_exp.
-
-Ltac internal_pose_local_bounds sz upper_bound_of_exponent bounds_exp bounds :=
-  let b_of := get_b_of upper_bound_of_exponent in
-  pose_term_with_type
-    (Tuple.tuple zrange sz)
-    ltac:(fun _ => eval compute in
-               (Tuple.map (fun e => b_of e) bounds_exp))
-           bounds.
-Ltac pose_local_bounds_tight sz upper_bound_of_exponent_tight bounds_exp bounds_tight :=
-  internal_pose_local_bounds sz upper_bound_of_exponent_tight bounds_exp bounds_tight.
-Ltac pose_local_bounds_loose sz upper_bound_of_exponent_loose bounds_exp bounds_loose :=
-  internal_pose_local_bounds sz upper_bound_of_exponent_loose bounds_exp bounds_loose.
-Ltac pose_local_bounds_limbwidths sz bounds_exp bounds_limbwidths :=
-  internal_pose_local_bounds sz (fun exp => (2^exp - 1)%Z) bounds_exp bounds_limbwidths.
-
-Ltac pose_bound1 r bound1 :=
-  cache_term_with_type_by
-    zrange
-    ltac:(exact {| lower := 0 ; upper := Z.pos r-1 |})
-           bound1.
-
-Ltac pose_local_lgbitwidth bitwidth lgbitwidth :=
-  pose_term_with
-    ltac:(fun _ => eval compute in (Z.to_nat (Z.log2_up bitwidth)))
-           lgbitwidth.
-
-Ltac pose_local_adjusted_bitwidth' lgbitwidth adjusted_bitwidth' :=
-  pose_term_with
-    ltac:(fun _ => eval compute in (2^lgbitwidth)%nat)
-           adjusted_bitwidth'.
-Ltac pose_adjusted_bitwidth adjusted_bitwidth' adjusted_bitwidth :=
-  cache_term adjusted_bitwidth' adjusted_bitwidth.
-
-Ltac pose_local_feZ sz feZ :=
-  pose_term_with
-    ltac:(fun _ => constr:(tuple Z sz))
-           feZ.
-
-Ltac pose_feW sz lgbitwidth feW :=
-  cache_term_with_type_by
-    Type
-    ltac:(let v := eval cbv [lgbitwidth] in (tuple (wordT lgbitwidth) sz) in exact v)
-           feW.
-Ltac internal_pose_feW_bounded feW bounds feW_bounded :=
-  cache_term_with_type_by
-    (feW -> Prop)
-    ltac:(let v := eval cbv [bounds] in (fun w : feW => is_bounded_by None bounds (map wordToZ w)) in exact_no_check v)
-           feW_bounded.
-Ltac pose_feW_tight_bounded feW bounds_tight feW_tight_bounded :=
-  internal_pose_feW_bounded feW bounds_tight feW_tight_bounded.
-Ltac pose_feW_loose_bounded feW bounds_loose feW_loose_bounded :=
-  internal_pose_feW_bounded feW bounds_loose feW_loose_bounded.
-Ltac pose_feW_limbwidths_bounded feW bounds_limbwidths feW_limbwidths_bounded :=
-  internal_pose_feW_bounded feW bounds_limbwidths feW_limbwidths_bounded.
-
-Ltac internal_pose_feBW sz adjusted_bitwidth' bounds feBW :=
-  cache_term_with_type_by
-    Type
-    ltac:(let v := eval cbv [adjusted_bitwidth' bounds] in (BoundedWord sz adjusted_bitwidth' bounds) in exact v)
-           feBW.
-Ltac pose_feBW_tight sz adjusted_bitwidth' bounds_tight feBW_tight :=
-  internal_pose_feBW sz adjusted_bitwidth' bounds_tight feBW_tight.
-Ltac pose_feBW_loose sz adjusted_bitwidth' bounds_loose feBW_loose :=
-  internal_pose_feBW sz adjusted_bitwidth' bounds_loose feBW_loose.
-Ltac pose_feBW_limbwidths sz adjusted_bitwidth' bounds_limbwidths feBW_limbwidths :=
-  internal_pose_feBW sz adjusted_bitwidth' bounds_limbwidths feBW_limbwidths.
-
-Lemma relax'_pf {sz in_bounds out_bounds} {v : tuple Z sz}
-      (Htight : fieldwiseb is_tighter_than_bool in_bounds out_bounds = true)
-  : is_bounded_by None in_bounds v -> is_bounded_by None out_bounds v.
-Proof.
-  destruct sz as [|sz]; simpl in *; trivial.
-  induction sz as [|sz IHsz]; simpl in *;
-    repeat first [ exact I
-                 | progress destruct_head'_prod
-                 | progress destruct_head' zrange
-                 | progress cbv [is_tighter_than_bool] in *
-                 | progress split_andb
-                 | progress Z.ltb_to_lt
-                 | progress cbn [fst snd ZRange.lower ZRange.upper] in *
-                 | progress destruct_head_hnf' and
-                 | progress intros
-                 | apply conj
-                 | omega
-                 | solve [ eauto ] ].
-Qed.
-
-Definition relax' {sz adjusted_bitwidth'} {in_bounds out_bounds}
-           (Htight : Tuple.fieldwiseb ZRange.is_tighter_than_bool in_bounds out_bounds = true)
-  : BoundedWord sz adjusted_bitwidth' in_bounds
-    -> BoundedWord sz adjusted_bitwidth' out_bounds
-  := fun w => exist _ (proj1_sig w) (relax'_pf Htight (proj2_sig w)).
-
-Ltac internal_pose_feBW_relax sz feBW_in feBW_out feBW_relax :=
-  cache_term_with_type_by
-    (feBW_in -> feBW_out)
-    ltac:(refine (@relax' sz _ _ _ _);
-          lazymatch goal with
-          | [ |- fieldwiseb is_tighter_than_bool ?in_bounds ?out_bounds = true ]
-            => try cbv [in_bounds];
-               try cbv [out_bounds]
-          end;
-          abstract vm_cast_no_check (eq_refl true))
-           feBW_relax.
-Ltac pose_feBW_relax sz feBW_tight feBW_loose feBW_relax :=
-  internal_pose_feBW_relax sz feBW_tight feBW_loose feBW_relax.
-Ltac pose_feBW_relax_limbwidths_to_tight sz feBW_limbwidths feBW_tight feBW_relax_limbwidths_to_tight :=
-  internal_pose_feBW_relax sz feBW_limbwidths feBW_tight feBW_relax_limbwidths_to_tight.
-Ltac pose_feBW_relax_limbwidths_to_loose sz feBW_limbwidths feBW_loose feBW_relax_limbwidths_to_loose :=
-  internal_pose_feBW_relax sz feBW_limbwidths feBW_loose feBW_relax_limbwidths_to_loose.
-
-Lemma feBW_bounded_helper'
-      sz adjusted_bitwidth' bounds
-      (feBW := BoundedWord sz adjusted_bitwidth' bounds)
-      (wt : nat -> Z)
-      (Hwt : forall i, 0 <= wt i)
-  : forall (a : feBW),
-    B.Positional.eval wt (map lower bounds)
-    <= B.Positional.eval wt (BoundedWordToZ sz adjusted_bitwidth' bounds a)
-    <= B.Positional.eval wt (map upper bounds).
-Proof.
-  let a := fresh "a" in
-  intro a;
-    destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
-  destruct sz as [|sz].
-  { cbv -[Z.le Z.lt Z.mul]; lia. }
-  { cbn [tuple map] in *.
-    revert dependent wt; induction sz as [|sz IHsz]; intros.
-    { cbv -[Z.le Z.lt wordToZ Z.mul Z.pow Z.add lower upper Nat.log2 wordT] in *.
-      repeat match goal with
-             | [ |- context[@wordToZ ?n ?x] ]
-               => generalize dependent (@wordToZ n x); intros
-             | [ H : forall j, 0 <= wt j |- context[wt ?i] ]
-               => pose proof (H i); generalize dependent (wt i); intros
-             end.
-      nia. }
-    { pose proof (Hwt 0%nat).
-      cbn [tuple' map'] in *.
-      destruct a as [a' a], bounds as [bounds b], H as [H [H' _]].
-      cbn [fst snd] in *.
-      setoid_rewrite (@B.Positional.eval_step (S _)).
-      specialize (IHsz bounds a' H (fun i => wt (S i)) (fun i => Hwt _)).
-      nia. } }
-Qed.
-Lemma feBW_bounded_helper
-      sz adjusted_bitwidth' bounds
-      (feBW := BoundedWord sz adjusted_bitwidth' bounds)
-      (wt : nat -> Z)
-      (Hwt : forall i, 0 <= wt i)
-      l u
-  : l <= B.Positional.eval wt (map lower bounds)
-    /\ B.Positional.eval wt (map upper bounds) < u
-    -> forall (a : feBW),
-      l <= B.Positional.eval wt (BoundedWordToZ sz adjusted_bitwidth' bounds a) < u.
-Proof.
-  intros [Hl Hu] a; split;
-    [ eapply Z.le_trans | eapply Z.le_lt_trans ];
-    [ | eapply feBW_bounded_helper' | eapply feBW_bounded_helper' | ];
-    assumption.
-Qed.
-
-Ltac internal_pose_feBW_bounded freeze wt sz feBW adjusted_bitwidth' bounds m wt_nonneg feBW_bounded :=
-  lazymatch (eval vm_compute in freeze) with
-  | true
-    => cache_proof_with_type_by
-         (forall a : feBW, 0 <= B.Positional.eval wt (BoundedWordToZ sz adjusted_bitwidth' bounds a) < 2 * Z.pos m)
-         ltac:(apply (@feBW_bounded_helper sz adjusted_bitwidth' bounds wt wt_nonneg);
-               cbv -[Z.lt Z.le];
-               clear; vm_decide)
-                feBW_bounded
-  | false
-    => cache_term tt feBW_bounded
-  end.
-Ltac pose_feBW_tight_bounded freeze wt sz feBW_tight adjusted_bitwidth' bounds_tight m wt_nonneg feBW_tight_bounded :=
-  internal_pose_feBW_bounded freeze wt sz feBW_tight adjusted_bitwidth' bounds_tight m wt_nonneg feBW_tight_bounded.
-Ltac pose_feBW_limbwidths_bounded freeze wt sz feBW_limbwidths adjusted_bitwidth' bounds_limbwidths m wt_nonneg feBW_limbwidths_bounded :=
-  internal_pose_feBW_bounded freeze wt sz feBW_limbwidths adjusted_bitwidth' bounds_limbwidths m wt_nonneg feBW_limbwidths_bounded.
-
-Ltac pose_phiW feW m wt phiW :=
-  cache_term_with_type_by
-    (feW -> F m)
-    ltac:(exact (fun x : feW => B.Positional.Fdecode wt (Tuple.map wordToZ x)))
-           phiW.
-Ltac internal_pose_phiBW feBW m wt phiBW :=
-  cache_term_with_type_by
-    (feBW -> F m)
-    ltac:(exact (fun x : feBW => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x)))
-           phiBW.
-Ltac pose_phiBW_tight feBW_tight m wt phiBW_tight :=
-  internal_pose_phiBW feBW_tight m wt phiBW_tight.
-Ltac pose_phiBW_loose feBW_loose m wt phiBW_loose :=
-  internal_pose_phiBW feBW_loose m wt phiBW_loose.
-Ltac pose_phiBW_limbwidths feBW_limbwidths m wt phiBW_limbwidths :=
-  internal_pose_phiBW feBW_limbwidths m wt phiBW_limbwidths.