Merge remote-tracking branch 'james/develop' into developdev-nadesh-merge

5 files changed, 377 insertions, 451 deletions

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index ba0a5dc..c9361c2 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -23,12 +23,14 @@ From Coq Require Export
      List
      Bool.
 
+Require Import Lia.
+
 From coqup Require Import Show.
 
 (* Depend on CompCert for the basic library, as they declare and prove some
    useful theorems. *)
 From compcert.lib Require Export Coqlib.
-From compcert Require Integers.
+From compcert Require Import Integers.
 
 Ltac unfold_rec c := unfold c; fold c.
 
@@ -44,18 +46,21 @@ Ltac solve_by_invert := solve_by_inverts 1.
 
 Ltac invert x := inversion x; subst; clear x.
 
+Ltac destruct_match :=
+  match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x end.
+
 Ltac clear_obvious :=
   repeat match goal with
          | [ H : ex _ |- _ ] => invert H
-         | [ H : ?C _ = ?C _ |- _ ] => invert H
+         | [ H : Some _ = Some _ |- _ ] => invert H
          | [ H : _ /\ _ |- _ ] => invert H
          end.
 
 Ltac nicify_goals :=
   repeat match goal with
          | [ |- _ /\ _ ] => split
-         | [ |- Some _ = Some _ ] => try reflexivity
-         | [ _ : ?x |- ?x ] => assumption
+         | [ |- Some _ = Some _ ] => f_equal
+         | [ |- S _ = S _ ] => f_equal
          end.
 
 Ltac kill_bools :=
@@ -124,9 +129,9 @@ Ltac unfold_constants :=
            end
          end.
 
-Ltac simplify := unfold_constants; simpl in *;
-                 repeat (clear_obvious; nicify_goals; kill_bools);
-                 simpl in *; try discriminate.
+Ltac crush := intros; unfold_constants; simpl in *;
+              repeat (clear_obvious; nicify_goals; kill_bools);
+              simpl in *; try discriminate; try congruence; try lia; try assumption.
 
 Global Opaque Nat.div.
 Global Opaque Z.mul.
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index 7d3156b..6bac18d 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -27,7 +27,7 @@ Module PtrofsExtra.
       rewrite Zmod_mod
     | [ _ : _ |- context[(_ mod Ptrofs.modulus) mod m ] ] =>
       rewrite <- Zmod_div_mod;
-      try (simplify; lia || assumption)
+      try (crush; lia || assumption)
 
     | [ _ : _ |- context[Ptrofs.modulus mod m] ] =>
       rewrite Zdivide_mod with (a := Ptrofs.modulus);
@@ -65,7 +65,7 @@ Module PtrofsExtra.
            | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
              rewrite <- Zmod_div_mod; try lia; try assumption
            | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed
-           end; try (simplify; lia); ptrofs_mod_tac m.
+           end; try crush; ptrofs_mod_tac m.
   Qed.
 
   Lemma of_int_mod :
@@ -96,7 +96,7 @@ Module PtrofsExtra.
            | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
              rewrite <- Zmod_div_mod; try lia; try assumption
            | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed
-           end; try (simplify; lia); ptrofs_mod_tac m.
+           end; try(crush; lia); ptrofs_mod_tac m.
   Qed.
 
   Lemma add_mod :
@@ -115,7 +115,7 @@ Module PtrofsExtra.
            | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
              rewrite <- Zmod_div_mod; try lia; try assumption
            | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed
-           end; try (simplify; lia); ptrofs_mod_tac m.
+           end; try (crush; lia); ptrofs_mod_tac m.
   Qed.
 
   Lemma mul_divu :
@@ -156,7 +156,7 @@ Module PtrofsExtra.
     eapply Z.le_trans.
     exact H0.
     rewrite Z.mul_comm.
-    apply Z.le_mul_diag_r; simplify; lia.
+    apply Z.le_mul_diag_r; crush.
   Qed.
 
   Lemma mul_unsigned :
@@ -184,6 +184,23 @@ Module PtrofsExtra.
   Qed.
 End PtrofsExtra.
 
+Ltac ptrofs :=
+  repeat match goal with
+         | [ |- context[Ptrofs.add (Ptrofs.zero) _] ] => setoid_rewrite Ptrofs.add_zero_l
+         | [ H : context[Ptrofs.add (Ptrofs.zero) _] |- _ ] => setoid_rewrite Ptrofs.add_zero_l in H
+
+         | [ |- context[Ptrofs.repr 0] ] => replace (Ptrofs.repr 0) with Ptrofs.zero by reflexivity
+         | [ H : context[Ptrofs.repr 0] |- _ ] =>
+           replace (Ptrofs.repr 0) with Ptrofs.zero in H by reflexivity
+
+         | [ H: context[Ptrofs.unsigned (Ptrofs.repr (Ptrofs.unsigned _))] |- _ ] =>
+           setoid_rewrite Ptrofs.unsigned_repr in H; [>| apply Ptrofs.unsigned_range_2]
+         | [ |- context[Ptrofs.unsigned (Ptrofs.repr (Ptrofs.unsigned _))] ] =>
+           rewrite Ptrofs.unsigned_repr; [>| apply Ptrofs.unsigned_range_2]
+
+         | [ |- context[0 <= Ptrofs.unsigned _] ] => apply Ptrofs.unsigned_range_2
+         end.
+
 Module IntExtra.
 
   Ltac int_mod_match m :=
@@ -202,7 +219,7 @@ Module IntExtra.
       rewrite Zmod_mod
     | [ _ : _ |- context[(_ mod Int.modulus) mod m ] ] =>
       rewrite <- Zmod_div_mod;
-      try (simplify; lia || assumption)
+      try (crush; lia || assumption)
 
     | [ _ : _ |- context[Int.modulus mod m] ] =>
       rewrite Zdivide_mod with (a := Int.modulus);
@@ -242,7 +259,7 @@ Module IntExtra.
            | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
              rewrite <- Zmod_div_mod; try lia; try assumption
            | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed
-           end; try (simplify; lia); int_mod_tac m.
+           end; try (crush; lia); int_mod_tac m.
   Qed.
 
   Lemma add_mod :
@@ -261,6 +278,6 @@ Module IntExtra.
            | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
              rewrite <- Zmod_div_mod; try lia; try assumption
            | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed
-           end; try (simplify; lia); int_mod_tac m.
+           end; try (crush; lia); int_mod_tac m.
   Qed.
 End IntExtra.
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 079cc1e..6e470d5 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -183,11 +183,11 @@ Lemma list_combine_none :
     length l = n ->
     list_combine Verilog.merge_cell (list_repeat None n) l = l.
 Proof.
-  induction n; intros; simplify.
+  induction n; intros; crush.
   - symmetry. apply length_zero_iff_nil. auto.
-  - destruct l; simplify.
+  - destruct l; crush.
     rewrite list_repeat_cons.
-    simplify. f_equal.
+    crush. f_equal.
     eauto.
 Qed.
 
@@ -198,7 +198,7 @@ Lemma combine_none :
 Proof.
   intros.
   unfold combine.
-  simplify.
+  crush.
 
   rewrite <- (arr_wf a) in H.
   apply list_combine_none.
@@ -211,12 +211,12 @@ Lemma list_combine_lookup_first :
     nth_error l1 n = Some None ->
     nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n.
 Proof.
-  induction l1; intros; simplify.
+  induction l1; intros; crush.
 
   rewrite nth_error_nil in H0.
   discriminate.
 
-  destruct l2 eqn:EQl2. simplify.
+  destruct l2 eqn:EQl2. crush.
   simpl in H. invert H.
   destruct n; simpl in *.
   invert H0. simpl. reflexivity.
@@ -243,9 +243,9 @@ Lemma list_combine_lookup_second :
     nth_error l1 n = Some (Some x) ->
     nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x).
 Proof.
-  induction l1; intros; simplify; auto.
+  induction l1; intros; crush; auto.
 
-  destruct l2 eqn:EQl2. simplify.
+  destruct l2 eqn:EQl2. crush.
   simpl in H. invert H.
   destruct n; simpl in *.
   invert H0. simpl. reflexivity.
@@ -432,43 +432,51 @@ Section CORRECTNESS.
       exists asr' asa',
         HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa').
 
