Require Import ZArith.
Require Import List.
Require Import util.
Require Import presburgerZ.
Require Import machine_int.
Import MachineInt.
Require Import machine_int_spec.
Require Import sum.
Require Import state.
Require Import mips.
Require Import mapstos.
Require Import mips_contrib.
Require Import mips_tactics.
Require Import Znumtheory.
Require Import ssum.

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

(* Some lemmas for verification *)

Ltac Update_store :=  
  rewrite <- gpr.lookup_update; [auto |
    match goal with
      | id: is_set (?l) |- _ =>
        simpl in id; intuition
    end
  ].

Ltac Update_store_hyp H :=  
  rewrite <- gpr.lookup_update in H; [auto |
    match goal with
      | id: is_set (?l) |- _ =>
        simpl in id; intuition
    end
  ].

(*********************************************************)
(*  Signed multi-precision integer (2's complement ver.) *)
(*********************************************************)

(* This macro makes the two's complement of a register r *)

Definition mips_cplt2 (r: gp_reg) :=
  nor r r gpr_zero;
  addiu r r (Z2u 16 1).

Lemma mips_cplt2_correctness: forall r v (SET: is_set (r::gpr_zero::nil)),  
  {{fun s s' m h => 
    gpr.lookup r s = v /\
    h = heap.emp
  }}
  mips_cplt2 r
  {{fun s s' m h => 
    gpr.lookup r s = (int_cplt2 v) /\
    h = heap.emp
  }}.
  intros.
  unfold mips_cplt2.
  eapply semax_seq with (
    fun s (s':cp0.store) (m: multiplier.m) (h: heap.h) => 
      gpr.lookup r s = (int_not v) /\
      h = heap.emp
  ).
  eapply semax_strengthen_pre; [idtac | eapply semax_nor].
  red; intros.
  red.
  rewrite gpr.lookup_update'. 
  rewrite gpr.gpr_zero_zero32.
  rewrite (proj1 H).

  unfold zero32.
  
  rewrite int_or_zero; tauto.  

  simpl in SET; intuition.

  eapply semax_strengthen_pre; [idtac | eapply semax_addiu].
  red; intros.
  red.
  rewrite (proj1 H).
  rewrite gpr.lookup_update'.
  rewrite sign_extend_16_32'.

  rewrite int_not_add1_cplt2.
  tauto.
  omega.
  simpl.
  omega.
  simpl in SET; intuition.
Qed.

(* This macro returns in r1 the absolute value of the previously stored value in r1 and r2 contains its sign (r2 = 0 -> positive /\ r2 = 1 -> negative) *)

Definition mips_ssum_sign (r1 r2: gp_reg) :=
  ifte_bltz r1 thendo (    
    (* r1 is negative  *)
    addiu r2 gpr_zero (Z2u 16 1);
    mips_cplt2 r1
  ) elsedo (
    addiu r2 gpr_zero (Z2u 16 0)    
  ).

Lemma mips_ssum_sign_specif: forall r1 r2 v (V: not_weird v),
  (is_set (r1::r2::gpr_zero::nil)) ->
  {{fun s s' m h => 
    gpr.lookup r1 s = v /\
    h = heap.emp
  }}
  mips_ssum_sign r1 r2
  {{fun s s' m h => 
    s2Z (gpr.lookup r1 s) >= 0 /\
    (gpr.lookup r2 s = (Z2u 32 1) \/ gpr.lookup r2 s = (Z2u 32 0)) /\
    (gpr.lookup r2 s = (Z2u 32 1) -> gpr.lookup r1 s = (int_cplt2 v) /\ s2Z v < 0) /\
    (gpr.lookup r2 s = (Z2u 32 0) -> gpr.lookup r1 s = v /\ s2Z v >= 0) /\ 
    h = heap.emp
  }}.

  intros.
  unfold mips_ssum_sign.
  eapply semax_ifte_bltz.
  eapply semax_seq with (
    fun (s1 : gpr.store) (_ : cp0.store) (_ : multiplier.m) (h : heap.h) =>
      gpr.lookup r1 s1 = v /\ s2Z (gpr.lookup r1 s1) < 0 /\
      gpr.lookup r2 s1 = (Z2u 32 1) /\ h = heap.emp
  ).
  eapply semax_strengthen_pre; [idtac | eapply semax_addiu].
  red; intros.
  inversion_clear H0.
  split.
  rewrite sign_extend_16_32'; try (simpl; omega).
  rewrite <- gpr.lookup_update; try tauto.
  simpl in H; intuition.  
  split.
  rewrite sign_extend_16_32'; try (simpl; omega).
  rewrite <- gpr.lookup_update; try tauto.
  simpl in H; intuition.  
  rewrite sign_extend_16_32'; try (simpl; omega).
  rewrite gpr.lookup_update'; try tauto.
  rewrite gpr.gpr_zero_zero32.
  rewrite add_com.
  unfold zero32.
  rewrite add_neutral.
  tauto. 
  simpl in H; intuition.  

  eapply semax_strengthen_pre with (
    ((fun s s' m h => gpr.lookup r1 s = v /\ h = heap.emp) ** (fun s s' m h => s2Z v < 0 /\ h = heap.emp) ** (fun s s' m h => gpr.lookup r2 s = Z2u 32 1 /\ h = heap.emp))
  ).
  red; intros.
  decompose [and] H0; clear H0.
  Compose_sepcon h heap.emp; auto.
  Compose_sepcon h heap.emp; auto.
  rewrite H1 in H3; auto.

  eapply semax_weaken_post with (
    ((fun s s' m h => gpr.lookup r1 s = (int_cplt2 v) /\ h = heap.emp) ** (fun s s' m h => s2Z v < 0 /\ h = heap.emp) ** (fun s s' m h => gpr.lookup r2 s = Z2u 32 1 /\ h = heap.emp))
  ).
  
  red; intros.
  Decompose_sepcon H0 h1 h2.
  Decompose_sepcon H2 h11 h12.
  
  split.

  rewrite H8.
  rewrite s2Z_int_cplt2.
  omega.
  auto.

  split; intros.
  auto.
  split; intros.
  auto.
  split.
  intros.
  rewrite H4 in H2.
  assert (Z2u 32 1 <> Z2u 32 0).
  eapply Z2u_dis; try omega.
  intuition.
  simpl.  
  constructor.
  intuition.
  simpl.
  constructor.
  tauto.
  Equal_heap.

  repeat rewrite <- con_assoc_equiv.
  simpl.
  eapply frame_rule.
  eapply frame_rule.

  eapply mips_cplt2_correctness.
  
  simpl; simpl in H; tauto.

  simpl.
  red; intros.
  intuition.
  
  simpl.
  red; intros.
  intuition.

  simpl.
  red; intros.
  assert (x = r1).
  simpl in H0.
  inversion_clear H0 ;auto.
  inversion_clear H1; auto.
  contradiction.
  subst x.

  split; intros.
  rewrite <- gpr.lookup_update; auto.
  simpl in H; intuition.
  rewrite <- gpr.lookup_update in H1; auto.
  simpl in H; intuition.

  simpl.
  red; intros.
  intuition.

  eapply semax_strengthen_pre; [idtac | eapply semax_addiu].
  red; intros.
  inversion_clear H0.
  split.
  rewrite <- gpr.lookup_update; auto.
  simpl in H; intuition.
  rewrite sign_extend_16_32'; try (simpl; omega).
  split; intros.
  
  rewrite gpr.lookup_update'; auto.
  right.
  rewrite gpr.gpr_zero_zero32.
  rewrite add_neutral.
  auto.
  simpl in H; intuition.  
  
  split; intros.
  rewrite gpr.lookup_update' in H0; auto.
  assert (Z2u 32 0 <> Z2u 32 1).
  eapply Z2u_dis; try omega.
  intuition.
  simpl.
  constructor.
  intuition.
  simpl.
  constructor.
  rewrite gpr.gpr_zero_zero32 in H0.
  rewrite add_neutral in H0.
  tauto.
  simpl in H; intuition.

  split; intros.
  rewrite <- gpr.lookup_update.
  rewrite (proj1 H1) in H2; tauto.
  simpl in H; intuition.
  tauto.
Qed.

(* transform a signed multiprecision integer stored in the heap into an unsigned, 
    - rk is the index of the most significant word
    - (r2 = 0 -> positive) /\ (r2 <> 0 -> negative)
*)

Definition sSum2Sum (r1 r2 ra rk rc: gp_reg) : cmd :=
  lwxs r1 rk ra;
  mips_ssum_sign r1 r2;
  ifte_beq r2, gpr_zero thendo (
    skip
  ) elsedo (
    sll rc rk (Z2u 5 2);
    addu rc rc ra;
    sw r1 zero16 rc    
  ).

Lemma sSum2Sum_specif: forall nk (Hk:(nk > O)%nat) na
  (Hna: 4 * na + 4 * Z_of_nat (S nk) < Zbeta 1)
  va (Hva: u2Z va = 4 * na)
  A (Ha:length A = S nk) vA r1 r2 ra rk rc
  (Not_weird:  not_weird (nth nk A zero32)),
  is_set (r1::r2::ra::rk::rc::gpr_zero::nil) ->
  {{ fun s s' m h =>      
    u2Z (gpr.lookup rk s) = Z_of_nat nk /\
    gpr.lookup ra s = va /\         
    (var_e ra |--> A) s s' m h /\
    sSum nk A = vA
  }}
  sSum2Sum r1 r2 ra rk rc
  {{ fun s s' m h => 
    (var_e ra |--> (ssum_lst2sum_lst nk A)) s s' m h /\    
    (u2Z (gpr.lookup r2 s) <> 0 -> (ssum_k_sign nk A) = true) /\
    ( u2Z (gpr.lookup r2 s) = 0  -> (ssum_k_sign nk A) = false)    
  }}.

  intros.
  unfold sSum2Sum.
  
  (* lwxs r1 rk ra *)
  eapply semax_seq with (
    fun s s' m h =>      
      u2Z (gpr.lookup rk s) = Z_of_nat nk /\
      gpr.lookup ra s = va /\         
      (var_e ra |--> A) s s' m h /\
      sSum nk A = vA /\
      gpr.lookup r1 s = nth nk A zero32
  ).

  eapply semax_lwxs_backwards'2.
  red; intros.
  decompose [and] H0; clear H0.
  exists (nth nk A zero32).
  split.  

  Decompose_list_32 A nk A1 A2; try omega.  

  (* finir mapstos_app_cons et faire mapstos_cons_app *)
  
  rewrite H0 in H2.

  destruct A2; [rewrite <- app_nil_end in H0 |
    rewrite H0 in Ha; rewrite length_app in Ha; simpl in Ha; rewrite H6 in Ha; assert False; [omega | contradiction]
  ].
  
  rewrite <- app_nil_end in H2.



  assert (       
    ((var_e ra |--> A1) **
      (add_e (var_e ra) (shl2_e (int_e (Z2u 32 (Z_of_nat nk))))
        |--> nth nk A zero32 :: nil)) s s' m h).

  apply (mapstos_decompose_app nk A1 (nth nk A zero32 :: nil) (S nk) A
    (var_e ra) (add_e (var_e ra) (shl2_e (int_e (Z2u 32 (Z_of_nat nk))))) s
    Ha H6 H0 s' m h).
  simpl eval.
  rewrite H3.
  rewrite Hva.
  auto.
  auto.
  rewrite H0; auto.
  Decompose_sepcon H4 h1 h2.
  simpl in H11.
  Decompose_sepcon H11 h21 h22.
  Compose_sepcon h21 (h1 +++ h22).
  eapply mapsto_equiv'.
  apply H11.
  simpl.
  assert (Z2u 32 (Z_of_nat nk) = gpr.lookup rk s).
  rewrite <- H1.
  eapply u2Z_injection.
  rewrite Z2u_injection.
  auto.
  intuition.
  simpl.
  rewrite H1.
  unfold Zbeta in Hna.
  simpl Zpower in Hna.
  generalize (min_u2Z va); intros.
  rewrite Hva in H10; generalize H10.
  generalize Hna.
  cutrewrite (S nk = nk + 1)%nat.
  rewrite inj_plus.
  simpl Z_of_nat.
  PresburgerZ_decision.
  omega.
  
  rewrite H10; auto.
  auto.
  red; auto.  

  (* finir mapstos_app_cons et faire mapstos_cons_app *)

  red.
  split.

  Update_store.
  split.
  Update_store.
  split.  
  eapply mapstos_equiv.
  apply H2.
  simpl.
  Update_store.
  split.
  auto.
  rewrite gpr.lookup_update'; auto.
  simpl in H; intuition.

  (*  mips_ssum_sign r1 r2; *)

  eapply semax_strengthen_pre with (
    (fun (s : gpr.store) (s' : cp0.store) (m : multiplier.m) (h : heap.h) =>
      gpr.lookup r1 s = nth nk A zero32 /\ (h = heap.emp)
    ) **
    (fun (s : gpr.store) (s' : cp0.store) (m : multiplier.m) (h : heap.h) =>
      gpr.lookup ra s = va /\  u2Z (gpr.lookup rk s) = Z_of_nat nk /\
      (var_e ra |--> A) s s' m h
    ) 
  ).

  red; intros.

  decompose [and] H0; clear H0.
  Compose_sepcon heap.emp h.
  auto.
  auto.
  
  eapply semax_seq with (
    (fun (s : gpr.store) (s' : cp0.store) (m : multiplier.m) (h : heap.h) =>
      s2Z (gpr.lookup r1 s) >= 0 /\
      (gpr.lookup r2 s = (Z2u 32 1) \/ gpr.lookup r2 s = (Z2u 32 0)) /\
      (gpr.lookup r2 s = (Z2u 32 1) -> gpr.lookup r1 s = (int_cplt2 (nth nk A zero32)) /\ s2Z (nth nk A zero32) < 0) /\
      (gpr.lookup r2 s = (Z2u 32 0) -> gpr.lookup r1 s = (nth nk A zero32) /\ s2Z (nth nk A zero32) >= 0) /\
      (h = heap.emp)
    ) **
    (fun (s : gpr.store) (s' : cp0.store) (m : multiplier.m) (h : heap.h) =>
      gpr.lookup ra s = va /\  u2Z (gpr.lookup rk s) = Z_of_nat nk /\
      (var_e ra |--> A) s s' m h
    ) 
  ).

  eapply frame_rule.
  eapply mips_ssum_sign_specif.
  auto.
  simpl in H; simpl; tauto.
  simpl; red; intros.
  assert (x = r2 \/ x = r1).
  simpl in H0.
  intuition.
  inversion_clear H1; subst x.

  split.
  intros.
  decompose [and] H1; clear H1.
  split.
  Update_store.
  split.
  Update_store.
  eapply mapstos_equiv.
  apply H5.
  simpl.
  Update_store.
  intros.
  decompose [and] H1; clear H1.
  split.
  Update_store_hyp H2.
  split.
  Update_store_hyp H4.
  eapply mapstos_equiv.
  apply H5.
  simpl.
  Update_store.

  split.
  intros.
  decompose [and] H1; clear H1.
  split.
  Update_store.
  split.
  Update_store.
  eapply mapstos_equiv.
  apply H5.
  simpl.
  Update_store.
  intros.
  decompose [and] H1; clear H1.
  split.
  Update_store_hyp H2.
  split.
  Update_store_hyp H4.
  eapply mapstos_equiv.
  apply H5.
  simpl.
  Update_store.

  red; simpl; intros; tauto.

  (* ifte_beq r2, gpr_zero *)
  
  eapply semax_ifte_beq.

  (* skip *)
  
  eapply semax_strengthen_pre; [idtac | eapply semax_skip].
  
  red; intros.
  
  inversion_clear H0.
  
  Decompose_sepcon H1 h1 h2.
  subst h1.
  assert (h = h2).
  Equal_heap.
  subst h2; clear H4 H0.
  rewrite gpr.gpr_zero_zero32 in H2.
  unfold zero32 in H2.
  generalize (H8 H2); clear H8 H3; intros.
  split.
  cutrewrite (ssum_lst2sum_lst nk A = A).
  auto.
  rewrite (proj1 H0) in H5.

  eapply ssum_lst2sum_lst_eq.
  auto.

  split; intros.
  rewrite H2 in H1.
  rewrite Z2u_injection in H1.
  assert (False); [omega | contradiction].
  intuition.
  simpl.
  constructor.
  rewrite (proj1 H0) in H5.

  
  apply ssum_k_sign_false; auto.
  
  (* sll rc rk (Z2u 5 5) *)

  eapply semax_seq with (
    fun (s : gpr.store) (s' : cp0.store) (m : multiplier.m) (h : heap.h) =>
      s2Z (gpr.lookup r1 s) >= 0 /\
      (gpr.lookup r2 s = (Z2u 32 1) -> gpr.lookup r1 s = (int_cplt2 (nth nk A zero32)) /\ s2Z (nth nk A zero32) < 0) /\
      (gpr.lookup r2 s = (Z2u 32 0) -> gpr.lookup r1 s = (nth nk A zero32)  /\ s2Z (nth nk A zero32) >= 0) /\      
      gpr.lookup ra s = va /\  u2Z (gpr.lookup rk s) = Z_of_nat nk /\
      (var_e ra |--> A) s s' m h /\
      gpr.lookup r2 s = (Z2u 32 1) /\
      gpr.lookup rc s = (shl2  (gpr.lookup rk s))
  ).

  eapply semax_strengthen_pre; [idtac | eapply semax_sll].

  red; intros.
  inversion_clear H0.  
  Decompose_sepcon H1 h1 h2.
  subst h1.
  assert (h2 = h).
  Equal_heap.
  subst h2.
  clear H4 H0.
  red.
  split.
  Update_store.
  split.
  Update_store.
  Update_store.
  split.
  Update_store.
  Update_store.
  split.
  Update_store.
  split.
  Update_store.
  split.
  eapply mapstos_equiv.
  apply H12.
  simpl.
  Update_store.
  split.
  Update_store.
  rewrite gpr.gpr_zero_zero32 in H2.
  inversion_clear H3.
  auto.
  rewrite H0 in H2.
  unfold zero32 in H2.
  intuition.
  rewrite gpr.lookup_update'.
  Update_store.
  rewrite Z2u_injection.
  unfold shl2.
  cutrewrite (nat_of_Z 2 = 2)%nat.
  auto.
  auto.
  constructor.
  omega.
  simpl.
  constructor.
  simpl in H; intuition.

  (* addu rc rc ra *)

  eapply semax_seq with (
    fun (s : gpr.store) (s' : cp0.store) (m : multiplier.m) (h : heap.h) =>
      s2Z (gpr.lookup r1 s) >= 0 /\
      (gpr.lookup r2 s = (Z2u 32 1) -> gpr.lookup r1 s = (int_cplt2 (nth nk A zero32)) /\ s2Z (nth nk A zero32) < 0) /\
      (gpr.lookup r2 s = (Z2u 32 0) -> gpr.lookup r1 s = (nth nk A zero32) /\ s2Z (nth nk A zero32) >= 0) /\      
      gpr.lookup ra s = va /\  u2Z (gpr.lookup rk s) = Z_of_nat nk /\
      (var_e ra |--> A) s s' m h /\
      gpr.lookup r2 s = (Z2u 32 1) /\
      gpr.lookup rc s = (shl2  (gpr.lookup rk s)) (+) va      
  ).

  eapply semax_strengthen_pre; [idtac | eapply semax_addu].

  red; intros.

  decompose [and] H0; clear H0.
  
  red.
  split.
  rewrite H9; rewrite H4.
  unfold shl2.
  rewrite <- gpr.lookup_update.
  generalize (H3 H7); intros.
  inversion_clear H0.
  rewrite H8.
  rewrite s2Z_int_cplt2; auto.
  omega.
  simpl in H; intuition.
  Update_store.
  Update_store.
  Update_store.
  Update_store.
  rewrite gpr.lookup_update'.
  split        .
  auto.
  split; auto.
  split; auto.
  split; auto.
  split.
  
  eapply mapstos_equiv.
  apply H6.
  simpl.
  Update_store.
  split.
  auto.
  rewrite H9.
  rewrite H4; auto.
  simpl in H; intuition.

  (* sw r1 zero16 rc *)
  
  eapply semax_strengthen_pre; [idtac | eapply semax_sw_backwards].
  red; intros.
  decompose [and] H0; clear H0.
  
  exists (int_e (nth nk A zero32)).  

  Decompose_list_32 A nk A1 A2; try omega.
  rewrite H0 in H6.
  
  destruct A2; [rewrite <- app_nil_end in H6 |
    rewrite H0 in Ha; rewrite length_app in Ha; simpl in Ha; rewrite H10 in Ha; assert False; [omega | contradiction]
  ].

  assert (       
    ((var_e ra |--> A1) **
      (add_e (var_e ra) (shl2_e (int_e (Z2u 32 (Z_of_nat nk))))
        |--> nth nk A zero32 :: nil)) s s' m h).

  apply (mapstos_decompose_app nk A1 (nth nk A zero32 :: nil) (S nk) A
    (var_e ra) (add_e (var_e ra) (shl2_e (int_e (Z2u 32 (Z_of_nat nk))))) s
    Ha H10 H0 s' m h).
  simpl eval.
  rewrite H4.
  rewrite Hva.
  auto.
  auto.
  rewrite H0; auto.
  generalize H8; clear H6 H8; intro H6.  

  Decompose_sepcon H6 h1 h2.
  simpl in H14.
  Decompose_sepcon H14 h21 h22.

  Compose_sepcon h21 (h1 +++ h22).
  eapply mapsto_equiv'.
  apply H14.
  unfold zero16.
  rewrite sign_extend_16_32'.
  simpl.
  rewrite H9.
  rewrite <- H4.
  rewrite <- H5.  
  cutrewrite (Z2u 32 (u2Z (gpr.lookup rk s)) =  (gpr.lookup rk s)).
  rewrite add_neutral.
  rewrite add_com.
  auto.
  apply u2Z_injection.
  rewrite Z2u_injection.
  auto.
  constructor.
  rewrite H5.
  omega.
  simpl.
  rewrite H5.
  unfold Zbeta in Hna.
  simpl Zpower in Hna.
  generalize (min_u2Z va); intros.
  rewrite Hva in H13; generalize H13.
  generalize Hna.
  cutrewrite (S nk = nk + 1)%nat.
  rewrite inj_plus.
  simpl Z_of_nat.  
  PresburgerZ_decision.
  omega.
  simpl; constructor.
  auto.
  Intro_sepimp h21' h'. 
  split.

  generalize (H3 H7); intros.
  inversion_clear H19.

  rewrite ssum_lst2sum_lst_chg_elt; auto.
  
  rewrite H0.
  
  rewrite chg_elt_app; try omega.
  rewrite <- app_nil_end; rewrite <- app_nil_end in H0.
  eapply mapstos_compose_app.
  rewrite length_app.
  rewrite H10.
  cutrewrite (nk - nk = 0)%nat; [idtac | omega].
  simpl.
  intuition.
  apply H10.
  rewrite H10.
  cutrewrite (nk - nk = 0)%nat; [idtac | omega].
  simpl.
  intuition.
  simpl eval.
  rewrite H4.
  rewrite Hva.
  cutrewrite (nk + 1 = S nk)%nat.
  auto.
  omega.
  intuition.

  Compose_sepcon h1 (h22 +++ h21').
  auto.
  simpl.
  Compose_sepcon h21' h22.
  eapply mapsto_equiv'.
  apply H16.
  simpl.
  rewrite H9.
  rewrite <- H5.
  unfold zero16.
  rewrite sign_extend_16_32'.
  rewrite H4.

  assert (Z2u 32 (u2Z (gpr.lookup rk s)) = gpr.lookup rk s).
  eapply u2Z_injection.
  rewrite Z2u_injection.
  auto.
  intuition.
  simpl.
  rewrite H5.
  unfold Zbeta in Hna.
  simpl Zpower in Hna.
  generalize (min_u2Z va); intros.
  rewrite Hva in H19; generalize H19.
  generalize Hna.
  cutrewrite (S nk = nk + 1)%nat.
  rewrite inj_plus.
  simpl Z_of_nat.  
  PresburgerZ_decision.
  omega.
  rewrite H19; clear H19.
  rewrite add_neutral.
  rewrite add_com.
  auto.
  simpl; constructor.
  simpl.
  rewrite nth_app.
  rewrite H10.
  cutrewrite (nk - nk = 0)%nat; try omega.
  simpl.
  auto.
  omega.
  red; auto.
  split; intros.

  generalize (H3 H7); intros.
  inversion_clear H20.
  
  apply ssum_k_sign_true.
  auto.
  auto.
  
  rewrite H7 in H19.
  rewrite Z2u_injection in H19.
  assert False; [omega | contradiction].
  intuition.
  simpl; constructor.
Qed.

(* inverse a signed multiprecision integer stored in the heap, 
    - rk is the index of the most significant word
*)

Definition negsSum_cmd (r ra rk rc: gp_reg) : cmd :=
  lwxs r rk ra;
  mips_cplt2 r;
  sll rc rk (Z2u 5 2);
  addu rc rc ra;
  sw r zero16 rc.

Lemma negsSum_cmd_specif: forall nk (Hk:(nk > O)%nat) na
  (Hna: 4 * na + 4 * Z_of_nat (S nk) < Zbeta 1)
  va (Hva: u2Z va = 4 * na)
  A (Ha:length A = S nk) vA r ra rk rc
  (Not_weird:  not_weird (nth nk A zero32)),
  is_set (r::ra::rk::rc::gpr_zero::nil) ->
  {{ fun s s' m h =>      
    u2Z (gpr.lookup rk s) = Z_of_nat nk /\
    (var_e ra |--> A) s s' m h /\
    gpr.lookup ra s = va /\         
    sSum nk A = vA
  }}
  negsSum_cmd r ra rk rc
  {{ fun s s' m h => 
    (var_e ra |--> (negsSum nk A)) s s' m h
  }}.
  intros.
  unfold negsSum_cmd.

  (* lwxs r1 rk ra *)
  
  eapply semax_seq with (
    fun s s' m h =>      
      u2Z (gpr.lookup rk s) = Z_of_nat nk /\
      (var_e ra |--> A) s s' m h /\
      gpr.lookup ra s = va /\         
      sSum nk A = vA /\
      gpr.lookup r s = nth nk A zero32
  ).

  eapply semax_lwxs_backwards'2.
  red; intros.
  decompose [and] H0; clear H0.
  exists (nth nk A zero32).
  split.  

  Decompose_list_32 A nk A1 A2; try omega.  

  (* finir mapstos_app_cons et faire mapstos_cons_app *)
  
  rewrite H0 in H3.

  destruct A2; [rewrite <- app_nil_end in H0 |
    rewrite H0 in Ha; rewrite length_app in Ha; simpl in Ha; rewrite H6 in Ha; assert False; [omega | contradiction]
  ].
  
  rewrite <- app_nil_end in H3.

  assert (       
    ((var_e ra |--> A1) **
      (add_e (var_e ra) (shl2_e (int_e (Z2u 32 (Z_of_nat nk))))
        |--> nth nk A zero32 :: nil)) s s' m h).

  apply (mapstos_decompose_app nk A1 (nth nk A zero32 :: nil) (S nk) A
    (var_e ra) (add_e (var_e ra) (shl2_e (int_e (Z2u 32 (Z_of_nat nk))))) s
    Ha H6 H0 s' m h).
  simpl eval.
  rewrite H2.
  rewrite Hva.
  auto.
  auto.
  rewrite H0; auto.
  Decompose_sepcon H4 h1 h2.
  simpl in H11.
  Decompose_sepcon H11 h21 h22.
  Compose_sepcon h21 (h1 +++ h22).
  eapply mapsto_equiv'.
  apply H11.
  simpl.
  assert (Z2u 32 (Z_of_nat nk) = gpr.lookup rk s).
  rewrite <- H1.
  eapply u2Z_injection.
  rewrite Z2u_injection.
  auto.
  intuition.
  simpl.
  rewrite H1.
  unfold Zbeta in Hna.
  simpl Zpower in Hna.
  generalize (min_u2Z va); intros.
  rewrite Hva in H10; generalize H10.
  generalize Hna.
  cutrewrite (S nk = nk + 1)%nat.
  rewrite inj_plus.
  simpl Z_of_nat.
  PresburgerZ_decision.
  omega.
  rewrite H10.
  auto.
  auto.
  red; auto.
  (* finir mapstos_app_cons et faire mapstos_cons_app *)

  red.
  split.

  Update_store.
  split.
  eapply mapstos_equiv.
  apply H3.
  simpl.
  Update_store.
  split.
  Update_store.
  split.
  auto.
  rewrite gpr.lookup_update'; auto.
  simpl in H; intuition.

  (*  mips_cplt2 r *)

  eapply semax_seq with (
    (fun s s' m h =>      
      gpr.lookup r s = int_cplt2 (nth nk A zero32) /\
      h = heap.emp) **
    (fun s s' m h =>      
      u2Z (gpr.lookup rk s) = Z_of_nat nk /\
      (var_e ra |--> A) s s' m h /\
      gpr.lookup ra s = va /\         
      sSum nk A = vA 
    )      
  ).

  eapply semax_strengthen_pre with (
    (fun s s' m h =>      
      gpr.lookup r s = (nth nk A zero32) /\
      h = heap.emp) **
    (fun s s' m h =>      
      u2Z (gpr.lookup rk s) = Z_of_nat nk /\
      (var_e ra |--> A) s s' m h /\
      gpr.lookup ra s = va /\         
      sSum nk A = vA 
    )      
  ).

  red; intros.
  Compose_sepcon heap.emp h; tauto.

  eapply frame_rule.

  eapply mips_cplt2_correctness.

  simpl in H; simpl; tauto.
  
  red; intros.
  simpl in H0.
  assert (r = x); try tauto.
  subst x.
  
  split; intros.  
  decompose [and] H1; clear H1.
  split.
  Update_store.
  split.
  eapply mapstos_equiv.
  apply H4.
  simpl.  
  Update_store.
  Update_store.

  decompose [and] H1; clear H1.
  split.
  Update_store_hyp H2.
  split.
  eapply mapstos_equiv.
  apply H4.
  simpl.  
  Update_store.
  split.
  Update_store_hyp H3.
  auto.

  red; simpl.
  intros.
  tauto.

  
  (*  sll rc rk (Z2u 5 2) *)

  eapply semax_seq with (
    (fun s s' m h =>      
      gpr.lookup r s = int_cplt2 (nth nk A zero32) /\
      u2Z (gpr.lookup rk s) = Z_of_nat nk /\
      (var_e ra |--> A) s s' m h /\
      gpr.lookup ra s = va /\         
      sSum nk A = vA /\
      gpr.lookup rc s = (shl2  (gpr.lookup rk s))
    )      
  ).
  
  eapply semax_strengthen_pre; [idtac | eapply  semax_sll].

  red; intros.
  Decompose_sepcon H0 h1 h2.
  assert (h2 = h).
  Equal_heap.
  subst h2.
  red.
  split.
  Update_store.
  split.
  Update_store.
  split.
  eapply mapstos_equiv.
  apply H5.
  simpl; Update_store.
  split.
  Update_store.
  split; auto.
  rewrite gpr.lookup_update'.
  rewrite Z2u_injection.
  unfold shl2.
  cutrewrite (nat_of_Z 2 = 2)%nat.
  Update_store.
  auto.
  constructor.
  omega.
  simpl.
  constructor.
  simpl in H; intuition.
  

  (*  addu rc rc ra *)
  eapply semax_seq with (
    (fun s s' m h =>      
      gpr.lookup r s = int_cplt2 (nth nk A zero32) /\
      u2Z (gpr.lookup rk s) = Z_of_nat nk /\
      (var_e ra |--> A) s s' m h /\
      gpr.lookup ra s = va /\         
      sSum nk A = vA /\
      gpr.lookup rc s = (shl2  (gpr.lookup rk s)) (+) va
    )      
  ).

  eapply semax_strengthen_pre; [idtac | eapply  semax_addu].

  red; intros.

  decompose [and] H0; clear H0.
  
  red.
  split.
  rewrite H7; rewrite H4.
  unfold shl2.
  rewrite <- gpr.lookup_update.
  auto.
  simpl in H; intuition.
  Update_store.
  Update_store.
  rewrite gpr.lookup_update'.
  split        .
  auto.
  split; auto.
  eapply mapstos_equiv.
  apply H2.
  simpl.
  Update_store.
  split; auto.
  split; auto.
  rewrite H7.
  rewrite H4; auto.
  simpl in H; intuition.


 (* sw r1 zero16 rc *)
  
  eapply semax_strengthen_pre; [idtac | eapply semax_sw_backwards].
  red; intros.
  decompose [and] H0; clear H0.
  
  exists (int_e (nth nk A zero32)).  

  Decompose_list_32 A nk A1 A2; try omega.
  rewrite H0 in H2.

  destruct A2; [rewrite <- app_nil_end in H2 |
    rewrite H0 in Ha; rewrite length_app in Ha; simpl in Ha; rewrite H8 in Ha; assert False; [omega | contradiction]
  ].

  assert (       
    ((var_e ra |--> A1) **
      (add_e (var_e ra) (shl2_e (int_e (Z2u 32 (Z_of_nat nk))))
        |--> nth nk A zero32 :: nil)) s s' m h).

  apply (mapstos_decompose_app nk A1 (nth nk A zero32 :: nil) (S nk) A
    (var_e ra) (add_e (var_e ra) (shl2_e (int_e (Z2u 32 (Z_of_nat nk))))) s
    Ha H8 H0 s' m h).
  simpl eval.
  rewrite H4.
  rewrite Hva.
  auto.
  auto.
  rewrite H0; auto.

  Decompose_sepcon H6 h1 h2.
  simpl in H13.
  Decompose_sepcon H13 h21 h22.

  Compose_sepcon h21 (h1 +++ h22).
  eapply mapsto_equiv'.
  apply H13.
  unfold zero16.
  rewrite sign_extend_16_32'.
  simpl.
  rewrite H7.
  rewrite <- H4.
  rewrite <- H3.  
  cutrewrite (Z2u 32 (u2Z (gpr.lookup rk s)) =  (gpr.lookup rk s)).
  rewrite add_neutral.
  rewrite add_com.
  auto.
  apply u2Z_injection.
  rewrite Z2u_injection.
  auto.
  constructor.
  rewrite H3.
  omega.
  simpl.
  rewrite H3.
  unfold Zbeta in Hna.
  simpl Zpower in Hna.
  generalize (min_u2Z va); intros.
  rewrite Hva in H12; generalize H12.
  generalize Hna.
  cutrewrite (S nk = nk + 1)%nat.
  rewrite inj_plus.
  simpl Z_of_nat.  
  PresburgerZ_decision.
  omega.
  simpl; constructor.
  auto.
  Intro_sepimp h21' h'. 
    
  rewrite negsSum_chg_elt; auto.
  
  rewrite H0.
  
  rewrite chg_elt_app; try omega.

  simpl.
  cutrewrite (nk - length A1 = 0)%nat; try omega.  
  eapply mapstos_compose_app.
  rewrite length_app.
  rewrite H8.
  simpl.
  intuition.
  apply H8.
  intuition.
  simpl eval.
  rewrite H4.
  cutrewrite (nk + 1 = S nk)%nat; try omega.
  intuition.
  
  Compose_sepcon h1 (h22 +++ h21').
  auto.
  simpl.
  Compose_sepcon h21' h22.
  
  eapply mapsto_equiv'.
  apply H15.
  simpl.
  unfold zero16.
  rewrite sign_extend_16_32'.
  simpl.
  rewrite H7.
  rewrite <- H4.
  rewrite <- H3.  
  cutrewrite (Z2u 32 (u2Z (gpr.lookup rk s)) =  (gpr.lookup rk s)).
  rewrite add_neutral.
  rewrite add_com.
  auto.
  apply u2Z_injection.
  rewrite Z2u_injection.
  auto.
  constructor.
  rewrite H3; try omega.
  rewrite H3.
  unfold Zbeta in Hna.
  simpl Zpower in Hna.
  generalize (min_u2Z va); intros.
  simpl.
  rewrite Hva in H18; generalize H18.
  generalize Hna.
  cutrewrite (S nk = nk + 1)%nat.
  rewrite inj_plus.
  simpl Z_of_nat.  
  PresburgerZ_decision.
  omega.
  constructor.
  simpl.
  rewrite H1.
  rewrite nth_app.
  cutrewrite (nk - length A1 = 0)%nat; try omega.
  auto.
  omega.
  red; auto.
Qed.