git rm -rf src/BoundedArithmetic/Double/Repeated/ (and users)

12 files changed, 0 insertions, 799 deletions

diff --git a/_CoqProject b/_CoqProject
index 952b493ac..de6c1cd42 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -28,8 +28,6 @@ src/BoundedArithmetic/Eta.v
 src/BoundedArithmetic/Interface.v
 src/BoundedArithmetic/InterfaceProofs.v
 src/BoundedArithmetic/StripCF.v
-src/BoundedArithmetic/X86ToZLike.v
-src/BoundedArithmetic/X86ToZLikeProofs.v
 src/BoundedArithmetic/Double/Core.v
 src/BoundedArithmetic/Double/Proofs/BitwiseOr.v
 src/BoundedArithmetic/Double/Proofs/Decode.v
@@ -42,15 +40,6 @@ src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v
 src/BoundedArithmetic/Double/Proofs/ShiftRight.v
 src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v
 src/BoundedArithmetic/Double/Proofs/SpreadLeftImmediate.v
-src/BoundedArithmetic/Double/Repeated/Core.v
-src/BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr.v
-src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v
-src/BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate.v
-src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v
-src/BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub.v
-src/BoundedArithmetic/Double/Repeated/Proofs/SelectConditional.v
-src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v
-src/BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate.v
 src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
 src/CompleteEdwardsCurve/EdwardsMontgomery.v
 src/CompleteEdwardsCurve/ExtendedCoordinates.v