-  Ltac big_tac :=
-    repeat (simplify;
-            match goal with
-            | [ |- context[Verilog.merge_regs _ _] ] =>
-              unfold Verilog.merge_regs; simplify; unfold_merge
-            | [ |- context[_ # ?d <- _ ! ?d] ] => apply AssocMap.gss
-            | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso; try apply st_greater_than_res
-            | [ |- context[valueToPos (posToValue 32 _)] ] => rewrite assumption_32bit
-            | [ |- context[match_states _ _] ] => econstructor; eauto
-            | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr; simplify
-            | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty; simplify
+  Opaque combine.
 
-            | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] =>
-              unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal
-
-            | [ |- match_assocmaps _ _ _ # _ <- (posToValue 32 _) ] =>
-              apply regs_lessdef_add_greater; [> apply greater_than_max_func | assumption]
-
-            | [  |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1; simplify
-
-            | [ |- match_arrs _ _ _ _ _ ] => econstructor; simplify
-            | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack; simplify
-            | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs; simplify
-            | [ |- context[(AssocMap.combine _ _ _) ! _] ] =>
-              try (rewrite AssocMap.gcombine; [> | reflexivity])
-
-            | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros
-            | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] =>
-              rewrite Registers.Regmap.gss
-            | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] =>
-              destruct (Pos.eq_dec s d) as [EQ|EQ];
-              [> rewrite EQ | rewrite Registers.Regmap.gso; auto]
-
-            | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set
+  Ltac tac0 :=
+    match goal with
+    | [ |- context[valueToPos (posToValue 32 _)] ] => rewrite assumption_32bit
+
+    | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs
+    | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr
+    | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge
+    | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros
+    | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set
+
+    | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack
+
+    | [ |- context[_ # ?d <- _ ! ?d] ] => rewrite AssocMap.gss
+    | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso
+    | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty
+
+    | [ |- context[array_get_error _ (combine Verilog.merge_cell (arr_repeat None _) _)] ] =>
+      rewrite combine_lookup_first
+
+    | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1
+    | [ |- context[match_states _ _] ] => econstructor; auto
+    | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto
+    | [ |- match_assocmaps _ _ _ # _ <- (posToValue 32 _) ] =>
+      apply regs_lessdef_add_greater; [> apply greater_than_max_func | assumption]
+
+    | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] =>
+      unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal
+    | [ |- context[(AssocMap.combine _ _ _) ! _] ] =>
+      try (rewrite AssocMap.gcombine; [> | reflexivity])
+
+    | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] =>
+      rewrite Registers.Regmap.gss
+    | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] =>
+      destruct (Pos.eq_dec s d) as [EQ|EQ];
+      [> rewrite EQ | rewrite Registers.Regmap.gso; auto]
+
+    | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H
+    | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |]
+    | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H
+    end.
 
-            | [ H : _ ! _ = Some _ |- _] => try (setoid_rewrite H; simplify)
-            end); simplify.
+  Ltac small_tac := repeat (crush; try array; try ptrofs); crush; auto.
+  Ltac big_tac := repeat (crush; try array; try ptrofs; try tac0); crush; auto.
 
   Lemma transl_inop_correct:
     forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
@@ -490,13 +498,12 @@ Section CORRECTNESS.
     apply assumption_32bit.
     (* processing of state *)
     econstructor.
-    simplify.
+    crush.
     econstructor.
     econstructor.
     econstructor.
 
     all: invert MARR; big_tac.
-
     Unshelve.
     constructor.
   Qed.
@@ -612,7 +619,7 @@ Section CORRECTNESS.
   Ltac inv_arr_access :=
     match goal with
     | [ _ : translate_arr_access ?chunk ?addr ?args _ _ = OK ?c _ _ |- _] =>
-      destruct c, chunk, addr, args; simplify; tac; simplify
+      destruct c, chunk, addr, args; crush; tac; crush
     end.
 
   Lemma transl_iload_correct:
@@ -633,24 +640,24 @@ Section CORRECTNESS.
     inv_state. inv_arr_access.
 
     + (** Preamble *)
-      invert MARR. simplify.
+      invert MARR. crush.
 
       unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; simplify.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
 
       unfold reg_stack_based_pointers in RSBP.
       pose proof (RSBP r0) as RSBPr0.
 
-      destruct (Registers.Regmap.get r0 rs) eqn:EQr0; simplify.
+      destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush.
 
-      rewrite ARCHI in H1. simplify.
+      rewrite ARCHI in H1. crush.
       subst.
 
       pose proof MASSOC as MASSOC'.
       invert MASSOC'.
       pose proof (H0 r0).
       assert (HPler0 : Ple r0 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; simplify; eauto).
+        by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
       apply H6 in HPler0.
       invert HPler0; try congruence.
       rewrite EQr0 in H8.
@@ -658,7 +665,7 @@ Section CORRECTNESS.
       clear H0. clear H6.
 
       unfold check_address_parameter_signed in *;
-      unfold check_address_parameter_unsigned in *; simplify.
+      unfold check_address_parameter_unsigned in *; crush.
 
       remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
                                     (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
@@ -666,24 +673,20 @@ Section CORRECTNESS.
       (** Modular preservation proof *)
       assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
       { rewrite HeqOFFSET.
-        apply PtrofsExtra.add_mod; simplify; try lia.
+        apply PtrofsExtra.add_mod; crush; try lia.
         exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
         rewrite Integers.Ptrofs.signed_repr; try assumption.
         admit. (* FIXME: Register bounds. *)
         apply PtrofsExtra.of_int_mod.
-        rewrite Integers.Int.signed_repr; simplify; try split; try assumption. }
+        rewrite Integers.Int.signed_repr; crush. }
 
       (** Read bounds proof *)
       assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
         unfold stack_bounds in BOUNDS.
         exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
         split; try lia; apply Integers.Ptrofs.unsigned_range_2.
-        simplify.
-        replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
-        rewrite Integers.Ptrofs.add_zero_l.
-        rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence.
-        apply Integers.Ptrofs.unsigned_range_2. }
+        small_tac. }
 
       (** Normalisation proof *)
       assert (Integers.Ptrofs.repr
@@ -692,7 +695,7 @@ Section CORRECTNESS.
         as NORMALISE.
       { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
         rewrite <- PtrofsExtra.mul_unsigned.
-        apply PtrofsExtra.mul_divu; simplify; auto; lia. }
+        apply PtrofsExtra.mul_divu; crush; auto. }
 
       (** Normalised bounds proof *)
       assert (0 <=
@@ -704,11 +707,11 @@ Section CORRECTNESS.
         assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
         unfold Integers.Ptrofs.divu at 2 in H0.
         rewrite H0. clear H0.
-        rewrite Integers.Ptrofs.unsigned_repr; simplify.
+        rewrite Integers.Ptrofs.unsigned_repr; crush.
         apply Zmult_lt_reg_r with (p := 4); try lia.
         repeat rewrite ZLib.div_mul_undo; try lia.
-        apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2.
-        apply Z.div_le_upper_bound; lia. }
+        apply Z.div_pos; small_tac.
+        apply Z.div_le_upper_bound; small_tac. }
 
       inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
       clear NORMALISE_BOUND.
@@ -718,33 +721,21 @@ Section CORRECTNESS.
       eapply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
       apply assumption_32bit.
-      econstructor. econstructor. econstructor. simplify.
-      econstructor. econstructor. econstructor. simplify.
+      econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor. econstructor. crush.
       econstructor. econstructor.
       econstructor. econstructor. econstructor. econstructor.
       econstructor. econstructor. econstructor. econstructor.
 
       all: big_tac.
 
+      1: { apply st_greater_than_res. }
+      2: { apply st_greater_than_res. }
+
       (** Match assocmaps *)
       apply regs_lessdef_add_match; big_tac.
 
       (** Equality proof *)
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      rewrite ZERO in H7. clear ZERO.
-      setoid_rewrite Integers.Ptrofs.add_zero_l in H7.
-
-      specialize (H7 (Integers.Ptrofs.unsigned
-                        (Integers.Ptrofs.divu
-                           OFFSET
-                           (Integers.Ptrofs.repr 4)))).
-
-      exploit H7.
-      rewrite Z2Nat.id; eauto.
-      apply Z.div_pos; lia.
-
-      intros I.
-
       match goal with
       | [ |- context [valueToNat ?x] ] =>
         assert (Z.to_nat
@@ -756,40 +747,35 @@ Section CORRECTNESS.
                 valueToNat x)
           as EXPR_OK by admit
       end.
