Library mips_bipl
Require Import ssreflect ssrbool eqtype.
Require Import ZArith_ext Lists_ext.
Require Import machine_int.
Import MachineInt.
Require Import ZArith_ext Lists_ext.
Require Import machine_int.
Import MachineInt.
This file provides:
- a definition of MIPS registers
- a module for "stores" (register files)
- a module for a language for expression built out of registers
- a module fot the language of assertions of Separation logic
General purpose registers
Inductive reg : Set :=
| r0 : reg
| reg_at : reg
| reg_v0 : reg
| reg_v1 : reg
| reg_a0 : reg
| reg_a1 : reg
| reg_a2 : reg
| reg_a3 : reg
| reg_t0 : reg
| reg_t1 : reg
| reg_t2 : reg
| reg_t3 : reg
| reg_t4 : reg
| reg_t5 : reg
| reg_t6 : reg
| reg_t7 : reg
| reg_t8 : reg
| reg_t9 : reg
| reg_s0 : reg
| reg_s1 : reg
| reg_s2 : reg
| reg_s3 : reg
| reg_s4 : reg
| reg_s5 : reg
| reg_s6 : reg
| reg_s7 : reg
| reg_k0 : reg
| reg_k1 : reg
| reg_gp : reg
| reg_sp : reg
| reg_fp : reg
| reg_ra : reg.
Definition regP (r1 r2 : reg) : bool :=
match (r1, r2) with
| (r0, r0) => true
| (reg_at, reg_at) => true
| (reg_v0, reg_v0) => true
| (reg_v1, reg_v1) => true
| (reg_a0, reg_a0) => true
| (reg_a1, reg_a1) => true
| (reg_a2, reg_a2) => true
| (reg_a3, reg_a3) => true
| (reg_t0, reg_t0) => true
| (reg_t1, reg_t1) => true
| (reg_t2, reg_t2) => true
| (reg_t3, reg_t3) => true
| (reg_t4, reg_t4) => true
| (reg_t5, reg_t5) => true
| (reg_t6, reg_t6) => true
| (reg_t7, reg_t7) => true
| (reg_t8, reg_t8) => true
| (reg_t9, reg_t9) => true
| (reg_s0, reg_s0) => true
| (reg_s1, reg_s1) => true
| (reg_s2, reg_s2) => true
| (reg_s3, reg_s3) => true
| (reg_s4, reg_s4) => true
| (reg_s5, reg_s5) => true
| (reg_s6, reg_s6) => true
| (reg_s7, reg_s7) => true
| (reg_k0, reg_k0) => true
| (reg_k1, reg_k1) => true
| (reg_gp, reg_gp) => true
| (reg_sp, reg_sp) => true
| (reg_fp, reg_fp) => true
| (reg_ra, reg_ra) => true
| _ => false
end.
Lemma regP_eq : forall n m, regP n m -> n = m.
Proof. by case; case. Qed.
Lemma regP_refl : forall n, regP n n.
Proof. by case. Qed.
Lemma eqregP : Equality.axiom regP.
Proof. move=> n m. apply: (iffP idP); move: n m; by case; case. Qed.
Canonical Structure reg_eqMixin := EqMixin eqregP.
Canonical Structure reg_eqType := Eval hnf in EqType _ reg_eqMixin.
Module store.
Definition var := reg.
Definition val := int 32.
| r0 : reg
| reg_at : reg
| reg_v0 : reg
| reg_v1 : reg
| reg_a0 : reg
| reg_a1 : reg
| reg_a2 : reg
| reg_a3 : reg
| reg_t0 : reg
| reg_t1 : reg
| reg_t2 : reg
| reg_t3 : reg
| reg_t4 : reg
| reg_t5 : reg
| reg_t6 : reg
| reg_t7 : reg
| reg_t8 : reg
| reg_t9 : reg
| reg_s0 : reg
| reg_s1 : reg
| reg_s2 : reg
| reg_s3 : reg
| reg_s4 : reg
| reg_s5 : reg
| reg_s6 : reg
| reg_s7 : reg
| reg_k0 : reg
| reg_k1 : reg
| reg_gp : reg
| reg_sp : reg
| reg_fp : reg
| reg_ra : reg.
Definition regP (r1 r2 : reg) : bool :=
match (r1, r2) with
| (r0, r0) => true
| (reg_at, reg_at) => true
| (reg_v0, reg_v0) => true
| (reg_v1, reg_v1) => true
| (reg_a0, reg_a0) => true
| (reg_a1, reg_a1) => true
| (reg_a2, reg_a2) => true
| (reg_a3, reg_a3) => true
| (reg_t0, reg_t0) => true
| (reg_t1, reg_t1) => true
| (reg_t2, reg_t2) => true
| (reg_t3, reg_t3) => true
| (reg_t4, reg_t4) => true
| (reg_t5, reg_t5) => true
| (reg_t6, reg_t6) => true
| (reg_t7, reg_t7) => true
| (reg_t8, reg_t8) => true
| (reg_t9, reg_t9) => true
| (reg_s0, reg_s0) => true
| (reg_s1, reg_s1) => true
| (reg_s2, reg_s2) => true
| (reg_s3, reg_s3) => true
| (reg_s4, reg_s4) => true
| (reg_s5, reg_s5) => true
| (reg_s6, reg_s6) => true
| (reg_s7, reg_s7) => true
| (reg_k0, reg_k0) => true
| (reg_k1, reg_k1) => true
| (reg_gp, reg_gp) => true
| (reg_sp, reg_sp) => true
| (reg_fp, reg_fp) => true
| (reg_ra, reg_ra) => true
| _ => false
end.
Lemma regP_eq : forall n m, regP n m -> n = m.
Proof. by case; case. Qed.
Lemma regP_refl : forall n, regP n n.
Proof. by case. Qed.
Lemma eqregP : Equality.axiom regP.
Proof. move=> n m. apply: (iffP idP); move: n m; by case; case. Qed.
Canonical Structure reg_eqMixin := EqMixin eqregP.
Canonical Structure reg_eqType := Eval hnf in EqType _ reg_eqMixin.
Module store.
Definition var := reg.
Definition val := int 32.
register file
The SmartMIPS multiplier is a set of registers called ACX, HI, and
LO that has been designed to enhance cryptographic computations. HI
and LO are 32 bits long; ACX is only known to be at least 8 bits
long. We formalize the multiplier as an abstract date type
m with three lookup functions acx,
hi, and lo that return respectively
a machine integer of length at list 8 bits and machine integers of
length 32 bits.
Definition t := (rf * (int acx_size * (int 32 * int 32)))%type.
Lemma acx_size_min : (8 <= acx_size)%nat. Proof. done. Qed.
Definition acx (s : t) := match s with (_, (a, _)) => a end.
Definition hi (s : t) := match s with (_, (_, (b, _))) => b end.
Definition lo (s : t) := match s with (_, (_, (_, c))) => c end.
Fixpoint get' (r : reg) (s : rf) : val :=
match s with
| nil => zero32
| (r', i) :: tl => if r == r' then i else get' r tl
end.
Definition get r (s : t) : val :=
match s with (s, _) => if r == r0 then zero32 else get' r s end.
Fixpoint upd' (r : reg) (i : int 32) (s : rf) : rf :=
match s with
| nil => (r, i) :: nil
| (r',i') :: tl => if r == r' then (r,i) :: tl else (r',i') :: upd' r i tl
end.
Definition upd r i (s : t) : t :=
match s with
(s, m) => if r == r0 then (s, m) else (upd' r i s, m)
end.
Lemma get_upd_p : forall st x y z, x <> y -> get' x (upd' y z st) = get' x st.
Proof.
elim => //.
- move=> x y z H /=.
have [->//] : x == y = false.
apply/negP. move/eqregP. done.
- move=> [a b] l Hst x y z Hxy /=.
have Hxy' : x == y = false.
apply/negP. move/eqregP. done.
have [H1 | H1] : x == a \/ x == a = false by case (x == a); auto.
+ rewrite H1.
have [H2 | H2] : y == a \/ y == a = false by case (y == a); auto.
* rewrite H2 /=.
have H3 : x == y.
case/eqregP:H1. case/eqregP: H2. move=> -> -> //.
rewrite H3 // in Hxy'.
* rewrite H2 /= H1 //.
+ rewrite H1.
have [H2 | H2] : y == a \/ y == a = false by case (y == a); auto.
* rewrite H2 /= Hxy' //.
* rewrite H2 /= H1; by apply Hst => //.
Qed.
Lemma get_upd : forall x y z st, x <> y -> get x (upd y z st) = get x st.
Proof.
move=> x y z [st mu] Hxy.
rewrite /get /upd.
case/orP : (orbN (x == r0)) => H1.
- rewrite H1 //.
case/orP : (orbN (y == r0)) => H2.
rewrite H2 //.
move/negbTE : H2 => H2.
rewrite H2 //.
- move/negbTE : H1 => H1.
rewrite H1.
case/orP : (orbN (y == r0)) => H2.
+ rewrite H2 //.
+ move/negbTE : H2 => H2.
by rewrite H2 get_upd_p.
Qed.
Lemma get_upd_p' : forall st w z , get' w (upd' w z st) = z.
Proof.
elim=> //=.
- move=> *; rewrite eq_refl //.
- move=> [a b] /= l Hst w z.
case/orP : (orbN (w == a)) => H1.
+ rewrite H1 //= eq_refl //.
+ move/negbTE : H1 => H1.
rewrite H1 /= H1; by apply Hst.
Qed.
Lemma get_upd' : forall x z st, x <> r0 -> get x (upd x z st) = z.
Proof.
move=> x z [st mu] H.
rewrite /get /upd.
have -> : x == r0 = false.
apply/negP. move/eqP. done.
apply get_upd_p'.
Qed.
Lemma upd_upd_p : forall st x z z', upd' x z' (upd' x z st) = upd' x z' st.
Proof.
elim.
- move=> x z z' /=.
by rewrite eqxx.
- move=> [hd hd'] tl IH x z z' /=.
case/orP : (orbN (x == hd)) => Htmp.
+ by rewrite Htmp /= eqxx.
+ by rewrite (negbTE Htmp) /= (negbTE Htmp) /= IH.
Qed.
Lemma upd_upd_eq : forall x z z' st,
upd x z' (upd x z st) = upd x z' st.
Proof.
move=> x z z' [st mu].
rewrite /upd.
case/orP : (orbN (x == r0)) => H1.
- rewrite H1 //.
- move/negbTE : H1 => H1.
rewrite H1.
by rewrite upd_upd_p.
Qed.
Lemma acx_size_min : (8 <= acx_size)%nat. Proof. done. Qed.
Definition acx (s : t) := match s with (_, (a, _)) => a end.
Definition hi (s : t) := match s with (_, (_, (b, _))) => b end.
Definition lo (s : t) := match s with (_, (_, (_, c))) => c end.
Fixpoint get' (r : reg) (s : rf) : val :=
match s with
| nil => zero32
| (r', i) :: tl => if r == r' then i else get' r tl
end.
Definition get r (s : t) : val :=
match s with (s, _) => if r == r0 then zero32 else get' r s end.
Fixpoint upd' (r : reg) (i : int 32) (s : rf) : rf :=
match s with
| nil => (r, i) :: nil
| (r',i') :: tl => if r == r' then (r,i) :: tl else (r',i') :: upd' r i tl
end.
Definition upd r i (s : t) : t :=
match s with
(s, m) => if r == r0 then (s, m) else (upd' r i s, m)
end.
Lemma get_upd_p : forall st x y z, x <> y -> get' x (upd' y z st) = get' x st.
Proof.
elim => //.
- move=> x y z H /=.
have [->//] : x == y = false.
apply/negP. move/eqregP. done.
- move=> [a b] l Hst x y z Hxy /=.
have Hxy' : x == y = false.
apply/negP. move/eqregP. done.
have [H1 | H1] : x == a \/ x == a = false by case (x == a); auto.
+ rewrite H1.
have [H2 | H2] : y == a \/ y == a = false by case (y == a); auto.
* rewrite H2 /=.
have H3 : x == y.
case/eqregP:H1. case/eqregP: H2. move=> -> -> //.
rewrite H3 // in Hxy'.
* rewrite H2 /= H1 //.
+ rewrite H1.
have [H2 | H2] : y == a \/ y == a = false by case (y == a); auto.
* rewrite H2 /= Hxy' //.
* rewrite H2 /= H1; by apply Hst => //.
Qed.
Lemma get_upd : forall x y z st, x <> y -> get x (upd y z st) = get x st.
Proof.
move=> x y z [st mu] Hxy.
rewrite /get /upd.
case/orP : (orbN (x == r0)) => H1.
- rewrite H1 //.
case/orP : (orbN (y == r0)) => H2.
rewrite H2 //.
move/negbTE : H2 => H2.
rewrite H2 //.
- move/negbTE : H1 => H1.
rewrite H1.
case/orP : (orbN (y == r0)) => H2.
+ rewrite H2 //.
+ move/negbTE : H2 => H2.
by rewrite H2 get_upd_p.
Qed.
Lemma get_upd_p' : forall st w z , get' w (upd' w z st) = z.
Proof.
elim=> //=.
- move=> *; rewrite eq_refl //.
- move=> [a b] /= l Hst w z.
case/orP : (orbN (w == a)) => H1.
+ rewrite H1 //= eq_refl //.
+ move/negbTE : H1 => H1.
rewrite H1 /= H1; by apply Hst.
Qed.
Lemma get_upd' : forall x z st, x <> r0 -> get x (upd x z st) = z.
Proof.
move=> x z [st mu] H.
rewrite /get /upd.
have -> : x == r0 = false.
apply/negP. move/eqP. done.
apply get_upd_p'.
Qed.
Lemma upd_upd_p : forall st x z z', upd' x z' (upd' x z st) = upd' x z' st.
Proof.
elim.
- move=> x z z' /=.
by rewrite eqxx.
- move=> [hd hd'] tl IH x z z' /=.
case/orP : (orbN (x == hd)) => Htmp.
+ by rewrite Htmp /= eqxx.
+ by rewrite (negbTE Htmp) /= (negbTE Htmp) /= IH.
Qed.
Lemma upd_upd_eq : forall x z z' st,
upd x z' (upd x z st) = upd x z' st.
Proof.
move=> x z z' [st mu].
rewrite /upd.
case/orP : (orbN (x == r0)) => H1.
- rewrite H1 //.
- move/negbTE : H1 => H1.
rewrite H1.
by rewrite upd_upd_p.
Qed.
r0 always evaluates to zero
r0 is invariant
Lemma upd_r0 : forall s x, upd r0 x s = s.
Proof. move=> [s mu] x. rewrite /upd eqtype.eq_refl //. Qed.
Lemma acx_upd : forall r v s, acx (upd r v s) = acx s.
Proof. move=> r v [s [a [h l]]] /=; case/orP: (orbN (r == r0));
[move=> -> // | move/negbTE; move=> -> //]. Qed.
Lemma hi_upd : forall r v s, hi (upd r v s) = hi s.
Proof. move=> r v [s [a [h l]]] /=; case/orP: (orbN (r == r0));
[move=> -> // | move/negbTE; move=> -> //]. Qed.
Lemma lo_upd : forall r v s, lo (upd r v s) = lo s.
Proof. move=> r v [s [a [h l]]] /=; case/orP: (orbN (r == r0));
[move=> -> // | move/negbTE; move=> -> //]. Qed.
Proof. move=> [s mu] x. rewrite /upd eqtype.eq_refl //. Qed.
Lemma acx_upd : forall r v s, acx (upd r v s) = acx s.
Proof. move=> r v [s [a [h l]]] /=; case/orP: (orbN (r == r0));
[move=> -> // | move/negbTE; move=> -> //]. Qed.
Lemma hi_upd : forall r v s, hi (upd r v s) = hi s.
Proof. move=> r v [s [a [h l]]] /=; case/orP: (orbN (r == r0));
[move=> -> // | move/negbTE; move=> -> //]. Qed.
Lemma lo_upd : forall r v s, lo (upd r v s) = lo s.
Proof. move=> r v [s [a [h l]]] /=; case/orP: (orbN (r == r0));
[move=> -> // | move/negbTE; move=> -> //]. Qed.
mthi
Definition mthi_op (x : int 32) (s : t) : t :=
match s with (s, (a, (b, c))) => (s, (a, (x, c))) end.
Lemma acx_mthi_op: forall s a, acx (mthi_op a s) = acx s.
Proof. move=> [s [a [l h] ]] n //=. Qed.
Lemma hi_mthi_op: forall m a, hi (mthi_op a m) = a.
Proof. move=> [s [a [l h] ]] n //=. Qed.
Lemma lo_mthi_op : forall m a, lo (mthi_op a m) = lo m.
Proof. move=> [_ [a [l h] ]] n //=. Qed.
match s with (s, (a, (b, c))) => (s, (a, (x, c))) end.
Lemma acx_mthi_op: forall s a, acx (mthi_op a s) = acx s.
Proof. move=> [s [a [l h] ]] n //=. Qed.
Lemma hi_mthi_op: forall m a, hi (mthi_op a m) = a.
Proof. move=> [s [a [l h] ]] n //=. Qed.
Lemma lo_mthi_op : forall m a, lo (mthi_op a m) = lo m.
Proof. move=> [_ [a [l h] ]] n //=. Qed.
mtlo
Definition mtlo_op (x : int 32) (m : t) : t :=
match m with (s, (a, (b, c))) => (s, (a, (b, x))) end.
Lemma acx_mtlo_op: forall m a, acx (mtlo_op a m) = acx m.
Proof. move=> [_ [a [l h] ]] n //=. Qed.
Lemma hi_mtlo_op: forall m a, hi (mtlo_op a m) = hi m.
Proof. move=> [_ [a [l h] ]] n //=. Qed.
Lemma lo_mtlo_op: forall m a, lo (mtlo_op a m) = a.
Proof. move=> [_ [a [l h] ]] n //=. Qed.
match m with (s, (a, (b, c))) => (s, (a, (b, x))) end.
Lemma acx_mtlo_op: forall m a, acx (mtlo_op a m) = acx m.
Proof. move=> [_ [a [l h] ]] n //=. Qed.
Lemma hi_mtlo_op: forall m a, hi (mtlo_op a m) = hi m.
Proof. move=> [_ [a [l h] ]] n //=. Qed.
Lemma lo_mtlo_op: forall m a, lo (mtlo_op a m) = a.
Proof. move=> [_ [a [l h] ]] n //=. Qed.
interpretation of the multiplier as an unsigned integer
Definition utoZ s :=
let acx_reg := acx s in
let (hi_reg, lo_reg) := (hi s, lo s) in
u2Z acx_reg * Zbeta 2 + u2Z hi_reg * Zbeta 1 + u2Z lo_reg.
Lemma utoZ_def: forall s, utoZ s = u2Z (lo s) + u2Z (hi s) * Zbeta 1 + u2Z (acx s) * Zbeta 2.
Proof. move=> [a [l h] ] /=. rewrite /utoZ /=. by ring. Qed.
Lemma utoZ_upd : forall r v s, utoZ (upd r v s) = utoZ s.
Proof. move=> r v [s [a [h l]]] /=; case/orP: (orbN (r == r0));
[move=> -> // | move/negbTE; move=> -> //]. Qed.
Lemma utoZ_pos : forall m, 0 <= utoZ m.
Proof.
move=> mu; rewrite utoZ_def.
move: (min_u2Z (lo mu)) => H.
have H' : 0 <= u2Z (hi mu) * Zbeta 1.
apply Zmult_le_0_compat. apply min_u2Z. move: (Zbeta_1 1). done.
have H'' : 0 <= u2Z (acx mu) * Zbeta 2.
apply Zmult_le_0_compat. apply min_u2Z. move: (Zbeta_1 2). done.
do 2 apply Zplus_le_0_compat => //.
Qed.
Lemma utoZ_acx_beta2 : forall m, utoZ m < Zbeta 2 -> acx m = Z2u acx_size 0.
Proof.
move=> [s [a [h l] ]] H /=.
rewrite /utoZ /= in H.
have [H0 | H0] : u2Z a = 0 \/ u2Z a > 0 by move: (min_u2Z a) => H'; by omega.
- apply u2Z_inj.
by rewrite u2Z_Z2u.
- have H1 : Zbeta 2 <= u2Z a * Zbeta 2.
apply Zle_trans with (1 * Zbeta 2); first by rewrite Zmult_1_l //.
apply Zmult_le_compat_r; first by omega.
apply Zbeta_0'.
have H2 : 0 <= u2Z h * Zbeta 1.
apply Zmult_le_0_compat; [apply min_u2Z | apply Zbeta_0'].
move: (min_u2Z l) => H3.
have [//] : ~ (u2Z a * Zbeta 2 + u2Z h * Zbeta 1 + u2Z l < Zbeta 2) by omega.
Qed.
Lemma hi_zero : forall m, utoZ m < Zbeta 1 -> hi m = Z2u 32 0.
Proof.
move=> [s [a [h l] ]] H /=.
rewrite /utoZ /= in H.
have [H0 | H0] : u2Z h = 0 \/ u2Z h > 0 by move: (min_u2Z h) => H'; by omega.
- apply u2Z_inj.
by rewrite u2Z_Z2u //.
- have H1 : 0 <= u2Z a * Zbeta 2.
apply Zmult_le_0_compat.
apply min_u2Z.
apply Zbeta_0'.
have H2 : Zbeta 1 <= u2Z h * Zbeta 1.
apply Zle_trans with (1 * Zbeta 1); first by rewrite Zmult_1_l //.
apply Zmult_le_compat_r; first by omega.
apply Zbeta_0'.
move: (min_u2Z l) => H3.
have Habsurd : ~ (u2Z a * Zbeta 2 + u2Z h * Zbeta 1 + u2Z l < Zbeta 1) by omega.
contradiction.
Qed.
Lemma acxhi_zero : forall m, utoZ m < Zbeta 1 -> utoZ m = u2Z (lo m).
Proof.
move=> mu H.
have [H1 H2] : acx mu = Z2u acx_size 0 /\ hi mu = Z2u 32 0.
split.
- apply utoZ_acx_beta2.
apply Zlt_trans with (Zbeta 1) => //.
- apply hi_zero => //.
move: mu H H1 H2.
move=> [a [h l] ] /= H H1 H2.
rewrite /utoZ /= H1 H2 /= u2Z_Z2u.
rewrite u2Z_Z2u //=.
split => //.
Qed.
Lemma utoZ_lo_beta1 : forall m, utoZ m < Zbeta 1 ->
acx m = Z2u acx_size 0 /\ hi m = Z2u 32 0 /\ utoZ m = u2Z (lo m).
Proof.
move=> mu H; split.
apply utoZ_acx_beta2.
apply Zlt_trans with (Zbeta 1) => //.
split.
apply hi_zero => //.
apply acxhi_zero => //.
Qed.
Local Open Scope machine_int_scope.
Lemma lo_remainder': forall m l (a : int l), (l = acx_size + 32 + 32)%nat ->
utoZ m = u2Z a -> lo m = a [.%] 32.
Proof.
move=> [s [i0 [i1 i2] ]] /= l a Hl H.
rewrite utoZ_def /= in H.
have H1 : u2Z a = u2Z ((i0 [.||] i1) [.||] i2).
rewrite 2!u2Z_concat -H Zbeta1_Zpower2 -Zpower_64_Zbeta /=; ring.
subst l.
apply u2Z_inj in H1.
by rewrite H1 (rem_concat (i0 [.||] i1) i2).
Qed.
Lemma lo_remainder : forall m l (a : int l), (l <= acx_size + 32 + 32)%nat ->
utoZ m = u2Z a -> lo m = a [.%] 32.
Proof.
move=> mu l a H H'.
rewrite (lo_remainder' mu _ (zext ((acx_size + 32 + 32) - l) a)).
- apply u2Z_inj.
by rewrite u2Z_rem_zext.
- move: acx_size_min => H''; omega.
- by rewrite u2Z_zext.
Qed.
Definition multi_null (s : t) := utoZ s = 0.
Definition null_multiplier (s : rf) : t := (s, (Z2u acx_size 0, (zero32, zero32))).
Lemma multi_null_utoZ : forall s, multi_null s -> utoZ s = 0.
Proof. rewrite //=. Qed.
Lemma utoZ_multi_null : forall m, utoZ m = 0 -> multi_null m.
Proof. rewrite //=. Qed.
Lemma multi_null_upd : forall r v s, multi_null (upd r v s) = multi_null s.
Proof. move=> r v [s mu] /=; case/orP: (orbN (r == r0));
[move=> -> // | move/negbTE; move=> -> //]. Qed.
Lemma multi_null_lo : forall m, multi_null m -> lo m = Z2u 32 0.
Proof.
move=> [s [a [h l]]] /=.
rewrite /multi_null /utoZ /= => H.
apply u2Z_inj.
rewrite u2Z_Z2u //.
have H1 : 0 <= u2Z a * Zbeta 2.
apply Zmult_le_0_compat.
by apply min_u2Z.
by apply Zbeta_0'.
have H2 : 0 <= u2Z h * Zbeta 1.
apply Zmult_le_0_compat.
by apply min_u2Z.
by apply Zbeta_0'.
move: (min_u2Z l) => H3; omega.
Qed.
let acx_reg := acx s in
let (hi_reg, lo_reg) := (hi s, lo s) in
u2Z acx_reg * Zbeta 2 + u2Z hi_reg * Zbeta 1 + u2Z lo_reg.
Lemma utoZ_def: forall s, utoZ s = u2Z (lo s) + u2Z (hi s) * Zbeta 1 + u2Z (acx s) * Zbeta 2.
Proof. move=> [a [l h] ] /=. rewrite /utoZ /=. by ring. Qed.
Lemma utoZ_upd : forall r v s, utoZ (upd r v s) = utoZ s.
Proof. move=> r v [s [a [h l]]] /=; case/orP: (orbN (r == r0));
[move=> -> // | move/negbTE; move=> -> //]. Qed.
Lemma utoZ_pos : forall m, 0 <= utoZ m.
Proof.
move=> mu; rewrite utoZ_def.
move: (min_u2Z (lo mu)) => H.
have H' : 0 <= u2Z (hi mu) * Zbeta 1.
apply Zmult_le_0_compat. apply min_u2Z. move: (Zbeta_1 1). done.
have H'' : 0 <= u2Z (acx mu) * Zbeta 2.
apply Zmult_le_0_compat. apply min_u2Z. move: (Zbeta_1 2). done.
do 2 apply Zplus_le_0_compat => //.
Qed.
Lemma utoZ_acx_beta2 : forall m, utoZ m < Zbeta 2 -> acx m = Z2u acx_size 0.
Proof.
move=> [s [a [h l] ]] H /=.
rewrite /utoZ /= in H.
have [H0 | H0] : u2Z a = 0 \/ u2Z a > 0 by move: (min_u2Z a) => H'; by omega.
- apply u2Z_inj.
by rewrite u2Z_Z2u.
- have H1 : Zbeta 2 <= u2Z a * Zbeta 2.
apply Zle_trans with (1 * Zbeta 2); first by rewrite Zmult_1_l //.
apply Zmult_le_compat_r; first by omega.
apply Zbeta_0'.
have H2 : 0 <= u2Z h * Zbeta 1.
apply Zmult_le_0_compat; [apply min_u2Z | apply Zbeta_0'].
move: (min_u2Z l) => H3.
have [//] : ~ (u2Z a * Zbeta 2 + u2Z h * Zbeta 1 + u2Z l < Zbeta 2) by omega.
Qed.
Lemma hi_zero : forall m, utoZ m < Zbeta 1 -> hi m = Z2u 32 0.
Proof.
move=> [s [a [h l] ]] H /=.
rewrite /utoZ /= in H.
have [H0 | H0] : u2Z h = 0 \/ u2Z h > 0 by move: (min_u2Z h) => H'; by omega.
- apply u2Z_inj.
by rewrite u2Z_Z2u //.
- have H1 : 0 <= u2Z a * Zbeta 2.
apply Zmult_le_0_compat.
apply min_u2Z.
apply Zbeta_0'.
have H2 : Zbeta 1 <= u2Z h * Zbeta 1.
apply Zle_trans with (1 * Zbeta 1); first by rewrite Zmult_1_l //.
apply Zmult_le_compat_r; first by omega.
apply Zbeta_0'.
move: (min_u2Z l) => H3.
have Habsurd : ~ (u2Z a * Zbeta 2 + u2Z h * Zbeta 1 + u2Z l < Zbeta 1) by omega.
contradiction.
Qed.
Lemma acxhi_zero : forall m, utoZ m < Zbeta 1 -> utoZ m = u2Z (lo m).
Proof.
move=> mu H.
have [H1 H2] : acx mu = Z2u acx_size 0 /\ hi mu = Z2u 32 0.
split.
- apply utoZ_acx_beta2.
apply Zlt_trans with (Zbeta 1) => //.
- apply hi_zero => //.
move: mu H H1 H2.
move=> [a [h l] ] /= H H1 H2.
rewrite /utoZ /= H1 H2 /= u2Z_Z2u.
rewrite u2Z_Z2u //=.
split => //.
Qed.
Lemma utoZ_lo_beta1 : forall m, utoZ m < Zbeta 1 ->
acx m = Z2u acx_size 0 /\ hi m = Z2u 32 0 /\ utoZ m = u2Z (lo m).
Proof.
move=> mu H; split.
apply utoZ_acx_beta2.
apply Zlt_trans with (Zbeta 1) => //.
split.
apply hi_zero => //.
apply acxhi_zero => //.
Qed.
Local Open Scope machine_int_scope.
Lemma lo_remainder': forall m l (a : int l), (l = acx_size + 32 + 32)%nat ->
utoZ m = u2Z a -> lo m = a [.%] 32.
Proof.
move=> [s [i0 [i1 i2] ]] /= l a Hl H.
rewrite utoZ_def /= in H.
have H1 : u2Z a = u2Z ((i0 [.||] i1) [.||] i2).
rewrite 2!u2Z_concat -H Zbeta1_Zpower2 -Zpower_64_Zbeta /=; ring.
subst l.
apply u2Z_inj in H1.
by rewrite H1 (rem_concat (i0 [.||] i1) i2).
Qed.
Lemma lo_remainder : forall m l (a : int l), (l <= acx_size + 32 + 32)%nat ->
utoZ m = u2Z a -> lo m = a [.%] 32.
Proof.
move=> mu l a H H'.
rewrite (lo_remainder' mu _ (zext ((acx_size + 32 + 32) - l) a)).
- apply u2Z_inj.
by rewrite u2Z_rem_zext.
- move: acx_size_min => H''; omega.
- by rewrite u2Z_zext.
Qed.
Definition multi_null (s : t) := utoZ s = 0.
Definition null_multiplier (s : rf) : t := (s, (Z2u acx_size 0, (zero32, zero32))).
Lemma multi_null_utoZ : forall s, multi_null s -> utoZ s = 0.
Proof. rewrite //=. Qed.
Lemma utoZ_multi_null : forall m, utoZ m = 0 -> multi_null m.
Proof. rewrite //=. Qed.
Lemma multi_null_upd : forall r v s, multi_null (upd r v s) = multi_null s.
Proof. move=> r v [s mu] /=; case/orP: (orbN (r == r0));
[move=> -> // | move/negbTE; move=> -> //]. Qed.
Lemma multi_null_lo : forall m, multi_null m -> lo m = Z2u 32 0.
Proof.
move=> [s [a [h l]]] /=.
rewrite /multi_null /utoZ /= => H.
apply u2Z_inj.
rewrite u2Z_Z2u //.
have H1 : 0 <= u2Z a * Zbeta 2.
apply Zmult_le_0_compat.
by apply min_u2Z.
by apply Zbeta_0'.
have H2 : 0 <= u2Z h * Zbeta 1.
apply Zmult_le_0_compat.
by apply min_u2Z.
by apply Zbeta_0'.
move: (min_u2Z l) => H3; omega.
Qed.
maddu
Definition maddu_op (p : int (2 * 32)) (m : t) : t :=
match m with
(s, m') =>
let acx_reg := acx m in
let hi_reg := hi m in
let lo_reg := lo m in
let sum := acx_reg [.||] (hi_reg [.||] lo_reg) in
let new_sum := zext 8 p [.+] sum in
let lo_reg' := new_sum [.%] 32 in
let sum' := shr_shrink 32 new_sum in
let hi_reg' := sum' [.%] 32 in
let acx_reg' := shr_shrink 32 sum' in
(s, (acx_reg', (hi_reg', lo_reg')))
end.
Lemma maddu_upd : forall a r v s, maddu_op a (upd r v s) = upd r v (maddu_op a s).
Proof.
move=> A r v [s [a0 [h l]]] /=.
case/orP: (orbN (r == r0)).
move=> -> //.
move/negbTE.
by move=> ->.
Qed.
Lemma concat_acx_hilo : forall (a : int acx_size) (b : int (2 * 32)),
u2Z (a [.||] b) = u2Z a * Zbeta 2 + u2Z b.
Proof. move=> a b. by rewrite u2Z_concat. Qed.
Local Open Scope zarith_ext_scope.
Lemma utoZ_maddu : forall m a, utoZ m < Zbeta 2 * (2 ^^ acx_size - 1) ->
utoZ (maddu_op a m) = u2Z a + utoZ m.
Proof.
move=> [accu [ h l ] ] a H /=; move: H.
rewrite /utoZ /acx /hi /lo /maddu_op => H.
rewrite (_ : Zbeta 2 = Zbeta 1 * Zbeta 1) //.
rewrite Zmult_assoc -Zmult_plus_distr_l (@u2Z_shr_shrink 40 _ 32) //; last by omega.
rewrite (@u2Z_shr_shrink 72 _ 32) //; last by omega.
rewrite [Zbeta]lock /= -lock u2Z_add.
- rewrite (u2Z_zext 8) concat_acx_hilo u2Z_concat -Zbeta_is_exp (_ : 1 + 1 = 2)%nat //.
by rewrite !Zplus_assoc.
- rewrite (u2Z_zext 8) concat_acx_hilo u2Z_concat !Zplus_assoc.
move: (max_u2Z a) => H'.
rewrite Zmult_minus_distr_l Zmult_1_r in H.
move: (Zpower_1 acx_size) => H''.
apply Zlt_le_trans with (u2Z a + Zbeta 2 * 2 ^^ acx_size - u2Z a).
+ move: (Zplus_lt_compat _ _ _ _ H' H) => H'''.
rewrite 2!Zplus_assoc in H'''.
by rewrite Zminus_plus.
+ by rewrite Zminus_plus.
Qed.
Definition multu_op (p : int (2 * 32)) (s : t) : t :=
match s with (lst, m') =>
let lo' := p [.%] 32 in
let hi' := shr_shrink 32 p in
(lst, (Z2u acx_size 0, (hi', lo')))
end.
Lemma utoZ_multu : forall p m, utoZ (multu_op p m) = u2Z p.
Proof.
move=> p [a [h l]] /=.
rewrite /multu_op /utoZ /acx u2Z_Z2u // Zbeta1_Zpower2.
have H : (32 <= 2 * 32)%nat by repeat constructor.
by move: (u2Z_shr_shrink p H) => H'.
Qed.
match m with
(s, m') =>
let acx_reg := acx m in
let hi_reg := hi m in
let lo_reg := lo m in
let sum := acx_reg [.||] (hi_reg [.||] lo_reg) in
let new_sum := zext 8 p [.+] sum in
let lo_reg' := new_sum [.%] 32 in
let sum' := shr_shrink 32 new_sum in
let hi_reg' := sum' [.%] 32 in
let acx_reg' := shr_shrink 32 sum' in
(s, (acx_reg', (hi_reg', lo_reg')))
end.
Lemma maddu_upd : forall a r v s, maddu_op a (upd r v s) = upd r v (maddu_op a s).
Proof.
move=> A r v [s [a0 [h l]]] /=.
case/orP: (orbN (r == r0)).
move=> -> //.
move/negbTE.
by move=> ->.
Qed.
Lemma concat_acx_hilo : forall (a : int acx_size) (b : int (2 * 32)),
u2Z (a [.||] b) = u2Z a * Zbeta 2 + u2Z b.
Proof. move=> a b. by rewrite u2Z_concat. Qed.
Local Open Scope zarith_ext_scope.
Lemma utoZ_maddu : forall m a, utoZ m < Zbeta 2 * (2 ^^ acx_size - 1) ->
utoZ (maddu_op a m) = u2Z a + utoZ m.
Proof.
move=> [accu [ h l ] ] a H /=; move: H.
rewrite /utoZ /acx /hi /lo /maddu_op => H.
rewrite (_ : Zbeta 2 = Zbeta 1 * Zbeta 1) //.
rewrite Zmult_assoc -Zmult_plus_distr_l (@u2Z_shr_shrink 40 _ 32) //; last by omega.
rewrite (@u2Z_shr_shrink 72 _ 32) //; last by omega.
rewrite [Zbeta]lock /= -lock u2Z_add.
- rewrite (u2Z_zext 8) concat_acx_hilo u2Z_concat -Zbeta_is_exp (_ : 1 + 1 = 2)%nat //.
by rewrite !Zplus_assoc.
- rewrite (u2Z_zext 8) concat_acx_hilo u2Z_concat !Zplus_assoc.
move: (max_u2Z a) => H'.
rewrite Zmult_minus_distr_l Zmult_1_r in H.
move: (Zpower_1 acx_size) => H''.
apply Zlt_le_trans with (u2Z a + Zbeta 2 * 2 ^^ acx_size - u2Z a).
+ move: (Zplus_lt_compat _ _ _ _ H' H) => H'''.
rewrite 2!Zplus_assoc in H'''.
by rewrite Zminus_plus.
+ by rewrite Zminus_plus.
Qed.
Definition multu_op (p : int (2 * 32)) (s : t) : t :=
match s with (lst, m') =>
let lo' := p [.%] 32 in
let hi' := shr_shrink 32 p in
(lst, (Z2u acx_size 0, (hi', lo')))
end.
Lemma utoZ_multu : forall p m, utoZ (multu_op p m) = u2Z p.
Proof.
move=> p [a [h l]] /=.
rewrite /multu_op /utoZ /acx u2Z_Z2u // Zbeta1_Zpower2.
have H : (32 <= 2 * 32)%nat by repeat constructor.
by move: (u2Z_shr_shrink p H) => H'.
Qed.
The mflhxu instruction performs a division by
2^32, whose remainder is put in a
general-purpose register and whose quotient is left in the multiplier.
The corresponding hardware circuitry is essentially a shift: it puts
the contents of LO into some general-purpose register, puts the contents
of HI into LO, and zeroes ACX.
Definition mflhxu_op m :=
match m with
| (s, m') => let (acx_reg, hi_reg) := (acx m, hi m) in (s, (Z2u acx_size 0, (zext 24 acx_reg, hi_reg)))
end.
Lemma mflhxu_upd : forall r v s, mflhxu_op (upd r v s) = upd r v (mflhxu_op s).
Proof.
move=> r v [s [a0 [h l]]] /=; case/orP: (orbN (r == r0)) ;
by [move=> -> // | move/negbTE; move=> -> //].
Qed.
Lemma hi_mflhxu_op : forall m, u2Z (hi (mflhxu_op m)) = u2Z (zext (32 - acx_size) (acx m)).
Proof. by move=> [i0 [ i1 i2 ]]. Qed.
Lemma lo_mflhxu_op : forall m, lo (mflhxu_op m) = hi m.
Proof. by move=> [i0 [ i1 i2 ]]. Qed.
Lemma acx_mflhxu_op : forall m, acx (mflhxu_op m) = Z2u acx_size 0.
Proof. by move=> [i0 [ i1 i2 ]]. Qed.
match m with
| (s, m') => let (acx_reg, hi_reg) := (acx m, hi m) in (s, (Z2u acx_size 0, (zext 24 acx_reg, hi_reg)))
end.
Lemma mflhxu_upd : forall r v s, mflhxu_op (upd r v s) = upd r v (mflhxu_op s).
Proof.
move=> r v [s [a0 [h l]]] /=; case/orP: (orbN (r == r0)) ;
by [move=> -> // | move/negbTE; move=> -> //].
Qed.
Lemma hi_mflhxu_op : forall m, u2Z (hi (mflhxu_op m)) = u2Z (zext (32 - acx_size) (acx m)).
Proof. by move=> [i0 [ i1 i2 ]]. Qed.
Lemma lo_mflhxu_op : forall m, lo (mflhxu_op m) = hi m.
Proof. by move=> [i0 [ i1 i2 ]]. Qed.
Lemma acx_mflhxu_op : forall m, acx (mflhxu_op m) = Z2u acx_size 0.
Proof. by move=> [i0 [ i1 i2 ]]. Qed.
The decimal values of the multiplier before and after mflhxu are related as follows:
Lemma mflhxu_utoZ : forall m, utoZ m = utoZ (mflhxu_op m) * Zbeta 1 + u2Z (lo m).
Proof.
move=> [s [acx_reg [hi_reg lo_reg] ]] /=.
rewrite /mflhxu_op /= /utoZ /=.
rewrite -(@u2Z_zext 24 acx_size acx_reg).
move: (Zbeta_is_exp 1 1) => H.
rewrite ( _ : 1 + 1 = 2%nat)%nat // in H.
rewrite H.
f_equal.
rewrite Zmult_plus_distr_l.
f_equal.
rewrite Zmult_plus_distr_l u2Z_Z2u //.
rewrite [Zbeta]lock /= -lock.
by apply Zmult_assoc.
Qed.
Lemma mflhxu_beta2_utoZ : forall m, utoZ m < Zbeta 2 -> utoZ (mflhxu_op m) < Zbeta 1.
Proof.
move=> [a [h l] ] /= H.
rewrite /mflhxu_op /=.
move: (utoZ_acx_beta2 _ H) => H0.
rewrite /= in H0.
rewrite H0.
have H1 : zext 24 (Z2u acx_size 0) = Z2u 32 0.
apply u2Z_inj.
by rewrite u2Z_zext u2Z_Z2u // u2Z_Z2u.
rewrite /utoZ /= H1 u2Z_Z2u // u2Z_Z2u //= Zbeta1_Zpower2.
by apply max_u2Z.
Qed.
Lemma mflhxu_kbeta1_utoZ : forall m k, utoZ m < Zbeta 1 * k -> utoZ (mflhxu_op m) < k.
Proof.
move=> mu.
destruct k.
- rewrite Zmult_0_r.
move: mu; move => [s [a [ h l]]] H.
rewrite utoZ_def /= in H.
have H' : u2Z l + u2Z h * Zbeta 1 + u2Z a * Zbeta 2 >= 0.
have H1 : 0 <= u2Z h * Zbeta 1.
apply Zmult_le_0_compat.
apply min_u2Z.
apply Zbeta_0'.
have H2 : 0 <= u2Z a * Zbeta 2.
apply Zmult_le_0_compat.
apply min_u2Z.
apply Zbeta_0'.
move: (min_u2Z l) => H3.
by omega.
by contradiction.
- move: mu; move => [s [a [ h l] ]] H.
rewrite mflhxu_utoZ /= /mflhxu_op /= utoZ_def /=.
rewrite utoZ_def in H.
simpl u2Z in H.
rewrite 2!(@u2Z_zext 24 acx_size) u2Z_Z2u //=.
have H1 : u2Z h * Zbeta 1 + u2Z a * Zbeta 2 < Zbeta 1 * Zpos p.
move: (min_u2Z l) => H'; by omega.
apply Zmult_gt_0_lt_reg_r with (Zbeta 1).
apply Zlt_gt; apply Zbeta_0.
rewrite 2!Zplus_0_r.
rewrite (_ : (u2Z a * Zbeta 1 + u2Z h) * Zbeta 1 = u2Z h * Zbeta 1 + u2Z a * Zbeta 2 ).
rewrite (Zmult_comm (Zpos p)) //.
rewrite /Zbeta /=; ring.
- move=> H.
move: (utoZ_pos mu) => H'.
have H1 : Zbeta 1 * Zneg p < 0.
rewrite /=.
apply Zlt_neg_0.
have H2 : utoZ mu < 0 by omega.
omega.
Qed.
Proof.
move=> [s [acx_reg [hi_reg lo_reg] ]] /=.
rewrite /mflhxu_op /= /utoZ /=.
rewrite -(@u2Z_zext 24 acx_size acx_reg).
move: (Zbeta_is_exp 1 1) => H.
rewrite ( _ : 1 + 1 = 2%nat)%nat // in H.
rewrite H.
f_equal.
rewrite Zmult_plus_distr_l.
f_equal.
rewrite Zmult_plus_distr_l u2Z_Z2u //.
rewrite [Zbeta]lock /= -lock.
by apply Zmult_assoc.
Qed.
Lemma mflhxu_beta2_utoZ : forall m, utoZ m < Zbeta 2 -> utoZ (mflhxu_op m) < Zbeta 1.
Proof.
move=> [a [h l] ] /= H.
rewrite /mflhxu_op /=.
move: (utoZ_acx_beta2 _ H) => H0.
rewrite /= in H0.
rewrite H0.
have H1 : zext 24 (Z2u acx_size 0) = Z2u 32 0.
apply u2Z_inj.
by rewrite u2Z_zext u2Z_Z2u // u2Z_Z2u.
rewrite /utoZ /= H1 u2Z_Z2u // u2Z_Z2u //= Zbeta1_Zpower2.
by apply max_u2Z.
Qed.
Lemma mflhxu_kbeta1_utoZ : forall m k, utoZ m < Zbeta 1 * k -> utoZ (mflhxu_op m) < k.
Proof.
move=> mu.
destruct k.
- rewrite Zmult_0_r.
move: mu; move => [s [a [ h l]]] H.
rewrite utoZ_def /= in H.
have H' : u2Z l + u2Z h * Zbeta 1 + u2Z a * Zbeta 2 >= 0.
have H1 : 0 <= u2Z h * Zbeta 1.
apply Zmult_le_0_compat.
apply min_u2Z.
apply Zbeta_0'.
have H2 : 0 <= u2Z a * Zbeta 2.
apply Zmult_le_0_compat.
apply min_u2Z.
apply Zbeta_0'.
move: (min_u2Z l) => H3.
by omega.
by contradiction.
- move: mu; move => [s [a [ h l] ]] H.
rewrite mflhxu_utoZ /= /mflhxu_op /= utoZ_def /=.
rewrite utoZ_def in H.
simpl u2Z in H.
rewrite 2!(@u2Z_zext 24 acx_size) u2Z_Z2u //=.
have H1 : u2Z h * Zbeta 1 + u2Z a * Zbeta 2 < Zbeta 1 * Zpos p.
move: (min_u2Z l) => H'; by omega.
apply Zmult_gt_0_lt_reg_r with (Zbeta 1).
apply Zlt_gt; apply Zbeta_0.
rewrite 2!Zplus_0_r.
rewrite (_ : (u2Z a * Zbeta 1 + u2Z h) * Zbeta 1 = u2Z h * Zbeta 1 + u2Z a * Zbeta 2 ).
rewrite (Zmult_comm (Zpos p)) //.
rewrite /Zbeta /=; ring.
- move=> H.
move: (utoZ_pos mu) => H'.
have H1 : Zbeta 1 * Zneg p < 0.
rewrite /=.
apply Zlt_neg_0.
have H2 : utoZ mu < 0 by omega.
omega.
Qed.
msubu
Definition msubu_op (p : int (2 * 32)) (s : t) : t :=
match s with (lst, mu) =>
let acx_reg := acx s in
let hi_reg := hi s in
let lo_reg := lo s in
let sum := (hi_reg [.||] lo_reg) in
let new_sum := sum [.-] p in
let lo_reg' := new_sum [.%] 32 in
let sum' := shr_shrink 32 new_sum in
let hi_reg' := sum' [.%] 32 in
(lst, (acx_reg, (hi_reg', lo_reg'))) end.
Lemma msubu_utoZ : forall m a, utoZ m < Zbeta 2 -> utoZ m >= u2Z a ->
utoZ (msubu_op a m) = utoZ m - u2Z a.
Proof.
move=> [s [accu [ h l]]] a H H0.
rewrite /msubu_op /= utoZ_def /= utoZ_def /=.
have H1 : u2Z accu = 0.
apply utoZ_acx_beta2 in H.
rewrite /= in H.
rewrite H u2Z_Z2u //=.
rewrite H1 /= Zplus_0_r u2Z_rem //; last by repeat constructor.
rewrite u2Z_rem //.
rewrite -Zbeta1_Zpower2 Zmult_minus_distr_r.
rewrite (shr_shrink_overflow (shr_shrink 32 ((h [.||] l) [.-] a))) //.
rewrite u2Z_Z2u //=.
rewrite Zminus_0_r.
rewrite u2Z_sub.
- rewrite (u2Z_concat h l).
by ring_simplify.
- rewrite (u2Z_concat h l).
rewrite Zplus_comm.
by rewrite utoZ_def /= H1 /= Zplus_0_r in H0.
Qed.
Lemma msubu_utoZ_overflow : forall m a, utoZ m < Zbeta 2 -> utoZ m < u2Z a ->
utoZ (msubu_op a m) = Zbeta 2 + utoZ m - u2Z a.
Proof.
move=> [s [accu [h l] ]] a H H0.
rewrite /msubu_op utoZ_def.
simpl u2Z.
have H1 : u2Z accu = 0.
apply utoZ_acx_beta2 in H.
rewrite /= in H.
rewrite H u2Z_Z2u //=.
rewrite H1 Zmult_0_l Zplus_0_r.
rewrite u2Z_rem //; last by repeat constructor.
rewrite u2Z_rem //.
rewrite -Zbeta1_Zpower2 Zmult_minus_distr_r.
rewrite (shr_shrink_overflow (shr_shrink 32 ((h [.||] l) [.-] a))); last by auto.
rewrite u2Z_Z2u; last by auto.
rewrite Zmult_0_l Zminus_0_r.
rewrite u2Z_sub_overflow.
- rewrite (u2Z_concat h l) Zpower_64_Zbeta utoZ_def.
simpl u2Z.
rewrite H1 Zmult_0_l.
by ring_simplify.
- rewrite (u2Z_concat h l) Zplus_comm.
by rewrite utoZ_def /= H1 /= Zplus_0_r in H0.
Qed.
Lemma get_multu_op : forall x z st, store.get x (store.multu_op z st) = store.get x st.
Proof. move=> x z [st m0]. by rewrite /store.get /store.multu_op. Qed.
Lemma get_mflhxu_op : forall x st, store.get x (store.mflhxu_op st) = store.get x st.
Proof. move=> x [st m0]. by rewrite /store.get /store.mflhxu_op. Qed.
Lemma get_maddu_op : forall x z st, store.get x (store.maddu_op z st) = store.get x st.
Proof. move=> x z [st m0]. by rewrite /store.get /store.maddu_op. Qed.
Lemma get_msubu_op : forall x z st, store.get x (store.msubu_op z st) = store.get x st.
Proof. move=> x z [st m0]. by rewrite /store.get /store.msubu_op. Qed.
Lemma get_mthi_op : forall x z st, store.get x (store.mthi_op z st) = store.get x st.
Proof. move=> x0 z0 [st [a [hi0 lo0]]]. by rewrite /store.get /store.mthi_op. Qed.
Lemma get_mtlo_op : forall x z st, store.get x (store.mtlo_op z st) = store.get x st.
Proof. move=> x0 z0 [st [a [hi0 lo0]]]. by rewrite /store.get /store.mtlo_op. Qed.
End store.
Local Open Scope zarith_ext_scope.
match s with (lst, mu) =>
let acx_reg := acx s in
let hi_reg := hi s in
let lo_reg := lo s in
let sum := (hi_reg [.||] lo_reg) in
let new_sum := sum [.-] p in
let lo_reg' := new_sum [.%] 32 in
let sum' := shr_shrink 32 new_sum in
let hi_reg' := sum' [.%] 32 in
(lst, (acx_reg, (hi_reg', lo_reg'))) end.
Lemma msubu_utoZ : forall m a, utoZ m < Zbeta 2 -> utoZ m >= u2Z a ->
utoZ (msubu_op a m) = utoZ m - u2Z a.
Proof.
move=> [s [accu [ h l]]] a H H0.
rewrite /msubu_op /= utoZ_def /= utoZ_def /=.
have H1 : u2Z accu = 0.
apply utoZ_acx_beta2 in H.
rewrite /= in H.
rewrite H u2Z_Z2u //=.
rewrite H1 /= Zplus_0_r u2Z_rem //; last by repeat constructor.
rewrite u2Z_rem //.
rewrite -Zbeta1_Zpower2 Zmult_minus_distr_r.
rewrite (shr_shrink_overflow (shr_shrink 32 ((h [.||] l) [.-] a))) //.
rewrite u2Z_Z2u //=.
rewrite Zminus_0_r.
rewrite u2Z_sub.
- rewrite (u2Z_concat h l).
by ring_simplify.
- rewrite (u2Z_concat h l).
rewrite Zplus_comm.
by rewrite utoZ_def /= H1 /= Zplus_0_r in H0.
Qed.
Lemma msubu_utoZ_overflow : forall m a, utoZ m < Zbeta 2 -> utoZ m < u2Z a ->
utoZ (msubu_op a m) = Zbeta 2 + utoZ m - u2Z a.
Proof.
move=> [s [accu [h l] ]] a H H0.
rewrite /msubu_op utoZ_def.
simpl u2Z.
have H1 : u2Z accu = 0.
apply utoZ_acx_beta2 in H.
rewrite /= in H.
rewrite H u2Z_Z2u //=.
rewrite H1 Zmult_0_l Zplus_0_r.
rewrite u2Z_rem //; last by repeat constructor.
rewrite u2Z_rem //.
rewrite -Zbeta1_Zpower2 Zmult_minus_distr_r.
rewrite (shr_shrink_overflow (shr_shrink 32 ((h [.||] l) [.-] a))); last by auto.
rewrite u2Z_Z2u; last by auto.
rewrite Zmult_0_l Zminus_0_r.
rewrite u2Z_sub_overflow.
- rewrite (u2Z_concat h l) Zpower_64_Zbeta utoZ_def.
simpl u2Z.
rewrite H1 Zmult_0_l.
by ring_simplify.
- rewrite (u2Z_concat h l) Zplus_comm.
by rewrite utoZ_def /= H1 /= Zplus_0_r in H0.
Qed.
Lemma get_multu_op : forall x z st, store.get x (store.multu_op z st) = store.get x st.
Proof. move=> x z [st m0]. by rewrite /store.get /store.multu_op. Qed.
Lemma get_mflhxu_op : forall x st, store.get x (store.mflhxu_op st) = store.get x st.
Proof. move=> x [st m0]. by rewrite /store.get /store.mflhxu_op. Qed.
Lemma get_maddu_op : forall x z st, store.get x (store.maddu_op z st) = store.get x st.
Proof. move=> x z [st m0]. by rewrite /store.get /store.maddu_op. Qed.
Lemma get_msubu_op : forall x z st, store.get x (store.msubu_op z st) = store.get x st.
Proof. move=> x z [st m0]. by rewrite /store.get /store.msubu_op. Qed.
Lemma get_mthi_op : forall x z st, store.get x (store.mthi_op z st) = store.get x st.
Proof. move=> x0 z0 [st [a [hi0 lo0]]]. by rewrite /store.get /store.mthi_op. Qed.
Lemma get_mtlo_op : forall x z st, store.get x (store.mtlo_op z st) = store.get x st.
Proof. move=> x0 z0 [st [a [hi0 lo0]]]. by rewrite /store.get /store.mtlo_op. Qed.
End store.
Local Open Scope zarith_ext_scope.
Properties derived from the module store
Lemma utoZ_maddu_op : forall k (m : store.t) (p : int (2 * 32)),
(k <= 64)%nat -> store.utoZ m < 2 ^^ k -> u2Z p < 2 ^^ k ->
store.utoZ (store.maddu_op p m) < 2 ^^ (S k).
Proof.
move=> k m p Hk Hm Hp.
rewrite store.utoZ_maddu.
- rewrite Zpower_S; by omega.
- apply Zlt_le_trans with (Zbeta 2 * 1) => //.
+ rewrite Zmult_1_r.
apply Zlt_le_trans with (2 ^^ k) => //.
rewrite -Zpower_64_Zbeta.
by apply Zpower_2_le.
Qed.
Lemma lo_remainder_zero : forall (s : store.t),
(exists K, store.utoZ s = K * Zbeta 1) -> store.lo s = zero32.
Proof.
move=> m [K H0].
have HK : 0 <= K.
move: (store.utoZ_pos m) => H1.
rewrite H0 in H1.
case/Zle_0_mult_inv : H1 => H1; first by omega.
move: (Zbeta_0 1) => ?; omega.
rewrite store.utoZ_def in H0.
have {H0}H0 : (u2Z (store.hi m) + u2Z (store.acx m) * Zbeta 1) * Zbeta 1 +
u2Z (store.lo m) = K * Zbeta 1 + 0.
rewrite -H0 (Zbeta_S 1); ring.
apply poly_eq_inv in H0.
apply u2Z_inj.
rewrite /zero32 u2Z_Z2u //; tauto.
split.
+ apply Zplus_le_0_compat.
by apply min_u2Z.
apply Zmult_le_0_compat.
by apply min_u2Z.
by apply Zbeta_0'.
+ split => //.
split; by [apply min_u2Z | apply max_u2Z].
Qed.
Module expr_m.
(k <= 64)%nat -> store.utoZ m < 2 ^^ k -> u2Z p < 2 ^^ k ->
store.utoZ (store.maddu_op p m) < 2 ^^ (S k).
Proof.
move=> k m p Hk Hm Hp.
rewrite store.utoZ_maddu.
- rewrite Zpower_S; by omega.
- apply Zlt_le_trans with (Zbeta 2 * 1) => //.
+ rewrite Zmult_1_r.
apply Zlt_le_trans with (2 ^^ k) => //.
rewrite -Zpower_64_Zbeta.
by apply Zpower_2_le.
Qed.
Lemma lo_remainder_zero : forall (s : store.t),
(exists K, store.utoZ s = K * Zbeta 1) -> store.lo s = zero32.
Proof.
move=> m [K H0].
have HK : 0 <= K.
move: (store.utoZ_pos m) => H1.
rewrite H0 in H1.
case/Zle_0_mult_inv : H1 => H1; first by omega.
move: (Zbeta_0 1) => ?; omega.
rewrite store.utoZ_def in H0.
have {H0}H0 : (u2Z (store.hi m) + u2Z (store.acx m) * Zbeta 1) * Zbeta 1 +
u2Z (store.lo m) = K * Zbeta 1 + 0.
rewrite -H0 (Zbeta_S 1); ring.
apply poly_eq_inv in H0.
apply u2Z_inj.
rewrite /zero32 u2Z_Z2u //; tauto.
split.
+ apply Zplus_le_0_compat.
by apply min_u2Z.
apply Zmult_le_0_compat.
by apply min_u2Z.
by apply Zbeta_0'.
+ split => //.
split; by [apply min_u2Z | apply max_u2Z].
Qed.
Module expr_m.
The language for expressions used in separating connectives. In this language,
variables are registers and constants are (32-bit) words.
Inductive expr : Type :=
| var_e : reg -> expr
| int_e : int 32 -> expr
| add_e : expr -> expr -> expr
| shl2_e : expr -> expr.
Fixpoint vars (e : expr) : list reg :=
match e with
| var_e x => x :: nil
| int_e _ => nil
| add_e e1 e2 => vars e1 ++ vars e2
| shl2_e e' => vars e'
end.
Definition sext_16_32 (a : int 16) : int 32 := sext 16 a.
Lemma sext_16_32': forall n, n < 2 ^^ 15 -> sext_16_32 (Z2u 16 n) = Z2u 32 n.
Proof. move=> n Hn; by rewrite /sext_16_32 sext_Z2u. Qed.
Local Open Scope machine_int_scope.
Definition shl2 l (a : int l) := a [.<<] 2.
Implicit Arguments shl2.
Lemma shift_2_mult_4 : forall (v : int 32) z, u2Z v = 4 * z -> v = shl2 (Z2u 32 z).
Proof.
move=> v [|p|p] H.
- apply u2Z_inj.
by rewrite (@u2Z_shl _ _ _ 30) // u2Z_Z2u //.
- apply u2Z_inj.
have Hp : Zpos p < 2 ^^ 30.
by apply Zpower_shift_2; rewrite -H /Zbeta; apply max_u2Z.
have Hp' : 0 <= Zpos p < 2 ^^ 32.
by split=> //; apply Zlt_trans with (2 ^^ 30) => //.
rewrite (@u2Z_shl _ _ _ 30) // u2Z_Z2u //.
by rewrite [Zpower _ _]/= Zmult_comm.
- have : u2Z v < 0 by rewrite H //.
by move/Zlt_not_le: (min_u2Z v).
Qed.
Lemma shl_S : forall n, 0 <= n -> n + 1 < 2 ^^ 30 ->
shl2 (Z2u 32 (n + 1)) = four32 [.+] shl2 (Z2u 32 n).
Proof.
move=> [|p|p] Hn H.
- apply u2Z_inj.
by rewrite u2Z_add // !(@u2Z_shl _ _ _ 30) // !u2Z_Z2u.
- have Hp : Zpos p < 2 ^^ 30.
apply Zlt_trans with (Zpos p + 1) => //; omega.
have Hp' : Zpos p < 2 ^^ 32.
by apply Zlt_trans with (2 ^^ 30).
apply u2Z_inj.
rewrite u2Z_add //.
+ have Hp1 : 0 <= Zpos p + 1 < 2 ^^ 32.
by split => //; apply Zlt_trans with (2 ^^ 30).
rewrite !(@u2Z_shl _ _ _ 30) // !u2Z_Z2u //.
by ring_simplify.
+ rewrite (@u2Z_shl _ _ _ 30) // !u2Z_Z2u // [Zpower _ _]/=.
apply Zlt_le_trans with (4 * 2 ^^ 30) => //; omega.
- by move/Zlt_not_le: (Zlt_neg_0 p).
Qed.
| var_e : reg -> expr
| int_e : int 32 -> expr
| add_e : expr -> expr -> expr
| shl2_e : expr -> expr.
Fixpoint vars (e : expr) : list reg :=
match e with
| var_e x => x :: nil
| int_e _ => nil
| add_e e1 e2 => vars e1 ++ vars e2
| shl2_e e' => vars e'
end.
Definition sext_16_32 (a : int 16) : int 32 := sext 16 a.
Lemma sext_16_32': forall n, n < 2 ^^ 15 -> sext_16_32 (Z2u 16 n) = Z2u 32 n.
Proof. move=> n Hn; by rewrite /sext_16_32 sext_Z2u. Qed.
Local Open Scope machine_int_scope.
Definition shl2 l (a : int l) := a [.<<] 2.
Implicit Arguments shl2.
Lemma shift_2_mult_4 : forall (v : int 32) z, u2Z v = 4 * z -> v = shl2 (Z2u 32 z).
Proof.
move=> v [|p|p] H.
- apply u2Z_inj.
by rewrite (@u2Z_shl _ _ _ 30) // u2Z_Z2u //.
- apply u2Z_inj.
have Hp : Zpos p < 2 ^^ 30.
by apply Zpower_shift_2; rewrite -H /Zbeta; apply max_u2Z.
have Hp' : 0 <= Zpos p < 2 ^^ 32.
by split=> //; apply Zlt_trans with (2 ^^ 30) => //.
rewrite (@u2Z_shl _ _ _ 30) // u2Z_Z2u //.
by rewrite [Zpower _ _]/= Zmult_comm.
- have : u2Z v < 0 by rewrite H //.
by move/Zlt_not_le: (min_u2Z v).
Qed.
Lemma shl_S : forall n, 0 <= n -> n + 1 < 2 ^^ 30 ->
shl2 (Z2u 32 (n + 1)) = four32 [.+] shl2 (Z2u 32 n).
Proof.
move=> [|p|p] Hn H.
- apply u2Z_inj.
by rewrite u2Z_add // !(@u2Z_shl _ _ _ 30) // !u2Z_Z2u.
- have Hp : Zpos p < 2 ^^ 30.
apply Zlt_trans with (Zpos p + 1) => //; omega.
have Hp' : Zpos p < 2 ^^ 32.
by apply Zlt_trans with (2 ^^ 30).
apply u2Z_inj.
rewrite u2Z_add //.
+ have Hp1 : 0 <= Zpos p + 1 < 2 ^^ 32.
by split => //; apply Zlt_trans with (2 ^^ 30).
rewrite !(@u2Z_shl _ _ _ 30) // !u2Z_Z2u //.
by ring_simplify.
+ rewrite (@u2Z_shl _ _ _ 30) // !u2Z_Z2u // [Zpower _ _]/=.
apply Zlt_le_trans with (4 * 2 ^^ 30) => //; omega.
- by move/Zlt_not_le: (Zlt_neg_0 p).
Qed.
Given an expression e and a store s, the function
eval returns the value of the expression e in store
s:
Fixpoint eval e (s : store.t) :=
match e with
| var_e w => store.get w s
| int_e x => x
| add_e e1 e2 => eval e1 s [.+] eval e2 s
| shl2_e e => eval e s [.<<] 2
end.
Notation "'[' x ']_' s" := (store.get x s) (at level 9) : mips_expr_scope.
Notation "'[' e ']e_' s" := (eval e s) (at level 9) : mips_expr_scope.
Delimit Scope mips_expr_scope with mips_expr.
Local Open Scope mips_expr_scope.
Lemma eval_upd' : forall e x, ~ In x (vars e) ->
forall s m v, [ e ]e_ (store.upd' x v s, m) = [ e ]e_ (s, m).
Proof.
elim => //.
- move=> g x /= g_x s m v.
rewrite store.get_upd_p //; tauto.
- move=> e1 IHe1 e2 IHe2 x /= HnotIn s m v.
rewrite IHe1; last by contradict HnotIn; apply in_or_app; left.
rewrite IHe2 //; by contradict HnotIn; apply in_or_app; right.
- move=> e IH x /= HnotIn s m v; by rewrite IH.
Qed.
Lemma eval_upd : forall e x, ~ In x (vars e) ->
forall s v, [ e ]e_ (store.upd x v s) = [ e ]e_ s.
Proof.
move=> e x H [s m] v /=.
case/orP : (orbN (x == r0)) => [->//|].
move/negbTE => ->; by rewrite eval_upd'.
Qed.
Lemma eval_inde_multiplier : forall e s m m', [ e ]e_ (s, m) = [ e ]e_ (s, m').
Proof.
elim=> //.
- move=> e1 H1 e2 H2 s m m' /=; f_equal; by [apply H1 | apply H2].
- move=> e IH s m m' /=; f_equal; by apply IH.
Qed.
Lemma eval_var_upd : forall x v s, x <> r0 ->
[ var_e x ]e_(store.upd x v s) = v.
Proof. move=> x0 v s H. by rewrite /= store.get_upd'. Qed.
match e with
| var_e w => store.get w s
| int_e x => x
| add_e e1 e2 => eval e1 s [.+] eval e2 s
| shl2_e e => eval e s [.<<] 2
end.
Notation "'[' x ']_' s" := (store.get x s) (at level 9) : mips_expr_scope.
Notation "'[' e ']e_' s" := (eval e s) (at level 9) : mips_expr_scope.
Delimit Scope mips_expr_scope with mips_expr.
Local Open Scope mips_expr_scope.
Lemma eval_upd' : forall e x, ~ In x (vars e) ->
forall s m v, [ e ]e_ (store.upd' x v s, m) = [ e ]e_ (s, m).
Proof.
elim => //.
- move=> g x /= g_x s m v.
rewrite store.get_upd_p //; tauto.
- move=> e1 IHe1 e2 IHe2 x /= HnotIn s m v.
rewrite IHe1; last by contradict HnotIn; apply in_or_app; left.
rewrite IHe2 //; by contradict HnotIn; apply in_or_app; right.
- move=> e IH x /= HnotIn s m v; by rewrite IH.
Qed.
Lemma eval_upd : forall e x, ~ In x (vars e) ->
forall s v, [ e ]e_ (store.upd x v s) = [ e ]e_ s.
Proof.
move=> e x H [s m] v /=.
case/orP : (orbN (x == r0)) => [->//|].
move/negbTE => ->; by rewrite eval_upd'.
Qed.
Lemma eval_inde_multiplier : forall e s m m', [ e ]e_ (s, m) = [ e ]e_ (s, m').
Proof.
elim=> //.
- move=> e1 H1 e2 H2 s m m' /=; f_equal; by [apply H1 | apply H2].
- move=> e IH s m m' /=; f_equal; by apply IH.
Qed.
Lemma eval_var_upd : forall x v s, x <> r0 ->
[ var_e x ]e_(store.upd x v s) = v.
Proof. move=> x0 v s H. by rewrite /= store.get_upd'. Qed.
Control-flow commands are parameterized by a type for boolean tests:
Inductive expr_b : Type :=
| beq : reg -> reg -> expr_b
| bne : reg -> reg -> expr_b
| bltz : reg -> expr_b
| bgez : reg -> expr_b
| blez : reg -> expr_b
| bgtz : reg -> expr_b.
Definition vars_b (e : expr_b) : list reg :=
match e with
| beq r1 r2 => add_set regP r1 (r2 :: nil)
| bne r1 r2 => add_set regP r1 (r2 :: nil)
| bltz r => r :: nil
| bgez r => r :: nil
| blez r => r :: nil
| bgtz r => r :: nil
end.
Definition neg t :=
match t with
| beq r1 r2 => bne r1 r2
| bne r1 r2 => beq r1 r2
| bltz r => bgez r
| bgez r => bltz r
| blez r => bgtz r
| bgtz r => blez r
end.
Definition eval_b (t : expr_b) (s : store.t) : bool :=
match t with
| beq r1 r2 => u2Z (store.get r1 s) == u2Z (store.get r2 s)
| bne r1 r2 => negb (u2Z (store.get r1 s) == u2Z (store.get r2 s))
| bltz r => Zlt_bool (s2Z (store.get r s)) 0
| bgez r => Zle_bool 0 (s2Z (store.get r s))
| blez r => Zle_bool (s2Z (store.get r s)) 0
| bgtz r => Zlt_bool 0 (s2Z (store.get r s))
end.
Lemma eval_b_neg : forall t s, eval_b (neg t) s = ~~ eval_b t s.
Proof.
case => //=.
move=> r r' s; by rewrite negb_involutive.
move=> r s; by rewrite Zle_bool_Zlt_bool.
move=> r s; rewrite Zle_bool_Zlt_bool; by apply negbRL.
move=> r s; by rewrite Zle_bool_Zlt_bool negb_involutive.
by move=> r s; rewrite Zle_bool_Zlt_bool.
Qed.
End expr_m.
| beq : reg -> reg -> expr_b
| bne : reg -> reg -> expr_b
| bltz : reg -> expr_b
| bgez : reg -> expr_b
| blez : reg -> expr_b
| bgtz : reg -> expr_b.
Definition vars_b (e : expr_b) : list reg :=
match e with
| beq r1 r2 => add_set regP r1 (r2 :: nil)
| bne r1 r2 => add_set regP r1 (r2 :: nil)
| bltz r => r :: nil
| bgez r => r :: nil
| blez r => r :: nil
| bgtz r => r :: nil
end.
Definition neg t :=
match t with
| beq r1 r2 => bne r1 r2
| bne r1 r2 => beq r1 r2
| bltz r => bgez r
| bgez r => bltz r
| blez r => bgtz r
| bgtz r => blez r
end.
Definition eval_b (t : expr_b) (s : store.t) : bool :=
match t with
| beq r1 r2 => u2Z (store.get r1 s) == u2Z (store.get r2 s)
| bne r1 r2 => negb (u2Z (store.get r1 s) == u2Z (store.get r2 s))
| bltz r => Zlt_bool (s2Z (store.get r s)) 0
| bgez r => Zle_bool 0 (s2Z (store.get r s))
| blez r => Zle_bool (s2Z (store.get r s)) 0
| bgtz r => Zlt_bool 0 (s2Z (store.get r s))
end.
Lemma eval_b_neg : forall t s, eval_b (neg t) s = ~~ eval_b t s.
Proof.
case => //=.
move=> r r' s; by rewrite negb_involutive.
move=> r s; by rewrite Zle_bool_Zlt_bool.
move=> r s; rewrite Zle_bool_Zlt_bool; by apply negbRL.
move=> r s; by rewrite Zle_bool_Zlt_bool negb_involutive.
by move=> r s; rewrite Zle_bool_Zlt_bool.
Qed.
End expr_m.
Require finmap.
Module Int32 <: finmap.EQTYPE.
Definition A : eqType := int_32_eqType.
End Int32.
Module heap := finmap.map order.NatOrder Int32.
Module heap_tac_m := finmap.Map_Tac heap.
Notation "k '---' l" := (heap.dif k l) (at level 69) : heap_scope.
Notation "k '+++' m" := (heap.union k m) (at level 69) : heap_scope.
Notation "k '#' m" := (heap.disj k m) (at level 79) : heap_scope.
Notation "k '[\m]' m" := (heap.difs k m) (at level 69) : heap_scope.
Local Open Scope heap_scope.
Module assert_m.
Assertions are encoded as truth-functions from states to
Prop, the type of predicates in Coq (this technique
is called shallow embedding). Using this type,
one can easily encode any first-order predicate.
Definition assert := store.t -> heap.t -> Prop.
Require while.
Definition FF : assert := while.FF store.t heap.t.
Definition TT : assert := while.TT store.t heap.t.
Definition Not (P : assert) : assert := while.Not P.
Notation "P '//\\' Q" := (while.And store.t heap.t P Q) (at level 80, no associativity) : mips_assert_scope.
Notation "P '\\//' Q" := (while.Or store.t heap.t P Q) (at level 80, no associativity) : mips_assert_scope.
Notation "P ===> Q" := (while.entails store.t heap.t P Q) (at level 90, no associativity) : mips_assert_scope.
Notation "P <==> Q" := (while.equiv store.t heap.t P Q) (at level 90, no associativity) : mips_assert_scope.
Delimit Scope mips_assert_scope with mips_assert.
Local Open Scope mips_assert_scope.
Import expr_m.
Local Open Scope mips_expr_scope.
Definition x_EQ_y (x y : reg) : assert := fun s _ => [ x ]_ s = [ y ]_ s .
Local Open Scope heap_scope.
Require while.
Definition FF : assert := while.FF store.t heap.t.
Definition TT : assert := while.TT store.t heap.t.
Definition Not (P : assert) : assert := while.Not P.
Notation "P '//\\' Q" := (while.And store.t heap.t P Q) (at level 80, no associativity) : mips_assert_scope.
Notation "P '\\//' Q" := (while.Or store.t heap.t P Q) (at level 80, no associativity) : mips_assert_scope.
Notation "P ===> Q" := (while.entails store.t heap.t P Q) (at level 90, no associativity) : mips_assert_scope.
Notation "P <==> Q" := (while.equiv store.t heap.t P Q) (at level 90, no associativity) : mips_assert_scope.
Delimit Scope mips_assert_scope with mips_assert.
Local Open Scope mips_assert_scope.
Import expr_m.
Local Open Scope mips_expr_scope.
Definition x_EQ_y (x y : reg) : assert := fun s _ => [ x ]_ s = [ y ]_ s .
Local Open Scope heap_scope.
The separating conjunction P ** Q
holds in a state whose heap can be divided into two disj heaps such that
P and Q hold:
Definition con (P Q : assert) : assert := fun s h =>
exists h1, exists h2, h1 # h2 /\ h = h1 +++ h2 /\ P s h1 /\ Q s h2.
Notation "P ** Q" := (con P Q) (at level 80) : mips_assert_scope.
Lemma con_cons : forall (P Q : assert) s h1 h2, h1 # h2 ->
P s h1 -> Q s h2 -> (P ** Q) s (h1 +++ h2).
Proof. move=> P Q s h1 h2 ? ? ?; exists h1; exists h2; repeat (split => //). Qed.
Lemma semi_distributivity : forall (P1 P2 Q : assert), (P1 //\\ P2) ** Q ===> (P1 ** Q) //\\ (P2 ** Q).
Proof. move=> ? ? ? ? ? [h1 [h2 [? [? [[? ?] ?]]]]]; split; exists h1; exists h2 => //. Qed.
exists h1, exists h2, h1 # h2 /\ h = h1 +++ h2 /\ P s h1 /\ Q s h2.
Notation "P ** Q" := (con P Q) (at level 80) : mips_assert_scope.
Lemma con_cons : forall (P Q : assert) s h1 h2, h1 # h2 ->
P s h1 -> Q s h2 -> (P ** Q) s (h1 +++ h2).
Proof. move=> P Q s h1 h2 ? ? ?; exists h1; exists h2; repeat (split => //). Qed.
Lemma semi_distributivity : forall (P1 P2 Q : assert), (P1 //\\ P2) ** Q ===> (P1 ** Q) //\\ (P2 ** Q).
Proof. move=> ? ? ? ? ? [h1 [h2 [? [? [[? ?] ?]]]]]; split; exists h1; exists h2 => //. Qed.
Extensionality of predicates can be safely added to Coq (see Coq FAQ)
Axiom assert_ext : forall P Q, (P <==> Q) -> P = Q.
Lemma And_com_equiv : forall P Q, (P //\\ Q) = (Q //\\ P).
Proof. move=> P Q; apply assert_ext=> s h; split; case=> HP HQ //. Qed.
Lemma con_com : forall P Q, P ** Q ===> Q ** P.
Proof.
move=> P Q s h [h1 [h2 [Ha [Hb [Hc Hd]]]]].
exists h2; exists h1.
split.
by apply heap.disj_sym.
split => //.
apply trans_eq with (h1 +++ h2) => //.
by apply heap.union_com.
Qed.
Lemma con_com_equiv : forall P Q, (P ** Q) = (Q ** P).
Proof. move=> P Q; apply assert_ext => s h; split => H; by apply con_com. Qed.
Module map_tac_m := finmap.Map_Tac heap.
Lemma con_assoc: forall P Q R, (P ** Q) ** R ===> P ** (Q ** R).
Proof.
move=> P Q R s h [h12 [h3 [H1 [H2 [H3 H4]]]]].
case: H3 => [h1 [h2 [H5 [H6 [H7 H8]]]]].
exists h1, (h2 +++ h3).
split.
- apply heap.disj_union_R => //.
by map_tac_m.Disj.
- split.
+ by rewrite heap.union_assoc H2 H6.
+ split => //.
exists h2, h3.
split => //.
by map_tac_m.Disj.
Qed.
Lemma con_assoc_equiv : forall P Q R, ((Q ** P) ** R) = (Q ** (P ** R)).
Proof.
move=> P Q R; apply assert_ext=> s h.
split; case=> h1 [h2 [H1 [H2 [H3 H4]]]].
- case: H3 => h11 [h12 [H31 [ H32 [ H33 H34]]]].
exists h11, (h12 +++ h2).
repeat (split => // || map_tac_m.Disj || map_tac_m.Equal).
exists h12, h2.
repeat (split => // || map_tac_m.Disj || map_tac_m.Equal).
- case: H4 => h21 [h22 [H41 [H42 [H43 H44]]]].
exists (h1 +++ h21), h22.
repeat (split => // || map_tac_m.Disj || map_tac_m.Equal).
exists h1, h21.
repeat (split => // || map_tac_m.Disj || map_tac_m.Equal).
Qed.
Lemma con_TT : forall P, P ===> P ** TT.
Proof.
move=> P s h.
exists h; exists heap.emp; split.
by apply heap.disj_emp_R.
by rewrite heap.union_emp_R.
Qed.
Lemma con_Q_con_TT : forall P Q, P ** Q ===> P ** TT.
Proof.
move=> P Q s h [h1 [h2 [H1 [H2 [H3 H4]]]]].
by exists h1, h2.
Qed.
Lemma monotony : forall (P1 P2 Q1 Q2 : assert) sm sm' h,
(forall h', P1 sm h' -> P2 sm' h') ->
(forall h', Q1 sm h' -> Q2 sm' h') ->
(P1 ** Q1) sm h -> (P2 ** Q2) sm' h.
Proof.
move=> P1 P2 Q1 Q2 sm sm' h H1 H2 [h1 [h2 [H3 [H4 [H5 H6]]]]].
exists h1, h2; repeat (split; eauto).
Qed.
Definition emp : assert := fun s h => h = heap.emp.
Lemma con_emp: forall P, P ** assert_m.emp ===> P.
Proof.
move=> P s h [h1 [h2 [Hdisj [Hunion [HPh1 Hemph2]]]]].
rewrite /emp in Hemph2; subst h2.
by rewrite Hunion heap.union_emp_R.
Qed.
Lemma con_emp': forall P, P ===> P ** assert_m.emp.
Proof.
move=> P s h H.
exists h; exists heap.emp; repeat (split => //).
by apply heap.disj_emp_R.
by rewrite heap.union_emp_R.
Qed.
Lemma con_emp_equiv : forall P, (P ** assert_m.emp) = P.
Proof. move=>P; apply assert_ext; split; [apply con_emp | apply con_emp']. Qed.
Definition imp (P Q : assert) : assert := fun s h =>
forall h', h # h' /\ P s h' -> forall h'', h'' = h +++ h' -> Q s h''.
Notation "P -* Q" := (imp P Q) (at level 80) : mips_assert_scope.
Lemma mp : forall P Q, Q ** (Q -* P) ===> P.
Proof.
move=> P Q s h [h1 [h2 [Hh1h2disj [Hh1h2union [HQh1 HQimpP]]]]].
apply HQimpP with h1.
split => //.
apply heap.disj_sym => //.
rewrite heap.union_com => //; by apply heap.disj_sym.
Qed.
Lemma pm : forall P Q, Q ===> P -* (P ** Q).
Proof.
move=> P Q s h HQ h' [Hhh'disj HPh'] h'' Hhh'union.
exists h'; exists h; repeat (split => //).
apply heap.disj_sym => //.
rewrite heap.union_com => //; by apply heap.disj_sym.
Qed.
Lemma currying : forall (P1 P2 P3 : assert) s,
(forall h, (P1 ** P2) s h -> P3 s h) ->
(forall h, P1 s h -> (P2 -* P3) s h).
Proof.
move=> P1 P2 P3 s H h H' h' [H1 H2] h'' H3.
apply H => //; by exists h, h'.
Qed.
Lemma uncurrying : forall (P1 P2 P3 : assert) s,
(forall h, P1 s h -> (P2 -* P3) s h) ->
(forall h, (P1 ** P2) s h -> P3 s h).
Proof.
move=> P1 P2 P3 s H h [h1 [h2 [H1 [H2 [HP1h1 H4]]]]].
apply H in HP1h1; by eapply HP1h1; eauto.
Qed.
Definition strictly_exact (P : assert) := forall s h h', P s h /\ P s h' -> h = h'.
Lemma strictly_exact_prop : forall P Q,
strictly_exact Q -> P //\\ (Q ** TT) ===> Q ** (Q -* P).
Proof.
move=> P Q HQ s h [H1 [h1 [h2 [H2 [H3 [H4 _]]]]]].
exists h1; exists h2; repeat (split => //).
move => h' [H'1 H'2] h'' H''.
have [->//] : h'' = h.
by rewrite H'' H3 (HQ _ _ _ (conj H4 H'2)) // heap.union_com.
Qed.
Definition domain_exact (P : assert) :=
forall s h h', P s h /\ P s h' -> heap.dom h = heap.dom h'.
Lemma And_com_equiv : forall P Q, (P //\\ Q) = (Q //\\ P).
Proof. move=> P Q; apply assert_ext=> s h; split; case=> HP HQ //. Qed.
Lemma con_com : forall P Q, P ** Q ===> Q ** P.
Proof.
move=> P Q s h [h1 [h2 [Ha [Hb [Hc Hd]]]]].
exists h2; exists h1.
split.
by apply heap.disj_sym.
split => //.
apply trans_eq with (h1 +++ h2) => //.
by apply heap.union_com.
Qed.
Lemma con_com_equiv : forall P Q, (P ** Q) = (Q ** P).
Proof. move=> P Q; apply assert_ext => s h; split => H; by apply con_com. Qed.
Module map_tac_m := finmap.Map_Tac heap.
Lemma con_assoc: forall P Q R, (P ** Q) ** R ===> P ** (Q ** R).
Proof.
move=> P Q R s h [h12 [h3 [H1 [H2 [H3 H4]]]]].
case: H3 => [h1 [h2 [H5 [H6 [H7 H8]]]]].
exists h1, (h2 +++ h3).
split.
- apply heap.disj_union_R => //.
by map_tac_m.Disj.
- split.
+ by rewrite heap.union_assoc H2 H6.
+ split => //.
exists h2, h3.
split => //.
by map_tac_m.Disj.
Qed.
Lemma con_assoc_equiv : forall P Q R, ((Q ** P) ** R) = (Q ** (P ** R)).
Proof.
move=> P Q R; apply assert_ext=> s h.
split; case=> h1 [h2 [H1 [H2 [H3 H4]]]].
- case: H3 => h11 [h12 [H31 [ H32 [ H33 H34]]]].
exists h11, (h12 +++ h2).
repeat (split => // || map_tac_m.Disj || map_tac_m.Equal).
exists h12, h2.
repeat (split => // || map_tac_m.Disj || map_tac_m.Equal).
- case: H4 => h21 [h22 [H41 [H42 [H43 H44]]]].
exists (h1 +++ h21), h22.
repeat (split => // || map_tac_m.Disj || map_tac_m.Equal).
exists h1, h21.
repeat (split => // || map_tac_m.Disj || map_tac_m.Equal).
Qed.
Lemma con_TT : forall P, P ===> P ** TT.
Proof.
move=> P s h.
exists h; exists heap.emp; split.
by apply heap.disj_emp_R.
by rewrite heap.union_emp_R.
Qed.
Lemma con_Q_con_TT : forall P Q, P ** Q ===> P ** TT.
Proof.
move=> P Q s h [h1 [h2 [H1 [H2 [H3 H4]]]]].
by exists h1, h2.
Qed.
Lemma monotony : forall (P1 P2 Q1 Q2 : assert) sm sm' h,
(forall h', P1 sm h' -> P2 sm' h') ->
(forall h', Q1 sm h' -> Q2 sm' h') ->
(P1 ** Q1) sm h -> (P2 ** Q2) sm' h.
Proof.
move=> P1 P2 Q1 Q2 sm sm' h H1 H2 [h1 [h2 [H3 [H4 [H5 H6]]]]].
exists h1, h2; repeat (split; eauto).
Qed.
Definition emp : assert := fun s h => h = heap.emp.
Lemma con_emp: forall P, P ** assert_m.emp ===> P.
Proof.
move=> P s h [h1 [h2 [Hdisj [Hunion [HPh1 Hemph2]]]]].
rewrite /emp in Hemph2; subst h2.
by rewrite Hunion heap.union_emp_R.
Qed.
Lemma con_emp': forall P, P ===> P ** assert_m.emp.
Proof.
move=> P s h H.
exists h; exists heap.emp; repeat (split => //).
by apply heap.disj_emp_R.
by rewrite heap.union_emp_R.
Qed.
Lemma con_emp_equiv : forall P, (P ** assert_m.emp) = P.
Proof. move=>P; apply assert_ext; split; [apply con_emp | apply con_emp']. Qed.
Definition imp (P Q : assert) : assert := fun s h =>
forall h', h # h' /\ P s h' -> forall h'', h'' = h +++ h' -> Q s h''.
Notation "P -* Q" := (imp P Q) (at level 80) : mips_assert_scope.
Lemma mp : forall P Q, Q ** (Q -* P) ===> P.
Proof.
move=> P Q s h [h1 [h2 [Hh1h2disj [Hh1h2union [HQh1 HQimpP]]]]].
apply HQimpP with h1.
split => //.
apply heap.disj_sym => //.
rewrite heap.union_com => //; by apply heap.disj_sym.
Qed.
Lemma pm : forall P Q, Q ===> P -* (P ** Q).
Proof.
move=> P Q s h HQ h' [Hhh'disj HPh'] h'' Hhh'union.
exists h'; exists h; repeat (split => //).
apply heap.disj_sym => //.
rewrite heap.union_com => //; by apply heap.disj_sym.
Qed.
Lemma currying : forall (P1 P2 P3 : assert) s,
(forall h, (P1 ** P2) s h -> P3 s h) ->
(forall h, P1 s h -> (P2 -* P3) s h).
Proof.
move=> P1 P2 P3 s H h H' h' [H1 H2] h'' H3.
apply H => //; by exists h, h'.
Qed.
Lemma uncurrying : forall (P1 P2 P3 : assert) s,
(forall h, P1 s h -> (P2 -* P3) s h) ->
(forall h, (P1 ** P2) s h -> P3 s h).
Proof.
move=> P1 P2 P3 s H h [h1 [h2 [H1 [H2 [HP1h1 H4]]]]].
apply H in HP1h1; by eapply HP1h1; eauto.
Qed.
Definition strictly_exact (P : assert) := forall s h h', P s h /\ P s h' -> h = h'.
Lemma strictly_exact_prop : forall P Q,
strictly_exact Q -> P //\\ (Q ** TT) ===> Q ** (Q -* P).
Proof.
move=> P Q HQ s h [H1 [h1 [h2 [H2 [H3 [H4 _]]]]]].
exists h1; exists h2; repeat (split => //).
move => h' [H'1 H'2] h'' H''.
have [->//] : h'' = h.
by rewrite H'' H3 (HQ _ _ _ (conj H4 H'2)) // heap.union_com.
Qed.
Definition domain_exact (P : assert) :=
forall s h h', P s h /\ P s h' -> heap.dom h = heap.dom h'.
The mapsto connective e1 |~> e2 holds in a state with a store s and a
singleton heap with address eval e1 s and
contents eval e2 s, under the restriction that
the heap-location is word-aligned:
Definition mapsto e e' : assert := fun s h =>
exists p, u2Z ([ e ]e_ s) = 4 * Z_of_nat p /\ h = heap.sing p ([ e' ]e_ s).
Notation "e1 |~> e2" := (mapsto e1 e2) (at level 77) : mips_assert_scope.
Lemma singl_equal : forall s h1 h2 e1 e2 e3 e4,
(e1 |~> e2) s h1 -> (e3 |~> e4) s h2 ->
[ e1 ]e_ s = [ e3 ]e_ s -> [ e2 ]e_ s = [ e4 ]e_ s -> h1 = h2.
Proof.
move=> s h1 h2 e1 e2 e3 e4 [p [H1 ->]] [p' [H3 ->]] Heq1 ->; f_equal.
rewrite Heq1 in H1; omega.
Qed.
Lemma mapsto_con_get : forall st h e1 e2 P, (e1 |~> e2 ** P) st h ->
heap.get (Zabs_nat (u2Z ([ e1 ]e_ st) / 4)) h = Some ([ e2 ]e_ st).
Proof.
move=> st h e1 e2 P [h1 [h2 [h1dh2 [-> [[p [Hh1 Hh1']] _]]]]]; apply heap.get_union_L => //.
by rewrite Hh1' Hh1 Zmult_comm Z_div_mult // Zabs_nat_Z_of_nat heap.get_sing.
Qed.
Lemma mapsto_inv_addr : forall e e' st h, (e |~> e') st h ->
u2Z ([ e ]e_ st) mod 4 = 0.
Proof. move=> e e' st h [e4 [-> _]]; by rewrite Zmult_comm Z_mod_mult. Qed.
Lemma mapsto_inj : forall e a b st h, (e |~> a) st h -> (e |~> b) st h ->
[ a ]e_ st = [ b ]e_ st.
Proof.
move=> e a b st h [pa [Hpa1 Hpa2]] [pb [Hpb1 Hpb2]].
have : pa = pb by omega.
move=> ?; subst pb.
rewrite Hpa2 in Hpb2.
by move/heap.sing_inj : Hpb2.
Qed.
Lemma mapsto_con_inj : forall e a b P Q st h,
(e |~> a ** P) st h -> (e |~> b ** Q) st h -> [ a ]e_ st = [ b ]e_ st.
Proof.
move=> e a b P Q st h; move/mapsto_con_get=> Ha; move/mapsto_con_get=> Hb.
rewrite Ha in Hb; by case: Hb.
Qed.
Lemma mapsto_ext : forall e1 e2 sm' e3 e4 sm h,
[ e1 ]e_ sm' = [ e3 ]e_ sm -> [ e2 ]e_ sm' = [ e4 ]e_ sm ->
(e1 |~> e2) sm' h -> (e3 |~> e4) sm h.
Proof.
move=> e1 e2 sm' e3 e4 sm h H1 H2 [p [Hp Hh]].
exists p; split; by rewrite -?H1 -?H2.
Qed.
exists p, u2Z ([ e ]e_ s) = 4 * Z_of_nat p /\ h = heap.sing p ([ e' ]e_ s).
Notation "e1 |~> e2" := (mapsto e1 e2) (at level 77) : mips_assert_scope.
Lemma singl_equal : forall s h1 h2 e1 e2 e3 e4,
(e1 |~> e2) s h1 -> (e3 |~> e4) s h2 ->
[ e1 ]e_ s = [ e3 ]e_ s -> [ e2 ]e_ s = [ e4 ]e_ s -> h1 = h2.
Proof.
move=> s h1 h2 e1 e2 e3 e4 [p [H1 ->]] [p' [H3 ->]] Heq1 ->; f_equal.
rewrite Heq1 in H1; omega.
Qed.
Lemma mapsto_con_get : forall st h e1 e2 P, (e1 |~> e2 ** P) st h ->
heap.get (Zabs_nat (u2Z ([ e1 ]e_ st) / 4)) h = Some ([ e2 ]e_ st).
Proof.
move=> st h e1 e2 P [h1 [h2 [h1dh2 [-> [[p [Hh1 Hh1']] _]]]]]; apply heap.get_union_L => //.
by rewrite Hh1' Hh1 Zmult_comm Z_div_mult // Zabs_nat_Z_of_nat heap.get_sing.
Qed.
Lemma mapsto_inv_addr : forall e e' st h, (e |~> e') st h ->
u2Z ([ e ]e_ st) mod 4 = 0.
Proof. move=> e e' st h [e4 [-> _]]; by rewrite Zmult_comm Z_mod_mult. Qed.
Lemma mapsto_inj : forall e a b st h, (e |~> a) st h -> (e |~> b) st h ->
[ a ]e_ st = [ b ]e_ st.
Proof.
move=> e a b st h [pa [Hpa1 Hpa2]] [pb [Hpb1 Hpb2]].
have : pa = pb by omega.
move=> ?; subst pb.
rewrite Hpa2 in Hpb2.
by move/heap.sing_inj : Hpb2.
Qed.
Lemma mapsto_con_inj : forall e a b P Q st h,
(e |~> a ** P) st h -> (e |~> b ** Q) st h -> [ a ]e_ st = [ b ]e_ st.
Proof.
move=> e a b P Q st h; move/mapsto_con_get=> Ha; move/mapsto_con_get=> Hb.
rewrite Ha in Hb; by case: Hb.
Qed.
Lemma mapsto_ext : forall e1 e2 sm' e3 e4 sm h,
[ e1 ]e_ sm' = [ e3 ]e_ sm -> [ e2 ]e_ sm' = [ e4 ]e_ sm ->
(e1 |~> e2) sm' h -> (e3 |~> e4) sm h.
Proof.
move=> e1 e2 sm' e3 e4 sm h H1 H2 [p [Hp Hh]].
exists p; split; by rewrite -?H1 -?H2.
Qed.
Using the separating conjunction, the mapsto connective can be generalized
to arrays of words: e |--> a::b::... holds in a state whose heap
contains a list of contiguous words a, b, etc. starting at address
eval e s:
Fixpoint mapstos e l : assert :=
match l with
| nil => fun st h => u2Z ([ e ]e_st) mod 4 = 0 /\ emp st h
| hd :: tl => (e |~> int_e hd) ** (mapstos (add_e e (int_e four32)) tl)
end.
Notation "x '|-->' l" := (mapstos x l) (at level 77) : mips_assert_scope.
Module map_prop_m := finmap.Map_Prop heap.
Lemma mapstos_inv_emp : forall l e st, (e |--> l) st heap.emp -> l = nil.
Proof.
elim=> // hd tl IH e st /= [h1 [h2 [Hdisj [Hunion [Hh1 Hh2]]]]].
case/heap.union_emp_inv : Hunion => H1 H2; subst h1 h2.
case: Hh1 => p [Hp].
by case/map_prop_m.emp_sing_dis.
Qed.
Lemma mapstos_inv_addr : forall l e st h, (e |--> l) st h -> u2Z ([ e ]e_ st) mod 4 = 0.
Proof.
case.
- rewrite /= => e st h [H1 H2].
rewrite /emp in H2; by subst h.
- move => hd tl e st h /= [h1 [h2 [Hdisj [Hunion [[p [Hp1 Hp2]] Hh2]]]]].
by rewrite Hp1 Zmult_comm Z_mod_mult.
Qed.
Local Open Scope machine_int_scope.
Lemma mapsto1_mapstos : forall e1 e2, (e1 |~> int_e e2) = (e1 |--> e2 :: nil).
Proof.
move=> e1 e2.
apply assert_m.assert_ext; split.
case=> p [H1 H2] /=.
exists h; exists heap.emp.
split; first by apply heap.disj_emp_R.
split; first by rewrite heap.union_emp_R.
split; first by exists p.
split; last by done.
rewrite u2Z_add_mod //.
by rewrite H1 Zmult_comm Z_mod_mult.
case=> h1 [h2 [h1dh2 [h1Uh2 [Hh1 [Hh2 Hh2']]]]].
by rewrite h1Uh2 Hh2' heap.union_emp_R.
Qed.
Lemma mapsto2_mapstos : forall e1 e2 e3,
(e1 |~> int_e e2 ** add_e e1 (int_e four32) |~> int_e e3) = (e1 |--> e2 :: e3 :: nil).
Proof.
move=> e1 e2 e3.
apply assert_m.assert_ext; split.
rewrite [List.cons e3 _]lock /= -lock.
apply assert_m.monotony => // h'.
by rewrite mapsto1_mapstos.
rewrite [List.cons e3 _]lock /= -lock.
apply assert_m.monotony => // h'.
by rewrite mapsto1_mapstos.
Qed.
Local Close Scope machine_int_scope.
Lemma mapstos_inv_dom : forall L e st h, u2Z ([ e ]e_st) + 4 * Z_of_nat (length L) < Zbeta 1 ->
(e |--> L) st h ->
seq (Zabs_nat (u2Z ([ e ]e_ st) / 4)) (length L) = seq_ext.s2l (heap.dom h).
Proof.
elim.
- move=> e st h /= _ [Hheap1 Hheap2].
rewrite /assert_m.emp in Hheap2.
by rewrite Hheap2 heap.dom_emp /=.
- move=> hd tl IH s st h Hfit /= [h1 [h2 [Hdisj [Hunion [[p [Hp Hh1]] Hh2]]]]].
rewrite [length _]/= Z_S in Hfit.
rewrite Hunion Hh1 heap.dom_union_sing /=.
+ rewrite Hp Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat; f_equal.
have -> : S p = Zabs_nat (u2Z ([ add_e s (int_e four32) ]e_ st) / 4).
have -> : p = Zabs_nat (u2Z ([ s ]e_ st)%mips_expr / 4).
by rewrite Hp Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat.
rewrite /= u2Z_add_Z2u //.
* rewrite {2}(_ : 4 = 1 * 4) // Z_div_plus_full // S_Zabs_nat //.
apply Z_div_pos => //.
by apply min_u2Z.
* rewrite -Zbeta1_Zpower2; omega.
apply IH => //.
rewrite [u2Z _]/= u2Z_add_Z2u //.
* omega.
* rewrite -Zbeta1_Zpower2; omega.
+ move=> m Hm.
have : u2Z ([ add_e s (int_e four32) ]e_ st) + 4 * Z_of_nat (length tl) < Zbeta 1.
rewrite [eval _ _]/= u2Z_add_Z2u //; last by rewrite -Zbeta1_Zpower2; omega.
omega.
move/(IH _ _ h2).
move/(_ Hh2).
rewrite [ [ _ ]e_ _ ]/= u2Z_add_Z2u // Hp; last by rewrite -Zbeta1_Zpower2; omega.
rewrite {2}(_ : 4 = 1 * 4) // Z_div_plus_full // Zmult_comm Z_div_mult_full //.
move/seq_ext.inP : Hm => Hm.
move=> X; rewrite -X in Hm.
case/In_seq_inv : Hm => Hm1 Hm2.
rewrite /heap.ltl /order.NatOrder.ltA.
apply/ssrnat.ltP.
rewrite Zabs_nat_plus_pos // in Hm1; last by apply Zle_0_nat.
rewrite Zabs_nat_Z_of_nat (_ : Zabs_nat 1 = 1%nat) // in Hm1; omega.
Qed.
Lemma mapstos_inv_cdom : forall lst e s h,
u2Z ([ e ]e_s)%mips_expr + 4 * Z_of_nat (length lst) < Zbeta 1 ->
(e |--> lst)%mips_assert s h ->
seq_ext.s2l (heap.cdom h) = List.map (fun e => [ int_e e ]e_s)%mips_expr lst.
Proof.
elim.
rewrite /= => e s h _ [H1 H2].
by rewrite H2 heap.cdom_emp.
move=> hd tl IH e s h H /=.
case=> h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh1 => p [Hp Hh1].
rewrite h1_U_h2 Hh1.
have IH' : u2Z [add_e e (int_e four32) ]e_ s + 4 * Z_of_nat (length tl) < Zbeta 1.
simpl u2Z.
simpl length in H.
rewrite Z_S in H.
rewrite u2Z_add_Z2u //.
omega.
rewrite -Zbeta1_Zpower2.
omega.
move/assert_m.mapstos_inv_dom : (Hh2).
move/(_ IH') => Hh2'.
apply IH in Hh2; last first.
done.
rewrite heap.cdom_union.
by rewrite heap.cdom_sing /= Hh2.
move=> i j.
rewrite heap.dom_sing.
rewrite seq.inE.
move/eqP => ?; subst p.
move=> Hj.
move/seq_ext.inP : Hj => Hj.
rewrite -Hh2' in Hj.
apply In_seq_inv in Hj.
rewrite /heap.ltl.
rewrite /order.NatOrder.ltA.
apply/ssrnat.ltP.
rewrite /= in Hj.
case: Hj => Hj _.
rewrite u2Z_add_Z2u // in Hj; last first.
rewrite [length _]/= Z_S in H.
rewrite -Zbeta1_Zpower2; omega.
rewrite Hp Zmult_comm Z_div_plus_full_l // Z_div_same_full // in Hj.
rewrite Zabs_nat_Zplus // in Hj; last first.
by apply Zle_0_nat.
rewrite Zabs_nat_Z_of_nat (_ : Zabs_nat 1 = 1%nat) // in Hj.
omega.
Qed.
Lemma mapstos_inv : forall lst e s h,
u2Z ([ e ]e_s)%mips_expr + 4 * Z_of_nat (length lst) < Zbeta 1 ->
(e |--> lst)%mips_assert s h ->
seq_ext.s2l (heap.dom h) = List.seq (Zabs_nat (u2Z ([ e ]e_ s) / 4)) (length lst) /\
seq_ext.s2l (heap.cdom h) = List.map (fun e => [ int_e e ]e_s)%mips_expr lst.
Proof.
intros.
split.
symmetry.
by apply assert_m.mapstos_inv_dom.
by eapply mapstos_inv_cdom; eauto.
Qed.
Lemma mapstos_inc_inv : forall st h e l, u2Z ([ e ]e_ st) + 4 * Z_of_nat (length l) < Zbeta 1 ->
(e |--> l ** assert_m.TT) st h ->
seq_ext.inc
(seq_ext.l2s ((seq (Zabs_nat (u2Z ([ e ]e_st)%mips_expr / 4)) (length l)) : list heap.l))
(heap.dom h).
Proof.
move=> st h e l Hfit [h1 [h2 [h1dh2 [h1Uh2 [Hh1 Hh2]]]]].
apply/seq_ext.incP => x; move/seq_ext.inP=> Hx.
apply mapstos_inv_dom in Hh1.
- rewrite Hh1 seq_ext.l2s2l in Hx.
rewrite h1Uh2.
apply/seq_ext.inP.
by apply heap.in_dom_union_L.
- exact Hfit.
Qed.
Lemma mapstos_get_inv : forall n l e s h,
length l = n ->
u2Z (eval e s) + 4 * Z_of_nat n < Zbeta 1 ->
(e |--> l)%mips_assert s h ->
forall i elt,
(i < n)%nat ->
ith i l = Some elt ->
heap.get (Zabs_nat (u2Z (eval e s) / 4) + i)%nat%mips_expr h = Some elt.
Proof.
elim.
- case=> //.
move=> x s h _ _ _ i elt.
by inversion 1.
- move=> n IH [|hd tl] // x s h [len_l] Hfit mem [|i] elt.
+ move=> _ /= [?]; subst hd.
case: mem => h1 [h2 [Hunion [Hdisj [Hh1 Hh2]]]].
case: Hh1 => p [Hp Hh1].
by rewrite plus_0_r Hdisj Hh1 Hp Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat heap.get_union_sing_eq /=.
+ move/le_S_n => /= Hi Helt.
rewrite /= in mem.
case: mem => h1 [h2 [Hdisj [Hunion [Hh1 Hh2]]]].
have : u2Z ([ add_e x (int_e four32) ]e_ s)%mips_expr + 4 * Z_of_nat n < Zbeta 1.
rewrite Z_S in Hfit.
rewrite [u2Z _]/= u2Z_add_Z2u //.
omega.
rewrite -Zbeta1_Zpower2; omega.
move/(IH _ (add_e x (int_e four32)) s h2 len_l).
move/(_ Hh2 _ _ Hi Helt).
rewrite [u2Z _]/= u2Z_add_Z2u //; last first.
rewrite Z_S in Hfit; rewrite -Zbeta1_Zpower2; omega.
rewrite -{1}(Zmult_1_l 4) Z_div_plus_full // Zabs_nat_plus_pos //; last first.
apply Z_div_pos => //; apply min_u2Z.
rewrite -plus_assoc /=.
move=> {IH}IH.
rewrite Hunion.
by apply heap.get_union_R.
Qed.
Lemma mapstos_inj : forall n l1 l2 e st h, length l1 = n -> length l2 = n ->
(e |--> l1) st h -> (e |--> l2) st h -> l1 = l2.
Proof.
elim.
- case=> //; by case.
- move=> n IH [|hd1 tl1]// [|hd2 tl2]// e st h /= [H1] [H2]
[h1 [h2 [Hdisj [Hunion [[p1 [Hh11 Hh12]] Hh2]]]]] [h1' [h2' [Hdisj' [Hunion' [[p1' [Hh11' Hh12']] Hh2']]]]].
have : p1 = p1' by omega.
move=> ?; subst p1'.
rewrite Hunion' in Hunion.
move: (heap.union_inv _ _ _ _ Hunion).
rewrite {1}Hh12 {1}Hh12'.
rewrite 2!heap.dom_sing.
move/(_ (refl_equal _)).
apply heap.disj_sym in Hdisj.
apply heap.disj_sym in Hdisj'.
case/(_ Hdisj' Hdisj)=> Hh1 X2; subst h1' h2'.
rewrite (IH _ _ _ _ _ H1 H2 Hh2 Hh2').
f_equal.
rewrite Hh12 in Hh1.
by move/heap.sing_inj : Hh1.
Qed.
Lemma mapstos_con_inj : forall n l1 l2 e st h P Q,
u2Z ([ e ]e_ st) + 4 * Z_of_nat n < Zbeta 1 ->
length l1 = n -> length l2 = n ->
(e |--> l1 ** P) st h -> (e |--> l2 ** Q) st h ->
l1 = l2.
Proof.
move=> n l1 l2 e st h P Q e_fit len_l1 len_l2.
case=> h1 [h2 [h1dh2 [h1Uh2 [Hh1 Hh2]]]].
case=> h1' [h2' [h1'dh2' [h1'Uh2' [Hh1' Hh2']]]].
have : h1 = h1'.
rewrite h1Uh2 in h1'Uh2'.
have dom_h1_h1' : heap.dom h1 = heap.dom h1'.
apply assert_m.mapstos_inv_dom in Hh1; last by rewrite len_l1.
apply assert_m.mapstos_inv_dom in Hh1'; last by rewrite len_l2.
apply seq_ext.s2l_inj => //; last by rewrite -Hh1 -Hh1' len_l1 len_l2.
apply (heap.union_inv h1 h1' h2 h2' h1'Uh2') => //.
by apply heap.disj_sym.
by apply heap.disj_sym.
move=> ?; subst h1'.
by apply assert_m.mapstos_inj with n e st h1.
Qed.
Lemma mapstos_ext : forall l st st' h e e', [ e ]e_st = [ e' ]e_st' ->
(e |--> l) st h -> (e' |--> l) st' h.
Proof.
elim.
- by move=> st st' h e e' /= ->.
- move=> hd tl IH st st' h e0 e' Heq /= [h1 [h2 [Hdisj [Hunion [Hh1 Hh2]]]]].
exists h1, h2; do 2 (split; first by done); split.
+ by move: Hh1; apply mapsto_ext.
+ apply IH with st (add_e e0 (int_e four32)) => //=; by rewrite Heq.
Qed.
Lemma mapsto_get1' : forall s h e e1 P,
(e |~> int_e e1 ** P)%list%mips_assert s h ->
heap.get (Zabs_nat (u2Z ([ e ]e_ s)/ 4)) h = Some e1.
Proof.
move=> s h e e1 P /=.
case=> h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh1 => p [Hp Hh1].
rewrite h1_U_h2.
apply heap.get_union_L => //.
by rewrite Hh1 Hp Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat heap.get_sing.
Qed.
Lemma mapstos_get1 : forall s h e e1 e2 P,
(e |--> e1 :: e2 :: List.nil ** P)%list%mips_assert s h ->
heap.get (Zabs_nat (u2Z ([ e ]e_ s)/ 4)) h = Some e1.
Proof.
move=> s h e e1 e2 P /=.
rewrite assert_m.con_assoc_equiv.
by move/mapsto_get1'.
Qed.
Local Open Scope machine_int_scope.
Lemma mapstos_get2 : forall s h e e1 e2 P,
(e |--> e1 :: e2 :: List.nil ** P) s h ->
heap.get (Zabs_nat (u2Z ([ e ]e_ s [.+] four32)/ 4)) h = Some e2.
Proof.
move=> s h e e1 e2 P /=.
rewrite assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv.
by move/mapsto_get1'.
Qed.
match l with
| nil => fun st h => u2Z ([ e ]e_st) mod 4 = 0 /\ emp st h
| hd :: tl => (e |~> int_e hd) ** (mapstos (add_e e (int_e four32)) tl)
end.
Notation "x '|-->' l" := (mapstos x l) (at level 77) : mips_assert_scope.
Module map_prop_m := finmap.Map_Prop heap.
Lemma mapstos_inv_emp : forall l e st, (e |--> l) st heap.emp -> l = nil.
Proof.
elim=> // hd tl IH e st /= [h1 [h2 [Hdisj [Hunion [Hh1 Hh2]]]]].
case/heap.union_emp_inv : Hunion => H1 H2; subst h1 h2.
case: Hh1 => p [Hp].
by case/map_prop_m.emp_sing_dis.
Qed.
Lemma mapstos_inv_addr : forall l e st h, (e |--> l) st h -> u2Z ([ e ]e_ st) mod 4 = 0.
Proof.
case.
- rewrite /= => e st h [H1 H2].
rewrite /emp in H2; by subst h.
- move => hd tl e st h /= [h1 [h2 [Hdisj [Hunion [[p [Hp1 Hp2]] Hh2]]]]].
by rewrite Hp1 Zmult_comm Z_mod_mult.
Qed.
Local Open Scope machine_int_scope.
Lemma mapsto1_mapstos : forall e1 e2, (e1 |~> int_e e2) = (e1 |--> e2 :: nil).
Proof.
move=> e1 e2.
apply assert_m.assert_ext; split.
case=> p [H1 H2] /=.
exists h; exists heap.emp.
split; first by apply heap.disj_emp_R.
split; first by rewrite heap.union_emp_R.
split; first by exists p.
split; last by done.
rewrite u2Z_add_mod //.
by rewrite H1 Zmult_comm Z_mod_mult.
case=> h1 [h2 [h1dh2 [h1Uh2 [Hh1 [Hh2 Hh2']]]]].
by rewrite h1Uh2 Hh2' heap.union_emp_R.
Qed.
Lemma mapsto2_mapstos : forall e1 e2 e3,
(e1 |~> int_e e2 ** add_e e1 (int_e four32) |~> int_e e3) = (e1 |--> e2 :: e3 :: nil).
Proof.
move=> e1 e2 e3.
apply assert_m.assert_ext; split.
rewrite [List.cons e3 _]lock /= -lock.
apply assert_m.monotony => // h'.
by rewrite mapsto1_mapstos.
rewrite [List.cons e3 _]lock /= -lock.
apply assert_m.monotony => // h'.
by rewrite mapsto1_mapstos.
Qed.
Local Close Scope machine_int_scope.
Lemma mapstos_inv_dom : forall L e st h, u2Z ([ e ]e_st) + 4 * Z_of_nat (length L) < Zbeta 1 ->
(e |--> L) st h ->
seq (Zabs_nat (u2Z ([ e ]e_ st) / 4)) (length L) = seq_ext.s2l (heap.dom h).
Proof.
elim.
- move=> e st h /= _ [Hheap1 Hheap2].
rewrite /assert_m.emp in Hheap2.
by rewrite Hheap2 heap.dom_emp /=.
- move=> hd tl IH s st h Hfit /= [h1 [h2 [Hdisj [Hunion [[p [Hp Hh1]] Hh2]]]]].
rewrite [length _]/= Z_S in Hfit.
rewrite Hunion Hh1 heap.dom_union_sing /=.
+ rewrite Hp Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat; f_equal.
have -> : S p = Zabs_nat (u2Z ([ add_e s (int_e four32) ]e_ st) / 4).
have -> : p = Zabs_nat (u2Z ([ s ]e_ st)%mips_expr / 4).
by rewrite Hp Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat.
rewrite /= u2Z_add_Z2u //.
* rewrite {2}(_ : 4 = 1 * 4) // Z_div_plus_full // S_Zabs_nat //.
apply Z_div_pos => //.
by apply min_u2Z.
* rewrite -Zbeta1_Zpower2; omega.
apply IH => //.
rewrite [u2Z _]/= u2Z_add_Z2u //.
* omega.
* rewrite -Zbeta1_Zpower2; omega.
+ move=> m Hm.
have : u2Z ([ add_e s (int_e four32) ]e_ st) + 4 * Z_of_nat (length tl) < Zbeta 1.
rewrite [eval _ _]/= u2Z_add_Z2u //; last by rewrite -Zbeta1_Zpower2; omega.
omega.
move/(IH _ _ h2).
move/(_ Hh2).
rewrite [ [ _ ]e_ _ ]/= u2Z_add_Z2u // Hp; last by rewrite -Zbeta1_Zpower2; omega.
rewrite {2}(_ : 4 = 1 * 4) // Z_div_plus_full // Zmult_comm Z_div_mult_full //.
move/seq_ext.inP : Hm => Hm.
move=> X; rewrite -X in Hm.
case/In_seq_inv : Hm => Hm1 Hm2.
rewrite /heap.ltl /order.NatOrder.ltA.
apply/ssrnat.ltP.
rewrite Zabs_nat_plus_pos // in Hm1; last by apply Zle_0_nat.
rewrite Zabs_nat_Z_of_nat (_ : Zabs_nat 1 = 1%nat) // in Hm1; omega.
Qed.
Lemma mapstos_inv_cdom : forall lst e s h,
u2Z ([ e ]e_s)%mips_expr + 4 * Z_of_nat (length lst) < Zbeta 1 ->
(e |--> lst)%mips_assert s h ->
seq_ext.s2l (heap.cdom h) = List.map (fun e => [ int_e e ]e_s)%mips_expr lst.
Proof.
elim.
rewrite /= => e s h _ [H1 H2].
by rewrite H2 heap.cdom_emp.
move=> hd tl IH e s h H /=.
case=> h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh1 => p [Hp Hh1].
rewrite h1_U_h2 Hh1.
have IH' : u2Z [add_e e (int_e four32) ]e_ s + 4 * Z_of_nat (length tl) < Zbeta 1.
simpl u2Z.
simpl length in H.
rewrite Z_S in H.
rewrite u2Z_add_Z2u //.
omega.
rewrite -Zbeta1_Zpower2.
omega.
move/assert_m.mapstos_inv_dom : (Hh2).
move/(_ IH') => Hh2'.
apply IH in Hh2; last first.
done.
rewrite heap.cdom_union.
by rewrite heap.cdom_sing /= Hh2.
move=> i j.
rewrite heap.dom_sing.
rewrite seq.inE.
move/eqP => ?; subst p.
move=> Hj.
move/seq_ext.inP : Hj => Hj.
rewrite -Hh2' in Hj.
apply In_seq_inv in Hj.
rewrite /heap.ltl.
rewrite /order.NatOrder.ltA.
apply/ssrnat.ltP.
rewrite /= in Hj.
case: Hj => Hj _.
rewrite u2Z_add_Z2u // in Hj; last first.
rewrite [length _]/= Z_S in H.
rewrite -Zbeta1_Zpower2; omega.
rewrite Hp Zmult_comm Z_div_plus_full_l // Z_div_same_full // in Hj.
rewrite Zabs_nat_Zplus // in Hj; last first.
by apply Zle_0_nat.
rewrite Zabs_nat_Z_of_nat (_ : Zabs_nat 1 = 1%nat) // in Hj.
omega.
Qed.
Lemma mapstos_inv : forall lst e s h,
u2Z ([ e ]e_s)%mips_expr + 4 * Z_of_nat (length lst) < Zbeta 1 ->
(e |--> lst)%mips_assert s h ->
seq_ext.s2l (heap.dom h) = List.seq (Zabs_nat (u2Z ([ e ]e_ s) / 4)) (length lst) /\
seq_ext.s2l (heap.cdom h) = List.map (fun e => [ int_e e ]e_s)%mips_expr lst.
Proof.
intros.
split.
symmetry.
by apply assert_m.mapstos_inv_dom.
by eapply mapstos_inv_cdom; eauto.
Qed.
Lemma mapstos_inc_inv : forall st h e l, u2Z ([ e ]e_ st) + 4 * Z_of_nat (length l) < Zbeta 1 ->
(e |--> l ** assert_m.TT) st h ->
seq_ext.inc
(seq_ext.l2s ((seq (Zabs_nat (u2Z ([ e ]e_st)%mips_expr / 4)) (length l)) : list heap.l))
(heap.dom h).
Proof.
move=> st h e l Hfit [h1 [h2 [h1dh2 [h1Uh2 [Hh1 Hh2]]]]].
apply/seq_ext.incP => x; move/seq_ext.inP=> Hx.
apply mapstos_inv_dom in Hh1.
- rewrite Hh1 seq_ext.l2s2l in Hx.
rewrite h1Uh2.
apply/seq_ext.inP.
by apply heap.in_dom_union_L.
- exact Hfit.
Qed.
Lemma mapstos_get_inv : forall n l e s h,
length l = n ->
u2Z (eval e s) + 4 * Z_of_nat n < Zbeta 1 ->
(e |--> l)%mips_assert s h ->
forall i elt,
(i < n)%nat ->
ith i l = Some elt ->
heap.get (Zabs_nat (u2Z (eval e s) / 4) + i)%nat%mips_expr h = Some elt.
Proof.
elim.
- case=> //.
move=> x s h _ _ _ i elt.
by inversion 1.
- move=> n IH [|hd tl] // x s h [len_l] Hfit mem [|i] elt.
+ move=> _ /= [?]; subst hd.
case: mem => h1 [h2 [Hunion [Hdisj [Hh1 Hh2]]]].
case: Hh1 => p [Hp Hh1].
by rewrite plus_0_r Hdisj Hh1 Hp Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat heap.get_union_sing_eq /=.
+ move/le_S_n => /= Hi Helt.
rewrite /= in mem.
case: mem => h1 [h2 [Hdisj [Hunion [Hh1 Hh2]]]].
have : u2Z ([ add_e x (int_e four32) ]e_ s)%mips_expr + 4 * Z_of_nat n < Zbeta 1.
rewrite Z_S in Hfit.
rewrite [u2Z _]/= u2Z_add_Z2u //.
omega.
rewrite -Zbeta1_Zpower2; omega.
move/(IH _ (add_e x (int_e four32)) s h2 len_l).
move/(_ Hh2 _ _ Hi Helt).
rewrite [u2Z _]/= u2Z_add_Z2u //; last first.
rewrite Z_S in Hfit; rewrite -Zbeta1_Zpower2; omega.
rewrite -{1}(Zmult_1_l 4) Z_div_plus_full // Zabs_nat_plus_pos //; last first.
apply Z_div_pos => //; apply min_u2Z.
rewrite -plus_assoc /=.
move=> {IH}IH.
rewrite Hunion.
by apply heap.get_union_R.
Qed.
Lemma mapstos_inj : forall n l1 l2 e st h, length l1 = n -> length l2 = n ->
(e |--> l1) st h -> (e |--> l2) st h -> l1 = l2.
Proof.
elim.
- case=> //; by case.
- move=> n IH [|hd1 tl1]// [|hd2 tl2]// e st h /= [H1] [H2]
[h1 [h2 [Hdisj [Hunion [[p1 [Hh11 Hh12]] Hh2]]]]] [h1' [h2' [Hdisj' [Hunion' [[p1' [Hh11' Hh12']] Hh2']]]]].
have : p1 = p1' by omega.
move=> ?; subst p1'.
rewrite Hunion' in Hunion.
move: (heap.union_inv _ _ _ _ Hunion).
rewrite {1}Hh12 {1}Hh12'.
rewrite 2!heap.dom_sing.
move/(_ (refl_equal _)).
apply heap.disj_sym in Hdisj.
apply heap.disj_sym in Hdisj'.
case/(_ Hdisj' Hdisj)=> Hh1 X2; subst h1' h2'.
rewrite (IH _ _ _ _ _ H1 H2 Hh2 Hh2').
f_equal.
rewrite Hh12 in Hh1.
by move/heap.sing_inj : Hh1.
Qed.
Lemma mapstos_con_inj : forall n l1 l2 e st h P Q,
u2Z ([ e ]e_ st) + 4 * Z_of_nat n < Zbeta 1 ->
length l1 = n -> length l2 = n ->
(e |--> l1 ** P) st h -> (e |--> l2 ** Q) st h ->
l1 = l2.
Proof.
move=> n l1 l2 e st h P Q e_fit len_l1 len_l2.
case=> h1 [h2 [h1dh2 [h1Uh2 [Hh1 Hh2]]]].
case=> h1' [h2' [h1'dh2' [h1'Uh2' [Hh1' Hh2']]]].
have : h1 = h1'.
rewrite h1Uh2 in h1'Uh2'.
have dom_h1_h1' : heap.dom h1 = heap.dom h1'.
apply assert_m.mapstos_inv_dom in Hh1; last by rewrite len_l1.
apply assert_m.mapstos_inv_dom in Hh1'; last by rewrite len_l2.
apply seq_ext.s2l_inj => //; last by rewrite -Hh1 -Hh1' len_l1 len_l2.
apply (heap.union_inv h1 h1' h2 h2' h1'Uh2') => //.
by apply heap.disj_sym.
by apply heap.disj_sym.
move=> ?; subst h1'.
by apply assert_m.mapstos_inj with n e st h1.
Qed.
Lemma mapstos_ext : forall l st st' h e e', [ e ]e_st = [ e' ]e_st' ->
(e |--> l) st h -> (e' |--> l) st' h.
Proof.
elim.
- by move=> st st' h e e' /= ->.
- move=> hd tl IH st st' h e0 e' Heq /= [h1 [h2 [Hdisj [Hunion [Hh1 Hh2]]]]].
exists h1, h2; do 2 (split; first by done); split.
+ by move: Hh1; apply mapsto_ext.
+ apply IH with st (add_e e0 (int_e four32)) => //=; by rewrite Heq.
Qed.
Lemma mapsto_get1' : forall s h e e1 P,
(e |~> int_e e1 ** P)%list%mips_assert s h ->
heap.get (Zabs_nat (u2Z ([ e ]e_ s)/ 4)) h = Some e1.
Proof.
move=> s h e e1 P /=.
case=> h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh1 => p [Hp Hh1].
rewrite h1_U_h2.
apply heap.get_union_L => //.
by rewrite Hh1 Hp Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat heap.get_sing.
Qed.
Lemma mapstos_get1 : forall s h e e1 e2 P,
(e |--> e1 :: e2 :: List.nil ** P)%list%mips_assert s h ->
heap.get (Zabs_nat (u2Z ([ e ]e_ s)/ 4)) h = Some e1.
Proof.
move=> s h e e1 e2 P /=.
rewrite assert_m.con_assoc_equiv.
by move/mapsto_get1'.
Qed.
Local Open Scope machine_int_scope.
Lemma mapstos_get2 : forall s h e e1 e2 P,
(e |--> e1 :: e2 :: List.nil ** P) s h ->
heap.get (Zabs_nat (u2Z ([ e ]e_ s [.+] four32)/ 4)) h = Some e2.
Proof.
move=> s h e e1 e2 P /=.
rewrite assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv.
by move/mapsto_get1'.
Qed.
inde l P iff the truth of assertion P does not depend on the value of registers in list l
Definition inde (l : list store.var) (P : assert) := forall s h,
(forall x v, In x l -> (P s h <-> P (store.upd x v s) h)).
Lemma inde_nil : forall P, inde nil P.
Proof. done. Qed.
Lemma incl_inde : forall a b P, inde b P -> incl a b -> inde a P.
Proof.
elim=> // hd tl IH b P H1 H2.
apply incl_cons_inv_L in H2.
case: H2 => H2 H3.
rewrite /inde => s h x v /= [].
- move=> ?; subst hd; by apply H1.
- move=> x_tl; by apply (IH _ _ H1 H3).
Qed.
Lemma In_inde : forall l y f, In y l -> inde l f -> inde (y :: l) f.
Proof.
move=> l y f HIn Hinde s h x v /= [H | H]; split=> Hf.
subst x; by rewrite -(Hinde s h y v HIn).
subst x; by rewrite (Hinde s h y v HIn).
by rewrite -(Hinde s h x v H).
by rewrite (Hinde s h x v H).
Qed.
Lemma inde_rotate : forall l y f, inde (l ++ y :: nil) f -> inde (y :: l) f.
Proof.
move=> l y f Hinde s h x v /= [H|H]; split => Hf.
- subst x.
have HIn : In y (l ++ y::nil) by apply in_or_app => /=; auto.
by rewrite -(Hinde s h y v HIn).
- subst x.
have HIn : In y (l ++ y::nil) by apply in_or_app => /=; auto.
by rewrite (Hinde s h y v HIn).
- have HIn : In x (l ++ y::nil) by apply in_or_app; simpl; auto.
by rewrite -(Hinde s h x v HIn).
- have HIn : In x (l ++ y::nil) by apply in_or_app; simpl; auto.
by rewrite (Hinde s h x v HIn).
Qed.
Lemma inde_upd_store : forall (P : assert) x z s h,
inde (x :: nil) P -> P s h -> P (store.upd x z s) h.
Proof. move=> P x z s h H. rewrite (H s h x z) /=; by auto. Qed.
Lemma inde_get : forall l x p, ~ In x l -> inde l (fun s h => [x]_s = p).
Proof.
rewrite /inde.
move=> l x0 HP; rewrite /inde => s h x_ v HIn.
split; rewrite store.get_upd //; by move=> Htmp; subst x0.
Qed.
Lemma inde_u2Z_get : forall l x p, ~ In x l -> inde l (fun s h => u2Z [x]_s = p).
Proof.
rewrite /inde.
move=> l x0 HP; rewrite /inde => s h x_ v HIn.
split; rewrite store.get_upd //; by move=> Htmp; subst x0.
Qed.
Lemma inde_u2Z_get_plus : forall l x p q, ~ In x l -> inde l (fun s h => u2Z [x]_s + q = p).
Proof.
rewrite /inde.
move=> l0 x0 HP; rewrite /inde => s h x_ v HIn.
split; rewrite store.get_upd //; by move=> Htmp; subst x0.
Qed.
Lemma inde_s2Z_get : forall l x p, ~ In x l -> inde l (fun s h => s2Z [x]_s = p).
Proof.
rewrite /inde.
move=> l_ x0 HP; rewrite /inde => s h x_ v HIn.
split; rewrite store.get_upd //; by move=> Htmp; subst x0.
Qed.
Lemma inde_TT : forall l, inde l TT. Proof. move=> l //. Qed.
Lemma inde_sep_and : forall l (P Q : assert), inde l P -> inde l Q -> inde l (P //\\ Q).
Proof.
rewrite /while.And /inde.
move=> l P Q HP HQ; rewrite /inde => s h x v HIn.
split; move=> [H1 H2]; split.
by rewrite -HP.
by rewrite -HQ.
by rewrite (HP s h x v).
by rewrite (HQ s h x v).
Qed.
Lemma inde_and : forall l P (Q : assert),
inde l P -> inde l Q -> inde l (fun s h => P s h /\ Q s h).
Proof.
rewrite /inde.
move=> l0 P Q HP HQ; rewrite /inde => s h x_ v HIn.
split; move=> [H1 H2]; split.
by rewrite -HP.
by rewrite -HQ.
by rewrite (HP s h x_ v).
by rewrite (HQ s h x_ v).
Qed.
Lemma inde_imp : forall (l : list reg) (P : Prop) (Q : store.t -> Prop),
inde l (fun s _ => Q s) ->
inde l (fun s _ => P -> Q s).
Proof.
move=> l P Q.
rewrite /inde => H s h x v Hx; split => H1 H2.
- rewrite -H //; by apply H1.
- rewrite (H s h x v) //; by apply H1.
Qed.
Lemma inde_imp2 : forall l P Q,
assert_m.inde l (fun st h => P st h) ->
assert_m.inde l (fun st h => Q st h) ->
assert_m.inde l (fun st h => P st h -> Q st h).
Proof.
move=> l P Q HP HQ.
rewrite /assert_m.inde.
move=> st h x v x_l.
split=> H1 H2.
- rewrite -(HQ st h x v) //.
apply H1.
by rewrite (HP st h x v).
- rewrite (HQ st h x v) //.
apply H1.
by rewrite -(HP st h x v).
Qed.
Lemma inde_exists : forall l P,
(forall y, assert_m.inde l (fun st h => P st h y)) ->
assert_m.inde l (fun st h => exists y : int 32, P st h y).
Proof.
move=> l P H.
rewrite /assert_m.inde => st h x z z_l; split; case => y P_y; exists y.
- by rewrite -(H y).
- by rewrite (H y st h x z).
Qed.
Lemma inde_sep_con : forall l (P Q : assert),
inde l P -> inde l Q -> inde l (P ** Q).
Proof.
move=> l P Q HP HQ; rewrite /inde => s h x v HIn.
split; move=> [h1 [h2 [H1 [H2 [H3 H4]]]]]; exists h1; exists h2; repeat (split => //).
by rewrite -(HP s h1).
by rewrite -(HQ s h2).
by rewrite (HP s h1 x v).
by rewrite (HQ s h2 x v).
Qed.
Lemma inde_emp : forall l, inde l emp.
Proof.
move=> l; rewrite /inde => s h x v x_l; split => H; red in H; by subst.
Qed.
Lemma inde_mapsto_int_e : forall e l v,
disj (vars e) l -> inde l (e |~> int_e v).
Proof.
elim.
- move=> g l v H [s m] h x v' HIn; split => /=.
+ case/orP : (orbN (x == r0)) => [->//|].
move/negbTE => ->.
apply mapsto_ext => //=.
case/orP : (orbN (g == r0)) => [->//|].
move/negbTE => ->; rewrite store.get_upd_p //.
move=> ?; subst x; case: (H g) => _; move/(_ HIn) => /=; tauto.
+ case/orP : (orbN (x == r0)) => [->//|].
move/negbTE => ->.
apply mapsto_ext => //=.
case/orP : (orbN (g == r0)) => [->//|].
move/negbTE => ->; rewrite store.get_upd_p //.
move=> ?; subst x; case: (H g) => _; move/(_ HIn) => /=; tauto.
- done.
- move=> e IHe e' IHe' l v /= H [s m] h g v' HIn; split => /=.
+ case/orP : (orbN (g == r0)) => [->//|].
move/negbTE => ->.
apply mapsto_ext => //=.
case/disj_app_inv : H => H1 H3.
rewrite eval_upd'; last by move=> H2; case: (H1 g); move/(_ H2); tauto.
rewrite eval_upd' //; last by move=> H2; case: (H3 g); move/(_ H2); tauto.
+ case/orP : (orbN (g == r0)) => [->//|].
move/negbTE => ->.
apply mapsto_ext => //=.
case/disj_app_inv: H => H1 H3.
rewrite eval_upd'; last by move=> H2; case: (H1 g); move/(_ H2); tauto.
rewrite eval_upd' //; last by move=> H2; case: (H3 g); move/(_ H2); tauto.
- move=> e IHe l v H [s m] h x v' HIn; split => /=.
+ case/orP : (orbN (x == r0)) => [->// | ].
move/negbTE => ->.
apply mapsto_ext => //=.
rewrite eval_upd' //; last by move=> H2; case: (H x); move/(_ H2); tauto.
+ case/orP : (orbN (x == r0)) => [->//|].
move/negbTE => ->.
apply mapsto_ext => //=.
rewrite eval_upd' //; last by move=> H2; case: (H x); move/(_ H2); tauto.
Qed.
Lemma inde_mapstos : forall v l e, disj (vars e) l -> inde l (e |--> v).
Proof.
elim.
- move=> l e Hinter s h x v Hx /=; split.
+ case=> H1 H2; rewrite /emp in H2; subst h; split; last by done.
rewrite eval_upd //.
by apply disj_not_In with l.
+ case=> H1 H2; rewrite /emp in H2; subst h; split; last by done.
rewrite eval_upd // in H1.
by apply disj_not_In with l.
- move=> // hd tl IH l e H /=.
apply inde_sep_con => //.
+ by apply inde_mapsto_int_e.
apply IH => //=.
by rewrite -app_nil_end.
Qed.
Lemma inde_mapstos_var_e : forall v l a, ~ In a l -> inde l (var_e a |--> v).
Proof.
move=> v l a H; apply inde_mapstos => /=.
apply disj_cons_L; by [apply disj_nil_L | done].
Qed.
Lemma inde_mapstos_int_e : forall v l a, inde l (int_e a |--> v).
Proof. move=> v l a H; apply inde_mapstos => /=; by apply disj_nil_L. Qed.
(forall x v, In x l -> (P s h <-> P (store.upd x v s) h)).
Lemma inde_nil : forall P, inde nil P.
Proof. done. Qed.
Lemma incl_inde : forall a b P, inde b P -> incl a b -> inde a P.
Proof.
elim=> // hd tl IH b P H1 H2.
apply incl_cons_inv_L in H2.
case: H2 => H2 H3.
rewrite /inde => s h x v /= [].
- move=> ?; subst hd; by apply H1.
- move=> x_tl; by apply (IH _ _ H1 H3).
Qed.
Lemma In_inde : forall l y f, In y l -> inde l f -> inde (y :: l) f.
Proof.
move=> l y f HIn Hinde s h x v /= [H | H]; split=> Hf.
subst x; by rewrite -(Hinde s h y v HIn).
subst x; by rewrite (Hinde s h y v HIn).
by rewrite -(Hinde s h x v H).
by rewrite (Hinde s h x v H).
Qed.
Lemma inde_rotate : forall l y f, inde (l ++ y :: nil) f -> inde (y :: l) f.
Proof.
move=> l y f Hinde s h x v /= [H|H]; split => Hf.
- subst x.
have HIn : In y (l ++ y::nil) by apply in_or_app => /=; auto.
by rewrite -(Hinde s h y v HIn).
- subst x.
have HIn : In y (l ++ y::nil) by apply in_or_app => /=; auto.
by rewrite (Hinde s h y v HIn).
- have HIn : In x (l ++ y::nil) by apply in_or_app; simpl; auto.
by rewrite -(Hinde s h x v HIn).
- have HIn : In x (l ++ y::nil) by apply in_or_app; simpl; auto.
by rewrite (Hinde s h x v HIn).
Qed.
Lemma inde_upd_store : forall (P : assert) x z s h,
inde (x :: nil) P -> P s h -> P (store.upd x z s) h.
Proof. move=> P x z s h H. rewrite (H s h x z) /=; by auto. Qed.
Lemma inde_get : forall l x p, ~ In x l -> inde l (fun s h => [x]_s = p).
Proof.
rewrite /inde.
move=> l x0 HP; rewrite /inde => s h x_ v HIn.
split; rewrite store.get_upd //; by move=> Htmp; subst x0.
Qed.
Lemma inde_u2Z_get : forall l x p, ~ In x l -> inde l (fun s h => u2Z [x]_s = p).
Proof.
rewrite /inde.
move=> l x0 HP; rewrite /inde => s h x_ v HIn.
split; rewrite store.get_upd //; by move=> Htmp; subst x0.
Qed.
Lemma inde_u2Z_get_plus : forall l x p q, ~ In x l -> inde l (fun s h => u2Z [x]_s + q = p).
Proof.
rewrite /inde.
move=> l0 x0 HP; rewrite /inde => s h x_ v HIn.
split; rewrite store.get_upd //; by move=> Htmp; subst x0.
Qed.
Lemma inde_s2Z_get : forall l x p, ~ In x l -> inde l (fun s h => s2Z [x]_s = p).
Proof.
rewrite /inde.
move=> l_ x0 HP; rewrite /inde => s h x_ v HIn.
split; rewrite store.get_upd //; by move=> Htmp; subst x0.
Qed.
Lemma inde_TT : forall l, inde l TT. Proof. move=> l //. Qed.
Lemma inde_sep_and : forall l (P Q : assert), inde l P -> inde l Q -> inde l (P //\\ Q).
Proof.
rewrite /while.And /inde.
move=> l P Q HP HQ; rewrite /inde => s h x v HIn.
split; move=> [H1 H2]; split.
by rewrite -HP.
by rewrite -HQ.
by rewrite (HP s h x v).
by rewrite (HQ s h x v).
Qed.
Lemma inde_and : forall l P (Q : assert),
inde l P -> inde l Q -> inde l (fun s h => P s h /\ Q s h).
Proof.
rewrite /inde.
move=> l0 P Q HP HQ; rewrite /inde => s h x_ v HIn.
split; move=> [H1 H2]; split.
by rewrite -HP.
by rewrite -HQ.
by rewrite (HP s h x_ v).
by rewrite (HQ s h x_ v).
Qed.
Lemma inde_imp : forall (l : list reg) (P : Prop) (Q : store.t -> Prop),
inde l (fun s _ => Q s) ->
inde l (fun s _ => P -> Q s).
Proof.
move=> l P Q.
rewrite /inde => H s h x v Hx; split => H1 H2.
- rewrite -H //; by apply H1.
- rewrite (H s h x v) //; by apply H1.
Qed.
Lemma inde_imp2 : forall l P Q,
assert_m.inde l (fun st h => P st h) ->
assert_m.inde l (fun st h => Q st h) ->
assert_m.inde l (fun st h => P st h -> Q st h).
Proof.
move=> l P Q HP HQ.
rewrite /assert_m.inde.
move=> st h x v x_l.
split=> H1 H2.
- rewrite -(HQ st h x v) //.
apply H1.
by rewrite (HP st h x v).
- rewrite (HQ st h x v) //.
apply H1.
by rewrite -(HP st h x v).
Qed.
Lemma inde_exists : forall l P,
(forall y, assert_m.inde l (fun st h => P st h y)) ->
assert_m.inde l (fun st h => exists y : int 32, P st h y).
Proof.
move=> l P H.
rewrite /assert_m.inde => st h x z z_l; split; case => y P_y; exists y.
- by rewrite -(H y).
- by rewrite (H y st h x z).
Qed.
Lemma inde_sep_con : forall l (P Q : assert),
inde l P -> inde l Q -> inde l (P ** Q).
Proof.
move=> l P Q HP HQ; rewrite /inde => s h x v HIn.
split; move=> [h1 [h2 [H1 [H2 [H3 H4]]]]]; exists h1; exists h2; repeat (split => //).
by rewrite -(HP s h1).
by rewrite -(HQ s h2).
by rewrite (HP s h1 x v).
by rewrite (HQ s h2 x v).
Qed.
Lemma inde_emp : forall l, inde l emp.
Proof.
move=> l; rewrite /inde => s h x v x_l; split => H; red in H; by subst.
Qed.
Lemma inde_mapsto_int_e : forall e l v,
disj (vars e) l -> inde l (e |~> int_e v).
Proof.
elim.
- move=> g l v H [s m] h x v' HIn; split => /=.
+ case/orP : (orbN (x == r0)) => [->//|].
move/negbTE => ->.
apply mapsto_ext => //=.
case/orP : (orbN (g == r0)) => [->//|].
move/negbTE => ->; rewrite store.get_upd_p //.
move=> ?; subst x; case: (H g) => _; move/(_ HIn) => /=; tauto.
+ case/orP : (orbN (x == r0)) => [->//|].
move/negbTE => ->.
apply mapsto_ext => //=.
case/orP : (orbN (g == r0)) => [->//|].
move/negbTE => ->; rewrite store.get_upd_p //.
move=> ?; subst x; case: (H g) => _; move/(_ HIn) => /=; tauto.
- done.
- move=> e IHe e' IHe' l v /= H [s m] h g v' HIn; split => /=.
+ case/orP : (orbN (g == r0)) => [->//|].
move/negbTE => ->.
apply mapsto_ext => //=.
case/disj_app_inv : H => H1 H3.
rewrite eval_upd'; last by move=> H2; case: (H1 g); move/(_ H2); tauto.
rewrite eval_upd' //; last by move=> H2; case: (H3 g); move/(_ H2); tauto.
+ case/orP : (orbN (g == r0)) => [->//|].
move/negbTE => ->.
apply mapsto_ext => //=.
case/disj_app_inv: H => H1 H3.
rewrite eval_upd'; last by move=> H2; case: (H1 g); move/(_ H2); tauto.
rewrite eval_upd' //; last by move=> H2; case: (H3 g); move/(_ H2); tauto.
- move=> e IHe l v H [s m] h x v' HIn; split => /=.
+ case/orP : (orbN (x == r0)) => [->// | ].
move/negbTE => ->.
apply mapsto_ext => //=.
rewrite eval_upd' //; last by move=> H2; case: (H x); move/(_ H2); tauto.
+ case/orP : (orbN (x == r0)) => [->//|].
move/negbTE => ->.
apply mapsto_ext => //=.
rewrite eval_upd' //; last by move=> H2; case: (H x); move/(_ H2); tauto.
Qed.
Lemma inde_mapstos : forall v l e, disj (vars e) l -> inde l (e |--> v).
Proof.
elim.
- move=> l e Hinter s h x v Hx /=; split.
+ case=> H1 H2; rewrite /emp in H2; subst h; split; last by done.
rewrite eval_upd //.
by apply disj_not_In with l.
+ case=> H1 H2; rewrite /emp in H2; subst h; split; last by done.
rewrite eval_upd // in H1.
by apply disj_not_In with l.
- move=> // hd tl IH l e H /=.
apply inde_sep_con => //.
+ by apply inde_mapsto_int_e.
apply IH => //=.
by rewrite -app_nil_end.
Qed.
Lemma inde_mapstos_var_e : forall v l a, ~ In a l -> inde l (var_e a |--> v).
Proof.
move=> v l a H; apply inde_mapstos => /=.
apply disj_cons_L; by [apply disj_nil_L | done].
Qed.
Lemma inde_mapstos_int_e : forall v l a, inde l (int_e a |--> v).
Proof. move=> v l a H; apply inde_mapstos => /=; by apply disj_nil_L. Qed.
inde_mult P iff the truth of assertion P does not depend on the multiplier
Definition inde_mult (P : assert) :=
forall s h, (forall m m', P (s,m) h <-> P (s,m') h).
Lemma inde_mult_TT : inde_mult TT. Proof. done. Qed.
Lemma inde_mult_sep_con : forall (P Q : assert),
inde_mult P -> inde_mult Q -> inde_mult (P ** Q).
Proof.
move=> P Q HP HQ s h m m'; split; move=> [h1 [h2 [H1 [H2 [H3 H4]]]]]; exists h1; exists h2; repeat (split => //).
by rewrite -(HP s h1 m).
by rewrite -(HQ s h2 m).
by rewrite (HP s h1 m m').
by rewrite (HQ s h2 m m').
Qed.
Lemma inde_mult_sep_and : forall P Q,inde_mult P -> inde_mult Q -> inde_mult (P //\\ Q).
Proof.
rewrite /inde_mult /while.And => P Q HP HQ s h m m'; split; case=> HP' HQ'.
split; by [rewrite -(HP _ _ m _) | rewrite -(HQ _ _ m _)].
split; by [rewrite (HP _ _ _ m') | rewrite (HQ _ _ _ m')].
Qed.
Lemma inde_mult_mapsto : forall a v, inde_mult (a |~> v).
Proof.
move=> a v s h m m'; split; apply mapsto_ext => //.
by apply eval_inde_multiplier.
by apply eval_inde_multiplier.
by apply eval_inde_multiplier.
by apply eval_inde_multiplier.
Qed.
Lemma inde_mult_mapstos : forall a v, inde_mult (a |--> v).
Proof. move=> a v s h m m'; split; apply mapstos_ext.
by apply eval_inde_multiplier.
by apply eval_inde_multiplier.
Qed.
Lemma inde_mult_maddu : forall (P : assert) p s h, inde_mult P ->
P s h -> P (store.maddu_op p s) h.
Proof. move=> P p [s m] h HP HP'. by rewrite -(HP s h m). Qed.
Lemma inde_mult_mflhxu_op : forall (P : assert) s h,
inde_mult P -> P s h -> P (store.mflhxu_op s) h.
Proof. move=> P [s m] h HP HP'. by rewrite -(HP s h m). Qed.
Lemma inde_mult_msubu : forall (P : assert) p s h,
inde_mult P -> P s h -> P (store.msubu_op p s) h.
Proof. move=> P p [s m] h HP HP'. by rewrite -(HP s h m). Qed.
Lemma inde_mult_mtlo : forall (P : assert) p s h,
inde_mult P -> P s h -> P (store.mtlo_op p s) h.
Proof. move=> P p [s [a [hi lo]]] h HP HP' /=.
by rewrite -(HP s h (a, (hi, lo))).
Qed.
Lemma inde_mult_mthi : forall (P : assert) p s h,
inde_mult P -> P s h -> P (store.mthi_op p s) h.
Proof. move=> P p [s [a [hi lo]]] h HP HP'.
by rewrite -(HP s h (a, (hi ,lo))). Qed.
Lemma inde_mult_multu : forall (P : assert) p s h,
inde_mult P -> P s h -> P (store.multu_op p s) h.
Proof. move=> P p [s m] h HP HP'. by rewrite -(HP s h m). Qed.
Lemma inde_mult_and : forall P (Q : assert),
inde_mult P -> inde_mult Q -> inde_mult (fun s h => P s h /\ Q s h).
Proof.
move=> P Q HP HQ s h m m'; split; case=> [H1 H2]; split.
by rewrite (HP _ _ _ m).
by rewrite (HQ _ _ _ m).
by rewrite (HP _ _ _ m').
by rewrite (HQ _ _ _ m').
Qed.
End assert_m.
forall s h, (forall m m', P (s,m) h <-> P (s,m') h).
Lemma inde_mult_TT : inde_mult TT. Proof. done. Qed.
Lemma inde_mult_sep_con : forall (P Q : assert),
inde_mult P -> inde_mult Q -> inde_mult (P ** Q).
Proof.
move=> P Q HP HQ s h m m'; split; move=> [h1 [h2 [H1 [H2 [H3 H4]]]]]; exists h1; exists h2; repeat (split => //).
by rewrite -(HP s h1 m).
by rewrite -(HQ s h2 m).
by rewrite (HP s h1 m m').
by rewrite (HQ s h2 m m').
Qed.
Lemma inde_mult_sep_and : forall P Q,inde_mult P -> inde_mult Q -> inde_mult (P //\\ Q).
Proof.
rewrite /inde_mult /while.And => P Q HP HQ s h m m'; split; case=> HP' HQ'.
split; by [rewrite -(HP _ _ m _) | rewrite -(HQ _ _ m _)].
split; by [rewrite (HP _ _ _ m') | rewrite (HQ _ _ _ m')].
Qed.
Lemma inde_mult_mapsto : forall a v, inde_mult (a |~> v).
Proof.
move=> a v s h m m'; split; apply mapsto_ext => //.
by apply eval_inde_multiplier.
by apply eval_inde_multiplier.
by apply eval_inde_multiplier.
by apply eval_inde_multiplier.
Qed.
Lemma inde_mult_mapstos : forall a v, inde_mult (a |--> v).
Proof. move=> a v s h m m'; split; apply mapstos_ext.
by apply eval_inde_multiplier.
by apply eval_inde_multiplier.
Qed.
Lemma inde_mult_maddu : forall (P : assert) p s h, inde_mult P ->
P s h -> P (store.maddu_op p s) h.
Proof. move=> P p [s m] h HP HP'. by rewrite -(HP s h m). Qed.
Lemma inde_mult_mflhxu_op : forall (P : assert) s h,
inde_mult P -> P s h -> P (store.mflhxu_op s) h.
Proof. move=> P [s m] h HP HP'. by rewrite -(HP s h m). Qed.
Lemma inde_mult_msubu : forall (P : assert) p s h,
inde_mult P -> P s h -> P (store.msubu_op p s) h.
Proof. move=> P p [s m] h HP HP'. by rewrite -(HP s h m). Qed.
Lemma inde_mult_mtlo : forall (P : assert) p s h,
inde_mult P -> P s h -> P (store.mtlo_op p s) h.
Proof. move=> P p [s [a [hi lo]]] h HP HP' /=.
by rewrite -(HP s h (a, (hi, lo))).
Qed.
Lemma inde_mult_mthi : forall (P : assert) p s h,
inde_mult P -> P s h -> P (store.mthi_op p s) h.
Proof. move=> P p [s [a [hi lo]]] h HP HP'.
by rewrite -(HP s h (a, (hi ,lo))). Qed.
Lemma inde_mult_multu : forall (P : assert) p s h,
inde_mult P -> P s h -> P (store.multu_op p s) h.
Proof. move=> P p [s m] h HP HP'. by rewrite -(HP s h m). Qed.
Lemma inde_mult_and : forall P (Q : assert),
inde_mult P -> inde_mult Q -> inde_mult (fun s h => P s h /\ Q s h).
Proof.
move=> P Q HP HQ s h m m'; split; case=> [H1 H2]; split.
by rewrite (HP _ _ _ m).
by rewrite (HQ _ _ _ m).
by rewrite (HP _ _ _ m').
by rewrite (HQ _ _ _ m').
Qed.
End assert_m.