Fault Tolerance Lemmas


Lemma SIM_C-TYPING
------------------

If Sf sim_c S then

(1) Sf = (C,h,Rf,b)
(2) S =  (C,h,R ,b)
(3) |- C : P
(4) P |- R : G
(5) P |-c Rf : G
(6) |- (h,l) : A
(7) |- Ei = l
(8) .;P;G;A;Ei;P(l+1) |- b 

Proof:
------

1. Sf = (C,h,Rf,b) and S = (C,h,R,b)			[ By inspection of (sim-S), a1 ]

2. |-c (C,h,Rf,b)					[ By inversion of (sim-S), a1 ]
3. |- (C,h,R,b)
4. Rf sim_c R

5. |- C : P						[ By inversion of (S-t), 3 ]
6. P |- R : G
7. |- (h,l) : A
8. . |- Ei = l
10. .;P;G;A;Ei;P(l+1) |- b 

11. Forall r. Rf(r) sim_c R				[ Inversion of (sim-R), 4 ]
12. Forall r. Rf_col(r) = R_col(r)			[ 11, inspection of (val-t) and (val-zap-c-t) ]

13. Forall r. .;P |- R(r) : G(r)
14. Forall r. G(r) = <R_col(c),t'_r, E_r>		[ def of G, 13 ]
15. Forall r. . |- E_r : kint				[ Inversion of (val-t), 14, 14 ]

16. Forall r where R_col(r) = c.			[ (val-zap-c-t), (14, 12), 15 ]
    .;P |-c Rf(r) : G(r)		

17. Forall r where R_col(r) =/= c.			[ Inversion of (val-t), 13 ]
    . |- E_r = R_val(r)	and P |- R_val(r) : t'_r
18. Forall r where R_col(r) =/= c.			[ (val-t), 17, (14, 12) ]
    .;P |-c Rf(r) : G(r)
    
19. P |-c Rf(r) : G(r)					[ 16/18 ]

20. conclusions 1 - 8					[ 1, 1, 5, 6, 19, 7, 8, 10 ]

* Lemma Sim_c-Typing complete

===========================================================================================================================================
===========================================================================================================================================

Lemma NonFaulty Block Execution
--------------------------------

If |- S  then  S --->* S'
If |- S  then  S -->^h S'

Proof: By repeated Progress Part 1 and Preservation Part 1


===========================================================================================================================================
===========================================================================================================================================

Lemma Prog Exec Split
----------------------

If S ->^h S' and length h >= 1 then  Exists S1,S2,S3 h1, h2. S -->^h1 S1 and S1 -->^l S2 and S2 -->* S3 and S3 -->^h2 S'   and h = (h1,l,h2).

Proof: By induction on the structure of S -->^h MS


===========================================================================================================================================
===========================================================================================================================================

Lemma Prog Exec Join
----------------------

If S -->^h1_k1 S1  and S1 -->^l S2 and S2 -->*_k2 S3 and S3 -->^h2_k3 S'
then S -->^(h1,l,h2)

Proof: By induction on the structure of S -->^h2_k3 S'


===========================================================================================================================================
===========================================================================================================================================

Lemma Fault Introduction
-------------------------

If S -->* S'  
then Exists c. S -->*_1 Sf  and  Sf sim_c S'  or  S -->*_1 recover

Proof:
By induction on the structure of S -->* S'.  Single step as in progress 3 -- also prove the Rf sim_c R.
Use Block Step Lemma after fault occurs.