-
       rewrite <- EXPR_OK.
-      rewrite NORMALISE in I.
-      rewrite H1 in I.
-      invert I. assumption.
+
+      specialize (H7 (Integers.Ptrofs.unsigned
+                        (Integers.Ptrofs.divu
+                           OFFSET
+                           (Integers.Ptrofs.repr 4)))).
+      exploit H7; big_tac.
 
       (** RSBP preservation *)
       unfold arr_stack_based_pointers in ASBP.
       specialize (ASBP (Integers.Ptrofs.unsigned
                           (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
-      exploit ASBP; auto; intros I.
-
-      rewrite NORMALISE in I.
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      rewrite ZERO in I. clear ZERO.
-      simplify.
-      rewrite Integers.Ptrofs.add_zero_l in I.
-      rewrite H1 in I.
-      assumption.
+      exploit ASBP; big_tac.
+      rewrite NORMALISE in H0. rewrite H1 in H0. assumption.
 
     + (** Preamble *)
-      invert MARR. simplify.
+      invert MARR. crush.
 
       unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; simplify.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
 
       unfold reg_stack_based_pointers in RSBP.
       pose proof (RSBP r0) as RSBPr0.
       pose proof (RSBP r1) as RSBPr1.
 
       destruct (Registers.Regmap.get r0 rs) eqn:EQr0;
-      destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify.
+      destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush.
 
-      rewrite ARCHI in H1. simplify.
+      rewrite ARCHI in H1. crush.
       subst.
       clear RSBPr1.
 
@@ -798,7 +784,7 @@ Section CORRECTNESS.
       pose proof (H0 r0).
       pose proof (H0 r1).
       assert (HPler0 : Ple r0 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; simplify; eauto).
+        by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
       assert (HPler1 : Ple r1 (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
       apply H6 in HPler0.
@@ -810,7 +796,7 @@ Section CORRECTNESS.
       clear H0. clear H6. clear H8.
 
       unfold check_address_parameter_signed in *;
-      unfold check_address_parameter_unsigned in *; simplify.
+      unfold check_address_parameter_unsigned in *; crush.
 
       remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
                                     (Integers.Ptrofs.of_int
@@ -820,30 +806,26 @@ Section CORRECTNESS.
       (** Modular preservation proof *)
       assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
       { rewrite HeqOFFSET.
-        apply PtrofsExtra.add_mod; simplify; try lia.
+        apply PtrofsExtra.add_mod; crush; try lia.
         exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
         rewrite Integers.Ptrofs.signed_repr; try assumption.
         admit. (* FIXME: Register bounds. *)
         apply PtrofsExtra.of_int_mod.
-        apply IntExtra.add_mod; simplify; try lia.
+        apply IntExtra.add_mod; crush; try lia.
         exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
-        apply IntExtra.mul_mod; simplify; try lia.
+        apply IntExtra.mul_mod; crush; try lia.
         exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
         admit. (* FIXME: Register bounds. *)
-        rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
-        rewrite Integers.Int.signed_repr; simplify; try split; try assumption. }
+        rewrite Integers.Int.signed_repr; crush.
+        rewrite Integers.Int.signed_repr; crush. }
 
       (** Read bounds proof *)
       assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
         unfold stack_bounds in BOUNDS.
         exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
         split; try lia; apply Integers.Ptrofs.unsigned_range_2.
-        simplify.
-        replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
-        rewrite Integers.Ptrofs.add_zero_l.
-        rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence.
-        apply Integers.Ptrofs.unsigned_range_2. }
+        small_tac. }
 
       (** Normalisation proof *)
       assert (Integers.Ptrofs.repr
@@ -852,7 +834,7 @@ Section CORRECTNESS.
         as NORMALISE.
       { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
         rewrite <- PtrofsExtra.mul_unsigned.
-        apply PtrofsExtra.mul_divu; simplify; auto; lia. }
+        apply PtrofsExtra.mul_divu; crush. }
 
       (** Normalised bounds proof *)
       assert (0 <=
@@ -864,10 +846,10 @@ Section CORRECTNESS.
         assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
         unfold Integers.Ptrofs.divu at 2 in H0.
         rewrite H0. clear H0.
-        rewrite Integers.Ptrofs.unsigned_repr; simplify.
+        rewrite Integers.Ptrofs.unsigned_repr; crush.
         apply Zmult_lt_reg_r with (p := 4); try lia.
         repeat rewrite ZLib.div_mul_undo; try lia.
-        apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2.
+        apply Z.div_pos; small_tac.
         apply Z.div_le_upper_bound; lia. }
 
       inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
@@ -878,8 +860,8 @@ Section CORRECTNESS.
       eapply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
       apply assumption_32bit.
-      econstructor. econstructor. econstructor. simplify.
-      econstructor. econstructor. econstructor. simplify.
+      econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor. econstructor. crush.
       econstructor. econstructor. econstructor.
       econstructor. econstructor. econstructor. econstructor.
       econstructor.
@@ -890,24 +872,13 @@ Section CORRECTNESS.
 
       all: big_tac.
 
+      1: { apply st_greater_than_res. }
+      2: { apply st_greater_than_res. }
+
       (** Match assocmaps *)
       apply regs_lessdef_add_match; big_tac.
 
       (** Equality proof *)
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      rewrite ZERO in H7. clear ZERO.
-      setoid_rewrite Integers.Ptrofs.add_zero_l in H7.
-
-      specialize (H7 (Integers.Ptrofs.unsigned
-                        (Integers.Ptrofs.divu
-                           OFFSET
-                           (Integers.Ptrofs.repr 4)))).
-
-      exploit H7.
-      rewrite Z2Nat.id; eauto.
-      apply Z.div_pos; lia.
-
-      intros I.
       match goal with
       | [ |- context [valueToNat ?x] ] =>
         assert (Z.to_nat
@@ -920,32 +891,28 @@ Section CORRECTNESS.
           as EXPR_OK by admit
       end.
       rewrite <- EXPR_OK.
-      rewrite NORMALISE in I.
-      rewrite H1 in I.
-      invert I. assumption.
+
+      specialize (H7 (Integers.Ptrofs.unsigned
+                        (Integers.Ptrofs.divu
+                           OFFSET
+                           (Integers.Ptrofs.repr 4)))).
+      exploit H7; big_tac.
 
       (** RSBP preservation *)
       unfold arr_stack_based_pointers in ASBP.
       specialize (ASBP (Integers.Ptrofs.unsigned
                           (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
-      exploit ASBP; auto; intros I.
-
-      rewrite NORMALISE in I.
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      rewrite ZERO in I. clear ZERO.
-      simplify.
-      rewrite Integers.Ptrofs.add_zero_l in I.
-      rewrite H1 in I.
-      assumption.
+      exploit ASBP; big_tac.
+      rewrite NORMALISE in H0. rewrite H1 in H0. assumption.
 
-    + invert MARR. simplify.
+    + invert MARR. crush.
 
       unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; simplify.
-      rewrite ARCHI in H0. simplify.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+      rewrite ARCHI in H0. crush.
 
       unfold check_address_parameter_unsigned in *;
-      unfold check_address_parameter_signed in *; simplify.
+      unfold check_address_parameter_signed in *; crush.
 
       assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
       rewrite ZERO in H1. clear ZERO.
@@ -958,14 +925,9 @@ Section CORRECTNESS.
 
       (** Read bounds proof *)
       assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
         unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
-        simplify.
-        replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
-        rewrite Integers.Ptrofs.add_zero_l.
-        rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence.
-        apply Integers.Ptrofs.unsigned_range_2. }
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); big_tac. }
 
       (** Normalisation proof *)
       assert (Integers.Ptrofs.repr
@@ -974,7 +936,7 @@ Section CORRECTNESS.
         as NORMALISE.
       { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
         rewrite <- PtrofsExtra.mul_unsigned.
-        apply PtrofsExtra.mul_divu; simplify; auto; try lia. }
+        apply PtrofsExtra.mul_divu; crush. }
 
       (** Normalised bounds proof *)
       assert (0 <=
@@ -986,10 +948,10 @@ Section CORRECTNESS.
         assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
         unfold Integers.Ptrofs.divu at 2 in H0.
         rewrite H0. clear H0.
-        rewrite Integers.Ptrofs.unsigned_repr; simplify.
+        rewrite Integers.Ptrofs.unsigned_repr; crush.
         apply Zmult_lt_reg_r with (p := 4); try lia.
         repeat rewrite ZLib.div_mul_undo; try lia.
-        apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2.
+        apply Z.div_pos; small_tac.
         apply Z.div_le_upper_bound; lia. }
 
       inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
@@ -1000,55 +962,43 @@ Section CORRECTNESS.
       eapply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
       apply assumption_32bit.
-      econstructor. econstructor. econstructor. simplify.
-      econstructor. econstructor. econstructor. econstructor. simplify.
+      econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor. econstructor. econstructor. crush.
 
       all: big_tac.
 
+      1: { apply st_greater_than_res. }
+      2: { apply st_greater_than_res. }
+
       (** Match assocmaps *)
       apply regs_lessdef_add_match; big_tac.
 
       (** Equality proof *)
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      rewrite ZERO in H7. clear ZERO.
-      setoid_rewrite Integers.Ptrofs.add_zero_l in H7.
+      match goal with
+      | [ |- context [valueToNat ?x] ] =>
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat x)
+          as EXPR_OK by admit
+      end.
+      rewrite <- EXPR_OK.
 
       specialize (H7 (Integers.Ptrofs.unsigned
                         (Integers.Ptrofs.divu
                            OFFSET
                            (Integers.Ptrofs.repr 4)))).
-
-      exploit H7.
-      rewrite Z2Nat.id; eauto.
-      apply Z.div_pos; lia.
-
-      intros I.
-      assert (Z.to_nat
-                (Integers.Ptrofs.unsigned
-                   (Integers.Ptrofs.divu
-                      OFFSET
-                      (Integers.Ptrofs.repr 4)))
-              =
-              valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4)))
-        as EXPR_OK by admit.
-      rewrite <- EXPR_OK.
-      rewrite NORMALISE in I.
-      rewrite H1 in I.
-      invert I. assumption.
+      exploit H7; big_tac.
 
       (** RSBP preservation *)
       unfold arr_stack_based_pointers in ASBP.
       specialize (ASBP (Integers.Ptrofs.unsigned
                           (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
-      exploit ASBP; auto; intros I.
-
-      rewrite NORMALISE in I.
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      rewrite ZERO in I. clear ZERO.
-      simplify.
-      rewrite Integers.Ptrofs.add_zero_l in I.
-      rewrite H1 in I.
-      assumption.
+      exploit ASBP; big_tac.
+      rewrite NORMALISE in H0. rewrite H1 in H0. assumption.
   Admitted.
   Hint Resolve transl_iload_correct : htlproof.
 
@@ -1069,24 +1019,24 @@ Section CORRECTNESS.
     inv_state. inv_arr_access.
 
     + (** Preamble *)
-      invert MARR. simplify.
+      invert MARR. crush.
 
       unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; simplify.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
 
       unfold reg_stack_based_pointers in RSBP.
       pose proof (RSBP r0) as RSBPr0.
 
-      destruct (Registers.Regmap.get r0 rs) eqn:EQr0; simplify.
+      destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush.
 
-      rewrite ARCHI in H1. simplify.
+      rewrite ARCHI in H1. crush.
       subst.
 
       pose proof MASSOC as MASSOC'.
       invert MASSOC'.
       pose proof (H0 r0).
       assert (HPler0 : Ple r0 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; simplify; eauto).
+        by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
       apply H6 in HPler0.
       invert HPler0; try congruence.
       rewrite EQr0 in H8.
@@ -1094,7 +1044,7 @@ Section CORRECTNESS.
       clear H0. clear H6.
 
       unfold check_address_parameter_unsigned in *;
-      unfold check_address_parameter_signed in *; simplify.
+      unfold check_address_parameter_signed in *; crush.
 
       remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
                                     (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
@@ -1102,24 +1052,18 @@ Section CORRECTNESS.
       (** Modular preservation proof *)
       assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
       { rewrite HeqOFFSET.
-        apply PtrofsExtra.add_mod; simplify; try lia.
+        apply PtrofsExtra.add_mod; crush; try lia.
         exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
         rewrite Integers.Ptrofs.signed_repr; try assumption.
         admit. (* FIXME: Register bounds. *)
         apply PtrofsExtra.of_int_mod.
-        rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
-      }
+        rewrite Integers.Int.signed_repr; crush. }
 
       (** Write bounds proof *)
       assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
         unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
-        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
-        simplify.
-        replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
-        rewrite Integers.Ptrofs.add_zero_l.
-        rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence.
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac.
         apply Integers.Ptrofs.unsigned_range_2. }
 
       (** Start of proof proper *)
@@ -1128,7 +1072,7 @@ Section CORRECTNESS.
       eapply HTL.step_module; eauto.
       apply assumption_32bit.
       econstructor. econstructor. econstructor.
-      eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
+      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
       econstructor.
       eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]).
       eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]).
