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

If  Sf sim_c S  and  S -->* S'

then either 	(1) Sf -->* Sf'  and  Sf' sim_c S'	
		(2) Sf -->* recover(S.h)
		
		
PROOF: By induction on the structure of  S -->* S'
------


CASE-BLK-EVAL-RECOVER:
~~~~~~~~~~~~~~~~~~~~~~

(C,h,R,b) -->_0 recover(h)
-------------------------- (blk-eval-recover)
(C,h,R,b) -->*_0 recover(h)

S -/->* recover(h)						[ Non Faulty Block Execution Lemma, a1 ]
subcase does not apply
* BLK-EVAL-RECOVER complete



CASE BLK-EVAL-BRZ:
~~~~~~~~~~~~~~~~~~

------------------------------------------- (blk-eval-brz)
(C,h,R,brz rz rt) -->*_0  (C,h,R,brz rz rt)

1. Sf = (C,h,Rf,jmp rt)					[ Inversion of (sim-S), a1 ]
2. Sf -->*_0 Sf						[ (blk-eval-brz), 1 ]
3. Sf -->* Sf and Sf sim_c S				[ 2, a1 ]	
* BLK-EVAL-BRZ complete




CASE BLK-EVAL-JMP:
~~~~~~~~~~~~~~~~~~


--------------------------------------- (blk-eval-jmp)
(C,h,R,jmp rt) -->*_0  (C,h,R,jmp rt)


1. Sf = (C,h,Rf,jmp rt)					[ Inversion of (sim-S), a1 ]
2. Sf -->*_0 Sf						[ (blk-eval-jmp), 1 ]
3. Sf -->* Sf and Sf sim_c S				[ 2, a1 ]				
* BLK-EVAL-JMP complete




CASE BLK-EVAL-SEQUENCE:
~~~~~~~~~~~~~~~~~~~~~~~

 
(C,h,R,b) -->_k1 (C,h,R',b')    (C,h,R',b') -->*_k2 MS''
----------------------------------------------------------------- (blk-eval-sequence)
(C,h,R,b) -->*_0 MS''




1. Sf -->_0 Sf'  and  Sf' sim_c (C,h,R',b')		[ Block Step Lemma, a1, p1 ]
   OR Sf -->_0 recover
subcase on 1.

SUBCASE BLK-EVAL-SEQUENCE.A: Faulty execution has been simulating original...
a1. Sf -->_0 Sf'
a2. Sf' sim_c (C,h,R',i';b')

3a. Sf' -->* Sf'' and Sf'' sim_c S''			[ I.H., a2, p2 ]
    OR Sf' -->* recover(h)
subcase on 3a.

subsubcase BLK-EVAL-SEQUENCE.A1: ...and continues to do so
aa1. Sf' -->* Sf''
aa2. Sf'' sim_c S''
4a1. Sf -->* Sf''					[ (blk-eval-sequence), a1, aa1 ]
5a1. Sf -->* Sf'' and Sf'' sim_c S''			[ 4a1, aa2 ]
* subsubcase BLK-EVAL-SEQUENCE.A1 complete

subsubcase BLK-EVAL-SEQUENCE.A2: ...but recovers in the last step
aa2. Sf' -->* recover(h)
5b2. Sf -->* recover(h)					[ (blk-eval-sequence), a1, ab1 ]
* subsubcase BLK-EVAL-SEQUENCE.A2 complete


SUBCASE BLK-EVAL-SEQUENCE.B: Faulty execution has already recovered
a1. Sf -->_0 recover(h)
2a. Sf -->* recover(h)					[ (blk-eval-recover), a1 ]
* SUBCASE BLK-EVAL-SEQUENCE.B complete


** Block Execution Lemma Complete



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


Block Step Lemma
------------------

If   Sf sim_c (C,h,R,b)  and  (C,h,R,b) -->_0 (C,h,R',b')

then either 	(1) Sf -->_0 Sf'  and  Sf' sim_c (C,h,R',b')
		(2) Sf -->_0 recover(h)
	
	
PROOF: By case analysis of (C,h,R,b) -->_0 (C,h,R',b')


