Library multi_mul2_simu
Require Epsilon.
Require Import ssreflect ssrbool eqtype seq.
Require Import ZArith_ext Lists_ext.
Require Import machine_int multi_int encode_decode integral_type.
Import MachineInt.
Require Import mips_bipl mips_seplog mips_tactics mips_syntax.
Import mips_bipl.expr_m.
Require Import simu.
Import simu.simu_m.
Require Import multi_mul2_prg multi_mul2_triple.
Local Open Scope zarith_ext_scope.
Local Open Scope machine_int_scope.
Local Open Scope heap_scope.
Local Open Scope assoc_scope.
Local Open Scope nodup_scope.
Lemma psim_mul2 : forall (x : bipl.var.v) (d : assoc.t) (rk rx a0 a1 a2 a3 : reg),
nodup(rk, rx, a0, a1, a2, a3, r0) ->
disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: a2 :: a3 :: nil) ->
x \notin assoc.dom d -> unsign rk rx \notin assoc.cdom d ->
psim (x |=> unsign rk rx \U+ d)
(fun s st h => ([ x ]_ s)%seplog_expr < 2 ^^ ((Zabs_nat (u2Z ([ rk ]_st)%mips_expr)) * 32 - 1))
(x <- var_e x *e nat_e 2)%seplog_expr%seplog_cmd
(multi_mul2 rk rx a0 a1 a2 a3).
Proof.
move=> x d rk rx a0 a1 a2 a3 Haux Hd Hd' Hd''.
rewrite /psim.
move=> s st h s_st_h HP0 s' exec_pseudo st' h' exec_mips.
have d_unchanged : forall v r, assoc.get v d = Some r ->
disj (mint_regs r) (mips_frame.modified_regs (multi_mul2 rk rx a0 a1 a2 a3)).
move=> v r Hvr; rewrite [mips_frame.modified_regs _]/=; Disj_remove_dup.
apply (disj_incl_LR _ _ _ _ Hd); last by apply incl_refl_Permutation; PermutProve.
apply incl_mint_regs.
apply/seq_ext.inP.
by apply (assoc.get_Some_in_cdom _ v).
set nk := Zabs_nat (u2Z ([rk ]_ st)%mips_expr).
have [st'' [h'' exec_mips_proj]] : exists st'', exists h'',
(Some (st, heap.proj h (heap.dom (heap_mint (unsign rk rx) st h)))
-- multi_mul2 rk rx a0 a1 a2 a3 ---> Some (st'', h''))%mips_cmd.
exists st'.
exists (heap.proj h' (heap.dom (heap_mint (unsign rk rx) st h))).
have Hoare_multi_mul2 : ( {{ (fun s0 h0 => [rx ]_ s0 = [rx ]_ st /\
u2Z ([rk ]_ s0) = Z_of_nat nk /\
(var_e rx |--> Z2ints 32 nk ([ x ]_s)%seplog_expr)%mips_assert s0 h0)%mips_expr }}
multi_mul2 rk rx a0 a1 a2 a3
{{ (fun s0 h0 => exists A', length A' = nk /\ [rx ]_ s0 = [rx ]_ st /\
u2Z ([rk ]_ s0) = Z_of_nat nk /\ (var_e rx |--> A')%mips_assert s0 h0 /\
Sum nk A' + u2Z ([a2 ]_ s0) * 2 ^^ (nk * 32) = 2 * Sum nk
(Z2ints 32 nk ([ x ]_ s)%seplog_expr))%mips_expr }} )%mips_hoare.
apply multi_mul2_triple => //.
by eapply state_mint_unsign_fit; eauto.
by rewrite len_Z2ints.
move/mips_syntax.triple_exec_proj : Hoare_multi_mul2; apply => //.
split; first by done.
split; first by rewrite Z_of_nat_Zabs_nat //; apply min_u2Z.
rewrite /heap_cut heap.proj_dom_proj.
apply (state_mint_var_mint _ _ _ _ x (unsign rk rx)) in s_st_h; last by assoc_get_Some.
rewrite /var_mint in s_st_h.
by case: s_st_h => _ [_ ?].
split.
- move=> y ry y_ry.
have [yx | yx] : y \in assoc.dom d \/ y = x.
case/assoc.get_union_Some_inv : y_ry => y_ry.
* by case/assoc.get_sing_inv : y_ry => -> _; right.
* by apply assoc.get_Some_in_dom in y_ry; left.
+ have x_y : y <> x.
move=> ?; subst y; by rewrite yx in Hd'.
move: {s_st_h}(proj1 s_st_h _ _ y_ry) (proj2 s_st_h) => s_st_h1 s_st_h2.
have y_unchanged : ([ y ]_s = [ y ]_s')%seplog_expr.
Var_unchanged. rewrite /=; contradict x_y; by case: x_y.
case: (mips_syntax.exec_deter_proj _ _ _ _ _ exec_mips
(heap.dom (heap_mint (unsign rk rx) st h)) _ _ exec_mips_proj) => H4 [H5 H_h_h'].
have <- : heap_mint ry st h = heap_mint ry st' h'.
apply heap_mint_unchanged2 with (d := heap_mint (unsign rk rx) st h) (x := y) (s := s) => //.
move=> rx0 Hrx0; Reg_unchanged.
apply (disj_not_In _ (mint_regs ry)); last by rewrite /=; intuition.
apply disj_sym, (d_unchanged y).
by rewrite -y_ry assoc.get_union_sing_neq.
apply s_st_h2 with y x => //.
by rewrite assoc.get_union_sing_eq.
move: s_st_h1; apply var_mint_invariant.
move=> rx0 Hrx0; Reg_unchanged.
apply (disj_not_In _ (mint_regs ry)); last by rewrite /=; intuition.
apply disj_sym, (d_unchanged y) => //.
by rewrite -y_ry assoc.get_union_sing_neq.
Var_unchanged; rewrite /=; by intuition.
+ subst y.
have ? : ry = unsign rk rx.
rewrite assoc.get_union_sing_eq in y_ry.
by case: y_ry.
subst ry.
move: {s_st_h}(proj1 s_st_h x (unsign rk rx) y_ry).
rewrite /var_mint.
set vx := u2Z (store.get rx st).
set nk' := Zabs_nat (u2Z (store.get rk st')).
set vx' := u2Z (store.get rx st').
case=> [s_st_h_fit [[s_st_h_over1 s_st_h_over2] s_st_h_heap]].
have Hset : nodup(rk, rx, a0, a1, a2, a3, r0) by Nodup_nodup r0.
move: (multi_mul2_triple _ _ _ _ _ _ Hset _ (store.get rx st) s_st_h_fit
(Z2ints 32 nk ([var_e x ]e_s)%seplog_expr)) => Hmul2.
rewrite len_Z2ints in Hmul2.
move: {Hmul2}(mips_frame.frame_rule _ _ _ (Hmul2 (refl_equal _)) assert_m.TT (assert_m.inde_TT _) (mips_frame.inde_cmd_mult_TT _)).
move/mips_seplog.hoare_prop_m.soundness.
rewrite /while.hoare_semantics.
move/(_ st h) => Hmul2.
lapply Hmul2; last first.
exists (heap_mint (unsign rk rx) st h), (h [\m] heap.dom (heap_mint (unsign rk rx) st h)).
split; first by apply heap.disj_difs', seq_ext.inc_refl.
split.
apply heap.union_difs => //.
rewrite /heap_cut; by apply heap.inclu_proj.
split; last by done.
split; first by done.
split; last by done.
rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
move=> {Hmul2} [Hmul2 Hmul2'].
move: {Hmul2'}(Hmul2' _ _ exec_mips).
case=> h1 [h2 [Hdisj [Hunion [[A' [Hmul2_1 [Hmul2_2 [Hmul2_3 [Hmul2_4 Hmul2_5]]]]] HTT]]]].
have nk_nk' : nk = nk' by rewrite /nk /nk' Hmul2_3 Z_of_nat_Zabs_nat //; apply min_u2Z.
subst nk'.
rewrite -nk_nk'.
have vx_vx' : vx' = vx by rewrite /vx /vx' Hmul2_2.
subst vx'.
rewrite /var_unsign vx_vx'.
+ split; first by exact s_st_h_fit.
split.
split.
- move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ -> /=.
syntax_m.seplog_m.assert_m.expr_m.Store_upd.
rewrite /ZIT.t_mult.
by apply Zmult_le_0_compat.
- move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ -> /=.
syntax_m.seplog_m.assert_m.expr_m.Store_upd.
rewrite /ZIT.t_mult Zmult_comm.
have [Hnk' | Hnk'] : nk = O \/ (O < nk)%nat by omega.
- rewrite -/nk Hnk' /Zbeta /= in s_st_h_over2.
rewrite Hnk' /Zbeta [_ ^^ _]/=; omega.
- rewrite /Zbeta (_ : nk * 32 = S (nk * 32 - 1))%nat; last by omega.
rewrite Zpower_S; by apply Zmult_lt_compat_l.
apply mapstos_inv_list2heap in Hmul2_4 => //; last first.
by rewrite [eval _ _]/= Hmul2_2 Hmul2_1.
rewrite u2Z_shrl' in Hmul2_4; last by repeat constructor.
rewrite /= Hmul2_2 in Hmul2_4.
rewrite /heap_cut Hunion Hmul2_4.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ -> /=.
syntax_m.seplog_m.assert_m.expr_m.Store_upd.
rewrite Sum_Z2ints_pos // [ ( [ _ ]e_ _ )%seplog_expr ]/= in Hmul2_5.
rewrite /ZIT.t_mult Zmult_comm.
case: (zerop nk) => Hnk'.
- rewrite -nk_nk' Hnk' Z2ints_0 /= /heap_cut heap.proj_nil.
split; last by done.
move/assert_m.mapstos_inv_addr : s_st_h_heap => /=.
by rewrite Hmul2_2.
- have Htmp : u2Z ([a2 ]_st')%mips_expr = 0.
have Htmp1 : 2 * ([ x ]_ s)%seplog_expr < 2 ^^ (nk * 32).
rewrite (_ : nk * 32 = S (nk * 32 - 1))%nat; last by omega.
rewrite Zpower_S; by apply Zmult_lt_compat_l.
rewrite -Hmul2_5 in Htmp1.
move: (min_u2Z ([a2]_st')%mips_expr).
case/Zle_lt_or_eq => Htmp2 //.
rewrite Zplus_comm mult_comm in Htmp1. move/(poly_Zlt1_inv _ _ _ (min_Sum _ _) (min_u2Z _) (Zpower_0' _)) : Htmp1 => Htmp1.
rewrite Htmp1 in Htmp2; by move/Zlt_irrefl : Htmp2.
rewrite -Hmul2_5 Htmp Zmult_0_l Zplus_0_r -Z2ints_Sum // /heap_cut vx_vx' -nk_nk'.
have <- : heap.dom (list2heap (Zabs_nat (vx / 4)) A') =
seq_ext.l2s (List.seq (Zabs_nat (vx / 4)) nk).
by rewrite dom_list2heap Hmul2_1.
rewrite heap.proj_union_L; last by rewrite -Hmul2_4.
rewrite heap.proj_itself.
apply mapstos_list2heap.
+ rewrite Z_of_nat_Zabs_nat //; last first.
apply Z_div_pos => //; by apply min_u2Z.
rewrite -Zdivide_Zdiv_eq //.
move/assert_m.mapstos_inv_addr : s_st_h_heap; by apply Zmod_divide.
+ rewrite /vx in s_st_h_fit.
rewrite [eval _ _]/= Hmul2_2; omega.
- apply (state_mint_part2_one_variable _ _ _ _ _ _ _ _ _ s_st_h).
+ move=> t x0 Ht Hx0.
Reg_unchanged. simpl mips_frame.modified_regs.
case/assoc.in_cdom_union_inv : Ht => Ht.
* rewrite assoc.cdom_sing /= seq.mem_seq1 in Ht.
move/eqP : Ht => Ht; subst t.
apply (disj_not_In _ (mint_regs (unsign rk rx))); last by rewrite /=; auto.
Disj_remove_dup.
simpl.
apply nodup_disj.
simpl app.
by Nodup_nodup r0.
* apply (disj_not_In _ (mint_regs t)); last by rewrite /=; auto.
Disj_remove_dup.
apply disj_sym.
apply (disj_incl_LR _ _ _ _ Hd); last by apply incl_refl_Permutation; PermutProve.
apply incl_mint_regs.
by apply/seq_ext.inP.
+ move: (mips_syntax.exec_deter_proj _ _ _ _ _ exec_mips _ _ _ exec_mips_proj); tauto.
+ by apply (mips_syntax.dom_heap_invariant _ _ _ _ _ exec_mips).
Qed.
Lemma safe_termination_mul2 : forall a0 a1 a2 a3 rx x rk d,
nodup(rk, rx, a0, a1, a2, a3, r0) ->
safe_termination (state_mint (x |=> unsign rk rx \U+ d))
(multi_mul2 rk rx a0 a1 a2 a3).
Proof.
move=> a0 a1 a2 a3 rx x rk d Hset.
rewrite /safe_termination.
move=> s st h H_s_st_h.
have [sf exec_mips] : {sf | Some (st, h) -- multi_mul2 rk rx a0 a1 a2 a3 ---> sf}%mips_cmd.
have [sf [exec_mips _]] : {sf | Some (st, h) -- multi_mul2 rk rx a0 a1 a2 a3 ---> sf /\
(forall s, sf = Some s -> True) }%mips_cmd.
rewrite /multi_mul2.
apply exists_addiu_seq_P.
rewrite sext_Z2u // add_0.
apply exists_addiu_seq_P.
rewrite sext_Z2u // add_0.
repeat reg_upd.
move Hs0 : (store.upd _ _ _) => s0.
have [na0 Ha0] : { na0 | u2Z ([ rk ]_s0) - u2Z ([ a0 ]_s0) = Z_of_nat na0 }%mips_expr.
apply Z_of_nat_complete_inf.
rewrite -Hs0.
repeat reg_upd.
rewrite u2Z_Z2u // Zminus_0_r.
by apply min_u2Z.
clear Hs0 H_s_st_h.
move: na0 s0 s st h Hset Ha0.
elim.
- move=> s0 s st h Hset Ha0.
exists (Some (s0, h)); split; last by done.
apply while.exec_while_false.
+ rewrite /= in Ha0 *.
apply/negPn. apply/Zeq_boolP; omega.
+ move=> na0 IH s0 s st h Hset Ha0.
apply exists_while_P.
* rewrite /=; rewrite Z_S in Ha0.
apply/Zeq_boolP; omega.
* apply exists_seq_P with (fun s => forall s', s = Some s' ->
u2Z ([ rk ]_(fst s')) - u2Z ([ a0 ]_(fst s')) = Z_of_nat na0)%mips_expr.
- exists_lwxs l_a0 H_l_a0 z_a0 H_z_a0.
apply exists_srl_seq_P.
repeat reg_upd.
apply exists_sll_seq_P.
repeat reg_upd.
apply exists_or_seq_P.
repeat reg_upd.
rewrite store.upd_upd_eq.
apply exists_addiu_seq_P.
repeat reg_upd.
apply exists_sll_seq_P.
repeat reg_upd.
apply exists_addu_seq_P.
repeat reg_upd.
rewrite store.upd_upd_eq.
exists_sw_P l_idx H_l_idx z_idx H_z_idx.
repeat reg_upd.
apply exists_addiu_P.
rewrite /=.
repeat reg_upd.
rewrite Z_S in Ha0.
rewrite sext_Z2u // u2Z_add_Z2u //.
omega.
move: (min_u2Z ([a0]_s0)%mips_expr) (min_u2Z ([rk]_s0)%mips_expr) (max_u2Z ([rk]_s0)%mips_expr) => ? ? ?.
omega.
- move=> si Hsi.
destruct si as [[sti hi] |].
+ apply IH => //.
by move: {Hsi}(Hsi _ (refl_equal _)).
+ exists None; split; [by apply while.exec_none | done].
by exists sf.
apply constructive_indefinite_description'.
have H1 : (u2Z ([ rx ]_ st) + 4 * Z_of_nat (Zabs_nat (u2Z ([rk ]_ st))) < Zbeta 1)%mips_expr.
eapply state_mint_unsign_fit; by apply H_s_st_h.
have H3 : (length (Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([ x ]_ s)%seplog_expr) =
Zabs_nat (u2Z ([rk ]_ st)))%mips_expr.
by rewrite len_Z2ints.
move: (multi_mul2_triple _ _ _ _ _ _ Hset _ _ H1 _ H3) => Htriple.
move: (mips_syntax.triple_exec_precond _ _ _ Htriple _ _ _ exec_mips
(seq_ext.l2s (List.seq (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))%mips_expr)).
apply.
split; first by done.
split.
- rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
- apply (state_mint_var_mint _ _ _ _ x (unsign rk rx)) in H_s_st_h; last by assoc_get_Some.
rewrite /var_mint /var_unsign in H_s_st_h; tauto.
Qed.
Require Import ssreflect ssrbool eqtype seq.
Require Import ZArith_ext Lists_ext.
Require Import machine_int multi_int encode_decode integral_type.
Import MachineInt.
Require Import mips_bipl mips_seplog mips_tactics mips_syntax.
Import mips_bipl.expr_m.
Require Import simu.
Import simu.simu_m.
Require Import multi_mul2_prg multi_mul2_triple.
Local Open Scope zarith_ext_scope.
Local Open Scope machine_int_scope.
Local Open Scope heap_scope.
Local Open Scope assoc_scope.
Local Open Scope nodup_scope.
Lemma psim_mul2 : forall (x : bipl.var.v) (d : assoc.t) (rk rx a0 a1 a2 a3 : reg),
nodup(rk, rx, a0, a1, a2, a3, r0) ->
disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: a2 :: a3 :: nil) ->
x \notin assoc.dom d -> unsign rk rx \notin assoc.cdom d ->
psim (x |=> unsign rk rx \U+ d)
(fun s st h => ([ x ]_ s)%seplog_expr < 2 ^^ ((Zabs_nat (u2Z ([ rk ]_st)%mips_expr)) * 32 - 1))
(x <- var_e x *e nat_e 2)%seplog_expr%seplog_cmd
(multi_mul2 rk rx a0 a1 a2 a3).
Proof.
move=> x d rk rx a0 a1 a2 a3 Haux Hd Hd' Hd''.
rewrite /psim.
move=> s st h s_st_h HP0 s' exec_pseudo st' h' exec_mips.
have d_unchanged : forall v r, assoc.get v d = Some r ->
disj (mint_regs r) (mips_frame.modified_regs (multi_mul2 rk rx a0 a1 a2 a3)).
move=> v r Hvr; rewrite [mips_frame.modified_regs _]/=; Disj_remove_dup.
apply (disj_incl_LR _ _ _ _ Hd); last by apply incl_refl_Permutation; PermutProve.
apply incl_mint_regs.
apply/seq_ext.inP.
by apply (assoc.get_Some_in_cdom _ v).
set nk := Zabs_nat (u2Z ([rk ]_ st)%mips_expr).
have [st'' [h'' exec_mips_proj]] : exists st'', exists h'',
(Some (st, heap.proj h (heap.dom (heap_mint (unsign rk rx) st h)))
-- multi_mul2 rk rx a0 a1 a2 a3 ---> Some (st'', h''))%mips_cmd.
exists st'.
exists (heap.proj h' (heap.dom (heap_mint (unsign rk rx) st h))).
have Hoare_multi_mul2 : ( {{ (fun s0 h0 => [rx ]_ s0 = [rx ]_ st /\
u2Z ([rk ]_ s0) = Z_of_nat nk /\
(var_e rx |--> Z2ints 32 nk ([ x ]_s)%seplog_expr)%mips_assert s0 h0)%mips_expr }}
multi_mul2 rk rx a0 a1 a2 a3
{{ (fun s0 h0 => exists A', length A' = nk /\ [rx ]_ s0 = [rx ]_ st /\
u2Z ([rk ]_ s0) = Z_of_nat nk /\ (var_e rx |--> A')%mips_assert s0 h0 /\
Sum nk A' + u2Z ([a2 ]_ s0) * 2 ^^ (nk * 32) = 2 * Sum nk
(Z2ints 32 nk ([ x ]_ s)%seplog_expr))%mips_expr }} )%mips_hoare.
apply multi_mul2_triple => //.
by eapply state_mint_unsign_fit; eauto.
by rewrite len_Z2ints.
move/mips_syntax.triple_exec_proj : Hoare_multi_mul2; apply => //.
split; first by done.
split; first by rewrite Z_of_nat_Zabs_nat //; apply min_u2Z.
rewrite /heap_cut heap.proj_dom_proj.
apply (state_mint_var_mint _ _ _ _ x (unsign rk rx)) in s_st_h; last by assoc_get_Some.
rewrite /var_mint in s_st_h.
by case: s_st_h => _ [_ ?].
split.
- move=> y ry y_ry.
have [yx | yx] : y \in assoc.dom d \/ y = x.
case/assoc.get_union_Some_inv : y_ry => y_ry.
* by case/assoc.get_sing_inv : y_ry => -> _; right.
* by apply assoc.get_Some_in_dom in y_ry; left.
+ have x_y : y <> x.
move=> ?; subst y; by rewrite yx in Hd'.
move: {s_st_h}(proj1 s_st_h _ _ y_ry) (proj2 s_st_h) => s_st_h1 s_st_h2.
have y_unchanged : ([ y ]_s = [ y ]_s')%seplog_expr.
Var_unchanged. rewrite /=; contradict x_y; by case: x_y.
case: (mips_syntax.exec_deter_proj _ _ _ _ _ exec_mips
(heap.dom (heap_mint (unsign rk rx) st h)) _ _ exec_mips_proj) => H4 [H5 H_h_h'].
have <- : heap_mint ry st h = heap_mint ry st' h'.
apply heap_mint_unchanged2 with (d := heap_mint (unsign rk rx) st h) (x := y) (s := s) => //.
move=> rx0 Hrx0; Reg_unchanged.
apply (disj_not_In _ (mint_regs ry)); last by rewrite /=; intuition.
apply disj_sym, (d_unchanged y).
by rewrite -y_ry assoc.get_union_sing_neq.
apply s_st_h2 with y x => //.
by rewrite assoc.get_union_sing_eq.
move: s_st_h1; apply var_mint_invariant.
move=> rx0 Hrx0; Reg_unchanged.
apply (disj_not_In _ (mint_regs ry)); last by rewrite /=; intuition.
apply disj_sym, (d_unchanged y) => //.
by rewrite -y_ry assoc.get_union_sing_neq.
Var_unchanged; rewrite /=; by intuition.
+ subst y.
have ? : ry = unsign rk rx.
rewrite assoc.get_union_sing_eq in y_ry.
by case: y_ry.
subst ry.
move: {s_st_h}(proj1 s_st_h x (unsign rk rx) y_ry).
rewrite /var_mint.
set vx := u2Z (store.get rx st).
set nk' := Zabs_nat (u2Z (store.get rk st')).
set vx' := u2Z (store.get rx st').
case=> [s_st_h_fit [[s_st_h_over1 s_st_h_over2] s_st_h_heap]].
have Hset : nodup(rk, rx, a0, a1, a2, a3, r0) by Nodup_nodup r0.
move: (multi_mul2_triple _ _ _ _ _ _ Hset _ (store.get rx st) s_st_h_fit
(Z2ints 32 nk ([var_e x ]e_s)%seplog_expr)) => Hmul2.
rewrite len_Z2ints in Hmul2.
move: {Hmul2}(mips_frame.frame_rule _ _ _ (Hmul2 (refl_equal _)) assert_m.TT (assert_m.inde_TT _) (mips_frame.inde_cmd_mult_TT _)).
move/mips_seplog.hoare_prop_m.soundness.
rewrite /while.hoare_semantics.
move/(_ st h) => Hmul2.
lapply Hmul2; last first.
exists (heap_mint (unsign rk rx) st h), (h [\m] heap.dom (heap_mint (unsign rk rx) st h)).
split; first by apply heap.disj_difs', seq_ext.inc_refl.
split.
apply heap.union_difs => //.
rewrite /heap_cut; by apply heap.inclu_proj.
split; last by done.
split; first by done.
split; last by done.
rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
move=> {Hmul2} [Hmul2 Hmul2'].
move: {Hmul2'}(Hmul2' _ _ exec_mips).
case=> h1 [h2 [Hdisj [Hunion [[A' [Hmul2_1 [Hmul2_2 [Hmul2_3 [Hmul2_4 Hmul2_5]]]]] HTT]]]].
have nk_nk' : nk = nk' by rewrite /nk /nk' Hmul2_3 Z_of_nat_Zabs_nat //; apply min_u2Z.
subst nk'.
rewrite -nk_nk'.
have vx_vx' : vx' = vx by rewrite /vx /vx' Hmul2_2.
subst vx'.
rewrite /var_unsign vx_vx'.
+ split; first by exact s_st_h_fit.
split.
split.
- move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ -> /=.
syntax_m.seplog_m.assert_m.expr_m.Store_upd.
rewrite /ZIT.t_mult.
by apply Zmult_le_0_compat.
- move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ -> /=.
syntax_m.seplog_m.assert_m.expr_m.Store_upd.
rewrite /ZIT.t_mult Zmult_comm.
have [Hnk' | Hnk'] : nk = O \/ (O < nk)%nat by omega.
- rewrite -/nk Hnk' /Zbeta /= in s_st_h_over2.
rewrite Hnk' /Zbeta [_ ^^ _]/=; omega.
- rewrite /Zbeta (_ : nk * 32 = S (nk * 32 - 1))%nat; last by omega.
rewrite Zpower_S; by apply Zmult_lt_compat_l.
apply mapstos_inv_list2heap in Hmul2_4 => //; last first.
by rewrite [eval _ _]/= Hmul2_2 Hmul2_1.
rewrite u2Z_shrl' in Hmul2_4; last by repeat constructor.
rewrite /= Hmul2_2 in Hmul2_4.
rewrite /heap_cut Hunion Hmul2_4.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ -> /=.
syntax_m.seplog_m.assert_m.expr_m.Store_upd.
rewrite Sum_Z2ints_pos // [ ( [ _ ]e_ _ )%seplog_expr ]/= in Hmul2_5.
rewrite /ZIT.t_mult Zmult_comm.
case: (zerop nk) => Hnk'.
- rewrite -nk_nk' Hnk' Z2ints_0 /= /heap_cut heap.proj_nil.
split; last by done.
move/assert_m.mapstos_inv_addr : s_st_h_heap => /=.
by rewrite Hmul2_2.
- have Htmp : u2Z ([a2 ]_st')%mips_expr = 0.
have Htmp1 : 2 * ([ x ]_ s)%seplog_expr < 2 ^^ (nk * 32).
rewrite (_ : nk * 32 = S (nk * 32 - 1))%nat; last by omega.
rewrite Zpower_S; by apply Zmult_lt_compat_l.
rewrite -Hmul2_5 in Htmp1.
move: (min_u2Z ([a2]_st')%mips_expr).
case/Zle_lt_or_eq => Htmp2 //.
rewrite Zplus_comm mult_comm in Htmp1. move/(poly_Zlt1_inv _ _ _ (min_Sum _ _) (min_u2Z _) (Zpower_0' _)) : Htmp1 => Htmp1.
rewrite Htmp1 in Htmp2; by move/Zlt_irrefl : Htmp2.
rewrite -Hmul2_5 Htmp Zmult_0_l Zplus_0_r -Z2ints_Sum // /heap_cut vx_vx' -nk_nk'.
have <- : heap.dom (list2heap (Zabs_nat (vx / 4)) A') =
seq_ext.l2s (List.seq (Zabs_nat (vx / 4)) nk).
by rewrite dom_list2heap Hmul2_1.
rewrite heap.proj_union_L; last by rewrite -Hmul2_4.
rewrite heap.proj_itself.
apply mapstos_list2heap.
+ rewrite Z_of_nat_Zabs_nat //; last first.
apply Z_div_pos => //; by apply min_u2Z.
rewrite -Zdivide_Zdiv_eq //.
move/assert_m.mapstos_inv_addr : s_st_h_heap; by apply Zmod_divide.
+ rewrite /vx in s_st_h_fit.
rewrite [eval _ _]/= Hmul2_2; omega.
- apply (state_mint_part2_one_variable _ _ _ _ _ _ _ _ _ s_st_h).
+ move=> t x0 Ht Hx0.
Reg_unchanged. simpl mips_frame.modified_regs.
case/assoc.in_cdom_union_inv : Ht => Ht.
* rewrite assoc.cdom_sing /= seq.mem_seq1 in Ht.
move/eqP : Ht => Ht; subst t.
apply (disj_not_In _ (mint_regs (unsign rk rx))); last by rewrite /=; auto.
Disj_remove_dup.
simpl.
apply nodup_disj.
simpl app.
by Nodup_nodup r0.
* apply (disj_not_In _ (mint_regs t)); last by rewrite /=; auto.
Disj_remove_dup.
apply disj_sym.
apply (disj_incl_LR _ _ _ _ Hd); last by apply incl_refl_Permutation; PermutProve.
apply incl_mint_regs.
by apply/seq_ext.inP.
+ move: (mips_syntax.exec_deter_proj _ _ _ _ _ exec_mips _ _ _ exec_mips_proj); tauto.
+ by apply (mips_syntax.dom_heap_invariant _ _ _ _ _ exec_mips).
Qed.
Lemma safe_termination_mul2 : forall a0 a1 a2 a3 rx x rk d,
nodup(rk, rx, a0, a1, a2, a3, r0) ->
safe_termination (state_mint (x |=> unsign rk rx \U+ d))
(multi_mul2 rk rx a0 a1 a2 a3).
Proof.
move=> a0 a1 a2 a3 rx x rk d Hset.
rewrite /safe_termination.
move=> s st h H_s_st_h.
have [sf exec_mips] : {sf | Some (st, h) -- multi_mul2 rk rx a0 a1 a2 a3 ---> sf}%mips_cmd.
have [sf [exec_mips _]] : {sf | Some (st, h) -- multi_mul2 rk rx a0 a1 a2 a3 ---> sf /\
(forall s, sf = Some s -> True) }%mips_cmd.
rewrite /multi_mul2.
apply exists_addiu_seq_P.
rewrite sext_Z2u // add_0.
apply exists_addiu_seq_P.
rewrite sext_Z2u // add_0.
repeat reg_upd.
move Hs0 : (store.upd _ _ _) => s0.
have [na0 Ha0] : { na0 | u2Z ([ rk ]_s0) - u2Z ([ a0 ]_s0) = Z_of_nat na0 }%mips_expr.
apply Z_of_nat_complete_inf.
rewrite -Hs0.
repeat reg_upd.
rewrite u2Z_Z2u // Zminus_0_r.
by apply min_u2Z.
clear Hs0 H_s_st_h.
move: na0 s0 s st h Hset Ha0.
elim.
- move=> s0 s st h Hset Ha0.
exists (Some (s0, h)); split; last by done.
apply while.exec_while_false.
+ rewrite /= in Ha0 *.
apply/negPn. apply/Zeq_boolP; omega.
+ move=> na0 IH s0 s st h Hset Ha0.
apply exists_while_P.
* rewrite /=; rewrite Z_S in Ha0.
apply/Zeq_boolP; omega.
* apply exists_seq_P with (fun s => forall s', s = Some s' ->
u2Z ([ rk ]_(fst s')) - u2Z ([ a0 ]_(fst s')) = Z_of_nat na0)%mips_expr.
- exists_lwxs l_a0 H_l_a0 z_a0 H_z_a0.
apply exists_srl_seq_P.
repeat reg_upd.
apply exists_sll_seq_P.
repeat reg_upd.
apply exists_or_seq_P.
repeat reg_upd.
rewrite store.upd_upd_eq.
apply exists_addiu_seq_P.
repeat reg_upd.
apply exists_sll_seq_P.
repeat reg_upd.
apply exists_addu_seq_P.
repeat reg_upd.
rewrite store.upd_upd_eq.
exists_sw_P l_idx H_l_idx z_idx H_z_idx.
repeat reg_upd.
apply exists_addiu_P.
rewrite /=.
repeat reg_upd.
rewrite Z_S in Ha0.
rewrite sext_Z2u // u2Z_add_Z2u //.
omega.
move: (min_u2Z ([a0]_s0)%mips_expr) (min_u2Z ([rk]_s0)%mips_expr) (max_u2Z ([rk]_s0)%mips_expr) => ? ? ?.
omega.
- move=> si Hsi.
destruct si as [[sti hi] |].
+ apply IH => //.
by move: {Hsi}(Hsi _ (refl_equal _)).
+ exists None; split; [by apply while.exec_none | done].
by exists sf.
apply constructive_indefinite_description'.
have H1 : (u2Z ([ rx ]_ st) + 4 * Z_of_nat (Zabs_nat (u2Z ([rk ]_ st))) < Zbeta 1)%mips_expr.
eapply state_mint_unsign_fit; by apply H_s_st_h.
have H3 : (length (Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([ x ]_ s)%seplog_expr) =
Zabs_nat (u2Z ([rk ]_ st)))%mips_expr.
by rewrite len_Z2ints.
move: (multi_mul2_triple _ _ _ _ _ _ Hset _ _ H1 _ H3) => Htriple.
move: (mips_syntax.triple_exec_precond _ _ _ Htriple _ _ _ exec_mips
(seq_ext.l2s (List.seq (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))%mips_expr)).
apply.
split; first by done.
split.
- rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
- apply (state_mint_var_mint _ _ _ _ x (unsign rk rx)) in H_s_st_h; last by assoc_get_Some.
rewrite /var_mint /var_unsign in H_s_st_h; tauto.
Qed.