@@ -1137,11 +1081,11 @@ Section CORRECTNESS.
       econstructor. econstructor. econstructor. econstructor.
       econstructor. econstructor. econstructor. econstructor.
 
-      all: simplify.
+      all: crush.
 
       (** State Lookup *)
       unfold Verilog.merge_regs.
-      simplify.
+      crush.
       unfold_merge.
       apply AssocMap.gss.
 
@@ -1150,33 +1094,36 @@ Section CORRECTNESS.
       econstructor; eauto.
 
       (** Match assocmaps *)
-      unfold Verilog.merge_regs. simplify. unfold_merge.
+      unfold Verilog.merge_regs. crush. unfold_merge.
       apply regs_lessdef_add_greater. apply greater_than_max_func.
       assumption.
 
       (** States well formed *)
-      unfold state_st_wf. inversion 1. simplify.
+      unfold state_st_wf. inversion 1. crush.
       unfold Verilog.merge_regs.
       unfold_merge.
       apply AssocMap.gss.
 
       (** Equality proof *)
-      assert (Z.to_nat
-                (Integers.Ptrofs.unsigned
-                   (Integers.Ptrofs.divu
-                      OFFSET
-                      (Integers.Ptrofs.repr 4)))
-              =
-              valueToNat (vdiv (vplus asr # r0 (ZToValue 32 z) ?EQ8) (ZToValue 32 4) ?EQ7))
-        as EXPR_OK by admit.
+      match goal with
+      | [ |- context [valueToNat ?x] ] =>
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat x)
+          as EXPR_OK by admit
+      end.
 
       assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
       inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
 
       econstructor.
-      repeat split; simplify.
+      repeat split; crush.
       unfold HTL.empty_stack.
-      simplify.
+      crush.
       unfold Verilog.merge_arrs.
 
       rewrite AssocMap.gcombine.
@@ -1190,15 +1137,17 @@ Section CORRECTNESS.
 
       rewrite combine_length.
       rewrite <- array_set_len.
-      unfold arr_repeat. simplify.
+      unfold arr_repeat. crush.
       apply list_repeat_len.
 
       rewrite <- array_set_len.
-      unfold arr_repeat. simplify.
+      unfold arr_repeat. crush.
       rewrite list_repeat_len.
       rewrite H4. reflexivity.
 
-      intros.
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+                                    (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
+
       destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
 
       erewrite Mem.load_store_same.
@@ -1213,19 +1162,19 @@ Section CORRECTNESS.
       simpl.
       assert (Ple src (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-      apply H0 in H14.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H14; eauto.
+      apply H0 in H13.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H13; eauto.
 
       rewrite <- array_set_len.
-      unfold arr_repeat. simplify.
+      unfold arr_repeat. crush.
       rewrite list_repeat_len. auto.
 
       assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
-      rewrite Z.mul_comm in H14.
-      rewrite Z_div_mult in H14; try lia.
-      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H14 by reflexivity.
-      rewrite <- PtrofsExtra.divu_unsigned in H14; unfold_constants; try lia.
-      rewrite H14. rewrite EXPR_OK.
+      rewrite Z.mul_comm in H13.
+      rewrite Z_div_mult in H13; try lia.
+      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H13 by reflexivity.
+      rewrite <- PtrofsExtra.divu_unsigned in H13; unfold_constants; try lia.
+      rewrite H13. rewrite EXPR_OK.
       rewrite array_get_error_set_bound.
       reflexivity.
       unfold arr_length, arr_repeat. simpl.
@@ -1242,12 +1191,11 @@ Section CORRECTNESS.
            right.
            apply ZExtra.mod_0_bounds; try lia.
            apply ZLib.Z_mod_mult'.
-           invert H13.
            rewrite Z2Nat.id in H19; try lia.
            apply Zmult_lt_compat_r with (p := 4) in H19; try lia.
            rewrite ZLib.div_mul_undo in H19; try lia.
            split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
       }
 
       rewrite <- EXPR_OK.
@@ -1259,26 +1207,26 @@ Section CORRECTNESS.
       eapply H7; eauto.
 
       rewrite <- array_set_len.
-      unfold arr_repeat. simplify.
+      unfold arr_repeat. crush.
       rewrite list_repeat_len. auto.
       rewrite array_gso.
       unfold array_get_error.
       unfold arr_repeat.
-      simplify.
+      crush.
       apply list_repeat_lookup.
       lia.
       unfold_constants.
       intro.
-      apply Z2Nat.inj_iff in H14; try lia.
+      apply Z2Nat.inj_iff in H13; try lia.
       apply Z.div_pos; try lia.
-      apply Integers.Ptrofs.unsigned_range_2.
+      apply Integers.Ptrofs.unsigned_range.
 
       assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
       unfold arr_stack_based_pointers.
       intros.
       destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
 
-      simplify.
+      crush.
       erewrite Mem.load_store_same.
       2: { rewrite ZERO.
            rewrite Integers.Ptrofs.add_zero_l.
@@ -1286,10 +1234,11 @@ Section CORRECTNESS.
            rewrite Integers.Ptrofs.unsigned_repr.
            exact H1.
            apply Integers.Ptrofs.unsigned_range_2. }
-      simplify.
+      crush.
       destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
       destruct (Archi.ptr64); try discriminate.
-      pose proof (RSBP src). rewrite EQ_SRC in H0. assumption.
+      pose proof (RSBP src). rewrite EQ_SRC in H0.
+      assumption.
 
       simpl.
       erewrite Mem.load_store_other with (m1 := m).
@@ -1307,7 +1256,7 @@ Section CORRECTNESS.
            apply Zmult_lt_compat_r with (p := 4) in H14; try lia.
            rewrite ZLib.div_mul_undo in H14; try lia.
            split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
       }
       apply ASBP; assumption.
 
@@ -1319,10 +1268,10 @@ Section CORRECTNESS.
       2: { right. right. simpl.
            rewrite ZERO.
            rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr; simplify; try lia.
-           apply ZExtra.mod_0_bounds; simplify; try lia. }
-      simplify.
-      exploit (BOUNDS ptr); try lia. intros. simplify.
+           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
+           apply ZExtra.mod_0_bounds; crush; try lia. }
+      crush.
+      exploit (BOUNDS ptr); try lia. intros. crush.
       exploit (BOUNDS ptr v); try lia. intros.
       invert H0.
       match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
@@ -1339,19 +1288,19 @@ Section CORRECTNESS.
       apply X in H0. invert H0. congruence.
 
     + (** Preamble *)
-      invert MARR. simplify.
+      invert MARR. crush.
 
       unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; simplify.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
 
       unfold reg_stack_based_pointers in RSBP.
       pose proof (RSBP r0) as RSBPr0.
       pose proof (RSBP r1) as RSBPr1.
 
       destruct (Registers.Regmap.get r0 rs) eqn:EQr0;
-      destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify.
+      destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush.
 
-      rewrite ARCHI in H1. simplify.
+      rewrite ARCHI in H1. crush.
       subst.
       clear RSBPr1.
 
@@ -1360,7 +1309,7 @@ Section CORRECTNESS.
       pose proof (H0 r0).
       pose proof (H0 r1).
       assert (HPler0 : Ple r0 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; simplify; eauto).
+        by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
       assert (HPler1 : Ple r1 (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
       apply H6 in HPler0.
@@ -1372,7 +1321,7 @@ Section CORRECTNESS.
       clear H0. clear H6. clear H8.
 
       unfold check_address_parameter_signed in *;
-      unfold check_address_parameter_unsigned in *; simplify.
+      unfold check_address_parameter_unsigned in *; crush.
 
       remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
                                     (Integers.Ptrofs.of_int
@@ -1382,31 +1331,27 @@ Section CORRECTNESS.
       (** Modular preservation proof *)
       assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
       { rewrite HeqOFFSET.
-        apply PtrofsExtra.add_mod; simplify; try lia.
+        apply PtrofsExtra.add_mod; crush; try lia.
         exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
         rewrite Integers.Ptrofs.signed_repr; try assumption.
         admit. (* FIXME: Register bounds. *)
         apply PtrofsExtra.of_int_mod.
-        apply IntExtra.add_mod; simplify; try lia.
+        apply IntExtra.add_mod; crush; try lia.
         exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
-        apply IntExtra.mul_mod; simplify; try lia.
+        apply IntExtra.mul_mod; crush; try lia.
         exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
         admit. (* FIXME: Register bounds. *)
-        rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
-        rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
+        rewrite Integers.Int.signed_repr; crush; try split; try assumption.
+        rewrite Integers.Int.signed_repr; crush; try split; try assumption.
       }
 
       (** Write bounds proof *)
       assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
         unfold stack_bounds in BOUNDS.
         exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
         split; try lia; apply Integers.Ptrofs.unsigned_range_2.
-        simplify.
-        replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
-        rewrite Integers.Ptrofs.add_zero_l.
-        rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence.
-        apply Integers.Ptrofs.unsigned_range_2. }
+        small_tac. }
 
       (** Start of proof proper *)
       eexists. split.
@@ -1414,7 +1359,7 @@ Section CORRECTNESS.
       eapply HTL.step_module; eauto.
       apply assumption_32bit.
       econstructor. econstructor. econstructor.
-      eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
+      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
       econstructor.
       eapply Verilog.erun_Vbinop with (EQ := ?[EQ9]).
       eapply Verilog.erun_Vbinop with (EQ := ?[EQ10]).
@@ -1426,11 +1371,11 @@ Section CORRECTNESS.
       econstructor. econstructor. econstructor. econstructor.
       econstructor. econstructor. econstructor. econstructor.
 
-      all: simplify.
+      all: crush.
 
       (** State Lookup *)
       unfold Verilog.merge_regs.
-      simplify.
+      crush.
       unfold_merge.
       apply AssocMap.gss.
 
@@ -1439,12 +1384,12 @@ Section CORRECTNESS.
       econstructor; eauto.
 
       (** Match assocmaps *)
-      unfold Verilog.merge_regs. simplify. unfold_merge.
+      unfold Verilog.merge_regs. crush. unfold_merge.
       apply regs_lessdef_add_greater. apply greater_than_max_func.
       assumption.
 
       (** States well formed *)
-      unfold state_st_wf. inversion 1. simplify.
+      unfold state_st_wf. inversion 1. crush.
       unfold Verilog.merge_regs.
       unfold_merge.
       apply AssocMap.gss.
@@ -1465,9 +1410,9 @@ Section CORRECTNESS.
       inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
 
       econstructor.
-      repeat split; simplify.
+      repeat split; crush.
       unfold HTL.empty_stack.
-      simplify.
+      crush.
       unfold Verilog.merge_arrs.
 
       rewrite AssocMap.gcombine.
@@ -1481,15 +1426,18 @@ Section CORRECTNESS.
 
       rewrite combine_length.
       rewrite <- array_set_len.
-      unfold arr_repeat. simplify.
+      unfold arr_repeat. crush.
       apply list_repeat_len.
 
       rewrite <- array_set_len.
-      unfold arr_repeat. simplify.
+      unfold arr_repeat. crush.
       rewrite list_repeat_len.
       rewrite H4. reflexivity.
 
-      intros.
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+                                    (Integers.Ptrofs.of_int
+                                       (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
+                                                         (Integers.Int.repr z0)))) as OFFSET.
       destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
 
       erewrite Mem.load_store_same.
@@ -1504,19 +1452,19 @@ Section CORRECTNESS.
       simpl.
       assert (Ple src (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-      apply H0 in H21.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H21; eauto.
+      apply H0 in H20.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H20; eauto.
 
       rewrite <- array_set_len.
-      unfold arr_repeat. simplify.
+      unfold arr_repeat. crush.
       rewrite list_repeat_len. auto.
 
       assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
-      rewrite Z.mul_comm in H21.
-      rewrite Z_div_mult in H21; try lia.
-      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H21 by reflexivity.
-      rewrite <- PtrofsExtra.divu_unsigned in H21; unfold_constants; try lia.
-      rewrite H21. rewrite EXPR_OK.
+      rewrite Z.mul_comm in H20.
+      rewrite Z_div_mult in H20; try lia.
+      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H20 by reflexivity.
+      rewrite <- PtrofsExtra.divu_unsigned in H20; unfold_constants; try lia.
+      rewrite H20. rewrite EXPR_OK.
       rewrite array_get_error_set_bound.
       reflexivity.
       unfold arr_length, arr_repeat. simpl.
@@ -1533,12 +1481,11 @@ Section CORRECTNESS.
            right.
            apply ZExtra.mod_0_bounds; try lia.
            apply ZLib.Z_mod_mult'.
-           invert H20.
            rewrite Z2Nat.id in H22; try lia.
            apply Zmult_lt_compat_r with (p := 4) in H22; try lia.
            rewrite ZLib.div_mul_undo in H22; try lia.
            split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
       }
 
       rewrite <- EXPR_OK.
@@ -1550,17 +1497,17 @@ Section CORRECTNESS.
       eapply H7; eauto.
 
       rewrite <- array_set_len.
-      unfold arr_repeat. simplify.
+      unfold arr_repeat. crush.
       rewrite list_repeat_len. auto.
       rewrite array_gso.
       unfold array_get_error.
       unfold arr_repeat.
-      simplify.
+      crush.
       apply list_repeat_lookup.
       lia.
       unfold_constants.
       intro.
-      apply Z2Nat.inj_iff in H21; try lia.
+      apply Z2Nat.inj_iff in H20; try lia.
       apply Z.div_pos; try lia.
       apply Integers.Ptrofs.unsigned_range.
 
@@ -1569,7 +1516,7 @@ Section CORRECTNESS.
       intros.
       destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
 
-      simplify.
+      crush.
       erewrite Mem.load_store_same.
       2: { rewrite ZERO.
            rewrite Integers.Ptrofs.add_zero_l.
@@ -1577,7 +1524,7 @@ Section CORRECTNESS.
            rewrite Integers.Ptrofs.unsigned_repr.
            exact H1.
            apply Integers.Ptrofs.unsigned_range_2. }
-      simplify.
+      crush.
       destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
       destruct (Archi.ptr64); try discriminate.
       pose proof (RSBP src). rewrite EQ_SRC in H0.
@@ -1599,7 +1546,7 @@ Section CORRECTNESS.
            apply Zmult_lt_compat_r with (p := 4) in H21; try lia.
            rewrite ZLib.div_mul_undo in H21; try lia.
            split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
       }
       apply ASBP; assumption.
 
@@ -1611,10 +1558,10 @@ Section CORRECTNESS.
       2: { right. right. simpl.
            rewrite ZERO.
            rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr; simplify; try lia.
-           apply ZExtra.mod_0_bounds; simplify; try lia. }
-      simplify.
-      exploit (BOUNDS ptr); try lia. intros. simplify.
+           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
+           apply ZExtra.mod_0_bounds; crush; try lia. }
+      crush.
+      exploit (BOUNDS ptr); try lia. intros. crush.
       exploit (BOUNDS ptr v); try lia. intros.
       invert H0.
       match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
@@ -1630,14 +1577,14 @@ Section CORRECTNESS.
                                                                  (Integers.Ptrofs.repr ptr))) v).
       apply X in H0. invert H0. congruence.
 