diff --git a/src/BoundedArithmetic/Double/Repeated/Core.v b/src/BoundedArithmetic/Double/Repeated/Core.v
deleted file mode 100644
index e19b702aa..000000000
--- a/src/BoundedArithmetic/Double/Repeated/Core.v
+++ /dev/null
@@ -1,127 +0,0 @@
-(*** Implementing Large Bounded Arithmetic via pairs *)
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.ListUtil.
-Require Import Crypto.Util.Notations.
-
-Local Open Scope nat_scope.
-Local Open Scope Z_scope.
-Local Open Scope type_scope.
-
-Local Coercion Z.of_nat : nat >-> Z.
-
-Fixpoint repeated_tuple W (base : nat) (exp : nat)
-  := match exp with
-     | O => W
-     | S exp' => tuple (repeated_tuple W base exp') base
-     end.
-
-Local Arguments Z.mul !_ !_.
-Local Opaque tuple_decoder.
-
-Section decode.
-  Context {n W}
-          {decode : decoder n W}
-          {base : nat}.
-
-  Fixpoint repeated_tuple_decoder {exp : nat}
-    : decoder (base^exp * n) (repeated_tuple W base exp)
-    := {| Interface.decode
-          := match exp return repeated_tuple W base exp -> Z with
-             | O => decode
-             | S exp' => Interface.decode : tuple (repeated_tuple W base exp') base -> Z
-             end |}.
-  Global Existing Instance repeated_tuple_decoder.
-End decode.
-
-Section all.
-  Context {n W}
-          {decode : decoder n W}
-          {ldi : load_immediate W}
-          {shrd : shift_right_doubleword_immediate W}
-          {sprl : spread_left_immediate W}
-          {shl : shift_left_immediate W}
-          {shr : shift_right_immediate W}
-          {mkl : mask_keep_low W}
-          {and : bitwise_and W}
-          {or : bitwise_or W}
-          {adc : add_with_carry W}
-          {subc : sub_with_carry W}
-          {mul : multiply W}
-          {mulhwll : multiply_low_low W}
-          {mulhwhl : multiply_high_low W}
-          {mulhwhh : multiply_high_high W}
-          {muldw : multiply_double W}
-          {selc : select_conditional W}
-          {addm : add_modulo W}.
-
-  Local Notation repeated_tuple_cls cls exp
-    := (match exp%nat as exp0 return cls (repeated_tuple W 2 exp0) with
-        | O => _ : cls W
-        | S exp' => _ : cls (tuple (repeated_tuple W 2 exp') 2)
-        end) (only parsing).
-
-  Fixpoint load_immediate_repeated_double {exp : nat}
-    := repeated_tuple_cls load_immediate exp.
-  Global Existing Instance load_immediate_repeated_double.
-  Fixpoint shift_right_doubleword_immediate_repeated_double {exp : nat}
-    := repeated_tuple_cls shift_right_doubleword_immediate exp.
-  Global Existing Instance shift_right_doubleword_immediate_repeated_double.
-  (*Fixpoint spread_left_immediate_repeated_double {exp : nat}
-    := repeated_tuple_cls spread_left_immediate exp.
-  Global Existing Instance spread_left_immediate_repeated_double.*)
-  Fixpoint bitwise_or_repeated_double {exp : nat}
-    := repeated_tuple_cls bitwise_or exp.
-  Global Existing Instance bitwise_or_repeated_double.
-  Local Hint Extern 1 =>
-  match goal with
-  | [ H : forall n, (_ * _)%type |- _ ]
-    => pose proof (fun n => fst (H n));
-         pose proof (fun n => snd (H n));
-         clear H
-  end : typeclass_instances.
-  Fixpoint shlr_repeated_double {exp : nat} : (shift_left_immediate (repeated_tuple W 2 exp) * shift_right_immediate (repeated_tuple W 2 exp))%type.
-  Proof.
-    refine (repeated_tuple_cls (fun T => shift_left_immediate T * shift_right_immediate T)%type exp);
-      split; exact _.
-  Defined.
-  Global Instance shift_left_immediate_repeated_double {exp : nat} : shift_left_immediate (repeated_tuple W 2 exp)
-    := fst (@shlr_repeated_double exp).
-  Global Instance shift_right_immediate_repeated_double {exp : nat} : shift_right_immediate (repeated_tuple W 2 exp)
-    := snd (@shlr_repeated_double exp).
-  (*Fixpoint mask_keep_low_repeated_double {exp : nat}
-    := repeated_tuple_cls mask_keep_low exp.
-  Global Existing Instance mask_keep_low_repeated_double.*)
-  Fixpoint bitwise_and_repeated_double {exp : nat}
-    := repeated_tuple_cls bitwise_and exp.
-  Global Existing Instance bitwise_and_repeated_double.
-  Fixpoint add_with_carry_repeated_double {exp : nat}
-    := repeated_tuple_cls add_with_carry exp.
-  Global Existing Instance add_with_carry_repeated_double.
-  Fixpoint sub_with_carry_repeated_double {exp : nat}
-    := repeated_tuple_cls sub_with_carry exp.
-  Global Existing Instance sub_with_carry_repeated_double.
-  (*Fixpoint multiply_repeated_double {exp : nat}
-    := repeated_tuple_cls multiply exp.
-  Global Existing Instance multiply_repeated_double.*)
-  Fixpoint multiply_double_repeated_double {exp : nat}
-    := repeated_tuple_cls multiply_double exp.
-  Global Existing Instance multiply_double_repeated_double.
-  Fixpoint multiply_low_low_repeated_double {exp : nat}
-    := repeated_tuple_cls multiply_low_low exp.
-  Global Existing Instance multiply_low_low_repeated_double.
-  Fixpoint multiply_high_low_repeated_double {exp : nat}
-    := repeated_tuple_cls multiply_high_low exp.
-  Global Existing Instance multiply_high_low_repeated_double.
-  Fixpoint multiply_high_high_repeated_double {exp : nat}
-    := repeated_tuple_cls multiply_high_high exp.
-  Global Existing Instance multiply_high_high_repeated_double.
-  Fixpoint select_conditional_repeated_double {exp : nat}
-    := repeated_tuple_cls select_conditional exp.
-  Global Existing Instance select_conditional_repeated_double.
-  (*Fixpoint add_modulo_repeated_double {exp : nat}
-    := repeated_tuple_cls add_modulo exp.
-  Global Existing Instance add_modulo_repeated_double.*)
-End all.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr.v b/src/BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr.v
deleted file mode 100644
index 7996dbca5..000000000
--- a/src/BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr.v
+++ /dev/null
@@ -1,26 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.BitwiseOr.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
-Require Import Crypto.Util.ZUtil.
-
-Local Open Scope Z_scope.
-Local Arguments Z.mul !_ !_.
-Local Arguments Z.pow : simpl never.
-Local Arguments Z.of_nat : simpl never.
-Local Opaque tuple_decoder.
-
-Section bitwise_or.
-  Context {n W}
-          {decode : decoder n W}
-          {is_decode : is_decode decode}
-          {or : bitwise_or W}
-          {is_or : is_bitwise_or or}.
-
-  Fixpoint is_bitwise_or_repeated_double {exp : nat} : is_bitwise_or (bitwise_or_repeated_double (exp:=exp)).
-  Proof. is_cls_fixpoint_t decode n exp is_or (@is_bitwise_or_repeated_double). Qed.
-  Global Existing Instance is_bitwise_or_repeated_double.
-End bitwise_or.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v b/src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v
deleted file mode 100644
index 230a7d27f..000000000
--- a/src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v
+++ /dev/null
@@ -1,114 +0,0 @@
-Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.InterfaceProofs.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
-Require Import Crypto.Util.ZUtil.
-
-Local Arguments Z.mul !_ !_.
-Local Opaque tuple_decoder.
-Local Coercion Z.of_nat : nat >-> Z.
-Local Open Scope Z_scope.
-
-Fixpoint project_repeated_tuple {W base exp} : repeated_tuple W base exp -> match base, exp with
-                                                                            | S _, _ => W
-                                                                            | O, O => W
-                                                                            | O, S _ => unit
-                                                                            end
-  := match exp, base
-           return repeated_tuple W base exp -> match base, exp with
-                                               | S _, _ => W
-                                               | O, O => W
-                                               | O, S _ => unit
-                                               end
-     with
-     | O, O
-     | O, S _
-       => fun x => x
-     | S exp', S O => @project_repeated_tuple W (S O) exp'
-     | S exp', S (S base') => fun x => @project_repeated_tuple W (S (S base')) exp' (snd x)
-     | S _, O => fun _ => tt
-     end.
-
-Lemma mul_1_l_decode {W} (P : forall n, decoder n W -> Prop)
-      {n} (decode : decoder n W)
-  : P n decode -> P (1 * n) {| Interface.decode := @Interface.decode n W decode |}.
-Proof.
-  pose proof (Z.mul_1_l n).
-  set (n' := 1 * n) in *; clearbody n'.
-  induction H.
-  destruct decode.
-  exact (fun x => x).
-Qed.
-
-Section decode.
-  Context {n W}
-          {decode : decoder n W}
-          {isdecode : is_decode decode}
-          {base : nat}.
-
-  Fixpoint is_repeated_tuple_decode {exp : nat}
-    : is_decode (@repeated_tuple_decoder n W decode base exp).
-  Proof.
-    refine match exp return is_decode (repeated_tuple_decoder (exp:=exp)) with
-           | O => fun x => _
-           | S exp' => fun x => _
-           end.
-    { clear is_repeated_tuple_decode.
-      simpl; rewrite Z.mul_1_l; apply isdecode. }
-    { specialize (is_repeated_tuple_decode exp').
-      change (base^S exp') with (base^(1 + exp')%nat) at 3.
-      rewrite (Nat2Z.inj_add 1 exp'), Z.pow_add_r, Z.pow_1_r by omega.
-      simpl.
-      destruct base as [|[| base' ]]; autorewrite with simpl_tuple_decoder.
-      { simpl; omega. }
-      { apply is_repeated_tuple_decode. }
-      { assert (0 <= n) by exact (decode_exponent_nonnegative _ (project_repeated_tuple x)).
-        assert (0 <= S (S base') ^ exp' * n) by zero_bounds.
-        assert (0 <= (S base' * (S (S base') ^ exp' * n))) by zero_bounds.
-        rewrite <- Z.mul_assoc.
-        change (2 ^ (S (S base') * (S (S base') ^ exp' * n)))
-        with (2 ^ (((1 + S base')%nat) * (S (S base') ^ exp' * n))).
-        rewrite (Nat2Z.inj_add 1 (S base')), Z.mul_add_distr_r, Z.mul_1_l, Z.pow_add_r by omega.
-        autorewrite with simpl_tuple_decoder Zshift_to_pow; generalize_decode; nia. } }
-  Qed.
-  Global Existing Instance is_repeated_tuple_decode.
-End decode.
-
-Ltac is_cls_fixpoint_t_gen decode n exp generalize_is_clsv IH :=
-  let exp' := fresh exp in
-  destruct exp as [|exp'];
-  [ clear IH;
-    destruct decode; generalize_is_clsv ();
-    simpl;
-    change (Z.of_nat 2 ^ Z.of_nat 0) with 1;
-    generalize (Z.mul_1_l n); generalize (1 * n);
-    intro; clear; induction 1;
-    intros; repeat apply pair; try assumption
-  | specialize (IH exp'); revert IH;
-    repeat match goal with
-           | [ |- (_ * _)%type -> _ ]
-             => let x := fresh in
-                let y := fresh in
-                intros [x y]; revert x y
-           | [ |- _ -> _ ]
-             => intro
-           end;
-    simpl @repeated_tuple_decoder; simpl;
-    change (Z.of_nat (S exp')) with (Z.of_nat (1 + exp'));
-    rewrite (Nat2Z.inj_add 1 exp'), Z.pow_add_r, Z.pow_1_r, <- !Z.mul_assoc, <- decoder_eta by omega;
-    repeat apply pair;
-    try exact _ ].
-
-Ltac is_cls_fixpoint_t decode n exp is_clsv IH :=
-  is_cls_fixpoint_t_gen decode n exp ltac:(fun _ => generalize is_clsv) IH.
-
-Ltac is_cls_fixpoint_t2 decode n exp is_clsv1 is_clsv2 IH :=
-  is_cls_fixpoint_t_gen decode n exp ltac:(fun _ => generalize is_clsv1, is_clsv2) IH.
-
-Ltac is_cls_fixpoint_t3 decode n exp is_clsv1 is_clsv2 is_clsv3 IH :=
-  is_cls_fixpoint_t_gen decode n exp ltac:(fun _ => generalize is_clsv1, is_clsv2, is_clsv3) IH.
-
-Ltac is_cls_fixpoint_t4 decode n exp is_clsv1 is_clsv2 is_clsv3 is_clsv4 IH :=
-  is_cls_fixpoint_t_gen decode n exp ltac:(fun _ => generalize is_clsv1, is_clsv2, is_clsv3, is_clsv4) IH.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate.v b/src/BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate.v
deleted file mode 100644
index 91b0c3ce7..000000000
--- a/src/BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate.v
+++ /dev/null
@@ -1,26 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.LoadImmediate.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
-Require Import Crypto.Util.ZUtil.
-
-Local Open Scope Z_scope.
-Local Arguments Z.mul !_ !_.
-Local Arguments Z.pow : simpl never.
-Local Arguments Z.of_nat : simpl never.
-Local Opaque tuple_decoder.
-
-Section load_immediate.
-  Context {n W}
-          {decode : decoder n W}
-          {is_decode : is_decode decode}
-          {ldi : load_immediate W}
-          {is_ldi : is_load_immediate ldi}.
-
-  Fixpoint is_load_immediate_repeated_double {exp : nat} : is_load_immediate (load_immediate_repeated_double (exp:=exp)).
-  Proof. is_cls_fixpoint_t decode n exp is_ldi (@is_load_immediate_repeated_double). Qed.
-  Global Existing Instance is_load_immediate_repeated_double.
-End load_immediate.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v b/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v
deleted file mode 100644
index a00e0c891..000000000
--- a/src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v
+++ /dev/null
@@ -1,96 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.InterfaceProofs.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Multiply.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.LoadImmediate.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.RippleCarryAddSub.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.ShiftLeftRight.
-Require Import Crypto.Util.ZUtil.
-
-Local Open Scope Z_scope.
-Local Arguments Z.mul !_ !_.
-Local Arguments Z.pow : simpl never.
-Local Arguments Z.of_nat : simpl never.
-Local Opaque tuple_decoder.
-
-Section multiply_double.
-  Context {n W}
-          {decode : decoder n W}
-          {is_decode : is_decode decode}
-          {ldi : load_immediate W}
-          {isldi : is_load_immediate ldi}
-          {shl : shift_left_immediate W}
-          {isshl : is_shift_left_immediate shl}
-          {shr : shift_right_immediate W}
-          {isshr : is_shift_right_immediate shr}
-          {or : bitwise_or W}
-          {isor : is_bitwise_or or}
-          {adc : add_with_carry W}
-          {isadc : is_add_with_carry adc}
-          {muldw : multiply_double W}
-          {ismuldw : is_mul_double muldw}.
-
-  Fixpoint is_multiply_double_repeated_double {exp : nat} : is_mul_double (multiply_double_repeated_double (exp:=exp)).
-  Proof. is_cls_fixpoint_t decode n exp ismuldw (@is_multiply_double_repeated_double). Qed.
-  Global Existing Instance is_multiply_double_repeated_double.
-End multiply_double.
-
-Section multiply.
-  Context {n_over_two W}
-          {decode : decoder (2 * n_over_two) W}
-          {is_decode : is_decode decode}
-          {ldi : load_immediate W}
-          {isldi : is_load_immediate ldi}
-          {shl : shift_left_immediate W}
-          {isshl : is_shift_left_immediate shl}
-          {shr : shift_right_immediate W}
-          {isshr : is_shift_right_immediate shr}
-          {or : bitwise_or W}
-          {isor : is_bitwise_or or}
-          {adc : add_with_carry W}
-          {isadc : is_add_with_carry adc}
-          {mulhwll : multiply_low_low W}
-          {mulhwhl : multiply_high_low W}
-          {mulhwhh : multiply_high_high W}
-          {ismulhwll : is_mul_low_low n_over_two mulhwll}
-          {ismulhwhl : is_mul_high_low n_over_two mulhwhl}
-          {ismulhwhh : is_mul_high_high n_over_two mulhwhh}.
-
-  Fixpoint is_multi_multiply_repeated_double {exp : nat}
-    : (is_mul_low_low (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_low_low_repeated_double (exp:=exp))
-       * is_mul_high_low (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_high_low_repeated_double (exp:=exp))
-       * is_mul_high_high (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_high_high_repeated_double (exp:=exp)))%type.
-  Proof using Type*.
-    destruct exp as [|exp']; [ clear is_multi_multiply_repeated_double | specialize (is_multi_multiply_repeated_double exp') ].
-    { destruct decode; generalize ismulhwll, ismulhwhl, ismulhwhh.
-      simpl.
-      change (Z.of_nat 2 ^ Z.of_nat 0) with 1.
-      generalize (eq_sym (Z.mul_1_l (2 * n_over_two))); generalize (1 * (2 * n_over_two)).
-      intro; clear; induction 1.
-      generalize (eq_sym (Z.mul_1_l (n_over_two))); generalize (1 * (n_over_two)).
-      intro; clear; induction 1.
-      intros; repeat apply pair; assumption. }
-    { destruct is_multi_multiply_repeated_double as [ [ ? ? ] ? ].
-      simpl @repeated_tuple_decoder; simpl;
-        change (Z.of_nat (S exp')) with (Z.of_nat (1 + exp')).
-      rewrite (Nat2Z.inj_add 1 exp'), Z.pow_add_r, Z.pow_1_r, (*!Z.mul_assoc, <- !(Z.mul_comm 2),*) <- !Z.mul_assoc by omega.
-      rewrite <- decoder_eta by omega.
-      rewrite (Z.mul_assoc (Z.of_nat 2) (_^_) n_over_two), (Z.mul_comm (Z.of_nat 2) (_^_)), <- (Z.mul_assoc (_^_) (Z.of_nat 2) n_over_two) by omega.
-      repeat apply pair;
-        try exact _. }
-  Qed.
-
-  Global Instance is_multiply_low_low_repeated_double {exp : nat}
-    : is_mul_low_low (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_low_low_repeated_double (exp:=exp))
-    := fst (fst (@is_multi_multiply_repeated_double exp)).
-  Global Instance is_multiply_high_low_repeated_double {exp : nat}
-    : is_mul_high_low (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_high_low_repeated_double (exp:=exp))
-    := snd (fst (@is_multi_multiply_repeated_double exp)).
-  Global Instance is_multiply_high_high_repeated_double {exp : nat}
-    : is_mul_high_high (Z.of_nat 2^Z.of_nat exp * n_over_two) (multiply_high_high_repeated_double (exp:=exp))
-    := snd (@is_multi_multiply_repeated_double exp).
-End multiply.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub.v b/src/BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub.v
deleted file mode 100644
index 07bc65c84..000000000
--- a/src/BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub.v
+++ /dev/null
@@ -1,38 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.RippleCarryAddSub.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
-Require Import Crypto.Util.ZUtil.
-
-Local Open Scope Z_scope.
-Local Arguments Z.mul !_ !_.
-Local Arguments Z.pow : simpl never.
-Local Arguments Z.of_nat : simpl never.
-Local Opaque tuple_decoder.
-
-Section add_with_carry.
-  Context {n W}
-          {decode : decoder n W}
-          {is_decode : is_decode decode}
-          {adc : add_with_carry W}
-          {is_adc : is_add_with_carry adc}.
-
-  Fixpoint is_add_with_carry_repeated_double {exp : nat} : is_add_with_carry (add_with_carry_repeated_double (exp:=exp)).
-  Proof. is_cls_fixpoint_t decode n exp is_adc (@is_add_with_carry_repeated_double). Qed.
-  Global Existing Instance is_add_with_carry_repeated_double.
-End add_with_carry.
-
-Section sub_with_carry.
-  Context {n W}
-          {decode : decoder n W}
-          {is_decode : is_decode decode}
-          {subc : sub_with_carry W}
-          {is_subc : is_sub_with_carry subc}.
-
-  Fixpoint is_sub_with_carry_repeated_double {exp : nat} : is_sub_with_carry (sub_with_carry_repeated_double (exp:=exp)).
-  Proof. is_cls_fixpoint_t decode n exp is_subc (@is_sub_with_carry_repeated_double). Qed.
-  Global Existing Instance is_sub_with_carry_repeated_double.
-End sub_with_carry.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/SelectConditional.v b/src/BoundedArithmetic/Double/Repeated/Proofs/SelectConditional.v
deleted file mode 100644
index 05ff40cd3..000000000
--- a/src/BoundedArithmetic/Double/Repeated/Proofs/SelectConditional.v
+++ /dev/null
@@ -1,26 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.SelectConditional.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
-Require Import Crypto.Util.ZUtil.
-
-Local Open Scope Z_scope.
-Local Arguments Z.mul !_ !_.
-Local Arguments Z.pow : simpl never.
-Local Arguments Z.of_nat : simpl never.
-Local Opaque tuple_decoder.
-
-Section select_conditional.
-  Context {n W}
-          {decode : decoder n W}
-          {is_decode : is_decode decode}
-          {selc : select_conditional W}
-          {is_selc : is_select_conditional selc}.
-
-  Fixpoint is_select_conditional_repeated_double {exp : nat} : is_select_conditional (select_conditional_repeated_double (exp:=exp)).
-  Proof. is_cls_fixpoint_t decode n exp is_selc (@is_select_conditional_repeated_double). Qed.
-  Global Existing Instance is_select_conditional_repeated_double.
-End select_conditional.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v b/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v
deleted file mode 100644
index acda67158..000000000
--- a/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v
+++ /dev/null
@@ -1,42 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.ShiftLeft.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.ShiftRight.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.LoadImmediate.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.BitwiseOr.
-Require Import Crypto.Util.ZUtil.
-
-Local Open Scope Z_scope.
-Local Arguments Z.mul !_ !_.
-Local Arguments Z.pow : simpl never.
-Local Arguments Z.of_nat : simpl never.
-Local Opaque tuple_decoder.
-
-Section shift_left_right.
-  Context {n W}
-          {decode : decoder n W}
-          {is_decode : is_decode decode}
-          {ldi : load_immediate W}
-          {is_ldi : is_load_immediate ldi}
-          {shl : shift_left_immediate W}
-          {is_shl : is_shift_left_immediate shl}
-          {shr : shift_right_immediate W}
-          {is_shr : is_shift_right_immediate shr}
-          {or : bitwise_or W}
-          {is_or : is_bitwise_or or}.
-
-  Fixpoint is_shift_left_right_immediate_repeated_double {exp : nat}
-    : (is_shift_left_immediate (shift_left_immediate_repeated_double (exp:=exp))
-       * is_shift_right_immediate (shift_right_immediate_repeated_double (exp:=exp)))%type.
-  Proof using Type*. is_cls_fixpoint_t2 decode n exp is_shl is_shr (@is_shift_left_right_immediate_repeated_double). Qed.
-  Global Instance is_shift_left_immediate_repeated_double {exp : nat}
-    : is_shift_left_immediate (shift_left_immediate_repeated_double (exp:=exp))
-    := fst (@is_shift_left_right_immediate_repeated_double exp).
-  Global Instance is_shift_right_immediate_repeated_double {exp : nat}
-    : is_shift_right_immediate (shift_right_immediate_repeated_double (exp:=exp))
-    := snd (@is_shift_left_right_immediate_repeated_double exp).
-End shift_left_right.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate.v b/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate.v
deleted file mode 100644
index 00d41c57f..000000000
--- a/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate.v
+++ /dev/null
@@ -1,30 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.ShiftRightDoubleWordImmediate.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.LoadImmediate.
-Require Import Crypto.Util.ZUtil.
-
-Local Open Scope Z_scope.
-Local Arguments Z.mul !_ !_.
-Local Arguments Z.pow : simpl never.
-Local Arguments Z.of_nat : simpl never.
-Local Opaque tuple_decoder.
-
-Section shift_right_doubleword_immediate.
-  Context {n W}
-          {decode : decoder n W}
-          {is_decode : is_decode decode}
-          {ldi : load_immediate W}
-          {is_ldi : is_load_immediate ldi}
-          {shrd : shift_right_doubleword_immediate W}
-          {is_shrd : is_shift_right_doubleword_immediate shrd}.
-
-  Fixpoint is_shift_right_doubleword_immediate_repeated_double {exp : nat}
-    : is_shift_right_doubleword_immediate (shift_right_doubleword_immediate_repeated_double (exp:=exp)).
-  Proof. is_cls_fixpoint_t decode n exp is_shrd (@is_shift_right_doubleword_immediate_repeated_double). Qed.
-  Global Existing Instance is_shift_right_doubleword_immediate_repeated_double.
-End shift_right_doubleword_immediate.
diff --git a/src/BoundedArithmetic/X86ToZLike.v b/src/BoundedArithmetic/X86ToZLike.v
deleted file mode 100644
index 29e777c0e..000000000
--- a/src/BoundedArithmetic/X86ToZLike.v
+++ /dev/null
@@ -1,73 +0,0 @@
-(*** Implementing ℤ-Like via Architecture *)
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
-Require Import Crypto.BoundedArithmetic.StripCF.
-Require Import Crypto.ModularArithmetic.ZBounded.
-Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.LetIn.
-Import NPeano.
-
-Local Open Scope Z_scope.
-Local Coercion Z.of_nat : nat >-> Z.
-
-Section x86_gen_barrett_foundation.
-  Context (full_width : nat) (n : nat) (ops : x86.instructions n) (modulus : Z).
-  Local Notation W := (repeated_tuple x86.W 2 (Nat.log2 (full_width / n))). (* full_width-width words *)
-
-  Local Instance ZLikeOps_of_x86_gen_Factored (smaller_bound_exp : Z)
-        (ldi_modulus ldi_0 : W)
-    : ZLikeOps (2^full_width) (2^smaller_bound_exp) modulus
-    := { LargeT := tuple W 2;
-         SmallT := W;
-         modulus_digits := ldi_modulus;
-         decode_large := decode;
-         decode_small := decode;
-         Mod_SmallBound v := fst v;
-         DivBy_SmallBound v := snd v;
-         DivBy_SmallerBound v := if smaller_bound_exp =? n
-                                 then snd v
-                                 else dlet v := v in shrd (snd v) (fst v) smaller_bound_exp;
-         Mul x y := muldw x y;
-         CarryAdd x y := adc x y false;
-         CarrySubSmall x y := subc x y false;
-         ConditionalSubtract b x := let v := selc b (ldi_modulus) (ldi_0) in snd (subc x v false);
-         ConditionalSubtractModulus y := dlet y := y in
-                                         let (CF, _) := subc y ldi_modulus false in
-                                         let maybe_modulus := ldi_0 in
-                                         let maybe_modulus := selc CF maybe_modulus ldi_modulus in
-                                         let (CF, y) := subc y maybe_modulus false in
-                                         y }.
-
-  Local Instance ZLikeOps_of_x86_gen (smaller_bound_exp : Z)
-    : ZLikeOps (2^full_width) (2^smaller_bound_exp) modulus :=
-    @ZLikeOps_of_x86_gen_Factored smaller_bound_exp (ldi modulus) (ldi 0).
-End x86_gen_barrett_foundation.
-
-Section x86_64_barrett_foundation.
-  Local Notation n := 64%nat.
-  Context (ops : x86.instructions n) (modulus : Z).
-  Local Notation W := (tuple (tuple x86.W 2) 2) (* 256-bit words *).
-
-  Local Instance ZLikeOps_of_x86_64_Factored (smaller_bound_exp : Z)
-        ldi_modulus ldi_0
-    : ZLikeOps (2^256) (2^smaller_bound_exp) modulus
-    := @ZLikeOps_of_x86_gen_Factored 256 n ops modulus smaller_bound_exp ldi_modulus ldi_0.
-  Global Instance ZLikeOps_of_x86_64 (smaller_bound_exp : Z)
-    : ZLikeOps (2^256) (2^smaller_bound_exp) modulus :=
-    @ZLikeOps_of_x86_64_Factored smaller_bound_exp (ldi modulus) (ldi 0).
-End x86_64_barrett_foundation.
-Section x86_32_barrett_foundation.
-  Local Notation n := 32%nat.
-  Context (ops : x86.instructions n) (modulus : Z).
-  Local Notation W := (tuple (tuple (tuple x86.W 2) 2) 2) (* 256-bit words *).
-
-  Local Instance ZLikeOps_of_x86_32_Factored (smaller_bound_exp : Z)
-        ldi_modulus ldi_0
-    : ZLikeOps (2^256) (2^smaller_bound_exp) modulus
-    := @ZLikeOps_of_x86_gen_Factored 256 n ops modulus smaller_bound_exp ldi_modulus ldi_0.
-  Global Instance ZLikeOps_of_x86_32 (smaller_bound_exp : Z)
-    : ZLikeOps (2^256) (2^smaller_bound_exp) modulus :=
-    @ZLikeOps_of_x86_32_Factored smaller_bound_exp (ldi modulus) (ldi 0).
-End x86_32_barrett_foundation.
diff --git a/src/BoundedArithmetic/X86ToZLikeProofs.v b/src/BoundedArithmetic/X86ToZLikeProofs.v
deleted file mode 100644
index 530c91dc9..000000000
--- a/src/BoundedArithmetic/X86ToZLikeProofs.v
+++ /dev/null
@@ -1,190 +0,0 @@
-(*** Implementing ℤ-Like via x86 *)
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.InterfaceProofs.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.RippleCarryAddSub.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Multiply.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.RippleCarryAddSub.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Multiply.
-Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
-Require Import Crypto.BoundedArithmetic.StripCF.
-Require Import Crypto.BoundedArithmetic.X86ToZLike.
-Require Import Crypto.ModularArithmetic.ZBounded.
-Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.ZUtil.
-Require Import Crypto.Util.Tactics.UniquePose.
-Require Import Crypto.Util.LetIn.
-Import NPeano.
-
-Local Open Scope Z_scope.
-Local Coercion Z.of_nat : nat >-> Z.
-
-Section x86_gen_barrett_foundation.
-  Context {n_over_two : nat}.
-  Local Notation n := (2 * n_over_two)%nat.
-  Context (full_width : nat) (ops : x86.instructions n) (modulus : Z).
-  Local Notation W := (repeated_tuple x86.W 2 (Nat.log2 (full_width / n))). (* full_width-width words *)
-
-  Local Arguments Z.mul !_ !_.
-  Local Arguments BaseSystem.decode !_ !_ / .
-  Local Arguments BaseSystem.accumulate / _ _.
-  Local Arguments BaseSystem.decode' !_ !_ / .
-
-  Local Ltac introduce_t_step :=
-    match goal with
-    | [ |- forall x : bool, _ ] => intros [|]
-    | [ |- True -> _ ] => intros _
-    | [ |- _ <= _ < _ -> _ ] => intro
-    | _ => let x := fresh "x" in
-           intro x;
-           try pose proof (decode_range (fst x));
-           try pose proof (decode_range (snd x));
-           pose proof (decode_range x)
-    end.
-  Local Ltac unfolder_t :=
-    progress unfold LargeT, SmallT, modulus_digits, decode_large, decode_small, Mod_SmallBound, DivBy_SmallBound, DivBy_SmallerBound, Mul, CarryAdd, CarrySubSmall, ConditionalSubtract, ConditionalSubtractModulus, ZLikeOps_of_x86_gen_Factored, ZLikeOps_of_x86_gen in *.
-  Local Ltac saturate_context_step :=
-    match goal with
-    | _ => unique assert (0 <= 2 * n_over_two) by solve [ eauto using decode_exponent_nonnegative with typeclass_instances | omega ]
-    | _ => unique assert (0 <= n_over_two) by solve [ eauto using decode_exponent_nonnegative with typeclass_instances | omega ]
-    | _ => unique assert (0 <= 2 * (2 * n_over_two)) by (eauto using decode_exponent_nonnegative with typeclass_instances)
-    | [ H : 0 <= ?x < _ |- _ ] => unique pose proof (proj1 H); unique pose proof (proj2 H)
-    end.
-  Local Ltac pre_t :=
-    repeat first [ tauto
-                 | introduce_t_step
-                 | unfolder_t
-                 | saturate_context_step ].
-  Local Ltac post_t_step :=
-    match goal with
-    | _ => reflexivity
-    | _ => progress subst
-    | _ => progress unfold Let_In
-    | _ => progress autorewrite with zsimplify_const
-    | [ |- fst ?x = (?a <=? ?b) :> bool ]
-      => cut (((if fst x then 1 else 0) = (if a <=? b then 1 else 0))%Z);
-         [ destruct (fst x), (a <=? b); intro; congruence | ]
-    | [ H : (_ =? _) = true |- _ ] => apply Z.eqb_eq in H; subst
-    | [ H : (_ =? _) = false |- _ ] => apply Z.eqb_neq in H
-    | _ => autorewrite with push_Zpow in *; solve [ reflexivity | assumption ]
-    | _ => autorewrite with pull_Zpow in *; pull_decode; reflexivity
-    | _ => progress push_decode
-    | _ => rewrite (Z.add_comm (_ << _) _); progress pull_decode
-    | [ |- context[if ?x =? ?y then _ else _] ] => destruct (x =? y) eqn:?
-    | _ => autorewrite with Zshift_to_pow; Z.rewrite_mod_small; reflexivity
-    end.
-  Local Ltac post_t := repeat post_t_step.
-  Axiom proof_admitted : False.
-  Tactic Notation "admit" := abstract case proof_admitted.
-  Local Ltac t := admit; pre_t; post_t.
-
-  Global Instance ZLikeProperties_of_x86_gen_Factored
-         {arith : x86.arithmetic ops}
-         (ldi_modulus ldi_0 : W)
-         (Hldi_modulus : ldi_modulus = ldi modulus)
-         (Hldi_0 : ldi_0 = ldi 0)
-         (modulus_in_range : 0 <= modulus < 2^full_width)
-         (smaller_bound_exp : Z)
-         (smaller_bound_smaller : 0 <= smaller_bound_exp <= full_width)
-         (n_pos : 0 < n)
-         (full_width_pos : 0 < full_width)
-    : ZLikeProperties (@ZLikeOps_of_x86_gen_Factored full_width n ops modulus smaller_bound_exp ldi_modulus ldi_0)
-    := { large_valid v := True;
-         medium_valid v := 0 <= decode_large v < 2^full_width * 2^smaller_bound_exp;
-         small_valid v := True }.
-  Proof.
-    (* In 8.5: *)
-    (* par:t. *)
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-    { abstract t. }
-  Defined.
-
-  Global Instance ZLikeProperties_of_x86_gen
-         {arith : x86.arithmetic ops}
-         (modulus_in_range : 0 <= modulus < 2^full_width)
-         (smaller_bound_exp : Z)
-         (smaller_bound_smaller : 0 <= smaller_bound_exp <= full_width)
-         (n_pos : 0 < n)
-         (full_width_pos : 0 < full_width)
-    : ZLikeProperties (@ZLikeOps_of_x86_gen _ _ ops modulus smaller_bound_exp)
-    := ZLikeProperties_of_x86_gen_Factored _ _ eq_refl eq_refl modulus_in_range _ smaller_bound_smaller n_pos full_width_pos.
-End x86_gen_barrett_foundation.
-
-Section x86_64_barrett_foundation.
-  Local Notation n := 64%nat.
-  Context (ops : x86.instructions n) (modulus : Z).
-  Local Notation W := (tuple (tuple x86.W 2) 2) (* 256-bit words *).
-
-  Global Instance ZLikeProperties_of_x86_64_Factored
-         {arith : x86.arithmetic ops}
-         (ldi_modulus ldi_0 : W)
-         (Hldi_modulus : ldi_modulus = ldi modulus)
-         (Hldi_0 : ldi_0 = ldi 0)
-         (modulus_in_range : 0 <= modulus < 2^256)
-         (smaller_bound_exp : Z)
-         (smaller_bound_smaller : 0 <= smaller_bound_exp <= 256)
-         (n_pos : 0 < n)
-    : ZLikeProperties (@ZLikeOps_of_x86_64_Factored ops modulus smaller_bound_exp ldi_modulus ldi_0)
-    := @ZLikeProperties_of_x86_gen_Factored 32 256 _ _ arith _ _ Hldi_modulus Hldi_0 modulus_in_range _ smaller_bound_smaller n_pos _.
-  Proof. clear; simpl; abstract omega. Defined.
-  Global Instance ZLikeProperties_of_x86_64
-         {arith : x86.arithmetic ops}
-         (modulus_in_range : 0 <= modulus < 2^256)
-         (smaller_bound_exp : Z)
-         (smaller_bound_smaller : 0 <= smaller_bound_exp <= 256)
-         (n_pos : 0 < n)
-    : ZLikeProperties (@ZLikeOps_of_x86_64 ops modulus smaller_bound_exp)
-    := ZLikeProperties_of_x86_64_Factored _ _ eq_refl eq_refl modulus_in_range _ smaller_bound_smaller n_pos.
-End x86_64_barrett_foundation.
-
-Section x86_32_barrett_foundation.
-  Local Notation n := 32%nat.
-  Context (ops : x86.instructions n) (modulus : Z).
-  Local Notation W := (tuple (tuple (tuple x86.W 2) 2) 2) (* 256-bit words *).
-
-  Global Instance ZLikeProperties_of_x86_32_Factored
-         {arith : x86.arithmetic ops}
-         (ldi_modulus ldi_0 : W)
-         (Hldi_modulus : ldi_modulus = ldi modulus)
-         (Hldi_0 : ldi_0 = ldi 0)
-         (modulus_in_range : 0 <= modulus < 2^256)
-         (smaller_bound_exp : Z)
-         (smaller_bound_smaller : 0 <= smaller_bound_exp <= 256)
-         (n_pos : 0 < n)
-    : ZLikeProperties (@ZLikeOps_of_x86_32_Factored ops modulus smaller_bound_exp ldi_modulus ldi_0)
-    := @ZLikeProperties_of_x86_gen_Factored 16 256 _ _ arith _ _ Hldi_modulus Hldi_0 modulus_in_range _ smaller_bound_smaller n_pos _.
-  Proof. clear; simpl; abstract omega. Defined.
-  Global Instance ZLikeProperties_of_x86_32
-         {arith : x86.arithmetic ops}
-         (modulus_in_range : 0 <= modulus < 2^256)
-         (smaller_bound_exp : Z)
-         (smaller_bound_smaller : 0 <= smaller_bound_exp <= 256)
-         (n_pos : 0 < n)
-    : ZLikeProperties (@ZLikeOps_of_x86_32 ops modulus smaller_bound_exp)
-    := ZLikeProperties_of_x86_32_Factored _ _ eq_refl eq_refl modulus_in_range _ smaller_bound_smaller n_pos.
-End x86_32_barrett_foundation.