Library multi_is_even_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_is_even_prg multi_is_even_triple.
Local Open Scope machine_int_scope.
Local Open Scope heap_scope.
Local Open Scope assoc_scope.
Local Open Scope nodup_scope.
Lemma var_mint_multi_is_even : forall u rk ru s st h a0,
nodup(rk, ru, a0, r0) ->
var_mint u (unsign rk ru) s st (heap_mint (unsign rk ru) st h) ->
forall st' h',
(Some (st, h) -- multi_is_even rk ru a0 ---> Some (st', h'))%mips_cmd ->
(([var_e u mode nat_e 2 =e nat_e 1 ]b_ s)%seplog_expr <->
(eval_b (beq a0 r0) st')).
Proof.
move=> u rk ru s st h a0 Hset u_ru st' h' exec_asm.
case: u_ru => u_ru [u_ru' u_ru''].
move: (multi_is_even_triple _ _ _ Hset (Zabs_nat (u2Z ([rk ]_ st))) (Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([u ]_ s)%seplog_expr) ([ru]_st))%mips_expr.
rewrite len_Z2ints.
move/(_ (refl_equal _)) => hoare_triple.
move/mips_seplog.hoare_prop_m.soundness : (hoare_triple).
rewrite /while.hoare_semantics.
move/(_ st (heap_mint (unsign rk ru) st h)).
rewrite Z_of_nat_Zabs_nat; last by apply min_u2Z.
move/( _ (conj (refl_equal _) (conj (refl_equal _) u_ru''))).
case=> _.
have exec_asm':
((Some (st, heap_mint (unsign rk ru) st h)) -- multi_is_even rk ru a0 ---> Some (st', heap_mint (unsign rk ru) st h'))%mips_cmd.
rewrite /heap_mint /heap_cut.
eapply mips_syntax.triple_exec_proj; last by exact exec_asm.
apply hoare_triple.
rewrite /= Z_of_nat_Zabs_nat //; by apply min_u2Z.
case/(_ _ _ exec_asm') => Hrk [Hru [Hmem [Heven Hodd]]].
split.
- rewrite /= /ZIT.t_eqb /ZIT.t_mod.
move/eqP => X.
rewrite store.get_r0 u2Z_Z2u //.
apply/eqP.
rewrite Hodd //; last first.
rewrite Sum_Z2ints_pos //.
apply not_Zmod_2_Zodd.
by rewrite X.
by rewrite u2Z_Z2u.
- rewrite /= /ZIT.t_eqb /ZIT.t_mod.
move/eqP => X.
rewrite store.get_r0 u2Z_Z2u // in X.
apply/Zeq_boolP.
rewrite Sum_Z2ints_pos // in Heven.
rewrite Sum_Z2ints_pos // in Hodd.
case: (Zeven_odd_dec ([u]_s)%seplog_expr) => abs.
apply Heven in abs.
by rewrite abs u2Z_Z2u in X.
by apply Zodd_Zmod_2.
Qed.
Lemma fwd_sim_b_multi_is_even : forall (u : bipl.var.v) rk ru d a0,
nodup(rk, ru, a0, r0) ->
disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: nil) ->
u \notin assoc.dom d ->
unsign rk ru \notin assoc.cdom d ->
fwd_sim_b (state_mint (u |=> unsign rk ru \U+ d ))
(var_e u mode nat_e 2 =e nat_e 1)%seplog_expr
(multi_is_even rk ru a0)
(beq a0 r0).
Proof.
move=> u rk ru d a0 Hregs d_a0 u_d rk_ru_d.
rewrite /fwd_sim_b => s st h s_st_h.
set nk := Zabs_nat (u2Z [rk]_st)%mips_expr.
set U := Z2ints 32 nk ([ u ]_ s)%seplog_expr.
have Hpre : (var_e ru |--> U)%mips_expr%mips_assert st (heap_mint (unsign rk ru) st h).
move: (proj1 s_st_h u (unsign rk ru)).
rewrite assoc.get_union_sing_eq. case/(_ (refl_equal _)) => _ [_]; exact.
move: (multi_is_even_triple _ _ _ Hregs nk U [ru]_st)%mips_expr.
rewrite /U len_Z2ints.
move/(_ (refl_equal _)) => Htriple.
set code := multi_is_even _ _ _.
have [st' Hst'] : exists st', (Some (st, h) -- code ---> Some (st', h))%mips_cmd.
have [[st' he'] Hst'] : exists st', (Some (st, h) -- code ---> Some st')%mips_cmd.
apply constructive_indefinite_description'.
eapply mips_seplog.hoare_prop_m.termi.
- apply mips_frame.frame_rule with (R := assert_m.TT).
+ by apply Htriple.
+ by Inde.
+ move=> ?; by Inde_mult.
- move=> s0 h0 /= H.
apply Epsilon.constructive_indefinite_description.
by apply mips_syntax.no_while_terminate.
- exists (heap_mint (unsign rk ru) st h).
exists (h [\m] seq_ext.ran (Zabs_nat (u2Z ([ru ]_ st) / 4)) nk)%mips_expr.
split.
rewrite /= /heap_cut.
apply heap.proj_difs_disj.
rewrite seq_ext.l2s_seq.
by apply seq_ext.inc_refl.
split.
rewrite /= /heap_cut seq_ext.l2s_seq.
by apply heap.proj_difs.
split; last by done.
split; first by rewrite /nk Z_of_nat_Zabs_nat //; apply min_u2Z.
split; first by reflexivity.
exact Hpre.
exists st'.
suff : h = 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 exact Hst'.
move/mips_seplog.soundness : (Htriple).
rewrite /while.hoare_semantics.
move/(_ st (heap_mint (unsign rk ru) st h)).
rewrite {1}/nk Z_of_nat_Zabs_nat; last by apply min_u2Z.
case/(_ (conj (refl_equal _) (conj (refl_equal _) Hpre))) => _ Hpost.
move: {Htriple}(mips_syntax.triple_exec_proj _ _ _ Htriple) => Hexec_proj.
rewrite {1}/nk Z_of_nat_Zabs_nat in Hexec_proj; last by apply min_u2Z.
rewrite /heap_mint /heap_cut in Hpre.
move: {Hexec_proj Hpre}(Hexec_proj _ _ _ _ _ (conj (refl_equal _) (conj (refl_equal _) Hpre)) Hst').
move/Hpost => {Hpost} Hpost.
case: Hpost => Hrk' [Hru' [Hmem Hret]].
rewrite Sum_Z2ints_pos in Hret; last first.
move: (proj1 s_st_h u (unsign rk ru)).
rewrite assoc.get_union_sing_eq.
move/(_ (refl_equal _)).
rewrite /var_mint.
by case=> ? [].
split=> [u_mod_2|].
+ apply/Zeq_boolP.
f_equal.
rewrite store.get_r0.
apply (proj2 Hret).
rewrite /= in u_mod_2.
apply not_Zmod_2_Zodd.
move/Zeq_boolP : u_mod_2.
by rewrite /ZIT.t_mod => ->.
+ apply contra => u_mod_2.
apply/Zeq_boolP => /=.
move/Zeq_boolP : u_mod_2.
rewrite store.get_r0 u2Z_Z2u // => Ha0.
case: (Zeven_odd_dec ([u ]_ s)%seplog_expr) => Hu.
by rewrite (proj1 Hret Hu) u2Z_Z2u in Ha0.
by apply Zodd_Zmod_2.
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_is_even_prg multi_is_even_triple.
Local Open Scope machine_int_scope.
Local Open Scope heap_scope.
Local Open Scope assoc_scope.
Local Open Scope nodup_scope.
Lemma var_mint_multi_is_even : forall u rk ru s st h a0,
nodup(rk, ru, a0, r0) ->
var_mint u (unsign rk ru) s st (heap_mint (unsign rk ru) st h) ->
forall st' h',
(Some (st, h) -- multi_is_even rk ru a0 ---> Some (st', h'))%mips_cmd ->
(([var_e u mode nat_e 2 =e nat_e 1 ]b_ s)%seplog_expr <->
(eval_b (beq a0 r0) st')).
Proof.
move=> u rk ru s st h a0 Hset u_ru st' h' exec_asm.
case: u_ru => u_ru [u_ru' u_ru''].
move: (multi_is_even_triple _ _ _ Hset (Zabs_nat (u2Z ([rk ]_ st))) (Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st))) ([u ]_ s)%seplog_expr) ([ru]_st))%mips_expr.
rewrite len_Z2ints.
move/(_ (refl_equal _)) => hoare_triple.
move/mips_seplog.hoare_prop_m.soundness : (hoare_triple).
rewrite /while.hoare_semantics.
move/(_ st (heap_mint (unsign rk ru) st h)).
rewrite Z_of_nat_Zabs_nat; last by apply min_u2Z.
move/( _ (conj (refl_equal _) (conj (refl_equal _) u_ru''))).
case=> _.
have exec_asm':
((Some (st, heap_mint (unsign rk ru) st h)) -- multi_is_even rk ru a0 ---> Some (st', heap_mint (unsign rk ru) st h'))%mips_cmd.
rewrite /heap_mint /heap_cut.
eapply mips_syntax.triple_exec_proj; last by exact exec_asm.
apply hoare_triple.
rewrite /= Z_of_nat_Zabs_nat //; by apply min_u2Z.
case/(_ _ _ exec_asm') => Hrk [Hru [Hmem [Heven Hodd]]].
split.
- rewrite /= /ZIT.t_eqb /ZIT.t_mod.
move/eqP => X.
rewrite store.get_r0 u2Z_Z2u //.
apply/eqP.
rewrite Hodd //; last first.
rewrite Sum_Z2ints_pos //.
apply not_Zmod_2_Zodd.
by rewrite X.
by rewrite u2Z_Z2u.
- rewrite /= /ZIT.t_eqb /ZIT.t_mod.
move/eqP => X.
rewrite store.get_r0 u2Z_Z2u // in X.
apply/Zeq_boolP.
rewrite Sum_Z2ints_pos // in Heven.
rewrite Sum_Z2ints_pos // in Hodd.
case: (Zeven_odd_dec ([u]_s)%seplog_expr) => abs.
apply Heven in abs.
by rewrite abs u2Z_Z2u in X.
by apply Zodd_Zmod_2.
Qed.
Lemma fwd_sim_b_multi_is_even : forall (u : bipl.var.v) rk ru d a0,
nodup(rk, ru, a0, r0) ->
disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: nil) ->
u \notin assoc.dom d ->
unsign rk ru \notin assoc.cdom d ->
fwd_sim_b (state_mint (u |=> unsign rk ru \U+ d ))
(var_e u mode nat_e 2 =e nat_e 1)%seplog_expr
(multi_is_even rk ru a0)
(beq a0 r0).
Proof.
move=> u rk ru d a0 Hregs d_a0 u_d rk_ru_d.
rewrite /fwd_sim_b => s st h s_st_h.
set nk := Zabs_nat (u2Z [rk]_st)%mips_expr.
set U := Z2ints 32 nk ([ u ]_ s)%seplog_expr.
have Hpre : (var_e ru |--> U)%mips_expr%mips_assert st (heap_mint (unsign rk ru) st h).
move: (proj1 s_st_h u (unsign rk ru)).
rewrite assoc.get_union_sing_eq. case/(_ (refl_equal _)) => _ [_]; exact.
move: (multi_is_even_triple _ _ _ Hregs nk U [ru]_st)%mips_expr.
rewrite /U len_Z2ints.
move/(_ (refl_equal _)) => Htriple.
set code := multi_is_even _ _ _.
have [st' Hst'] : exists st', (Some (st, h) -- code ---> Some (st', h))%mips_cmd.
have [[st' he'] Hst'] : exists st', (Some (st, h) -- code ---> Some st')%mips_cmd.
apply constructive_indefinite_description'.
eapply mips_seplog.hoare_prop_m.termi.
- apply mips_frame.frame_rule with (R := assert_m.TT).
+ by apply Htriple.
+ by Inde.
+ move=> ?; by Inde_mult.
- move=> s0 h0 /= H.
apply Epsilon.constructive_indefinite_description.
by apply mips_syntax.no_while_terminate.
- exists (heap_mint (unsign rk ru) st h).
exists (h [\m] seq_ext.ran (Zabs_nat (u2Z ([ru ]_ st) / 4)) nk)%mips_expr.
split.
rewrite /= /heap_cut.
apply heap.proj_difs_disj.
rewrite seq_ext.l2s_seq.
by apply seq_ext.inc_refl.
split.
rewrite /= /heap_cut seq_ext.l2s_seq.
by apply heap.proj_difs.
split; last by done.
split; first by rewrite /nk Z_of_nat_Zabs_nat //; apply min_u2Z.
split; first by reflexivity.
exact Hpre.
exists st'.
suff : h = 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 exact Hst'.
move/mips_seplog.soundness : (Htriple).
rewrite /while.hoare_semantics.
move/(_ st (heap_mint (unsign rk ru) st h)).
rewrite {1}/nk Z_of_nat_Zabs_nat; last by apply min_u2Z.
case/(_ (conj (refl_equal _) (conj (refl_equal _) Hpre))) => _ Hpost.
move: {Htriple}(mips_syntax.triple_exec_proj _ _ _ Htriple) => Hexec_proj.
rewrite {1}/nk Z_of_nat_Zabs_nat in Hexec_proj; last by apply min_u2Z.
rewrite /heap_mint /heap_cut in Hpre.
move: {Hexec_proj Hpre}(Hexec_proj _ _ _ _ _ (conj (refl_equal _) (conj (refl_equal _) Hpre)) Hst').
move/Hpost => {Hpost} Hpost.
case: Hpost => Hrk' [Hru' [Hmem Hret]].
rewrite Sum_Z2ints_pos in Hret; last first.
move: (proj1 s_st_h u (unsign rk ru)).
rewrite assoc.get_union_sing_eq.
move/(_ (refl_equal _)).
rewrite /var_mint.
by case=> ? [].
split=> [u_mod_2|].
+ apply/Zeq_boolP.
f_equal.
rewrite store.get_r0.
apply (proj2 Hret).
rewrite /= in u_mod_2.
apply not_Zmod_2_Zodd.
move/Zeq_boolP : u_mod_2.
by rewrite /ZIT.t_mod => ->.
+ apply contra => u_mod_2.
apply/Zeq_boolP => /=.
move/Zeq_boolP : u_mod_2.
rewrite store.get_r0 u2Z_Z2u // => Ha0.
case: (Zeven_odd_dec ([u ]_ s)%seplog_expr) => Hu.
by rewrite (proj1 Hret Hu) u2Z_Z2u in Ha0.
by apply Zodd_Zmod_2.
Qed.