a1. Sf sim_c (C,h,R,b)
a2. (C,h,R,b) -->_0 (C,h,R',b')

1. Sf = (C,h,Rf,b)							[ Lemma Sim_c-Typing, a1 ]
2. |- C : P
3. P |- R : G
4. P |-c Rf : G
5. |- h : A
6. |- Ei = end(h)
7. .;P;G;A;Ei;P(l+1) |- b

8. Forall r. Rf(r) sim_c R(r)						[ Inversion of (sim-S), a1, Inversion of (sim-R) ]

9. |- (C,h,R',b')							[ Preservation Part 1, (Inversion of (sim-S), a1), a2 ]
10. |-c (C,h,Rf,b)							[ Inversion of (sim-S), a1 ]



CASE MOVI:
~~~~~~~~~~
	
---------------------------------------------------- (movi)
(C, h, R, movi rd v; b) -->_0 (C, h, R[rd -> v], b)

15. (C, h, Rf, movi rd v; b) -->_0 (C, h, Rf[rd -> v], b)		[ (movi) ]
16. |-c (C, h, Rf[rd -> v], b)						[ Preservation-No-Elevation, 10, 15 ]

17. v sim_c v								[ (sim-val) ]
18. Rf[rd -> v]  sim_c R[rd -> v]					[ (sim-R), 8, 17 ]
19. (C, h, Rf[rd -> v], b) sim_c (C, h, R[rd -> v], b)			[ (sim-S), 9, 16, 18 ]

20. Sf -->_0 Sf'  and  Sf' sim_c S'					[ 15, 19 ]
* MOVI complete



CASE SUB:
~~~~~~~~~

