Preservation: forall k, If |- S well-formed and S -k-> S' then |- S' well-formed. Proof by induction on S -k-> S' /////////////////////////////////////////////////////////////// Case S-Assign: H1 S = (~c, ~P) H2 S' = (~c, ~P[k=(r,s[x=s[e]],b)]) H3 ~P[k] = (r, s, x := e; b) H4 x in dom(s) H5 S -k-> S' H6 |- S well-formed > |- S' well-formed * all properties of |- S' well-formed follow directly from H6 EXCEPT: > exists A. ~R;D;k |- (r,s[x=s[e]],b) : A H7 ~R;D;k |- (r, s, x := e; b) : A // H6 * all properties of the current goal follow directly from H7 EXCEPT > exists A'. r;s[x=s[e]] |= B and ~R;dom(s[x=s[e]]);D |-z {B} b {C} H8 r;s |= A // H7 H9 ~R;dom(s);D |-z {A} x := e; b {C} // H7 H10 ~R;dom(s) |-b {A} x := e; b {C} // Inversion of H9 (H-BlockZ) H11 ~R;dom(s) |-i {A} x := e {B} // Inversion of H10 (H-SeqBlock) H12 ~R;dom(s) |-b {B} b {C} // Inversion of H10 (H-SeqBlock) H13 A |- B'[e/x]*F // Inversion of H11 using ihoare_inv H14 B'*F |- B // " H15 x in dom(s) // " H16 FV(x := e) /\ FV(F) = empty // " H17 x not in FV(F) // H16 H18 r;s |= B'[e/x]*F // H8 and H13 H19 r;s[x=s[e]] |= B'*F // subst_free_star H17 H18 H20 r;s[x=s[e]] |= B // H19 and H14 H21 dom(s[x=s[e]]) = dom(s) // Update of env doesn't change domain H22 ~R;dom(s[x=s[e]]) |-b {B} b {C} // rewrite H12 with H21 H23 ~R;dom(s[x=s[e]]);D |-z {B} b {C} // H-BlockZ H22 exists B s.t. H20 and H23 End Case S-Assign /////////////////////////////////////////////////////////////// Case S-Fetch: H1 S = (~c, ~P) H2 S' = (~c, ~P[k=(r,s[x=v],s,b)]) H3 ~P[k] = (r, s, x:= [e]; b) H4 x in dom(s) H5 r.h(s[e]) = v H6 S --> S' H7 |- S well-formed > |- S' well-formed * all properties of |- S' well-formed follow directly from H6 EXCEPT: > exists A. ~R;D;k |- (r,s[x=v],b) : A H8 ~R;D;k |- (r,s, x:= [e]; b) : A // H7 * all properties of the current goal follow directly from H7 EXCEPT > exists B, r;s[x=v] |= B and ~R;dom(s[x=v]);D |-z {B} b {C} H9 r;s |= A // H8 H10 ~R;dom(s);D |-z {A} x:= [e]; b {C} // H8 H11 ~R;dom(s) |-b {A} x:= [e]; b {C} // Inversion of H10 (H-BlockZ) H12 ~R;dom(s) |-i {A} x:= [e] {B} // Inversion of H11 (H-SeqBlock) H13 ~R;dom(s) |-b {B} b {C} // " H14 A |- (exists x1. (e -> x1) * ((e -> x1) -* B'[x1/x])) * D // Inversion of H12 using ihoare_inv H15 B'*D |- B // " H16 FV(x:= [e]) intersect FV(D) = empty // " H17 x not in dom(s) // " H18 r;s |= (exists x1. (e -> x1) * ((e -> x1) -* B'[x1/x])) * D // H9 H14 H19 r;s |= (e -> v * (e -> v -* B'[v/x])) * D // H5 H20 r;s |= B'[v/x] * D // H21 r;s[x=v] |= B' * D // subst_free_star H17 H20 H22 r;s[x=v] |= B // H15 H23 ~R;dom(s);D |-z {B} b {C} // Apply H-BlockZ to H13 H24 ~R;dom(s[x=v]);D |-z {B} b {C} // H4 (domain doesn't change) exists B s.t. H24 H22 /////////////////////////////////////////////////////////////// Case S-Store: H1 S = (~c, ~P) H2 S' = (~c, ~P[k=(r[s[e1] |-> s[e2]],s,b)]) H3 ~P[k] = (r, s, [e1] := e2; b) H5 S -k-> S' H6 |- S well-formed > |- S' well-formed * all properties of |- S' well-formed follow directly from H6 EXCEPT: 1> exists A'. ~R;D;k |- (r[h(s[e1]) = s[e2]],s,b) : A' 2> r' = forall+ k. ~P[k=(r[h(s[e1]) = s[e2]],b)][k].r + forall+ d. ~c[d].rG 3> total-res r' Goals 2 and 3 are trivial to show: updating a value in r does not change the heap layout > exists A', ~R;D;k |- (r[s[e1] |-> s[e2]],s,b) : A' H7 ~R;D;k |- (r,s, [e1] := e2; b) : A // H6 * all properties of the current goal follow directly from H7 EXCEPT > exists B, r[h(s[e1]) = s[e2]];s |= B and ~R;dom(s);D |-z {B} b {C} H8 r;s |= A // H7 H9 ~R;dom(s);D |-z {A} [e1] := e2; b {C} // H7 H10 ~R;dom(s) |-b {A} [e1] := e2; b {C} // Inversion of H9 (H-BlockZ) H11 ~R;dom(s) |-i {A} [e1] := e2 {B} // Inversion of H10 (H-SeqBlock) H12 ~R;dom(s) |-b {B} b {C} // Inversion of H10 (H-SeqBlock) H13 A |- e1 -> - * ((e1 -> e2) -* B')) * F // Inversion of H11 using ihoare_inv H14 B'*F |- B // " H15 r[h(s[e1]) = s[e2]];s |= e1 -> e2 * ((e1 -> e2) -* B')) * F // heap_upd_frame H13 H16 r[h(s[e1]) = s[e2]];s |= B' * F // H15 H17 r[h(s[e1]) = s[e2]];s |= B // H16 and H14 H18 ~R;dom(s);D |-z {B} b {C} // Apply H-BlockZ with H12 exists A' s.t. H17 and H18 End Case S-Store /////////////////////////////////////////////////////////////// Case S-WhileTrue: H1 S = (~c, ~P) H2 S' = (~c, ~P[k=(r,s, i; (while e i; b))]) H3 ~P[k] = (r, s, while e i; b) H4 s[e] = true H5 S -k-> S' H6 |- S well-formed > |- S' well-formed * all properties of |- S' well-formed follow directly from H6 EXCEPT: > exists A'. ~R;D;k |- (r,s, i; (while e i; b)) : A' H7 ~R;D;k |- (r,s, while e i; b) : A * all properties of the current goal follow directly from H7 EXCEPT > exists B, r;s |= B and ~R;dom(s);D |-z {B} i; (while e i; b) {C} H8 r;s |= A // H7 H9 ~R;dom(s);D |-z {A} while e i; b {C} // H7 H10 ~R;dom(s) |-b {A} while e i; b {C} // Inversion of H9 (H-BlockZ) H11 ~R;dom(s) |-i {A} while e i {B} // Inversion of H10 (H-SeqBlock) H12 ~R;dom(s) |-b {B} b {C} // Inversion of H10 (H-SeqBlock) H13 A |- A'*F // Inversion of H11 using ihoare_inv H14 (A' /\ !e) * F |- B // " H15 forall d, F |- HistFree d // " H16 FV(while e i) intersect FV(F) = empty // " H17 ~R;dom(s) |-i {A'} while e i {A' /\ !e} // " H18 ~R;dom(s) |-i {A' /\ e} i {A'} // " H19 FV(i) intersect FV(F) = empty // H16 H20 ~R;dom(s) |-i {(A' /\ e) * F} i {A' * F} // H-Frame H18 H19 H15 H21 ~R;dom(s) |-i {A' * F} while e i {(A' /\ !e) * F} // H-Frame H17 H16 H15 H22 ~R;dom(s) |-i {A' * F} while e i {B} // H-Consequence H21 H14 H23 ~R;dom(s) |-b {A' * F} while e i; b {C} // H-SeqBlock H22 H12 H24 ~R;dom(s) |-b {(A' /\ e) * F} i; (while e i; b) {C} // H-SeqBlock H20 H23 H25 r;s |= A'*F // H8 and H13 H26 r;s |= (A' /\ true) * F // H25 H27 r;s |= (A' /\ e) * F // H26 and H4 exists (A' /\ e) * F with H27 H24 End Case S-WhileTrue /////////////////////////////////////////////////////////////// Case S-WhileFalse: H1 S = (~c, ~P) H2 S' = (~c, ~P[k=(r,s, b2)]) H3 ~P[k] = (r, s, while e i; b) H4 s[e] = false H5 S -k-> S' H6 |- S well-formed > |- S' well-formed * all properties of |- S' well-formed follow directly from H6 EXCEPT: > exists A'. ~R;Dk |- (r,s,b) : A' H7 ~R;D;k |- (r,s, while e i; b) : A * all properties of the current goal follow directly from H7 EXCEPT > exists B, r;s |= B and ~R;dom(s);D |-z {B} b {C} H8 r;s |= A // H7 H9 ~R;dom(s);D |-z {A} while e i; b {C} // H7 H10 ~R;dom(s) |-b {A} while e i; b {C} // Inversion of H9 (H-BlockZ) H11 ~R;dom(s) |-i {A} while e i {B} // Inversion of H10 (H-SeqBlock) H12 ~R;dom(s) |-b {B} b {C} // Inversion of H10 (H-SeqBlock) H13 A |- A'*F // Inversion of H11 using ihoare_inv H14 (A' /\ !e) * F |- B // " H15 r;s |= A' * F // H8 and H13 H16 r;s |= (A' /\ true) * F // H15 H17 r;s |= (A' /\ !e) * F // H16 and H4 H18 r;s |= B // H17 and H14 H19 ~R;dom(s);D |-z {B} b {C} // H-BlockZ H12 exists B with H18 H19 End Case S-WhileFalse /////////////////////////////////////////////////////////////// Case S-Assert: H1 S = (~c, ~P) H2 S' = (~c, ~P[k=(r,s, b)]) H3 ~P[k] = (r, s, assert C; b) H4 r;s |= C*True H5 S -k-> S' H6 |- S well-formed > |- S' well-formed * all properties of |- S' well-formed follow directly from H6 EXCEPT: > exists A'. ~R;D;k |- (r,s,b) : A' H7 ~R;D;k |- (r,s, assert C; b) : A // H6 * all properties of the current goal follow directly from H7 EXCEPT > exists B, r;s |= B and ~R;dom(s);D |-z {B} b {C} H8 r;s |= A // H7 H9 ~R;dom(s);D |-z {A} assert E; b {C} // H7 H10 ~R;dom(s) |-b {A} assert E; b {C} // Inversion of H9 (H-BlockZ) H11 ~R;dom(s) |-i {A} assert E {B} // Inversion of H10 (H-SeqBlock) H12 ~R;dom(s) |-b {B} b {C} // Inversion of H10 (H-SeqBlock) H13 A |- E*F // Inversion of H11 using ihoare_inv H14 E*F |- B // " H15 r;s |= E*F // H8 with H13 H16 r;s |= B // H15 with H14 H17 ~R;dom(s);D |-z {B} b {C} // S-BlockZ H12 exists B with H16 and H17 End Case S-Assert /////////////////////////////////////////////////////////////// Case S-Produce: H1 S = (~c, ~P) H2 S' = (~c[d=(R,rG+r1,v::q,hc)], ~P[k=(r2,s,b)]) H3 ~P[k] = (r, s, produce d e; b) H4 ~c[d] = (R,rG,q,hc) H5 s[e] = v H6 r[p(d)+=v] = r1 + r2 H7 rG+r1;. |= R(v::q,hc) H8 S -k-> S' H9 |- S well-formed > |- S' well-formed * all properties of |- S' well-formed follow directly from H9 EXCEPT: >exists rt' 1> forall d. d |- ~c[d=(R,rG+r1,v::q,hc)][d] ok 2> rt' = forall+ k. ~P[k=(r2,s,b)][k].r + forall+ d. ~c[d=(R,rG+r1,v::q,hc)][d].rG 3> total-res rt' 4> forall k. exists Ak. ~R;D;k |- ~P[k=(r2,s,b)][k] : Ak 5> forall d R rG q hc. ~c[d=(R,rG+r1,v::q,hc)][d]=(R,rG,q,hc) implies (q@hc in rt'.p(d).H) and (hc in rt'.c(d).H) simplifying our goals: > exists rt' 1> d |- (R,rG+r1,v::q,hc) ok 2> rt' = forall+ k. ~P[k=(r2,s,b)][k].r + forall+ d. ~c[d=(R,rG+r1,v::q,hc)][d].rG 3> total-res rt' 4> exists Ak. ~R;D;k |- (r2,s,b) : Ak 5> (v::q@hc in rt'.p(d).H) and (hc in rt'.c(d).h) H10 d |- (R,rG,q,hc) ok // H9 H12 rG;. |= R(q,hc) // H10 Goal 1 > d |- (R,rG+r1,v::q,hc) ok or rather: 2> rG+r1;. |= R(v::q,hc) subgoal 2 is satisfied by H7 End Goal 1 H13 rt = forall+ k. ~P[k].r + forall+ d. ~c[d].rG // H9 H11 exists ro. rt = r + ro // H13 intro ro // H11 H11' rt = r + ro // " in goals, exists rt' = r[p: d+=v] + ro 2> r[p: d+=v] + ro = forall+ k. ~P[k=(r2,s,b)][k].r + forall+ d. ~c[d=(R,rG+r1,v::q,hc)][d].rG 3> total-res (r[p: d+=v] + ro) 4> exists Ak. ~R;D;k |- (r2,s,b) : Ak 5> v::q@hc in (r[p: d+=v] + ro).p(d).h 6> hc in (r[p: d+=v] + ro).c(d).h Goal 2 > r[p: d+=v] + ro = forall+ k. ~P[k=(r2,s,b)][k].r + forall+ d. ~c[d=(R,rG+r1,v::q,hc)][d].rG H14 rt = (forall+ k'!=k. ~P[k'].r) + r + (forall+ d'!=d. ~c[d'].rG) + rG // H13 H15 r+ro = ((forall+ k'!=k. ~P[k'].r) + r + (forall+ d'!=d. ~c[d'].rG) + rG) // H14, H11' H16 r[p: d+=v]+ro = ((forall+ k'!=k. ~P[k'].r) + r[p: d+=v] + (forall+ d'!=d. ~c[d'].rG) + rG) // H15 H17 r[p: d+=v]+ro = (forall+ k'!=k. ~P[k'].r) + r1 + r2 + (forall+ d'!=d. ~c[d'].rG) + rG // rewrite H16 with H6 H18 r[p: d+=v]+ro = (forall+ k. ~P[k=(r2,s,b)][k].r) + (forall+ d'!=d. ~c[d'].rG) + (rG + r1) // H17 H19 r[p: d+=v]+ro = (forall+ k. ~P[k=(r2,s,b)][k].r) + (forall+ d. ~c[d=(R,rG+r1,v::q,hc)][d].rG) // H18 End Goal 2 H20 total-res rt // H9 H21 total-res r[p: d+=v]+ro // H21; total-res doesn't care about history goal 3 is satisfied by H21 Goal 5 & 6 1> v::q@hc in (r[p: d+=v]+ro).p(d).H 2> hc in (r[p: d+=v]+ro).c(d).H H22 forall d R rG q hc. ~c[d]=(R,rG,q,hc) implies (q@hc in rt.p(d).H) and (hc in rt.c(d).H) // H9 H23 q@hc in rt.p(d).H // H22 H4 H24 hc in rt.c(d).H // " H25 hc in (r[p: d+=v]+ro).c(d).H // H24: produce history is independent of consume history H26 v::q@hc in v::(rt.p(d).H) // H23 H27 v::q@hc in (r[p: d+=v]+ro).p(d).H // H26 subgoals 1 and 2 (Goal 5) is satisfied by H27 and H25 End Goal 5 Goal 4 > exists Ak. ~R;D;k |- (r2,s,b) : Ak H28 ~R;D;k |- (r, s, produce d e; b) : A // H9 H29 r;s |= A // H28 H30 ~R;dom(s);D |-z {A} produce d e; b {C} // " H31 D(k) = (dom(s),C) // " H32 ~R;dom(s) |-b {A} produce d e; b {C} // Inversion of H30 (H-BlockZ) H33 ~R;dom(s) |-i {A} produce d e {B} // Inversion of H32 (H-SeqBlock) H34 ~R;dom(s) |-b {B} b {C} // " in goal, exists B > ~R;D;k |- (r2,s,b) : B H35 ~R;dom(s);D |-z {B} b {C} // Apply H-BlockZ to H34 H36 A |- (d,pi,H)! * ((d,pi,e::H)! =* E*B') * F // Inversion of H33 using ihoare_inv H37 B'*F |- B // " H38 (forall lq lc, SubIn pi (lq++lc) H -> E * ~R[d](lq,lc) |- ~R[d](e::lq,lc) // " H39 (d,pi,e::H)! =* E * B' |- PNoHist d // " H40 forall d' in FV(produce d e), F |- HistFree d' // " H41 F |- HistFree d // H40 H42 r;s |= (d,pi,H)! * ((d,pi,e::H)! =* E*B') * F // H29 and H36 intro v H42' s[e] = v // H42 H43 r[p: d+=v];s |= (d,pi,e::H)! * ((d,pi,e::H)! =* E*B') * F // histfree_ppush_star H42 H39 H41, H42' H44 r[p: d+=v];s |= E * B' * F // H43 H45 rG;.|= ~R[d](q,hc) // H12 and H4 H10 H46 rG;s|= ~R[d](q,hc) // H45 and H10 (def. closed) H47 r[p: d+=v]+rG;s |= E * B' * F * ~R[d](q,hc) // H44 H46 (total-world implies joinable) Assert: SubIn pi (q++hc) H > SubIn pi (q++hc) H implied by H9: history sets are always pieces of the global queue and consume history End assert H48 SubIn pi (q++hc) H // assertion H49 r[p: d+=v]+rG; s |= B' * F * ~R[d](e::q,hc) // H47 and H38 H48 H50 r1 + r2 + rG; s |= B' * F * ~R[d](e::q,hc) // rewrite H50 with H6 H51 r1 + r2 + rG; s |= B' * F * R(e::q,hc) // H10 H52 r2;s |= B' * F // H7 and H10 (def. precise) H53 r2;s |= B // H37 H54 ~R;D;k |- (r2,s,b) : B // H53 H35 H31 the goal is satisfied by H54 End Goal 4. All goals have been satisfied. End Case S-Produce. /////////////////////////////////////////////////////////////// Case S-Consume: H1 S = (~c, ~P) H2 S' = (~c[d=(R,rG,q,v::hc)], ~P[k=((r+r')[c: d+=v],s[x=v], b)]) H4 ~P[k] = (r, s, consume d x; b) H5 x in dom(s) H6 ~c[d] = (R,rG+r',q@[v],hc) H7 rG;. |= R(q,v::hc) H8 S -k-> S' H9 |- S well-formed > |- S' well-formed * all properties of |- S' well-formed follow directly from H9 EXCEPT: exists rt' 1> forall d. d |- ~c[d=(R,rG,q,v::hc)][d] ok 2> rt' = forall+ k. ~P[k=((r+r')[c: d+=v],s[x=v], b)][k].r + forall+ d. ~c[d=(R,rG,q,v::hc)][d].rG 3> total-res rt' // all permissions are either 1 or 0, etc 4> forall k. exists Ak. ~R;D;k |- ~P[k=((r+r')[c: d+=v],s[x=v], b)][k] : Ak 5> forall d R rG q hc. ~c[d=(R,rG,q,v::hc)][d]=(R,rG,q,hc) implies (q@hc in rt'.p(d).H) and (hc in rt'.c(d).H) H10 rt = forall+ k. ~P[k].r + forall+ d. ~c[d].rG // H9 H10' exists ro. rt = r + r' + ro // H10 H6 H4 intro ro H10'' rt = r + r' + ro in goal, exists (r+r')[c: d+=v] + ro, and after simplification: 1> d |- (R,rG,q,v::hc) ok 2> (r+r')[c: d+=v] + ro = forall+ k. ~P[k=((r+r')[c:d+=v],s[x=v], b)][k].r + forall+ d. ~c[d=(R,rG,q,v::hc)][d].rG 3> total-res ((r+r')[c:d+=v] + ro) // all permissions are either 1 or 0, etc 4> exists Ak. ~R;D;k |- ((r+r')[c:d+=v],s[x=v], b) : Ak 5> q@v::hc in ((r+r')[c: d+=v] + ro).p(d).H 6> v::hc in ((r+r')[c: d+=v] + ro).c(d).H H11 d |- (R,rG+r',q@[v],hc) ok // H9 H12 d |- R ok // H11 H13 rG+r';. |= R(q@[v],hc) // H11 Goal 1 > d |- (R,rG,q,v::hc) ok or rather: 1> rG;. |= R(q,v::hc) subgoal 1 is satisfied by H7 End Goal 1 Goal 2 > (r+r')[c: d+=v] + ro = forall+ k. ~P[k=((r+r')[c(d)+=v],s[x=v], b)][k].r + forall+ d. ~c[d=(R,rG,q,v::hc)][d].rG H14 rt = (forall+ k'!=k. ~P[k'].r) + r + (forall+ d'!=d. ~c[d'].rG) + (rG+r') // H10 and H4,H6 H15 r + r' + ro = (forall+ k'!=k. ~P[k'].r) + (r+r') + (forall+ d'!=d. ~c[d'].rG) + rG // H14 H16 (r+r')[c: d+=v] + ro = (forall+ k'!=k. ~P[k'].r) + (r+r')[c: d+=v] + (forall+ d'!=d. ~c[d'].rG) + rG // H15 H18 (r+r')[c: d+=v] + ro = (forall+ k. ~P[k=((r+r')[c:d+=v],s[x=v], b)][k].r) + (forall+ d'!=d. ~c[d'].rG) + rG // H17 H19 (r+r')[c: d+=v] + ro = (forall+ k. ~P[k=((r+r')[c:d+=v],s[x=v], b)][k].r) + (forall+ d. ~c[d=(R,rG,q,v::hc)][d].rG) // H18 End Goal 2 H20 total-res rt // H9 H21 total-res ((r+r')[c: d+=v] + ro) // H20; total-res doesn't care about history goal 3 is satisfied by H21 Goal 5 1> q@v::hc = ((r+r')[c: d+=v] + ro).p(d).h 2> v::hc = ((r+r')[c: d+=v] + ro).c(d).h H22 forall d R rG q hc. ~c[d]=(R,rG,q,hc) implies q@hc in rt.p(d).H and hc in rt.c(d).H // H9 H23 q@hc in rt.p(d).H // H22 H24 hc in rt.c(d).H // H22 H25 q@hc in ((r+r')[c: d+=v] + ro).p(d).H // H23: produce history is independent of consume history H26 v::hc in v::(rt.c(d).H) // H24 H27 v::hc in ((r+r')[c: d+=v] + ro).c(d).H // H26 subgoals 1 and 2 (Goal 5) is satisfied by H27 and H25 End Goal 5 Goal 4 > exists Ak. ~R;D;k |- ((r+r')[c:d+=v],s[x=v], b) : Ak H28 ~R;D;k |- (r, s, consume d x; b) : A // H9 H29 r;s |= A // H28 H30 ~R;dom(s);D |-z {A} consume d x; b {C} // " H31 D(k) = (dom(s),B) // " H32 ~R;dom(s) |-b {A} consume d x; b {C} // Inversion of H30 (H-BlockZ) H33 ~R;dom(s) |-i {A} consume d x {B} // Inversion of H32 (H-SeqBlock) H34 ~R;dom(s) |-b {B} b {C} // " in goal, exists A' > ~R;D;k |- ((r+r')[c:d+=v],s[x=v], b) : B H35 ~R;dom(s);D |-z {B} b {C} // Apply H-BlockZ to H34 H36 A |- (d,pi,H)? * (forall v. ((d,pi,H)? * E(v))[c:d+=v] =* B'[v/x]) * F // Inversion on H33 using ihoare_inv H37 B'*F |- B // " H38 x in G // " H39 forall lq v lc, SubIn pi lc H -> ~R[d](lq++v::nil,lc) |- E(v) * ~R[d](lq,v::lc) // " H40 forall v, ((d,pi,H)? * E(v))[c:d+=v] =* B'[v/x]) |- CNoHist d // " H41 forall d' in FV(consume d x), F |- CNoHist d' // " H42 FV(consume d x) intersect FV(F) = empty // " H43 x not in FV(F) // H42 H44 F |- CNoHist d // H41 H45 R(q@[v],hc) is closed // H12 H46 rG+r';s |= R(q@[v],hc) // H13 and H45 (def closed) H47 forall d. ~R[d] = ~c[d].R // H9 H48 rG+r';s |= ~R[d](q@[v],hc) // H46 and H47 and H4 H49 exists r''. r' = r + rG+r' // H10 H50 r;s |= (d,pi,H)? * (((d,pi,H)? * E(v))[c:d+=v] =* B'[v/x]) * F // H29 H36 H51 r+r'+rG;s |= (d,pi,H)? * (((d,pi,H)? * E(v))[c:d+=v] =* B'[v/x]) * F * ~R[d](q@[v],hc) // H50 H48 H49 Assert: SubIn pi hc H > SubIn pi hc H implied by H9: history sets are always pieces of the global queue and consume history H52 SubIn pi hc H // assertion H53 r+r'+rG;s |= (d,pi,H)? * (((d,pi,H)? * E(v))[c:d+=v] =* B'[v/x]) * F * E(v) * ~R[d](q,v::hc) // H51 H39 H52 H54 r+r';s |= (d,pi,H)? * (((d,pi,H)? * E(v))[c:d+=v] =* B'[v/x]) * F * E(v) // H7, H11 (def. precise, closed) H55 (r+r')[c:d+=v];s |= ((d,pi,H)? * E(v))[c:d+=v] * (((d,pi,H)? * E(v))[c:d+=v] =* B'[v/x]) * F // histfree_cpush_star H54 H40 H44 H56 (r+r')[c:d+=v];s |= B'[v/x] * F // H55 H58 (r+r')[c:d+=v];s[x=v] |= B' * F // subst_free_star H43 H59 ~R;D;k |- ((r+r')[c(d)+=v],s[x=v], b) : B // H58, H35, and H31 the goal is satisfied by H59 End Goal 4. All goals have been satisfied. End Case S-Consume /////////////////////////////////////////////////////////////// Case S-BlockingConsume: H1 S = (~c, ~P) H2 ~P[k] = (r, s, consume d x; b) H3 ~c[d] = (R,rG,nil,hc) H4 S -k-> S H5 |- S well-formed > |- S well-formed the goal is immediately satisfied by H5 End Case S-BlockingConsume /////////////////////////////////////////////////////////////// Case S-Skip: H1 S = (~c, ~P) H2 S' = (~c, ~P[k=(r,s,b)]) H3 ~P[k] = (r, s, skip; b) H4 S -k-> S' H5 |- S well-formed > |- S' well-formed * all properties of |- S' well-formed follow directly from H5 EXCEPT: > exists A'. ~R;D;k |- (r,s,b) : A' H6 ~R;D;k |- (r, s, skip; b) : A // H5 * all properties of the current goal follow directly from H6 EXCEPT > exists B. r;s |= B and ~R;dom(s);D |-z {B} b {C} H7 r;s |= A // H6 H8 ~R;dom(s);D |-z {A} skip; b {C} // H6 H9 ~R;dom(s) |-b {A} skip; b {C} // Inversion of H8 (H-BlockZ) H10 ~R;dom(s) |-i {A} skip {B} // Inversion of H9 (H-SeqBlock) H11 ~R;dom(s) |-b {B} b {C} // Inversion of H9 (H-SeqBlock) H12 A |- A'*F // Inversion of H10 using ihoare_inv H13 A'*F |- B // " H14 r;s |= A'*F // H7 with H12 H15 r;s |= B // H14 with H13 H16 ~R;dom(s);D |-z {B} b {C} // Z-Block H11 exists B s.t. H15 H16 End case S-Skip /////////////////////////////////////////////////////////////// Case S-Fork: H1 S = (~c, ~P) H2 S' = (~c, ~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2)) H3 ~P[k] = (r, s, ([G1;A1]b1 || [G2;A2]b2); b])) H4 r = r1 + r2 H5 s = s1 + s2 H6 s1 disjoint s2 H7 G1 subset dom(s1) H8 G2 = dom(s2) H9 r1; s1 |= A1*true H10 r2; s2 |= A2 H11 k1 = length(~P) H12 k2 = length(~P)+1 H13 S -k-> S' H14 |- S well-formed > |- S' well-formed unfolding well-formed in the goal (minus that which immediately follows from H13: exists rt': 1> rt' = forall+ k. (~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k].r + forall+ d. ~c[d].rG 2> total-res rt' 3> exists D'. forall k'. exists Ak. ~R;D';k |- (~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k'] : Ak 4> forall k3 k4. k3!=k4 implies dom((~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k3].s) disjoint dom((~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k4].s) 5> forall d R rG q hc. ~c[d]=(R,rG,q,hc) implies (q@hc in rt'.p(d).H) and (hc in rt'.c(d).H) 6> |- (~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2)) cont-ok in goal, exists rt 1> rt = forall+ k'. (~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k'].r + forall+ d. ~c[d].rG 2> total-res rt 3> exists D'. forall k'. exists Ak. ~R;D';k |- (~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k'] : Ak 4> forall k3 k4. k3!=k4 implies dom((~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k3].s) disjoint dom((~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k4].s) 5> forall d R rG q hc. ~c[d]=(R,rG,q,hc) implies q@hc in rt.p(d).H and hc in rt.c(d).H 6> |- (~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2)) cont-ok Goal 1: > rt = forall+ k'. (~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k'].r + forall+ d. ~c[d].rG H15 rt = forall+ k'. ~P[k'].r + forall+ d. ~c[d].rG // H14 H16 rt = (forall+ k'!=k. ~P[k'].r) + r + forall+ d. ~c[d].rG // H3 H17 rt = (forall+ k'!=k. ~P[k'].r) + r1 + r2 + forall+ d. ~c[d].rG // rewrite with H4 H18 rt = (forall+ k'. ~P[k=(.,., wait k1 k2; b)][k'].r) + r1 + r2 + forall+ d. ~c[d].rG // H19 rt = (forall+ k'. ~P[k=(.,., wait k1 k2; b)+(r1,s1,b1)+(r2,s2,b2)][k'].r) + forall+ d. ~c[d].rG // goal 1 is satisfied by H19 End Goal 1 Goal 2 follows directly from H14 H20 ~R;D;k |- (r, s, ([G1;A1]b1 || [G2;A2]b2); b])) : A // H13 H21 r;s |= A // H20 H22 ~R;dom(s);D |-z {A} [G1;A1]b1 || [G2;A2]b2; b {C} // " H23 D(k) = (dom(s),B) // " H24 ~R;dom(s) |-b {A} [G1;A1]b1 || [G2;A2]b2; b {C} // Inversion of H22 (H-BlockZ) H25 ~R;dom(s) |-i {A} [G1;A1]b1 || [G2;A2]b2 {B} // Inversion of H24 (H-SeqBlock) H26 ~R;dom(s) |-b {B} b {C} // " H27 A |- A1*A2*F // Inversion of H25 using ihoare_inv H28 B1*B2*F |- B // " H29 FV([G1;A1]b1 || [G2;A2]b2) intersect FV(F) = empty // " H30 forall d in FV([G1;A1]b1 || [G2;A2]b2), F |- PNoHist d // " H31 forall d in FV([G1;A1]b1 || [G2;A2]b2), F |- CNoHist d // " H32 ~R;G1 |-b {A1} b1 {B1} // " H33 ~R;G2 |-b {A2} b2 {B2} // " H34 G1 disjoint G2 // " H35 G1 + G2 subset dom(s) // " H36 FV(A1) subset G1 // " H37 FV(A2) subset G2 // " H38 A2 precise // " H39 FV(F) subset dom(s) // " H40 exists D'. D'(x) = (.,C) if x=k, else D'(x) = (dom(s1),B1*F) if x=k1, else D'(x) = (G2,B2) if x=k2, else D'(x)=D(x) XH28 A = A1*A2 // Inversion of H26 (H-Parallel) XH29 A' = B1*B2 // " XH30 ~R;G1 |-b {A1} b1 {B1} // " XH31 ~R;G2 |-b {A2} b2 {B2} // " XH32 G1 + G2 = dom(s) // " XH33 G1 disjoint G2 // " XH34 exists D'. D'(x) = (G1,B1) if x=k1, else D'(x) = (G2,B2) if x=k2, else D'(x)=D(x) Goal 3 > exists D'. forall k'. exists Ak. ~R;D;k |- (~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k'] : Ak in goal, exists D' from H34, and simplification from H14: 1> exists Ak. ~R;D';k |- (.,., wait k1 k2; b) : Ak 2> exists Ak. ~R;D';k1 |- (r1,s1,b1) : Ak 2> exists Ak. ~R;D';k2 |- (r2,s2,b2) : Ak goal 1: exists emp goal 2: exists A1*F goal 3: exists A2 1> ~R;D';k |- (.,., wait k1 k2; b) : emp 2> ~R;D';k1 |- (r1,s1,b1) : A1*F 2> ~R;D';k2 |- (r2,s2,b2) : A2 H41 D'(k) = (.,C) // H40 H42 D'(k1) = (dom(s1),B1*F) // H40 H43 D'(k2) = (G2,B2) // H40 Subgoal 1 > ~R;D';k |- (.,., wait k1 k2; b) : emp H44 .;. |= emp // def emp H45 ~R;dom(s) |-b {B1*B2*F} b {C} // block_consequence H26 H28 H46 ~R;dom(s1)+G2 |-b {B1*B2*F} b {C} // rewrite H45 with H5 H8 H47 ~R;.;D' |-z {emp} wait k1 k2; b {C} // H-ContZ H42 H43 (H6 H7 H8) H46 H48 ~R;D';k |- (.,.,wait k1 k2; b) : emp // Process-Okay with H44 H47 H41 End subgoal 1 Subgoal 2 > ~R;D';k1 |- (r1,s1,b1) : A1*F H49 r1+r2;s |= A1*A2*F // H21 H4 H50 r1;s |= A1*F // H49 H38 H10 H51 FV(A1) subset dom(s1) // H36 H7 H52 FV(F) subset dom(s1) // H39 H29 H53 FV(A1*F) subset dom(s1) // H51 H52 H54 r1;s1 |= A1*F // shrink_env H50 H53 H5 H55 FV(b1) intersect FV(F) = empty // H29 H56 forall d in FV(b1), F |- PNoHist d // H30 H57 forall d in FV(b1), F |- CNoHist d // H31 H58 ~R;G1 |-b {A1*F} b1 {B1*F} // block_frame H32 H55 H56 H57 H59 ~R;dom(s1) |-b {A1*F} b1 {B1*F} // H58 H7 H60 ~R;dom(s1);D' |-z {A1*F} b1 {B1*F} // H-ContZ H59 H61 ~R;D';k1 |- (r1,s1,b1) : A1*F // Process-Okay H54 H60 H42 End subgoal 2 Subgoal 3 > ~R;D';k2 |- (r2,s2,b2) : A2 H62 ~R;G2;D |-z {A2}b2{B2} // H-BlockZ H33 H63 ~R;dom(s2);D |-z {A2}b2{B2} // rewrite H62 with H8 H64 ~R;D';k2 |- (r2,s2,b2) : A2 // Process-Okay with H10 H63 H43 End subgoal 3 End Goal 2 Goal 4 > forall k3 k4. k3!=k4 implies dom((~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k3].s) disjoint dom((~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k4].s) intro k3 k4 H60 H60 k3!=k4 > dom((~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k3].s) disjoint dom((~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k4].s) H61 forall k3 k4, k3!=k4 implies dom(~P[k3].s) disjoint dom(~P[k4].s) // H14 We know that in ~P, each process' environment is disjoint. In ~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2), we take one process' environment and split it between two new processes. These two new processes have disjoint environments from all other processes because their parent's environment (their sum) was disjoint to all other processes' environments. Furthermore, we have defined the two new processes' environments such that they are disjoint. Finally, the parent loses its environment, so it too is disjoint from all other processes. End Goal 4 Goal 5 is directly satisfied by H14 Goal 6 > |- (~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2)) cont-ok unfolding cont-ok 1> forall k' k1' k2' ... . (~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k] = (.,., wait k1 k2; b) implies k' < k1' < k2' and k2' < length(~P) 2> forall k1' k2' ... . (~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k1'] = (.,., wait k11 k12; b1) and (~P[k=(.,., wait k1 k2; b)] + (r1,s1,b1) + (r2,s2,b2))[k2'] = (.,., wait k21 k22; b2) and k1'<>k2' implies k11 <> k12 <> k21 <> k22 H62 |- ~P cont-ok // H14 H63 forall k' k1' k2' ... . ~P[k] = (.,., wait k1 k2; b) // H62 implies k' < k1' < k2' and k2' < length(~P) H64 forall k1' k2' ... . ~P[k1'] = (.,., wait k11 k12; b1) // H62 and ~P[k2'] = (.,., wait k21 k22; b2) and k1'<>k2' implies k11 <> k12 <> k21 <> k22 Subgoal 1: We must show that every process ID is valid (within range of ~P[k=...][k1=...][k2=...]). Using H63, we know that this is true for ~P. We only need to consider the three changes: k k1, and k2. We know that processes k1 and k2 cannot have the form "wait ..." because they are blocks (b) and "wait" is a top-level (z) instruction. Finally, we know that the k1 and k2 in process k's instruction, "wait k1 k2; b", are within range because we defined them to be the last two processes in ~P[k=...][k1=...][k2=...] (k1=length(~P) and k2=length(~P)+1) Subgoal 2: We must show that no two different processes (within ~P[k=...][k1=...][k2=...]) may wait for any of the same children. We know this is true for ~P (H64). This remains true because processes k1 and k2 cannot be waiting for children (they are executing a block (b), not a top-level instruction (z)) and process k is waiting for children k1 and k2 that, by H63, are out of range for all other processes. End Goal 6 End Case S-Fork /////////////////////////////////////////////////////////////// Case S-Wait: H1 S = (~c, ~P) H2 S' = (~c, ~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)]) H3 ~P[k] = (.,., wait k1 k2; b) H4 ~P[k1] = (r1,s1,exit) H5 ~P[k2] = (r2,s2,exit) H6 S -k1-> S' H7 |- S well-formed > |- S' well-formed unfolding well-formed in the goal (minus that which immediately follows from H10: 1> rt' = forall+ k. (~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k].r + forall+ d. ~c[d].rG 2> total-res rt' 3> exists D'. forall k. exists Ak. ~R;D';k |- (~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k] : Ak 4> forall k3 k4. k3!=k4 implies dom((~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k3].s) disjoint dom((~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k4].s) 5> forall d R rG q hc. ~c[d]=(R,rG,q,hc) implies q@hc in rt'.p(d).H and hc in rt'.c(d).H 6> |- (~P[k1=(r1+r2,s1+s2, b)][k2=(.,.halted)]) cont-ok In goals, there exists rt' = rt 1> rt = forall+ k. (~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k].r + forall+ d. ~c[d].rG 2> total-res rt 3> exists D'. forall k. exists Ak. ~R;D';k |- (~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k] : Ak 4> forall k3 k4. k3!=k4 implies dom((~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k3].s) disjoint dom((~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k4].s) 5> forall d R rG q hc. ~c[d]=(R,rG,q,hc) implies q@hc in rt'.p(d).H and hc in rt'.c(d).H 6> |- (~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)]) cont-ok Goal 1 > rt = forall+ k'. (~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k'].r + forall+ d. ~c[d].rG H8 rt = forall+ k'. ~P[k'].r + forall+ d. ~c[d].rG // H7 H9 rt = (forall+ k'<>k<>k1<>k2. ~P[k'].r) + r1 + r2 + forall+ d. ~c[d].rG // H3 H4 H5 H10 rt = (forall+ k'<>k1<>k2. (~P[k=(r1+r2,s1+s2, b)])[k'].r) + forall+ d. ~c[d].rG // H11 rt = forall+ k'. (~P[k1=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k'].r + forall+ d. ~c[d].rG // End Goal 1 Goal 2 is directly satisfied by H6 Goal 3 > exists D'. forall k. exists Ak. ~R;D';k |- (~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k] : Ak H12 forall k. exists Ak. ~R;D;k |- ~P[k] : Ak // H7 H13 ~R;D;k |- (.,., wait k1 k2; b) : A // H12 H14 ~R;D;k1 |- (r1,s1, exit) : A1 // " H15 ~R;D;k2 |- (r2,s2, exit) : A2 // " H16 ~R;.;D |-z {A} wait k1 k2; b {C} // H13 H17 .;. |= A // " H18 D(k1) = (G1,B1') // Inversion of H16 (H-ContZ) H19 D(k2) = (G2,B2') // " H20 G1 disjoint G2 // " H21 ~R;G1+G2 |-b {B1' * B2'} b {C} // " H22 ~R;dom(s1);D |-z {A1} exit {B1} // H14 H23 ~R;dom(s1);D |-b {B1} exit {B1} // Inversion of H14 (H-Exit) H24 r1;s1 |= B1 // " H25 D(k1) = (dom(s1),B1) // " H26 ~R;dom(s2);D |-z {A2} exit {B2} // H15 H27 ~R;dom(s2);D |-b {B2} exit {B2} // Inversion of H15 (H-Exit) H28 r2;s2 |= B2 // " H29 D(k2) = (dom(s2),B2) // " H30 B1=B1', B2=B2', G1=dom(s1), G2=dom(s2) // H18 H25; H19 H29 H31 ~R;dom(s1+s2) |-b {B1 * B2} b {C} // rewrite H21 with H30 H32 exists D'. D'(x) = (.,False) if x = k1, else D'(x) = (.,False) if x = k2, else D'(x)=(dom(s1+s2),C) if x=k, else D'(x)=D(x) exists D' in goal > forall k. exists Ak. ~R;D';k |- (~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k] : Ak the goal is satisfied by H7 for all k except: 1> exists A'. ~R;D';k |- (r1+r2,s1+s2, b) : A' 2> exists A'. ~R;D';k1 |- (.,.,halted) : A' 3> exists A'. ~R;D';k2 |- (.,.,halted) : A' goal 1: exists B1*B2 goal 2: exists emp goal 2: exists emp 1> ~R;D';k |- (r1+r2,s1+s2, b) : B1*B2 2> ~R;D';k1 |- (.,.,halted) : emp 3> ~R;D';k2 |- (.,.,halted) : emp H33 .;. |= emp // def emp H34 ~R;dom(.);D' |-z {emp} halted {False} // H-HaltedZ H35 ~R;D';k1 |- (.,.,halted) : emp // Process-Okay with H33 H34 H32 H36 ~R;D';k2 |- (.,.,halted) : emp // Process-Okay with H33 H34 H32 subgoal 2: satisfied by H35 subgoal 3: satisfied by H36 H37 r1+r2;s1+s2 |= B1*B2 // H24 H28 (joinable by total-res: H6) H38 ~R;dom(s1+s2);D' |-z {B1 * B2} b {C} // H-BlockZ H31 H39 D'(k) = (dom(s1+s2),C) // H32 H40 ~R;D';k |- (r1+r2,s1+s2, b) : B1*B2 // Process-Okay with H37 H38, H39 subgoal 3 is satisfied by H40 End Goal 3 Goal 4 > forall k3 k4. k3!=k4 implies dom((~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k3].s) disjoint dom((~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k4].s) Intro k3 k4 H50 H50 k3!=k4 > dom((~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k3].s) disjoint dom((~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k4].s) H51 forall k5 k6. k5!=k6 implies dom(~P[k5].s) disjoint dom(~P[k6].s) // H7 We must prove that in the updated list of processes ~P[k=...][k1=...][k2=..], each process' environment is disjoint from the others. We know this is true for ~P by H51. With processes k1 and k2, the environment becomes empty and thus disjoint from all others. In process k, the environment becomes s1+s2; H51 tells us that s1 and s2 are disjoint from all ohter processes' environments, so s1+s2 must still be disjoint from those environments. End Goal 4 Goal 5 is directly satisfied by H7 Goal 6 > |- (~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)]) cont-ok unfolding cont-ok 1> forall k' k1' k2' ... . (~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k'] = (.,., wait k1' k2'; b) implies k' < k1' < k2' and k2' < length(~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)]) 2> forall k1' k2' ... . (~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k1'] = (.,., wait k11 k12; b1) and (~P[k=(r1+r2,s1+s2, b)][k1=(.,.,halted)][k2=(.,.,halted)])[k2'] = (.,., wait k21 k22; b2) and k1'<>k2' implies k11 <> k12 <> k21 <> k22 H52 |- ~P cont-ok // H6 H53 forall k' k1' k2' ... . ~P[k'] = (.,., wait k1' k2'; b) // H52 implies k' < k1' < k2' and k2' < length(~P) H54 forall k1' k2' ... . ~P[k1'] = (.,., wait k11 k12; b1) // H52 and ~P[k2'] = (.,., wait k21 k22; b2) and k1'<>k2' implies k11 <> k12 <> k21 <> k22 Subgoal 1: We must show that all process ID's are valid. By H2, we know that this was the case for ~P. This is still the case for ~P[k=...][k1=...][k2=...] because processes k1 and k2 are "halted" and don't refer to processes, and process k is now executing block b, which is not top-level (z) so cannot be a "wait". Subgoal 2: We must show that no two different processes refer to the same child processes. This was the case before and remains true because we do not add any more "wait" instructions (b cannot be a "wait" since it is a block) and processes k1 and k2 are "halted". End Goal 6 End Case S-Wait /////////////////////////////////////////////////////////////// Case S-BlockingWait: H1 S = (~c, ~P) H2 S' = (~c, ~P) H3 ~P[k1] = (r1,s1,b1) H4 ~P[k2] = (r2,s2,b2) H5 ~P[k] = (.,., wait k1 k2; b) H6 b1<>exit OR b2<>exit H7 S -k1-> S H8 |- S well-formed > |- S well-formed the goal is immediately satisfied by H8 End Case S-BlockingWait /////////////////////////////////////////////////////////////// Case S-Exit: H1 S = (~c, ~P) H2 S' = (~c, ~P) H3 S --> S' H4 |- S well-formed > |- S' well-formed the goal is immediately satisfied by H3 because S=S' by rule S-Exit End Case S-Exit /////////////////////////////////////////////////////////////// Case S-Seq: H1 S = (~c, ~P) H2 S' = (~c, ~P[k=(r,s, i1; (i2; b))]) H3 ~P[k] = (r,s, (i1; i2); b) H4 S --> S' H5 |- S well-formed > |- S' well-formed the goal is immediately satisfied by H5 except for: 1> exists Ak. ~R;D;k |- (r,s, i1; (i2; b)) : Ak 2> forall k1 k2, k1!=k2 implies dom((~P[k=(r,s, i1; (i2; b))])[k1].s) disjoint dom((~P[k=(r,s, i1; (i2; b))]))[k2].s) 3> |- (~P[k=(r,s, i1; (i2; b))])) cont-ok Goal 2 is satisfied by H5 because the environments are preserved Goal 3 is satisfied by H5 because the continuation is the same as before 2> exists Ak. ~R;D;k |- (r,s, i1; (i2; b)) : Ak H6 ~R;D;k |- (r,s, (i1; i2); b) : A // H5 H7 ~R;dom(s);D |-z {A} (i1; i2); b {B} // H6 H8 ~R;dom(s) |-b {A} (i1; i2); b {B} // Inversion of H6 (H-BlockZ) H9 ~R;dom(s) |-i {A} (i1; i2) {A3} // Inversion of H8 (H-SeqBlock) H10 ~R;dom(s) |-b {A3} b {B} // Inversion of H8 (H-SeqBlock) H11 ~R;dom(s) |-i {A} i1 {A2} // Inversion of H9 (H-Seq) H12 ~R;dom(s) |-i {A2} i2 {A3} // Inversion of H9 (H-Seq) H13 ~R;dom(s) |-b {A2} i2; b {B} // H-SeqBlock with H12 H10 H14 ~R;dom(s) |-b {A} i1; (i2; b) {B} // H-SeqBlock with H11 H13 H15 ~R;dom(s);D |-z {A} i1; (i2; b) {B} // H-BlockZ with H14 H16 ~R;D;k |- (r,s, i1; (i2; b)) : A // H6 and H15 exists A s.t. H16 the goal is satisfied by H16 End Case S-Seq End Preservation