diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v
index 6a27291723..371e490db6 100644
--- a/src/Assembly/Equivalence.v
+++ b/src/Assembly/Equivalence.v
@@ -131,23 +131,29 @@ Definition default_assembly_conventions : assembly_conventions_opt
      |}.
 
 Module Export Options.
+  Export Assembly.Symbolic.Options.
   Class equivalence_checker_options_opt :=
     { assembly_conventions_ : assembly_conventions_opt
+    ; symbolic_options_ : symbolic_options_opt
     }.
   Definition default_equivalence_checker_options : equivalence_checker_options_opt
     := {| assembly_conventions_ := default_assembly_conventions
+       ; symbolic_options_ := default_symbolic_options
        |}.
 End Options.
 
 Module Export EquivalenceCheckerHints.
+  Export Assembly.Symbolic.Hints.
   Global Existing Instances
    Build_equivalence_checker_options_opt
    assembly_conventions_
+   symbolic_options_
   .
   #[global]
    Hint Cut [
       ( _ * )
         (assembly_conventions_
+        | symbolic_options_
         ) ( _ * )
         (Build_equivalence_checker_options_opt
         )
@@ -709,7 +715,7 @@ Global Instance show_EquivalenceCheckingError : Show EquivalenceCheckingError
 Definition merge_fresh_symbol {descr:description} : dag.M idx := fun d => merge_node (dag.gensym 64%N d) d.
 Definition merge_literal {descr:description} (l:Z) : dag.M idx := merge_node ((const l, nil)).
 
-Definition SetRegFresh {descr:description} (r : REG) : M idx :=
+Definition SetRegFresh {opts : symbolic_options_computed_opt} {descr:description} (r : REG) : M idx :=
   (idx <- lift_dag merge_fresh_symbol;
   _ <- SetReg r idx;
   Symbolic.ret idx).
@@ -726,7 +732,7 @@ Bind Scope symex_scope with symexM.
 Notation "'slet' x .. y <- X ; B"  := (symex_bind X (fun x => .. (fun y => B%symex) .. )) : symex_scope.
 Notation "A <- X ; B" := (symex_bind X (fun A => B%symex)) : symex_scope.
 (* light alias *)
-Definition App {descr:description} (e : Symbolic.node idx) : symexM idx := fun st => Success (merge (simplify st e) st).
+Definition App {opts : symbolic_options_computed_opt} {descr:description} (e : Symbolic.node idx) : symexM idx := fun st => Success (merge (simplify st e) st).
 Definition RevealConstant (i : idx) : symexM N := fun st =>
   match reveal st 1 i with
   | ExprApp (const n, nil) =>
@@ -803,17 +809,17 @@ Fixpoint build_inputs {descr:description} (types : type_spec) : dag.M (list (idx
      end%dagM.
 
 (* we factor this out so that conversion is not slow when proving things about this *)
-Definition compute_array_address {descr:description} (base : idx) (i : nat)
+Definition compute_array_address {opts : symbolic_options_computed_opt} {descr:description} (base : idx) (i : nat)
   := (offset <- Symbolic.App (zconst 64%N (8 * Z.of_nat i), nil);
       Symbolic.App (add 64%N, [base; offset]))%x86symex.
 
-Definition build_merge_array_addresses {descr:description} (base : idx) (items : list idx) : M (list idx)
+Definition build_merge_array_addresses {opts : symbolic_options_computed_opt} {descr:description} (base : idx) (items : list idx) : M (list idx)
   := mapM (fun '(i, idx) =>
              (addr <- compute_array_address base i;
               (fun s => Success (addr, update_mem_with s (cons (addr,idx)))))
           )%x86symex (List.enumerate items).
 
-Fixpoint build_merge_base_addresses {descr:description} {dereference_scalar:bool} (items : list (idx + list idx)) (reg_available : list REG) : M (list ((REG + idx) + idx))
+Fixpoint build_merge_base_addresses {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} (items : list (idx + list idx)) (reg_available : list REG) : M (list ((REG + idx) + idx))
   := match items, reg_available with
      | [], _ | _, [] => Symbolic.ret []
      | inr idxs :: xs, r :: reg_available
@@ -1003,7 +1009,7 @@ Fixpoint symex_T_app_curried {t : API.type} : symex_T t -> type.for_each_lhs_of_
 
 Bind Scope symex_scope with symex_T.
 
-Definition symex_ident {descr:description} {t} (idc : ident t) : symex_T t.
+Definition symex_ident {opts : symbolic_options_computed_opt} {descr:description} {t} (idc : ident t) : symex_T t.
 Proof.
   refine (let symex_mod_zrange idx '(ZRange.Build_zrange l u) :=
             let u := Z.succ u in
@@ -1195,7 +1201,7 @@ Proof.
   all: cbn in *.
 Defined.
 
-Fixpoint symex_expr {descr:description} {t} (e : API.expr (var:=var) t) : symex_T t
+Fixpoint symex_expr {opts : symbolic_options_computed_opt} {descr:description} {t} (e : API.expr (var:=var) t) : symex_T t
   := let _ := @Compilers.ToString.PHOAS.expr.partially_show_expr in
      match e in expr.expr t return symex_T t with
      | expr.Ident _ idc => symex_ident idc
@@ -1218,7 +1224,7 @@ Fixpoint symex_expr {descr:description} {t} (e : API.expr (var:=var) t) : symex_
      end.
 
 (* takes and returns PHOAS-style things *)
-Definition symex_PHOAS_PHOAS {t} (expr : API.Expr t) (input_var_data : type.for_each_lhs_of_arrow _ t) (d : dag)
+Definition symex_PHOAS_PHOAS {opts : symbolic_options_computed_opt} {t} (expr : API.Expr t) (input_var_data : type.for_each_lhs_of_arrow _ t) (d : dag)
   : ErrorT EquivalenceCheckingError (base_var (type.final_codomain t) * dag)
   := let ast : API.expr (type.base (type.final_codomain t))
          := invert_expr.smart_App_curried (expr _) input_var_data in
@@ -1226,6 +1232,7 @@ Definition symex_PHOAS_PHOAS {t} (expr : API.Expr t) (input_var_data : type.for_
 
 (* takes and returns assembly/list style things *)
 Definition symex_PHOAS
+           {opts : symbolic_options_computed_opt}
            {t} (expr : API.Expr t)
            (inputs : list (idx + list idx))
            (d : dag)
@@ -1252,25 +1259,25 @@ Definition init_symbolic_state (d : dag) : symbolic_state
        symbolic_flag_state := Tuple.repeat None 6;
      |}.
 
-Definition compute_stack_base {descr:description} (stack_size : nat) : M idx
+Definition compute_stack_base {opts : symbolic_options_computed_opt} {descr:description} (stack_size : nat) : M idx
   := (rsp_val <- SetRegFresh rsp;
       stack_size <- Symbolic.App (zconst 64 (-8 * Z.of_nat stack_size), []);
       Symbolic.App (add 64%N, [rsp_val; stack_size]))%x86symex.
 
-Definition build_merge_stack_placeholders {descr:description} (stack_size : nat)
+Definition build_merge_stack_placeholders {opts : symbolic_options_computed_opt} {descr:description} (stack_size : nat)
   : M idx
   := (stack_placeholders <- lift_dag (build_inputarray stack_size);
       stack_base <- compute_stack_base stack_size;
       _ <- build_merge_array_addresses stack_base stack_placeholders;
       ret stack_base)%x86symex.
 
-Definition LoadArray {descr:description} (base : idx) (len : nat) : M (list idx)
+Definition LoadArray {opts : symbolic_options_computed_opt} {descr:description} (base : idx) (len : nat) : M (list idx)
   := mapM (fun i =>
              (addr <- compute_array_address base i;
               Remove64 addr)%x86symex)
           (seq 0 len).
 
-Definition LoadOutputs_internal {descr:description} {dereference_scalar:bool} (outputaddrs : list ((REG + idx) + idx)) (output_types : type_spec)
+Definition LoadOutputs_internal {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} (outputaddrs : list ((REG + idx) + idx)) (output_types : type_spec)
   : M (list (idx + list idx))
   := (mapM (fun '(ocells, spec) =>
             match ocells, spec with
@@ -1289,7 +1296,7 @@ Definition LoadOutputs_internal {descr:description} {dereference_scalar:bool} (o
                   ret (inr v))
             end) (List.combine outputaddrs output_types))%N%x86symex.
 
-Definition LoadOutputs {descr:description} {dereference_scalar:bool} (outputaddrs : list ((REG + idx) + idx)) (output_types : type_spec)
+Definition LoadOutputs {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} (outputaddrs : list ((REG + idx) + idx)) (output_types : type_spec)
   : M (ErrorT EquivalenceCheckingError (list (idx + list idx)))
   := (* In the following line, we match on the result so we can emit Internal_error_output_load_failed in the calling function, rather than passing through the placeholder error from LoadOutputs *)
   fun s => if (List.length outputaddrs =? List.length output_types)%nat
@@ -1307,6 +1314,7 @@ Definition LoadOutputs {descr:description} {dereference_scalar:bool} (outputaddr
              Success (Error (Internal_error_LoadOutputs_length_mismatch outputaddrs output_types), s).
 
 Definition symex_asm_func_M
+           {opts : symbolic_options_computed_opt}
            (dereference_input_scalars:=false)
            {dereference_output_scalars:bool}
            (callee_saved_registers : list REG)
@@ -1344,6 +1352,7 @@ Definition symex_asm_func_M
                     s)))%N%x86symex.
 
 Definition symex_asm_func
+           {opts : symbolic_options_computed_opt}
            {dereference_output_scalars:bool}
            (d : dag) (callee_saved_registers : list REG) (output_types : type_spec) (stack_size : nat)
            (inputs : list (idx + list idx)) (reg_available : list REG) (asm : Lines)
@@ -1374,7 +1383,8 @@ Definition symex_asm_func
              end.
 
 Section check_equivalence.
-  Context {assembly_calling_registers' : assembly_calling_registers_opt}
+  Context {symbolic_opts : symbolic_options_computed_opt}
+          {assembly_calling_registers' : assembly_calling_registers_opt}
           {assembly_stack_size' : assembly_stack_size_opt}
           {assembly_output_first : assembly_output_first_opt}
           {assembly_argument_registers_left_to_right : assembly_argument_registers_left_to_right_opt}
diff --git a/src/Assembly/EquivalenceProofs.v b/src/Assembly/EquivalenceProofs.v
index 3c1ff3bac7..5288028750 100644
--- a/src/Assembly/EquivalenceProofs.v
+++ b/src/Assembly/EquivalenceProofs.v
@@ -300,7 +300,7 @@ Local Ltac saturate_eval_merge_step :=
         | solve [ eauto 100 ] ].
 Local Ltac saturate_eval_merge := repeat saturate_eval_merge_step.
 
-Lemma App_correct {descr:description} n d (Hdag : gensym_dag_ok G d) i d' (H : App n d = Success (i, d'))
+Lemma App_correct {opts : symbolic_options_computed_opt} {descr:description} n d (Hdag : gensym_dag_ok G d) i d' (H : App n d = Success (i, d'))
   v (Heval : eval_node G d n v)
   : eval G d' (ExprRef i) v /\ gensym_dag_ok G d' /\ (forall e n, eval G d e n -> eval G d' e n).
 Proof using Type.
@@ -321,6 +321,7 @@ Lemma unfold_symex_bind {A B} ma amb :
 Proof using Type. exact eq_refl. Qed.
 
 Theorem symex_ident_correct
+        {opts : symbolic_options_computed_opt}
         {descr:description}
         {t} (idc : ident t)
         (d : dag)
@@ -420,6 +421,7 @@ Proof using Type.
 Qed.
 
 Theorem symex_expr_correct
+        {opts : symbolic_options_computed_opt}
         {descr:description}
         {t} (expr1 : API.expr (var:=var) t) (expr2 : API.expr (var:=API.interp_type) t)
         (d : dag)
@@ -520,7 +522,7 @@ Proof using Type.
                     | progress specialize_under_binders_by eauto using lift_eval_var_impl ].
 Qed.
 
