Require Import ZArith. Require Import List. Require Import util. 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_tactics. Require Import mips_contrib. 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. (* register that contains 1 *) Definition a := gpr_a0. (* arguments *) Definition b := gpr_a1. Definition c := gpr_a2. Definition t := gpr_t0. (* pointer for sw *) Definition j := gpr_t2. (* counter for input *) Definition u := gpr_t3. (* test for overflow *) Definition bor := gpr_t4. (* borrow *) Definition atmp := gpr_t5. (* local variables *) Definition btmp := gpr_t6. Definition btmp' := gpr_t7. (* btmp + borrow *) Definition ctmp := gpr_t8. Definition multisub := addiu one gpr_zero one16; addiu j gpr_zero zero16; addiu t c zero16; addiu bor gpr_zero zero16; while_bne j k ( lwxs atmp j a; lwxs btmp j b; addu btmp' btmp bor; sltu u btmp' btmp; ifte_beq u, gpr_zero thendo multu atmp one; msubu btmp' one; mflhxu ctmp; sltu u atmp btmp'; ifte_beq u, gpr_zero thendo addiu bor gpr_zero zero16 elsedo addiu bor gpr_zero one16 elsedo addiu ctmp atmp zero16; sw ctmp zero16 t; addiu t t four16; addiu j j one16 ). Lemma multisub_specif : forall nk (Hk:(nk > O)%nat) na nb nc (Hna: 4 * na + 4 * Z_of_nat nk < Zbeta 1) (Hnb: 4 * nb + 4 * Z_of_nat nk < Zbeta 1) (Hnc: 4 * nc + 4 * 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 /\ 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 }} multisub {{ fun s s' m h => exists C, length C = nk /\ ((var_e c |--> C) ** TT) s s' m h /\ Sum nk C = Sum nk A - Sum nk B + u2Z (gpr.lookup bor s) * Zbeta nk }}. intros. unfold multisub. (********************* addi one gpr_zero one16; *********************) apply semax_addiu'' with (fun s s' m h => exists C, length C = nk /\ 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 /\ gpr.lookup one s = one32 ). 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. rewrite gpr.lookup_update'; [idtac | apply gp_reg_beq_false; auto]. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. Inde_update_store. apply u2Z_injection. Rewrite_u2Z. reflexivity. Constraint. Constraint. Constraint. Constraint. (********************* addi j zero zero16; *********************) apply semax_addiu'' with (fun s s' m h => exists C, length C = nk /\ 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 /\ gpr.lookup one s = one32 /\ gpr.lookup j 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. 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. Inde_update_store. split; trivial. unfold zero16. rewrite sign_extend_16_32'. rewrite add_neutral. apply gpr.gpr_zero_zero32. Constraint. (********************* addi t c zero16 *********************) apply semax_addiu'' with (fun s s' m h => exists C, length C = nk /\ 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 /\ gpr.lookup one s = one32 /\ gpr.lookup j 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. 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. Inde_update_store. split; trivial. split; trivial. unfold zero16. rewrite sign_extend_16_32'. rewrite add_neutral. rewrite H3; assumption. Constraint. (********************* addi bor zero zero16; ********************) apply semax_addiu'' with (fun s s' m h => exists C, length C = nk /\ 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 /\ gpr.lookup one s = one32 /\ gpr.lookup j s = zero32 /\ u2Z (gpr.lookup t s) = 4 * nc /\ gpr.lookup bor 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. 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. Inde_update_store. split; trivial. split; trivial. split; trivial. unfold zero16. rewrite sign_extend_16_32'. rewrite add_neutral. apply gpr.gpr_zero_zero32. Constraint. (********************* while_bne j k ( *********************) apply semax_strengthen_pre with (fun s s' m h => exists C, exists nj, exists nbor, length C = nk /\ 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 /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup j s) = Z_of_nat nj /\ (nj <= nk)%nat /\ u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat nj /\ u2Z (gpr.lookup bor s) = nbor /\ nbor <= 1 /\ Sum nj C = Sum nj A - Sum nj B + nbor * Zbeta nj ). red; intros. inversion_clear H as [C]. decompose [and] H0; clear H0. exists C; exists O; exists 0. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. rewrite H7. Rewrite_u2Z. auto. Constraint. split. red in Hk. red in Hk. apply le_trans with 1%nat. repeat constructor. assumption. split. rewrite Zmult_0_r. rewrite <-Zplus_0_r_reverse. assumption. split. rewrite H10. Rewrite_u2Z. auto. Constraint. simpl. omega. apply semax_weaken_post with (fun s s' m h => (exists C, exists nj, exists nbor, length C = nk /\ 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 /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup j s) = Z_of_nat nj /\ (nj <= nk)%nat /\ u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat nj /\ u2Z (gpr.lookup bor s) = nbor /\ nbor <= 1 /\ Sum nj C = Sum nj A - Sum nj B + nbor * Zbeta nj) /\ u2Z (gpr.lookup j s) = u2Z (gpr.lookup k s) ). red; intros. inversion_clear H. inversion_clear H0 as [C]. inversion_clear H as [nj]. inversion_clear H0 as [nbor]. decompose [and] H; clear H. exists C. split; trivial. split. apply my_sep_trivial with ((var_e a |--> A) ** (var_e b |--> B)). Monotony H6. Monotony H. assumption. rewrite H11. rewrite H8 in H1; rewrite H5 in H1. generalize (Z_of_nat_inj _ _ H1); clear H1; intro H1; subst nj. assumption. apply semax_while_bne with (P:=fun s s' m h => (exists C, exists nj, exists nbor, length C = nk /\ 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 /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup j s) = Z_of_nat nj /\ (nj <= nk)%nat /\ u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat nj /\ u2Z (gpr.lookup bor s) = nbor /\ nbor <= 1 /\ Sum nj C = Sum nj A - Sum nj B + nbor * Zbeta nj) ). (********************* lwxs atmp j a; ********************) apply semax_lwxs_backwards'' with (fun s s' m h => exists C, exists nj, exists nbor, length C = nk /\ 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 /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup j s) = Z_of_nat nj /\ (nj < nk)%nat /\ u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat nj /\ u2Z (gpr.lookup bor s) = nbor /\ nbor <= 1 /\ Sum nj C = Sum nj A - Sum nj B + nbor * Zbeta nj /\ gpr.lookup atmp s = nth nj A zero32 ). red; intros. inversion_clear H. inversion_clear H0 as [C]. inversion_clear H as [nj]. inversion_clear H0 as [nbor]. decompose [and] H; clear H. exists (nth nj 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 j))) s = eval (add_e (var_e a) (shl2_e (int_e (Z2u 32 (Z_of_nat nj))))) s /\ eval (add_e (add_e (var_e a) (shl2_e (var_e j))) (int_e four32)) s = eval (add_e (add_e (var_e a) (shl2_e (var_e j))) (int_e four32)) s). simpl eval. rewrite H3. split. omega. split. cutrewrite (gpr.lookup j s = Z2u 32 (Z_of_nat nj)). reflexivity. apply u2Z_injection. rewrite H8. rewrite Z2u_injection. reflexivity. generalize (min_u2Z va); intro. Constraint. reflexivity. Decompose_list_32 A nj A1 A2. lapply (mapstos_decompose_generic_P _ _ _ _ _ _ (var_e a) (add_e (var_e a) (shl2_e (var_e j))) (add_e (add_e (var_e a) (shl2_e (var_e j))) (int_e four32)) s ((var_e b |--> B) ** (var_e c |--> C)) Ha H15 H s' m h). simpl app. 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 H16. generalize (H13 (H16 H6)); clear H16 H13; intro. simpl app in H13. Monotony H13. Adjunction H13. red. exists C; exists nj; exists nbor. 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. 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. Inde_update_store. assoc_comm H13. eapply mapstos_compose_generic with (e':=add_e (var_e a) (shl2_e (var_e j))) (e'':=(add_e (add_e (var_e a) (shl2_e (var_e j))) (int_e four32))). apply Ha. apply H15. simpl. apply H. exact Htmp. assoc_comm H13. split; trivial. split; trivial. split. rewrite <-Ha. rewrite H. rewrite length_app. simpl. rewrite H15. omega. split; trivial. split; trivial. split; trivial. split; trivial. exact Htmp. rewrite Ha. omega. (********************* lwxs btmp j b; ********************) apply semax_lwxs_backwards'' with (fun s s' m h => exists C, exists nj, exists nbor, length C = nk /\ 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 /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup j s) = Z_of_nat nj /\ (nj < nk)%nat /\ u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat nj /\ u2Z (gpr.lookup bor s) = nbor /\ nbor <= 1 /\ Sum nj C = Sum nj A - Sum nj B + nbor * Zbeta nj /\ gpr.lookup atmp s = nth nj A zero32 /\ gpr.lookup btmp s = nth nj B zero32 ). red; intros. inversion_clear H as [C]. inversion_clear H0 as [nj]. inversion_clear H as [nbor]. decompose [and] H0; clear H0. 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 H1. split. omega. split. cutrewrite ((gpr.lookup j s) = (Z2u 32 (Z_of_nat nj))). reflexivity. apply u2Z_injection. rewrite H7. 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 H15 H0 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 H16. generalize (H13 (H16 H5)); clear H16 H13; intro. simpl app in H13. Monotony H13. Adjunction H13. red. exists C; exists nj; exists nbor. 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. 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. Inde_update_store. assoc_comm H13. 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 H15. simpl. apply H0. exact Htmp. simpl app. assoc_comm H13. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. exact Htmp. rewrite Hb. assumption. (********************* addu btmp' btmp bor; *********************) apply semax_addu'' with (fun s s' m h => exists C, exists nj, exists nbor, length C = nk /\ 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 /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup j s) = Z_of_nat nj /\ (nj < nk)%nat /\ u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat nj /\ u2Z (gpr.lookup bor s) = nbor /\ nbor <= 1 /\ Sum nj C = Sum nj A - Sum nj B + nbor * Zbeta nj /\ gpr.lookup atmp s = nth nj A zero32 /\ gpr.lookup btmp s = nth nj B zero32 /\ gpr.lookup btmp' s = gpr.lookup btmp s (+) gpr.lookup bor s ). red; intros. inversion_clear H as [C]. inversion_clear H0 as [nj]. inversion_clear H as [nbor]. decompose [and] H0; clear H0. red. exists C; exists nj; exists nbor. 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. 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. Inde_update_store. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. (******************** sltu u btmp' btmp; *********************) apply semax_sltu'' with (fun s s' m h => exists C, exists nj, exists nbor, length C = nk /\ 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 /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup j s) = Z_of_nat nj /\ (nj < nk)%nat /\ u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat nj /\ u2Z (gpr.lookup bor s) = nbor /\ nbor <= 1 /\ Sum nj C = Sum nj A - Sum nj B + nbor * Zbeta nj /\ gpr.lookup atmp s = nth nj A zero32 /\ gpr.lookup btmp s = nth nj B zero32 /\ gpr.lookup btmp' s = gpr.lookup btmp s (+) gpr.lookup bor s /\ gpr.lookup u s = if Zlt_bool (u2Z (gpr.lookup btmp' s)) (u2Z (gpr.lookup btmp s)) then one32 else zero32 ). red; intros. inversion_clear H as [C]. inversion_clear H0 as [nj]. inversion_clear H as [nbor]. decompose [and] H0; clear H0. red. exists C; exists nj; exists nbor. 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. 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; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. (********************* ifte_beq u, zero thendo *********************) apply semax_seq with (fun s s' m h => exists C, exists nj, exists nbor, length C = nk /\ 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 /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup j s) = Z_of_nat nj /\ (nj < nk)%nat /\ u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat nj /\ gpr.lookup atmp s = nth nj A zero32 /\ gpr.lookup btmp s = nth nj B zero32 /\ u2Z (gpr.lookup bor s) = nbor /\ nbor <= 1 /\ Sum nj C + u2Z (gpr.lookup ctmp s) * Zbeta nj = Sum nj A - Sum nj B + u2Z (nth nj A zero32) * Zbeta nj - u2Z (nth nj B zero32) * Zbeta nj + nbor * Zbeta (nj + 1) ). apply semax_ifte_beq. (* TODO: implement semax_beq'' *) (********************* (multu atmp one; ********************) apply semax_multu'' with (fun s1 s2 m h => exists C, exists nj, exists nbor, length C = nk /\ gpr.lookup a s1 = va /\ gpr.lookup b s1 = vb /\ gpr.lookup c s1 = vc /\ u2Z (gpr.lookup k s1) = Z_of_nat nk /\ (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s1 s2 m h /\ gpr.lookup one s1 = one32 /\ u2Z (gpr.lookup j s1) = Z_of_nat nj /\ (nj < nk)%nat /\ u2Z (gpr.lookup t s1) = 4 * nc + 4 * Z_of_nat nj /\ u2Z (gpr.lookup bor s1) = nbor /\ nbor <= 1 /\ Sum nj C = Sum nj A - Sum nj B + nbor * Zbeta nj /\ gpr.lookup atmp s1 = nth nj A zero32 /\ gpr.lookup btmp s1 = nth nj B zero32 /\ gpr.lookup btmp' s1 = gpr.lookup btmp s1 (+) gpr.lookup bor s1 /\ u2Z (gpr.lookup btmp' s1) = u2Z (gpr.lookup btmp s1) + nbor /\ multiplier.utoZ m = u2Z (nth nj A zero32) ). intros. inversion_clear H. inversion_clear H0 as [C]. inversion_clear H as [nj]. inversion_clear H0 as [nbor]. decompose [and] H; clear H. exists C; exists nj; exists nbor. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. Inde_mult_multu. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. rewrite H1 in H18. rewrite gpr.gpr_zero_zero32 in H18. generalize (Z_lt_ge_bool (u2Z (gpr.lookup btmp' s)) (u2Z (gpr.lookup btmp s))); intro X. inversion_clear X as [x]; destruct x. rewrite Zlt_bool_Prop in H18; auto. unfold zero32 in H18; unfold one32 in H18. assert (u2Z (Z2u 32 0) = u2Z (Z2u 32 1)). rewrite H18; reflexivity. do 2 rewrite Z2u_injection in H17. discriminate. Constraint. Constraint. Constraint. rewrite H16. Rewrite_u2Z. rewrite H11. reflexivity. apply add_le_u2Z. rewrite <-H16. omega. rewrite multiplier.multu_utoZ. rewrite H7. unfold one32. rewrite umul_1. rewrite zero_extend_u2Z_32. rewrite H14. reflexivity. (********************* msubu btmp' one; ********************) apply semax_msubu'' with (fun s1 s2 m h => exists C, exists nj, exists nbor, length C = nk /\ gpr.lookup a s1 = va /\ gpr.lookup b s1 = vb /\ gpr.lookup c s1 = vc /\ u2Z (gpr.lookup k s1) = Z_of_nat nk /\ (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s1 s2 m h /\ gpr.lookup one s1 = one32 /\ u2Z (gpr.lookup j s1) = Z_of_nat nj /\ (nj < nk)%nat /\ u2Z (gpr.lookup t s1) = 4 * nc + 4 * Z_of_nat nj /\ u2Z (gpr.lookup bor s1) = nbor /\ nbor <= 1 /\ Sum nj C = Sum nj A - Sum nj B + nbor * Zbeta nj /\ gpr.lookup atmp s1 = nth nj A zero32 /\ gpr.lookup btmp s1 = nth nj B zero32 /\ gpr.lookup btmp' s1 = gpr.lookup btmp s1 (+) gpr.lookup bor s1 /\ u2Z (gpr.lookup btmp' s1) = u2Z (gpr.lookup btmp s1) + nbor /\ ((u2Z (nth nj A zero32) >= u2Z (gpr.lookup btmp' s1) -> multiplier.utoZ m = u2Z (nth nj A zero32) - u2Z (gpr.lookup btmp' s1)) /\ ((u2Z (nth nj A zero32) < u2Z (gpr.lookup btmp' s1) -> multiplier.utoZ m = Zbeta 2 + u2Z (nth nj A zero32) - u2Z (gpr.lookup btmp' s1)) )) ). intros. inversion_clear H as [C]. inversion_clear H0 as [nj]. inversion_clear H as [nbor]. decompose [and] H0; clear H0. exists C; exists nj; exists nbor. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. Inde_mult_msubu. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. intros. rewrite multiplier.msubu_utoZ. rewrite H18. rewrite H6. unfold one32. rewrite umul_1. rewrite zero_extend_u2Z_32. reflexivity. rewrite H18. apply Zlt_trans with (Zbeta 1). apply max_u2Z_32. apply Zbeta_lt. repeat constructor. rewrite H6. unfold one32. rewrite umul_1. rewrite zero_extend_u2Z_32. rewrite H18. assumption. intros. rewrite multiplier.msubu_utoZ_overflow. rewrite H18. rewrite H6. unfold one32. rewrite umul_1. rewrite zero_extend_u2Z_32. reflexivity. rewrite H18. apply Zlt_trans with (Zbeta 1). apply max_u2Z_32. apply Zbeta_lt. repeat constructor. rewrite H6. unfold one32. rewrite umul_1. rewrite zero_extend_u2Z_32. rewrite H18. assumption. (********************* mflhxu ctmp; ********************) apply semax_mflhxu'' with (fun s1 s2 m h => exists C, exists nj, exists nbor, length C = nk /\ gpr.lookup a s1 = va /\ gpr.lookup b s1 = vb /\ gpr.lookup c s1 = vc /\ u2Z (gpr.lookup k s1) = Z_of_nat nk /\ (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s1 s2 m h /\ gpr.lookup one s1 = one32 /\ u2Z (gpr.lookup j s1) = Z_of_nat nj /\ (nj < nk)%nat /\ u2Z (gpr.lookup t s1) = 4 * nc + 4 * Z_of_nat nj /\ u2Z (gpr.lookup bor s1) = nbor /\ nbor <= 1 /\ Sum nj C = Sum nj A - Sum nj B + nbor * Zbeta nj /\ gpr.lookup atmp s1 = nth nj A zero32 /\ gpr.lookup btmp s1 = nth nj B zero32 /\ gpr.lookup btmp' s1 = gpr.lookup btmp s1 (+) gpr.lookup bor s1 /\ u2Z (gpr.lookup btmp' s1) = u2Z (gpr.lookup btmp s1) + nbor /\ ((u2Z (nth nj A zero32) >= u2Z (gpr.lookup btmp' s1) -> (u2Z (gpr.lookup ctmp s1) = u2Z (nth nj A zero32) - u2Z (gpr.lookup btmp' s1) /\ Sum nj C + u2Z (gpr.lookup ctmp s1) * Zbeta nj = Sum nj A - Sum nj B + u2Z (nth nj A zero32) * Zbeta nj - u2Z (nth nj B zero32) * Zbeta nj) ) /\ (u2Z (nth nj A zero32) < u2Z (gpr.lookup btmp' s1) -> (u2Z (gpr.lookup ctmp s1) = Zbeta 1 + u2Z (nth nj A zero32) - u2Z (gpr.lookup btmp' s1) /\ Sum nj C + u2Z (gpr.lookup ctmp s1) * Zbeta nj = Sum nj A - Sum nj B + u2Z (nth nj A zero32) * Zbeta nj - u2Z (nth nj B zero32) * Zbeta nj + Zbeta (nj+1)))) ). red; intros. inversion_clear H as [C]. inversion_clear H0 as [nj]. inversion_clear H as [nbor]. decompose [and] H0; clear H0. red. exists C; exists nj; exists nbor. 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. 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. Inde_update_store. Inde_mult_mflhxu_op. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. clear H19; intro X; generalize (H17 X); clear H17; intro. assert ( multiplier.utoZ m < Zbeta 1). rewrite H0. generalize (max_u2Z_32 (nth nj A zero32)); intro. generalize (min_u2Z (gpr.lookup btmp' s)); intro. omega. generalize ( multiplier.utoZ_lo_beta1 _ H17); intro Y; decompose [and] Y; clear Y. rewrite H21 in H0. split; trivial. rewrite H0. rewrite H16. rewrite H14. rewrite H12. ring. clear H17; intro X; generalize (H19 X); clear H19; intro. assert ( multiplier.acx m = Z2u multiplier.acx_size 0 ). apply multiplier.utoZ_acx_beta2. rewrite H0. omega. rewrite multiplier.utoZ_def in H0. rewrite H17 in H0; clear H17. rewrite Z2u_injection in H0. rewrite Zmult_0_l in H0. rewrite <-Zplus_0_r_reverse in H0. cutrewrite (Zbeta 2 = Zbeta 1 * (Zbeta 1 - 1) + Zbeta 1) in H0. lapply (coeff_unique (u2Z (multiplier.hi m)) (u2Z (multiplier.lo m)) (Zbeta 1 - 1) (Zbeta 1 + u2Z (nth nj A zero32) - u2Z (gpr.lookup btmp' s)) (Zbeta 1)). intro. assert (u2Z (multiplier.hi m) * Zbeta 1 + u2Z (multiplier.lo m) = (Zbeta 1 - 1) * Zbeta 1 + (Zbeta 1 + u2Z (nth nj A zero32) - u2Z (gpr.lookup btmp' s))). rewrite Zplus_comm. rewrite H0. ring. generalize (H17 H18); clear H17 H18; intro. inversion_clear H17. split; trivial. rewrite H12. rewrite H19. rewrite Zbeta_is_exp. rewrite H16. rewrite H14. ring. split. (*TODO: constraint should do that*) split. apply min_u2Z. apply max_u2Z_32. split. split. apply min_u2Z. apply max_u2Z_32. split. split. unfold Zbeta. simpl. Constraint. unfold Zbeta. simpl. Constraint. generalize (min_u2Z (nth nj A zero32)); intro. generalize (max_u2Z_32 (gpr.lookup btmp' s)); intro. omega. ring. Constraint. (********************* sltu u atmp btmp'; *********************) apply semax_sltu'' with (fun s1 s2 m h => exists C, exists nj, exists nbor, length C = nk /\ gpr.lookup a s1 = va /\ gpr.lookup b s1 = vb /\ gpr.lookup c s1 = vc /\ u2Z (gpr.lookup k s1) = Z_of_nat nk /\ (((var_e a |--> A) ** (var_e b |--> B)) ** (var_e c |--> C)) s1 s2 m h /\ gpr.lookup one s1 = one32 /\ u2Z (gpr.lookup j s1) = Z_of_nat nj /\ (nj < nk)%nat /\ u2Z (gpr.lookup t s1) = 4 * nc + 4 * Z_of_nat nj /\ u2Z (gpr.lookup bor s1) = nbor /\ nbor <= 1 /\ gpr.lookup atmp s1 = nth nj A zero32 /\ gpr.lookup btmp s1 = nth nj B zero32 /\ gpr.lookup btmp' s1 = gpr.lookup btmp s1 (+) gpr.lookup bor s1 /\ u2Z (gpr.lookup btmp' s1) = u2Z (gpr.lookup btmp s1) + nbor /\ (u2Z (nth nj A zero32) >= u2Z (gpr.lookup btmp' s1) -> u2Z (gpr.lookup ctmp s1) = u2Z (nth nj A zero32) - u2Z (gpr.lookup btmp' s1) /\ Sum nj C + u2Z (gpr.lookup ctmp s1) * Zbeta nj = Sum nj A - Sum nj B + u2Z (nth nj A zero32) * Zbeta nj - u2Z (nth nj B zero32) * Zbeta nj) /\ (u2Z (nth nj A zero32) < u2Z (gpr.lookup btmp' s1) -> u2Z (gpr.lookup ctmp s1) = Zbeta 1 + u2Z (nth nj A zero32) - u2Z (gpr.lookup btmp' s1) /\ Sum nj C + u2Z (gpr.lookup ctmp s1) * Zbeta nj = Sum nj A - Sum nj B + u2Z (nth nj A zero32) * Zbeta nj - u2Z (nth nj B zero32) * Zbeta nj + Zbeta (nj + 1)) /\ gpr.lookup u s1 = (if (Zlt_bool (u2Z (gpr.lookup atmp s1)) (u2Z (gpr.lookup btmp' s1))) then one32 else zero32) ). red; intros. inversion_clear H as [C]. inversion_clear H0 as [nj]. inversion_clear H as [nbor]. decompose [and] H0; clear H0. red. exists C; exists nj; exists nbor. 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. 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]. 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. split; trivial. split; trivial. (********************* ifte_beq u, gpr_zero thendo *********************) apply semax_ifte_beq. (********************* addiu bor gpr_zero zero16 *********************) apply semax_addiu'. red; intros. inversion_clear H. inversion_clear H0 as [C]. inversion_clear H as [nj]. inversion_clear H0 as [nbor]. decompose [and] H; clear H. red. exists C; exists nj; exists 0. 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. 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. Inde_update_store. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. Rewrite_u2Z. reflexivity. Constraint. Constraint. Constraint. split. Constraint. simpl. rewrite <-Zplus_0_r_reverse. rewrite H1 in H20. rewrite gpr.gpr_zero_zero32 in H20. assert (u2Z (gpr.lookup btmp' s) <= u2Z (gpr.lookup atmp s) ). generalize (Z_le_gt_dec (u2Z (gpr.lookup btmp' s)) (u2Z (gpr.lookup atmp s))); intro _X; inversion_clear _X. assumption. lapply (Zlt_bool_Prop (u2Z (gpr.lookup atmp s)) (u2Z (gpr.lookup btmp' s))). intro. rewrite H19 in H20. assert (zero32 <> one32). unfold zero32; unfold one32. apply Z2u_dis. Constraint. Constraint. intro; discriminate. tauto. omega. rewrite H13 in H. lapply H17. intros. inversion_clear H19. assumption. omega. (********************* addiu bor one one16 *********************) apply semax_addiu'. red; intros. inversion_clear H. inversion_clear H0 as [C]. inversion_clear H as [nj]. inversion_clear H0 as [nbor]. decompose [and] H; clear H. red. exists C; exists nj; exists 1. 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. 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. Inde_update_store. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. Rewrite_u2Z. reflexivity. Constraint. Constraint. Constraint. split. apply Zle_refl. assert (u2Z (gpr.lookup atmp s) < u2Z (gpr.lookup btmp' s)). generalize (Z_le_gt_dec (u2Z (gpr.lookup btmp' s)) (u2Z (gpr.lookup atmp s))); intro _X; inversion_clear _X. lapply (Zlt_bool_Prop' (u2Z (gpr.lookup btmp' s)) (u2Z (gpr.lookup atmp s))). intro. rewrite H19 in H20. rewrite H20 in H1. rewrite gpr.gpr_zero_zero32 in H1. tauto. omega. omega. rewrite H13 in H. generalize (H18 H); intro. inversion_clear H19. rewrite Zmult_1_l. assumption. (********************* addiu ctmp atmp zero16); ********************) apply semax_addiu'. (* we are in the branch where btmp' = btmp + bor has overflowed *) red; intros. inversion_clear H. inversion_clear H0 as [C]. inversion_clear H as [nj]. inversion_clear H0 as [nbor]. decompose [and] H; clear H. red. exists C; exists nj; exists nbor. 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. 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. Inde_update_store. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. assert (nbor = 1 /\ u2Z (nth nj B zero32) = Zbeta 1 - 1). assert ( gpr.lookup u s = one32 \/ gpr.lookup u s = zero32 ). destruct Zlt_bool; auto. inversion_clear H. assert ( u2Z (gpr.lookup btmp' s) < u2Z (gpr.lookup btmp s) ). generalize (Z_le_gt_dec (u2Z (gpr.lookup btmp s)) (u2Z (gpr.lookup btmp' s))); intro _X; inversion_clear _X. lapply (Zlt_bool_Prop' (u2Z (gpr.lookup btmp s)) (u2Z (gpr.lookup btmp' s))). intro. rewrite H19 in H18. rewrite H18 in H17. assert (zero32 <> one32 ). unfold zero32; unfold one32. apply Z2u_dis. Constraint. Constraint. intro; discriminate. tauto. omega. omega. rewrite H15 in H. rewrite H16 in H. rewrite H15 in H. generalize (add_lt_u2Z_overflow _ _ _ H); intro. rewrite <-Zbeta_power1 in H19. generalize (max_u2Z_32' (nth nj B zero32)); intro. generalize (min_u2Z (nth nj B zero32)); intro. generalize (min_u2Z (gpr.lookup bor s)); intro. omega. rewrite H17 in H1. rewrite gpr.gpr_zero_zero32 in H1. tauto. split; intuition. cutrewrite ( u2Z (gpr.lookup atmp s (+) sign_extend_16_32 zero16) = u2Z (gpr.lookup atmp s) ). rewrite H13. rewrite H19. rewrite H17. repeat rewrite Zmult_1_l. rewrite H14. rewrite Zbeta_is_exp. ring. unfold sign_extend_16_32. unfold zero16. rewrite sign_extend_Z2u. simpl plus. rewrite add_neutral. reflexivity. repeat constructor. Constraint. (********************* sw ctmp zero16 t; *********************) apply semax_sw_backwards'' with (fun s s' m h => exists C, exists nj, exists nbor, length C = nk /\ 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 /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup j s) = Z_of_nat nj /\ (nj < nk)%nat /\ u2Z (gpr.lookup t s) = 4 * nc + 4 * Z_of_nat nj /\ u2Z (gpr.lookup bor s) = nbor /\ nbor <= 1 /\ Sum (nj+1) C = Sum (nj+1) A - Sum (nj+1) B + nbor * Zbeta (nj+1) /\ gpr.lookup atmp s = nth nj A zero32 /\ gpr.lookup btmp s = nth nj B zero32 ). red; intros. inversion_clear H as [C]. inversion_clear H0 as [nj]. inversion_clear H as [nbor]. decompose [and] H0; clear H0. exists (int_e (nth nj C zero32)). assert (Htmp : u2Z (eval (var_e c) s) + 4 * Z_of_nat nk < Zbeta 1 /\ eval (add_e (var_e t) (int_e (sign_extend_16_32 zero16))) s = eval (add_e (var_e c) (shl2_e (int_e (Z2u 32 (Z_of_nat nj))))) s /\ eval (add_e (add_e (var_e t) (int_e (sign_extend_16_32 zero16))) (int_e four32)) s = eval (add_e (add_e (var_e t) (int_e (sign_extend_16_32 zero16))) (int_e four32)) s). simpl eval. rewrite H3. split. Constraint. split. unfold zero16. unfold sign_extend_16_32. rewrite sign_extend_Z2u. simpl plus. rewrite add_neutral. apply u2Z_injection. rewrite H9. symmetry. Rewrite_u2Z. rewrite Hvc; ring. generalize (min_u2Z va); intro. Constraint. generalize (min_u2Z va); intro. Constraint. generalize (min_u2Z va); intro. Constraint. Constraint. generalize (min_u2Z va); intro. Constraint. generalize (min_u2Z va); intro. Constraint. generalize (min_u2Z va); intro. Constraint. repeat constructor. Constraint. reflexivity. Decompose_list_32 C nj lst1 lst2. lapply (mapstos_decompose_generic_P _ _ _ _ _ _ (var_e c) (add_e (var_e t) (int_e (sign_extend_16_32 zero16))) (add_e (add_e (var_e t) (int_e (sign_extend_16_32 zero16))) (int_e four32)) s ((var_e b |--> B) ** (var_e a |--> A)) H H16 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 H17. generalize (H14 (H17 H5)); clear H14 H17; intro. simpl app in H14. Monotony H14. Adjunction H14. exists (update_list C nj (gpr.lookup ctmp s)). exists nj. exists nbor. split. apply length_update_list; auto. split; trivial. split; trivial. split; trivial. split; trivial. split. assoc_comm H14. eapply mapstos_compose_generic with (lst2:=lst2) (w:=gpr.lookup ctmp s) (e':=add_e (var_e t) (int_e (sign_extend_16_32 zero16))) (e'':=add_e (add_e (var_e t) (int_e (sign_extend_16_32 zero16))) (int_e four32)). apply length_update_list. apply H. apply H16. rewrite H0. rewrite update_list_app. simpl. rewrite H16. rewrite <-minus_n_n. reflexivity. rewrite H16. constructor. exact Htmp. assoc_comm H14. generalize H14; clear H14. apply mapsto_ext'. reflexivity. simpl. reflexivity. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. assert (C = (lst1 ++ nth nj C zero32 :: nil) ++ lst2). rewrite app_ass. exact H0. rewrite H17; clear H17. rewrite update_list_app'. rewrite update_list_app. rewrite H16. rewrite <-minus_n_n. simpl update_list. rewrite <-Sum_beyond. rewrite (Sum_cut nj lst1 H16 (nj+1) ((lst1 ++ gpr.lookup ctmp s :: nil)) (gpr.lookup ctmp s :: nil)). cutrewrite (nj+1-nj=1)%nat. simpl Sum. rewrite H0 in H15. rewrite <-Sum_beyond in H15. rewrite Zmult_comm. rewrite H15. Decompose_list_32 A nj A1 A2. pattern A at 3. assert (A = (A1 ++ nth nj A zero32 :: nil) ++ A2). rewrite app_ass. assumption. rewrite H18. rewrite <-Sum_beyond. rewrite (Sum_cut nj A1 H19 (nj+1) ((A1 ++ nth nj A zero32 :: nil)) (nth nj A zero32 :: nil)). cutrewrite (nj+1-nj=1)%nat. simpl Sum. Decompose_list_32 B nj B1 B2. pattern B at 3. assert (B = (B1 ++ nth nj B zero32 :: nil) ++ B2). rewrite app_ass. assumption. rewrite H21. rewrite <-Sum_beyond. rewrite (Sum_cut nj B1 H22 (nj+1) ((B1 ++ nth nj B zero32 :: nil)) (nth nj B zero32 :: nil)). cutrewrite (nj+1-nj=1)%nat. simpl Sum. ring. rewrite H20. rewrite <-Sum_beyond. rewrite H17. rewrite <-Sum_beyond. ring. assumption. assumption. apply minus_plus. rewrite length_app; simpl; auto. reflexivity. rewrite length_app; simpl; auto. rewrite Hb. assumption. apply minus_plus. rewrite length_app; simpl; auto. reflexivity. rewrite length_app; simpl; auto. rewrite Ha. assumption. assumption. apply minus_plus. rewrite length_app; simpl; auto. reflexivity. rewrite length_app; simpl; auto. rewrite H16. constructor. rewrite length_app; rewrite H16; simpl. omega. split; trivial. exact Htmp. rewrite H. assumption. (********************* addiu t t four16; *********************) apply semax_addiu'' with (fun s s' m h => exists C, exists nj, exists nbor, length C = nk /\ 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 /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup j s) = Z_of_nat nj /\ (nj < nk)%nat /\ u2Z (gpr.lookup t s) = 4 * nc + 4 * (Z_of_nat nj + 1) /\ u2Z (gpr.lookup bor s) = nbor /\ nbor <= 1 /\ Sum (nj+1) C = Sum (nj+1) A - Sum (nj+1) B + nbor * Zbeta (nj+1) /\ gpr.lookup atmp s = nth nj A zero32 /\ gpr.lookup btmp s = nth nj B zero32 ). red; intros. inversion_clear H as [C]. inversion_clear H0 as [nj]. inversion_clear H as [nbor]. decompose [and] H0; clear H0. red. exists C; exists nj; exists nbor. 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. Inde_update_store. split; trivial. split; trivial. split; trivial. split. Rewrite_u2Z. rewrite H9. ring. Constraint. Constraint. Constraint. split; trivial. split; trivial. split; trivial. split; trivial. (********************* addiu j j one16 *********************) apply semax_addiu'. red; intros. inversion_clear H as [C]. inversion_clear H0 as [nj]. inversion_clear H as [nbor]. decompose [and] H0; clear H0. red. exists C; exists (S nj); exists nbor. 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. Inde_update_store. split; trivial. split. Rewrite_u2Z. rewrite Z_S. rewrite H7; ring. Constraint. generalize (min_u2Z va); intro. Constraint. Constraint. split. omega. split. rewrite Z_S. assumption. split; trivial. split; trivial. cutrewrite (S nj = nj + 1)%nat. assumption. ring. Qed.