Props
This file proves the main result: safety of CETS.
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'
)
)
.
(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'
)
)
.
(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'
)
)
.
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).
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).
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.
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 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')).
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))
).
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))
).
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'.
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.
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.
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)).
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)
).
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').
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').