-    + invert MARR. simplify.
+    + invert MARR. crush.
 
       unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; simplify.
-      rewrite ARCHI in H0. simplify.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+      rewrite ARCHI in H0. crush.
 
       unfold check_address_parameter_unsigned in *;
-      unfold check_address_parameter_signed in *; simplify.
+      unfold check_address_parameter_signed in *; crush.
 
       assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
       rewrite ZERO in H1. clear ZERO.
@@ -1650,14 +1597,12 @@ Section CORRECTNESS.
 
       (** Write bounds proof *)
       assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
         unfold stack_bounds in BOUNDS.
         exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
-        simplify.
+        crush.
         replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
-        rewrite Integers.Ptrofs.add_zero_l.
-        rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence.
-        apply Integers.Ptrofs.unsigned_range_2. }
+        small_tac. }
 
       (** Start of proof proper *)
       eexists. split.
@@ -1665,14 +1610,14 @@ Section CORRECTNESS.
       eapply HTL.step_module; eauto.
       apply assumption_32bit.
       econstructor. econstructor. econstructor.
-      eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
+      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
       econstructor. econstructor. econstructor. econstructor.
 
-      all: simplify.
+      all: crush.
 
       (** State Lookup *)
       unfold Verilog.merge_regs.
-      simplify.
+      crush.
       unfold_merge.
       apply AssocMap.gss.
 
