diff --git a/src/Assembly/Equality.v b/src/Assembly/Equality.v
index 4575629772..336da900e8 100644
--- a/src/Assembly/Equality.v
+++ b/src/Assembly/Equality.v
@@ -35,8 +35,8 @@ Bind Scope REG_scope with REG.
 Infix "=?" := REG_beq : REG_scope.
 
 Global Instance REG_beq_spec : reflect_rel (@eq REG) REG_beq | 10
-  := reflect_of_beq internal_REG_dec_bl internal_REG_dec_lb.
-Definition REG_beq_eq x y : (x =? y)%REG = true <-> x = y := conj (@internal_REG_dec_bl _ _) (@internal_REG_dec_lb _ _).
+  := reflect_of_beq REG_dec_bl REG_dec_lb.
+Definition REG_beq_eq x y : (x =? y)%REG = true <-> x = y := conj (@REG_dec_bl _ _) (@REG_dec_lb _ _).
 Lemma REG_beq_neq x y : (x =? y)%REG = false <-> x <> y.
 Proof. rewrite <- REG_beq_eq; destruct (x =? y)%REG; intuition congruence. Qed.
 Global Instance REG_beq_compat : Proper (eq ==> eq ==> eq) REG_beq | 10.
@@ -95,8 +95,8 @@ Bind Scope AccessSize_scope with AccessSize.
 Infix "=?" := AccessSize_beq : AccessSize_scope.
 
 Global Instance AccessSize_beq_spec : reflect_rel (@eq AccessSize) AccessSize_beq | 10
-  := reflect_of_beq internal_AccessSize_dec_bl internal_AccessSize_dec_lb.
-Definition AccessSize_beq_eq x y : (x =? y)%AccessSize = true <-> x = y := conj (@internal_AccessSize_dec_bl _ _) (@internal_AccessSize_dec_lb _ _).
+  := reflect_of_beq AccessSize_dec_bl AccessSize_dec_lb.
+Definition AccessSize_beq_eq x y : (x =? y)%AccessSize = true <-> x = y := conj (@AccessSize_dec_bl _ _) (@AccessSize_dec_lb _ _).
 Lemma AccessSize_beq_neq x y : (x =? y)%AccessSize = false <-> x <> y.
 Proof. rewrite <- AccessSize_beq_eq; destruct (x =? y)%AccessSize; intuition congruence. Qed.
 Global Instance AccessSize_beq_compat : Proper (eq ==> eq ==> eq) AccessSize_beq | 10.
@@ -141,8 +141,8 @@ Bind Scope FLAG_scope with FLAG.
 Infix "=?" := FLAG_beq : FLAG_scope.
 
 Global Instance FLAG_beq_spec : reflect_rel (@eq FLAG) FLAG_beq | 10
-  := reflect_of_beq internal_FLAG_dec_bl internal_FLAG_dec_lb.
-Definition FLAG_beq_eq x y : (x =? y)%FLAG = true <-> x = y := conj (@internal_FLAG_dec_bl _ _) (@internal_FLAG_dec_lb _ _).
+  := reflect_of_beq FLAG_dec_bl FLAG_dec_lb.
+Definition FLAG_beq_eq x y : (x =? y)%FLAG = true <-> x = y := conj (@FLAG_dec_bl _ _) (@FLAG_dec_lb _ _).
 Lemma FLAG_beq_neq x y : (x =? y)%FLAG = false <-> x <> y.
 Proof. rewrite <- FLAG_beq_eq; destruct (x =? y)%FLAG; intuition congruence. Qed.
 Global Instance FLAG_beq_compat : Proper (eq ==> eq ==> eq) FLAG_beq | 10.
@@ -155,8 +155,8 @@ Bind Scope OpCode_scope with OpCode.
 Infix "=?" := OpCode_beq : OpCode_scope.
 
 Global Instance OpCode_beq_spec : reflect_rel (@eq OpCode) OpCode_beq | 10
-  := reflect_of_beq internal_OpCode_dec_bl internal_OpCode_dec_lb.
-Definition OpCode_beq_eq x y : (x =? y)%OpCode = true <-> x = y := conj (@internal_OpCode_dec_bl _ _) (@internal_OpCode_dec_lb _ _).
+  := reflect_of_beq OpCode_dec_bl OpCode_dec_lb.
+Definition OpCode_beq_eq x y : (x =? y)%OpCode = true <-> x = y := conj (@OpCode_dec_bl _ _) (@OpCode_dec_lb _ _).
 Lemma OpCode_beq_neq x y : (x =? y)%OpCode = false <-> x <> y.
 Proof. rewrite <- OpCode_beq_eq; destruct (x =? y)%OpCode; intuition congruence. Qed.
 Global Instance OpCode_beq_compat : Proper (eq ==> eq ==> eq) OpCode_beq | 10.
@@ -169,8 +169,8 @@ Bind Scope OpPrefix_scope with OpPrefix.
 Infix "=?" := OpPrefix_beq : OpPrefix_scope.
 
 Global Instance OpPrefix_beq_spec : reflect_rel (@eq OpPrefix) OpPrefix_beq | 10
-  := reflect_of_beq internal_OpPrefix_dec_bl internal_OpPrefix_dec_lb.
-Definition OpPrefix_beq_eq x y : (x =? y)%OpPrefix = true <-> x = y := conj (@internal_OpPrefix_dec_bl _ _) (@internal_OpPrefix_dec_lb _ _).
+  := reflect_of_beq OpPrefix_dec_bl OpPrefix_dec_lb.
+Definition OpPrefix_beq_eq x y : (x =? y)%OpPrefix = true <-> x = y := conj (@OpPrefix_dec_bl _ _) (@OpPrefix_dec_lb _ _).
 Lemma OpPrefix_beq_neq x y : (x =? y)%OpPrefix = false <-> x <> y.
 Proof. rewrite <- OpPrefix_beq_eq; destruct (x =? y)%OpPrefix; intuition congruence. Qed.
 Global Instance OpPrefix_beq_compat : Proper (eq ==> eq ==> eq) OpPrefix_beq | 10.
diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v
index aff15463cd..bf5dc1f3fc 100644
--- a/src/Assembly/Equivalence.v
+++ b/src/Assembly/Equivalence.v
@@ -1275,10 +1275,10 @@ 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 16 d in
+     let '(initial_reg_idxs, d) := dag_gensym_n (List.length widest_registers) d in
      {|
        dag_state := d;
-       symbolic_reg_state := Tuple.from_list_default None 16 (List.map Some initial_reg_idxs);
+       symbolic_reg_state := Tuple.from_list_default None _ (List.map Some initial_reg_idxs);
        symbolic_mem_state := [];
        symbolic_flag_state := Tuple.repeat None 6;
      |}.
diff --git a/src/Assembly/EquivalenceProofs.v b/src/Assembly/EquivalenceProofs.v
index a4340e146f..f086330c74 100644
--- a/src/Assembly/EquivalenceProofs.v
+++ b/src/Assembly/EquivalenceProofs.v
@@ -1847,7 +1847,7 @@ Qed.
 (* TODO: this is Symbolic.get_reg; move to SymbolicProofs? *)
 Lemma get_reg_set_reg_full s rn rn' v
   : get_reg (set_reg s rn v) rn'
