Require Import ZArith.
Require Import List.
Require Import util.
Require Import machine_int.
Import MachineInt.
Require Import machine_int_spec.
Require Import heap.

Open Local Scope Z_scope.

(********************************************)
(* heaps *)
(********************************************)

Module int32.
  Definition elem := int 32.
End int32.

Module heap := map int32.

Notation "k '---' l" := (heap.dif k l) (at level 69) : asm_heap_scope.
Notation "k '+++' m" := (heap.union k m) (at level 69) : asm_heap_scope.
Notation "k '#' m" := (heap.disjoint k m) (at level 79) : asm_heap_scope.

(********************************************)
(* stores *)
(********************************************)

(* general purpose registers *)
Inductive gp_reg : Set :=
  gpr_r0 : gp_reg
  | gpr_zero : gp_reg (* $0: always return zero, writes are ignored *)
  | gpr_at : gp_reg (* $1: assembler temporary *)
  | gpr_v0 : gp_reg (* $2,$3: values return by subroutine *)
  | gpr_v1 : gp_reg 
  | gpr_a0 : gp_reg (* $4-$7: first four parameters for a subroutine *)
  | gpr_a1 : gp_reg 
  | gpr_a2 : gp_reg 
  | gpr_a3 : gp_reg 
  | gpr_t0 : gp_reg (* $8-$15,$24,$25: subroutines may use w.o. saving *)
  | gpr_t1 : gp_reg 
  | gpr_t2 : gp_reg 
  | gpr_t3 : gp_reg 
  | gpr_t4 : gp_reg 
  | gpr_t5 : gp_reg 
  | gpr_t6 : gp_reg 
  | gpr_t7 : gp_reg 
  | gpr_t8 : gp_reg 
  | gpr_t9 : gp_reg
  | gpr_s0 : gp_reg (* $16-$23: must be restored by the subroutine *)
  | gpr_s1 : gp_reg 
  | gpr_s2 : gp_reg 
  | gpr_s3 : gp_reg 
  | gpr_s4 : gp_reg 
  | gpr_s5 : gp_reg 
  | gpr_s6 : gp_reg 
  | gpr_s7 : gp_reg 
  | gpr_s8 : gp_reg
  | gpr_k0 : gp_reg (* $26,$27: reserved for use by interrupt/trap handler *)
  | gpr_k1 : gp_reg 
  | gpr_gp : gp_reg (* $29: stack pointer *)
  | gpr_sp : gp_reg (* $30: (or "s8") frame pointer *)
  | gpr_ra : gp_reg. (* $31: used by the subroutine calling instructions for the return address *)

Definition gpr_fp := gpr_s8.

Definition gp_reg_beq (r1 r2: gp_reg) : bool :=
  match (r1,r2) with
    | (gpr_r0,gpr_r0) => true
    | (gpr_zero,gpr_zero) => true
    | (gpr_at,gpr_at) => true
    | (gpr_v0,gpr_v0) => true
    | (gpr_v1,gpr_v1) => true
    | (gpr_a0,gpr_a0) => true
    | (gpr_a1,gpr_a1) => true
    | (gpr_a2,gpr_a2) => true
    | (gpr_a3,gpr_a3) => true
    | (gpr_t0,gpr_t0) => true
    | (gpr_t1,gpr_t1) => true
    | (gpr_t2,gpr_t2) => true
    | (gpr_t3,gpr_t3) => true
    | (gpr_t4,gpr_t4) => true
    | (gpr_t5,gpr_t5) => true
    | (gpr_t6,gpr_t6) => true
    | (gpr_t7,gpr_t7) => true
    | (gpr_t8,gpr_t8) => true
    | (gpr_t9,gpr_t9) => true
    | (gpr_s0,gpr_s0) => true
    | (gpr_s1,gpr_s1) => true
    | (gpr_s2,gpr_s2) => true
    | (gpr_s3,gpr_s3) => true
    | (gpr_s4,gpr_s4) => true
    | (gpr_s5,gpr_s5) => true
    | (gpr_s6,gpr_s6) => true
    | (gpr_s7,gpr_s7) => true
    | (gpr_s8,gpr_s8) => true
    | (gpr_k0,gpr_k0) => true
    | (gpr_k1,gpr_k1) => true
    | (gpr_gp,gpr_gp) => true
    | (gpr_sp,gpr_sp) => true
    | (gpr_ra,gpr_ra) => true
    | _ => false
  end.

Lemma gp_reg_beq_true: forall r1 r2,
  gp_reg_beq r1 r2 = true -> r1 = r2.
  destruct r1; destruct r2; simpl; intros; (simpl in H; (discriminate || auto)).
Qed.

Lemma gp_reg_beq_false: forall r1 r2,
  gp_reg_beq r1 r2 = false -> r1 <> r2.
  destruct r1; destruct r2; simpl; intros; (simpl in H; (discriminate || auto)).
Qed.

Lemma gp_reg_beq_false': forall r1 r2,
  r1 <> r2 -> gp_reg_beq r1 r2 = false.
  unfold gp_reg_beq.
  destruct r1; destruct r2; simpl; intros; (apply refl_equal || intuition).
Qed.

Lemma gp_reg_beq_refl: forall r,
  gp_reg_beq r r = true.
  destruct r; simpl; auto.
Qed.

