Whole-program behaviors
Require Import Classical.
Require Import ClassicalEpsilon.
Require Import Coqlib.
Require Import Events.
Require Import Globalenvs.
Require Import Integers.
Require Import Smallstep.
Set Implicit Arguments.
Behaviors for program executions
The four possible outcomes for the execution of a program:
-
Termination, with a finite trace of observable events
and an integer value that stands for the process exit code
(the return value of the main function).
-
Divergence with a finite trace of observable events.
(At some point, the program runs forever without doing any I/O.)
-
Reactive divergence with an infinite trace of observable events.
(The program performs infinitely many I/O operations separated
by finite amounts of internal computations.)
-
Going wrong, with a finite trace of observable events
performed before the program gets stuck.
:
Type :=
|
Terminates:
trace ->
int ->
program_behavior
|
Diverges:
trace ->
program_behavior
|
Reacts:
traceinf ->
program_behavior
|
Goes_wrong:
trace ->
program_behavior.
Operations and relations on behaviors
Definition not_wrong (
beh:
program_behavior) :
Prop :=
match beh with
|
Terminates _ _ =>
True
|
Diverges _ =>
True
|
Reacts _ =>
True
|
Goes_wrong _ =>
False
end.
Definition behavior_app (
t:
trace) (
beh:
program_behavior):
program_behavior :=
match beh with
|
Terminates t1 r =>
Terminates (
t **
t1)
r
|
Diverges t1 =>
Diverges (
t **
t1)
|
Reacts T =>
Reacts (
t ***
T)
|
Goes_wrong t1 =>
Goes_wrong (
t **
t1)
end.
Lemma behavior_app_assoc:
forall t1 t2 beh,
behavior_app (
t1 **
t2)
beh =
behavior_app t1 (
behavior_app t2 beh).
Proof.
intros. destruct beh; simpl; f_equal; traceEq.
Qed.
Lemma behavior_app_E0:
forall beh,
behavior_app E0 beh =
beh.
Proof.
destruct beh; auto.
Qed.
Definition behavior_prefix (
t:
trace) (
beh:
program_behavior) :
Prop :=
exists beh',
beh =
behavior_app t beh'.
Definition behavior_improves (
beh1 beh2:
program_behavior) :
Prop :=
beh1 =
beh2 \/
exists t,
beh1 =
Goes_wrong t /\
behavior_prefix t beh2.
Lemma behavior_improves_refl:
forall beh,
behavior_improves beh beh.
Proof.
intros; red; auto.
Qed.
Lemma behavior_improves_trans:
forall beh1 beh2 beh3,
behavior_improves beh1 beh2 ->
behavior_improves beh2 beh3 ->
behavior_improves beh1 beh3.
Proof.
intros.
red.
destruct H;
destruct H0;
subst;
auto.
destruct H as [
t1 [
EQ1 [
beh2'
EQ1']]].
destruct H0 as [
t2 [
EQ2 [
beh3'
EQ2']]].
subst.
destruct beh2';
simpl in EQ2;
try discriminate.
inv EQ2.
right.
exists t1;
split;
auto.
exists (
behavior_app t beh3').
apply behavior_app_assoc.
Qed.
Lemma behavior_improves_bot:
forall beh,
behavior_improves (
Goes_wrong E0)
beh.
Proof.
intros.
right.
exists E0;
split;
auto.
exists beh.
rewrite behavior_app_E0;
auto.
Qed.
Lemma behavior_improves_app:
forall t beh1 beh2,
behavior_improves beh1 beh2 ->
behavior_improves (
behavior_app t beh1) (
behavior_app t beh2).
Proof.
intros.
red;
destruct H.
left;
congruence.
destruct H as [
t' [
A [
beh'
B]]].
subst.
right;
exists (
t **
t');
split;
auto.
exists beh'.
rewrite behavior_app_assoc;
auto.
Qed.
Associating behaviors to programs.
Section PROGRAM_BEHAVIORS.
Variable L:
semantics.
Inductive state_behaves (
s:
state L):
program_behavior ->
Prop :=
|
state_terminates:
forall t s'
r,
Star L s t s' ->
final_state L s'
r ->
state_behaves s (
Terminates t r)
|
state_diverges:
forall t s',
Star L s t s' ->
Forever_silent L s' ->
state_behaves s (
Diverges t)
|
state_reacts:
forall T,
Forever_reactive L s T ->
state_behaves s (
Reacts T)
|
state_goes_wrong:
forall t s',
Star L s t s' ->
Nostep L s' ->
(
forall r, ~
final_state L s'
r) ->
state_behaves s (
Goes_wrong t).
Inductive program_behaves:
program_behavior ->
Prop :=
|
program_runs:
forall s beh,
initial_state L s ->
state_behaves s beh ->
program_behaves beh
|
program_goes_initially_wrong:
(
forall s, ~
initial_state L s) ->
program_behaves (
Goes_wrong E0).
Lemma state_behaves_app:
forall s1 t s2 beh,
Star L s1 t s2 ->
state_behaves s2 beh ->
state_behaves s1 (
behavior_app t beh).
Proof.
Existence of behaviors
We now show that any program admits at least one behavior.
The proof requires classical logic: the axiom of excluded middle
and an axiom of description.
The most difficult part of the proof is to show the existence
of an infinite trace in the case of reactive divergence.
Section TRACEINF_REACTS.
Variable s0:
state L.
Hypothesis reacts:
forall s1 t1,
Star L s0 t1 s1 ->
exists s2,
exists t2,
Star L s1 t2 s2 /\
t2 <>
E0.
Lemma reacts':
forall s1 t1,
Star L s0 t1 s1 ->
{
s2 :
state L & {
t2 :
trace |
Star L s1 t2 s2 /\
t2 <>
E0 } }.
Proof.
CoFixpoint build_traceinf' (
s1:
state L) (
t1:
trace) (
ST:
Star L s0 t1 s1) :
traceinf' :=
match reacts'
ST with
|
existT s2 (
exist t2 (
conj A B)) =>
Econsinf'
t2
(
build_traceinf' (
star_trans ST A (
eq_refl _)))
B
end.
Lemma reacts_forever_reactive_rec:
forall s1 t1 (
ST:
Star L s0 t1 s1),
Forever_reactive L s1 (
traceinf_of_traceinf' (
build_traceinf'
ST)).
Proof.
cofix COINDHYP; intros.
rewrite (unroll_traceinf' (build_traceinf' ST)). simpl.
destruct (reacts' ST) as [s2 [t2 [A B]]].
rewrite traceinf_traceinf'_app.
econstructor. eexact A. auto. apply COINDHYP.
Qed.
Lemma reacts_forever_reactive:
exists T,
Forever_reactive L s0 T.
Proof.
End TRACEINF_REACTS.
Lemma diverges_forever_silent:
forall s0,
(
forall s1 t1,
Star L s0 t1 s1 ->
exists s2,
Step L s1 E0 s2) ->
Forever_silent L s0.
Proof.
cofix COINDHYP;
intros.
destruct (
H s0 E0)
as [
s1 ST].
constructor.
econstructor.
eexact ST.
apply COINDHYP.
intros.
eapply H.
eapply star_left;
eauto.
Qed.
Lemma state_behaves_exists:
forall s,
exists beh,
state_behaves s beh.
Proof.
Theorem program_behaves_exists:
exists beh,
program_behaves beh.
Proof.
End PROGRAM_BEHAVIORS.
Forward simulations and program behaviors
Section FORWARD_SIMULATIONS.
Context L1 L2 index order match_states (
S:
fsim_properties L1 L2 index order match_states).
Lemma forward_simulation_state_behaves:
forall i s1 s2 beh1,
match_states i s1 s2 ->
state_behaves L1 s1 beh1 ->
exists beh2,
state_behaves L2 s2 beh2 /\
behavior_improves beh1 beh2.
Proof.
End FORWARD_SIMULATIONS.
Theorem forward_simulation_behavior_improves:
forall L1 L2,
forward_simulation L1 L2 ->
forall beh1,
program_behaves L1 beh1 ->
exists beh2,
program_behaves L2 beh2 /\
behavior_improves beh1 beh2.
Proof.
Corollary forward_simulation_same_safe_behavior:
forall L1 L2,
forward_simulation L1 L2 ->
forall beh,
program_behaves L1 beh ->
not_wrong beh ->
program_behaves L2 beh.
Proof.
Backward simulations and program behaviors
Section BACKWARD_SIMULATIONS.
Context L1 L2 index order match_states (
S:
bsim_properties L1 L2 index order match_states).
Definition safe_along_behavior (
s:
state L1) (
b:
program_behavior) :
Prop :=
forall t1 s'
b2,
Star L1 s t1 s' ->
b =
behavior_app t1 b2 ->
(
exists r,
final_state L1 s'
r)
\/ (
exists t2,
exists s'',
Step L1 s'
t2 s'').
Remark safe_along_safe:
forall s b,
safe_along_behavior s b ->
safe L1 s.
Proof.
intros;
red;
intros.
eapply H;
eauto.
symmetry;
apply behavior_app_E0.
Qed.
Remark star_safe_along:
forall s b t1 s'
b2,
safe_along_behavior s b ->
Star L1 s t1 s' ->
b =
behavior_app t1 b2 ->
safe_along_behavior s'
b2.
Proof.
Remark not_safe_along_behavior:
forall s b,
~
safe_along_behavior s b ->
exists t,
exists s',
behavior_prefix t b
/\
Star L1 s t s'
/\
Nostep L1 s'
/\ (
forall r, ~(
final_state L1 s'
r)).
Proof.
intros.
destruct (
not_all_ex_not _ _ H)
as [
t1 A];
clear H.
destruct (
not_all_ex_not _ _ A)
as [
s'
B];
clear A.
destruct (
not_all_ex_not _ _ B)
as [
b2 C];
clear B.
destruct (
imply_to_and _ _ C)
as [
D E];
clear C.
destruct (
imply_to_and _ _ E)
as [
F G];
clear E.
destruct (
not_or_and _ _ G)
as [
P Q];
clear G.
exists t1;
exists s'.
split.
exists b2;
auto.
split.
auto.
split.
red;
intros;
red;
intros.
elim Q.
exists t;
exists s'0;
auto.
intros;
red;
intros.
elim P.
exists r;
auto.
Qed.
Lemma backward_simulation_star:
forall s2 t s2',
Star L2 s2 t s2' ->
forall i s1 b,
match_states i s1 s2 ->
safe_along_behavior s1 (
behavior_app t b) ->
exists i',
exists s1',
Star L1 s1 t s1' /\
match_states i'
s1'
s2'.
Proof.
Lemma backward_simulation_forever_silent:
forall i s1 s2,
Forever_silent L2 s2 ->
match_states i s1 s2 ->
safe L1 s1 ->
Forever_silent L1 s1.
Proof.
Lemma backward_simulation_forever_reactive:
forall i s1 s2 T,
Forever_reactive L2 s2 T ->
match_states i s1 s2 ->
safe_along_behavior s1 (
Reacts T) ->
Forever_reactive L1 s1 T.
Proof.
Lemma backward_simulation_state_behaves:
forall i s1 s2 beh2,
match_states i s1 s2 ->
state_behaves L2 s2 beh2 ->
exists beh1,
state_behaves L1 s1 beh1 /\
behavior_improves beh1 beh2.
Proof.
End BACKWARD_SIMULATIONS.
Theorem backward_simulation_behavior_improves:
forall L1 L2,
backward_simulation L1 L2 ->
forall beh2,
program_behaves L2 beh2 ->
exists beh1,
program_behaves L1 beh1 /\
behavior_improves beh1 beh2.
Proof.
Corollary backward_simulation_same_safe_behavior:
forall L1 L2,
backward_simulation L1 L2 ->
(
forall beh,
program_behaves L1 beh ->
not_wrong beh) ->
(
forall beh,
program_behaves L2 beh ->
program_behaves L1 beh).
Proof.
Program behaviors for the "atomic" construction
Section ATOMIC.
Variable L:
semantics.
Hypothesis Lwb:
well_behaved_traces L.
Remark atomic_finish:
forall s t,
output_trace t ->
Star (
atomic L) (
t,
s)
t (
E0,
s).
Proof.
Lemma step_atomic_plus:
forall s1 t s2,
Step L s1 t s2 ->
Plus (
atomic L) (
E0,
s1)
t (
E0,
s2).
Proof.
Lemma star_atomic_star:
forall s1 t s2,
Star L s1 t s2 ->
Star (
atomic L) (
E0,
s1)
t (
E0,
s2).
Proof.
Lemma atomic_forward_simulation:
forward_simulation L (
atomic L).
Proof.
Lemma atomic_star_star_gen:
forall ts1 t ts2,
Star (
atomic L)
ts1 t ts2 ->
exists t',
Star L (
snd ts1)
t' (
snd ts2) /\
fst ts1 **
t' =
t **
fst ts2.
Proof.
induction 1.
exists E0;
split.
apply star_refl.
traceEq.
destruct IHstar as [
t' [
A B]].
simpl in H;
inv H;
simpl in *.
exists t';
split.
eapply star_left;
eauto.
auto.
exists (
ev ::
t0 **
t');
split.
eapply star_left;
eauto.
rewrite B;
auto.
exists t';
split.
auto.
rewrite B;
auto.
Qed.
Lemma atomic_star_star:
forall s1 t s2,
Star (
atomic L) (
E0,
s1)
t (
E0,
s2) ->
Star L s1 t s2.
Proof.
intros.
exploit atomic_star_star_gen;
eauto.
intros [
t' [
A B]].
simpl in *.
replace t with t'.
auto.
subst;
traceEq.
Qed.
Lemma atomic_forever_silent_forever_silent:
forall s,
Forever_silent (
atomic L)
s ->
Forever_silent L (
snd s).
Proof.
Remark star_atomic_output_trace:
forall s t t'
s',
Star (
atomic L) (
E0,
s)
t (
t',
s') ->
output_trace t'.
Proof.
assert (
forall ts1 t ts2,
Star (
atomic L)
ts1 t ts2 ->
output_trace (
fst ts1) ->
output_trace (
fst ts2)).
induction 1;
intros.
auto.
inv H;
simpl in *.
apply IHstar.
auto.
apply IHstar.
exploit Lwb;
eauto.
destruct H2.
apply IHstar.
auto.
intros.
change t'
with (
fst (
t',
s')).
eapply H;
eauto.
simpl;
auto.
Qed.
Lemma atomic_forever_reactive_forever_reactive:
forall s T,
Forever_reactive (
atomic L) (
E0,
s)
T ->
Forever_reactive L s T.
Proof.
assert (
forall t s T,
Forever_reactive (
atomic L) (
t,
s)
T ->
exists T',
Forever_reactive (
atomic L) (
E0,
s)
T' /\
T =
t ***
T').
induction t;
intros.
exists T;
auto.
inv H.
inv H0.
congruence.
simpl in H;
inv H.
destruct (
IHt s (
t2***
T0))
as [
T' [
A B]].
eapply star_forever_reactive;
eauto.
exists T';
split;
auto.
simpl.
congruence.
cofix COINDHYP;
intros.
inv H0.
destruct s2 as [
t2 s2].
destruct (
H _ _ _ H3)
as [
T' [
A B]].
assert (
Star (
atomic L) (
E0,
s) (
t**
t2) (
E0,
s2)).
eapply star_trans.
eauto.
apply atomic_finish.
eapply star_atomic_output_trace;
eauto.
auto.
replace (
t ***
T0)
with ((
t **
t2) ***
T').
apply forever_reactive_intro with s2.
apply atomic_star_star;
auto.
destruct t;
simpl in *;
unfold E0 in *;
congruence.
apply COINDHYP.
auto.
subst T0;
traceEq.
Qed.
Theorem atomic_behaviors:
forall beh,
program_behaves L beh <->
program_behaves (
atomic L)
beh.
Proof.
End ATOMIC.
Additional results about infinite reduction sequences
We now show that any infinite sequence of reductions is either of
the "reactive" kind or of the "silent" kind (after a finite number
of non-silent transitions). The proof necessitates the axiom of
excluded middle. This result is used below to relate
the coinductive big-step semantics for divergence with the
small-step notions of divergence.
Unset Implicit Arguments.
Section INF_SEQ_DECOMP.
Variable genv:
Type.
Variable state:
Type.
Variable step:
genv ->
state ->
trace ->
state ->
Prop.
Variable ge:
genv.
Inductive tstate:
Type :=
ST:
forall (
s:
state) (
T:
traceinf),
forever step ge s T ->
tstate.
Definition state_of_tstate (
S:
tstate):
state :=
match S with ST s T F =>
s end.
Definition traceinf_of_tstate (
S:
tstate) :
traceinf :=
match S with ST s T F =>
T end.
Inductive tstep:
trace ->
tstate ->
tstate ->
Prop :=
|
tstep_intro:
forall s1 t T s2 S F,
tstep t (
ST s1 (
t ***
T) (@
forever_intro genv state step ge s1 t s2 T S F))
(
ST s2 T F).
Inductive tsteps:
tstate ->
tstate ->
Prop :=
|
tsteps_refl:
forall S,
tsteps S S
|
tsteps_left:
forall t S1 S2 S3,
tstep t S1 S2 ->
tsteps S2 S3 ->
tsteps S1 S3.
Remark tsteps_trans:
forall S1 S2,
tsteps S1 S2 ->
forall S3,
tsteps S2 S3 ->
tsteps S1 S3.
Proof.
induction 1; intros. auto. econstructor; eauto.
Qed.
Let treactive (
S:
tstate) :
Prop :=
forall S1,
tsteps S S1 ->
exists S2,
exists S3,
exists t,
tsteps S1 S2 /\
tstep t S2 S3 /\
t <>
E0.
Let tsilent (
S:
tstate) :
Prop :=
forall S1 t S2,
tsteps S S1 ->
tstep t S1 S2 ->
t =
E0.
Lemma treactive_or_tsilent:
forall S,
treactive S \/ (
exists S',
tsteps S S' /\
tsilent S').
Proof.
Lemma tsteps_star:
forall S1 S2,
tsteps S1 S2 ->
exists t,
star step ge (
state_of_tstate S1)
t (
state_of_tstate S2)
/\
traceinf_of_tstate S1 =
t ***
traceinf_of_tstate S2.
Proof.
induction 1.
exists E0;
split.
apply star_refl.
auto.
inv H.
destruct IHtsteps as [
t' [
A B]].
exists (
t **
t');
split.
simpl;
eapply star_left;
eauto.
simpl in *.
subst T.
traceEq.
Qed.
Lemma tsilent_forever_silent:
forall S,
tsilent S ->
forever_silent step ge (
state_of_tstate S).
Proof.
Lemma treactive_forever_reactive:
forall S,
treactive S ->
forever_reactive step ge (
state_of_tstate S) (
traceinf_of_tstate S).
Proof.
Theorem forever_silent_or_reactive:
forall s T,
forever step ge s T ->
forever_reactive step ge s T \/
exists t,
exists s',
exists T',
star step ge s t s' /\
forever_silent step ge s' /\
T =
t ***
T'.
Proof.
End INF_SEQ_DECOMP.
Set Implicit Arguments.
Big-step semantics and program behaviors
Section BIGSTEP_BEHAVIORS.
Variable B:
bigstep_semantics.
Variable L:
semantics.
Hypothesis sound:
bigstep_sound B L.
Lemma behavior_bigstep_terminates:
forall t r,
bigstep_terminates B t r ->
program_behaves L (
Terminates t r).
Proof.
Lemma behavior_bigstep_diverges:
forall T,
bigstep_diverges B T ->
program_behaves L (
Reacts T)
\/
exists t,
program_behaves L (
Diverges t) /\
traceinf_prefix t T.
Proof.
intros.
exploit (
bigstep_diverges_sound sound);
eauto.
intros [
s1 [
P Q]].
exploit forever_silent_or_reactive;
eauto.
intros [
X | [
t [
s' [
T' [
X [
Y Z]]]]]].
left.
econstructor;
eauto.
constructor;
auto.
right.
exists t;
split.
econstructor;
eauto.
econstructor;
eauto.
exists T';
auto.
Qed.
End BIGSTEP_BEHAVIORS.