| # lpt1 = # avol, # lpt0 = # avol, isbuf ↔ isbuf1, lpt1[bleb1.leb] = mklp(m3, m5, lpf, m4), bleb0 = bleb1, keyset(gch) = gc-heap(lpt1, log0), log = log0, lpt = lpt0, m = m2, awbuf-inv(avol, bleb1), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(isbuf1, bleb1, lpt1, avol), bufs-log-only(bleb1, log0, lpt1), freelist-cons(lpt1, freelist), log-group-block(log0, lpt1), lpt-free-unref(lpt1), lpt-free-unref(lpt0), lpt-leb-size(lpt1), lpt-leb-size(lpt0), lpt-ram-flash(lpt1, lpt0, log0), bleb1.isbuf? ∧ ¬ isbuf1 → bleb1.leb < # avol ∧ # avol[bleb1.leb].data ≤ LEB_SIZE ∧ avol[bleb1.leb].mapped? ∧ m5 = # avol[bleb1.leb].data ∧ lpf ≠ LP_FREE ∧ is-aligned(# avol[bleb1.leb].data, 2 * NODE_HEADER_SIZE) ⊦ ⟪bleb := bleb0; awbuf_is_readonly#(adr, m2, log0, avol, lpt0, ns, bleb1, isbuf1; ; isbuf); awbuf_get_page_size#(adr, m2, log0, avol, lpt0, ns, bleb1, isbuf1; ; m1); if ¬ isbuf then if bleb.isbuf? then let m0 = lpt1[bleb.leb].size in if ¬ is-aligned(m0, m1) then let m = m1 - m0 % m1 in let buf = mkbuf(m) in {persistence_encode_padding_node#(; buf; err); if err = ESUCCESS then {awbuf_write_buf#(# buf, buf, adr, m2, log0, lpt0, ns, bleb1; avol, isbuf1; err); if err = ESUCCESS then lpt1[bleb.leb] := mklp(lpt1[bleb.leb].ref-size, lpt1[bleb.leb].size + m, lpt1[bleb.leb].flags, lpt1[bleb.leb].gcheapidx) else {debug#("persistence: flushing of LEB " + bleb.leb.toString + " failed"); lpt1[bleb.leb] := mklp(lpt1[bleb.leb].ref-size, LEB_SIZE, lpt1[bleb.leb].flags, lpt1[bleb.leb].gcheapidx); awbuf_enter_readonly#(adr, m2, log0, avol, lpt0, ns, bleb1; ; isbuf1)}} else {debug#("persistence: could not encode padding node"); awbuf_enter_readonly#(adr, m2, log0, avol, lpt0, ns, bleb1; ; isbuf1)}} else err := EROFS⟫ ( lpt-free-unref(lpt1) ∧ freelist-cons(lpt1, freelist) ∧ bin-heap-inv(gch, lpt1) ∧ keyset(gch) = gc-heap(lpt1, log0) ∧ bufs-log-only(bleb1, log0, lpt1) ∧ # lpt1 = # avol ∧ log-group-block(log0, lpt1) ∧ buf-ro-rw-mode(isbuf1, bleb1, lpt1, avol) ∧ lpt-leb-size(lpt1) ∧ lpt-ram-flash(lpt1, lpt0, log0) ∧ awbuf-inv(avol, bleb1) ∧ # lpt0 = # avol) |
# lpt0 = # avol, # lpt1 = # avol, isbuf ↔ isbuf1, lpt1[bleb1.leb] = mklp(m3, m5, lpf, m4), bleb0 = bleb1, keyset(gch) = gc-heap(lpt1, log0), log = log0, lpt = lpt0, m = m2, awbuf-inv(avol, bleb1), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(isbuf1, bleb1, lpt1, avol), bufs-log-only(bleb1, log0, lpt1), freelist-cons(lpt1, freelist), log-group-block(log0, lpt1), lpt-free-unref(lpt0), lpt-free-unref(lpt1), lpt-leb-size(lpt0), lpt-leb-size(lpt1), lpt-ram-flash(lpt1, lpt0, log0), bleb1.isbuf? ∧ ¬ isbuf1 → bleb1.leb < # avol ∧ # avol[bleb1.leb].data ≤ LEB_SIZE ∧ avol[bleb1.leb].mapped? ∧ m5 = # avol[bleb1.leb].data ∧ lpf ≠ LP_FREE ∧ is-aligned(# avol[bleb1.leb].data, 2 * NODE_HEADER_SIZE) ⊦ ⟪awbuf_is_readonly#(adr, m2, log0, avol, lpt0, ns, bleb1, isbuf1; ; isbuf); awbuf_get_page_size#(adr, m2, log0, avol, lpt0, ns, bleb1, isbuf1; ; m1); if ¬ isbuf then if bleb0.isbuf? then let m0 = lpt1[bleb0.leb].size in if ¬ is-aligned(m0, m1) then let m = m1 - m0 % m1 in let buf = mkbuf(m) in {persistence_encode_padding_node#(; buf; err); if err = ESUCCESS then {awbuf_write_buf#(# buf, buf, adr, m2, log0, lpt0, ns, bleb1; avol, isbuf1; err); if err = ESUCCESS then lpt1[bleb0.leb] := mklp(lpt1[bleb0.leb].ref-size, lpt1[bleb0.leb].size + m, lpt1[bleb0.leb].flags, lpt1[bleb0.leb].gcheapidx) else {debug#("persistence: flushing of LEB " + bleb0.leb.toString + " failed"); lpt1[bleb0.leb] := mklp(lpt1[bleb0.leb].ref-size, LEB_SIZE, lpt1[bleb0.leb].flags, lpt1[bleb0.leb].gcheapidx); awbuf_enter_readonly#(adr, m2, log0, avol, lpt0, ns, bleb1; ; isbuf1)}} else {debug#("persistence: could not encode padding node"); awbuf_enter_readonly#(adr, m2, log0, avol, lpt0, ns, bleb1; ; isbuf1)}} else err := EROFS⟫ ( lpt-free-unref(lpt1) ∧ freelist-cons(lpt1, freelist) ∧ bin-heap-inv(gch, lpt1) ∧ keyset(gch) = gc-heap(lpt1, log0) ∧ bufs-log-only(bleb1, log0, lpt1) ∧ # lpt1 = # avol ∧ log-group-block(log0, lpt1) ∧ buf-ro-rw-mode(isbuf1, bleb1, lpt1, avol) ∧ lpt-leb-size(lpt1) ∧ lpt-ram-flash(lpt1, lpt0, log0) ∧ awbuf-inv(avol, bleb1) ∧ # lpt0 = # avol)