Merge pull request #8 from mit-plv/rsloan-pipeline-example-init

Make Pipeline.v Build on 8.4

4 files changed, 3 insertions, 933 deletions

diff --git a/src/Assembly/BoundedWord.v b/src/Assembly/BoundedWord.v
deleted file mode 100644
index 3c5684793..000000000
--- a/src/Assembly/BoundedWord.v
+++ /dev/null
@@ -1,421 +0,0 @@
-
-Require Import Bedrock.Word Bedrock.Nomega.
-Require Import NArith PArith Ndigits Compare_dec Arith.
-Require Import ProofIrrelevance.
-Require Import Ring.
-Require Import Wordize.
-
-Section BoundedWord.
-
-  Local Open Scope wordize_scope.
-
-  Context {n: nat}.
-
-  (* Word Operations *)
-
-  Definition shiftr (w: word n) (bits: nat): word n.
-    destruct (le_dec bits n).
-
-    - replace n with (bits + (n - bits)) in * by (abstract intuition).
-      refine (zext (split1 bits (n - bits) w) (n - bits)).
-
-    - exact (wzero n).
-  Defined.
-
-  Lemma shiftr_spec: forall (w : word n) (bits: nat),
-      wordToN (shiftr w bits) = N.shiftr (wordToN w) (N.of_nat bits).
-    intros; unfold shiftr; destruct (le_dec bits n).
-
-    - admit.
-
-    - replace (wordToN (wzero n)) with 0%N by admit.
-      unfold N.shiftr.
-      induction bits.
-
-      + replace (N.of_nat 0) with 0%N by intuition.
-        assert (n = 0) by intuition; clear n0; subst.
-        replace w with WO; intuition.
-
-      + induction bits; admit.
-  Qed.
-
-  Definition mask (m: nat) (w: word n): word n.
-    destruct (le_dec m n).
-
-    - replace n with (m + (n - m)) in * by (abstract intuition).
-      refine (w ^& (zext (wones m) (n - m))).
-
-    - exact w.
-  Defined.
-
-  (* Definitions of Inequality and simple bounds. *)
-
-  Lemma le_ge : forall n m, (n <= m -> m >= n)%nat.
-  Proof.
-    intros; omega.
-  Qed.
-
-  Lemma ge_le : forall n m, (n >= m -> m <= n)%nat.
-  Proof.
-    intros; omega.
-  Qed.
-
-  Ltac ge_to_le :=
-    try apply N.ge_le;
-    repeat match goal with
-           | [ H : _ |- _ ] => apply N.le_ge in H
-           end.
-
-  Ltac ge_to_le_nat :=
-    try apply le_ge;
-    repeat match goal with
-           | [ H : _ |- _ ] => apply ge_le in H
-           end.
-
-  Ltac preomega := unfold wordLeN; intros; ge_to_le; pre_nomega.
-
-  Hint Rewrite wordToN_nat Nat2N.inj_add N2Nat.inj_add Nat2N.inj_mul N2Nat.inj_mul Npow2_nat : N.
-
-  Theorem word_size_bound : forall (w: word n),
-    w <= Npow2 n - 1.
-  Proof.
-    intros; unfold wordLeN; rewrite wordToN_nat.
-
-    assert (B := wordToNat_bound w);
-      rewrite <- Npow2_nat in B;
-      apply nat_compare_lt in B.
-
-    unfold N.le; intuition;
-      rewrite N2Nat.inj_compare in H;
-      rewrite Nat2N.id in H.
-
-    apply nat_compare_lt in B.
-    apply nat_compare_gt in H.
-
-    replace (N.to_nat (Npow2 n)) with (S (N.to_nat (Npow2 n - 1))) in * by admit.
-    intuition.
-  Qed.
-
-  Theorem constant_bound_N : forall k,
-    NToWord n k <= k.
-  Proof.
-    preomega.
-    rewrite NToWord_nat.
-    destruct (le_lt_dec (pow2 n) (N.to_nat k)).
-
-    specialize (wordToNat_bound (natToWord n (N.to_nat k))); nomega.
-
-    rewrite wordToNat_natToWord_idempotent; nomega.
-  Qed.
-
-  Theorem constant_bound_nat : forall k,
-    natToWord n k <= N.of_nat k.
-  Proof.
-    preomega.
-    destruct (le_lt_dec (pow2 n) k).
-
-    specialize (wordToNat_bound (natToWord n k)); nomega.
-
-    rewrite wordToNat_natToWord_idempotent; nomega.
-  Qed.
-
-  Lemma let_bound : forall (x: word n) (f: word n -> word n) xb fb, x <= xb
-    -> (forall x', x' <= xb -> f x' <= fb)
-    -> (let k := x in f k) <= fb.
-    eauto.
-  Qed.
-
-  Theorem wplus_bound : forall (w1 w2 : word n) b1 b2,
-    w1 <= b1
-    -> w2 <= b2
-    -> w1 ^+ w2 <= b1 + b2.
-  Proof.
-    preomega.
-    destruct (le_lt_dec (pow2 n) (N.to_nat b1 + N.to_nat b2)).
-
-    specialize (wordToNat_bound (w1 ^+ w2)); nomega.
-
-    rewrite wplus_alt.
-    unfold wplusN, wordBinN.
-    rewrite wordToNat_natToWord_idempotent; nomega.
-  Qed.
-
-  Theorem wmult_bound : forall (w1 w2 : word n) b1 b2,
-    w1 <= b1
-    -> w2 <= b2
-    -> w1 ^* w2 <= b1 * b2.
-  Proof.
-    preomega.
-    destruct (le_lt_dec (pow2 n) (N.to_nat b1 * N.to_nat b2)).
-
-    specialize (wordToNat_bound (w1 ^* w2)); nomega.
-
-    rewrite wmult_alt.
-    unfold wmultN, wordBinN.
-    rewrite wordToNat_natToWord_idempotent.
-    ge_to_le_nat.
-
-    apply Mult.mult_le_compat; nomega.
-    pre_nomega.
-    apply Lt.le_lt_trans with (N.to_nat b1 * N.to_nat b2); auto.
-    apply Mult.mult_le_compat; nomega.
-  Qed.
-
-  Theorem shiftr_bound : forall (w : word n) b bits,
-    w <= b
-    -> shiftr w bits <= N.shiftr b (N.of_nat bits).
-  Proof.
-    admit.
-  Qed.
-
-  Theorem mask_bound : forall (w : word n) m,
-    mask m w <= Npow2 m - 1.
-  Proof.
-    admit.
-  Qed.
-
-  Theorem mask_update_bound : forall (w : word n) b m,
-    w <= b
-    -> mask m w <= (N.min b (Npow2 m - 1)).
-  Proof.
-    admit.
-  Qed.
-
-
-  Ltac word_bound :=
-    repeat (
-       eassumption
-       || apply wplus_bound
-       || apply wmult_bound
-       || apply mask_update_bound
-       || apply mask_bound
-       || apply shiftr_bound
-       || apply constant_bound_N
-       || apply constant_bound_nat
-       || apply word_size_bound
-      ).
-
-  Notation "$" := (natToWord _).
-
-  Lemma example1 : forall (w1 w2 w3 w4 : word n) b1 b2 b3 b4,
-    w1 <= b1
-    -> w2 <= b2
-    -> w3 <= b3
-    -> w4 <= b4
-    -> { b | w1 ^+ (w2 ^* w3) ^* w4 <= b }.    
-  Proof.
-    eexists.
-    word_bound.
-  Defined.
-
-  (* Eval simpl in fun (w1 w2 w3 w4 : word n) (b1 b2 b3 b4 : N)
-                    (H1 : w1 <= b1) (H2 : w2 <= b2) (H3 : w3 <= b3) (H4 : w4 <= b4) =>
-                  projT1 (example1 H1 H2 H3 H4). *)
-
-  Lemma example2 : forall (w1 w2 w3 w4 : word n) b1 b2 b3 b4,
-    w1 <= b1
-    -> w2 <= b2
-    -> w3 <= b3
-    -> w4 <= b4
-    -> { b | w1 ^+ (w2 ^* $7 ^* w3) ^* w4 ^+ $8 ^+ w2 <= b }.
-  Proof.
-    eexists.
-    word_bound.
-  Defined.
-
-  (*Eval simpl in fun (w1 w2 w3 w4 : word n) (b1 b2 b3 b4 : N)
-                    (H1 : w1 <= b1) (H2 : w2 <= b2) (H3 : w3 <= b3) (H4 : w4 <= b4) =>
-                  projT1 (example2 H1 H2 H3 H4). *)
-
-  Lemma example3 : forall (w1 w2 w3 w4 : word n),
-    w1 <= Npow2 3
-    -> w2 <= Npow2 4
-    -> w3 <= Npow2 8
-    -> w4 <= Npow2 16
-    -> { b | w1 ^+ (w2 ^* $7 ^* w3) ^* w4 ^+ $8 ^+ w2 <= b }.
-  Proof.
-    eexists.
-    word_bound.
-  Defined.
-
-  (* Eval simpl in fun (w1 w2 w3 w4 : word n)
-                    (H1 : w1 <= _) (H2 : w2 <= _) (H3 : w3 <= _) (H4 : w4 <= _) =>
-                  projT1 (example3 H1 H2 H3 H4). *)
-
-End BoundedWord.
-
-Section MulmodExamples.
-
-  Notation "A <= B" := (wordLeN A B) (at level 70).
-  Notation "$" := (natToWord _).
-
-  Lemma mask_wand : forall (n: nat) (x: word n) m b,
-    mask (N.to_nat m) x <= b
-    -> x ^& (@NToWord n (N.ones m)) <= b.
-  Proof.
-  Admitted.
-
-  Ltac word_bound_step :=
-    idtac; match goal with
-    | [ H: ?x <= _ |- ?x <= _] => eexact H
-    | [|- (let x := ?y in @?z x) <= ?b ] => refine (@let_bound _ y z _ b _ _); [ | intros ? ? ]
-    | [|- (let x := ?y in (?a <= ?b)) ] => change ((let x := y in a) <= b)
-    | [|- (let x := ?y in (?a <= @?b x)) ] => change ((let x := y in a) <= b y); cbv beta
-    | [|- mask _ _ <= _] => apply mask_bound
-    | [|- _ ^+ _ <= _] => apply wplus_bound
-    | [|- _ ^* _ <= _] => apply wmult_bound
-    | [|- shiftr _ _ <= _] => apply shiftr_bound
-    | [|- $ _ <= _] => apply constant_bound_nat
-    | [|- NToWord _ _ <= _] => apply constant_bound_N
-    | [|- _ <= Npow2 _ - 1] => apply word_size_bound 
-    | [|- _ ^& (@NToWord _ (N.ones _)) <= _] => apply mask_wand
-    end.
-
-  Ltac simpl_hyps :=
-    match goal with
-    | [ H: ?x <= _ |- context[?x]] =>
-      unfold Npow, Pos.pow, Npow2, N.shiftr in H;
-      simpl in H
-    | [ H: _ |- _ ] => clear H
-    | _ => idtac
-    end.
-
-  Ltac word_bound := repeat (word_bound_step; simpl_hyps).
-
-  Ltac word_bound_danger :=
-    word_bound; try eassumption; try apply word_size_bound.
- 
-  Lemma example_and : forall x : word 32,
-      wand x (NToWord 32 (N.ones 10)) <= 1023.
-    intros.
-    replace (wand x (NToWord 32 (N.ones 10))) with (mask 10 x) by admit.
-    word_bound.
-  Qed.
- 
-  Lemma example_shiftr : forall x : word 32, shiftr x 30 <= 3.
-    intros.
-    replace 3%N with (N.shiftr (Npow2 32 - 1) (N.of_nat 30)) by (simpl; intuition).
-    word_bound.
-  Qed.
-
-  Lemma example_shiftr2 : forall x : word 32, x <= 1023 -> shiftr x 5 <= 31.
-    intros.
-    replace 31%N with (N.shiftr 1023%N 5%N) by (simpl; intuition).
-    word_bound.
-  Qed.
-    
-  Variable f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 : word 32.
-  Variable g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 : word 32.
-  Hypothesis Hf0 : f0 <= 2^26.
-  Hypothesis Hf1 : f1 <= 2^25.
-  Hypothesis Hf2 : f2 <= 2^26.
-  Hypothesis Hf3 : f3 <= 2^25.
-  Hypothesis Hf4 : f4 <= 2^26.
-  Hypothesis Hf5 : f5 <= 2^25.
-  Hypothesis Hf6 : f6 <= 2^26.
-  Hypothesis Hf7 : f7 <= 2^25.
-  Hypothesis Hf8 : f8 <= 2^26.
-  Hypothesis Hf9 : f9 <= 2^25.
-  Hypothesis Hg0 : g0 <= 2^26.
-  Hypothesis Hg1 : g1 <= 2^25.
-  Hypothesis Hg2 : g2 <= 2^26.
-  Hypothesis Hg3 : g3 <= 2^25.
-  Hypothesis Hg4 : g4 <= 2^26.
-  Hypothesis Hg5 : g5 <= 2^25.
-  Hypothesis Hg6 : g6 <= 2^26.
-  Hypothesis Hg7 : g7 <= 2^25.
-
-  Hypothesis Hg8 : g8 <= 2^26.
-  Hypothesis Hg9 : g9 <= 2^25.
-    
-  Lemma example_mulmod_s_ppt : { b | f0 ^* g0  <= b}.
-    eexists.
-    word_bound.
-  Defined.
-
-  Lemma example_mulmod_s_pp :  { b | f0 ^* g0 ^+ $19 ^* (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+  f1 ^* g9 ^* $2) <= b}.
-    eexists.
-    word_bound.
-  Defined.
-
-  Lemma example_mulmod_s_pp_shiftr :
-      { b | shiftr (f0 ^* g0 ^+  $19 ^* (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+  f1 ^* g9 ^* $2)) 26 <= b}.
-    eexists.
-    word_bound.
-  Defined.
-
-  Lemma example_mulmod_u_fg1 :  { b |
-        (let y : word 32 := (* the type declarations on the let-s make type inference not take forever *)
-           (f0 ^* g0 ^+
-            $19 ^*
-            (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+
-             f1 ^* g9 ^* $2)) in
-         let y0 : word 32 :=
-           (shiftr y 26 ^+
-            (f1 ^* g0 ^+ f0 ^* g1 ^+
-             $19 ^* (f9 ^* g2 ^+ f8 ^* g3 ^+ f7 ^* g4 ^+ f6 ^* g5 ^+ f5 ^* g6 ^+ f4 ^* g7 ^+ f3 ^* g8 ^+ f2 ^* g9))) in
-         let y1 : word 32 :=
-           (shiftr y0 25 ^+
-            (f2 ^* g0 ^+ f1 ^* g1 ^* $2 ^+ f0 ^* g2 ^+
-             $19 ^* (f9 ^* g3 ^* $2 ^+ f8 ^* g4 ^+ f7 ^* g5 ^* $2 ^+ f6 ^* g6 ^+ f5 ^* g7 ^* $2 ^+ f4 ^* g8 ^+ f3 ^* g9 ^* $2))) in
-         let y2 : word 32 :=
-           (shiftr y1 26 ^+
-            (f3 ^* g0 ^+ f2 ^* g1 ^+ f1 ^* g2 ^+ f0 ^* g3 ^+
-             $19 ^* (f9 ^* g4 ^+ f8 ^* g5 ^+ f7 ^* g6 ^+ f6 ^* g7 ^+ f5 ^* g8 ^+ f4 ^* g9))) in
-         let y3 : word 32 :=
-           (shiftr y2 25 ^+
-            (f4 ^* g0 ^+ f3 ^* g1 ^* $2 ^+ f2 ^* g2 ^+ f1 ^* g3 ^* $2 ^+ f0 ^* g4 ^+
-             $19 ^* (f9 ^* g5 ^* $2 ^+ f8 ^* g6 ^+ f7 ^* g7 ^* $2 ^+ f6 ^* g8 ^+ f5 ^* g9 ^* $2))) in
-         let y4 : word 32 :=
-           (shiftr y3 26 ^+
-            (f5 ^* g0 ^+ f4 ^* g1 ^+ f3 ^* g2 ^+ f2 ^* g3 ^+ f1 ^* g4 ^+ f0 ^* g5 ^+
-             $19 ^* (f9 ^* g6 ^+ f8 ^* g7 ^+ f7 ^* g8 ^+ f6 ^* g9))) in
-         let y5 : word 32 :=
-           (shiftr y4 25 ^+
-            (f6 ^* g0 ^+ f5 ^* g1 ^* $2 ^+ f4 ^* g2 ^+ f3 ^* g3 ^* $2 ^+ f2 ^* g4 ^+ f1 ^* g5 ^* $2 ^+ f0 ^* g6 ^+
-             $19 ^* (f9 ^* g7 ^* $2 ^+ f8 ^* g8 ^+ f7 ^* g9 ^* $2))) in
-         let y6 : word 32 :=
-           (shiftr y5 26 ^+
-            (f7 ^* g0 ^+ f6 ^* g1 ^+ f5 ^* g2 ^+ f4 ^* g3 ^+ f3 ^* g4 ^+ f2 ^* g5 ^+ f1 ^* g6 ^+ f0 ^* g7 ^+
-             $19 ^* (f9 ^* g8 ^+ f8 ^* g9))) in
-         let y7 : word 32 :=
-           (shiftr y6 25 ^+
-            (f8 ^* g0 ^+ f7 ^* g1 ^* $2 ^+ f6 ^* g2 ^+ f5 ^* g3 ^* $2 ^+ f4 ^* g4 ^+ f3 ^* g5 ^* $2 ^+ f2 ^* g6 ^+ f1 ^* g7 ^* $2 ^+
-             f0 ^* g8 ^+ $19 ^* f9 ^* g9 ^* $2)) in
-         let y8 : word 32 :=
-           (shiftr y7 26 ^+
-            (f9 ^* g0 ^+ f8 ^* g1 ^+ f7 ^* g2 ^+ f6 ^* g3 ^+ f5 ^* g4 ^+ f4 ^* g5 ^+ f3 ^* g6 ^+ f2 ^* g7 ^+ f1 ^* g8 ^+
-             f0 ^* g9)) in
-         let y9 : word 32 :=
-           ($19 ^* shiftr y8 25 ^+
-            wand
-              (f0 ^* g0 ^+
-               $19 ^*
-               (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+
-                f2 ^* g8 ^+ f1 ^* g9 ^* $2)) (@NToWord 32 (N.ones 26%N))) in
-         let fg1 : word 32 := (shiftr y9 26 ^+
-          wand
-            (shiftr y 26 ^+
-             (f1 ^* g0 ^+ f0 ^* g1 ^+
-              $19 ^* (f9 ^* g2 ^+ f8 ^* g3 ^+ f7 ^* g4 ^+ f6 ^* g5 ^+ f5 ^* g6 ^+ f4 ^* g7 ^+ f3 ^* g8 ^+ f2 ^* g9)))
-            (@NToWord 32 (N.ones 26%N))) in
-         fg1) <= b }.
-  Proof.
-    eexists.
-    (* Time word_bound. *) (* <- It works, but don't do this in the build! *)
-  Abort.
-
-  Require Import ZArith.
-  Variable shiftra : forall {l}, word l -> nat -> word l. (* "arithmetic" aka "signed" bitshift *)
-  Hypothesis shiftra_spec : forall {l} (w : word l) (n:nat), wordToZ (shiftra l w n) = Z.shiftr (wordToZ w) (Z.of_nat n).
-
-  Lemma example_shiftra : forall x : word 4, shiftra 4 x 2 <= 15.
-  Abort.
-
-  Lemma example_shiftra : forall x : word 4, x <= 7 -> shiftra 4 x 2 <= 1.
-  Abort.
-
-  Lemma example_mulmod_s_pp_shiftra :
-      { b | shiftra 32 (f0 ^* g0 ^+  $19 ^* (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+  f1 ^* g9 ^* $2)) 26 <= b}.
-  Abort.
-End MulmodExamples.
diff --git a/src/Assembly/MultiBoundedWord.v b/src/Assembly/MultiBoundedWord.v
deleted file mode 100644
index add2aa1a2..000000000
--- a/src/Assembly/MultiBoundedWord.v
+++ /dev/null
@@ -1,252 +0,0 @@
-
-Require Import Bedrock.Word Bedrock.Nomega.
-Require Import NArith PArith Ndigits Compare_dec Arith.
-Require Import ProofIrrelevance Ring.
-Require Import BoundedWord.
-
-Import BoundedWord.
-
-(* Parameters of boundedness calculations *)
-Notation "A <= B" := (wordLeN A B) (at level 70).
-Notation "$" := (natToWord _).
-
-(* Hypothesis-based word-bound tactic *)
-Ltac multi_apply0 A L := pose proof (L A).
-
-Ltac multi_apply1 A L :=
-  match goal with
-  | [ H: A <= ?b |- _] => pose proof (L A b H)
-  end.
-
-Ltac multi_apply2 A B L :=
-  match goal with
-  | [ H1: A <= ?b1, H2: B <= ?b2 |- _] => pose proof (L A B b1 b2 H1 H2)
-  end.
-
-Ltac multi_recurse n T :=
-  match goal with
-  | [ H: T <= _ |- _] => idtac
-  | _ =>
-    is_var T;
-    let T' := (eval cbv delta [T] in T) in multi_recurse n T';
-    match goal with
-    | [ H : T' <= ?x |- _ ] =>
-    pose proof (H : T <= x)
-    end
-
-  | _ =>
-    match T with
-    | ?W1 ^+ ?W2 =>
-      multi_recurse n W1; multi_recurse n W2;
-      multi_apply2 W1 W2 (@wplus_bound n)
-
-    | ?W1 ^* ?W2 =>
-      multi_recurse n W1; multi_recurse n W2;
-      multi_apply2 W1 W2 (@wmult_bound n)
-
-    | mask ?m ?w =>
-      multi_recurse n w;
-      multi_apply1 w (fun b => @mask_update_bound n w b)
-
-    | mask ?m ?w =>
-      multi_recurse n w;
-      pose proof (@mask_bound n w m)
-
-    | ?x ^& (@NToWord _ (N.ones ?m)) =>
-      multi_recurse n (mask (N.to_nat m) x);
-      match goal with
-      | [ H: (mask (N.to_nat m) x) <= ?b |- _] =>
-        pose proof (@mask_wand n x m b H)
-      end
-
-    | shiftr ?w ?bits =>
-      multi_recurse n w;
-      match goal with
-      | [ H: w <= ?b |- _] =>
-        pose proof (@shiftr_bound n w b bits H)
-      end
-
-    | NToWord _ ?k => pose proof (@constant_bound_N n k)
-    | natToWord _ ?k => pose proof (@constant_bound_nat n k)
-    | ($ ?k) => pose proof (@constant_bound_nat n k)
-    | _ => pose proof (@word_size_bound n T)
-    end
-  end.
-
-Lemma unwrap_let: forall {n} (y: word n) (f: word n -> word n) (b: N),
-    (let x := y in f x) <= b <-> let x := y in (f x <= b).
-Proof. intuition. Qed.
-
-Ltac multi_bound n :=
-  match goal with
-  | [|- let A := ?B in _] =>
-    multi_recurse n B; intro; multi_bound n
-  | [|- (let A := _ in _) <= _] =>
-    apply unwrap_let; multi_bound n
-  | [|- ?W <= _ ] =>
-    multi_recurse n W
-  end.
-
-(* Examples *)
-Lemma example1 : forall {n} (w1 w2 w3 w4 : word n) b1 b2 b3 b4,
-    w1 <= b1
-    -> w2 <= b2
-    -> w3 <= b3
-    -> w4 <= b4
-    -> { b | let w5 := w2 ^* w3 in w1 ^+ w5 ^* w4 <= b }.    
-Proof.
-  eexists.
-  multi_bound n.
-  eassumption.
-Defined.
-
-Lemma example2 : forall {n} (w1 w2 w3 w4 : word n) b1 b2 b3 b4,
-    w1 <= b1
-    -> w2 <= b2
-    -> w3 <= b3
-    -> w4 <= b4
-    -> { b | (let w5 := (w2 ^* $7 ^* w3) in w1 ^+ w5 ^* w4 ^+ $8 ^+ w2) <= b }.
-Proof.
-  eexists.
-  multi_bound n.
-  eassumption.
-Defined.
-
-Lemma example3 : forall {n} (w1 w2 w3 w4 : word n),
-    w1 <= Npow2 3
-    -> w2 <= Npow2 4
-    -> w3 <= Npow2 8
-    -> w4 <= Npow2 16
-    -> { b | w1 ^+ (w2 ^* $7 ^* w3) ^* w4 ^+ $8 ^+ w2 <= b }.
-Proof.
-  eexists.
-  multi_bound n.
-  eassumption.
-Defined.
-
-Section MulmodExamples.
-
-  Notation "A <= B" := (wordLeN A B) (at level 70).
-  Notation "$" := (natToWord 32).
-
-  Lemma example_and : forall x : word 32, wand x (NToWord 32 (N.ones 10)) <= 1023.
-    intros.
-    replace (wand x (NToWord 32 (N.ones 10))) with (mask 10 x) by admit.
-    multi_bound 32; eassumption.
-  Qed.
-
-  Lemma example_shiftr : forall x : word 32, shiftr x 30 <= 3.
-    intros.
-    replace 3%N with (N.shiftr (Npow2 32 - 1) (N.of_nat 30)) by (simpl; intuition).
-    multi_bound 32; eassumption.
-  Qed.
-
-  Lemma example_shiftr2 : forall x : word 32, x <= 1023 -> shiftr x 5 <= 31.
-    intros.
-    replace 31%N with (N.shiftr 1023%N 5%N) by (simpl; intuition).
-    multi_bound 32; eassumption.
-  Qed.
-
-  Variable f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 : word 32.
-  Variable g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 : word 32.
-  Hypothesis Hf0 : f0 <= 2^26.
-  Hypothesis Hf1 : f1 <= 2^25.
-  Hypothesis Hf2 : f2 <= 2^26.
-  Hypothesis Hf3 : f3 <= 2^25.
-  Hypothesis Hf4 : f4 <= 2^26.
-  Hypothesis Hf5 : f5 <= 2^25.
-  Hypothesis Hf6 : f6 <= 2^26.
-  Hypothesis Hf7 : f7 <= 2^25.
-  Hypothesis Hf8 : f8 <= 2^26.
-  Hypothesis Hf9 : f9 <= 2^25.
-  Hypothesis Hg0 : g0 <= 2^26.
-  Hypothesis Hg1 : g1 <= 2^25.
-  Hypothesis Hg2 : g2 <= 2^26.
-  Hypothesis Hg3 : g3 <= 2^25.
-  Hypothesis Hg4 : g4 <= 2^26.
-  Hypothesis Hg5 : g5 <= 2^25.
-  Hypothesis Hg6 : g6 <= 2^26.
-  Hypothesis Hg7 : g7 <= 2^25.
-  Hypothesis Hg8 : g8 <= 2^26.
-  Hypothesis Hg9 : g9 <= 2^25.
-
-  Lemma example_mulmod_s_ppt : { b | f0 ^* g0  <= b}.
-    eexists.
-    multi_bound 32; eassumption.
-  Defined.
-
-  Lemma example_mulmod_s_pp :  { b | f0 ^* g0 ^+ $19 ^* (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+  f1 ^* g9 ^* $2) <= b}.
-    eexists.
-    multi_bound 32; eassumption.
-  Defined.
-
-  Lemma example_mulmod_s_pp_shiftr :
-    { b | shiftr (f0 ^* g0 ^+  $19 ^* (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+  f1 ^* g9 ^* $2)) 26 <= b}.
-    eexists.
-    multi_bound 32; eassumption.
-  Defined.
-
-  Lemma example_mulmod_u_fg1 :  { b |
-      (let y : word 32 := 
-        (f0 ^* g0 ^+
-            $19 ^*
-            (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+ f2 ^* g8 ^+
-            f1 ^* g9 ^* $2)) in
-        let y0 : word 32 :=
-        (shiftr y 26 ^+
-            (f1 ^* g0 ^+ f0 ^* g1 ^+
-            $19 ^* (f9 ^* g2 ^+ f8 ^* g3 ^+ f7 ^* g4 ^+ f6 ^* g5 ^+ f5 ^* g6 ^+ f4 ^* g7 ^+ f3 ^* g8 ^+ f2 ^* g9))) in
-        let y1 : word 32 :=
-        (shiftr y0 25 ^+
-            (f2 ^* g0 ^+ f1 ^* g1 ^* $2 ^+ f0 ^* g2 ^+
-            $19 ^* (f9 ^* g3 ^* $2 ^+ f8 ^* g4 ^+ f7 ^* g5 ^* $2 ^+ f6 ^* g6 ^+ f5 ^* g7 ^* $2 ^+ f4 ^* g8 ^+ f3 ^* g9 ^* $2))) in
-        let y2 : word 32 :=
-        (shiftr y1 26 ^+
-            (f3 ^* g0 ^+ f2 ^* g1 ^+ f1 ^* g2 ^+ f0 ^* g3 ^+
-            $19 ^* (f9 ^* g4 ^+ f8 ^* g5 ^+ f7 ^* g6 ^+ f6 ^* g7 ^+ f5 ^* g8 ^+ f4 ^* g9))) in
-        let y3 : word 32 :=
-        (shiftr y2 25 ^+
-            (f4 ^* g0 ^+ f3 ^* g1 ^* $2 ^+ f2 ^* g2 ^+ f1 ^* g3 ^* $2 ^+ f0 ^* g4 ^+
-            $19 ^* (f9 ^* g5 ^* $2 ^+ f8 ^* g6 ^+ f7 ^* g7 ^* $2 ^+ f6 ^* g8 ^+ f5 ^* g9 ^* $2))) in
-        let y4 : word 32 :=
-        (shiftr y3 26 ^+
-            (f5 ^* g0 ^+ f4 ^* g1 ^+ f3 ^* g2 ^+ f2 ^* g3 ^+ f1 ^* g4 ^+ f0 ^* g5 ^+
-            $19 ^* (f9 ^* g6 ^+ f8 ^* g7 ^+ f7 ^* g8 ^+ f6 ^* g9))) in
-        let y5 : word 32 :=
-        (shiftr y4 25 ^+
-            (f6 ^* g0 ^+ f5 ^* g1 ^* $2 ^+ f4 ^* g2 ^+ f3 ^* g3 ^* $2 ^+ f2 ^* g4 ^+ f1 ^* g5 ^* $2 ^+ f0 ^* g6 ^+
-            $19 ^* (f9 ^* g7 ^* $2 ^+ f8 ^* g8 ^+ f7 ^* g9 ^* $2))) in
-        let y6 : word 32 :=
-        (shiftr y5 26 ^+
-            (f7 ^* g0 ^+ f6 ^* g1 ^+ f5 ^* g2 ^+ f4 ^* g3 ^+ f3 ^* g4 ^+ f2 ^* g5 ^+ f1 ^* g6 ^+ f0 ^* g7 ^+
-            $19 ^* (f9 ^* g8 ^+ f8 ^* g9))) in
-        let y7 : word 32 :=
-        (shiftr y6 25 ^+
-            (f8 ^* g0 ^+ f7 ^* g1 ^* $2 ^+ f6 ^* g2 ^+ f5 ^* g3 ^* $2 ^+ f4 ^* g4 ^+ f3 ^* g5 ^* $2 ^+ f2 ^* g6 ^+ f1 ^* g7 ^* $2 ^+
-            f0 ^* g8 ^+ $19 ^* f9 ^* g9 ^* $2)) in
-        let y8 : word 32 :=
-        (shiftr y7 26 ^+
-            (f9 ^* g0 ^+ f8 ^* g1 ^+ f7 ^* g2 ^+ f6 ^* g3 ^+ f5 ^* g4 ^+ f4 ^* g5 ^+ f3 ^* g6 ^+ f2 ^* g7 ^+ f1 ^* g8 ^+
-            f0 ^* g9)) in
-        let y9 : word 32 :=
-        ($19 ^* shiftr y8 25 ^+
-            wand
-            (f0 ^* g0 ^+
-            $19 ^*
-            (f9 ^* g1 ^* $2 ^+ f8 ^* g2 ^+ f7 ^* g3 ^* $2 ^+ f6 ^* g4 ^+ f5 ^* g5 ^* $2 ^+ f4 ^* g6 ^+ f3 ^* g7 ^* $2 ^+
-                f2 ^* g8 ^+ f1 ^* g9 ^* $2)) (@NToWord 32 (N.ones 26%N))) in
-        let fg1 : word 32 := (shiftr y9 26 ^+
-        wand
-            (shiftr y 26 ^+
-            (f1 ^* g0 ^+ f0 ^* g1 ^+
-            $19 ^* (f9 ^* g2 ^+ f8 ^* g3 ^+ f7 ^* g4 ^+ f6 ^* g5 ^+ f5 ^* g6 ^+ f4 ^* g7 ^+ f3 ^* g8 ^+ f2 ^* g9)))
-            (@NToWord 32 (N.ones 26%N))) in
-        fg1) <= b }.
-  Proof.
-    eexists; multi_bound 32; eassumption.
-
-  Defined.
-
-  Eval simpl in (proj1_sig example_mulmod_u_fg1).
-
-End MulmodExamples.
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
index ceb98a3a2..8e58e7345 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -27,6 +27,7 @@ Module PipelineExamples.
   Local Notation "v [[ i ]]" := (nth i v (wzero _)) (at level 40).
   Local Notation "$$ v" := (natToWord _ v) (at level 40).
 
+  (*
   Definition add_example: @pseudeq 32 W32 1 1 (fun v =>
       plet a := $$ 1 in
       plet b := v[[0]] in
@@ -68,9 +69,10 @@ Module PipelineExamples.
       plet b := v[[0]] in
       ([b ^& a; a ^+ b])).
     pseudo_solve.
-  Admitted. (* TODO (rsloan): eapply unification *)
+  Admitted.
 
   Definition comb_ex_str :=
     (Pipeline.toString (proj1_sig comb_example)).
+  *)
 
 End PipelineExamples.
diff --git a/src/Galois/GaloisField.v b/src/Galois/GaloisField.v
deleted file mode 100644
index 73eb17549..000000000
--- a/src/Galois/GaloisField.v
+++ /dev/null
@@ -1,259 +0,0 @@
-Require Import BinInt BinNat ZArith Znumtheory.
-Require Import BoolEq Field_theory.
-Require Export Crypto.Galois.Galois Crypto.Galois.GaloisTheory.
-Require Import Crypto.Tactics.VerdiTactics.
-
-(* This file is for the actual field tactics and some specialized
- * morphisms that help field operate.
- *
- * When you want a Galois Field, this is the /only module/ you
- * should import, because it automatically pulls in everything
- * from Galois and the Modulus.
- *)
-Module GaloisField (M: Modulus).
-  Module G := Galois M.
-  Module T := GaloisTheory M.
-  Export M G T.
-
-  (* Define a "ring morphism" between GF and Z, i.e. an equivalence
-   * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'.
-   *
-   * Doing this allows us to do our coefficient manipulations in Z
-   * rather than GF, because we know it's equivalent to inject the
-   * result afterward.
-   *)
-  Lemma GFring_morph:
-      ring_morph GFzero GFone GFplus GFmult GFminus GFopp eq
-                 0%Z    1%Z   Zplus  Zmult  Zminus  Zopp  Zeq_bool
-                 inject.
-  Proof.
-    constructor; intros; try galois;
-      try (apply gf_eq; simpl; intuition).
-
-    apply Zmod_small; destruct modulus; simpl;
-      apply prime_ge_2 in p; intuition.
-
-    replace (- (x mod modulus)) with (0 - (x mod modulus));
-      try rewrite Zminus_mod_idemp_r; trivial.
-
-    replace x with y; intuition.
-      symmetry; apply Zeq_bool_eq; trivial.
-  Qed.
-
-  (* Redefine our division theory under the ring morphism *)
-  Lemma GFmorph_div_theory: 
-      div_theory eq Zplus Zmult inject Z.quotrem.
-  Proof.
-    constructor; intros; intuition.
-    replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b);
-      try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
-
-    eq_remove_proofs; demod;
-      rewrite <- (Z.quot_rem' a b);
-      destruct a; simpl; trivial.
-  Qed.
-
-  (* Some simple utility lemmas *)
-  Lemma injectZeroIsGFZero :
-    GFzero = inject 0.
-  Proof.
-    apply gf_eq; simpl; trivial.
-  Qed.
-
-  Lemma injectOneIsGFOne :
-    GFone = inject 1.
-  Proof.
-    apply gf_eq; simpl; intuition.
-    symmetry; apply Zmod_small; destruct modulus; simpl;
-      apply prime_ge_2 in p; intuition.
-  Qed.
-
-  Lemma divOneIsX :
-    forall (x: GF), (x / 1)%GF = x.
-  Proof.
-    intros; unfold GFdiv.
-
-    replace (GFinv 1)%GF with 1%GF by (
-      replace (GFinv 1)%GF with (GFinv 1 * 1)%GF by ring;
-      rewrite GF_multiplicative_inverse; intuition).
-
-    ring.
-  Qed.
-
-  Lemma exist_neq: forall A (P: A -> Prop) x y Px Py, x <> y -> exist P x Px <> exist P y Py.
-  Proof.
-    intuition; solve_by_inversion.
-  Qed.
-
-  (* Change all GFones to (inject 1) and GFzeros to (inject 0) so that
-   * we can use our ring morphism to simplify them
-   *)
-  Ltac GFpreprocess :=
-    repeat rewrite injectZeroIsGFZero;
-    repeat rewrite injectOneIsGFOne.
-
-  (* Split up the equation (because field likes /\, then
-   * change back all of our GFones and GFzeros.
-   *
-   * TODO (adamc): what causes it to generate these subproofs?
-   *)
-  Ltac GFpostprocess :=
-    repeat split;
-
-    repeat match goal with
-    | [ |- context[exist ?a ?b (inject_subproof ?x)] ] =>
-      replace (exist a b (inject_subproof x)) with (inject x%Z) by reflexivity
-    end;
-
-    repeat rewrite <- injectZeroIsGFZero;
-    repeat rewrite <- injectOneIsGFOne;
-    repeat rewrite divOneIsX.
-
-  (* Tactic to passively convert from GF to Z in special circumstances *)
-  Ltac GFconstant t :=
-    match t with
-    | inject ?x => x
-    | _ => NotConstant
-    end.
-
-  (* Add our ring with all the fixin's *)
-  Add Ring GFring_Z : GFring_theory
-    (morphism GFring_morph,
-     constants [GFconstant],
-     div GFmorph_div_theory,
-     power_tac GFpower_theory [GFexp_tac]). 
-
-  (* Add our field with all the fixin's *)
-  Add Field GFfield_Z : GFfield_theory
-    (morphism GFring_morph,
-     preprocess [GFpreprocess],
-     postprocess [GFpostprocess],
-     constants [GFconstant],
-     div GFmorph_div_theory,
-     power_tac GFpower_theory [GFexp_tac]). 
-
-  Local Open Scope GF_scope.
-
-  Lemma GF_mul_eq : forall x y z, z <> 0 -> x * z = y * z -> x = y.
-  Proof.
-    intros ? ? ? z_nonzero mul_z_eq.
-    replace x with (x * 1) by field.
-    rewrite <- (GF_multiplicative_inverse z_nonzero).
-    replace (x * (GFinv z * z)) with ((x * z) * GFinv z) by ring.
-    rewrite mul_z_eq.
-    replace (y * z * GFinv z) with (y * (GFinv z * z)) by ring.
-    rewrite GF_multiplicative_inverse; auto; field.
-  Qed.
-
-  Lemma GF_mul_0_l : forall x, 0 * x = 0.
-  Proof.
-    intros; field.
-  Qed.
-
-  Lemma GF_mul_0_r : forall x, x * 0 = 0.
-  Proof.
-    intros; field.
-  Qed.
-
-  Definition GF_eq_dec : forall x y : GF, {x = y} + {x <> y}.
-    intros.
-    assert (H := Z.eq_dec (inject x) (inject y)).
-
-    destruct H.
-    
-    - left; galois; intuition.
-
-    - right; intuition.
-      rewrite H in n.
-      assert (y = y); intuition.
-  Qed.
-
-    Lemma mul_nonzero_l : forall a b, a*b <> 0 -> a <> 0.
-    intros; intuition; subst.
-    assert (0 * b = 0) by field; intuition.
-  Qed.
-
-  Lemma mul_nonzero_r : forall a b, a*b <> 0 -> b <> 0.
-    intros; intuition; subst.
-    assert (a * 0 = 0) by field; intuition.
-  Qed.
-
-  Lemma mul_zero_why : forall a b, a*b = 0 -> a = 0 \/ b = 0.
-    intros.
-    assert (Z := GF_eq_dec a 0); destruct Z.
-
-    - left; intuition.
-
-    - assert (a * b / a = 0) by
-        ( rewrite H; field; intuition ).
-
-      field_simplify in H0.
-      replace (b/1) with b in H0 by (field; intuition).
-      right; intuition.
-      apply n in H0; intuition.
-  Qed.
-
-  Lemma mul_nonzero_nonzero : forall a b, a <> 0 -> b <> 0 -> a*b <> 0.
-    intros; intuition; subst.
-    apply mul_zero_why in H1.
-    destruct H1; subst; intuition.
-  Qed.
-  Hint Resolve mul_nonzero_nonzero.
-
-  Lemma GFexp_distr_mul : forall x y z, (0 <= z)%N ->
-    (x ^ z) * (y ^ z) = (x * y) ^ z.
-  Proof.
-    intros.
-    replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id.
-    apply natlike_ind with (x := Z.of_N z); simpl; [ field | | 
-      replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto].
-    intros z' z'_nonneg IHz'.
-    rewrite Z2N.inj_succ by auto.
-    rewrite (GFexp_pred x) by apply N.neq_succ_0.
-    rewrite (GFexp_pred y) by apply N.neq_succ_0.
-    rewrite (GFexp_pred (x * y)) by apply N.neq_succ_0.
-    rewrite N.pred_succ.
-    rewrite <- IHz'.
-    field.
-  Qed.
-
-  Lemma GF_square_mul : forall x y z, (y <> 0) ->
-    x ^ 2 = z * y ^ 2 -> exists sqrt_z, sqrt_z ^ 2 = z.
-  Proof.
-    intros ? ? ? y_nonzero A.
-    exists (x / y).
-    assert ((x / y) ^ 2 = x ^ 2 / y ^ 2) as square_distr_div. {
-      unfold GFdiv, GFexp, GFexp'.
-      replace (GFinv (y * y)) with (GFinv y * GFinv y); try ring.
-      unfold GFinv.
-      destruct (N.eq_dec (N.pred (totientToN totient)) 0) as [ eq_zero | neq_zero ];
-        [ rewrite eq_zero | rewrite GFexp_distr_mul ]; try field.
-      simpl.
-      do 2 rewrite <- Z2N.inj_pred.
-      replace 0%N with (Z.to_N 0%Z) by auto.
-      apply Z2N.inj_le; modulus_bound.
-    }
-    assert (y ^ 2 <> 0) as y2_nonzero by (apply mul_nonzero_nonzero; auto).
-    rewrite (GF_mul_eq _ z (y ^ 2)); auto.
-    unfold GFdiv.
-    rewrite <- A.
-    field; auto.
-  Qed.
-
-  Lemma sqrt_solutions : forall x y, y ^ 2 = x ^ 2 -> y = x \/ y = GFopp x.
-  Proof.
-    intros.
-    (* TODO(jadep) *)
-  Admitted.
-
-  Lemma GFopp_swap : forall x y, GFopp x = y <-> x = GFopp y.
-  Proof.
-    split; intro; subst; field.
-  Qed.
-
-  Lemma GFopp_involutive : forall x, GFopp (GFopp x) = x.
-  Proof.
-    intros; field.
-  Qed.
-
-End GaloisField.