-Lemma symex_expr_App_curried {descr:description} {t} (e : API.expr t) input_var_data d
+Lemma symex_expr_App_curried {opts : symbolic_options_computed_opt} {descr:description} {t} (e : API.expr t) input_var_data d
   : symex_expr (invert_expr.App_curried e (type.map_for_each_lhs_of_arrow (fun t v => ($$v)%expr) input_var_data)) d
     = symex_T_app_curried (symex_expr e) input_var_data d.
 Proof using Type.
@@ -537,7 +539,7 @@ Proof using Type.
   all: destruct_head'_or; destruct_head'_ex; destruct_head'_and; congruence.
 Qed.
 
-Lemma symex_expr_smart_App_curried {descr:description} {t} (e : API.expr t) input_var_data d
+Lemma symex_expr_smart_App_curried {opts : symbolic_options_computed_opt} {descr:description} {t} (e : API.expr t) input_var_data d
   : symex_expr (invert_expr.smart_App_curried e input_var_data) d
     = symex_T_app_curried (symex_expr e) input_var_data d.
 Proof using Type.
@@ -548,6 +550,7 @@ Proof using Type.
 Qed.
 
 Theorem symex_PHOAS_PHOAS_correct
+        {opts : symbolic_options_computed_opt}
         {t} (expr : API.Expr t)
         (d : dag)
         (input_var_data : type.for_each_lhs_of_arrow var t) (input_runtime_var : type.for_each_lhs_of_arrow API.interp_type t)
@@ -729,6 +732,7 @@ Proof using Type.
 Qed.
 
 Theorem symex_PHOAS_correct
+        {opts : symbolic_options_computed_opt}
         {t} (expr : API.Expr t)
         (d : dag)
         (inputs : list (idx + list idx)) (runtime_inputs : list (Z + list Z))
@@ -751,7 +755,7 @@ Proof using Type.
   all: lazymatch goal with
        | [ H : symex_PHOAS_PHOAS _ _ _ = Success _,
                input_runtime_var : type.for_each_lhs_of_arrow API.interp_type _
-           |- _ ] => apply (@symex_PHOAS_PHOAS_correct _ _ _ _ input_runtime_var) in H; try assumption; [ | clear H .. ]
+           |- _ ] => apply @symex_PHOAS_PHOAS_correct with (input_runtime_var:=input_runtime_var) in H; try assumption; [ | clear H .. ]
        | [ |- False ] => idtac
        end.
   all: repeat first [ progress break_innermost_match_hyps
@@ -961,12 +965,13 @@ Definition lift_dag_G {A} (v : dagG.M A) : G.M A
   := fun '(G, s) => let '(v, (G, d)) := v (G, s.(dag_state)) in
                     Some (v, (G, update_dag_with s (fun _ => d))).
 
-Definition SetRegFresh_G {descr:description} (r : REG) (v : Z) : G.M idx
+Definition SetRegFresh_G {opts : symbolic_options_computed_opt} {descr:description} (r : REG) (v : Z) : G.M idx
   := (idx <- lift_dag_G (merge_fresh_symbol_G v);
       _ <- G.lift (SetReg r idx);
       G.ret idx)%GM.
 
 Fixpoint build_merge_base_addresses_G
+         {opts : symbolic_options_computed_opt}
          {descr:description}
          {dereference_scalar:bool}
          (items : list (idx + list idx)) (reg_available : list REG) (runtime_reg : list Z) {struct items}
@@ -992,13 +997,13 @@ Fixpoint build_merge_base_addresses_G
            G.ret (inl addr :: rest))
      end%GM%N%x86symex.
 
-Definition compute_stack_base_G {descr:description} (rsp_val : Z) (stack_size : nat)
+Definition compute_stack_base_G {opts : symbolic_options_computed_opt} {descr:description} (rsp_val : Z) (stack_size : nat)
   : G.M idx
   := (rsp_idx <- SetRegFresh_G rsp rsp_val;
       stack_size <- G.lift (Symbolic.App (zconst 64 (-8 * Z.of_nat stack_size), []));
       G.lift (Symbolic.App (add 64%N, [rsp_idx; stack_size])))%GM.
 
