Preservation 1. If |- S and S -->_0 S' then |- S' 2. If |-f S and S -->_0 S' then Exists Z'. |-Z' S' and Z' >= f 3. If |- S and S -->_1 S' then Exists c. |-c S' Corollary: Preservation-Fault-Elevation If |-Z S and S -->_k S' then Exists Z'. |-Z' S' and Z' >= Z =========================================================================================================== =========================================================================================================== ************************************ * Lemma Preservation-No-Elevation: * ************************************ If |-Z (C,h,R,b) and b =/= brz and b =/= jmp and (C,h,R,b) --> S' then |-Z S' PROOF: By case analysis of S -->_0 S' ****** CASE MOVI: ~~~~~~~~~~ ----------------------------------------------------------- (movi) (C, (h,l), R, movi rd v; b) -->_0 (C, (h,l), R[rd -> v], b) a1. |-Z (C, h, R, movi rd v; b) 1. |- C : P 2. P |-Z R : G 3. |- (h,l) : A 4x. Z = cf ? . |- Ei =/= l : |- Ei = l 4y. G(ri) =/= ==> . |- Ei = l 5. .;P;G;A;Ei;to |- movi rd v; b 6. .;P;G; |- movi rd (c i) : G[ rd <- ] [ Inversion of (seqence-t), 5, Inspection of (movi-t) ] 5'. .;P;G[rd->];A;Ei;t |- b [ Inversion of (sequence-t), 5, 6 ] 7. P |- i : int [ (int-t) ] 8. . |- i = i [ (E-eq) ] 9. .;P |- c i : [ (val-t), 7, 8 ] 10. .;P |-Z c i : [ Color Weakening Lemma, 9 ] 11. Forall r'. .;P |-Z R(r') : G(r') [ Inversion of (R-t), 2 ] 2'. P |- R[rd -> c i] : G[rd ->] [ (R-t), 11, 10 ] 12. rd =/= ri [ Inversion of (movi-t), 6 ] 4y'. G[rd ->](ri) =/= ==> . |- Ei = l [ 12, 4y ] 12. |-Z (C, (h,l), R[rd -> v], b) [ (S-t), 1, 2', 3, 4x, 4y', 5' ] * MOVI complete CASE SUB: ~~~~~~~~~ v' = R_col(rs1) (R_val(rs1) - R_val(rs2)) --------------------------------------------------------------------- (sub) (C, (h,l), R, sub rd, rs1, rs2; b) -->_0 (C,(h,l), R[ rd -> v' ], b) a1. |-Z (C, (h,l), R, sub rd, rs1, rs2; b) 1. |- C : P 2. P |-Z R : G 3. |- (h,l) : A 4x. Z = cf ? . |- Ei =/= l : |- Ei = l 4y. G(ri) =/= ==> . |- Ei = l 5. .;P;G;A;Ei;to |- sub rd, rs1, rs2; b 6. .;P;G |- sub rd, rs1, rs2 : G[ rd <- ] [ Inversion of (seqence-t), 5, Inspection of (sub-t) ] 5'. .;P;G[rd<-];A;Ei;t |- b [ Inversion of (sequence-t), 5, 6 ] 7. G(rs1) = [ Inversion of (sub-t), 6 ] 8. G(rs2) = 9. .;P |-Z R(rs1) : [ Inversion of (R-t), 2, 7 ] 10. .;P |-Z R(rs2) : [ Inversion of (R-t), 2, 8 ] subcase Z =/= c and (Z =/= cf or c =/= B and c =/= G) 11a. R_col(rs1) = c and . |- Es1 = R_val(rs1) [ Canonical Forms, 9, 1 ] 12a. R_col(rs2) = c and . |- Es2 = R_val(rs2) [ Canonical Forms, 10, 1 ] 13a. [[Es1]] = R_val(rs1) and [[Es2]] = R_val(rs2) [ Inversion of (E-eq), 11a, 12a ] 14a. [[Es1]] - [[Es2]] = R_val(rs1) - R_val(rs2) [ 13a ] 15a. [[Es1-Es2]] = R_val(rs1) - R_val(rs2) [ def of [[E]], 14a ] 16a. . |- Es1-Es2 = R_val(rs1) - R_val(rs2) [ (E-eq), 15a ] 17a. P |- R_val(rs1) - R_val(rs2) : int [ (int-t) ] 18a. .;P |-Z R_col(rs) (R_val(rs1) - R_val(rs2)) : [ (val-t), 11a, 16a, 17a ] subcase Z = c 11b. R_col(rs1) = c and . |- Es1 : kint [ Canonical Forms, 9, 1 ] 12b. R_col(rs2) = c and . |- Es2 : kint [ Canonical Forms, 10, 1 ] 13b. . |- (Es1-Es2) : kint [ (wf-sub), 12b ] 14b. .;P |-c R_col(rs1) (R_val(rs1) - R_val(rs2)) : [ (val-zap-c-t), 13b, 11b ] subcase Z = cf and (c = B or c = G) 11c. . |- Es1 : kint [ Canonical Forms, 9, 1 ] 12c. . |- Es2 : kint [ Canonical Forms, 10, 1 ] 13c. . |- (Es1-Es2) : kint [ (wf-sub), 11c, 12c ] 14c. .;P |-cf R_col(rs) (R_val(rs1) - R_val(rs2)) : [ (val-zap-cf-t), 12c ] merge: 19. .;P |-Z R_col(rs) (R_val(rs1) - R_val(rs2)) : [ 18a, 14b, 14c ] 2'. P |-Z R[ rd -> v' ]: G[ rd <- ] [ (R-t), (Inversion of (R-t), 2), (19, p1) ] 20. rd =/= ri [ Inversion of (sub-t), 6 ] 4y'. G[rd ->](ri) =/= ==> . |- Ei = l [ 12, 4y ] 21. |-Z (C, (h,l), R[ rd -> v' ], b) [ (S-t), 1, 2', 3, 4x, 4y', 5' ] * SUB complete CASE INTEND: ~~~~~~~~~~~~ ---------------------------------------------------------------- (intend) (C, (h,l), R, intend rt; b) -->_0 (C, (h,l), R[ri -> R(rt)], b) a1. |-Z (C, (h,l), R, intend ri rt; b) 1. |- C : P 2. P |-Z R : G 3. |- (h,l) : A 4x. Z = cf ? . |- Ei =/= l : |- Ei = l 4y. G(ri) =/= ==> . |- Ei = l 5. .;P;G;A;Ei;to |- intend ri rt; b 6. .;P;G |- intend ri rt : G[ri -> [ Inversion of (sequence-t), 5, Inspection of (intend-t) ] 5'. .;P;G[ ri <- ];A;Ei;t |- b [ Inversion of (sequence-t), 5, 6 ] 7. G(rt) = [ Inversion of (intend-t), 6 ] 8. .;P |-Z R(rt) : [ Inversion of (R-t), 2, 7 ] subcase Z = cf 10a. . |- Et : kint [ Canonical Forms, (9, subcase assumption), 1 ] 11a. .;P |-cf R(rt) : [ (val-t), 10a, 11a ] subcase Z = B 10b. . |- Et : kint and R_col(rt) = B [ Canonical Forms, (9, subcase assumption), 1 ] 11b. .;P |-B R(rt) : [ (val-zap-c-t), 10b ] subcase Z =/= B and Z =/= cf 10c. . |- R_val(rt) = Et and R_col(rt) = B [ Canonical Forms, (9, subcase assumption), 1 ] 11c. P |- R_val(rt) : int [ (int-t) ] 12c. .;P |-G R(rt) : [ (val-t), 10c, 11c ] merge 13. .;P |-Z R(rt) : [ 11a, 11b, 12c ] 14. Forall r'. .;P |-Z R(r') : G(r') [ Inversion of (R-t), 2 ] 2'. P |-Z R[ri -> R(rt)] : G[ri -> ] [ (R-t), 14, 13 ] 15. G(ri) = [ Inversion of (intend-t), 6 ] 4y'. . |- Ei = l [ 4y, 15 ] 16. |-Z (C, (h,l), R[ri -> R(rt)], b) [ (S-t), 1, 2', 3, 4x, 4y', 5' ] * INTEND complete CASE INTENDZ-SET: ~~~~~~~~~~~~~~~~~ R_val(rz) = 0 --------------------------------------------------------------------- (intendz-set) (C, (h,l), R, intendz rz rt; b) -->_0 (C, (h,l), R[ri -> R(rt)], b) a1. |-Z (C, (h,l), R, intendz rz rt; b) 1. |- C : P 2. P |-Z R : G 3. |- (h,l) : A 4x. Z = cf ? . |- Ei =/= l : |- Ei = l 4y. G(ri) =/= ==> . |- Ei = l 5. .;P;G;A;Ei;to |- intendz rz ri rt; b 6. .;P;G |- intendz rz ri rt : G'[ri <- ] [ Inversion of (sequence-t), 5, Inspection of (intendz-t) ] 5'. .; P; G[ri -> ]; seq~>Ez?:Et; A |- b [ Inversion of (sequence-t), 5, 6 ] 7. G(rt) = [ Inversion of (intendz-t), 6 ] 8. G(rz) = 9. G(ri) = 11. .;P |-Z R(rt) : [ Inversion of (R-t), 2, 7 ] 12. .;P |-Z R(rz) : [ Inversion of (R-t), 2, 8 ] 13. .;P |-Z R(ri) : [ Inversion of (R-t), 2, 9 ] 4y'. . |- Ei = l [ 4y, 9 ] subcase Z =/= B and Z =/= cf 14a. . |- R_val(rz) = Ez [ Canonical Forms, 12, subcase assumption, 1 ] 15a. . |- Ez = 0 [ Exp Eq Transitivity Lemma, p1, 14a ] 16a. . |- Ez?Ei:Et = Et [ Exp Conditional Lemma, 15a ] 17a. R_col(rt) = B and . |- R_val(rt) = Et [ Canonical Forms, 11, subcase assumption, 1 ] 18a. . |- R_val(rt) = Ez?Ei:Et [ Exp Eq Transitivity, 16a, 17a ] 19a. P |- R_val(rt) : go [ (rit-t) ] 20a. .;P |-Z R(rt) : [ (val-t), 17a, 18a, 19a ] subcase Z = B 14b. R_col(rt) = B and . |- Et : kint [ Canonical Forms, 11, subcase assumption, 1 ] 15b. . |- Ez : kint [ Canonical Forms, 10, 1 ] 16b. . |- Ei : kint [ Canonical Forms, 11, 1 ] 17b. . |- Ez?Ei:Et : kint [ (wf-ifexp, 14b, 15b, 16b ] 18b. .;P |-B R(rt) : [ (val-zap-c-t), 14b, 17b ] subcase Z = cf 14c. . |- Ei =/= l [ 4x, Z=cf ] 15c. contradiction -- subcase does not apply [ 4y', 15c ] merge 21. .;P |-Z R(rt) : [ 20a, 18b, 15c ] 2'. P |-Z R[ri -> R(rt)] : G[ri -> ] [ (R-t), (Inversion of (R-t), 2), 27 ] 22. |-Z (C, (h,l), R[ri -> R(rt)], b) [ (S-t), 1, 2', 3, 4x, 4y', 5' ] * INTENDZ-SET complete CASE INTENDZ-UNSET: ~~~~~~~~~~~~~~~~~~~ R_val(rz) =/= 0 ------------------------------------------------- (intendz-unset) (C, (h,l), R, intendz rz rt; b) -->_0 (C, (h,l), R, b) a1. |-Z (C, (h,l), R, intendz rz rt; b) 1. |- C : P 2. P |-Z R : G 3. |- (h,l) : A 4x. Z = cf ? . |- Ei =/= l : |- Ei = l 4y. G(ri) =/= ==> . |- Ei = l 5. .;P;G;A;Ei;to |- intendz rz ri rt; b 6. .;P;G |- intendz rz ri rt : G'[ri <- ] [ Inversion of (sequence-t), 5, Inspection of (intendz-t) ] 5'. .; P; G[ri -> ]; seq~>Ez?:Et; A |- b [ Inversion of (sequence-t), 5, 6 ] 7. G(rt) = [ Inversion of (intendz-t), 6 ] 8. G(rz) = 9. G(ri) = 11. .;P |-Z R(rt) : [ Inversion of (R-t), 2, 7 ] 12. .;P |-Z R(rz) : [ Inversion of (R-t), 2, 8 ] 13. .;P |-Z R(ri) : [ Inversion of (R-t), 2, 9 ] 4y'. . |- Ei = l [ 4y, 9 ] subcase Z =/= B and Z =/= cf 14a. . |- R_val(rz) = Ez [ Canonical Forms, 12, subcase assumption, 1 ] 15a. . |- Ez =/0 0 [ Exp Eq Transitivity Lemma, p1, 14a ] 16a. . |- Ez?Ei:Et = Ei [ Exp Conditional Lemma, 15a ] 17a. R_col(ri) = B and . |- R_val(ri) = Ei [ Canonical Forms, 13, subcase assumption, 1 ] 18a. . |- R_val(rt) = Ez?Ei:Et [ Exp Eq Transitivity, 16a, 17a ] 19a. P |- R_val(rt) : goz [ (rit-t) ] 20a. .;P |-Z R(rt) : [ (val-t), 17a, 18a, 19a ] subcase Z = B 14b. R_col(ri) = B and . |- Ei:kint [ Canonical Forms, 13, subcase assumption, 1 ] 15b. . |- Ez : kint [ Canonical Forms, 12, 1 ] 16b. . |- Et : kint [ Canonical Forms, 11, 1 ] 17b. . |- Ez?Ei:Et : kint [ (wf-ifexp, 14b, 15b, 16b ] 18b. .;P |-B R(ri) : [ (val-zap-c-t), 14b, 17b ] subcase Z = cf 14c. . |- Ei =/= l [ 4x, Z=cf ] 15c. contradiction -- subcase does not apply [ 4y', 15c ] merge 24. .;P |-Z R(ri) : [ 23a, 18b, 15c ] 2'. P |-Z R : G[ri -> ] [ (R-t), (Inversion of (R-t), 2), 24 ] 15. |-Z (C, (h,l), R, b) [ (S-t), 1, 2', 3, 4x, 4y', 5' ] * INTENDZ-UNSET complete CASE RECOVERNZ-OK: ~~~~~~~~~~~~~~~~~~ R_val(rz) = 0 ----------------------------------------------------- (recovernz-ok) (C, (h,l), R, recovernz rz; b) -->_0 (C, (h,l), R, b) a1. |-Z (C, (h,l), R, recovernz rz; b) 1. |- C : P 2. P |-Z R : G 3. |- (h,l) : A 4x. Z = cf ? . |- Ei =/= l : . |- Ei = l 4y. G(ri) =/= ==> . |- Ei = l 5. .;P;G;A;Ei;to |- recovernz rz; b subcase on the structure of 5 - (recovernz-t) does not apply as D is empty SUBCASE RECOVERNZ-OK.A: using (recovernz-eq-t) G(rz) = G(ri) = . |- Ez = Eli - Ela . |- Eli = Ela .; P; G[ri -> ]; seq o Ela; Eli; to |- b ------------------------------------------------- (recovernz-eq-t) .; P; G; seq o Ela; Eli; to |- recovernz rz ; b 6a. .;P |-Z R_val(ri) : [ Inversion of (R-t), 2, pa2 ] 7a. .;P |-Z R_val(ri) : [ (val-t), Inversion/Reconstruction of val-t rules, using (rit-t) for (val-t) case ] 2'. P |-Z R : G[ri -> ] [ (R-t), 2, 7a ] 5'. .; P; G[ri -> ]; seq o Ela; Eli |- b [ pa5 ] 8a. . |- Ela = l [ Inversion of (h-append-t), 3 ] 4y'. . |- Eli = l [ Exp Eq Transitivity, p4, 8a ] 8a. |-Z (C, (h,l), R, b) [ (S-t), 1, 2', 3, 4x, 4y', 5' ] * RECOVERNZ-OK.A complete SUBCASE B: using (recovernz-neq-t) G(rz) = G(ri) = . |- Ez = Eli - Ela . |- Eli =/= Ela ------------------------------------------------- (recovernz-neq-t) .; P; G; seq o Ela; Eli; to |- recovernz rz; b subsubcase B1: Z =/= R 6b1. . |- R_val(rz) = Ez [ Canonical Forms, (Inversion of (R-t), 2, pb1), 1 ] 7b1. . |- Ez = 0 [ Exp Eq Transitivity, 6b1, p1 ] 8b1. . |- Eli = Ela [ pb3, 7b1 ] 9b1. 8b1 contradicts p4. subsubcase doesn't apply subsubcase B2: Z = R 6b2. . |- Ela = l [ Inversion of (h-append-t), 3 ] 7b2. . |- Eli = l [ 4x, subcase assumption ] 8b2. . |- Eli = Ela [ Exp Eq Transitivity, 7b2, 8b2 ] 9b2. 8b2 contradicts p4. subsubcase doesn't apply * RECOVERNZ-OK.B complete CASE RECOVERNZ-HALT: ~~~~~~~~~~~~~~~~~~~~ R_val(rz) =/= 0 ---------------------------------------------- (recovernz-halt) (C, h, R, recovernz rz; b) -->_0 recover recover(h) =/= S' case does not apply * RECOVERNZ-HALT complete CASES BRZ-UNTAKEN, BRZ-TAKEN, BRZ-HW-ERROR: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Do not apply (i = brz) CASES JMP, JMP-HW-ERROR: ~~~~~~~~~~~~~~~~~~~~~~~~ Do not apply (i = jmp). ** LEMMA PRESERVATION-NO-ELEVATION complete =========================================================================================================== =========================================================================================================== ************************************** * LEMMA PRESERVATION-JMP-BRZ-EMPTY-Z * ************************************** If |- S and and b = brz or b = jmp and S -->_0 S' then |- S' PROOF: By case analysis of S -->_0 S' ****** CASES MOVI, SUB, INTEND, INTENDZ-SET, INTENDZ-UNSET, RECOVERNZ-OK, RECOVERNZ-HALT: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ a1. |- S a2. S -->_0 S' 1. i =/= jmp or brz [ inspection of rules ] * CASES MOVI, SUB, INTEND, INTENDZ-SET, INTENDZ-UNSET, RECOVERNZ-OK, RECOVERNZ-HALT complete 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. |- (C, (h,l), R, brz rz rt) 1. |- C : P 2. P |- R : G 3. |- (h,l) : A 4x. . |- Ei = l 4y. G(ri) =/= ==> . |- Ei = l 5. .;P;G;A;Ei;P(l+1) |- brz rz rt 6. .;P;G;seq o Ela; Ei; All[Df](Gf,Af) |- brz rz rt [ Inspection of (brz-t), 5 ] 7. G(ri)= [ Inversion of (brz-t), 6 ] 8. . |- Ef' = Ela + 1 9. G(rz) = 10. . |- Ez = Ez' 11. Exists Sf. . |- Sf : Df 12. . |- G[ri -> ] <= Sf(Gf) 13. . |- seq o Ela o Ef' = Sf(Af) 14. Forall r'. .;P |- R(r') : G(r') [ Inversion of (R-t), 2 ] 15. .;P |- R(ri) : [ 14, 7 ] 16. . |- R_val(ri) = Ez'?Ef':Et' [ Inversion of (val-t), 15 ] 17. P |- R_val(ri) : check [ (rit-t) ] 18. .;P |- R(rz) : [ 14, 9 ] 19. . |- R_val(rz) = Ez [ Inversion of (val-t), 18 ] 20. . |- Ez' =/= 0 [ Exp Eq Transitivity, 19, p1, 10 ] 21. . |- Ez'?Ef':Et' = Ef' [ Exp Conditional Lemma, 20 ] 22. . |- R_val(ri) = Ef' [ Exp Eq Transitivity, 16, 21 ] 23. .;P |- R R_val(ri) : [ (val-t), 17, 22 ] 24. P |- R[ri -> R R_val(ri)] : G[ri -> ] [ (R-t), 14, 23 ] 2'. P |- R[ri -> R R_val(ri)] : Sf(Gf) [ Repeated applications of Subtyping Lemma, 12, 24 ] 25. . |- l = Ela [ Inversion of (h-append), 3, 6 ] 26. . |- Ef' = l + 1 [ Exp Eq Transitivity, 8, 25 ] 27. . |- (h,l,l+1) : seq o Ela o Ef' [ (h-append), 3, 26 ] 3'. . |- (h,l,l+1) : Sf(Af) [ Exp Eq Transitivity, 27, 12 ] 28. P(l+1) = All[Df](Gf,Af) [ Inspection of 5, 6 ] 29. Df = (Df', Y:kint, alpha:kseq) and Af = alpha o (l+1) [ Inversion of (C-t), 1, p2, 28 ] 30. Gf(ri) = 31. Df; P; Gf; Af; Y; P(l+2) |- C(l+1) 5'. .; P; Sf(Gf); Sf(Af); Sf(Y); Sf(P(l+2)) |- C(l+1) [ Substitution Lemma, 11, 31 ] 32. . |- <= Sf() [ 12, 30 ] 33. . |- Ef' = Sf(Y) [ Inversion of (subtp-reflex), 32 ] 4'. . |- Sf(Y) = l+1 [ Exp Eq Transitivity, 26, 33 ] 34: |- (C, (h,l,l+1), R[ri -> R R_val(ri)], C(l+1)) [ (S-t), 1, 2', 3', 4', 4', 5' ] * 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. |- (C, (h,l), R, brz rz rt) 1. |- C : P 2. P |- R : G 3. |- (h,l) : A 4x. |- Ei = l 4y. G(ri) =/= ==> . |- Ei = l 5. .;P;G;A;Ei;P(l+1) |- brz rz rt 6. .;P;G;seq o Ela; Ei; All[Df](Gf,Af) |- brz rz rt [ Inspection of (brz-t), 5 ] 7. G(ri)= [ Inversion of (brz-t), 6 ] 8. G(rz) = 9. . |- Ez = Ez' 10. G(rt) = 11. . |- Et = Et' 12. Exists St. D |- St : Dt 13. . |- G[ri -> ] <= St(Gt) 14. . |- seq o Ela o Et' = St(At) 15. Forall r'. .;P |- R(r') : G(r') [ Inversion of (R-t), 2 ] 16. .;P |- R(ri) : [ 15, 7 ] 17. . |- R_val(ri) = Ez'?Ef':Et' [ Inversion of (val-t), 16 ] 18. P |- R_val(ri) : check [ (rit-t) ] 19. .;P |- R(rz) : [ 15, 8 ] 20. . |- R_val(rz) = Ez [ Inversion of (val-t), 19 ] 21. . |- Ez' = 0 [ Exp Eq Transitivity, 20, p1, 9 ] 22. . |- Ez'?Ef':Et' = Et' [ Exp Conditional Lemma, 21 ] 23. . |- R_val(ri) = Et' [ Exp Eq Transitivity, 17, 22 ] 24. .;P |- R R_val(ri) : [ (val-t), 18, 23 ] 25. P |- R[ri -> R R_val(ri)] : G[ri -> ] [ (R-t), 15, 24 ] 2'. P |- R[ri -> R R_val(ri)] : St(Gt) [ Repeated applications of Subtyping Lemma, 13, 24 ] 26. .;P |- rt : [ 15, 10 ] 27. . |- R_val(rt) = Et [ Inversion of (val-t), 26 ] 28. . |- (h,l,R_val(rt)) : seq o Ela o Et' [ (h-append), 3, 27 ] 3'. . |- (h,l,R_val(rt)) : St(At) [ Exp Eq Transitivity, 28, 14 ] 29. Dt = (Dt', Y:kint, alpha:kseq) and At = alpha o R_val(rt) [ Inversion of (C-t), 1, p2, (Inversion of (val-t), 26) ] 30. Gt(ri) = 31. Dt; P; Gt; At; Y; P(R_val(rt)+1) |- C(R_val(rt)) 5'. .;P;St(Gt); St(At); St(Y); St(R_val(rt)+1) |- C(R_val(rt)) [ Substitution Lemma, 31, 12 ] 32. . |- <= St() [ 13, 30 ] 33. . |- Et' = St(Y) [ Inversion of (subtp-reflex), 32 ] 4'. . |- St(Y) = R_val(rt) [ Exp Eq Transitivity, 33, 27, 11 ] 34: |- (C,(h,l,R_val(rt)),R[ri -> R R_val(ri)],C(R_val(rt))) [ (S-t), 1, 2', 3', 4', 4', 5' ] * BRZ-TAKEN complete CASE JMP: ~~~~~~~~~ R_val(r) in Dom(C) -------------------------------------------------------------------------------- (jmp) (C, h, R, jmp rt) -->_0 (C, (h,l,R_val(rt)), R[ri -> R R_val(ri)], C(R_val(rt))) a1. |- (C, (h,l), R, jmp rt) 1. |- C : P 2. P |- R : G 3. |- (h,l) : A 4x. . |- Ei = l 4y. G(ri) =/= ==> . |- Ei = l 5. .;P;G;A;Ei;P(l+1) |- jmp rt 6. .; P; G; seq o Ela; Ei; t |- jmp rt [ Inspection of (jmp-t), 5 ] 7. G(ri)= [ Inversion of (jmp-t), 6 ] 8. G(rt) = 9. . |- Et = Et' 10. Exists S. D |- St : Dt 11. . |- G[ri -> ] <= St(Gt) 12. . |- seq o Ela o Et = St(At) 13. Forall r'. .;P |- R(r') : G(r') [ Inversion of (R-t), 2 ] 14. .;P |- R(ri) : [ 13, 7 ] 15. . |- R_val(ri) = Et' [ Inversion of (val-t), 14 ] 16. P |- R_val(ri) : check [ (rit-t) ] 17. .;P |- R R_val(ri) : [ (val-t), 15, 16 ] 18. P |- R[ri -> R R_val(ri)] : G[ri -> ] [ (R-t), 13, 17 ] 2'. P |- R[ri -> R R_val(ri)] : St(Gt) [ Repeated applications of Subtyping Lemma, 11, 18 ] 19. .;P |- rt : [ 13, 8 ] 20. . |- R_val(rt) = Et [ Inversion of (val-t), 19 ] 21. . |- (h,l,R_val(rt)) : seq o Ela o Et' [ (h-append), 3, 20 ] 3'. . |- (h,l,R_val(rt)) : St(At) [ Exp Eq Transitivity, 21, 12 ] 22. Dt = (Dt', Y:kint, alpha:kseq) and At = alpha o R_val(rt) [ Inversion of (C-t), 1, p1, (Inversion of (val-t), 19) ] 23. Gt(ri) = 24. Dt; P; Gt; At; Y; P(R_val(rt)+1) |- C(R_val(rt)) 5'. .;P;St(Gt); St(At); St(Y); St(R_val(rt)+1) |- C(R_val(rt)) [ Substitution Lemma, 24, 10 ] 25. . |- <= St() [ 11, 23 ] 26. . |- Et' = St(Y) [ Inversion of (subtp-reflex), 25 ] 4'. . |- St(Y) = R_val(rt) [ Exp Eq Transitivity, 26, 9, 20 ] 34: |- (C, (h,l,R_val(rt)), R[ri -> R R_val(ri)], C(R_val(rt))) [ (S-t), 1, 2', 3', 4', 4', 5' ] * JMP complete CASES BRZ-HW-ERROR, JMP-HW-ERROR: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ R_val(rz) = 0 R_val(rz) not in Dom(C) ------------------------------------------------------------ (brz-hw-error) (C, h, R, brz rz rd) -->_0 hw-error R_val(r) not in Dom(C) ---------------------------------------------------------------- (jmp-hw-error) (C, h, R, jmp r) -->_0 hw-error (C,h,R,b) --/-->_0 S cases do not apply * BRZ-HW-ERROR, JMP-HW-ERROR complete. ** PRESERVATION-JMP-BRZ-EMPTY-Z COMPLETE =========================================================================================================== =========================================================================================================== ********************************************* * LEMMA PRESERVATION-BRZ-POSSIBLE-ELEVATION * ********************************************* If |-f (C, (h,l), R, brz rz rt) and G is regfile type used and G(rz) = and G(ri) = and G(rt) = and |- h : seq o Ela and (C,(h,l),R,brz rz rt) -->_0 S' then (1) f = R ==> |-R S' (2) f =/= cf (3) f = G and (a) R_val(rz) =/= 0 and . |- Ez =/= 0 ==> |-G S' // correct fallthru (rz correct) (b) R_val(rz) =/= 0 and . |- Et = Ela + 1 ==> |-G S' // correct fallthru (branch/fallthru targets are equal) (a) R_val(rz) =/= 0 and . |- Ez = 0 and . |- Et =/= Ela + 1 ==> |-cf S' // incorrect fallthru (that doesn't accidentally work out) (c) R_val(rz) = 0 and . |- Ez = 0 and . |- R_val(rt) = Et ==> |-G S' // correct branch (c) R_val(rz) = 0 and . |- Ez = 0 and . |- R_val(rt) =/= Et ==> |-cf S' // incorrect branch (rt corrupt) (d) R_val(rz) = 0 and . |- Ez =/= 0 and . |- R_val(rt) = Ela + 1 ==> |-G S' // correct branch (two wrongs make a right) (b) R_val(rz) = 0 and . |- Ez =/= 0 and . |- R_val(rt) =/= Ela + 1 ==> |-cf S' // incorrect branch (rz corrupt, doesn't accidentally work out) (5) f = B and (a) R_val(rz) =/= 0 and . |- R_val(ri) = Ef' ==> |-B S' // correct fallthru (b) R_val(rz) =/= 0 and . |- R_val(ri) =/= Ef' ==> |-cf S' // incorrect faullthru (c) R_val(rz) = 0 and . |- R_val(ri) = Et' ==> |-B S' // correct branch (d) R_val(rz) = 0 and . |- R_val(ri) =/= Et' ==> |-cf S' // incorrect branch PROOF: By case analysis of S -->_0 S' ****** CASES MOVI, SUB, INTEND, INTENDZ-SET, INTENDZ-UNSET, RECOVERNZ-OK, RECOVERNZ-HALT, JMP, JMP-HW-ERROR: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ a1. |-f S a2. S -->_0 S' 1. i =/= brz [ inspection of rules ] * CASES MOVI, SUB, INTEND, INTENDZ-SET, INTENDZ-UNSET, RECOVERNZ-OK, RECOVERNZ-HALT, JMP, JMP-HW-ERROR complete 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. |-f (C, (h,l), R, brz rz rt) 1. |- C : P 2. P |-f R : G 3. |- (h,l) : A 4x. f = cf ? . |- Ei =/= l : . |- Ei = l 4y. G(ri) =/= ==> . |- Ei = l 5. .;P;G;A;Ei;P(l+1) |- brz rz rt 6. .;P;G;seq o Ela; Ei; All[Df](Gf,Af) |- brz rz rt [ Inspection of (brz-t), 5 ] 7. G(ri)= [ Inversion of (brz-t), 6 ] 8. . |- Ef' = Ela + 1 9. G(rz) = 10. . |- Ez = Ez' and . |- Et = Et' 11. Exists Sf. . |- Sf : Df 12. . |- G[ri -> ] <= Sf(Gf) 13. . |- seq o Ela o Ef' = Sf(Af) 14. Forall r'. .;P |-f R(r') : G(r') [ Inversion of (R-t), 2 ] 15. .;P |-f R(ri) : [ 15, 7 ] 16. .;P |-f R(rz) : [ 15, 9 ] 18. P(l+1) = All[Df](Gf,Af) [ Inspection of 5, 6 ] 19. Df = (Df', Y:kint, alpha:kseq) and Af = alpha o (l+1) [ Inversion of (C-t), 1, p2, 18 ] 20. Gf = Gf', ri-> 21. Df; P; Gf; Af; Y; P(l+2) |- C(l+1) 22. Df' |- Gf' ok /\ Df' |- P(l+2) ok 23. Sf = Ealpha/alpha, EY/Y, Sf'/Df' and . |- Sf':Df' [ Substitution Structure Lemma, 12, 19 ] d1. Let Sfb = (seq o Ela)/alpha, R_val(ri)/Y, Sf'/Df' [ definition ] 24. . |- Sfb : Df [ (subst-t), 23, d1 ] 6'. .; P; Sfb(Gf); Sfb(Af); Sfb(Y); Sfb(P(l+2)) |- C(l+1) [ Substitution Lemma, 24, 21 ] 25. Forall r' =/= ri. . |- G(r') <= Sf(Gf)(r') [ Inversion of (G-subtp), 13 ] 26. Forall r' =/= ri. . |- G(r') <= Sfb(Gf)(r') [ 25, 23, d1, 20, 22 ] 27. Forall r' =/= ri. [ Repeated Application of the Subtyping lemma, 14, 26 ] .;P |-f R[ri -> R R_val(ri)](r') : Sfb(Gf)(r') 28. P |- R_val(ri) : check [ (rit-t) ] 29. .;P |-f R R_val(ri) : [ (val-t), 28 ] 30. Sfb(Gf)(ri) = [ 20, d1 ] 31. .;P |-f R[ri -> R R_val(ri)](ri) : Sfb(Gf)(ri) [ 29, 30 ] 2''. P |-f R[ri -> R R_val(ri)] : Sfb(Gf) [ (R-t), 27, 31 ] 32. |- (h,l,l+1) : seq o Ela o l+1 [ (h-append), 3 ] 33. |- (h,l,l+1) : Sfb(alpha o l+1) [ 32, d1 ] 3'. |- (h,l,l+1) : Sfb(Af) [ 33, 19 ] subcase f = R : 34a. . |- R_val(ri) = Ez'?Ef':Et' [ Inversion of (val-t), f = R, 15 ] 35a. . |- R_val(rz) = Ez [ Inversion of (val-t), f = R, 16 ] 36a. . |- Ez' =/= 0 [ Exp Eq Transitivity, 11, 35a, p1 ] 37a. . |- Ez'?Ef':Et' = Ef' [ Exp Conditional Lemma, 36a ] 38a. . |- R_val(ri) = Ef' [ Exp Eq Transitivity, 34a, 37a ] 39a. . |- Sfb(Y) = Ef' [ 38a, d1 ] 40a. . |- Ela = l [ Inversion of (h-append), 3 ] 4a'. . |- Sfb(Y) = l + 1 [ Exp Eq Transitivity, 39a, 8, 40a ] 2a'. P |-R R[ri -> R R_val(ri)] : Sfb(Gf) [ 2'', f = R ] subcase f = G and . |- Ez =/= 0 : green corruption does not affect branch direction ==> no fault elevation 34b. . |- R_val(ri) = Ez'?Ef':Et' [ Inversion of (val-t), f = G, 15 ] 35b. . |- Ez' =/= 0 [ Exp Eq Transitivity, 10, subcase assumption ] 36b. . |- Ez'?Ef':Et' = Ef' [ Exp Conditional Lemma, 35b ] 37b. . |- R_val(ri) = Ef' [ Exp Eq Transitivity, 34b, 36b ] 38b. . |- Sfb(Y) = Ef' [ 37b, d1 ] 39b. . |- Ela = l [ Inversion of (h-append), 3 ] 4b'. . |- Sfb(Y) = l + 1 [ Exp Eq Transitivity, 38b, 8, 39b ] 2b'. P |-G R[ri -> R R_val(ri)] : Sfb(Gf) [ 2'', f = G ] subcase f = G and . |- Et = Ela + 1 : branch and fallthru are equal ==> no fault elevation 34c. . |- R_val(ri) = Ez'?Ef':Et' [ Inversion of (val-t), 15 ] 35c. . |- Et' = Ef' [ Exp Eq Transitivity, subcase assumption, 8 ] 36c. . |- R_val(ri) = Ef' [ 34c, 35c ] 37c. . |- Sfb(Y) = Ef' [ 356c, d1 ] 38c. . |- Ela = l [ Inversion of (h-append), 3 ] 4c'. . |- Sfb(Y) = l + 1 [ Exp Eq Transitivity, 37b, 8, 38b ] 2c'. P |-G R[ri -> R R_val(ri)] : Sfb(Gf) [ 2'', f = G ] subcase f = G and . |- Ez = 0 and . |- Et =/= Ela + 1 : wrong branch taken ==> elevate Z to cf fault 34d. . |-G R_val(ri) = Ez'?Ef':Et' [ Inversion of (val-t), f = G, 15 ] 35d. . |- Ez' = 0 [ Exp Eq Transitivity, 10, subcase assumption ] 36d. . |- Ez'?Ef':Et' = Et' [ Exp Conditional Lemma, 35d ] 37d. . |- R_val(ri) = Et [ Exp Eq Transitivity, 34d, 36d, 10 ] 38d. . |- Sfb(Y) = Et [ Exp Eq Transitivity, 37d, d1 ] 39d. . |- Ela = l [ Inversion of (h-append), 3 ] 40d. . |- Et =/= l + 1 [ Exp Eq Transitivity, subcase assumption, 39d ] 4d'. . |- Sfb(Y) =/= l+1 [ Exp Eq Transitivity, 40d, 39d ] 2d'. P |-cf R[ri -> R R_val(ri)] : Sfb(Gf) [ Repeated applications of Color Weakening Lemma, 2'' ] subcase f = B and . |- R_val(ri) = Ef': intention set correctly ==> no fault elevation 34e. . |- Ela = l [ Inversion of (h-append), 3 ] 35e. . |- Ef' = l + 1 [ Exp Eq Transitivity, 34e, 8 ] 36e. . |- R_val(ri) = l+1 [ Exp Eq Transitivity, 35e, subcase assumption ] 4e'. . |- Sfb(Y) = l+1 [ 36e, d1 ] 2e'. P |-B R[ri -> R R_val(ri)] : Sfb(Gf) [ 2'', f = B ] subcase f = B and . |- R_val(ri) =/= Ef': intention set wrong ==> elevate to cf fault 34f. . |- Ela = l [ Inversion of (h-append), 3 ] 35f. . |- Ef' = l + 1 [ Exp Eq Transitivity, 34f, 8 ] 36f. . |- R_val(ri) =/= l+1 [ Exp Eq Transitivity, 35f, subcase assumption ] 4f'. . |- Sfb(Y) =/= l+1 [ 36f, d1 ] 2f'. P |-B R[ri -> R R_val(ri)] : Sfb(Gf) [ Repeated applications of Color Weakening Lemma, 2'' ] subcase f = cf: 34g. . |- Ei =/= l [ 4x, subcase assumption ] 35g. . |- Ei = l [ 5x, 7 ] 36g. contradiction, subcase doesn't apply [ 34g, 35g ] merge: 4x'. f' = cf ? . |- Ei =/= l : . |- Ei = l [ 4a', 4b', 4c', 4d', 4e', 4f', 36g ] 2'. P |-f' R[ri -> R R_val(ri)] : Sfb(Gf) [ 2a', 2b', 2c', 2d', 2e', 2f', 36g ] 4y'. Gf(ri) = 43. |-f (C, (h,l,l+1), R[ri -> R R_val(ri)], C(l+1)) [ (S-t), 1, 2', 3', 4x', 4y', 5' ] * 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. |-f (C, (h,l), R, brz rz rt) 1. |- C : P 2. P |-f R : G 3. |- (h,l) : A 4. f = cf ==> . |- Ei =/= l : . |- Ei = l 5. G(ri) =/= ==> . |- Ei = l 6. .;P;G;A;Ei;P(l+1) |- brz rz rt 7. .;P;G;seq o Ela; Ei; All[Df](Gf,Af) |- brz rz rt [ Inspection of (brz-t), 6 ] 8. G(ri)= [ Inversion of (brz-t), 7 ] 9. G(rz) = 10. . |- Ez = Ez' and . |- Ef' = Ela + 1 11. G(rt) = 12. . |- Et = Et' 13. Exists St. . |- St : Dt 14. . |- G[ri -> ] <= St(Gt) 15. . |- seq o Ela o Et' = St(At) 16. Forall r'. .;P |-f R(r') : G(r') [ Inversion of (R-t), 2 ] 17. .;P |-f R(ri) : [ 16, 8 ] 18. .;P |-f R(rz) : [ 16, 9 ] 19. .;P |-f R(rt) : [ 16, 11 ] 20.P(R_val(rt)) = All[Dl](Gl,Al) [ Inversion of (C-t), 1, p2 ] 21. Dl = (Dl',Y:kint,alpha:kseq) 22. Gl = (Gl',ri->) 23. Al = alpha o R_val(rt) 24. Dl' |- Gl' ok /\ Forall r' in Dom(Gl'). Gl'(r') =/= 25. Dl' |- P(R_val(rt)+1) ok 26. Dl; P; Gl; Al; Y; P(R_val(rt)+1) |- C(R_val(rt)) 8 subcases (based on f, further subdivided for f = G and B) divided into groups depending on outcome GROUP A: Control Flow OK subcase f = R : 30a1. . |- R_val(rt) = Et [ Inversion of (val-t), f=R, 19 ] 31a1. . |- R_val(rz) = Ez [ Inversion of (val-t), f=R, 18 ] 32a1. . |- R_val(ri) = [ Inversion of (val-t), f=R, 17 ] 33a1. . |- Ez' = 0 [ Exp Eq Transitivity, 31a1, p1, 10 ] 34a1. . |- R_val(ri) = Et' [ Exp Eq Transitivity, 32a1, (Conditional Exp Lemma, 33a1) ] subcase f = G and . |- Ez = 0 and . |- R_val(rt) = Et: green corruption does not affect branch direction or location ==> no fault elevation 30a2. . |- R_val(rt) = Et [ subcase assumption ] 31a2. . |- Ez'?Ef':Et' = Et' [ Exp Conditional Lemma, (subcase assumption, 10) ] 32a2. . |- R_val(ri) = Ez'?Ef':Et' [ Inversion of (val-t), f=G, 17 ] 33a2. . |- R_val(ri) = Et' [ Exp Eq Transitivity, (Exp Conditional Lemma, 31a2), 32a2 ] subcase f = B and . |- R_val(ri) = Et' 30a3. . |- R_val(rt) = Et [ Inversion of (val-t), f=B, 19 ] 31a3. . |- R_val(ri) = Et' [ subcase assumption ] merge: 35a. . |- R_val(rt) = Et [ 30a1, 30a2, 30a3 ] 36a. . |- R_val(ri) = Et' [ 34a1, 33a2, 31a3 ] 37a. P(R_val(rt)) = All[Dt](Gt,At) [ Equal Code Labels Lemma, (Inversion of (R-t), 2, 11), 35a ] 38a. Dl = Dt, Gl = Gt, Al = At [ 37a, 20 ] 39a. . |- G[ri -> ] <= St(Gt) [ 14 ] 40a. .;P |-f R R_val(ri) : [ (val-t), (rit-t), 36a ] 41a. P |-f R[ri -> R R_val(ri)] : G[ri -> ] [ (R-t), 2, 40a ] 2'. P |-f R[ri -> R R_val(ri)] : St(Gt) [ Repeated applications of Subtyping Lemma, 39a, 41a ] 6'. . ; P; St(Gt); St(At); St(Y); St(P(R_val(rt)+1))) |- C(R_val(rt)) [ Substitution Lemma, (13, 38a), 26 ] 42a. |- (h,l,R_val(rt)) : seq o Ela o Et' [ (h-append), 3, (Exp Eq Transitivity, 35a, 12) ] 3'. |- (h,l,R_val(rt)) = St(At) [ 42a, 15 ] 43a. . |- <= St(R,check,Y) [ 39a, 22 ] 44a. . |- Et' = St(Y) [ Inversion of (subtp-reflex), 43a ] 4'. . |- St(Y) = R_val(rt) [ Exp Eq Transitivity, 44a, 12, 35a ] 5'. St(Gl)(ri) = St() [ 22 ] 45a. |-f (C, (h,l,R_val(rt)), R[ri -> R R_val(ri)], C(R_val(rt))) [ (S-t), 1, 2', 3', 4', 5', 6' ] * BRZ-TAKEN.A complete GROUP B: Control Flow Messed up - elevate to cf fault d1b. Let Sl' = {42/x | Dl(x) = kint} union {empty/x | Dl(x) = kseq } [ build a substitution of nonsense values ] d2b. Let Sl = Sl', (seq o Ela)/alpha, R_val(ri)/Y 29b. . |- Sl : (Dl',alpha:kseq,Y:kint) [ (subst-t), d1b, d2b ] 6'. .;P;Sl(Gl);Sl(Al);Sl(Y);Sl(P(R_val(rt)+1)) |- C(R_val(rt)) [ Substitution Lemma, 29b, 28b ] 30b. Forall r' =/= ri. .;P |-cf R(r') : S(Gl)(r') [ (val-zap-cf-t), 24 ] 31b. P |- R_val(ri) : check [ (rit-t) ] 32b. .;P |-cf R R_val(ri) : [ (val-t), 31b ] 33b. .;P |-cf R[ri -> R R_val(ri)](ri) : Sl(Gl)(ri) [ 32b, d2b, 22 ] 2': P |-cf R[ri -> R R_val(ri)] : Sl(Gl) [ (R-t), 30b, 33b ] 34b. |- (h,l,R_val(rt)) : seq o Ela o R_val(rt) [ (h-append-t), 3 ] 3'. |- (h,l,R_val(rt)) : Sl(Al) [ 34b, d2b, 23 ] 35b. . |- R_val(ri) = Ez'?Ef':Et' [ Inversion of (val-t), 17, f=G ] 36b. . |- Ela = l [ Inversion of (h-append), 3 ] subcase: f = G and . |- Ez =/= 0 and . |- R_val(rt) =/= Ela + 1 : should have taken fallthru but didn't end up there ==> elevate to cf fault 37b1. . |- R_val(ri) = Ef' [ Conditional Exp Lemma, 35b, (subcase assumption, 10) ] 38b1. . |- R_val(ri) = Ela + 1 [ Exp Eq Transitivity, 37b1, 10 ] 39b1. . |- R_val(ri) =/= R_val(rt) [ Exp Eq Transitivity, 38b1, subcase assumption ] subcase: f = G and . |- Ez = 0 and . |- R_val(rt) =/= Et : should have jumped, but went to wrong place ==> elevate to cf fault 37b2. . |- R_val(ri) = Et [ Conditional Exp Lemma, 35b, (subcase assumption, 12) ] 38b2. . |- R_val(ri) =/= R_val(rt) [ Exp Eq Transitivity, 37b2, subcase assumption ] subcase: f = B and . |- R_val(ri) =/= Et' : intentions think we should have gone elsewhere 37b3. . |- R_val(rt) = Et [ Inversion of (val-t), f=B, 19 ] 38b3. . |- R_val(ri) =/= R_val(rt) [ Exp Eq Transitivity, subcase assumption, 12, 37b3 ] merge: 40b. . |- R_val(ri) =/= R_val(rt) [ 39b1, 38b2, 37b3 ] 4'. . |- Sl(Y) =/= R_val(rt) [ 40b, db2 ] 5'. Sl(Gl)(ri) = Sl() [ 22 ] 41b. |-cf (C, (h,l,R_val(rt)), R[ri -> R R_val(ri)], C(R_val(rt))) [ (S-t), 1, 2', 3', 4', 5', 6' ] * BRZ-TAKEN.B complete SUBCASE C: f = G and . |- Ez =/= 0 and . |- R_val(rt) = Ela + 1 : Two wrongs make a right - control flow should have taken fallthru, but ends up jmping to fallthru 30c. P(l+1) = All[Df](Gf,Af) [ Inspection of 6, 7 ] 31c. Exists Sf. . |- Sf : Df [ Inversion of (brz-t), 7 ] 32c. |- G[ri -> ] <= Sf(Gf) 33c. |- seq o Ela o Ef' = Sf(Af) 34c. . |- Ela = l [ Inversion of (h-append), 3 ] 35c. . |- R_val(rt) = l + 1 [ Exp Eq Transitivity, subcase assumption, 34c ] 36c. . |- R_val(ri) = Ez'?Ef':Et' [ Inversion of (val-t), f=G, 17 ] 37c. . |- Ez'?Ef':Et' = Ef' [ Conditional Exp Lemma, (Exp Eq Transitivity, subcase assumption, 10) ] 38c. . |- R_val(ri) = Ef' [ Exp Eq Transitivity, 36c, 37c ] 39c. .;P |-f R R_val(ri) : [ (val-t), (rit-t), 38c ] 40c. Df = Dl, Gf = Gl, Af = Al [ 20, 30c, 35c ] 41c. . |- G[ri -> ] <= Sf(Gf) [ 32c ] 42c. P |-G R[ri -> R R_val(ri)] : G[ri -> ] [ (R-t), 2, 39c ] 2'. P |-G R[ri -> R R_val(ri)] : Sf(Gf) [ Repeated applications of Subtyping Lemma, 41c, 42c ] 6'. .;P;Sf(Gf);Sf(Af);Sf(Y);Sf(P(R_val(rt)+1)) |- C(R_val(rt)) [ Substitution Lemma, 31c, 26, 40c ] 43c. . |- R_val(rt) = Ef' [ Exp Eq Transitivity, 35c, 10 ] 44c. |- (h,l,R_val(rt)) : seq o Ela o Ef' [ (h-append-t), 3, 43c ] 3'. |- (h,l,R_val(rt)) : Sf(Af) [ Exp Eq Transitivity, 44c, 33c ] 45c. . |- <= Sf() [ 32c, 40c, 22 ] 46c. . |- Sf(Y) = Ef' [ Inversion of (subtp-reflex), 45c ] 4'. . |- Sf(Y) = R_val(rt) [ Exp Eq Transitivity, 46c, 43c ] 5'. Sf(Gf)(ri) = Sf() [ 22 ] 41b. |-G (C, (h,l,R_val(rt)), R[ri -> R R_val(ri)], C(R_val(rt))) [ (S-t), 1, 2', 3', 4', 5', 6' ] * BRZ-TAKEN.C complete SUBCASE D: f = cf: 30d. . |- Ei =/= l [ 4, subcase assumption ] 41d. . |- Ei = l [ 5, 8 ] 32d. contradiction, subcase doesn't apply [ 30d, 31d ] * BRZ-TAKEN.D complete * BRZ-TAKEN complete CASES BRZ-HW-ERROR: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ R_val(rz) = 0 R_val(rz) not in Dom(C) ------------------------------------------------------------ (brz-hw-error) (C, h, R, brz rz rd) -->_0 hw-error (C,h,R,b) --/-->_0 S cases do not apply * BRZ-HW-ERROR complete. ** LEMMA PRESERVATION-BRZ-POSSIBLE-ELEVATION =========================================================================================================== =========================================================================================================== ********************************************* * LEMMA PRESERVATION-JMP-POSSIBLE-ELEVATION * ********************************************* If |-f (C, (h,l), R, jmp rt) and G is regfile type used and G(ri) = and G(rt) = and (C,(h,l),R,brz rz rt) -->_0 S' then (1) f = R ==> |-R S' (2) f =/= cf (3) f = G and (a) R_val(rt) = Et ==> |-G S' // correct jump target (b) R_val(rt) =/= Et ==> |-cf S' // incorrect jump target (4) f = B and (a) R_val(ri) = Et' ==> |-B S' // correct intention (b) R_val(ri) =/= Et' ==> |-cf S' // incorrect intention PROOF: By case analysis of S -->_0 S' ****** CASES MOVI, SUB, INTEND, INTENDZ-SET, INTENDZ-UNSET, RECOVERNZ-OK, RECOVERNZ-HALT, BRZ-TAKEN, BRZ-UNTAKEN, BRZ-HW-ERROR: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ a1. |-f S a2. S -->_0 S' 1. i =/= brz [ inspection of rules ] * CASES MOVI, SUB, INTEND, INTENDZ-SET, INTENDZ-UNSET, RECOVERNZ-OK, RECOVERNZ-HALT, BRZ-TAKEN, BRZ-UNTAKEN, BRZ-HW-ERROR 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))) 1. |- C : P 2. P |-Z R : G 3. |- (h,l) : A 4x. Z = cf ==> . |- Ei =/= l and Z = R/./G ==> |- Ei = l 4y. G(ri) =/= ==> . |- Ei = l 5. .;P;G;A;Ei;P(l+1) |- jmp rt 6. .; P; G; seq o Ela; Ei; t |- jmp rt [ Inspection of (jmp-t), 5 ] 7. G(ri)= [ Inversion of (jmp-t), 6 ] 8. G(rt) = 9. . |- Et = Et' 10. Exists S. D |- St : Dt 11. . |- G[ri -> ] <= St(Gt) 12. . |- seq o Ela o Et = St(At) 13. Forall r'. .;P |- R(r') : G(r') [ Inversion of (R-t), 2 ] 14. .;P |- R(ri) : [ 13, 7 ] 15. .;P |- R(rt) : [ 13, 8 ] 16.P(R_val(rt)) = All[Dl](Gl,Al) [ Inversion of (C-t), 1, p1 ] 17. Dl = (Dl',Y:kint,alpha:kseq) 18. Gl = (Gl',ri->) 19. Al = alpha o R_val(rt) 20. Dl' |- Gl' ok /\ Forall r' in Dom(Gl'). Gl'(r') =/= 22. Dl' |- P(R_val(rt)+1) ok 23. Dl; P; Gl; Al; Y; P(R_val(rt)+1) |- C(R_val(rt)) 5 subcases (based on f, further subdivided for f = G and f = B) divided into groups depending on outcome GROUP A: Control Flow OK ( f = R or f = G and . |- R_val(rt) = Et or f = B and . |- R_val(ri) = Et' ) subcase f = R : 24a1. . |- R_val(ri) = Et' [ Inversion of (val-t), f=R, 14 ] 25a1. . |- R_val(rt) = Et [ Inversion of (val-t), f=R, 15 ] subcase f = G and . |- R_val(rt) = Et: green corruption does not affect jmp location 24a2. . |- R_val(ri) = Et' [ Inversion of (val-t), f=G, 14 ] 25a2. . |- R_val(rt) = Et [ subcase assumption ] subcase f = B and . |- R_val(ri) = Et': blue corruption does not affect intention 24a3. . |- R_val(ri) = Et' [ subcase assumption ] 25a3. . |- R_val(rt) = Et [ Inversion of (val-t), f=B, 15 ] merge: 24a. . |- R_val(ri) = Et' 26a. . |- R_val(rt) = Et [ 25a1, 25a2 ] 27a. P(R_val(rt)) = All[Dt](Gt,At) [ Equal Code Labels Lemma, 8, 26a ] 28a. Dl = Dt, Gl = Gt, Al = At [ 27a, 16 ] 29a. .;P |-f R R_val(ri) : [ (val-t), (rit-t), (Exp Eq Transitivity, 24a, 9) ] 30a. P |-f R[ri -> R R_val(ri)] : G[ri -> ] [ (R-t), 2, 29a ] 2'. P |-f R[ri -> R R_val(ri)] : St(Gt) [ Repeated applications of Subtyping Lemma, 29a, 11 ] 6'. . ; P; St(Gt); St(At); St(Y); St(P(R_val(rt)+1))) |- C(R_val(rt)) [ Substitution Lemma, (13, 28a), 23 ] 31a. |- (h,l,R_val(rt)) : seq o Ela o Et [ (h-append), 3, 26a ] 3'. |- (h,l,R_val(rt)) = St(At) [ 31a, 12 ] 32a. . |- <= St() [ 11, (18, 28a) ] 33a. . |- Et' = St(Y) [ Inversion of (subtp-reflex), 32a ] 4'. . |- St(Y) = R_val(rt) [ Exp Eq Transitivity, 33a, 9, 26a ] 5'. St(Gl)(ri) = St() [ 22 ] 45a. |-f (C, (h,l,R_val(rt)), R[ri -> R R_val(ri)], C(R_val(rt))) [ (S-t), 1, 2', 3', 4', 5', 6' ] * JMP.A complete GROUP B: Control Flow Messed up - elevate to cf fault d1b. Let Sl' = {42/x | Dl(x) = kint} union {empty/x | Dl(x) = kseq } [ build a substitution of nonsense values ] d2b. Let Sl = Sl', (seq o Ela)/alpha, R_val(ri)/Y 29b. . |- Sl : (Dl',alpha:kseq,Y:kint) [ (subst-t), d1b, d2b ] 5'. .;P;Sl(Gl);Sl(Al);Sl(Y);Sl(P(R_val(rt)+1)) |- C(R_val(rt)) [ Substitution Lemma, 29b, 23 ] 30b. Forall r' =/= ri. .;P |-cf R(r') : S(Gl)(r') [ (val-zap-cf-t), 20 ] 31b. P |- R_val(ri) : check [ (rit-t) ] 32b. .;P |-cf R R_val(ri) : [ (val-t), 31b ] 33b. .;P |-cf R[ri -> R R_val(ri)](ri) : Sl(Gl)(ri) [ 32b, d2b, 18 ] 2': P |-cf R : Sl(Gl) [ (R-t), 30b, 33b ] 34b. |- (h,l,R_val(rt)) : seq o Ela o R_val(rt) [ (h-append-t), 3 ] 3'. |- (h,l,R_val(rt)) : Sl(Al) [ 34b, d2b, 19 ] subcase: f = G and . |- R_val(rt) =/= Et : Jumped to wrong place 35b1. . |- R_val(ri) = Et' [ Inversion of (val-t), 14, f=G ] 36b1. . |- R_val(ri) =/= R_val(rt) [ Exp Eq Transitivity, subcase assumption, 12, 35b1 ] subcase: f = B and . |- R_val(ri) =/= Et': Intended target is wrong 35b2. . |- R_val(rt) = Et [ Inversion of (val-t), 15, f = B ] 36b2. . |- R_val(ri) =/= R_val(rt) [ Exp Eq Transitivity, subcase assumption, 12, 25b2 ] merge: 36b. . |- R_val(ri) =/= R_val(rt) [ 36b1/36b2 ] 4x'. . |- Sl(Y) =/= R_val(rt) [ 36b, d2b ] 4y'. Sl(Gl)(ri) = Sl() [ 22 ] 41b. |-cf (C, (h,l,R_val(rt)), R[ri -> R R_val(ri)], C(R_val(rt))) [ (S-t), 1, 2', 3', 4x', 4y', 5' ] * JMP.B complete SUBCASE C: f = cf: 30c. . |- Ei =/= l [ 4, subcase assumption ] 31c. . |- Ei = l [ 5, 8 ] 32c. contradiction, subcase doesn't apply [ 30c, 31c ] * JMP.C complete * JMP complete CASES JMP-HW-ERROR: ~~~~~~~~~~~~~~~~~~~~ R_val(r) not in Dom(C) ---------------------------------------------------------------- (jmp-hw-error) (C, h, R, jmp r) -->_0 hw-error (C,h,R,b) --/-->_0 S case does not apply * JMP-HW-ERROR complete. ** LEMMA PRESERVATION-JMP-POSSIBLE-ELEVATION complete =========================================================================================================== =========================================================================================================== ************************ * PRESERVATION PART 1: * ************************ 1. If |- S and S -->_0 S' then |- S' PROOF: By case analysis on the structure of S.b ****** Each case uses Lemma Preservation-No-Elevation or Lemma Preservation-Jmp-Brz-Empty-Z as appropriate. =========================================================================================================== =========================================================================================================== ************************ * PRESERVATION PART 2: * ************************ 2. If |-f S and S -->_0 S' then Exists Z'. |-Z' S' and Z' >= f PROOF: By case analysis on the structure of S.b ****** Each case uses Lemma Preservation-No-Elevation or Lemma Preservation-Brz-Possible-Elevation or Lemma Preservation-Jmp-Possible-Elevation as appropriate. =========================================================================================================== =========================================================================================================== ************************ * PRESERVATION PART 3: * ************************ If |- S and S -->_1 S' then Exists c. |-c S' PROOF: By case analysis of S -->_1 S' ****** CASE ZAP-REG: ~~~~~~~~~~~~~ R(r) = c n ---------------------------------------------------- (zap-reg) (C, (h,l), R, b) -->_1 (C, (h,l), R[r -> c n'], b) a1. |- (C,(h,l),R,b) 1. |- C : P [ Inversion of (S-t), a1 ] 2. P |- R : G 3. . |- (h,l) : A 4x. . |- Ei = l 4y. G(ri) =/= ==> . |- Ei = l 5. .;P;G;A;Ei |- b 6. Forall r'. P;. |- R(r') : G(r') [ Inversion of (R-t), 2 ] 7. P;. |- R(r) : G(r) [ 6 ] 8. Exists t',E. G(r) = [ 7, p1, inspection of (val-t) ] 9. P;. |-c c n' : [ (val-zap-c-t) ] 10. Forall r'. P;. |-c R(r') : G(r') [ Color Weakening Lemma, 6 ] 2'. P |-c R[r -> c n'] : G [ (R-t), 10, 8, 9 ] 12. |-c (C, hi, ha, R[r -> c n'], b) [ (S-t), 1, 2', 3, 4x, 4x, 5 ] * ZAP-REG complete CASE ZAP-RECOVER: ~~~~~~~~~~~~~~~~~ R(rz) =/= 0 l' in Dom(C) --------------------------------------------------------------- (zap-recover-linC) (C, (h,l), R, recover rz; b) -->_1 (C, (h,l,l'), R, C(l')) R(rz) =/= 0 --------------------------------------------------------------- (zap-recover-lnotinC) (C, (h,l), R, recover rz; b) -->_1 hw-error(h) a1. |- (C,(h,l),R,b) 1. |- C : P [ Inversion of (S-t), a1, Inspection of (recovernz-t)'s ] 2. P |- R : G 3. . |- (h,l) : seq o Ela 4x. . |- Ei = l 4y. G(ri) =/= ==> . |- Ei = l1 5. .;P;G;seq o Ela;Ei |- recover rz;b subcase on structure of 5 (recovernz-t does not apply as D = . ) subcase RECOVERNZ-EQ-T: G(rz) = G(ri) = . |- Ez = Ei - Ela . |- Ei = Ela .; P; G[ri -> ]; seq o Ela; Ei; to |- b ------------------------------------------------- (recovernz-eq-t) .; P; G; seq o Ela; Ei; to |- recovernz rz ; b 6a. G(rz) = [ Inversion of (recovernz-eq-t), 5 ] 7a. . |- Ez = Ei - Ela 8a. . |- R_val(rz) = Ez [ Inversion of (val-t), Z = ., (2, 6a) ] 9a. . |- Ez = 0 [ Exp Eq Transitivity, 8a, p1 ] 10a. . |- Ei =/= Ela [ 9a, 7a ] 11a. . |- l = Ela [ Inversion of (h-append-t), 3 ] 12a. . |- Ei =/= l [ Exp Eq Transitivity, 10a, 11a ] subcase does not apply [ 12a contradicts 4x ] subcase RECOVERNZ-NEQ-T: G(rz) = G(ri) = . |- Ez = Ei - Ela . |- Ei =/= Ela ------------------------------------------------- (recovernz-neq-t) .; P; G; seq o Ela; Ei; to |- recovernz rz; b subcase does not apply [ p4 contradicts 4x ] * ZAP-RECOVER-LinC and ZAP-RECOVER-LnotinC complete CASE ZAP-RECOVER: ~~~~~~~~~~~~~~~~~ l in Dom(C) --------------------------------------------------------------- (zap-recover-linC) (C, (h,l), R, recover rz; b) -->_1 (C, (h,l), R, C(l)) Rz ** Progress Part 3 complete =========================================================================================================== =========================================================================================================== COROLLARY: PRESERVATION-FAULT-ELEVATION: **************************************** If |-Z S and S -->_k S' and k <= 1 then Exists Z'. |-Z' S' and Z' >= Z PROOF: By Case analysis on Z and k. ****** If Z = . and k = 0, then by Preservation Part 1 and . >= . If Z = f and k = 0, then by Preservation Part 2 If k = 1, then by Preservation Part 3 * Corollary Complete