diff --git a/_CoqProject b/_CoqProject
index 865816f9b4..52305feaa3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -370,6 +370,7 @@ src/Util/Structures/Orders/Sum.v
 src/Util/Tactics/AllInstances.v
 src/Util/Tactics/AllSuccesses.v
 src/Util/Tactics/AppendUnderscores.v
+src/Util/Tactics/Beta1.v
 src/Util/Tactics/BreakMatch.v
 src/Util/Tactics/CPSId.v
 src/Util/Tactics/CacheTerm.v
@@ -383,6 +384,7 @@ src/Util/Tactics/Contains.v
 src/Util/Tactics/ConvoyDestruct.v
 src/Util/Tactics/CountBinders.v
 src/Util/Tactics/DebugPrint.v
+src/Util/Tactics/Delta1.v
 src/Util/Tactics/DestructHead.v
 src/Util/Tactics/DestructHyps.v
 src/Util/Tactics/DestructTrivial.v
@@ -393,9 +395,11 @@ src/Util/Tactics/EvarExists.v
 src/Util/Tactics/EvarNormalize.v
 src/Util/Tactics/FindHyp.v
 src/Util/Tactics/Forward.v
+src/Util/Tactics/GeneralizeOverHoles.v
 src/Util/Tactics/GetGoal.v
 src/Util/Tactics/HasBody.v
 src/Util/Tactics/Head.v
+src/Util/Tactics/HeadConstrEq.v
 src/Util/Tactics/HeadUnderBinders.v
 src/Util/Tactics/MoveLetIn.v
 src/Util/Tactics/NormalizeCommutativeIdentifier.v
@@ -415,6 +419,7 @@ src/Util/Tactics/SimplifyProjections.v
 src/Util/Tactics/SimplifyRepeatedIfs.v
 src/Util/Tactics/SpecializeAllWays.v
 src/Util/Tactics/SpecializeBy.v
+src/Util/Tactics/SpecializeUnderBindersBy.v
 src/Util/Tactics/SplitInContext.v
 src/Util/Tactics/SubstEvars.v
 src/Util/Tactics/SubstLet.v
@@ -425,6 +430,7 @@ src/Util/Tactics/UnifyAbstractReflexivity.v
 src/Util/Tactics/UniquePose.v
 src/Util/Tactics/VM.v
 src/Util/Tactics/WarnIfGoalsRemain.v
+src/Util/Tactics/Zeta1.v
 src/Util/Telescope/Core.v
 src/Util/Telescope/Equality.v
 src/Util/Telescope/Instances.v
diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v
index 295d935a05..1adc34dc8d 100644
--- a/src/Assembly/Symbolic.v
+++ b/src/Assembly/Symbolic.v
@@ -2300,6 +2300,9 @@ Definition Address {sa : AddressSize} (a : MEM) : M idx :=
   bi <- App (add sa, [base; index]);
   App (add sa, [bi; offset]).
 
+Definition mem_of_reg (r : REG) : MEM :=
+  {| mem_is_byte := false ; mem_base_reg := Some r ; mem_offset := None ; mem_scale_reg := None |}.
+
 Definition Load {s : OperationSize} {sa : AddressSize} (a : MEM) : M idx :=
   if negb (orb (Syntax.operand_size a s =? 8 )( Syntax.operand_size a s =? 64))%N
   then err (error.unsupported_memory_access_size (Syntax.operand_size a s)) else
diff --git a/src/Assembly/Syntax.v b/src/Assembly/Syntax.v
index f3375f666d..0e0322d521 100644
--- a/src/Assembly/Syntax.v
+++ b/src/Assembly/Syntax.v
@@ -2,6 +2,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.NArith.NArith.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
+Require Import Coq.derive.Derive.
+Require Import Crypto.Util.Option.
 Require Crypto.Util.Tuple.
 Require Crypto.Util.OptionList.
 Import ListNotations.
@@ -231,6 +233,27 @@ Definition reg_offset (r : REG) : N :=
 Definition index_and_shift_and_bitcount_of_reg (r : REG) :=
   (reg_index r, reg_offset r, reg_size r).
 
