Block Transition Lemma ---------------------- If Sf sim_c S and S -->^l S' then either (1) Sf -->^l Sf' and Sf' sim_c S' (2) Sf -->_0 hw_error(S.h) (3) Sf -->^l' Sf' and Sf' -->* recover(S.h,l') Proof: ------ By analysis of the structure of S -->^l' S'. By inspection of (trans-eval), we're looking at all -->_0 rules where the history is extended. CASE BRZ-UNTAKEN: ~~~~~~~~~~~~~~~~~ R_val(rz) =/= 0 l+1 in Dom(C) ---------------------------------------------------------------------------- (brz-untaken) (C, (h,l), R, brz rz rt) -->_0 (C, (h,l,l+1), R[ri -> R R_val(ri)], C(l+1)) a1. Sf sim_sc S a2. S -->^l' S' 1. Sf = (C,(h,l),Rf,brz rz rt) [ Lemma Sim_c-Typing, a1, Inspection of (brz-t) ] 2. S = (C,(h,l),R ,brz rz rt) 3. |- C : P 4. P |- R : G 5. P |-c Rf : G 6. |- (h,l) : seq o Ela 7. |- Ei = l 8. .;P;G;seq o ELa;Ei;P(l+1) |- brz rz rt 9. Forall r. Rf(r) sim_c R(r) [ Inversion of (sim-S), a1, Inversion of (sim-R) ] 10. |-c Sf [ Inversion of (sim-S), a1 ] 11. G(rz) = [ Inversion of (brz-t), 10 ] 12. .;P |- R(rz) : [ Inversion of (R-t), 4, 11 ] 13. . |- R_val(rz) = Ez and R_col(rz) = G [ Canonical Forms, 12, 3 ] 14. .;P |-c Rf(rz) : [ Inversion of (R-t), 5, 11 ] 15. . |- Ez =/= 0 [ Exp Eq Transitivity, p1, 13 ] 16. G(rt) = [ Inversion of (brz-t), 10 ] 17. .;P |- R(rt) : [ Inversion of (R-t), 4, 11 ] 18. . |- R_val(rt) = Et and R_col(rt) = G [ Canonical Forms, 17, 3 ] 19. .;P |-c Rf(rt) : [ Inversion of (R-t), 5, 11 ] 20. G(ri) = [ Inversion of (brz-t), 10 ] 21. .;P |- R(ri) : [ Inversion of (R-t), 4, 11 ] 22. . |- R_val(ri) = Ez'?Ef':Et' and R_col(ri) = B [ Canonical Forms, 21, 3 ] 23. .;P |-c Rf(ri) : [ Inversion of (R-t), 5, 11 ] 24. . |- l = Ela [ Inversion of (h-append-t), 6 25. . |- Ez = Ez' [ Inversion of (brz-t), 10 ] 25. |- S' [ Preservation, (Inversion of sim-S, a1), (Inversion of trans-eval-brz, a2) ] subcase on c SUBCASE BRZ-UNTAKEN.R: c = R 25r. Rf(ri) = R(ri) [ Inspection of (sim-val), 9, 22, c=R ] 26r. Rf[ri -> R Rf_val(ri)] sim_c R[ri -> R R_val(ri)] [ (sim-R), 9, (sim-val), 25r ] 27r. Rf(rz) = R(rz) [ Inspection of (sim-val), 9, 14, c=R ] 28r. Rf_val(rz) =/= 0 [ 27r, p1 ] 29r. Sf -->_0 (C, (h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1)) [ (brz-untaken), 28r, p2 ] 30r. |-R (C, (h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1)) [ Lemma Preservation-Brz-Possible-Elevation, 10, f=R ] 31r. (C, (h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1)) sim_R S' [ (sim-S), 26r, 30r, 25 ] 32r. Sf -->^(l+1) Sf' and Sf' sim_R S' [ 29r, 31r ] * BRZ-UNTAKEN.A complete SUBCASE BRZ-UNTAKEN.B: c = B 25b. Rf(rz) = R(rz) [ Inspection of (sim-val), 9, 14, c=B ] 26b. Rf_val(rz) =/= 0 [ 26b, p1 ] 27b. Sf -->_0 (C, (h,l,l+1), R[ri -> R R_val(ri)], C(l+1)) [ (brz-untaken), 26b, p2 ] subsubcase on Rf_val(ri) ?= R_val(ri) subsubcase B1: . |- Rf_val(ri) = R_val(ri) - blue fault does not affect intention value and simulation continues 28b1. Rf[ri -> R Rf_val(ri)] sim_B R[ri -> R R_val(ri)] [ (sim-R), 9, (sim-val), subsubcase assumption ] 29b1. . |- Ez'?Ef':Et' = Ef' [ Exp Conditional Lemma, (Exp Eq Transitivity, 15, 25) ] 30b1. . |- Rf_val(ri) = Ef' [ Exp Eq Transitivity, 22, 29b1, subcase assumption ] 31b1. |-B (C, (h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1)) [ Lemma Preservation-Brz-Possible-Elevation, 10, f=B, 26b, 30b1 ] 32b1. (C, (h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1)) sim_B S' [ (sim-S), 28b1, 31b1, 25 ] 32a. Sf -->^(l+1) Sf' and Sf' sim_B S' [ 27b, 32b1 ] * BRZ-UNTAKEN.B1 complete subsubcase B2: . |- Rf_val(ri) =/= R_val(ri) - blue fault does affect intention value and faulty version recovers 28b2. . |- Ez'?Ef':Et' = Ef' [ Exp Conditional Lemma, (Exp Eq Transitivity, 15, 25) ] 29b2. . |- Rf_val(ri) =/= Ef' [ Exp Eq Transitivity, 22, 28b2, subcase assumption ] 30b2. |-cf (C, (h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1)) [ Lemma Preservation-Brz-Possible-Elevation, 10, f=B, 27b, 29b2 ] 31b2. Sf' -->* recover(h,l,l+1) [ CF Lemma, 30b2 ] 32b2. Sf -->^(l+1) Sf' and Sf' -->* recover(h,l,l+1) [ 27b, 31b2 ] * BRZ-UNTAKEN.B2 complete SUBCASE BRZ-UNTAKEN.G: c = G 25g. Rf(ri) = R(ri) 26g. Rf[ri -> R Rf_val(ri)] sim_G R[ri -> R R_val(ri)] [ (sim-R), 9, (sim-val), 25g ] subsubcase on Rf_val(rz) =?= 0 and then Rf_val(rt) =?= Ela + 1 and then Rf_val(rt) in Dom(C) subsubcase G1: Rf_val(rz) =/= 0: rz faults to another non-zero value, fallthru proceeds 27g1. Sf -->_0 (C, (h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1)) [ (brz-untaken), subcase assumption, p2 ] 28g1. |-G (C, (h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1)) [ Lemma Preservation-Brz-Possible-Elevation, 10, f=G, 27g1, subcase assumption, 15 ] 29g1. (C, (h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1)) sim_G S' [ (sim-S), 29g1, 25, 26g ] 30g1. Sf -->^(l+1) Sf' and Sf' sim_c S' [ 27g1, 29g1 ] * BRZ-UNTAKEN.G1 complete subsubcase G2: Rf_val(rz) = 0 and . |- Rf_val(rt) = Ela + 1 : faulty computation incorrectly branches, but target is same as fallthrough, so everything a-ok 27g2. . |- R_val(rt) = l + 1 [ subcase assumption, 24 ] 28g2. Sf -->_0 (C,(h,l,R_val(rt)), Rf[ri -> R Rf_val(ri)], C(R_val(rt)))[ (brz-taken), subcase assumption, p2 ] 29g2. |-G (C,(h,l,R_val(rt)),Rf[ri -> R Rf_val(ri)], C(R_val(rt))) [ Lemma Preservation-Brz-Possible-Elevation, 10, f=G, 28g2, subcase assumptions, 15 ] 30g2. (C,(h,l,R_val(rt)),Rf[ri -> R Rf_val(ri)],C(R_val(rt))) sim_G S' [ (sim-S), 29g2, 25, 26g, 27g2 ] 31g2. Sf -->^(l+1) Sf' and Sf' sim_c S' [ 28g2, 31g2 ] * BRZ-UNTAKEN.G2 complete subsubcase G3: Rf_val(rz) = 0 and . |- Rf_val(rt) =/= Ela + 1 and . |- Rf_val(rt) in Dom(C) : faulty computations incorrectly branches somewhere else in C 27g3. Sf -->_0 (C,(h,l,R_val(rt)), Rf[ri -> R Rf_val(ri)], C(R_val(rt)))[ (brz-taken), subcase assumptions ] 28g3. |-cf (C,(h,l,R_val(rt)),Rf[ri -> R Rf_val(ri)], C(R_val(rt))) [ Lemma Preservation-Brz-Possible-Elevation, 10, f=G, 27g3, subcase assumptions, 15 ] 29g3. Sf' -->* recover(h,l,R_val(rt)) [ CF Lemma, 28g3 ] 30g3. Sf -->^(l+1) Sf' and Sf' -->* recover(h,l,R_val(rt)) [ 27g3, 29g3 ] * BRZ-UNTAKEN.G3 complete subsubcase G4: Rf_val(rz) = 0 and . |- Rf_val(rt) =/= Ela + 1 and . |- Rf_val(rt) not in Dom(C) : faulty computations incorrectly branches and craps out 27g4. Sf -->_0 hw-error(h,l) [ (brz-hw-error), subcase assumptions ] * BRZ-UNTAKEN.G4 complete * BRZ-UNTAKEN complete CASE BRZ-TAKEN: ~~~~~~~~~~~~~~~ R_val(rz) = 0 R_val(rt) in Dom(C) ----------------------------------------------------------------------------------------- (brz-taken) (C, (h,l), R, brz rz rt) -->_0 (C, (h,l,R_val(rt)), R[ri -> R R_val(ri)], C(R_val(rt))) a1. Sf sim_sc S a2. S -->^l' S' 1. Sf = (C,(h,l),Rf,brz rz rt) [ Lemma Sim_c-Typing, a1, Inspection of (brz-t) ] 2. S = (C,(h,l),R ,brz rz rt) 3. |- C : P 4. P |- R : G 5. P |-c Rf : G 6. |- (h,l) : seq o Ela 7. |- Ei = l 8. .;P;G;seq o ELa;Ei;P(l+1) |- brz rz rt 9. Forall r. Rf(r) sim_c R(r) [ Inversion of (sim-S), a1, Inversion of (sim-R) ] 10. |-c Sf [ Inversion of (sim-S), a1 ] 11. G(rz) = [ Inversion of (brz-t), 10 ] 12. .;P |- R(rz) : [ Inversion of (R-t), 4, 11 ] 13. . |- R_val(rz) = Ez and R_col(rz) = G [ Canonical Forms, 12, 3 ] 14. .;P |-c Rf(rz) : [ Inversion of (R-t), 5, 11 ] 15. . |- Ez = 0 [ Exp Eq Transitivity, p1, 13 ] 16. G(rt) = [ Inversion of (brz-t), 10 ] 17. .;P |- R(rt) : [ Inversion of (R-t), 4, 11 ] 18. . |- R_val(rt) = Et and R_col(rt) = G [ Canonical Forms, 17, 3 ] 19. .;P |-c Rf(rt) : [ Inversion of (R-t), 5, 11 ] 20. G(ri) = [ Inversion of (brz-t), 10 ] 21. .;P |- R(ri) : [ Inversion of (R-t), 4, 11 ] 22. . |- R_val(ri) = Ez'?Ef':Et' and R_col(ri) = B [ Canonical Forms, 21, 3 ] 23. .;P |-c Rf(ri) : [ Inversion of (R-t), 5, 11 ] 24. . |- l = Ela [ Inversion of (h-append-t), 6 25. . |- Ez = Ez' [ Inversion of (brz-t), 10 ] 25. |- S' [ Preservation, (Inversion of sim-S, a1), (Inversion of trans-eval-brz, a2) ] SUBCASE BRZ-TAKEN.R: c = R 25r. Rf(ri) = R(ri) [ Inspection of (sim-val), 9, 22, c=R ] 26r. Rf[ri -> R Rf_val(ri)] sim_c R[ri -> R R_val(ri)] [ (sim-R), 9, (sim-val), 25r ] 27r. Rf(rz) = R(rz) [ Inspection of (sim-val), 9, 14, c=R ] 28r. Rf_val(rz) = 0 [ 27r, p1 ] 29r. Rf(rt) = R(rt) [ Inspection of (sim-val), 9, 18, c = R ] 30r. Rf_val(rt) in Dom(C) [ 29r ] 31r. Sf -->_0 (C,(h,l,Rf_val(rt)),Rf[ri -> R Rf_val(ri)],C(Rf_val(rt))) [ (brz-taken), 28r, 30r ] 32r. |-R (C,(h,l,Rf_val(rt)),Rf[ri -> R Rf_val(ri)],C(Rf_val(rt))) [ Lemma Preservation-Brz-Possible-Elevation, 10, 31r, f=R ] 33r. (C,(h,l,Rf_val(rt)),Rf[ri -> R Rf_val(ri)],C(Rf_val(rt))) sim_R S' [ (sim-S), 26r, 32r, 25, 29r ] 32r. Sf -->^(l+1) Sf' and Sf' sim_R S' [ 31r, 33r ] * BRZ-TAKEN.A complete SUBCASE BRZ-UNTAKEN.B: c = B 25b. Rf(rz) = R(rz) [ Inspection of (sim-val), 9, 14, c=B ] 26b. Rf_val(rz) =/= 0 [ 26b, p1 ] 27b. Rf(rt) = R(rt) [ Inspection of (sim-val), 9, 18, c=B ] 28b. Rf_val(rt) in Dom(C) [ 27b, p1 ] 29b. Sf -->_0 (C,(h,l,Rf_val(rt)),Rf[ri -> R Rf_val(ri)],C(Rf_val(rt))) [ (brz-taken), 26b, p2 ] subsubcase on Rf_val(ri) ?= R_val(ri) subsubcase B1: . |- Rf_val(ri) = R_val(ri) - blue fault does not affect intention value and simulation continues 28b1. Rf[ri -> R Rf_val(ri)] sim_B R[ri -> R R_val(ri)] [ (sim-R), 9, (sim-val), subsubcase assumption ] 29b1. . |- Ez'?Ef':Et' = Et' [ Exp Conditional Lemma, (Exp Eq Transitivity, 15, 25) ] 30b1. . |- Rf_val(ri) = Et' [ Exp Eq Transitivity, 22, 29b1, subcase assumption ] 31b1. |-B Sf' [ Lemma Preservation-Brz-Possible-Elevation, 10, f=B, 29b, 30b1 ] 32b1. (C,(h,l,Rf_val(rt)),Rf[ri -> R Rf_val(ri)],C(Rf_val(rt)))sim_B S' [ (sim-S), 28b1, 31b1, 25, 27b ] 32a. Sf -->^(l+1) Sf' and Sf' sim_B S' [ 27b, 32b1 ] * BRZ-UNTAKEN.B1 complete subsubcase B2: . |- Rf_val(ri) =/= R_val(ri) - blue fault does affect intention value and faulty version recovers 28b2. . |- Ez'?Ef':Et' = Et' [ Exp Conditional Lemma, (Exp Eq Transitivity, 15, 25) ] 29b2. . |- Rf_val(ri) =/= Et' [ Exp Eq Transitivity, 22, 28b2, subcase assumption ] 30b2. |-cf Sf' [ Lemma Preservation-Brz-Possible-Elevation, 10, f=B, 29b, 29b2 ] 31b2. Sf' -->* recover(h,l,Rf_val(rt)) [ CF Lemma, 30b2 ] 32b2. Sf -->^(l+1) Sf' and Sf' -->* recover(h,l,R_val(rt)) [ 27b, 31b2, 27b ] * BRZ-UNTAKEN.B2 complete SUBCASE BRZ-UNTAKEN.G: c = G 25g. Rf(ri) = R(ri) 26g. Rf[ri -> R Rf_val(ri)] sim_G R[ri -> R R_val(ri)] [ (sim-R), 9, (sim-val), 25g ] subsubcase G1: Rf_val(rz) =/= 0 and . |- Et = Ela + 1 - faulty computation falls through when original branches, but it's ok because branch target is same as fallthru 26g1. . |- R_val(rt) = l + 1 [ subcase assumption, 24 ] 27g1. Sf -->_0 (C,(h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1)) [ (brz-taken), subcase assumption, p2 ] 28g1. |-G (C,(h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1))) [ Lemma Preservation-Brz-Possible-Elevation, 10, f=G, 27g1, subcase assumptions, 15 ] 29g1. (C,(h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1)) sim_G S' [ (sim-S), 29g1, 26g1, 25, 26g ] 30g1. Sf -->^(l+1) Sf' and Sf' sim_c S' [ 27g1, 29g1 ] * BRZ-TAKEN.G1 complete subsubcase G2: Rf_val(rz) =/= 0 and . |- Et =/= Ela + 1 - faulty computation falls through when original branches off elsewhere 27g2. . |- R_val(rt) = l + 1 [ subcase assumption, 24 ] 28g2. Sf -->_0 (C,(h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1)) [ (brz-untaken), subcase assumption, p2 ] 29g2. |-cf (C,(h,l,l+1), Rf[ri -> R Rf_val(ri)], C(l+1)) [ Lemma Preservation-Brz-Possible-Elevation, 10, f=G, subcase assumptions, 15 ] 30g2. Sf' -->* recover(h,l,l+1) [ CF Lemma, 29g2 ] 31g2. Sf -->^(l+1) Sf' and Sf' -->* recover(h,l,l+1) [ 28g2, 30g2 ] * BRZ-TAKEN.G2 complete subsubcase G3: Rf_val(rz) = 0 and . |- Rf_val(rt) = Et - faulty computation takes the same branch as original 26g3. . |- Rf_val(rt) = R_val(rt) [ Exp Eq Transitivity, subcase assumption, 18 ] 27g3. Sf -->_0 (C,(h,l,Rf_val(rt)),Rf[ri -> R Rf_val(ri)],C(Rf_val(rt)))[ (brz-taken), subcase assumption, (p2, 26g3) ] 28g3. |-G Sf' [ Lemma Preservation-Brz-Possible-Elevation, 10, f=G, subcase assumptions, 15 ] 29g3. Sf' sim_c S' [ (sim-S), 25, 29g3, 26g2, 26g ] 30g1. Sf -->^(l+1) Sf' and Sf' sim_c S' [ 27g1, 29g1 ] * BRZ-TAKEN.G3 complete subsubcase G4: Rf_val(rz) = 0 and . |- Rf_val(rt) =/= Et and Rf_val(rt) in Dom(C) - faulty computation branches off elsewhere in C 26g4. Sf -->_0 (C,(h,l,Rf_val(rt)),Rf[ri -> R Rf_val(ri)],C(Rf_val(rt)))[ (brz-taken), subcase assumptions ] 27g4. |-cf Sf' [ Lemma Preservation-Brz-Possible-Elevation, 10, f=G, subcase assumptions, 15 ] 28g4. Sf' -->* recover(h,l,Rf_val(rt)) [ CF Lemma, 27g4 ] 29g4. Sf -->^(Rf_val(rt)) Sf' and Sf' -->* recover(h,l,Rf_val(rt)) [ 26g4, 28g4 ] * BRZ-TAKEN.G4 complete subsubcase G5: Rf_val(rz) = 0 and . |- Rf_val(rt) =/= Et and Rf_val(rt) not in Dom(C) - faulty computation craps out 26g5. Sf -->_0 hw-error(Rf_val(rt)) [ (brz-hw-error), subcase assumptions ] * BRZ-TAKEN.G5 complete CASE JMP: ~~~~~~~~~ R_val(rt) in Dom(C) ------------------------------------------------------------------------------ (jmp) (C, h, R, jmp rt) -->_0 (C, (h,R_val(rt)), R[ri -> R R_val(ri)], C(R_val(rt))) Similar to BRZ cases