Library multi_lt_simu
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 multi_lt_prg multi_lt_triple multi_lt_termination.
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.
Lemma fwd_sim_b_ge_multi_lt : forall rk ru rv a3 flag a0 a1 ret ret2
z u d, nodup(z, u) ->
nodup(rk, ru, rv, a3, flag, ret, ret2, a0, a1, r0) ->
fwd_sim_b (state_mint (u |=> unsign rk ru \U+ (z |=> unsign rk rv \U+ d)))
(var_e u >>= var_e z)%seplog_expr
(multi_lt rk ru rv a3 flag ret ret2 a0 a1)
(beq ret r0).
Proof.
move=> rk ru rv a3 flag a0 a1 ret ret2 z u d Hvars Hregs.
rewrite /fwd_sim_b => s st h s_st_h.
set nk := Zabs_nat (u2Z [rk]_st).
set U := Z2ints 32 nk ([ u ]_ s)%seplog_expr.
set ZE := Z2ints 32 nk ([ z ]_ s)%seplog_expr.
have Hpre : (var_e ru |--> U ** var_e rv |--> ZE)%mips_assert st
(heap_mint (unsign rk ru) st h +++ heap_mint (unsign rk rv) st h).
apply assert_m.con_cons.
- apply (proj2 s_st_h u z); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
- move: (proj1 s_st_h u (unsign rk ru)).
rewrite assoc.get_union_sing_eq. case/(_ (refl_equal _)) => _ [_]; exact.
- move: (proj1 s_st_h z (unsign rk rv)).
rewrite assoc_prop_m.swap_heads; last by rewrite [Equality.sort _]/= in Hvars *; Nodup_nodup O.
rewrite assoc.get_union_sing_eq. case/(_ (refl_equal _)) => _ [_]; exact.
move: (multi_lt_triple _ _ _ _ _ _ _ _ _ Hregs nk U ZE [ru]_st [rv]_st).
rewrite /U len_Z2ints /ZE len_Z2ints.
move/(_ (refl_equal _) (refl_equal _)) => Htriple.
Local Open Scope mips_hoare_scope.
set code := multi_lt _ _ _ _ _ _ _ _ _.
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 termination_multi_lt; by Nodup_nodup r0.
- exists (heap_mint (unsign rk ru) st h +++ heap_mint (unsign rk rv) st h)%mips_expr.
exists (h [\m] (seq.cat
(seq_ext.ran (Zabs_nat (u2Z ([ru ]_ st) / 4)) nk)
(seq_ext.ran (Zabs_nat (u2Z ([rv ]_ st) / 4)) nk))).
split.
rewrite /= /heap_cut -heap.proj_app.
apply heap.proj_difs_disj.
rewrite 2!seq_ext.l2s_seq.
by apply seq_ext.inc_refl.
split.
rewrite /= /heap_cut -heap.proj_app 2!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.
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 +++ heap_mint (unsign rk rv) st h)).
rewrite {1}/nk Z_of_nat_Zabs_nat; last by apply min_u2Z.
case/(_ (conj (refl_equal _) (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 -heap.proj_app in Hpre.
move: {Hexec_proj Hpre}(Hexec_proj _ _ _ _ _ (conj (refl_equal _) (conj (refl_equal _) (conj (refl_equal _) Hpre))) Hst').
rewrite heap.proj_app.
move/Hpost => {Hpost} Hpost.
case: Hpost => Hrk' [Hru' [Hrv' [Hret Hmem]]].
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=> _ [].
rewrite Sum_Z2ints_pos in Hret; last first.
move: (proj1 s_st_h z (unsign rk rv)).
rewrite assoc_prop_m.swap_heads; last by rewrite [Equality.sort _]/= in Hvars *; Nodup_nodup O.
rewrite assoc.get_union_sing_eq.
move/(_ (refl_equal _)).
rewrite /var_mint.
by case=> _ [].
split => u_z.
+ case: Hret => Hret.
* case: Hret => u_z' _.
rewrite /= in u_z.
move/ZIT.t_geb_true : u_z; rewrite /ZIT.t_ge => u_z.
exfalso; omega.
* apply/Zeq_boolP.
rewrite store.get_r0.
f_equal.
tauto.
+ case : Hret => Hret.
* apply/Zeq_boolP.
by rewrite (proj1 (proj2 Hret)) store.get_r0 !u2Z_Z2u.
* rewrite /= in u_z.
suff : False by done.
move/negP : u_z; apply.
apply ZIT.t_geb_true'.
rewrite /ZIT.t_ge /=.
omega.
Qed.
Lemma fwd_sim_b_gt_multi_lt : forall rk ru rv a3 flag a0 a1 ret ret2 z u d,
nodup(z, u) -> nodup(rk, ru, rv, a3, flag, ret, ret2, a0, a1, r0) ->
fwd_sim_b (state_mint (u |=> unsign rk ru \U+ (z |=> unsign rk rv \U+ d)))
(var_e z >> var_e u)%seplog_expr
(multi_lt rk ru rv a3 flag ret ret2 a0 a1)
(bne ret r0).
Proof.
move=> rk ru rv a3 flag a0 a1 ret ret2 z u d Hvars Hset.
apply fwd_sim_b_cond_neg with (var_e u >>= var_e z)%seplog_expr (beq ret r0).
move=> s st h s_st_h.
rewrite /= -ZIT.t_gt_t_ge.
by apply/negbRL.
by move=> st /=.
by apply fwd_sim_b_ge_multi_lt.
Qed.
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 multi_lt_prg multi_lt_triple multi_lt_termination.
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.
Lemma fwd_sim_b_ge_multi_lt : forall rk ru rv a3 flag a0 a1 ret ret2
z u d, nodup(z, u) ->
nodup(rk, ru, rv, a3, flag, ret, ret2, a0, a1, r0) ->
fwd_sim_b (state_mint (u |=> unsign rk ru \U+ (z |=> unsign rk rv \U+ d)))
(var_e u >>= var_e z)%seplog_expr
(multi_lt rk ru rv a3 flag ret ret2 a0 a1)
(beq ret r0).
Proof.
move=> rk ru rv a3 flag a0 a1 ret ret2 z u d Hvars Hregs.
rewrite /fwd_sim_b => s st h s_st_h.
set nk := Zabs_nat (u2Z [rk]_st).
set U := Z2ints 32 nk ([ u ]_ s)%seplog_expr.
set ZE := Z2ints 32 nk ([ z ]_ s)%seplog_expr.
have Hpre : (var_e ru |--> U ** var_e rv |--> ZE)%mips_assert st
(heap_mint (unsign rk ru) st h +++ heap_mint (unsign rk rv) st h).
apply assert_m.con_cons.
- apply (proj2 s_st_h u z); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
- move: (proj1 s_st_h u (unsign rk ru)).
rewrite assoc.get_union_sing_eq. case/(_ (refl_equal _)) => _ [_]; exact.
- move: (proj1 s_st_h z (unsign rk rv)).
rewrite assoc_prop_m.swap_heads; last by rewrite [Equality.sort _]/= in Hvars *; Nodup_nodup O.
rewrite assoc.get_union_sing_eq. case/(_ (refl_equal _)) => _ [_]; exact.
move: (multi_lt_triple _ _ _ _ _ _ _ _ _ Hregs nk U ZE [ru]_st [rv]_st).
rewrite /U len_Z2ints /ZE len_Z2ints.
move/(_ (refl_equal _) (refl_equal _)) => Htriple.
Local Open Scope mips_hoare_scope.
set code := multi_lt _ _ _ _ _ _ _ _ _.
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 termination_multi_lt; by Nodup_nodup r0.
- exists (heap_mint (unsign rk ru) st h +++ heap_mint (unsign rk rv) st h)%mips_expr.
exists (h [\m] (seq.cat
(seq_ext.ran (Zabs_nat (u2Z ([ru ]_ st) / 4)) nk)
(seq_ext.ran (Zabs_nat (u2Z ([rv ]_ st) / 4)) nk))).
split.
rewrite /= /heap_cut -heap.proj_app.
apply heap.proj_difs_disj.
rewrite 2!seq_ext.l2s_seq.
by apply seq_ext.inc_refl.
split.
rewrite /= /heap_cut -heap.proj_app 2!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.
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 +++ heap_mint (unsign rk rv) st h)).
rewrite {1}/nk Z_of_nat_Zabs_nat; last by apply min_u2Z.
case/(_ (conj (refl_equal _) (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 -heap.proj_app in Hpre.
move: {Hexec_proj Hpre}(Hexec_proj _ _ _ _ _ (conj (refl_equal _) (conj (refl_equal _) (conj (refl_equal _) Hpre))) Hst').
rewrite heap.proj_app.
move/Hpost => {Hpost} Hpost.
case: Hpost => Hrk' [Hru' [Hrv' [Hret Hmem]]].
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=> _ [].
rewrite Sum_Z2ints_pos in Hret; last first.
move: (proj1 s_st_h z (unsign rk rv)).
rewrite assoc_prop_m.swap_heads; last by rewrite [Equality.sort _]/= in Hvars *; Nodup_nodup O.
rewrite assoc.get_union_sing_eq.
move/(_ (refl_equal _)).
rewrite /var_mint.
by case=> _ [].
split => u_z.
+ case: Hret => Hret.
* case: Hret => u_z' _.
rewrite /= in u_z.
move/ZIT.t_geb_true : u_z; rewrite /ZIT.t_ge => u_z.
exfalso; omega.
* apply/Zeq_boolP.
rewrite store.get_r0.
f_equal.
tauto.
+ case : Hret => Hret.
* apply/Zeq_boolP.
by rewrite (proj1 (proj2 Hret)) store.get_r0 !u2Z_Z2u.
* rewrite /= in u_z.
suff : False by done.
move/negP : u_z; apply.
apply ZIT.t_geb_true'.
rewrite /ZIT.t_ge /=.
omega.
Qed.
Lemma fwd_sim_b_gt_multi_lt : forall rk ru rv a3 flag a0 a1 ret ret2 z u d,
nodup(z, u) -> nodup(rk, ru, rv, a3, flag, ret, ret2, a0, a1, r0) ->
fwd_sim_b (state_mint (u |=> unsign rk ru \U+ (z |=> unsign rk rv \U+ d)))
(var_e z >> var_e u)%seplog_expr
(multi_lt rk ru rv a3 flag ret ret2 a0 a1)
(bne ret r0).
Proof.
move=> rk ru rv a3 flag a0 a1 ret ret2 z u d Hvars Hset.
apply fwd_sim_b_cond_neg with (var_e u >>= var_e z)%seplog_expr (beq ret r0).
move=> s st h s_st_h.
rewrite /= -ZIT.t_gt_t_ge.
by apply/negbRL.
by move=> st /=.
by apply fwd_sim_b_ge_multi_lt.
Qed.