Require Import ZArith.
Require Import List.
Require Import util.
Require Import util_tactic.
Require Import machine_int.
Import MachineInt.
Require Import machine_int_spec.
Require Import sum.
Require Import state.
Require Import mips.
Require Import mips_tactics.
Require Import mips_contrib.
Require Import mapstos.

Open Local Scope asm_heap_scope.
Open Local Scope mips_scope.
Open Local Scope Z_scope.

(*****************************************************************************)

Definition k := gpr_s0. (* length of multi-precision integers *)
Definition one := gpr_s1. (* the value "1" *)
Definition a := gpr_a0. (* arguments *)
Definition b := gpr_a1.
Definition c := gpr_a2.
Definition z := gpr_t0. (* pointer for sw *)
Definition t := gpr_t1. (* initial value of z *)
Definition i := gpr_t2. (* counter for "a" *)
Definition j := gpr_t3. (* counter for "b" *)
Definition l := gpr_t4. (* counter for "c" *)
Definition atmp := gpr_t5. (* local variables *)
Definition btmp := gpr_t6. 
Definition ctmp := gpr_t7.
  
Definition multimul :=
  addiu i gpr_zero zero16;
  addiu t c zero16;
  while_bne i k (
    addiu z t zero16;
    lwxs atmp i a;
    addiu j gpr_zero zero16;
    while_bne j k (
      lwxs btmp j b;
      maddu atmp btmp;
      addu l i j;
      lwxs ctmp l c;
      maddu ctmp one;
      mflhxu ctmp;
      sw ctmp zero16 z;
      addiu z z four16;
      addiu j j one16
    );
    mflhxu ctmp;
    sw ctmp zero16 z;
    addiu t t four16;
    addiu i i one16
  ).

Lemma multimul_specif : forall nk na nb nc 
  (Hk:(O < nk)%nat) 
  (Hna:4*na + 4*Z_of_nat nk < Zbeta 1) (Hnb:4*nb + 4*Z_of_nat nk < Zbeta 1) (Hnc:4*nc + 8*Z_of_nat nk < Zbeta 1)
  va vb vc (Hva: u2Z va = 4 * na) (Hvb: u2Z vb = 4 * nb) (Hvc: u2Z vc = 4 * nc)
  A B (Ha: length A = nk) (Hb: length B = nk), 
  {{ fun s s' m h => exists C, length C = (nk+nk)%nat /\
     gpr.lookup one s = one32 /\
     gpr.lookup a s = va /\ gpr.lookup b s = vb /\ gpr.lookup c s = vc /\
     u2Z (gpr.lookup k s) = Z_of_nat nk /\
     ((var_e a |--> A) ** (var_e b |--> B) ** (var_e c |--> C)) s s' m h /\
     multiplier.is_null m /\ list_of_zeros C }}
  
  multimul

  {{ fun s s' m h => exists C, length C = (nk+nk)%nat /\
     ((var_e c |--> C) ** TT) s s' m h /\ 
     Sum (nk+nk) C = Sum nk A * Sum nk B }}.

