We proved that if a CETS instrumented program terminates successfully, the original C program will not cause any memory violation.

Lemma s_lhs__implies__us_lhs : forall E lhs l r ri t,
  s_lhs E lhs (RLoc (l, r, ri)) t ->
  us_lhs (Env2uEnv E) lhs (uRLoc l) t.

Lemma s_lhs__cannot__SystemError : forall E lhs R t,
  s_lhs E lhs R t -> R <> SystemError.

Lemma s_rhs__implies__us_rhs : forall E rhs v m t E',
  s_rhs E rhs (RVal (v, m)) t E' ->
  us_rhs (Env2uEnv E) rhs (uRVal v) t (Env2uEnv E').

Lemma ErrorR__inv : forall R,
  Error R -> R = ROK \/ R = SystemError \/ R = Abort.

Lemma s_cmd__cannot__RVal_or_RLoc : forall E cmd R E',
  s_cmd E cmd R E' ->
  R = ROK \/ R = SystemError \/ R = Abort.

Lemma uROK__isnot__uErrorR : ~ uError uROK.

Lemma s_cmd__implies__us_cmd : forall E cmd E',
  s_cmd E cmd ROK E' -> us_cmd (Env2uEnv E) cmd uROK (Env2uEnv E').