Library begcd_mips_prelude
Require Import Epsilon.
Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int encode_decode integral_type nodup.
Import MachineInt.
Require Import mips_bipl mips_tactics mips_syntax.
Import mips_bipl.expr_m.
Require Import simu.
Import simu.simu_m.
Require Import begcd.
Require Import multi_div2_prg multi_div2_simu.
Require Import multi_mul2_prg multi_mul2_simu.
Require Import multi_lt_prg multi_lt_termination.
Require Import begcd_mips_prelude_prg.
Require Import multi_is_even_and_prg multi_is_even_and_simu.
Require seq_ext.
Local Open Scope machine_int_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope heap_scope.
Local Open Scope mips_cmd_scope.
Local Open Scope assoc_scope.
Local Open Scope nodup_scope.
Local Open Scope mips_expr_scope.
Lemma sim_begcd_prelude : forall g u v u1 u2 u3 v1 v2 v3 t1 t2 t3
L
rk rg ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3,
nodup(g, u, v, u1, u2, u3, v1, v2, v3, t1, t2, t3) ->
nodup(rk, rg, ru, rv, ru1, ru2, ru3, rv1, rv2, rv3, rt1, rt2, rt3, a0, a1, a2, a3, r0) ->
sim
(g |=> unsign rk rg \U+ (u |=> unsign rk ru \U+ (v |=> unsign rk rv \U+
(u1 |=> signed L ru1 \U+ (u2 |=> signed L ru2 \U+ (u3 |=> signed L ru3 \U+
(v1 |=> signed L rv1 \U+ (v2 |=> signed L rv2 \U+ (v3 |=> signed L rv3 \U+
(t1 |=> signed L rt1 \U+ (t2 |=> signed L rt2 \U+ t3 |=> signed L rt3)))))))))))
(fun s st h =>
([ u ]_ s * [ g ]_ s)%seplog_expr < Zbeta (Zabs_nat (u2Z [ rk ]_st)) /\
(0 <= [ g ]_s)%seplog_expr /\
(0 < [ u ]_s)%seplog_expr /\
0 < (u2Z [ rk ]_st))
(EGCD.prelude u v g)
(prelude_mips rk rg ru rv a0 a1 a2 a3).
Proof.
move=> g u v u1 u2 u3 v1 v2 v3 t1 t2 t3
L
rk rg ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3
Hvars Haux.
apply fwd_sim_while ; first by done.
- rewrite /inv_R => s st h Hyp st' h' Hmips.
split.
+ case : Hyp => Hyp _.
set tmparg := assoc.union _ _ in Hyp.
have : inv_R (state_mint tmparg) (multi_is_even_and rk ru rv a0 a1).
apply state_mint_invariant => //.
rewrite /tmparg. rewrite [mips_frame.modified_regs _]/=.
Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply nodup.nodup_disj; rewrite [_ ++ _]/=; by Nodup_nodup r0.
by move/(_ s st h Hyp _ _ Hmips).
+ suff : [ rk ]_ st = [ rk ]_ st' by move=> <-; tauto.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
- rewrite /rela_hoare => s st h Hyp s' Hseplog st' h' Hmips.
have -> : ([ u ]_ s' = [ u ]_ s / 2)%seplog_expr.
case/syntax_m.seplog_m.semop_prop_m.exec_seq_inv : Hseplog.
case.
+ move=> [s'' h''] [Hseplog1 Hseplog2].
apply trans_eq with ([ u ]_ s'')%seplog_expr.
+ symmetry; Var_unchanged. rewrite [syntax_m.seplog_m.modified_vars _]/=; by Nodup_not_In.
+ move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : Hseplog1.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
by syntax_m.seplog_m.assert_m.expr_m.Store_upd.
+ case=> _. by move/syntax_m.seplog_m.semop_prop_m.from_none.
have -> : ([ g ]_ s' = [ g ]_ s * 2)%seplog_expr.
move/syntax_m.seplog_m.semop_prop_m.exec_seq_assoc' : Hseplog.
case/syntax_m.seplog_m.semop_prop_m.exec_seq_inv => s'' [Hss'' Hs''s'].
destruct s'' as [[s'' h'']|]; last first.
by move/syntax_m.seplog_m.semop_prop_m.from_none : Hs''s'.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : Hs''s'.
case/syntax_m.seplog_m.exec0_assign_inv => Hh'' Hs'.
rewrite /= Hs'.
syntax_m.seplog_m.assert_m.expr_m.Store_upd.
rewrite (syntax_m.var_unchanged _ _ _ _ _ Hss'' g) //.
rewrite [syntax_m.seplog_m.modified_vars _]/=; by Nodup_not_In.
have <- : [ rk ]_ st = [ rk ]_ st'.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
split.
rewrite Zmult_comm -Zmult_assoc -Zdivide_Zdiv_eq //.
+ rewrite Zmult_comm; tauto.
+ apply Zmod_divide => //. case : Hyp => _ [] _ /=. case/andP. by move/Zeq_bool_eq.
split; first by omega.
split.
apply: (proj1 (Zdivide_Zdiv_lt_pos _ _ _ _ _)) => //.
+ tauto.
+ apply Zmod_divide => //. case : Hyp => _ [] _ /=. case/andP. by move/Zeq_bool_eq.
tauto.
- apply fwd_sim_b_stren with (state_mint
(g |=> unsign rk rg \U+ (u |=> unsign rk ru \U+ (v |=> unsign rk rv \U+
(u1 |=> signed L ru1 \U+ (u2 |=> signed L ru2 \U+ (u3 |=> signed L ru3 \U+
(v1 |=> signed L rv1 \U+ (v2 |=> signed L rv2 \U+ (v3 |=> signed L rv3 \U+
(t1 |=> signed L rt1 \U+ (t2 |=> signed L rt2 \U+ t3 |=> signed L rt3)))))))))))).
by intuition.
assoc_put_in_front v.
assoc_put_in_front u.
apply fwd_sim_b_multi_is_even_and.
rewrite [Equality.sort assoc.l]/= in Hvars *; by Nodup_nodup O.
by Nodup_nodup r0 .
- apply fwd_sim_seq with (fun s st h =>
0 <= [ g ]_ s /\
0 < [ u ]_ s /\
([u]_s * [g]_s) < 2 ^^ (Zabs_nat (u2Z ([rk ]_ st)%mips_expr) * 32 - 1))%seplog_expr => //.
+ rewrite /rela_hoare => s st h Hyp s' Hseplog st' h' Hmips.
have -> : ([ u ]_ s' = [ u ]_ s / 2)%seplog_expr.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : Hseplog => Hseplog.
case/syntax_m.seplog_m.exec0_assign_inv : Hseplog => _ ?; subst s'.
by syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([ g ]_ s = [ g ]_ s' )%seplog_expr.
Var_unchanged. rewrite [syntax_m.seplog_m.modified_vars _]/=; by Nodup_not_In.
have <- : [ rk ]_ st = [ rk ]_ st'.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
split; first by tauto.
split.
+ apply: (proj1 (Zdivide_Zdiv_lt_pos _ _ _ _ _)) => //.
* tauto.
* apply Zmod_divide => //. case : Hyp => /= _ [] _. case/andP => Hyp _. by move/Zeq_bool_eq : Hyp.
+ apply Zlt_le_trans with (Zbeta (Zabs_nat (u2Z ([rk ]_ st))) / 2).
+ rewrite Zmult_comm -Zdivide_Zdiv_eq_2 //.
* apply Zdiv_lt_upper_bound => //.
rewrite (Zmult_comm _ 2) -Z_div_exact_full_2 //.
- rewrite Zmult_comm; tauto.
- apply Zpower_mod.
apply lt_O_neq.
apply mult_lt_compat_0; last by repeat constructor.
apply lt_O_neq.
apply O_lt_Zabs_nat; tauto.
* apply Zmod_divide => //. case : Hyp => /= _ [] _. case/andP => Hyp _. by move/Zeq_bool_eq : Hyp.
+ rewrite Zpower_div //.
* by apply Zle_refl.
* apply lt_O_neq.
apply mult_lt_compat_0; last by repeat constructor.
apply lt_O_neq.
apply O_lt_Zabs_nat; tauto.
+ assoc_put_in_front u.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2; Nodup_nodup r0.
apply pfwd_sim_div2.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
+ apply fwd_sim_seq with (fun s st _ =>
([ g ]_ s)%seplog_expr < 2 ^^ ((Zabs_nat (u2Z ([rk ]_ st)) * 32) - 1)) => //.
* rewrite /rela_hoare => s st h HP0 s' Hseplog st' h' Hmips.
have <- : ( [ g ]_ s = [ g ]_ s' )%seplog_expr.
Var_unchanged. rewrite [syntax_m.seplog_m.modified_vars _]/=; by Nodup_not_In.
have <- : [ rk ]_ st = [ rk ]_ st'.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
apply Zmult_lt_compat3 with ([ u ]_ s)%seplog_expr.
- tauto.
- tauto.
- apply Zle_trans with 1 => //.
by apply Zpower_1.
- rewrite Zmult_comm; tauto.
*
assoc_put_in_front u.
apply pfwd_sim_fwd_sim; last first.
assoc_put_in_front v.
apply safe_termination_div2; by Nodup_nodup r0.
assoc_put_in_front v.
apply pfwd_sim_div2 => //.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl map. by Nodup_not_In.
* apply pfwd_sim_fwd_sim; last by apply safe_termination_mul2; Nodup_nodup r0.
apply psim_mul2.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl map. by Nodup_not_In.
Qed.
Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int encode_decode integral_type nodup.
Import MachineInt.
Require Import mips_bipl mips_tactics mips_syntax.
Import mips_bipl.expr_m.
Require Import simu.
Import simu.simu_m.
Require Import begcd.
Require Import multi_div2_prg multi_div2_simu.
Require Import multi_mul2_prg multi_mul2_simu.
Require Import multi_lt_prg multi_lt_termination.
Require Import begcd_mips_prelude_prg.
Require Import multi_is_even_and_prg multi_is_even_and_simu.
Require seq_ext.
Local Open Scope machine_int_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope heap_scope.
Local Open Scope mips_cmd_scope.
Local Open Scope assoc_scope.
Local Open Scope nodup_scope.
Local Open Scope mips_expr_scope.
Lemma sim_begcd_prelude : forall g u v u1 u2 u3 v1 v2 v3 t1 t2 t3
L
rk rg ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3,
nodup(g, u, v, u1, u2, u3, v1, v2, v3, t1, t2, t3) ->
nodup(rk, rg, ru, rv, ru1, ru2, ru3, rv1, rv2, rv3, rt1, rt2, rt3, a0, a1, a2, a3, r0) ->
sim
(g |=> unsign rk rg \U+ (u |=> unsign rk ru \U+ (v |=> unsign rk rv \U+
(u1 |=> signed L ru1 \U+ (u2 |=> signed L ru2 \U+ (u3 |=> signed L ru3 \U+
(v1 |=> signed L rv1 \U+ (v2 |=> signed L rv2 \U+ (v3 |=> signed L rv3 \U+
(t1 |=> signed L rt1 \U+ (t2 |=> signed L rt2 \U+ t3 |=> signed L rt3)))))))))))
(fun s st h =>
([ u ]_ s * [ g ]_ s)%seplog_expr < Zbeta (Zabs_nat (u2Z [ rk ]_st)) /\
(0 <= [ g ]_s)%seplog_expr /\
(0 < [ u ]_s)%seplog_expr /\
0 < (u2Z [ rk ]_st))
(EGCD.prelude u v g)
(prelude_mips rk rg ru rv a0 a1 a2 a3).
Proof.
move=> g u v u1 u2 u3 v1 v2 v3 t1 t2 t3
L
rk rg ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3
Hvars Haux.
apply fwd_sim_while ; first by done.
- rewrite /inv_R => s st h Hyp st' h' Hmips.
split.
+ case : Hyp => Hyp _.
set tmparg := assoc.union _ _ in Hyp.
have : inv_R (state_mint tmparg) (multi_is_even_and rk ru rv a0 a1).
apply state_mint_invariant => //.
rewrite /tmparg. rewrite [mips_frame.modified_regs _]/=.
Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply nodup.nodup_disj; rewrite [_ ++ _]/=; by Nodup_nodup r0.
by move/(_ s st h Hyp _ _ Hmips).
+ suff : [ rk ]_ st = [ rk ]_ st' by move=> <-; tauto.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
- rewrite /rela_hoare => s st h Hyp s' Hseplog st' h' Hmips.
have -> : ([ u ]_ s' = [ u ]_ s / 2)%seplog_expr.
case/syntax_m.seplog_m.semop_prop_m.exec_seq_inv : Hseplog.
case.
+ move=> [s'' h''] [Hseplog1 Hseplog2].
apply trans_eq with ([ u ]_ s'')%seplog_expr.
+ symmetry; Var_unchanged. rewrite [syntax_m.seplog_m.modified_vars _]/=; by Nodup_not_In.
+ move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : Hseplog1.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
by syntax_m.seplog_m.assert_m.expr_m.Store_upd.
+ case=> _. by move/syntax_m.seplog_m.semop_prop_m.from_none.
have -> : ([ g ]_ s' = [ g ]_ s * 2)%seplog_expr.
move/syntax_m.seplog_m.semop_prop_m.exec_seq_assoc' : Hseplog.
case/syntax_m.seplog_m.semop_prop_m.exec_seq_inv => s'' [Hss'' Hs''s'].
destruct s'' as [[s'' h'']|]; last first.
by move/syntax_m.seplog_m.semop_prop_m.from_none : Hs''s'.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : Hs''s'.
case/syntax_m.seplog_m.exec0_assign_inv => Hh'' Hs'.
rewrite /= Hs'.
syntax_m.seplog_m.assert_m.expr_m.Store_upd.
rewrite (syntax_m.var_unchanged _ _ _ _ _ Hss'' g) //.
rewrite [syntax_m.seplog_m.modified_vars _]/=; by Nodup_not_In.
have <- : [ rk ]_ st = [ rk ]_ st'.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
split.
rewrite Zmult_comm -Zmult_assoc -Zdivide_Zdiv_eq //.
+ rewrite Zmult_comm; tauto.
+ apply Zmod_divide => //. case : Hyp => _ [] _ /=. case/andP. by move/Zeq_bool_eq.
split; first by omega.
split.
apply: (proj1 (Zdivide_Zdiv_lt_pos _ _ _ _ _)) => //.
+ tauto.
+ apply Zmod_divide => //. case : Hyp => _ [] _ /=. case/andP. by move/Zeq_bool_eq.
tauto.
- apply fwd_sim_b_stren with (state_mint
(g |=> unsign rk rg \U+ (u |=> unsign rk ru \U+ (v |=> unsign rk rv \U+
(u1 |=> signed L ru1 \U+ (u2 |=> signed L ru2 \U+ (u3 |=> signed L ru3 \U+
(v1 |=> signed L rv1 \U+ (v2 |=> signed L rv2 \U+ (v3 |=> signed L rv3 \U+
(t1 |=> signed L rt1 \U+ (t2 |=> signed L rt2 \U+ t3 |=> signed L rt3)))))))))))).
by intuition.
assoc_put_in_front v.
assoc_put_in_front u.
apply fwd_sim_b_multi_is_even_and.
rewrite [Equality.sort assoc.l]/= in Hvars *; by Nodup_nodup O.
by Nodup_nodup r0 .
- apply fwd_sim_seq with (fun s st h =>
0 <= [ g ]_ s /\
0 < [ u ]_ s /\
([u]_s * [g]_s) < 2 ^^ (Zabs_nat (u2Z ([rk ]_ st)%mips_expr) * 32 - 1))%seplog_expr => //.
+ rewrite /rela_hoare => s st h Hyp s' Hseplog st' h' Hmips.
have -> : ([ u ]_ s' = [ u ]_ s / 2)%seplog_expr.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : Hseplog => Hseplog.
case/syntax_m.seplog_m.exec0_assign_inv : Hseplog => _ ?; subst s'.
by syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([ g ]_ s = [ g ]_ s' )%seplog_expr.
Var_unchanged. rewrite [syntax_m.seplog_m.modified_vars _]/=; by Nodup_not_In.
have <- : [ rk ]_ st = [ rk ]_ st'.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
split; first by tauto.
split.
+ apply: (proj1 (Zdivide_Zdiv_lt_pos _ _ _ _ _)) => //.
* tauto.
* apply Zmod_divide => //. case : Hyp => /= _ [] _. case/andP => Hyp _. by move/Zeq_bool_eq : Hyp.
+ apply Zlt_le_trans with (Zbeta (Zabs_nat (u2Z ([rk ]_ st))) / 2).
+ rewrite Zmult_comm -Zdivide_Zdiv_eq_2 //.
* apply Zdiv_lt_upper_bound => //.
rewrite (Zmult_comm _ 2) -Z_div_exact_full_2 //.
- rewrite Zmult_comm; tauto.
- apply Zpower_mod.
apply lt_O_neq.
apply mult_lt_compat_0; last by repeat constructor.
apply lt_O_neq.
apply O_lt_Zabs_nat; tauto.
* apply Zmod_divide => //. case : Hyp => /= _ [] _. case/andP => Hyp _. by move/Zeq_bool_eq : Hyp.
+ rewrite Zpower_div //.
* by apply Zle_refl.
* apply lt_O_neq.
apply mult_lt_compat_0; last by repeat constructor.
apply lt_O_neq.
apply O_lt_Zabs_nat; tauto.
+ assoc_put_in_front u.
apply pfwd_sim_fwd_sim; last by apply safe_termination_div2; Nodup_nodup r0.
apply pfwd_sim_div2.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
+ apply fwd_sim_seq with (fun s st _ =>
([ g ]_ s)%seplog_expr < 2 ^^ ((Zabs_nat (u2Z ([rk ]_ st)) * 32) - 1)) => //.
* rewrite /rela_hoare => s st h HP0 s' Hseplog st' h' Hmips.
have <- : ( [ g ]_ s = [ g ]_ s' )%seplog_expr.
Var_unchanged. rewrite [syntax_m.seplog_m.modified_vars _]/=; by Nodup_not_In.
have <- : [ rk ]_ st = [ rk ]_ st'.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
apply Zmult_lt_compat3 with ([ u ]_ s)%seplog_expr.
- tauto.
- tauto.
- apply Zle_trans with 1 => //.
by apply Zpower_1.
- rewrite Zmult_comm; tauto.
*
assoc_put_in_front u.
apply pfwd_sim_fwd_sim; last first.
assoc_put_in_front v.
apply safe_termination_div2; by Nodup_nodup r0.
assoc_put_in_front v.
apply pfwd_sim_div2 => //.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl map. by Nodup_not_In.
* apply pfwd_sim_fwd_sim; last by apply safe_termination_mul2; Nodup_nodup r0.
apply psim_mul2.
- by Nodup_nodup r0.
- Disj_f_cdom2list Permutation_mints_regs.
Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
- apply/seq_ext.inP.
Not_In_dom2list; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl map. by Nodup_not_In.
Qed.