Library multi_zero_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_seplog mips_tactics mips_syntax.
Import mips_bipl.expr_m.
Require Import simu.
Import simu.simu_m.
Require Import multi_zero_prg multi_zero_triple.
Local Open Scope machine_int_scope.
Local Open Scope heap_scope.
Local Open Scope assoc_scope.
Local Open Scope nodup_scope.
Lemma pfwd_sim_zero_unsigned : forall (P : simu_m.relat) (x : bipl.var.v) d (rk rx a0 a1 : reg),
nodup(rk, rx, a0, a1, r0) ->
disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: 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 <- nat_e%seplog_expr O)%seplog_cmd
(multi_zero rk rx a0 a1).
Proof.
move=> P x d rk rx a0 a1 Hregs Hd x_d rk_rk_d.
have Hd_unchanged : forall v r, assoc.get v d = Some r ->
disj (mint_regs r) (mips_frame.modified_regs (multi_zero rk rx a0 a1)).
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).
rewrite /pfwd_sim.
move=> s st h s_st_h HP s' exec_seplog st' h' exec_mips.
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_zero rk rx a0 a1 ---> Some (st'', h''))%mips_cmd.
exists st'.
exists (heap.proj h' (heap.dom (heap_mint (unsign rk rx) st h))).
set nk := Zabs_nat (u2Z ([rk ]_ st)%mips_expr).
have Hoare_multi_zero : ( {{ (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_zero rk rx a0 a1
{{ (fun s0 h0 => [rx ]_ s0 = [rx ]_ st /\
u2Z ([rk ]_ s0) = Z_of_nat nk /\ (var_e rx |--> rep zero32 nk) s0 h0) }} )%mips_assert%mips_expr%mips_hoare.
apply multi_zero_triple => //.
by rewrite len_Z2ints.
by eapply state_mint_unsign_fit; eauto.
move/mips_syntax.triple_exec_proj : Hoare_multi_zero; 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 => _ [_ ?].
rewrite /state_mint; split.
- move=> y ry y_ry.
have [y_d | y_x] : 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.
+ move: (proj1 s_st_h y) => s_st_h1.
have x_y : x <> y.
move=> X; subst y. by rewrite y_d in x_d.
move: {s_st_h1}(s_st_h1 _ y_ry) => s_st_h1.
have <- : heap_mint ry st h = heap_mint ry st' h'.
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'].
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, (Hd_unchanged y).
by rewrite -y_ry assoc.get_union_sing_neq; last by auto.
apply (proj2 s_st_h) with y x => //.
by auto.
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, (Hd_unchanged y) => //.
by rewrite -y_ry assoc.get_union_sing_neq; auto.
Var_unchanged; rewrite /=; by intuition.
+ subst y.
rewrite assoc.get_union_sing_eq in y_ry; case: y_ry => ?; subst ry.
move: {s_st_h}(proj1 s_st_h x (unsign rk rx)).
rewrite assoc.get_union_sing_eq.
case/(_ (refl_equal _)) => s_st_h1 [s_st_h2 s_st_h3].
rewrite /var_mint /var_unsign.
have <- : ([rx ]_ st = [rx ]_ st')%mips_expr.
Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
have <- : ([rk ]_ st = [rk ]_ st')%mips_expr.
Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_seplog.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
syntax_m.seplog_m.assert_m.expr_m.Store_upd.
split; first by exact s_st_h1.
split.
split; [done | by apply Zbeta_0].
have : nodup(rk, rx, a0, a1, r0) by Nodup_nodup r0.
move/multi_zero_triple.
set nk := Zabs_nat (u2Z ([rk ]_ st)%mips_expr).
set vx := ([rx ]_ st)%mips_expr.
move/(_ nk (Z2ints 32 nk ([x ]_ s)%seplog_expr) vx).
rewrite len_Z2ints.
move/(_ (refl_equal _) s_st_h1).
move/mips_seplog.hoare_prop_m.soundness.
rewrite /while.hoare_semantics.
move/(_ st (heap_mint (unsign rk rx) st h)).
rewrite {1}/nk Z_of_nat_Zabs_nat; last by apply min_u2Z.
rewrite {1}/vx {1}/nk.
move/( _ (conj (refl_equal _) (conj (refl_equal _) s_st_h3))).
case=> _.
rewrite (var_mint_unsign_dom_heap_mint x s rk rx st h (conj s_st_h1 (conj s_st_h2 s_st_h3))) in exec_mips_proj.
move/(_ _ _ exec_mips_proj).
case=> _ [] _.
rewrite (proj1 (proj2 (mips_syntax.exec_deter_proj _ _ _ _ _ exec_mips _ _ _ exec_mips_proj))).
rewrite -(proj1 (mips_syntax.exec_deter_proj _ _ _ _ _ exec_mips _ _ _ exec_mips_proj)).
rewrite /heap_mint /heap_cut.
have <- : ([rx ]_ st = [rx ]_ st')%mips_expr.
Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
have <- : ([rk ]_ st = [rk ]_ st')%mips_expr.
Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
done.
- 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.
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_zero_prg multi_zero_triple.
Local Open Scope machine_int_scope.
Local Open Scope heap_scope.
Local Open Scope assoc_scope.
Local Open Scope nodup_scope.
Lemma pfwd_sim_zero_unsigned : forall (P : simu_m.relat) (x : bipl.var.v) d (rk rx a0 a1 : reg),
nodup(rk, rx, a0, a1, r0) ->
disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: 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 <- nat_e%seplog_expr O)%seplog_cmd
(multi_zero rk rx a0 a1).
Proof.
move=> P x d rk rx a0 a1 Hregs Hd x_d rk_rk_d.
have Hd_unchanged : forall v r, assoc.get v d = Some r ->
disj (mint_regs r) (mips_frame.modified_regs (multi_zero rk rx a0 a1)).
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).
rewrite /pfwd_sim.
move=> s st h s_st_h HP s' exec_seplog st' h' exec_mips.
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_zero rk rx a0 a1 ---> Some (st'', h''))%mips_cmd.
exists st'.
exists (heap.proj h' (heap.dom (heap_mint (unsign rk rx) st h))).
set nk := Zabs_nat (u2Z ([rk ]_ st)%mips_expr).
have Hoare_multi_zero : ( {{ (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_zero rk rx a0 a1
{{ (fun s0 h0 => [rx ]_ s0 = [rx ]_ st /\
u2Z ([rk ]_ s0) = Z_of_nat nk /\ (var_e rx |--> rep zero32 nk) s0 h0) }} )%mips_assert%mips_expr%mips_hoare.
apply multi_zero_triple => //.
by rewrite len_Z2ints.
by eapply state_mint_unsign_fit; eauto.
move/mips_syntax.triple_exec_proj : Hoare_multi_zero; 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 => _ [_ ?].
rewrite /state_mint; split.
- move=> y ry y_ry.
have [y_d | y_x] : 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.
+ move: (proj1 s_st_h y) => s_st_h1.
have x_y : x <> y.
move=> X; subst y. by rewrite y_d in x_d.
move: {s_st_h1}(s_st_h1 _ y_ry) => s_st_h1.
have <- : heap_mint ry st h = heap_mint ry st' h'.
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'].
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, (Hd_unchanged y).
by rewrite -y_ry assoc.get_union_sing_neq; last by auto.
apply (proj2 s_st_h) with y x => //.
by auto.
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, (Hd_unchanged y) => //.
by rewrite -y_ry assoc.get_union_sing_neq; auto.
Var_unchanged; rewrite /=; by intuition.
+ subst y.
rewrite assoc.get_union_sing_eq in y_ry; case: y_ry => ?; subst ry.
move: {s_st_h}(proj1 s_st_h x (unsign rk rx)).
rewrite assoc.get_union_sing_eq.
case/(_ (refl_equal _)) => s_st_h1 [s_st_h2 s_st_h3].
rewrite /var_mint /var_unsign.
have <- : ([rx ]_ st = [rx ]_ st')%mips_expr.
Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
have <- : ([rk ]_ st = [rk ]_ st')%mips_expr.
Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_seplog.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
syntax_m.seplog_m.assert_m.expr_m.Store_upd.
split; first by exact s_st_h1.
split.
split; [done | by apply Zbeta_0].
have : nodup(rk, rx, a0, a1, r0) by Nodup_nodup r0.
move/multi_zero_triple.
set nk := Zabs_nat (u2Z ([rk ]_ st)%mips_expr).
set vx := ([rx ]_ st)%mips_expr.
move/(_ nk (Z2ints 32 nk ([x ]_ s)%seplog_expr) vx).
rewrite len_Z2ints.
move/(_ (refl_equal _) s_st_h1).
move/mips_seplog.hoare_prop_m.soundness.
rewrite /while.hoare_semantics.
move/(_ st (heap_mint (unsign rk rx) st h)).
rewrite {1}/nk Z_of_nat_Zabs_nat; last by apply min_u2Z.
rewrite {1}/vx {1}/nk.
move/( _ (conj (refl_equal _) (conj (refl_equal _) s_st_h3))).
case=> _.
rewrite (var_mint_unsign_dom_heap_mint x s rk rx st h (conj s_st_h1 (conj s_st_h2 s_st_h3))) in exec_mips_proj.
move/(_ _ _ exec_mips_proj).
case=> _ [] _.
rewrite (proj1 (proj2 (mips_syntax.exec_deter_proj _ _ _ _ _ exec_mips _ _ _ exec_mips_proj))).
rewrite -(proj1 (mips_syntax.exec_deter_proj _ _ _ _ _ exec_mips _ _ _ exec_mips_proj)).
rewrite /heap_mint /heap_cut.
have <- : ([rx ]_ st = [rx ]_ st')%mips_expr.
Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
have <- : ([rk ]_ st = [rk ]_ st')%mips_expr.
Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
done.
- 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.