+Definition regs_of_index (index : nat) : list (list REG) :=
+  match index with
+  |  0 => [ [  al ; ah] ; [  ax] ; [ eax] ; [rax] ]
+  |  1 => [ [  cl ; ch] ; [  cx] ; [ ecx] ; [rcx] ]
+  |  2 => [ [  dl ; dh] ; [  dx] ; [ edx] ; [rdx] ]
+  |  3 => [ [  bl ; bh] ; [  bx] ; [ ebx] ; [rbx] ]
+  |  4 => [ [ spl     ] ; [  sp] ; [ esp] ; [rsp] ]
+  |  5 => [ [ bpl     ] ; [  bp] ; [ ebp] ; [rbp] ]
+  |  6 => [ [ sil     ] ; [  si] ; [ esi] ; [rsi] ]
+  |  7 => [ [ dil     ] ; [  di] ; [ edi] ; [rdi] ]
+  |  8 => [ [ r8b     ] ; [ r8w] ; [ r8d] ; [r8 ] ]
+  |  9 => [ [ r9b     ] ; [ r9w] ; [ r9d] ; [r9 ] ]
+  | 10 => [ [r10b     ] ; [r10w] ; [r10d] ; [r10] ]
+  | 11 => [ [r11b     ] ; [r11w] ; [r11d] ; [r11] ]
+  | 12 => [ [r12b     ] ; [r12w] ; [r12d] ; [r12] ]
+  | 13 => [ [r13b     ] ; [r13w] ; [r13d] ; [r13] ]
+  | 14 => [ [r14b     ] ; [r14w] ; [r14d] ; [r14] ]
+  | 15 => [ [r15b     ] ; [r15w] ; [r15d] ; [r15] ]
+  | _  => []
+  end.
+
 (** convenience printing function *)
 Definition widest_register_of_index (n : nat) : REG
   := match n with
@@ -252,6 +275,22 @@ Definition widest_register_of_index (n : nat) : REG
      | 15 => r15
      | _ => rax
      end%nat.
+
+Definition reg_of_index_and_shift_and_bitcount_opt :=
+  fun '(index, offset, size) =>
+    let sz := N.log2 (size / 8) in
+    let offset_n := (offset / 8)%N in
+    if ((8 * 2^sz =? size) && (offset =? offset_n * 8))%N%bool
+    then (rs <- nth_error (regs_of_index index) (N.to_nat sz);
+          nth_error rs (N.to_nat offset_n))%option
+    else None.
+Definition reg_of_index_and_shift_and_bitcount :=
+  fun '(index, offset, size) =>
+    match reg_of_index_and_shift_and_bitcount_opt (index, offset, size) with
+    | Some r => r
+    | None => widest_register_of_index index
+    end.
+
 Lemma widest_register_of_index_correct
   : forall n,
     (~exists r, reg_index r = n)
@@ -267,3 +306,44 @@ Proof.
   all: try (left; reflexivity).
   all: try (right; vm_compute; reflexivity).
 Qed.
