Lemma Progress: If |- S well-formed then S is safe Invert |- S well-formed: HA1 S = (~c, ~P) HA2 forall d. d |- ~c[d] ok HA3 rt = forall+ k. ~P[k].r + forall+ d. ~c[d].rG HA4 total-res rt // all permissions are either 1 or 0, etc HA5 forall d. ~R[d] = ~c[d].R HA6 forall k. exists Ak. ~R;D;k |- ~P[k] : Ak HA7 forall k1 k2. k1!=k2 implies dom(~P[k1].s) disjoint dom(~P[k2].s) HA8 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) HA9 |- ~P cont-ok > forall k, exists S', S -k-> S' \/ halted S k intro k destruct (HA6 with k) HA10 ~R;D;k |- ~P[k] : A HA11 ~P[k] = (r,s,z) HA12 r;s |= A HA13 ~R;dom(s);D |-z {A}z{C} HA14 D(k) = (dom(s),C) > exists S'. S -->k S' or (halted S k) ***Proof by inversion of z*** Case z = halted H1 ~R;dom(s);D |-z {A} halted {C} H2 ~R;.;D |-z {emp} halted {False} H3 A = emp H4 B = False H5 r;s |= emp H6 r = . H7 s = . H8 ~P[k] = (.,.,halted) H9 halted k S End Case z = halted Case z = wait k1 k2; b H1 z = wait k1 k2; b H2 ~R;dom(s);D |-z {A} wait k1 k2; b {C} // HA13 and case z = ... H3 ~R;.;D |-z {emp} wait k1 k2; b {C} // Inversion of H1 (H-ContZ) H4 A = emp // " H5 dom(s) = . // " H6 D(k1) = (G1,B1) // " H7 D(k2) = (G2,B2) // " H8 G1 disjoint G2 // " H9 ~R;G1+G2 |-b {B1 * B2} b {C} // " H10 forall k k1 k2 ... . ~P[k] = (.,., wait k1 k2; b) // HA9 implies k < k1 < k2 and k2 < length(~P) H11 r;s |= emp // HA12 with H4 H12 r=. // H11 H13 ~P[k] = (.,., wait k1 k2; b) // rewrite HA11 with H1 H12 H5 H14 k1 < length(~P) // H10 H13 H15 k2 < length(~P) // " (intro s1 r1 b1) H16 let ~P[k1] = (s1,r1,b1) // H14 (intro s2 r2 b2) H17 let ~P[k2] = (s2,r2,b2) // H15 Destruct (b1=exit /\ b2=exit) or (b1<>exit \/ b2<>exit) Case b1=exit and b2=exit H18 b1=exit // assumption of case H19 b2=exit // assumption of case H20 ~P[k1] = (r1,s1,exit) // rewrite H16 with H18 H21 ~P[k2] = (r2,s2,exit) // rewrite H17 with H19 H22 exists r'. r' = r1 + r2 // HA3 H23 (~c, ~P) -k-> (~c, ~P[k=(r1+r2,s1+s2,b)][k1=(.,.,halted)][k2=(.,.,halted)]) // S-Wait with H21 H20 H13 exists S' = (~c, ~P[k=(r1+r2,s1+s2,b)][k1=(.,.,halted)][k2=(.,.,halted)]) s.t. S -k-> S' the goal is satisfied by H23 Case b1<>exit H24 b1<>exit \/ b2<>exit // assumption of case H25 S -k-> S // S-BlockingWait H17 H16 H13 H24 exists S the goal is satisified by H25 End Cases End Case z = wait k1 k2; b Case z = b = exit H1 z = b = exit // assumption of case H2 ~P[k] = (r,s,exit) // rewrite HA11 with H1 H3 (~c, ~P) -k-> (~c, ~P) // S-Exit the goal is satisfied by H3 End Case z = b = exit Case z = b = i; b' = (i1; i2); b' H1 z = b = i; b' = (i1; i2); b' // assumption of case H2 ~P[k] = (r,s(i1; i2), b') // rewrite HA11 with H1 H3 (~c, ~P) -k-> (~c, ~P[k=(r,s, i1; (i2; b))]) // S-Seq with H2 the goal is satisfied by H3 End Case z = b = i; b' = (i1; i2); b' Case z = b = i; b' = x := e; b' H1 z = b = i; b' = x := e; b' // assumption of case H2 ~P[k] = (r,s, x := e; b') // rewrite HA11 with H1 H3 ~R;dom(s);D |-z {A} x := e; b' {C} // rewrite HA13 with H1 H4 ~R;dom(s) |-b {A} x := e; b' {C} // Inversion of H3 (H-BlockZ) H5 ~R;dom(s) |-i {A} x := e {B} // Inversion of H4 (H-SeqBlock) H6 ~R;dom(s) |-b {B} b' {C} // " H7 x in G // Inversion of H5 (H-Assign) using ihoare_inv (~c, ~P) -k-> (~c, ~P[k=(r,s[x=s[e]],b')]) // S-Assign with H2 H7 End Case z = b = i; b' = x := e; b' Case z = b = i; b' = x := [e]; b' H1 z = b = i; b' = x := [e]; b' // assumption of case H2 ~P[k] = (r,s, x := [e]; b') // rewrite HA11 with H1 H3 ~R;dom(s);D |-z {A} x := [e]; b' {C} // rewrite HA13 with H1 H4 ~R;dom(s) |-b {A} x := [e]; b' {C} // Inversion of H3 (H-BlockZ) H5 ~R;dom(s) |-i {A} x := [e] {B} // Inversion of H4 (H-SeqBlock) H6 x in G // Inversion of H5 using ihoare_inv H7 (~c, ~P) -k-> (~c, ~P[k=(r,s[x=r.m(s[e])],b')]) // S-Fetch with H2 H6 End Case z = b = i; b' = x := [e]; b' Case z = b = i; b' = [e1] := e2; b' H1 z = b = i; b' = [e1] := e2; b' // assumption of case H2 ~P[k] = (r,s, [e1] := e2; b') // rewrite HA11 with H1 H3 (~c, ~P) -k-> (~c, ~P[k=(r(h,s[e1] = s[e2]),s,b)]) // S-Store with H2 End Case z = b = i; b' = [e1] := e2; b' Case z = b = i; b' = produce d e; b' H1 z = b = i; b' = produce d e; b' // assumption of case H2 ~P[k] = (r,s, produce d e; b') // rewrite HA11 with H1 H3 ~R;dom(s);D |-z {A} produce d e; b' {C} // rewrite HA13 with H1 H4 ~R;dom(s) |-b {A} produce d e; b' {C} // Inversion of H3 (H-BlockZ) H5 ~R;dom(s) |-i {A} produce d e {B} // Inversion of H4 (H-SeqBlock) H6 ~R;dom(s) |-b {B} b' {C} // " H7 A |- (d,pi,H)! * ((d,pi,e::H)! =* D*B') * F // Inversion of H5 using ihoare_inv H8 forall d' in FV(produce d e), F |- PNoHist d' // " H9 (d,pi,e::H)! =* D*B' |- PNoHist d // " H10 (forall lq lc, SubIn pi (lq++lc) H -> D * ~R[d](lq,lc) |- ~R[d](e::lq,lc) // " H8' F |- PNoHist d // H8 H13 r;s |= (d,pi,H)! * ((d,pi,e::H)! =* D*B') * F // HA12 and H7 intro v H11 s[e] = v // H13 H14 r[p(d)+=v];s |= (d,pi,e::H)! * ((d,pi,e::H)! =* D*B') * F // lemma histfree_ppush_star H13 H9 H8', H11 H15 r[p(d)+=v];s |= D * B' * F // H14 intro r1 r2 // destruct H15 H16 r[p(d)+=v] = r1 + r2 // H19 let (R,rG,q,hc) = ~c[d] // H16 H20 ~R[d] = R // H19 and HA2 Assert: D * ~R[d](q,hc) |- ~R[d](e::q,hc) using H10 > SubIn pi (q++hc) H implied by HA8: history sets are always pieces of the global queue and consume history H21 SubIn pi (q++hc) H Assert: rG+r1;. |= ~R[d](v::q,hc) > rG+r1;. |= ~R[d](v::q,hc) H22 rG;. |= ~R[d](q,hc) // HA2 and H20, H19 H23 forall q hc, R(q,hc) is closed // HA2 H24 rG;s |= ~R[d](q,hc) // H22 and H23 with H20 (def closed) H25 r1+rG;s |= ~R[d](q,hc) * D // HA4: r1 rg are joinable H26 r1+rG;s |= ~R[d](e::q,hc) // H25 and H10 H21 H27 r1+rG;. |= ~R[d](v::q,hc) // H23 (def closed) and H11 the goal is satisfied by H27 End Assert H28 rG+r1;. |= ~R[d](v::q,hc) // ^assertion: H27 H29 rG+r1;. |= R(v::q,hc) // rewrite H28 with H20 H30 (~c, ~P) -k-> (~c[d=(R,rG+r1,v::q,hc)], ~P[k=(r2,s,b')]) // S-Produce with H2 H19 H11 H16 H29 the goal is satisfied by H30 End Case z = b = i; b' = produce d x; b' Case z = b = i; b' = consume d x; b' H1 z = b = i; b' = consume d x; b' // assumption of case H2 ~P[k] = (r,s, consume d x; b') // rewrite HA11 with H1 H3 ~R;dom(s);D |-z {A} consume d x; b' {C} // rewrite HA13 with H1 H4 ~R;dom(s) |-b {A} consume d x; b' {C} // Inversion of H3 (H-BlockZ) H5 ~R;dom(s) |-i {A} consume d x {B} // Inversion of H4 (H-SeqBlock) H6 ~R;dom(s) |-b {B} b' {C} // " H7 x in dom(s) // Inversion of H5 (H-Consume) using ihoare_inv H8 forall lq v lc, SubIn pi lc H -> ~R[d](lq++v::nil,lc) |- D(v) * ~R[d](lq,v::lc) // " H9 let (R,rG,q,hc) = ~c[d] // Destruct q= q'@[v] or q=[] Case q = q'@[v] H10 q = q'@[v] Assert: ~R[d](q'@[v],hc) |- D(v) * ~R[d](q',v::hc) using H8 > SubIn pi hc H implied by HA8: history sets are always pieces of the global queue and consume history End assert H11 ~R[d](q'@[v],hc) |- D(v) * ~R[d](q',v::hc) // assert H12 d |- R ok // HA2 with H9 H13 rG;. |= R(q'@[v],hc) // " H14 forall q, hc, R(q,hc) is closed // H12 H15 rG;s |= R(q'@[v],hc) // H13 H14 H16 rG;s |= ~R[d](q'@[v],hc) // H9 H12 H17 rG;s |= D(v) * ~R[d](q',v::hc) // H11 H16 Intro rG' r' // destruct H17 H18 rG = rG'+r' // " H19 rG';s |= ~R[d](q',v::hc) // " H20 r';s |= D(v) // " H21 rG';. |= ~R[d](q',v::hc) // H14 with H19 H21 rG';. |= R(q',v::hc) // rewrite H21 with H12, H9 H22 ~c[d] = (R,rG'+r',q'@[v],hc) // rewrite H9 with H18, H10 H23 (~c, ~P) -k-> (~c[d=(R,rG',q',v::hc)], ~P[k=((r+r')[c(d)+=v],s[x=v], b')]) // H-Consume with H2, H7, H22, H21 the goal is satisfied by H23 Case q = [] H24 q = [] H25 ~c[d] = (R,rG,[],hc) // rewrite H9 with H24 H26 (~c, ~P) -k-> (~c, ~P) // H-BlockingConsume with H2 H25 the goal is satisfied by H26 End cases End Case z = b = i; b' = consume d x; b' Case z = b = i; b' = consume d x; b' H1 z = b = i; b' = consume d x; b' // assumption of case H2 ~P[k] = (r,s, consume d x; b') // rewrite HA11 with H1 H3 ~R;dom(s);D |-z {A} consume d x; b' {C} // rewrite HA13 with H1 H4 ~R;dom(s) |-b {A} consume d x; b' {C} // Inversion of H3 (H-BlockZ) H5 ~R;dom(s) |-i {A} consume d x {B} // Inversion of H4 (H-SeqBlock) H6 ~R;dom(s) |-b {B} b' {C} // " H7 x in dom(s) // Inversion of H5 (H-Consume) using ihoare_inv H8 forall lq lc, SubIn pi lc H -> ~R[d](lq++v::nil,lc) |- D * ~R[d](lq,v::lc) // " H9 let (R,rG,q,hc) = ~c[d] // Destruct q= q'@[v] or q=[] Case q = q'@[v] H10 q = q'@[v] Assert: ~R[d](q'@[v],hc) |- D * ~R[d](q',v::hc) using H8 > SubIn pi hc H implied by HA8: history sets are always pieces of the global queue and consume history End assert H11 ~R[d](q'@[v],hc) |- D * ~R[d](q',v::hc) // assert H12 d |- R ok // HA2 with H9 H13 rG;. |= R(q'@[v],hc) // " H14 forall q, hc, R(q,hc) is closed // H12 H15 rG;s |= R(q'@[v],hc) // H13 H14 H16 rG;s |= ~R[d](q'@[v],hc) // H9 H12 H17 rG;s |= D * ~R[d](q',v::hc) // H11 H16 Intro rG' r' // destruct H17 H18 rG = rG'+r' // " H19 rG';s |= ~R[d](q',v::hc) // " H20 r';s |= D // " H21 rG';. |= ~R[d](q',v::hc) // H14 with H19 H21 rG';. |= R(q',v::hc) // rewrite H21 with H12, H9 H22 ~c[d] = (R,rG'+r',q'@[v],hc) // rewrite H9 with H18, H10 H23 (~c, ~P) -k-> (~c[d=(R,rG',q',v::hc)], ~P[k=((r+r')[c(d)+=v],s[x=v], b')]) // H-Consume with H2, H7, H22, H21 the goal is satisfied by H23 Case q = [] H24 q = [] H25 ~c[d] = (R,rG,[],hc) // rewrite H9 with H24 H26 (~c, ~P) -k-> (~c, ~P) // H-BlockingConsume with H2 H25 the goal is satisfied by H26 End cases End Case z = b = i; b' = consume d x; b' Case z = b = i; b' = assert D; b' H1 z = b = i; b' = assert D; b' // assumption of case H2 ~P[k] = (r,s, assert D; b') // rewrite HA11 with H1 H3 ~R;dom(s);D |-z {A} assert D; b' {C} // rewrite HA13 with H1 H4 ~R;dom(s) |-b {A} assert D; b' {C} // Inversion of H3 (H-BlockZ) H5 ~R;dom(s) |-i {A} assert D {B} // Inversion of H4 (H-SeqBlock) H6 ~R;dom(s) |-b {B} b' {C} // " H7 A |- D*F // Inversion of H5 using ihoare_inv H8 D*F |- B H9 r;s|= D*F // HA12 and H8 H12 r;s|= D*true // H9 H14 (~c, ~P) -k-> (~c, ~P[k=(r,s,b')]) // S-Assert with H2 H12 End Case z = b = i; b' = assert D; b' Case z = b = i; b' = while e i; b' H1 z = b = i; b' = while e i; b' // assumption of case H2 ~P[k] = (r,s, while e i; b') // rewrite HA11 with H1 H3 ~R;dom(s);D |-z {A} while e i; b' {C} // rewrite HA13 with H1 H4 ~R;dom(s) |-b {A} while e i; b' {C} // Inversion of H3 (H-BlockZ) H5 ~R;dom(s) |-i {A} while e i {B} // Inversion of H4 (H-SeqBlock) Destruct s[e] =true \/ s[e] = false Case s[e] = true H10 s[e] = true // assumption of case H11 (~c, ~P) -k-> (~c, ~P[k=(r,s, i; while e i; b)]) // S-WhileTrue with H2, H10 Case s[e] = false H13 s[e] = false // assumption of case H14 (~c, ~P) -k-> (~c, ~P[k=(r,s, b)]) // S-WhileFalse with H2, H13 End Cases End Case z = b = i; b' = while e i; b' Case z = b = i; b' = skip; b' H1 z = b = i; b' = skip; b' // assumption of case H2 ~P[k] = (r,s, skip; b') // rewrite HA11 with H1 H3 (~c, ~P) -k-> (~c, ~P[r,s,b']) // Apply S-Skip End Case z = b = i; b' = skip; b' Case z = b = i; b' = [G1;A1]b1 || [G2;A2]b2; b' H1 z = b = i; b' = [G1;A1]b1 || [G2;A2]b2; b' // assumption of case H2 ~P[k] = (r,s,[G1;A1]b1 || [G2;A2]b2; b') // rewrite HA14 with H1 H3 ~R;dom(s);D |-z {A} [G1;A1]b1 || [G2;A2]b2; b' {C} // rewrite HA16 with H1 H4 ~R;dom(s);D |-b {A} [G1;A1]b1 || [G2;A2]b2; b' {C} // Inversion of H3 (H-BlockZ) H5 ~R;dom(s);D |-i {A} [G1;A1]b1 || [G2;A2]b2 {B} // Inversion of H4 (H-SeqBlock) H6 ~R;dom(s);D |-b {B} b' {C} // " FV([G1;A1]b1 || [G2;A2]b2) intersect FV(D) = empty FV(b1) intersect FV(F) = empty FV(A2) intersect FV(F) = empty H7 ~R;G1 |-b {A1} b1 {B1} // Inversion of H5 (H-Parallel) using ihoare_inv H8 ~R;G2 |-b {A2} b2 {B2} // " H9 G1 disjoint G2 // " H10 G1 + G2 = dom(s) // " H11 FV(A1) subset G1 // " H12 FV(A2) subset G2 // " H13 A |- A1*A2*D // " H14 B1*B2*D |- B // " H15 r;s |= A1*A2*D // HA12 H13 H16 r = r1 + r2 // destruct H15 H17 r1;s |= A1*D // " H18 r2;s |= A2 // " H19 r1;s |= A1*true // H17 H20 exists s1 s2. s = s1 + s2 and dom(s1)=G1 and dom(s2) = G2 // H10 H21 s = s1 + s2 // destruct H20 H22 dom(s1) = G1 // " H23 dom(s2) = G2 // " H24 s1 disjoint s2 // rewrite H9 with H22 and H23 H25 FV(A1) subset dom(s1) // rewrite H11 with H22 H26 FV(A2) subset dom(s2) // rewrite H12 with H23 H27 s1 subset s // H21 H28 s2 subset s // H21 H29 FV(A1*true) subset dom(s1) // H25 H30 r1;s1 |= A1*true // shrink_env H19 H29 H27 H31 r2;s2 |= A2 // shrink_env H18 H26 H28 H32 let k1:= length(~P) H33 let k2:= length(~P)+1 H34 (~c, ~P) -k-> (~c, ~P[k=(.,., wait k1 k2; b')] + (r1,s1,b1) + (r2,s2,b2)) // Apply S-Fork with H2 H16 H21 H24 H22 H23 H30 H31 H32 H33 exists S' = (~c, ~P[k=(.,., wait k1 k2; b')] + (r1,s1,b1) + (r2,s2,b2)) the goal is satisfied by H34 End Case z = b = i; b' = [G1;A1]b1 || [G2;A2]b2; b'