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. Require Import mont. Open Local Scope asm_heap_scope. Open Local Scope mips_scope. Open Local Scope Z_scope. (*********************** specification of the montgomery function (part I) ******************************************) Lemma montgomery_specif : forall nk (Hk:(nk > O)%nat) nx ny nm nz (Hnx:4*nx+4*Z_of_nat nk exists Z, length Z = nk /\ list_of_zeros Z /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m_ h /\ multiplier.is_null m_ }} montgomery k alpha x y z m int_ ext X_ Y_ M_ Z_ one gpr_zero quot C t s {{ fun s s' m_ h => exists Z, length Z = nk /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m_ h /\ Zbeta nk * Sum (nk+1) (Z ++ gpr.lookup C s::nil) == Sum nk X * Sum nk Y [[ Sum nk M ]] /\ Sum (nk+1) (Z ++ gpr.lookup C s::nil) < 2 * Sum nk M }}. intros. generalize (min_u2Z vx); intro Hx_pos. generalize (min_u2Z vy); intro Hy_pos. generalize (min_u2Z vz); intro Hz_pos. generalize (min_u2Z vm); intro Hm_pos. unfold montgomery. (********************* addiu one zero one16; ********************) apply semax_addiu'' with (fun s s' m_ h => exists Z, length Z = nk /\ list_of_zeros Z /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m_ h /\ multiplier.is_null m_ /\ gpr.lookup one s = one32 ). red; intros. inversion_clear H as [Z]. decompose [and] H0; clear H0. red. exists Z. split; trivial. 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; trivial. split; trivial. split. Inde_update_store. split; trivial. apply u2Z_injection. Rewrite_u2Z. reflexivity. Constraint. Constraint. Constraint. Constraint. (********************* addiu C zero zero16; ********************) apply semax_addiu'' with (fun s s' m_ h => exists Z, length Z = nk /\ list_of_zeros Z /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m_ h /\ multiplier.is_null m_ /\ gpr.lookup one s = one32 /\ gpr.lookup C s = zero32 ). red; intros. inversion_clear H as [Z]. decompose [and] H0; clear H0. red. exists Z. split; trivial. 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; trivial. split; trivial. split. Inde_update_store. split; trivial. split; trivial. apply u2Z_injection. Rewrite_u2Z. reflexivity. Constraint. Constraint. Constraint. Constraint. (********************* addiu ext zero zero16; ********************) apply semax_addiu'' with (fun s s' m_ h => exists Z, length Z = nk /\ list_of_zeros Z /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m_ h /\ multiplier.is_null m_ /\ gpr.lookup one s = one32 /\ gpr.lookup C s = zero32 /\ gpr.lookup ext s = zero32 ). red; intros. inversion_clear H as [Z]. decompose [and] H0; clear H0. red. exists Z. split; trivial. 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; trivial. split; trivial. split. Inde_update_store. split; trivial. split; trivial. split; trivial. apply u2Z_injection. Rewrite_u2Z. reflexivity. Constraint. Constraint. Constraint. Constraint. (********************* while_bne ext k ********************) apply semax_strengthen_pre with (fun s s' m_ h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m_ h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ u2Z (gpr.lookup ext s) <= u2Z (gpr.lookup k s) /\ gpr.lookup one s = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) ). red; intros. inversion_clear H as [Z]. decompose [and] H0; clear H0. exists Z. exists O. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. rewrite H13. Rewrite_u2Z. reflexivity. Constraint. split. rewrite H13; rewrite H6. Rewrite_u2Z. Constraint. Constraint. split; trivial. exists 0. rewrite H11. rewrite Sum_list_of_zeros. split. reflexivity. simpl Sum. assert (0 < Sum nk M). apply Zle_lt_trans with (Sum nk X). apply Sum_pos. assumption. unfold Zbeta. simpl Zpower. omega. apply list_of_zeros_app. assumption. unfold zero32. unfold list_of_zeros. reflexivity. apply semax_weaken_post with (fun s s' m_ h => (exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m_ h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ u2Z (gpr.lookup ext s) <= u2Z (gpr.lookup k s) /\ gpr.lookup one s = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) ) /\ u2Z (gpr.lookup ext s) = u2Z (gpr.lookup k s) ). red; intros. inversion_clear H. inversion_clear H0 as [Z]. inversion_clear H as [next]. decompose [and] H0; clear H0. exists Z. split; trivial. split; trivial. assert (nk = next). omega. subst next. inversion_clear H13 as [K]. inversion_clear H0. split. exists K; trivial. apply Zmult_gt_0_lt_reg_r with (Zbeta nk). generalize (Zbeta_1 nk); intro. omega. rewrite Zmult_comm. rewrite H12. assumption. apply semax_while_bne with (P := fun s s' m_ h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m_ h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ u2Z (gpr.lookup ext s) <= u2Z (gpr.lookup k s) /\ gpr.lookup one s = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) ). (********************* lwxs X ext x; ********************) apply semax_lwxs_backwards''2 with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ u2Z (gpr.lookup ext s) < u2Z (gpr.lookup k s) /\ gpr.lookup one s = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 ). red; intros. inversion_clear H. inversion_clear H0 as [Z]. inversion_clear H as [next]. decompose [and] H0; clear H0. exists (nth next X zero32). split. Decompose_list_32 X next X1 X2. lapply (mapstos_decompose_generic_P _ _ _ _ _ _ (var_e x) (add_e (var_e x) (shl2_e (var_e ext))) (add_e (add_e (var_e x) (shl2_e (var_e ext))) (int_e four32)) s ((((var_e y |--> Y)) ** (var_e z |--> Z)) ** (var_e mont.m |--> M)) Hx H14 H0 s' m h). intro. simpl app in H12. assert ( ((var_e x |--> X) ** (((var_e y |--> Y) ** (var_e z |--> Z)) ** (var_e mont.m |--> M))) s s' m h ). assoc_comm H8. assumption. generalize (H12 H15); clear H12 H15; intro. apply my_sep_trivial with ( ((var_e x |--> X1) ** (add_e (add_e (var_e x) (shl2_e (var_e ext))) (int_e four32) |--> X2)) ** (((var_e y |--> Y) ** (var_e z |--> Z)) ** (var_e mont.m |--> M)) ). assoc_comm H12. assumption. simpl eval. split. rewrite H3. Constraint. split. cutrewrite ( gpr.lookup ext s = Z2u 32 (Z_of_nat next) ). reflexivity. apply u2Z_injection. rewrite H9. rewrite Z2u_injection. reflexivity. Constraint. reflexivity. rewrite Hx. apply Z_of_nat_lt_inj. omega. red. exists Z; exists next. split; 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. 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; trivial. split. Inde_update_store. split; trivial. split. omega. split; trivial. split; trivial. split. omega. reflexivity. (********************* lw Y zero16 y; *********************) apply semax_lw_backwards''2 with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ u2Z (gpr.lookup ext s) < u2Z (gpr.lookup k s) /\ gpr.lookup one s = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ gpr.lookup Y_ s = nth O Y zero32 ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. destruct Y as [_ | hdy tly]. simpl in Hy; rewrite <-Hy in Hk; inversion Hk. exists hdy. split. Decompose_sepcon H7 h1 h2. Decompose_sepcon H13 h11 h12. Decompose_sepcon H16 h111 h112. simpl in H23. Decompose_sepcon H23 h1121 h1122. Compose_sepcon h1121 (h1122 +++ h111 +++ h12 +++ h2). eapply mapsto_equiv'. apply H23. simpl eval. rewrite H1. apply u2Z_injection. Rewrite_u2Z. ring. Constraint. Constraint. Constraint. reflexivity. red; auto. red. exists Z; exists next. 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; trivial. split; trivial. split. Inde_update_store. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. (********************* lw Z_ zero16 z; *********************) apply semax_lw_backwards''2 with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ u2Z (gpr.lookup ext s) < u2Z (gpr.lookup k s) /\ gpr.lookup one s = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ gpr.lookup Y_ s = nth O Y zero32 /\ gpr.lookup Z_ s = nth O Z zero32 ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. destruct Z as [_ | hdz tlz]. simpl in H0; rewrite <-H0 in Hk; inversion Hk. exists hdz. split. Decompose_sepcon H7 h1 h2. Decompose_sepcon H14 h11 h12. simpl in H21. Decompose_sepcon H21 h121 h122. Compose_sepcon h121 (h122 +++ h11 +++ h2). eapply mapsto_equiv'. apply H21. simpl eval. rewrite H3. apply u2Z_injection. Rewrite_u2Z. ring. Constraint. Constraint. Constraint. reflexivity. red; auto. red. exists (hdz::tlz); exists next. 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. rewrite gpr.lookup_update'; [idtac | apply gp_reg_beq_false; auto]. split; trivial. 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. (********************* multu X Y; ********************) apply semax_multu'' with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((((var_e x |--> X) ** (var_e y |--> Y)) ** (var_e z |--> Z)) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ u2Z (gpr.lookup ext s) < u2Z (gpr.lookup k s) /\ gpr.lookup one s = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ gpr.lookup Y_ s = nth O Y zero32 /\ gpr.lookup Z_ s = nth O Z zero32 /\ multiplier.utoZ m0 <= (Zbeta 1 - 1) * (Zbeta 1 - 1) /\ multiplier.utoZ m0 = u2Z (nth next X zero32) * u2Z (nth O Y zero32) ). intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. exists Z; exists next. split; trivial. split; trivial. 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. rewrite multiplier.multu_utoZ. apply max_u2Z_umul_32. rewrite multiplier.multu_utoZ. rewrite umul_u2Z_32. rewrite H13; rewrite H14. reflexivity. (********************* lw M zero16 m; ********************) apply semax_lw_backwards''2 with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ u2Z (gpr.lookup ext s) < u2Z (gpr.lookup k s) /\ gpr.lookup one s = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ gpr.lookup Y_ s = nth O Y zero32 /\ gpr.lookup Z_ s = nth O Z zero32 /\ multiplier.utoZ m0 <= (Zbeta 1 - 1) * (Zbeta 1 - 1) /\ multiplier.utoZ m0 = u2Z (nth next X zero32) * u2Z (nth O Y zero32) /\ gpr.lookup M_ s = nth O M zero32 ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. destruct M as [_ | hdm tlm]. simpl in Hm; rewrite <- Hm in Hk; inversion_clear Hk. exists hdm. split. Decompose_sepcon H7 h1 h2. simpl in H21. Decompose_sepcon H21 h21 h22. Compose_sepcon h21 (h22 +++ h1). eapply mapsto_equiv'. apply H21. simpl eval. rewrite H4. apply u2Z_injection. Rewrite_u2Z. ring. Constraint. Constraint. Constraint. reflexivity. red; auto. red. exists Z; exists next. 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; 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. (********************* maddu Z_ one; ********************) apply semax_maddu'' with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ u2Z (gpr.lookup ext s) < u2Z (gpr.lookup k s) /\ gpr.lookup one s = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ gpr.lookup Y_ s = nth O Y zero32 /\ gpr.lookup Z_ s = nth O Z zero32 /\ multiplier.utoZ m0 <= Zbeta 1 * (Zbeta 1 - 1) /\ multiplier.utoZ m0 = u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\ gpr.lookup M_ s = nth O M zero32 ). intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. exists Z; exists next. assert (Htmp : multiplier.utoZ m < Zbeta 2 * (Zpower 2 multiplier.acx_size - 1)). apply Zle_lt_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1)). assumption. apply Zlt_le_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; trivial. split. Inde_mult_maddu. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. rewrite multiplier.maddu_utoZ. rewrite H15; rewrite H10. unfold one32. rewrite umul_1. rewrite zero_extend_u2Z_32. apply Zle_trans with ((Zbeta 1 - 1) + (Zbeta 1 - 1) * (Zbeta 1 - 1)). apply Zplus_le_compat. apply max_u2Z_32'. rewrite H17. rewrite <-umul_u2Z. apply max_u2Z_umul_32. simpl. Constraint_constant. exact Htmp. split; trivial. rewrite multiplier.maddu_utoZ. rewrite H15; rewrite H10. unfold one32; rewrite umul_1. rewrite zero_extend_u2Z_32. rewrite H17. apply Zplus_comm. exact Htmp. (********************* mflo t; ********************) apply semax_mflo'' with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ u2Z (gpr.lookup ext s) < u2Z (gpr.lookup k s) /\ gpr.lookup one s = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ gpr.lookup Y_ s = nth O Y zero32 /\ gpr.lookup Z_ s = nth O Z zero32 /\ multiplier.utoZ m0 <= Zbeta 1 * (Zbeta 1 - 1) /\ multiplier.utoZ m0 = u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\ gpr.lookup M_ s = nth O M zero32 /\ gpr.lookup t s = rem 32 ((umul (nth next X zero32) (nth O Y zero32)) (+) (zero_extend 32 (nth O Z zero32))) ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. red. exists Z; exists next. 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. 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; 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. apply multiplier.lo_remainder. rewrite <-plus_assoc. rewrite (plus_comm multiplier.acx_size). apply le_plus_trans. constructor. rewrite H17. symmetry. Rewrite_u2Z. rewrite zero_extend_u2Z_32. reflexivity. rewrite zero_extend_u2Z_32. rewrite Zpower_is_exp. rewrite <-Zbeta_power1. rewrite <-Zbeta_is_exp. simpl plus. apply Zle_lt_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1) + (Zbeta 1 - 1)). apply Zplus_le_compat. rewrite <-umul_u2Z. apply max_u2Z_umul_32. apply max_u2Z_32'. unfold Zbeta. simpl. Constraint_constant. (********************* mfhi s; ********************) apply semax_mfhi'' with (fun s0 s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s0 = vx /\ gpr.lookup y s0 = vy /\ gpr.lookup z s0 = vz /\ gpr.lookup m s0 = vm /\ u2Z (gpr.lookup k s0) = Z_of_nat nk /\ gpr.lookup alpha s0 = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s0 s' m0 h /\ u2Z (gpr.lookup ext s0) = Z_of_nat next /\ u2Z (gpr.lookup ext s0) < u2Z (gpr.lookup k s0) /\ gpr.lookup one s0 = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s0)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s0 = nth next X zero32 /\ gpr.lookup Y_ s0 = nth O Y zero32 /\ gpr.lookup Z_ s0 = nth O Z zero32 /\ multiplier.utoZ m0 <= Zbeta 1 * (Zbeta 1 - 1) /\ multiplier.utoZ m0 = u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\ gpr.lookup M_ s0 = nth O M zero32 /\ gpr.lookup t s0 = rem 32 ((umul (nth next X zero32) (nth O Y zero32)) (+) (zero_extend 32 (nth O Z zero32))) /\ u2Z (gpr.lookup s s0 ||| gpr.lookup t s0) = u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. exists Z; exists next. 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. 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; 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. rewrite H20. reflexivity. assert (multiplier.lo m = gpr.lookup t s). rewrite H20. apply multiplier.lo_remainder. rewrite <-plus_assoc. rewrite (plus_comm multiplier.acx_size). apply le_plus_trans. constructor. rewrite H17. symmetry. Rewrite_u2Z. rewrite zero_extend_u2Z_32. reflexivity. rewrite zero_extend_u2Z_32. rewrite Zpower_is_exp. rewrite <-Zbeta_power1. rewrite <-Zbeta_is_exp. simpl plus. apply Zle_lt_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1) + (Zbeta 1 - 1)). apply Zplus_le_compat. rewrite <-umul_u2Z. apply max_u2Z_umul_32. apply max_u2Z_32'. unfold Zbeta. simpl. Constraint_constant. rewrite <-H. rewrite concat_u2Z. rewrite multiplier.utoZ_def in H17. rewrite <-Zbeta_power1. rewrite multiplier.utoZ_acx_beta2 in H17. rewrite Z2u_injection in H17. rewrite <-H17. ring. Constraint. apply Zle_lt_trans with (Zbeta 1 * (Zbeta 1 - 1)). assumption. unfold Zbeta. simpl. Constraint_constant. (********************* multu t alpha; *********************) apply semax_multu'' with (fun s0 s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s0 = vx /\ gpr.lookup y s0 = vy /\ gpr.lookup z s0 = vz /\ gpr.lookup m s0 = vm /\ u2Z (gpr.lookup k s0) = Z_of_nat nk /\ gpr.lookup alpha s0 = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s0 s' m0 h /\ u2Z (gpr.lookup ext s0) = Z_of_nat next /\ u2Z (gpr.lookup ext s0) < u2Z (gpr.lookup k s0) /\ gpr.lookup one s0 = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s0)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s0 = nth next X zero32 /\ gpr.lookup Y_ s0 = nth O Y zero32 /\ gpr.lookup Z_ s0 = nth O Z zero32 /\ multiplier.utoZ m0 <= (Zbeta 1 - 1) * (Zbeta 1 - 1) /\ gpr.lookup M_ s0 = nth O M zero32 /\ gpr.lookup t s0 = rem 32 ((umul (nth next X zero32) (nth O Y zero32)) (+) (zero_extend 32 (nth O Z zero32))) /\ u2Z ((gpr.lookup s s0) ||| (gpr.lookup t s0)) = u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\ multiplier.utoZ m0 = u2Z (gpr.lookup t s0) * u2Z (gpr.lookup alpha s0) ). intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. exists Z; exists next. split; trivial. split; trivial. 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. rewrite multiplier.multu_utoZ. apply max_u2Z_umul_32. split; trivial. split; trivial. split; trivial. rewrite multiplier.multu_utoZ. rewrite <-umul_u2Z. reflexivity. (********************* addiu int_ zero one16; ********************) apply semax_addiu'' with (fun s0 s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s0 = vx /\ gpr.lookup y s0 = vy /\ gpr.lookup z s0 = vz /\ gpr.lookup m s0 = vm /\ u2Z (gpr.lookup k s0) = Z_of_nat nk /\ gpr.lookup alpha s0 = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s0 s' m0 h /\ u2Z (gpr.lookup ext s0) = Z_of_nat next /\ u2Z (gpr.lookup ext s0) < u2Z (gpr.lookup k s0) /\ gpr.lookup one s0 = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s0)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s0 = nth next X zero32 /\ gpr.lookup Y_ s0 = nth O Y zero32 /\ gpr.lookup Z_ s0 = nth O Z zero32 /\ multiplier.utoZ m0 <= (Zbeta 1 - 1) * (Zbeta 1 - 1) /\ gpr.lookup M_ s0 = nth O M zero32 /\ gpr.lookup t s0 = rem 32 ((umul (nth next X zero32) (nth O Y zero32)) (+) (zero_extend 32 (nth O Z zero32))) /\ u2Z ((gpr.lookup s s0) ||| (gpr.lookup t s0)) = u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\ multiplier.utoZ m0 = u2Z (gpr.lookup t s0) * u2Z (gpr.lookup alpha s0) /\ gpr.lookup int_ s0 = one32 ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. red. exists Z; exists next. 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. 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; 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. split; trivial. apply u2Z_injection. Rewrite_u2Z. reflexivity. Constraint. Constraint. Constraint. Constraint. (********************* mflo quot; ********************) apply semax_mflo'' with (fun s0 s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s0 = vx /\ gpr.lookup y s0 = vy /\ gpr.lookup z s0 = vz /\ gpr.lookup m s0 = vm /\ u2Z (gpr.lookup k s0) = Z_of_nat nk /\ gpr.lookup alpha s0 = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s0 s' m0 h /\ u2Z (gpr.lookup ext s0) = Z_of_nat next /\ u2Z (gpr.lookup ext s0) < u2Z (gpr.lookup k s0) /\ gpr.lookup one s0 = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s0)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s0 = nth next X zero32 /\ gpr.lookup Y_ s0 = nth O Y zero32 /\ gpr.lookup Z_ s0 = nth O Z zero32 /\ multiplier.utoZ m0 <= (Zbeta 1 - 1) * (Zbeta 1 - 1) /\ gpr.lookup M_ s0 = nth O M zero32 /\ gpr.lookup t s0 = rem 32 ((umul (nth next X zero32) (nth O Y zero32)) (+) (zero_extend 32 (nth O Z zero32))) /\ u2Z ((gpr.lookup s s0) ||| (gpr.lookup t s0)) = u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\ multiplier.utoZ m0 = u2Z (gpr.lookup t s0) * u2Z (gpr.lookup alpha s0) /\ gpr.lookup int_ s0 = one32 /\ gpr.lookup quot s0 = rem 32 (umul (rem 32 ((umul (nth next X zero32) (nth O Y zero32)) (+) (zero_extend 32 (nth O Z zero32)))) (gpr.lookup alpha s0)) ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. red. exists Z; exists next. 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. 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; 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. split; trivial. split; trivial. apply multiplier.lo_remainder. rewrite <-plus_assoc. rewrite (plus_comm multiplier.acx_size). apply le_plus_trans. constructor. rewrite H20. rewrite H18. rewrite <-umul_u2Z. reflexivity. (********************* mthi s; ********************) apply semax_mthi'' with (fun s0 s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s0 = vx /\ gpr.lookup y s0 = vy /\ gpr.lookup z s0 = vz /\ gpr.lookup m s0 = vm /\ u2Z (gpr.lookup k s0) = Z_of_nat nk /\ gpr.lookup alpha s0 = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s0 s' m0 h /\ u2Z (gpr.lookup ext s0) = Z_of_nat next /\ u2Z (gpr.lookup ext s0) < u2Z (gpr.lookup k s0) /\ gpr.lookup one s0 = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s0)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s0 = nth next X zero32 /\ gpr.lookup Y_ s0 = nth O Y zero32 /\ gpr.lookup Z_ s0 = nth O Z zero32 /\ multiplier.utoZ m0 < Zbeta 2 /\ gpr.lookup M_ s0 = nth O M zero32 /\ gpr.lookup t s0 = rem 32 ((umul (nth next X zero32) (nth O Y zero32)) (+) (zero_extend 32 (nth O Z zero32))) /\ u2Z (gpr.lookup s s0 ||| gpr.lookup t s0) = u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\ gpr.lookup int_ s0 = one32 /\ gpr.lookup quot s0 = rem 32 (umul (rem 32 ((umul (nth next X zero32) (nth O Y zero32)) (+) (zero_extend 32 (nth O Z zero32)))) (gpr.lookup alpha s0)) /\ multiplier.hi m0 = gpr.lookup s s0 ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. red. exists Z; exists next. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. Inde_mult_mthi. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. rewrite multiplier.utoZ_def. rewrite multiplier.hi_mthi_op. rewrite multiplier.acx_mthi_op. rewrite multiplier.lo_mthi_op. rewrite multiplier.utoZ_acx_beta2. rewrite Z2u_injection. simpl. rewrite <-Zplus_0_r_reverse. apply Zle_lt_trans with ((Zbeta 1 - 1) + (Zbeta 1 - 1) * Zbeta 1). apply Zplus_le_compat. apply max_u2Z_32'. apply Zmult_le_compat_r. apply max_u2Z_32'. Constraint_constant. unfold Zbeta. simpl. Constraint_constant. Constraint. apply Zle_lt_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1)). assumption. unfold Zbeta. simpl. Constraint_constant. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. apply multiplier.hi_mthi_op. (********************* mtlo t; ********************) apply semax_mtlo'' with (fun s0 s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s0 = vx /\ gpr.lookup y s0 = vy /\ gpr.lookup z s0 = vz /\ gpr.lookup m s0 = vm /\ u2Z (gpr.lookup k s0) = Z_of_nat nk /\ gpr.lookup alpha s0 = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s0 s' m0 h /\ u2Z (gpr.lookup ext s0) = Z_of_nat next /\ u2Z (gpr.lookup ext s0) < u2Z (gpr.lookup k s0) /\ gpr.lookup one s0 = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s0)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s0 = nth next X zero32 /\ gpr.lookup Y_ s0 = nth O Y zero32 /\ gpr.lookup Z_ s0 = nth O Z zero32 /\ multiplier.utoZ m0 < Zbeta 2 /\ gpr.lookup M_ s0 = nth O M zero32 /\ gpr.lookup t s0 = rem 32 ((umul (nth next X zero32) (nth O Y zero32)) (+) (zero_extend 32 (nth O Z zero32))) /\ u2Z (gpr.lookup s s0 ||| gpr.lookup t s0) = u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\ gpr.lookup int_ s0 = one32 /\ gpr.lookup quot s0 = rem 32 (umul (rem 32 ((umul (nth next X zero32) (nth O Y zero32)) (+) (zero_extend 32 (nth O Z zero32)))) (gpr.lookup alpha s0)) /\ multiplier.hi m0 = gpr.lookup s s0 /\ multiplier.lo m0 = gpr.lookup t s0 ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. red. exists Z; exists next. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. Inde_mult_mtlo. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. rewrite multiplier.utoZ_def. rewrite multiplier.acx_mtlo_op. rewrite multiplier.lo_mtlo_op. rewrite multiplier.hi_mtlo_op. rewrite multiplier.utoZ_acx_beta2. rewrite Z2u_injection. simpl. rewrite <-Zplus_0_r_reverse. apply Zle_lt_trans with ((Zbeta 1 - 1) + (Zbeta 1 - 1) * Zbeta 1). apply Zplus_le_compat. apply max_u2Z_32'. apply Zmult_le_compat_r. apply max_u2Z_32'. Constraint. unfold Zbeta. simpl. Constraint_constant. Constraint. assumption. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. rewrite <- H23. apply multiplier.hi_mtlo_op. apply multiplier.lo_mtlo_op. (********************* maddu quot M; ********************) apply semax_maddu'' with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ u2Z (gpr.lookup ext s) < u2Z (gpr.lookup k s) /\ gpr.lookup one s = one32 /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ gpr.lookup Y_ s = nth O Y zero32 /\ gpr.lookup Z_ s = nth O Z zero32 /\ gpr.lookup M_ s = nth O M zero32 /\ gpr.lookup int_ s = one32 /\ gpr.lookup quot s = rem 32 (umul (rem 32 ((umul (nth next X zero32) (nth O Y zero32)) (+) (zero_extend 32 (nth O Z zero32)))) (gpr.lookup alpha s)) /\ multiplier.utoZ m0 = u2Z (gpr.lookup quot s) * u2Z (nth O M zero32) + u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\ multiplier.lo m0 = zero32 ). intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. exists Z; exists next. split; trivial. 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; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. rewrite multiplier.maddu_utoZ. rewrite H17. rewrite <-umul_u2Z. ring. ring. rewrite multiplier.utoZ_def. rewrite multiplier.utoZ_acx_beta2. rewrite Z2u_injection. ring. rewrite H24; rewrite H22. rewrite Zmult_comm. rewrite <-concat_u2Z''. rewrite H19; ring. Constraint. assumption. apply Zlt_le_trans with (Zbeta 2 * 1). assumption. apply Zmult_le_compat_l. apply Zle_trans with (Zpower 2 8 - 1). simpl. Constraint_constant. apply Zminus_le_compat. apply Zpower_2_le. apply multiplier.acx_size_min. Constraint_constant. rewrite H21. apply montgomery_lemma. rewrite H17. rewrite H6. exact Halpha. assumption. rewrite multiplier.utoZ_def. rewrite multiplier.utoZ_acx_beta2. rewrite Z2u_injection. ring. rewrite <-concat_u2Z''. rewrite H22; rewrite H24. rewrite H19. rewrite <-umul_u2Z. rewrite add_u2Z. rewrite zero_extend_u2Z_32. reflexivity. rewrite zero_extend_u2Z_32. apply Zle_lt_trans with ((Zbeta 1 - 1)*(Zbeta 1 - 1) + (Zbeta 1 - 1)). apply Zplus_le_compat. apply max_u2Z_umul_32. apply max_u2Z_32'. simpl. Constraint_constant. Constraint. assumption. (********************* mflhxu Z_; *********************) apply semax_mflhxu'' with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ gpr.lookup Y_ s = nth O Y zero32 /\ gpr.lookup M_ s = nth O M zero32 /\ gpr.lookup int_ s = one32 /\ gpr.lookup quot s = rem 32 (umul (rem 32 ((umul (nth next X zero32) (nth O Y zero32)) (+) (zero_extend 32 (nth O Z zero32)))) (gpr.lookup alpha s)) /\ Zbeta 1 * u2Z ((multiplier.hi m0) ||| (multiplier.lo m0)) = u2Z (gpr.lookup quot s) * u2Z (nth O M zero32) + u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\ multiplier.utoZ m0 < 2 * Zbeta 1 - 2 ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. exists Z; exists next. decompose [and] H; clear H. 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. 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; trivial. split. Inde_mult_mflhxu_op. Inde_update_store. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. rewrite concat_u2Z''. rewrite multiplier.hi_mflhxu_op. rewrite multiplier.lo_mflhxu_op. rewrite <-H19. rewrite multiplier.utoZ_def. ring. rewrite Zmult_assoc. rewrite <-Zbeta_is_exp. simpl (1+1)%nat. rewrite zero_extend_u2Z. rewrite H21. unfold zero32. rewrite Z2u_injection. ring. Constraint. apply multiplier.mflhxu_kbeta1_utoZ. apply Zle_lt_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1) + (Zbeta 1 - 1) * (Zbeta 1 - 1) + (Zbeta 1 - 1)). rewrite H19. apply Zplus_le_compat. apply Zplus_le_compat. rewrite <-umul_u2Z. apply max_u2Z_umul_32. rewrite <-umul_u2Z. apply max_u2Z_umul_32. apply max_u2Z_32'. unfold Zbeta. simpl. Constraint_constant. (********************* addiu t z zero16; *********************) apply semax_addiu'' with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (exists K, Zbeta next * Sum (nk+1) (Z ++ (gpr.lookup C s)::nil) = Sum next X * Sum nk Y + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ gpr.lookup Y_ s = nth O Y zero32 /\ gpr.lookup M_ s = nth O M zero32 /\ gpr.lookup int_ s = one32 /\ gpr.lookup quot s = rem 32 (umul (rem 32 ((umul (nth next X zero32) (nth O Y zero32)) (+) (zero_extend 32 (nth O Z zero32)))) (gpr.lookup alpha s)) /\ Zbeta 1 * u2Z (multiplier.hi m0 ||| multiplier.lo m0) = u2Z (gpr.lookup quot s) * u2Z (nth O M zero32) + u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\ multiplier.utoZ m0 < 2 * Zbeta 1 - 2 /\ gpr.lookup t s = vz ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. exists Z; exists next. decompose [and] H; clear H. 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. 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; 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. rewrite H3. unfold zero16. rewrite sign_extend_16_32'. apply add_neutral. Constraint_constant. (********************* while_bne int_ k *********************) apply semax_strengthen_pre with (fun s s' m0 h => exists Z, exists next, exists nint_, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ u2Z (gpr.lookup int_ s) = Z_of_nat nint_ /\ (nint_ >= 1)%nat /\ u2Z (gpr.lookup int_ s) <= u2Z (gpr.lookup k s) /\ multiplier.utoZ m0 < 2 * Zbeta 1 - 1 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * (Z_of_nat nint_ - 1) /\ (exists K, Zbeta (next + 1) * Sum_hole (nk+1) (nint_-1) (Z ++ gpr.lookup C s :: nil) + u2Z (multiplier.hi m0 ||| multiplier.lo m0) * Zbeta (next + nint_) = Sum next X * Sum nk Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next + Sum nint_ M * u2Z (gpr.lookup quot s) * Zbeta next + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. exists Z; exists next. decompose [and] H; clear H. exists 1%nat. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. rewrite H15. Rewrite_u2Z. reflexivity. Constraint. split. constructor. split. rewrite H15; rewrite H6. Rewrite_u2Z. OmegaZ. Constraint. split. apply Zlt_le_trans with (2 * Zbeta 1 - 2). assumption. simpl. Constraint_constant. split. rewrite H20. rewrite Hvz. simpl Z_of_nat. simpl Zminus. ring. inversion_clear H10 as [K]. inversion_clear H. exists K. split. rewrite Sum_hole_last'. rewrite plus_minus_assoc. simpl minus. rewrite <-plus_n_O. cutrewrite ( u2Z (multiplier.hi m ||| multiplier.lo m) * Zbeta (next + 1) = Zbeta next * (Zbeta 1 * u2Z (multiplier.hi m ||| multiplier.lo m)) ). rewrite H17. cutrewrite ( Zbeta (next + 1) * Sum nk (tail (Z ++ gpr.lookup C s :: nil)) = Zbeta next * (Zbeta 1 * Sum nk (tail (Z ++ gpr.lookup C s :: nil))) ). rewrite Sum_beta_0. apply trans_eq with ( Zbeta next * (Sum (S nk) (zero32 :: tail (Z ++ gpr.lookup C s :: nil)) + u2Z (nth 0 Z zero32)) + Zbeta next * (u2Z (gpr.lookup quot s) * u2Z (nth 0 M zero32) + u2Z (nth next X zero32) * u2Z (nth 0 Y zero32)) ). ring. rewrite Sum_0. rewrite tail_app. cutrewrite ( nth 0 Z zero32 :: tail Z ++ gpr.lookup C s :: nil = (nth 0 Z zero32 :: tail Z) ++ gpr.lookup C s :: nil ). rewrite list_tail'. cutrewrite (S nk = nk + 1)%nat. rewrite H10. rewrite Sum_1. rewrite Sum_1. ring. rewrite S_to_plus_one. apply plus_comm. rewrite H0; assumption. reflexivity. rewrite H0; assumption. rewrite tail_length. rewrite length_app. simpl length. rewrite plus_minus_assoc. simpl minus. rewrite <-plus_n_O. assumption. constructor. rewrite tail_length. (*TODO: same as above*) rewrite length_app. simpl length. rewrite plus_minus_assoc. simpl minus. rewrite <-plus_n_O. assumption. constructor. rewrite Zbeta_is_exp. ring. rewrite Zbeta_is_exp. ring. constructor. rewrite length_app; simpl length; rewrite H0; ring. assumption. apply semax_seq with (fun s s' m0 h => (exists Z, exists next, exists nint_, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ u2Z (gpr.lookup int_ s) = Z_of_nat nint_ /\ (nint_ >= 1)%nat /\ u2Z (gpr.lookup int_ s) <= u2Z (gpr.lookup k s) /\ multiplier.utoZ m0 < 2 * Zbeta 1 - 1 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * (Z_of_nat nint_ - 1) /\ (exists K, Zbeta (next + 1) * Sum_hole (nk+1) (nint_-1) (Z ++ gpr.lookup C s :: nil) + u2Z (multiplier.hi m0 ||| multiplier.lo m0) * Zbeta (next + nint_) = Sum next X * Sum nk Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next + Sum nint_ M * u2Z (gpr.lookup quot s) * Zbeta next + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next)) /\ u2Z (gpr.lookup int_ s) = u2Z (gpr.lookup k s) ). apply semax_while_bne with (P:=fun s0 s' m0 h => exists Z, exists next, exists nint_, length Z = nk /\ gpr.lookup x s0 = vx /\ gpr.lookup y s0 = vy /\ gpr.lookup z s0 = vz /\ gpr.lookup m s0 = vm /\ gpr.lookup one s0 = one32 /\ u2Z (gpr.lookup k s0) = Z_of_nat nk /\ gpr.lookup alpha s0 = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s0 s' m0 h /\ u2Z (gpr.lookup ext s0) = Z_of_nat next /\ (next < nk)%nat /\ gpr.lookup X_ s0 = nth next X zero32 /\ u2Z (gpr.lookup int_ s0) = Z_of_nat nint_ /\ (nint_ >= 1)%nat /\ u2Z (gpr.lookup int_ s0) <= u2Z (gpr.lookup k s0) /\ multiplier.utoZ m0 < 2 * Zbeta 1 - 1 /\ u2Z (gpr.lookup t s0) = 4 * nz + 4 * (Z_of_nat nint_ - 1) /\ (exists K, Zbeta (next + 1) * Sum_hole (nk+1) (nint_-1) (Z ++ gpr.lookup C s0 :: nil) + u2Z (multiplier.hi m0 ||| multiplier.lo m0) * Zbeta (next + nint_) = Sum next X * Sum nk Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next + Sum nint_ M * u2Z (gpr.lookup quot s0) * Zbeta next + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) ). (********************* lwxs Y int_ y; ********************) apply semax_lwxs_backwards''2 with (fun s s' m0 h => exists Z, exists next, exists nint_, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (next < nk)%nat /\ (nint_ < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ u2Z (gpr.lookup int_ s) = Z_of_nat nint_ /\ (nint_ >= 1)%nat /\ multiplier.utoZ m0 < 2 * Zbeta 1 - 1 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * (Z_of_nat nint_ - 1) /\ (exists K, Zbeta (next + 1) * Sum_hole (nk+1) (nint_-1) (Z ++ gpr.lookup C s :: nil) + u2Z (multiplier.hi m0 ||| multiplier.lo m0) * Zbeta (next + nint_) = Sum next X * Sum nk Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next + Sum nint_ M * u2Z (gpr.lookup quot s) * Zbeta next + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ gpr.lookup Y_ s = nth nint_ Y zero32 ). red; intros. inversion_clear H. inversion_clear H0 as [Z]. inversion_clear H as [next]. inversion_clear H0 as [nint_]. decompose [and] H; clear H. exists (nth nint_ Y zero32). split. Decompose_list_32 Y nint_ Y1 Y2. lapply (mapstos_decompose_generic_P _ _ _ _ _ _ (var_e y) (add_e (var_e y) (shl2_e (var_e int_))) (add_e (add_e (var_e y) (shl2_e (var_e int_))) (int_e four32)) s ((((var_e x |--> X)) ** (var_e z |--> Z)) ** (var_e mont.m |--> M)) Hy H20 H s' m h). intro. simpl app in H18. assert ( ((var_e y |--> Y) ** (((var_e x |--> X) ** (var_e z |--> Z)) ** (var_e mont.m |--> M))) s s' m h ). assoc_comm H9. assumption. generalize (H18 H21); clear H18 H21; intro. apply my_sep_trivial with ( ((var_e y |--> Y1) ** (add_e (add_e (var_e y) (shl2_e (var_e int_))) (int_e four32) |--> Y2)) ** (((var_e x |--> X) ** (var_e z |--> Z)) ** (var_e mont.m |--> M))). assoc_comm H18. exact H18. simpl eval. split. rewrite H2. Constraint. split. cutrewrite ( gpr.lookup int_ s = Z2u 32 (Z_of_nat nint_) ). reflexivity. apply u2Z_injection. rewrite H13. rewrite Z2u_injection. reflexivity. Constraint. reflexivity. rewrite Hy. apply Z_of_nat_lt_inj. omega. red. exists Z; exists next; exists nint_. 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. 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; trivial. split; trivial. split; trivial. split. Inde_update_store. split; trivial. split; trivial. split. omega. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. (********************* lwxs Z int_ z; ********************) apply semax_lwxs_backwards''2 with (fun s s' m0 h => exists Z, exists next, exists nint_, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (next < nk)%nat /\ (nint_ < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ u2Z (gpr.lookup int_ s) = Z_of_nat nint_ /\ (nint_ >= 1)%nat /\ multiplier.utoZ m0 < 2 * Zbeta 1 - 1 /\ u2Z (gpr.lookup t s) = u2Z (gpr.lookup z s) + 4 * (Z_of_nat nint_ - 1) /\ (exists K, Zbeta (next + 1) * Sum_hole (nk+1) (nint_-1) (Z ++ gpr.lookup C s :: nil) + u2Z (multiplier.hi m0 ||| multiplier.lo m0) * Zbeta (next + nint_) = Sum next X * Sum nk Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next + Sum nint_ M * u2Z (gpr.lookup quot s) * Zbeta next + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ gpr.lookup Y_ s = nth nint_ Y zero32 /\ gpr.lookup Z_ s = nth nint_ Z zero32 ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. inversion_clear H as [nint_]. decompose [and] H0; clear H0. exists (nth nint_ Z zero32). split. Decompose_list_32 Z nint_ Z1 Z2. lapply (mapstos_decompose_generic_P _ _ _ _ _ _ (var_e z) (add_e (var_e z) (shl2_e (var_e int_))) (add_e (add_e (var_e z) (shl2_e (var_e int_))) (int_e four32)) s ((((var_e x |--> X)) ** (var_e y |--> Y)) ** (var_e mont.m |--> M)) H H20 H0 s' m h). intro. simpl app in H18. assert ( ((var_e z |--> Z) ** (((var_e x |--> X) ** (var_e y |--> Y)) ** (var_e mont.m |--> M))) s s' m h ). assoc_comm H8. generalize (H18 H21); clear H18 H21; intro. apply my_sep_trivial with ( ((var_e z |--> Z1) ** (add_e (add_e (var_e z) (shl2_e (var_e int_))) (int_e four32) |--> Z2)) ** (((var_e x |--> X) ** (var_e y |--> Y)) ** (var_e mont.m |--> M))). assoc_comm H18. exact H18. simpl eval. split. rewrite H3. Constraint. split. cutrewrite ( gpr.lookup int_ s = Z2u 32 (Z_of_nat nint_) ). reflexivity. apply u2Z_injection. rewrite H13. rewrite Z2u_injection. reflexivity. Constraint. reflexivity. rewrite H. apply Z_of_nat_lt_inj. omega. red. exists Z; exists next; exists nint_. 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. 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; trivial. split; trivial. split; trivial. split. Inde_update_store. split; trivial. split; trivial. split. omega. split; trivial. split; trivial. split; trivial. split; trivial. split. rewrite H16. rewrite H3. rewrite Hvz. reflexivity. split; trivial. split; trivial. (********************* maddu X Y; ********************) apply semax_maddu'' with (fun s s' m0 h => exists Z, exists next, exists nint_, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (next < nk)%nat /\ (nint_ < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ u2Z (gpr.lookup int_ s) = Z_of_nat nint_ /\ (nint_ >= 1)%nat /\ multiplier.utoZ m0 < Zbeta 2 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * (Z_of_nat nint_ - 1) /\ gpr.lookup Y_ s = nth nint_ Y zero32 /\ gpr.lookup Z_ s = nth nint_ Z zero32 /\ (exists K, Zbeta (next + 1) * Sum_hole (nk+1) (nint_-1) (Z ++ gpr.lookup C s :: nil) + multiplier.utoZ m0 * Zbeta (next + nint_) = Sum next X * Sum nk Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next + Sum nint_ M * u2Z (gpr.lookup quot s) * Zbeta next + u2Z (nth next X zero32) * u2Z (nth nint_ Y zero32) * Zbeta (next + nint_) + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) ). intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. inversion_clear H as [nint_]. exists Z; exists next; exists nint_. decompose [and] H0; clear H0. assert (Htmp : multiplier.utoZ m < Zbeta 2 * (2 ^^ multiplier.acx_size - 1) ). apply Zlt_le_trans with (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; trivial. split; trivial. split. Inde_mult_maddu. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. rewrite multiplier.maddu_utoZ. apply Zlt_le_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1) + (2 * Zbeta 1 - 1)). apply Zplus_le_lt_compat. apply max_u2Z_umul_32. assumption. unfold Zbeta. simpl. Constraint_constant. exact Htmp. split. rewrite H16; rewrite H3; rewrite Hvz. reflexivity. split; trivial. split; trivial. inversion_clear H17 as [K]. inversion_clear H0. exists K. split. apply trans_eq with (Sum next X * Sum nk Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next + Sum nint_ M * u2Z (gpr.lookup quot s) * Zbeta next + K * Sum nk M + u2Z (nth next X zero32) * u2Z (nth nint_ Y zero32) * Zbeta (next + nint_)). rewrite <-H17. rewrite multiplier.maddu_utoZ. rewrite multiplier.utoZ_def. rewrite multiplier.utoZ_acx_beta2. rewrite Z2u_injection. simpl. rewrite <-umul_u2Z. rewrite concat_u2Z''. rewrite <-Zplus_0_r_reverse. rewrite H18. rewrite H12. ring. ring. ring. ring. Constraint. apply Zlt_le_trans with (2*Zbeta 1-1). assumption. unfold Zbeta. simpl. Constraint_constant. exact Htmp. ring. assumption. (********************* lwxs M int_ m; ********************) apply semax_lwxs_backwards''2 with (fun s s' m0 h => exists Z, exists next, exists nint_, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (next < nk)%nat /\ (nint_ < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ u2Z (gpr.lookup int_ s) = Z_of_nat nint_ /\ (nint_ >= 1)%nat /\ multiplier.utoZ m0 < Zbeta 2 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * ( Z_of_nat nint_ - 1) /\ gpr.lookup Y_ s = nth nint_ Y zero32 /\ gpr.lookup Z_ s = nth nint_ Z zero32 /\ (exists K, Zbeta (next + 1) * Sum_hole (nk+1) (nint_-1) (Z ++ gpr.lookup C s :: nil) + multiplier.utoZ m0 * Zbeta (next + nint_) = Sum next X * Sum nk Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next + Sum nint_ M * u2Z (gpr.lookup quot s) * Zbeta next + u2Z (nth next X zero32) * u2Z (nth nint_ Y zero32) * Zbeta (next + nint_) + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ gpr.lookup M_ s = nth nint_ M zero32 ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. inversion_clear H as [nint_]. decompose [and] H0; clear H0. exists (nth nint_ M zero32). split. Decompose_list_32 M nint_ M1 M2. lapply (mapstos_decompose_generic_P _ _ _ _ _ _ (var_e mont.m) (add_e (var_e mont.m) (shl2_e (var_e int_))) (add_e (add_e (var_e mont.m) (shl2_e (var_e int_))) (int_e four32)) s ((((var_e x |--> X)) ** (var_e y |--> Y)) ** (var_e z |--> Z)) Hm H21 H0 s' m h). intro. simpl app in H19. assert ( ((var_e mont.m |--> M) ** (((var_e x |--> X) ** (var_e y |--> Y)) ** (var_e z |--> Z))) s s' m h ). assoc_comm H8. generalize (H19 H22); clear H19 H22; intro. apply my_sep_trivial with ( ((var_e mont.m |--> M1) ** (add_e (add_e (var_e mont.m) (shl2_e (var_e int_))) (int_e four32) |--> M2)) ** (((var_e x |--> X) ** (var_e y |--> Y)) ** (var_e z |--> Z)) ). assoc_comm H19. exact H19. simpl eval. split. rewrite H4. Constraint. split. cutrewrite ( gpr.lookup int_ s = Z2u 32 (Z_of_nat nint_) ). reflexivity. apply u2Z_injection. rewrite H13. rewrite Z2u_injection. reflexivity. Constraint. reflexivity. rewrite Hm. apply Z_of_nat_lt_inj. omega. red. exists Z; exists next; exists nint_. 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. 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; trivial. split; trivial. split; trivial. split. Inde_update_store. split; trivial. split; trivial. split. omega. split; trivial. split; trivial. split; trivial. split; trivial. split. rewrite H16. ring. split; trivial. split; trivial. split; trivial. (********************* maddu Z_ one; ********************) apply semax_maddu'' with (fun s s' m0 h => exists Z, exists next, exists nint_, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (next < nk)%nat /\ (nint_ < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ u2Z (gpr.lookup int_ s) = Z_of_nat nint_ /\ (nint_ >= 1)%nat /\ multiplier.utoZ m0 < Zbeta 2 + Zbeta 1 - 1 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * (Z_of_nat nint_ - 1) /\ gpr.lookup Y_ s = nth nint_ Y zero32 /\ gpr.lookup Z_ s = nth nint_ Z zero32 /\ gpr.lookup M_ s = nth nint_ M zero32 /\ (exists K, Zbeta (next + 1) * Sum_hole (nk+1) (nint_ - 1) (Z ++ gpr.lookup C s :: nil) + multiplier.utoZ m0 * Zbeta (next + nint_) = Sum next X * Sum nk Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next + Sum nint_ M * u2Z (gpr.lookup quot s) * Zbeta next + u2Z (nth next X zero32) * u2Z (nth nint_ Y zero32) * Zbeta (next + nint_) + u2Z (nth nint_ Z zero32) * Zbeta (next + nint_) + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) ). intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. inversion_clear H as [nint_]. exists Z; exists next; exists nint_. decompose [and] H0; clear H0. assert (Htmp: multiplier.utoZ m < Zbeta 2 * (2 ^^ multiplier.acx_size - 1)). apply Zlt_le_trans with (Zbeta 2 * 1). rewrite Zmult_1_r. assumption. apply Zle_trans with (Zbeta 2 * (Zpower 2 8 - 1)). apply Zmult_le_compat_l. simpl. Constraint_constant. 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; trivial. split; trivial. split. Inde_mult_maddu. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. rewrite multiplier.maddu_utoZ. rewrite H5. unfold one32. rewrite umul_1. rewrite zero_extend_u2Z_32. apply Zlt_le_trans with ((Zbeta 1 - 1) + Zbeta 2). apply Zplus_le_lt_compat. apply max_u2Z_32'. assumption. unfold Zbeta. simpl. Constraint_constant. exact Htmp. split; trivial. split; trivial. split; trivial. split; trivial. inversion_clear H19 as [K]. inversion_clear H0. exists K. split. rewrite multiplier.maddu_utoZ. rewrite H5. unfold one32. rewrite umul_1. rewrite H18. rewrite zero_extend_u2Z_32. apply trans_eq with (Zbeta (next + 1) * Sum_hole (nk + 1) (nint_ - 1) (Z ++ gpr.lookup C s :: nil) + multiplier.utoZ m * Zbeta (next + nint_) + u2Z (nth nint_ Z zero32) * Zbeta (next + nint_)). ring. rewrite H19. ring. exact Htmp. assumption. (********************* maddu quot M; ********************) apply semax_maddu'' with (fun s s' m0 h => exists Z, exists next, exists nint_, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (next < nk)%nat /\ (nint_ < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ u2Z (gpr.lookup int_ s) = Z_of_nat nint_ /\ (nint_ >= 1)%nat /\ multiplier.utoZ m0 < 2 * Zbeta 2 - Zbeta 1 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * (Z_of_nat nint_ - 1) /\ gpr.lookup Y_ s = nth nint_ Y zero32 /\ gpr.lookup Z_ s = nth nint_ Z zero32 /\ gpr.lookup M_ s = nth nint_ M zero32 /\ (exists K, Zbeta (next + 1) * Sum_hole (nk+1) (nint_-1) (Z ++ gpr.lookup C s :: nil) + multiplier.utoZ m0 * Zbeta (next + nint_) = Sum next X * Sum nk Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next + Sum nint_ M * u2Z (gpr.lookup quot s) * Zbeta next + u2Z (nth next X zero32) * u2Z (nth nint_ Y zero32) * Zbeta (next + nint_) + u2Z (nth nint_ Z zero32) * Zbeta (next + nint_) + u2Z (nth nint_ M zero32) * u2Z (gpr.lookup quot s) * Zbeta (next + nint_) + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) ). intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. inversion_clear H as [nint_]. exists Z; exists next; exists nint_. decompose [and] H0; clear H0. assert (Htmp : multiplier.utoZ m < Zbeta 2 * (Zpower 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; trivial. split; trivial. split. Inde_mult_maddu. split; trivial. split; trivial. 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 2 + Zbeta 1 - 1)). apply Zplus_le_lt_compat. apply max_u2Z_umul_32. assumption. unfold Zbeta. simpl. Constraint_constant. exact Htmp. split; trivial. split; trivial. split; trivial. split; trivial. inversion_clear H21 as [K]. inversion_clear H0. exists K. split. rewrite multiplier.maddu_utoZ. rewrite Zmult_plus_distr_l. apply trans_eq with (Zbeta (next + 1) * Sum_hole (nk + 1) (nint_ - 1) (Z ++ gpr.lookup C s :: nil) + multiplier.utoZ m * Zbeta (next + nint_) + (u2Z (umul (gpr.lookup quot s) (gpr.lookup M_ s)) * Zbeta (next + nint_))). ring. ring. ring. rewrite H20. rewrite H19. rewrite umul_u2Z. ring. exact Htmp. assumption. (********************* addiu int_ int_ one16; ********************) apply semax_addiu'' with (fun s s' m0 h => exists Z, exists next, exists nint_, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (next < nk)%nat /\ (nint_ <= nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ u2Z (gpr.lookup int_ s) = Z_of_nat nint_ /\ (nint_ >= 2)%nat /\ multiplier.utoZ m0 < 2 * Zbeta 2 - Zbeta 1 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * (Z_of_nat nint_ - 2) /\ (exists K, Zbeta (next + 1) * Sum_hole (nk+1) (nint_-2) (Z ++ gpr.lookup C s :: nil) + multiplier.utoZ m0 * Zbeta (next + nint_-1) = Sum next X * Sum nk Y + Sum (nint_-1) Y * u2Z (nth next X zero32) * Zbeta next + Sum (nint_-1) M * u2Z (gpr.lookup quot s) * Zbeta next + u2Z (nth next X zero32) * u2Z (nth (nint_-1) Y zero32) * Zbeta (next + nint_ - 1)+ u2Z (nth (nint_-1) Z zero32) * Zbeta (next + nint_ - 1) + u2Z (nth (nint_-1) M zero32) * u2Z (gpr.lookup quot s) * Zbeta (next + nint_ - 1) + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) ). red; intros. red. inversion_clear H as [Z]. inversion_clear H0 as [next]. inversion_clear H as [nint_]. exists Z; exists next; exists (nint_ + 1)%nat. decompose [and] H0; clear H0. 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. elim gpr.lookup_update; try var. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. Inde_update_store. split; trivial. split; trivial. split. red in H11. rewrite S_to_plus_one in H11. rewrite plus_comm. assumption. split; trivial. split. Rewrite_u2Z. rewrite H13. rewrite inj_plus. reflexivity. Constraint. Constraint. Constraint. split. red. apply le_trans with (1+1)%nat. constructor. apply plus_le_compat. assumption. constructor. split; trivial. split. rewrite H16. rewrite inj_plus. simpl Z_of_nat. ring. inversion_clear H21 as [K]. inversion_clear H0. exists K. split. cutrewrite (nint_ + 1 - 2 = nint_ - 1)%nat. cutrewrite (nint_ + 1 - 1 = nint_)%nat. cutrewrite (next + (nint_ + 1) - 1 = next + nint_)%nat. assumption. symmetry. apply plus_minus. ring. symmetry. apply plus_minus. ring. symmetry. apply plus_minus. rewrite <-plus_minus_assoc. apply plus_minus. ring. assumption. assumption. (********************* mflhxu Z_; ********************) apply semax_mflhxu'' with (fun s s' m0 h => exists Z, exists next, exists nint_, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (next < nk)%nat /\ (nint_ <= nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ u2Z (gpr.lookup int_ s) = Z_of_nat nint_ /\ (nint_ >= 2)%nat /\ multiplier.utoZ m0 < 2 * Zbeta 1 - 1 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * (Z_of_nat nint_-2) /\ (exists K, Zbeta (next + 1) * Sum_hole (nk+1) (nint_-2) (Z ++ gpr.lookup C s :: nil) + u2Z ((multiplier.hi m0) ||| (multiplier.lo m0)) * Zbeta (next + nint_) + u2Z (gpr.lookup Z_ s) * Zbeta (next + nint_-1) = Sum next X * Sum nk Y + Sum (nint_-1) Y * u2Z (nth next X zero32) * Zbeta next + Sum (nint_-1) M * u2Z (gpr.lookup quot s) * Zbeta next + u2Z (nth next X zero32) * u2Z (nth (nint_-1) Y zero32) * Zbeta (next + nint_ - 1) + u2Z (nth (nint_-1) Z zero32) * Zbeta (next + nint_ - 1) + u2Z (nth (nint_-1) M zero32) * u2Z (gpr.lookup quot s) * Zbeta (next + nint_ - 1) + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) ). red; intros. red. inversion_clear H as [Z]. inversion_clear H0 as [next]. inversion_clear H as [nint_]. exists Z; exists next; exists nint_. decompose [and] H0; clear H0. 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]. elim gpr.lookup_update; try var. split; trivial. split; trivial. split; trivial. 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; trivial. split; trivial. split. apply multiplier.mflhxu_kbeta1_utoZ. apply Zlt_le_trans with (2 * Zbeta 2 - Zbeta 1). assumption. unfold Zbeta. simpl. Constraint_constant. split; trivial. inversion_clear H18 as [K]. inversion_clear H0. exists K. split. rewrite <-H17. rewrite concat_u2Z''. rewrite multiplier.hi_mflhxu_op. rewrite multiplier.lo_mflhxu_op. rewrite zero_extend_u2Z. rewrite multiplier.utoZ_def. rewrite <-Zplus_assoc. apply Zplus_compat. reflexivity. rewrite Zmult_plus_distr_l. rewrite Zmult_plus_distr_l. rewrite Zmult_plus_distr_l. rewrite <-Zmult_assoc. rewrite <-Zmult_assoc. rewrite <-Zmult_assoc. rewrite <-Zbeta_is_exp. rewrite <-Zbeta_is_exp. rewrite <-Zbeta_is_exp. rewrite le_plus_minus_r. cutrewrite ( 2 + (next + nint_ - 1) = 1 + (next + nint_) )%nat. ring. rewrite <-plus_minus_assoc. symmetry. apply plus_minus. ring. red. rewrite plus_comm. apply le_plus_trans. apply le_trans with 2%nat. repeat constructor. assumption. rewrite plus_comm. apply le_plus_trans. apply le_trans with 2%nat. repeat constructor. assumption. assumption. (********************* addiu t t four16; ********************) apply semax_addiu'' with (fun s s' m0 h => exists Z, exists next, exists nint_, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (next < nk)%nat /\ (nint_ <= nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ u2Z (gpr.lookup int_ s) = Z_of_nat nint_ /\ (nint_ >= 2)%nat /\ multiplier.utoZ m0 < 2 * Zbeta 1 - 1 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * (Z_of_nat nint_-1) /\ (exists K, Zbeta (next + 1) * Sum_hole (nk+1) (nint_-2) (Z ++ gpr.lookup C s :: nil) + u2Z (multiplier.hi m0 ||| multiplier.lo m0) * Zbeta (next + nint_) + u2Z (gpr.lookup Z_ s) * Zbeta (next + nint_-1) = Sum next X * Sum nk Y + Sum (nint_-1) Y * u2Z (nth next X zero32) * Zbeta next + Sum (nint_-1) M * u2Z (gpr.lookup quot s) * Zbeta next + u2Z (nth next X zero32) * u2Z (nth (nint_-1) Y zero32) * Zbeta (next + nint_ - 1) + u2Z (nth (nint_-1) Z zero32) * Zbeta (next + nint_ - 1 )+ u2Z (nth (nint_-1) M zero32) * u2Z (gpr.lookup quot s) * Zbeta (next + nint_ - 1) + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) ). red; intros. red. inversion_clear H as [Z]. inversion_clear H0 as [next]. inversion_clear H as [nint_]. exists Z; exists next; exists nint_. decompose [and] H0; clear H0. 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. 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; trivial. split; trivial. split. Inde_update_store. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. Rewrite_u2Z. rewrite H16. ring. Constraint. Constraint. Constraint. assumption. (********************* sw Z_ mfour16 t ********************) apply semax_sw_backwards'. red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. inversion_clear H as [nint_]. decompose [and] H0; clear H0. exists (int_e (nth (nint_ - 2) Z zero32)). assert (Htmp : u2Z (eval (var_e z) s) + 4 * Z_of_nat nk < Zbeta 1 /\ eval (add_e (var_e t) (int_e (sign_extend_16_32 mfour16))) s = eval (add_e (var_e z) (shl2_e (int_e (Z2u 32 (Z_of_nat (nint_ - 2)))))) s /\ eval (add_e (add_e (var_e t) (int_e (sign_extend_16_32 mfour16))) (int_e four32)) s = eval (add_e (add_e (var_e t) (int_e (sign_extend_16_32 mfour16))) (int_e four32)) s). simpl eval. rewrite H3. rewrite Hvz. split. Constraint. split. assert (s2Z (sign_extend_16_32 mfour16) = - 4). unfold sign_extend_16_32. unfold mfour16. rewrite sign_extend_Z2s. simpl plus. rewrite Z2s_injection. reflexivity. simpl. split. Constraint_constant. Constraint_constant. simpl. split. Constraint_constant. Constraint_constant. assert ( u2Z (shl2 (Z2u 32 (Z_of_nat nint_ - 2))) = 4 * (Z_of_nat nint_ - 2) ). unfold shl2. rewrite (@shl_u2Z 2 _ (Z2u 32 (Z_of_nat nint_ - 2)) 30). rewrite Z2u_injection. simpl Zpower. apply Zmult_comm. split. (*TODO: Constraint fails here*) omega. Constraint_variable. constructor. rewrite Z2u_injection. Constraint_variable. split. omega. Constraint_variable. symmetry. rewrite inj_minus1. simpl Z_of_nat. apply u2Z_injection. rewrite add_u2Z. rewrite add_u2Z_s2Z. rewrite H16. rewrite Hvz. rewrite H0. rewrite H17. ring. rewrite H0. rewrite H16. assert (2 <= Z_of_nat nint_). omega. split. omega. Constraint. rewrite H17. rewrite Hvz. Constraint. omega. reflexivity. Decompose_list_32 Z (nint_-2)%nat Z1 Z2. lapply (mapstos_decompose_generic_P _ _ _ _ _ _ (var_e z) (add_e (var_e t) (int_e (sign_extend_16_32 mfour16))) (add_e (add_e (var_e t) (int_e (sign_extend_16_32 mfour16))) (int_e four32)) s ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e mont.m |--> M)) H H19 H0 s' m h). intro. assert ( ((var_e z |--> Z) ** (((var_e x |--> X) ** (var_e y |--> Y)) ** (var_e mont.m |--> M))) s s' m h ). assoc_comm H8. generalize (H17 H20); clear H17 H20; intro. Monotony H17. Adjunction H17. exists (update_list Z (nint_ - 2) (gpr.lookup Z_ s)). exists next. exists nint_. split. apply length_update_list; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. assoc_comm H17. eapply mapstos_compose_generic with (lst2:=Z2) (w:=gpr.lookup Z_ s) (e':=add_e (var_e t) (int_e (sign_extend_16_32 mfour16))) (e'':=add_e (add_e (var_e t) (int_e (sign_extend_16_32 mfour16))) (int_e four32)). apply length_update_list. apply H. apply H19. rewrite H0. rewrite update_list_app. rewrite H19. rewrite <-minus_n_n. simpl. reflexivity. rewrite H19. constructor. exact Htmp. simpl in H17. assoc_comm H17. generalize H17; clear H17; apply mapsto_ext'. reflexivity. reflexivity. split; trivial. split; trivial. split; trivial. split; trivial. split. red. apply le_trans with 2%nat. repeat constructor. assumption. split. rewrite H13; rewrite H6. apply Z_of_nat_le_inj'. assumption. split; trivial. split; trivial. inversion_clear H18 as [K]. inversion_clear H20. exists K. split. (* technicalities: at this point, we have an hypothesis about K with ( z_0 ... z_{nint-2} ... z_{k-1} ++ C::nil )\{nint-2} whereas in the goal, we have ( z_0 ... Z ... z_{k-1} ++ C::nil )\{nint-1} we will: 1. coax the hypothesis and the goal to have the same Sum_hole predicate 1.a. add z_{nint-1} to the goal 1.b. use the Sum_hole_shift property to change the Sum_hole predicate in the goal 2. check that the goal can be obtained from the hypo by rewriting *) (* 1. *) (* 1.a. *) apply Zplus_reg_l with (Zbeta (next + 1) * u2Z (nth (nint_ - 1) Z zero32) * Zbeta (nint_ - 2)). rewrite Zplus_assoc. rewrite <-Zmult_assoc. rewrite <-(Zmult_plus_distr_r (Zbeta (next + 1))). (* 1.b. *) assert ( Sum_hole (nk + 1) (nint_ - 1) (update_list Z (nint_ - 2) (gpr.lookup Z_ s) ++ gpr.lookup C s::nil) + u2Z (nth (nint_ - 1) Z zero32) * Zbeta (nint_ - 2) = Sum_hole (nk + 1) (nint_ - 2) (Z ++ gpr.lookup C s::nil) + u2Z (gpr.lookup Z_ s) * Zbeta (nint_ - 2) ). assert ( length (update_list Z (nint_-2) (gpr.lookup Z_ s)++gpr.lookup C s::nil) = nk+1)%nat. rewrite length_app. rewrite (length_update_list (int 32) nk). simpl. reflexivity. assumption. assert ( nint_ - 1 < nk + 1 )%nat. red. rewrite minus_Sn_m. simpl. rewrite <-minus_n_O. apply le_trans with nk. assumption. apply le_plus_trans. constructor. apply le_trans with 2%nat. auto. assumption. generalize (Sum_hole_shift _ _ H20 _ H22); clear H20 H22; intro. rewrite <-nth_beyond in H20. rewrite <-nth_beyond in H20. rewrite nth_update_list' in H20. cutrewrite (nint_ - 1 - 1 = nint_ - 2)%nat in H20. rewrite nth_update_list in H20. cutrewrite (Sum_hole (nk + 1) (nint_ - 2) (Z ++ gpr.lookup C s :: nil) = Sum_hole (nk + 1) (nint_ - 2) (update_list Z (nint_ - 2) (gpr.lookup Z_ s) ++ gpr.lookup C s :: nil) ). auto. rewrite <-update_list_app'. rewrite <-Sum_hole_update_list. reflexivity. rewrite length_app. simpl. rewrite H. reflexivity. rewrite H. red. rewrite minus_Sn_m. simpl. apply le_trans with nint_. apply le_minus. assumption. assumption. rewrite H. red. rewrite minus_Sn_m. simpl. apply le_trans with nint_. apply le_minus. assumption. assumption. apply plus_minus. simpl. rewrite minus_Sn_m. rewrite minus_Sn_m. rewrite minus_Sn_m. simpl. do 2 rewrite <-minus_n_O. reflexivity. apply le_trans with 2%nat. auto. assumption. rewrite minus_Sn_m. simpl. rewrite <-minus_n_O. apply le_trans with 2%nat. auto. assumption. apply le_trans with 2%nat. auto. assumption. apply plus_le_minus. assumption. destruct nint_. inversion H14. destruct nint_. inversion H14. inversion H23. simpl. rewrite <-minus_n_O. auto. rewrite (length_update_list (int 32) nk). apply lt_le_trans with nint_. red. rewrite minus_Sn_m. simpl. rewrite <-minus_n_O. apply le_minus. apply plus_le_minus. assumption. assumption. assumption. rewrite (length_update_list (int 32) nk). red. rewrite minus_Sn_m. simpl. rewrite <-minus_n_O. assumption. apply le_trans with 2%nat. auto. assumption. assumption. rewrite (Zplus_comm (u2Z (nth (nint_ - 1) Z zero32) * Zbeta (nint_ - 2))). rewrite H20; clear H20. (* 2. *) assert ( Htmp2 : (next + 1 + (nint_ - 2) = next + nint_ - 1)%nat). rewrite <-plus_minus_assoc. symmetry. apply plus_minus. simpl. rewrite minus_Sn_m. simpl. rewrite <-minus_n_O. rewrite (plus_comm next). reflexivity. rewrite plus_comm. apply le_plus_trans. apply le_trans with 2%nat. repeat constructor. assumption. assumption. apply trans_eq with ( Zbeta (next + 1) * Sum_hole (nk + 1) (nint_ - 2) (Z ++ gpr.lookup C s :: nil) + u2Z (multiplier.hi m ||| multiplier.lo m) * Zbeta (next + nint_) + u2Z (gpr.lookup Z_ s) * (Zbeta (next + 1) * Zbeta (nint_ - 2)) ); [ring | idtac]. rewrite <-Zbeta_is_exp. rewrite Htmp2. rewrite H18; clear H18. repeat rewrite plus_assoc. apply trans_eq with ( (Sum (nint_ - 1) Y * u2Z (nth next X zero32) * Zbeta next + u2Z (nth next X zero32) * u2Z (nth (nint_ - 1) Y zero32) * Zbeta (next + nint_ - 1)) + (Sum (nint_ - 1) M * u2Z (gpr.lookup quot s) * Zbeta next + u2Z (nth (nint_ - 1) M zero32) * u2Z (gpr.lookup quot s) * Zbeta (next + nint_ - 1)) + K * Sum nk M + Sum next X * Sum nk Y + u2Z (nth (nint_ - 1) Z zero32) * Zbeta (next + nint_ - 1) ); [ring | idtac]. apply trans_eq with ( Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next + Sum nint_ M * u2Z (gpr.lookup quot s) * Zbeta next + K * Sum nk M + Sum next X * Sum nk Y + (u2Z (nth (nint_ - 1) Z zero32) * (Zbeta (next + 1) * Zbeta (nint_ - 2))) ); [idtac | ring]. apply Zplus_compat; [idtac | idtac]. apply Zplus_compat; [idtac | reflexivity]. apply Zplus_compat; [idtac | reflexivity]. apply Zplus_compat. apply trans_eq with ((Sum (nint_ - 1) Y + u2Z (nth (nint_ - 1) Y zero32) * Zbeta (nint_ - 1)) * (u2Z (nth next X zero32) * Zbeta next) ). rewrite plus_minus_assoc. rewrite Zbeta_is_exp. ring. red; apply le_trans with 2%nat. auto. assumption. rewrite Sum_remove_last_32. cutrewrite (S(nint_-1)=nint_). ring. rewrite minus_Sn_m. simpl. rewrite <-minus_n_O. reflexivity. apply le_trans with 2%nat. auto. assumption. apply trans_eq with ((Sum (nint_ - 1) M + u2Z (nth (nint_ - 1) M zero32) * Zbeta (nint_ - 1)) * (u2Z (gpr.lookup quot s) * Zbeta next) ). rewrite plus_minus_assoc. rewrite Zbeta_is_exp. ring. red; apply le_trans with 2%nat. auto. assumption. rewrite Sum_remove_last_32. cutrewrite (S(nint_-1)=nint_). ring. rewrite minus_Sn_m. simpl. rewrite <-minus_n_O. reflexivity. apply le_trans with 2%nat. auto. assumption. rewrite <-Zbeta_is_exp. rewrite Htmp2. reflexivity. assumption. exact Htmp. rewrite H. apply plus_lt_minus'. assumption. omega. (********************* maddu C one; ********************) apply semax_maddu'' with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup mont.m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((((var_e x |--> X) ** (var_e y |--> Y)) ** (var_e z |--> Z)) ** (var_e mont.m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ u2Z (gpr.lookup int_ s) = Z_of_nat nk /\ multiplier.utoZ m0 < 3 * Zbeta 1 - 2 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * (Z_of_nat nk - 1) /\ (exists K, Zbeta (next + 1) * Sum (nk-1) Z + multiplier.utoZ m0 * Zbeta (next + nk) = Sum next X * Sum nk Y + Sum nk Y * u2Z (nth next X zero32) * Zbeta next + Sum nk M * u2Z (gpr.lookup quot s) * Zbeta next + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) ). intros. inversion_clear H. inversion_clear H0 as [Z]. inversion_clear H as [next]. inversion_clear H0 as [nint_]. exists Z; exists next. decompose [and] H; clear H. assert (Htmp : multiplier.utoZ m < Zbeta 2 * (Zpower 2 multiplier.acx_size - 1)). apply Zlt_le_trans with (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; trivial. split; trivial. split. Inde_mult_maddu. split; trivial. split; trivial. split; trivial. split. rewrite H1. assumption. split. rewrite multiplier.maddu_utoZ. rewrite H6. unfold one32. rewrite umul_1. rewrite zero_extend_u2Z_32. apply Zlt_le_trans with ((Zbeta 1 - 1) + (2 * Zbeta 1 - 1)). apply Zplus_le_lt_compat. apply max_u2Z_32'. assumption. unfold Zbeta. simpl. Constraint_constant. assumption. split. rewrite H17. rewrite H13 in H1. rewrite H7 in H1. rewrite H1. reflexivity. inversion_clear H19 as [K]. inversion_clear H. exists K. split. rewrite H13 in H1. rewrite H7 in H1. generalize (Z_of_nat_inj _ _ H1); clear H1; intro H1. subst nint_. rewrite <-H18. rewrite multiplier.maddu_utoZ. rewrite H6. unfold one32. rewrite umul_1. rewrite zero_extend_u2Z_32. rewrite Zmult_plus_distr_l. rewrite Zplus_assoc. unfold Sum_hole. rewrite plus_minus_assoc. rewrite <-minus_n_n. rewrite <-plus_n_O. rewrite multiplier.utoZ_def. rewrite multiplier.utoZ_acx_beta2. rewrite Z2u_injection. rewrite Zmult_0_l. rewrite <-Zplus_0_r_reverse. rewrite concat_u2Z''. assert (length Z > 0)%nat. rewrite H0; assumption. generalize (list_last _ _ H); clear H; intro _X; inversion_clear _X as [Z' _Y]; inversion_clear _Y as [tl]. pattern Z at 2. rewrite H. rewrite app_ass. assert (length Z' = nk - 1)%nat. rewrite H in H0; rewrite length_app in H0; simpl in H0. apply plus_minus. rewrite plus_comm. symmetry. assumption. simpl. rewrite (del_nth_app _ (nk-1) Z' H1 (Z' ++ tl::gpr.lookup C s::nil) tl (gpr.lookup C s :: nil)); auto. generalize (Sum_remove_last _ (Z' ++ gpr.lookup C s :: nil) (nk-1)); intro. pattern (Sum (nk - 1) (Z' ++ gpr.lookup C s :: nil)) in H20. rewrite <-Sum_beyond in H20. rewrite nth_app in H20. cutrewrite (nk - 1 - length Z' = 0)%nat in H20. simpl nth in H19. cutrewrite (S(nk-1)=nk) in H20. rewrite H20. rewrite (Zmult_plus_distr_r (Zbeta (next + 1))). assert ( Sum (nk - 1) Z = Sum (nk - 1) Z' ). rewrite H. rewrite <- (Sum_beyond (nk-1) 32 Z'). reflexivity. rewrite H in H0. rewrite length_app in H0. assumption. rewrite H21. rewrite <-Zbeta_power. rewrite Zmult_assoc. rewrite <-Zbeta_is_exp. cutrewrite (next + 1 + (nk - 1) = next + nk)%nat. rewrite (Zmult_comm (Zbeta (next + nk))). rewrite (Zplus_comm (u2Z (multiplier.lo m))). reflexivity. rewrite <-plus_assoc. rewrite le_plus_minus_r. reflexivity. red in Hk. red in Hk. assumption. rewrite minus_Sn_m. simpl. rewrite <-minus_n_O. reflexivity. red in Hk. red in Hk. assumption. rewrite H1. rewrite <-minus_n_n. reflexivity. rewrite H1; constructor. assumption. Constraint. apply Zlt_le_trans with (2 * Zbeta 1 - 1). assumption. unfold Zbeta. simpl. Constraint_constant. constructor. exact Htmp. assumption. (********************* mflhxu Z_; ********************) apply semax_mflhxu'' with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup mont.m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e mont.m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (next < nk)%nat /\ gpr.lookup X_ s = nth next X zero32 /\ multiplier.utoZ m0 < 3 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * (Z_of_nat nk - 1) /\ (exists K, Zbeta (next + 1) * Sum (nk-1) Z + u2Z (multiplier.lo m0) * Zbeta (next + nk + 1) + u2Z (gpr.lookup Z_ s) * Zbeta (next + nk) = Sum next X * Sum nk Y + Sum nk Y * u2Z (nth next X zero32) * Zbeta next + Sum nk M * u2Z (gpr.lookup quot s) * Zbeta next + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. red. exists Z; exists next. 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; trivial. split; trivial. split; trivial. split. Inde_update_store. Inde_mult_mflhxu_op. split; trivial. split; trivial. split; trivial. split. apply multiplier.mflhxu_kbeta1_utoZ. apply Zlt_trans with (3 * Zbeta 1 - 2). assumption. unfold Zbeta. simpl. Constraint_constant. split; trivial. inversion_clear H16 as [K]. inversion_clear H. exists K. split. rewrite <-H15. rewrite multiplier.lo_mflhxu_op. rewrite multiplier.utoZ_def. rewrite multiplier.utoZ_acx_beta2. rewrite Z2u_injection. rewrite Zmult_0_l. rewrite <-Zplus_0_r_reverse. rewrite Zmult_plus_distr_l. rewrite <-Zmult_assoc. rewrite <-Zbeta_is_exp. rewrite (plus_comm 1). ring. Constraint. apply Zlt_le_trans with (3 * Zbeta 1 -2). assumption. unfold Zbeta. simpl. Constraint_constant. assumption. (********************* addiu ext ext one16; ********************) apply semax_addiu'' with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup mont.m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e mont.m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (1<= next <= nk)%nat /\ multiplier.utoZ m0 < 3 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * (Z_of_nat nk - 1) /\ (exists K, Zbeta next * Sum (nk-1) Z + u2Z (multiplier.lo m0) * Zbeta (next + nk) + u2Z (gpr.lookup Z_ s) * Zbeta (next + nk - 1) = Sum (next-1) X * Sum nk Y + Sum nk Y * u2Z (nth (next-1) X zero32) * Zbeta (next-1) + Sum nk M * u2Z (gpr.lookup quot s) * Zbeta (next-1) + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M + (Zbeta 1 - 1) * (Zbeta (next - 1) * Sum nk M) < 2 * Sum nk M * Zbeta next) ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. red. exists Z; exists (next+1)%nat. 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; trivial. split; trivial. split; trivial. split. Inde_update_store. split. Rewrite_u2Z. rewrite H9. rewrite inj_plus. simpl Z_of_nat. reflexivity. Constraint. rewrite H9. Constraint_variable. Constraint. split. split. rewrite plus_comm. apply le_plus_trans. constructor. red in H10. rewrite S_to_plus_one in H10. rewrite plus_comm in H10. assumption. split; trivial. split; trivial. inversion_clear H15 as [K]. inversion_clear H. exists K. split. cutrewrite (next + 1 - 1 = next)%nat. rewrite <-H14. cutrewrite (next + 1 + nk - 1 = next + nk)%nat. cutrewrite (next + 1 + nk = next + nk + 1)%nat. auto. ring. symmetry. apply plus_minus. ring. rewrite plus_minus_assoc. rewrite <-minus_n_n. rewrite <-plus_n_O. reflexivity. constructor. cutrewrite (Sum (next+1) X = Sum (S next) X). rewrite <-Sum_remove_last_32. rewrite Zmult_plus_distr_l. apply Zlt_le_trans with (2 * Sum nk M * Zbeta next + u2Z (nth next X zero32) * Zbeta next * Sum nk Y + (Zbeta 1 - 1) * Zbeta (next + 1 - 1) * Sum nk M). apply Zplus_lt_le_compat. omega. rewrite Zmult_assoc. apply Zle_refl. apply Zle_trans with ( 2 * Sum nk M * Zbeta next + (Zbeta 1 - 1) * Zbeta next * Sum nk Y + (Zbeta 1 - 1) * Zbeta (next + 1 - 1) * Sum nk M). apply Zplus_le_compat. apply Zplus_le_compat. apply Zle_refl. rewrite <-Zmult_assoc. rewrite <-Zmult_assoc. apply Zmult_le_compat_r. apply max_u2Z_32'. apply Zmult_le_0_compat. generalize (Zbeta_1 next); intro. omega. apply Sum_pos. apply Zle_refl. rewrite <-Zplus_assoc. rewrite plus_minus_assoc. rewrite <-minus_n_n. rewrite <-plus_n_O. apply Zle_trans with (2 * Sum nk M * Zbeta next + ((Zbeta 1 - 1) * Zbeta next * Sum nk M + (Zbeta 1 - 1) * Zbeta next * Sum nk M)). apply Zplus_le_compat. apply Zle_refl. apply Zplus_le_compat. apply Zmult_le_compat_l. omega. apply Zmult_le_0_compat. unfold Zbeta. simpl. Constraint_constant. generalize (Zbeta_1 next); intro. omega. apply Zle_refl. cutrewrite ( 2 * Sum nk M * Zbeta next + ((Zbeta 1 - 1) * Zbeta next * Sum nk M + (Zbeta 1 - 1) * Zbeta next * Sum nk M) = 2 * Sum nk M * Zbeta (next + 1) ). apply Zle_refl. rewrite Zbeta_is_exp. ring. constructor. cutrewrite (next + 1 = S next)%nat. reflexivity. ring. (********************* sw Z_ zero16 t; ********************) apply semax_sw_backwards'' with (fun s s' m0 h => exists Z, exists next, length Z = nk /\ gpr.lookup x s = vx /\ gpr.lookup y s = vy /\ gpr.lookup z s = vz /\ gpr.lookup m s = vm /\ gpr.lookup one s = one32 /\ u2Z (gpr.lookup k s) = Z_of_nat nk /\ gpr.lookup alpha s = valpha /\ ((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> Z) ** (var_e m |--> M)) s s' m0 h /\ u2Z (gpr.lookup ext s) = Z_of_nat next /\ (1 <= next <= nk)%nat /\ multiplier.utoZ m0 < 3 /\ u2Z (gpr.lookup t s) = 4 * nz + 4 * (Z_of_nat nk - 1) /\ (exists K, Zbeta next * Sum nk Z + u2Z (multiplier.lo m0) * Zbeta (next + nk) = Sum (next-1) X * Sum nk Y + Sum nk Y * u2Z (nth (next-1) X zero32) * Zbeta (next-1) + Sum nk M * u2Z (gpr.lookup quot s) * Zbeta (next-1) + K * Sum nk M /\ Sum next X * Sum nk Y + K * Sum nk M + (Zbeta 1 - 1) * (Zbeta (next - 1) * Sum nk M) < 2 * Sum nk M * Zbeta next) ). red; intros. inversion_clear H as [Z]. inversion_clear H0 as [next]. decompose [and] H; clear H. assert (Htmp : eval (add_e (var_e z) (shl2_e (int_e (Z2u 32 (Z_of_nat nk - 1))))) s = eval (add_e (var_e t) (int_e (sign_extend_16_32 zero16))) s). simpl. apply u2Z_injection. Rewrite_u2Z. rewrite H3. rewrite H12. rewrite Hvz. ring. Constraint. Constraint_variable. Constraint. split. omega. Constraint_variable. Constraint_variable. split. omega. Constraint_variable. rewrite H3. Constraint_variable. split. omega. Constraint_variable. Constraint. split. omega. Constraint_variable. assert (length Z > 0)%nat. rewrite H0; assumption. generalize (list_last _ _ H); clear H; intro _X; inversion_clear _X as [lst1]. inversion_clear H as [last]. exists (int_e last). assert (((var_e x |--> X) ** (var_e y |--> Y) ** (var_e z |--> lst1) ** (add_e (var_e z) (shl2_e (int_e (Z2u 32 (Z_of_nat nk - 1)))) |-> int_e last) ** (var_e mont.m |--> M) ) s s' m h). Monotony H8. Monotony H. rewrite sep.con_com_equiv in H. rewrite <-sep.con_assoc_equiv. rewrite sep.con_com_equiv. Monotony H. cutrewrite (1=Z_of_nat 1). rewrite <-inj_minus1. apply (mapstos_decompose_last lst1 nk Z last (nk-1)). assumption. rewrite H14 in H0; simpl in H0; rewrite length_app in H0; simpl in H0. apply plus_minus. rewrite <-H0; apply plus_comm. assumption. simpl eval. rewrite H3. split. omega. reflexivity. assumption. assumption. reflexivity. generalize H; clear H. rotate_sepcon. rotate_sepcon. rotate_sepcon. rotate_sepcon. rotate_sepcon. apply monotony. split. intros. eapply mapsto_equiv'. apply H. exact Htmp. reflexivity. intros. Adjunction H. exists (update_list Z (nk - 1) (gpr.lookup Z_ s)). exists next. split. apply length_update_list; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. split. Monotony H. Monotony H. generalize H; clear H. rotate_sepcon. rotate_sepcon. intro. rewrite sep.con_com_equiv. Monotony H. eapply mapstos_compose_last with (w:=gpr.lookup Z_ s) (n:=nk) (lst1:=lst1) (nj:=(nk-1)%nat) (e':=add_e (var_e t) (int_e (sign_extend_16_32 zero16))). apply length_update_list. assumption. rewrite H14 in H0; rewrite length_app in H0; simpl in H0. apply plus_minus. rewrite <-H0; apply plus_comm. rewrite H14. rewrite update_list_app. simpl. cutrewrite (length lst1 = nk - 1 )%nat. rewrite <-minus_n_n. reflexivity. rewrite H14 in H0; rewrite length_app in H0; simpl in H0. apply plus_minus. rewrite <-H0; apply plus_comm. rewrite H14 in H0; rewrite length_app in H0; simpl in H0. apply plus_le_minus. rewrite H0; constructor. simpl eval. rewrite H3; rewrite Hvz. split. assumption. simpl in Htmp. rewrite <-Htmp. rewrite H3. rewrite inj_minus1. simpl Z_of_nat. reflexivity. assumption. assumption. split; trivial. split; trivial. split; trivial. split; trivial. split; trivial. inversion_clear H15 as [K]. inversion_clear H16. exists K. split. rewrite <-H15. assert (update_list Z (nk - 1) (gpr.lookup Z_ s) = lst1 ++ (gpr.lookup Z_ s)::nil). rewrite H14. rewrite update_list_app. simpl update_list. cutrewrite (nk-1-length lst1=0)%nat. auto. rewrite H14 in H0. rewrite length_app in H0. simpl in H0. rewrite <-H0. symmetry. apply plus_minus. symmetry. apply plus_minus. ring. rewrite H14 in H0. rewrite length_app in H0. simpl in H0. apply plus_le_minus. rewrite H0; constructor. rewrite H16. rewrite (Sum_cut_last nk). rewrite Zmult_plus_distr_r. rewrite Zmult_assoc. rewrite <-Zbeta_is_exp. cutrewrite (next+(nk-1)=next+nk-1)%nat. ring. rewrite Zmult_comm. rewrite H14. rewrite <- (Sum_beyond (nk-1) 32 lst1). reflexivity. rewrite H14 in H0; rewrite length_app in H0; simpl in H0. apply plus_minus. rewrite <-H0; apply plus_comm. rewrite plus_minus_assoc. reflexivity. red in Hk. red in Hk. assumption. assumption. rewrite length_app. simpl. rewrite H14 in H0. rewrite length_app in H0. simpl in H0. assumption. assumption. (********************* mflhxu C ********************) apply semax_mflhxu'. red; intros. red. inversion_clear H as [Z]. inversion_clear H0 as [next]. exists Z; exists next. decompose [and] H; clear H. 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; trivial. split; trivial. split; trivial. split. Inde_mult_mflhxu_op. Inde_update_store. split; trivial. split. rewrite H9; rewrite H6. apply Z_of_nat_le_inj'. assumption. split; trivial. inversion_clear H15 as [K]. inversion_clear H. exists (K + u2Z (gpr.lookup quot s) * Zbeta (next - 1)). split. rewrite Sum_cut_last. cutrewrite (nk+1-1=nk)%nat. rewrite Zmult_plus_distr_r. rewrite Zmult_assoc. rewrite <-Zbeta_is_exp. rewrite (Zmult_comm (Zbeta (next+nk))). assert (Sum (next - 1) X + u2Z (nth (next - 1) X zero32) * Zbeta (next - 1) = Sum next X). assert (next-1