Library copy_triple
Require Import ssreflect ssrbool.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int.
Import MachineInt.
Require Import mips_seplog mips_tactics mips_contrib mapstos.
Require Import copy_prg.
Local Open Scope machine_int_scope.
Local Open Scope heap_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope nodup_scope.
Import expr_m.
Local Open Scope mips_expr_scope.
Import assert_m.
Local Open Scope mips_assert_scope.
Local Open Scope mips_cmd_scope.
Local Open Scope mips_hoare_scope.
Lemma copy_triple : forall rk rx ry tmp ytmp i,
nodup(rk, rx, ry, tmp, ytmp, i, r0) ->
forall X Y nk, length X = nk -> length Y = nk ->
forall ny, u2Z ny + 4 * Z_of_nat nk < Zbeta 1 ->
{{ fun s h =>
[ry]_s = ny /\
u2Z [rk]_s = Z_of_nat nk /\
(var_e rx |--> X ** var_e ry |--> Y) s h }}
copy rk ry rx tmp ytmp i
{{ fun s h =>
[ry]_s = ny /\
u2Z [rk]_s = Z_of_nat nk /\
(var_e rx |--> X ** var_e ry |--> X) s h }}.
Proof.
move=> rk rx ry tmp ytmp i Hset X Y nk len_X len_Y ny Hfit.
rewrite /copy.
apply mips_contrib.hoare_addiu with (fun s h =>
[ry]_s = ny /\
u2Z [rk ]_ s = Z_of_nat nk /\
[ytmp]_s = [ry]_s /\
(var_e rx |--> X ** var_e ry |--> Y) s h).
move=> s h [r_y [r_k mem]].
rewrite /mips_seplog.wp_addiu.
repeat reg_upd; repeat (split; trivial).
by rewrite sext_Z2u // add_0.
by Assert_upd.
apply mips_contrib.hoare_addiu with (fun s h =>
[ry]_s = ny /\
u2Z ([rk ]_ s) = Z_of_nat nk /\
[ytmp]_s = [ry]_s /\
[i]_s = zero32 /\
(var_e rx |--> X ** var_e ry |--> Y) s h).
move=> s h [r_y [r_k [r_ytmp mem]]].
rewrite /mips_seplog.wp_addiu.
repeat reg_upd; repeat (split => //).
by rewrite sext_Z2u // add_0.
by Assert_upd.
apply mips_seplog.hoare_prop_m.hoare_while_invariant with (fun s h =>
[ry]_s = ny /\
u2Z [rk ]_ s = Z_of_nat nk /\
u2Z [ytmp]_s = u2Z [ry]_s + u2Z [i]_s * 4 /\
u2Z [i]_s <= Z_of_nat nk /\
(var_e rx |--> X ** var_e ry |-->
firstn (Zabs_nat (u2Z [i]_s)) X ++
skipn (Zabs_nat (u2Z [i]_s)) Y) s h).
move=> s h [r_y [r_k [r_ytmp [r_i mem]]]].
repeat (split; trivial).
by rewrite r_i u2Z_Z2u // Zmult_0_l Zplus_0_r r_ytmp.
rewrite r_i u2Z_Z2u //; by apply Zle_0_nat.
by rewrite r_i u2Z_Z2u.
move=> s h [[r_y [r_k [r_ytmp [r_i mem]]]] i_k].
repeat (split; trivial).
move/negPn : i_k. move/Zeq_boolP. move/u2Z_inj => /= i_k.
rewrite i_k r_k Zabs_nat_Z_of_nat in mem.
rewrite firstn_all in mem; last by rewrite len_X.
by rewrite skipn_all // -app_nil_end in mem.
apply mips_contrib.hoare_lwxs_back_alt'' with (fun s h =>
[ry]_s = ny /\
u2Z [rk ]_ s = Z_of_nat nk /\
u2Z [ytmp]_s = u2Z [ry]_s + u2Z [i]_s * 4 /\
u2Z [i]_s < Z_of_nat nk /\
[tmp]_s = nth (Zabs_nat (u2Z [i ]_ s)) X zero32 /\
(var_e rx |--> X **
var_e ry |--> firstn (Zabs_nat (u2Z [i ]_ s)) X ++
skipn (Zabs_nat (u2Z [i ]_ s)) Y) s h).
move=> s h [[r_y [r_k [r_ytmp [i_k' mem]]]] i_k].
move/Zeq_boolP : i_k => /= i_k.
exists (nth (Zabs_nat (u2Z [i ]_ s)) X zero32); split.
Decompose_32 X (Zabs_nat (u2Z ([i ]_ s))) X1 X2 HlenX1 HX'; last first.
apply Z_of_nat_lt_inj.
rewrite Z_of_nat_Zabs_nat //.
- rewrite len_X.
apply Zle_neq_lt => //.
by rewrite -r_k.
- by apply min_u2Z.
rewrite {1}HX' in mem.
rewrite (mapstos.decompose_equiv _ _ _ _ _ HlenX1) in mem.
rewrite !assert_m.con_assoc_equiv in mem.
rewrite assert_m.con_com_equiv in mem.
rewrite !assert_m.con_assoc_equiv in mem.
move: mem; apply assert_m.monotony => h' //.
apply assert_m.mapsto_ext => //.
rewrite [mult]lock /= -lock.
f_equal.
apply u2Z_inj.
have Htmp : u2Z ([i ]_ s) < 2 ^^ 30.
apply Zle_lt_trans with (Z_of_nat nk) => //.
apply Zmult_lt_reg_l with 4 => //.
rewrite (_ : 4 = Zpower 2 2) // -Zpower_is_exp //.
rewrite [plus _ _]/= -Zbeta1_Zpower2 [Zpower _ _]/=.
move: (min_u2Z ([ry]_s)); rewrite r_y => ?; omega.
rewrite u2Z_Z2u; last first.
split; first by apply Zle_0_nat.
rewrite inj_mult. simpl Z_of_nat.
rewrite {2}(_ : 32 = 2 + 30)%nat // Zpower_is_exp.
simpl (Zpower 2 2).
apply Zmult_lt_compat_l => //.
rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
rewrite (@u2Z_shl _ 32 _ 30) //; last first.
rewrite inj_mult. simpl Z_of_nat.
rewrite Z_of_nat_Zabs_nat; last by apply min_u2Z.
simpl Zpower; ring.
rewrite /mips_contrib.update_store_lwxs.
repeat reg_upd; repeat (split => //).
- omega.
- by Assert_upd.
apply mips_contrib.hoare_sw_back'' with (fun s h =>
[ry]_s = ny /\
u2Z [rk ]_ s = Z_of_nat nk /\
u2Z [ytmp]_s = u2Z [ry]_s + u2Z [i]_s * 4 /\
u2Z [i]_s < Z_of_nat nk /\
(var_e rx |--> X **
var_e ry |--> firstn (Zabs_nat (u2Z [i ]_ s + 1)) X ++
skipn (Zabs_nat (u2Z [i ]_ s + 1)) Y) s h).
move=> s h [r_y [r_k [r_ytmp [r_i [r_tmp mem]]]]].
set ni := Zabs_nat (u2Z ([i]_s)) in mem.
exists (int_e (nth O (skipn ni Y) zero32)).
Decompose_32 (firstn ni X ++ skipn ni Y) (Zabs_nat (u2Z ([i ]_ s))) XY1 XY2 HlenXY1 HXY'; last first.
rewrite app_length (len_firstn nk) //; last first.
apply Z_of_nat_le_inj.
rewrite Z_of_nat_Zabs_nat; [omega | by apply min_u2Z].
rewrite len_skipn -le_plus_minus; last first.
rewrite len_Y.
apply Z_of_nat_le_inj.
rewrite Z_of_nat_Zabs_nat; [omega | by apply min_u2Z].
rewrite len_Y.
apply Z_of_nat_lt_inj.
rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
have Htmp : [add_e (var_e ry)
(int_e (Z2u 32 (Z_of_nat (4 * ni)))) ]e_ s =
[add_e (var_e ytmp) (int_e (Z2u (16 + 16) 0)) ]e_ s.
rewrite [mult]lock /= -lock.
apply u2Z_inj.
rewrite add_0 r_ytmp u2Z_add_Z2u //.
rewrite inj_mult.
rewrite [Z_of_nat _]/= Z_of_nat_Zabs_nat //; [ring | by apply min_u2Z].
by apply Zle_0_nat.
rewrite inj_mult [Z_of_nat _]/=.
rewrite Z_of_nat_Zabs_nat //; last by apply min_u2Z.
rewrite r_y -Zbeta1_Zpower2; omega.
rewrite HXY' /= in mem.
rewrite (mapstos.decompose_equiv _ _ _ _ _ HlenXY1) in mem.
rewrite !assert_m.con_assoc_equiv in mem.
rewrite assert_m.con_com_equiv in mem.
rewrite !assert_m.con_assoc_equiv in mem.
rewrite assert_m.con_com_equiv in mem.
rewrite !assert_m.con_assoc_equiv in mem.
move: mem.
apply assert_m.monotony => // h'.
apply assert_m.mapsto_ext => //.
by rewrite sext_Z2u //.
rewrite app_nth2; last first.
rewrite (len_firstn nk) //.
apply Z_of_nat_le_inj.
rewrite /ni.
rewrite Z_of_nat_Zabs_nat; [omega | by apply min_u2Z].
rewrite (len_firstn nk) //; last first.
apply Z_of_nat_le_inj.
rewrite /ni.
rewrite Z_of_nat_Zabs_nat; [omega | by apply min_u2Z].
by rewrite -minus_n_n.
rewrite -/ni.
apply assert_m.currying => h'' Hh''.
repeat (split => //).
rewrite !assert_m.con_assoc_equiv in Hh''.
rewrite assert_m.con_com_equiv in Hh''.
rewrite !assert_m.con_assoc_equiv in Hh''.
move: Hh''.
apply assert_m.monotony => h''' //.
have -> : Zabs_nat (u2Z ([i ]_ s) + 1) = S ni.
rewrite Zabs_nat_plus_pos //.
by rewrite plus_comm.
by apply min_u2Z.
rewrite (firstn_S zero32); last first.
rewrite len_X.
apply Z_of_nat_lt_inj.
rewrite /ni.
rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
rewrite app_ass (mapstos.decompose_equiv _ ni); last first.
rewrite (len_firstn nk) //.
apply Z_of_nat_le_inj.
rewrite /ni.
rewrite Z_of_nat_Zabs_nat; [omega | by apply min_u2Z].
rewrite !assert_m.con_assoc_equiv.
apply app_inv in HXY'; last first.
rewrite (len_firstn nk) //.
apply Z_of_nat_le_inj.
rewrite /ni.
rewrite Z_of_nat_Zabs_nat; [omega | by apply min_u2Z].
apply assert_m.monotony => h4 //.
suff : XY1 = firstn ni X by move=> ->.
symmetry; tauto.
apply assert_m.monotony => h5r //.
apply assert_m.mapsto_ext => //.
by rewrite /= sext_Z2u // add_0.
suff : XY2 = skipn (S ni) Y by move=> ->.
rewrite {1}(skipn_S zero32) in HXY'.
- case: HXY' => _ HXY'.
by case: HXY' => _ HXY'.
- rewrite /ni.
apply Z_of_nat_lt_inj.
rewrite Z_of_nat_Zabs_nat //.
rewrite len_Y; omega.
by apply min_u2Z.
apply mips_contrib.hoare_addiu with (fun s h =>
[ry]_s = ny /\
u2Z [rk ]_ s = Z_of_nat nk /\
u2Z [ytmp]_s = u2Z [ry]_s + (u2Z [i]_s - 1) * 4 /\
u2Z [i]_s <= Z_of_nat nk /\
(var_e rx |--> X **
var_e ry |--> firstn (Zabs_nat (u2Z [i ]_ s)) X ++
skipn (Zabs_nat (u2Z [i ]_ s)) Y) s h).
move=> s h [r_y [r_k [r_ytmp [r_i mem]]]].
rewrite /mips_seplog.wp_addiu.
repeat reg_upd; repeat (split; trivial).
rewrite r_ytmp.
f_equal.
rewrite sext_Z2u // u2Z_add_Z2u //.
ring.
rewrite -Zbeta1_Zpower2.
move: (min_u2Z ([ry]_s)); rewrite r_y => ?; omega.
rewrite sext_Z2u // u2Z_add_Z2u //.
omega.
rewrite -Zbeta1_Zpower2.
move: (min_u2Z ([ry]_s)); rewrite r_y => ?; omega.
rewrite sext_Z2u // u2Z_add_Z2u //; last first.
rewrite -Zbeta1_Zpower2.
move: (min_u2Z ([ry]_s)); rewrite r_y => ?; omega.
by Assert_upd.
apply mips_contrib.hoare_addiu'.
move=> s h [r_y [r_k [r_ytmp [i_k mem]]]].
rewrite /mips_seplog.wp_addiu.
repeat reg_upd; repeat (split; trivial).
rewrite sext_Z2u // u2Z_add_Z2u //; last first.
rewrite r_ytmp r_y -Zbeta1_Zpower2 -{2}(Zmult_1_l 4) -Zplus_assoc -Zmult_plus_distr_l Zmult_comm; omega.
rewrite r_ytmp; ring.
by Assert_upd.
Qed.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int.
Import MachineInt.
Require Import mips_seplog mips_tactics mips_contrib mapstos.
Require Import copy_prg.
Local Open Scope machine_int_scope.
Local Open Scope heap_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope nodup_scope.
Import expr_m.
Local Open Scope mips_expr_scope.
Import assert_m.
Local Open Scope mips_assert_scope.
Local Open Scope mips_cmd_scope.
Local Open Scope mips_hoare_scope.
Lemma copy_triple : forall rk rx ry tmp ytmp i,
nodup(rk, rx, ry, tmp, ytmp, i, r0) ->
forall X Y nk, length X = nk -> length Y = nk ->
forall ny, u2Z ny + 4 * Z_of_nat nk < Zbeta 1 ->
{{ fun s h =>
[ry]_s = ny /\
u2Z [rk]_s = Z_of_nat nk /\
(var_e rx |--> X ** var_e ry |--> Y) s h }}
copy rk ry rx tmp ytmp i
{{ fun s h =>
[ry]_s = ny /\
u2Z [rk]_s = Z_of_nat nk /\
(var_e rx |--> X ** var_e ry |--> X) s h }}.
Proof.
move=> rk rx ry tmp ytmp i Hset X Y nk len_X len_Y ny Hfit.
rewrite /copy.
apply mips_contrib.hoare_addiu with (fun s h =>
[ry]_s = ny /\
u2Z [rk ]_ s = Z_of_nat nk /\
[ytmp]_s = [ry]_s /\
(var_e rx |--> X ** var_e ry |--> Y) s h).
move=> s h [r_y [r_k mem]].
rewrite /mips_seplog.wp_addiu.
repeat reg_upd; repeat (split; trivial).
by rewrite sext_Z2u // add_0.
by Assert_upd.
apply mips_contrib.hoare_addiu with (fun s h =>
[ry]_s = ny /\
u2Z ([rk ]_ s) = Z_of_nat nk /\
[ytmp]_s = [ry]_s /\
[i]_s = zero32 /\
(var_e rx |--> X ** var_e ry |--> Y) s h).
move=> s h [r_y [r_k [r_ytmp mem]]].
rewrite /mips_seplog.wp_addiu.
repeat reg_upd; repeat (split => //).
by rewrite sext_Z2u // add_0.
by Assert_upd.
apply mips_seplog.hoare_prop_m.hoare_while_invariant with (fun s h =>
[ry]_s = ny /\
u2Z [rk ]_ s = Z_of_nat nk /\
u2Z [ytmp]_s = u2Z [ry]_s + u2Z [i]_s * 4 /\
u2Z [i]_s <= Z_of_nat nk /\
(var_e rx |--> X ** var_e ry |-->
firstn (Zabs_nat (u2Z [i]_s)) X ++
skipn (Zabs_nat (u2Z [i]_s)) Y) s h).
move=> s h [r_y [r_k [r_ytmp [r_i mem]]]].
repeat (split; trivial).
by rewrite r_i u2Z_Z2u // Zmult_0_l Zplus_0_r r_ytmp.
rewrite r_i u2Z_Z2u //; by apply Zle_0_nat.
by rewrite r_i u2Z_Z2u.
move=> s h [[r_y [r_k [r_ytmp [r_i mem]]]] i_k].
repeat (split; trivial).
move/negPn : i_k. move/Zeq_boolP. move/u2Z_inj => /= i_k.
rewrite i_k r_k Zabs_nat_Z_of_nat in mem.
rewrite firstn_all in mem; last by rewrite len_X.
by rewrite skipn_all // -app_nil_end in mem.
apply mips_contrib.hoare_lwxs_back_alt'' with (fun s h =>
[ry]_s = ny /\
u2Z [rk ]_ s = Z_of_nat nk /\
u2Z [ytmp]_s = u2Z [ry]_s + u2Z [i]_s * 4 /\
u2Z [i]_s < Z_of_nat nk /\
[tmp]_s = nth (Zabs_nat (u2Z [i ]_ s)) X zero32 /\
(var_e rx |--> X **
var_e ry |--> firstn (Zabs_nat (u2Z [i ]_ s)) X ++
skipn (Zabs_nat (u2Z [i ]_ s)) Y) s h).
move=> s h [[r_y [r_k [r_ytmp [i_k' mem]]]] i_k].
move/Zeq_boolP : i_k => /= i_k.
exists (nth (Zabs_nat (u2Z [i ]_ s)) X zero32); split.
Decompose_32 X (Zabs_nat (u2Z ([i ]_ s))) X1 X2 HlenX1 HX'; last first.
apply Z_of_nat_lt_inj.
rewrite Z_of_nat_Zabs_nat //.
- rewrite len_X.
apply Zle_neq_lt => //.
by rewrite -r_k.
- by apply min_u2Z.
rewrite {1}HX' in mem.
rewrite (mapstos.decompose_equiv _ _ _ _ _ HlenX1) in mem.
rewrite !assert_m.con_assoc_equiv in mem.
rewrite assert_m.con_com_equiv in mem.
rewrite !assert_m.con_assoc_equiv in mem.
move: mem; apply assert_m.monotony => h' //.
apply assert_m.mapsto_ext => //.
rewrite [mult]lock /= -lock.
f_equal.
apply u2Z_inj.
have Htmp : u2Z ([i ]_ s) < 2 ^^ 30.
apply Zle_lt_trans with (Z_of_nat nk) => //.
apply Zmult_lt_reg_l with 4 => //.
rewrite (_ : 4 = Zpower 2 2) // -Zpower_is_exp //.
rewrite [plus _ _]/= -Zbeta1_Zpower2 [Zpower _ _]/=.
move: (min_u2Z ([ry]_s)); rewrite r_y => ?; omega.
rewrite u2Z_Z2u; last first.
split; first by apply Zle_0_nat.
rewrite inj_mult. simpl Z_of_nat.
rewrite {2}(_ : 32 = 2 + 30)%nat // Zpower_is_exp.
simpl (Zpower 2 2).
apply Zmult_lt_compat_l => //.
rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
rewrite (@u2Z_shl _ 32 _ 30) //; last first.
rewrite inj_mult. simpl Z_of_nat.
rewrite Z_of_nat_Zabs_nat; last by apply min_u2Z.
simpl Zpower; ring.
rewrite /mips_contrib.update_store_lwxs.
repeat reg_upd; repeat (split => //).
- omega.
- by Assert_upd.
apply mips_contrib.hoare_sw_back'' with (fun s h =>
[ry]_s = ny /\
u2Z [rk ]_ s = Z_of_nat nk /\
u2Z [ytmp]_s = u2Z [ry]_s + u2Z [i]_s * 4 /\
u2Z [i]_s < Z_of_nat nk /\
(var_e rx |--> X **
var_e ry |--> firstn (Zabs_nat (u2Z [i ]_ s + 1)) X ++
skipn (Zabs_nat (u2Z [i ]_ s + 1)) Y) s h).
move=> s h [r_y [r_k [r_ytmp [r_i [r_tmp mem]]]]].
set ni := Zabs_nat (u2Z ([i]_s)) in mem.
exists (int_e (nth O (skipn ni Y) zero32)).
Decompose_32 (firstn ni X ++ skipn ni Y) (Zabs_nat (u2Z ([i ]_ s))) XY1 XY2 HlenXY1 HXY'; last first.
rewrite app_length (len_firstn nk) //; last first.
apply Z_of_nat_le_inj.
rewrite Z_of_nat_Zabs_nat; [omega | by apply min_u2Z].
rewrite len_skipn -le_plus_minus; last first.
rewrite len_Y.
apply Z_of_nat_le_inj.
rewrite Z_of_nat_Zabs_nat; [omega | by apply min_u2Z].
rewrite len_Y.
apply Z_of_nat_lt_inj.
rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
have Htmp : [add_e (var_e ry)
(int_e (Z2u 32 (Z_of_nat (4 * ni)))) ]e_ s =
[add_e (var_e ytmp) (int_e (Z2u (16 + 16) 0)) ]e_ s.
rewrite [mult]lock /= -lock.
apply u2Z_inj.
rewrite add_0 r_ytmp u2Z_add_Z2u //.
rewrite inj_mult.
rewrite [Z_of_nat _]/= Z_of_nat_Zabs_nat //; [ring | by apply min_u2Z].
by apply Zle_0_nat.
rewrite inj_mult [Z_of_nat _]/=.
rewrite Z_of_nat_Zabs_nat //; last by apply min_u2Z.
rewrite r_y -Zbeta1_Zpower2; omega.
rewrite HXY' /= in mem.
rewrite (mapstos.decompose_equiv _ _ _ _ _ HlenXY1) in mem.
rewrite !assert_m.con_assoc_equiv in mem.
rewrite assert_m.con_com_equiv in mem.
rewrite !assert_m.con_assoc_equiv in mem.
rewrite assert_m.con_com_equiv in mem.
rewrite !assert_m.con_assoc_equiv in mem.
move: mem.
apply assert_m.monotony => // h'.
apply assert_m.mapsto_ext => //.
by rewrite sext_Z2u //.
rewrite app_nth2; last first.
rewrite (len_firstn nk) //.
apply Z_of_nat_le_inj.
rewrite /ni.
rewrite Z_of_nat_Zabs_nat; [omega | by apply min_u2Z].
rewrite (len_firstn nk) //; last first.
apply Z_of_nat_le_inj.
rewrite /ni.
rewrite Z_of_nat_Zabs_nat; [omega | by apply min_u2Z].
by rewrite -minus_n_n.
rewrite -/ni.
apply assert_m.currying => h'' Hh''.
repeat (split => //).
rewrite !assert_m.con_assoc_equiv in Hh''.
rewrite assert_m.con_com_equiv in Hh''.
rewrite !assert_m.con_assoc_equiv in Hh''.
move: Hh''.
apply assert_m.monotony => h''' //.
have -> : Zabs_nat (u2Z ([i ]_ s) + 1) = S ni.
rewrite Zabs_nat_plus_pos //.
by rewrite plus_comm.
by apply min_u2Z.
rewrite (firstn_S zero32); last first.
rewrite len_X.
apply Z_of_nat_lt_inj.
rewrite /ni.
rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
rewrite app_ass (mapstos.decompose_equiv _ ni); last first.
rewrite (len_firstn nk) //.
apply Z_of_nat_le_inj.
rewrite /ni.
rewrite Z_of_nat_Zabs_nat; [omega | by apply min_u2Z].
rewrite !assert_m.con_assoc_equiv.
apply app_inv in HXY'; last first.
rewrite (len_firstn nk) //.
apply Z_of_nat_le_inj.
rewrite /ni.
rewrite Z_of_nat_Zabs_nat; [omega | by apply min_u2Z].
apply assert_m.monotony => h4 //.
suff : XY1 = firstn ni X by move=> ->.
symmetry; tauto.
apply assert_m.monotony => h5r //.
apply assert_m.mapsto_ext => //.
by rewrite /= sext_Z2u // add_0.
suff : XY2 = skipn (S ni) Y by move=> ->.
rewrite {1}(skipn_S zero32) in HXY'.
- case: HXY' => _ HXY'.
by case: HXY' => _ HXY'.
- rewrite /ni.
apply Z_of_nat_lt_inj.
rewrite Z_of_nat_Zabs_nat //.
rewrite len_Y; omega.
by apply min_u2Z.
apply mips_contrib.hoare_addiu with (fun s h =>
[ry]_s = ny /\
u2Z [rk ]_ s = Z_of_nat nk /\
u2Z [ytmp]_s = u2Z [ry]_s + (u2Z [i]_s - 1) * 4 /\
u2Z [i]_s <= Z_of_nat nk /\
(var_e rx |--> X **
var_e ry |--> firstn (Zabs_nat (u2Z [i ]_ s)) X ++
skipn (Zabs_nat (u2Z [i ]_ s)) Y) s h).
move=> s h [r_y [r_k [r_ytmp [r_i mem]]]].
rewrite /mips_seplog.wp_addiu.
repeat reg_upd; repeat (split; trivial).
rewrite r_ytmp.
f_equal.
rewrite sext_Z2u // u2Z_add_Z2u //.
ring.
rewrite -Zbeta1_Zpower2.
move: (min_u2Z ([ry]_s)); rewrite r_y => ?; omega.
rewrite sext_Z2u // u2Z_add_Z2u //.
omega.
rewrite -Zbeta1_Zpower2.
move: (min_u2Z ([ry]_s)); rewrite r_y => ?; omega.
rewrite sext_Z2u // u2Z_add_Z2u //; last first.
rewrite -Zbeta1_Zpower2.
move: (min_u2Z ([ry]_s)); rewrite r_y => ?; omega.
by Assert_upd.
apply mips_contrib.hoare_addiu'.
move=> s h [r_y [r_k [r_ytmp [i_k mem]]]].
rewrite /mips_seplog.wp_addiu.
repeat reg_upd; repeat (split; trivial).
rewrite sext_Z2u // u2Z_add_Z2u //; last first.
rewrite r_ytmp r_y -Zbeta1_Zpower2 -{2}(Zmult_1_l 4) -Zplus_assoc -Zmult_plus_distr_l Zmult_comm; omega.
rewrite r_ytmp; ring.
by Assert_upd.
Qed.