Props



This file proves the main result: safety of CETS.

s_rhs and s_cmd preserve Global and Stack.


s_rhs and s_cmd do not change Global.
Lemma s_rhs__G :
(forall E rhs R t E', s_rhs E rhs R t E' ->
  (forall G AMB S MM M RI rev G' AMB' S' M' MM' RI' rev',
      E = MkEnv M MM AMB G S RI rev ->
      E' = MkEnv M' MM' AMB' G' S' RI' rev'->
      G = G'
  )
)
.

Lemma s_cmd__G :
(forall E c E', s_cmd E c ROK E' ->
  (forall G S M MM AMB RI rev G' S' M' MM' AMB' RI' rev',
      E = MkEnv M MM AMB G S RI rev ->
      E' = MkEnv M' MM' AMB' G' S' RI' rev' ->
      G = G'
  )
)
.

s_rhs and s_cmd do not change Stack. To prove that s_cmd preserves Stack, we need to prove that s_rhs and s_cmd preserve well-formed frames first.
Lemma s_rhs__S :
(forall E rhs R t E', s_rhs E rhs R t E' ->
  (forall G S M MM AMB RI rev G' S' M' MM' AMB' RI' rev',
      E = MkEnv M MM AMB G S RI rev ->
      E' = MkEnv M' MM' AMB' G' S' RI' rev'->
      S = S'
  )
)
.

Lemma s_rhs__wfFrms : forall E rhs R t E',
  s_rhs E rhs R t E' ->
  wfFrms E.(rev) E.(stack) ->
  wfFrms E'.(rev) E'.(stack).

Lemma s_cmd__S_wfFrms : forall E c E',
  s_cmd E c ROK E' ->
  wfFrms E.(rev) E.(stack) ->
  (forall G S M MM AMB RI rev G' S' M' MM' AMB' RI' rev',
      E = MkEnv M MM AMB G S RI rev ->
      E' = MkEnv M' MM' AMB' G' S' RI' rev' ->
      S = S'
  ) /\
  wfFrms E'.(rev) E'.(stack).

Lemma s_cmd__S :
(forall E c E', s_cmd E c ROK E' ->
  wfFrms E.(rev) E.(stack) ->
  (forall G S M MM AMB RI rev G' S' M' MM' AMB' RI' rev',
      E = MkEnv M MM AMB G S RI rev ->
      E' = MkEnv M' MM' AMB' G' S' RI' rev' ->
      S = S'
  )
)
.

Lookup functions return valid Addresses.

Given a well-formed Env, the return result of lookup functions, lookUpGlobal lookUpStack is a validAddress.
Lemma wfE_lookUpGlobal_validAddresses : forall M MM AMB G S RI rev v l t,
  wfEnv (MkEnv M MM AMB G S RI rev) ->
  lookUpGlobal G v = Some (l, t) ->
  validAddress M (l).

Lemma wfStack_lookUpStack__lookUpFrame : forall M RI rev S v l t r ri,
  wfStack M RI rev S ->
  lookUpStack S v = Some (l, t, r, ri) ->
  exists F, wfFrame M RI F /\ lookUpFrame F v = Some (l, t)/\
    baseAddress < F.(from) /\ F.(from) < F.(to) <= maxAddress /\
    F.(fr) < rev /\ r = F.(fr) /\ ri = F.(fri) /\ head (frames S) = Some F.

Lemma wfEnv_lookUpStack__lookUpFrame : forall M MM AMB G S RI rev v l t r ri,
  wfEnv (MkEnv M MM AMB G S RI rev) ->
  lookUpStack S v = Some (l, t, r, ri) ->
  exists F, wfFrame M RI F /\ lookUpFrame F v = Some (l, t) /\
    baseAddress < F.(from) /\ F.(from) < F.(to) <= maxAddress /\
    F.(fr) < rev /\ r = F.(fr) /\ ri = F.(fri) /\ head (frames S) = Some F.

Lemma wfE_lookUpStack_validAddresses : forall M MM AMB G S RI rev v l t r ri,
  wfEnv (MkEnv M MM AMB G S RI rev) ->
  lookUpStack S v = Some (l, t, r, ri) ->
  validAddress M (l).

Inversion properties of s_lhs and s_rhs.