@@ -1681,12 +1626,12 @@ Section CORRECTNESS.
       econstructor; eauto.
 
       (** Match assocmaps *)
-      unfold Verilog.merge_regs. simplify. unfold_merge.
+      unfold Verilog.merge_regs. crush. unfold_merge.
       apply regs_lessdef_add_greater. apply greater_than_max_func.
       assumption.
 
       (** States well formed *)
-      unfold state_st_wf. inversion 1. simplify.
+      unfold state_st_wf. inversion 1. crush.
       unfold Verilog.merge_regs.
       unfold_merge.
       apply AssocMap.gss.
@@ -1705,9 +1650,9 @@ Section CORRECTNESS.
       inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
 
       econstructor.
-      repeat split; simplify.
+      repeat split; crush.
       unfold HTL.empty_stack.
-      simplify.
+      crush.
       unfold Verilog.merge_arrs.
 
       rewrite AssocMap.gcombine.
@@ -1721,15 +1666,15 @@ Section CORRECTNESS.
 
       rewrite combine_length.
       rewrite <- array_set_len.
-      unfold arr_repeat. simplify.
+      unfold arr_repeat. crush.
       apply list_repeat_len.
 
       rewrite <- array_set_len.
-      unfold arr_repeat. simplify.
+      unfold arr_repeat. crush.
       rewrite list_repeat_len.
       rewrite H4. reflexivity.
 
-      intros.
+      remember i0 as OFFSET.
       destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
 
       erewrite Mem.load_store_same.
