diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v
index bf5dc1f3fc..4cce3b8915 100644
--- a/src/Assembly/Equivalence.v
+++ b/src/Assembly/Equivalence.v
@@ -4,6 +4,7 @@ From Coq Require Import ZArith.
 From Coq Require Import NArith.
 Require Import Crypto.Assembly.Syntax.
 Require Import Crypto.Assembly.Parse.
+Require Import Crypto.Assembly.Equality.
 Require Import Crypto.Assembly.Symbolic.
 Require Import Crypto.Util.Strings.Parse.Common.
 Require Import Crypto.Util.ErrorT.
@@ -277,8 +278,8 @@ Definition show_annotated_Line : Show AnnotatedLine
               end)%string.
 
 Global Instance show_lines_AnnotatedLines : ShowLines AnnotatedLines
-  := fun '(ls, ss)
-     => let d := dag.eager.force ss.(dag_state) in
+  := fun '(ls, sst)
+     => let d := dag.eager.force sst.(dag_state) in
         List.map (fun l => show_annotated_Line (l, d)) ls.
 
 Fixpoint remove_common_indices {T} (eqb : T -> T -> bool) (xs ys : list T) (start_idx : nat) : list (nat * T) * list T
@@ -731,11 +732,11 @@ Global Instance show_lines_EquivalenceCheckingError : ShowLines EquivalenceCheck
 Global Instance show_EquivalenceCheckingError : Show EquivalenceCheckingError
   := fun err => String.concat String.NewLine (show_lines err).
 
-Definition merge_fresh_symbol {descr:description} : dag.M idx := fun d => merge_node (dag.gensym 64%N d) d.
+Definition merge_fresh_symbol {descr:description} (sz : OperationSize) : dag.M idx := fun d => merge_node (dag.gensym sz d) d.
 Definition merge_literal {descr:description} (l:Z) : dag.M idx := merge_node ((const l, nil)).
 
 Definition SetRegFresh {opts : symbolic_options_computed_opt} {descr:description} (r : REG) : M idx :=