Lemma lhs__wft : forall lhs t E l r ri,
  s_lhs E lhs (RLoc (l, r, ri)) t ->
  wfEnv E ->
  wf_AType t.

Lemma rhs__wft : forall G S rhs t E M MM AMB RI rev d E',
  s_rhs E rhs (RVal d) t E' ->
  E = MkEnv M MM AMB G S RI rev -> wfEnv E ->
  wf_AType t.

Lemma lhs__inversion : forall G S lhs t E M MM AMB RI rev l r ri,
  s_lhs E lhs (RLoc (l, r, ri)) t ->
  E = MkEnv M MM AMB G S RI rev -> wfEnv E ->
  validAddress M l /\
  (l <> 0 /\ l >= minAddress /\ l+sizeOfAType t <= maxAddress /\ r <> 0)
  .

Lemma s_lhs__wf_lhs : forall E lhs l t,
  s_lhs E lhs (RLoc l) t ->
  wf_lhs E.(global) (Stack2frame (stack E)) lhs t.

Preservation


s_rhs preserves well-formed Envs.

Lemma accessMemMeta__s_rhs__accessMemMeta : forall E rhs R t E',
  s_rhs E rhs R t E' ->
  forall i a,
    accessMemMeta E.(mem) E.(mmeta) i = Some a ->
    accessMemMeta E'.(mem) E'.(mmeta) i = Some a.