@@ -1744,19 +1689,19 @@ Section CORRECTNESS.
       simpl.
       assert (Ple src (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-      apply H0 in H10.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H10; eauto.
+      apply H0 in H8.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H8; eauto.
 
       rewrite <- array_set_len.
-      unfold arr_repeat. simplify.
+      unfold arr_repeat. crush.
       rewrite list_repeat_len. auto.
 
       assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
-      rewrite Z.mul_comm in H10.
-      rewrite Z_div_mult in H10; try lia.
-      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H10 by reflexivity.
-      rewrite <- PtrofsExtra.divu_unsigned in H10; unfold_constants; try lia.
-      rewrite H10. rewrite EXPR_OK.
+      rewrite Z.mul_comm in H8.
+      rewrite Z_div_mult in H8; try lia.
+      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H8 by reflexivity.
+      rewrite <- PtrofsExtra.divu_unsigned in H8; unfold_constants; try lia.
+      rewrite H8. rewrite EXPR_OK.
       rewrite array_get_error_set_bound.
       reflexivity.
       unfold arr_length, arr_repeat. simpl.
@@ -1773,12 +1718,11 @@ Section CORRECTNESS.
            right.
            apply ZExtra.mod_0_bounds; try lia.
            apply ZLib.Z_mod_mult'.
-           invert H8.
            rewrite Z2Nat.id in H12; try lia.
            apply Zmult_lt_compat_r with (p := 4) in H12; try lia.
            rewrite ZLib.div_mul_undo in H12; try lia.
            split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
       }
 
       rewrite <- EXPR_OK.
@@ -1790,17 +1734,17 @@ Section CORRECTNESS.
       eapply H7; eauto.
 
       rewrite <- array_set_len.
-      unfold arr_repeat. simplify.
+      unfold arr_repeat. crush.
       rewrite list_repeat_len. auto.
       rewrite array_gso.
       unfold array_get_error.
       unfold arr_repeat.
-      simplify.
+      crush.
       apply list_repeat_lookup.
       lia.
       unfold_constants.
       intro.
-      apply Z2Nat.inj_iff in H10; try lia.
+      apply Z2Nat.inj_iff in H8; try lia.
       apply Z.div_pos; try lia.
       apply Integers.Ptrofs.unsigned_range.
 
@@ -1809,7 +1753,7 @@ Section CORRECTNESS.
       intros.
       destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
 
-      simplify.
+      crush.
       erewrite Mem.load_store_same.
       2: { rewrite ZERO.
            rewrite Integers.Ptrofs.add_zero_l.
@@ -1817,7 +1761,7 @@ Section CORRECTNESS.
            rewrite Integers.Ptrofs.unsigned_repr.
            exact H1.
            apply Integers.Ptrofs.unsigned_range_2. }
-      simplify.
+      crush.
       destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
       destruct (Archi.ptr64); try discriminate.
       pose proof (RSBP src). rewrite EQ_SRC in H0.
@@ -1839,7 +1783,7 @@ Section CORRECTNESS.
            apply Zmult_lt_compat_r with (p := 4) in H10; try lia.
            rewrite ZLib.div_mul_undo in H10; try lia.
            split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
       }
       apply ASBP; assumption.
 
@@ -1851,10 +1795,10 @@ Section CORRECTNESS.
       2: { right. right. simpl.
            rewrite ZERO.
            rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr; simplify; try lia.
-           apply ZExtra.mod_0_bounds; simplify; try lia. }
-      simplify.
-      exploit (BOUNDS ptr); try lia. intros. simplify.
+           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
+           apply ZExtra.mod_0_bounds; crush; try lia. }
+      crush.
+      exploit (BOUNDS ptr); try lia. intros. crush.
       exploit (BOUNDS ptr v); try lia. intros.
       invert H0.
       match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
@@ -1906,66 +1850,10 @@ Section CORRECTNESS.
     apply boolToValue_ValueToBool.
     constructor.
 
-    unfold Verilog.merge_regs.
-    unfold_merge.
-    apply AssocMap.gss.
-
-    destruct b.
-    rewrite assumption_32bit.
-    simplify.
-    apply match_state with (sp' := sp'); eauto.
-    unfold Verilog.merge_regs.
-    unfold_merge.
-    apply regs_lessdef_add_greater. apply greater_than_max_func.
-    assumption.
-
-    unfold state_st_wf. intros.
-    invert H3.
-    unfold Verilog.merge_regs. unfold_merge.
-    apply AssocMap.gss.
-
-    (** Match arrays *)
-    invert MARR. simplify.
-    econstructor.
-    repeat split; simplify.
-    unfold HTL.empty_stack.
-    simplify.
-    unfold Verilog.merge_arrs.
-
-    rewrite AssocMap.gcombine.
-    2: { reflexivity. }
-    rewrite AssocMap.gss.
-    unfold Verilog.merge_arr.
-    setoid_rewrite H4.
-    reflexivity.
-
-    rewrite combine_length.
-    unfold arr_repeat. simplify.
-    rewrite list_repeat_len.
-    reflexivity.
-
-    unfold arr_repeat. simplify.
-    rewrite list_repeat_len.
-    congruence.
-
-    intros.
-    erewrite array_get_error_equal.
-    eauto. apply combine_none.
-    assumption.
-
-    rewrite assumption_32bit.
-    apply match_state with (sp' := sp'); eauto.
-    unfold Verilog.merge_regs. unfold_merge.
-    apply regs_lessdef_add_greater. apply greater_than_max_func.
-    assumption.
-
-    unfold state_st_wf. intros.
-    invert H1.
-    unfold Verilog.merge_regs. unfold_merge.
-    apply AssocMap.gss.
+    big_tac.
 
-    (** Match arrays *)
-    all: invert MARR. big_tac.
+    invert MARR.
+    destruct b; rewrite assumption_32bit; big_tac.
 
     Unshelve.
     constructor.
@@ -2018,6 +1906,8 @@ Section CORRECTNESS.
       constructor. constructor.
 
       unfold state_st_wf in WF; big_tac; eauto.
+      apply st_greater_than_res.
+      apply st_greater_than_res.
 
       apply HTL.step_finish.
       unfold Verilog.merge_regs.
@@ -2043,6 +1933,8 @@ Section CORRECTNESS.
       constructor. constructor. constructor.
 
       unfold state_st_wf in WF; big_tac; eauto.
+      apply st_greater_than_res.
+      apply st_greater_than_res.
 
       apply HTL.step_finish.
       unfold Verilog.merge_regs.
@@ -2081,7 +1973,7 @@ Section CORRECTNESS.
 
     inversion MSTATE; subst. inversion TF; subst.
     econstructor. split. apply Smallstep.plus_one.
