Library multi_is_even_and_simu
Require Import Epsilon.
Require Import ssreflect ssrbool eqtype.
Require Import ZArith_ext Lists_ext.
Require Import machine_int nodup multi_int.
Import MachineInt.
Require Import mips_bipl mips_seplog mips_tactics.
Import expr_m.
Require Import integral_type.
Require Import simu.
Import simu_m.
Require Import begcd_mips_prelude_prg multi_is_even_and_prg multi_is_even_triple.
Local Open Scope zarith_ext_scope.
Local Open Scope machine_int_scope.
Local Open Scope nodup_scope.
Local Open Scope assoc_scope.
Local Open Scope heap_scope.
Local Open Scope mips_expr_scope.
Local Open Scope mips_cmd_scope.
Lemma fwd_sim_b_multi_is_even_and : forall rk ru rv a0 a1 u v d,
nodup(u, v) -> nodup(rk, ru, rv, a0, a1, r0) ->
fwd_sim_b (fun s st h =>
state_mint ((u |=> unsign rk ru \U+ (v |=> unsign rk rv \U+ d ))) s st h)
(var_e u mode nat_e 2 =e nat_e 0 &e var_e v mode nat_e 2 =e nat_e 0)%seplog_expr
(multi_is_even_and rk ru rv a0 a1) (bne a0 r0).
Proof.
move=> rk ru rv a0 a1 u v d u_v Hregs.
- rewrite /fwd_sim_b => s st he Hstate_mint.
have Hset_rx : nodup(rk, ru, a0, r0) by Nodup_nodup r0.
move: (len_Z2ints (Zabs_nat (u2Z [rk]_ st)) 32 ([u ]_ s)%seplog_expr).
move/(multi_is_even_triple _ _ _ Hset_rx _ _) => {Hset_rx} Heven_rx.
have Hset_ry : nodup(rk, rv, a1, r0) by Nodup_nodup r0.
move: (len_Z2ints (Zabs_nat (u2Z [rk ]_ st)) 32 ([v ]_ s)%seplog_expr).
move/(multi_is_even_triple _ _ _ Hset_ry _ _) => {Hset_ry} Heven_ry.
have [st' Hst'] : exists st', Some (st, he) -- multi_is_even_and rk ru rv a0 a1 ---> Some (st', he).
have [[st' he'] Hst'] : exists st', Some (st, he) -- multi_is_even_and rk ru rv a0 a1 ---> Some st'.
apply constructive_indefinite_description'.
apply mips_seplog.hoare_prop_m.termi with (P :=
((fun st0 h => u2Z [rk ]_ st0 = u2Z [rk ]_ st /\ [ru ]_ st0 = [ru ]_ st /\
(var_e ru |--> Z2ints 32 (Zabs_nat (u2Z [rk ]_ st)) ([u ]_ s)%seplog_expr)%mips_assert
st0 h) **
((fun st0 h => u2Z [rk ]_ st0 = u2Z [rk ]_ st /\ [rv ]_ st0 = [rv ]_ st /\
(var_e rv |--> Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([v ]_ s)%seplog_expr)%mips_assert
st0 h) ** assert_m.TT))%mips_assert) (Q := assert_m.TT).
+ eapply while.hoare_seq.
* apply mips_frame.frame_rule.
- rewrite Z_of_nat_Zabs_nat in Heven_rx; last by apply min_u2Z.
by apply Heven_rx.
- by Inde_frame.
- move=> ?; by Inde_mult.
* eapply while.hoare_seq.
- apply mips_contrib.hoare_con_comm_pre.
apply mips_contrib.hoare_con_assoc_pre.
apply mips_frame.frame_rule.
+ rewrite Z_of_nat_Zabs_nat in Heven_ry; last by apply min_u2Z.
by apply Heven_ry.
+ Inde_frame.
* apply assert_m.inde_imp.
apply assert_m.inde_get.
by Nodup_not_In.
* apply assert_m.inde_imp.
apply assert_m.inde_get.
by Nodup_not_In.
+ move=> ?; by Inde_mult.
- by apply mips_contrib.cmd_and_true.
+ move=> st0 h0 H0.
by apply constructive_indefinite_description, mips_syntax.no_while_terminate.
+ exists (heap_mint (unsign rk ru) st he).
exists (heap_mint (unsign rk rv) st he +++ (he [\m] seq.cat
(seq_ext.ran (Zabs_nat (u2Z ([ru ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))
(seq_ext.ran (Zabs_nat (u2Z ([rv ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st)))))).
split.
* apply heap.disj_union_R.
- apply (proj2 Hstate_mint u v).
by Nodup_neq.
by assoc_get_Some.
by assoc_get_Some.
- apply heap.proj_difs_disj.
by rewrite -seq_ext.l2s_seq seq_ext.inc_app_L.
* split.
- by rewrite heap.union_assoc -heap.proj_app 2!seq_ext.l2s_seq -heap.proj_difs.
- split.
+ split.
* done.
* apply (state_mint_var_mint _ _ _ _ u (unsign rk ru)) in Hstate_mint; last by assoc_get_Some.
rewrite /var_mint /var_unsign in Hstate_mint; tauto.
+ apply assert_m.con_cons; last by done.
* apply heap.proj_difs_disj.
by rewrite seq_ext.l2s_seq seq_ext.inc_app_R.
* split; first by reflexivity.
apply (state_mint_var_mint _ _ _ _ v (unsign rk rv)) in Hstate_mint; last by assoc_get_Some.
rewrite /var_mint /var_unsign in Hstate_mint; tauto.
exists st'.
suff : he = he' by move=> X; rewrite -X in Hst'.
by apply (mips_syntax.no_sw_heap_invariant _ _ _ Hst' (refl_equal _) _ _ _ _ (refl_equal _) (refl_equal _)).
exists st'; split; first by done.
case/mips_cmd.semop_prop_m.exec_seq_inv : Hst' => st1 [] Hst1.
case/mips_cmd.semop_prop_m.exec_seq_inv=> st2 [] Hst2 Hst'.
destruct st1 as [[st1 he1]|]; last first.
destruct st2 as [[st2 he2]|]; last first.
by move/semop_prop_m.from_none : Hst'.
by move/semop_prop_m.from_none : Hst2.
have ? : he = he1 by eapply (mips_syntax.no_sw_heap_invariant _ _ _ Hst1).
subst he1.
destruct st2 as [[st2 he2]|]; last by move/semop_prop_m.from_none : Hst'.
have Htmp : he = he2 by eapply (mips_syntax.no_sw_heap_invariant _ _ _ Hst2).
subst he2.
have Hry : [rv ]_ st = [rv ]_ st1.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _ ]/=; by Nodup_not_In.
have Hrk : [rk ]_ st = [rk ]_ st1.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _ ]/=; by Nodup_not_In.
split.
+ rewrite /= /ZIT.t_eqb /ZIT.t_mod.
case/andP. move/eqP => Heval_b1. move/eqP => Heval_b2.
have Ha0 : [ a0 ]_ st1 = one32.
clear Heven_ry.
move/mips_seplog.hoare_prop_m.soundness : (Heven_rx [ru]_st).
rewrite /while.hoare_semantics.
move/(_ st (heap_cut he (Zabs_nat (u2Z ([ru ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))).
rewrite Z_of_nat_Zabs_nat; last by apply min_u2Z.
have Htmp : (var_e ru |-->
Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([u ]_ s)%seplog_expr)%mips_assert
st
(heap_cut he (Zabs_nat (u2Z ([ru ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st)))).
apply (state_mint_var_mint _ _ _ _ u (unsign rk ru)) in Hstate_mint; last by assoc_get_Some.
rewrite /var_mint /var_unsign in Hstate_mint; tauto.
move/(_ (conj (refl_equal _) (conj (refl_equal _) Htmp))) => Heven_rx'.
eapply (proj2 Heven_rx'); clear Heven_rx'.
eapply mips_syntax.triple_exec_proj; first by apply (Heven_rx [ru]_st).
split.
rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
split; first by reflexivity.
exact Htmp.
by apply Hst1.
apply (state_mint_var_mint _ _ _ _ u (unsign rk ru)) in Hstate_mint; last by assoc_get_Some.
rewrite Sum_Z2ints_pos.
+ by apply Zmod_2_Zeven.
+ rewrite /var_mint /var_unsign in Hstate_mint.
rewrite -Zbeta_power; tauto.
have Ha1 : [a1]_st2 = one32.
clear Heven_rx.
move/mips_seplog.hoare_prop_m.soundness : (Heven_ry [rv]_st).
rewrite /while.hoare_semantics.
move/(_ st1 (heap_cut he (Zabs_nat (u2Z [rv ]_ st / 4)) (Zabs_nat (u2Z ([rk ]_ st))))).
have Htmp : u2Z ([rk ]_ st1) = Z_of_nat (Zabs_nat (u2Z ([rk ]_ st))) /\
(var_e rv |--> Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([v ]_ s)%seplog_expr)%mips_assert
st1
(heap_cut he (Zabs_nat (u2Z ([rv ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st)))).
split.
rewrite Z_of_nat_Zabs_nat; last by apply min_u2Z.
f_equal.
symmetry.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
apply (state_mint_var_mint _ _ _ _ v (unsign rk rv)) in Hstate_mint; last by assoc_get_Some.
rewrite /var_mint /heap_mint in Hstate_mint.
case: Hstate_mint => _ [_ Htmp].
move: Htmp; apply assert_m.mapstos_ext => /=.
congruence.
case: Htmp => Htmp1 Htmp2.
symmetry in Hry.
move/(_ (conj Htmp1 (conj Hry Htmp2))) => Heven_ry'.
eapply (proj2 Heven_ry'); clear Heven_ry'.
eapply mips_syntax.triple_exec_proj; first by apply (Heven_ry [rv]_st).
by tauto.
by apply Hst2.
apply (state_mint_var_mint _ _ _ _ v (unsign rk rv)) in Hstate_mint; last by assoc_get_Some.
rewrite Sum_Z2ints_pos.
+ by apply Zmod_2_Zeven.
+ rewrite /var_mint /var_unsign in Hstate_mint.
rewrite -Zbeta_power; tauto.
have {Ha0}Ha0 : [a0 ]_ st2 = one32.
rewrite -Ha0.
symmetry. mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _ ]/=; by Nodup_not_In.
move/mips_cmd.semop_prop_m.exec_cmd0_inv : Hst'.
case/mips_cmd.exec0_and_inv => Hst'.
rewrite Ha1 Ha0 int_and_idempotent in Hst'.
rewrite {1}Hst'.
reg_upd.
by rewrite store.get_r0 !u2Z_Z2u.
+ rewrite /= /ZIT.t_eqb /ZIT.t_mod.
case/nandP.
* move/eqP => Heval_b.
have Ha0 : [a0]_st' = zero32.
have Ha0 : [a0]_st1 = zero32.
clear Heven_ry.
move/mips_seplog.hoare_prop_m.soundness : (Heven_rx [ru]_st).
rewrite /while.hoare_semantics.
move/(_ st (heap_cut he (Zabs_nat (u2Z ([ru ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))).
have Htmp : u2Z [rk ]_ st = Z_of_nat (Zabs_nat (u2Z ([rk ]_ st))) /\
(var_e ru |--> Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([u ]_ s)%seplog_expr)%mips_assert st
(heap_cut he (Zabs_nat (u2Z ([ru ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st)))).
split.
by rewrite Z_of_nat_Zabs_nat; last by apply min_u2Z.
apply (state_mint_var_mint _ _ _ _ u (unsign rk ru)) in Hstate_mint; last by assoc_get_Some.
rewrite /var_mint /var_unsign in Hstate_mint; tauto.
case: Htmp => Htmp1 Htmp2.
move/(_ (conj Htmp1 (conj (refl_equal _) Htmp2))) => Heven_rx'.
eapply (proj2 Heven_rx'); clear Heven_rx'.
eapply mips_syntax.triple_exec_proj; first by apply (Heven_rx [ru]_st).
tauto.
by apply Hst1.
apply (state_mint_var_mint _ _ _ _ u (unsign rk ru)) in Hstate_mint; last by assoc_get_Some.
rewrite Sum_Z2ints_pos.
+ by apply not_Zmod_2_Zodd.
+ rewrite /var_mint /var_unsign in Hstate_mint.
rewrite -Zbeta_power; tauto.
have Ha0' : [ a0 ]_ st2 = zero32.
rewrite -Ha0.
symmetry.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _ ]/=; by Nodup_not_In.
move/mips_cmd.semop_prop_m.exec_cmd0_inv : Hst'.
case/exec0_and_inv => Hst'.
rewrite Ha0' int_and_comm int_and_0 in Hst'.
rewrite Hst'.
by reg_upd.
by rewrite Ha0 store.get_r0 eqxx.
* move/eqP => Heval_b.
have Ha0 : [a0]_st' = zero32.
have Ha1 : [a1]_st2 = zero32.
clear Heven_rx.
move/mips_seplog.hoare_prop_m.soundness : (Heven_ry [rv]_st).
rewrite /while.hoare_semantics.
move/(_ st1 (heap_cut he (Zabs_nat (u2Z ([rv ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))).
have Htmp : u2Z ([rk ]_ st1) = Z_of_nat (Zabs_nat (u2Z ([rk ]_ st))) /\
(var_e rv |--> Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([v ]_ s)%seplog_expr)%mips_assert st1
(heap_cut he (Zabs_nat (u2Z ([rv ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st)))).
split.
- rewrite Z_of_nat_Zabs_nat; last by apply min_u2Z.
f_equal.
symmetry.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
apply (state_mint_var_mint _ _ _ _ v (unsign rk rv)) in Hstate_mint; last by assoc_get_Some.
rewrite /var_mint /heap_mint in Hstate_mint.
case: Hstate_mint => _ [_ Htmp].
move: Htmp; apply assert_m.mapstos_ext => /=; exact Hry.
case: Htmp => Htmp1 Htmp2.
symmetry in Hry.
move/(_ (conj Htmp1 (conj Hry Htmp2))) => Heven_ry'.
eapply (proj2 Heven_ry'); clear Heven_ry'.
eapply mips_syntax.triple_exec_proj; first by apply (Heven_ry [rv]_st).
tauto.
by apply Hst2.
apply (state_mint_var_mint _ _ _ _ v (unsign rk rv)) in Hstate_mint; last by assoc_get_Some.
rewrite Sum_Z2ints_pos.
- by apply not_Zmod_2_Zodd.
- rewrite /var_mint /var_unsign in Hstate_mint.
rewrite -Zbeta_power; tauto.
move/mips_cmd.semop_prop_m.exec_cmd0_inv : Hst'.
case/exec0_and_inv => Hst'.
rewrite Ha1 int_and_0 in Hst'.
rewrite Hst'.
by reg_upd.
by rewrite Ha0 store.get_r0 eqxx.
Qed.
Require Import ssreflect ssrbool eqtype.
Require Import ZArith_ext Lists_ext.
Require Import machine_int nodup multi_int.
Import MachineInt.
Require Import mips_bipl mips_seplog mips_tactics.
Import expr_m.
Require Import integral_type.
Require Import simu.
Import simu_m.
Require Import begcd_mips_prelude_prg multi_is_even_and_prg multi_is_even_triple.
Local Open Scope zarith_ext_scope.
Local Open Scope machine_int_scope.
Local Open Scope nodup_scope.
Local Open Scope assoc_scope.
Local Open Scope heap_scope.
Local Open Scope mips_expr_scope.
Local Open Scope mips_cmd_scope.
Lemma fwd_sim_b_multi_is_even_and : forall rk ru rv a0 a1 u v d,
nodup(u, v) -> nodup(rk, ru, rv, a0, a1, r0) ->
fwd_sim_b (fun s st h =>
state_mint ((u |=> unsign rk ru \U+ (v |=> unsign rk rv \U+ d ))) s st h)
(var_e u mode nat_e 2 =e nat_e 0 &e var_e v mode nat_e 2 =e nat_e 0)%seplog_expr
(multi_is_even_and rk ru rv a0 a1) (bne a0 r0).
Proof.
move=> rk ru rv a0 a1 u v d u_v Hregs.
- rewrite /fwd_sim_b => s st he Hstate_mint.
have Hset_rx : nodup(rk, ru, a0, r0) by Nodup_nodup r0.
move: (len_Z2ints (Zabs_nat (u2Z [rk]_ st)) 32 ([u ]_ s)%seplog_expr).
move/(multi_is_even_triple _ _ _ Hset_rx _ _) => {Hset_rx} Heven_rx.
have Hset_ry : nodup(rk, rv, a1, r0) by Nodup_nodup r0.
move: (len_Z2ints (Zabs_nat (u2Z [rk ]_ st)) 32 ([v ]_ s)%seplog_expr).
move/(multi_is_even_triple _ _ _ Hset_ry _ _) => {Hset_ry} Heven_ry.
have [st' Hst'] : exists st', Some (st, he) -- multi_is_even_and rk ru rv a0 a1 ---> Some (st', he).
have [[st' he'] Hst'] : exists st', Some (st, he) -- multi_is_even_and rk ru rv a0 a1 ---> Some st'.
apply constructive_indefinite_description'.
apply mips_seplog.hoare_prop_m.termi with (P :=
((fun st0 h => u2Z [rk ]_ st0 = u2Z [rk ]_ st /\ [ru ]_ st0 = [ru ]_ st /\
(var_e ru |--> Z2ints 32 (Zabs_nat (u2Z [rk ]_ st)) ([u ]_ s)%seplog_expr)%mips_assert
st0 h) **
((fun st0 h => u2Z [rk ]_ st0 = u2Z [rk ]_ st /\ [rv ]_ st0 = [rv ]_ st /\
(var_e rv |--> Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([v ]_ s)%seplog_expr)%mips_assert
st0 h) ** assert_m.TT))%mips_assert) (Q := assert_m.TT).
+ eapply while.hoare_seq.
* apply mips_frame.frame_rule.
- rewrite Z_of_nat_Zabs_nat in Heven_rx; last by apply min_u2Z.
by apply Heven_rx.
- by Inde_frame.
- move=> ?; by Inde_mult.
* eapply while.hoare_seq.
- apply mips_contrib.hoare_con_comm_pre.
apply mips_contrib.hoare_con_assoc_pre.
apply mips_frame.frame_rule.
+ rewrite Z_of_nat_Zabs_nat in Heven_ry; last by apply min_u2Z.
by apply Heven_ry.
+ Inde_frame.
* apply assert_m.inde_imp.
apply assert_m.inde_get.
by Nodup_not_In.
* apply assert_m.inde_imp.
apply assert_m.inde_get.
by Nodup_not_In.
+ move=> ?; by Inde_mult.
- by apply mips_contrib.cmd_and_true.
+ move=> st0 h0 H0.
by apply constructive_indefinite_description, mips_syntax.no_while_terminate.
+ exists (heap_mint (unsign rk ru) st he).
exists (heap_mint (unsign rk rv) st he +++ (he [\m] seq.cat
(seq_ext.ran (Zabs_nat (u2Z ([ru ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))
(seq_ext.ran (Zabs_nat (u2Z ([rv ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st)))))).
split.
* apply heap.disj_union_R.
- apply (proj2 Hstate_mint u v).
by Nodup_neq.
by assoc_get_Some.
by assoc_get_Some.
- apply heap.proj_difs_disj.
by rewrite -seq_ext.l2s_seq seq_ext.inc_app_L.
* split.
- by rewrite heap.union_assoc -heap.proj_app 2!seq_ext.l2s_seq -heap.proj_difs.
- split.
+ split.
* done.
* apply (state_mint_var_mint _ _ _ _ u (unsign rk ru)) in Hstate_mint; last by assoc_get_Some.
rewrite /var_mint /var_unsign in Hstate_mint; tauto.
+ apply assert_m.con_cons; last by done.
* apply heap.proj_difs_disj.
by rewrite seq_ext.l2s_seq seq_ext.inc_app_R.
* split; first by reflexivity.
apply (state_mint_var_mint _ _ _ _ v (unsign rk rv)) in Hstate_mint; last by assoc_get_Some.
rewrite /var_mint /var_unsign in Hstate_mint; tauto.
exists st'.
suff : he = he' by move=> X; rewrite -X in Hst'.
by apply (mips_syntax.no_sw_heap_invariant _ _ _ Hst' (refl_equal _) _ _ _ _ (refl_equal _) (refl_equal _)).
exists st'; split; first by done.
case/mips_cmd.semop_prop_m.exec_seq_inv : Hst' => st1 [] Hst1.
case/mips_cmd.semop_prop_m.exec_seq_inv=> st2 [] Hst2 Hst'.
destruct st1 as [[st1 he1]|]; last first.
destruct st2 as [[st2 he2]|]; last first.
by move/semop_prop_m.from_none : Hst'.
by move/semop_prop_m.from_none : Hst2.
have ? : he = he1 by eapply (mips_syntax.no_sw_heap_invariant _ _ _ Hst1).
subst he1.
destruct st2 as [[st2 he2]|]; last by move/semop_prop_m.from_none : Hst'.
have Htmp : he = he2 by eapply (mips_syntax.no_sw_heap_invariant _ _ _ Hst2).
subst he2.
have Hry : [rv ]_ st = [rv ]_ st1.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _ ]/=; by Nodup_not_In.
have Hrk : [rk ]_ st = [rk ]_ st1.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _ ]/=; by Nodup_not_In.
split.
+ rewrite /= /ZIT.t_eqb /ZIT.t_mod.
case/andP. move/eqP => Heval_b1. move/eqP => Heval_b2.
have Ha0 : [ a0 ]_ st1 = one32.
clear Heven_ry.
move/mips_seplog.hoare_prop_m.soundness : (Heven_rx [ru]_st).
rewrite /while.hoare_semantics.
move/(_ st (heap_cut he (Zabs_nat (u2Z ([ru ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))).
rewrite Z_of_nat_Zabs_nat; last by apply min_u2Z.
have Htmp : (var_e ru |-->
Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([u ]_ s)%seplog_expr)%mips_assert
st
(heap_cut he (Zabs_nat (u2Z ([ru ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st)))).
apply (state_mint_var_mint _ _ _ _ u (unsign rk ru)) in Hstate_mint; last by assoc_get_Some.
rewrite /var_mint /var_unsign in Hstate_mint; tauto.
move/(_ (conj (refl_equal _) (conj (refl_equal _) Htmp))) => Heven_rx'.
eapply (proj2 Heven_rx'); clear Heven_rx'.
eapply mips_syntax.triple_exec_proj; first by apply (Heven_rx [ru]_st).
split.
rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
split; first by reflexivity.
exact Htmp.
by apply Hst1.
apply (state_mint_var_mint _ _ _ _ u (unsign rk ru)) in Hstate_mint; last by assoc_get_Some.
rewrite Sum_Z2ints_pos.
+ by apply Zmod_2_Zeven.
+ rewrite /var_mint /var_unsign in Hstate_mint.
rewrite -Zbeta_power; tauto.
have Ha1 : [a1]_st2 = one32.
clear Heven_rx.
move/mips_seplog.hoare_prop_m.soundness : (Heven_ry [rv]_st).
rewrite /while.hoare_semantics.
move/(_ st1 (heap_cut he (Zabs_nat (u2Z [rv ]_ st / 4)) (Zabs_nat (u2Z ([rk ]_ st))))).
have Htmp : u2Z ([rk ]_ st1) = Z_of_nat (Zabs_nat (u2Z ([rk ]_ st))) /\
(var_e rv |--> Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([v ]_ s)%seplog_expr)%mips_assert
st1
(heap_cut he (Zabs_nat (u2Z ([rv ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st)))).
split.
rewrite Z_of_nat_Zabs_nat; last by apply min_u2Z.
f_equal.
symmetry.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
apply (state_mint_var_mint _ _ _ _ v (unsign rk rv)) in Hstate_mint; last by assoc_get_Some.
rewrite /var_mint /heap_mint in Hstate_mint.
case: Hstate_mint => _ [_ Htmp].
move: Htmp; apply assert_m.mapstos_ext => /=.
congruence.
case: Htmp => Htmp1 Htmp2.
symmetry in Hry.
move/(_ (conj Htmp1 (conj Hry Htmp2))) => Heven_ry'.
eapply (proj2 Heven_ry'); clear Heven_ry'.
eapply mips_syntax.triple_exec_proj; first by apply (Heven_ry [rv]_st).
by tauto.
by apply Hst2.
apply (state_mint_var_mint _ _ _ _ v (unsign rk rv)) in Hstate_mint; last by assoc_get_Some.
rewrite Sum_Z2ints_pos.
+ by apply Zmod_2_Zeven.
+ rewrite /var_mint /var_unsign in Hstate_mint.
rewrite -Zbeta_power; tauto.
have {Ha0}Ha0 : [a0 ]_ st2 = one32.
rewrite -Ha0.
symmetry. mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _ ]/=; by Nodup_not_In.
move/mips_cmd.semop_prop_m.exec_cmd0_inv : Hst'.
case/mips_cmd.exec0_and_inv => Hst'.
rewrite Ha1 Ha0 int_and_idempotent in Hst'.
rewrite {1}Hst'.
reg_upd.
by rewrite store.get_r0 !u2Z_Z2u.
+ rewrite /= /ZIT.t_eqb /ZIT.t_mod.
case/nandP.
* move/eqP => Heval_b.
have Ha0 : [a0]_st' = zero32.
have Ha0 : [a0]_st1 = zero32.
clear Heven_ry.
move/mips_seplog.hoare_prop_m.soundness : (Heven_rx [ru]_st).
rewrite /while.hoare_semantics.
move/(_ st (heap_cut he (Zabs_nat (u2Z ([ru ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))).
have Htmp : u2Z [rk ]_ st = Z_of_nat (Zabs_nat (u2Z ([rk ]_ st))) /\
(var_e ru |--> Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([u ]_ s)%seplog_expr)%mips_assert st
(heap_cut he (Zabs_nat (u2Z ([ru ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st)))).
split.
by rewrite Z_of_nat_Zabs_nat; last by apply min_u2Z.
apply (state_mint_var_mint _ _ _ _ u (unsign rk ru)) in Hstate_mint; last by assoc_get_Some.
rewrite /var_mint /var_unsign in Hstate_mint; tauto.
case: Htmp => Htmp1 Htmp2.
move/(_ (conj Htmp1 (conj (refl_equal _) Htmp2))) => Heven_rx'.
eapply (proj2 Heven_rx'); clear Heven_rx'.
eapply mips_syntax.triple_exec_proj; first by apply (Heven_rx [ru]_st).
tauto.
by apply Hst1.
apply (state_mint_var_mint _ _ _ _ u (unsign rk ru)) in Hstate_mint; last by assoc_get_Some.
rewrite Sum_Z2ints_pos.
+ by apply not_Zmod_2_Zodd.
+ rewrite /var_mint /var_unsign in Hstate_mint.
rewrite -Zbeta_power; tauto.
have Ha0' : [ a0 ]_ st2 = zero32.
rewrite -Ha0.
symmetry.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _ ]/=; by Nodup_not_In.
move/mips_cmd.semop_prop_m.exec_cmd0_inv : Hst'.
case/exec0_and_inv => Hst'.
rewrite Ha0' int_and_comm int_and_0 in Hst'.
rewrite Hst'.
by reg_upd.
by rewrite Ha0 store.get_r0 eqxx.
* move/eqP => Heval_b.
have Ha0 : [a0]_st' = zero32.
have Ha1 : [a1]_st2 = zero32.
clear Heven_rx.
move/mips_seplog.hoare_prop_m.soundness : (Heven_ry [rv]_st).
rewrite /while.hoare_semantics.
move/(_ st1 (heap_cut he (Zabs_nat (u2Z ([rv ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))).
have Htmp : u2Z ([rk ]_ st1) = Z_of_nat (Zabs_nat (u2Z ([rk ]_ st))) /\
(var_e rv |--> Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([v ]_ s)%seplog_expr)%mips_assert st1
(heap_cut he (Zabs_nat (u2Z ([rv ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st)))).
split.
- rewrite Z_of_nat_Zabs_nat; last by apply min_u2Z.
f_equal.
symmetry.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
apply (state_mint_var_mint _ _ _ _ v (unsign rk rv)) in Hstate_mint; last by assoc_get_Some.
rewrite /var_mint /heap_mint in Hstate_mint.
case: Hstate_mint => _ [_ Htmp].
move: Htmp; apply assert_m.mapstos_ext => /=; exact Hry.
case: Htmp => Htmp1 Htmp2.
symmetry in Hry.
move/(_ (conj Htmp1 (conj Hry Htmp2))) => Heven_ry'.
eapply (proj2 Heven_ry'); clear Heven_ry'.
eapply mips_syntax.triple_exec_proj; first by apply (Heven_ry [rv]_st).
tauto.
by apply Hst2.
apply (state_mint_var_mint _ _ _ _ v (unsign rk rv)) in Hstate_mint; last by assoc_get_Some.
rewrite Sum_Z2ints_pos.
- by apply not_Zmod_2_Zodd.
- rewrite /var_mint /var_unsign in Hstate_mint.
rewrite -Zbeta_power; tauto.
move/mips_cmd.semop_prop_m.exec_cmd0_inv : Hst'.
case/exec0_and_inv => Hst'.
rewrite Ha1 int_and_0 in Hst'.
rewrite Hst'.
by reg_upd.
by rewrite Ha0 store.get_r0 eqxx.
Qed.