Lemma validAddress__s_rhs__validAddress :
(forall E rhs ds t E', s_rhs E rhs (RVal ds) t E' -> (forall i, validAddress E.(mem) i -> validAddress E'.(mem) i)).

Lemma wfE__s_rhs__wfE :
(forall E rhs R t E', s_rhs E rhs R t E' -> (wfEnv E -> wfEnv E')).

s_rhs evaluates to wfData.

Lemma wfD__cast__wfD : forall M RI ds t t' v' m' rev,
  rev >= 2 ->
  wf_AType t ->
  wf_AType t' ->
  wfData M RI (snd ds) rev ->
  dataCast t' ds t = (v', m') ->
  wfData M RI m' rev.

Lemma wfE_lookUpGlobal_wfD : forall E l v t ds,
  wfEnv E ->
  lookUpGlobal E.(global) v = Some (l, t) ->
  accessMemMeta (E.(mem)) (E.(mmeta)) l = Some ds ->
  wfData E.(mem) E.(revInfo) (snd ds) E.(rev)
  .

Lemma wfE_lookUpStack_wfD : forall E l v t r ri ds,
  wfEnv E ->
  lookUpStack E.(stack) v = Some (l, t, r, ri) ->
  accessMemMeta (E.(mem)) (E.(mmeta)) l = Some ds ->
  wfData E.(mem) E.(revInfo) (snd ds) E.(rev)
  .

Lemma wfE__s_lhs__wfD : forall E lhs loc t r ri ds,
  wfEnv E ->
  s_lhs E lhs (RLoc (loc, r, ri)) t ->
  accessMemMeta (E.(mem)) (E.(mmeta)) loc = Some ds ->
  wfData E.(mem) E.(revInfo) (snd ds) E.(rev)
  .

Lemma wfData__monorev : forall M RI b e r ri rev,
  wfData M RI (b, e, r, ri) rev ->
  r < rev.

Lemma wfE__s_lhs__monorev : forall E lhs loc t r ri,
  wfEnv E ->
  s_lhs E lhs (RLoc (loc, r, ri)) t ->
  r < E.(rev)
  .

Lemma wfE_rev_ge_two : forall E,
  wfEnv E -> rev E >= 2.

Lemma wfE__s_rhs__monorev : forall E rhs v b e r ri t' E',
  wfEnv E ->
  s_rhs E rhs (RVal (v, (b, e, r, ri))) t' E' ->
  r < E'.(rev) /\ E.(rev) <= E'.(rev)
  .

Lemma wfE__s_rhs__monoRI : forall E rhs R t E' r,
  wfEnv E ->
  s_rhs E rhs R t E' ->
  ((E.(revInfo) r <> 0 -> E.(revInfo) r = E'.(revInfo) r) /\
  (E.(revInfo) r = 0 ->
      ((E.(revInfo) r < E'.(revInfo) r /\ E.(rev) <= E'.(revInfo) r)) \/
      (E.(revInfo) r = E'.(revInfo) r))
  ).

Lemma wfE__s_rhs__wfD :
(forall E rhs ds t E',
  s_rhs E rhs (RVal ds) t E' ->
  (wfEnv E -> wfData E'.(mem) E'.(revInfo) (snd ds) E'.(rev))
).

dataCast preserves well-formed Datas.


Lemma wfGlobalPtr_dataCast : forall tl tr v b e r ri v' b' e' r' ri',
  wfGlobalPtr b r ri ->
  dataCast tl (v, (b, e, r, ri)) tr = (v', (b', e', r', ri')) ->
  wfGlobalPtr b' r' ri'.

Lemma wfNonGlobalPtr_dataCast : forall tl tr v b e r ri v' b' e' r' ri',
  wfNonGlobalPtr e r ->
  dataCast tl (v, (b, e, r, ri)) tr = (v', (b', e', r', ri')) ->
  wfNonGlobalPtr e' r'.

Lemma wfStackPtr_dataCast : forall S RI tl tr v b e r ri v' b' e' r' ri',
  wfStackPtr S RI b e r ri ->
  dataCast tl (v, (b, e, r, ri)) tr = (v', (b', e', r', ri')) ->
  wfStackPtr S RI b' e' r' ri'.

Lemma wfNonStackPtr_dataCast : forall S RI tl tr v b e r ri v' b' e' r' ri',
  wfNonStackPtr S RI b r ri ->
  dataCast tl (v, (b, e, r, ri)) tr = (v', (b', e', r', ri')) ->
  wfNonStackPtr S RI b' r' ri'.

Lemma wfUniqRentryH_dataCast : forall E tl tr v b e r ri v' b' e' r' ri',
  wfUniqRentryH E b e r ri ->
  dataCast tl (v, (b, e, r, ri)) tr = (v', (b', e', r', ri')) ->
  wfUniqRentryH E b' e' r' ri'.

Lemma wfUniqRentryGS_dataCast : forall E tl tr v b e r ri v' b' e' r' ri',
  wfUniqRentryGS E r ri ->
  dataCast tl (v, (b, e, r, ri)) tr = (v', (b', e', r', ri')) ->
  wfUniqRentryGS E r' ri'.

Lemma wfOverlapped_dataCast : forall E tl tr v b e r ri v' b' e' r' ri',
  wfOverlapped E b e r ri ->
  dataCast tl (v, (b, e, r, ri)) tr = (v', (b', e', r', ri')) ->
  wfOverlapped E b' e' r' ri'.

Lemma wfOverlappedAMB_dataCast : forall E tl tr v b e r ri v' b' e' r' ri',
  wfOverlappedAMB E b e r ri ->
  dataCast tl (v, (b, e, r, ri)) tr = (v', (b', e', r', ri')) ->
  wfOverlappedAMB E b' e' r' ri'.

accessMemMeta returns well-formed Datas.


Lemma wfE__accessMemMeta__wfGlobalPtr : forall E loc v b e r ri,
  wfEnv E ->
  accessMemMeta (E.(mem)) (E.(mmeta)) loc = Some (v, (b, e, r, ri)) ->
  wfGlobalPtr b r ri.

Lemma wfE__accessMemMeta__wfStackPtr : forall E loc v b e r ri,
  wfEnv E ->
  accessMemMeta (E.(mem)) (E.(mmeta)) loc = Some (v, (b, e, r, ri)) ->
  wfStackPtr E.(stack) E.(revInfo) b e r ri.

Lemma wfE__accessMemMeta__wfNonStackPtr : forall E loc v b e r ri,
  wfEnv E ->
  accessMemMeta (E.(mem)) (E.(mmeta)) loc = Some (v, (b, e, r, ri)) ->
  wfNonStackPtr E.(stack) E.(revInfo) b r ri.

Lemma wfE__accessMemMeta__wfNonGlobalPtr : forall E loc v b e r ri,
  wfEnv E ->
  accessMemMeta (E.(mem)) (E.(mmeta)) loc = Some (v, (b, e, r, ri)) ->
  wfNonGlobalPtr e r.

Lemma wfE__accessMemMeta__wfOverlapped : forall E loc v b e r ri,
  wfEnv E ->
  accessMemMeta (E.(mem)) (E.(mmeta)) loc = Some (v, (b, e, r, ri)) ->
  wfOverlapped E b e r ri.

Lemma wfE__accessMemMeta__wfOverlappedAMB : forall E loc v b e r ri,
  wfEnv E ->
  accessMemMeta (E.(mem)) (E.(mmeta)) loc = Some (v, (b, e, r, ri)) ->
  wfOverlappedAMB E b e r ri.

Lemma wfE__accessMemMeta__wfUniqRentryH : forall E loc v b e r ri,
  wfEnv E ->
  accessMemMeta (E.(mem)) (E.(mmeta)) loc = Some (v, (b, e, r, ri)) ->
  wfUniqRentryH E b e r ri.

Lemma wfE__accessMemMeta__wfUniqRentryGS : forall E loc v b e r ri,
  wfEnv E ->
  accessMemMeta (E.(mem)) (E.(mmeta)) loc = Some (v, (b, e, r, ri)) ->
  wfUniqRentryGS E r ri.

Well-formed Datas are preserved by subset operations.


Lemma wfStackPtr_subset : forall S RI b e r ri b' e',
  wfStackPtr S RI b e r ri ->
  (b <= b' /\ e' <= e) ->
  minAddress <= b < e ->
  wfStackPtr S RI b' e' r ri.

Lemma wfOverlapped_subset : forall E b e r ri b' e',
  wfOverlapped E b e r ri ->
  (b <= b' /\ e' <= e) ->
  minAddress <= b < e ->
  wfOverlapped E b' e' r ri.

Lemma wfOverlappedAMB_subset : forall E b e r ri b' e',
  wfOverlappedAMB E b e r ri ->
  (b <= b' /\ e' <= e) ->
  minAddress <= b < e ->
  wfOverlappedAMB E b' e' r ri.

Lemma wfUniqRentryH_subset : forall E b e r ri b' e',
  wfUniqRentryH E b e r ri ->
  (b <= b' /\ e' <= e) ->
  minAddress <= b < e ->
  wfUniqRentryH E b' e' r ri.

s_lhs evaluates to well-formed Datas.


Lemma wfE__s_lhs__wfGlobalPtr : forall E lhs loc r ri t,
  wfEnv E ->
  s_lhs E lhs (RLoc (loc, r, ri)) t ->
  wfGlobalPtr loc r ri.

Lemma wfE__s_lhs__wfNonGlobalPtr : forall E lhs loc r ri t,
  wfEnv E ->
  s_lhs E lhs (RLoc (loc, r, ri)) t ->
  wfNonGlobalPtr (loc+sizeOfAType t) r.

Lemma wfE__s_lhs__wfNonStackPtr : forall E lhs loc r ri t,
  wfEnv E ->
  s_lhs E lhs (RLoc (loc, r, ri)) t ->
  wfNonStackPtr E.(stack) E.(revInfo) loc r ri.

Lemma wfE__s_lhs__wfUniqRentryGS : forall E lhs loc r ri t,
  wfEnv E ->
  s_lhs E lhs (RLoc (loc, r, ri)) t ->
  wfUniqRentryGS E r ri.

Lemma wfE__s_lhs__wfOverlapped_wfStackPtr : forall E lhs loc r ri t,
  wfEnv E ->
  s_lhs E lhs (RLoc (loc, r, ri)) t ->
  ((r = 1 /\ ri = gri /\
    (minAddress <= loc /\ loc + sizeOfAType t <= baseAddress) /\
     E.(revInfo) ri = r
    ) \/
    (exists F,
        head (frames E.(stack)) = Some F /\ F.(from) <= loc < F.(to) /\
        r = (revInfo E) ri /\ r = F.(fr) /\ ri = F.(fri)
    ) \/
    (exists l, exists b, exists e, exists l',
        accessMemMeta (mem E) (mmeta E) l = Some (l', (b, e, r, ri)) /\
        minAddress <= b /\ b <= l' /\ l' <= loc /\ loc < e /\ r = (revInfo E) ri)).

s_rhs evaluates to well-formed Datas.


Lemma wfE__s_rhs__wfGlobalPtr :
(forall E rhs v b e r ri t E',
  s_rhs E rhs (RVal (v, (b, e, r, ri))) t E' ->
  (wfEnv E -> wfGlobalPtr b r ri)
).

Lemma wfE__s_rhs__wfNonGlobalPtr :
(forall E rhs v b e r ri t E',
  s_rhs E rhs (RVal (v, (b, e, r, ri))) t E' ->
  (wfEnv E -> wfNonGlobalPtr e r)
).

Lemma wfE__s_rhs__wfUniqRentryGS :
(forall E rhs v b e r ri t E',
  s_rhs E rhs (RVal (v, (b, e, r, ri))) t E' ->
  (wfEnv E -> wfUniqRentryGS E' r ri)
).

Lemma wfE__s_rhs__wfStackPtr :
(forall E rhs v b e r ri t E',
  s_rhs E rhs (RVal (v, (b, e, r, ri))) t E' ->
  (wfEnv E -> wfStackPtr E'.(stack) E'.(revInfo) b e r ri)
).

Lemma wfE__s_rhs__wfNonStackPtr :
(forall E rhs v b e r ri t E',
  s_rhs E rhs (RVal (v, (b, e, r, ri))) t E' ->
  (wfEnv E -> wfNonStackPtr E'.(stack) E'.(revInfo) b r ri)
).

Lemma accessNoneSome__s_rhs__accessZero : forall E rhs R t E' l v b e r ri,
  s_rhs E rhs R t E' ->
  accessMemMeta (mem E) (mmeta E) l = None ->
  accessMemMeta (mem E') (mmeta E') l = Some (v, (b, e, r, ri)) ->
  v = 0 /\ b = 0 /\ e = 0 /\ r = 0 /\ ri = 0.

Lemma wfE__s_rhs__wfOverlapped :
(forall E rhs v b e r ri t E',
  s_rhs E rhs (RVal (v, (b, e, r, ri))) t E' ->
  (wfEnv E -> wfOverlapped E' b e r ri)
).

Lemma wfE__s_rhs__wfUniqRentryH :
(forall E rhs v b e r ri t E',
  s_rhs E rhs (RVal (v, (b, e, r, ri))) t E' ->
  (wfEnv E -> wfUniqRentryH E' b e r ri)
).

Lemma wfE__s_rhs__monoAMB : forall E rhs R t E',
  wfEnv E ->
  s_rhs E rhs R t E' ->
  (forall b e, E.(amb) b = Some e -> E'.(amb) b = Some e) /\
  (forall b e,
     E.(amb) b = None ->
     E'.(amb) b = Some e ->
     forall i, b <= i < e -> ~ validAddress E.(mem) i).

Lemma wfE__s_rhs__wfOverlappedAMB :
(forall E rhs v b e r ri t E',
  s_rhs E rhs (RVal (v, (b, e, r, ri))) t E' ->
  (wfEnv E -> wfOverlappedAMB E' b e r ri)
).

s_cmd preserves well-formed Envs.


Theorem wfE__s_cmd__wfE :
(forall E c R E', s_cmd E c R E' -> (wfEnv E -> wfEnv E')).

Progress

Lemma lhs_progress: forall G S f lhs t E M MM AMB RI rev,
  wf_lhs G f lhs t ->
  f = (Stack2frame (stack E)) ->
  E = MkEnv M MM AMB G S RI rev ->
   wfEnv E ->
  (exists l, exists r, exists ri, s_lhs E lhs (RLoc (l, r, ri)) t) \/ s_lhs E lhs Abort t.

Lemma rhs_progress:
(forall G f rhs t, wf_rhs G f rhs t ->
  (forall E M MM AMB S RI rev, wfEnv E ->
                       f = (Stack2frame (stack E)) ->
                       E = (MkEnv M MM AMB G S RI rev) ->
                       (exists ds, exists E', s_rhs E rhs (RVal ds) t E') \/
                       (exists t', exists E', s_rhs E rhs SystemError t' E') \/
                       (exists t', exists E', s_rhs E rhs Abort t' E')
                       )
).

Theorem Progress : forall E M MM AMB G S RI rev f c,
  wf_cmd G f c ->
  f = (Stack2frame (stack E)) ->
  E = (MkEnv M MM AMB G S RI rev) ->
  wfEnv E ->
  (exists E', s_cmd E c ROK E') \/
  (exists E', s_cmd E c SystemError E') \/
  (exists E', s_cmd E c Abort E').