[Imprint][Data Privacy Statement][E-Mail]



View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 130 from proof refine-add-gnds (previous step)

# lpt1 [buffered(log1.last).leb, mklp (lpt1[buffered(log1.last).leb].ref-size, lpt1[buffered(log1.last).leb].size + gndx0.flashsize, lpt1[buffered(log1.last).leb].flags, lpt1[buffered(log1.last).leb].gcheapidx) ] = # avol[m, mapped(avol[m].data + subarray(buf0, 0, gndx0.flashsize))], # lpt0 = # avol[m, mapped(avol[m].data + subarray(buf0, 0, gndx0.flashsize))], # gndx0 = # lax0, # buf0 = gndx0.flashsize, # lpt0 = # avol, # lpt1 = # avol, (elems nx ∪ dom gstore0) ++ n = dom gstore ∪ ginval, isbuf ↔ false, lpt1[n] = mklp(m1, # buf1, LP_GROUP_NODES, m2), gstore[n] = groupblock(gndx, lax, m1), avol[n] = mapped(buf1), err = ESUCCESS, err = err0, keyset(gch) = gc-heap (lpt1 [buffered(log1.last).leb, mklp (lpt1[buffered(log1.last).leb].ref-size, lpt1[buffered(log1.last).leb].size + gndx0.flashsize, lpt1[buffered(log1.last).leb].flags, lpt1[buffered(log1.last).leb].gcheapidx) ], log1), keyset(gch) = gc-heap(lpt1, nx + n '), log1 = nx + n ', m = buffered((nx + n ').last).leb, remove-refsize0(gstore0) = gstore0, remove-refsize0(istore0) = istore0, ginval ∩ elems nx = ∅, buffered(log1.last).isbuf?, buffered((nx + n ').last).isbuf?, avol[m].mapped?, buffered(log1.last).leb < # lpt1, n < # avol, ginval < # avol, m < # avol, abs-gstore(avol, lpt1, gstore, ginval), abs-istore(avol, lpt1, istore), abs-nodes(buf0, # buf1, gndx0, lax0, false), awbuf-inv(avol[m, mapped(avol[m].data + subarray(buf0, 0, gndx0.flashsize))], buffered(n)), awbuf-inv(avol, buffered(n)), bin-heap-inv (gch, lpt1 [buffered(log1.last).leb, mklp (lpt1[buffered(log1.last).leb].ref-size, lpt1[buffered(log1.last).leb].size + gndx0.flashsize, lpt1[buffered(log1.last).leb].flags, lpt1[buffered(log1.last).leb].gcheapidx) ]), bin-heap-inv(gch, lpt1), buf-ro-rw-mode (isbuf, buffered(n), lpt1 [buffered(log1.last).leb, mklp (lpt1[buffered(log1.last).leb].ref-size, lpt1[buffered(log1.last).leb].size + gndx0.flashsize, lpt1[buffered(log1.last).leb].flags, lpt1[buffered(log1.last).leb].gcheapidx) ], avol[m, mapped(avol[m].data + subarray(buf0, 0, gndx0.flashsize))]), buf-ro-rw-mode(false, buffered(n), lpt1, avol), bufs-log-only (buffered(n), log1, lpt1 [buffered(log1.last).leb, mklp (lpt1[buffered(log1.last).leb].ref-size, lpt1[buffered(log1.last).leb].size + gndx0.flashsize, lpt1[buffered(log1.last).leb].flags, lpt1[buffered(log1.last).leb].gcheapidx) ]), bufs-log-only(buffered(n), nx + n ', lpt1), flash-lpt-cons(lpt0, istore0, gstore0), freelist-cons (lpt1 [buffered(log1.last).leb, mklp (lpt1[buffered(log1.last).leb].ref-size, lpt1[buffered(log1.last).leb].size + gndx0.flashsize, lpt1[buffered(log1.last).leb].flags, lpt1[buffered(log1.last).leb].gcheapidx) ], freelist), freelist-cons(lpt1, freelist), inv(gstore \ ginval), inv(gstore0), inv(istore), inv(istore0), inv(groupblock(gndx, lax, m1)), log-group-block (log1, lpt1 [buffered(log1.last).leb, mklp (lpt1[buffered(log1.last).leb].ref-size, lpt1[buffered(log1.last).leb].size + gndx0.flashsize, lpt1[buffered(log1.last).leb].flags, lpt1[buffered(log1.last).leb].gcheapidx) ]), log-group-block(nx + n ', lpt1), lpt-free-unref (lpt1 [buffered(log1.last).leb, mklp (lpt1[buffered(log1.last).leb].ref-size, lpt1[buffered(log1.last).leb].size + gndx0.flashsize, lpt1[buffered(log1.last).leb].flags, lpt1[buffered(log1.last).leb].gcheapidx) ]), lpt-free-unref(lpt0), lpt-free-unref(lpt1), lpt-leb-size (lpt1 [buffered(log1.last).leb, mklp (lpt1[buffered(log1.last).leb].ref-size, lpt1[buffered(log1.last).leb].size + gndx0.flashsize, lpt1[buffered(log1.last).leb].flags, lpt1[buffered(log1.last).leb].gcheapidx) ]), lpt-leb-size(lpt0), lpt-leb-size(lpt1), lpt-ram-flash (lpt1 [buffered(log1.last).leb, mklp (lpt1[buffered(log1.last).leb].ref-size, lpt1[buffered(log1.last).leb].size + gndx0.flashsize, lpt1[buffered(log1.last).leb].flags, lpt1[buffered(log1.last).leb].gcheapidx) ], lpt0, log1), lpt-ram-flash(lpt1, lpt0, nx + n '), n ∈ gstore, # buf1 + gndx0.flashsize ≤ LEB_SIZE, 0 + gndx0.flashsize ≤ # buf0, istore0 ⊑ istore, isbuf1 → synced(avol), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟨pstate := journal(log1.last); apersistence_add_gnds#(gndx0, adr0, istore, istore0, ginval, gstore0, log1, m0, ns0; ax0, gstore, pstate, isbuf1; err1)⟩ ( abs-istore (avol[m, mapped(avol[m].data + subarray(buf0, 0, gndx0.flashsize))], lpt1 [buffered(log1.last).leb, mklp (lpt1[buffered(log1.last).leb].ref-size, lpt1[buffered(log1.last).leb].size + gndx0.flashsize, lpt1[buffered(log1.last).leb].flags, lpt1[buffered(log1.last).leb].gcheapidx) ], istore) ∧ abs-gstore (avol[m, mapped(avol[m].data + subarray(buf0, 0, gndx0.flashsize))], lpt1 [buffered(log1.last).leb, mklp (lpt1[buffered(log1.last).leb].ref-size, lpt1[buffered(log1.last).leb].size + gndx0.flashsize, lpt1[buffered(log1.last).leb].flags, lpt1[buffered(log1.last).leb].gcheapidx) ], gstore, ginval) ∧ ginval < # lpt1 [buffered(log1.last).leb, mklp (lpt1[buffered(log1.last).leb].ref-size, lpt1[buffered(log1.last).leb].size + gndx0.flashsize, lpt1[buffered(log1.last).leb].flags, lpt1[buffered(log1.last).leb].gcheapidx) ] ∧ (isbuf1 → synced(avol[m, mapped(avol[m].data + subarray(buf0, 0, gndx0.flashsize))])) ∧ pstate ≠ unbuffered ∧ (pstate = readonly ↔ isbuf) ∧ (pstate ≠ readonly → n = pstate.lnum) ∧ lax0.to-adr(n) = ax0 ∧ err = err1), nx + n ' = [], gndx0 = [], log1 = [], dups(nx), n ∈ ginval, n ∈ nx

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Rule argument

Additional information