| gstore0[maxino] = groupblock(gndlist0, lax0, m, m0, m1, false), remove-refsize0(istore0) = istore0, remove-refsize0(gstore2) = gstore2, dom gstore2 ∪ elems nx0 = dom gstore0 ∪ ginval0, elems nx0 ∩ ginval0 = ∅, ax1 = ax0, gstore1 = gstore0, maxino ∈ nx0, btree-inv(rp, adr, gstore0 \ ginval0, istore, istore0, zh, ri0, fi2, ld1), inv(groupblock(gndlist0, lax0, m, m0, m1, false)), maxino ∈ gstore0, istore0 ⊑ istore, flushed(istore0), inv(istore0), inv(istore), btree-inv(rp, adr, gstore0 \ ginval0, istore, istore0, zh, ri, fi1, ld0), ri-inj(fi0), ri-inj(fi), gstore2 \ ginval0 lpt= gstore0 \ elems nx0, flushed(gstore0 \ (ginval0 ∪ elems nx0)), inv(gstore2), inv(gstore0 \ ginval0), btree-inv(rp, adr, gstore0 \ ginval0, istore, istore0, zh, fi, fi0, ld), m0 + gndlist.flashsize ≤ LEB_SIZE, ¬ maxino ∈ ginval0, ¬ dups(nx0), nx = nx0, ⌊err0⌋ ∨ err0 = ESUCCESS, ¬ dups(gstore1[maxino].ladrlist + lax), # lax ≤ # gndlist, inv-flashsize(prefixn(# lax, gndlist), lax), err0 = ESUCCESS ↔ # lax = # gndlist, ax = lax.to-adr(maxino), err = err0, gstore3 = gstore1[maxino, gstore1[maxino].gndlist:= (gstore1[maxino].gndlist + prefixn(# lax, gndlist))] [maxino, gstore1[maxino, gstore1[maxino].gndlist:= (gstore1[maxino].gndlist + prefixn(# lax, gndlist))][maxino] .ladrlist:= (gstore1[maxino, gstore1[maxino].gndlist:= (gstore1[maxino].gndlist + prefixn(# lax, gndlist))][maxino].ladrlist + lax) ], err = ESUCCESS, gstore = gstore3[maxino, gstore3[maxino].size:= (gstore3[maxino].size + gndlist.flashsize)], gstore[maxino].flushindex ≤ n, n ≤ # gstore[maxino].gndlist, ∃ ri, fi, ld. btree-inv(rp, adr, gstore[maxino, gstore[maxino].flushindex:= n] \ ginval0, istore, istore0, zh, ri, fi, ld), inv(gstore[maxino, gstore[maxino].flushindex:= n] \ ginval0), flushed(gstore[maxino, gstore[maxino].flushindex:= n] \ (ginval0 ∪ elems nx0)), dom gstore0 ∪ ginval0 = dom gstore[maxino, gstore[maxino].flushindex:= n] ∪ ginval0, gstore2 \ ginval0 lpt= gstore[maxino, gstore[maxino].flushindex:= n] \ elems nx0 ⊦ ⟨index+persistence_add_gnds#(maxino, gndlist, nx0; ax0, gstore0; err1)⟩ ( gstore0 = gstore[maxino, gstore[maxino].flushindex:= n] ∧ btree-inv(rp, adr, gstore[maxino, gstore[maxino].flushindex:= n] \ ginval0, istore, istore0, zh, fi, fi0, ld) ∧ ax = ax0 ∧ err = err1) |
# lax = # gndlist, elems nx0 ∩ ginval0 = ∅, dom gstore2 ∪ elems nx0 = dom gstore0 ∪ ginval0, remove-refsize0(gstore2) = gstore2, remove-refsize0(istore0) = istore0, gstore0[maxino] = groupblock(gndlist0, lax0, m, m0, m1, false), gstore = gstore0[maxino, groupblock(gndlist0 + gndlist, lax0 + lax, m, m0 + gndlist.flashsize, m1, false)], inv-flashsize(gndlist, lax), m0 + gndlist.flashsize ≤ LEB_SIZE, btree-inv(rp, adr, gstore0 \ ginval0, istore, istore0, zh, fi, fi0, ld), inv(gstore0 \ ginval0), inv(gstore2), flushed(gstore0 \ (ginval0 ∪ elems nx0)), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, gstore0 \ ginval0, istore, istore0, zh, ri, fi1, ld0), inv(istore), inv(istore0), flushed(istore0), istore0 ⊑ istore, maxino ∈ gstore0, btree-inv(rp, adr, gstore0 \ ginval0, istore, istore0, zh, ri0, fi2, ld1), maxino ∈ nx0, inv(groupblock(gndlist0, lax0, m, m0, m1, false)), gstore2 \ ginval0 lpt= gstore0 \ elems nx0, flushed(gstore0[maxino, groupblock(gndlist0 + gndlist, lax0 + lax, n, m0 + gndlist.flashsize, m1, false)] \ (ginval0 ∪ elems nx0)), inv(groupblock(gndlist0 + gndlist, lax0 + lax, n, m0 + gndlist.flashsize, m1, false)), btree-inv (rp, adr, gstore0[maxino, groupblock(gndlist0 + gndlist, lax0 + lax, n, m0 + gndlist.flashsize, m1, false)] \ ginval0, istore, istore0, zh, ri1, fi3, ld2), n ≤ # gndlist0 + # gndlist, m ≤ n, m ≤ # gndlist0 + # gndlist, ¬ dups(lax), ¬ dups(nx0), ¬ maxino ∈ ginval0 ⊦ ⟨index+persistence_add_gnds#(maxino, gndlist, nx0; ax0, gstore0; err1)⟩ ( gstore0 = gstore[maxino, gstore[maxino].flushindex:= n] ∧ btree-inv(rp, adr, gstore[maxino, gstore[maxino].flushindex:= n] \ ginval0, istore, istore0, zh, fi, fi0, ld) ∧ lax.to-adr(maxino) = ax0 ∧ ESUCCESS = err1)
Used simplifier rules: inv-nodups: ⊦ inv(groupblock(gndlist, lax, m0, m1, m2, boolvar)) → ¬ dups(lax); from specification ablock-store-inv[group-store]%inv-nodups-app-left: ⊦ inv(groupblock(gndlist, lax0 + lax1, m0, m1, m2, boolvar)) → ¬ dups(lax0); from specification ablock-store-inv[group-store]%ler: ⊦ m ≤ m; from specification nat%upd-06: ⊦ groupblock(gndlist, lax, m, m0, m1, boolvar).flushindex:= m2 = groupblock(gndlist, lax, m2, m0, m1, boolvar); from specification ablock[group-store]%sel-06: ⊦ groupblock(gndlist, lax, m, m0, m1, boolvar).flushindex = m; from specification ablock[group-store]%upd-07: ⊦ groupblock(gndlist, lax, m, m0, m1, boolvar).size:= m3 = groupblock(gndlist, lax, m, m3, m1, boolvar); from specification ablock[group-store]%sel-07: ⊦ groupblock(gndlist, lax, m, m0, m1, boolvar).size = m0; from specification ablock[group-store]%upd-05: ⊦ groupblock(gndlist, lax, m, m0, m1, boolvar).ladrlist:= lax0 = groupblock(gndlist, lax0, m, m0, m1, boolvar); from specification ablock[group-store]%sel-05: ⊦ groupblock(gndlist, lax, m, m0, m1, boolvar).ladrlist = lax; from specification ablock[group-store]%upd-04: ⊦ groupblock(gndlist, lax, m, m0, m1, boolvar).gndlist:= gndlist0 = groupblock(gndlist0, lax, m, m0, m1, boolvar); from specification ablock[group-store]%sel-04: ⊦ groupblock(gndlist, lax, m, m0, m1, boolvar).gndlist = gndlist; from specification ablock[group-store]%a: ⊦ (lax + lax0) + lax1 = lax + lax0 + lax1; from specification list[laddress-list]%a: ⊦ ¬ dups(lax + lax0) → ¬ dups(lax) ∧ ¬ dups(lax0); (forward) from specification list-dup[laddress-list]%fwd-inv-gblock-rem: ⊦ inv(gstore \ ginval) ∧ n ∈ gstore ∧ ¬ n ∈ ginval ∧ gstore[n] = gblock → inv(gblock); (forward) from specification apersistence-base%let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat%esuccess: ⊦ ¬ ⌊ESUCCESS⌋ ; from specification error-class%lpteq-write-left-diff-notin: ⊦ n ∈ nx → ( gstore0 lpt= gstore1[n, gblock] \ elems nx ↔ gstore0 lpt= gstore1 \ elems nx); from specification apersistence-base%inv-reduce: ⊦ inv(gstore \ ns) → (inv(gstore[n, gblock] \ ns) ↔ n ∈ ns ∨ inv(gblock)); from specification ablock-store-inv[group-store]%a: ⊦ (gndlist + gndlist0) + gndlist1 = gndlist + gndlist0 + gndlist1; from specification list[group-store]%len: ⊦ #(gndlist + gndlist0) = # gndlist + # gndlist0; from specification list[group-store]%updsel-09: ⊦ (gblock.gndlist:= gndlist).gndlist = gndlist; from specification ablock[group-store]%updsel-26: ⊦ (gblock.ladrlist:= lax).gndlist = gblock.gndlist; from specification ablock[group-store]%updsel-11: ⊦ (gblock.size:= m0).gndlist = gblock.gndlist; from specification ablock[group-store]%updsel-13: ⊦ (gblock.gndlist:= gndlist).flushindex = gblock.flushindex; from specification ablock[group-store]%updsel-33: ⊦ (gblock.ladrlist:= lax).flushindex = gblock.flushindex; from specification ablock[group-store]%updsel-15: ⊦ (gblock.size:= m0).flushindex = gblock.flushindex; from specification ablock[group-store]%dom-add-in: ⊦ n ∈ gstore → dom gstore ++ n = dom gstore; from specification store+set[group-store-ablock-store-nat-store]%dom-ins: ⊦ dom gstore[n, gblock] = dom gstore ++ n; from specification store+set[group-store-ablock-store-nat-store]%irreflexivity: ⊦ ¬ n < n; from specification oelem[nat-set]%lels-01: ⊦ ¬ m ≤ n ↔ n < m; from specification nat%updsel-06: ⊦ (gblock.gndlist:= gndlist).size = gblock.size; from specification ablock[group-store]%updsel-31: ⊦ (gblock.ladrlist:= lax).size = gblock.size; from specification ablock[group-store]%insins: ⊦ gstore[n, gblock][n, gblock0] = gstore[n, gblock0]; from specification store[group-store-ablock-store-nat-store]%updsel-28: ⊦ (gblock.gndlist:= gndlist).ladrlist = gblock.ladrlist; from specification ablock[group-store]%At-same: ⊦ gstore[n, gblock][n] = gblock; from specification store[group-store-ablock-store-nat-store]%prefixn-fulln: # gndlist ≤ m ⊦ prefixn(m, gndlist) = gndlist; from specification list-prefixn[group-store]%anti: ⊦ m ≤ n → (n ≤ m ↔ m = n); from specification nat