Library begcd_mips_subtract
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 pick_sign_prg.
Require Import multi_add_signed_unsigned_prg.
Require Import multi_sub_signed_unsigned_prg.
Require Import begcd_mips_init.
Require Import multi_add_signed_unsigned_simu.
Require Import 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 assoc_scope.
Local Open Scope nodup_scope.
Definition subtract_mips rk ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 a7 a8 :=
((multi_sub_signed_signed_signed rk rt1 ru1 rv1 a0 a1 a2 a3 a4 a5 a6 a7 a8;
multi_sub_signed_signed_signed rk rt2 ru2 rv2 a0 a1 a2 a3 a4 a5 a6 a7 a8;
multi_sub_signed_signed_signed rk rt3 ru3 rv3 a0 a1 a2 a3 a4 a5 a6 a7 a8);
(pick_sign rt1 a0 a1;
while.ifte (blez a1)
(multi_add_s_u rk rt1 rv a0 a1 a2 a3 a4 a5 a6 ;
multi_sub_s_u rk rt2 ru a0 a1 a2 a3 a4 a5 a6)
nop))%mips_cmd.
Lemma fwd_sim_begcd_subtract : 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 a7 a8,
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,a7,a8,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 /\
(Zodd ([u ]_ s) \/ Zodd ([v ]_ s)) /\
EGCD.CVectors u v u1 u2 u3 v1 v2 v3 t1 t2 t3 s /\
(0 <= [t3 ]_ s ->
Zgcd vu vv = ([g ]_ s) * Zgcd ([t3 ]_ s) ([v3 ]_ s) /\
Zodd ([u3 ]_ s) /\ [u3 ]_ s = [t3 ]_ s) /\
([t3 ]_ s < 0 ->
Zgcd vu vv = ([g ]_ s) * Zgcd ([u3 ]_ s) ([t3 ]_ s) /\
Zodd ([v3 ]_ s) /\
[v3 ]_ s = - [t3 ]_ s) /\
EGCD.uivi_bounds u v u1 v1 u2 v2 u3 v3 s /\
EGCD.ti_bounds u v t1 t2 t3 s /\ EGCD.C5 u3 v3 s) /\
uv_bound rk st u v s L)%seplog_expr
(EGCD.TAOCP.subtract u v u1 u2 u3 v1 v2 v3 t1 t2 t3)
(subtract_mips rk ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 a7 a8).
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 a7 a8 Hvars Hregs
Hvu Hvv.
rewrite /EGCD.TAOCP.subtract /subtract_mips.
apply fwd_sim_seq with (fun s st _ =>
uv_bound rk st u v s L /\
([t1]_s <= 0 ->
0 <= [t1 ]_ s + [v ]_ s <= [v ]_ s /\
- [u ]_ s <= [t2 ]_ s - [u ]_ s <= 0))%seplog_expr => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
rewrite /uv_bound in Hcond.
split.
local_Var_unchanged u s.
local_Var_unchanged v s.
tauto.
move: (EGCD.TAOCP2.begcd_subtract_part1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ 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)) => _.
move/(_ _ _ exec_pseudo).
move=> H.
move=> Ht1.
tauto.
- 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 ([u2 ]_ s)%seplog_expr < Zbeta (L - 1) /\
Zabs ([v2 ]_ s)%seplog_expr < Zbeta (L - 1) /\
Zabs ([u3 ]_ s)%seplog_expr < Zbeta (L - 1) /\
Zabs ([v3 ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
rewrite /uv_bound in Hcond.
split.
move=> abs; rewrite abs u2Z_Z2u // in Hcond.
omega.
repeat (split; first by tauto).
rewrite /EGCD.uivi_bounds in Hcond.
local_Var_unchanged u2 s.
local_Var_unchanged v2 s.
local_Var_unchanged u3 s.
local_Var_unchanged v3 s.
rewrite Zabs_non_eq; last by omega.
rewrite Zabs_non_eq; last by omega.
rewrite Zabs_eq; last by omega.
rewrite Zabs_eq; last by omega.
omega.
- apply fwd_sim_stren with (fun s st _ => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([u1 ]_ s)%seplog_expr < Zbeta (L - 1) /\
Zabs ([v1 ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr.
move=> s st h H.
rewrite /uv_bound in H.
split.
move=> abs; rewrite abs u2Z_Z2u // in H; omega.
repeat (split; first by tauto).
rewrite /EGCD.uivi_bounds in H.
rewrite Zabs_eq; last by omega.
rewrite Zabs_eq; last by omega.
omega.
assoc_put_in_front v1.
assoc_put_in_front u1.
assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last by apply safe_termination_multi_sub_signed_signed_signed; Nodup_nodup r0.
apply pfwd_sim_multi_sub_signed_signed_signed_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.
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.
- 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 _ => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([u3 ]_ s)%seplog_expr < Zbeta (L - 1) /\
Zabs ([v3 ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
rewrite /uv_bound in Hcond.
split.
move=> abs; rewrite abs u2Z_Z2u // in Hcond.
tauto.
repeat (split; first by tauto).
rewrite /EGCD.uivi_bounds in Hcond.
local_Var_unchanged u3 s.
local_Var_unchanged v3 s.
tauto.
- apply fwd_sim_stren with (fun s st _ =>
([rk ]_ st)%mips_expr <> zero32 /\
u2Z ([rk ]_ st)%mips_expr < 2 ^^ 31 /\
L <> 0%nat /\
L = Zabs_nat (u2Z ([rk ]_ st)%mips_expr) /\
Zabs ([u2 ]_ s)%seplog_expr < Zbeta (L - 1) /\
Zabs ([v2 ]_ s)%seplog_expr < Zbeta (L - 1)).
move=> s st h; tauto.
assoc_put_in_front v2.
assoc_put_in_front u2.
assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_multi_sub_signed_signed_signed; Nodup_nodup r0.
apply pfwd_sim_multi_sub_signed_signed_signed_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.
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.
- 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 u3.
assoc_put_in_front t3.
apply pfwd_sim_fwd_sim; last by apply safe_termination_multi_sub_signed_signed_signed; Nodup_nodup r0.
apply pfwd_sim_multi_sub_signed_signed_signed_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.
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.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [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 t1.
by apply fwd_sim_b_pick_sign_lez.
- 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 ([t2 ]_ 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.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
rewrite /uv_bound in Hcond.
split.
move=> abs; rewrite abs u2Z_Z2u // in Hcond.
omega.
local_Var_unchanged t2 s.
local_Var_unchanged u s.
repeat (split; first by tauto).
case: Hcond => Hcond [_] /=.
move/Zge_boolP.
rewrite /= in Hcond.
move=> H.
rewrite Zabs_eq; last by omega.
omega.
+ apply fwd_sim_stren with (fun s st _ => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([t1 ]_ s)%seplog_expr < Zbeta (L - 1) /\
0 <= ([v ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr.
move=> s st h H.
rewrite /uv_bound in H.
split.
move=> abs; rewrite abs u2Z_Z2u // in H.
omega.
repeat (split; first by tauto).
rewrite Zabs_non_eq; last first.
case: H => _ [_] /=.
move/Zge_boolP.
by move/Zge_le.
omega.
assoc_put_in_front v.
assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last first.
by apply safe_termination_multi_add_s_u; Nodup_nodup r0.
apply pfwd_sim_multi_add_s_u_wo_overflow.
- rewrite [Equality.sort _]/= /bipl.var.v 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 u.
assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last first.
by apply safe_termination_multi_sub_s_u; Nodup_nodup r0.
apply pfwd_sim_multi_sub_s_u_wo_overflow.
- rewrite [Equality.sort _]/= /bipl.var.v 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.
- by apply fwd_sim_nop.
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 pick_sign_prg.
Require Import multi_add_signed_unsigned_prg.
Require Import multi_sub_signed_unsigned_prg.
Require Import begcd_mips_init.
Require Import multi_add_signed_unsigned_simu.
Require Import 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 assoc_scope.
Local Open Scope nodup_scope.
Definition subtract_mips rk ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 a7 a8 :=
((multi_sub_signed_signed_signed rk rt1 ru1 rv1 a0 a1 a2 a3 a4 a5 a6 a7 a8;
multi_sub_signed_signed_signed rk rt2 ru2 rv2 a0 a1 a2 a3 a4 a5 a6 a7 a8;
multi_sub_signed_signed_signed rk rt3 ru3 rv3 a0 a1 a2 a3 a4 a5 a6 a7 a8);
(pick_sign rt1 a0 a1;
while.ifte (blez a1)
(multi_add_s_u rk rt1 rv a0 a1 a2 a3 a4 a5 a6 ;
multi_sub_s_u rk rt2 ru a0 a1 a2 a3 a4 a5 a6)
nop))%mips_cmd.
Lemma fwd_sim_begcd_subtract : 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 a7 a8,
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,a7,a8,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 /\
(Zodd ([u ]_ s) \/ Zodd ([v ]_ s)) /\
EGCD.CVectors u v u1 u2 u3 v1 v2 v3 t1 t2 t3 s /\
(0 <= [t3 ]_ s ->
Zgcd vu vv = ([g ]_ s) * Zgcd ([t3 ]_ s) ([v3 ]_ s) /\
Zodd ([u3 ]_ s) /\ [u3 ]_ s = [t3 ]_ s) /\
([t3 ]_ s < 0 ->
Zgcd vu vv = ([g ]_ s) * Zgcd ([u3 ]_ s) ([t3 ]_ s) /\
Zodd ([v3 ]_ s) /\
[v3 ]_ s = - [t3 ]_ s) /\
EGCD.uivi_bounds u v u1 v1 u2 v2 u3 v3 s /\
EGCD.ti_bounds u v t1 t2 t3 s /\ EGCD.C5 u3 v3 s) /\
uv_bound rk st u v s L)%seplog_expr
(EGCD.TAOCP.subtract u v u1 u2 u3 v1 v2 v3 t1 t2 t3)
(subtract_mips rk ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 a7 a8).
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 a7 a8 Hvars Hregs
Hvu Hvv.
rewrite /EGCD.TAOCP.subtract /subtract_mips.
apply fwd_sim_seq with (fun s st _ =>
uv_bound rk st u v s L /\
([t1]_s <= 0 ->
0 <= [t1 ]_ s + [v ]_ s <= [v ]_ s /\
- [u ]_ s <= [t2 ]_ s - [u ]_ s <= 0))%seplog_expr => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
rewrite /uv_bound.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
rewrite /uv_bound in Hcond.
split.
local_Var_unchanged u s.
local_Var_unchanged v s.
tauto.
move: (EGCD.TAOCP2.begcd_subtract_part1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ 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)) => _.
move/(_ _ _ exec_pseudo).
move=> H.
move=> Ht1.
tauto.
- 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 ([u2 ]_ s)%seplog_expr < Zbeta (L - 1) /\
Zabs ([v2 ]_ s)%seplog_expr < Zbeta (L - 1) /\
Zabs ([u3 ]_ s)%seplog_expr < Zbeta (L - 1) /\
Zabs ([v3 ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
rewrite /uv_bound in Hcond.
split.
move=> abs; rewrite abs u2Z_Z2u // in Hcond.
omega.
repeat (split; first by tauto).
rewrite /EGCD.uivi_bounds in Hcond.
local_Var_unchanged u2 s.
local_Var_unchanged v2 s.
local_Var_unchanged u3 s.
local_Var_unchanged v3 s.
rewrite Zabs_non_eq; last by omega.
rewrite Zabs_non_eq; last by omega.
rewrite Zabs_eq; last by omega.
rewrite Zabs_eq; last by omega.
omega.
- apply fwd_sim_stren with (fun s st _ => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([u1 ]_ s)%seplog_expr < Zbeta (L - 1) /\
Zabs ([v1 ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr.
move=> s st h H.
rewrite /uv_bound in H.
split.
move=> abs; rewrite abs u2Z_Z2u // in H; omega.
repeat (split; first by tauto).
rewrite /EGCD.uivi_bounds in H.
rewrite Zabs_eq; last by omega.
rewrite Zabs_eq; last by omega.
omega.
assoc_put_in_front v1.
assoc_put_in_front u1.
assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last by apply safe_termination_multi_sub_signed_signed_signed; Nodup_nodup r0.
apply pfwd_sim_multi_sub_signed_signed_signed_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.
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.
- 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 _ => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([u3 ]_ s)%seplog_expr < Zbeta (L - 1) /\
Zabs ([v3 ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
rewrite /uv_bound in Hcond.
split.
move=> abs; rewrite abs u2Z_Z2u // in Hcond.
tauto.
repeat (split; first by tauto).
rewrite /EGCD.uivi_bounds in Hcond.
local_Var_unchanged u3 s.
local_Var_unchanged v3 s.
tauto.
- apply fwd_sim_stren with (fun s st _ =>
([rk ]_ st)%mips_expr <> zero32 /\
u2Z ([rk ]_ st)%mips_expr < 2 ^^ 31 /\
L <> 0%nat /\
L = Zabs_nat (u2Z ([rk ]_ st)%mips_expr) /\
Zabs ([u2 ]_ s)%seplog_expr < Zbeta (L - 1) /\
Zabs ([v2 ]_ s)%seplog_expr < Zbeta (L - 1)).
move=> s st h; tauto.
assoc_put_in_front v2.
assoc_put_in_front u2.
assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last by apply safe_termination_multi_sub_signed_signed_signed; Nodup_nodup r0.
apply pfwd_sim_multi_sub_signed_signed_signed_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.
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.
- 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 u3.
assoc_put_in_front t3.
apply pfwd_sim_fwd_sim; last by apply safe_termination_multi_sub_signed_signed_signed; Nodup_nodup r0.
apply pfwd_sim_multi_sub_signed_signed_signed_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.
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.
- apply/seq_ext.inP.
Not_In_dom2list.
apply not_In_mint_ptr. rewrite [mint_ptr _]/= [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 t1.
by apply fwd_sim_b_pick_sign_lez.
- 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 ([t2 ]_ 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.
have <- : ([rk]_st = [rk]_ st')%mips_expr.
mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
rewrite /uv_bound in Hcond.
split.
move=> abs; rewrite abs u2Z_Z2u // in Hcond.
omega.
local_Var_unchanged t2 s.
local_Var_unchanged u s.
repeat (split; first by tauto).
case: Hcond => Hcond [_] /=.
move/Zge_boolP.
rewrite /= in Hcond.
move=> H.
rewrite Zabs_eq; last by omega.
omega.
+ apply fwd_sim_stren with (fun s st _ => [rk ]_ st <> zero32 /\
u2Z ([rk ]_ st) < 2 ^^ 31 /\
L <> O /\
L = Zabs_nat (u2Z ([rk ]_ st)) /\
Zabs ([t1 ]_ s)%seplog_expr < Zbeta (L - 1) /\
0 <= ([v ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr.
move=> s st h H.
rewrite /uv_bound in H.
split.
move=> abs; rewrite abs u2Z_Z2u // in H.
omega.
repeat (split; first by tauto).
rewrite Zabs_non_eq; last first.
case: H => _ [_] /=.
move/Zge_boolP.
by move/Zge_le.
omega.
assoc_put_in_front v.
assoc_put_in_front t1.
apply pfwd_sim_fwd_sim; last first.
by apply safe_termination_multi_add_s_u; Nodup_nodup r0.
apply pfwd_sim_multi_add_s_u_wo_overflow.
- rewrite [Equality.sort _]/= /bipl.var.v 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 u.
assoc_put_in_front t2.
apply pfwd_sim_fwd_sim; last first.
by apply safe_termination_multi_sub_s_u; Nodup_nodup r0.
apply pfwd_sim_multi_sub_s_u_wo_overflow.
- rewrite [Equality.sort _]/= /bipl.var.v 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.
- by apply fwd_sim_nop.
Qed.