Library begcd_mips_init
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_zero_prg.
Require Import multi_negate_prg.
Require Import multi_is_even_prg multi_is_even_simu.
Require Import multi_sub_signed_unsigned_prg multi_sub_signed_unsigned_simu.
Require Import library_interfaces.
Local Open Scope machine_int_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope heap_scope.
Local Open Scope nodup_scope.
Local Open Scope assoc_scope.
Definition init_mips rk ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3
a0 a1 a2 a3 a4 a5 a6 :=
((multi_one_signed ru1 a0 a1 a2 a3 ;
multi_zero_signed ru2 a0 a1 a2 a3 ;
copy_signed_unsigned ru3 rk ru a0 a1 a2 a3 ;
copy_signed_unsigned rv1 rk rv a0 a1 a2 a3 ;
(multi_one_signed rv2 a0 a1 a2 a3 ;
multi_sub_s_u rk rv2 ru a0 a1 a2 a3 a4 a5 a6) ;
copy_signed_unsigned rv3 rk rv a0 a1 a2 a3) ;
multi_is_even rk ru a0 ;
while.ifte (beq a0 r0)
(multi_zero_signed rt1 a0 a1 a2 a3 ;
(multi_one_signed rt2 a0 a1 a2 a3 ;
negate rt2 a0) ;
(copy_signed_unsigned rt3 rk rv a0 a1 a2 a3 ;
negate rt3 a0))
(multi_one_signed rt1 a0 a1 a2 a3 ;
multi_zero_signed rt2 a0 a1 a2 a3 ;
copy_signed_unsigned rt3 rk ru a0 a1 a2 a3))%mips_cmd.
Definition uv_bound rk st u v s L :=
0 < u2Z ([rk ]_ st)%mips_expr < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)%mips_expr) /\
0 < ([u ]_ s)%seplog_expr < Zbeta (L - 1) /\
0 < ([v ]_ s)%seplog_expr < Zbeta (L - 1).
Lemma fwd_sim_begcd_init : forall vu vv 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 a4 a5 a6,
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,a4,a5,a6,r0) ->
0 < vu -> 0 < vv ->
fwd_sim (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))))))))))))
(fun s st _ => (EGCD.C2 vu vv u v g s /\ EGCD.C3 vu vv u v g s) /\ uv_bound rk st u v s L)
(EGCD.TAOCP.init u v u1 u2 u3 v1 v2 v3 t1 t2 t3)
(init_mips rk ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6).
Proof.
move=> vu vv 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 a4 a5 a6
Hvars Hset Hvu Hvv.
rewrite /EGCD.TAOCP.init /init_mips.
apply fwd_sim_seq with (fun s st h => (EGCD.C2 vu vv u v g s /\ EGCD.C3 vu vv u v g s /\
EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\ uv_bound rk st u v s L) => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
move: (EGCD.TAOCP.begcd_verif_init0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hvars Hvu Hvv).
move/syntax_m.seplog_m.hoare_prop_m.soundness.
rewrite /while.hoare_semantics.
case/( _ _ syntax_m.seplog_m.assert_m.heap.emp (proj1 Hcond)) => _.
by move/(_ _ _ exec_pseudo).
- rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
local_Var_unchanged v s.
rewrite /uv_bound in Hcond; tauto.
- apply fwd_sim_seq with (fun s st _ => (EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s) /\ uv_bound rk st u v s L) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
* rewrite /EGCD.C2 / EGCD.C3 in Hcond *.
rewrite /=.
local_Var_unchanged u s.
local_Var_unchanged v s.
local_Var_unchanged g s.
tauto.
* rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
local_Var_unchanged v s.
tauto.
+ assoc_put_in_front u1.
apply pfwd_sim_fwd_sim; last by apply safe_termination_one_signed; Nodup_nodup r0.
apply pfwd_sim_one_signed.
- 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 List.map. by Nodup_not_In.
apply fwd_sim_seq with (fun s st _ => (EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s) /\ uv_bound rk st u v s L) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
* rewrite /EGCD.C2 / EGCD.C3 in Hcond *.
rewrite /=.
local_Var_unchanged u s.
local_Var_unchanged v s.
local_Var_unchanged g s.
tauto.
* rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
local_Var_unchanged v s.
tauto.
+ assoc_put_in_front u2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_zero_signed; Nodup_nodup r0.
apply pfwd_sim_zero_signed.
- 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 List.map. by Nodup_not_In.
apply fwd_sim_seq with (fun s st _ => (EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s) /\ uv_bound rk st u v s L) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
* rewrite /EGCD.C2 / EGCD.C3 in Hcond *.
rewrite /=.
local_Var_unchanged u s.
local_Var_unchanged v s.
local_Var_unchanged g s.
tauto.
* rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
local_Var_unchanged v s.
tauto.
+ assoc_put_in_front u3.
assoc_put_in_front u.
apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_unsigned; Nodup_nodup r0.
apply pfwd_sim_copy_signed_unsigned.
- 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.
apply not_In_mint_ptr. simpl map. simpl mint_ptr. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
apply fwd_sim_seq with (fun s st _ => (EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s) /\ uv_bound rk st u v s L) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
* rewrite /EGCD.C2 / EGCD.C3 in Hcond *.
rewrite /=.
local_Var_unchanged u s.
local_Var_unchanged v s.
local_Var_unchanged g s.
tauto.
* rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
local_Var_unchanged v s.
tauto.
+ assoc_put_in_front v1.
assoc_put_in_front v.
apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_unsigned; Nodup_nodup r0.
apply pfwd_sim_copy_signed_unsigned.
- 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.
apply not_In_mint_ptr. simpl map. simpl mint_ptr. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
apply fwd_sim_seq with (fun s st _ => (EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s) /\ uv_bound rk st u v s L) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
* rewrite /EGCD.C2 / EGCD.C3 in Hcond *.
rewrite /=.
local_Var_unchanged u s.
local_Var_unchanged v s.
local_Var_unchanged g s.
tauto.
* rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
local_Var_unchanged v s.
tauto.
apply fwd_sim_pcode_equiv with (v2 <- nat_e 1 ; v2 <- var_e v2 .-e var_e u)%seplog_expr%seplog_cmd; last by apply equivalent_pseudo_code_example2; Nodup_neq.
apply fwd_sim_seq with (fun s st _ => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([v2 ]_ s)%seplog_expr < Zbeta (L - 1) /\
0 <= ([u ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
rewrite /uv_bound in Hcond.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
split; first by move=> abs; rewrite abs u2Z_Z2u // in Hcond; omega.
repeat (split; first by tauto).
split; first by move: (Zbeta_0' L) => /= ?; omega.
omega.
+ assoc_put_in_front v2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_one_signed; Nodup_nodup r0.
apply pfwd_sim_one_signed.
- 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 List.map. by Nodup_not_In.
assoc_put_in_front u.
assoc_put_in_front v2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_multi_sub_s_u; Nodup_nodup r0.
apply pfwd_sim_multi_sub_s_u_wo_overflow.
- rewrite [Equality.sort _]/= in Hvars *. by Nodup_nodup O.
- 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; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
assoc_put_in_front v3.
assoc_put_in_front v.
apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_unsigned; Nodup_nodup r0.
apply pfwd_sim_copy_signed_unsigned.
- 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.
apply not_In_mint_ptr. simpl map. simpl mint_ptr. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
apply fwd_sim_ifte => //.
- rewrite /inv_R => s st h [s_st_h Hcond] st' h' exec_asm; split.
+ eapply state_mint_invariant; [idtac | idtac | apply s_st_h | apply exec_asm] => //.
Disj_f_cdom2list Permutation_mints_regs.
rewrite [mips_frame.modified_regs _]/=.
Disj_remove_dup.
apply: nodup.nodup_disj. rewrite [List.app _ _]/=. by Nodup_nodup r0.
+ rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
- assoc_put_in_front u.
apply fwd_sim_b_multi_is_even.
+ 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 _]/= [List.map _ _]/=. by Nodup_not_In.
- apply fwd_sim_seq with (fun s st _ => ((EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s /\ EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\
uv_bound rk st u v s L) /\
([var_e u mode nat_e 2 =e nat_e 1 ]b_ s)%seplog_expr) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
rewrite /EGCD.C2 /EGCD.C3 /EGCD.uivi_init /uv_bound in Hcond *.
simpl.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
+ assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last by apply safe_termination_zero_signed; Nodup_nodup r0.
apply pfwd_sim_zero_signed.
- 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 List.map. by Nodup_not_In.
- apply fwd_sim_seq with (fun s st _ =>
((EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s /\ EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\
uv_bound rk st u v s L) /\
([var_e u mode nat_e 2 =e nat_e 1 ]b_ s)%seplog_expr) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
rewrite /EGCD.C2 /EGCD.C3 /EGCD.uivi_init /uv_bound in Hcond *.
simpl.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
apply fwd_sim_pcode_equiv with (t2 <- nat_e 1 ; t2 <- .--e (var_e t2))%seplog_expr%seplog_cmd; last first.
eapply equivalent_pseudo_code_trans; by [apply equivalent_pseudo_code_example3 | apply equivalent_pseudo_code_example_assign].
apply fwd_sim_seq with (fun s st _ => ((EGCD.C2 vu vv u v g s /\
EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\ uv_bound rk st u v s L)) => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
rewrite /EGCD.C2 /EGCD.uivi_init /uv_bound in Hcond *.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
- assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_one_signed; Nodup_nodup r0.
apply pfwd_sim_one_signed.
- 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 List.map. by Nodup_not_In.
- assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_negate; Nodup_nodup r0.
apply pfwd_sim_negate.
- 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 List.map. by Nodup_not_In.
- apply fwd_sim_pcode_equiv with (t3 <- var_e v ; t3 <- .--e (var_e t3))%seplog_expr%seplog_cmd; last first.
eapply equivalent_pseudo_code_trans; by [apply equivalent_pseudo_code_example3 | apply equivalent_pseudo_code_example_assign].
apply fwd_sim_seq with (fun s st _ =>
((EGCD.C2 vu vv u v g s /\ EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\
uv_bound rk st u v s L)) => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
rewrite /EGCD.C2 /EGCD.uivi_init /uv_bound in Hcond *.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
- assoc_put_in_front t3.
assoc_put_in_front v.
apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_unsigned; Nodup_nodup r0.
apply pfwd_sim_copy_signed_unsigned.
- 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.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
- assoc_put_in_front t3.
apply pfwd_sim_fwd_sim; last by apply safe_termination_negate; Nodup_nodup r0.
apply pfwd_sim_negate.
- 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 List.map. by Nodup_not_In.
apply fwd_sim_seq with (fun s st _ =>
((EGCD.C2 vu vv u v g s /\ EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\
uv_bound rk st u v s L) ) => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
rewrite /EGCD.C2 /EGCD.uivi_init /uv_bound in Hcond *.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
- assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last by apply safe_termination_one_signed; Nodup_nodup r0.
apply pfwd_sim_one_signed.
- 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 List.map. by Nodup_not_In.
apply fwd_sim_seq with (fun s st _ =>
(EGCD.C2 vu vv u v g s /\ EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\
uv_bound rk st u v s L) => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
rewrite /EGCD.C2 /EGCD.uivi_init /uv_bound in Hcond *.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
- assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_zero_signed; Nodup_nodup r0.
apply pfwd_sim_zero_signed.
- 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 List.map. by Nodup_not_In.
- assoc_put_in_front t3.
assoc_put_in_front u.
apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_unsigned; Nodup_nodup r0.
apply pfwd_sim_copy_signed_unsigned.
- 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.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.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_zero_prg.
Require Import multi_negate_prg.
Require Import multi_is_even_prg multi_is_even_simu.
Require Import multi_sub_signed_unsigned_prg multi_sub_signed_unsigned_simu.
Require Import library_interfaces.
Local Open Scope machine_int_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope heap_scope.
Local Open Scope nodup_scope.
Local Open Scope assoc_scope.
Definition init_mips rk ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3
a0 a1 a2 a3 a4 a5 a6 :=
((multi_one_signed ru1 a0 a1 a2 a3 ;
multi_zero_signed ru2 a0 a1 a2 a3 ;
copy_signed_unsigned ru3 rk ru a0 a1 a2 a3 ;
copy_signed_unsigned rv1 rk rv a0 a1 a2 a3 ;
(multi_one_signed rv2 a0 a1 a2 a3 ;
multi_sub_s_u rk rv2 ru a0 a1 a2 a3 a4 a5 a6) ;
copy_signed_unsigned rv3 rk rv a0 a1 a2 a3) ;
multi_is_even rk ru a0 ;
while.ifte (beq a0 r0)
(multi_zero_signed rt1 a0 a1 a2 a3 ;
(multi_one_signed rt2 a0 a1 a2 a3 ;
negate rt2 a0) ;
(copy_signed_unsigned rt3 rk rv a0 a1 a2 a3 ;
negate rt3 a0))
(multi_one_signed rt1 a0 a1 a2 a3 ;
multi_zero_signed rt2 a0 a1 a2 a3 ;
copy_signed_unsigned rt3 rk ru a0 a1 a2 a3))%mips_cmd.
Definition uv_bound rk st u v s L :=
0 < u2Z ([rk ]_ st)%mips_expr < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)%mips_expr) /\
0 < ([u ]_ s)%seplog_expr < Zbeta (L - 1) /\
0 < ([v ]_ s)%seplog_expr < Zbeta (L - 1).
Lemma fwd_sim_begcd_init : forall vu vv 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 a4 a5 a6,
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,a4,a5,a6,r0) ->
0 < vu -> 0 < vv ->
fwd_sim (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))))))))))))
(fun s st _ => (EGCD.C2 vu vv u v g s /\ EGCD.C3 vu vv u v g s) /\ uv_bound rk st u v s L)
(EGCD.TAOCP.init u v u1 u2 u3 v1 v2 v3 t1 t2 t3)
(init_mips rk ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6).
Proof.
move=> vu vv 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 a4 a5 a6
Hvars Hset Hvu Hvv.
rewrite /EGCD.TAOCP.init /init_mips.
apply fwd_sim_seq with (fun s st h => (EGCD.C2 vu vv u v g s /\ EGCD.C3 vu vv u v g s /\
EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\ uv_bound rk st u v s L) => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
move: (EGCD.TAOCP.begcd_verif_init0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hvars Hvu Hvv).
move/syntax_m.seplog_m.hoare_prop_m.soundness.
rewrite /while.hoare_semantics.
case/( _ _ syntax_m.seplog_m.assert_m.heap.emp (proj1 Hcond)) => _.
by move/(_ _ _ exec_pseudo).
- rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
local_Var_unchanged v s.
rewrite /uv_bound in Hcond; tauto.
- apply fwd_sim_seq with (fun s st _ => (EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s) /\ uv_bound rk st u v s L) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
* rewrite /EGCD.C2 / EGCD.C3 in Hcond *.
rewrite /=.
local_Var_unchanged u s.
local_Var_unchanged v s.
local_Var_unchanged g s.
tauto.
* rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
local_Var_unchanged v s.
tauto.
+ assoc_put_in_front u1.
apply pfwd_sim_fwd_sim; last by apply safe_termination_one_signed; Nodup_nodup r0.
apply pfwd_sim_one_signed.
- 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 List.map. by Nodup_not_In.
apply fwd_sim_seq with (fun s st _ => (EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s) /\ uv_bound rk st u v s L) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
* rewrite /EGCD.C2 / EGCD.C3 in Hcond *.
rewrite /=.
local_Var_unchanged u s.
local_Var_unchanged v s.
local_Var_unchanged g s.
tauto.
* rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
local_Var_unchanged v s.
tauto.
+ assoc_put_in_front u2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_zero_signed; Nodup_nodup r0.
apply pfwd_sim_zero_signed.
- 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 List.map. by Nodup_not_In.
apply fwd_sim_seq with (fun s st _ => (EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s) /\ uv_bound rk st u v s L) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
* rewrite /EGCD.C2 / EGCD.C3 in Hcond *.
rewrite /=.
local_Var_unchanged u s.
local_Var_unchanged v s.
local_Var_unchanged g s.
tauto.
* rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
local_Var_unchanged v s.
tauto.
+ assoc_put_in_front u3.
assoc_put_in_front u.
apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_unsigned; Nodup_nodup r0.
apply pfwd_sim_copy_signed_unsigned.
- 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.
apply not_In_mint_ptr. simpl map. simpl mint_ptr. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
apply fwd_sim_seq with (fun s st _ => (EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s) /\ uv_bound rk st u v s L) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
* rewrite /EGCD.C2 / EGCD.C3 in Hcond *.
rewrite /=.
local_Var_unchanged u s.
local_Var_unchanged v s.
local_Var_unchanged g s.
tauto.
* rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
local_Var_unchanged v s.
tauto.
+ assoc_put_in_front v1.
assoc_put_in_front v.
apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_unsigned; Nodup_nodup r0.
apply pfwd_sim_copy_signed_unsigned.
- 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.
apply not_In_mint_ptr. simpl map. simpl mint_ptr. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
apply fwd_sim_seq with (fun s st _ => (EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s) /\ uv_bound rk st u v s L) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
* rewrite /EGCD.C2 / EGCD.C3 in Hcond *.
rewrite /=.
local_Var_unchanged u s.
local_Var_unchanged v s.
local_Var_unchanged g s.
tauto.
* rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
local_Var_unchanged v s.
tauto.
apply fwd_sim_pcode_equiv with (v2 <- nat_e 1 ; v2 <- var_e v2 .-e var_e u)%seplog_expr%seplog_cmd; last by apply equivalent_pseudo_code_example2; Nodup_neq.
apply fwd_sim_seq with (fun s st _ => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([v2 ]_ s)%seplog_expr < Zbeta (L - 1) /\
0 <= ([u ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
rewrite /uv_bound in Hcond.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
local_Var_unchanged u s.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
split; first by move=> abs; rewrite abs u2Z_Z2u // in Hcond; omega.
repeat (split; first by tauto).
split; first by move: (Zbeta_0' L) => /= ?; omega.
omega.
+ assoc_put_in_front v2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_one_signed; Nodup_nodup r0.
apply pfwd_sim_one_signed.
- 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 List.map. by Nodup_not_In.
assoc_put_in_front u.
assoc_put_in_front v2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_multi_sub_s_u; Nodup_nodup r0.
apply pfwd_sim_multi_sub_s_u_wo_overflow.
- rewrite [Equality.sort _]/= in Hvars *. by Nodup_nodup O.
- 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; by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
assoc_put_in_front v3.
assoc_put_in_front v.
apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_unsigned; Nodup_nodup r0.
apply pfwd_sim_copy_signed_unsigned.
- 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.
apply not_In_mint_ptr. simpl map. simpl mint_ptr. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
apply fwd_sim_ifte => //.
- rewrite /inv_R => s st h [s_st_h Hcond] st' h' exec_asm; split.
+ eapply state_mint_invariant; [idtac | idtac | apply s_st_h | apply exec_asm] => //.
Disj_f_cdom2list Permutation_mints_regs.
rewrite [mips_frame.modified_regs _]/=.
Disj_remove_dup.
apply: nodup.nodup_disj. rewrite [List.app _ _]/=. by Nodup_nodup r0.
+ rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
- assoc_put_in_front u.
apply fwd_sim_b_multi_is_even.
+ 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 _]/= [List.map _ _]/=. by Nodup_not_In.
- apply fwd_sim_seq with (fun s st _ => ((EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s /\ EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\
uv_bound rk st u v s L) /\
([var_e u mode nat_e 2 =e nat_e 1 ]b_ s)%seplog_expr) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
rewrite /EGCD.C2 /EGCD.C3 /EGCD.uivi_init /uv_bound in Hcond *.
simpl.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
+ assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last by apply safe_termination_zero_signed; Nodup_nodup r0.
apply pfwd_sim_zero_signed.
- 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 List.map. by Nodup_not_In.
- apply fwd_sim_seq with (fun s st _ =>
((EGCD.C2 vu vv u v g s /\
EGCD.C3 vu vv u v g s /\ EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\
uv_bound rk st u v s L) /\
([var_e u mode nat_e 2 =e nat_e 1 ]b_ s)%seplog_expr) => //.
+ rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
rewrite /EGCD.C2 /EGCD.C3 /EGCD.uivi_init /uv_bound in Hcond *.
simpl.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
apply fwd_sim_pcode_equiv with (t2 <- nat_e 1 ; t2 <- .--e (var_e t2))%seplog_expr%seplog_cmd; last first.
eapply equivalent_pseudo_code_trans; by [apply equivalent_pseudo_code_example3 | apply equivalent_pseudo_code_example_assign].
apply fwd_sim_seq with (fun s st _ => ((EGCD.C2 vu vv u v g s /\
EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\ uv_bound rk st u v s L)) => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
rewrite /EGCD.C2 /EGCD.uivi_init /uv_bound in Hcond *.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
- assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_one_signed; Nodup_nodup r0.
apply pfwd_sim_one_signed.
- 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 List.map. by Nodup_not_In.
- assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_negate; Nodup_nodup r0.
apply pfwd_sim_negate.
- 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 List.map. by Nodup_not_In.
- apply fwd_sim_pcode_equiv with (t3 <- var_e v ; t3 <- .--e (var_e t3))%seplog_expr%seplog_cmd; last first.
eapply equivalent_pseudo_code_trans; by [apply equivalent_pseudo_code_example3 | apply equivalent_pseudo_code_example_assign].
apply fwd_sim_seq with (fun s st _ =>
((EGCD.C2 vu vv u v g s /\ EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\
uv_bound rk st u v s L)) => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
rewrite /EGCD.C2 /EGCD.uivi_init /uv_bound in Hcond *.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
- assoc_put_in_front t3.
assoc_put_in_front v.
apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_unsigned; Nodup_nodup r0.
apply pfwd_sim_copy_signed_unsigned.
- 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.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
- assoc_put_in_front t3.
apply pfwd_sim_fwd_sim; last by apply safe_termination_negate; Nodup_nodup r0.
apply pfwd_sim_negate.
- 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 List.map. by Nodup_not_In.
apply fwd_sim_seq with (fun s st _ =>
((EGCD.C2 vu vv u v g s /\ EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\
uv_bound rk st u v s L) ) => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
rewrite /EGCD.C2 /EGCD.uivi_init /uv_bound in Hcond *.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
- assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last by apply safe_termination_one_signed; Nodup_nodup r0.
apply pfwd_sim_one_signed.
- 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 List.map. by Nodup_not_In.
apply fwd_sim_seq with (fun s st _ =>
(EGCD.C2 vu vv u v g s /\ EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s) /\
uv_bound rk st u v s L) => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
rewrite /EGCD.C2 /EGCD.uivi_init /uv_bound in Hcond *.
repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
tauto.
- assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_zero_signed; Nodup_nodup r0.
apply pfwd_sim_zero_signed.
- 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 List.map. by Nodup_not_In.
- assoc_put_in_front t3.
assoc_put_in_front u.
apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_unsigned; Nodup_nodup r0.
apply pfwd_sim_copy_signed_unsigned.
- 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.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
Qed.