Library multi_div2_simu
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_tactics mips_syntax.
Import mips_bipl.expr_m.
Require Import simu.
Import simu.simu_m.
Require Import multi_div2_prg multi_div2_triple.
Local Open Scope heap_scope.
Local Open Scope assoc_scope.
Local Open Scope nodup_scope.
Local Open Scope machine_int_scope.
Lemma pfwd_sim_div2 : forall (P : simu_m.relat) (x : bipl.var.v) d (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 ->
pfwd_sim (state_mint (x |=> unsign rk rx \U+ d)) P
(x <- var_e x ./e nat_e 2)%seplog_expr%seplog_cmd
(multi_div2 rk rx a0 a1 a2 a3).
Proof.
move=> P x d rk rx a0 a1 a2 a3 Haux Hd Hd' Hd''.
rewrite /pfwd_sim.
move=> s st h s_st_h _ s' exec_pseudo st' h' exec_mips.
have Hd_unchanged : forall v r, assoc.get v d = Some r ->
disj (mint_regs r) (mips_frame.modified_regs (multi_div2 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_div2 rk rx a0 a1 a2 a3 ---> Some (st'', h''))%mips_cmd.
exists st', (heap.proj h' (heap.dom (heap_mint (unsign rk rx) st h))).
have Hhoare_multi_div2 : mips_seplog.WMIPS_Hoare.hoare
(fun st0 h0 => [rx ]_ st0 = [rx ]_ st /\ u2Z ([rk ]_ st0) = Z_of_nat nk /\
(var_e rx |--> Z2ints 32 nk ([ x ]_ s)%seplog_expr)%mips_assert st0 h0)%mips_expr
(multi_div2 rk rx a0 a1 a2 a3)
(fun st0 h0 => exists A', length A' = nk /\ (var_e rx |--> A')%mips_assert st0 h0 /\
2 * Sum nk A' + u2Z ([a2 ]_ st0 [.>>] 31) = Sum nk (Z2ints 32 nk ([ x ]_ s)%seplog_expr))%mips_expr.
apply multi_div2_triple => //.
by eapply state_mint_unsign_fit; eauto.
by rewrite len_Z2ints.
apply (mips_syntax.triple_exec_proj _ _ _ Hhoare_multi_div2) => {Hhoare_multi_div2} //.
split; first by reflexivity.
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 /var_unsign in s_st_h; tauto.
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 x'_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 done.
apply disj_sym, (Hd_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 done.
apply disj_sym, (Hd_unchanged y) => //.
by rewrite -y_ry assoc.get_union_sing_neq.
exact x'_unchanged.
+ 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 /heap_mint.
set vx := u2Z ([ rx ]_ st)%mips_expr.
set nk' := Zabs_nat (u2Z (store.get rk st')).
set vx' := u2Z (store.get rx st').
case=> Hs_st_h_fit [[Hs_st_h_over1 Hs_st_h_over2] Hs_st_h_heap].
have Hset : nodup(rk, rx, a0, a1, a2, a3, r0) by Nodup_nodup r0.
move: (multi_div2_triple _ _ _ _ _ _ Hset _ (store.get rx st) Hs_st_h_fit (Z2ints 32 nk ([var_e x ]e_s))%seplog_expr).
rewrite len_Z2ints.
move/(_ (refl_equal _)) => Hdiv2.
move: {Hdiv2}(mips_frame.frame_rule _ _ _ Hdiv2 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) => Hdiv2.
lapply Hdiv2; 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 => //; 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=> {Hdiv2} [Hdiv2 Hdiv2'].
move: {Hdiv2'}(Hdiv2' _ _ exec_mips).
move=> [h1 [h2 [Hdisj [Hunion [[A' [Hdiv2_1 [Hdiv2_2 Hdiv2_3]]] HTT]]]]].
have Hnknk' : nk = nk'.
rewrite /nk /nk'; do 2 f_equal.
Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
subst nk'.
have Hvxvx' : vx = vx'.
rewrite /vx /vx'; f_equal.
Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
subst vx'.
split.
by rewrite -Hvxvx' -Hnknk'.
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.
by apply Z_div_pos.
- 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_div.
apply Zle_lt_trans with ([ x ]_s)%seplog_expr => //.
apply Zdiv_le_upper_bound => //; omega.
by rewrite -Hnknk'.
move: (Hdiv2_2) => Hdiv2_2_save.
apply mapstos_inv_list2heap in Hdiv2_2 => //; last first.
by rewrite [eval _ _]/= Hdiv2_1 -Hvxvx'.
rewrite u2Z_shrl' in Hdiv2_2; last by repeat constructor.
rewrite /= -Hvxvx' in Hdiv2_2.
rewrite /heap_cut Hunion Hdiv2_2.
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 // in Hdiv2_3.
rewrite [syntax_m.seplog_m.assert_m.expr_m.eval _ _]/= in Hdiv2_3.
rewrite -Hdiv2_3 Zmult_comm /ZIT.t_div Z_div_plus_full_l //.
rewrite (Zdiv_small (u2Z ([a2]_ st' [.>>]31)))%mips_expr.
rewrite Zplus_0_r -Hnknk' -Z2ints_Sum //.
rewrite /heap_cut.
have <- : heap.dom (list2heap (Zabs_nat (vx / 4)) A') =
seq_ext.l2s ((List.seq (Zabs_nat (u2Z ([rx ]_ st')%mips_expr / 4)) nk) : list assoc.l).
by rewrite dom_list2heap Hdiv2_1 Hvxvx'.
rewrite heap.proj_union_L; last by rewrite -Hdiv2_2.
rewrite heap.proj_itself.
rewrite -Hdiv2_2; exact Hdiv2_2_save.
split; first by apply min_u2Z.
by apply (shrl_lt (store.get a2 st') 31).
- 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_div2 : 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_div2 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 Htmp : {x0 | Some (st, h) -- multi_div2 rk rx a0 a1 a2 a3 --->x0}%mips_cmd.
have Htmp : {x0 | Some (st, h) -- multi_div2 rk rx a0 a1 a2 a3 ---> x0 /\ (forall s, x0 = Some s -> True)}%mips_cmd.
rewrite /multi_div2.
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 ([a0]_s0)%mips_expr = Z_of_nat na0 }.
apply Z_of_nat_complete_inf; 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 *.
rewrite store.get_r0 u2Z_Z2u //.
by apply/negPn; apply/Zeq_boolP.
+ move=> na0 IH s0 s st h Hset Ha0.
apply exists_while_P.
* rewrite /= store.get_r0 u2Z_Z2u // Ha0 Z_S.
apply/Zeq_boolP; omega.
* apply exists_seq_P with (fun s => forall s', s = Some s' ->
u2Z ([ a0 ]_(fst s')) = Z_of_nat na0)%mips_expr.
- apply exists_addiu_seq_P.
exists_lwxs l_a0 H_l_a0 z_a0 H_z_a0.
apply exists_andi_seq_P.
repeat reg_upd.
apply exists_srl_seq_P.
repeat reg_upd.
apply exists_or_seq_P.
repeat reg_upd.
apply exists_addiu_seq_P.
repeat reg_upd.
apply exists_sll_seq_P.
repeat reg_upd.
apply exists_sll_seq_P.
repeat reg_upd.
apply exists_addu_seq_P.
repeat reg_upd.
exists_sw1 l_idx H_l_idx z_idx H_z_idx.
rewrite /=.
repeat reg_upd.
rewrite sext_Z2s // u2Z_add_Z2s // Ha0 Z_S; 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.
case: Htmp => x0 [Htmp _].
by exists x0.
apply constructive_indefinite_description'.
have H1 : (u2Z ([ rx ]_ st) + 4 * Z_of_nat (Zabs_nat (u2Z ([rk ]_ st))) < Zbeta 1)%mips_expr.
apply state_mint_unsign_fit with x d s h.
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_div2_triple _ _ _ _ _ _ Hset _ _ H1 _ H3) => Htriple.
case: Htmp => x0 Htmp.
move: (mips_syntax.triple_exec_precond _ _ _ Htriple _ _ _ Htmp (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.
by apply H_s_st_h.
Qed.
Require Import ZArith_ext Lists_ext.
Require Import machine_int multi_int encode_decode integral_type.
Import MachineInt.
Require Import mips_bipl mips_tactics mips_syntax.
Import mips_bipl.expr_m.
Require Import simu.
Import simu.simu_m.
Require Import multi_div2_prg multi_div2_triple.
Local Open Scope heap_scope.
Local Open Scope assoc_scope.
Local Open Scope nodup_scope.
Local Open Scope machine_int_scope.
Lemma pfwd_sim_div2 : forall (P : simu_m.relat) (x : bipl.var.v) d (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 ->
pfwd_sim (state_mint (x |=> unsign rk rx \U+ d)) P
(x <- var_e x ./e nat_e 2)%seplog_expr%seplog_cmd
(multi_div2 rk rx a0 a1 a2 a3).
Proof.
move=> P x d rk rx a0 a1 a2 a3 Haux Hd Hd' Hd''.
rewrite /pfwd_sim.
move=> s st h s_st_h _ s' exec_pseudo st' h' exec_mips.
have Hd_unchanged : forall v r, assoc.get v d = Some r ->
disj (mint_regs r) (mips_frame.modified_regs (multi_div2 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_div2 rk rx a0 a1 a2 a3 ---> Some (st'', h''))%mips_cmd.
exists st', (heap.proj h' (heap.dom (heap_mint (unsign rk rx) st h))).
have Hhoare_multi_div2 : mips_seplog.WMIPS_Hoare.hoare
(fun st0 h0 => [rx ]_ st0 = [rx ]_ st /\ u2Z ([rk ]_ st0) = Z_of_nat nk /\
(var_e rx |--> Z2ints 32 nk ([ x ]_ s)%seplog_expr)%mips_assert st0 h0)%mips_expr
(multi_div2 rk rx a0 a1 a2 a3)
(fun st0 h0 => exists A', length A' = nk /\ (var_e rx |--> A')%mips_assert st0 h0 /\
2 * Sum nk A' + u2Z ([a2 ]_ st0 [.>>] 31) = Sum nk (Z2ints 32 nk ([ x ]_ s)%seplog_expr))%mips_expr.
apply multi_div2_triple => //.
by eapply state_mint_unsign_fit; eauto.
by rewrite len_Z2ints.
apply (mips_syntax.triple_exec_proj _ _ _ Hhoare_multi_div2) => {Hhoare_multi_div2} //.
split; first by reflexivity.
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 /var_unsign in s_st_h; tauto.
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 x'_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 done.
apply disj_sym, (Hd_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 done.
apply disj_sym, (Hd_unchanged y) => //.
by rewrite -y_ry assoc.get_union_sing_neq.
exact x'_unchanged.
+ 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 /heap_mint.
set vx := u2Z ([ rx ]_ st)%mips_expr.
set nk' := Zabs_nat (u2Z (store.get rk st')).
set vx' := u2Z (store.get rx st').
case=> Hs_st_h_fit [[Hs_st_h_over1 Hs_st_h_over2] Hs_st_h_heap].
have Hset : nodup(rk, rx, a0, a1, a2, a3, r0) by Nodup_nodup r0.
move: (multi_div2_triple _ _ _ _ _ _ Hset _ (store.get rx st) Hs_st_h_fit (Z2ints 32 nk ([var_e x ]e_s))%seplog_expr).
rewrite len_Z2ints.
move/(_ (refl_equal _)) => Hdiv2.
move: {Hdiv2}(mips_frame.frame_rule _ _ _ Hdiv2 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) => Hdiv2.
lapply Hdiv2; 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 => //; 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=> {Hdiv2} [Hdiv2 Hdiv2'].
move: {Hdiv2'}(Hdiv2' _ _ exec_mips).
move=> [h1 [h2 [Hdisj [Hunion [[A' [Hdiv2_1 [Hdiv2_2 Hdiv2_3]]] HTT]]]]].
have Hnknk' : nk = nk'.
rewrite /nk /nk'; do 2 f_equal.
Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
subst nk'.
have Hvxvx' : vx = vx'.
rewrite /vx /vx'; f_equal.
Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
subst vx'.
split.
by rewrite -Hvxvx' -Hnknk'.
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.
by apply Z_div_pos.
- 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_div.
apply Zle_lt_trans with ([ x ]_s)%seplog_expr => //.
apply Zdiv_le_upper_bound => //; omega.
by rewrite -Hnknk'.
move: (Hdiv2_2) => Hdiv2_2_save.
apply mapstos_inv_list2heap in Hdiv2_2 => //; last first.
by rewrite [eval _ _]/= Hdiv2_1 -Hvxvx'.
rewrite u2Z_shrl' in Hdiv2_2; last by repeat constructor.
rewrite /= -Hvxvx' in Hdiv2_2.
rewrite /heap_cut Hunion Hdiv2_2.
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 // in Hdiv2_3.
rewrite [syntax_m.seplog_m.assert_m.expr_m.eval _ _]/= in Hdiv2_3.
rewrite -Hdiv2_3 Zmult_comm /ZIT.t_div Z_div_plus_full_l //.
rewrite (Zdiv_small (u2Z ([a2]_ st' [.>>]31)))%mips_expr.
rewrite Zplus_0_r -Hnknk' -Z2ints_Sum //.
rewrite /heap_cut.
have <- : heap.dom (list2heap (Zabs_nat (vx / 4)) A') =
seq_ext.l2s ((List.seq (Zabs_nat (u2Z ([rx ]_ st')%mips_expr / 4)) nk) : list assoc.l).
by rewrite dom_list2heap Hdiv2_1 Hvxvx'.
rewrite heap.proj_union_L; last by rewrite -Hdiv2_2.
rewrite heap.proj_itself.
rewrite -Hdiv2_2; exact Hdiv2_2_save.
split; first by apply min_u2Z.
by apply (shrl_lt (store.get a2 st') 31).
- 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_div2 : 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_div2 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 Htmp : {x0 | Some (st, h) -- multi_div2 rk rx a0 a1 a2 a3 --->x0}%mips_cmd.
have Htmp : {x0 | Some (st, h) -- multi_div2 rk rx a0 a1 a2 a3 ---> x0 /\ (forall s, x0 = Some s -> True)}%mips_cmd.
rewrite /multi_div2.
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 ([a0]_s0)%mips_expr = Z_of_nat na0 }.
apply Z_of_nat_complete_inf; 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 *.
rewrite store.get_r0 u2Z_Z2u //.
by apply/negPn; apply/Zeq_boolP.
+ move=> na0 IH s0 s st h Hset Ha0.
apply exists_while_P.
* rewrite /= store.get_r0 u2Z_Z2u // Ha0 Z_S.
apply/Zeq_boolP; omega.
* apply exists_seq_P with (fun s => forall s', s = Some s' ->
u2Z ([ a0 ]_(fst s')) = Z_of_nat na0)%mips_expr.
- apply exists_addiu_seq_P.
exists_lwxs l_a0 H_l_a0 z_a0 H_z_a0.
apply exists_andi_seq_P.
repeat reg_upd.
apply exists_srl_seq_P.
repeat reg_upd.
apply exists_or_seq_P.
repeat reg_upd.
apply exists_addiu_seq_P.
repeat reg_upd.
apply exists_sll_seq_P.
repeat reg_upd.
apply exists_sll_seq_P.
repeat reg_upd.
apply exists_addu_seq_P.
repeat reg_upd.
exists_sw1 l_idx H_l_idx z_idx H_z_idx.
rewrite /=.
repeat reg_upd.
rewrite sext_Z2s // u2Z_add_Z2s // Ha0 Z_S; 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.
case: Htmp => x0 [Htmp _].
by exists x0.
apply constructive_indefinite_description'.
have H1 : (u2Z ([ rx ]_ st) + 4 * Z_of_nat (Zabs_nat (u2Z ([rk ]_ st))) < Zbeta 1)%mips_expr.
apply state_mint_unsign_fit with x d s h.
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_div2_triple _ _ _ _ _ _ Hset _ _ H1 _ H3) => Htriple.
case: Htmp => x0 Htmp.
move: (mips_syntax.triple_exec_precond _ _ _ Htriple _ _ _ Htmp (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.
by apply H_s_st_h.
Qed.