-  (idx <- lift_dag merge_fresh_symbol;
+  (idx <- lift_dag (merge_fresh_symbol (widest_reg_size_of r));
   _ <- SetReg r idx;
   Symbolic.ret idx).
 
@@ -812,13 +813,13 @@ Fixpoint simplify_input_type
      end%error.
 
 Definition build_inputarray {descr:description} (len : nat) : dag.M (list idx) :=
-  List.foldmap (fun _ => merge_fresh_symbol) (List.seq 0 len).
+  List.foldmap (fun _ => merge_fresh_symbol 64%N) (List.seq 0 len).
 
 Fixpoint build_inputs {descr:description} (types : type_spec) : dag.M (list (idx + list idx))
   := match types with
      | [] => dag.ret []
      | None :: tys
-       => (idx <- merge_fresh_symbol;
+       => (idx <- merge_fresh_symbol 64%N;
            rest <- build_inputs tys;
            dag.ret (inl idx :: rest))
      | Some len :: tys
@@ -858,12 +859,12 @@ Fixpoint build_merge_base_addresses {opts : symbolic_options_computed_opt} {desc
            Symbolic.ret (inl addr :: rest))
      end%N%x86symex.
 
-Fixpoint dag_gensym_n {descr:description} (n : nat) : dag.M (list symbol) :=
-  match n with
-  | O => dag.ret nil
-  | S n =>
-      (i <- merge_fresh_symbol;
-       rest <- dag_gensym_n n;
+Fixpoint dag_gensym_ls {descr:description} (ls : list OperationSize) : dag.M (list symbol) :=
+  match ls with
+  | nil => dag.ret nil
+  | sz :: ls =>
+      (i <- merge_fresh_symbol sz;
+       rest <- dag_gensym_ls ls;
        dag.ret (cons i rest))
   end%dagM.
 
@@ -1275,7 +1276,7 @@ Definition init_symbolic_state_descr : description := Build_description "init_sy
 
 Definition init_symbolic_state (d : dag) : symbolic_state
   := let _ := init_symbolic_state_descr in
-     let '(initial_reg_idxs, d) := dag_gensym_n (List.length widest_registers) d in
+     let '(initial_reg_idxs, d) := dag_gensym_ls (List.map reg_size widest_registers) d in
      {|
        dag_state := d;
        symbolic_reg_state := Tuple.from_list_default None _ (List.map Some initial_reg_idxs);
diff --git a/src/Assembly/EquivalenceProofs.v b/src/Assembly/EquivalenceProofs.v
index b885f1bd8c..5506bd6f6b 100644
--- a/src/Assembly/EquivalenceProofs.v
+++ b/src/Assembly/EquivalenceProofs.v
@@ -915,11 +915,11 @@ Module dagG.
   Definition M A := (symbol -> option Z) * dag -> A * ((symbol -> option Z) * dag).
 End dagG.
 
-Definition merge_fresh_symbol_G {descr:description} (v : Z) : dagG.M idx
-  := fun '(G, d) => let '(idx, d) := merge_fresh_symbol d in (idx, (ctx_set idx v G, d)).
+Definition merge_fresh_symbol_G {descr:description} (size : OperationSize) (v : Z) : dagG.M idx
+  := fun '(G, d) => let '(idx, d) := merge_fresh_symbol size d in (idx, (ctx_set idx v G, d)).
 
 Definition build_inputarray_G {descr:description} (vals : list Z) : dagG.M (list idx)
-  := List.foldmap merge_fresh_symbol_G vals.
+  := List.foldmap (merge_fresh_symbol_G 64%N) vals.
 
 Fixpoint build_inputs_G {descr:description} (vals : list (Z + list Z))
   : dagG.M (list (idx + list idx))
@@ -932,18 +932,19 @@ Fixpoint build_inputs_G {descr:description} (vals : list (Z + list Z))
              (inr idxs :: rest, st)
      | inl v :: args
        => fun st
-          => let '(idx, st) := merge_fresh_symbol_G v st in
+          => let '(idx, st) := merge_fresh_symbol_G 64%N v st in
              let '(rest, st) := build_inputs_G args st in
              (inl idx :: rest, st)
      end.
 
-Fixpoint dag_gensym_n_G {descr:description} (vals : list Z) : dagG.M (list idx)
-  := match vals with
-     | nil => fun st => ([], st)
-     | v :: vs
+Fixpoint dag_gensym_ls_G {descr:description} (sizes : list OperationSize) (vals : list Z) : dagG.M (list idx)
+  := match sizes, vals with
+     | nil, nil => fun st => ([], st)
+     | nil, _ :: _ | _ :: _, nil => fun st => ([], st)
+     | size :: sizes, v :: vs
        => fun st
-          => let '(idx, st) := merge_fresh_symbol_G v st in
-             let '(rest, st) := dag_gensym_n_G vs st in
+          => let '(idx, st) := merge_fresh_symbol_G size v st in
+             let '(rest, st) := dag_gensym_ls_G sizes vs st in
              (idx :: rest, st)
      end.
 
@@ -968,7 +969,7 @@ Definition lift_dag_G {A} (v : dagG.M A) : G.M A
                     Some (v, (G, update_dag_with s (fun _ => d))).
 
 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);
+  := (idx <- lift_dag_G (merge_fresh_symbol_G (widest_reg_size_of r) v);
       _ <- G.lift (SetReg r idx);
       G.ret idx)%GM.
 
@@ -1107,17 +1108,17 @@ Proof.
   all: intros; break_match; intuition.
 Qed.
 
-Lemma merge_fresh_symbol_eq_G {descr:description} G d v
-      (res := merge_fresh_symbol_G v (G, d))
-  : merge_fresh_symbol d = (fst res, snd (snd res)).
+Lemma merge_fresh_symbol_eq_G {descr:description} G sz d v
+      (res := merge_fresh_symbol_G sz v (G, d))
+  : merge_fresh_symbol sz d = (fst res, snd (snd res)).
 Proof.
   subst res; cbv [merge_fresh_symbol_G]; break_innermost_match; reflexivity.
 Qed.
 
-Lemma merge_fresh_symbol_G_ok {descr:description} G d v G' d' idx
+Lemma merge_fresh_symbol_G_ok {descr:description} G sz d v G' d' idx
       (Hd : gensym_dag_ok G d)
-      (H : merge_fresh_symbol_G v (G, d) = (idx, (G', d')))
-  : eval_idx_Z G' d' idx (Z.land v (Z.ones (Z.of_N 64)))
+      (H : merge_fresh_symbol_G sz v (G, d) = (idx, (G', d')))
+  : eval_idx_Z G' d' idx (Z.land v (Z.ones (Z.of_N sz)))
     /\ gensym_dag_ok G' d'
     /\ (forall e n, eval G d e n -> eval G' d' e n).
 Proof.
@@ -1177,15 +1178,16 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma merge_fresh_symbol_G_ok_bounded {descr:description} G d v G' d' idx
+Lemma merge_fresh_symbol_G_ok_bounded {descr:description} G sz d v G' d' idx
       (Hd : gensym_dag_ok G d)
-      (H : merge_fresh_symbol_G v (G, d) = (idx, (G', d')))
-      (Hv : (0 <= v < 2^64)%Z)
+      (H : merge_fresh_symbol_G sz v (G, d) = (idx, (G', d')))
+      (Hv : (0 <= v < 2^Z.of_N sz)%Z)
   : eval_idx_Z G' d' idx v
     /\ gensym_dag_ok G' d'
     /\ (forall e n, eval G d e n -> eval G' d' e n).
 Proof.
-  replace v with (Z.land v (Z.ones (Z.of_N 64))); [ now apply merge_fresh_symbol_G_ok | rewrite land_ones_eq_of_bounded by assumption ].
+  subst.
+  replace v with (Z.land v (Z.ones (Z.of_N sz))); [ now apply merge_fresh_symbol_G_ok | rewrite land_ones_eq_of_bounded by assumption ].
   reflexivity.
 Qed.
 
@@ -1225,8 +1227,8 @@ Proof.
                  | match goal with
                    | [ H : ?x :: ?xs = ?y :: ?ys |- _ ] => assert (x = y /\ xs = ys) by (now inversion H; split); clear H
                    end ].
-    let lem := match goal with |- context[merge_fresh_symbol_G ?v (?G, ?d)] => constr:(merge_fresh_symbol_G_ok_bounded G d v) end in
-    pose proof (lem _ _ _ ltac:(assumption) ltac:(repeat rewrite <- surjective_pairing; reflexivity) ltac:(lia)).
+    let lem := match goal with |- context[merge_fresh_symbol_G ?sz ?v (?G, ?d)] => constr:(merge_fresh_symbol_G_ok_bounded G sz d v) end in
+    epose proof (lem _ _ _ ltac:(assumption) ltac:(repeat rewrite <- surjective_pairing; reflexivity) ltac:(lia)).
     repeat first [ progress subst
                  | progress destruct_head'_and
                  | assumption
@@ -1254,33 +1256,30 @@ Proof.
   repeat first [ eassumption | apply path_prod | reflexivity ].
 Qed.
 
-Lemma dag_gensym_n_eq_G {descr:description} G d vals (len := List.length vals)
-  : dag_gensym_n len d = (fst (dag_gensym_n_G vals (G, d)), snd (snd (dag_gensym_n_G vals (G, d)))).
+Lemma dag_gensym_ls_eq_G {descr:description} G d ls vals (Hlen : List.length vals = List.length ls)
+  : dag_gensym_ls ls d = (fst (dag_gensym_ls_G ls vals (G, d)), snd (snd (dag_gensym_ls_G ls vals (G, d)))).
 Proof.
-  subst len.
-  revert G d; induction vals as [|v vals IHvals]; cbn [dag_gensym_n dag_gensym_n_G fst snd List.length]; [ reflexivity | ]; intros.
+  revert G d vals Hlen; induction ls as [|sz ls IH], vals; cbn [dag_gensym_ls dag_gensym_ls_G fst snd List.length]; try reflexivity; intros; try congruence; [].
   cbv [dag.bind dag.ret]; eta_expand; cbn [fst snd].
-  erewrite !@merge_fresh_symbol_eq_G, IHvals; cbn [fst snd]; eta_expand; reflexivity.
+  erewrite !@merge_fresh_symbol_eq_G, IH; cbn [fst snd]; eta_expand; try reflexivity; congruence.
 Qed.
 
-Lemma dag_gensym_n_G_ok {descr:description} G d vals G' d' ia
+Lemma dag_gensym_ls_G_ok {descr:description} G d ls vals G' d' ia
       (Hd : gensym_dag_ok G d)
-      (H : dag_gensym_n_G vals (G, d) = (ia, (G', d')))
-      (Hbounds : Forall (fun v => (0 <= v < 2^64)%Z) vals)
+      (H : dag_gensym_ls_G ls vals (G, d) = (ia, (G', d')))
+      (Hbounds : Forall2 (fun sz v => (0 <= v < 2^Z.of_N sz)%Z) ls vals)
   : Forall2 (eval_idx_Z G' d') ia vals
     /\ gensym_dag_ok G' d'
     /\ (forall e n, eval G d e n -> eval G' d' e n).
 Proof.
   revert ia G d G' d' Hd H.
-  induction vals as [|v vals IHvals], ia as [|i ia]; cbn [dag_gensym_n_G]; intros;
+  induction Hbounds as [|???? Hbound Hbounds IH], ia as [|i ia]; cbn [dag_gensym_ls_G]; intros;
     try solve [ inversion_prod; subst; eta_expand; cbn [fst snd] in *; eauto; try congruence ].
   { break_innermost_match_hyps.
-    inversion Hbounds; subst; clear Hbounds.
-    destruct_head'_prod.
-    specialize (fun H => IHvals ltac:(assumption) _ _ _ _ _ H ltac:(eassumption)).
-    match goal with H : pair _ _ = pair _ _ |- _ => inversion H; clear H end; subst.
-    let lem := match goal with H : context[merge_fresh_symbol_G ?v (?G, ?d)] |- _ => constr:(merge_fresh_symbol_G_ok_bounded G d v) end in
-    pose proof (lem _ _ _ ltac:(assumption) ltac:(eassumption) ltac:(lia)).
+    inversion_prod; inversion_list; subst.
+    let lem := match goal with |- context[merge_fresh_symbol_G ?sz ?v (?G, ?d)] => constr:(merge_fresh_symbol_G_ok_bounded G sz d v) end in
+    pose proof (lem _ _ _ ltac:(assumption) ltac:(repeat rewrite <- surjective_pairing; reflexivity) ltac:(lia)) as H'.
+    specialize (IH _ _ _ _ _ ltac:(apply H') ltac:(repeat rewrite <- surjective_pairing; reflexivity)).
     destruct_head'_and; specialize_by_assumption.
     repeat first [ progress subst
                  | progress destruct_head'_and
@@ -1295,18 +1294,18 @@ Proof.
                    end ]. }
 Qed.
 
-Lemma dag_gensym_n_ok {descr:description} G d len idxs args d'
+Lemma dag_gensym_ls_ok {descr:description} G d ls idxs args d'
       (d_ok : gensym_dag_ok G d)
-      (H : dag_gensym_n len d = (idxs, d'))
-      (Hargs : List.length args = len)
-      (Hbounds : Forall (fun v => (0 <= v < 2^64)%Z) args)
+      (H : dag_gensym_ls ls d = (idxs, d'))
+      (Hargs : List.length args = List.length ls)
+      (Hbounds : Forall2 (fun sz v => (0 <= v < 2^Z.of_N sz)%Z) ls args)
   : exists G',
     Forall2 (eval_idx_Z G' d') idxs args
     /\ gensym_dag_ok G' d'
     /\ (forall e n, eval G d e n -> eval G' d' e n).
 Proof.
-  subst len; erewrite dag_gensym_n_eq_G in H; inversion_prod.
-  eexists; eapply dag_gensym_n_G_ok; try eassumption.
+  erewrite dag_gensym_ls_eq_G in H by eassumption; inversion_prod.
+  eexists; eapply dag_gensym_ls_G_ok; try eassumption.
   repeat first [ eassumption | apply path_prod | reflexivity ].
 Qed.
 
@@ -1333,7 +1332,7 @@ Proof.
                     | reflexivity
                     | match goal with
                       | [ H : pair _ _ = pair _ _ |- _ ] => inversion H; clear H
-                      | [ H : merge_fresh_symbol _ = _, H' : merge_fresh_symbol_G _ _ = _ |- _ ] => erewrite merge_fresh_symbol_eq_G, H' in H
+                      | [ H : merge_fresh_symbol _ _ = _, H' : merge_fresh_symbol_G _ _ _ = _ |- _ ] => erewrite merge_fresh_symbol_eq_G, H' in H
                       | [ H : build_inputarray _ _ = _, H' : build_inputarray_G _ _ = _ |- _ ] => erewrite build_inputarray_eq_G, H' in H
                       | [ H : build_inputs _ _ = _, H' : build_inputs_G _ _ = _ |- _ ] => erewrite IHvals, H' in H
                       end ].
@@ -1359,7 +1358,7 @@ Proof.
                       | solve [ eauto ]
                       | match goal with
                         | [ H : ?x :: ?xs = ?y :: ?ys |- _ ] => assert (x = y /\ xs = ys) by (now inversion H; split); clear H
-                        | [ H : merge_fresh_symbol_G _ _ = _ |- _ ] => apply merge_fresh_symbol_G_ok_bounded in H; [ | (assumption  + lia) .. ]
+                        | [ H : merge_fresh_symbol_G _ _ _ = _ |- _ ] => apply merge_fresh_symbol_G_ok_bounded in H; [ | (assumption  + lia) .. ]
                         | [ H : build_inputarray_G _ _ = _ |- _ ] => apply build_inputarray_G_ok in H; [ | assumption .. ]
                         | [ H : build_inputs_G _ _ = _ |- _ ] => apply IHvals in H; [ | assumption .. ]
                         | [ H : Forall _ (_ :: _) |- _ ] => inversion H; clear H
@@ -1535,7 +1534,8 @@ Qed.
 
 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)
+      (width := reg_size (widest_register_of_index rn))
+      (Hwide : sz = width)
       (H : SetReg reg idx s = Success (tt, s'))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
@@ -1549,13 +1549,13 @@ Lemma SetReg_ok {opts : symbolic_options_computed_opt} {descr:description} G s s
       (Hidx : eval_idx_Z G d idx v)
   : ((exists idx',
          set_reg r rn idx' = r'
-         /\ eval_idx_Z G d' idx' (Z.land v (Z.ones 64)))
+         /\ eval_idx_Z G d' idx' (Z.land v (Z.ones (Z.of_N width))))
      /\ f = f'
      /\ m = m')
     /\ gensym_dag_ok G d'
     /\ (forall e n, eval G d e n -> eval G d' e n).
 Proof.
-  cbv [SetReg Symbolic.bind ErrorT.bind Crypto.Util.Option.bind GetReg SetReg64] in *.
+  cbv [SetReg Symbolic.bind ErrorT.bind Crypto.Util.Option.bind GetReg SetRegFull] in *.
   break_match_hyps.
   all: repeat first [ progress inversion_option
                     | progress cbn [fst snd dag_state symbolic_reg_state symbolic_flag_state symbolic_mem_state] in *
@@ -1595,7 +1595,8 @@ Qed.
 
 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)
+      (width := reg_size (widest_register_of_index rn))
+      (Hwide : sz = width)
       (H : SetReg reg idx s = Success (tt, s'))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
@@ -1607,7 +1608,7 @@ Lemma SetReg_ok_bounded {opts : symbolic_options_computed_opt} {descr:descriptio
       (m' := s'.(symbolic_mem_state))
       (Hd : gensym_dag_ok G d)
       (Hidx : eval_idx_Z G d idx v)
-      (Hv : (0 <= v < 2^64)%Z)
+      (Hv : (0 <= v < 2^Z.of_N width)%Z)
   : ((exists idx',
          set_reg r rn idx' = r'
          /\ eval_idx_Z G d' idx' v)
@@ -1616,13 +1617,14 @@ Lemma SetReg_ok_bounded {opts : symbolic_options_computed_opt} {descr:descriptio
     /\ gensym_dag_ok G d'
     /\ (forall e n, eval G d e n -> eval G d' e n).
 Proof.
-  replace v with (Z.land v (Z.ones (Z.of_N 64))); [ eapply SetReg_ok; eassumption | rewrite land_ones_eq_of_bounded by assumption ].
+  replace v with (Z.land v (Z.ones (Z.of_N width))); [ eapply SetReg_ok; eassumption | rewrite land_ones_eq_of_bounded by assumption ].
   reflexivity.
 Qed.
 
 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)
+      (width := reg_size (widest_register_of_index rn))
+      (Hwide : sz = width)
       (H : SetRegFresh_G reg v (G, s) = Some (idx, (G', s')))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
@@ -1633,10 +1635,10 @@ Lemma SetRegFresh_G_ok {opts : symbolic_options_computed_opt} {descr:description
       (m := s.(symbolic_mem_state))
       (m' := s'.(symbolic_mem_state))
       (Hd : gensym_dag_ok G d)
-  : (eval_idx_Z G' d' idx (Z.land v (Z.ones 64))
+  : (eval_idx_Z G' d' idx (Z.land v (Z.ones (Z.of_N width)))
      /\ (exists idx',
             set_reg r rn idx' = r'
-            /\ eval_idx_Z G' d' idx' (Z.land v (Z.ones 64)))
+            /\ eval_idx_Z G' d' idx' (Z.land v (Z.ones (Z.of_N width))))
      /\ f = f'
      /\ m = m')
     /\ gensym_dag_ok G' d'
@@ -1652,11 +1654,12 @@ Proof.
                | progress subst_prod
                | progress cbv [update_dag_with] in *
                | progress cbn [dag_state symbolic_reg_state symbolic_flag_state symbolic_mem_state] in *
+               | progress cbv [index_and_shift_and_bitcount_of_reg] in *
                | rewrite Z.land_same_r in *
                | solve [ cbv [eval_idx_Z] in *; eauto ]
                | match goal with
                  | [ H := _ |- _ ] => subst H
-                 | [ H : merge_fresh_symbol_G _ _ = _ |- _ ]
+                 | [ H : merge_fresh_symbol_G _ _ _ = _ |- _ ]
                    => apply merge_fresh_symbol_G_ok in H; [ | assumption .. ]
                  | [ H : SetReg _ _ _ = _ |- _ ]
                    => eapply SetReg_ok in H;
@@ -1667,8 +1670,9 @@ Proof.
 Qed.
 
 Lemma SetRegFresh_G_ok_bounded {opts : symbolic_options_computed_opt} {descr:description} G G' s s' reg idx rn lo sz v
+      (width := widest_reg_size_of reg)
       (Hreg : index_and_shift_and_bitcount_of_reg reg = (rn, lo, sz))
-      (H64 : sz = 64%N)
+      (Hwidth : sz = width)
       (H : SetRegFresh_G reg v (G, s) = Some (idx, (G', s')))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
@@ -1679,7 +1683,7 @@ Lemma SetRegFresh_G_ok_bounded {opts : symbolic_options_computed_opt} {descr:des
       (m := s.(symbolic_mem_state))
       (m' := s'.(symbolic_mem_state))
       (Hd : gensym_dag_ok G d)
-      (Hv : (0 <= v < 2^64)%Z)
+      (Hv : (0 <= v < 2^Z.of_N width)%Z)
   : (eval_idx_Z G' d' idx v
      /\ (exists idx',
             set_reg r rn idx' = r'
@@ -1689,13 +1693,16 @@ Lemma SetRegFresh_G_ok_bounded {opts : symbolic_options_computed_opt} {descr:des
     /\ gensym_dag_ok G' d'
     /\ (forall e n, eval G d e n -> eval G' d' e n).
 Proof.
-  replace v with (Z.land v (Z.ones (Z.of_N 64))); [ eapply SetRegFresh_G_ok; eassumption | rewrite land_ones_eq_of_bounded by assumption ].
+  cbv [widest_reg_size_of index_and_shift_and_bitcount_of_reg] in *.
+  inversion_prod; subst.
+  replace v with (Z.land v (Z.ones (Z.of_N width))); [ eapply SetRegFresh_G_ok; try eassumption; reflexivity | rewrite land_ones_eq_of_bounded by assumption ].
   reflexivity.
 Qed.
 
 Lemma GetReg_ok {opts : symbolic_options_computed_opt} {descr:description} G s s' reg idx rn lo sz v
+      (width := widest_reg_size_of reg)
       (Hreg : index_and_shift_and_bitcount_of_reg reg = (rn, lo, sz))
-      (H64 : sz = 64%N)
+      (Hwidth : sz = width)
       (H : GetReg reg s = Success (idx, s'))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
@@ -1710,14 +1717,14 @@ Lemma GetReg_ok {opts : symbolic_options_computed_opt} {descr:description} G s s
   : ((exists idx',
          get_reg r rn = Some idx'
          /\ eval_idx_Z G d idx' v)
-     /\ eval_idx_Z G d' idx (Z.land v (Z.ones 64))
+     /\ eval_idx_Z G d' idx (Z.land v (Z.ones (Z.of_N width)))
      /\ r = r'
      /\ f = f'
      /\ m = m')
     /\ gensym_dag_ok G d'
     /\ (forall e n, eval G d e n -> eval G d' e n).
 Proof.
-  cbv [GetReg GetReg64 some_or Symbolic.bind ErrorT.bind Symbolic.App Merge] in *.
+  cbv [GetReg GetRegFull some_or Symbolic.bind ErrorT.bind Symbolic.App Merge] in *.
   subst sz.
   assert (lo = 0%N) by (
       clear -Hreg; inversion_prod; subst;
@@ -1753,8 +1760,9 @@ Proof.
 Qed.
 
 Lemma GetReg_ok_bounded {opts : symbolic_options_computed_opt} {descr:description} G s s' reg idx rn lo sz v
+      (width := widest_reg_size_of reg)
       (Hreg : index_and_shift_and_bitcount_of_reg reg = (rn, lo, sz))
-      (H64 : sz = 64%N)
+      (Hwidth : sz = width)
       (H : GetReg reg s = Success (idx, s'))
       (d := s.(dag_state))
       (d' := s'.(dag_state))
@@ -1766,7 +1774,7 @@ Lemma GetReg_ok_bounded {opts : symbolic_options_computed_opt} {descr:descriptio
       (m' := s'.(symbolic_mem_state))
       (Hd : gensym_dag_ok G d)
       (Hr : forall idx', get_reg r rn = Some idx' -> eval_idx_Z G d idx' v)
-      (Hv : (0 <= v < 2^64)%Z)
+      (Hv : (0 <= v < 2^Z.of_N width)%Z)
   : ((exists idx',
          get_reg r rn = Some idx'
          /\ eval_idx_Z G d idx' v)
@@ -1777,7 +1785,7 @@ Lemma GetReg_ok_bounded {opts : symbolic_options_computed_opt} {descr:descriptio
     /\ gensym_dag_ok G d'
     /\ (forall e n, eval G d e n -> eval G d' e n).
 Proof.
-  replace v with (Z.land v (Z.ones (Z.of_N 64))) at 1; [ eapply GetReg_ok; eassumption | rewrite land_ones_eq_of_bounded by assumption ].
+  replace v with (Z.land v (Z.ones (Z.of_N width))) at 1; [ eapply GetReg_ok; eassumption | rewrite land_ones_eq_of_bounded by assumption ].
   reflexivity.
 Qed.
 
@@ -2233,7 +2241,7 @@ Lemma build_merge_base_addresses_G_ok
            (m' := s'.(symbolic_mem_state))
            (Hd : gensym_dag_ok G d)
            (Hruntime_reg_bounded : Forall (fun v => (0 <= v < 2^64)%Z) runtime_reg)
-           (Hreg_available_wide : Forall (fun reg => let '(rn, lo, sz) := index_and_shift_and_bitcount_of_reg reg in sz = 64%N) reg_available),
+           (Hreg_available_wide : Forall (fun reg => reg_size reg = widest_reg_size_of reg /\ let '(rn, lo, sz) := index_and_shift_and_bitcount_of_reg reg in sz = 64%N) reg_available),
     ((exists (outputaddrs' : list (idx * option idx + idx * list idx)),
          let addrs_vals_of := fun base_reg_val addrs' => List.map (fun i => Z.land (base_reg_val + 8 * Z.of_nat i) (Z.ones 64)) (seq 0 (List.length addrs')) in
          fold_left (fun rst '(r, idx')
@@ -2323,7 +2331,7 @@ Proof.
         runtime_reg as [|runtime_reg runtime_regs];
     try specialize (IH reg_availables runtime_regs).
   all: repeat first [ progress cbn [build_merge_base_addresses_G List.length firstn] in *
-                    | progress cbv [Symbolic.bind ErrorT.bind Symbolic.ret G.ret G.lift G.bind Crypto.Util.Option.bind] in *
+                    | progress cbv [Symbolic.bind ErrorT.bind Symbolic.ret G.ret G.lift G.bind Crypto.Util.Option.bind widest_reg_size_of] in *
                     | progress intros
                     | progress inversion_option
                     | progress inversion_prod
@@ -2369,7 +2377,7 @@ Proof.
                  (*
                       | [ H : symbolic_flag_state _ = symbolic_flag_state ?x, H' : symbolic_flag_state ?x = _ |- _ ]
                         => is_var x; destruct x*)
-                 end
+                end
                | break_innermost_match_hyps_step
                | apply conj; eauto 10; []
                | progress cbv [index_and_shift_and_bitcount_of_reg] in * ].
@@ -2388,6 +2396,7 @@ Proof.
                | rewrite <- ?app_assoc; progress cbn [List.app]
                | rewrite !app_assoc
                | rewrite app_nil_r
+               | progress change (Z.of_N 64) with 64%Z in *
                | progress cbv [option_eq] in *
                | progress inversion_prod
                | progress subst
@@ -2412,6 +2421,9 @@ Proof.
                  | [ |- ?x ++ ?y = ?y ] => cut (x = []); [ now intros -> | ]
                  | [ |- ?y ++ ?x = ?y ] => cut (x = []); [ now intros ->; rewrite app_nil_r | ]
                  | [ |- rev ?x = nil ] => cut (x = []); [ now intros -> | ]
+                 | [ H : ?x = 64%N |- context[?x] ] => rewrite H in *
+                 | [ H : ?x = 64%N, H' : context[?x] |- _ ] => rewrite H in *
+                 | [ H : 64%N = ?x |- _ ] => progress symmetry in H
                  | [ H : eval_idx_Z _ _ ?i ?v |- eval_idx_Z _ _ ?i ?v' ]
                    => cut (v' = v); [ intros ->; eapply lift_eval_idx_Z_impl; [ | exact H ]; eauto | rewrite !Z.land_ones, !Z.mod_small by lia ]
                  (*| [ |- match ?e with inl _ => ?v | inr _ => _ end = ?v' ]
@@ -2425,6 +2437,12 @@ Proof.
                    => erewrite map_ext; [ eapply Forall2_weaken; [ | exact H ] | cbv beta ];
                       [ eauto using lift_eval_idx_Z_impl
                       | intros; rewrite !Z.land_ones by lia; push_Zmod; pull_Zmod ]
+                 end
+               | rewrite Z.mod_small by lia
+               | progress (push_Zmod; pull_Zmod)
+               | match goal with
+                 | [ H : eval_idx_Z _ _ ?i ?v |- eval_idx_Z _ _ ?i ?v' ]
+                    => cut (v' = v); [ intros ->; eapply lift_eval_idx_Z_impl; [ | exact H ]; eauto | rewrite !Z.land_ones by lia ]
                  end ].
 Qed.
 
@@ -2516,7 +2534,7 @@ Lemma build_merge_base_addresses_ok
       (H : build_merge_base_addresses (dereference_scalar:=dereference_scalar) idxs reg_available s = Success (outputaddrs, s'))
       (Hd : gensym_dag_ok G d)
       (Hruntime_reg_bounded : Forall (fun v => (0 <= v < 2^64)%Z) runtime_reg)
-      (Hreg_available_wide : Forall (fun reg => let '(rn, lo, sz) := index_and_shift_and_bitcount_of_reg reg in sz = 64%N) reg_available)
+      (Hreg_available_wide : Forall (fun reg => reg_size reg = widest_reg_size_of reg /\ let '(rn, lo, sz) := index_and_shift_and_bitcount_of_reg reg in sz = 64%N) reg_available)
   : exists G',
     ((exists (outputaddrs' : list (idx * option idx + idx * list idx)),
          let addrs_vals_of := fun base_reg_val addrs' => List.map (fun i => Z.land (base_reg_val + 8 * Z.of_nat i) (Z.ones 64)) (seq 0 (List.length addrs')) in
diff --git a/src/Assembly/Parse.v b/src/Assembly/Parse.v
index f12d03a8b0..8f59b14d2f 100644
--- a/src/Assembly/Parse.v
+++ b/src/Assembly/Parse.v
@@ -79,16 +79,26 @@ Definition parse_label : ParserAction string
        (fun '(char, ls) => string_of_list_ascii (char :: ls))
        (([a-zA-Z] || parse_any_ascii "._?$") ;;
         (([a-zA-Z] || parse_any_ascii "0123456789_$#@~.?")* )).
+Definition parse_non_access_size_label : ParserAction string
+:= parse_lookahead_not parse_AccessSize ;;R parse_label.
 
 Definition parse_MEM : ParserAction MEM
-  := parse_map
-       (fun '(access_size, (br (*base reg*), sr (*scale reg, including z *), offset, base_label))
-        => {| mem_bits_access_size := access_size:option AccessSize
-           ; mem_base_reg := br:option REG
-           ; mem_base_label := base_label
-           ; mem_scale_reg := sr:option (Z * REG)
-           ; mem_offset := offset:option Z |})
+  := parse_option_list_map
+       (fun '(access_size, (constant_location_label, (br (*base reg*), sr (*scale reg, including z *), offset, base_label)))
+        => match base_label, constant_location_label with
+           | Some _, Some _ => (* invalid? *) None
+           | Some _ as lbl, None
+           | None, Some _ as lbl
+           | None, None as lbl =>
+               Some
+                {| mem_bits_access_size := access_size:option AccessSize
+                ; mem_base_reg := br:option REG
+                ; mem_base_label := lbl
+                ; mem_scale_reg := sr:option (Z * REG)
+                ; mem_offset := offset:option Z |}
+          end)
        (((strip_whitespace_after parse_AccessSize)?) ;;
+        (parse_non_access_size_label?) ;;
         (parse_option_list_map
            (fun '(offset, vars)
             => (vars <-- List.map (fun '(c, (v, e), vs) => match vs, e with [], 1%Z => Some (c, v) | _, _ => None end) vars;
@@ -144,7 +154,8 @@ Definition parse_OpCode_list : list (string * OpCode)
         ; (".word", dw)
         ; (".long", dd)
         ; (".int", dd)
-        ; (".quad", dq)].
+        ; (".quad", dq)
+        ; (".octa", do)].
 
 Definition parse_OpCode : ParserAction OpCode
   := parse_strs_case_insensitive parse_OpCode_list.
@@ -266,11 +277,21 @@ Global Instance show_lvl_MEM : ShowLevel MEM
                                  then "0x08 * " ++ Decimal.show_Z (offset / 8)
                                  else Hex.show_Z offset)
                     end%Z) in
-              "[" ++ match m.(mem_base_label) with
-                     | None => reg_part ++ offset_part
-                     | Some l => "((" ++ l ++ offset_part ++ "))"
-                     end
-                  ++ "]").
+              match m.(mem_base_label), m.(mem_base_reg), m.(mem_offset), m.(mem_scale_reg) with
+              | Some lbl, Some rip, None, None => lbl ++ "[" ++ reg_part ++ offset_part ++ "]"
+              | Some lbl, _, _, _ => let l_offset := lbl ++ offset_part in
+                  "[" ++
+                      (if reg_part =? ""
+                      then "((" ++ l_offset ++ "))"
+                      else reg_part ++ " + " ++ l_offset)
+                      ++ "]"
+              | None, _, _, _ =>
+                  "[" ++
+                    (if reg_part =? ""
+                    then "((" ++ offset_part ++ "))"
+                    else reg_part ++ offset_part)
+                    ++ "]"
+              end).
 Global Instance show_MEM : Show MEM := show_lvl_MEM.
 
 Global Instance show_lvl_JUMP_LABEL : ShowLevel JUMP_LABEL
@@ -489,20 +510,86 @@ Definition find_globals (ls : Lines) : list string
                  end)
        ls.
 
-Fixpoint split_code_to_functions' (globals : list string) (ls : Lines) : Lines (* prefix *) * list (string (* global name *) * Lines)
+Definition find_labels (ls : Lines) : list string
+  := Option.List.map
+       (fun l => match l.(rawline) with
+                 | LABEL name => Some name
+                 | _ => None
+                 end)
+       ls.
+
+Fixpoint split_code_to_functions' (label_is_function : string -> bool) (ls : Lines) : Lines (* prefix *) * list (string (* global name *) * Lines)
   := match ls with
      | [] => ([], [])
      | l :: ls
-       => let '(prefix, rest) := split_code_to_functions' globals ls in
+       => let '(prefix, rest) := split_code_to_functions' label_is_function ls in
           let default := (l :: prefix, rest) in
           match l.(rawline) with
-          | LABEL name => if List.existsb (fun n => name =? n)%string globals
+          | LABEL name => if label_is_function name
                           then ([], (name, l::prefix) :: rest)
                           else default
           | _ => default
           end
      end.
 
-Definition split_code_to_functions (ls : Lines) : Lines (* prefix *) * list (string (* global name *) * Lines)
+Definition string_matches_loose (allow_prefix : bool) (allow_suffix : bool) (longer_string shorter_string : string) : bool
+  := match allow_prefix, allow_suffix with
+     | false, false => shorter_string =? longer_string
+     | true, false => String.endswith shorter_string longer_string
+     | false, true => String.startswith shorter_string longer_string
+     | true, true => String.is_substring shorter_string longer_string
+     end.
+Definition split_code_to_listed_functions {allow_prefix allow_suffix : bool} (functions : list string) (ls : Lines) : Lines (* prefix *) * list (string (* global name *) * Lines)
+  := split_code_to_functions' (fun name => List.existsb (fun f => string_matches_loose allow_prefix allow_suffix f name)%string functions) ls.
+Definition split_code_to_global_functions (ls : Lines) : Lines (* prefix *) * list (string (* global name *) * Lines)
   := let globals := find_globals ls in
-     split_code_to_functions' globals ls.
+     split_code_to_listed_functions (allow_prefix:=false) (allow_suffix:=false) globals ls.
+Definition split_code_at_labels (ls : Lines) : Lines (* prefix *) * list (string (* label name *) * Lines)
+  := let labels := find_labels ls in
+     split_code_to_listed_functions (allow_prefix:=false) (allow_suffix:=false) labels ls.
+
+Fixpoint get_initial_data (ls : Lines) : list (AccessSize * list Z)
+  := let get_arg_consts args :=
+           Option.List.lift
+            (List.map (fun arg => match arg with
+                                    | const c => Some c
+                                    | _ => None
+                                    end)
+                     args) in
+     match ls with
+     | [] => []
+     | l :: ls
+       => match l.(rawline) with
+          | INSTR instr =>
+              match accesssize_of_declaration instr.(op) with
+              | None => []
+              | Some size =>
+                  let csts := get_arg_consts instr.(args) in
+                  match csts with
+                  | Some csts => (size, csts) :: get_initial_data ls
+                  | None => []
+                  end
+              end
+          | LABEL _
+          | EMPTY
+          | GLOBAL _
+          | DEFAULT_REL
+            => get_initial_data ls
+          | SECTION _
+          | ALIGN _
+             => []
+          end
+     end.
+
+Definition get_labeled_data (ls : Lines) : list (string * list (AccessSize * list Z)) :=
+  let '(_, labeled_data) := split_code_at_labels ls in
+  let labeled_data := List.map (fun '(lbl, lines) => (lbl, get_initial_data lines)) labeled_data in
+  let labeled_data := List.filter (fun '(_, data) => match data with nil => false | _ => true end) labeled_data in
+  labeled_data.
+
+Definition parse_assembly_options (ls : Lines) : assembly_program_options
+  := {| default_rel := Option.is_Some (List.find (fun l => match l.(rawline) with
+                                | DEFAULT_REL => true
+                                | _ => false
+                                end) ls)
+     |}.
diff --git a/src/Assembly/Parse/TestAsm.v b/src/Assembly/Parse/TestAsm.v
index 86dcddbdb9..258e84685a 100644
--- a/src/Assembly/Parse/TestAsm.v
+++ b/src/Assembly/Parse/TestAsm.v
@@ -65,13 +65,13 @@ Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_O1.example.
 Proof. Time native_compute. exact eq_refl. Abort.
 (*Redirect "log" Compute parse fiat_25519_all_gcc_14_1_O1.example.*)
 Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_O2.example.
-Proof. Time native_compute. Fail exact eq_refl. Abort.
+Proof. Time native_compute. exact eq_refl. Abort.
 (*Redirect "log" Compute parse fiat_25519_all_gcc_14_1_O2.example.*)
 Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_O3.example.
-Proof. Time native_compute. Fail exact eq_refl. Abort.
+Proof. Time native_compute. exact eq_refl. Abort.
 (*Redirect "log" Compute parse fiat_25519_all_gcc_14_1_O3.example.*)
 Goal parse_correct_on_debug fiat_25519_all_gcc_14_1_Os.example.
-Proof. Time native_compute.  exact eq_refl. Abort.
+Proof. Time native_compute. exact eq_refl. Abort.
 (*Redirect "log" Compute parse fiat_25519_all_gcc_14_1_Os.example.*)
 Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_O0.example.
 Proof. Time native_compute. exact eq_refl. Abort.
@@ -80,11 +80,11 @@ Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_O1.example.
 Proof. Time native_compute. exact eq_refl. Abort.
 (*Redirect "log" Compute parse fiat_25519_all_clang_19_1_0_O1.example.*)
 Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_O2.example.
-Proof. Time native_compute. Fail exact eq_refl. Abort.
+Proof. Time native_compute. exact eq_refl. Abort.
 (*Redirect "log" Compute parse fiat_25519_all_clang_19_1_0_O2.example.*)
 Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_O3.example.
-Proof. Time native_compute. Fail exact eq_refl. Abort.
+Proof. Time native_compute. exact eq_refl. Abort.
 (*Redirect "log" Compute parse fiat_25519_all_clang_19_1_0_O3.example.*)
 Goal parse_correct_on_debug fiat_25519_all_clang_19_1_0_Os.example.
-Proof. Time native_compute. Fail exact eq_refl. Abort.
+Proof. Time native_compute. exact eq_refl. Abort.
 (*Redirect "log" Compute parse fiat_25519_all_clang_19_1_0_Os.example.*)
diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v
index 99eb5546a2..80204bc310 100644
--- a/src/Assembly/Symbolic.v
+++ b/src/Assembly/Symbolic.v
@@ -3938,15 +3938,15 @@ Global Instance ShowLines_symbolic_state : ShowLines symbolic_state :=
  fun X : symbolic_state =>
  match X with
  | {|
-     dag_state := ds;
+     dag_state := dagst;
      symbolic_reg_state := rs;
-     symbolic_flag_state := fs;
+     symbolic_flag_state := flst;
      symbolic_mem_state := ms
    |} =>
    ["(*symbolic_state*) {|";
-   "  dag_state :="] ++ show_lines ds ++ [";";
+   "  dag_state :="] ++ show_lines dagst ++ [";";
    ("  symbolic_reg_state := " ++ show rs ++ ";")%string;
-   ("  symbolic_flag_state := " ++ show fs ++";")%string;
+   ("  symbolic_flag_state := " ++ show flst ++";")%string;
    "  symbolic_mem_state :="] ++show_lines ms ++ [";";
    "|}"]
  end%list%string.
@@ -4048,11 +4048,11 @@ Definition error_get_reg_of_reg_index ri : symbolic_state -> error
   := error.get_reg (let r := widest_register_of_index ri in
                     if (reg_index r =? ri)%N
                     then inr r
-                    else inl ri).
+                    else inl (N.to_nat ri)).
 
 Definition GetFlag f : M idx :=
   some_or (fun s => get_flag s f) (error.get_flag f).
-Definition GetReg64 ri : M idx :=
+Definition GetRegFull ri : M idx :=
   some_or (fun st => get_reg st ri) (error_get_reg_of_reg_index ri).
 Definition Load64 (a : idx) : M idx := some_or (load a) (error.load a).
 Definition Remove64 (a : idx) : M idx
@@ -4071,7 +4071,7 @@ Definition PreserveFlag {T} (f : FLAG) (k : M T) : M T :=
   x <- k;
   _ <- (fun s => Success (tt, update_flag_with s (fun s => set_flag_internal s f vf)));
   ret x.
-Definition SetReg64 rn i : M unit :=
+Definition SetRegFull rn i : M unit :=
   fun s => Success (tt, update_reg_with s (fun s => set_reg s rn i)).
 Definition Store64 (a v : idx) : M unit :=
   ms <- some_or (store a v) (error.store a v);
@@ -4092,16 +4092,17 @@ Definition RevealConst (i : idx) : M Z :=
 
 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;
+  v <- GetRegFull rn;
   App ((slice lo sz), [v]).
 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]);
-       SetReg64 rn v (* works even if old value is unspecified *)
-  else old <- GetReg64 rn;
+  let widest_size := reg_size (widest_register_of_index rn) in
+  if (sz =? widest_size)%N
+  then v <- App (slice 0 widest_size, [v]);
+       SetRegFull rn v (* works even if old value is unspecified *)
+  else old <- GetRegFull rn;
        v <- App ((set_slice lo sz), [old; v]);
-       SetReg64 rn v.
+       SetRegFull rn v.
 
 Class AddressSize := address_size : OperationSize.
 Definition Address {opts : symbolic_options_computed_opt} {descr:description} {sa : AddressSize} (a : MEM) : M idx :=
diff --git a/src/Assembly/Syntax.v b/src/Assembly/Syntax.v
index 410f6e7469..bccf79a4c8 100644
--- a/src/Assembly/Syntax.v
+++ b/src/Assembly/Syntax.v
@@ -18,10 +18,34 @@ Local Set Implicit Arguments.
 Local Set Primitive Projections.
 
 Inductive REG :=
+(* XMM/YMM/ZMM registers *)
+| zmm0  | zmm1  | zmm2  | zmm3  | zmm4  | zmm5  | zmm6  | zmm7  | zmm8  | zmm9  | zmm10  | zmm11  | zmm12  | zmm13  | zmm14  | zmm15 | zmm16 | zmm17 | zmm18 | zmm19 | zmm20 | zmm21 | zmm22 | zmm23 | zmm24 | zmm25 | zmm26  | zmm27  | zmm28  | zmm29  | zmm30  | zmm31
+| ymm0  | ymm1  | ymm2  | ymm3  | ymm4  | ymm5  | ymm6  | ymm7  | ymm8  | ymm9  | ymm10  | ymm11  | ymm12  | ymm13  | ymm14  | ymm15
+| xmm0  | xmm1  | xmm2  | xmm3  | xmm4  | xmm5  | xmm6  | xmm7  | xmm8  | xmm9  | xmm10  | xmm11  | xmm12  | xmm13  | xmm14  | xmm15
+(* Segment registers *)
+| cs | ds | es | fs | gs | ss
+(* Control registers *)
+| cr0 | cr1 | cr2 | cr3 | cr4 | cr8 | cr9 | cr10 | cr11 | cr12 | cr13 | cr14 | cr15
+| msw
+| mxcsr
+(* Debug registers *)
+| dr0 | dr1 | dr2 | dr3 | dr4 | dr5 | dr6 | dr7 | dr8 | dr9 | dr10 | dr11 | dr12 | dr13 | dr14 | dr15
+(* General purpose registers (64/32/16/8 bit) *)
 |     rax |     rcx |     rdx |     rbx | rsp  | rbp  | rsi  | rdi  | r8  | r9  | r10  | r11  | r12  | r13  | r14  | r15  | rip
 |     eax |     ecx |     edx |     ebx | esp  | ebp  | esi  | edi  | r8d | r9d | r10d | r11d | r12d | r13d | r14d | r15d | eip
 |      ax |      cx |      dx |      bx |  sp  |  bp  |  si  |  di  | r8w | r9w | r10w | r11w | r12w | r13w | r14w | r15w | ip
 | ah | al | ch | cl | dh | dl | bh | bl |  spl |  bpl |  sil |  dil | r8b | r9b | r10b | r11b | r12b | r13b | r14b | r15b
+(* MMX registers *)
+| mm0 | mm1 | mm2 | mm3 | mm4 | mm5 | mm6 | mm7
+(* Special registers *)
+| st0 | st1 | st2 | st3 | st4 | st5 | st6 | st7  (* FPU stack registers*)
+| k0 | k1 | k2 | k3 | k4 | k5 | k6 | k7          (* AVX-512 mask registers *)
+| gdtr | idtr | ldtr | tr
+| cw | sw | tw | fp_cs | fp_opc | fp_ds
+(* Flags registers *)
+(* | rflags
+| eflags
+| flags *)
 .
 
 Derive REG_Listable SuchThat (@FinitelyListable REG REG_Listable) As REG_FinitelyListable.
@@ -35,7 +59,7 @@ Definition REG_eq_dec : forall x y : REG, {x = y} + {x <> y} := eq_dec_of_listab
 Definition CONST := Z.
 Coercion CONST_of_Z (x : Z) : CONST := x.
 
-Inductive AccessSize := byte | word | dword | qword.
+Inductive AccessSize := byte | word | dword | qword | tbyte | xmmword | ymmword | zmmword.
 
 Derive AccessSize_Listable SuchThat (@FinitelyListable AccessSize AccessSize_Listable) As AccessSize_FinitelyListable.
 Proof. prove_ListableDerive. Qed.
@@ -51,6 +75,10 @@ Coercion bits_of_AccessSize (x : AccessSize) : N
      | word => 16
      | dword => 32
      | qword => 64
+     | tbyte => 80
+     | xmmword => 128
+     | ymmword => 256
+     | zmmword => 512
      end.
 
 Record MEM := { mem_bits_access_size : option AccessSize ; mem_base_reg : option REG ; mem_scale_reg : option (Z * REG) ; mem_base_label : option string ; mem_offset : option Z }.
@@ -102,6 +130,10 @@ Inductive OpCode :=
 | dw
 | dd
 | dq
+| dt
+| do
+| dy
+| dz
 | dec
 | imul
 | inc
@@ -176,6 +208,10 @@ Definition accesssize_of_declaration (opc : OpCode) : option AccessSize :=
   | dd => Some dword
   | dq => Some qword
   | dw => Some word
+  | dt => Some tbyte
+  | do => Some xmmword
+  | dy => Some ymmword
+  | dz => Some zmmword
   | adc
   | adcx
   | add
@@ -276,14 +312,38 @@ Definition Lines := list Line.
 
 Definition reg_size (r : REG) : N :=
       match r with
+      |(xmm0 | xmm1 | xmm2 | xmm3 | xmm4 | xmm5 | xmm6 | xmm7 | xmm8 | xmm9 | xmm10 | xmm11 | xmm12 | xmm13 | xmm14 | xmm15)
+       => 128
+      |(zmm0 | zmm1 | zmm2 | zmm3 | zmm4 | zmm5 | zmm6 | zmm7 | zmm8 | zmm9 | zmm10 | zmm11 | zmm12 | zmm13 | zmm14 | zmm15 | zmm16 | zmm17 | zmm18 | zmm19 | zmm20 | zmm21 | zmm22 | zmm23 | zmm24 | zmm25 | zmm26  | zmm27  | zmm28  | zmm29  | zmm30  | zmm31)
+       => 512
+      |(ymm0 | ymm1 | ymm2 | ymm3 | ymm4 | ymm5 | ymm6 | ymm7 | ymm8 | ymm9 | ymm10 | ymm11 | ymm12 | ymm13 | ymm14 | ymm15)
+       => 256
       |(    rax |     rcx |     rdx |     rbx | rsp  | rbp  | rsi  | rdi  | r8  | r9  | r10  | r11  | r12  | r13  | r14  | r15  | rip)
        => 64
       |(    eax |     ecx |     edx |     ebx | esp  | ebp  | esi  | edi  | r8d | r9d | r10d | r11d | r12d | r13d | r14d | r15d | eip)
        => 32
       |(     ax |      cx |      dx |      bx |  sp  |  bp  |  si  |  di  | r8w | r9w | r10w | r11w | r12w | r13w | r14w | r15w | ip)
        => 16
+      |(cs | ds | es | fs | gs | ss)
+       => 16
       |(ah | al | ch | cl | dh | dl | bh | bl |  spl |  bpl |  sil |  dil | r8b | r9b | r10b | r11b | r12b | r13b | r14b | r15b)
        => 8
+      |(cr0 | cr1 | cr2 | cr3 | cr4 | cr8 | cr9 | cr10 | cr11 | cr12 | cr13 | cr14 | cr15)
+       => 64
+      |(dr0 | dr1 | dr2 | dr3 | dr4 | dr5 | dr6 | dr7 | dr8 | dr9 | dr10 | dr11 | dr12 | dr13 | dr14 | dr15)
+       => 64
+      |(mm0 | mm1 | mm2 | mm3 | mm4 | mm5 | mm6 | mm7)
+       => 64
+      |(st0 | st1 | st2 | st3 | st4 | st5 | st6 | st7)
+       => 80
+      |(k0 | k1 | k2 | k3 | k4 | k5 | k6 | k7)
+       => 64
+      |(gdtr | idtr | ldtr | tr)
+       => 16
+      |(cw | sw | tw | fp_cs | fp_opc | fp_ds)
+       => 16
+      | msw => 16
+      | mxcsr => 32
       end.
 
 Definition standalone_operand_size (x : ARG) : option N :=
@@ -355,6 +415,25 @@ Definition widest_register_of (r : REG) : REG :=
   | (r14b | r14w | r14d | r14) => r14
   | (r15b | r15w | r15d | r15) => r15
   | (ip | eip | rip) => rip
+  (* | (flags | eflags | rflags) => rflags *)
+  | (xmm0 | ymm0 | zmm0) => zmm0
+  | (xmm1 | ymm1 | zmm1) => zmm1
+  | (xmm2 | ymm2 | zmm2) => zmm2
+  | (xmm3 | ymm3 | zmm3) => zmm3
+  | (xmm4 | ymm4 | zmm4) => zmm4
+  | (xmm5 | ymm5 | zmm5) => zmm5
+  | (xmm6 | ymm6 | zmm6) => zmm6
+  | (xmm7 | ymm7 | zmm7) => zmm7
+  | (xmm8 | ymm8 | zmm8) => zmm8
+  | (xmm9 | ymm9 | zmm9) => zmm9
+  | (xmm10 | ymm10 | zmm10) => zmm10
+  | (xmm11 | ymm11 | zmm11) => zmm11
+  | (xmm12 | ymm12 | zmm12) => zmm12
+  | (xmm13 | ymm13 | zmm13) => zmm13
+  | (xmm14 | ymm14 | zmm14) => zmm14
+  | (xmm15 | ymm15 | zmm15) => zmm15
+  | (msw | cr0) => cr0
+  | _ => r
   end.
 
 Definition widest_registers := Eval lazy in List.filter (fun x => REG_beq x (widest_register_of x)) (list_all REG).
diff --git a/src/Assembly/WithBedrock/Semantics.v b/src/Assembly/WithBedrock/Semantics.v
index 23cd75aa9d..325910eb03 100644
--- a/src/Assembly/WithBedrock/Semantics.v
+++ b/src/Assembly/WithBedrock/Semantics.v
@@ -9,6 +9,7 @@ Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.Bool.Reflect.
 Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.Strings.StringMap.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Notations.
@@ -86,10 +87,19 @@ Require Import coqutil.Map.Interface. (* coercions *)
 Require Import coqutil.Word.LittleEndianList.
 Require Import bedrock2.Memory. Import WithoutTuples.
 Require coqutil.Word.Naive coqutil.Map.SortedListWord.
+
 Definition mem_state := (SortedListWord.map (Naive.word 64) Byte.byte).
 
-Definition get_mem (st : mem_state) (addr : Z) (nbytes : nat) : option Z
-  := (bs <- load_bytes st (word.of_Z addr) nbytes; Some (LittleEndianList.le_combine bs))%option.
+Definition get_mem (st : mem_state) (addr : option (string * bool) * Z) (nbytes : nat) : option Z :=
+  let '(base_label, offset) := addr in
+  match base_label with
+  | Some (base_label, true) => None (* TODO: NOT YET IMPLEMENTED *)
+  | Some (_, false) => None
+  | None =>
+      bs <- load_bytes st (word.of_Z offset) nbytes;
+      Some (LittleEndianList.le_combine bs)
+  end%option.
+
 Definition set_mem (st : mem_state) (addr : Z) (nbytes : nat) (v : Z) : option mem_state
   := store_bytes st (word.of_Z addr) (LittleEndianList.le_split nbytes v).
 
@@ -104,29 +114,36 @@ Definition update_mem_with (st : machine_state) (f : mem_state -> mem_state) : m
 Definition DenoteConst (sz : N) (a : CONST) : Z :=
   Z.land a (Z.ones (Z.of_N sz)).
 
-Definition DenoteAddress (sa : N) (st : machine_state) (a : MEM) : Z :=
+Definition DenoteAddress {opts:assembly_program_options} (sa : N) (st : machine_state) (a : MEM) : option (string * bool) * Z :=
+  let '(lbl, base_reg) :=
+    match mem_base_label a, mem_base_reg a with
+    | Some lbl, Some rip => (Some (lbl, true), None)
+    | Some lbl, r => (Some (lbl, default_rel), r)
+    | None, r => (None, r)
+    end in
+  (lbl,
   Z.land (
-    match mem_base_reg  a with Some     r  => get_reg st r                    | _ => 0 end +
+    match base_reg        with Some     r  => get_reg st r                    | _ => 0 end +
     match mem_scale_reg a with Some (z, r) => get_reg st r * DenoteConst sa z | _ => 0 end +
     match mem_offset    a with Some  z     =>                DenoteConst sa z | _ => 0 end
-  ) (Z.ones (Z.of_N sa)).
+  ) (Z.ones (Z.of_N sa))).
 
-Definition DenoteOperand (sa s : N) (st : machine_state) (a : ARG) : option Z :=
+Definition DenoteOperand {opts:assembly_program_options} (sa s : N) (st : machine_state) (a : ARG) : option Z :=
   match a with
   | reg a => Some (get_reg st a)
   | mem a => get_mem st (DenoteAddress sa st a) (N.to_nat (N.div (operand_size a s) 8))
   | const a => Some (DenoteConst (operand_size a s) a)
   | label _ => None
-  end.
+  end%option.
 
 Definition SetMem (st : machine_state) (addr : Z) (nbytes : nat) (v : Z) : option machine_state :=
   ms <- set_mem st addr nbytes v;
   Some (update_mem_with st (fun _ => ms)).
 
-Definition SetOperand (sa s : N) (st : machine_state) (a : ARG) (v : Z) : option machine_state :=
+Definition SetOperand {opts:assembly_program_options} (sa s : N) (st : machine_state) (a : ARG) (v : Z) : option machine_state :=
   match a with
   | reg a => Some (update_reg_with st (fun rs => set_reg rs a v))
-  | mem a => SetMem st (DenoteAddress sa st a) (N.to_nat (N.div (operand_size a s) 8)) v
+  | mem a => let '(_lbl, addr) := DenoteAddress sa st a in SetMem st addr (N.to_nat (N.div (operand_size a s) 8)) v
   | const a => None
   | label _ => None
   end.
@@ -158,7 +175,7 @@ Definition rcrcnt s cnt : Z :=
 
 (* NOTE: currently immediate operands are treated as if sign-extension has been
  * performed ahead of time. *)
-Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstruction) : option machine_state :=
+Definition DenoteNormalInstruction {opts:assembly_program_options} (st : machine_state) (instr : NormalInstruction) : option machine_state :=
   let sa := 64%N in
   let stack_addr_size := 64%N in
   match operation_size instr with Some s =>
@@ -196,7 +213,9 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
     then SetOperand sa s st dst v
     else Some st
   | lea, [reg dst; mem src] => (* Flags Affected: None *)
-    Some (update_reg_with st (fun rs => set_reg rs dst (DenoteAddress sa st src)))
+    let '(lbl, addr) := DenoteAddress sa st src in
+    _ <- match lbl with None => Some tt | Some _ => None end; (* We don't support extracting label addresses *)
+    Some (update_reg_with st (fun rs => set_reg rs dst addr))
   | (add | adc) as opc, [dst; src] =>
     c <- (match opc with adc => get_flag st CF | _ => Some false end);
     let c := Z.b2z c in
@@ -381,6 +400,10 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
   | dw, _
   | dd, _
   | dq, _
+  | do, _
+  | dt, _
+  | dy, _
+  | dz, _
   | mulx, _
   | mul, _
   | call, _
@@ -452,7 +475,7 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
  end | _ => None end | _ => None end%Z%option.
 
 
-Definition DenoteRawLine (st : machine_state) (rawline : RawLine) : option machine_state :=
+Definition DenoteRawLine {opts:assembly_program_options} (st : machine_state) (rawline : RawLine) : option machine_state :=
   match rawline with
   | EMPTY
   | LABEL _
@@ -466,10 +489,10 @@ Definition DenoteRawLine (st : machine_state) (rawline : RawLine) : option machi
     => None
   end.
 
-Definition DenoteLine (st : machine_state) (line : Line) : option machine_state
+Definition DenoteLine {opts:assembly_program_options} (st : machine_state) (line : Line) : option machine_state
   := DenoteRawLine st line.(rawline).
 
-Fixpoint DenoteLines (st : machine_state) (lines : Lines) : option machine_state
+Fixpoint DenoteLines {opts:assembly_program_options} (st : machine_state) (lines : Lines) : option machine_state
   := match lines with
      | [] => Some st
      | line :: lines
diff --git a/src/Assembly/WithBedrock/SymbolicProofs.v b/src/Assembly/WithBedrock/SymbolicProofs.v
index 9ce30966d0..3c5955e239 100644
--- a/src/Assembly/WithBedrock/SymbolicProofs.v
+++ b/src/Assembly/WithBedrock/SymbolicProofs.v
@@ -94,8 +94,10 @@ Section WithDag.
 Context (d : dag).
 Local Notation eval := (Symbolic.eval G d).
 
+(* TODO: FIX ME use access size here *)
 Definition R_reg (x : option idx) (v : Z) : Prop :=
   (forall i, x = Some i -> eval i v) /\ (v = Z.land v (Z.ones 64)).
+
 Definition R_regs : Symbolic.reg_state -> Semantics.reg_state -> Prop :=
   Tuple.fieldwise R_reg.
 
@@ -232,8 +234,10 @@ Qed.
 Lemma R_flags_subsumed d s m (HR : R_flags d s m) d' (Hlt : d :< d')
   : R_flags' d' s m.
 Proof using Type.
-  cbv [R_flags Tuple.fieldwise Tuple.fieldwise'] in *;
-    intuition eauto using R_flag_subsumed.
+  cbv [R_flags] in *.
+  revert HR.
+  eapply Tuple.fieldwise_Proper; [ repeat intro | reflexivity .. ].
+  eapply R_flag_subsumed; eassumption.
 Qed.
 
 Lemma R_reg_subsumed d s m (HR : R_reg d s m) d' (Hlt : d :< d')
@@ -243,8 +247,10 @@ Proof using Type. cbv [R_reg] in *; intuition eauto. Qed.
 Lemma R_regs_subsumed d s m (HR : R_regs d s m) d' (Hlt : d :< d')
   : R_regs' d' s m.
 Proof using Type.
-  cbv [R_regs Tuple.fieldwise Tuple.fieldwise'] in *;
-    intuition eauto using R_reg_subsumed.
+  cbv [R_regs] in *.
+  revert HR.
+  eapply Tuple.fieldwise_Proper; [ repeat intro | reflexivity .. ].
+  eapply R_reg_subsumed; eassumption.
 Qed.
 
 Local Existing Instance Naive.word64_ok.
@@ -349,7 +355,7 @@ Proof using Type. cbv; destruct v; trivial. Qed.
 
 (* workaround: using cbn instead of this lemma makes Qed hang after next rewrite in same hyp *)
 Lemma unfold_bind {A B} ma amb s :
-  @bind A B ma amb s = ltac:(let t := eval unfold bind, ErrorT.bind in (@bind A B ma amb s) in exact t).
+  @bind A B ma amb s = ltac:(let t := eval unfold bind, ErrorT.bind in ( @bind A B ma amb s ) in exact t).
 Proof using Type. exact eq_refl. Qed.
 
 Local Hint Resolve gensym_dag_ok_of_R : core.
@@ -481,7 +487,7 @@ Lemma GetReg_R {opts : symbolic_options_computed_opt} {descr:description} s m (H
   (H : GetReg r s = Success (i, s'))
   : R s' m  /\ s :< s' /\ eval s' i (get_reg m r).
 Proof using Type.
-  cbv [GetReg GetReg64 bind some_or get_reg index_and_shift_and_bitcount_of_reg] in *.
+  cbv [GetReg GetRegFull bind some_or get_reg index_and_shift_and_bitcount_of_reg] in *.
   pose proof (get_reg_R s _ ltac:(eassumption) (reg_index r)) as Hr.
   destruct Symbolic.get_reg in *; [|inversion H]; cbn in H.
   specialize (Hr _ eq_refl); case Hr as (v&Hi0&Hv).
@@ -499,8 +505,8 @@ Ltac step_GetReg :=
     [eassumption|..|clear H]
   end.
 
-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.
+Lemma Address_R {popts : assembly_program_options} {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 popts sa m o = (None, 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.
   all : repeat first [ progress inversion_ErrorT
@@ -548,18 +554,18 @@ Qed.
 Lemma Load64_R s m (HR : R s m) (a : idx)
   va (Ha : eval s a va)
   i s' (H : Load64 a s = Success (i, s'))
-  : s' = s /\ exists v, eval s i v /\ get_mem m va 8 = Some v /\ v = Z.land v (Z.ones 64).
+  : s' = s /\ exists v, eval s i v /\ get_mem m (None, va) 8 = Some v /\ v = Z.land v (Z.ones 64).
 Proof using Type.
   cbv [Load64 some_or Symbolic.load option_map] in *.
   destruct find as [(?&?)|] eqn:? in *;
     inversion_ErrorT; Prod.inversion_prod; subst.
   split;trivial.
   eapply ListUtil.find_some_iff in Heqo;
-    repeat (cbn in *; destruct_head'_and; destruct_head'_ex).
+    repeat (cbn [fst] in *; destruct_head'_and; destruct_head'_ex).
   clear H1. autoforward with typeclass_instances in H0; subst.
   eapply nth_error_split in H;
-    repeat (cbn in *; destruct_head'_and; destruct_head'_ex).
-  destruct s'; cbn in *; destruct_head'_and; subst.
+    repeat (destruct_head'_and; destruct_head'_ex).
+  destruct s'; cbn [Symbolic.symbolic_mem_state Symbolic.dag_state R] in *; destruct_head'_and; subst.
   progress unfold machine_mem_state in *.
   eapply R_mem_Permutation in H4;
     [|symmetry; eapply Permutation.Permutation_middle].
@@ -567,7 +573,7 @@ Proof using Type.
   eapply load_bytes_Rcell64 in H4; eauto; [];
     repeat (destruct_head'_and; destruct_head'_ex).
   eexists; split; try eassumption; split.
-  { destruct_one_match; simpl in *; try congruence. }
+  { destruct_one_match; congruence. }
   { epose proof le_combine_bound x as HH.
     erewrite length_load_bytes in HH by eassumption.
     rewrite Z.land_ones, Z.mod_small; lia. }
@@ -647,7 +653,7 @@ Proof using Type.
 Qed.
 
 Lemma store8 m a
-  old (Hold : get_mem m a 8 = Some old) b
+  old (Hold : get_mem m (None, a) 8 = Some old) b
   m'  (Hm': set_mem m a 8 (Z.lor (Z.land b (Z.ones 8)) (Z.ldiff old (Z.ones 8))) = Some m')
   : set_mem m a 1 b = Some m'.
 Proof using Type.
@@ -712,9 +718,9 @@ Proof using Type.
 Qed.
 
 
-Lemma GetOperand_R {opts : symbolic_options_computed_opt} {descr:description} s m (HR: R s m) (so:OperationSize) (sa:AddressSize) a i s'
+Lemma GetOperand_R {popts : assembly_program_options} {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.
+  : R s' m /\ s :< s' /\ exists v, eval s' i v /\ @DenoteOperand popts sa so m a = Some v.
 Proof using Type.
   cbv [GetOperand DenoteOperand err] in *; break_innermost_match; inversion_ErrorT.
   { eapply GetReg_R in H; intuition eauto. }
@@ -738,11 +744,14 @@ Proof using Type.
       simpl load_bytes.
       change (Pos.to_nat 1) with 1%nat.
       cbv [load_bytes footprint List.map seq List.option_all].
+      eta_expand; break_innermost_match_step; eta_expand; try congruence; [].
       setoid_rewrite E0.
       eexists; split; eauto.
       cbv [le_combine].
       rewrite Z.shiftl_0_l, Z.lor_0_r.
-      change (Z.lor (Byte.byte.unsigned b) (Z.shiftl (le_combine l) 8) = x) in H4.
+      let H4 := multimatch goal with H : _ |- _ => H end in
+      let H5 := multimatch goal with H : _ |- _ => H end in
+      change (Z.lor (Byte.byte.unsigned b) (Z.shiftl (le_combine l) 8) = x) in H4;
       rewrite <-H4 in H5 at 2; rewrite H5; clear H4 H5.
       f_equal.
       rewrite <-Byte.byte.wrap_unsigned at 1; setoid_rewrite <-Z.land_ones; [|clear;lia].
@@ -751,8 +760,11 @@ Proof using Type.
       rewrite Z.land_lor_distr_l.
       bitblast.Z.bitblast. subst.
       rewrite (Z.testbit_neg_r _ (_-8)) by lia; Btauto.btauto. }
-    { setoid_rewrite H4.
+    { destruct DenoteAddress; cbn [fst snd] in *; subst.
+      let H4 := multimatch goal with H : _ |- _ => H end in
+      setoid_rewrite H4.
       eexists; split; eauto; f_equal.
+      let H5 := multimatch goal with H : _ |- _ => H end in
       rewrite H5 at 1; trivial. } }
   { step_symex; repeat (eauto||econstructor). }
 Qed.
@@ -767,13 +779,13 @@ Ltac step_GetOperand :=
   end.
 
 (* note: do the two SetOperand both truncate inputs or not?... *)
-Lemma R_SetOperand {opts : symbolic_options_computed_opt} {descr:description} s m (HR : R s m)
+Lemma R_SetOperand {popts : assembly_program_options} {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'.
 Proof using Type.
   destruct a in *; cbn in H; cbv [err] in *; inversion_ErrorT; [ | ];
-    cbv [SetOperand Crypto.Util.Option.bind SetReg64 update_reg_with Symbolic.update_reg_with] in *;
+    cbv [SetOperand Crypto.Util.Option.bind SetRegFull update_reg_with Symbolic.update_reg_with] in *;
     repeat (BreakMatch.break_innermost_match_hyps; Prod.inversion_prod; ErrorT.inversion_ErrorT; subst).
 
   { repeat step_symex.
@@ -801,7 +813,7 @@ Proof using Type.
     { cbn -[Z.ones]; rewrite !Z.land_ones, Zmod_mod by (clear;lia); trivial. } }
   { eexists; split; [exact eq_refl|].
     repeat (step_symex; []).
-    cbv [GetReg64 some_or] in *.
+    cbv [GetRegFull some_or] in *.
     pose proof (get_reg_R s _ ltac:(eassumption) (reg_index r)) as Hr.
     destruct (Symbolic.get_reg _ _) in *; cbn [ErrorT.bind] in H;
       ErrorT.inversion_ErrorT; Prod.inversion_prod; subst;cbn [fst snd] in *.
@@ -819,7 +831,7 @@ Proof using Type.
     cbv [R_reg]; intuition idtac; try Option.inversion_option; subst; try eval_same_expr_goal;
     cbv [bitmask_of_reg index_and_shift_and_bitcount_of_reg].
     { rewrite <-Tuple.nth_default_to_list. cbv [nth_default]; rewrite H5. trivial. }
-    assert (Z.of_N (reg_size r) + Z.of_N (reg_offset r) <= 64) by (destruct r; clear; cbv; discriminate).
+    (* assert (Z.of_N (reg_size r) + Z.of_N (reg_offset r) <= 64) by (destruct r; clear; cbv; discriminate). *)
     eapply Z.bits_inj_iff'; intros j Hj.
     rewrite Z.land_spec, Z.testbit_ones_nonneg by (clear -Hj; lia).
     destr.destr (j <? 64); rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; trivial; [].