-    = if ((rn <? ((fun n (_ : Tuple.tuple _ n) => n) _ s)) && (rn =? rn'))%nat%bool
+    = if ((rn <? ((fun n (_ : Tuple.tuple _ n) => N.of_nat n) _ s)) && (rn =? rn'))%N%bool
       then Some v
       else get_reg s rn'.
 Proof.
@@ -1863,7 +1863,7 @@ Qed.
 
 (* TODO: this is Symbolic.get_reg; move to SymbolicProofs? *)
 Local Lemma get_reg_set_reg_same s rn v
-      (H : (rn < (fun n (_ : Tuple.tuple _ n) => n) _ s)%nat)
+      (H : (rn < (fun n (_ : Tuple.tuple _ n) => N.of_nat n) _ s)%N)
   : get_reg (set_reg s rn v) rn = Some v.
 Proof.
   rewrite get_reg_set_reg_full; break_innermost_match; reflect_hyps; cbv beta in *; try reflexivity; lia.
diff --git a/src/Assembly/Parse.v b/src/Assembly/Parse.v
index 7b0f313d2a..486c886602 100644
--- a/src/Assembly/Parse.v
+++ b/src/Assembly/Parse.v
@@ -22,34 +22,18 @@ Local Open Scope list_scope.
 Local Open Scope string_scope.
 Local Open Scope parse_scope.
 
-Derive REG_Listable SuchThat (@FinitelyListable REG REG_Listable) As REG_FinitelyListable.
-Proof. prove_ListableDerive. Qed.
-Global Existing Instances REG_Listable REG_FinitelyListable.
-
 Global Instance show_REG : Show REG.
 Proof. prove_Show_enum (). Defined.
 Global Instance show_lvl_REG : ShowLevel REG := show_REG.
 
-Derive FLAG_Listable SuchThat (@FinitelyListable FLAG FLAG_Listable) As FLAG_FinitelyListable.
-Proof. prove_ListableDerive. Qed.
-Global Existing Instances FLAG_Listable FLAG_FinitelyListable.
-
 Global Instance show_FLAG : Show FLAG.
 Proof. prove_Show_enum (). Defined.
 Global Instance show_lvl_FLAG : ShowLevel FLAG := show_FLAG.
 
-Derive OpCode_Listable SuchThat (@FinitelyListable OpCode OpCode_Listable) As OpCode_FinitelyListable.
-Proof. prove_ListableDerive. Qed.
-Global Existing Instances OpCode_Listable OpCode_FinitelyListable.
-
 Global Instance show_OpCode : Show OpCode.
 Proof. prove_Show_enum (). Defined.
 Global Instance show_lvl_OpCode : ShowLevel OpCode := show_OpCode.
 
-Derive OpPrefix_Listable SuchThat (@FinitelyListable OpPrefix OpPrefix_Listable) As OpPrefix_FinitelyListable.
-Proof. prove_ListableDerive. Qed.
-Global Existing Instances OpPrefix_Listable OpPrefix_FinitelyListable.
-
 Global Instance show_OpPrefix : Show OpPrefix.
 Proof. prove_Show_enum (). Defined.
 Global Instance show_lvl_OpPrefix : ShowLevel OpPrefix := show_OpPrefix.
@@ -72,10 +56,6 @@ Definition parse_FLAG_list : list (string * FLAG)
 Definition parse_FLAG : ParserAction FLAG
   := parse_strs parse_FLAG_list.
 
-Derive AccessSize_Listable SuchThat (@FinitelyListable AccessSize AccessSize_Listable) As AccessSize_FinitelyListable.
-Proof. prove_ListableDerive. Qed.
-Global Existing Instances AccessSize_Listable AccessSize_FinitelyListable.
-
 Global Instance show_AccessSize : Show AccessSize.
 Proof. prove_Show_enum (). Defined.
 Global Instance show_lvl_AccessSize : ShowLevel AccessSize := show_AccessSize.
diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v
index 593a30c720..f2a2c93cc3 100644
--- a/src/Assembly/Symbolic.v
+++ b/src/Assembly/Symbolic.v
@@ -3829,7 +3829,7 @@ Definition simplify {opts : symbolic_options_computed_opt} (dag : dag) (e : node
 Lemma eval_simplify {opts : symbolic_options_computed_opt} G d n v : gensym_dag_ok G d -> 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.
+Definition reg_state := Tuple.tuple (option idx) (compute! (List.length widest_registers)).
 Definition flag_state := Tuple.tuple (option idx) 6.
 Definition mem_state := list (idx * idx).
 
@@ -3863,16 +3863,16 @@ Definition reverse_lookup_flag (st : flag_state) (i : idx) : option FLAG
        (List.find (fun v => option_beq N.eqb (Some i) (fst v))
                   (Tuple.to_list _ (Tuple.map2 (@pair _ _) st (CF, PF, AF, ZF, SF, OF)))).
 
-Definition get_reg (st : reg_state) (ri : nat) : option idx
-  := Tuple.nth_default None ri st.
-Definition set_reg (st : reg_state) ri (i : idx) : reg_state
+Definition get_reg (st : reg_state) (ri : N) : option idx
+  := Tuple.nth_default None (N.to_nat ri) st.
+Definition set_reg (st : reg_state) (ri : N) (i : idx) : reg_state
   := Tuple.from_list_default None _ (ListUtil.set_nth
-       ri
+       (N.to_nat ri)
        (Some i)
        (Tuple.to_list _ st)).
 Definition reverse_lookup_widest_reg (st : reg_state) (i : idx) : option REG
   := option_map
-       (fun v => widest_register_of_index (fst v))
+       (fun v => widest_register_of_index (N.of_nat (fst v)))
        (List.find (fun v => option_beq N.eqb (Some i) (snd v))
                   (List.enumerate (Tuple.to_list _ st))).
 
@@ -3906,7 +3906,7 @@ Definition update_mem_with (st : symbolic_state) (f : mem_state -> mem_state) :
   := {| dag_state := st.(dag_state); symbolic_reg_state := st.(symbolic_reg_state) ; symbolic_flag_state := st.(symbolic_flag_state) ; symbolic_mem_state := f st.(symbolic_mem_state) |}.
 
 Global Instance show_reg_state : Show reg_state := fun st =>
-  show (List.map (fun '(n, v) => (widest_register_of_index n, v)) (ListUtil.List.enumerate (Option.List.map id (Tuple.to_list _ st)))).
+  show (List.combine widest_registers (Option.List.map id (Tuple.to_list _ st))).
 
 Global Instance show_flag_state : Show flag_state :=
   fun '(cfv, pfv, afv, zfv, sfv, ofv) => (
@@ -3953,7 +3953,7 @@ Module error.
   Local Unset Decidable Equality Schemes.
   Variant error :=
   | get_flag (f : FLAG) (s : flag_state)
-  | get_reg (r : nat + REG) (s : reg_state)
+  | get_reg (r : N + REG) (s : reg_state)
   | load (a : idx) (s : symbolic_state)
   | remove (a : idx) (s : symbolic_state)
   | remove_has_duplicates (a : idx) (vs : list idx) (s : symbolic_state)
@@ -3977,7 +3977,7 @@ Module error.
             => ["In flag state " ++ show_flag_state s;
                 "Flag " ++ show f ++ " was read without being set."]
           | get_reg (inl i) s
-            => ["Invalid reg index " ++ show_nat i]
+            => ["Invalid reg index " ++ show i]
           | get_reg (inr r) s
             => ["In reg state " ++ show_reg_state s;
                 "Register " ++ show (r : REG) ++ " read without being set."]
@@ -4042,7 +4042,7 @@ Definition mapM_ {A B} (f: A -> M B) l : M unit := _ <- mapM f l; ret tt.
 
 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)%nat
+                    if (reg_index r =? ri)%N
                     then inr r
                     else inl ri).
 
diff --git a/src/Assembly/Syntax.v b/src/Assembly/Syntax.v
index 50dd2e5046..29638b22a2 100644
--- a/src/Assembly/Syntax.v
+++ b/src/Assembly/Syntax.v
@@ -3,7 +3,11 @@ From Coq Require Import NArith.
 From Coq Require Import String.
 From Coq Require Import List.
 From Coq Require Import Derive.
+Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Bool.Reflect.
+Require Import Crypto.Util.Listable.
+Require Import Crypto.Util.ListUtil.
 Require Crypto.Util.Tuple.
 Require Crypto.Util.OptionList.
 Import ListNotations.
@@ -11,8 +15,6 @@ Import ListNotations.
 Local Open Scope list_scope.
 
 Local Set Implicit Arguments.
-Local Set Boolean Equality Schemes.
-Local Set Decidable Equality Schemes.
 Local Set Primitive Projections.
 
 Inductive REG :=
@@ -22,10 +24,27 @@ Inductive REG :=
 | ah | al | ch | cl | dh | dl | bh | bl |  spl |  bpl |  sil |  dil | r8b | r9b | r10b | r11b | r12b | r13b | r14b | r15b
 .
 
+Derive REG_Listable SuchThat (@FinitelyListable REG REG_Listable) As REG_FinitelyListable.
+Proof. prove_ListableDerive. Qed.
+Global Existing Instances REG_Listable REG_FinitelyListable.
+Definition REG_beq : REG -> REG -> bool := eqb_of_listable.
+Definition REG_dec_bl : forall x y, REG_beq x y = true -> x = y := eqb_of_listable_bl.
+Definition REG_dec_lb : forall x y, x = y -> REG_beq x y = true := eqb_of_listable_lb.
+Definition REG_eq_dec : forall x y : REG, {x = y} + {x <> y} := eq_dec_of_listable.
+
 Definition CONST := Z.
 Coercion CONST_of_Z (x : Z) : CONST := x.
 
 Inductive AccessSize := byte | word | dword | qword.
+
+Derive AccessSize_Listable SuchThat (@FinitelyListable AccessSize AccessSize_Listable) As AccessSize_FinitelyListable.
+Proof. prove_ListableDerive. Qed.
+Global Existing Instances AccessSize_Listable AccessSize_FinitelyListable.
+Definition AccessSize_beq : AccessSize -> AccessSize -> bool := eqb_of_listable.
+Definition AccessSize_dec_bl : forall x y, AccessSize_beq x y = true -> x = y := eqb_of_listable_bl.
+Definition AccessSize_dec_lb : forall x y, x = y -> AccessSize_beq x y = true := eqb_of_listable_lb.
+Definition AccessSize_eq_dec : forall x y : AccessSize, {x = y} + {x <> y} := eq_dec_of_listable.
+
 Coercion bits_of_AccessSize (x : AccessSize) : N
   := match x with
      | byte => 8
@@ -41,12 +60,28 @@ Definition mem_of_reg (r : REG) : MEM :=
 
 Inductive FLAG := CF | PF | AF | ZF | SF | OF.
 
+Derive FLAG_Listable SuchThat (@FinitelyListable FLAG FLAG_Listable) As FLAG_FinitelyListable.
+Proof. prove_ListableDerive. Qed.
+Global Existing Instances FLAG_Listable FLAG_FinitelyListable.
+Definition FLAG_beq : FLAG -> FLAG -> bool := eqb_of_listable.
+Definition FLAG_dec_bl : forall x y, FLAG_beq x y = true -> x = y := eqb_of_listable_bl.
+Definition FLAG_dec_lb : forall x y, x = y -> FLAG_beq x y = true := eqb_of_listable_lb.
+Definition FLAG_eq_dec : forall x y : FLAG, {x = y} + {x <> y} := eq_dec_of_listable.
+
 Inductive OpPrefix :=
 | rep
 | repz
 | repnz
 .
 
+Derive OpPrefix_Listable SuchThat (@FinitelyListable OpPrefix OpPrefix_Listable) As OpPrefix_FinitelyListable.
+Proof. prove_ListableDerive. Qed.
+Global Existing Instances OpPrefix_Listable OpPrefix_FinitelyListable.
+Definition OpPrefix_beq : OpPrefix -> OpPrefix -> bool := eqb_of_listable.
+Definition OpPrefix_dec_bl : forall x y, OpPrefix_beq x y = true -> x = y := eqb_of_listable_bl.
+Definition OpPrefix_dec_lb : forall x y, x = y -> OpPrefix_beq x y = true := eqb_of_listable_lb.
+Definition OpPrefix_eq_dec : forall x y : OpPrefix, {x = y} + {x <> y} := eq_dec_of_listable.
+
 Inductive OpCode :=
 | adc
 | adcx
@@ -62,10 +97,10 @@ Inductive OpCode :=
 | cmovo
 | cmp
 | db
+| dw
 | dd
-| dec
 | dq
-| dw
+| dec
 | imul
 | inc
 | je
@@ -95,6 +130,64 @@ Inductive OpCode :=
 | xor
 .
 
+Derive OpCode_Listable SuchThat (@FinitelyListable OpCode OpCode_Listable) As OpCode_FinitelyListable.
+Proof. prove_ListableDerive. Qed.
+Global Existing Instances OpCode_Listable OpCode_FinitelyListable.
+Definition OpCode_beq : OpCode -> OpCode -> bool := eqb_of_listable.
+Definition OpCode_dec_bl : forall x y, OpCode_beq x y = true -> x = y := eqb_of_listable_bl.
+Definition OpCode_dec_lb : forall x y, x = y -> OpCode_beq x y = true := eqb_of_listable_lb.
+Definition OpCode_eq_dec : forall x y : OpCode, {x = y} + {x <> y} := eq_dec_of_listable.
+
+Definition accesssize_of_declaration (opc : OpCode) : option AccessSize :=
+  match opc with
+  | db => Some byte
+  | dd => Some dword
+  | dq => Some qword
+  | dw => Some word
+  | adc
+  | adcx
+  | add
+  | adox
+  | and
+  | bzhi
+  | call
+  | clc
+  | cmovb
+  | cmovc
+  | cmovnz
+  | cmovo
+  | cmp
+  | dec
+  | imul
+  | inc
+  | je
+  | jmp
+  | lea
+  | mov
+  | movzx
+  | mul
+  | mulx
+  | or
+  | pop
+  | push
+  | rcr
+  | ret
+  | sar
+  | sbb
+  | setc
+  | seto
+  | shl
+  | shlx
+  | shr
+  | shrx
+  | shrd
+  | sub
+  | test
+  | xchg
+  | xor
+    => None
+  end.
+
 Record JUMP_LABEL := { jump_near : bool ; label_name : string }.
 
 Inductive ARG := reg (r : REG) | mem (m : MEM) | const (c : CONST) | label (l : JUMP_LABEL).
@@ -172,154 +265,73 @@ Definition operand_size (x : ARG) (operation_size : N) : N :=
   | None => operation_size
   end.
 
-
-Definition reg_index (r : REG) : nat
-  :=  match r with
-      |     rax
-      |     eax
-      |      ax
-      |(ah | al)
-       => 0
-      |     rcx
-      |     ecx
-      |      cx
-      |(ch | cl)
-       => 1
-      |     rdx
-      |     edx
-      |      dx
-      |(dh | dl)
-       => 2
-      |     rbx
-      |     ebx
-      |      bx
-      |(bh | bl)
-       => 3
-      | rsp
-      | esp
-      |  sp
-      |( spl)
-       => 4
-      | rbp
-      | ebp
-      |  bp
-      |( bpl)
-       => 5
-      | rsi
-      | esi
-      |  si
-      |( sil)
-       => 6
-      | rdi
-      | edi
-      |  di
-      |( dil)
-       => 7
-      | r8
-      | r8d
-      | r8w
-      | r8b
-        => 8
-      | r9
-      | r9d
-      | r9w
-      | r9b
-        => 9
-      | r10
-      | r10d
-      | r10w
-      | r10b
-        => 10
-      | r11
-      | r11d
-      | r11w
-      | r11b
-        => 11
-      | r12
-      | r12d
-      | r12w
-      | r12b
-        => 12
-      | r13
-      | r13d
-      | r13w
-      | r13b
-        => 13
-      | r14
-      | r14d
-      | r14w
-      | r14b
-        => 14
-      | r15
-      | r15d
-      | r15w
-      | r15b
-        => 15
-      end.
 Definition reg_offset (r : REG) : N :=
-      match r with
-      |(    rax |     rcx |     rdx |     rbx | rsp  | rbp  | rsi  | rdi  | r8  | r9  | r10  | r11  | r12  | r13  | r14  | r15 )
-      |(    eax |     ecx |     edx |     ebx | esp  | ebp  | esi  | edi  | r8d | r9d | r10d | r11d | r12d | r13d | r14d | r15d)
-      |(     ax |      cx |      dx |      bx |  sp  |  bp  |  si  |  di  | r8w | r9w | r10w | r11w | r12w | r13w | r14w | r15w)
-      |(     al |      cl |      dl |      bl |  spl |  bpl |  sil |  dil | r8b | r9b | r10b | r11b | r12b | r13b | r14b | r15b)
-       => 0
-      |(ah      | ch      | dh      | bh      )
-       => 8
-      end.
-Definition index_and_shift_and_bitcount_of_reg (r : REG) :=
-  (reg_index r, reg_offset r, reg_size r).
+    match r with
+    |(ah      | ch      | dh      | bh      )
+      => 8
+    | _ => 0
+    end.
 
-Definition regs_of_index (index : nat) : list (list REG) :=
-  match index with
-  |  0 => [ [  al ; ah] ; [  ax] ; [ eax] ; [rax] ]
-  |  1 => [ [  cl ; ch] ; [  cx] ; [ ecx] ; [rcx] ]
-  |  2 => [ [  dl ; dh] ; [  dx] ; [ edx] ; [rdx] ]
-  |  3 => [ [  bl ; bh] ; [  bx] ; [ ebx] ; [rbx] ]
-  |  4 => [ [ spl     ] ; [  sp] ; [ esp] ; [rsp] ]
-  |  5 => [ [ bpl     ] ; [  bp] ; [ ebp] ; [rbp] ]
-  |  6 => [ [ sil     ] ; [  si] ; [ esi] ; [rsi] ]
-  |  7 => [ [ dil     ] ; [  di] ; [ edi] ; [rdi] ]
-  |  8 => [ [ r8b     ] ; [ r8w] ; [ r8d] ; [r8 ] ]
-  |  9 => [ [ r9b     ] ; [ r9w] ; [ r9d] ; [r9 ] ]
-  | 10 => [ [r10b     ] ; [r10w] ; [r10d] ; [r10] ]
-  | 11 => [ [r11b     ] ; [r11w] ; [r11d] ; [r11] ]
-  | 12 => [ [r12b     ] ; [r12w] ; [r12d] ; [r12] ]
-  | 13 => [ [r13b     ] ; [r13w] ; [r13d] ; [r13] ]
-  | 14 => [ [r14b     ] ; [r14w] ; [r14d] ; [r14] ]
-  | 15 => [ [r15b     ] ; [r15w] ; [r15d] ; [r15] ]
-  | _  => []
+Definition widest_register_of (r : REG) : REG :=
+  match r with
+  | ((al | ah) | ax | eax | rax) => rax
+  | ((cl | ch) | cx | ecx | rcx) => rcx
+  | ((dl | dh) | dx | edx | rdx) => rdx
+  | ((bl | bh) | bx | ebx | rbx) => rbx
+  | (spl | sp | esp | rsp) => rsp
+  | (bpl | bp | ebp | rbp) => rbp
+  | (sil | si | esi | rsi) => rsi
+  | (dil | di | edi | rdi) => rdi
+  | (r8b | r8w | r8d | r8) => r8
+  | (r9b | r9w | r9d | r9) => r9
+  | (r10b | r10w | r10d | r10) => r10
+  | (r11b | r11w | r11d | r11) => r11
+  | (r12b | r12w | r12d | r12) => r12
+  | (r13b | r13w | r13d | r13) => r13
+  | (r14b | r14w | r14d | r14) => r14
+  | (r15b | r15w | r15d | r15) => r15
   end.
 
+Definition widest_registers := Eval lazy in List.filter (fun x => REG_beq x (widest_register_of x)) (list_all REG).
+
+Definition wide_reg_index_pairs := Eval lazy in List.map (fun '(n, r) => (N.of_nat n, r)) (List.enumerate widest_registers).
+
+Definition eta_reg {A} : (REG -> A) -> (REG -> A).
+Proof.
+  intros f r; pose (f r) as fr; destruct r.
+  all: let v := eval cbv in fr in exact v.
+Defined.
+
+Definition reg_index (r : REG) : N := Eval lazy in
+  eta_reg (fun r =>
+    Option.value
+      (option_map (@fst _ _) (find (fun '(n, r') => REG_beq (widest_register_of r) r') wide_reg_index_pairs))
+      0%N)
+    r.
+
+Definition widest_register_of_index_opt (n : N) : option REG
+  := List.nth_error (List.map (@snd _ _) wide_reg_index_pairs) (N.to_nat n).
+
 (** convenience printing function *)
-Definition widest_register_of_index (n : nat) : REG
-  := match n with
-     | 0 => rax
-     | 1 => rcx
-     | 2 => rdx
-     | 3 => rbx
-     | 4 => rsp
-     | 5 => rbp
-     | 6 => rsi
-     | 7 => rdi
-     | 8 => r8
-     | 9 => r9
-     | 10 => r10
-     | 11 => r11
-     | 12 => r12
-     | 13 => r13
-     | 14 => r14
-     | 15 => r15
-     | _ => rax
-     end%nat.
+Definition widest_register_of_index (n : N) : REG
+  := Option.value (widest_register_of_index_opt n) rax.
+
+Definition widest_reg_size_of (r : REG) : N :=
+  reg_size (widest_register_of_index (reg_index r)).
+
+Definition index_and_shift_and_bitcount_of_reg (r : REG) :=
+  (reg_index r, reg_offset r, reg_size r).
+
+Definition overlapping_registers (r : REG) : list REG := Eval lazy in eta_reg
+  (fun r => List.filter (fun r' => REG_beq (widest_register_of r) (widest_register_of r')) (list_all REG))
+  r.
 
 Definition reg_of_index_and_shift_and_bitcount_opt :=
   fun '(index, offset, size) =>
-    let sz := N.log2 (size / 8) in
-    let offset_n := (offset / 8)%N in
-    if ((8 * 2^sz =? size) && (offset =? offset_n * 8))%N%bool
-    then (rs <- nth_error (regs_of_index index) (N.to_nat sz);
-          nth_error rs (N.to_nat offset_n))%option
-    else None.
+    (wr <- widest_register_of_index_opt index;
+    let rs := overlapping_registers wr in
+    List.find (fun r => ((reg_size r =? size) && (reg_offset r =? offset))%N%bool) rs)%option.
+
 Definition reg_of_index_and_shift_and_bitcount :=
   fun '(index, offset, size) =>
     match reg_of_index_and_shift_and_bitcount_opt (index, offset, size) with
@@ -327,59 +339,6 @@ Definition reg_of_index_and_shift_and_bitcount :=
     | None => widest_register_of_index index
     end.
 
-Lemma widest_register_of_index_correct
-  : forall n,
-    (~exists r, reg_index r = n)
-    \/ (let r := widest_register_of_index n in reg_index r = n
-       /\ forall r', reg_index r' = n -> r = r' \/ (reg_size r' < reg_size r)%N).
-Proof.
-  intro n; set (r := widest_register_of_index n).
-  cbv in r.
-  repeat match goal with r := context[match ?n with _ => _ end] |- _ => destruct n; [ right | ] end;
-    [ .. | left; intros [ [] H]; cbv in H; congruence ].
-  all: subst r; split; [ reflexivity | ].
-  all: intros [] H; cbv in H; try (exfalso; congruence).
-  all: try (left; reflexivity).
-  all: try (right; vm_compute; reflexivity).
-Qed.
-
-Lemma reg_of_index_and_shift_and_bitcount_opt_correct v r
-  : reg_of_index_and_shift_and_bitcount_opt v = Some r <-> index_and_shift_and_bitcount_of_reg r = v.
-Proof.
-  split; [ | intro; subst; destruct r; vm_compute; reflexivity ].
-  cbv [index_and_shift_and_bitcount_of_reg]; destruct v as [ [index shift] bitcount ].
-  cbv [reg_of_index_and_shift_and_bitcount_opt].
-  generalize (shift / 8)%N (N.log2 (bitcount / 8)); intros *.
-  repeat first [ congruence
-               | progress subst
-               | match goal with
-                 | [ H : _ /\ _ |- _ ] => destruct H
-                 | [ H : N.to_nat _ = _ |- _ ] => apply (f_equal N.of_nat) in H; rewrite N2Nat.id in H; subst
-                 | [ |- Some _ = Some _ -> _ ] => inversion 1; subst
-                 | [ |- context[match ?x with _ => _ end] ] => destruct x eqn:?; subst
-                 end
-               | progress cbv [regs_of_index]
-               | match goal with
-                 | [ |- context[nth_error _ ?n] ] => destruct n eqn:?; cbn [nth_error Option.bind]
-                 end
-               | rewrite Bool.andb_true_iff, ?N.eqb_eq in * |- ].
-  all: vm_compute; reflexivity.
-Qed.
-
-Lemma reg_of_index_and_shift_and_bitcount_of_reg r
-  : reg_of_index_and_shift_and_bitcount (index_and_shift_and_bitcount_of_reg r) = r.
-Proof. destruct r; vm_compute; reflexivity. Qed.
-
-Lemma reg_of_index_and_shift_and_bitcount_eq v r
-  : reg_of_index_and_shift_and_bitcount v = r
-    -> (index_and_shift_and_bitcount_of_reg r = v
-        \/ ((~exists r, index_and_shift_and_bitcount_of_reg r = v)
-            /\ r = widest_register_of_index (fst (fst v)))).
-Proof.
-  cbv [reg_of_index_and_shift_and_bitcount].
-  destruct v as [ [index offset] size ].
-  destruct reg_of_index_and_shift_and_bitcount_opt eqn:H;
-    [ left | right; split; [ intros [r' H'] | ] ]; subst; try reflexivity.
-  { rewrite reg_of_index_and_shift_and_bitcount_opt_correct in H; assumption. }
-  { rewrite <- reg_of_index_and_shift_and_bitcount_opt_correct in H'; congruence. }
-Qed.
+Class assembly_program_options := {
+  default_rel : bool ;
+}.
diff --git a/src/Assembly/SyntaxTests.v b/src/Assembly/SyntaxTests.v
new file mode 100644
index 0000000000..4659c239df
--- /dev/null
+++ b/src/Assembly/SyntaxTests.v
@@ -0,0 +1,155 @@
+From Coq Require Import ZArith.
+From Coq Require Import NArith.
+From Coq Require Import String.
+From Coq Require Import List.
+From Coq Require Import Derive.
+Require Import Crypto.Util.Prod.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Bool.Reflect.
+Require Import Crypto.Util.Listable.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Assembly.Syntax.
+Require Crypto.Util.Tuple.
+Require Crypto.Util.OptionList.
+Import ListNotations.
+
+Local Open Scope list_scope.
+
+Local Set Implicit Arguments.
+Local Set Primitive Projections.
+
+Local Coercion N.of_nat : nat >-> N.
+
+Lemma reg_of_index_and_shift_and_bitcount_opt_of_index_and_shift_and_bitcount_of_reg : forall r : REG, reg_of_index_and_shift_and_bitcount_opt (index_and_shift_and_bitcount_of_reg r) = Some r.
+Proof. destruct r; vm_compute; try reflexivity. Defined.
+
+Lemma reg_of_index_and_shift_and_bitcount_of_index_and_shift_and_bitcount_of_reg : forall r : REG, reg_of_index_and_shift_and_bitcount (index_and_shift_and_bitcount_of_reg r) = r.
+Proof. destruct r; vm_compute; reflexivity. Defined.
+
+Lemma reg_index_widest_register_of : forall r : REG, reg_index (widest_register_of r) = reg_index r.
+Proof. destruct r; reflexivity. Defined.
+
+Lemma reg_index_widest_register_of_index_opt : forall index : N, (N.to_nat index <? List.length widest_registers) = true -> option_map reg_index (widest_register_of_index_opt index) = Some index.
+Proof.
+  intros index; cbv [widest_register_of_index_opt].
+  rewrite <- (N2Nat.id index), Nat2N.id; generalize (N.to_nat index); clear index; intro index.
+  vm_compute List.map.
+  vm_compute List.length.
+  cbv [Nat.ltb]; cbn [Nat.leb].
+  repeat lazymatch goal with
+  | [ |- false = true -> _ ] => discriminate
+  | [ |- (?index <=? _) = true -> _ ] =>
+      is_var index; destruct index; [ reflexivity | cbn [Nat.leb] ]
+  end.
+Qed.
+
+Lemma widest_register_of_index_opt_Some_length_iff : forall index : N, (exists r, widest_register_of_index_opt index = Some r) <-> (N.to_nat index <? List.length widest_registers) = true.
+Proof.
+  intros index; cbv [widest_register_of_index_opt].
+  rewrite <- (N2Nat.id index), Nat2N.id; generalize (N.to_nat index); clear index; intro index.
+  vm_compute List.map.
+  vm_compute List.length.
+  cbv [Nat.ltb]; cbn [Nat.leb].
+  repeat lazymatch goal with
+  | [ |- (exists r, nth_error nil ?index = Some _) <-> _ ] => is_var index; destruct index; cbn [nth_error]
+  | [ |- _ <-> false = true ] => split; [ | discriminate ]
+  | [ |- _ <-> true = true ] => repeat esplit
+  | [ |- _ <-> (?index <=? _) = true ] =>
+      is_var index; destruct index; cbn [Nat.leb nth_error]
+  end.
+  all: intros [? H]; discriminate.
+Qed.
+
+Lemma reg_index_widest_register_of_index : forall index : N, (N.to_nat index <? List.length widest_registers) = true -> reg_index (widest_register_of_index index) = index.
+Proof.
+  intros index H; cbv [widest_register_of_index].
+  apply reg_index_widest_register_of_index_opt in H.
+  destruct widest_register_of_index_opt; cbv [option_map] in *; inversion H; subst.
+  reflexivity.
+Qed.
+
+Lemma reg_index_overlapping_registers : forall r r' n, nth_error (overlapping_registers r) n = Some r' -> reg_index r' = reg_index r.
+Proof.
+  intros r r' n; destruct r.
+  all: vm_compute overlapping_registers.
+  all: repeat lazymatch goal with
+  | [ |- nth_error (_ :: _) ?v = Some _ -> _ ] => is_var v; destruct v; cbn [nth_error]
+  | [ |- nth_error [] ?v = Some _ -> _ ] => is_var v; destruct v; cbn [nth_error]
+  | [ |- Some _ = Some _ -> _ ] => let H := fresh in intro H; inversion H
+  | [ |- None = Some _ -> _ ] => let H := fresh in intro H; inversion H
+  end.
+  all: subst; reflexivity.
+Qed.
+
+Lemma reg_of_index_and_shift_and_bitcount_of_reg r
+  : reg_of_index_and_shift_and_bitcount (index_and_shift_and_bitcount_of_reg r) = r.
+Proof. destruct r; vm_compute; reflexivity. Qed.
+
+Lemma widest_register_of_index_opt_correct
+  : forall n r, widest_register_of_index_opt n = Some r ->
+      reg_index r = n
+       /\ forall r', reg_index r' = n -> r = r' \/ (reg_size r' < reg_size r)%N.
+Proof.
+  intros n r H.
+  epose proof (proj1 (widest_register_of_index_opt_Some_length_iff _) (ex_intro _ _ H)) as H'.
+  pose proof H' as H''.
+  apply reg_index_widest_register_of_index_opt in H''.
+  rewrite H in H''; cbn in H''; inversion H''; subst.
+  split; [ reflexivity | ].
+  destruct r, r'.
+  all: vm_compute; try (constructor; reflexivity); try discriminate.
+Qed.
+
+Lemma widest_register_of_index_correct
+  : forall n,
+    (~exists r, reg_index r = n)
+    \/ (let r := widest_register_of_index n in reg_index r = n
+       /\ forall r', reg_index r' = n -> r = r' \/ (reg_size r' < reg_size r)%N).
+Proof.
+  intro n; pose proof (widest_register_of_index_opt_correct n) as H.
+  cbv [widest_register_of_index].
+  destruct (widest_register_of_index_opt n) as [r |] eqn:H'; [ right; apply H; reflexivity | left ].
+  intros [ [] H'' ]; subst; cbv in H'.
+  all: inversion H'.
+Qed.
+
+Lemma reg_of_index_and_shift_and_bitcount_opt_correct v r
+  : reg_of_index_and_shift_and_bitcount_opt v = Some r <-> index_and_shift_and_bitcount_of_reg r = v.
+Proof.
+  split; [ | intro; subst; destruct r; vm_compute; reflexivity ].
+  cbv [index_and_shift_and_bitcount_of_reg]; destruct v as [ [index shift] bitcount ].
+  cbv [reg_of_index_and_shift_and_bitcount_opt].
+  pose proof (reg_index_widest_register_of_index index) as H''.
+  cbv [widest_register_of_index] in H''.
+  rewrite <- widest_register_of_index_opt_Some_length_iff in H''.
+  destruct widest_register_of_index_opt eqn:H; [ | intro H'; cbv in H'; now inversion H' ].
+  cbv [Option.bind Option.sequence_return] in *.
+  specialize (H'' (ex_intro _ _ eq_refl)).
+  subst.
+  rewrite find_some_iff.
+  repeat first
+    [ progress intros
+    | progress destruct_head'_ex
+    | progress destruct_head'_and
+    | progress reflect_hyps
+    | progress subst
+    | match goal with
+      | [ H : nth_error (overlapping_registers _) _ = Some _ |- _ ] =>
+          apply reg_index_overlapping_registers in H; try rewrite H
+      end
+    | reflexivity ].
+Qed.
+
+Lemma reg_of_index_and_shift_and_bitcount_eq v r
+  : reg_of_index_and_shift_and_bitcount v = r
+    -> (index_and_shift_and_bitcount_of_reg r = v
+        \/ ((~exists r, index_and_shift_and_bitcount_of_reg r = v)
+            /\ r = widest_register_of_index (fst (fst v)))).
+Proof.
+  cbv [reg_of_index_and_shift_and_bitcount].
+  destruct v as [ [index offset] size ].
+  destruct reg_of_index_and_shift_and_bitcount_opt eqn:H;
+    [ left | right; split; [ intros [r' H'] | ] ]; subst; try reflexivity.
+  { rewrite reg_of_index_and_shift_and_bitcount_opt_correct in H; assumption. }
+  { rewrite <- reg_of_index_and_shift_and_bitcount_opt_correct in H'; congruence. }
+Qed.
diff --git a/src/Assembly/WithBedrock/Proofs.v b/src/Assembly/WithBedrock/Proofs.v
index aa0cf55824..08ec58e652 100644
--- a/src/Assembly/WithBedrock/Proofs.v
+++ b/src/Assembly/WithBedrock/Proofs.v
@@ -245,7 +245,7 @@ Definition init_symbolic_state_G (m : machine_state)
         let '(initial_reg_idxs, (G, d)) := dag_gensym_n_G vals st in
         (G,
          {| dag_state := d
-            ; symbolic_reg_state := Tuple.from_list_default None 16 (List.map Some initial_reg_idxs)
+            ; symbolic_reg_state := Tuple.from_list_default None _ (List.map Some initial_reg_idxs)
             ; symbolic_flag_state := Tuple.repeat None 6
             ; symbolic_mem_state := []
          |}).
@@ -254,7 +254,7 @@ Lemma init_symbolic_state_eq_G G d m
   : init_symbolic_state d = snd (init_symbolic_state_G m (G, d)).
 Proof.
   cbv [init_symbolic_state init_symbolic_state_G].
-  epose proof (dag_gensym_n_eq_G G d (Tuple.to_list 16 m.(machine_reg_state))) as H.
+  epose proof (dag_gensym_n_eq_G G d (Tuple.to_list _ m.(machine_reg_state))) as H.
   rewrite Tuple.length_to_list in H; rewrite H; clear H.
   eta_expand; cbn [fst snd].
   reflexivity.
@@ -266,7 +266,7 @@ Lemma init_symbolic_state_G_ok m G d G' ss
       (H : init_symbolic_state_G m (G, d) = (G', ss))
       (d' := ss.(dag_state))
       (Hframe : frame m)
-      (Hbounds : Forall (fun v => (0 <= v < 2^64)%Z) (Tuple.to_list 16 m.(machine_reg_state)))
+      (Hbounds : Forall (fun v => (0 <= v < 2^64)%Z) (Tuple.to_list _ m.(machine_reg_state)))
   : R frame G' ss m
     /\ (forall reg, Option.is_Some (Symbolic.get_reg ss.(symbolic_reg_state) (reg_index reg)) = true)
     /\ gensym_dag_ok G' d'
@@ -291,11 +291,11 @@ Proof.
          by (eapply dag_gensym_n_G_ok; [ | eta_expand; reflexivity | ]; assumption).
        clear; cbv [reg_index]; break_innermost_match; lia. }
   set (v := dag_gensym_n_G _ _) in *; clearbody v; destruct_head'_prod; cbn [fst snd] in *.
-  eassert (H' : Tuple.to_list 16 m.(machine_reg_state) = _).
+  eassert (H' : Tuple.to_list _ m.(machine_reg_state) = _).
   { repeat match goal with H : _ |- _ => clear H end.
       cbv [Tuple.to_list Tuple.to_list'].
       set_evars; eta_expand; subst_evars; reflexivity. }
-  generalize dependent (Tuple.to_list 16 m.(machine_reg_state)); intros; subst.
+  generalize dependent (Tuple.to_list _ m.(machine_reg_state)); intros; subst.
   repeat match goal with H : context[?x :: _] |- _ => assert_fails is_var x; set x in * end.
   repeat match goal with H : Forall2 _ ?v (_ :: _) |- _ => is_var v; inversion H; clear H; subst end.
   repeat match goal with H : Forall2 _ ?v nil |- _ => is_var v; inversion H; clear H; subst end.
@@ -313,7 +313,7 @@ Lemma init_symbolic_state_ok m G d
       (Hd : gensym_dag_ok G d)
       (ss := init_symbolic_state d)
       (d' := ss.(dag_state))
-      (Hbounds : Forall (fun v => (0 <= v < 2^64)%Z) (Tuple.to_list 16 m.(machine_reg_state)))
+      (Hbounds : Forall (fun v => (0 <= v < 2^64)%Z) (Tuple.to_list _ m.(machine_reg_state)))
       (Hframe : frame m)
   : exists G',
     R frame G' ss m
@@ -332,12 +332,12 @@ Lemma get_reg_of_R_regs G d r mr reg
   : forall idx', Symbolic.get_reg r (reg_index reg) = Some idx' -> eval_idx_Z G d idx' (Semantics.get_reg mr reg).
 Proof.
   assert (reg_offset reg = 0%N) by now destruct reg.
-  assert (reg_index reg < length (Tuple.to_list _ r))
+  assert (N.to_nat (reg_index reg) < List.length (Tuple.to_list _ r))
     by now rewrite Tuple.length_to_list; destruct reg; cbv [reg_index]; lia.
   cbv [Symbolic.get_reg Semantics.get_reg R_regs] in *.
   rewrite Tuple.fieldwise_to_list_iff in Hreg.
   erewrite @Forall2_forall_iff in Hreg by now rewrite !Tuple.length_to_list.
-  specialize (Hreg (reg_index reg) ltac:(assumption)); rewrite !@Tuple.nth_default_to_list in *.
+  specialize (Hreg (N.to_nat (reg_index reg)) ltac:(assumption)); rewrite !@Tuple.nth_default_to_list in *.
   cbv [index_and_shift_and_bitcount_of_reg] in *.
   generalize dependent (reg_size reg); intros; subst.
   generalize dependent (reg_offset reg); intros; subst.
@@ -464,7 +464,7 @@ Definition R_regs_preserved_v rn (m : Semantics.reg_state)
   := Z.land (Tuple.nth_default 0%Z rn m) (Z.ones 64).
 
 Definition R_regs_preserved G d G' d' (m : Semantics.reg_state) rs rs'
-  := forall rn idx, Symbolic.get_reg rs' rn = Some idx -> exists idx', Symbolic.get_reg rs rn = Some idx' /\ let v := R_regs_preserved_v rn m in eval_idx_Z G d idx' v -> eval_idx_Z G' d' idx v.
+  := forall rn idx, Symbolic.get_reg rs' rn = Some idx -> exists idx', Symbolic.get_reg rs rn = Some idx' /\ let v := R_regs_preserved_v (N.to_nat rn) m in eval_idx_Z G d idx' v -> eval_idx_Z G' d' idx v.
 
 Global Instance R_regs_preserved_Reflexive G d m : Reflexive (R_regs_preserved G d G d m) | 100.
 Proof. intro; cbv [R_regs_preserved]; eauto. Qed.
@@ -476,19 +476,22 @@ Lemma R_regs_subsumed_get_reg_same_eval G d G' d' rs rs' rm
 Proof.
   cbv [R_regs Symbolic.get_reg R_regs_preserved R_regs_preserved_v] in *.
   rewrite @Tuple.fieldwise_to_list_iff, @Forall2_forall_iff_nth_error in *.
-  intro i; specialize (H i); specialize (H_impl i).
+  intro i; specialize (H i); specialize (H_impl (N.of_nat i)).
   rewrite <- !@Tuple.nth_default_to_list in *.
   cbv [nth_default option_eq] in *.
   repeat first [ progress destruct_head'_and
                | progress destruct_head'_ex
+               | progress inversion_option
                | rewrite @Tuple.length_to_list in *
                | progress cbv [R_reg eval_idx_Z] in *
                | progress break_innermost_match
                | progress break_innermost_match_hyps
+               | rewrite !Nat2N.id in *
                | now auto
                | progress intros
                | progress subst
                | match goal with
+                 | [ H : ?x = Some ?a, H' : ?x = Some ?b |- _ ] => rewrite H in H'
                  | [ H : nth_error _ _ = None |- _ ] => apply nth_error_error_length in H
                  | [ H : ?i >= ?n, H' : context[nth_error (Tuple.to_list ?n _) ?i] |- _ ]
                    => rewrite nth_error_length_error in H' by now rewrite Tuple.length_to_list; lia
@@ -501,12 +504,13 @@ Qed.
 
 Lemma R_regs_preserved_set_reg G d G' d' rs rs' ri rm v
       (H : R_regs_preserved G d G' d' rm rs rs')
-      (H_same : (ri < 16)%nat -> exists idx, Symbolic.get_reg rs ri = Some idx /\ let v' := R_regs_preserved_v ri rm in eval_idx_Z G d idx v' -> eval_idx_Z G' d' v v')
+      (H_same : (ri < N.of_nat (List.length widest_registers))%N -> exists idx, Symbolic.get_reg rs ri = Some idx /\ let v' := R_regs_preserved_v (N.to_nat ri) rm in eval_idx_Z G d idx v' -> eval_idx_Z G' d' v v')
   : R_regs_preserved G d G' d' rm rs (Symbolic.set_reg rs' ri v).
 Proof.
   cbv [R_regs_preserved] in *.
   intros rn idx; specialize (H rn).
   rewrite get_reg_set_reg_full; intro.
+  vm_compute (length widest_registers) in *.
   repeat first [ progress break_innermost_match_hyps
                | progress inversion_option
                | progress subst
@@ -527,7 +531,7 @@ Qed.
 
 Lemma R_regs_preserved_fold_left_set_reg_index {T1 T2} G d G' d' rs rs' rm (r_idxs : list (_ * (_ * T1 + _ * T2)))
       (H : R_regs_preserved G d G' d' rm rs rs')
-      (H_same : Forall (fun '(r, v) => let v := match v with inl (v, _) => v | inr (v, _) => v end in exists idx, Symbolic.get_reg rs (reg_index r) = Some idx /\ let v' := R_regs_preserved_v (reg_index r) rm in eval_idx_Z G d idx v' -> eval_idx_Z G' d' v v') r_idxs)
+      (H_same : Forall (fun '(r, v) => let v := match v with inl (v, _) => v | inr (v, _) => v end in exists idx, Symbolic.get_reg rs (reg_index r) = Some idx /\ let v' := R_regs_preserved_v (N.to_nat (reg_index r)) rm in eval_idx_Z G d idx v' -> eval_idx_Z G' d' v v') r_idxs)
   : R_regs_preserved
       G d G' d' rm
       rs
@@ -548,12 +552,12 @@ Qed.
 Lemma Semantics_get_reg_eq_nth_default_of_R_regs G d ss ms r
       (Hsz : reg_size r = 64%N)
       (HR : R_regs G d ss ms)
-  : Semantics.get_reg ms r = Tuple.nth_default 0%Z (reg_index r) (ms : Semantics.reg_state).
+  : Semantics.get_reg ms r = Tuple.nth_default 0%Z (N.to_nat (reg_index r)) (ms : Semantics.reg_state).
 Proof.
   assert (Hro : reg_offset r = 0%N) by now revert Hsz; clear; cbv; destruct r; lia.
   cbv [R_regs R_reg] in HR.
   rewrite Tuple.fieldwise_to_list_iff, Forall2_forall_iff_nth_error in HR.
-  specialize (HR (reg_index r)).
+  specialize (HR (N.to_nat (reg_index r))).
   cbv [Semantics.get_reg index_and_shift_and_bitcount_of_reg].
   rewrite Hro, Hsz; change (Z.of_N 0) with 0%Z; change (Z.of_N 64) with 64%Z.
   rewrite Z.shiftr_0_r, <- Tuple.nth_default_to_list; cbv [nth_default option_eq] in *.
@@ -563,7 +567,7 @@ Qed.
 Lemma Semantics_get_reg_eq_nth_default_of_R frame G ss ms r
       (Hsz : reg_size r = 64%N)
       (HR : R frame G ss ms)
-  : Semantics.get_reg ms r = Tuple.nth_default 0%Z (reg_index r) (ms : Semantics.reg_state).
+  : Semantics.get_reg ms r = Tuple.nth_default 0%Z (N.to_nat (reg_index r)) (ms : Semantics.reg_state).
 Proof.
   destruct ss, ms; eapply Semantics_get_reg_eq_nth_default_of_R_regs; try eassumption; apply HR.
 Qed.
@@ -586,7 +590,7 @@ Lemma Forall2_R_regs_preserved_same_helper G d reg_available idxs m rs
   : Forall (fun '(r, v)
             => let v := match v with inl (v, _) => v | inr (v, _) => v end in
                exists idx, Symbolic.get_reg rs (reg_index r) = Some idx
-                           /\ let v' := R_regs_preserved_v (reg_index r) m in eval_idx_Z G d idx v' -> eval_idx_Z G d v v')
+                           /\ let v' := R_regs_preserved_v (N.to_nat (reg_index r)) m in eval_idx_Z G d idx v' -> eval_idx_Z G d v v')
            (List.combine reg_available idxs).
 Proof.
   cbv [get_asm_reg] in *.
diff --git a/src/Assembly/WithBedrock/Semantics.v b/src/Assembly/WithBedrock/Semantics.v
index f436d155d7..695e4aa6c2 100644
--- a/src/Assembly/WithBedrock/Semantics.v
+++ b/src/Assembly/WithBedrock/Semantics.v
@@ -53,23 +53,23 @@ Definition havoc_flag (st : flag_state) (f : FLAG) : flag_state
 Definition havoc_flags : flag_state
   := (None, None, None, None, None, None).
 
-Definition reg_state := Tuple.tuple Z 16.
+Definition reg_state := Tuple.tuple Z (compute! (List.length widest_registers)).
 Definition bitmask_of_reg (r : REG) : Z
   := let '(idx, shift, bitcount) := index_and_shift_and_bitcount_of_reg r in
      Z.shiftl (Z.ones (Z.of_N bitcount)) (Z.of_N shift).
 Definition get_reg (st : reg_state) (r : REG) : Z
   := let '(idx, shift, bitcount) := index_and_shift_and_bitcount_of_reg r in
-  let rv := Tuple.nth_default 0%Z idx st in
+  let rv := Tuple.nth_default 0%Z (N.to_nat idx) st in
   Z.land (Z.shiftr rv (Z.of_N shift)) (Z.ones (Z.of_N bitcount)).
 Definition set_reg (st : reg_state) (r : REG) (v : Z) : reg_state
   := let '(idx, shift, bitcount) := index_and_shift_and_bitcount_of_reg r in
      Tuple.from_list_default 0%Z _ (ListUtil.update_nth
-       idx
+       (N.to_nat idx)
        (fun curv => Z.lor (Z.shiftl (Z.land v (Z.ones (Z.of_N bitcount))) (Z.of_N shift))
                           (Z.ldiff curv (Z.shiftl (Z.ones (Z.of_N bitcount)) (Z.of_N shift))))
        (Tuple.to_list _ st)).
 Definition annotate_reg_state (st : reg_state) : list (REG * Z)
-  := List.map (fun '(n, v) => (widest_register_of_index n, v)) (enumerate (Tuple.to_list _ st)).
+  := List.combine widest_registers (Tuple.to_list _ st).
 Ltac print_reg_state st := let st' := (eval cbv in (annotate_reg_state st)) in idtac st'.
 
 (* Kludge since [byte] isn't present in Coq 8.9 *)
diff --git a/src/Assembly/WithBedrock/SymbolicProofs.v b/src/Assembly/WithBedrock/SymbolicProofs.v
index 38e9c0ccaf..a5ffb70215 100644
--- a/src/Assembly/WithBedrock/SymbolicProofs.v
+++ b/src/Assembly/WithBedrock/SymbolicProofs.v
@@ -314,7 +314,7 @@ Qed.
 
 Lemma get_reg_R_regs d s m (HR : R_regs d s m) ri :
   forall i, Symbolic.get_reg s ri = Some i ->
-  exists v, eval d i v /\ Tuple.nth_default 0 ri m = v.
+  exists v, eval d i v /\ Tuple.nth_default 0 (N.to_nat ri) m = v.
 Proof using Type.
   cbv [Symbolic.get_reg]; intros.
   rewrite <-Tuple.nth_default_to_list in H.
@@ -336,7 +336,7 @@ Qed.
 
 Lemma get_reg_R s m (HR : R s m) ri :
   forall i, Symbolic.get_reg s ri = Some i ->
-  exists v, eval s i v /\ Tuple.nth_default 0 ri (m : reg_state) = v.
+  exists v, eval s i v /\ Tuple.nth_default 0 (N.to_nat ri) (m : reg_state) = v.
 Proof using Type.
   destruct s, m; apply get_reg_R_regs, HR.
 Qed.
diff --git a/src/Util/Listable.v b/src/Util/Listable.v
index feaad2c888..f898c909e7 100644
--- a/src/Util/Listable.v
+++ b/src/Util/Listable.v
@@ -7,6 +7,7 @@ Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Bool.Reflect.
 Import ListNotations.
 
+(* TODO: move to using [N] for performance instead of [nat] *)
 Class Listable T := { list_all : list T ; find_index : T -> nat }.
 
 Arguments find_index {T} {_} _.