v' = R_col(rs1) (R_val(rs1) - R_val(rs2))
--------------------------------------------------------------- (sub)
(C, h, R, sub rd, rs1, rs2; b) -->_0 (C, h, R[ rd -> v' ],  b)

15. Rf(rs1) sim_c R(rs1)						[ 8 ]
16. Rf_col(rs1) = R_col(rs1)						[ Inspection of (val-t) ]

d1. let vf' = Rf_col(rs1) (Rf_val(rs1) - Rf_val(rs2))

subcase Rf_col(rs1) = c
17a. vf' sim_c vf							[ (sim-val-zap), 16, subcase assumption ]
subcase Rf_col(rs1) =/= c
17b. .;P;G |- sub rd, rs1, rs2 : G'					[ Inversion of (sequence-t), 7 ]
18b. R_col(rs1) = R_col(rs2)						[ Inversion of (sub-t), 3 ]
19b. Rf(rs1) = R(rs1)  and  Rf(rs2) = R(rs2)				[ Inversion of (sim-val), 18, subcase assumption ]
20b. vf' sim_c v'							[ (sim-val), 19b, d1, p1 ]
merge:
21. vf' sim_c v'							[ 17a/20b]

22. (C, h, Rf, sub rd, rs1, rs2; b) -->_0 (C, h, Rf[ rd -> vf' ],  b)	[ (sub) ]
23. |-c (C, h, Rf[rd -> v], b)						[ Preservation-No-Elevation, 10, 22 ]

24. Rf[rd -> vf']  sim_c R[rd -> v']					[ (sim-R), 8, 21 ]
25. (C, h, Rf[rd -> v], b) sim_c (C, h, R[rd -> v], b)			[ (sim-S), 9, 23, 24 ]

26. Sf -->_0 Sf'  and  Sf' sim_c S'					[ 22, 25 ]
* SUB complete



CASE INTEND:
~~~~~~~~~~~~

---------------------------------------------------------- (intend)
(C, h, R, intend rt; b) -->_0 (C, h, R[ri -> R(rt)],  b)

15. (C, h, Rf, intend rt; b) -->_0 (C, h, Rf[ri -> Rf(rt)],  b)		[ (intend) ]
16. |-c (C, h, Rf[ri -> Rf(rt)], b)					[ Preservation-No-Elevation, 10, 15 ]

17. Rf(rt) sim_c R(rt)							[ 8 ]
18. Rf[ri -> Rf(rt)]  sim_c R[ri -> R(rt)]				[ (sim-R), 8, 17 ]
19. (C, h, Rf[ri -> Rf(rt)],  b) sim_c (C, h, R[ri -> R(rt)], b)	[ (sim-S), 9, 16, 18 ]

20. Sf -->_0 Sf'  and  Sf' sim_c S'					[ 15, 19 ]
* INTEND complete




CASE INTENDZ-SET:
~~~~~~~~~~~~~~~~~

R_val(rz) = 0
-------------------------------------------------------------- (intendz-set)
(C, h, R, intendz rz rt; b) -->_0 (C, h, R[ri -> R(rt)],  b)    

14. R_col(rz) = Rf_col(rz) = B						[ Inversion on (sequence-t), (intendz), Canonical Forms, 4, 5 ]

subcase c =/= B:
14a. R_val(rz) = Rf_val(rz)						[ Inversion on (val-t), c =/= B, 14a, 8 ]
15a. (C, h, Rf, intendz rz rt; b) -->_0 (C, h, Rf[ri -> Rf(rt)],  b)	[ (intendz-set), (14a, p1) ]
16a. |-c (C, h, Rf[ri -> Rf(rt)],  b)					[ Preservation-No-Elevation, 10, 15a ]
17a. Rf[ri -> Rf(rt)] sim_c R[ri -> R(rt)]				[ (sim-R), 8, 14a, 14 ]
18a. (C, h, Rf[ri -> Rf(rt)],  b) sim_c (C, h, R[ri -> R(rt)],  b) 	[ (sim-S), 17a, 9, 16a ]
19a. Sf -->_0 Sf'  and  Sf' sim_c S'					[ 15a, 18a ]
* INTENDZ-SET.A complete

subcase c = B  and Rf_val(rz) = 0
14b. (C, h, Rf, intendz rz rt; b) -->_0 (C, h, Rf[ri -> Rf(rt)],  b)	[ (intendz-set), subcase assumption ]
15b. |-c (C, h, Rf[ri -> Rf(rt)],  b)					[ Preservation-No-Elevation, 10, 14b ]
16b. Rf(rt) sim_B R(rt)							[ (sim-val), 14, c = B ]
17b. Rf[ri -> Rf(rt)] sim_c R[ri -> R(rt)]				[ (sim-R), 8, 16b ]
18b. (C, h, Rf[ri -> Rf(rt)],  b) sim_B (C, h, R[ri -> R(rt)],  b)	[ (sim-S), 16b, 15b, 9 ]
19b. Sf -->_0 Sf'  and  Sf' sim_c S'					[ 14b, 18b ]
* INTENDZ-SET.B complete

subcase c = B and  Rf_val =/= 0
14c. (C, h, Rf, intendz rz rt; b) -->_0 (C, h, Rf, b)			[ (intendz-unset), subcase assumption ]
15c. |-c (C, h, Rf, b)							[ Preservation-No-Elevation, 10, 14c ]
16c. Rf_col(ri) = B							[ Inversion on (sequence-t), (intendz), Canonical Forms, 5 ]
17c. Rf(ri) sim_B R(rt)							[ (sim-val-zap-c), c = B, 16c, 14 ]
18c. Rf sim_B R[ri -> R(rt)]						[ (sim-R), 8, 17c ]
19c. (C, h, Rf, b) sim_B (C, h, R[ri -> R(rt)],  b)			[ (sim-S), 18c, 15c, 9 ]
20c. Sf -->_0 Sf'  and  Sf' sim_c S'					[ 14c, 19c ]
* INTENDZ-SET.C complete



CASE INTENDZ-UNSET:
~~~~~~~~~~~~~~~~~~~

R_val(rz) =/= 0
------------------------------------------------- (intendz-unset)
(C, h, R, intendz rz rt; b) -->_0 (C, h, R, b)

14. R_col(rz) = Rf_col(rz) = B						[ Inversion on (sequence-t), (intendz), Canonical Forms, 4, 5 ]

subcase c =/= B:
14a. R_val(rz) = Rf_val(rz)						[ Inversion on (sim-val), c =/= B, 14a, 8 ]
15a. (C, h, Rf, intendz rz rt; b) -->_0 (C, h, Rf,  b)			[ (intendz-unset), (14a, p1) ]
16a. |-c (C, h, Rf,  b)							[ Preservation-No-Elevation, 10, 15a ]
17a. Rf sim_c R								[ Inversion on (sim-S), a1 ]
18a. (C, h, Rf,  b) sim_c (C, h, R,  b) 				[ (sim-S), 17a, 9, 16a ]
19a. Sf -->_0 Sf'  and  Sf' sim_c S'					[ 15a, 18a ]
* INTENDZ-UNSET.A complete

subcase c = B  and Rf_val(rz) =/= 0
14b. (C, h, Rf, intendz rz rt; b) -->_0 (C, h, Rf, b)			[ (intendz-unset), subcase assumption ]
15b. |-c (C, h, Rf,  b)							[ Preservation-No-Elevation, 10, 14b ]
16b. Rf sim_c R								[ Inversion on (sim-S), a1 ]
17b. (C, h, Rf,  b) sim_B (C, h, R, b)					[ (sim-S), 16b, 15b, 9 ]
18b. Sf -->_0 Sf'  and  Sf' sim_c S'					[ 14b, 17b ]
* INTENDZ-SET.B complete

subcase c = B and  Rf_val = 0
14c. (C, h, Rf, intendz rz rt; b) -->_0 (C, h, Rf[ri -> R(rt)], b)	[ (intendz-set), subcase assumption ]
15c. |-c (C, h, Rf[ri -> R(rt)], b)					[ Preservation-No-Elevation, 10, 14c ]
16c. Rf_col(rt) = B							[ Inversion on (sequence-t), (intendz), Canonical Forms, 5 ]
17c. Rf(rt) sim_B R(rt)							[ (sim-val-zap-c), c = B, 16c, 14 ]
18c. Rf[ri -> R(rt)] sim_B R						[ (sim-R), 8, 17c ]
19c. (C, h, Rf[ri -> R(rt)], b) sim_B (C, h, R,  b)			[ (sim-S), 18c, 15c, 9 ]
20c. Sf -->_0 Sf'  and  Sf' sim_c S'					[ 14c, 19c ]
* INTENDZ-SET.C complete




CASE RECOVERNZ-OK:
~~~~~~~~~~~~~~~~~

R_val(rz) = 0
---------------------------------------------- (recovernz-ok)
(C, h, R, recovernz rz; b) -->_0 (C, h, R, b) 
 
14. R_col(rz) = Rf_col(rz) = R						[ Inversion on (sequence-t), (intendz), Canonical Forms, 4, 5 ]

subcase Rf_val(rz) = 0:
15a. (C, h, Rf, recovernz rz; b) -->_0 (C, h, Rf, b)			[ (recovernz-ok), subcase assumption ]
16a. |-c (C, h, Rf, b)							[ Preservation-No-Elevation, 10, 15c ]
17a. Rf sim_c R 							[ Inversion on (sim-S), a1 ]
18a. (C, h, Rf, b) sim_R (C, h, R, b)					[ (sim-S), 17a, 16a, 9 ]
19a. Sf -->_0 Sf'  and  Sf' sim_c S'					[ 15a, 18a ]
* RECOVERNZ-OK.A complete

subcase Rf_val(rz) =/= 0:
15a. (C, h, Rf, recovernz rz; b) -->_0 halt(h)				[ (recovernz-halt), subcase assumption ]
* RECOVERNZ-OK.B complete



CASE RECOVERNZ-HALT:
~~~~~~~~~~~~~~~~~~~~

R_val(rz) =/= 0
-------------------------------------------- (recovernz-halt)
(C, h, R, recovernz rz; b) -->_0 recover(h)

S -/->_0 S'
case does not apply
* RECOVERNZ-HALT complete



CASES BRZ-UNTAKEN, BRZ-TAKEN, JMP:
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

S'.h =/= S.h
cases do not apply
* BRZ-UNTAKEN, BRZ-TAKEN, JMP complete




CASES BRZ-HW-ERROR, JMP-HW-ERROR:
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

S -/->_0 S'
cases do not apply
* BRZ-HW-ERROR, JMP-HW-ERROR complete


** BLOCK STEP LEMMA COMPLETE