This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| stable-I10 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ ls.e ≠ ls.e0 ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → (ls.e0 ≠ ⊥ → ls.e0 = gs0.ar[ls.n]) ∧ ls.e ≠ ls.e0 ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b | A Proof Obligation |
| stable-I4 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.n = ls.n0) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.n = ls.n0 | A Proof Obligation |
| definedness-M6 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ pre(gs, ls, M6, a) → ls.n < # gs.ar | A Proof Obligation |
| step-M10-M13 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ ls.e ≠ ls.e0 ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ pre(gs, ls, M10, a) ∧ pcstepf(gs, ls, M10, a) = M13 → (# gstepf(gs, ls, M10, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M10, a).ar)) ∧ lstepf(gs, ls, M10, a).n < # gstepf(gs, ls, M10, a).ar ∧ lstepf(gs, ls, M10, a).e ≠ ⊥ ∧ lstepf(gs, ls, M10, a).sz = # gstepf(gs, ls, M10, a).ar ∧ ( lstepf(gs, ls, M10, a).n0 < # gstepf(gs, ls, M10, a).ar ∧ lstepf(gs, ls, M10, a).n0 = get_hash(lstepf(gs, ls, M10, a).e, lstepf(gs, ls, M10, a).sz)) ∧ ¬ lstepf(gs, ls, M10, a).b ∧ (gstepf(gs, ls, M10, a).ar[lstepf(gs, ls, M10, a).n] ≠ ⊥ ∧ gstepf(gs, ls, M10, a).ar[lstepf(gs, ls, M10, a).n] ≠ lstepf(gs, ls, M10, a).e) ∧ lstepf(gs, ls, M10, a).e ≠ lstepf(gs, ls, M10, a).e0 ∧ allslotsfull(gstepf(gs, ls, M10, a).ar, lstepf(gs, ls, M10, a).n0, lstepf(gs, ls, M10, a).n, lstepf(gs, ls, M10, a).e, false) | A Proof Obligation |
| step-I13-I14 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ (gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] = ls.e0) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I13, a) ∧ pcstepf(gs, ls, I13, a) = I14 → (# gstepf(gs, ls, I13, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I13, a).ar)) ∧ lstepf(gs, ls, I13, a).e = lstepf(gs, ls, I13, a).e0 ∧ lstepf(gs, ls, I13, a).e = gstepf(gs, ls, I13, a).ar[lstepf(gs, ls, I13, a).n] ∧ allslotsfull(gstepf(gs, ls, I13, a).ar, lstepf(gs, ls, I13, a).n0, lstepf(gs, ls, I13, a).n, lstepf(gs, ls, I13, a).e, false) ∧ lstepf(gs, ls, I13, a).n < # gstepf(gs, ls, I13, a).ar ∧ lstepf(gs, ls, I13, a).e ≠ ⊥ ∧ lstepf(gs, ls, I13, a).sz = # gstepf(gs, ls, I13, a).ar ∧ ( lstepf(gs, ls, I13, a).n0 < # gstepf(gs, ls, I13, a).ar ∧ lstepf(gs, ls, I13, a).n0 = get_hash(lstepf(gs, ls, I13, a).e, lstepf(gs, ls, I13, a).sz)) ∧ ¬ lstepf(gs, ls, I13, a).b | A Proof Obligation |
| step-M9-idle | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.b ∧ (∃ n. n < # gs.ar ∧ gs.ar[n] = ls.e) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ pre(gs, ls, M9, a) ∧ pcstepf(gs, ls, M9, a) = idle → (# gstepf(gs, ls, M9, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M9, a).ar)) ∧ (lstepf(gs, ls, M9, a).b → (∃ n. n < # gstepf(gs, ls, M9, a).ar ∧ gstepf(gs, ls, M9, a).ar[n] = lstepf(gs, ls, M9, a).e)) | A Proof Obligation |
| stable-M15 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n0, ls.e, true)) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs0.ar, ls.n0, ls.n0, ls.e, true) | A Proof Obligation |
| step-I2-I3 | ⊦ ((# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar) ∧ pre(gs, ls, I2, a) ∧ pcstepf(gs, ls, I2, a) = I3 → (# gstepf(gs, ls, I2, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I2, a).ar)) ∧ lstepf(gs, ls, I2, a).e ≠ ⊥ ∧ lstepf(gs, ls, I2, a).sz = # gstepf(gs, ls, I2, a).ar ∧ lstepf(gs, ls, I2, a).n0 < # gstepf(gs, ls, I2, a).ar ∧ lstepf(gs, ls, I2, a).n0 = get_hash(lstepf(gs, ls, I2, a).e, lstepf(gs, ls, I2, a).sz) | A Proof Obligation |
| step-I12-I13 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I12, a) ∧ pcstepf(gs, ls, I12, a) = I13 → (# gstepf(gs, ls, I12, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I12, a).ar)) ∧ (gstepf(gs, ls, I12, a).ar[lstepf(gs, ls, I12, a).n] ≠ ⊥ ∧ gstepf(gs, ls, I12, a).ar[lstepf(gs, ls, I12, a).n] = lstepf(gs, ls, I12, a).e0) ∧ allslotsfull(gstepf(gs, ls, I12, a).ar, lstepf(gs, ls, I12, a).n0, lstepf(gs, ls, I12, a).n, lstepf(gs, ls, I12, a).e, false) ∧ lstepf(gs, ls, I12, a).n < # gstepf(gs, ls, I12, a).ar ∧ lstepf(gs, ls, I12, a).e ≠ ⊥ ∧ lstepf(gs, ls, I12, a).sz = # gstepf(gs, ls, I12, a).ar ∧ ( lstepf(gs, ls, I12, a).n0 < # gstepf(gs, ls, I12, a).ar ∧ lstepf(gs, ls, I12, a).n0 = get_hash(lstepf(gs, ls, I12, a).e, lstepf(gs, ls, I12, a).sz)) ∧ ¬ lstepf(gs, ls, I12, a).b | A Proof Obligation |
| HashsetInv-thm | ⊦ HashsetInv(gs, lsf, pcf) ∧ hashsetStep(mkstate(gs, lsf, pcf), a, mkstate(gs0, lsf0, pcf0)) → HashsetInv(gs0, lsf0, pcf0) | An Axiom |
| stable-M8 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ (∃ n. n < # gs.ar ∧ gs.ar[n] = ls.e) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ (∃ n. n < # gs0.ar ∧ gs0.ar[n] = ls.e) ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) | A Proof Obligation |
| step-I17-I20 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, true) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I17, a) ∧ pcstepf(gs, ls, I17, a) = I20 → (# gstepf(gs, ls, I17, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I17, a).ar)) ∧ allslotsfull(gstepf(gs, ls, I17, a).ar, lstepf(gs, ls, I17, a).n0, lstepf(gs, ls, I17, a).n, lstepf(gs, ls, I17, a).e, false) ∧ lstepf(gs, ls, I17, a).n ≠ lstepf(gs, ls, I17, a).n0 ∧ lstepf(gs, ls, I17, a).n < # gstepf(gs, ls, I17, a).ar ∧ lstepf(gs, ls, I17, a).e ≠ ⊥ ∧ lstepf(gs, ls, I17, a).sz = # gstepf(gs, ls, I17, a).ar ∧ ( lstepf(gs, ls, I17, a).n0 < # gstepf(gs, ls, I17, a).ar ∧ lstepf(gs, ls, I17, a).n0 = get_hash(lstepf(gs, ls, I17, a).e, lstepf(gs, ls, I17, a).sz)) ∧ ¬ lstepf(gs, ls, I17, a).b | A Proof Obligation |
| step-I3-I4 | ⊦ ((# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ pre(gs, ls, I3, a) ∧ pcstepf(gs, ls, I3, a) = I4 → (# gstepf(gs, ls, I3, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I3, a).ar)) ∧ allslotsfull(gstepf(gs, ls, I3, a).ar, lstepf(gs, ls, I3, a).n0, lstepf(gs, ls, I3, a).n, lstepf(gs, ls, I3, a).e, false) ∧ lstepf(gs, ls, I3, a).n < # gstepf(gs, ls, I3, a).ar ∧ lstepf(gs, ls, I3, a).e ≠ ⊥ ∧ lstepf(gs, ls, I3, a).sz = # gstepf(gs, ls, I3, a).ar ∧ ( lstepf(gs, ls, I3, a).n0 < # gstepf(gs, ls, I3, a).ar ∧ lstepf(gs, ls, I3, a).n0 = get_hash(lstepf(gs, ls, I3, a).e, lstepf(gs, ls, I3, a).sz)) ∧ lstepf(gs, ls, I3, a).n = lstepf(gs, ls, I3, a).n0 | A Proof Obligation |
| definedness-I16 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ (gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] ≠ ls.e) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I16, a) → ls.sz ≠ 0 | A Proof Obligation |
| step-idle-I1 | ⊦ (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ pre(gs, ls, idle, a) ∧ pcstepf(gs, ls, idle, a) = I1 → (# gstepf(gs, ls, idle, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, idle, a).ar)) ∧ lstepf(gs, ls, idle, a).e ≠ ⊥ | A Proof Obligation |
| step-M7-M10 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ pre(gs, ls, M7, a) ∧ pcstepf(gs, ls, M7, a) = M10 → (# gstepf(gs, ls, M7, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M7, a).ar)) ∧ lstepf(gs, ls, M7, a).n < # gstepf(gs, ls, M7, a).ar ∧ lstepf(gs, ls, M7, a).e ≠ ⊥ ∧ lstepf(gs, ls, M7, a).sz = # gstepf(gs, ls, M7, a).ar ∧ ( lstepf(gs, ls, M7, a).n0 < # gstepf(gs, ls, M7, a).ar ∧ lstepf(gs, ls, M7, a).n0 = get_hash(lstepf(gs, ls, M7, a).e, lstepf(gs, ls, M7, a).sz)) ∧ ¬ lstepf(gs, ls, M7, a).b ∧ (lstepf(gs, ls, M7, a).e0 ≠ ⊥ → lstepf(gs, ls, M7, a).e0 = gstepf(gs, ls, M7, a).ar[lstepf(gs, ls, M7, a).n]) ∧ lstepf(gs, ls, M7, a).e ≠ lstepf(gs, ls, M7, a).e0 ∧ allslotsfull(gstepf(gs, ls, M7, a).ar, lstepf(gs, ls, M7, a).n0, lstepf(gs, ls, M7, a).n, lstepf(gs, ls, M7, a).e, false) | A Proof Obligation |
| stable-M5 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) | A Proof Obligation |
| step-M12-idle | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ ls.e ≠ ls.e0) ∧ pre(gs, ls, M12, a) ∧ pcstepf(gs, ls, M12, a) = idle → (# gstepf(gs, ls, M12, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M12, a).ar)) ∧ (lstepf(gs, ls, M12, a).b → (∃ n. n < # gstepf(gs, ls, M12, a).ar ∧ gstepf(gs, ls, M12, a).ar[n] = lstepf(gs, ls, M12, a).e)) | A Proof Obligation |
| stable-I3 | ⊦ ( ((# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz) | A Proof Obligation |
| step-M5-M6 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ pre(gs, ls, M5, a) ∧ pcstepf(gs, ls, M5, a) = M6 → (# gstepf(gs, ls, M5, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M5, a).ar)) ∧ lstepf(gs, ls, M5, a).n < # gstepf(gs, ls, M5, a).ar ∧ lstepf(gs, ls, M5, a).e ≠ ⊥ ∧ lstepf(gs, ls, M5, a).sz = # gstepf(gs, ls, M5, a).ar ∧ ( lstepf(gs, ls, M5, a).n0 < # gstepf(gs, ls, M5, a).ar ∧ lstepf(gs, ls, M5, a).n0 = get_hash(lstepf(gs, ls, M5, a).e, lstepf(gs, ls, M5, a).sz)) ∧ ¬ lstepf(gs, ls, M5, a).b ∧ allslotsfull(gstepf(gs, ls, M5, a).ar, lstepf(gs, ls, M5, a).n0, lstepf(gs, ls, M5, a).n, lstepf(gs, ls, M5, a).e, false) | A Proof Obligation |
| step-I10-I11 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ ls.e ≠ ls.e0 ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I10, a) ∧ pcstepf(gs, ls, I10, a) = I11 → (# gstepf(gs, ls, I10, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I10, a).ar)) ∧ lstepf(gs, ls, I10, a).e ≠ lstepf(gs, ls, I10, a).e0 ∧ (lstepf(gs, ls, I10, a).e0 ≠ ⊥ ∧ lstepf(gs, ls, I10, a).e0 = gstepf(gs, ls, I10, a).ar[lstepf(gs, ls, I10, a).n]) ∧ allslotsfull(gstepf(gs, ls, I10, a).ar, lstepf(gs, ls, I10, a).n0, lstepf(gs, ls, I10, a).n, lstepf(gs, ls, I10, a).e, false) ∧ lstepf(gs, ls, I10, a).n < # gstepf(gs, ls, I10, a).ar ∧ lstepf(gs, ls, I10, a).e ≠ ⊥ ∧ lstepf(gs, ls, I10, a).sz = # gstepf(gs, ls, I10, a).ar ∧ ( lstepf(gs, ls, I10, a).n0 < # gstepf(gs, ls, I10, a).ar ∧ lstepf(gs, ls, I10, a).n0 = get_hash(lstepf(gs, ls, I10, a).e, lstepf(gs, ls, I10, a).sz)) ∧ ¬ lstepf(gs, ls, I10, a).b | A Proof Obligation |
| stable-M14 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, true)) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, true) | A Proof Obligation |
| rely-reflexive | # ar ≠ 0 ∧ htok(ar) ⊦ rely(ar, ar) | A Proof Obligation |
| stable-M17 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n ≠ ls.n0) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n ≠ ls.n0 | A Proof Obligation |
| step-M15-M16 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n0, ls.e, true)) ∧ pre(gs, ls, M15, a) ∧ pcstepf(gs, ls, M15, a) = M16 → (# gstepf(gs, ls, M15, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M15, a).ar)) ∧ lstepf(gs, ls, M15, a).n < # gstepf(gs, ls, M15, a).ar ∧ lstepf(gs, ls, M15, a).e ≠ ⊥ ∧ lstepf(gs, ls, M15, a).sz = # gstepf(gs, ls, M15, a).ar ∧ ( lstepf(gs, ls, M15, a).n0 < # gstepf(gs, ls, M15, a).ar ∧ lstepf(gs, ls, M15, a).n0 = get_hash(lstepf(gs, ls, M15, a).e, lstepf(gs, ls, M15, a).sz)) ∧ ¬ lstepf(gs, ls, M15, a).b ∧ allslotsfull(gstepf(gs, ls, M15, a).ar, lstepf(gs, ls, M15, a).n0, lstepf(gs, ls, M15, a).n0, lstepf(gs, ls, M15, a).e, true) | A Proof Obligation |
| stable-I12 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b | A Proof Obligation |
| step-I13-I16 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ (gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] = ls.e0) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I13, a) ∧ pcstepf(gs, ls, I13, a) = I16 → (# gstepf(gs, ls, I13, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I13, a).ar)) ∧ (gstepf(gs, ls, I13, a).ar[lstepf(gs, ls, I13, a).n] ≠ ⊥ ∧ gstepf(gs, ls, I13, a).ar[lstepf(gs, ls, I13, a).n] ≠ lstepf(gs, ls, I13, a).e) ∧ allslotsfull(gstepf(gs, ls, I13, a).ar, lstepf(gs, ls, I13, a).n0, lstepf(gs, ls, I13, a).n, lstepf(gs, ls, I13, a).e, false) ∧ lstepf(gs, ls, I13, a).n < # gstepf(gs, ls, I13, a).ar ∧ lstepf(gs, ls, I13, a).e ≠ ⊥ ∧ lstepf(gs, ls, I13, a).sz = # gstepf(gs, ls, I13, a).ar ∧ ( lstepf(gs, ls, I13, a).n0 < # gstepf(gs, ls, I13, a).ar ∧ lstepf(gs, ls, I13, a).n0 = get_hash(lstepf(gs, ls, I13, a).e, lstepf(gs, ls, I13, a).sz)) ∧ ¬ lstepf(gs, ls, I13, a).b | A Proof Obligation |
| stable-M11 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ ls.e ≠ ls.e0) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ ls.e ≠ ls.e0 | A Proof Obligation |
| stable-I9 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.e = gs.ar[ls.n] ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.b) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) ∧ ls.e = gs0.ar[ls.n] ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.b | A Proof Obligation |
| step-HashsetLInv | ⊦ HashsetGInv(gs) ∧ HashsetLInv(gs, ls, pc) ∧ lstep(gs, ls, pc, a, gs0, ls0, pc0) → HashsetGInv(gs0) ∧ HashsetLInv(gs0, ls0, pc0) ∧ ls.tid = ls0.tid | An Axiom |
| stable-I15 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e = gs.ar[ls.n] ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.b) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.e = gs0.ar[ls.n] ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.b | A Proof Obligation |
| step-I9-idle | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.e = gs.ar[ls.n] ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.b) ∧ pre(gs, ls, I9, a) ∧ pcstepf(gs, ls, I9, a) = idle → (# gstepf(gs, ls, I9, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I9, a).ar)) ∧ (lstepf(gs, ls, I9, a).b ↔ (∃ n. n < # gstepf(gs, ls, I9, a).ar ∧ gstepf(gs, ls, I9, a).ar[n] = lstepf(gs, ls, I9, a).e)) | A Proof Obligation |
| step-M14-M15 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, true)) ∧ pre(gs, ls, M14, a) ∧ pcstepf(gs, ls, M14, a) = M15 → (# gstepf(gs, ls, M14, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M14, a).ar)) ∧ lstepf(gs, ls, M14, a).n < # gstepf(gs, ls, M14, a).ar ∧ lstepf(gs, ls, M14, a).e ≠ ⊥ ∧ lstepf(gs, ls, M14, a).sz = # gstepf(gs, ls, M14, a).ar ∧ ( lstepf(gs, ls, M14, a).n0 < # gstepf(gs, ls, M14, a).ar ∧ lstepf(gs, ls, M14, a).n0 = get_hash(lstepf(gs, ls, M14, a).e, lstepf(gs, ls, M14, a).sz)) ∧ ¬ lstepf(gs, ls, M14, a).b ∧ allslotsfull(gstepf(gs, ls, M14, a).ar, lstepf(gs, ls, M14, a).n0, lstepf(gs, ls, M14, a).n0, lstepf(gs, ls, M14, a).e, true) | A Proof Obligation |
| step-M6-M7 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ pre(gs, ls, M6, a) ∧ pcstepf(gs, ls, M6, a) = M7 → (# gstepf(gs, ls, M6, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M6, a).ar)) ∧ lstepf(gs, ls, M6, a).n < # gstepf(gs, ls, M6, a).ar ∧ lstepf(gs, ls, M6, a).e ≠ ⊥ ∧ lstepf(gs, ls, M6, a).sz = # gstepf(gs, ls, M6, a).ar ∧ ( lstepf(gs, ls, M6, a).n0 < # gstepf(gs, ls, M6, a).ar ∧ lstepf(gs, ls, M6, a).n0 = get_hash(lstepf(gs, ls, M6, a).e, lstepf(gs, ls, M6, a).sz)) ∧ ¬ lstepf(gs, ls, M6, a).b ∧ (lstepf(gs, ls, M6, a).e0 ≠ ⊥ → lstepf(gs, ls, M6, a).e0 = gstepf(gs, ls, M6, a).ar[lstepf(gs, ls, M6, a).n]) ∧ allslotsfull(gstepf(gs, ls, M6, a).ar, lstepf(gs, ls, M6, a).n0, lstepf(gs, ls, M6, a).n, lstepf(gs, ls, M6, a).e, false) | A Proof Obligation |
| rely-I12-I13 | ⊦ ls.tid ≠ tid0 ∧ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I12, a) ∧ pcstepf(gs, ls, I12, a) = I13 → rely(gs.ar, gstepf(gs, ls, I12, a).ar) | A Proof Obligation |
| stable-I18 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n0, ls.e, true) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → allslotsfull(gs0.ar, ls.n0, ls.n0, ls.e, true) ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b | A Proof Obligation |
| step-M17-M5 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n ≠ ls.n0) ∧ pre(gs, ls, M17, a) ∧ pcstepf(gs, ls, M17, a) = M5 → (# gstepf(gs, ls, M17, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M17, a).ar)) ∧ lstepf(gs, ls, M17, a).n < # gstepf(gs, ls, M17, a).ar ∧ lstepf(gs, ls, M17, a).e ≠ ⊥ ∧ lstepf(gs, ls, M17, a).sz = # gstepf(gs, ls, M17, a).ar ∧ ( lstepf(gs, ls, M17, a).n0 < # gstepf(gs, ls, M17, a).ar ∧ lstepf(gs, ls, M17, a).n0 = get_hash(lstepf(gs, ls, M17, a).e, lstepf(gs, ls, M17, a).sz)) ∧ ¬ lstepf(gs, ls, M17, a).b ∧ allslotsfull(gstepf(gs, ls, M17, a).ar, lstepf(gs, ls, M17, a).n0, lstepf(gs, ls, M17, a).n, lstepf(gs, ls, M17, a).e, false) | A Proof Obligation |
| step-I5-I21 | ⊦ ¬ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I5, a) ∧ pcstepf(gs, ls, I5, a) = I21) | A Proof Obligation |
| stable-HashsetLInv | ⊦ HashsetGInv(gs) ∧ HashsetLInv(gs, ls, pc) ∧ HashsetGInv(gs0) ∧ HashsetRely(gs, ls.tid, gs0) → HashsetLInv(gs0, ls, pc) | An Axiom |
| step-M13-M14 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ (gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] ≠ ls.e) ∧ ls.e ≠ ls.e0 ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ pre(gs, ls, M13, a) ∧ pcstepf(gs, ls, M13, a) = M14 → (# gstepf(gs, ls, M13, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M13, a).ar)) ∧ lstepf(gs, ls, M13, a).n < # gstepf(gs, ls, M13, a).ar ∧ lstepf(gs, ls, M13, a).e ≠ ⊥ ∧ lstepf(gs, ls, M13, a).sz = # gstepf(gs, ls, M13, a).ar ∧ ( lstepf(gs, ls, M13, a).n0 < # gstepf(gs, ls, M13, a).ar ∧ lstepf(gs, ls, M13, a).n0 = get_hash(lstepf(gs, ls, M13, a).e, lstepf(gs, ls, M13, a).sz)) ∧ ¬ lstepf(gs, ls, M13, a).b ∧ allslotsfull(gstepf(gs, ls, M13, a).ar, lstepf(gs, ls, M13, a).n0, lstepf(gs, ls, M13, a).n, lstepf(gs, ls, M13, a).e, true) | A Proof Obligation |
| definedness-I6 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I6, a) → ls.n < # gs.ar | A Proof Obligation |
| step-I11-I17 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e ≠ ls.e0 ∧ (ls.e0 ≠ ⊥ ∧ ls.e0 = gs.ar[ls.n]) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I11, a) ∧ pcstepf(gs, ls, I11, a) = I17 → (# gstepf(gs, ls, I11, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I11, a).ar)) ∧ allslotsfull(gstepf(gs, ls, I11, a).ar, lstepf(gs, ls, I11, a).n0, lstepf(gs, ls, I11, a).n, lstepf(gs, ls, I11, a).e, true) ∧ lstepf(gs, ls, I11, a).n < # gstepf(gs, ls, I11, a).ar ∧ lstepf(gs, ls, I11, a).e ≠ ⊥ ∧ lstepf(gs, ls, I11, a).sz = # gstepf(gs, ls, I11, a).ar ∧ ( lstepf(gs, ls, I11, a).n0 < # gstepf(gs, ls, I11, a).ar ∧ lstepf(gs, ls, I11, a).n0 = get_hash(lstepf(gs, ls, I11, a).e, lstepf(gs, ls, I11, a).sz)) ∧ ¬ lstepf(gs, ls, I11, a).b | A Proof Obligation |
| definedness-I12 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I12, a) → ls.n < # gs.ar ∧ (gs.ar[ls.n] = ⊥ ⊃ ls.n < # gs.ar;ls.n < # gs.ar) | A Proof Obligation |
| stable-M7 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs0.ar[ls.n]) ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) | A Proof Obligation |
| step-I4-I5 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.n = ls.n0) ∧ pre(gs, ls, I4, a) ∧ pcstepf(gs, ls, I4, a) = I5 → (# gstepf(gs, ls, I4, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I4, a).ar)) ∧ allslotsfull(gstepf(gs, ls, I4, a).ar, lstepf(gs, ls, I4, a).n0, lstepf(gs, ls, I4, a).n, lstepf(gs, ls, I4, a).e, false) ∧ lstepf(gs, ls, I4, a).n < # gstepf(gs, ls, I4, a).ar ∧ lstepf(gs, ls, I4, a).e ≠ ⊥ ∧ lstepf(gs, ls, I4, a).sz = # gstepf(gs, ls, I4, a).ar ∧ ( lstepf(gs, ls, I4, a).n0 < # gstepf(gs, ls, I4, a).ar ∧ lstepf(gs, ls, I4, a).n0 = get_hash(lstepf(gs, ls, I4, a).e, lstepf(gs, ls, I4, a).sz)) ∧ ¬ lstepf(gs, ls, I4, a).b | A Proof Obligation |
| step-I19-idle | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n0, ls.e, true) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I19, a) ∧ pcstepf(gs, ls, I19, a) = idle → (# gstepf(gs, ls, I19, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I19, a).ar)) ∧ (lstepf(gs, ls, I19, a).b ↔ (∃ n. n < # gstepf(gs, ls, I19, a).ar ∧ gstepf(gs, ls, I19, a).ar[n] = lstepf(gs, ls, I19, a).e)) | A Proof Obligation |
| step-M7-M8 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ pre(gs, ls, M7, a) ∧ pcstepf(gs, ls, M7, a) = M8 → (# gstepf(gs, ls, M7, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M7, a).ar)) ∧ lstepf(gs, ls, M7, a).n < # gstepf(gs, ls, M7, a).ar ∧ lstepf(gs, ls, M7, a).e ≠ ⊥ ∧ lstepf(gs, ls, M7, a).sz = # gstepf(gs, ls, M7, a).ar ∧ ( lstepf(gs, ls, M7, a).n0 < # gstepf(gs, ls, M7, a).ar ∧ lstepf(gs, ls, M7, a).n0 = get_hash(lstepf(gs, ls, M7, a).e, lstepf(gs, ls, M7, a).sz)) ∧ (∃ n. n < # gstepf(gs, ls, M7, a).ar ∧ gstepf(gs, ls, M7, a).ar[n] = lstepf(gs, ls, M7, a).e) ∧ allslotsfull(gstepf(gs, ls, M7, a).ar, lstepf(gs, ls, M7, a).n0, lstepf(gs, ls, M7, a).n, lstepf(gs, ls, M7, a).e, false) | A Proof Obligation |
| step-M11-M12 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ ls.e ≠ ls.e0) ∧ pre(gs, ls, M11, a) ∧ pcstepf(gs, ls, M11, a) = M12 → (# gstepf(gs, ls, M11, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M11, a).ar)) ∧ lstepf(gs, ls, M11, a).n < # gstepf(gs, ls, M11, a).ar ∧ lstepf(gs, ls, M11, a).e ≠ ⊥ ∧ lstepf(gs, ls, M11, a).sz = # gstepf(gs, ls, M11, a).ar ∧ ( lstepf(gs, ls, M11, a).n0 < # gstepf(gs, ls, M11, a).ar ∧ lstepf(gs, ls, M11, a).n0 = get_hash(lstepf(gs, ls, M11, a).e, lstepf(gs, ls, M11, a).sz)) ∧ ¬ lstepf(gs, ls, M11, a).b ∧ lstepf(gs, ls, M11, a).e ≠ lstepf(gs, ls, M11, a).e0 | A Proof Obligation |
| init-state-inv | (∃ n. n > 0 ∧ gs.ar = mkar(n, ⊥) ∧ pcf = (λ tid. idle)) ∧ (∀ tid. tid = lsf(tid).tid) ⊦ HashsetInv(gs, lsf, pcf) | A Proof Obligation |
| step-M1-M2 | ⊦ ((# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e ≠ ⊥) ∧ pre(gs, ls, M1, a) ∧ pcstepf(gs, ls, M1, a) = M2 → (# gstepf(gs, ls, M1, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M1, a).ar)) ∧ lstepf(gs, ls, M1, a).e ≠ ⊥ ∧ lstepf(gs, ls, M1, a).sz = # gstepf(gs, ls, M1, a).ar | A Proof Obligation |
| step-M10-M11 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ ls.e ≠ ls.e0 ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ pre(gs, ls, M10, a) ∧ pcstepf(gs, ls, M10, a) = M11 → (# gstepf(gs, ls, M10, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M10, a).ar)) ∧ lstepf(gs, ls, M10, a).n < # gstepf(gs, ls, M10, a).ar ∧ lstepf(gs, ls, M10, a).e ≠ ⊥ ∧ lstepf(gs, ls, M10, a).sz = # gstepf(gs, ls, M10, a).ar ∧ ( lstepf(gs, ls, M10, a).n0 < # gstepf(gs, ls, M10, a).ar ∧ lstepf(gs, ls, M10, a).n0 = get_hash(lstepf(gs, ls, M10, a).e, lstepf(gs, ls, M10, a).sz)) ∧ ¬ lstepf(gs, ls, M10, a).b ∧ lstepf(gs, ls, M10, a).e ≠ lstepf(gs, ls, M10, a).e0 | A Proof Obligation |
| stable-M4 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.n = ls.n0 ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.n = ls.n0 ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) | A Proof Obligation |
| stable-M13 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ (gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] ≠ ls.e) ∧ ls.e ≠ ls.e0 ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ (gs0.ar[ls.n] ≠ ⊥ ∧ gs0.ar[ls.n] ≠ ls.e) ∧ ls.e ≠ ls.e0 ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) | A Proof Obligation |
| step-M8-M9 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ (∃ n. n < # gs.ar ∧ gs.ar[n] = ls.e) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ pre(gs, ls, M8, a) ∧ pcstepf(gs, ls, M8, a) = M9 → (# gstepf(gs, ls, M8, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M8, a).ar)) ∧ lstepf(gs, ls, M8, a).n < # gstepf(gs, ls, M8, a).ar ∧ lstepf(gs, ls, M8, a).e ≠ ⊥ ∧ lstepf(gs, ls, M8, a).sz = # gstepf(gs, ls, M8, a).ar ∧ ( lstepf(gs, ls, M8, a).n0 < # gstepf(gs, ls, M8, a).ar ∧ lstepf(gs, ls, M8, a).n0 = get_hash(lstepf(gs, ls, M8, a).e, lstepf(gs, ls, M8, a).sz)) ∧ lstepf(gs, ls, M8, a).b ∧ (∃ n. n < # gstepf(gs, ls, M8, a).ar ∧ gstepf(gs, ls, M8, a).ar[n] = lstepf(gs, ls, M8, a).e) ∧ allslotsfull(gstepf(gs, ls, M8, a).ar, lstepf(gs, ls, M8, a).n0, lstepf(gs, ls, M8, a).n, lstepf(gs, ls, M8, a).e, false) | A Proof Obligation |
| stable-I2 | ⊦ (((# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar | A Proof Obligation |
| step-I5-I6 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I5, a) ∧ pcstepf(gs, ls, I5, a) = I6 → (# gstepf(gs, ls, I5, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I5, a).ar)) ∧ allslotsfull(gstepf(gs, ls, I5, a).ar, lstepf(gs, ls, I5, a).n0, lstepf(gs, ls, I5, a).n, lstepf(gs, ls, I5, a).e, false) ∧ lstepf(gs, ls, I5, a).n < # gstepf(gs, ls, I5, a).ar ∧ lstepf(gs, ls, I5, a).e ≠ ⊥ ∧ lstepf(gs, ls, I5, a).sz = # gstepf(gs, ls, I5, a).ar ∧ ( lstepf(gs, ls, I5, a).n0 < # gstepf(gs, ls, I5, a).ar ∧ lstepf(gs, ls, I5, a).n0 = get_hash(lstepf(gs, ls, I5, a).e, lstepf(gs, ls, I5, a).sz)) ∧ ¬ lstepf(gs, ls, I5, a).b | A Proof Obligation |
| stable-I17 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, true) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, true) ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b | A Proof Obligation |
| other-HashsetLInv | ⊦ HashsetGInv(gs) ∧ HashsetLInv(gs, ls, pc) ∧ ls.tid ≠ ls0.tid ∧ HashsetLInv(gs, ls0, pc0) ∧ lstep(gs, ls, pc, a, gs0, ls1, pc1) → HashsetLInv(gs0, ls0, pc0) | An Axiom |
| step-M2-M3 | ⊦ ((# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar) ∧ pre(gs, ls, M2, a) ∧ pcstepf(gs, ls, M2, a) = M3 → (# gstepf(gs, ls, M2, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M2, a).ar)) ∧ lstepf(gs, ls, M2, a).e ≠ ⊥ ∧ lstepf(gs, ls, M2, a).sz = # gstepf(gs, ls, M2, a).ar ∧ lstepf(gs, ls, M2, a).n0 < # gstepf(gs, ls, M2, a).ar ∧ lstepf(gs, ls, M2, a).n0 = get_hash(lstepf(gs, ls, M2, a).e, lstepf(gs, ls, M2, a).sz) | A Proof Obligation |
| stable-I11 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e ≠ ls.e0 ∧ (ls.e0 ≠ ⊥ ∧ ls.e0 = gs.ar[ls.n]) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.e ≠ ls.e0 ∧ (ls.e0 ≠ ⊥ ∧ ls.e0 = gs0.ar[ls.n]) ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b | A Proof Obligation |
| definedness-I11 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e ≠ ls.e0 ∧ (ls.e0 ≠ ⊥ ∧ ls.e0 = gs.ar[ls.n]) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I11, a) → ls.sz ≠ 0 | A Proof Obligation |
| stable-I8 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e = ls.e0 ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.e = gs.ar[ls.n] ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.e = ls.e0 ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) ∧ ls.e = gs0.ar[ls.n] ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b | A Proof Obligation |
| stable-I20 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n ≠ ls.n0 ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n ≠ ls.n0 ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b | A Proof Obligation |
| step-I7-I10 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I7, a) ∧ pcstepf(gs, ls, I7, a) = I10 → (# gstepf(gs, ls, I7, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I7, a).ar)) ∧ (lstepf(gs, ls, I7, a).e0 ≠ ⊥ → lstepf(gs, ls, I7, a).e0 = gstepf(gs, ls, I7, a).ar[lstepf(gs, ls, I7, a).n]) ∧ lstepf(gs, ls, I7, a).e ≠ lstepf(gs, ls, I7, a).e0 ∧ allslotsfull(gstepf(gs, ls, I7, a).ar, lstepf(gs, ls, I7, a).n0, lstepf(gs, ls, I7, a).n, lstepf(gs, ls, I7, a).e, false) ∧ lstepf(gs, ls, I7, a).n < # gstepf(gs, ls, I7, a).ar ∧ lstepf(gs, ls, I7, a).e ≠ ⊥ ∧ lstepf(gs, ls, I7, a).sz = # gstepf(gs, ls, I7, a).ar ∧ ( lstepf(gs, ls, I7, a).n0 < # gstepf(gs, ls, I7, a).ar ∧ lstepf(gs, ls, I7, a).n0 = get_hash(lstepf(gs, ls, I7, a).e, lstepf(gs, ls, I7, a).sz)) ∧ ¬ lstepf(gs, ls, I7, a).b | A Proof Obligation |
| step-idle-M1 | ⊦ (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ pre(gs, ls, idle, a) ∧ pcstepf(gs, ls, idle, a) = M1 → (# gstepf(gs, ls, idle, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, idle, a).ar)) ∧ lstepf(gs, ls, idle, a).e ≠ ⊥ | A Proof Obligation |
| step-I15-idle | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e = gs.ar[ls.n] ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.b) ∧ pre(gs, ls, I15, a) ∧ pcstepf(gs, ls, I15, a) = idle → (# gstepf(gs, ls, I15, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I15, a).ar)) ∧ (lstepf(gs, ls, I15, a).b ↔ (∃ n. n < # gstepf(gs, ls, I15, a).ar ∧ gstepf(gs, ls, I15, a).ar[n] = lstepf(gs, ls, I15, a).e)) | A Proof Obligation |
| stable-I14 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e = ls.e0 ∧ ls.e = gs.ar[ls.n] ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.e = ls.e0 ∧ ls.e = gs0.ar[ls.n] ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b | A Proof Obligation |
| step-I18-I19 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n0, ls.e, true) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I18, a) ∧ pcstepf(gs, ls, I18, a) = I19 → (# gstepf(gs, ls, I18, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I18, a).ar)) ∧ allslotsfull(gstepf(gs, ls, I18, a).ar, lstepf(gs, ls, I18, a).n0, lstepf(gs, ls, I18, a).n0, lstepf(gs, ls, I18, a).e, true) ∧ lstepf(gs, ls, I18, a).n < # gstepf(gs, ls, I18, a).ar ∧ lstepf(gs, ls, I18, a).e ≠ ⊥ ∧ lstepf(gs, ls, I18, a).sz = # gstepf(gs, ls, I18, a).ar ∧ ( lstepf(gs, ls, I18, a).n0 < # gstepf(gs, ls, I18, a).ar ∧ lstepf(gs, ls, I18, a).n0 = get_hash(lstepf(gs, ls, I18, a).e, lstepf(gs, ls, I18, a).sz)) ∧ ¬ lstepf(gs, ls, I18, a).b | A Proof Obligation |
| step-I6-I7 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I6, a) ∧ pcstepf(gs, ls, I6, a) = I7 → (# gstepf(gs, ls, I6, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I6, a).ar)) ∧ (lstepf(gs, ls, I6, a).e0 ≠ ⊥ → lstepf(gs, ls, I6, a).e0 = gstepf(gs, ls, I6, a).ar[lstepf(gs, ls, I6, a).n]) ∧ allslotsfull(gstepf(gs, ls, I6, a).ar, lstepf(gs, ls, I6, a).n0, lstepf(gs, ls, I6, a).n, lstepf(gs, ls, I6, a).e, false) ∧ lstepf(gs, ls, I6, a).n < # gstepf(gs, ls, I6, a).ar ∧ lstepf(gs, ls, I6, a).e ≠ ⊥ ∧ lstepf(gs, ls, I6, a).sz = # gstepf(gs, ls, I6, a).ar ∧ ( lstepf(gs, ls, I6, a).n0 < # gstepf(gs, ls, I6, a).ar ∧ lstepf(gs, ls, I6, a).n0 = get_hash(lstepf(gs, ls, I6, a).e, lstepf(gs, ls, I6, a).sz)) ∧ ¬ lstepf(gs, ls, I6, a).b | A Proof Obligation |
| stable-M10 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ ls.e ≠ ls.e0 ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs0.ar[ls.n]) ∧ ls.e ≠ ls.e0 ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) | A Proof Obligation |
| step-M3-M4 | ⊦ ((# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ pre(gs, ls, M3, a) ∧ pcstepf(gs, ls, M3, a) = M4 → (# gstepf(gs, ls, M3, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M3, a).ar)) ∧ lstepf(gs, ls, M3, a).n < # gstepf(gs, ls, M3, a).ar ∧ lstepf(gs, ls, M3, a).e ≠ ⊥ ∧ lstepf(gs, ls, M3, a).sz = # gstepf(gs, ls, M3, a).ar ∧ ( lstepf(gs, ls, M3, a).n0 < # gstepf(gs, ls, M3, a).ar ∧ lstepf(gs, ls, M3, a).n0 = get_hash(lstepf(gs, ls, M3, a).e, lstepf(gs, ls, M3, a).sz)) ∧ lstepf(gs, ls, M3, a).n = lstepf(gs, ls, M3, a).n0 ∧ allslotsfull(gstepf(gs, ls, M3, a).ar, lstepf(gs, ls, M3, a).n0, lstepf(gs, ls, M3, a).n, lstepf(gs, ls, M3, a).e, false) | A Proof Obligation |
| step-I17-I18 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, true) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I17, a) ∧ pcstepf(gs, ls, I17, a) = I18 → (# gstepf(gs, ls, I17, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I17, a).ar)) ∧ allslotsfull(gstepf(gs, ls, I17, a).ar, lstepf(gs, ls, I17, a).n0, lstepf(gs, ls, I17, a).n0, lstepf(gs, ls, I17, a).e, true) ∧ lstepf(gs, ls, I17, a).n < # gstepf(gs, ls, I17, a).ar ∧ lstepf(gs, ls, I17, a).e ≠ ⊥ ∧ lstepf(gs, ls, I17, a).sz = # gstepf(gs, ls, I17, a).ar ∧ ( lstepf(gs, ls, I17, a).n0 < # gstepf(gs, ls, I17, a).ar ∧ lstepf(gs, ls, I17, a).n0 = get_hash(lstepf(gs, ls, I17, a).e, lstepf(gs, ls, I17, a).sz)) ∧ ¬ lstepf(gs, ls, I17, a).b | A Proof Obligation |
| definedness-M13 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ (gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] ≠ ls.e) ∧ ls.e ≠ ls.e0 ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ pre(gs, ls, M13, a) → ls.sz ≠ 0 | A Proof Obligation |
| step-M14-M17 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, true)) ∧ pre(gs, ls, M14, a) ∧ pcstepf(gs, ls, M14, a) = M17 → (# gstepf(gs, ls, M14, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M14, a).ar)) ∧ lstepf(gs, ls, M14, a).n < # gstepf(gs, ls, M14, a).ar ∧ lstepf(gs, ls, M14, a).e ≠ ⊥ ∧ lstepf(gs, ls, M14, a).sz = # gstepf(gs, ls, M14, a).ar ∧ ( lstepf(gs, ls, M14, a).n0 < # gstepf(gs, ls, M14, a).ar ∧ lstepf(gs, ls, M14, a).n0 = get_hash(lstepf(gs, ls, M14, a).e, lstepf(gs, ls, M14, a).sz)) ∧ ¬ lstepf(gs, ls, M14, a).b ∧ allslotsfull(gstepf(gs, ls, M14, a).ar, lstepf(gs, ls, M14, a).n0, lstepf(gs, ls, M14, a).n, lstepf(gs, ls, M14, a).e, false) ∧ lstepf(gs, ls, M14, a).n ≠ lstepf(gs, ls, M14, a).n0 | A Proof Obligation |
| step-I16-I17 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ (gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] ≠ ls.e) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I16, a) ∧ pcstepf(gs, ls, I16, a) = I17 → (# gstepf(gs, ls, I16, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I16, a).ar)) ∧ allslotsfull(gstepf(gs, ls, I16, a).ar, lstepf(gs, ls, I16, a).n0, lstepf(gs, ls, I16, a).n, lstepf(gs, ls, I16, a).e, true) ∧ lstepf(gs, ls, I16, a).n < # gstepf(gs, ls, I16, a).ar ∧ lstepf(gs, ls, I16, a).e ≠ ⊥ ∧ lstepf(gs, ls, I16, a).sz = # gstepf(gs, ls, I16, a).ar ∧ ( lstepf(gs, ls, I16, a).n0 < # gstepf(gs, ls, I16, a).ar ∧ lstepf(gs, ls, I16, a).n0 = get_hash(lstepf(gs, ls, I16, a).e, lstepf(gs, ls, I16, a).sz)) ∧ ¬ lstepf(gs, ls, I16, a).b | A Proof Obligation |
| step-I10-I12 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ ls.e ≠ ls.e0 ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I10, a) ∧ pcstepf(gs, ls, I10, a) = I12 → (# gstepf(gs, ls, I10, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I10, a).ar)) ∧ allslotsfull(gstepf(gs, ls, I10, a).ar, lstepf(gs, ls, I10, a).n0, lstepf(gs, ls, I10, a).n, lstepf(gs, ls, I10, a).e, false) ∧ lstepf(gs, ls, I10, a).n < # gstepf(gs, ls, I10, a).ar ∧ lstepf(gs, ls, I10, a).e ≠ ⊥ ∧ lstepf(gs, ls, I10, a).sz = # gstepf(gs, ls, I10, a).ar ∧ ( lstepf(gs, ls, I10, a).n0 < # gstepf(gs, ls, I10, a).ar ∧ lstepf(gs, ls, I10, a).n0 = get_hash(lstepf(gs, ls, I10, a).e, lstepf(gs, ls, I10, a).sz)) ∧ ¬ lstepf(gs, ls, I10, a).b | A Proof Obligation |
| step-I7-I8 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I7, a) ∧ pcstepf(gs, ls, I7, a) = I8 → (# gstepf(gs, ls, I7, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I7, a).ar)) ∧ lstepf(gs, ls, I7, a).e = lstepf(gs, ls, I7, a).e0 ∧ allslotsfull(gstepf(gs, ls, I7, a).ar, lstepf(gs, ls, I7, a).n0, lstepf(gs, ls, I7, a).n, lstepf(gs, ls, I7, a).e, false) ∧ lstepf(gs, ls, I7, a).e = gstepf(gs, ls, I7, a).ar[lstepf(gs, ls, I7, a).n] ∧ lstepf(gs, ls, I7, a).n < # gstepf(gs, ls, I7, a).ar ∧ lstepf(gs, ls, I7, a).e ≠ ⊥ ∧ lstepf(gs, ls, I7, a).sz = # gstepf(gs, ls, I7, a).ar ∧ ( lstepf(gs, ls, I7, a).n0 < # gstepf(gs, ls, I7, a).ar ∧ lstepf(gs, ls, I7, a).n0 = get_hash(lstepf(gs, ls, I7, a).e, lstepf(gs, ls, I7, a).sz)) ∧ ¬ lstepf(gs, ls, I7, a).b | A Proof Obligation |
| stable-I7 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ (ls.e0 ≠ ⊥ → ls.e0 = gs.ar[ls.n]) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → (ls.e0 ≠ ⊥ → ls.e0 = gs0.ar[ls.n]) ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b | A Proof Obligation |
| step-M5-M18 | ⊦ ¬ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ pre(gs, ls, M5, a) ∧ pcstepf(gs, ls, M5, a) = M18) | A Proof Obligation |
| step-I20-I5 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n ≠ ls.n0 ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I20, a) ∧ pcstepf(gs, ls, I20, a) = I5 → (# gstepf(gs, ls, I20, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I20, a).ar)) ∧ allslotsfull(gstepf(gs, ls, I20, a).ar, lstepf(gs, ls, I20, a).n0, lstepf(gs, ls, I20, a).n, lstepf(gs, ls, I20, a).e, false) ∧ lstepf(gs, ls, I20, a).n < # gstepf(gs, ls, I20, a).ar ∧ lstepf(gs, ls, I20, a).e ≠ ⊥ ∧ lstepf(gs, ls, I20, a).sz = # gstepf(gs, ls, I20, a).ar ∧ ( lstepf(gs, ls, I20, a).n0 < # gstepf(gs, ls, I20, a).ar ∧ lstepf(gs, ls, I20, a).n0 = get_hash(lstepf(gs, ls, I20, a).e, lstepf(gs, ls, I20, a).sz)) ∧ ¬ lstepf(gs, ls, I20, a).b | A Proof Obligation |
| stable-I13 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ (gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] = ls.e0) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → (gs0.ar[ls.n] ≠ ⊥ ∧ gs0.ar[ls.n] = ls.e0) ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b | A Proof Obligation |
| step-M4-M5 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.n = ls.n0 ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ pre(gs, ls, M4, a) ∧ pcstepf(gs, ls, M4, a) = M5 → (# gstepf(gs, ls, M4, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M4, a).ar)) ∧ lstepf(gs, ls, M4, a).n < # gstepf(gs, ls, M4, a).ar ∧ lstepf(gs, ls, M4, a).e ≠ ⊥ ∧ lstepf(gs, ls, M4, a).sz = # gstepf(gs, ls, M4, a).ar ∧ ( lstepf(gs, ls, M4, a).n0 < # gstepf(gs, ls, M4, a).ar ∧ lstepf(gs, ls, M4, a).n0 = get_hash(lstepf(gs, ls, M4, a).e, lstepf(gs, ls, M4, a).sz)) ∧ ¬ lstepf(gs, ls, M4, a).b ∧ allslotsfull(gstepf(gs, ls, M4, a).ar, lstepf(gs, ls, M4, a).n0, lstepf(gs, ls, M4, a).n, lstepf(gs, ls, M4, a).e, false) | A Proof Obligation |
| step-I1-I2 | ⊦ ((# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e ≠ ⊥) ∧ pre(gs, ls, I1, a) ∧ pcstepf(gs, ls, I1, a) = I2 → (# gstepf(gs, ls, I1, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I1, a).ar)) ∧ lstepf(gs, ls, I1, a).e ≠ ⊥ ∧ lstepf(gs, ls, I1, a).sz = # gstepf(gs, ls, I1, a).ar | A Proof Obligation |
| stable-M9 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.b ∧ (∃ n. n < # gs.ar ∧ gs.ar[n] = ls.e) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false)) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ls.b ∧ (∃ n. n < # gs0.ar ∧ gs0.ar[n] = ls.e) ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) | A Proof Obligation |
| rely-HashsetLInv | ⊦ ls.tid ≠ tid0 ∧ HashsetGInv(gs) ∧ HashsetLInv(gs, ls, pc) ∧ lstep(gs, ls, pc, a, gs0, ls0, pc0) → HashsetRely(gs, tid0, gs0) | An Axiom |
| step-I8-I9 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e = ls.e0 ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.e = gs.ar[ls.n] ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I8, a) ∧ pcstepf(gs, ls, I8, a) = I9 → (# gstepf(gs, ls, I8, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I8, a).ar)) ∧ allslotsfull(gstepf(gs, ls, I8, a).ar, lstepf(gs, ls, I8, a).n0, lstepf(gs, ls, I8, a).n, lstepf(gs, ls, I8, a).e, false) ∧ lstepf(gs, ls, I8, a).e = gstepf(gs, ls, I8, a).ar[lstepf(gs, ls, I8, a).n] ∧ lstepf(gs, ls, I8, a).n < # gstepf(gs, ls, I8, a).ar ∧ lstepf(gs, ls, I8, a).e ≠ ⊥ ∧ lstepf(gs, ls, I8, a).sz = # gstepf(gs, ls, I8, a).ar ∧ ( lstepf(gs, ls, I8, a).n0 < # gstepf(gs, ls, I8, a).ar ∧ lstepf(gs, ls, I8, a).n0 = get_hash(lstepf(gs, ls, I8, a).e, lstepf(gs, ls, I8, a).sz)) ∧ lstepf(gs, ls, I8, a).b | A Proof Obligation |
| stable-I1 | ⊦ (((# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e ≠ ⊥) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → ls.e ≠ ⊥ | A Proof Obligation |
| stable-I16 | ⊦ ( ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ (gs.ar[ls.n] ≠ ⊥ ∧ gs.ar[ls.n] ≠ ls.e) ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ # gs0.ar ≠ 0 ∧ htok(gs0.ar)) ∧ rely(gs.ar, gs0.ar) → (gs0.ar[ls.n] ≠ ⊥ ∧ gs0.ar[ls.n] ≠ ls.e) ∧ allslotsfull(gs0.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs0.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs0.ar ∧ (ls.n0 < # gs0.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b | A Proof Obligation |
| step-M16-idle | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n0, ls.e, true)) ∧ pre(gs, ls, M16, a) ∧ pcstepf(gs, ls, M16, a) = idle → (# gstepf(gs, ls, M16, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, M16, a).ar)) ∧ (lstepf(gs, ls, M16, a).b → (∃ n. n < # gstepf(gs, ls, M16, a).ar ∧ gstepf(gs, ls, M16, a).ar[n] = lstepf(gs, ls, M16, a).e)) | A Proof Obligation |
| step-I14-I15 | ⊦ ( (# gs.ar ≠ 0 ∧ htok(gs.ar)) ∧ ls.e = ls.e0 ∧ ls.e = gs.ar[ls.n] ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false) ∧ ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b) ∧ pre(gs, ls, I14, a) ∧ pcstepf(gs, ls, I14, a) = I15 → (# gstepf(gs, ls, I14, a).ar ≠ 0 ∧ htok(gstepf(gs, ls, I14, a).ar)) ∧ lstepf(gs, ls, I14, a).e = gstepf(gs, ls, I14, a).ar[lstepf(gs, ls, I14, a).n] ∧ allslotsfull(gstepf(gs, ls, I14, a).ar, lstepf(gs, ls, I14, a).n0, lstepf(gs, ls, I14, a).n, lstepf(gs, ls, I14, a).e, false) ∧ lstepf(gs, ls, I14, a).n < # gstepf(gs, ls, I14, a).ar ∧ lstepf(gs, ls, I14, a).e ≠ ⊥ ∧ lstepf(gs, ls, I14, a).sz = # gstepf(gs, ls, I14, a).ar ∧ ( lstepf(gs, ls, I14, a).n0 < # gstepf(gs, ls, I14, a).ar ∧ lstepf(gs, ls, I14, a).n0 = get_hash(lstepf(gs, ls, I14, a).e, lstepf(gs, ls, I14, a).sz)) ∧ lstepf(gs, ls, I14, a).b | A Proof Obligation |