This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| abs-istore-def | ⊦ abs-istore(avol, lpt, istore) ↔ (∀ n. (n < # lpt ∧ lpt[n].flags = LP_INDEX_NODES ↔ n ∈ istore) ∧ (n ∈ istore → abs-leb(avol[n], istore[n], lpt[n]) ∧ lpt[n].ref-size = istore[n].ref-size)) | An Axiom |
| abs-gstore-def | ⊦ abs-gstore(avol, lpt, gstore, ginval) ↔ (∀ n. (n < # lpt ∧ lpt[n].flags = LP_GROUP_NODES ↔ n ∈ gstore) ∧ (n ∈ gstore ∧ ¬ n ∈ ginval → abs-leb(avol[n], gstore[n], lpt[n])) ∧ (n ∈ gstore → lpt[n].ref-size = gstore[n].ref-size)) | An Axiom |
| remove-wbufs | ⊦ remove-wbufs(ns, lpt) = lpt.mapIndices(ns, λ lp. lp.size:= LEB_SIZE) | An Axiom |
| lpt-free-unref | ⊦ lpt-free-unref(lpt) ↔ (∀ n. n < # lpt ∧ lpt[n].flags = LP_FREE → lpt[n].ref-size = 0) | An Axiom |
| bufs-log-only | ⊦ bufs-log-only(bleb, nx, lpt) ↔ bleb = nobuffer ∨ bleb.leb < # lpt ∧ (nx ≠ [] ∧ bleb.leb = nx.last ∧ lpt[bleb.leb].flags = LP_GROUP_NODES ∨ lpt[bleb.leb].flags = LP_INDEX_NODES) | An Axiom |
| cleanup-lpt | ⊦ cleanup-lpt(lpt) = lpt.map(λ lp. (lp.ref-size = 0 ∧ lp.flags ≠ LP_FREE ⊃ mklp(0, 0, LP_FREE, lp.gcheapidx);lp)) | An Axiom |
| cleanup-lpt-rec | n < # lpt ⊦ cleanup-lpt(lpt, n + 1) = (lpt[n].ref-size = 0 ∧ lpt[n].flags ≠ LP_FREE ⊃ cleanup-lpt(lpt, n)[n, mklp(0, 0, LP_FREE, lpt[n].gcheapidx)];cleanup-lpt(lpt, n)) | An Axiom |
| cleanup-lpt-base | ⊦ cleanup-lpt(lpt, 0) = lpt | An Axiom |
| avol-cleanup-lpt-unchanged | ⊦ avol-cleanup-lpt-unchanged(avol0, avol1, lpt) ↔ # avol0 = # avol1 ∧ # avol0 = # lpt ∧ (∀ n. n < # avol0 ∧ (lpt[n].ref-size ≠ 0 ∨ lpt[n].flags = LP_FREE) → avol0[n] = avol1[n]) | An Axiom |
| replay-lpt-rec | n < # lpt ⊦ replay-lpt(lpt, nx, n + 1) = (lpt[n].flags = LP_FREE ∨ n ∈ nx ⊃ replay-lpt(lpt, nx, n) ;(lpt[n].flags = LP_INDEX_NODES ∧ lpt[n].ref-size ≠ 0 ⊃ replay-lpt(lpt, nx, n)[n, lpt[n].size:= LEB_SIZE] ;(lpt[n].ref-size = 0 ⊃ replay-lpt(lpt, nx, n)[n, mklp(0, 0, LP_FREE, lpt[n].gcheapidx)];replay-lpt(lpt, nx, n)) ) ) | An Axiom |
| replay-lpt-base | ⊦ replay-lpt(lpt, nx, 0) = lpt | An Axiom |
| avol-replay-lpt-unchanged | ⊦ avol-replay-lpt-unchanged(avol0, avol1, lpt, nx) ↔ # avol0 = # avol1 ∧ # avol0 = # lpt ∧ (∀ n. n < # avol0 ∧ (n ∈ nx ∨ lpt[n].ref-size ≠ 0 ∨ lpt[n].flags = LP_FREE) → avol0[n] = avol1[n]) | An Axiom |
| freelist-cons | ⊦ freelist-cons(lpt, freelist) ↔ ¬ dups(freelist) ∧ (∀ n. n < # lpt ∧ lpt[n].flags = LP_FREE ↔ n ∈ freelist) | An Axiom |
| replay-log | ⊦ replay-log(lpt, nx) = lpt.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx)) | An Axiom |
| gc-heap-rec | ⊦ n < # lpt → gc-heap(lpt, nx, n + 1) = gc-heap(lpt, nx, n) ∪ (¬ n ∈ nx ∧ lpt[n].flags = LP_GROUP_NODES ⊃ {key-index(lpt[n].ref-size, n)} ;∅) | An Axiom |
| gc-heap-base | ⊦ gc-heap(lpt, nx, 0) = ∅ | An Axiom |
| gc-heap | ⊦ gc-heap(lpt, nx) = gc-heap(lpt, nx, # lpt) | An Axiom |
| flash-lpt-cons | ⊦ flash-lpt-cons(lpt0, istore0, gstore0) ↔ lpt-free-unref(lpt0) ∧ (∀ n. n < # lpt0 → (n ∈ istore0 ↔ lpt0[n].flags = LP_INDEX_NODES ∧ lpt0[n].ref-size ≠ 0) ∧ (n ∈ gstore0 ↔ lpt0[n].flags = LP_GROUP_NODES ∧ lpt0[n].ref-size ≠ 0) ∧ (n ∈ istore0 → lpt0[n].ref-size = istore0[n].ref-size) ∧ (n ∈ gstore0 → lpt0[n].ref-size = gstore0[n].ref-size) ∧ (lpt0[n].flags = LP_FREE → lpt0[n].ref-size = 0)) | An Axiom |
| log-group-block | ⊦ log-group-block(nx, lpt) ↔ (∀ n. n ∈ nx → n < # lpt ∧ lpt[n].flags = LP_GROUP_NODES) | An Axiom |
| buf-ro-rw-mode | ⊦ buf-ro-rw-mode(boolvar, bleb, lpt, avol) ↔ bleb.isbuf? → bleb.leb < # lpt ∧ (boolvar ∧ lpt[bleb.leb].size = LEB_SIZE ∨ lpt[bleb.leb].size = # avol[bleb.leb].data) | An Axiom |
| lpt-leb-size | ⊦ lpt-leb-size(lpt) ↔ (∀ n. n < # lpt → lpt[n].size ≤ LEB_SIZE) | An Axiom |
| lpt-ram-flash | ⊦ lpt-ram-flash(lpt1, lpt0, nx) ↔ # lpt0 = # lpt1 ∧ (∀ n. n < # lpt1 ∧ lpt0[n].flags = LP_GROUP_NODES ∧ lpt1[n].flags = LP_GROUP_NODES ∧ ¬ n ∈ nx → lpt1[n].size = lpt0[n].size) | An Axiom |
| read-gblock-inv | ⊦ read-gblock-inv(m, n, ax, gndx, ax0, gndx0, buf, boolvar) ↔ (∃ gndx1, gndx2, lax1, lax2, buf0, buf1. ax = ax0 + lax1.to-adr(m) ∧ gndx = gndx0 + gndx1 ∧ buf = buf0 + buf1 ∧ # buf0 = n ∧ abs-nodes(buf0, gndx1, lax1, false) ∧ abs-nodes(buf1, # buf0, gndx2, lax2, true) ∧ (boolvar → gndx2 = [] ∧ lax2 = [])) | An Axiom |
| abs-gstore-avol-change-other | lpf ≠ LP_GROUP_NODES ⊦ lpt[n] = mklp(n0, n1, lpf, n2) → (abs-gstore(avol[n, aleb], lpt, gstore, ginval) ↔ abs-gstore(avol, lpt, gstore, ginval)) | A User Theorem |
| abs-gstore-cleanup-lpt | ⊦ abs-gstore(avol0, lpt, gstore, ginval) ∧ avol-cleanup-lpt-unchanged(avol0, avol1, lpt) ∧ dom remove-refsize0(gstore) ∩ ginval = ∅ → (¬ abs-gstore(avol1, cleanup-lpt(lpt), remove-refsize0(gstore), ∅) ↔ false) | A User Theorem |
| abs-gstore-crash | n = # lpt0, # avol0 = # lpt, # lpt0 = # lpt ⊦ abs-gstore(avol0, lpt, gstore, ginval) ∧ abs-istore(avol0, lpt, istore) ∧ avol1 ↓ avol0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ bufs-log-only(bleb, nx, lpt) ∧ synced(avol0) ∧ awbuf-inv(avol0, bleb) ∧ ginval < # lpt ∧ istore0 ⊑ istore ∧ dom istore ∩ elems nx = ∅ ∧ lpt-ram-flash(lpt, lpt0, nx) → abs-gstore(avol1, replay-lpt(replay-log(lpt0, nx), nx, n), crash(gstore, gstore0, ginval, nx), ginval) | A User Theorem |
| abs-gstore-idcircle | lpf ≠ LP_GROUP_NODES ⊦ # lpt = # avol0 ∧ n < # lpt ∧ id○(avol0, avol1, n) ∧ abs-gstore(avol0, lpt, gstore, ginval) ∧ lpt[n] = mklp(m0, m1, lpf, m2) → abs-gstore(avol1, lpt, gstore, ginval) | A User Theorem |
| abs-gstore-lpt-change-other | lpf ≠ LP_GROUP_NODES, lp.flags ≠ LP_GROUP_NODES ⊦ lpt[n] = mklp(n0, n1, lpf, n2) → (abs-gstore(avol, lpt[n, lp], gstore, ginval) ↔ abs-gstore(avol, lpt, gstore, ginval)) | A User Theorem |
| abs-gstore-reduce-write | # lpt = # avol ⊦ abs-gstore(avol, lpt, gstore, ginval) → ( abs-gstore(avol[n, aleb], lpt[n, lp], gstore[n, gblock], ginval) ↔ n < # lpt ∧ ((lpt[n].flags = LP_GROUP_NODES → lpt[n].ref-size = gstore[n].ref-size) → lp.ref-size = gblock.ref-size ∧ lp.flags = LP_GROUP_NODES) ∧ (¬ n ∈ ginval ∧ (lpt[n].flags = LP_GROUP_NODES → abs-leb(avol[n], gstore[n], lpt[n])) → abs-leb(aleb, gblock, lp))) | A User Theorem |
| abs-gstore-reduce-write-idcircle | # lpt = # avol0 ⊦ abs-gstore(avol0, lpt, gstore, ginval) ∧ id○(avol1, avol0, n) → ( abs-gstore(avol1, lpt[n, lp], gstore[n, gblock], ginval) ↔ n < # lpt ∧ ((lpt[n].flags = LP_GROUP_NODES → lpt[n].ref-size = gstore[n].ref-size) → lp.ref-size = gblock.ref-size ∧ lp.flags = LP_GROUP_NODES) ∧ (¬ n ∈ ginval ∧ (lpt[n].flags = LP_GROUP_NODES → abs-leb(avol0[n], gstore[n], lpt[n])) → abs-leb(avol1[n], gblock, lp))) | A User Theorem |
| abs-gstore-replay-lpt-unchanged | n = # lpt ⊦ avol-replay-lpt-unchanged(avol0, avol1, lpt, nx) → ( abs-gstore(avol1, replay-lpt(lpt, nx, n), crash(gstore, gstore0, ginval, nx), ginval) ↔ abs-gstore(avol0, replay-lpt(lpt, nx, n), crash(gstore, gstore0, ginval, nx), ginval)) | A User Theorem |
| abs-gstore-set-lebsize | n < # avol ⊦ lpt[n] = mklp(n0, n1, LP_GROUP_NODES, n2) ∧ abs-gstore(avol, lpt, gstore, ginval) → abs-gstore(avol, lpt[n, mklp(n0, LEB_SIZE, LP_GROUP_NODES, n2)], gstore, ginval) | A User Theorem |
| abs-gstore-set-refsize | ⊦ n ∈ gstore ∧ gstore[n] = groupblock(gndx, lax, n3) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ lpt[n] = mklp(n0, n1, LP_GROUP_NODES, n4) → abs-gstore(avol, lpt[n, mklp(m0, n1, LP_GROUP_NODES, n2)], gstore[n, groupblock(gndx, lax, m0)], ginval) | A User Theorem |
| abs-istore-avol-change-other | lpf ≠ LP_INDEX_NODES ⊦ lpt[n] = mklp(n0, n1, lpf, n2) → (abs-istore(avol[n, aleb], lpt, istore) ↔ abs-istore(avol, lpt, istore)) | A User Theorem |
| abs-istore-cleanup-lpt | ⊦ abs-istore(avol0, lpt, istore) ∧ avol-cleanup-lpt-unchanged(avol0, avol1, lpt) → (¬ abs-istore(avol1, cleanup-lpt(lpt), remove-refsize0(istore)) ↔ false) | A User Theorem |
| abs-istore-crash | n = # lpt0, # avol0 = # lpt, # lpt0 = # lpt ⊦ abs-istore(avol0, lpt, istore) ∧ avol1 ↓ avol0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ istore0 ⊑ istore ∧ synced(avol0) ∧ dom istore ∩ elems nx = ∅ → abs-istore(avol1, replay-lpt(replay-log(lpt0, nx), nx, n), remove-refsize0(crash(istore, istore0))) | A User Theorem |
| abs-istore-idcircle | lpf ≠ LP_INDEX_NODES ⊦ # lpt = # avol0 ∧ n < # lpt ∧ id○(avol0, avol1, n) ∧ abs-istore(avol0, lpt, istore) ∧ lpt[n] = mklp(m0, m1, lpf, m2) → abs-istore(avol1, lpt, istore) | A User Theorem |
| abs-istore-lpt-change-other | lpf ≠ LP_INDEX_NODES, lp.flags ≠ LP_INDEX_NODES ⊦ lpt[n] = mklp(n0, n1, lpf, n2) → (abs-istore(avol, lpt[n, lp], istore) ↔ abs-istore(avol, lpt, istore)) | A User Theorem |
| abs-istore-reduce-write | # lpt = # avol ⊦ abs-istore(avol, lpt, istore) → ( abs-istore(avol[n, aleb], lpt[n, lp], istore[n, iblock]) ↔ n < # lpt ∧ ((lpt[n].flags = LP_INDEX_NODES → lpt[n].ref-size = istore[n].ref-size) → lp.ref-size = iblock.ref-size ∧ lp.flags = LP_INDEX_NODES) ∧ ((lpt[n].flags = LP_INDEX_NODES → abs-leb(avol[n], istore[n], lpt[n])) → abs-leb(aleb, iblock, lp))) | A User Theorem |
| abs-istore-reduce-write-idcircle | # lpt = # avol0 ⊦ abs-istore(avol0, lpt, istore) ∧ id○(avol1, avol0, n) → ( abs-istore(avol1, lpt[n, lp], istore[n, iblock]) ↔ n < # lpt ∧ ((lpt[n].flags = LP_INDEX_NODES → lpt[n].ref-size = istore[n].ref-size) → lp.ref-size = iblock.ref-size ∧ lp.flags = LP_INDEX_NODES) ∧ ((lpt[n].flags = LP_INDEX_NODES → abs-leb(avol0[n], istore[n], lpt[n])) → abs-leb(avol1[n], iblock, lp))) | A User Theorem |
| abs-istore-replay-lpt-unchanged | n = # lpt ⊦ avol-replay-lpt-unchanged(avol0, avol1, lpt, nx) → (abs-istore(avol1, replay-lpt(lpt, nx, n), remove-refsize0(istore)) ↔ abs-istore(avol0, replay-lpt(lpt, nx, n), remove-refsize0(istore))) | A User Theorem |
| abs-istore-set-lebsize | n < # avol ⊦ lpt[n] = mklp(n0, n1, LP_INDEX_NODES, n2) ∧ abs-istore(avol, lpt, istore) → abs-istore(avol, lpt[n, mklp(n0, LEB_SIZE, LP_INDEX_NODES, n2)], istore) | A User Theorem |
| abs-istore-set-refsize | ⊦ n ∈ istore ∧ istore[n] = indexblock(indx, lax, n3) ∧ abs-istore(avol, lpt, istore) ∧ lpt[n] = mklp(n0, n1, LP_INDEX_NODES, n4) → abs-istore(avol, lpt[n, mklp(m0, n1, LP_INDEX_NODES, n2)], istore[n, indexblock(indx, lax, m0)]) | A User Theorem |
| abs-nodes-inv-flashsize | ⊦ abs-nodes(buf, gndx, lax, weak) → inv-flashsize(gndx, lax) | A User Theorem |
| abs-nodes-inv-flashsize-h | ⊦ abs-nodes(buf, m, gndx, lax, weak) → inv-flashsize(gndx, lax) | A User Theorem |
| avol-cleanup-lpt-unchanged-extract-right | lpt[n].ref-size ≠ 0 ∨ lpt[n].flags = LP_FREE ⊦ avol-cleanup-lpt-unchanged(avol0, avol1, lpt) ∧ n < # lpt → avol1[n] = avol0[n] | A User Theorem |
| avol-cleanup-lpt-unchanged-refl | ⊦ avol-cleanup-lpt-unchanged(avol, avol, lpt) ↔ # avol = # lpt | A User Theorem |
| avol-replay-lpt-unchanged-extract-right | n ∈ nx ∨ lpt[n].ref-size ≠ 0 ∨ lpt[n].flags = LP_FREE ⊦ avol-replay-lpt-unchanged(avol0, avol1, lpt, nx) ∧ n < # lpt → avol1[n] = avol0[n] | A User Theorem |
| avol-replay-lpt-unchanged-refl | ⊦ avol-replay-lpt-unchanged(avol, avol, lpt, nx) ↔ # avol = # lpt | A User Theorem |
| avol-replay-lpt-unchanged-size | ⊦ avol-replay-lpt-unchanged(avol0, avol1, lpt, nx) → # avol1 = # avol0 | A User Theorem |
| avol-replay-lpt-unchanged-write-right | n < # avol1 ⊦ avol-replay-lpt-unchanged(avol0, avol1, lpt, nx) → (avol-replay-lpt-unchanged(avol0, avol1[n, aleb], lpt, nx) ↔ ¬(aleb ≠ avol0[n] ∧ (n ∈ nx ∨ lpt[n].ref-size ≠ 0 ∨ lpt[n].flags = LP_FREE))) | A User Theorem |
| bin-heap-inv-cleanup-lpt | ⊦ bin-heap-inv(gch, cleanup-lpt(lpt)) ↔ bin-heap-inv(gch, lpt) | A User Theorem |
| bin-heap-inv-write-other | lpf0 ≠ LP_GROUP_NODES, n < # lpt ⊦ lpt[n] = mklp(m0, m1, lpf0, m2) ∧ keyset(gch) = gc-heap(lpt, nx) → (bin-heap-inv(gch, lpt[n, mklp(n0, n1, lpf1, n2)]) ↔ bin-heap-inv(gch, lpt)) | A User Theorem |
| bin-heap-inv-write-other-fields | n < # lpt ⊦ lpt[n] = mklp(m0, m1, lpf0, m2) → (bin-heap-inv(gch, lpt[n, mklp(n0, n1, lpf1, m2)]) ↔ bin-heap-inv(gch, lpt)) | A User Theorem |
| binheap-inv-remove-wbufs | ⊦ bin-heap-inv(gch, lpt) → bin-heap-inv(gch, remove-wbufs(ns, lpt)) | A User Theorem |
| buf-ro-rw-mode-id-idx | ⊦ id-idx(lpt0, lpt1) → (buf-ro-rw-mode(boolvar, bleb, lpt1, avol) ↔ buf-ro-rw-mode(boolvar, bleb, lpt0, avol)) | A User Theorem |
| buf-ro-rw-mode-leb-size | ⊦ buf-ro-rw-mode(true, buffered(n), lpt[n, mklp(m0, LEB_SIZE, lpf, m1)], avol) ↔ n < # lpt | A User Theorem |
| buf-ro-rw-mode-nobuffer | ⊦ buf-ro-rw-mode(boolvar, nobuffer, lpt, avol) | A User Theorem |
| buf-ro-rw-mode-switch | ⊦ buf-ro-rw-mode(boolvar, bleb, lpt, avol) → buf-ro-rw-mode(true, bleb, lpt, avol) | A User Theorem |
| buf-ro-rw-mode-write | n < # lpt, n < # avol ⊦ buf-ro-rw-mode(false, buffered(n), lpt[n, mklp(m0, m1, lpf, m2)], avol[n, mapped(buf)]) ↔ m1 = # buf | A User Theorem |
| buf-ro-rw-mode-write-lpt-other | ⊦ bleb ≠ buffered(n) → (buf-ro-rw-mode(boolvar, bleb, lpt[n, lp], avol) ↔ buf-ro-rw-mode(boolvar, bleb, lpt, avol)) | A User Theorem |
| buf-ro-rw-mode-write-other-fields | ⊦ lpt[n] = mklp(m0, n1, lpf0, m1) → (buf-ro-rw-mode(boolvar, bleb, lpt[n, mklp(n0, n1, lpf1, n2)], avol) ↔ buf-ro-rw-mode(boolvar, bleb, lpt, avol)) | A User Theorem |
| buf-ro-rw-mode-write-vol-other | ⊦ bleb ≠ buffered(n) → (buf-ro-rw-mode(boolvar, bleb, lpt, avol[n, aleb]) ↔ buf-ro-rw-mode(boolvar, bleb, lpt, avol)) | A User Theorem |
| bufs-log-only-empty | ⊦ bufs-log-only(nobuffer, nx, lpt) | A User Theorem |
| bufs-log-only-id-idx | ⊦ id-idx(lpt0, lpt1) → (bufs-log-only(bleb, nx, lpt1) ↔ bufs-log-only(bleb, nx, lpt0)) | A User Theorem |
| bufs-log-only-notfree | ⊦ lpt[n] = mklp(n0, n1, LP_FREE, n2) → ¬ bufs-log-only(buffered(n), freelist, lpt) | A User Theorem |
| bufs-log-only-rembuf | ⊦ bufs-log-only(bleb, nx, lpt) → bufs-log-only(nobuffer, nx, lpt) | A User Theorem |
| bufs-log-only-write-lpt-free | lpt[n].flags = LP_FREE ⊦ bufs-log-only(bleb, nx, lpt) → bufs-log-only(bleb, nx, lpt[n, lp]) | A User Theorem |
| bufs-log-only-write-lpt-same-flags | lpt[n].flags = lp.flags ⊦ bufs-log-only(bleb, nx, lpt) → bufs-log-only(bleb, nx, lpt[n, lp]) | A User Theorem |
| cleanup-lpt-n-at | m < n, n ≤ # lpt ⊦ cleanup-lpt(lpt, n)[m] = (lpt[m].ref-size = 0 ∧ lpt[m].flags ≠ LP_FREE ⊃ mklp(0, 0, LP_FREE, lpt[m].gcheapidx);lpt[m]) | A User Theorem |
| cleanup-lpt-n-read-above | n ≤ m, m < # lpt ⊦ cleanup-lpt(lpt, n)[m] = lpt[m] | A User Theorem |
| cleanup-lpt-n-size | n ≤ # lpt ⊦ # cleanup-lpt(lpt, n) = # lpt | A User Theorem |
| cleanup-lpt-size | ⊦ # cleanup-lpt(lpt) = # lpt | A User Theorem |
| cleanup-lpt-to-n | ⊦ cleanup-lpt(lpt, # lpt) = cleanup-lpt(lpt) | A User Theorem |
| free-unref-at | n < # lpt ⊦ lpt-free-unref(lpt) ∧ lpt[n] = mklp(n0, n1, LP_FREE, n2) → n0 = 0 | A User Theorem |
| freelist-cons-add | lpf ≠ LP_FREE ⊦ freelist-cons(lpt, freelist) ∧ n < # lpt ∧ lpt[n] = mklp(n0, n1, lpf, n2) → freelist-cons(lpt[n, mklp(m0, m1, LP_FREE, m3)], freelist + n ') | A User Theorem |
| freelist-cons-alloc | lpf ≠ LP_FREE ⊦ freelist-cons(lpt, n ' + freelist) → freelist-cons(lpt[n, mklp(m0, m1, lpf, m2)], freelist) | A User Theorem |
| freelist-cons-first-free | ⊦ freelist-cons(lpt, n ' + freelist) → n < # lpt ∧ lpt[n].flags = LP_FREE | A User Theorem |
| freelist-cons-remove-wbufs | ⊦ freelist-cons(lpt, freelist) → freelist-cons(remove-wbufs(ns, lpt), freelist) | A User Theorem |
| freelist-cons-write-lpt-other | ⊦ freelist-cons(lpt, freelist) ∧ lpt[n] = mklp(m0, m1, lpf, m2) → freelist-cons(lpt[n, mklp(n0, n1, lpf, n2)], freelist) | A User Theorem |
| gc-heap-allocate | n < # lpt ⊦ lpt[n] = mklp(m0, m1, LP_FREE, m2) → gc-heap(lpt[n, lp], nx + n ') = gc-heap(lpt, nx) | A User Theorem |
| gc-heap-allocate-h | n < # lpt ⊦ lpt[n] = mklp(m0, m1, LP_FREE, m2) ∧ n < # lpt ∧ m ≤ # lpt → gc-heap(lpt[n, lp], nx + n ', m) = gc-heap(lpt, nx, m) | A User Theorem |
| gc-heap-append-log | ⊦ lpt[n] = mklp(n0, n1, LP_GROUP_NODES, n2) ∧ ¬ n ∈ nx → gc-heap(lpt, n ' + nx) = gc-heap(lpt, nx) -- key-index(lpt[n].ref-size, n) | A User Theorem |
| gc-heap-append-log-h | ⊦ m ≤ # lpt ∧ lpt[n] = mklp(n0, n1, LP_GROUP_NODES, n2) ∧ ¬ n ∈ nx → gc-heap(lpt, n ' + nx, m) = gc-heap(lpt, nx, m) -- key-index(lpt[n].ref-size, n) | A User Theorem |
| gc-heap-fill-free | ⊦ gc-heap(fill(mklparray(n), mklp(n0, n1, LP_FREE, n2)), nx) = ∅ | A User Theorem |
| gc-heap-fill-free-h | ⊦ m ≤ n → gc-heap(fill(mklparray(n), mklp(n0, n1, LP_FREE, n2)), nx, m) = ∅ | A User Theorem |
| gc-heap-free | ⊦ n < # lpt ∧ lpt[n] = mklp(n0, n1, LP_GROUP_NODES, n2) ∧ ¬ n ∈ nx → gc-heap(lpt[n, mklp(m0, m1, LP_FREE, m2)], nx) = gc-heap(lpt, nx) -- key-index(n0, n) | A User Theorem |
| gc-heap-free-h | ⊦ n < m ∧ m ≤ # lpt ∧ lpt[n] = mklp(n0, n1, LP_GROUP_NODES, n2) ∧ ¬ n ∈ nx → gc-heap(lpt[n, mklp(m0, m1, LP_FREE, m2)], nx, m) = gc-heap(lpt, nx, m) -- key-index(n0, n) | A User Theorem |
| gc-heap-ididx-h | m ≤ # lpt1 ⊦ id-idx(lpt0, lpt1) → gc-heap(lpt1, nx, m) = gc-heap(lpt0, nx, m) | A User Theorem |
| gc-heap-in | ⊦ key-index(n0, n1) ∈ gc-heap(lpt, nx) ↔ n1 < # lpt ∧ ¬ n1 ∈ nx ∧ lpt[n1].ref-size = n0 ∧ lpt[n1].flags = LP_GROUP_NODES | A User Theorem |
| gc-heap-in-h | ⊦ n ≤ # lpt → (key-index(n0, n1) ∈ gc-heap(lpt, nx, n) ↔ n1 < n ∧ ¬ n1 ∈ nx ∧ lpt[n1].ref-size = n0 ∧ lpt[n1].flags = LP_GROUP_NODES) | A User Theorem |
| gc-heap-remove-wbufs | ⊦ gc-heap(remove-wbufs(ns, lpt), nx) = gc-heap(lpt, nx) | A User Theorem |
| gc-heap-remove-wbufs-h | ⊦ n ≤ # lpt → gc-heap(remove-wbufs(ns, lpt), nx, n) = gc-heap(lpt, nx, n) | A User Theorem |
| gc-heap-update | ⊦ n < # lpt ∧ lpt[n] = mklp(n0, n1, LP_GROUP_NODES, n2) ∧ ¬ n ∈ nx → gc-heap(lpt[n, mklp(m0, m1, LP_GROUP_NODES, m2)], nx) = (gc-heap(lpt, nx) -- key-index(n0, n)) ++ key-index(m0, n) | A User Theorem |
| gc-heap-update-h | ⊦ n < m ∧ m ≤ # lpt ∧ lpt[n] = mklp(n0, n1, LP_GROUP_NODES, n2) ∧ ¬ n ∈ nx → gc-heap(lpt[n, mklp(m0, m1, LP_GROUP_NODES, m2)], nx, m) = (gc-heap(lpt, nx, m) -- key-index(n0, n)) ++ key-index(m0, n) | A User Theorem |
| gc-heap-update-log | ⊦ n < # lpt ∧ lpt[n] = mklp(n0, n1, LP_GROUP_NODES, n2) ∧ n ∈ nx → gc-heap(lpt[n, mklp(m0, m1, LP_GROUP_NODES, m2)], nx) = gc-heap(lpt, nx) | A User Theorem |
| gc-heap-update-log-h | ⊦ n < m ∧ m ≤ # lpt ∧ lpt[n] = mklp(n0, n1, LP_GROUP_NODES, n2) ∧ n ∈ nx → gc-heap(lpt[n, mklp(m0, m1, LP_GROUP_NODES, m2)], nx, m) = gc-heap(lpt, nx, m) | A User Theorem |
| gc-heap-write-above | ⊦ n < # lpt ∧ m ≤ n → gc-heap(lpt[n, lp], nx, m) = gc-heap(lpt, nx, m) | A User Theorem |
| gc-heap-write-nochange | n < # lpt ⊦ lpt[n] = mklp(m0, m1, LP_GROUP_NODES, m2) → gc-heap(lpt[n, mklp(m0, n1, LP_GROUP_NODES, n2)], nx) = gc-heap(lpt, nx) | A User Theorem |
| gc-heap-write-nochange-h | ⊦ lpt[n] = mklp(m0, m1, LP_GROUP_NODES, m2) ∧ n < # lpt ∧ m ≤ # lpt → gc-heap(lpt[n, mklp(m0, n1, LP_GROUP_NODES, n2)], nx, m) = gc-heap(lpt, nx, m) | A User Theorem |
| gc-heap-write-other | lpf0 ≠ LP_GROUP_NODES, lpf1 ≠ LP_GROUP_NODES, n < # lpt ⊦ lpt[n] = mklp(m0, m1, lpf0, m2) → gc-heap(lpt[n, mklp(n0, n1, lpf1, n2)], nx) = gc-heap(lpt, nx) | A User Theorem |
| gc-heap-write-other-h | lpf0 ≠ LP_GROUP_NODES, lpf1 ≠ LP_GROUP_NODES ⊦ lpt[n] = mklp(m0, m1, lpf0, m2) ∧ n < # lpt ∧ m ≤ # lpt → gc-heap(lpt[n, mklp(n0, n1, lpf1, n2)], nx, m) = gc-heap(lpt, nx, m) | A User Theorem |
| id-idx-abs-gstore | ⊦ id-idx(lpt0, lpt1) → (abs-gstore(avol, lpt1, gstore, ginval) ↔ abs-gstore(avol, lpt0, gstore, ginval)) | A User Theorem |
| id-idx-abs-istore | ⊦ id-idx(lpt0, lpt1) → (abs-istore(avol, lpt1, istore) ↔ abs-istore(avol, lpt0, istore)) | A User Theorem |
| id-idx-freelist-cons | ⊦ id-idx(lpt0, lpt1) → (freelist-cons(lpt1, freelist) ↔ freelist-cons(lpt0, freelist)) | A User Theorem |
| id-idx-gcheap | ⊦ id-idx(lpt0, lpt1) → gc-heap(lpt1, nx) = gc-heap(lpt0, nx) | A User Theorem |
| id-idx-lpt-free-unref | ⊦ id-idx(lpt0, lpt1) → (lpt-free-unref(lpt1) ↔ lpt-free-unref(lpt0)) | A User Theorem |
| id-idx-write-both | ⊦ id-idx(lpt0, lpt1) → id-idx(lpt0[n, mklp(n0, n1, lpf, n2)], lpt1[n, mklp(n0, n1, lpf, m2)]) | A User Theorem |
| log-disjoint-istore | ⊦ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ elems nx ∩ ginval = ∅ ∧ abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) → dom istore ∩ elems nx = ∅ | A User Theorem |
| log-group-block-empty | ⊦ log-group-block([], lpt) | A User Theorem |
| log-group-block-id-idx | ⊦ id-idx(lpt0, lpt1) ∧ log-group-block(nx, lpt0) → log-group-block(nx, lpt1) | A User Theorem |
| log-group-block-remove-wbufs | ⊦ log-group-block(nx, lpt) → log-group-block(nx, remove-wbufs(ns, lpt)) | A User Theorem |
| log-group-block-write-at | n < # lpt ⊦ lpt[n] = mklp(n0, n1, LP_GROUP_NODES, n2) ∧ log-group-block(nx, lpt) → log-group-block(nx, lpt[n, mklp(m0, m1, LP_GROUP_NODES, m2)]) | A User Theorem |
| log-group-block-write-other | n < # lpt, lpf ≠ LP_GROUP_NODES ⊦ lpt[n] = mklp(n0, n1, lpf, n2) ∧ log-group-block(nx, lpt) → log-group-block(nx, lpt[n, lp]) | A User Theorem |
| lpt-free-unref-cleanup-lpt | ⊦ lpt-free-unref(cleanup-lpt(lpt)) ↔ lpt-free-unref(lpt) | A User Theorem |
| lpt-free-unref-remove-wbufs | ⊦ lpt-free-unref(remove-wbufs(ns, lpt)) ↔ lpt-free-unref(lpt) | A User Theorem |
| lpt-free-unref-replay-log | ⊦ lpt-free-unref(lpt) → lpt-free-unref(replay-log(lpt, nx)) | A User Theorem |
| lpt-free-unref-replay-lpt | n ≤ # lpt ⊦ lpt-free-unref(replay-lpt(lpt, nx, n)) ↔ lpt-free-unref(lpt) | A User Theorem |
| lpt-free-unref-write | ⊦ lpt-free-unref(lpt) → (lpt-free-unref(lpt[n, lp]) ↔ n < # lpt ∧ lp.flags = LP_FREE → lp.ref-size = 0) | A User Theorem |
| lpt-leb-size-at | n < # lpt ⊦ lpt[n] = mklp(n0, n1, lpf, n2) ∧ lpt-leb-size(lpt) → ¬ LEB_SIZE < n1 | A User Theorem |
| lpt-leb-size-cleanup | ⊦ lpt-leb-size(lpt) → lpt-leb-size(cleanup-lpt(lpt)) | A User Theorem |
| lpt-leb-size-id-idx | ⊦ id-idx(lpt0, lpt1) → (lpt-leb-size(lpt1) ↔ lpt-leb-size(lpt0)) | A User Theorem |
| lpt-leb-size-write | ⊦ lpt-leb-size(lpt) → (lpt-leb-size(lpt[n, lp]) ↔ # lpt ≤ n ∨ lp.size ≤ LEB_SIZE) | A User Theorem |
| lpt-ram-flash-allocate | ⊦ lpt-ram-flash(lpt1, lpt0, nx) → lpt-ram-flash(lpt1, lpt0, nx + n ') | A User Theorem |
| lpt-ram-flash-cleanup | ⊦ lpt-ram-flash(lpt1, lpt0, []) → lpt-ram-flash(cleanup-lpt(lpt1), lpt0, []) | A User Theorem |
| lpt-ram-flash-commit | ⊦ lpt-ram-flash(lpt, lpt, []) | A User Theorem |
| lpt-ram-flash-id-idx | ⊦ id-idx(lpt0, lpt1) → (lpt-ram-flash(lpt1, lpt, nx) ↔ lpt-ram-flash(lpt0, lpt, nx)) | A User Theorem |
| lpt-ram-flash-refl | ⊦ lpt-ram-flash(lpt, lpt, nx) | A User Theorem |
| lpt-ram-flash-write-allocate | ⊦ lpt-ram-flash(lpt[n, lp], lpt0, nx + n ') ↔ lpt-ram-flash(lpt, lpt0, nx + n ') | A User Theorem |
| lpt-ram-flash-write-log | n < # lpt ⊦ n ∈ nx → (lpt-ram-flash(lpt[n, lp], lpt0, nx) ↔ lpt-ram-flash(lpt, lpt0, nx)) | A User Theorem |
| lpt-ram-flash-write-log-buf | n < # lpt ⊦ bufs-log-only(buffered(n), nx, lpt) ∧ lpt-ram-flash(lpt, lpt0, nx) ∧ lpt[n] = mklp(n0, n1, lpf, n2) → lpt-ram-flash(lpt[n, mklp(m0, m1, lpf, m2)], lpt0, nx) | A User Theorem |
| lpt-ram-flash-write-non-group | n < # lpt, lpf ≠ LP_GROUP_NODES ⊦ lpt-ram-flash(lpt, lpt0, nx) → lpt-ram-flash(lpt[n, mklp(n0, n1, lpf, n2)], lpt0, nx) | A User Theorem |
| lpt-ram-flash-write-same | n < # lpt ⊦ lpt[n] = mklp(n0, m, lpf, n2) → (lpt-ram-flash(lpt[n, mklp(m0, m, lpf, m2)], lpt0, nx) ↔ lpt-ram-flash(lpt, lpt0, nx)) | A User Theorem |
| remove-wbufs-at | m < # lpt ⊦ remove-wbufs(ns, lpt)[m] = (m ∈ ns ⊃ lpt[m].size:= LEB_SIZE;lpt[m]) | A User Theorem |
| remove-wbufs-empty | ⊦ remove-wbufs(∅, lpt) = lpt | A User Theorem |
| remove-wbufs-rec | ¬ n ∈ ns ⊦ remove-wbufs(ns ++ n, lpt) = remove-wbufs(ns, lpt)[n, remove-wbufs(ns, lpt)[n].size:= LEB_SIZE] | A User Theorem |
| remove-wbufs-size | ⊦ # remove-wbufs(ns, lpt) = # lpt | A User Theorem |
| replay-log-append-one | ⊦ ¬ n ∈ nx → replay-log(lpt, nx + n ') = replay-log(lpt, nx)[n, mklp(lpt[n].ref-size, LEB_SIZE, LP_GROUP_NODES, lpt[n].gcheapidx)] | A User Theorem |
| replay-log-at | n < # lpt ⊦ n ∈ nx → replay-log(lpt, nx)[n] = mklp(lpt[n].ref-size, LEB_SIZE, LP_GROUP_NODES, lpt[n].gcheapidx) | A User Theorem |
| replay-log-at-other | n < # lpt ⊦ ¬ n ∈ nx → replay-log(lpt, nx)[n] = lpt[n] | A User Theorem |
| replay-log-base | ⊦ replay-log(lpt, []) = lpt | A User Theorem |
| replay-log-size | ⊦ # replay-log(lpt, nx) = # lpt | A User Theorem |
| replay-lpt-at | m < n, n ≤ # lpt ⊦ replay-lpt(lpt, nx, n)[m] = (lpt[m].flags = LP_FREE ∨ m ∈ nx ⊃ lpt[m] ;(lpt[m].flags = LP_INDEX_NODES ∧ lpt[m].ref-size ≠ 0 ⊃ lpt[m].size:= LEB_SIZE ;(lpt[m].ref-size = 0 ⊃ mklp(0, 0, LP_FREE, lpt[m].gcheapidx);lpt[m]) ) ) | A User Theorem |
| replay-lpt-at-above | n ≤ m, m < # lpt ⊦ replay-lpt(lpt, nx, n)[m] = lpt[m] | A User Theorem |
| replay-lpt-size | n ≤ # lpt ⊦ # replay-lpt(lpt, nx, n) = # lpt | A User Theorem |
| set-less-ar0 | ⊦ ginval < # lpt ∧ n ∈ ginval → n < # lpt | A User Theorem |
| set-less-ar1 | ⊦ ginval < # lpt ∧ n ∈ ginval → ¬ # lpt ≤ n | A User Theorem |