Require Import List.
Import ListNotations.
Require Import Relations.
Require Import util.
Require Import specification.
Require Import plf.
Require Import PLFO.
Require Import PL.
Require Import PLO.
Require Import PLF_PLFO.
Require Import PLFO_PL.
Require Import PL_PLO.
Require Import PLO_SPEC.
Final correctness result
Definition of the subtrace relation, by sequential composition
of the subtrace_chk and subtrace_log relations.
Definition subtrace (
te:
PLF.trace) (
to:
SPEC.trace) :
Prop :=
exists ti bchkpt blog,
subtrace_chk bchkpt te ti
/\
subtrace_log blog ti to.
The unicity property of the subtrace relation derives from the
unicity properties of the subtrace_log and subtrace_chk
relations.
Lemma subtrace_unicity :
forall te to to',
subtrace te to ->
subtrace te to' ->
to =
to'.
Proof.
unfold subtrace.
intros.
destruct H as [
ti [
bc [
bl [
Hsub_chkpt Hsub_log]]]].
destruct H0 as [
ti' [
bc' [
bl' [
Hsub_chkpt'
Hsub_log']]]].
assert (
bc' =
bc /\
ti' =
ti)
by eauto using subtrace_chk_unique.
intuition subst.
assert (
bl' =
bl /\
to' =
to)
by eauto using subtrace_log_unique.
intuition subst.
auto.
Qed.
Basic transitivity result about the subtrace relation
Lemma subtrace_trans :
forall (
te:
PLF.trace)(
ti:
PLFO.trace),
forall bchkpt blog,
subtrace_chk bchkpt te ti ->
forall (
to:
SPEC.trace),
subtrace_log blog ti to ->
subtrace te to.
Proof.
intros.
exists ti.
exists bchkpt.
exists blog.
split; auto.
Qed.
Final correctness result of the checkpointing model.
Trace inclusion, modulo the subtrace relation.
Theorem correctness_final :
forall t,
PLF.sem t ->
exists t',
SPEC.sem t' /\
subtrace t t'.
Proof.