Library multi_sub_signed_unsigned_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.
Import expr_m.
Require Import simu.
Import simu_m.
Require Import multi_sub_signed_unsigned_prg multi_sub_signed_unsigned_triple.
Local Open Scope machine_int_scope.
Local Open Scope mips_expr_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope assoc_scope.
Local Open Scope nodup_scope.
Local Open Scope heap_scope.
Require Import seq.
Lemma pfwd_sim_multi_sub_s_u : forall (A y : assoc.l) d
L rk rA ry a0 a1 a2 a3 a4 a5 X,
nodup(A, y) ->
nodup(rk, rA, ry, a0, a1, a2, a3, a4, a5, X, r0) ->
disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: X :: List.nil)%list ->
A \notin assoc.dom d -> y \notin assoc.dom d ->
signed L rA \notin assoc.cdom d -> unsign rk ry \notin assoc.cdom d ->
pfwd_sim
(state_mint (A |=> signed L rA \U+ (y |=> unsign rk ry \U+ d)))
(fun s st _ =>
[rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([A ]_ s)%seplog_expr < Zbeta L /\
0 <= ([y ]_ s)%seplog_expr < Zbeta L /\
Zabs (([A ]_ s)%seplog_expr - ([y ]_ s)%seplog_expr) < Zbeta L)
(A <- (var_e A .-e var_e y)%seplog_expr)%seplog_cmd
(multi_sub_s_u rk rA ry a0 a1 a2 a3 a4 a5 X).
Proof.
move=> A y d L rk rA ry a0 a1 a2 a3 a4 a5 X Hvars Hregs Hd A_d y_d rA_d rk_ry_d.
rewrite /pfwd_sim.
move=> s st h s_st_h [rk_st_neq0 [rk_st_max [L_rk [A_L [y_s A_y_s]]]]] s' exec_pseudo st' h' exec_asm.
have Hd_unchanged : forall v r, assoc.get v d = Some r ->
disj (mint_regs r) (mips_frame.modified_regs (multi_sub_s_u rk rA ry a0 a1 a2 a3 a4 a5 X)).
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 move/assoc.get_Some_in_cdom : Hvr.
set nk := Zabs_nat (u2Z ([rk ]_ st)).
set vA := [rA ]_st.
set vy := [ry ]_st.
lapply (state_mint_var_mint _ _ _ _ A (signed L rA) s_st_h); [move=> var_mint_A | by assoc_get_Some].
rewrite /var_mint /var_signed in var_mint_A.
case: var_mint_A => va_fit [slen [ptr [A0 [A0_nk [Hlen [Hsgn [HA [ptr_fit [Sum_A0 Hmem]]]]]]]]].
have Hhoare_multi_sub_s_u :
({{ fun st h => [rA]_st = vA /\ [ry]_st = vy /\ u2Z [rk]_st = Z_of_nat nk /\
((var_e rA |--> (slen :: ptr :: List.nil)%list ** int_e ptr |--> A0) **
var_e ry |--> Z2ints 32 nk ([y]_s)%seplog_expr) st h }}
multi_sub_s_u rk rA ry a0 a1 a2 a3 a4 a5 X
{{ fun st h => exists A', exists slen', length A' = nk /\ [rA]_st = vA /\ [ry]_st = vy /\
s2Z slen' = Zsgn (s2Z slen') * Z_of_nat nk /\
Zsgn (s2Z slen') = Zsgn (Zsgn (s2Z slen) * Sum nk A0 - Sum nk (Z2ints 32 nk ([y]_s)))%seplog_expr /\
(var_e rA |--> (slen' :: ptr :: List.nil)%list ** int_e ptr |--> A' ** var_e ry |--> Z2ints 32 nk ([y]_s)%seplog_expr) st h /\
u2Z ([a3]_ st) <= 1 /\
Zsgn (s2Z slen') * (Sum nk A' + u2Z ([a3]_ st) * Zbeta nk) =
Zsgn (s2Z slen) * Sum nk A0 - Sum nk (Z2ints 32 nk ([y]_s)%seplog_expr) }})%mips_assert%mips_hoare.
apply multi_sub_s_u_triple.
by Nodup_nodup r0.
contradict rk_st_neq0. move/Zabs_nat_0 in rk_st_neq0. apply u2Z_inj. by rewrite rk_st_neq0 u2Z_Z2u.
rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
rewrite /nk -L_rk; exact ptr_fit.
rewrite assoc_prop_m.swap_heads in s_st_h; last by done.
rewrite /nk ; by apply (state_mint_unsign_fit _ _ _ _ _ _ _ s_st_h).
by rewrite /nk -L_rk.
by rewrite len_Z2ints.
rewrite /nk -L_rk; exact Hlen.
case: (Z_zerop (s2Z slen)) => slen_neq0; first by rewrite slen_neq0.
by rewrite /nk -L_rk -Sum_A0.
have [st'' [h'' exec_asm_proj]] : exists st'', exists h'',
(Some (st, heap.proj h (heap.dom (heap_mint (unsign rk ry) st h +++ heap_mint (signed L rA) st h)))
-- multi_sub_s_u rk rA ry a0 a1 a2 a3 a4 a5 X --->
Some (st'', h''))%mips_cmd.
exists st', (heap.proj h' (heap.dom (heap_mint (unsign rk ry) st h +++ heap_mint (signed L rA) st h))).
apply (mips_syntax.triple_exec_proj _ _ _ Hhoare_multi_sub_s_u) => {Hhoare_multi_sub_s_u} //.
split; first by done.
split; first by done.
split.
rewrite /nk Z_of_nat_Zabs_nat //; by apply min_u2Z.
rewrite heap.proj_dom_union; last first.
apply (proj2 s_st_h y A); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
rewrite heap.union_com; last first.
apply heap.dis_disj_proj.
rewrite -heap.disjE.
apply (proj2 s_st_h y A); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
apply assert_m.con_cons.
apply heap.dis_disj_proj.
rewrite -heap.disjE.
apply (proj2 s_st_h A y); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
move: (heap_inclu_heap_mint_signed h st L rA).
move/heap.incluE => ->; exact Hmem.
have y_ry : var_mint y (unsign rk ry) s st (heap_mint (unsign rk ry) st h).
apply (state_mint_var_mint _ _ _ _ _ _ s_st_h); by assoc_get_Some.
case: (y_ry) => _ [] _ Hry.
rewrite /heap_mint /heap_cut in y_ry.
by rewrite /nk (var_mint_unsign_dom_heap_mint _ _ _ _ _ _ y_ry).
have ry_st_st' : [ry]_st = [ry]_st'.
mips_syntax.Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
have rk_st_st' : [rk ]_ st = [rk ]_ st'.
mips_syntax.Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
have y_s_s' : ([y ]_ s = [y ]_ s')%seplog_expr.
Var_unchanged. simpl syntax_m.seplog_m.modified_vars. by Nodup_not_In.
have rA_st_st' : [rA ]_ st = [rA ]_ st'.
mips_syntax.Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
rewrite /state_mint; split.
- move=> x rx x_rx.
have [x_d | x_A ] : x \in assoc.dom (y |=> unsign rk ry \U+ d) \/ x = A.
rewrite assoc.union_com in x_rx; last first.
apply assoc.disj_union_R.
apply assoc.disj_sing; by Nodup_neq.
by apply assoc.disj_sym, assoc.disj_sing_R.
case/assoc.get_union_Some_inv : x_rx => x_rx.
left.
by apply assoc.get_Some_in_dom with rx.
case/assoc.get_sing_inv : x_rx => ? ?; subst x rx.
by right.
+
have x_A : x <> A.
move=> ?; subst x.
case/assoc.in_dom_union_inv : x_d.
* case/assoc.in_dom_get_Some => z.
case/assoc.get_sing_inv => x_d _.
move: x_d.
rewrite -/(~ _); by Nodup_neq.
* by rewrite (negbTE A_d).
case/orP : (orbN (x == y)) => x_y.
move/eqP : x_y => ?; subst x.
rewrite assoc.union_com in x_rx; last first.
apply assoc.disj_union_R.
apply assoc.disj_sing; by auto.
by apply assoc.disj_sym, assoc.disj_sing_R.
rewrite -assoc.union_assoc assoc.get_union_sing_eq in x_rx.
case: x_rx => ?; subst rx.
move: {Hhoare_multi_sub_s_u}(mips_frame.frame_rule _ _ _ Hhoare_multi_sub_s_u assert_m.TT (assert_m.inde_TT _) (mips_frame.inde_cmd_mult_TT _)).
move/mips_seplog.hoare_prop_m.soundness.
Notation "'hoare_semantics'" := (@while.hoare_semantics WMIPS_Hoare.store WMIPS_Hoare.heap _
WMIPS_Hoare.exec0 _ WMIPS_Hoare.eval_b) : mips_hoare_scope.
rewrite /while.hoare_semantics.
Notation "s -- c ---> t" := (@while.exec WMIPS_Hoare.store WMIPS_Hoare.heap _ WMIPS_Hoare.exec0 _
WMIPS_Hoare.eval_b s c t) (at level 74, no associativity) : mips_cmd_scope.
move/(_ st h) => Hmulti_sub_s_u.
lapply Hmulti_sub_s_u; last first.
exists (heap_mint (signed L rA) st h +++ heap_mint (unsign rk ry) st h).
exists (h [\m] heap.dom (heap_mint (signed L rA) st h +++ heap_mint (unsign rk ry) st h)).
split.
by apply heap.disj_difs', seq_ext.inc_refl.
split.
apply heap.union_difs; last by done.
apply heap_prop_m.inclu_union; by [apply heap_inclu_heap_mint_signed | apply heap.inclu_proj].
split; last by done.
repeat (split=> //).
- rewrite /nk Z_of_nat_Zabs_nat //; by apply min_u2Z.
- apply assert_m.con_cons.
+ apply (proj2 s_st_h A y); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
+ exact Hmem.
+ move: (proj1 s_st_h y (unsign rk ry)).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
rewrite assoc.get_union_sing_eq.
case/(_ (refl_equal _))=> _ [] _; exact.
case=> _.
move/(_ _ _ exec_asm).
case=> h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh1 => A' [slen' Hh1].
decompose [and] Hh1; clear Hh1.
case: H4 => h11 [h12 [h11_d_h12 [h11_U_h12 [Hh11 Hh12]]]].
move: (proj1 s_st_h y (unsign rk ry)).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
rewrite assoc.get_union_sing_eq.
move/(_ (refl_equal _)).
have <- : heap_mint (unsign rk ry) st h = heap_mint (unsign rk ry) st' h'.
rewrite {2}/heap_mint /heap_cut h1_U_h2 h11_U_h12.
move/assert_m.mapstos_inv_dom : (Hh12) => Hh12'.
have : u2Z [var_e ry ]e_ st' +
4 * Z_of_nat (length (Z2ints 32 nk ([y ]_ s)%seplog_expr)) < Zbeta 1.
simpl u2Z.
rewrite len_Z2ints -ry_st_st'.
move: (proj1 s_st_h y (unsign rk ry)).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
rewrite assoc.get_union_sing_eq /nk.
by case/(_ (refl_equal _)).
move/Hh12' => {Hh12'}Hh12'.
rewrite len_Z2ints /nk rk_st_st' in Hh12'.
rewrite {}Hh12' seq_ext.l2s2l.
rewrite heap.proj_union_L; last by heap_tac_m.Disj.
rewrite heap.proj_union_R; last by heap_tac_m.Disj.
move: (proj1 s_st_h y (unsign rk ry)).
rewrite assoc.get_union_sing_neq; last by auto.
rewrite assoc.get_union_sing_eq.
move/(_ (refl_equal _)).
case=> X1 [X2 X3].
apply assert_m.mapstos_inv in Hh12.
apply assert_m.mapstos_inv in X3.
apply heap.dom_cdom_heap.
apply seq_ext.s2l_inj.
case: X3 => -> ?.
case: Hh12 => -> ? /=.
by rewrite -ry_st_st' /nk.
apply seq_ext.s2l_inj.
case: X3 => _ ->.
by case: Hh12 => _ ->.
by rewrite len_Z2ints.
by rewrite len_Z2ints /nk [u2Z _]/= -ry_st_st'.
apply var_mint_invariant_unsign; [exact ry_st_st' | exact rk_st_st' | exact y_s_s'].
move: {s_st_h}(proj1 s_st_h _ _ x_rx) (proj2 s_st_h) => s_st_h1 s_st_h2.
have x_unchanged : ( [ x ]_s = [ x ]_s' )%seplog_expr.
Var_unchanged. simpl. contradict x_A. by case: x_A.
case: (mips_syntax.exec_deter_proj _ _ _ _ _ exec_asm
(heap.dom (heap_mint (unsign rk ry) st h +++ heap_mint (signed L rA) st h)) _ _
exec_asm_proj) => H4 [H5 H_h_h'].
have <- : heap_mint rx st h = heap_mint rx st' h'.
apply heap_mint_unchanged2 with (d := heap_mint (unsign rk ry) st h +++
heap_mint (signed L rA) st h) (x := x) (s := s) => //.
move=> rx0 Hrx0; mips_syntax.Reg_unchanged.
apply (disj_not_In _ (mint_regs rx)); last done.
apply disj_sym, (Hd_unchanged x).
rewrite assoc.get_union_sing_neq in x_rx; last by done.
rewrite assoc.get_union_sing_neq // in x_rx.
by apply/eqP.
apply heap.disj_union_R.
apply s_st_h2 with x y => //.
by apply/eqP.
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
by rewrite assoc.get_union_sing_eq.
apply s_st_h2 with x A => //.
by rewrite assoc.get_union_sing_eq.
move: s_st_h1; apply var_mint_invariant; last by exact x_unchanged.
move=> rx0 Hrx0; mips_syntax.Reg_unchanged.
apply (disj_not_In _ (mint_regs rx)); last by done.
apply disj_sym, (Hd_unchanged x) => //.
rewrite assoc.get_union_sing_neq in x_rx; last by done.
rewrite assoc.get_union_sing_neq // in x_rx.
by apply/eqP.
+ subst x.
have rx_rA : rx = signed L rA.
rewrite assoc.get_union_sing_eq in x_rx; by case: x_rx.
subst rx.
move: (proj1 s_st_h A (signed L rA) x_rx).
rewrite /var_mint.
move: {Hhoare_multi_sub_s_u}(mips_frame.frame_rule _ _ _ Hhoare_multi_sub_s_u 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) => Hmulti_add_s_u.
lapply Hmulti_add_s_u; last first.
exists (heap_mint (signed L rA) st h +++ heap_mint (unsign rk ry) st h).
exists (h [\m]heap.dom (heap_mint (signed L rA) st h +++ heap_mint (unsign rk ry) st h)).
split.
by apply heap.disj_difs', seq_ext.inc_refl.
split.
apply heap.union_difs; last by done.
apply heap_prop_m.inclu_union; by [apply heap_inclu_heap_mint_signed | apply heap.inclu_proj].
split; last by done.
repeat (split=> //).
rewrite /nk Z_of_nat_Zabs_nat //; by apply min_u2Z.
apply assert_m.con_cons.
+ apply (proj2 s_st_h A y); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
+ exact Hmem.
+ move: (proj1 s_st_h y (unsign rk ry)).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
rewrite assoc.get_union_sing_eq.
case/(_ (refl_equal _))=> _ [] _; exact.
move=> {Hmulti_add_s_u} [_ Hmulti_add_s_u'].
move: {Hmulti_add_s_u'}(Hmulti_add_s_u' _ _ exec_asm).
move=> [h1 [h2 [Hdisj [Hunion [[A' [slen' [Hsub_s_us_1 [r_A [r_B [Hsub_s_us_2 [Hsub_s_us_3 [Hsub_s_us_4 [Hsub_s_us_5 Hsub_s_us_6]]]]]]]]]] HTT]]]].
split.
+ by rewrite /vA -rA_st_st'.
+ simpl.
have -> : heap.get (Zabs_nat (u2Z ([rA ]_ st')%mips_expr / 4)) h' = Some slen'.
rewrite Hunion; apply heap.get_union_L => //.
rewrite assert_m.con_assoc_equiv in Hsub_s_us_4.
by apply assert_m.mapstos_get1 in Hsub_s_us_4.
have -> : heap.get (Zabs_nat (u2Z ([rA ]_ st' [.+] four32) / 4)) h' = Some ptr.
rewrite Hunion; apply heap.get_union_L => //.
rewrite assert_m.con_assoc_equiv in Hsub_s_us_4.
by apply assert_m.mapstos_get2 in Hsub_s_us_4.
rewrite /var_signed.
exists slen', ptr, A'.
split.
rewrite L_rk; exact Hsub_s_us_1.
split.
rewrite L_rk; exact Hsub_s_us_2.
have A'_A_y : ([A ]_ s' = [A ]_ s - [y ]_ s )%seplog_expr.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ -> /=.
by syntax_m.seplog_m.assert_m.expr_m.Store_upd.
split.
rewrite !Sum_Z2ints_pos in Hsub_s_us_6 Hsub_s_us_3; last first.
by rewrite L_rk in y_s.
by rewrite Hsub_s_us_3 /nk -L_rk -Sum_A0 A'_A_y.
split.
rewrite A'_A_y; exact A_y_s.
split.
exact ptr_fit.
split.
rewrite !Sum_Z2ints_pos in Hsub_s_us_6 Hsub_s_us_3; last first.
by rewrite L_rk in y_s.
rewrite /nk -L_rk -Sum_A0 -A'_A_y in Hsub_s_us_6.
case: (Z_zerop (s2Z slen')) => slen'_neq0.
rewrite -Hsub_s_us_6 slen'_neq0 /=; ring.
have Hi : u2Z [a3 ]_ st' = 0.
have : Zabs (Zsgn (s2Z slen') * (Sum L A' + u2Z [a3 ]_ st' * Zbeta L)) < Zbeta L.
by rewrite Hsub_s_us_6 A'_A_y.
rewrite Zabs_Zmult Zabs_Zsgn_1 // Zmult_1_l Zplus_comm.
apply: poly_Zlt1_inv_new.
by apply min_Sum.
by apply min_u2Z.
by apply Zbeta_0'.
by rewrite Hi Zmult_0_l Zplus_0_r in Hsub_s_us_6.
case: Hsub_s_us_4 => h11 [h12 [h11_d_h12 [h11_U_h12 [Hh11 Hh12]]]].
set hh := _ +++ _.
suff : hh = h11 by move=> ->.
rewrite /hh.
case: Hh11 => h111 [h112 [h111_d_h112 [h111_U_h112 [Hh111 Hh112]]]].
rewrite /heap_cut.
apply assert_m.mapstos_inv_dom in Hh111; last first.
rewrite [length _]/= [u2Z _]/= -rA_st_st'; exact va_fit.
rewrite Hh111 seq_ext.l2s2l.
apply assert_m.mapstos_inv_dom in Hh112; last first.
by rewrite Hsub_s_us_1 /nk -L_rk.
rewrite Hsub_s_us_1 in Hh112.
rewrite L_rk Hh112 seq_ext.l2s2l /hh /heap_cut Hunion h11_U_h12 h111_U_h112.
rewrite heap.proj_union_L; last by heap_tac_m.Disj.
rewrite heap.proj_union_L; last by heap_tac_m.Disj.
rewrite heap.proj_union_L; last by exact h111_d_h112.
rewrite heap.proj_itself.
rewrite heap.proj_union_L; last by heap_tac_m.Disj.
rewrite heap.proj_union_L; last by heap_tac_m.Disj.
by rewrite heap.proj_union_R.
- move: {Hhoare_multi_sub_s_u}(mips_frame.frame_rule _ _ _ Hhoare_multi_sub_s_u 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) => Hmulti_sub_s_u.
lapply Hmulti_sub_s_u; last first.
exists (heap_mint (signed L rA) st h +++ heap_mint (unsign rk ry) st h).
exists (h [\m] heap.dom (heap_mint (signed L rA) st h +++ heap_mint (unsign rk ry) st h)).
split.
by apply heap.disj_difs', seq_ext.inc_refl.
split.
apply heap.union_difs; last by done.
apply heap_prop_m.inclu_union; by [apply heap_inclu_heap_mint_signed | apply heap.inclu_proj].
split; last by done.
repeat (split=> //).
- rewrite /nk Z_of_nat_Zabs_nat //; by apply min_u2Z.
- apply assert_m.con_cons.
+ apply (proj2 s_st_h A y); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
+ exact Hmem.
+ move: (proj1 s_st_h y (unsign rk ry)).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
rewrite assoc.get_union_sing_eq.
case/(_ (refl_equal _))=> _ [] _; exact.
move=> {Hmulti_sub_s_u} [_ Hmulti_sub_s_u'].
move: {Hmulti_sub_s_u'}(Hmulti_sub_s_u' _ _ exec_asm).
move=> [h1 [h2 [Hdisj [Hunion [[A' [slen' [Hsub_s_us_1 [r_A [r_y [Hsub_s_us_2 [Hsub_s_us_3 [Hsub_s_us_4 [Hsub_s_us_5 Hsub_s_us_6]]]]]]]]]] HTT]]]].
have Hslen' : heap.get (Zabs_nat (u2Z ([rA ]_ st')%mips_expr / 4)) h' = Some slen'.
rewrite Hunion.
apply heap.get_union_L => //.
rewrite assert_m.con_assoc_equiv in Hsub_s_us_4.
by apply assert_m.mapstos_get1 in Hsub_s_us_4.
have Hptr : heap.get (Zabs_nat (u2Z ([rA ]_ st' [.+] four32 )%mips_expr / 4)) h' = Some ptr.
rewrite Hunion.
apply heap.get_union_L => //.
rewrite assert_m.con_assoc_equiv in Hsub_s_us_4.
by apply assert_m.mapstos_get2 in Hsub_s_us_4.
apply state_mint_part2_two_variables with s st h => //.
+ move/assert_m.mapstos_get2 : (Hmem).
move/heap_get_heap_mint_inv => ptr_vA4.
move/assert_m.mapstos_get1 : (Hmem).
move/heap_get_heap_mint_inv => slen_vA.
symmetry.
apply dom_heap_mint_sign_unchanged2 with A s slen slen'.
exact rA_st_st'.
exact slen_vA.
exact Hslen'.
by rewrite Hptr.
rewrite assoc_prop_m.swap_heads in s_st_h; last by done.
apply (state_mint_var_mint _ _ _ _ _ _ s_st_h).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
by rewrite assoc.get_union_sing_eq.
by apply (mips_syntax.dom_heap_invariant _ _ _ _ _ exec_asm).
+ symmetry.
apply dom_heap_mint_unsign_unchanged2 with y s.
exact rk_st_st'.
exact ry_st_st'.
apply (state_mint_var_mint _ _ _ _ _ _ s_st_h).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
by rewrite assoc.get_union_sing_eq.
by apply (mips_syntax.dom_heap_invariant _ _ _ _ _ exec_asm).
+ move=> t Ht x0 Hx0.
mips_syntax.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 (signed L rA))); last by rewrite /=; auto.
Disj_remove_dup.
simpl.
apply nodup_disj.
simpl app.
by Nodup_nodup r0.
* 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 ry))); 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.
+ by Nodup_neq.
+ move: (mips_syntax.exec_deter_proj _ _ _ _ _ exec_asm _ _ _ exec_asm_proj); tauto.
Qed.
Lemma pfwd_sim_multi_sub_s_u_wo_overflow : forall (A y : assoc.l) d
L rk ry rA a0 a1 a2 a3 a4 a5 X,
nodup(A, y) ->
nodup(rk, rA, ry, a0, a1, a2, a3, a4, a5, X, r0) ->
disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: X :: List.nil)%list ->
A \notin assoc.dom d -> y \notin assoc.dom d ->
signed L rA \notin assoc.cdom d -> unsign rk ry \notin assoc.cdom d ->
pfwd_sim (state_mint (A |=> signed L rA \U+ (y |=> unsign rk ry \U+ d)))
(fun s st _ => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([A ]_ s)%seplog_expr < Zbeta (L - 1) /\
0 <= ([y ]_ s)%seplog_expr < Zbeta (L - 1))
(A <- (var_e A .-e var_e y)%seplog_expr)%seplog_cmd
(multi_sub_s_u rk rA ry a0 a1 a2 a3 a4 a5 X).
Proof.
move=> A y d L rk rA ry a0 a1 a2 a3 a4 a5 X Hvars Hregs Hd A_d y_d rA_d rk_ry_d.
eapply pfwd_sim_stren; last by apply pfwd_sim_multi_sub_s_u.
move=> s st h [rk_neq0 [rk_max [L_neq0 [L_rk [A_max y_bounds]]]]].
split; first by assumption.
split; first by assumption.
split; first by assumption.
split.
eapply Zlt_trans; first by apply A_max.
apply Zbeta_lt; omega.
split.
split; first by tauto.
eapply Zlt_trans; first by apply (proj2 y_bounds).
apply Zbeta_lt; omega.
eapply Zle_lt_trans; first by apply Zabs_triangle.
rewrite Zabs_Zopp.
rewrite (Zabs_eq ([y ]_ s)%seplog_expr); last by omega.
eapply Zlt_trans.
apply Zplus_lt_compat.
by apply A_max.
by apply (proj2 y_bounds).
rewrite /Zbeta Zpower_plus.
apply Zpower_2_lt; omega.
Qed.
Require Import ZArith_ext Lists_ext.
Require Import machine_int nodup multi_int.
Import MachineInt.
Require Import mips_bipl mips_seplog.
Import expr_m.
Require Import simu.
Import simu_m.
Require Import multi_sub_signed_unsigned_prg multi_sub_signed_unsigned_triple.
Local Open Scope machine_int_scope.
Local Open Scope mips_expr_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope assoc_scope.
Local Open Scope nodup_scope.
Local Open Scope heap_scope.
Require Import seq.
Lemma pfwd_sim_multi_sub_s_u : forall (A y : assoc.l) d
L rk rA ry a0 a1 a2 a3 a4 a5 X,
nodup(A, y) ->
nodup(rk, rA, ry, a0, a1, a2, a3, a4, a5, X, r0) ->
disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: X :: List.nil)%list ->
A \notin assoc.dom d -> y \notin assoc.dom d ->
signed L rA \notin assoc.cdom d -> unsign rk ry \notin assoc.cdom d ->
pfwd_sim
(state_mint (A |=> signed L rA \U+ (y |=> unsign rk ry \U+ d)))
(fun s st _ =>
[rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([A ]_ s)%seplog_expr < Zbeta L /\
0 <= ([y ]_ s)%seplog_expr < Zbeta L /\
Zabs (([A ]_ s)%seplog_expr - ([y ]_ s)%seplog_expr) < Zbeta L)
(A <- (var_e A .-e var_e y)%seplog_expr)%seplog_cmd
(multi_sub_s_u rk rA ry a0 a1 a2 a3 a4 a5 X).
Proof.
move=> A y d L rk rA ry a0 a1 a2 a3 a4 a5 X Hvars Hregs Hd A_d y_d rA_d rk_ry_d.
rewrite /pfwd_sim.
move=> s st h s_st_h [rk_st_neq0 [rk_st_max [L_rk [A_L [y_s A_y_s]]]]] s' exec_pseudo st' h' exec_asm.
have Hd_unchanged : forall v r, assoc.get v d = Some r ->
disj (mint_regs r) (mips_frame.modified_regs (multi_sub_s_u rk rA ry a0 a1 a2 a3 a4 a5 X)).
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 move/assoc.get_Some_in_cdom : Hvr.
set nk := Zabs_nat (u2Z ([rk ]_ st)).
set vA := [rA ]_st.
set vy := [ry ]_st.
lapply (state_mint_var_mint _ _ _ _ A (signed L rA) s_st_h); [move=> var_mint_A | by assoc_get_Some].
rewrite /var_mint /var_signed in var_mint_A.
case: var_mint_A => va_fit [slen [ptr [A0 [A0_nk [Hlen [Hsgn [HA [ptr_fit [Sum_A0 Hmem]]]]]]]]].
have Hhoare_multi_sub_s_u :
({{ fun st h => [rA]_st = vA /\ [ry]_st = vy /\ u2Z [rk]_st = Z_of_nat nk /\
((var_e rA |--> (slen :: ptr :: List.nil)%list ** int_e ptr |--> A0) **
var_e ry |--> Z2ints 32 nk ([y]_s)%seplog_expr) st h }}
multi_sub_s_u rk rA ry a0 a1 a2 a3 a4 a5 X
{{ fun st h => exists A', exists slen', length A' = nk /\ [rA]_st = vA /\ [ry]_st = vy /\
s2Z slen' = Zsgn (s2Z slen') * Z_of_nat nk /\
Zsgn (s2Z slen') = Zsgn (Zsgn (s2Z slen) * Sum nk A0 - Sum nk (Z2ints 32 nk ([y]_s)))%seplog_expr /\
(var_e rA |--> (slen' :: ptr :: List.nil)%list ** int_e ptr |--> A' ** var_e ry |--> Z2ints 32 nk ([y]_s)%seplog_expr) st h /\
u2Z ([a3]_ st) <= 1 /\
Zsgn (s2Z slen') * (Sum nk A' + u2Z ([a3]_ st) * Zbeta nk) =
Zsgn (s2Z slen) * Sum nk A0 - Sum nk (Z2ints 32 nk ([y]_s)%seplog_expr) }})%mips_assert%mips_hoare.
apply multi_sub_s_u_triple.
by Nodup_nodup r0.
contradict rk_st_neq0. move/Zabs_nat_0 in rk_st_neq0. apply u2Z_inj. by rewrite rk_st_neq0 u2Z_Z2u.
rewrite Z_of_nat_Zabs_nat //; by apply min_u2Z.
rewrite /nk -L_rk; exact ptr_fit.
rewrite assoc_prop_m.swap_heads in s_st_h; last by done.
rewrite /nk ; by apply (state_mint_unsign_fit _ _ _ _ _ _ _ s_st_h).
by rewrite /nk -L_rk.
by rewrite len_Z2ints.
rewrite /nk -L_rk; exact Hlen.
case: (Z_zerop (s2Z slen)) => slen_neq0; first by rewrite slen_neq0.
by rewrite /nk -L_rk -Sum_A0.
have [st'' [h'' exec_asm_proj]] : exists st'', exists h'',
(Some (st, heap.proj h (heap.dom (heap_mint (unsign rk ry) st h +++ heap_mint (signed L rA) st h)))
-- multi_sub_s_u rk rA ry a0 a1 a2 a3 a4 a5 X --->
Some (st'', h''))%mips_cmd.
exists st', (heap.proj h' (heap.dom (heap_mint (unsign rk ry) st h +++ heap_mint (signed L rA) st h))).
apply (mips_syntax.triple_exec_proj _ _ _ Hhoare_multi_sub_s_u) => {Hhoare_multi_sub_s_u} //.
split; first by done.
split; first by done.
split.
rewrite /nk Z_of_nat_Zabs_nat //; by apply min_u2Z.
rewrite heap.proj_dom_union; last first.
apply (proj2 s_st_h y A); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
rewrite heap.union_com; last first.
apply heap.dis_disj_proj.
rewrite -heap.disjE.
apply (proj2 s_st_h y A); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
apply assert_m.con_cons.
apply heap.dis_disj_proj.
rewrite -heap.disjE.
apply (proj2 s_st_h A y); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
move: (heap_inclu_heap_mint_signed h st L rA).
move/heap.incluE => ->; exact Hmem.
have y_ry : var_mint y (unsign rk ry) s st (heap_mint (unsign rk ry) st h).
apply (state_mint_var_mint _ _ _ _ _ _ s_st_h); by assoc_get_Some.
case: (y_ry) => _ [] _ Hry.
rewrite /heap_mint /heap_cut in y_ry.
by rewrite /nk (var_mint_unsign_dom_heap_mint _ _ _ _ _ _ y_ry).
have ry_st_st' : [ry]_st = [ry]_st'.
mips_syntax.Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
have rk_st_st' : [rk ]_ st = [rk ]_ st'.
mips_syntax.Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
have y_s_s' : ([y ]_ s = [y ]_ s')%seplog_expr.
Var_unchanged. simpl syntax_m.seplog_m.modified_vars. by Nodup_not_In.
have rA_st_st' : [rA ]_ st = [rA ]_ st'.
mips_syntax.Reg_unchanged. simpl mips_frame.modified_regs. by Nodup_not_In.
rewrite /state_mint; split.
- move=> x rx x_rx.
have [x_d | x_A ] : x \in assoc.dom (y |=> unsign rk ry \U+ d) \/ x = A.
rewrite assoc.union_com in x_rx; last first.
apply assoc.disj_union_R.
apply assoc.disj_sing; by Nodup_neq.
by apply assoc.disj_sym, assoc.disj_sing_R.
case/assoc.get_union_Some_inv : x_rx => x_rx.
left.
by apply assoc.get_Some_in_dom with rx.
case/assoc.get_sing_inv : x_rx => ? ?; subst x rx.
by right.
+
have x_A : x <> A.
move=> ?; subst x.
case/assoc.in_dom_union_inv : x_d.
* case/assoc.in_dom_get_Some => z.
case/assoc.get_sing_inv => x_d _.
move: x_d.
rewrite -/(~ _); by Nodup_neq.
* by rewrite (negbTE A_d).
case/orP : (orbN (x == y)) => x_y.
move/eqP : x_y => ?; subst x.
rewrite assoc.union_com in x_rx; last first.
apply assoc.disj_union_R.
apply assoc.disj_sing; by auto.
by apply assoc.disj_sym, assoc.disj_sing_R.
rewrite -assoc.union_assoc assoc.get_union_sing_eq in x_rx.
case: x_rx => ?; subst rx.
move: {Hhoare_multi_sub_s_u}(mips_frame.frame_rule _ _ _ Hhoare_multi_sub_s_u assert_m.TT (assert_m.inde_TT _) (mips_frame.inde_cmd_mult_TT _)).
move/mips_seplog.hoare_prop_m.soundness.
Notation "'hoare_semantics'" := (@while.hoare_semantics WMIPS_Hoare.store WMIPS_Hoare.heap _
WMIPS_Hoare.exec0 _ WMIPS_Hoare.eval_b) : mips_hoare_scope.
rewrite /while.hoare_semantics.
Notation "s -- c ---> t" := (@while.exec WMIPS_Hoare.store WMIPS_Hoare.heap _ WMIPS_Hoare.exec0 _
WMIPS_Hoare.eval_b s c t) (at level 74, no associativity) : mips_cmd_scope.
move/(_ st h) => Hmulti_sub_s_u.
lapply Hmulti_sub_s_u; last first.
exists (heap_mint (signed L rA) st h +++ heap_mint (unsign rk ry) st h).
exists (h [\m] heap.dom (heap_mint (signed L rA) st h +++ heap_mint (unsign rk ry) st h)).
split.
by apply heap.disj_difs', seq_ext.inc_refl.
split.
apply heap.union_difs; last by done.
apply heap_prop_m.inclu_union; by [apply heap_inclu_heap_mint_signed | apply heap.inclu_proj].
split; last by done.
repeat (split=> //).
- rewrite /nk Z_of_nat_Zabs_nat //; by apply min_u2Z.
- apply assert_m.con_cons.
+ apply (proj2 s_st_h A y); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
+ exact Hmem.
+ move: (proj1 s_st_h y (unsign rk ry)).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
rewrite assoc.get_union_sing_eq.
case/(_ (refl_equal _))=> _ [] _; exact.
case=> _.
move/(_ _ _ exec_asm).
case=> h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh1 => A' [slen' Hh1].
decompose [and] Hh1; clear Hh1.
case: H4 => h11 [h12 [h11_d_h12 [h11_U_h12 [Hh11 Hh12]]]].
move: (proj1 s_st_h y (unsign rk ry)).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
rewrite assoc.get_union_sing_eq.
move/(_ (refl_equal _)).
have <- : heap_mint (unsign rk ry) st h = heap_mint (unsign rk ry) st' h'.
rewrite {2}/heap_mint /heap_cut h1_U_h2 h11_U_h12.
move/assert_m.mapstos_inv_dom : (Hh12) => Hh12'.
have : u2Z [var_e ry ]e_ st' +
4 * Z_of_nat (length (Z2ints 32 nk ([y ]_ s)%seplog_expr)) < Zbeta 1.
simpl u2Z.
rewrite len_Z2ints -ry_st_st'.
move: (proj1 s_st_h y (unsign rk ry)).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
rewrite assoc.get_union_sing_eq /nk.
by case/(_ (refl_equal _)).
move/Hh12' => {Hh12'}Hh12'.
rewrite len_Z2ints /nk rk_st_st' in Hh12'.
rewrite {}Hh12' seq_ext.l2s2l.
rewrite heap.proj_union_L; last by heap_tac_m.Disj.
rewrite heap.proj_union_R; last by heap_tac_m.Disj.
move: (proj1 s_st_h y (unsign rk ry)).
rewrite assoc.get_union_sing_neq; last by auto.
rewrite assoc.get_union_sing_eq.
move/(_ (refl_equal _)).
case=> X1 [X2 X3].
apply assert_m.mapstos_inv in Hh12.
apply assert_m.mapstos_inv in X3.
apply heap.dom_cdom_heap.
apply seq_ext.s2l_inj.
case: X3 => -> ?.
case: Hh12 => -> ? /=.
by rewrite -ry_st_st' /nk.
apply seq_ext.s2l_inj.
case: X3 => _ ->.
by case: Hh12 => _ ->.
by rewrite len_Z2ints.
by rewrite len_Z2ints /nk [u2Z _]/= -ry_st_st'.
apply var_mint_invariant_unsign; [exact ry_st_st' | exact rk_st_st' | exact y_s_s'].
move: {s_st_h}(proj1 s_st_h _ _ x_rx) (proj2 s_st_h) => s_st_h1 s_st_h2.
have x_unchanged : ( [ x ]_s = [ x ]_s' )%seplog_expr.
Var_unchanged. simpl. contradict x_A. by case: x_A.
case: (mips_syntax.exec_deter_proj _ _ _ _ _ exec_asm
(heap.dom (heap_mint (unsign rk ry) st h +++ heap_mint (signed L rA) st h)) _ _
exec_asm_proj) => H4 [H5 H_h_h'].
have <- : heap_mint rx st h = heap_mint rx st' h'.
apply heap_mint_unchanged2 with (d := heap_mint (unsign rk ry) st h +++
heap_mint (signed L rA) st h) (x := x) (s := s) => //.
move=> rx0 Hrx0; mips_syntax.Reg_unchanged.
apply (disj_not_In _ (mint_regs rx)); last done.
apply disj_sym, (Hd_unchanged x).
rewrite assoc.get_union_sing_neq in x_rx; last by done.
rewrite assoc.get_union_sing_neq // in x_rx.
by apply/eqP.
apply heap.disj_union_R.
apply s_st_h2 with x y => //.
by apply/eqP.
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
by rewrite assoc.get_union_sing_eq.
apply s_st_h2 with x A => //.
by rewrite assoc.get_union_sing_eq.
move: s_st_h1; apply var_mint_invariant; last by exact x_unchanged.
move=> rx0 Hrx0; mips_syntax.Reg_unchanged.
apply (disj_not_In _ (mint_regs rx)); last by done.
apply disj_sym, (Hd_unchanged x) => //.
rewrite assoc.get_union_sing_neq in x_rx; last by done.
rewrite assoc.get_union_sing_neq // in x_rx.
by apply/eqP.
+ subst x.
have rx_rA : rx = signed L rA.
rewrite assoc.get_union_sing_eq in x_rx; by case: x_rx.
subst rx.
move: (proj1 s_st_h A (signed L rA) x_rx).
rewrite /var_mint.
move: {Hhoare_multi_sub_s_u}(mips_frame.frame_rule _ _ _ Hhoare_multi_sub_s_u 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) => Hmulti_add_s_u.
lapply Hmulti_add_s_u; last first.
exists (heap_mint (signed L rA) st h +++ heap_mint (unsign rk ry) st h).
exists (h [\m]heap.dom (heap_mint (signed L rA) st h +++ heap_mint (unsign rk ry) st h)).
split.
by apply heap.disj_difs', seq_ext.inc_refl.
split.
apply heap.union_difs; last by done.
apply heap_prop_m.inclu_union; by [apply heap_inclu_heap_mint_signed | apply heap.inclu_proj].
split; last by done.
repeat (split=> //).
rewrite /nk Z_of_nat_Zabs_nat //; by apply min_u2Z.
apply assert_m.con_cons.
+ apply (proj2 s_st_h A y); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
+ exact Hmem.
+ move: (proj1 s_st_h y (unsign rk ry)).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
rewrite assoc.get_union_sing_eq.
case/(_ (refl_equal _))=> _ [] _; exact.
move=> {Hmulti_add_s_u} [_ Hmulti_add_s_u'].
move: {Hmulti_add_s_u'}(Hmulti_add_s_u' _ _ exec_asm).
move=> [h1 [h2 [Hdisj [Hunion [[A' [slen' [Hsub_s_us_1 [r_A [r_B [Hsub_s_us_2 [Hsub_s_us_3 [Hsub_s_us_4 [Hsub_s_us_5 Hsub_s_us_6]]]]]]]]]] HTT]]]].
split.
+ by rewrite /vA -rA_st_st'.
+ simpl.
have -> : heap.get (Zabs_nat (u2Z ([rA ]_ st')%mips_expr / 4)) h' = Some slen'.
rewrite Hunion; apply heap.get_union_L => //.
rewrite assert_m.con_assoc_equiv in Hsub_s_us_4.
by apply assert_m.mapstos_get1 in Hsub_s_us_4.
have -> : heap.get (Zabs_nat (u2Z ([rA ]_ st' [.+] four32) / 4)) h' = Some ptr.
rewrite Hunion; apply heap.get_union_L => //.
rewrite assert_m.con_assoc_equiv in Hsub_s_us_4.
by apply assert_m.mapstos_get2 in Hsub_s_us_4.
rewrite /var_signed.
exists slen', ptr, A'.
split.
rewrite L_rk; exact Hsub_s_us_1.
split.
rewrite L_rk; exact Hsub_s_us_2.
have A'_A_y : ([A ]_ s' = [A ]_ s - [y ]_ s )%seplog_expr.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ -> /=.
by syntax_m.seplog_m.assert_m.expr_m.Store_upd.
split.
rewrite !Sum_Z2ints_pos in Hsub_s_us_6 Hsub_s_us_3; last first.
by rewrite L_rk in y_s.
by rewrite Hsub_s_us_3 /nk -L_rk -Sum_A0 A'_A_y.
split.
rewrite A'_A_y; exact A_y_s.
split.
exact ptr_fit.
split.
rewrite !Sum_Z2ints_pos in Hsub_s_us_6 Hsub_s_us_3; last first.
by rewrite L_rk in y_s.
rewrite /nk -L_rk -Sum_A0 -A'_A_y in Hsub_s_us_6.
case: (Z_zerop (s2Z slen')) => slen'_neq0.
rewrite -Hsub_s_us_6 slen'_neq0 /=; ring.
have Hi : u2Z [a3 ]_ st' = 0.
have : Zabs (Zsgn (s2Z slen') * (Sum L A' + u2Z [a3 ]_ st' * Zbeta L)) < Zbeta L.
by rewrite Hsub_s_us_6 A'_A_y.
rewrite Zabs_Zmult Zabs_Zsgn_1 // Zmult_1_l Zplus_comm.
apply: poly_Zlt1_inv_new.
by apply min_Sum.
by apply min_u2Z.
by apply Zbeta_0'.
by rewrite Hi Zmult_0_l Zplus_0_r in Hsub_s_us_6.
case: Hsub_s_us_4 => h11 [h12 [h11_d_h12 [h11_U_h12 [Hh11 Hh12]]]].
set hh := _ +++ _.
suff : hh = h11 by move=> ->.
rewrite /hh.
case: Hh11 => h111 [h112 [h111_d_h112 [h111_U_h112 [Hh111 Hh112]]]].
rewrite /heap_cut.
apply assert_m.mapstos_inv_dom in Hh111; last first.
rewrite [length _]/= [u2Z _]/= -rA_st_st'; exact va_fit.
rewrite Hh111 seq_ext.l2s2l.
apply assert_m.mapstos_inv_dom in Hh112; last first.
by rewrite Hsub_s_us_1 /nk -L_rk.
rewrite Hsub_s_us_1 in Hh112.
rewrite L_rk Hh112 seq_ext.l2s2l /hh /heap_cut Hunion h11_U_h12 h111_U_h112.
rewrite heap.proj_union_L; last by heap_tac_m.Disj.
rewrite heap.proj_union_L; last by heap_tac_m.Disj.
rewrite heap.proj_union_L; last by exact h111_d_h112.
rewrite heap.proj_itself.
rewrite heap.proj_union_L; last by heap_tac_m.Disj.
rewrite heap.proj_union_L; last by heap_tac_m.Disj.
by rewrite heap.proj_union_R.
- move: {Hhoare_multi_sub_s_u}(mips_frame.frame_rule _ _ _ Hhoare_multi_sub_s_u 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) => Hmulti_sub_s_u.
lapply Hmulti_sub_s_u; last first.
exists (heap_mint (signed L rA) st h +++ heap_mint (unsign rk ry) st h).
exists (h [\m] heap.dom (heap_mint (signed L rA) st h +++ heap_mint (unsign rk ry) st h)).
split.
by apply heap.disj_difs', seq_ext.inc_refl.
split.
apply heap.union_difs; last by done.
apply heap_prop_m.inclu_union; by [apply heap_inclu_heap_mint_signed | apply heap.inclu_proj].
split; last by done.
repeat (split=> //).
- rewrite /nk Z_of_nat_Zabs_nat //; by apply min_u2Z.
- apply assert_m.con_cons.
+ apply (proj2 s_st_h A y); by [Nodup_neq | assoc_get_Some | assoc_get_Some].
+ exact Hmem.
+ move: (proj1 s_st_h y (unsign rk ry)).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
rewrite assoc.get_union_sing_eq.
case/(_ (refl_equal _))=> _ [] _; exact.
move=> {Hmulti_sub_s_u} [_ Hmulti_sub_s_u'].
move: {Hmulti_sub_s_u'}(Hmulti_sub_s_u' _ _ exec_asm).
move=> [h1 [h2 [Hdisj [Hunion [[A' [slen' [Hsub_s_us_1 [r_A [r_y [Hsub_s_us_2 [Hsub_s_us_3 [Hsub_s_us_4 [Hsub_s_us_5 Hsub_s_us_6]]]]]]]]]] HTT]]]].
have Hslen' : heap.get (Zabs_nat (u2Z ([rA ]_ st')%mips_expr / 4)) h' = Some slen'.
rewrite Hunion.
apply heap.get_union_L => //.
rewrite assert_m.con_assoc_equiv in Hsub_s_us_4.
by apply assert_m.mapstos_get1 in Hsub_s_us_4.
have Hptr : heap.get (Zabs_nat (u2Z ([rA ]_ st' [.+] four32 )%mips_expr / 4)) h' = Some ptr.
rewrite Hunion.
apply heap.get_union_L => //.
rewrite assert_m.con_assoc_equiv in Hsub_s_us_4.
by apply assert_m.mapstos_get2 in Hsub_s_us_4.
apply state_mint_part2_two_variables with s st h => //.
+ move/assert_m.mapstos_get2 : (Hmem).
move/heap_get_heap_mint_inv => ptr_vA4.
move/assert_m.mapstos_get1 : (Hmem).
move/heap_get_heap_mint_inv => slen_vA.
symmetry.
apply dom_heap_mint_sign_unchanged2 with A s slen slen'.
exact rA_st_st'.
exact slen_vA.
exact Hslen'.
by rewrite Hptr.
rewrite assoc_prop_m.swap_heads in s_st_h; last by done.
apply (state_mint_var_mint _ _ _ _ _ _ s_st_h).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
by rewrite assoc.get_union_sing_eq.
by apply (mips_syntax.dom_heap_invariant _ _ _ _ _ exec_asm).
+ symmetry.
apply dom_heap_mint_unsign_unchanged2 with y s.
exact rk_st_st'.
exact ry_st_st'.
apply (state_mint_var_mint _ _ _ _ _ _ s_st_h).
rewrite assoc.get_union_sing_neq; last by Nodup_neq.
by rewrite assoc.get_union_sing_eq.
by apply (mips_syntax.dom_heap_invariant _ _ _ _ _ exec_asm).
+ move=> t Ht x0 Hx0.
mips_syntax.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 (signed L rA))); last by rewrite /=; auto.
Disj_remove_dup.
simpl.
apply nodup_disj.
simpl app.
by Nodup_nodup r0.
* 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 ry))); 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.
+ by Nodup_neq.
+ move: (mips_syntax.exec_deter_proj _ _ _ _ _ exec_asm _ _ _ exec_asm_proj); tauto.
Qed.
Lemma pfwd_sim_multi_sub_s_u_wo_overflow : forall (A y : assoc.l) d
L rk ry rA a0 a1 a2 a3 a4 a5 X,
nodup(A, y) ->
nodup(rk, rA, ry, a0, a1, a2, a3, a4, a5, X, r0) ->
disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: X :: List.nil)%list ->
A \notin assoc.dom d -> y \notin assoc.dom d ->
signed L rA \notin assoc.cdom d -> unsign rk ry \notin assoc.cdom d ->
pfwd_sim (state_mint (A |=> signed L rA \U+ (y |=> unsign rk ry \U+ d)))
(fun s st _ => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([A ]_ s)%seplog_expr < Zbeta (L - 1) /\
0 <= ([y ]_ s)%seplog_expr < Zbeta (L - 1))
(A <- (var_e A .-e var_e y)%seplog_expr)%seplog_cmd
(multi_sub_s_u rk rA ry a0 a1 a2 a3 a4 a5 X).
Proof.
move=> A y d L rk rA ry a0 a1 a2 a3 a4 a5 X Hvars Hregs Hd A_d y_d rA_d rk_ry_d.
eapply pfwd_sim_stren; last by apply pfwd_sim_multi_sub_s_u.
move=> s st h [rk_neq0 [rk_max [L_neq0 [L_rk [A_max y_bounds]]]]].
split; first by assumption.
split; first by assumption.
split; first by assumption.
split.
eapply Zlt_trans; first by apply A_max.
apply Zbeta_lt; omega.
split.
split; first by tauto.
eapply Zlt_trans; first by apply (proj2 y_bounds).
apply Zbeta_lt; omega.
eapply Zle_lt_trans; first by apply Zabs_triangle.
rewrite Zabs_Zopp.
rewrite (Zabs_eq ([y ]_ s)%seplog_expr); last by omega.
eapply Zlt_trans.
apply Zplus_lt_compat.
by apply A_max.
by apply (proj2 y_bounds).
rewrite /Zbeta Zpower_plus.
apply Zpower_2_lt; omega.
Qed.