Library multi_sub_termination
Require Import ssreflect ssrbool.
Require Import ZArith_ext Lists_ext.
Require Import machine_int.
Import MachineInt.
Require Import mips_cmd mips_tactics mips_contrib.
Require Import multi_sub_prg.
Local Open Scope mips_expr_scope.
Local Open Scope mips_cmd_scope.
Local Open Scope machine_int_scope.
Local Open Scope nodup_scope.
Import expr_m.
Lemma termination_multi_sub : forall s h k m z ext int_ quot C_ M_ B2K_,
nodup(k, m, z, ext, int_, quot, C_, M_, B2K_, r0) ->
{ si | Some (s, h) -- multi_sub k z m z ext int_ quot C_ M_ B2K_ ---> si }.
Proof.
move=> s h k m z ext int_ quot C_ M_ B2K_ Hset.
rewrite /multi_sub.
apply exists_addiu_seq.
repeat reg_upd.
rewrite add_com add_0.
apply exists_addiu_seq.
repeat reg_upd.
rewrite sext_Z2u // add_0.
apply exists_addiu_seq.
repeat reg_upd.
rewrite sext_Z2u // add_0.
set s0 := store.upd _ _ _.
have [kint_ Hkint_] : { kint_ | u2Z [k]_s0 - u2Z [int_]_s0 = Z_of_nat kint_}.
have [kint_ Hkint_] : { kint_ | u2Z [k]_s0 - u2Z [int_]_s0 = kint_} by eapply exist; reflexivity.
have : 0 <= kint_. rewrite -Hkint_ /s0. repeat reg_upd. rewrite u2Z_Z2u // Zminus_0_r; by apply min_u2Z.
case/Z_of_nat_complete_inf => kint_' H.
exists kint_'; by rewrite -H.
move: kint_ s0 Hkint_ h.
elim.
- move=> s0 Hkint_ h.
eapply exist.
apply while.exec_while_false.
rewrite /= in Hkint_ *.
apply/negPn; apply/Zeq_boolP; omega.
- move=> kint_ IH s0 Hkint_ h.
apply exists_while.
+ rewrite /=; apply/Zeq_boolP; rewrite Z_S in Hkint_; omega.
+ apply exists_seq_P2 with (fun st, u2Z [k]_(fst st) - u2Z [int_]_(fst st) = Z_of_nat kint_).
* exists_lwxs l_m_ H_l_m_ z_m_ H_z_m_.
apply exists_addu_seq_P.
repeat reg_upd.
eapply exists_sltu_seq_P.
reflexivity.
repeat reg_upd.
move Hss : (store.upd _ _ _) => ss.
exists_lwxs l_z H_l_z z_z H_z_z.
apply exists_seq_P with (fun s' => forall st, s' = Some st ->
u2Z [k]_(fst st) - u2Z [int_]_(fst st) = Z_of_nat (S kint_)).
- apply exists_ifte_P.
+ apply exists_addiu_seq_P.
repeat reg_upd.
rewrite add_com add_0 sext_Z2u //.
apply exists_multu_seq_P.
repeat reg_upd.
apply exists_msubu_seq_P.
repeat reg_upd.
eapply exists_sltu_seq_P.
repeat reg_upd.
reflexivity.
apply exists_mflhxu_P.
rewrite Z_S /= in Hkint_ *.
rewrite -Hss.
by repeat reg_upd.
+ apply exists_nop_P.
rewrite Z_S /= in Hkint_ *.
rewrite -Hss.
by repeat reg_upd.
- move=> [[ si hi] | ] Hsi.
rewrite Z_S in Hsi *.
move: {Hsi}(Hsi _ (refl_equal _)) => H1.
rewrite /= in H1.
exists_sw_P l_t H_l_t z_t H_z_t.
apply exists_addiu_seq_P.
repeat reg_upd.
apply exists_addiu_P.
rewrite /=.
repeat reg_upd.
rewrite sext_Z2u // u2Z_add_Z2u //.
rewrite /= in H1; omega.
move: (max_u2Z ([k]_si)) => ?; omega.
* exists None; split; [by apply while.exec_none | done].
+ move=> [ si hi ] Hsi.
by apply IH.
Qed.
Require Import ZArith_ext Lists_ext.
Require Import machine_int.
Import MachineInt.
Require Import mips_cmd mips_tactics mips_contrib.
Require Import multi_sub_prg.
Local Open Scope mips_expr_scope.
Local Open Scope mips_cmd_scope.
Local Open Scope machine_int_scope.
Local Open Scope nodup_scope.
Import expr_m.
Lemma termination_multi_sub : forall s h k m z ext int_ quot C_ M_ B2K_,
nodup(k, m, z, ext, int_, quot, C_, M_, B2K_, r0) ->
{ si | Some (s, h) -- multi_sub k z m z ext int_ quot C_ M_ B2K_ ---> si }.
Proof.
move=> s h k m z ext int_ quot C_ M_ B2K_ Hset.
rewrite /multi_sub.
apply exists_addiu_seq.
repeat reg_upd.
rewrite add_com add_0.
apply exists_addiu_seq.
repeat reg_upd.
rewrite sext_Z2u // add_0.
apply exists_addiu_seq.
repeat reg_upd.
rewrite sext_Z2u // add_0.
set s0 := store.upd _ _ _.
have [kint_ Hkint_] : { kint_ | u2Z [k]_s0 - u2Z [int_]_s0 = Z_of_nat kint_}.
have [kint_ Hkint_] : { kint_ | u2Z [k]_s0 - u2Z [int_]_s0 = kint_} by eapply exist; reflexivity.
have : 0 <= kint_. rewrite -Hkint_ /s0. repeat reg_upd. rewrite u2Z_Z2u // Zminus_0_r; by apply min_u2Z.
case/Z_of_nat_complete_inf => kint_' H.
exists kint_'; by rewrite -H.
move: kint_ s0 Hkint_ h.
elim.
- move=> s0 Hkint_ h.
eapply exist.
apply while.exec_while_false.
rewrite /= in Hkint_ *.
apply/negPn; apply/Zeq_boolP; omega.
- move=> kint_ IH s0 Hkint_ h.
apply exists_while.
+ rewrite /=; apply/Zeq_boolP; rewrite Z_S in Hkint_; omega.
+ apply exists_seq_P2 with (fun st, u2Z [k]_(fst st) - u2Z [int_]_(fst st) = Z_of_nat kint_).
* exists_lwxs l_m_ H_l_m_ z_m_ H_z_m_.
apply exists_addu_seq_P.
repeat reg_upd.
eapply exists_sltu_seq_P.
reflexivity.
repeat reg_upd.
move Hss : (store.upd _ _ _) => ss.
exists_lwxs l_z H_l_z z_z H_z_z.
apply exists_seq_P with (fun s' => forall st, s' = Some st ->
u2Z [k]_(fst st) - u2Z [int_]_(fst st) = Z_of_nat (S kint_)).
- apply exists_ifte_P.
+ apply exists_addiu_seq_P.
repeat reg_upd.
rewrite add_com add_0 sext_Z2u //.
apply exists_multu_seq_P.
repeat reg_upd.
apply exists_msubu_seq_P.
repeat reg_upd.
eapply exists_sltu_seq_P.
repeat reg_upd.
reflexivity.
apply exists_mflhxu_P.
rewrite Z_S /= in Hkint_ *.
rewrite -Hss.
by repeat reg_upd.
+ apply exists_nop_P.
rewrite Z_S /= in Hkint_ *.
rewrite -Hss.
by repeat reg_upd.
- move=> [[ si hi] | ] Hsi.
rewrite Z_S in Hsi *.
move: {Hsi}(Hsi _ (refl_equal _)) => H1.
rewrite /= in H1.
exists_sw_P l_t H_l_t z_t H_z_t.
apply exists_addiu_seq_P.
repeat reg_upd.
apply exists_addiu_P.
rewrite /=.
repeat reg_upd.
rewrite sext_Z2u // u2Z_add_Z2u //.
rewrite /= in H1; omega.
move: (max_u2Z ([k]_si)) => ?; omega.
* exists None; split; [by apply while.exec_none | done].
+ move=> [ si hi ] Hsi.
by apply IH.
Qed.