-Definition build_merge_stack_placeholders_G {descr:description} (rsp_val : Z) (stack_vals : list Z)
+Definition build_merge_stack_placeholders_G {opts : symbolic_options_computed_opt} {descr:description} (rsp_val : Z) (stack_vals : list Z)
   : G.M idx
   := (let stack_size := List.length stack_vals in
       stack_placeholders <- lift_dag_G (build_inputarray_G stack_vals);
@@ -1395,7 +1400,7 @@ Proof.
   eexists; reflexivity.
 Qed.
 
-Lemma SetRegFresh_eq_G {descr:description} G r s v idx s'
+Lemma SetRegFresh_eq_G {opts : symbolic_options_computed_opt} {descr:description} G r s v idx s'
       (H : SetRegFresh r s = Success (idx, s'))
   : exists G',
     SetRegFresh_G r v (G, s) = Some (idx, (G', s')).
@@ -1422,14 +1427,15 @@ Proof.
                | progress destruct_head'_prod ].
 Qed.
 
-Lemma build_merge_base_addresses_eq_G {descr:description} {dereference_scalar:bool}
+Lemma build_merge_base_addresses_eq_G {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool}
       G items reg_available runtime_reg s res s'
       (Hreg : Nat.min (List.length items) (List.length reg_available) <= List.length runtime_reg)
       (H : build_merge_base_addresses (dereference_scalar:=dereference_scalar) items reg_available s = Success (res, s'))
   : exists G',
     build_merge_base_addresses_G (dereference_scalar:=dereference_scalar) items reg_available runtime_reg (G, s) = Some (res, (G', s')).
 Proof.
-  move H at top; move items at top; move dereference_scalar at top; repeat match goal with H : _ |- _ => revert H end; intro.
+  move H at top; move items at top; move dereference_scalar at top; move opts at top; repeat match goal with H : _ |- _ => revert H end.
+  intros until items.
   induction items as [|? ? IH]; cbn [build_merge_base_addresses build_merge_base_addresses_G].
   all: cbv [G.ret Symbolic.ret Symbolic.bind ErrorT.bind G.bind Crypto.Util.Option.bind G.lift]; intros.
   all: repeat first [ progress destruct_head'_ex
@@ -1468,7 +1474,7 @@ Proof.
                     | progress destruct_head'_prod ].
 Qed.
 
-Lemma compute_stack_base_eq_G {descr:description} G rsp_val stack_size s res s'
+Lemma compute_stack_base_eq_G {opts : symbolic_options_computed_opt} {descr:description} G rsp_val stack_size s res s'
       (H : compute_stack_base stack_size s = Success (res, s'))
   : exists G',
     compute_stack_base_G rsp_val stack_size (G, s) = Some (res, (G', s')).
@@ -1494,7 +1500,7 @@ Proof.
                | break_innermost_match_step ].
 Qed.
 
-Lemma build_merge_stack_placeholders_eq_G {descr:description} G rsp_val stack_vals s res s'
+Lemma build_merge_stack_placeholders_eq_G {opts : symbolic_options_computed_opt} {descr:description} G rsp_val stack_vals s res s'
       (H : build_merge_stack_placeholders (List.length stack_vals) s = Success (res, s'))
   : exists G',
     build_merge_stack_placeholders_G rsp_val stack_vals (G, s) = Some (res, (G', s')).
@@ -1525,7 +1531,7 @@ Proof.
                | break_innermost_match_step ].
 Qed.
 
-Lemma SetReg_ok {descr:description} G s s' reg idx rn lo sz v
+Lemma SetReg_ok {opts : symbolic_options_computed_opt} {descr:description} G s s' reg idx rn lo sz v
       (Hreg : index_and_shift_and_bitcount_of_reg reg = (rn, lo, sz))
       (H64 : sz = 64%N)
       (H : SetReg reg idx s = Success (tt, s'))
@@ -1567,7 +1573,7 @@ Proof.
   (* need to do this early to deal with conversion slowness *)
   repeat match goal with
          | [ H : context[simplify ?s ?n] |- _ ]
-           => unshelve epose proof (@eval_simplify _ s n _ _); shelve_unifiable;
+           => unshelve epose proof (@eval_simplify _ _ s n _ _); shelve_unifiable;
               [ solve [ repeat first [ eassumption | exactly_once econstructor ] ] | ];
               generalize dependent (simplify s n); intros
          | [ H : context[merge ?e ?d] |- _ ]
@@ -1585,7 +1591,7 @@ Proof.
                | eapply ex_intro ].
 Qed.
 
-Lemma SetReg_ok_bounded {descr:description} G s s' reg idx rn lo sz v
+Lemma SetReg_ok_bounded {opts : symbolic_options_computed_opt} {descr:description} G s s' reg idx rn lo sz v
       (Hreg : index_and_shift_and_bitcount_of_reg reg = (rn, lo, sz))
       (H64 : sz = 64%N)
       (H : SetReg reg idx s = Success (tt, s'))
@@ -1612,7 +1618,7 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma SetRegFresh_G_ok {descr:description} G G' s s' reg idx rn lo sz v
+Lemma SetRegFresh_G_ok {opts : symbolic_options_computed_opt} {descr:description} G G' s s' reg idx rn lo sz v
       (Hreg : index_and_shift_and_bitcount_of_reg reg = (rn, lo, sz))
       (H64 : sz = 64%N)
       (H : SetRegFresh_G reg v (G, s) = Some (idx, (G', s')))
@@ -1658,7 +1664,7 @@ Proof.
                | eapply ex_intro ].
 Qed.
 
-Lemma SetRegFresh_G_ok_bounded {descr:description} G G' s s' reg idx rn lo sz v
+Lemma SetRegFresh_G_ok_bounded {opts : symbolic_options_computed_opt} {descr:description} G G' s s' reg idx rn lo sz v
       (Hreg : index_and_shift_and_bitcount_of_reg reg = (rn, lo, sz))
       (H64 : sz = 64%N)
       (H : SetRegFresh_G reg v (G, s) = Some (idx, (G', s')))
@@ -1685,7 +1691,7 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma GetReg_ok {descr:description} G s s' reg idx rn lo sz v
+Lemma GetReg_ok {opts : symbolic_options_computed_opt} {descr:description} G s s' reg idx rn lo sz v
       (Hreg : index_and_shift_and_bitcount_of_reg reg = (rn, lo, sz))
       (H64 : sz = 64%N)
       (H : GetReg reg s = Success (idx, s'))
@@ -1722,7 +1728,7 @@ Proof.
   (* need to do this early to deal with conversion slowness *)
   repeat match goal with
          | [ H : context[simplify ?s ?n] |- _ ]
-           => unshelve epose proof (@eval_simplify _ s n _ _); shelve_unifiable;
+           => unshelve epose proof (@eval_simplify _ _ s n _ _); shelve_unifiable;
               [ solve [ repeat first [ eassumption | exactly_once econstructor ] ] | ];
               generalize dependent (simplify s n); intros
          | [ H : context[merge ?e ?d] |- _ ]
@@ -1744,7 +1750,7 @@ Proof.
                     | eapply ex_intro ].
 Qed.
 
-Lemma GetReg_ok_bounded {descr:description} G s s' reg idx rn lo sz v
+Lemma GetReg_ok_bounded {opts : symbolic_options_computed_opt} {descr:description} G s s' reg idx rn lo sz v
       (Hreg : index_and_shift_and_bitcount_of_reg reg = (rn, lo, sz))
       (H64 : sz = 64%N)
       (H : GetReg reg s = Success (idx, s'))
@@ -1861,7 +1867,7 @@ Proof.
   rewrite get_reg_set_reg_full; break_innermost_match; reflect_hyps; cbv beta in *; try reflexivity; lia.
 Qed.
 
-Lemma compute_array_address_ok {descr:description} G s s' base i idx base_val
+Lemma compute_array_address_ok {opts : symbolic_options_computed_opt} {descr:description} G s s' base i idx base_val
       (H : compute_array_address base i s = Success (idx, s'))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
@@ -1900,7 +1906,7 @@ Proof.
   (* need to do this early to deal with conversion slowness *)
   repeat first [ match goal with
                  | [ H : context[simplify ?s ?n] |- _ ]
-                   => unshelve epose proof (@eval_simplify _ s n _ _); shelve_unifiable;
+                   => unshelve epose proof (@eval_simplify _ _ s n _ _); shelve_unifiable;
                       [ solve [ repeat first [ eassumption | solve [ eauto ] | exactly_once econstructor ] ] | ];
                       generalize dependent (simplify s n); intros
                  | [ H : context[merge ?e ?d] |- _ ]
@@ -1928,7 +1934,7 @@ Proof.
                     | progress (push_Zmod; pull_Zmod) ].
 Qed.
 
-Lemma compute_array_address_ok_bounded {descr:description} G s s' base i idx base_val
+Lemma compute_array_address_ok_bounded {opts : symbolic_options_computed_opt} {descr:description} G s s' base i idx base_val
       (H : compute_array_address base i s = Success (idx, s'))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
@@ -1953,7 +1959,7 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma build_merge_array_addresses_ok {descr:description} G s s'
+Lemma build_merge_array_addresses_ok {opts : symbolic_options_computed_opt} {descr:description} G s s'
       base base_val items addrs
       (H : build_merge_array_addresses base items s = Success (addrs, s'))
       (d := s.(dag_state))
@@ -2025,7 +2031,7 @@ Proof.
     eauto 20. }
 Qed.
 
-Lemma compute_stack_base_G_ok {descr:description} G G' s s' rv
+Lemma compute_stack_base_G_ok {opts : symbolic_options_computed_opt} {descr:description} G G' s s' rv
       (rsp_val : Z) (stack_size : nat)
       (H : compute_stack_base_G rsp_val stack_size (G, s) = Some (rv, (G', s')))
       (d := s.(dag_state))
@@ -2072,7 +2078,7 @@ Proof.
                       | [ H : (tt, (?y, ?z)) = (tt, (?y', ?z')) |- _ ]
                         => is_var y; is_var z; is_var y'; is_var z'; inversion H; clear H
                       | [ H : context[simplify ?s ?n] |- _ ]
-                        => unshelve epose proof (@eval_simplify _ s n _ _); shelve_unifiable;
+                        => unshelve epose proof (@eval_simplify _ _ s n _ _); shelve_unifiable;
                            [ solve [ repeat first [ eassumption | solve [ eauto ] | exactly_once econstructor ] ] | ];
                            generalize dependent (simplify s n); intros
                       | [ H : context[merge ?e ?d] |- _ ]
@@ -2099,7 +2105,7 @@ Proof.
                     | f_equal; lia ].
 Qed.
 
-Lemma build_merge_stack_placeholders_G_ok {descr:description} G G' s s'
+Lemma build_merge_stack_placeholders_G_ok {opts : symbolic_options_computed_opt} {descr:description} G G' s s'
       (rsp_val : Z) (stack_vals : list Z) stack_base
       (H : build_merge_stack_placeholders_G rsp_val stack_vals (G, s) = Some (stack_base, (G', s')))
       (d := s.(dag_state))
@@ -2192,7 +2198,7 @@ Ltac handle_eval_eval :=
          end.
 
 Lemma build_merge_base_addresses_G_ok
-      {descr:description} {dereference_scalar:bool}
+      {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool}
   : forall (idxs : list (idx + list idx))
            (reg_available : list REG)
            (runtime_reg : list Z)
@@ -2414,7 +2420,7 @@ Proof.
                  end ].
 Qed.
 
-Lemma compute_stack_ok {descr:description} G s s' base
+Lemma compute_stack_ok {opts : symbolic_options_computed_opt} {descr:description} G s s' base
       (rsp_val : Z) (stack_size : nat)
       (H : compute_stack_base stack_size s = Success (base, s'))
       (d := s.(dag_state))
@@ -2441,7 +2447,7 @@ Proof.
   eapply compute_stack_base_G_ok in H; try eassumption.
 Qed.
 
-Lemma build_merge_stack_placeholders_ok {descr:description} G s s'
+Lemma build_merge_stack_placeholders_ok {opts : symbolic_options_computed_opt} {descr:description} G s s'
       (rsp_val : Z) (stack_vals : list Z) stack_base
       (H : build_merge_stack_placeholders (List.length stack_vals) s = Success (stack_base, s'))
       (d := s.(dag_state))
@@ -2474,7 +2480,7 @@ Proof.
 Qed.
 
 Lemma build_merge_base_addresses_ok
-      {descr:description} {dereference_scalar:bool}
+      {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool}
       (idxs : list (idx + list idx))
       (reg_available : list REG)
       (runtime_reg : list Z)
@@ -2594,7 +2600,7 @@ Proof.
 Qed.
 
 
-Lemma mapM_GetReg_ok_bounded {descr:description} G
+Lemma mapM_GetReg_ok_bounded {opts : symbolic_options_computed_opt} {descr:description} G
   : forall regs idxs reg_vals s s'
            (H : mapM GetReg regs s = Success (idxs, s'))
            (d := s.(dag_state))
@@ -2769,19 +2775,19 @@ Local Instance Merge_reg_same {descr:description} x : same_reg_some_of_success (
 Proof. same_reg_some_of_success_t. Qed.
 
 (* TODO: move? *)
-Local Instance App_reg_same {descr:description} x : same_reg_some_of_success (Symbolic.App x).
+Local Instance App_reg_same {opts : symbolic_options_computed_opt} {descr:description} x : same_reg_some_of_success (Symbolic.App x).
 Proof. same_reg_some_of_success_t. Qed.
 
 (* TODO: move? *)
-Local Instance GetReg_reg_same {descr:description} r : same_reg_some_of_success (GetReg r).
+Local Instance GetReg_reg_same {opts : symbolic_options_computed_opt} {descr:description} r : same_reg_some_of_success (GetReg r).
 Proof. same_reg_some_of_success_t. Qed.
 
 (* TODO: move? *)
-Local Instance Address_reg_same {descr:description} {sa:AddressSize} a : same_reg_some_of_success (Address a).
+Local Instance Address_reg_same {opts : symbolic_options_computed_opt} {descr:description} {sa:AddressSize} a : same_reg_some_of_success (Address a).
 Proof. same_reg_some_of_success_t. Qed.
 
 (* TODO: move? *)
-Local Instance GetOperand_reg_same {descr:description} {sz:OperationSize} {sa:AddressSize} arg : same_reg_some_of_success (GetOperand arg).
+Local Instance GetOperand_reg_same {opts : symbolic_options_computed_opt} {descr:description} {sz:OperationSize} {sa:AddressSize} arg : same_reg_some_of_success (GetOperand arg).
 Proof. same_reg_some_of_success_t. Qed.
 
 (* TODO: move? *)
@@ -2789,7 +2795,7 @@ Local Instance GetFlag_reg_same f : same_reg_some_of_success (GetFlag f).
 Proof. same_reg_some_of_success_t. Qed.
 
 (* TODO: move? *)
-Local Instance SetOperand_reg_same {descr:description} {sz:OperationSize} {sa:AddressSize} arg v : same_reg_some_of_success (SetOperand arg v).
+Local Instance SetOperand_reg_same {opts : symbolic_options_computed_opt} {descr:description} {sz:OperationSize} {sa:AddressSize} arg v : same_reg_some_of_success (SetOperand arg v).
 Proof. same_reg_some_of_success_t. Qed.
 
 (* TODO: move? *)
@@ -2829,7 +2835,7 @@ Proof.
 Defined.
 
 (* TODO: move? *)
-Fixpoint Symeval_reg_same descr sz sa args {struct args} : same_reg_some_of_success (@Symeval descr sz sa args).
+Fixpoint Symeval_reg_same opts descr sz sa args {struct args} : same_reg_some_of_success (@Symeval opts descr sz sa args).
 Proof.
   destruct args; cbn [Symeval] in *; typeclasses eauto.
 Qed.
@@ -2840,7 +2846,7 @@ Typeclasses Opaque Symeval.
 Typeclasses Transparent AddressSize OperationSize.
 
 (* TODO: move? *)
-Local Instance SymexNormalInstruction_reg_same {descr:description} instr : same_reg_some_of_success (SymexNormalInstruction instr).
+Local Instance SymexNormalInstruction_reg_same {opts : symbolic_options_computed_opt} {descr:description} instr : same_reg_some_of_success (SymexNormalInstruction instr).
 Proof.
   destruct instr; cbv [SymexNormalInstruction err Symbolic.bind ret Syntax.op Syntax.args ErrorT.bind same_reg_some_of_success] in *; intros.
   same_reg_some_of_success_t.
@@ -2853,14 +2859,14 @@ Proof.
 Qed.
 
 (* TODO: move? *)
-Local Instance SymexLine_reg_same line : same_reg_some_of_success (SymexLine line).
+Local Instance SymexLine_reg_same {opts : symbolic_options_computed_opt} line : same_reg_some_of_success (SymexLine line).
 Proof.
   cbv [SymexLine SymexRawLine err ret] in *; break_innermost_match; try congruence.
   apply SymexNormalInstruction_reg_same.
 Qed.
 
 (* TODO: move? *)
-Lemma SymexLines_reg_same lines s s'
+Lemma SymexLines_reg_same {opts : symbolic_options_computed_opt} lines s s'
       (H : SymexLines lines s = Success (tt, s'))
   : same_reg_some s s'.
 Proof.
@@ -2931,19 +2937,19 @@ Local Instance Merge_mem_same {descr:description} x : same_mem_addressed_of_succ
 Proof. same_mem_addressed_of_success_t. Qed.
 
 (* TODO: move? *)
-Local Instance App_mem_same {descr:description} x : same_mem_addressed_of_success (Symbolic.App x).
+Local Instance App_mem_same {opts : symbolic_options_computed_opt} {descr:description} x : same_mem_addressed_of_success (Symbolic.App x).
 Proof. same_mem_addressed_of_success_t. Qed.
 
 (* TODO: move? *)
-Local Instance GetReg_mem_same {descr:description} r : same_mem_addressed_of_success (GetReg r).
+Local Instance GetReg_mem_same {opts : symbolic_options_computed_opt} {descr:description} r : same_mem_addressed_of_success (GetReg r).
 Proof. same_mem_addressed_of_success_t. Qed.
 
 (* TODO: move? *)
-Local Instance Address_mem_same descr sa a : same_mem_addressed_of_success (@Address descr sa a).
+Local Instance Address_mem_same opts descr sa a : same_mem_addressed_of_success (@Address opts descr sa a).
 Proof. same_mem_addressed_of_success_t. Qed.
 
 (* TODO: move? *)
-Local Instance GetOperand_mem_same descr sz sa arg : same_mem_addressed_of_success (@GetOperand descr sz sa arg).
+Local Instance GetOperand_mem_same opts descr sz sa arg : same_mem_addressed_of_success (@GetOperand opts descr sz sa arg).
 Proof. same_mem_addressed_of_success_t. Qed.
 
 (* TODO: move? *)
@@ -2951,7 +2957,7 @@ Local Instance GetFlag_mem_same f : same_mem_addressed_of_success (GetFlag f).
 Proof. same_mem_addressed_of_success_t. Qed.
 
 (* TODO: move? *)
-Local Instance SetOperand_mem_same descr sz sa arg v : same_mem_addressed_of_success (@SetOperand descr sz sa arg v).
+Local Instance SetOperand_mem_same opts descr sz sa arg v : same_mem_addressed_of_success (@SetOperand opts descr sz sa arg v).
 Proof. same_mem_addressed_of_success_t. Qed.
 
 (* TODO: move? *)
@@ -2999,7 +3005,7 @@ Proof.
 Defined.
 
 (* TODO: move? *)
-Fixpoint Symeval_mem_same descr sz sa args {struct args} : same_mem_addressed_of_success (@Symeval descr sz sa args).
+Fixpoint Symeval_mem_same opts descr sz sa args {struct args} : same_mem_addressed_of_success (@Symeval opts descr sz sa args).
 Proof.
   destruct args; cbn [Symeval] in *; typeclasses eauto.
 Qed.
@@ -3010,21 +3016,21 @@ Typeclasses Opaque Symeval.
 Typeclasses Transparent AddressSize OperationSize.
 
 (* TODO: move? *)
-Local Instance SymexNormalInstruction_mem_same {descr:description} instr : same_mem_addressed_of_success (SymexNormalInstruction instr).
+Local Instance SymexNormalInstruction_mem_same {opts : symbolic_options_computed_opt} {descr:description} instr : same_mem_addressed_of_success (SymexNormalInstruction instr).
 Proof.
   destruct instr; cbv [SymexNormalInstruction err Symbolic.bind ret Syntax.op Syntax.args ErrorT.bind same_mem_addressed_of_success] in *; intros.
   same_mem_addressed_of_success_t.
 Qed.
 
 (* TODO: move? *)
-Local Instance SymexLine_mem_same line : same_mem_addressed_of_success (SymexLine line).
+Local Instance SymexLine_mem_same {opts : symbolic_options_computed_opt} line : same_mem_addressed_of_success (SymexLine line).
 Proof.
   cbv [SymexLine SymexRawLine err ret] in *; break_innermost_match; try congruence.
   apply SymexNormalInstruction_mem_same.
 Qed.
 
 (* TODO: move? *)
-Lemma SymexLines_mem_same lines s s'
+Lemma SymexLines_mem_same {opts : symbolic_options_computed_opt} lines s s'
       (H : SymexLines lines s = Success (tt, s'))
   : same_mem_addressed s s'.
 Proof.
@@ -3339,7 +3345,7 @@ Proof.
 Qed.
 
 Local Existing Instance Permutation_cons | 0.
-Lemma LoadArray_ok {descr:description} G s s' base base_val len idxs
+Lemma LoadArray_ok {opts : symbolic_options_computed_opt} {descr:description} G s s' base base_val len idxs
       (H : LoadArray base len s = Success (idxs, s'))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
@@ -3447,7 +3453,7 @@ Ltac saturate_lengths_step :=
   end.
 Ltac saturate_lengths := repeat saturate_lengths_step.
 
-Lemma LoadOutputs_ok {descr:description} {dereference_scalar:bool} G s s' outputaddrs output_types output_vals idxs
+Lemma LoadOutputs_ok {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} G s s' outputaddrs output_types output_vals idxs
       (H : LoadOutputs (dereference_scalar:=dereference_scalar) outputaddrs output_types s = Success (Success idxs, s'))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v
index aacfd5d67b..98ab6c5b8f 100644
--- a/src/Assembly/Symbolic.v
+++ b/src/Assembly/Symbolic.v
@@ -74,10 +74,14 @@ Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.ZUtil.Lxor.
 Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
 Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.Listable.
+Require Import Crypto.Util.Strings.Parse.Common.
 Require Import Crypto.Util.Tactics.WarnIfGoalsRemain.
 Require Import Crypto.Util.Bool.Reflect.
 Require Import coqutil.Z.bitblast.
-Require Import Coq.Strings.String Crypto.Util.Strings.Show.
+Require Import Coq.Strings.String.
+Require Import Crypto.Util.Strings.Show.
+Require Import Crypto.Util.Strings.Show.Enum.
 Require Import Crypto.Assembly.Syntax.
 Import ListNotations.
 Definition idx := N.
@@ -317,6 +321,130 @@ End FMapOp.
 
 Module OpMap := FMapOp.OpMap.
 
+Module Export RewritePass.
+  Variant rewrite_pass :=
+    | addbyte_small
+    | addcarry_bit
+    | addcarry_small
+    | addoverflow_bit
+    | addoverflow_small
+    | combine_consts
+    | constprop
+    | consts_commutative
+    | drop_identity
+    | flatten_associative
+    | flatten_bounded_associative
+    | fold_consts_to_and
+    | set_slice0_small
+    | set_slice_set_slice
+    | shift_to_mul
+    | slice0
+    | slice01_addcarryZ
+    | slice01_subborrowZ
+    | slice_set_slice
+    | truncate_small
+    | unary_truncate
+    | xor_same
+  .
+  Definition rewrite_pass_beq (x y : rewrite_pass) : bool := if rewrite_pass_eq_dec x y then true else false.
+
+  Derive rewrite_pass_Listable SuchThat (@FinitelyListable rewrite_pass rewrite_pass_Listable) As rewrite_pass_FinitelyListable.
+  Proof. prove_ListableDerive. Qed.
+  Global Existing Instances rewrite_pass_Listable rewrite_pass_FinitelyListable.
+
+  Global Instance show_rewrite_pass : Show rewrite_pass.
+  Proof. prove_Show_enum (). Defined.
+  Global Instance show_lvl_rewrite_pass : ShowLevel rewrite_pass := show_rewrite_pass.
+
+  Definition parse_rewrite_pass_list : list (string * rewrite_pass)
+    := Eval vm_compute in
+      List.map
+        (fun r => (show r, r))
+        (list_all rewrite_pass).
+
+  Definition parse_rewrite_pass : ParserAction rewrite_pass
+    := parse_strs parse_rewrite_pass_list.
+
+  Definition default_rewrite_pass_order : list rewrite_pass
+    := [constprop
+        ;slice0
+        ;slice01_addcarryZ
+        ;slice01_subborrowZ
+        ;set_slice_set_slice
+        ;slice_set_slice
+        ;set_slice0_small
+        ;shift_to_mul
+        ;flatten_associative
+        ;consts_commutative
+        ;fold_consts_to_and
+        ;drop_identity
+        ;flatten_bounded_associative
+        ;unary_truncate
+        ;truncate_small
+        ;combine_consts
+        ;addoverflow_bit
+        ;addcarry_bit
+        ;addcarry_small
+        ;addoverflow_small
+        ;addbyte_small
+        ;xor_same
+    ].
+End RewritePass.
+
+Module Export Options.
+  (* Holds the order and multiplicity of passes *)
+  Class rewriting_pipeline_opt := rewriting_pipeline : list rewrite_pass.
+  (* Holds the passes that are enabled *)
+  Class rewriting_pass_filter_opt := rewriting_pass_filter : rewrite_pass -> bool.
+  (* Holds the actual list of passes that are used; we make this a
+     separate option so that it is computed once and for all rather
+     than every time, because it is (currently) quadratic to compute
+     in the number of passes *)
+  Class rewriting_passes_opt := rewriting_passes : list rewrite_pass.
+  Definition default_rewriting_passes
+             {rewriting_pipeline : rewriting_pipeline_opt}
+             {rewriting_pass_filter : rewriting_pass_filter_opt}
+    : rewriting_passes_opt
+    := List.filter rewriting_pass_filter rewriting_pipeline.
+
+  Class symbolic_options_opt :=
+    { asm_rewriting_pipeline : rewriting_pipeline_opt
+    ; asm_rewriting_pass_filter : rewriting_pass_filter_opt
+    }.
+
+  (* This holds the list of computed options, which are passed around between methods *)
+  Class symbolic_options_computed_opt :=
+    { asm_rewriting_passes : rewriting_passes_opt
+    }.
+
+  (* N.B. The default rewriting pass filter should not be changed here, but instead changed in CLI.v where it is derived from a default string *)
+  Definition default_symbolic_options : symbolic_options_opt
+    := {| asm_rewriting_pipeline := default_rewrite_pass_order
+       ; asm_rewriting_pass_filter := fun _ => true
+       |}.
+End Options.
+Module Export Hints.
+  Global Existing Instance default_rewriting_passes.
+  Global Existing Instances
+         Build_symbolic_options_opt
+         Build_symbolic_options_computed_opt
+         asm_rewriting_pipeline
+         asm_rewriting_pass_filter
+         asm_rewriting_passes
+  .
+  #[global]
+   Hint Cut [
+      ( _ * )
+        (asm_rewriting_pipeline
+        | asm_rewriting_pass_filter
+        | asm_rewriting_passes
+        ) ( _ * )
+        (Build_symbolic_options_opt
+        | Build_symbolic_options_computed_opt
+        )
+    ] : typeclass_instances.
+End Hints.
+
 Definition associative o := match o with add _|addZ|mul _|mulZ|or _|and _|xor _|andZ|orZ|xorZ=> true | _ => false end.
 Definition commutative o := match o with add _|addZ|addcarry _|addoverflow _|mul _|mulZ|or _|and _|xor _|andZ|orZ|xorZ => true | _ => false end.
 Definition identity o := match o with mul s => Some match s with N0 => 0%Z | _ => 1%Z end| mulZ=>Some 1%Z |add _|addZ|or _|orZ|xor _|xorZ|addcarry _|addcarryZ _|addoverflow _ => Some 0%Z | and s => Some (Z.ones (Z.of_N s))|andZ => Some (-1)%Z |_=> None end.
@@ -2014,7 +2142,9 @@ Definition isCst (e : expr) :=
 
 Module Rewrite.
 Class Ok r := rwok : forall G d e v, eval G d e v -> eval G d (r e) v.
-
+Class description_of (r : expr -> expr) := describe : string.
+#[global] Bind Scope string_scope with description_of.
+#[global] Typeclasses Opaque description_of.
 Ltac resolve_match_using_hyp :=
   match goal with |- context[match ?x with _ => _ end] =>
   match goal with H : x = ?v |- _ =>
@@ -2084,6 +2214,8 @@ Definition slice0 :=
     ExprApp (slice 0 s, [(ExprApp ((addZ|mulZ|negZ|shlZ|shrZ|andZ|orZ|xorZ) as o, args))]) =>
         ExprApp ((match o with addZ=>add s|mulZ=>mul s|negZ=>neg s|shlZ=>shl s|shrZ => shr s|andZ => and s| orZ => or s|xorZ => xor s |_=>old 0%N 999999%N end), args)
       | _ => e end.
+#[local] Instance describe_slice0 : description_of Rewrite.slice0
+  := "Merges (slice 0 s) into addZ,mulZ,negZ,shlZ,shrZ,andZ,orZ,xorZ".
 Global Instance slice0_ok : Ok slice0. Proof using Type. t. Qed.
 
 Definition slice01_addcarryZ :=
@@ -2091,6 +2223,8 @@ Definition slice01_addcarryZ :=
     ExprApp (slice 0 1, [(ExprApp (addcarryZ s, args))]) =>
         ExprApp (addcarry s, args)
       | _ => e end.
+#[local] Instance describe_slice01_addcarryZ : description_of Rewrite.slice01_addcarryZ
+  := "Merges (slice 0 1) into addcarryZ".
 Global Instance slice01_addcarryZ_ok : Ok slice01_addcarryZ.
 Proof using Type. t; rewrite ?Z.shiftr_0_r, ?Z.land_ones, ?Z.shiftr_div_pow2; trivial; Lia.lia. Qed.
 
@@ -2099,6 +2233,8 @@ Definition slice01_subborrowZ :=
     ExprApp (slice 0 1, [(ExprApp (subborrowZ s, args))]) =>
         ExprApp (subborrow s, args)
       | _ => e end.
+#[local] Instance describe_slice01_subborrowZ : description_of Rewrite.slice01_subborrowZ
+  := "Merges (slice 0 1) into subborrowZ".
 Global Instance slice01_subborrowZ_ok : Ok slice01_subborrowZ.
 Proof using Type. t; rewrite ?Z.shiftr_0_r, ?Z.land_ones, ?Z.shiftr_div_pow2; trivial; Lia.lia. Qed.
 
@@ -2106,6 +2242,8 @@ Definition slice_set_slice :=
   fun e => match e with
     ExprApp (slice 0 s1, [ExprApp (set_slice 0 s2, [_; e'])]) =>
       if N.leb s1 s2 then ExprApp (slice 0 s1, [e']) else e | _ => e end.
+#[local] Instance describe_slice_set_slice : description_of Rewrite.slice_set_slice
+  := "Simplifies slice applied to set_slice".
 Global Instance slice_set_slice_ok : Ok slice_set_slice.
 Proof using Type. t. f_equal. Z.bitblast. Qed.
 
@@ -2113,6 +2251,8 @@ Definition set_slice_set_slice :=
   fun e => match e with
     ExprApp (set_slice lo1 s1, [ExprApp (set_slice lo2 s2, [x; e']); y]) =>
       if andb (N.eqb lo1 lo2) (N.leb s2 s1) then ExprApp (set_slice lo1 s1, [x; y]) else e | _ => e end.
+#[local] Instance describe_set_slice_set_slice : description_of Rewrite.set_slice_set_slice
+  := "Simplifies set_slice applied to set_slice".
 Global Instance set_slice_set_slice_ok : Ok set_slice_set_slice.
 Proof using Type. t. f_equal. Z.bitblast. Qed.
 
@@ -2122,6 +2262,8 @@ Definition set_slice0_small :=
       match bound_expr x, bound_expr y with Some a, Some b =>
       if Z.leb 0 (ZRange.lower a) && Z.leb 0 (ZRange.lower b) && Z.leb (ZRange.upper a) (Z.ones (Z.of_N s)) && Z.leb (ZRange.upper b) (Z.ones (Z.of_N s)) then y
       else e | _, _ => e end | _ => e end%bool.
+#[local] Instance describe_set_slice0_small : description_of Rewrite.set_slice0_small
+  := "Simplifies set_slice when the slice being set fully overwrites the original".
 Global Instance set_slice0_small_ok : Ok set_slice0_small.
 Proof using Type.
   t.
@@ -2143,6 +2285,8 @@ Definition truncate_small :=
       if Z.leb 0 (ZRange.lower b) && Z.leb (ZRange.upper b) (Z.ones (Z.of_N s))
       then e'
       else e | _ => e end | _ => e end.
+#[local] Instance describe_truncate_small : description_of Rewrite.truncate_small
+  := "Simplifies slice when it's a no-op".
 Global Instance truncate_small_ok : Ok truncate_small. Proof using Type. t; []. cbn in *; eapply Z.land_ones_low_alt_ones; eauto. firstorder; Lia.lia. Qed.
 
 Definition addcarry_bit :=
@@ -2154,6 +2298,8 @@ Definition addcarry_bit :=
       | Some 0, Some 0 => ExprApp (const 0, nil)
       | _, _ => e
       end else e | _ => e end%Z%bool.
+#[local] Instance describe_addcarry_bit : description_of Rewrite.addcarry_bit
+  := "Simplifies (addcarry s, [const a; b]) when b is known to be a single bit".
 Global Instance addcarry_bit_ok : Ok addcarry_bit.
 Proof using Type.
   repeat step;
@@ -2172,6 +2318,8 @@ Definition addoverflow_bit :=
       | Some 0, Some 0 => ExprApp (const 0, nil)
       | _, _ => e
       end else e | _ => e end%Z%bool.
+#[local] Instance describe_addoverflow_bit : description_of Rewrite.addoverflow_bit
+  := "Simplifies (addoverflow s, [const a; b]) when b is known to be a single bit".
 Global Instance addoverflow_bit_ok : Ok addoverflow_bit.
 Proof using Type.
   repeat step;
@@ -2189,6 +2337,8 @@ Definition addbyte_small :=
           if Z.leb 0 (List.fold_right Z.add 0%Z (List.map lower bounds)) && Z.leb (List.fold_right Z.add 0%Z (List.map upper bounds)) (Z.ones (Z.of_N s))
           then ExprApp (add 64%N, args)
           else e | _ => e end | _ =>  e end.
+#[local] Instance describe_addbyte_small : description_of Rewrite.addbyte_small
+  := "Replaces (add 8, args) with (add 64, args) when doing so doesn't change semantics".
 Global Instance addbyte_small_ok : Ok addbyte_small.
 Proof using Type.
   t; f_equal.
@@ -2206,6 +2356,8 @@ Definition addcarry_small :=
           if Z.leb 0 (List.fold_right Z.add 0%Z (List.map lower bounds)) && Z.leb (List.fold_right Z.add 0%Z (List.map upper bounds)) (Z.ones (Z.of_N s))
           then (ExprApp (const 0, nil))
           else e | _ => e end | _ =>  e end.
+#[local] Instance describe_addcarry_small : description_of Rewrite.addcarry_small
+  := "Replaces (addcarry _, args) with 0 when bounds analysis can prove there's no carry".
 Global Instance addcarry_small_ok : Ok addcarry_small.
 Proof using Type.
   t; f_equal.
@@ -2233,6 +2385,8 @@ Definition addoverflow_small :=
           if List.forallb (Z.leb 0) (List.map lower bounds) && Z.leb (List.fold_right Z.add 0%Z (List.map upper bounds)) (Z.ones (Z.of_N s-1))
           then (ExprApp (const 0, nil))
           else e | _ => e end | _ =>  e end.
+#[local] Instance describe_addoverflow_small : description_of Rewrite.addoverflow_small
+  := "Replaces (addoverflow _, args) when there are at most 3 args and when bounds analysis can prove there's no overflow".
 Global Instance addoverflow_small_ok : Ok addoverflow_small.
 Proof using Type.
   t; cbv [Option.List.lift Crypto.Util.Option.bind fold_right map List.forallb] in *;
@@ -2250,6 +2404,8 @@ Definition constprop :=
   fun e => match interp0_expr e with
            | Some v => ExprApp (const v, nil)
            | _ => e end.
+#[local] Instance describe_constprop : description_of Rewrite.constprop
+  := "Performs constant propagation, evaluating expressions that are known to be constant".
 Global Instance constprop_ok : Ok constprop.
 Proof using Type. t. f_equal; eauto using eval_eval. Qed.
 
@@ -2263,7 +2419,8 @@ Definition unary_truncate :=
     | Some (Zpos p)
       => ExprApp (slice 0%N (Npos p), [x])
     | _ => e end | _ => e end.
-
+#[local] Instance describe_unary_truncate : description_of Rewrite.unary_truncate
+  := "Some operations are equivalent to truncation when applied to only one argument; this pass canonicalizes such expressions".
 Global Instance unary_truncate_ok : Ok unary_truncate.
 Proof using Type.
   t.
@@ -2527,6 +2684,8 @@ Definition flatten_associative :=
         | ExprApp (o', args') => if op_beq o o' then args' else [e']
         | _ => [e'] end) args)
     else e | _ => e end.
+#[local] Instance describe_flatten_associative : description_of Rewrite.flatten_associative
+  := "Flattens nested associative operations, such as turning (add [x; add [y; z]]) into (add [x; y; z])".
 Global Instance flatten_associative_ok : Ok flatten_associative.
 Proof using Type.
   repeat step.
@@ -2558,6 +2717,8 @@ Definition flatten_bounded_associative :=
         | Some (drop_if_bounded bound o'') => match bound_expr (ExprApp (o'', args')) with
         | Some ubound => if is_tighter_than_bool ubound bound then args' else [e']
                                               | _ => [e'] end | _ => [e'] end | _ => [e'] end) args) | _ => e end.
+#[local] Instance describe_flatten_bounded_associative : description_of Rewrite.flatten_bounded_associative
+  := "Flattens some nested operations such as add inside addcarry".
 
 Lemma fold_right_add_cps_id init ls
   : fold_right Z.add init ls = fold_right Z.add 0 ls + init.
@@ -2637,6 +2798,8 @@ Definition consts_commutative :=
          end
     else ExprApp (o, fst csts_exprs ++ snd csts_exprs)
     else e | _ => e end.
+#[local] Instance describe_consts_commutative : description_of Rewrite.consts_commutative
+  := "Moves all constants to the beginning of commutative n-ary operation lists, additionally combining the constants into a single node when the operation is associative".
 
 Global Instance consts_commutative_ok : Ok consts_commutative.
 Proof using Type.
@@ -2691,6 +2854,8 @@ Definition drop_identity :=
         let args := List.filter (neqconst i) args in
         ExprApp (o, arg :: args)
     | _, _ => e end end | _ => e end.
+#[local] Instance describe_drop_identity : description_of Rewrite.drop_identity
+  := "Drops constant identity subexpressions, such as 0s in add and 1s in mul".
 
 Lemma filter_neqconst_helper G d id
       l args
@@ -2788,6 +2953,8 @@ Definition fold_consts_to_and :=
                           else ExprApp (and (Z.to_N v_sz), ExprApp (const v', nil) :: args)
            | _ => e
            end.
+#[local] Instance describe_fold_consts_to_and : description_of Rewrite.fold_consts_to_and
+  := "Truncates constant arguments to bitwise and, dropping them if they provably do not change the result".
 
 Global Instance fold_consts_to_and_Ok : Ok fold_consts_to_and.
 Proof using Type.
@@ -2848,6 +3015,8 @@ Qed.
 Definition xor_same :=
   fun e => match e with ExprApp (xor _,[x;y]) =>
     if expr_beq x y then ExprApp (const 0, nil) else e | _ => e end.
+#[local] Instance describe_xor_same : description_of Rewrite.xor_same
+  := "Replaces xor x x with 0".
 Global Instance xor_same_ok : Ok xor_same.
 Proof using Type.
   t; cbn [fold_right]. rewrite Z.lxor_0_r, Z.lxor_nilpotent; trivial.
@@ -2867,6 +3036,8 @@ Definition shift_to_mul :=
       else if Z.ltb 0 v
       then ExprApp (o', [e'; ExprApp (const (2^v)%Z, [])])
       else e | _ => e end.
+#[local] Instance describe_shift_to_mul : description_of Rewrite.shift_to_mul
+  := "Rewrites shl to an equivalent multiplication".
 Global Instance shift_to_mul_ok : Ok shift_to_mul.
 Proof. t; cbn in *; rewrite ?Z.shiftl_mul_pow2, ?Z.land_0_r by lia; repeat (lia + f_equal). Qed.
 
@@ -2952,6 +3123,8 @@ Definition cleanup_combine_consts : expr -> expr :=
                    | _ => e end.
 
 Definition combine_consts : expr -> expr := fun e => cleanup_combine_consts (combine_consts_pre e).
+#[local] Instance describe_combine_consts : description_of Rewrite.combine_consts
+  := "Rewrites expressions like (x + x * 5) into (x * 6)".
 
 Lemma split_consts_correct o i ls G d argsv
       (H : Forall2 (eval G d) ls argsv)
@@ -3359,47 +3532,62 @@ Qed.
 Global Instance combine_consts_Ok : Ok combine_consts.
 Proof. repeat step; apply cleanup_combine_consts_Ok, combine_consts_pre_Ok; assumption. Qed.
 
-Definition expr : expr -> expr :=
+(* M-x query-replace-regex RET \(| RewritePass\.\)\([^ ]*\) => _ RET \1\2 => \2 *)
+Definition named_pass (name : RewritePass.rewrite_pass) : expr -> expr
+  := match name with
+     | RewritePass.addbyte_small => addbyte_small
+     | RewritePass.addcarry_bit => addcarry_bit
+     | RewritePass.addcarry_small => addcarry_small
+     | RewritePass.addoverflow_bit => addoverflow_bit
+     | RewritePass.addoverflow_small => addoverflow_small
+     | RewritePass.combine_consts => combine_consts
+     | RewritePass.constprop => constprop
+     | RewritePass.consts_commutative => consts_commutative
+     | RewritePass.drop_identity => drop_identity
+     | RewritePass.flatten_associative => flatten_associative
+     | RewritePass.flatten_bounded_associative => flatten_bounded_associative
+     | RewritePass.fold_consts_to_and => fold_consts_to_and
+     | RewritePass.set_slice0_small => set_slice0_small
+     | RewritePass.set_slice_set_slice => set_slice_set_slice
+     | RewritePass.shift_to_mul => shift_to_mul
+     | RewritePass.slice0 => slice0
+     | RewritePass.slice01_addcarryZ => slice01_addcarryZ
+     | RewritePass.slice01_subborrowZ => slice01_subborrowZ
+     | RewritePass.slice_set_slice => slice_set_slice
+     | RewritePass.truncate_small => truncate_small
+     | RewritePass.unary_truncate => unary_truncate
+     | RewritePass.xor_same => xor_same
+     end.
+
+Global Instance named_pass_Ok {n} : Ok (named_pass n).
+Proof. destruct n; cbv [named_pass]; exact _. Qed.
+
+Global Instance describe_pass n : description_of (named_pass n).
+Proof.
+  destruct n; cbv [named_pass]; try exact _.
+  all: fail_if_goals_remain ().
+Defined.
+
+Definition expr {rewriting_passes : rewriting_passes_opt} : expr -> expr :=
   List.fold_left (fun e f => f e)
-  [constprop
-  ;slice0
-  ;slice01_addcarryZ
-  ;slice01_subborrowZ
-  ;set_slice_set_slice
-  ;slice_set_slice
-  ;set_slice0_small
-  ;shift_to_mul
-  ;flatten_associative
-  ;consts_commutative
-  ;fold_consts_to_and
-  ;drop_identity
-  ;flatten_bounded_associative
-  ;unary_truncate
-  ;truncate_small
-  ;combine_consts
-  ;addoverflow_bit
-  ;addcarry_bit
-  ;addcarry_small
-  ;addoverflow_small
-  ;addbyte_small
-  ;xor_same
-  ].
-
-Lemma eval_expr c d e v : eval c d e v -> eval c d (expr e) v.
-Proof using Type.
-  intros H; cbv [expr fold_left].
-  repeat lazymatch goal with
-  | H : eval ?c ?d ?e _ |- context[?r ?e] =>
-    let Hr := fresh in epose proof ((_:Ok r) _ _ _ _ H) as Hr; clear H
-  end.
-  eassumption.
+                 (List.map named_pass rewriting_passes).
+
+Local Instance expr_Ok {rewriting_passes : rewriting_passes_opt} : Ok expr.
+Proof.
+  pose proof (@named_pass_Ok).
+  cbv [expr]; induction rewriting_passes; cbn [map fold_left]; cbv [Ok] in *; eauto.
+Qed.
+
+Lemma eval_expr {rewriting_passes : rewriting_passes_opt} c d e v : eval c d e v -> eval c d (expr e) v.
+Proof.
+  apply expr_Ok.
 Qed.
 End Rewrite.
 
-Definition simplify (dag : dag) (e : node idx) :=
+Definition simplify {opts : symbolic_options_computed_opt} (dag : dag) (e : node idx) :=
   Rewrite.expr (reveal_node_at_least dag 3 e).
 
-Lemma eval_simplify G d n v : eval_node G d n v -> eval G d (simplify d n) v.
+Lemma eval_simplify {opts : symbolic_options_computed_opt} G d n v : eval_node G d n v -> eval G d (simplify d n) v.
 Proof using Type. eauto using Rewrite.eval_expr, eval_node_reveal_node_at_least. Qed.
 
 Definition reg_state := Tuple.tuple (option idx) 16.
@@ -3648,7 +3836,7 @@ Definition Store64 (a v : idx) : M unit :=
 Definition Merge {descr : description} (e : expr) : M idx := fun s =>
   let i_dag := merge e s in
   Success (fst i_dag, update_dag_with s (fun _ => snd i_dag)).
-Definition App {descr : description} (n : node idx) : M idx :=
+Definition App {opts : symbolic_options_computed_opt} {descr : description} (n : node idx) : M idx :=
   fun s => Merge (simplify s n) s.
 Definition Reveal n (i : idx) : M expr :=
   fun s => Success (reveal s n i, s).
@@ -3659,11 +3847,11 @@ Definition RevealConst (i : idx) : M Z :=
   | _ => err (error.expected_const i x)
   end.
 
-Definition GetReg {descr:description} r : M idx :=
+Definition GetReg {opts : symbolic_options_computed_opt} {descr:description} r : M idx :=
   let '(rn, lo, sz) := index_and_shift_and_bitcount_of_reg r in
   v <- GetReg64 rn;
   App ((slice lo sz), [v]).
-Definition SetReg {descr:description} r (v : idx) : M unit :=
+Definition SetReg {opts : symbolic_options_computed_opt} {descr:description} r (v : idx) : M unit :=
   let '(rn, lo, sz) := index_and_shift_and_bitcount_of_reg r in
   if N.eqb sz 64
   then v <- App (slice 0 64, [v]);
@@ -3673,7 +3861,7 @@ Definition SetReg {descr:description} r (v : idx) : M unit :=
        SetReg64 rn v.
 
 Class AddressSize := address_size : OperationSize.
-Definition Address {descr:description} {sa : AddressSize} (a : MEM) : M idx :=
+Definition Address {opts : symbolic_options_computed_opt} {descr:description} {sa : AddressSize} (a : MEM) : M idx :=
   _ <- match a.(mem_base_label) with
        | None => ret tt
        | Some l => err (error.unsupported_label_in_memory l)
@@ -3692,21 +3880,21 @@ Definition Address {descr:description} {sa : AddressSize} (a : MEM) : M idx :=
   bi <- App (add sa, [base; index]);
   App (add sa, [bi; offset]).
 
-Definition Load {descr:description} {s : OperationSize} {sa : AddressSize} (a : MEM) : M idx :=
+Definition Load {opts : symbolic_options_computed_opt} {descr:description} {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
   addr <- Address a;
   v <- Load64 addr;
   App ((slice 0 (Syntax.operand_size a s)), [v]).
 
-Definition Remove {descr:description} {s : OperationSize} {sa : AddressSize} (a : MEM) : M idx :=
+Definition Remove {opts : symbolic_options_computed_opt} {descr:description} {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
   addr <- Address a;
   v <- Remove64 addr;
   App ((slice 0 (Syntax.operand_size a s)), [v]).
 
-Definition Store {descr:description} {s : OperationSize} {sa : AddressSize} (a : MEM) v : M unit :=
+Definition Store {opts : symbolic_options_computed_opt} {descr:description} {s : OperationSize} {sa : AddressSize} (a : MEM) v : M unit :=
   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
   addr <- Address a;
@@ -3716,7 +3904,7 @@ Definition Store {descr:description} {s : OperationSize} {sa : AddressSize} (a :
   Store64 addr v.
 
 (* note: this could totally just handle truncation of constants if semanics handled it *)
-Definition GetOperand {descr:description} {s : OperationSize} {sa : AddressSize} (o : ARG) : M idx :=
+Definition GetOperand {opts : symbolic_options_computed_opt} {descr:description} {s : OperationSize} {sa : AddressSize} (o : ARG) : M idx :=
   match o with
   | Syntax.const a => App (zconst s a, [])
   | mem a => Load a
@@ -3724,7 +3912,7 @@ Definition GetOperand {descr:description} {s : OperationSize} {sa : AddressSize}
   | label l => err (error.unsupported_label_argument l)
   end.
 
-Definition SetOperand {descr:description} {s : OperationSize} {sa : AddressSize} (o : ARG) (v : idx) : M unit :=
+Definition SetOperand {opts : symbolic_options_computed_opt} {descr:description} {s : OperationSize} {sa : AddressSize} (o : ARG) (v : idx) : M unit :=
   match o with
   | Syntax.const a => err (error.set_const a v)
   | mem a => Store a v
@@ -3748,7 +3936,7 @@ Example __testPreARG_boring : ARG -> list pre_expr := fun x : ARG => @cons pre_e
 Example __testPreARG : ARG -> list pre_expr := fun x : ARG => [x].
 *)
 
-Fixpoint Symeval {descr:description} {s : OperationSize} {sa : AddressSize} (e : pre_expr) : M idx :=
+Fixpoint Symeval {opts : symbolic_options_computed_opt} {descr:description} {s : OperationSize} {sa : AddressSize} (e : pre_expr) : M idx :=
   match e with
   | PreARG o => GetOperand o
   | PreFLG f => GetFlag f
@@ -3764,7 +3952,7 @@ Definition rcrcnt s cnt : Z :=
   Z.land cnt (Z.of_N s-1).
 
 Notation "f @ ( x , y , .. , z )" := (PreApp f (@cons pre_expr x (@cons pre_expr y .. (@cons pre_expr z nil) ..))) (at level 10) : x86symex_scope.
-Definition SymexNormalInstruction {descr:description} (instr : NormalInstruction) : M unit :=
+Definition SymexNormalInstruction {opts : symbolic_options_computed_opt} {descr:description} (instr : NormalInstruction) : M unit :=
   let stack_addr_size : AddressSize := 64%N in
   let sa : AddressSize := 64%N in
   match Syntax.operation_size instr with Some s =>
@@ -3964,7 +4152,7 @@ Definition SymexNormalInstruction {descr:description} (instr : NormalInstruction
   | Some prefix => err (error.unimplemented_prefix instr) end
   | None => err (error.ambiguous_operation_size instr) end%N%x86symex.
 
-Definition SymexRawLine {descr:description} (rawline : RawLine) : M unit :=
+Definition SymexRawLine {opts : symbolic_options_computed_opt} {descr:description} (rawline : RawLine) : M unit :=
   match rawline with
   | EMPTY
   | LABEL _
@@ -3978,11 +4166,11 @@ Definition SymexRawLine {descr:description} (rawline : RawLine) : M unit :=
       => err (error.unsupported_line rawline)
   end.
 
-Definition SymexLine line :=
+Definition SymexLine {opts : symbolic_options_computed_opt} line :=
   let descr:description := Build_description (Parse.show_Line_with_line_number line) false in
   SymexRawLine line.(rawline).
 
-Fixpoint SymexLines (lines : Lines) : M unit
+Fixpoint SymexLines {opts : symbolic_options_computed_opt} (lines : Lines) : M unit
   := match lines with
      | [] => ret tt
      | line :: lines
diff --git a/src/Assembly/WithBedrock/Proofs.v b/src/Assembly/WithBedrock/Proofs.v
index c0346ce09d..7123bc7eb8 100644
--- a/src/Assembly/WithBedrock/Proofs.v
+++ b/src/Assembly/WithBedrock/Proofs.v
@@ -1450,7 +1450,7 @@ Proof.
   eapply R_subsumed; eassumption.
 Qed.
 
-Lemma build_merge_stack_placeholders_ok_R {descr:description} G s s' frame frame' ms
+Lemma build_merge_stack_placeholders_ok_R {opts : symbolic_options_computed_opt} {descr:description} G s s' frame frame' ms
       (rsp_val : Z) (stack_vals : list Z) base_stack base_stack_word_val
       (H : build_merge_stack_placeholders (List.length stack_vals) s = Success (base_stack, s'))
       (d := s.(dag_state))
@@ -1757,7 +1757,7 @@ Local Ltac handle_eval_eval :=
          end.
 
 Lemma build_merge_base_addresses_ok_R
-      {descr:description} {dereference_scalar:bool}
+      {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool}
       (idxs : list (idx + list idx))
       (reg_available : list REG)
       (runtime_reg : list Z)
@@ -1961,7 +1961,7 @@ Proof.
     all: eauto with nocore. }
 Qed.
 
-Lemma mapM_GetReg_ok_R_full {descr:description} G regs idxs reg_vals s s' frame ms
+Lemma mapM_GetReg_ok_R_full {opts : symbolic_options_computed_opt} {descr:description} G regs idxs reg_vals s s' frame ms
       (H : mapM GetReg regs s = Success (idxs, s'))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
@@ -1995,7 +1995,7 @@ Proof.
   all: eauto using R_regs_subsumed, R_flags_subsumed, R_mem_subsumed.
 Qed.
 
-Lemma mapM_GetReg_ok_R {descr:description} G regs idxs s s' frame (ms : machine_state)
+Lemma mapM_GetReg_ok_R {opts : symbolic_options_computed_opt} {descr:description} G regs idxs s s' frame (ms : machine_state)
       (H : mapM GetReg regs s = Success (idxs, s'))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
@@ -2031,7 +2031,8 @@ Proof.
   all: try solve [ cbv [R] in HR; destruct s; eapply Forall2_get_reg_of_R_regs; try assumption; try apply HR ].
 Qed.
 
-Lemma SymexLines_ok_R frame G s m asm _tt s'
+Lemma SymexLines_ok_R {opts : symbolic_options_computed_opt}
+      frame G s m asm _tt s'
       (d := s.(dag_state))
       (d' := s'.(dag_state))
       (r := s.(symbolic_reg_state))
@@ -2103,7 +2104,7 @@ Qed.
 Lemma get_asm_reg_bounded s rs : Forall (fun v => (0 <= v < 2 ^ 64)%Z) (get_asm_reg s rs).
 Proof. apply get_reg_bounded_Forall. Qed.
 
-Lemma LoadArray_ok_R {descr:description} frame G s ms s' base base_val base_word_val len idxs
+Lemma LoadArray_ok_R {opts : symbolic_options_computed_opt} {descr:description} frame G s ms s' base base_val base_word_val len idxs
       (H : LoadArray base len s = Success (idxs, s'))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
@@ -2402,7 +2403,7 @@ Proof.
                     | apply SeparationLogic.impl1_r_sep_emp; split; [ | reflexivity ] ].
 Qed.
 
-Lemma LoadOutputs_ok_R {descr:description} {dereference_scalar:bool} frame G s ms s' outputaddrs output_types output_vals idxs
+Lemma LoadOutputs_ok_R {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} frame G s ms s' outputaddrs output_types output_vals idxs
       (H : LoadOutputs (dereference_scalar:=dereference_scalar) outputaddrs output_types s = Success (Success idxs, s'))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
@@ -2823,6 +2824,7 @@ Qed.
 Local Ltac debug_run tac := tac ().
 
 Theorem symex_asm_func_M_correct
+        {opts : symbolic_options_computed_opt}
         {output_scalars_are_pointers:bool}
         d frame asm_args_out asm_args_in (G : symbol -> option Z) (s := init_symbolic_state d)
         (s' : symbolic_state) (m : machine_state) (output_types : type_spec) (stack_size : nat) (stack_base : Naive.word 64)
@@ -3267,6 +3269,7 @@ Proof.
 Time Qed. (* Finished transaction in 14.751 secs (14.751u,0.s) *)
 
 Theorem symex_asm_func_correct
+        {opts : symbolic_options_computed_opt}
         {output_scalars_are_pointers:bool}
         frame asm_args_out asm_args_in (G : symbol -> option Z) (d : dag) (output_types : type_spec) (stack_size : nat) (stack_base : Naive.word 64)
         (inputs : list (idx + list idx)) (callee_saved_registers : list REG) (reg_available : list REG) (asm : Lines)
@@ -3301,6 +3304,7 @@ Proof.
 Qed.
 
 Theorem check_equivalence_correct
+        {opts : symbolic_options_computed_opt}
         (output_scalars_are_pointers:=false)
         {assembly_calling_registers' : assembly_calling_registers_opt}
         {assembly_stack_size' : assembly_stack_size_opt}
@@ -3409,6 +3413,7 @@ Proof.
 Qed.
 
 Theorem generate_assembly_of_hinted_expr_correct
+        {opts : symbolic_options_computed_opt}
         (output_scalars_are_pointers:=false)
         {assembly_calling_registers' : assembly_calling_registers_opt}
         {assembly_stack_size' : assembly_stack_size_opt}
diff --git a/src/Assembly/WithBedrock/SymbolicProofs.v b/src/Assembly/WithBedrock/SymbolicProofs.v
index 7f467dd4a3..20935faa64 100644
--- a/src/Assembly/WithBedrock/SymbolicProofs.v
+++ b/src/Assembly/WithBedrock/SymbolicProofs.v
@@ -408,7 +408,7 @@ Ltac step_Merge :=
 Ltac step_symex2 := first [step_symex1 | step_Merge].
 Ltac step_symex ::= step_symex2.
 
-Lemma App_R {descr:description} s m (HR : R s m) e v (H : eval_node G s e v) :
+Lemma App_R {opts : symbolic_options_computed_opt} {descr:description} s m (HR : R s m) e v (H : eval_node G s e v) :
   forall i s', Symbolic.App e s = Success (i, s') ->
   R s' m /\ s :< s' /\ eval s' i v.
 Proof using Type.
@@ -470,7 +470,7 @@ Ltac step_SetFlag :=
     [eassumption|..|clear H]
   end.
 
-Lemma GetReg_R {descr:description} s m (HR: R s m) r i s'
+Lemma GetReg_R {opts : symbolic_options_computed_opt} {descr:description} s m (HR: R s m) r i s'
   (H : GetReg r s = Success (i, s'))
   : R s' m  /\ s :< s' /\ eval s' i (get_reg m r).
 Proof using Type.
@@ -492,7 +492,7 @@ Ltac step_GetReg :=
     [eassumption|..|clear H]
   end.
 
-Lemma Address_R {descr:description} s m (HR : R s m) (sa:AddressSize) o a s' (H : Symbolic.Address o s = Success (a, s'))
+Lemma Address_R {opts : symbolic_options_computed_opt} {descr:description} s m (HR : R s m) (sa:AddressSize) o a s' (H : Symbolic.Address o s = Success (a, s'))
   : R s' m /\ s :< s' /\ exists v, eval s' a v /\ @DenoteAddress sa m o = v.
 Proof using Type.
   destruct o as [? ? ? ?]; cbv [Address DenoteAddress Syntax.mem_base_reg Syntax.mem_offset Syntax.mem_scale_reg err ret] in *; repeat step_symex.
@@ -707,7 +707,7 @@ Proof using Type.
 Qed.
 
 
-Lemma GetOperand_R {descr:description} s m (HR: R s m) (so:OperationSize) (sa:AddressSize) a i s'
+Lemma GetOperand_R {opts : symbolic_options_computed_opt} {descr:description} s m (HR: R s m) (so:OperationSize) (sa:AddressSize) a i s'
   (H : GetOperand a s = Success (i, s'))
   : R s' m /\ s :< s' /\ exists v, eval s' i v /\ DenoteOperand sa so m a = Some v.
 Proof using Type.
@@ -762,7 +762,7 @@ Ltac step_GetOperand :=
   end.
 
 (* note: do the two SetOperand both truncate inputs or not?... *)
-Lemma R_SetOperand {descr:description} s m (HR : R s m)
+Lemma R_SetOperand {opts : symbolic_options_computed_opt} {descr:description} s m (HR : R s m)
   (sz:OperationSize) (sa:AddressSize) a i _tt s' (H : Symbolic.SetOperand a i s = Success (_tt, s'))
   v (Hv : eval s i v)
   : exists m', SetOperand sa sz m a v = Some m' /\ R s' m' /\ s :< s'.
@@ -1103,7 +1103,7 @@ Proof using Type.
 Qed.
 
 
-Lemma SymexNornalInstruction_R {descr:description} s m (HR : R s m) instr :
+Lemma SymexNornalInstruction_R {opts : symbolic_options_computed_opt} {descr:description} s m (HR : R s m) instr :
   forall _tt s', Symbolic.SymexNormalInstruction instr s = Success (_tt, s') ->
   exists m', Semantics.DenoteNormalInstruction m instr = Some m' /\ R s' m' /\ s :< s'.
 Proof using Type.
@@ -1354,7 +1354,7 @@ Proof using Type.
   all: fail_if_goals_remain ().
 Qed.
 
-Lemma SymexLines_R s m (HR : R s m) asm :
+Lemma SymexLines_R {opts : symbolic_options_computed_opt} s m (HR : R s m) asm :
   forall _tt s', Symbolic.SymexLines asm s = Success (_tt, s') ->
   exists m', Semantics.DenoteLines m asm = Some m' /\ R s' m' /\ s :< s'.
 Proof using Type.
diff --git a/src/CLI.v b/src/CLI.v
index ce08d1f206..99c15e6c26 100644
--- a/src/CLI.v
+++ b/src/CLI.v
@@ -7,6 +7,7 @@ Require Import Coq.Strings.HexString.
 Require Crypto.Util.Strings.String.
 Require Import Crypto.Assembly.Syntax.
 Require Import Crypto.Assembly.Parse.
+Require Import Crypto.Assembly.Symbolic.
 Require Import Crypto.Assembly.Equivalence.
 Require Import Crypto.Util.Strings.Decimal.
 Require Import Crypto.Util.Strings.ParseArithmetic.
@@ -16,8 +17,10 @@ Require Import Crypto.Util.Strings.NamingConventions.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.OptionList.
 Require Import Crypto.Util.Strings.Show.
+Require Import Crypto.Util.Strings.Sorting.
 Require Import Crypto.Util.Strings.ParseFlagOptions.
 Require Import Crypto.Util.DebugMonad.
+Require Import Crypto.Util.Listable.
 Require Crypto.PushButtonSynthesis.SaturatedSolinas.
 Require Crypto.PushButtonSynthesis.UnsaturatedSolinas.
 Require Crypto.PushButtonSynthesis.WordByWordMontgomery.
@@ -61,6 +64,9 @@ Module ForExtraction.
   Definition parse_list_REG (s : string) : option (list REG)
     := finalize (parse_comma_list parse_REG) s.
 
+  Definition parse_list_rewrite_pass (s : string) : option (list rewrite_pass)
+    := finalize (parse_comma_list parse_rewrite_pass) s.
+
   Definition parse_comma_list_Z (s : string) : option (list Z)
     := (ls <- finalize (parse_comma_list ParseArithmetic.parse_Qexpr) s;
           ls <-- List.map ParseArithmetic.eval_Qexpr_strict ls;
@@ -201,6 +207,24 @@ Module ForExtraction.
   (** This string gets parsed as the initial argument to --debug, to be updated by subsequent arguments *)
   Definition default_debug : string := "rewriting".
 
+  Definition known_asm_rewriting_pass_flags : list string
+    := Eval compute in StringSort.sort (List.map show (list_all Assembly.Symbolic.RewritePass.rewrite_pass)).
+  Definition known_asm_rewriting_pass_flags_with_spec : list (string * string)
+    := Eval compute in
+      Option.invert_Some
+        (Option.List.lift
+           (List.map
+              (fun s => p <- finalize parse_rewrite_pass s; Some (s, Assembly.Symbolic.Rewrite.describe_pass p:string))%option
+              known_asm_rewriting_pass_flags)).
+  Definition special_asm_rewriting_pass_flags : list (string * flag_option_kind)
+    := [("all", all)
+    ].
+  (** This string gets parsed as the initial argument to --asm-rewriting-passes, to be updated by subsequent arguments *)
+  Definition default_asm_rewriting_passes : string := "all".
+
+  Definition default_asm_rewriting_pipeline : string
+    := Eval compute in String.concat "," (List.map show default_rewrite_pass_order).
+
   Definition CollectErrors
              {machine_wordsize : machine_wordsize_opt}
              {output_language_api : ToString.OutputLanguageAPI}
@@ -254,6 +278,28 @@ Module ForExtraction.
   Local Notation anon_argT := (string * Arg.spec * Arg.doc)%type (only parsing).
   Local Notation named_argT := (list Arg.key * Arg.spec * Arg.doc)%type (only parsing).
 
+  Definition describe_flag_options (kind:string) (all_descr:string) (special_options : list (string * flag_option_kind)) (known_options_with_spec : list (string * string)) : list string
+    := let len := List.fold_right Nat.max 0%nat (List.map String.length (List.map fst known_options_with_spec ++ List.map fst special_options)) in
+       let fill s := (s ++ String.repeat " " (len - String.length s))%string in
+       ((["Valid " ++ kind ++ " flags:"]%string)
+          ++ (List.flat_map
+                (fun '(opt, k)
+                 => match k with
+                    | all => ["- " ++ fill opt ++ String.Tab ++ all_descr]
+                    | alias _ => []
+                    end)%string
+                special_options)
+          ++ (List.map
+                (fun '(opt, descr) => "- " ++ fill opt ++ String.Tab ++ descr)%string
+                known_options_with_spec)
+          ++ (List.flat_map
+                (fun '(opt, k)
+                 => match k with
+                    | all => []
+                    | alias ls => ["- " ++ fill opt ++ String.Tab ++ "an alias for " ++ String.concat "," ls]
+                    end)%string
+                special_options)).
+
   Definition curve_description_spec : anon_argT
     := ("curve_description",
         Arg.String,
@@ -444,7 +490,15 @@ Module ForExtraction.
   Definition asm_error_on_unique_names_mismatch_spec : named_argT
     := ([Arg.long_key "asm-error-on-unique-name-mismatch"],
         Arg.Unit,
-        ["By default, when there's only one assembly function in a --hints-file and only one function requested to be synthesized, the name of the assembly function is ignored.  Passing this flag disables this behavior, raising an error if the names mismatch regardless of whether there are multiple functions or just one."]).
+         ["By default, when there's only one assembly function in a --hints-file and only one function requested to be synthesized, the name of the assembly function is ignored.  Passing this flag disables this behavior, raising an error if the names mismatch regardless of whether there are multiple functions or just one."]).
+  Definition asm_rewriting_pipeline_spec : named_argT
+    := ([Arg.long_key "asm-rewriting-pipeline"],
+         Arg.Custom (parse_string_and parse_list_rewrite_pass) "REWRITE_PASS",
+         ["Specifies the order and multiplicity of rewriting passes used in the assembly equivalence checker.  Default: " ++ default_asm_rewriting_passes]).
+  Definition asm_rewriting_passes_spec : named_argT
+    := ([Arg.long_key "asm-rewriting-passes"],
+         Arg.String,
+         ["A comma-separated list of rewriting passes to enable.  Prefix with - to disable a pass.  This list only impacts passes listed in --asm-rewriting-pipeline.  Default : " ++ (if default_asm_rewriting_passes =? "" then "(none)" else default_asm_rewriting_passes)]%string ++ describe_flag_options "rewriting pass" "Enable all rewriting passes" special_asm_rewriting_pass_flags known_asm_rewriting_pass_flags_with_spec)%list.
   Definition doc_text_before_function_name_spec : named_argT
     := ([Arg.long_key "doc-text-before-function-name"],
         Arg.String,
@@ -470,29 +524,9 @@ Module ForExtraction.
         Arg.String,
         ["Documentation Option: Prepend a line at the beginning of the documentation header at the top of the file.  This argument can be passed multiple times to insert multiple lines.  Lines will be automatically commented."]).
   Definition debug_spec : named_argT
-    := let len := List.fold_right Nat.max 0%nat (List.map String.length (known_debug_options ++ List.map fst special_debug_options)) in
-       let fill s := (s ++ String.repeat " " (len - String.length s))%string in
-       ([Arg.long_key "debug"; Arg.short_key "d"],
+    := ([Arg.long_key "debug"; Arg.short_key "d"],
          Arg.String,
-         (["A comma-separated list of debug options to turn on.  Use - to disable an option.  Default debug options: " ++ (if default_debug =? "" then "(none)" else default_debug)
-           ; "Valid debug options:"]%string)
-           ++ (List.flat_map
-                 (fun '(opt, k)
-                  => match k with
-                     | all => ["- " ++ fill opt ++ String.Tab ++ "Turn all debugging on"]
-                     | alias _ => []
-                     end)%string
-                 special_debug_options)
-           ++ (List.map
-                 (fun '(opt, descr) => "- " ++ fill opt ++ String.Tab ++ descr)%string
-                 known_debug_options_with_spec)
-           ++ (List.flat_map
-                 (fun '(opt, k)
-                  => match k with
-                     | all => []
-                     | alias ls => ["- " ++ fill opt ++ String.Tab ++ "an alias for " ++ String.concat "," ls]
-                     end)%string
-                 special_debug_options))%list.
+         (["A comma-separated list of debug options to turn on.  Use - to disable an option.  Default debug options: " ++ (if default_debug =? "" then "(none)" else default_debug)]%string ++ describe_flag_options "debug" "Turn all debugging on" special_debug_options known_debug_options_with_spec))%list.
 
   Definition collapse_list_default {A} (default : A) (ls : list A)
     := List.hd default (List.rev ls).
@@ -645,6 +679,8 @@ Module ForExtraction.
         ; asm_input_first_spec
         ; asm_reg_rtl_spec
         ; asm_error_on_unique_names_mismatch_spec
+        ; asm_rewriting_pipeline_spec
+        ; asm_rewriting_passes_spec
         ; doc_text_before_function_name_spec
         ; doc_text_before_type_name_spec
         ; doc_newline_before_package_declaration_spec
@@ -700,6 +736,8 @@ Module ForExtraction.
              , asm_input_firstv
              , asm_reg_rtlv
              , asm_error_on_unique_names_mismatchv
+             , asm_rewriting_pipelinev
+             , asm_rewriting_passesv
              , doc_text_before_function_namev
              , doc_text_before_type_namev
              , doc_newline_before_package_declarationv
@@ -717,6 +755,11 @@ Module ForExtraction.
                              | nil => None
                              | ls => Some (List.concat ls)
                              end in
+       let to_rewriting_pipeline_list ls
+         := match List.map (@snd _ _) (List.map (@snd _ _) ls) with
+            | nil => default_rewrite_pass_order
+            | ls => List.concat ls
+            end in
        let to_assembly_callee_saved_registers_opt ls := choose_one_of_many (List.map (fun '(_, (_, v)) => v) ls) in
        let to_assembly_callee_saved_registers_default ls default := Option.value (to_assembly_callee_saved_registers_opt ls) default in
        let to_N_opt ls := choose_one_of_many (to_N_list ls) in
@@ -728,6 +771,8 @@ Module ForExtraction.
            := option_map (fun d => {| capitalization_convention_data := d ; only_lower_first_letters := true |})
                          (to_capitalization_data_opt ls) in
        let '(_, unknown_debug_options, (debug_on_successv, debug_rewritingv)) := parse_flag_opts special_debug_options known_debug_options (default_debug :: List.map snd debugv) in
+       let default_asm_rewriting_pass_status := true (* default status of non-explicit passes; it doesn't actually matter because we're going to control the default with default_asm_rewriting_passes *) in
+       let '(unknown_asm_rewriting_passes, asm_rewriting_pass_filterv) := parse_flag_opts_to_bool_filter default_asm_rewriting_pass_status special_asm_rewriting_pass_flags known_asm_rewriting_pass_flags (default_asm_rewriting_passes :: List.map snd asm_rewriting_passesv) in
        let res
            := ({|
                   hint_file_names := to_string_list hint_file_namesv
@@ -775,6 +820,10 @@ Module ForExtraction.
                       ; assembly_output_first_ := negb (to_bool asm_input_firstv)
                       ; assembly_argument_registers_left_to_right_ := negb (to_bool asm_reg_rtlv)
                       |}
+                    ; symbolic_options_ :=
+                      {| asm_rewriting_pipeline := to_rewriting_pipeline_list asm_rewriting_pipelinev
+                      ; asm_rewriting_pass_filter := fun p => asm_rewriting_pass_filterv (show_rewrite_pass p)
+                      |}
                     |}
                   ; ignore_unique_asm_names := negb (to_bool asm_error_on_unique_names_mismatchv)
                   ; error_on_unused_assembly_functions := negb (to_bool no_error_on_unused_asm_functionsv)
@@ -790,12 +839,23 @@ Module ForExtraction.
                   ; debug_on_success := flag_to_bool debug_on_successv
                |},
                snd (List.hd lang_default langv)) in
-       match langv, unknown_debug_options with
-       | ([] | [_]), [] => inl res
-       | _ :: _ :: _, _ => inr ["Only one language specification with --lang is allowed; multiple languages were requested: " ++ String.concat ", " (List.map (@fst _ _) langv)]
-       | _, _ :: _
-         => inr ["Unrecognized debug option" ++ (if (1 <? List.length unknown_debug_options)%nat then "s" else "") ++ ": " ++ String.concat ", " (List.map fst unknown_debug_options)]
-       end.
+       let unknown_errs descr sing_suffix plural_suffix arg unknown_opts
+         := match unknown_opts with
+            | [] => []
+            | _ :: _ => ["Unrecognized " ++ descr ++ (if (1 <? List.length unknown_opts)%nat then plural_suffix else sing_suffix) ++ " (from " ++ arg ++ "): " ++ String.concat ", " (List.map fst unknown_opts)]
+            end in
+       let lang_errs
+         := match langv with
+            | [] | [_] => []
+            | _ :: _ :: _ => ["Only one language specification with --lang is allowed; multiple languages were requested: " ++ String.concat ", " (List.map (@fst _ _) langv)]
+            end in
+       match lang_errs
+               ++ unknown_errs "debug flag" "" "s" "--debug" unknown_debug_options
+               ++ unknown_errs "assembly rewriting pass" "" "es" "--asm-rewriting-passes" unknown_asm_rewriting_passes
+       with
+       | [] => inl res
+       | errs => inr errs
+       end%list.
 
   (** We define a class for the various operations that are specific to a pipeline *)
   Class PipelineAPI :=
diff --git a/src/StandaloneDebuggingExamples.v b/src/StandaloneDebuggingExamples.v
index 83aead8538..0cabb7f19b 100644
--- a/src/StandaloneDebuggingExamples.v
+++ b/src/StandaloneDebuggingExamples.v
@@ -26,7 +26,8 @@ Module debugging_no_asm.
     cbv [ForExtraction.hint_file_names] in v.
     cbn [map fst snd] in v.
     vm_compute ParseFlagOptions.parse_flag_opts in v.
-    cbv beta iota in v.
+    vm_compute ParseFlagOptions.parse_flag_opts_to_bool_filter in v.
+    cbn [List.app] in v.
     cbn [ForExtraction.with_read_concat_asm_files_cps] in v.
     set (k := ForExtraction.with_read_file "t.asm") in (value of v).
     assert (k = (fun k => k ["SECTION .text"
@@ -125,7 +126,8 @@ Module debugging_typedef_bounds.
     cbv [ForExtraction.hint_file_names] in v.
     cbn [map] in v.
     vm_compute ParseFlagOptions.parse_flag_opts in v.
-    cbv beta iota in v.
+    vm_compute ParseFlagOptions.parse_flag_opts_to_bool_filter in v.
+    cbn [List.app] in v.
     cbn [ForExtraction.with_read_concat_asm_files_cps] in v.
     vm_compute ForExtraction.parse_args in v.
     cbv beta iota zeta in v.
diff --git a/src/Util/Strings/ParseFlagOptions.v b/src/Util/Strings/ParseFlagOptions.v
index 41df38f283..1d9fc1d3b4 100644
--- a/src/Util/Strings/ParseFlagOptions.v
+++ b/src/Util/Strings/ParseFlagOptions.v
@@ -87,9 +87,31 @@ Definition post_parse_flag_opts (known_options : list string) (status : full_fla
      let unknown_options := List.filter (fun '(opt, _) => negb (StringSet.mem opt known_options_set)) (StringMap.elements status) in
      (all_status, unknown_options, format_flag_opts known_options status).
 
+Definition post_parse_flag_opts_to_filter (known_options : list string) (status : full_flag_status (* all status *) * StringMap.t flag_status)
+  : full_flag_status (* all status *) * list (string * flag_status) (* unknown options *) * (string -> full_flag_status)
+  := let '(all_status, status) := status in
+     let known_options_set := List.fold_right StringSet.add StringSet.empty known_options in
+     let unknown_options := List.filter (fun '(opt, _) => negb (StringSet.mem opt known_options_set)) (StringMap.elements status) in
+     (all_status, unknown_options, fun s => match StringMap.find s status with
+                                            | Some s => explicit s
+                                            | None => elided
+                                            end).
+
 Definition parse_flag_opts (spec : list (string * flag_option_kind)) (known_options : list string) (args : list string)
   : full_flag_status (* all status *) * list (string * flag_status) (* unknown options *) * Tuple.tuple full_flag_status (List.length known_options)
   := let res := preparse_flag_opts spec args in
      let res := aggregate_flag_opts res in
      let res := post_parse_flag_opts known_options res in
      res.
+
+Definition parse_flag_opts_to_filter (spec : list (string * flag_option_kind)) (known_options : list string) (args : list string)
+  : full_flag_status (* all status *) * list (string * flag_status) (* unknown options *) * (string -> full_flag_status)
+  := let res := preparse_flag_opts spec args in
+     let res := aggregate_flag_opts res in
+     let res := post_parse_flag_opts_to_filter known_options res in
+     res.
+
+Definition parse_flag_opts_to_bool_filter (default : bool) (spec : list (string * flag_option_kind)) (known_options : list string) (args : list string)
+  : list (string * flag_status) (* unknown options *) * (string -> bool)
+  := let '(all_status, unknown, filter) := parse_flag_opts_to_filter spec known_options args in
+     (unknown, fun s => bool_of_full_flag_status (filter s) default).