-    eapply HTL.step_call. simplify.
+    eapply HTL.step_call. crush.
 
     apply match_state with (sp' := stk); eauto.
 
@@ -2093,8 +1985,6 @@ Section CORRECTNESS.
 
     constructor.
 
-    apply list_repeat_len.
-    intros.
     destruct (Mem.load AST.Mint32 m' stk
                        (Integers.Ptrofs.unsigned (Integers.Ptrofs.add
                                                     Integers.Ptrofs.zero
@@ -2103,17 +1993,20 @@ Section CORRECTNESS.
     pose proof H as ALLOC.
     eapply LOAD_ALLOC in ALLOC.
     2: { exact LOAD. }
+    ptrofs. rewrite LOAD.
     rewrite ALLOC.
     repeat constructor.
-    constructor.
+
+    ptrofs. rewrite LOAD.
+    repeat constructor.
 
     unfold reg_stack_based_pointers. intros.
-    unfold RTL.init_regs; simplify.
+    unfold RTL.init_regs; crush.
     destruct (RTL.fn_params f);
     rewrite Registers.Regmap.gi; constructor.
 
     unfold arr_stack_based_pointers. intros.
-    simplify.
+    crush.
     destruct (Mem.load AST.Mint32 m' stk
                        (Integers.Ptrofs.unsigned (Integers.Ptrofs.add
                                                     Integers.Ptrofs.zero
@@ -2134,36 +2027,34 @@ Section CORRECTNESS.
 
     unfold Mem.alloc in H.
     invert H.
-    simplify.
+    crush.
     unfold Mem.load.
     intros.
     match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence.
     invert v0. unfold Mem.range_perm in H3.
-    unfold Mem.perm in H3. simplify.
+    unfold Mem.perm in H3. crush.
     unfold Mem.perm_order' in H3.
-    rewrite Integers.Ptrofs.add_zero_l in H3.
-    rewrite Integers.Ptrofs.unsigned_repr in H3; simplify; try lia.
-    exploit (H3 ptr). lia. intros.
+    small_tac.
+    exploit (H3 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros.
     rewrite Maps.PMap.gss in H8.
     match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction.
-    simplify.
+    crush.
     apply proj_sumbool_true in H10. lia.
 
     unfold Mem.alloc in H.
     invert H.
-    simplify.
+    crush.
     unfold Mem.store.
     intros.
     match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence.
     invert v0. unfold Mem.range_perm in H3.
-    unfold Mem.perm in H3. simplify.
+    unfold Mem.perm in H3. crush.
     unfold Mem.perm_order' in H3.
-    rewrite Integers.Ptrofs.add_zero_l in H3.
-    rewrite Integers.Ptrofs.unsigned_repr in H3; simplify; try lia.
-    exploit (H3 ptr). lia. intros.
+    small_tac.
+    exploit (H3 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros.
     rewrite Maps.PMap.gss in H8.
     match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction.
-    simplify.
+    crush.
     apply proj_sumbool_true in H10. lia.
     Opaque Mem.alloc.
     Opaque Mem.load.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index a78256b..0cdecba 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -426,7 +426,7 @@ Proof.
   destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW;
     destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH;
     destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN;
-    simplify;
+    crush;
     monadInv Heqr.
 
   (* TODO: We should be able to fold this into the automation. *)
diff --git a/src/verilog/Array.v b/src/verilog/Array.v
index f3e1cd7..be06541 100644
--- a/src/verilog/Array.v
+++ b/src/verilog/Array.v
@@ -29,7 +29,7 @@ Lemma list_set_spec1 {A : Type} :
   forall l i (x : A),
     i < length l -> nth_error (list_set i x l) i = Some x.
 Proof.
-  induction l; intros; destruct i; simplify; try lia; try reflexivity; firstorder.
+  induction l; intros; destruct i; crush; firstorder.
 Qed.
 Hint Resolve list_set_spec1 : array.
 
@@ -37,7 +37,7 @@ Lemma list_set_spec2 {A : Type} :
   forall l i (x : A) d,
     i < length l -> nth i (list_set i x l) d = x.
 Proof.
-  induction l; intros; destruct i; simplify; try lia; try reflexivity; firstorder.
+  induction l; intros; destruct i; crush; firstorder.
 Qed.
 Hint Resolve list_set_spec2 : array.
 
@@ -46,7 +46,7 @@ Lemma list_set_spec3 {A : Type} :
     i1 <> i2 ->
     nth_error (list_set i1 x l) i2 = nth_error l i2.
 Proof.
-  induction l; intros; destruct i1; destruct i2; simplify; try lia; try reflexivity; firstorder.
+  induction l; intros; destruct i1; destruct i2; crush; firstorder.
 Qed.
 Hint Resolve list_set_spec3 : array.
 
@@ -56,7 +56,7 @@ Lemma array_set_wf {A : Type} :
 Proof.
   induction l; intros; destruct i; auto.
 
-  invert H; simplify; auto.
+  invert H; crush; auto.
 Qed.
 
 Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) :=
@@ -72,7 +72,7 @@ Proof.
   intros.
 
   rewrite <- a.(arr_wf) in H.
-  unfold array_set. simplify.
+  unfold array_set. crush.
   eauto with array.
 Qed.
 Hint Resolve array_set_spec1 : array.
@@ -84,7 +84,7 @@ Proof.
   intros.
 
   rewrite <- a.(arr_wf) in H.
-  unfold array_set. simplify.
+  unfold array_set. crush.
   eauto with array.
 Qed.
 Hint Resolve array_set_spec2 : array.
@@ -93,7 +93,7 @@ Lemma array_set_len {A : Type} :
   forall a i (x : A),
     a.(arr_length) = (array_set i x a).(arr_length).
 Proof.
-  unfold array_set. simplify. reflexivity.
+  unfold array_set. crush.
 Qed.
 
 Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A :=
@@ -104,7 +104,7 @@ Lemma array_get_error_equal {A : Type} :
     a.(arr_contents) = b.(arr_contents) ->
     array_get_error i a = array_get_error i b.
 Proof.
-  unfold array_get_error. congruence.
+  unfold array_get_error. crush.
 Qed.
 
 Lemma array_get_error_bound {A : Type} :
@@ -142,7 +142,7 @@ Proof.
 
   unfold array_get_error.
   unfold array_set.
-  simplify.
+  crush.
   eauto with array.
 Qed.
 
@@ -180,18 +180,17 @@ Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A :=
 Lemma list_repeat'_len {A : Type} : forall (a : A) n l,
     length (list_repeat' l a n) = (n + Datatypes.length l)%nat.
 Proof.
-  induction n; intros; simplify; try reflexivity.
+  induction n; intros; crush; try reflexivity.
 
   specialize (IHn (a :: l)).
   rewrite IHn.
-  simplify.
-  lia.
+  crush.
 Qed.
 
 Lemma list_repeat'_app {A : Type} : forall (a : A) n l,
     list_repeat' l a n = list_repeat' [] a n ++ l.
 Proof.
-  induction n; intros; simplify; try reflexivity.
+  induction n; intros; crush; try reflexivity.
 
   pose proof IHn.
   specialize (H (a :: l)).
@@ -207,7 +206,7 @@ Qed.
 Lemma list_repeat'_head_tail {A : Type} : forall n (a : A),
   a :: list_repeat' [] a n = list_repeat' [] a n ++ [a].
 Proof.
-  induction n; intros; simplify; try reflexivity.
+  induction n; intros; crush; try reflexivity.
   rewrite list_repeat'_app.
 
   replace (a :: list_repeat' [] a n ++ [a]) with (list_repeat' [] a n ++ [a] ++ [a]).
@@ -232,17 +231,17 @@ Proof.
   intros.
   unfold list_repeat.
   rewrite list_repeat'_len.
-  simplify. lia.
+  crush.
 Qed.
 
 Lemma dec_list_repeat_spec {A : Type} : forall n (a : A) a',
     (forall x x' : A, {x' = x} + {~ x' = x}) ->
     In a' (list_repeat a n) -> a' = a.
 Proof.
-  induction n; intros; simplify; try contradiction.
+  induction n; intros; crush.
 
   unfold list_repeat in *.
-  simplify.
+  crush.
 
   rewrite list_repeat'_app in H.
   pose proof (X a a').
@@ -278,14 +277,19 @@ Lemma list_repeat_lookup {A : Type} :
 Proof.
   induction n; intros.
 
-  destruct i; simplify; lia.
+  destruct i; crush.
 
   rewrite list_repeat_cons.
-  destruct i; simplify; firstorder.
+  destruct i; crush; firstorder.
 Qed.
 
 Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n).
 
+Lemma arr_repeat_length {A : Type} : forall n (a : A), arr_length (arr_repeat a n) = n.
+Proof.
+  unfold list_repeat. crush. apply list_repeat_len.
+Qed.
+
 Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C :=
   match x, y with
   | a :: t, b :: t' => f a b :: list_combine f t t'
@@ -295,9 +299,9 @@ Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B)
 Lemma list_combine_length {A B C : Type} (f : A -> B -> C) : forall (x : list A) (y : list B),
     length (list_combine f x y) = min (length x) (length y).
 Proof.
-  induction x; intros; simplify; try reflexivity.
+  induction x; intros; crush.
 
-  destruct y; simplify; auto.
+  destruct y; crush; auto.
 Qed.
 
 Definition combine {A B C : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C :=
@@ -310,15 +314,24 @@ Proof.
 
   unfold combine.
   unfold make_array.
-  simplify.
+  crush.
 
   rewrite <- (arr_wf x) in *.
   rewrite <- (arr_wf y) in *.
 
-  destruct (arr_contents x); simplify.
-  - reflexivity.
-  - destruct (arr_contents y); simplify.
-    f_equal.
-    rewrite list_combine_length.
-    destruct (Min.min_dec (length l) (length l0)); congruence.
+  destruct (arr_contents x); destruct (arr_contents y); crush.
+  rewrite list_combine_length.
+  destruct (Min.min_dec (length l) (length l0)); congruence.
 Qed.
+
+Ltac array :=
+  try match goal with
+      | [ |- context[arr_length (combine _ _ _)] ] =>
+        rewrite combine_length
+      | [ |- context[length (list_repeat _ _)] ] =>
+        rewrite list_repeat_len
+      | |- context[array_get_error _ (arr_repeat ?x _) = Some ?x] =>
+        unfold array_get_error, arr_repeat
+      | |- context[nth_error (list_repeat ?x _) _ = Some ?x] =>
+        apply list_repeat_lookup
+      end.