intros.
unfold multimul.

  apply semax_addiu'' with (fun s s' m h => exists C,
    length C = (nk+nk)%nat /\
    gpr.lookup one s = one32 /\
    gpr.lookup a s = va /\
    gpr.lookup b s = vb /\
    gpr.lookup c s = vc /\
    u2Z (gpr.lookup k s) = Z_of_nat nk /\
    (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\ 
    multiplier.is_null m /\ list_of_zeros C /\
    gpr.lookup i s = zero32
  ).

  red; intros.
  red.
  inversion_clear H as [C].
  decompose [and] H0; clear H0.
  exists C.
  split; trivial.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_update_store.
  split; trivial.
  split; trivial.
  unfold zero16.
  rewrite sign_extend_16_32'.
  rewrite add_neutral.
  rewrite gpr.gpr_zero_zero32.
  reflexivity.
  Constraint.

  apply semax_addiu'' with (fun s s' m h => exists C,
    length C = (nk+nk)%nat /\
    gpr.lookup one s = one32 /\
    gpr.lookup a s = va /\
    gpr.lookup b s = vb /\
    gpr.lookup c s = vc /\
    u2Z (gpr.lookup k s) = Z_of_nat nk /\
    (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\ 
    multiplier.is_null m /\ list_of_zeros C /\
    gpr.lookup i s = zero32 /\
    u2Z (gpr.lookup t s) = 4 * nc 
  ).

  red; intros.
  red.
  inversion_clear H as [C].
  decompose [and] H0; clear H0.
  exists C.
  split; trivial.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  elim gpr.lookup_update; try var.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_update_store.
  split; trivial.
  split; trivial.
  split; trivial.
  unfold zero16.
  rewrite sign_extend_16_32'.
  rewrite add_neutral.
  rewrite H4.
  assumption.
  Constraint.

  apply semax_strengthen_pre with (fun s s' m h =>
    exists C, exists ni,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      ((var_e a |--> A) ** (var_e b |--> B) ** (var_e c |--> C)) s s' m h /\ 
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      (ni <= nk)%nat /\
      multiplier.is_null m /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      Sum (ni + nk) C = Sum ni A * Sum nk B
  ).
  
  red; intros.
  inversion_clear H as [C].
  decompose [and] H0; clear H0.
  exists C; exists O.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  rewrite H9.
  Rewrite_u2Z.
  reflexivity.
  Constraint.
  split.
  apply le_O_n.
  split; trivial.
  split.
  rewrite H11.
  ring.
  simpl.
  apply Sum_list_of_zeros; auto.

apply semax_weaken_post with (fun s s' m h =>
  (exists C, exists ni, 
    length C = (nk+nk)%nat /\
    gpr.lookup one s = one32 /\
    gpr.lookup a s = va /\
    gpr.lookup b s = vb /\
    gpr.lookup c s = vc /\
    u2Z (gpr.lookup k s) = Z_of_nat nk /\
    (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\ 
    u2Z (gpr.lookup i s) = Z_of_nat ni /\
    (ni <= nk)%nat /\
    multiplier.is_null m /\
    u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
    Sum (ni+nk) C = Sum ni A * Sum nk B)
  /\
  u2Z (gpr.lookup i s) = u2Z (gpr.lookup k s)
).

red; intros.
inversion_clear H.
inversion_clear H0 as [C].
inversion_clear H as [ni].
decompose [and] H0; clear H0.
exists C.
split; trivial.
split.
apply my_sep_trivial with ((var_e a |--> A) ** (var_e b |--> B)).
assoc_comm H7.
assert (ni=nk).
apply Z_of_nat_inj.
rewrite <-H6; rewrite <-H8; assumption.
subst ni.
assumption.

apply semax_while_bne with (P:=fun s s' m h =>
  exists C, exists ni,
    length C = (nk+nk)%nat /\
    gpr.lookup one s = one32 /\
    gpr.lookup a s = va /\
    gpr.lookup b s = vb /\
    gpr.lookup c s = vc /\
    u2Z (gpr.lookup k s) = Z_of_nat nk /\
    (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\ 
    u2Z (gpr.lookup i s) = Z_of_nat ni /\
    (ni <= nk)%nat /\
    multiplier.is_null m /\
    u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
    Sum (ni+nk) C = Sum ni A * Sum nk B).

  apply semax_addiu'' with (fun s s' m h =>
    exists C, exists ni,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      (ni < nk)%nat /\
      multiplier.is_null m /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      Sum (ni + nk) C = Sum ni A * Sum nk B /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s)).

  red; intros.
  inversion_clear H.
  inversion_clear H0 as [C].
  inversion_clear H as [ni].
  decompose [and] H0; clear H0.
  red.
  exists C; exists ni.
  split; trivial.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  elim gpr.lookup_update; try var.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_update_store.
  split; trivial.
  split.
  omega.
  split; trivial.
  split; trivial.
  split; trivial.
  Rewrite_u2Z.
  ring.
  Constraint.
  Constraint.
  Constraint.

  apply semax_lwxs_backwards'' with (fun s s' m h =>
    exists C, exists ni,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      (ni < nk)%nat /\
      multiplier.is_null m /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      Sum (ni + nk) C = Sum ni A * Sum nk B /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s) /\
      gpr.lookup atmp s = nth ni A zero32
  ).

  red; intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  decompose [and] H; clear H.
  exists (nth ni A zero32).
  
  assert (Htmp : u2Z (eval (var_e a) s) + 4 * Z_of_nat nk < Zbeta 1 /\
    eval (add_e (var_e a) (shl2_e (var_e i))) s =
    eval (add_e (var_e a) (shl2_e (int_e (Z2u 32 (Z_of_nat ni))))) s /\
    eval (add_e (add_e (var_e a) (shl2_e (var_e i))) (int_e four32)) s =
    eval (add_e (add_e (var_e a) (shl2_e (var_e i))) (int_e four32)) s).
  simpl eval.
  rewrite H1.
  split.
  Constraint.
  split.
  cutrewrite ( gpr.lookup i s = Z2u 32 (Z_of_nat ni) ).
  reflexivity.
  apply u2Z_injection.
  rewrite H7.
  rewrite Z2u_injection.
  reflexivity.
  generalize (min_u2Z va); intro.
  Constraint.
  reflexivity.

  Decompose_list_32 A ni A1 A2.
  lapply (mapstos_decompose_generic_P _ _ _ _ _ _ 
    (var_e a) (add_e (var_e a) (shl2_e (var_e i))) (add_e (add_e (var_e a) (shl2_e (var_e i))) (int_e four32)) 
    s ((var_e b |--> B) ** (var_e c |--> C)) Ha H14 H s' m h).
  intro.
  assert ( (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C))
    s s' m h -> ((var_e a |--> A) ** ((var_e b |--> B) ** (var_e c |--> C)))
    s s' m h).
  intro.
  assoc_comm H15.
  generalize (H12 (H15 H6)); clear H15 H12; intro.
  simpl app in H12.
  Monotony H12.
  Adjunction H12.

  red.
  exists C; exists ni.
  split; trivial.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_update_store.

  assoc_comm H12.
  eapply mapstos_compose_generic with (e':=add_e (var_e a) (shl2_e (var_e i)))
    (e'':=(add_e (add_e (var_e a) (shl2_e (var_e i))) (int_e four32))).
  apply Ha.
  apply H14.
  simpl.
  apply H.
  exact Htmp.
  assoc_comm H12.

  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  exact Htmp.

  omega.

  apply semax_addiu'' with (fun s s' m h =>
    exists C, exists ni,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      (ni < nk)%nat /\
      multiplier.is_null m /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      Sum (ni + nk) C = Sum ni A * Sum nk B /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s) /\
      gpr.lookup atmp s = nth ni A zero32 /\
      gpr.lookup j s = zero32
  ).

  red; intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  decompose [and] H; clear H.
  red.
  exists C; exists ni.
  split; trivial.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_update_store.
  split; trivial.
  split; trivial. 
  split; trivial. 
  split; trivial. 
  split; trivial. 
  split; trivial. 
  split; trivial. 
  unfold zero16.
  rewrite sign_extend_16_32'.
  rewrite add_neutral.
  rewrite gpr.gpr_zero_zero32.
  reflexivity.
  Constraint.

  apply semax_strengthen_pre with (fun s s' m h =>
    exists C, exists ni, exists nj,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      u2Z (gpr.lookup j s) = Z_of_nat nj /\
      (ni < nk)%nat /\
      (nj <= nk)%nat /\
      multiplier.utoZ m < Zbeta 1 /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s) + 4 * Z_of_nat nj /\
      gpr.lookup atmp s = nth ni A zero32 /\
      Sum (ni + nk) C + u2Z (multiplier.lo m) * Zbeta (ni + nj) = 
      Sum ni A * Sum nk B + Sum nj B * u2Z (nth ni A zero32) * Zbeta ni
  ).
  
  red; intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  decompose [and] H; clear H.
  exists C; exists ni; exists O.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  rewrite H15.
  Rewrite_u2Z.
  reflexivity.
  Constraint.
  split; trivial.
  split.
  apply le_O_n.
  split.
  rewrite multiplier.is_null_utoZ.
  Constraint.
  assumption.
  split; trivial.
  split.
  rewrite H12.
  ring.
  split; trivial.
  simpl.
  rewrite multiplier.is_null_lo.
  rewrite Z2u_injection.
  ring.
  rewrite H11; ring.
  Constraint.
  assumption.
  
  apply semax_seq with (fun s s' m h =>
    (exists C, exists ni, exists nj,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      u2Z (gpr.lookup j s) = Z_of_nat nj /\
      (ni < nk)%nat /\
      (nj <= nk)%nat /\
      multiplier.utoZ m < Zbeta 1 /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s) + 4 * Z_of_nat nj /\
      gpr.lookup atmp s = nth ni A zero32 /\
      Sum (ni + nk) C + u2Z (multiplier.lo m) * Zbeta (ni + nj) = 
      Sum ni A * Sum nk B + Sum nj B * u2Z (nth ni A zero32) * Zbeta ni) /\
    u2Z (gpr.lookup j s) = u2Z (gpr.lookup k s)
  ).
  
  apply semax_while_bne with (P:=fun s s' m h =>
    (exists C, exists ni, exists nj,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      u2Z (gpr.lookup j s) = Z_of_nat nj /\
      (ni < nk)%nat /\
      (nj <= nk)%nat /\
      multiplier.utoZ m < Zbeta 1 /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s) + 4 * Z_of_nat nj /\
      gpr.lookup atmp s = nth ni A zero32 /\
      Sum (ni + nk) C + u2Z (multiplier.lo m) * Zbeta (ni + nj) = 
      Sum ni A * Sum nk B + Sum nj B * u2Z (nth ni A zero32) * Zbeta ni)).
  
  apply semax_lwxs_backwards'' with (fun s s' m h =>
    exists C, exists ni, exists nj,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      u2Z (gpr.lookup j s) = Z_of_nat nj /\
      (ni < nk)%nat /\
      (nj < nk)%nat /\
      multiplier.utoZ m < Zbeta 1 /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s) + 4 * Z_of_nat nj /\
      gpr.lookup atmp s = nth ni A zero32 /\
      Sum (ni + nk) C + u2Z (multiplier.lo m) * Zbeta (ni + nj) = 
      Sum ni A * Sum nk B + Sum nj B * u2Z (nth ni A zero32) * Zbeta ni /\
      gpr.lookup btmp s = nth nj B zero32
  ).

  red; intros.
  inversion_clear H.
  inversion_clear H0 as [C].
  inversion_clear H as [ni].
  inversion_clear H0 as [nj].
  decompose [and] H; clear H.
  exists (nth nj B zero32).
  
  assert (Htmp : u2Z (eval (var_e b) s) + 4 * Z_of_nat nk < Zbeta 1 /\
    eval (add_e (var_e b) (shl2_e (var_e j))) s =
    eval (add_e (var_e b) (shl2_e (int_e (Z2u 32 (Z_of_nat nj))))) s /\
    eval (add_e (add_e (var_e b) (shl2_e (var_e j))) (int_e four32)) s =
    eval (add_e (add_e (var_e b) (shl2_e (var_e j))) (int_e four32)) s).
  simpl eval.
  rewrite H4.
  split.
  Constraint.
  split.
  cutrewrite ( gpr.lookup j s = Z2u 32 (Z_of_nat nj) ).
  reflexivity.
  apply u2Z_injection.
  rewrite H9.
  rewrite Z2u_injection.
  reflexivity.
  generalize (min_u2Z va); intro.
  Constraint.
  reflexivity.

  Decompose_list_32 B nj B1 B2.
  lapply (mapstos_decompose_generic_P _ _ _ _ _ _ 
    (var_e b) (add_e (var_e b) (shl2_e (var_e j))) (add_e (add_e (var_e b) (shl2_e (var_e j))) (int_e four32)) 
    s ((var_e a |--> A) ** (var_e c |--> C)) Hb H18 H s' m h).
  intro.
  assert ( (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C))
    s s' m h -> ((var_e b |--> B) ** ((var_e a |--> A) ** (var_e c |--> C)))
    s s' m h).
  intro.
  assoc_comm H19.
  generalize (H16 (H19 H7)); clear H16 H19; intro.
  simpl app in H16.
  Monotony H16.
  Adjunction H16.

  red.
  exists C; exists ni; exists nj.
  split; trivial.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_update_store.

  assoc_comm H16.

  eapply mapstos_compose_generic with (e':=add_e (var_e b) (shl2_e (var_e j)))
    (e'':=(add_e (add_e (var_e b) (shl2_e (var_e j))) (int_e four32))).
  apply Hb.
  apply H18.
  simpl.
  apply H.
  exact Htmp.
  assoc_comm H16.

  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  omega.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  exact Htmp.

  omega.

  apply semax_maddu'' with (fun s s' m h =>
    exists C, exists ni, exists nj,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      u2Z (gpr.lookup j s) = Z_of_nat nj /\
      (ni < nk)%nat /\
      (nj < nk)%nat /\
      multiplier.utoZ m < Zbeta 2 - Zbeta 1 + 1  /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s) + 4 * Z_of_nat nj /\
      gpr.lookup atmp s = nth ni A zero32 /\
      Sum (ni + nk) C + multiplier.utoZ m * Zbeta (ni + nj) = 
      Sum ni A * Sum nk B + Sum nj B * u2Z (nth ni A zero32) * Zbeta ni + 
      u2Z (nth ni A zero32) * u2Z (nth nj B zero32) * Zbeta (ni + nj) /\
      gpr.lookup btmp s = nth nj B zero32).
  
  intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  inversion_clear H as [nj].
  decompose [and] H0; clear H0.
  exists C; exists ni; exists nj.

  assert ( Htmp : multiplier.utoZ m < Zbeta 2 * (2 ^^ multiplier.acx_size - 1)).
  apply Zlt_le_trans with (Zbeta 1).
  assumption.
  apply Zle_trans with (Zbeta 2 * (Zpower 2 8 - 1)).
  unfold Zbeta.
  simpl.
  Constraint.
  apply Zmult_le_compat_l.
  apply Zminus_le_compat.
  apply Zpower_2_le.
  apply multiplier.acx_size_min.
  Constraint.

  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_mult_maddu.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  rewrite multiplier.maddu_utoZ.
  apply Zlt_le_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1) + Zbeta 1).
  apply Zplus_le_lt_compat.
  apply max_u2Z_umul_32.
  assumption.
  unfold Zbeta.
  simpl.
  apply Zle_refl.
  exact Htmp.

  split; trivial.
  split; trivial.
  split; trivial.
  split.
  rewrite multiplier.maddu_utoZ.
  rewrite H17; rewrite H14.
  rewrite umul_u2Z_32.
  cutrewrite ( multiplier.utoZ m = u2Z (multiplier.lo m) ).
  ring.
  apply trans_eq with (Sum (ni + nk) C + u2Z (multiplier.lo m) * Zbeta (ni + nj)).
  ring.
  rewrite H15.
  ring.
  generalize (multiplier.utoZ_lo_beta1 _ H11); intro.
  tauto.
  exact Htmp.

  assumption.

  apply semax_addu'' with (fun s s' m h =>
    exists C, exists ni, exists nj,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      u2Z (gpr.lookup j s) = Z_of_nat nj /\
      (ni < nk)%nat /\
      (nj < nk)%nat /\
      multiplier.utoZ m < Zbeta 2 - Zbeta 1 + 1 /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s) + 4 * Z_of_nat nj /\
      gpr.lookup atmp s = nth ni A zero32 /\
      Sum (ni + nk) C + multiplier.utoZ m * Zbeta (ni + nj) = 
      Sum ni A * Sum nk B + Sum nj B * u2Z (nth ni A zero32) * Zbeta ni + 
      u2Z (nth ni A zero32) * u2Z (nth nj B zero32) * Zbeta (ni + nj) /\
      gpr.lookup btmp s = nth nj B zero32 /\
      gpr.lookup l s = gpr.lookup i s (+) gpr.lookup j s
  ).

  red; intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  inversion_clear H as [nj].
  decompose [and] H0; clear H0.
  red.
  exists C; exists ni; exists nj.
  split; trivial.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_update_store.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.

  apply semax_lwxs_backwards'' with (fun s s' m h =>
    exists C, exists ni, exists nj,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      u2Z (gpr.lookup j s) = Z_of_nat nj /\
      (ni < nk)%nat /\
      (nj < nk)%nat /\
      multiplier.utoZ m < Zbeta 2 - Zbeta 1 + 1 /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s) + 4 * Z_of_nat nj /\
      gpr.lookup atmp s = nth ni A zero32 /\
      Sum (ni + nk) C + multiplier.utoZ m * Zbeta (ni + nj) = 
      Sum ni A * Sum nk B + Sum nj B * u2Z (nth ni A zero32) * Zbeta ni + 
      u2Z (nth ni A zero32) * u2Z (nth nj B zero32) * Zbeta (ni + nj) /\
      gpr.lookup btmp s = nth nj B zero32 /\
      gpr.lookup l s = gpr.lookup i s (+) gpr.lookup j s /\
      gpr.lookup ctmp s = nth (ni+nj) C zero32
  ).

  red; intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  inversion_clear H as [nj].
  decompose [and] H0; clear H0.
  exists (nth (ni+nj) C zero32).
  
  assert (Htmp :  u2Z (eval (var_e c) s) + 4 * Z_of_nat (nk + nk) < Zbeta 1 /\
    eval (add_e (var_e c) (shl2_e (var_e l))) s =
    eval (add_e (var_e c) (shl2_e (int_e (Z2u 32 (Z_of_nat (ni + nj)))))) s /\
    eval (add_e (add_e (var_e c) (shl2_e (var_e l))) (int_e four32)) s =
    eval (add_e (add_e (var_e c) (shl2_e (var_e l))) (int_e four32)) s ).
  simpl eval.
  rewrite H4.
  split.
  rewrite inj_plus.
  Constraint.
  split.
  cutrewrite ( gpr.lookup l s = Z2u 32 (Z_of_nat (ni+nj)) ).
  reflexivity.
  apply u2Z_injection.
  rewrite H18.
  Rewrite_u2Z.
  rewrite inj_plus.
  omega.
  rewrite inj_plus.
  (*TODO: Constraint fails here*)
  split.
  omega.
  Clean_beta1.
  generalize (min_u2Z va); intro.
  omega.
  rewrite H7; rewrite H8.
  Clean_beta1.
  generalize (min_u2Z va); intro.
  omega.
  reflexivity.

  Decompose_list_32 C (ni+nj)%nat lst1 lst2.
  lapply (mapstos_decompose_generic_P _ _ _ _ _ _ 
    (var_e c) (add_e (var_e c) (shl2_e (var_e l))) (add_e (add_e (var_e c) (shl2_e (var_e l))) (int_e four32)) 
    s ((var_e a |--> A) ** (var_e b |--> B)) H H19 H0 s' m h).
  intro.
  assert ( (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C))
    s s' m h -> ((var_e c |--> C) ** ((var_e a |--> A) ** (var_e b |--> B)))
    s s' m h).
  intro.
  assoc_comm H20.
  generalize (H17 (H20 H6)); clear H17 H20; intro.
  simpl app in H17.
  Monotony H17.
  Adjunction H17.

  red.
  exists C; exists ni; exists nj.
  split; trivial.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_update_store.

  assoc_comm H17.
  eapply mapstos_compose_generic with (e':=add_e (var_e c) (shl2_e (var_e l)))
    (e'':=(add_e (add_e (var_e c) (shl2_e (var_e l))) (int_e four32))).
  apply H.
  apply H19.
  simpl.
  apply H0.
  exact Htmp.
  assoc_comm H17.

  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  exact Htmp.
  
  omega.

  apply semax_maddu'' with (fun s s' m h =>
    exists C, exists ni, exists nj,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      u2Z (gpr.lookup j s) = Z_of_nat nj /\
      (ni < nk)%nat /\
      (nj < nk)%nat /\
      multiplier.utoZ m < Zbeta 2 /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s) + 4 * Z_of_nat nj /\
      gpr.lookup atmp s = nth ni A zero32 /\
      Sum (ni + nk) C + multiplier.utoZ m * Zbeta (ni + nj) = 
      Sum ni A * Sum nk B + Sum nj B * u2Z (nth ni A zero32) * Zbeta ni + 
      u2Z (nth ni A zero32) * u2Z (nth nj B zero32) * Zbeta (ni + nj) +
      u2Z (nth (ni+nj) C zero32) * Zbeta (ni + nj) /\
      gpr.lookup btmp s = nth nj B zero32 /\
      gpr.lookup l s = gpr.lookup i s (+) gpr.lookup j s /\
      gpr.lookup ctmp s = nth (ni+nj) C zero32
  ).
  
  intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  inversion_clear H as [nj].
  decompose [and] H0; clear H0.
  exists C; exists ni; exists nj.

  assert (Htmp : multiplier.utoZ m < Zbeta 2 * (2 ^^ multiplier.acx_size - 1)).
  apply Zlt_le_trans with (Zbeta 2 - Zbeta 1 + 1).
  assumption.
  apply Zle_trans with (Zbeta 2 * (Zpower 2 8 - 1)).
  unfold Zbeta.
  simpl.
  Constraint_constant.
  apply Zmult_le_compat_l.
  apply Zminus_le_compat.
  apply Zpower_2_le.
  apply multiplier.acx_size_min.
  Constraint_constant.

  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_mult_maddu.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  rewrite multiplier.maddu_utoZ.
  rewrite H2.
  unfold one32.
  rewrite umul_1.
  rewrite zero_extend_u2Z_32.
  apply Zlt_le_trans with ((Zbeta 1 - 1) + (Zbeta 2 - Zbeta 1 + 1)).
  apply Zplus_le_lt_compat.
  apply max_u2Z_32'.
  assumption.
  unfold Zbeta.
  simpl.
  apply Zle_refl.

  exact Htmp.

  split; trivial.
  split; trivial.
  split; trivial.
  split.
  rewrite multiplier.maddu_utoZ.
  rewrite H2.
  unfold one32.
  rewrite umul_1.
  rewrite zero_extend_u2Z_32.
  rewrite H19.
  apply trans_eq with (Sum (ni + nk) C + multiplier.utoZ m * Zbeta (ni + nj) 
    + u2Z (nth (ni + nj) C zero32) * Zbeta (ni + nj) ).
  ring.
  rewrite H15.
  ring.
  exact Htmp.
  
  split; trivial.
  split; trivial.

  apply semax_mflhxu'' with (fun s s' m h =>
    exists C, exists ni, exists nj,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      u2Z (gpr.lookup j s) = Z_of_nat nj /\
      (ni < nk)%nat /\
      (nj < nk)%nat /\
      multiplier.utoZ m < Zbeta 1 /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s) + 4 * Z_of_nat nj /\
      gpr.lookup atmp s = nth ni A zero32 /\
      Sum (ni + nk) C + multiplier.utoZ m * Zbeta (ni + nj + 1) + u2Z (gpr.lookup ctmp s) * Zbeta (ni + nj) = 
      Sum ni A * Sum nk B + Sum nj B * u2Z (nth ni A zero32) * Zbeta ni + 
      u2Z (nth ni A zero32) * u2Z (nth nj B zero32) * Zbeta (ni + nj) +
      u2Z (nth (ni+nj) C zero32) * Zbeta (ni + nj) /\
      gpr.lookup btmp s = nth nj B zero32 /\
      gpr.lookup l s = gpr.lookup i s (+) gpr.lookup j s
  ).

  red; intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  inversion_clear H as [nj].
  decompose [and] H0; clear H0.
  red.
  exists C; exists ni; exists nj.
  split; trivial.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_mult_mflhxu_op.
  Inde_update_store.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  apply multiplier.mflhxu_beta2_utoZ.
  assumption.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  generalize (multiplier.mflhxu_utoZ m); intro.
  rewrite H0 in H15.
  apply trans_eq with (Sum (ni + nk) C +
        (multiplier.utoZ (multiplier.mflhxu_op m) * Zbeta 1 +
         u2Z (multiplier.lo m)) * Zbeta (ni + nj)).
  rewrite Zbeta_is_exp.
  ring.
  rewrite H15.
  ring.
  split; trivial.

  apply semax_sw_backwards'' with (fun s s' m h =>
    exists C, exists ni, exists nj,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      u2Z (gpr.lookup j s) = Z_of_nat nj /\
      (ni < nk)%nat /\
      (nj < nk)%nat /\
      multiplier.utoZ m < Zbeta 1 /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s) + 4 * Z_of_nat nj /\
      gpr.lookup atmp s = nth ni A zero32 /\
      Sum (ni + nk) C + multiplier.utoZ m * Zbeta (ni + nj + 1) = 
      Sum ni A * Sum nk B + Sum nj B * u2Z (nth ni A zero32) * Zbeta ni + 
      u2Z (nth ni A zero32) * u2Z (nth nj B zero32) * Zbeta (ni + nj)  /\
      gpr.lookup btmp s = nth nj B zero32 /\
      gpr.lookup l s = gpr.lookup i s (+) gpr.lookup j s
  ).
  
  red; intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  inversion_clear H as [nj].
  decompose [and] H0; clear H0.
  exists (int_e (nth (ni+nj) C zero32)).

  assert (Htmp : u2Z (eval (var_e c) s) + 4 * Z_of_nat (nk + nk) < Zbeta 1 /\
    eval (add_e (var_e z) (int_e (sign_extend_16_32 zero16))) s =
    eval (add_e (var_e c) (shl2_e (int_e (Z2u 32 (Z_of_nat (ni + nj)))))) s /\
    eval (add_e (add_e (var_e z) (int_e (sign_extend_16_32 zero16))) (int_e four32)) s =
    eval (add_e (add_e (var_e z) (int_e (sign_extend_16_32 zero16))) (int_e four32)) s ).
  generalize (min_u2Z va); intro.
  generalize (min_u2Z vc); intro.
  simpl eval.
  rewrite H4.
  split.
  rewrite inj_plus.
  Constraint.
  split.
  unfold zero16.
  unfold sign_extend_16_32.
  rewrite sign_extend_Z2u.
  simpl plus.
  rewrite add_neutral.
  apply u2Z_injection.
  rewrite H13.
  rewrite H12.
  symmetry.
  Rewrite_u2Z.
  rewrite inj_plus.
  rewrite Hvc.
  ring.
  rewrite inj_plus.
  (*TODO: constraint does not work here*)
  split.
  omega.
  Clean_beta1.
  omega.
  rewrite inj_plus.
  Clean_beta1.
  Mult 2%nat.
  omega.
  omega.
  rewrite inj_plus.
  Clean_beta1.
  omega.
  rewrite inj_plus.
  Clean_beta1.
  omega.
  split.
  omega.
  rewrite inj_plus.
  Clean_beta1.
  omega.
  rewrite inj_plus.
  Clean_beta1.
  Mult 2%nat.
  omega.
  Clean_beta1.
  omega.
  rewrite inj_plus.
  split.
  omega.
  Clean_beta1.
  omega.
  repeat constructor.
  Constraint.
  reflexivity.

  Decompose_list_32 C (ni+nj)%nat lst1 lst2.
  lapply (mapstos_decompose_generic_P _ _ _ _ _ _ 
    (var_e c) 
    (add_e (var_e z) (int_e (sign_extend_16_32 zero16))) 
    (add_e (add_e (var_e z) (int_e (sign_extend_16_32 zero16))) (int_e four32)) 
    s 
    ((var_e b |--> B) ** (var_e a |--> A)) 
    H H19 H0 s' m h).
  intro.
  assert ( (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h ->
    ((var_e c |--> C) ** ((var_e b |--> B) ** (var_e a |--> A))) s s' m h ).
  intro.
  assoc_comm H20.
  generalize (H17 (H20 H6)); clear H17 H20; intro.
  simpl app in H17.
  Monotony H17.
  Adjunction H17.

  exists (update_list C (ni+nj) (gpr.lookup ctmp s)).
  exists ni.
  exists nj.
  split.
  apply length_update_list; auto.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.

  assoc_comm H17.
  eapply mapstos_compose_generic with (lst2:=lst2) (w:=gpr.lookup ctmp s)
    (e':=add_e (var_e z) (int_e (sign_extend_16_32 zero16)))
    (e'':=add_e (add_e (var_e z) (int_e (sign_extend_16_32 zero16))) (int_e four32)).
  apply length_update_list.
  apply H.
  apply H19.
  rewrite H0.
  rewrite update_list_app.
  simpl.
  rewrite H19.
  rewrite <-minus_n_n.
  reflexivity.
  rewrite H19.
  constructor.
  exact Htmp.

  assoc_comm H17.
  generalize H17; clear H17.
  apply mapsto_ext'.
  reflexivity.
  simpl.
  reflexivity.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  
  lapply (list_split2 _ C (ni+nk)).
  intro.
  inversion_clear H20 as [l1].
  inversion_clear H21 as [l2].
  inversion_clear H20.
  rewrite H22.
  rewrite update_list_app'.
  rewrite <-Sum_beyond.
  rewrite H22 in H15.
  rewrite <-Sum_beyond in H15.
  
  rewrite <-Sum_update_list2.
  
  apply trans_eq with (
    (Sum (ni + nk) l1 + multiplier.utoZ m * Zbeta (ni + nj + 1) +
      u2Z (gpr.lookup ctmp s) * Zbeta (ni + nj)) 
    - u2Z (nth (ni + nj) l1 zero32) * Zbeta (ni + nj)
  ).
  ring.
  rewrite H15.
  rewrite <-nth_beyond.
  ring.
  rewrite H21.
  omega.
  assumption.
  omega.
  assumption.
  apply length_update_list.
  assumption.
  rewrite H21.
  omega.
  rewrite H.
  omega.

  split; trivial.

  exact Htmp.

  omega.
  
  apply semax_addiu'' with (fun s s' m h =>
    exists C, exists ni, exists nj,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      u2Z (gpr.lookup j s) = Z_of_nat nj /\
      (ni < nk)%nat /\
      (nj < nk)%nat /\
      multiplier.utoZ m < Zbeta 1 /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      u2Z (gpr.lookup z s) = u2Z (gpr.lookup t s) + 4 * (Z_of_nat nj + 1) /\
      gpr.lookup atmp s = nth ni A zero32 /\
      Sum (ni + nk) C + multiplier.utoZ m * Zbeta (ni + nj + 1) = 
      Sum ni A * Sum nk B + Sum nj B * u2Z (nth ni A zero32) * Zbeta ni + 
      u2Z (nth ni A zero32) * u2Z (nth nj B zero32) * Zbeta (ni + nj) /\
      gpr.lookup btmp s = nth nj B zero32 /\
      gpr.lookup l s = gpr.lookup i s (+) gpr.lookup j s
  ).

  red; intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  inversion_clear H as [nj].
  decompose [and] H0; clear H0.
  red.
  exists C; exists ni; exists nj.
  split; trivial.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_update_store.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Rewrite_u2Z.
  rewrite H13.
  ring.
  Constraint.
  Constraint.
  Constraint.
  split; trivial.
  split; trivial.
  split; trivial.
  
  apply semax_addiu'.

  red; intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  inversion_clear H as [nj].
  decompose [and] H0; clear H0.
  red.
  exists C; exists ni; exists (S nj).
  split; trivial.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_update_store.
  split; trivial.
  split.
  Rewrite_u2Z.
  rewrite Z_S; omega.
  Constraint.
  generalize (min_u2Z vc); intro.
  Constraint.
  Constraint.
  split; trivial.
  split.
  omega.
  split; trivial.
  split; trivial.
  split.
  rewrite Z_S.
  omega.
  split; trivial.
  generalize (multiplier.utoZ_lo_beta1 _ H11); intro X; decompose [and] X; clear X.
  rewrite <-H20.
  cutrewrite (ni+S nj = ni+nj+1)%nat.
  rewrite H15.
  ring.
  ring.
  rewrite Zbeta_is_exp.
  rewrite Sum_remove_last.
  rewrite <-Zbeta_power.
  fold zero32.
  ring.
  omega.

  apply semax_mflhxu'' with (fun s s' m h =>
    exists C, exists ni,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) **
        (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      (ni < nk)%nat /\
      multiplier.is_null m /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      u2Z (gpr.lookup z s) =
      u2Z (gpr.lookup t s) + 4 * Z_of_nat nk /\
      gpr.lookup atmp s = nth ni A zero32 /\
      Sum (ni + nk) C + u2Z (gpr.lookup ctmp s) * Zbeta (ni + nk) =
      Sum ni A * Sum nk B +
      Sum nk B * u2Z (nth ni A zero32) * Zbeta ni).

  red; intros.
  inversion_clear H.
  inversion_clear H0 as [C].
  inversion_clear H as [ni].
  inversion_clear H0 as [nj].
  decompose [and] H; clear H.
  red.
  exists C; exists ni.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_update_store.
  Inde_mult_mflhxu_op.
  split; trivial.
  split; trivial.
  split.
  apply multiplier.utoZ_is_null.
  assert ( multiplier.utoZ (multiplier.mflhxu_op m) < 1 ).
  apply multiplier.mflhxu_kbeta1_utoZ.
  assumption.
  generalize (multiplier.utoZ_pos (multiplier.mflhxu_op m)); intro.
  omega.
  split; trivial.
  split.
  rewrite H9 in H1; rewrite H6 in H1.
  rewrite <-H1; assumption.
  split; trivial.
  assert (nj=nk).
  apply Z_of_nat_inj.
  rewrite <-H9; rewrite <-H6; assumption.
  subst nj.
  assumption.

  apply semax_sw_backwards'' with (fun s s' m h =>
    exists C, exists ni,
      length C = (nk+nk)%nat /\
      gpr.lookup one s = one32 /\
      gpr.lookup a s = va /\
      gpr.lookup b s = vb /\
      gpr.lookup c s = vc /\
      u2Z (gpr.lookup k s) = Z_of_nat nk /\
      (((var_e a |--> A) ** (var_e b |--> B)) **
        (var_e c |--> C)) s s' m h /\
      u2Z (gpr.lookup i s) = Z_of_nat ni /\
      (ni < nk)%nat /\
      multiplier.is_null m /\
      u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat ni /\
      u2Z (gpr.lookup z s) =
      u2Z (gpr.lookup t s) + 4 * Z_of_nat nk /\
      gpr.lookup atmp s = nth ni A zero32 /\
      Sum (ni + nk + 1) C =
      Sum ni A * Sum nk B +
      Sum nk B * u2Z (nth ni A zero32) * Zbeta ni).
  
  red; intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  decompose [and] H; clear H.
  exists (int_e (nth (ni+nk) C zero32)).

  assert (Htmp : u2Z (eval (var_e c) s) + 4 * Z_of_nat (nk + nk) < Zbeta 1 /\
    eval (add_e (var_e z) (int_e (sign_extend_16_32 zero16))) s =
    eval (add_e (var_e c) (shl2_e (int_e (Z2u 32 (Z_of_nat (ni + nk)))))) s /\
    eval (add_e (add_e (var_e z) (int_e (sign_extend_16_32 zero16))) (int_e four32)) s =
    eval (add_e (add_e (var_e z) (int_e (sign_extend_16_32 zero16))) (int_e four32)) s).
  generalize (min_u2Z va); intro.
  generalize (min_u2Z vc); intro.
  simpl eval.
  rewrite H4.
  split.
  rewrite inj_plus.
  Constraint.
  split.
  unfold zero16.
  unfold sign_extend_16_32.
  rewrite sign_extend_Z2u.
  simpl plus.
  rewrite add_neutral.
  apply u2Z_injection.
  rewrite H11.
  rewrite H10.
  symmetry.
  Rewrite_u2Z.
  rewrite inj_plus.
  rewrite Hvc.
  ring.
  rewrite inj_plus.
  (*TODO: constraint does not work here*)
  split.
  omega.
  Clean_beta1.
  omega.
  rewrite inj_plus.
  Clean_beta1.
  Mult 2%nat.
  omega.
  omega.
  rewrite inj_plus.
  Clean_beta1.
  omega.
  rewrite inj_plus.
  Clean_beta1.
  omega.
  split.
  omega.
  rewrite inj_plus.
  Clean_beta1.
  omega.
  rewrite inj_plus.
  Clean_beta1.
  Mult 2%nat.
  omega.
  Clean_beta1.
  omega.
  rewrite inj_plus.
  split.
  omega.
  Clean_beta1.
  omega.
  repeat constructor.
  Constraint.
  reflexivity.

  Decompose_list_32 C (ni+nk)%nat lst1 lst2.
  lapply (mapstos_decompose_generic_P _ _ _ _ _ _ 
    (var_e c) 
    (add_e (var_e z) (int_e (sign_extend_16_32 zero16))) 
    (add_e (add_e (var_e z) (int_e (sign_extend_16_32 zero16))) (int_e four32)) 
    s 
    ((var_e b |--> B) ** (var_e a |--> A)) 
    H0 H15 H s' m h).
  intro.
  assert ( (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h ->
    ((var_e c |--> C) ** ((var_e b |--> B) ** (var_e a |--> A))) s s' m h ).
  intro.
  assoc_comm H16.
  generalize (H13 (H16 H6)); clear H13 H16; intro.
  simpl app in H13.
  Monotony H13.
  Adjunction H13.

  exists (update_list C (ni+nk) (gpr.lookup ctmp s)).
  exists ni.
  split.
  apply length_update_list; auto.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  assoc_comm H13.
  
  eapply mapstos_compose_generic with (lst2:=lst2) (w:=gpr.lookup ctmp s)
    (e':=add_e (var_e z) (int_e (sign_extend_16_32 zero16)))
    (e'':=add_e (add_e (var_e z) (int_e (sign_extend_16_32 zero16))) (int_e four32)).
  apply length_update_list.
  apply H0.
  apply H15.
  rewrite H.
  rewrite update_list_app.
  simpl.
  rewrite H15.
  rewrite <-minus_n_n.
  reflexivity.
  rewrite H15.
  constructor.
  exact Htmp.
  assoc_comm H13.

  generalize H13; clear H13.
  apply mapsto_ext'.
  reflexivity.
  simpl.
  reflexivity.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.

  rewrite <-H14.
  pattern C at 1.
  rewrite H.
  cutrewrite ( lst1 ++ nth (ni + nk) C zero32 :: nil ++ lst2
    = (lst1 ++ nth (ni + nk) C zero32 :: nil) ++ lst2).
  rewrite update_list_app'.
  rewrite <-Sum_beyond.
  rewrite update_list_app.
  rewrite H15.
  rewrite <-minus_n_n.
  simpl update_list.
  rewrite Sum_cut_last.
  cutrewrite ( ni + nk + 1 - 1 = ni + nk)%nat.
  rewrite H.
  rewrite <-Sum_beyond.
  ring.
  assumption.
  omega.
  omega.
  rewrite length_app; simpl; omega.
  rewrite H15; constructor.
  apply length_update_list.
  rewrite length_app; simpl; omega.
  rewrite length_app; simpl; omega.
  rewrite app_ass; reflexivity.

  exact Htmp.

  omega.

  apply semax_addiu'' with (fun s s' m h =>
     exists C, exists ni,
       length C = (nk+nk)%nat /\
       gpr.lookup one s = one32 /\
       gpr.lookup a s = va /\
       gpr.lookup b s = vb /\
       gpr.lookup c s = vc /\
       u2Z (gpr.lookup k s) = Z_of_nat nk /\
       (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s s' m h /\
       u2Z (gpr.lookup i s) = Z_of_nat ni /\
       (ni < nk)%nat /\
       multiplier.is_null m /\
       u2Z (gpr.lookup t s) = 4 * nc + 4 * (Z_of_nat ni + 1) /\
       gpr.lookup atmp s = nth ni A zero32 /\
       Sum (ni + nk + 1) C =
       Sum ni A * Sum nk B +
       Sum nk B * u2Z (nth ni A zero32) * Zbeta ni).

  red; intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  decompose [and] H; clear H.
  red.
  exists C; exists ni.
  split; trivial.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_update_store.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Rewrite_u2Z.
  omega.
  Constraint.
  Constraint.
  Constraint.
  split; trivial.

  apply semax_addiu'.

  red; intros.
  inversion_clear H as [C].
  inversion_clear H0 as [ni].
  decompose [and] H; clear H.
  red.
  exists C.
  exists (S ni).
  split; trivial.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  elim gpr.lookup_update; try var.
  rewrite gpr.lookup_update'; [idtac |  apply gp_reg_beq_false;  auto].
  elim gpr.lookup_update; try var.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split; trivial.
  split.
  Inde_update_store.
  split.
  Rewrite_u2Z.
  rewrite Z_S.
  omega.
  Constraint.
  generalize (min_u2Z va); intro.
  Constraint.
  Constraint.
  split.
  omega.
  split; trivial.
  split.
  rewrite Z_S.
  omega.
  cutrewrite (S ni+nk = ni+nk+1)%nat.
  rewrite H13.
  rewrite Sum_remove_last.
  rewrite <-Zbeta_power.
  fold zero32.
  ring.
  omega.
Qed.