| # lpt0 = # avol, # lpt1 = # avol, gstore1[log1.last] = groupblock(gndx0, lax0, m0), avol[log1.last] = mapped(buf), lpt1[log1.last] = mklp(m0, m1, LP_GROUP_NODES, m2), ax = [], err0 = ESUCCESS, gstore = gstore1[pstate.lnum, gstore1[pstate.lnum].gndlist:= gstore1[pstate.lnum].gndlist] [pstate.lnum, gstore1[pstate.lnum, gstore1[pstate.lnum].gndlist:= gstore1[pstate.lnum].gndlist][pstate.lnum] .ladrlist:= gstore1[pstate.lnum, gstore1[pstate.lnum].gndlist:= gstore1[pstate.lnum].gndlist][pstate.lnum].ladrlist ], keyset(gch) = gc-heap(lpt1, log1), pstate = journal(log1.last), remove-refsize0(gstore0) = gstore0, remove-refsize0(istore1) = istore1, elems log1 ∩ ginval = ∅, dom gstore0 ∪ elems log1 = dom gstore1 ∪ ginval, ginval < # avol, log1.last < # avol, abs-gstore(avol, lpt1, gstore1, ginval), abs-istore(avol, lpt1, istore2), awbuf-inv(avol, buffered(log1.last)), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(false, buffered(log1.last), lpt1, avol), bufs-log-only(buffered(log1.last), log1, lpt1), flash-lpt-cons(lpt0, istore1, gstore0), freelist-cons(lpt1, freelist), inv(gstore1 \ ginval), inv(gstore0), inv(istore2), inv(istore1), inv(groupblock(gndx0, lax0, m0)), log-group-block(log1, lpt1), lpt-free-unref(lpt0), lpt-free-unref(lpt1), lpt-leb-size(lpt0), lpt-leb-size(lpt1), lpt-ram-flash(lpt1, lpt0, log1), log1.last ∈ gstore1, pstate.lnum ∈ gstore1[pstate.lnum, gstore1[pstate.lnum].gndlist:= gstore1[pstate.lnum].gndlist], pstate.lnum ∈ gstore1, istore1 ⊑ istore2, isbuf1 → synced(avol), pstate.index? ∨ pstate.journal? ⊦ ⟨isbuf1 := ?⟩ ( abs-gstore(avol, lpt1, gstore, ginval) ∧ (isbuf1 → synced(avol)) ∧ pstate ≠ unbuffered ∧ pstate ≠ readonly ∧ log1.last = pstate.lnum ∧ [] = ax ∧ ESUCCESS = err0), log1 = [], dups(log1), log1.last ∈ ginval |
Used simplifier rules: fwd-in-gstore-lpt: ⊦ n ∈ gstore ∧ abs-gstore(avol, lpt, gstore, ginval) → n < # lpt ∧ lpt[n].ref-size = gstore[n].ref-size ∧ lpt[n].flags = LP_GROUP_NODES;% ⊦ journal(m).lnum = m; (s)% ⊦ n ∈ gstore[n, gblock]; (s)% ⊦ ¬ journal(m).index?; (s)% ⊦ journal(m).journal?; (s)% ⊦ gstore[n, gblock][n] = gblock; (s)% ⊦ (gblock.gndlist:= gndx).ladrlist = gblock.ladrlist; (s)% ⊦ gstore[n, gblock][n, gblock0] = gstore[n, gblock0]; (s)% ⊦ unbuffered ≠ journal(m); (s)% ⊦ readonly ≠ journal(m); (s)%int-a: ⊦ (ns ∩ ns0) ∩ ns1 = ns ∩ ns0 ∩ ns1; from specification set-union[nat-set]%int-c: ⊦ ns ∩ ns0 = ns0 ∩ ns; from specification set-union[nat-set]%una: ⊦ (ns ∪ ns0) ∪ ns1 = ns ∪ ns0 ∪ ns1; from specification set-union[nat-set]%unc: ⊦ ns ∪ ns0 = ns0 ∪ ns; from specification set-union[nat-set]%fwd-in-gstore-loghead: ⊦ nx ≠ [] ∧ ginval ∩ elems nx = ∅ ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval → nx.last ∈ gstore; (forward) from specification apersistence-base%fwd-inv-loghead: ⊦ nx ≠ [] ∧ inv(gstore \ ginval) ∧ ginval ∩ elems nx = ∅ ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval → inv(gstore[nx.last]); (forward) from specification apersistence-base% ⊦ groupblock(gndx, lax, m).gndlist = gndx; (s)%⊦ groupblock(gndx, lax, m).gndlist:= gndx0 = groupblock(gndx0, lax, m); (s)% ⊦ groupblock(gndx, lax, m).ladrlist = lax; (s)%⊦ groupblock(gndx, lax, m).ladrlist:= lax0 = groupblock(gndx, lax0, m); (s)% ⊦ gstore[n] = gblock ∧ n ∈ gstore → gstore[n, gblock] = gstore; (s)