+
+Lemma reg_of_index_and_shift_and_bitcount_opt_correct v r
+  : reg_of_index_and_shift_and_bitcount_opt v = Some r <-> index_and_shift_and_bitcount_of_reg r = v.
+Proof.
+  split; [ | intro; subst; destruct r; vm_compute; reflexivity ].
+  cbv [index_and_shift_and_bitcount_of_reg]; destruct v as [ [index shift] bitcount ].
+  cbv [reg_of_index_and_shift_and_bitcount_opt].
+  generalize (shift / 8)%N (N.log2 (bitcount / 8)); intros *.
+  repeat first [ congruence
+               | progress subst
+               | match goal with
+                 | [ H : _ /\ _ |- _ ] => destruct H
+                 | [ H : N.to_nat _ = _ |- _ ] => apply (f_equal N.of_nat) in H; rewrite N2Nat.id in H; subst
+                 | [ |- Some _ = Some _ -> _ ] => inversion 1; subst
+                 | [ |- context[match ?x with _ => _ end] ] => destruct x eqn:?; subst
+                 end
+               | progress cbv [regs_of_index]
+               | match goal with
+                 | [ |- context[nth_error _ ?n] ] => destruct n eqn:?; cbn [nth_error Option.bind]
+                 end
+               | rewrite Bool.andb_true_iff, ?N.eqb_eq in * |- ].
+  all: vm_compute; reflexivity.
+Qed.
+
+Lemma reg_of_index_and_shift_and_bitcount_of_reg r
+  : reg_of_index_and_shift_and_bitcount (index_and_shift_and_bitcount_of_reg r) = r.
+Proof. destruct r; vm_compute; reflexivity. Qed.
+
+Lemma reg_of_index_and_shift_and_bitcount_eq v r
+  : reg_of_index_and_shift_and_bitcount v = r
+    -> (index_and_shift_and_bitcount_of_reg r = v
+        \/ ((~exists r, index_and_shift_and_bitcount_of_reg r = v)
+            /\ r = widest_register_of_index (fst (fst v)))).
+Proof.
+  cbv [reg_of_index_and_shift_and_bitcount].
+  destruct v as [ [index offset] size ].
+  destruct reg_of_index_and_shift_and_bitcount_opt eqn:H;
+    [ left | right; split; [ intros [r' H'] | ] ]; subst; try reflexivity.
+  { rewrite reg_of_index_and_shift_and_bitcount_opt_correct in H; assumption. }
+  { rewrite <- reg_of_index_and_shift_and_bitcount_opt_correct in H'; congruence. }
+Qed.
diff --git a/src/Util/Strings/Parse/Common.v b/src/Util/Strings/Parse/Common.v
index 7dbd553deb..bc22bdf40d 100644
--- a/src/Util/Strings/Parse/Common.v
+++ b/src/Util/Strings/Parse/Common.v
@@ -65,6 +65,15 @@ Definition parse_ascii (prefix : ascii) : ParserAction ascii
 
 Coercion parse_ascii : ascii >-> ParserAction.
 
+Definition parse_ascii_case_insensitive (prefix : ascii) : ParserAction ascii
+  := fun s
+     => match s with
+        | EmptyString => []
+        | String ch s' => if (Ascii.to_lower ch =? Ascii.to_lower prefix)%char
+                          then [(ch, s')]
+                          else []
+        end.
+
 Definition parse_str (prefix : string) : ParserAction string
   := fun s
      => if startswith prefix s
@@ -73,6 +82,16 @@ Definition parse_str (prefix : string) : ParserAction string
 
 Coercion parse_str : string >-> ParserAction.
 
+Definition parse_str_case_insensitive (prefix : string) : ParserAction string
+  := fun s
+     => let '(s1, s2) := (substring 0 (String.length prefix) s,
+                           substring (String.length prefix) (String.length s) s) in
+        if (String.to_lower prefix =? String.to_lower s1)%string
+        then [(s1, s2)]
+        else [].
+
+Notation casefold := parse_str_case_insensitive (only parsing).
+
 Definition parse_map {A B} (f : A -> B) : ParserAction A -> ParserAction B
   := fun p s
      => List.map (fun '(v, s) => (f v, s)) (p s).
@@ -145,6 +164,11 @@ Definition parse_alt_list {T} (ls : list (ParserAction T)) : ParserAction T
 Definition parse_strs {T} (ls : list (string * T)) : ParserAction T
   := parse_alt_list (List.map (fun '(s, v) => parse_map (fun _ => v) (s:string)) ls).
 
+Definition parse_strs_case_insensitive {T} (ls : list (string * T)) : ParserAction T
+  := parse_alt_list (List.map (fun '(s, v) => parse_map (fun _ => v) (casefold s)) ls).
+
+Notation parse_strs_casefold := parse_strs_case_insensitive (only parsing).
+
 Definition parse_one_whitespace : ParserAction string
   := Eval cbv [List.fold_right List.fold_left whitespace whitespace_strs List.tl List.hd parse_strs List.combine] in
       (List.fold_left (B:=string) parse_alt (tl whitespace_strs) (hd " " whitespace_strs)).
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 7af926f1df..0d9f98c378 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -3,6 +3,7 @@ Require Export Crypto.Util.FixCoqMistakes.
 Require Export Crypto.Util.Tactics.AllInstances.
 Require Export Crypto.Util.Tactics.AllSuccesses.
 Require Export Crypto.Util.Tactics.AppendUnderscores.
+Require Export Crypto.Util.Tactics.Beta1.
 Require Export Crypto.Util.Tactics.BreakMatch.
 Require Export Crypto.Util.Tactics.CPSId.
 Require Export Crypto.Util.Tactics.CacheTerm.
@@ -16,6 +17,7 @@ Require Export Crypto.Util.Tactics.Contains.
 Require Export Crypto.Util.Tactics.ConvoyDestruct.
 Require Export Crypto.Util.Tactics.CountBinders.
 Require Export Crypto.Util.Tactics.DebugPrint.
+Require Export Crypto.Util.Tactics.Delta1.
 Require Export Crypto.Util.Tactics.DestructHead.
 Require Export Crypto.Util.Tactics.DestructHyps.
 Require Export Crypto.Util.Tactics.DestructTrivial.
@@ -26,9 +28,11 @@ Require Export Crypto.Util.Tactics.EvarExists.
 Require Export Crypto.Util.Tactics.EvarNormalize.
 Require Export Crypto.Util.Tactics.FindHyp.
 Require Export Crypto.Util.Tactics.Forward.
+Require Export Crypto.Util.Tactics.GeneralizeOverHoles.
 Require Export Crypto.Util.Tactics.GetGoal.
 Require Export Crypto.Util.Tactics.HasBody.
 Require Export Crypto.Util.Tactics.Head.
+Require Export Crypto.Util.Tactics.HeadConstrEq.
 Require Export Crypto.Util.Tactics.HeadUnderBinders.
 Require Export Crypto.Util.Tactics.MoveLetIn.
 Require Export Crypto.Util.Tactics.NormalizeCommutativeIdentifier.
@@ -48,6 +52,7 @@ Require Export Crypto.Util.Tactics.SimplifyProjections.
 Require Export Crypto.Util.Tactics.SimplifyRepeatedIfs.
 Require Export Crypto.Util.Tactics.SpecializeAllWays.
 Require Export Crypto.Util.Tactics.SpecializeBy.
+Require Export Crypto.Util.Tactics.SpecializeUnderBindersBy.
 Require Export Crypto.Util.Tactics.SplitInContext.
 Require Export Crypto.Util.Tactics.SubstEvars.
 Require Export Crypto.Util.Tactics.SubstLet.
@@ -58,3 +63,4 @@ Require Export Crypto.Util.Tactics.UnifyAbstractReflexivity.
 Require Export Crypto.Util.Tactics.UniquePose.
 Require Export Crypto.Util.Tactics.VM.
 Require Export Crypto.Util.Tactics.WarnIfGoalsRemain.
+Require Export Crypto.Util.Tactics.Zeta1.
diff --git a/src/Util/Tactics/Beta1.v b/src/Util/Tactics/Beta1.v
new file mode 100644
index 0000000000..746bc04a1f
--- /dev/null
+++ b/src/Util/Tactics/Beta1.v
@@ -0,0 +1,6 @@
+Require Export Crypto.Util.Notations.
+
+Ltac beta1 x :=
+  lazymatch x with
+  | (fun a => ?f) ?b => constr:(subst_let a := b in f)
+  end.
diff --git a/src/Util/Tactics/Delta1.v b/src/Util/Tactics/Delta1.v
new file mode 100644
index 0000000000..7dbf180114
--- /dev/null
+++ b/src/Util/Tactics/Delta1.v
@@ -0,0 +1,4 @@
+Require Export Crypto.Util.FixCoqMistakes.
+
+Ltac delta1 x :=
+  eval cbv delta [x] in x.
diff --git a/src/Util/Tactics/GeneralizeOverHoles.v b/src/Util/Tactics/GeneralizeOverHoles.v
new file mode 100644
index 0000000000..5112b4df34
--- /dev/null
+++ b/src/Util/Tactics/GeneralizeOverHoles.v
@@ -0,0 +1,8 @@
+Require Export Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Tactics.Zeta1.
+Require Import Coq.ssr.ssreflect.
+
+Ltac generalize_over_holes tac :=
+  zeta1 (ltac:(let H := fresh in
+               (pose H := ltac:(let v := tac () in refine v));
+               exact H)).
diff --git a/src/Util/Tactics/HeadConstrEq.v b/src/Util/Tactics/HeadConstrEq.v
new file mode 100644
index 0000000000..d91e1bdcd4
--- /dev/null
+++ b/src/Util/Tactics/HeadConstrEq.v
@@ -0,0 +1,16 @@
+Require Import Crypto.Util.Tactics.Head.
+
+Ltac head_constr_eq T1 T2 :=
+  let h1 := head T1 in
+  let h2 := head T2 in
+  constr_eq h1 h2.
+
+Ltac head_constr_eq_nounivs T1 T2 :=
+  let h1 := head T1 in
+  let h2 := head T2 in
+  constr_eq_nounivs h1 h2.
+
+Ltac head_constr_eq_strict T1 T2 :=
+  let h1 := head T1 in
+  let h2 := head T2 in
+  constr_eq_strict h1 h2.
diff --git a/src/Util/Tactics/SpecializeUnderBindersBy.v b/src/Util/Tactics/SpecializeUnderBindersBy.v
new file mode 100644
index 0000000000..700921fe01
--- /dev/null
+++ b/src/Util/Tactics/SpecializeUnderBindersBy.v
@@ -0,0 +1,74 @@
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.GeneralizeOverHoles.
+
+Ltac guarded_specialize_term_under_binders_by' guard_tac H tac :=
+  lazymatch type of H with
+  | forall a, _
+    => match goal with
+       | _ => let __ := lazymatch goal with _ => guard_tac H end in
+              open_constr:(H ltac:(progress tac))
+       | _ => let H := open_constr:(H _) in
+              guarded_specialize_term_under_binders_by' guard_tac H tac
+       end
+  end.
+
+Ltac guarded_specialize_term_under_binders_by guard_tac H tac :=
+  generalize_over_holes ltac:(fun _ => guarded_specialize_term_under_binders_by' guard_tac H tac).
+
+Ltac guarded_specialize_hyp_under_binders_by guard_tac H tac :=
+  idtac;
+  let is_transparent := match goal with
+                        | _ => let __ := (eval cbv delta [H] in H) in
+                               constr:(true)
+                        | _ => constr:(false)
+                        end in
+  lazymatch is_transparent with
+  | true
+    => let H' := fresh in
+       rename H into H';
+       let H'' := guarded_specialize_term_under_binders_by guard_tac H' tac in
+       pose H'' as H;
+       subst H'
+  | false
+    => let H := guarded_specialize_term_under_binders_by guard_tac H tac in
+       specialize H
+  end.
+
+Ltac guard_noop H := idtac.
+
+Ltac guard_nondep H :=
+  lazymatch type of H with
+  | ?A -> ?B => idtac
+  end.
+
+(** try to specialize all non-dependent hypotheses using [tac] at any point under their binders, maintaining transparency *)
+Ltac guarded_specialize_under_binders_by' tac guard_tac :=
+  idtac;
+  match goal with
+  | [ H : _ |- _ ]
+    => guard_tac H;
+       guarded_specialize_hyp_under_binders_by guard_nondep H tac
+  end.
+Ltac guarded_specialize_dep_under_binders_by' tac guard_tac :=
+  idtac;
+  match goal with
+  | [ H : _ |- _ ]
+    => guard_tac H;
+       guarded_specialize_hyp_under_binders_by guard_noop H tac
+  end.
+
+Ltac specialize_under_binders_by' tac := guarded_specialize_under_binders_by' tac ltac:(fun _ => idtac).
+Ltac specialize_dep_under_binders_by' tac := guarded_specialize_dep_under_binders_by' tac ltac:(fun _ => idtac).
+
+Ltac guarded_specialize_under_binders_by tac guard_tac := repeat guarded_specialize_under_binders_by' tac guard_tac.
+Ltac guarded_specialize_dep_under_binders_by tac guard_tac := repeat guarded_specialize_dep_under_binders_by' tac guard_tac.
+
+Ltac specialize_under_binders_by tac := repeat specialize_under_binders_by' tac.
+Ltac specialize_dep_under_binders_by tac := repeat specialize_dep_under_binders_by' tac.
+
+(** [specialize_under_binders_by auto] should not mean [specialize_under_binders_by ( auto
+    with * )]!!!!!!! (see
+    https://coq.inria.fr/bugs/show_bug.cgi?id=4966) We fix this design
+    flaw. *)
+Tactic Notation "specialize_under_binders_by" tactic3(tac) := specialize_under_binders_by tac.
+Tactic Notation "specialize_dep_under_binders_by" tactic3(tac) := specialize_dep_under_binders_by tac.
diff --git a/src/Util/Tactics/Zeta1.v b/src/Util/Tactics/Zeta1.v
new file mode 100644
index 0000000000..45fef2f4cb
--- /dev/null
+++ b/src/Util/Tactics/Zeta1.v
@@ -0,0 +1,6 @@
+Require Export Crypto.Util.Notations.
+
+Ltac zeta1 x :=
+  lazymatch x with
+  | let a := ?b in ?f => constr:(subst_let a := b in f)
+  end.