Library multi_is_zero_triple
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import ssreflect ssrbool.
Require Import machine_int multi_int.
Import MachineInt.
Require Import mips_seplog mips_contrib mips_tactics.
Require Import multi_is_even_prg.
Local Open Scope machine_int_scope.
Local Open Scope heap_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope nodup_scope.
Import expr_m.
Local Open Scope mips_expr_scope.
Import assert_m.
Local Open Scope mips_assert_scope.
Local Open Scope mips_cmd_scope.
Local Open Scope mips_hoare_scope.
Require Import multi_is_zero_prg.
Lemma multi_is_zero_triple :forall k x ret a0 k0, nodup(k, x, a0, k0, ret, r0) ->
forall nk X vx, length X = nk ->
u2Z vx + 4 * Z_of_nat nk < Zbeta 1 ->
{{ fun s h => u2Z [ k ]_s = Z_of_nat nk /\ [x]_s = vx /\ (var_e x |--> X) s h }}
multi_is_zero k x k0 a0 ret
{{ fun s h => u2Z [ k ]_s = Z_of_nat nk /\ [x]_s = vx /\ (var_e x |--> X) s h /\
((0 = Sum nk X -> [ret]_s = one32) /\
(0 < Sum nk X -> [ret]_s = zero32))}}.
Proof.
move=> k x ret a0 k0 Hregs nk X vx X_nk Hfit.
rewrite /multi_is_zero.
NextAddiu.
move=> s h [Hk [Hx mem]].
rewrite /wp_addiu.
repeat reg_upd.
repeat (split => //).
by Assert_upd.
NextAddiu.
move=> s h [[Hk [Hx mem]] Hk0].
rewrite /wp_addiu.
repeat reg_upd.
repeat (split => //).
by Assert_upd.
apply hoare_prop_m.hoare_while_invariant with (fun s h => exists i,
u2Z [ k ]_s = Z_of_nat nk /\ [x]_s = vx /\
u2Z [k0]_s = Z_of_nat i /\
(i <= nk)%nat /\
(var_e x |--> X) s h /\
(0 = Sum i X -> [ret]_s = one32) /\
(0 < Sum i X -> [ret]_s = zero32)
).
move=> s h /= H.
case: H => H Hret.
case: H => H Hk0.
case: H => Hk [Hx mem].
exists O.
repeat (split => //).
by rewrite Hk0 sext_Z2u // add_0 store.get_r0 u2Z_Z2u //.
by apply le_0_n.
move=> _.
apply u2Z_inj.
by rewrite Hret add_com store.get_r0 add_0 sext_Z2u //.
move=> s h [[i [Hk [Hx [Hk0 [i_nk [mem Hret]]]]]] Hk0'].
rewrite /= in Hk0'.
rewrite negb_involutive in Hk0'.
move/Zeq_boolP/u2Z_inj in Hk0'.
rewrite Hk0' in Hk0.
rewrite Hk0 in Hk.
apply Z_of_nat_inj in Hk.
subst i.
by repeat (split => //).
apply hoare_lwxs_back_alt'' with (fun s h => (exists i : nat,
u2Z [k ]_ s = Z_of_nat nk /\
[x ]_ s = vx /\
u2Z [k0 ]_ s = Z_of_nat i /\
(i < nk)%nat /\
[a0]_s = nth i X zero32 /\
(var_e x |--> X) s h /\
(0 = Sum (i) X -> [ret ]_ s = one32) /\
(0 < Sum (i) X -> [ret ]_ s = zero32))).
move=> s h [[i [Hk [Hx [Hk0 [i_nk [mem Hret]]]]]] Hk0'].
rewrite /= in Hk0'.
move/Zeq_boolP in Hk0'.
rewrite Hk Hk0 in Hk0'.
apply Z_of_nat_inj_neq in Hk0'.
exists (nth i X zero32); split.
- Decompose_32 X i X1 X2 HlenX1 HX'; last first.
rewrite X_nk.
omega.
Require Import mapstos.
rewrite HX' (decompose_equiv _ _ _ _ _ HlenX1)
in mem.
rewrite con_assoc_equiv in mem.
rewrite con_com_equiv in mem.
rewrite con_assoc_equiv in mem.
move: mem; apply monotony => // h'.
apply mapsto_ext => //.
by rewrite [mult]lock /= -lock shl_Z2u inj_mult Hk0 [Zmult]lock /= -lock Zmult_comm.
- rewrite /update_store_lwxs.
exists i.
repeat reg_upd; repeat (split; trivial).
omega.
by Assert_upd.
apply hoare_movn with (fun (s : store.t) (h : heap.t) =>
exists i : nat,
u2Z [k ]_ s = Z_of_nat nk /\
[x ]_ s = vx /\
u2Z [k0 ]_ s = Z_of_nat i /\
(i < nk)%nat /\
[a0 ]_ s = nth i X zero32 /\
(var_e x |--> X) s h /\
(0 = Sum (S i) X -> [ret ]_ s = one32) /\
(0 < Sum (S i) X -> [ret ]_ s = zero32)).
move=> s h [i [Hk [Hx [Hk0 [i_nk [Ha0 [mem Hret]]]]]]].
rewrite /wp_movn.
repeat reg_upd.
split; move=> Ha0'.
exists i.
repeat (split => //).
by Assert_upd.
move=> H; symmetry in H.
apply Sum_0_inv_new in H; last first.
rewrite X_nk.
omega.
rewrite (firstn_S zero32) in H; last first.
by rewrite X_nk.
rewrite rep_last in H.
apply app_inv in H; last first.
rewrite (len_firstn nk) //; last by omega.
by rewrite len_rep.
case: H => _ [H].
rewrite H in Ha0.
rewrite Ha0 in Ha0'.
rewrite /zero32 in Ha0'.
tauto.
exists i.
repeat reg_upd.
repeat (split => //).
move=> H.
apply (proj1 Hret).
symmetry in H.
apply Sum_0_inv_new in H; last first.
rewrite X_nk.
omega.
rewrite (firstn_S zero32) in H; last by rewrite X_nk.
rewrite rep_last in H.
apply app_inv in H; last first.
rewrite (len_firstn nk) //; last by omega.
by rewrite len_rep.
case: H => H _.
Lemma Sum_firstn : forall n i (X : list (int n)),
(i <= length X)%nat ->
Sum i X = Sum i (firstn i X).
Proof.
move=> n i X H.
rewrite -{1}(firstn_skipn i X).
symmetry.
apply Sum_beyond.
by rewrite (len_firstn (length X)) //.
Qed.
rewrite Sum_firstn; last first.
rewrite X_nk.
omega.
rewrite H.
by rewrite Sum_rep_0.
move=> H.
apply (proj2 Hret).
rewrite Sum_remove_last in H.
rewrite -Ha0 in H.
rewrite Ha0' in H.
rewrite u2Z_Z2u // Zmult_0_r in H.
omega.
apply hoare_addiu'.
move=> s h [i [Hk [Hx [Hk0 [i_nk [Ha0 [mem Hret]]]]]]].
rewrite /wp_addiu.
repeat reg_upd.
exists (S i).
repeat (split => //).
rewrite sext_Z2u // u2Z_add_Z2u //.
rewrite Z_S.
rewrite Hk0.
done.
rewrite Hk0.
rewrite -/(Zbeta 1).
move: (min_u2Z vx) => ?; omega.
by Assert_upd.
Qed.
Require Import ssreflect ssrbool.
Require Import machine_int multi_int.
Import MachineInt.
Require Import mips_seplog mips_contrib mips_tactics.
Require Import multi_is_even_prg.
Local Open Scope machine_int_scope.
Local Open Scope heap_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope nodup_scope.
Import expr_m.
Local Open Scope mips_expr_scope.
Import assert_m.
Local Open Scope mips_assert_scope.
Local Open Scope mips_cmd_scope.
Local Open Scope mips_hoare_scope.
Require Import multi_is_zero_prg.
Lemma multi_is_zero_triple :forall k x ret a0 k0, nodup(k, x, a0, k0, ret, r0) ->
forall nk X vx, length X = nk ->
u2Z vx + 4 * Z_of_nat nk < Zbeta 1 ->
{{ fun s h => u2Z [ k ]_s = Z_of_nat nk /\ [x]_s = vx /\ (var_e x |--> X) s h }}
multi_is_zero k x k0 a0 ret
{{ fun s h => u2Z [ k ]_s = Z_of_nat nk /\ [x]_s = vx /\ (var_e x |--> X) s h /\
((0 = Sum nk X -> [ret]_s = one32) /\
(0 < Sum nk X -> [ret]_s = zero32))}}.
Proof.
move=> k x ret a0 k0 Hregs nk X vx X_nk Hfit.
rewrite /multi_is_zero.
NextAddiu.
move=> s h [Hk [Hx mem]].
rewrite /wp_addiu.
repeat reg_upd.
repeat (split => //).
by Assert_upd.
NextAddiu.
move=> s h [[Hk [Hx mem]] Hk0].
rewrite /wp_addiu.
repeat reg_upd.
repeat (split => //).
by Assert_upd.
apply hoare_prop_m.hoare_while_invariant with (fun s h => exists i,
u2Z [ k ]_s = Z_of_nat nk /\ [x]_s = vx /\
u2Z [k0]_s = Z_of_nat i /\
(i <= nk)%nat /\
(var_e x |--> X) s h /\
(0 = Sum i X -> [ret]_s = one32) /\
(0 < Sum i X -> [ret]_s = zero32)
).
move=> s h /= H.
case: H => H Hret.
case: H => H Hk0.
case: H => Hk [Hx mem].
exists O.
repeat (split => //).
by rewrite Hk0 sext_Z2u // add_0 store.get_r0 u2Z_Z2u //.
by apply le_0_n.
move=> _.
apply u2Z_inj.
by rewrite Hret add_com store.get_r0 add_0 sext_Z2u //.
move=> s h [[i [Hk [Hx [Hk0 [i_nk [mem Hret]]]]]] Hk0'].
rewrite /= in Hk0'.
rewrite negb_involutive in Hk0'.
move/Zeq_boolP/u2Z_inj in Hk0'.
rewrite Hk0' in Hk0.
rewrite Hk0 in Hk.
apply Z_of_nat_inj in Hk.
subst i.
by repeat (split => //).
apply hoare_lwxs_back_alt'' with (fun s h => (exists i : nat,
u2Z [k ]_ s = Z_of_nat nk /\
[x ]_ s = vx /\
u2Z [k0 ]_ s = Z_of_nat i /\
(i < nk)%nat /\
[a0]_s = nth i X zero32 /\
(var_e x |--> X) s h /\
(0 = Sum (i) X -> [ret ]_ s = one32) /\
(0 < Sum (i) X -> [ret ]_ s = zero32))).
move=> s h [[i [Hk [Hx [Hk0 [i_nk [mem Hret]]]]]] Hk0'].
rewrite /= in Hk0'.
move/Zeq_boolP in Hk0'.
rewrite Hk Hk0 in Hk0'.
apply Z_of_nat_inj_neq in Hk0'.
exists (nth i X zero32); split.
- Decompose_32 X i X1 X2 HlenX1 HX'; last first.
rewrite X_nk.
omega.
Require Import mapstos.
rewrite HX' (decompose_equiv _ _ _ _ _ HlenX1)
in mem.
rewrite con_assoc_equiv in mem.
rewrite con_com_equiv in mem.
rewrite con_assoc_equiv in mem.
move: mem; apply monotony => // h'.
apply mapsto_ext => //.
by rewrite [mult]lock /= -lock shl_Z2u inj_mult Hk0 [Zmult]lock /= -lock Zmult_comm.
- rewrite /update_store_lwxs.
exists i.
repeat reg_upd; repeat (split; trivial).
omega.
by Assert_upd.
apply hoare_movn with (fun (s : store.t) (h : heap.t) =>
exists i : nat,
u2Z [k ]_ s = Z_of_nat nk /\
[x ]_ s = vx /\
u2Z [k0 ]_ s = Z_of_nat i /\
(i < nk)%nat /\
[a0 ]_ s = nth i X zero32 /\
(var_e x |--> X) s h /\
(0 = Sum (S i) X -> [ret ]_ s = one32) /\
(0 < Sum (S i) X -> [ret ]_ s = zero32)).
move=> s h [i [Hk [Hx [Hk0 [i_nk [Ha0 [mem Hret]]]]]]].
rewrite /wp_movn.
repeat reg_upd.
split; move=> Ha0'.
exists i.
repeat (split => //).
by Assert_upd.
move=> H; symmetry in H.
apply Sum_0_inv_new in H; last first.
rewrite X_nk.
omega.
rewrite (firstn_S zero32) in H; last first.
by rewrite X_nk.
rewrite rep_last in H.
apply app_inv in H; last first.
rewrite (len_firstn nk) //; last by omega.
by rewrite len_rep.
case: H => _ [H].
rewrite H in Ha0.
rewrite Ha0 in Ha0'.
rewrite /zero32 in Ha0'.
tauto.
exists i.
repeat reg_upd.
repeat (split => //).
move=> H.
apply (proj1 Hret).
symmetry in H.
apply Sum_0_inv_new in H; last first.
rewrite X_nk.
omega.
rewrite (firstn_S zero32) in H; last by rewrite X_nk.
rewrite rep_last in H.
apply app_inv in H; last first.
rewrite (len_firstn nk) //; last by omega.
by rewrite len_rep.
case: H => H _.
Lemma Sum_firstn : forall n i (X : list (int n)),
(i <= length X)%nat ->
Sum i X = Sum i (firstn i X).
Proof.
move=> n i X H.
rewrite -{1}(firstn_skipn i X).
symmetry.
apply Sum_beyond.
by rewrite (len_firstn (length X)) //.
Qed.
rewrite Sum_firstn; last first.
rewrite X_nk.
omega.
rewrite H.
by rewrite Sum_rep_0.
move=> H.
apply (proj2 Hret).
rewrite Sum_remove_last in H.
rewrite -Ha0 in H.
rewrite Ha0' in H.
rewrite u2Z_Z2u // Zmult_0_r in H.
omega.
apply hoare_addiu'.
move=> s h [i [Hk [Hx [Hk0 [i_nk [Ha0 [mem Hret]]]]]]].
rewrite /wp_addiu.
repeat reg_upd.
exists (S i).
repeat (split => //).
rewrite sext_Z2u // u2Z_add_Z2u //.
rewrite Z_S.
rewrite Hk0.
done.
rewrite Hk0.
rewrite -/(Zbeta 1).
move: (min_u2Z vx) => ?; omega.
by Assert_upd.
Qed.