Additional lemmas over the Clight semantics, prooving that the eval_expr relation is deterministic
Require Import Clight.
Require Import Ctypes.
Require Import Values.
Require Export Integers.
Lemma assign_loc_determ:
forall (
ce :
composite_env) (
ty :
type) (
m :
Memory.Mem.mem) (
b :
block) (
ofs :
ptrofs) (
v:
val)
(
m1 m2:
Memory.Mem.mem),
assign_loc ce ty m b ofs v m1 ->
assign_loc ce ty m b ofs v m2 ->
m1 =
m2.
Proof.
intros ce ty m b ofs v m1 m2.
intros E1 E2.
generalize dependent m2.
induction E1.
- intros m2 E2; inversion E2; subst.
+ rewrite H1 in H.
inversion H.
rewrite H4 in H2.
rewrite H2 in H0.
inversion H0.
reflexivity.
+ rewrite H1 in H.
inversion H.
- intros v2 E2; inversion E2; subst.
+ rewrite H5 in H.
inversion H.
+ rewrite H11 in H3.
inversion H3.
rewrite H6 in H13.
rewrite H13 in H4.
inversion H4.
reflexivity.
Qed.
Lemma deref_loc_determ:
forall (
ty:
type) (
m:
Memory.Mem.mem) (
b:
block) (
ofs:
ptrofs) (
v1 v2:
val),
deref_loc ty m b ofs v1 ->
deref_loc ty m b ofs v2 ->
v1 =
v2.
Proof.
intros ty m b ofs v1 v2.
intros E1 E2.
generalize dependent v2.
induction E1.
- intros v2 E2; inversion E2; subst.
+ rewrite H1 in H.
inversion H.
rewrite H4 in H2.
rewrite H2 in H0.
inversion H0.
reflexivity.
+ rewrite H1 in H.
inversion H.
+ rewrite H1 in H.
inversion H.
- intros v2 E2; inversion E2; subst.
+ rewrite H0 in H.
inversion H.
+ reflexivity.
+ reflexivity.
- intros v2 E2; inversion E2; subst.
+ rewrite H0 in H.
inversion H.
+ rewrite H0 in H.
inversion H.
+ reflexivity.
Qed.
Lemma eval_expr_determ:
forall (
ge :
genv) (
e :
env) (
le :
temp_env) (
m :
Memory.Mem.mem)
x v1 v2,
eval_expr ge e le m x v1 ->
eval_expr ge e le m x v2 ->
v1 =
v2
with eval_lvalue_determ:
forall (
ge :
genv) (
e :
env) (
le :
temp_env) (
m :
Memory.Mem.mem)
x b1 b2 ofs1 ofs2,
eval_lvalue ge e le m x b1 ofs1 ->
eval_lvalue ge e le m x b2 ofs2 ->
b1 =
b2 /\
ofs1 =
ofs2.
Proof.
-
intros ge e le m x v1 v2.
intros E1 E2.
generalize dependent v2.
induction E1.
+
intros v2 E2;
inversion E2;
subst.
*
reflexivity.
*
inversion H.
+
intros v2 E2;
inversion E2;
subst.
*
reflexivity.
*
inversion H.
+
intros v2 E2;
inversion E2;
subst.
*
reflexivity.
*
inversion H.
+
intros v2 E2;
inversion E2;
subst.
*
reflexivity.
*
inversion H.
+
intros v2 E2;
inversion E2;
subst.
*
rewrite H3 in H.
inversion H.
auto.
*
inversion H0.
+
intros v2 E2;
inversion E2;
subst.
*
pose proof eval_lvalue_determ _ _ _ _ _ _ _ _ _ H H3 as [
Hloc Hofs].
subst.
reflexivity.
*
inversion H0.
+
intros v2 E2;
inversion E2;
subst.
*
apply IHE1 in H4.
rewrite H4 in H.
rewrite H5 in H.
inversion H.
reflexivity.
*
inversion H0.
+
intros v0 E2;
inversion E2;
subst.
*
apply IHE1_1 in H5.
apply IHE1_2 in H6.
rewrite H5,
H6 in H.
rewrite H7 in H.
inversion H.
reflexivity.
*
inversion H0.
+
intros v2 E2;
inversion E2;
subst.
*
apply IHE1 in H2.
rewrite H2 in H.
rewrite H4 in H.
inversion H.
reflexivity.
*
inversion H0.
+
intros v2 E2;
inversion E2;
subst.
*
reflexivity.
*
inversion H.
+
intros v2 E2;
inversion E2;
subst.
*
reflexivity.
*
inversion H.
+
intros v2 E2;
inversion E2;
subst;
inversion H.
*
pose proof eval_lvalue_determ _ _ _ _ _ _ _ _ _ H H1 as [
Hloc Hofs].
subst.
apply (
deref_loc_determ _ _ _ _ _ _ H0 H2).
*
pose proof eval_lvalue_determ _ _ _ _ _ _ _ _ _ H H1 as [
Hloc Hofs].
subst.
apply (
deref_loc_determ _ _ _ _ _ _ H0 H2).
*
pose proof eval_lvalue_determ _ _ _ _ _ _ _ _ _ H H1 as [
Hloc Hofs].
subst.
apply (
deref_loc_determ _ _ _ _ _ _ H0 H2).
*
pose proof eval_lvalue_determ _ _ _ _ _ _ _ _ _ H H1 as [
Hloc Hofs].
subst.
apply (
deref_loc_determ _ _ _ _ _ _ H0 H2).
*
pose proof eval_lvalue_determ _ _ _ _ _ _ _ _ _ H H1 as [
Hloc Hofs].
subst.
apply (
deref_loc_determ _ _ _ _ _ _ H0 H2).
-
intros ge e le m x b1 b2 ofs1 ofs2.
intros E1 E2.
generalize dependent ofs2.
generalize dependent b2.
induction E1.
+
intros b2 ofs2 E2;
inversion E2;
subst.
*
rewrite H4 in H.
inversion H.
split;
reflexivity.
*
rewrite H2 in H.
inversion H.
+
intros b2 ofs2 E2;
inversion E2;
subst.
*
rewrite H5 in H.
inversion H.
*
rewrite H6 in H0.
inversion H0.
split;
reflexivity.
+
intros b2 ofs2 E2;
inversion E2;
subst.
pose proof eval_expr_determ _ _ _ _ _ _ _ H H4 as Hv.
inversion Hv.
split;
reflexivity.
+
intros b2 ofs2 E2;
inversion E2;
subst.
*
pose proof eval_expr_determ _ _ _ _ _ _ _ H H6 as Hv.
inversion Hv.
rewrite H7 in H0.
inversion H0.
subst.
rewrite H10 in H1.
inversion H1.
subst.
rewrite H11 in H2.
inversion H2.
split;
reflexivity.
*
rewrite H9 in H0.
inversion H0.
+
intros b2 ofs2 E2;
inversion E2;
subst.
*
rewrite H6 in H0.
inversion H0.
*
pose proof eval_expr_determ _ _ _ _ _ _ _ H H5 as Hv.
inversion Hv.
split;
reflexivity.
Qed.