| # avol0 = # avol2, # lpt1 = # avol2, # buf = EB_PAGE_SIZE, rofs ↔ rofs2, adr = adr2, adr0 = adr3, adr2 = adr1, adr3 = adr4, avol = avol1, bleb = bleb2, log = plog3, lpt = lpt2, lpt0 = lpt3, lpt2 = lpt1, lpt3 = lpt4, m = m9, m0 = m1, m1 = m4, m10 = m6, m4 = m5, m9 = m8, ns = ns2, ns0 = ns3, ns2 = ns1, ns3 = ns4, plog = plog0, plog0 = plog1, wbuf = wbuf0, abs(avol2, bleb0, mkwbuf(buf, m2, m3), avol0, rofs0), awbuf-inv(avol2, bleb0), ebm-vol-inv(avol0), avol0 ⊆ avol1, bleb0 ≠ nobuffer → bleb0.leb < # avol2 ∧ wbuf-cons(mkwbuf(buf, m2, m3), avol0[bleb0.leb], rofs0), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪err := err0; if err = ESUCCESS then adr0 := adr, m0 := m, log := plog, lpt0 := lpt, ns0 := ns else avol := ?, adr := ?, m := ?, plog := ?, lpt := ?, adr0 := ?, m0 := ?, log := ?, lpt0 := ?, ns0 := ?, ns := ?; if err = ESUCCESS then {apersistence_io_get_page_size#(adr, m, plog, avol, lpt, ns; ; m10); bleb := nobuffer; wbuf.content := mkbuf(m10); rofs := false}⟫ ( ( err = ESUCCESS → (∃ avol0. avol0 ↓ avol2 ∧ ⟨awbuf_recover#(; adr4, m5, ns4, plog3, lpt4, adr1, m8, plog1, lpt1, ns1, avol0; bleb0, rofs0, err1)⟩ ( abs(avol0, bleb, wbuf, avol, rofs) ∧ bleb0 = bleb ∧ adr1 = adr ∧ m8 = m ∧ plog1 = plog ∧ lpt1 = lpt ∧ ns1 = ns ∧ (rofs0 ↔ rofs) ∧ adr0 = adr4 ∧ m0 = m5 ∧ ns0 = ns4 ∧ log = plog3 ∧ lpt0 = lpt4 ∧ ESUCCESS = err1))) ∧ ( err ≠ ESUCCESS → (∀ adr, m, plog, avol, lpt, ns, bleb, rofs. ⟨awbuf_recover#(; adr4, m5, ns4, plog3, lpt4, adr5, m7, plog4, lpt5, ns5, avol3; bleb3, rofs3, err1)⟩ ( adr = adr5 ∧ m = m7 ∧ plog = plog4 ∧ avol = avol3 ∧ lpt = lpt5 ∧ ns = ns5 ∧ bleb = bleb3 ∧ (rofs ↔ rofs3) ∧ adr0 = adr4 ∧ m0 = m5 ∧ ns0 = ns4 ∧ log = plog3 ∧ lpt0 = lpt4 ∧ err = err1)))) |
# buf = EB_PAGE_SIZE, # lpt1 = # avol2, # avol0 = # avol2, rofs ↔ rofs2, adr = adr2, adr0 = adr3, adr2 = adr1, adr3 = adr4, avol = avol1, bleb = bleb2, err = err0, log = plog3, lpt = lpt2, lpt0 = lpt3, lpt2 = lpt1, lpt3 = lpt4, m = m9, m0 = m1, m1 = m4, m10 = m6, m4 = m5, m9 = m8, ns = ns2, ns0 = ns3, ns2 = ns1, ns3 = ns4, plog = plog0, plog0 = plog1, wbuf = wbuf0, abs(avol2, bleb0, mkwbuf(buf, m2, m3), avol0, rofs0), awbuf-inv(avol2, bleb0), ebm-vol-inv(avol0), avol0 ⊆ avol1, bleb0 ≠ nobuffer → bleb0.leb < # avol2 ∧ wbuf-cons(mkwbuf(buf, m2, m3), avol0[bleb0.leb], rofs0), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪if err = ESUCCESS then adr0 := adr, m0 := m, log := plog, lpt0 := lpt, ns0 := ns else avol := ?, adr := ?, m := ?, plog := ?, lpt := ?, adr0 := ?, m0 := ?, log := ?, lpt0 := ?, ns0 := ?, ns := ?; if err = ESUCCESS then {apersistence_io_get_page_size#(adr, m, plog, avol, lpt, ns; ; m10); bleb := nobuffer; wbuf.content := mkbuf(m10); rofs := false}⟫ ( ( err = ESUCCESS → (∃ avol0. avol0 ↓ avol2 ∧ ⟨awbuf_recover#(; adr4, m5, ns4, plog3, lpt4, adr1, m8, plog1, lpt1, ns1, avol0; bleb0, rofs0, err1)⟩ ( abs(avol0, bleb, wbuf, avol, rofs) ∧ bleb0 = bleb ∧ adr1 = adr ∧ m8 = m ∧ plog1 = plog ∧ lpt1 = lpt ∧ ns1 = ns ∧ (rofs0 ↔ rofs) ∧ adr0 = adr4 ∧ m0 = m5 ∧ ns0 = ns4 ∧ log = plog3 ∧ lpt0 = lpt4 ∧ ESUCCESS = err1))) ∧ ( err ≠ ESUCCESS → (∀ adr, m, plog, avol, lpt, ns, bleb, rofs. ⟨awbuf_recover#(; adr4, m5, ns4, plog3, lpt4, adr5, m7, plog4, lpt5, ns5, avol3; bleb3, rofs3, err1)⟩ ( adr = adr5 ∧ m = m7 ∧ plog = plog4 ∧ avol = avol3 ∧ lpt = lpt5 ∧ ns = ns5 ∧ bleb = bleb3 ∧ (rofs ↔ rofs3) ∧ adr0 = adr4 ∧ m0 = m5 ∧ ns0 = ns4 ∧ log = plog3 ∧ lpt0 = lpt4 ∧ err = err1))))