(*
Module Type STORE.
  Parameter store : Set.
  Parameter var : Set.
  Parameter val : Set.
  
  Parameter lookup : var -> store -> val.
  Parameter update : var -> val -> store -> store.
  Parameter lookup_update : forall x y z st,
    x <> y -> lookup x st = lookup x (update y z st).
  Parameter lookup_update' : forall x z st,
    lookup x (update x z st) = z.
End STORE.
*)
Module gpr.
  (*<: STORE 
  with Definition var := gp_reg
    with Definition val := int 32.*)
  Definition var := gp_reg.
  Definition val := int 32.
  Definition store := list (gp_reg * int 32).

  Fixpoint lookup' (r: gp_reg) (s: store) {struct s}: int 32 :=
    match s with
      | nil => zero32
      | (r',i)::tl => 
        if (gp_reg_beq r r') then i else
          lookup' r tl
    end.

  Definition lookup (r: gp_reg) (s: store) : int 32 :=
    if (gp_reg_beq r gpr_zero) then zero32
      else lookup' r s.

  Fixpoint update' (r: gp_reg) (i: int 32) (s: store) {struct s}: store :=
    match s with
      | nil => (r,i)::nil
      | (r',i')::tl => 
        if (gp_reg_beq r r') then ((r,i)::tl) else
          (r',i')::(update' r i tl)
    end.
  
  Definition update (r: gp_reg) (i: int 32) (s: store) : store :=
    if (gp_reg_beq r gpr_zero) then s
      else update' r i s.
 
  Lemma lookup_update_p : forall st x y z,
    x <> y -> lookup' x st = lookup' x (update' y z st).
    induction st.
    intros.
    simpl.
    rewrite (gp_reg_beq_false' _ _ H); auto.
    intros.
    destruct a.
    simpl.
    assert (gp_reg_beq x g = true \/ gp_reg_beq x g = false).
    destruct (gp_reg_beq x g); auto.
    assert (gp_reg_beq y g = true \/ gp_reg_beq y g = false).
    destruct (gp_reg_beq y g); auto.
    inversion_clear H0.
    rewrite H2.
    inversion_clear H1.
    rewrite (gp_reg_beq_true _ _ H2) in H.
    rewrite (gp_reg_beq_true _ _ H0) in H.
    intuition.
    rewrite H0.
    simpl.
    rewrite H2.
    auto.
    rewrite H2.
    inversion_clear H1.
    rewrite H0.
    simpl.
    rewrite (gp_reg_beq_false' _ _ H); auto.
    rewrite H0.
    simpl.
    rewrite H2.
    apply IHst.
    auto.
  Qed.

  Lemma lookup_update : forall x y z st,
    x <> y -> lookup x st = lookup x (update y z st).
    intros.
    unfold lookup; unfold update.
    assert (gp_reg_beq x gpr_zero = true \/ gp_reg_beq x gpr_zero = false).
    destruct (gp_reg_beq x gpr_zero); auto.
    assert (gp_reg_beq y gpr_zero = true \/ gp_reg_beq y gpr_zero = false).
    destruct (gp_reg_beq y gpr_zero); auto.
    inversion_clear H0; inversion_clear H1.
    rewrite (gp_reg_beq_true _ _ H2) in H.
    rewrite (gp_reg_beq_true _ _ H0) in H.
    intuition.
    rewrite H2; auto.
    rewrite H2.
    rewrite H0.
    auto.
    rewrite H2; rewrite H0.
    apply lookup_update_p; auto.
  Qed.
    
  Lemma lookup_update_p' : forall st w z ,
    lookup' w (update' w z st) = z.
    induction st; simpl; intros.
    rewrite gp_reg_beq_refl.
    auto.
    destruct a.
    assert (gp_reg_beq w g = true \/ gp_reg_beq w g = false).
    destruct (gp_reg_beq w g); auto.
    inversion_clear H.
    rewrite H0.
    simpl.
    rewrite gp_reg_beq_refl.
    auto.
    rewrite H0.
    simpl.
    rewrite H0.
    apply IHst; auto.
Qed.


  Lemma lookup_update' : forall x z st,
    x <> gpr_zero ->
    lookup x (update x z st) = z.
    intros.
    unfold lookup; unfold update.
    assert (gp_reg_beq x gpr_zero = true \/ gp_reg_beq x gpr_zero = false).
    destruct (gp_reg_beq x gpr_zero); auto.
    inversion_clear H0.
    rewrite (gp_reg_beq_true _ _ H1) in H.
    intuition.
    rewrite H1.
    apply lookup_update_p'.
  Qed.
    
  
  (* gpr_zero always evaluates to zero *)
  Lemma gpr_zero_zero32 : forall s, 
    lookup gpr_zero s = zero32.
    intros.
    unfold lookup.
    rewrite gp_reg_beq_refl.
    auto.
  Qed.

End gpr.

Inductive cp0_reg : Set :=
  cp0_0 : cp0_reg 
  | cp0_1 : cp0_reg 
  | cp0_2 : cp0_reg 
  | cp0_3 : cp0_reg 
  | cp0_4 : cp0_reg 
  | cp0_5 : cp0_reg 
  | cp0_6 : cp0_reg 
  | cp0_7 : cp0_reg 
  | cp0_8 : cp0_reg 
  | cp0_9 : cp0_reg 
  | cp0_10 : cp0_reg 
  | cp0_11 : cp0_reg 
  | cp0_12 : cp0_reg 
  | cp0_13 : cp0_reg 
  | cp0_14 : cp0_reg 
  | cp0_15 : cp0_reg 
  | cp0_16 : cp0_reg 
  | cp0_17 : cp0_reg 
  | cp0_18 : cp0_reg 
  | cp0_19 : cp0_reg 
  | cp0_20 : cp0_reg 
  | cp0_21 : cp0_reg 
  | cp0_22 : cp0_reg 
  | cp0_23 : cp0_reg 
  | cp0_24 : cp0_reg 
  | cp0_25 : cp0_reg 
  | cp0_26 : cp0_reg 
  | cp0_27 : cp0_reg 
  | cp0_28 : cp0_reg 
  | cp0_29 : cp0_reg 
  | cp0_30 : cp0_reg 
  | cp0_31 : cp0_reg.

Definition cp0_status := cp0_12.
Definition cp0_cause := cp0_13.
Definition cp0_epc := cp0_14.

Definition cp0_reg_beq (r1 r2: cp0_reg) : bool :=
  match (r1,r2) with
    | (cp0_0,cp0_0) => true
    | (cp0_1,cp0_1) => true
    | (cp0_2,cp0_2) => true
    | (cp0_3,cp0_3) => true
    | (cp0_4,cp0_4) => true
    | (cp0_5,cp0_5) => true
    | (cp0_6,cp0_6) => true
    | (cp0_7,cp0_7) => true
    | (cp0_8,cp0_8) => true
    | (cp0_9,cp0_9) => true
    | (cp0_10,cp0_10) => true
    | (cp0_11,cp0_11) => true
    | (cp0_12,cp0_12) => true
    | (cp0_13,cp0_13) => true
    | (cp0_14,cp0_14) => true
    | (cp0_15,cp0_15) => true
    | (cp0_16,cp0_16) => true
    | (cp0_17,cp0_17) => true
    | (cp0_18,cp0_18) => true
    | (cp0_19,cp0_19) => true
    | (cp0_20,cp0_20) => true
    | (cp0_21,cp0_21) => true
    | (cp0_22,cp0_22) => true
    | (cp0_23,cp0_23) => true
    | (cp0_24,cp0_24) => true
    | (cp0_25,cp0_25) => true
    | (cp0_26,cp0_26) => true
    | (cp0_27,cp0_27) => true
    | (cp0_28,cp0_28) => true
    | (cp0_29,cp0_29) => true
    | (cp0_30,cp0_30) => true
    | (cp0_31,cp0_31) => true
    | _ => false
  end.

Lemma cp0_reg_beq_true: forall r1 r2,
  cp0_reg_beq r1 r2 = true -> r1 = r2.
  destruct r1; destruct r2; simpl; intros; (simpl in H; (discriminate || auto)).
Qed.

Lemma cp0_reg_beq_false: forall r1 r2,
  cp0_reg_beq r1 r2 = false -> r1 <> r2.
  destruct r1; destruct r2; simpl; intros; (simpl in H; (discriminate || auto)).
Qed.

Lemma cp0_reg_beq_false': forall r1 r2,
  r1 <> r2 -> cp0_reg_beq r1 r2 = false.
  unfold gp_reg_beq.
  destruct r1; destruct r2; simpl; intros; (apply refl_equal || intuition).
Qed.

Lemma cp0_reg_beq_refl: forall r,
  cp0_reg_beq r r = true.
  destruct r; simpl; auto.
Qed.

Module cp0.
(*<: STORE
  with Definition var := cp0_reg
    with Definition val := int 32.*)
  
  Definition var := cp0_reg.
  Definition val := int 32.
  Definition store := list (cp0_reg * (int 32)).

  Fixpoint lookup (r: cp0_reg) (s: store) {struct s}: int 32 :=
    match s with
      | nil => zero32
      | (r',i)::tl => 
        if (cp0_reg_beq r r') then i else
          lookup r tl
    end.

  Fixpoint update (r: cp0_reg) (i: int 32) (s: store) {struct s}: store :=
    match s with
      | nil => (r,i)::nil
      | (r',i')::tl => 
        if (cp0_reg_beq r r') then ((r,i)::tl) else
          (r',i')::(update r i tl)
    end.
  
  Lemma lookup_update : forall x y z st,
    x <> y -> lookup x st = lookup x (update y z st).
    intros.
    generalize st x y z H.
    clear st x y z H.
    induction st.
    simpl; intros.
    rewrite (cp0_reg_beq_false' _ _ H).
    auto.
    destruct a; simpl; intros.
    assert (cp0_reg_beq x c = true \/ cp0_reg_beq x c = false).
    destruct (cp0_reg_beq x c); auto.
    assert (cp0_reg_beq y c = true \/ cp0_reg_beq y c = false).
    destruct (cp0_reg_beq y c); auto.
    inversion_clear H0; inversion_clear H1.
    rewrite (cp0_reg_beq_true _ _ H2) in H.
    rewrite (cp0_reg_beq_true _ _ H0) in H.
    intuition.
    rewrite H2.
    rewrite H0.
    simpl.
    rewrite H2.
    auto.
    rewrite H2.
    rewrite H0.
    simpl.
    rewrite (cp0_reg_beq_false' _ _ H); auto.
    rewrite H2; rewrite H0.
    simpl.
    rewrite H2.
    apply IHst; auto.
  Qed.

  Lemma lookup_update' : forall w z st,
    lookup w (update w z st) = z.
    intros.
    generalize st w z.
    clear st w z.
    induction st.
    simpl.
    intros.
    rewrite (cp0_reg_beq_refl).
    auto.
    destruct a; simpl; intros.
    assert (cp0_reg_beq w c = true \/ cp0_reg_beq w c = false).
    destruct (cp0_reg_beq w c); auto.
    inversion_clear H.
    rewrite H0.
    simpl.
    rewrite (cp0_reg_beq_refl).
    auto.
    rewrite H0.
    simpl.
    rewrite H0.
    apply IHst.
  Qed.

End cp0.

(****************************************************************************)
(* multiplier and properties *)
(***********************************************************************)

Module Type MULTIPLIER.
  Parameter acx_size : nat.
  Parameter m : Set.
  
  Parameter acx_size_min : (8 <= acx_size)%nat.
  
  Parameter acx : m -> int acx_size.
  Parameter lo : m -> int 32.
  Parameter hi : m -> int 32.
  
  (* mthi *)
  Parameter mthi_op : int 32 -> m -> m.
  Parameter acx_mthi_op : forall m a, acx (mthi_op a m) =  acx m.
  Parameter hi_mthi_op : forall m a, hi (mthi_op a m) = a.
  Parameter lo_mthi_op : forall m a, lo (mthi_op a m) = lo m.
  
  (* mtlo *)
  Parameter mtlo_op : int 32 -> m -> m.
  Parameter acx_mtlo_op : forall m a, acx (mtlo_op a m) = acx m.
  Parameter hi_mtlo_op : forall m a, hi (mtlo_op a m) = hi m.
  Parameter lo_mtlo_op : forall m a, lo (mtlo_op a m) = a.
  
  (* utoZ interpret the contents of the muliplier as an unsigned integer *)
  Parameter utoZ : m -> Z.
  Parameter utoZ_def: forall m, utoZ m = 
    u2Z (lo m) + u2Z (hi m) * Zbeta 1 + u2Z (acx m) * Zbeta 2.
  Parameter utoZ_pos : forall m, 0 <= utoZ m.
  Parameter utoZ_acx_beta2 : forall (m0:m),
    utoZ m0 < Zbeta 2 -> acx m0 = Z2u acx_size 0.
  Parameter lo_remainder: forall m l (a:int l),
    (l <= acx_size + 32 + 32)%nat ->
    utoZ m = u2Z a ->
    lo m = rem 32 a.
  Parameter utoZ_lo_beta1 : forall (m0:m),
    utoZ m0 < Zbeta 1 ->
    acx m0 = Z2u acx_size 0 /\ hi m0 = Z2u 32 0 /\ 
    utoZ m0 = u2Z (lo m0).
  
  (* is_null predicate *)
  Parameter is_null : m -> Prop.
  Parameter is_null_utoZ : forall (m0:m), is_null m0 -> utoZ m0 = 0.
  Parameter utoZ_is_null : forall (m0:m), utoZ m0 = 0 -> is_null m0.
  Parameter is_null_lo : forall (m0:m), 
    is_null m0 -> lo m0 = Z2u 32 0.
  
  (* maddu *)
  Parameter maddu_op : int (2 * 32) -> m -> m.
  Parameter maddu_utoZ : forall m a,
    utoZ m < Zbeta 2 * (Zpower 2 acx_size - 1) ->
    utoZ (maddu_op a m) = u2Z a + utoZ m.

  (* multu *)
  Parameter multu_op : int (2 * 32) -> m -> m.
  Parameter multu_utoZ: forall p m,
    utoZ (multu_op p m) = u2Z p.
  
  (* msubu *)
  Parameter msubu_op : int (2 * 32) -> m -> m.
  Parameter msubu_utoZ : forall m a,
    utoZ m < Zbeta 2 ->
    utoZ m >= u2Z a ->
    utoZ (msubu_op a m) = utoZ m - u2Z a.
  Parameter msubu_utoZ_overflow : forall m a,
    utoZ m < Zbeta 2 ->
    utoZ m < u2Z a ->
    utoZ (msubu_op a m) = Zbeta 2 + utoZ m - u2Z a.

  (* mflhxu *)
  Parameter mflhxu_op : m -> m.
  Parameter mflhxu_utoZ : forall m,
    utoZ m = utoZ (mflhxu_op m) * Zbeta 1 + u2Z (lo m).
  Parameter hi_mflhxu_op : forall (m0:m),
    u2Z (hi (mflhxu_op m0)) =
    u2Z (zero_extend (32 - acx_size) (acx m0)).
  Parameter lo_mflhxu_op : forall (m0:m), 
    lo (mflhxu_op m0) = hi m0.
  Parameter mflhxu_kbeta1_utoZ : forall (m0:m) k,
    utoZ m0 < Zbeta 1 * k ->
    utoZ (mflhxu_op m0) < k.
  Parameter mflhxu_beta2_utoZ : forall (m0:m),
    utoZ m0 < Zbeta 2 ->
    utoZ (mflhxu_op m0) < Zbeta 1.
End MULTIPLIER.

Module multiplier : MULTIPLIER.
  
  Definition acx_size := 8%nat.
  
  Definition m := prod (int acx_size) (prod (int 32) (int 32)).
  
  Lemma acx_size_min : (8 <= acx_size)%nat.
    unfold acx_size.
    auto.
  Qed.
  
  Definition acx (m0:m) : int acx_size := match m0 with (a, _) => a end.
  Definition hi (m0:m) : int 32 := match m0 with (_, (b, _)) => b end.
  Definition lo (m0:m) : int 32 := match m0 with (_, (_, c)) => c end.
  
  (*
   * mthi
   *)
  
  Definition mthi_op (x:int 32) (m0:m) : m := match m0 with (a, (b, c)) => (a, (x, c)) end.
  
  Lemma acx_mthi_op: forall m a,
    acx (mthi_op a m) = acx m.
    intros.
    destruct m0.
    destruct p.
    unfold acx; unfold mthi_op; auto.
  Qed.
  
  Lemma hi_mthi_op: forall m a,
    hi (mthi_op a m) = a.
    intros.
    destruct m0.
    destruct p.
    unfold hi; unfold mthi_op; auto.
  Qed.
  
  Lemma lo_mthi_op : forall m a,
    lo (mthi_op a m) = lo m.
    destruct m0.
    destruct p.
    auto.
  Qed.
  
  (*
   * mtlo
   *)
  
  Definition mtlo_op (x:int 32) (m0:m) : m := match m0 with (a, (b, c)) => (a, (b, x)) end.
  
  Lemma acx_mtlo_op: forall m a,
    acx (mtlo_op a m) = acx m.
    intros.
    destruct m0.
    destruct p.
    unfold acx; unfold mtlo_op; auto.
  Qed.
  
  Lemma hi_mtlo_op: forall m a,
    hi (mtlo_op a m) = hi m.
    intros.
    destruct m0.
    destruct p.
    unfold hi; unfold mtlo_op; auto.
  Qed.
  
  Lemma lo_mtlo_op: forall m a,
    lo (mtlo_op a m) = a.
    intros.
    destruct m0.
    destruct p.
    unfold lo; unfold mtlo_op; auto.
  Qed.
  
  (*  
   * interpretation of the multiplier as an unsigned integer
   *)
  
  Definition utoZ m :=
    let acx_reg := acx m in
      let (hi_reg, lo_reg) := (hi m, lo m) in
	u2Z acx_reg * Zbeta 2 + u2Z hi_reg * Zbeta 1 + u2Z lo_reg.
  
  Lemma utoZ_def: forall m,
    utoZ m = u2Z (lo m) + u2Z (hi m) * Zbeta 1 + u2Z (acx m) * Zbeta 2.
    unfold utoZ.
    intros; omega.
  Qed.

  Lemma utoZ_pos : forall m, 0 <= utoZ m.
    intros.
    rewrite utoZ_def.
    generalize (min_u2Z (lo m0)); intro.
    assert ( 0 <= u2Z (hi m0) * Zbeta 1 ).
    apply Zmult_le_0_compat.
    apply min_u2Z.
    generalize (Zbeta_1 1); omega.
    assert ( 0 <= u2Z (acx m0) * Zbeta 2 ).
    apply Zmult_le_0_compat.
    apply min_u2Z.
    generalize (Zbeta_1 2); omega.
    omega.
  Qed.
    
  Lemma utoZ_acx_beta2 : forall (m0:multiplier.m),
    utoZ m0 < Zbeta 2 ->
    acx m0 = Z2u acx_size 0.
    intros.
    destruct m0 as [i0 p].
    destruct p as [i1 i2].
    simpl.
    unfold utoZ in H.
    simpl in H.
    assert (u2Z i0 = 0 \/ u2Z i0 > 0).
    generalize (min_u2Z i0); intro.
    omega.
    inversion_clear H0.
    apply u2Z_injection.
    rewrite Z2u_injection.
    auto.
    generalize (Zpower_1 acx_size); omega.
    assert (u2Z i0 >= 1).
    omega.
    assert (Zbeta 2 <= u2Z i0 * Zbeta 2).
    apply Zle_trans with (1 * Zbeta 2).
    omega.
    apply Zmult_le_compat_r.
    omega.
    assert ( u2Z i0 * Zbeta 2 < Zbeta 2 ).
    assert (u2Z i1 = 0 \/ u2Z i1 > 0).
    generalize (min_u2Z i1); intro.
    omega.
    inversion_clear H2.
    assert (u2Z i2 = 0 \/ u2Z i2 > 0).
    generalize (min_u2Z i2); intro.
    omega.
    inversion_clear H2.
    rewrite H3 in H; rewrite H4 in H.
    omega.
    rewrite H3 in H.
    omega.
    assert (u2Z i2 = 0 \/ u2Z i2 > 0).
    generalize (min_u2Z i2); intro.
    omega.
    inversion_clear H2.
    rewrite H4 in H.
    generalize (Zbeta_1 1); intro.
    apply Zlt_trans with (u2Z i0 * Zbeta 2 + u2Z i1 * Zbeta 1).
    assert ( 1 <= u2Z i1 * Zbeta 1).
    assert ( 1 <= u2Z i1 ).
    omega.
    apply Zle_trans with (1*Zbeta 1).
    omega.
    apply Zmult_le_compat_r.
    auto.
    omega.
    omega.
    generalize (Zbeta_1 1); intro.
    omega.
    apply Zlt_trans with (u2Z i0 * Zbeta 2 + u2Z i1 * Zbeta 1 + u2Z i2).
    generalize (Zbeta_1 1); intros.
    assert ( 1 <= u2Z i1 * Zbeta 1).
    assert ( 1 <= u2Z i1 ).
    omega.
    apply Zle_trans with (1*Zbeta 1).
    omega.
    apply Zmult_le_compat_r.
    omega.
    omega.
    omega.
    assumption.
    generalize (Zbeta_1 2); omega.
    assert ( u2Z i0 * Zbeta 2 + u2Z i1 * Zbeta 1 + u2Z i2 > Zbeta 2).
    generalize (Zbeta_1 1); intro.
    generalize (Zbeta_1 2); intro.
    generalize (min_u2Z i2); intro.
    generalize (min_u2Z i1); intro.
    assert (0 <= u2Z i1 * Zbeta 1).
    apply Zmult_le_0_compat; omega.
    omega.
    red in H.
    red in H3.
    rewrite H in H3.
    discriminate.
  Qed.

  Lemma hi_zero : forall (m0:multiplier.m),
    utoZ m0 < Zbeta 1 ->
    hi m0 = Z2u 32 0.
    intros.
    destruct m0 as [i0 p].
    destruct p as [i1 i2].
    simpl.
    unfold utoZ in H.
    simpl in H.
    assert (u2Z i1 = 0 \/ u2Z i1 > 0).
    generalize (min_u2Z i1); omega.
    inversion_clear H0.
    cutrewrite (0 = u2Z (Z2u 32 0)) in H1.
    generalize (u2Z_injection H1); intro.
    auto.
    rewrite Z2u_injection.
    auto.
    generalize (Zpower_1 32); omega.
    assert (u2Z i1 >= 1).
    omega.
    assert (Zbeta 1 <= u2Z i1 * Zbeta 1).
    apply Zle_trans with (1 * Zbeta 1).
    omega.
    apply Zmult_le_compat_r.
    omega.
    assert ( u2Z i1 * Zbeta 1 < Zbeta 1 ).
    assert (u2Z i0 = 0 \/ u2Z i0 > 0).
    generalize (min_u2Z i0); omega.
    inversion_clear H2.
    assert (u2Z i2 = 0 \/ u2Z i2 > 0).
    generalize (min_u2Z i2); omega.
    inversion_clear H2.
    rewrite H4 in H; rewrite H3 in H.
    omega.
    rewrite H3 in H.
    omega.
    assert (u2Z i2 = 0 \/ u2Z i2 > 0).
    generalize (min_u2Z i2); omega.
    inversion_clear H2.
    rewrite H4 in H.
    generalize (Zbeta_1 2); intro.
    apply Zlt_trans with (u2Z i0 * Zbeta 2 + u2Z i1 * Zbeta 1).
    assert ( 1 <= u2Z i0 * Zbeta 2).
    assert ( 1 <= u2Z i0 ).
    omega.
    apply Zle_trans with (1*Zbeta 2).
    omega.
    apply Zmult_le_compat_r.
    auto.
    omega.
    omega.
    omega.
    apply Zlt_trans with (u2Z i0 * Zbeta 2 + u2Z i1 * Zbeta 1 + u2Z i2).
    assert (1 * 1 <= u2Z i1 * Zbeta 1).
    apply Zmult_le_compat.
    omega.
    generalize (Zbeta_1 1); omega.
    omega.
    omega.
    assert (1 * 1 <= u2Z i0 * Zbeta 2).
    apply Zmult_le_compat.
    omega.
    apply Zbeta_1.
    omega.
    omega.
    simpl (1*1) in H2.
    simpl (1*1) in H5.
    omega.
    assumption.
    generalize (Zbeta_1 1); omega.
    assert ( u2Z i0 * Zbeta 2 + u2Z i1 * Zbeta 1 + u2Z i2 >= Zbeta 1).
    generalize (Zbeta_1 1); intro.
    generalize (Zbeta_1 2); intro.
    generalize (min_u2Z i2); intro.
    assert (1 * Zbeta 1 <= u2Z i1 * Zbeta 1).
    apply Zmult_le_compat_r.
    omega.
    omega.
    rewrite Zmult_1_l in H6.
    generalize (min_u2Z i0);intro.
    generalize (Zbeta_1 2); intro.
    assert (0 <= u2Z i0 * Zbeta 2).
    apply Zmult_le_0_compat.
    omega.
    omega.
    omega.
    generalize (Zlt_not_le _ _ H); intro.
    assert (~ (u2Z i0 * Zbeta 2 + u2Z i1 * Zbeta 1 + u2Z i2 >= Zbeta 1)).
    omega.
    tauto.
  Qed.

  Lemma acxhi_zero : forall (m0:m),
    utoZ m0 < Zbeta 1 ->
    utoZ m0 = u2Z (lo m0).
    intros.
    assert (acx m0 = Z2u acx_size 0 /\ hi m0 = Z2u 32 0 ).
    split.
    apply utoZ_acx_beta2.
    apply Zlt_trans with (Zbeta 1).
    auto.
    apply Zbeta_lt.
    omega.
    apply hi_zero.
    auto.
    inversion_clear H0.
    destruct m0 as [i0 p].
    destruct p as [i1 i2].
    unfold utoZ.
    rewrite H1.
    rewrite H2.
    simpl.
    rewrite Z2u_injection.
    rewrite Z2u_injection.
    ring.
    generalize (Zpower_1 32); omega.
    generalize (Zpower_1 acx_size); omega.
  Qed.

  Lemma utoZ_lo_beta1 : forall (m0:m),
    utoZ m0 < Zbeta 1 ->
    acx m0 = Z2u acx_size 0 /\ hi m0 = Z2u 32 0 /\ 
    utoZ m0 = u2Z (lo m0).
    intros.
    split.
    apply utoZ_acx_beta2.
    apply Zlt_trans with (Zbeta 1).
    auto.
    apply Zbeta_lt.
    omega.
    split.
    apply hi_zero.
    auto.
    apply acxhi_zero.
    auto.
  Qed.

  Lemma lo_remainder': forall m l (a:int l),
    (l = acx_size + 32 + 32)%nat ->
    utoZ m = u2Z a ->
    lo m = rem 32 a.
    intros.
    destruct m0 as [i0 p].
    destruct p as [i1 i2].
    simpl.
    rewrite utoZ_def in H0.
    simpl in H0.
    assert (u2Z a = u2Z ((i0 ||| i1) ||| i2)).
    rewrite concat_u2Z.
    rewrite concat_u2Z.
    rewrite <-H0.
    rewrite Zbeta_power1.
    rewrite <-Zpower_64_Zbeta.
    ring.
    rewrite Zmult_assoc.
    rewrite <-Zpower_is_exp.
    simpl plus.
    ring.
    generalize a H0 H1; clear a H0 H1.
    rewrite H.
    intros.
    generalize (@u2Z_injection _ a ((i0 ||| i1) ||| i2) H1); intros.
    rewrite H2.
    symmetry.
    apply (@rem_concat (acx_size+32) (i0 ||| i1) 32 i2).
  Qed.

  Lemma lo_remainder: forall m l (a:int l),
    (l <= acx_size + 32 + 32)%nat ->
    utoZ m = u2Z a ->
    lo m = rem 32 a.
    intros.
    lapply (lo_remainder' m0 _ (zero_extend (( acx_size + 32 + 32)-l) a)).
    intros.
    rewrite H1.
    apply u2Z_injection.
    rewrite rem_zero_extend.
    auto.
    rewrite zero_extend_u2Z.
    auto.
    omega.
  Qed.

  (*
   * is_null
   *)

  Definition is_null (mult:m) := 
    utoZ mult = 0.
(*    mult = (Z2u acx_size 0, (Z2u 32 0, Z2u 32 0)).*)

  Lemma is_null_utoZ : forall (m0:m), is_null m0 -> utoZ m0 = 0.
    intros.
    red in H.
    assumption.
  Qed.

  Lemma utoZ_is_null : forall m, utoZ m = 0 -> is_null m.
    intros.
    red.
    assumption.
  Qed.

  Lemma is_null_lo : forall (m0:m), is_null m0 -> lo m0 = Z2u 32 0.
    intros.
    destruct m0.
    destruct p.
    simpl.
    red in H.
    unfold utoZ in H.
    simpl in H.
    generalize (min_u2Z i); intro.
    generalize (min_u2Z i0); intro.
    generalize (min_u2Z i1); intro.
    generalize (Zbeta_1 2); intro.
    generalize (Zbeta_1 1); intro.
    apply u2Z_injection.
    rewrite Z2u_injection.
    assert (0 <= u2Z i * Zbeta 2).
    apply Zmult_le_0_compat.
    omega.
    omega.
    assert (0 <= u2Z i0 * Zbeta 1).
    apply Zmult_le_0_compat.
    omega.
    omega.
    omega.
    split.
    apply Zle_refl.
    assert (2^^32 > 0).
    simpl.
    apply Zgt_pos_0.
    omega.
  Qed.

  (*
   * maddu
   *)

  Definition maddu_op (p:int (2 * 32)) (mult:m) : m :=
    let acx_reg := acx mult in
      let hi_reg := hi mult in
	let lo_reg := lo mult in
	  let sum := acx_reg ||| (hi_reg ||| lo_reg) in
	    let new_sum := add (zero_extend 8 p) sum in
	      let lo_reg' := rem 32 new_sum in
		let sum' := shr_shrink 32 new_sum in 
		  let hi_reg' := rem 32 sum' in
		    let acx_reg' := shr_shrink 32 sum' in
		      (acx_reg', (hi_reg', lo_reg')).

  Lemma concat_u2Z' : forall (a:int acx_size) (b:int (2*32)),
    u2Z (a ||| b) = u2Z a * Zbeta 2 + u2Z b.
    intros.
    apply (@concat_u2Z acx_size (2*32)).
  Qed.

  Lemma maddu_utoZ : forall m a,
    utoZ m < Zbeta 2 * (Zpower 2 acx_size - 1) ->
    utoZ (maddu_op a m) = u2Z a + utoZ m.
    intros.
    destruct m0.
    destruct p.
    generalize H; clear H.
    unfold utoZ; unfold acx; unfold hi; unfold lo; unfold maddu_op.
    intro.
    cutrewrite (Zbeta 2 = Zbeta 1 * Zbeta 1).
    rewrite Zmult_assoc.
    rewrite <-Zmult_plus_distr_l.
    rewrite shr_shrink_u2Z_beta_40.
    rewrite shr_shrink_u2Z_beta_72.
    simpl acx; simpl hi; simpl lo.
    rewrite add_u2Z.
    rewrite zero_extend_u2Z.
    rewrite concat_u2Z'.
    rewrite concat_u2Z''.
    rewrite <-Zbeta_is_exp.
    simpl (1+1)%nat.
    repeat rewrite Zplus_assoc.
    auto.
    rewrite zero_extend_u2Z.
    rewrite concat_u2Z'.
    rewrite concat_u2Z''.
    repeat rewrite Zplus_assoc.
    generalize (max_u2Z_64 a); intro.
    rewrite Zmult_minus_distr_l in H.
    rewrite Zmult_1_r in H.
    generalize (Zpower_1 acx_size); intro.
    apply Zlt_le_trans with (u2Z a + Zbeta 2 * Zpower 2 acx_size - u2Z a).
    generalize (Zplus_lt_compat _ _ _ _ H0 H); intro.
    repeat rewrite Zplus_assoc in H2.
    ring ( u2Z a + Zbeta 2 * Zpower 2 acx_size - u2Z a ).
    generalize H2; clear H2.
    ring ( Zbeta 2 + (Zbeta 2 * Zpower 2 acx_size - Zbeta 2) ).
    intros.
    assumption.
    simpl.
    omega.
    rewrite <-Zbeta_is_exp.
    auto.
  Qed.

  (*
   * multu
   *)
  
  Definition multu_op (p:int (2 * 32)) (mult:m) : m :=
    let lo' := rem 32 p in
      let hi' := shr_shrink 32 p in 
	(Z2u acx_size 0, (hi', lo')).

  Lemma multu_utoZ: forall p m,
    utoZ (multu_op p m) = u2Z p.
    intros.
    destruct m0.
    destruct p0.
    unfold multu_op.
    unfold utoZ.
    unfold acx.
    rewrite Z2u_injection.
    simpl mult; simpl plus.
    rewrite Zbeta_power1.
    assert (2 * 32 >= 32)%nat.
    omega.
    generalize (shr_shrink_u2Z p H); intros.
    auto.
    generalize (Zpower_1 acx_size).
    intros.
    omega.
  Qed.
  
  (*
   * mflhxu
   *)

  Definition mflhxu_op m :=
    let (acx_reg, hi_reg) := (acx m, hi m) in
      (Z2u acx_size 0, (zero_extend 24 acx_reg, hi_reg)).

  Lemma mflhxu_utoZ : forall m,
    utoZ m = utoZ (mflhxu_op m) * Zbeta 1 + u2Z (lo m).
    intros.
    destruct m0 as [acx_reg].
    destruct p as [hi_reg lo_reg].
    simpl.
    unfold mflhxu_op.
    simpl.
    unfold utoZ.
    simpl.
    rewrite <-(@zero_extend_u2Z 24 acx_size acx_reg).
    generalize (Zbeta_is_exp 1 1).
    cutrewrite (1 + 1 = 2)%nat.
    generalize (Zbeta 1).
    generalize (Zbeta 2).
    intros.
    rewrite H.
    ring.
    rewrite Z2u_injection.
    ring.
    generalize (Zpower_1 acx_size); omega.
    auto.
  Qed.
  
  Lemma mflhxu_beta2_utoZ : forall (m0:multiplier.m),
    utoZ m0 < Zbeta 2 ->
    utoZ (mflhxu_op m0) < Zbeta 1.
    intros.
    destruct m0.
    destruct p.
    unfold mflhxu_op.
    simpl.
    generalize (utoZ_acx_beta2 _ H); intro.
    simpl in H0.
    rewrite H0.
    assert ( zero_extend 24 (Z2u acx_size 0) = Z2u 32 0).
    apply u2Z_injection.
    rewrite zero_extend_u2Z.
    rewrite Z2u_injection.
    rewrite Z2u_injection.
    auto.
    generalize (Zpower_1 32); omega.
    generalize (Zpower_1 acx_size); omega.
    unfold utoZ.
    simpl.
    rewrite H1.
    rewrite Z2u_injection.
    rewrite Z2u_injection.
    simpl.
    apply max_u2Z_32.
    generalize (Zpower_1 32); omega.
    generalize (Zpower_1 acx_size); omega.
  Qed.

  Lemma hi_mflhxu_op : forall (m0:m),
    u2Z (hi (mflhxu_op m0)) =
    u2Z (zero_extend (32 - acx_size) (acx m0)).
    intros.
    destruct m0.
    destruct p.
    simpl.
    reflexivity.
  Qed.

  Lemma lo_mflhxu_op : forall (m0:m), 
    lo (mflhxu_op m0) = hi m0.
    destruct m0.
    destruct p.
    auto.
  Qed.
  
  Lemma mflhxu_kbeta1_utoZ : forall (m0:m) k,
    utoZ m0 < Zbeta 1 * k ->
    utoZ (mflhxu_op m0) < k.
    destruct k.
    rewrite Zmult_0_r.
    intros.
    destruct m0.
    destruct p.
    rewrite utoZ_def in H.
    simpl in H.
    assert (u2Z i1 + u2Z i0 * Zbeta 1 + u2Z i * Zbeta 2 >= 0).
    generalize (min_u2Z i1); intro.
    assert ( 0 <= u2Z i0 * Zbeta 1 ).
    apply Zmult_le_0_compat.
    apply min_u2Z.
    generalize (Zbeta_1 1); omega.
    assert ( 0 <= u2Z i * Zbeta 2 ).
    apply Zmult_le_0_compat.
    apply min_u2Z.
    generalize (Zbeta_1 2); omega.
    omega.
    assert (~(u2Z i1 + u2Z i0 * Zbeta 1 + u2Z i * Zbeta 2 < 0)).
    omega.
    tauto.
    destruct m0.
    destruct p0.
    intros.
    rewrite mflhxu_utoZ.
    simpl.
    unfold mflhxu_op.
    simpl.
    rewrite utoZ_def.
    simpl.
    rewrite utoZ_def in H.
    simpl u2Z in H.
    rewrite (@zero_extend_u2Z 24 acx_size).
    rewrite (@zero_extend_u2Z 24 acx_size).
    rewrite Z2u_injection.
    simpl.
    assert (u2Z i0 * Zbeta 1 + u2Z i * Zbeta 2 < Zbeta 1 * Zpos p).
    generalize (min_u2Z i1); intro.
    omega.
    apply Zmult_gt_0_lt_reg_r with (Zbeta 1).
    generalize (Zbeta_1 1); intro.
    omega.
    do 2 rewrite Zplus_0_r.
    cutrewrite ( (u2Z i * Zbeta 1 + u2Z i0) * Zbeta 1 =
      u2Z i0 * Zbeta 1 + u2Z i * Zbeta 2 ).
    rewrite (Zmult_comm (Zpos p)).
    assumption.
    ring.
    rewrite <-Zbeta_is_exp.
    simpl plus.
    apply Zmult_comm.
    split.
    apply Zle_refl.
    generalize (Zpower_1 acx_size); intro.
    omega.
    (* if K < 0, we have a contradiction *)
    intros.
    generalize (utoZ_pos m0); intro.
    assert (Zbeta 1 * Zneg p < 0).
    simpl.
    apply Zlt_neg_0.
    assert (utoZ m0 < 0).
    omega.
    assert (~(0 <= utoZ m0)).
    omega.
    tauto.
  Qed.

  (*
   * msubu
   *)

  Definition msubu_op (p:int (2 * 32)) (mult:m) : m :=
    let acx_reg := acx mult in
      let hi_reg := hi mult in
	let lo_reg := lo mult in
	  let sum := (hi_reg ||| lo_reg) in
	    let new_sum := sub sum p in
	      let lo_reg' := rem 32 new_sum in
		let sum' := shr_shrink 32 new_sum in 
		  let hi_reg' := rem 32 sum' in
		      (acx_reg, (hi_reg', lo_reg')).

  Lemma msubu_utoZ : forall m a,
    utoZ m < Zbeta 2 ->
    utoZ m >= u2Z a ->
    utoZ (msubu_op a m) = utoZ m - u2Z a.
    intros.
    destruct m0 as [i0 p].
    destruct p as [i1 i2].
    unfold msubu_op.
    simpl.
    rewrite utoZ_def.
    simpl.
    rewrite utoZ_def.
    simpl.
    rewrite utoZ_def in H.
    simpl in H.
    rewrite utoZ_def in H0.
    simpl in H0.
    cut ( u2Z i0 = 0).
    intro.
    rewrite H1.
    simpl.
    rewrite Zplus_0_r.
    rewrite rem_u2Z; try omega.
    rewrite rem_u2Z; try omega.
    rewrite <-Zbeta_power1.
    rewrite Zmult_minus_distr_r.
    rewrite H1 in H0.
    rewrite H1 in H.
    simpl in H.
    simpl in H0.
    rewrite Zplus_0_r in H.
    rewrite Zplus_0_r in H0.
    rewrite (shr_shrink_overflow (shr_shrink 32 (sub (i1 ||| i2) a))).
    simpl.

    rewrite Z2u_injection.
    simpl.
    rewrite Zminus_0_r.
    rewrite sub_u2Z.
    rewrite concat_u2Z''.
    ring.

    rewrite concat_u2Z''.
    rewrite Zplus_comm.
    assumption.
    
    simpl.
    omega.
    simpl.
    constructor.

    assert (u2Z i0 = 0 \/ 0 < u2Z i0).
    generalize (min_u2Z i0); omega.
    inversion_clear H1; auto.
    assert (Zbeta 2 <= u2Z i0 * Zbeta 2).
    pattern (Zbeta 2) at 1.
    rewrite <-(Zmult_1_l (Zbeta 2)).
    apply Zmult_le_compat_r.
    omega.
    generalize (Zbeta_1 2); omega.
    assert (Zbeta 2 <= u2Z i2 + u2Z i1 * Zbeta 1 + u2Z i0 * Zbeta 2).
    apply Zle_trans with (u2Z i0 * Zbeta 2).
    auto.
    assert (0 <= u2Z i1 * Zbeta 1).
    apply Zmult_le_0_compat.
    apply min_u2Z.
    generalize (Zbeta_1 1); omega.
    generalize (min_u2Z i2); omega.
    omega.
  Qed.

  Lemma msubu_utoZ_overflow : forall m a,
    utoZ m < Zbeta 2 ->
    utoZ m < u2Z a ->
    utoZ (msubu_op a m) = Zbeta 2 + utoZ m - u2Z a.
    intros.
    destruct m0 as [i0 p].
    destruct p as [i1 i2].
    unfold msubu_op.
    simpl u2Z.
    rewrite utoZ_def.
    simpl u2Z.
    rewrite utoZ_def in H.
    simpl in H.
    rewrite utoZ_def in H0.
    simpl in H0.
    cut ( u2Z i0 = 0).
    intro.
    rewrite H1.
    rewrite Zmult_0_l.
    rewrite Zplus_0_r.
    rewrite rem_u2Z; try omega.
    rewrite rem_u2Z; try omega.
    rewrite <-Zbeta_power1.
    rewrite Zmult_minus_distr_r.
    rewrite H1 in H0.
    rewrite H1 in H.
    simpl in H.
    simpl in H0.
    rewrite Zplus_0_r in H.
    rewrite Zplus_0_r in H0.
    rewrite (shr_shrink_overflow (shr_shrink 32 (sub (i1 ||| i2) a))).
    simpl utoZ.
    rewrite Z2u_injection.
    rewrite Zmult_0_l.
    rewrite Zminus_0_r.

    rewrite sub_u2Z_overflow.
    rewrite concat_u2Z''.
    rewrite Zpower_64_Zbeta.
    rewrite utoZ_def.
    simpl u2Z.
    rewrite H1.
    rewrite Zmult_0_l.
    ring.
    
    rewrite concat_u2Z''.
    rewrite Zplus_comm.
    assumption.
    simpl.
    omega.
    
    simpl.
    constructor.
    
    assert (u2Z i0 = 0 \/ 0 < u2Z i0).
    generalize (min_u2Z i0); intro.
    omega.
    inversion_clear H1; auto.
    assert (Zbeta 2 <= u2Z i0 * Zbeta 2).
    pattern (Zbeta 2) at 1.
    rewrite <-(Zmult_1_l (Zbeta 2)).
    apply Zmult_le_compat_r.
    omega.
    generalize (Zbeta_1 2); omega.
    assert (Zbeta 2 <= u2Z i2 + u2Z i1 * Zbeta 1 + u2Z i0 * Zbeta 2).
    assert (0 <= (u2Z i1 * Zbeta 1)).
    apply Zmult_le_0_compat.
    apply min_u2Z.
    generalize (Zbeta_1 1); omega.
    apply Zle_trans with (u2Z i0 * Zbeta 2).
    auto.
    generalize (min_u2Z i2); omega.
    assert (~ (u2Z i2 + u2Z i1 * Zbeta 1 + u2Z i0 * Zbeta 2 < Zbeta 2)).
    omega.
  tauto.
  Qed.  

End multiplier.

Lemma utoZ_maddu_op : forall k (m0:multiplier.m) (p:int (2*32)),
  (k <= 64)%nat ->
  multiplier.utoZ m0 < Zpower 2 k ->
  u2Z p < Zpower 2 k ->
  multiplier.utoZ (multiplier.maddu_op p m0) < Zpower 2 (S k).
  intros.
  rewrite multiplier.maddu_utoZ.
  rewrite Zpower_S.
  omega.
  apply Zlt_le_trans with (Zbeta 2 * 1).
  rewrite Zmult_1_r.
  apply Zlt_le_trans with (Zpower 2 k).
  auto.
  rewrite <-Zpower_64_Zbeta.
  apply Zpower_2_le; omega.
  apply Zmult_le_compat_l.
  assert (Zpower 2 8 <= Zpower 2 multiplier.acx_size).
  apply Zpower_2_le.
  apply multiplier.acx_size_min.
  assert (2 <= 8)%nat.
  omega.
  generalize (Zpower_2_le _ _ H3); intro.
  simpl in H4.
  simpl in H2.
  omega.
  generalize (Zbeta_1 2); omega.
Qed.

Lemma lo_remainder_zero' : forall n k a b,
  0 <= a -> 0 <= b ->
  a < b ->
  a + n * b = k * b ->
  a = 0.
  intros.
  assert (n=k \/ n <> k).
  omega.
  inversion_clear H3.
  subst n.
  omega.
  assert (n<k \/ n>k).
  omega.
  inversion_clear H3.
  assert (a = k * b - n * b).
  omega.
  rewrite <-Zmult_minus_distr_r in H3.
  assert (k-n>=1).
  omega.
  assert (1*b<=a).
  rewrite H3.
  apply Zmult_le_compat_r.
  omega.
  omega.
  rewrite Zmult_1_l in H7.
  omega.
  assert (a = k * b - n * b).
  omega.
  rewrite <-Zmult_minus_distr_r in H3.
  assert (k-n<0).
  omega.
  assert (b=0 \/ 0 < b).
  omega.
  inversion_clear H7.
  subst b.
  rewrite Zmult_0_r in H3.
  auto.
  assert ( (k - n) * b < 0 ).
  rewrite Zmult_minus_distr_r.
  assert (k * b < n * b).
  apply Zmult_lt_compat_r.
  auto.
  omega.
  omega.
  rewrite <-H3 in H7.
  omega.
Qed.

Lemma lo_remainder_zero : forall (m0:multiplier.m),
  (exists K, multiplier.utoZ m0 = K * Zbeta 1) ->
  multiplier.lo m0 = zero32.
  intros.
  inversion_clear H as [K].
  rewrite multiplier.utoZ_def in H0.
  apply u2Z_injection.
  unfold zero32.
  rewrite Z2u_injection.
  assert ( u2Z (multiplier.lo m0) < Zbeta 1).
  apply max_u2Z_32.
  assert (Zbeta 2 = Zbeta 1 * Zbeta 1).
  rewrite <-Zbeta_is_exp.
  auto.
  rewrite H1 in H0; clear H1.
  rewrite <-Zplus_assoc in H0.
  assert ( u2Z (multiplier.hi m0) * Zbeta 1 + u2Z (multiplier.acx m0) * (Zbeta 1 * Zbeta 1) =
    Zbeta 1 * ( u2Z (multiplier.hi m0) + u2Z (multiplier.acx m0) * Zbeta 1 ) ).
  ring.
  rewrite H1 in H0; clear H1.
  generalize H0; clear H0; generalize (u2Z (multiplier.hi m0) + u2Z (multiplier.acx m0) * Zbeta 1); intros.
  eapply lo_remainder_zero' with (b:=Zbeta 1) (n:=z).
  apply min_u2Z.
  generalize (Zbeta_1 1); omega.
  assumption.
  rewrite Zmult_comm.
  apply H0.
  generalize (Zpower_1 32); omega.
Qed.