[Imprint][Data Privacy Statement][E-Mail]
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,
enrich
apersistence-base
,
awbuf-inv
,
lp-array
,
gc-heap-rename
,
encoding-index-node
,
encoding-group-node
with
functions remove-wbufs : nat-set × lp-array → lp-array;
cleanup-lpt : lp-array → lp-array;
cleanup-lpt : lp-array × nat → lp-array;
replay-lpt : lp-array × nat-list × nat → lp-array;
replay-log : lp-array × nat-list → lp-array;
gc-heap : lp-array × nat-list × nat → gc-heap-set;
gc-heap : lp-array × nat-list → gc-heap-set;
predicates abs-istore : avolume × lp-array × index-store;
abs-gstore : avolume × lp-array × group-store × nat-set;
lpt-leb-size : lp-array;
lpt-free-unref : lp-array;
freelist-cons : lp-array × nat-list;
bufs-log-only : bufleb × nat-list × lp-array;
buf-ro-rw-mode : bool × bufleb × lp-array × avolume;
avol-cleanup-lpt-unchanged : avolume × avolume × lp-array;
avol-replay-lpt-unchanged : avolume × avolume × lp-array × nat-list;
flash-lpt-cons : lp-array × index-store × group-store;
log-group-block : nat-list × lp-array;
lpt-ram-flash : lp-array × lp-array × nat-list;
read-gblock-inv : nat × nat × address-list × group-node-list × address-list × group-node-list × buffer × bool;
variables freelist : nat-list;
gch : binheap;
axioms replay-lpt-base : ⊦ replay-lpt(lpt, nx, 0) = lpt;
used for: s, ls;
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))
)
);
used for: s, ls;
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]);
used for: ls;
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]);
used for: ls;
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));
used for: ls;
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));
used for: ls;
remove-wbufs : ⊦ remove-wbufs(ns, lpt) = lpt.mapIndices(ns, λ lp. lp.size:= LEB_SIZE);
used for: ls;
lpt-free-unref : ⊦ lpt-free-unref(lpt) ↔ (∀ n. n < # lpt ∧ lpt[n].flags = LP_FREE → lpt[n].ref-size = 0);
used for: ls;
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);
used for: ls;
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);
used for: ls;
cleanup-lpt : ⊦ cleanup-lpt(lpt) = lpt.map(λ lp. (lp.ref-size = 0 ∧ lp.flags ≠ LP_FREE ⊃ mklp(0, 0, LP_FREE, lp.gcheapidx);lp));
used for: ls;
cleanup-lpt-base : ⊦ cleanup-lpt(lpt, 0) = lpt;
used for: s, ls;
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));
used for: s, ls;
freelist-cons : ⊦ freelist-cons(lpt, freelist) ↔ ¬ dups(freelist) ∧ (∀ n. n < # lpt ∧ lpt[n].flags = LP_FREE ↔ n ∈ freelist);
used for: ls;
replay-log : ⊦ replay-log(lpt, nx) = lpt.mapIndices(elems nx, λ lp. mklp(lp.ref-size, LEB_SIZE, LP_GROUP_NODES, lp.gcheapidx));
used for: ls;
gc-heap-base : ⊦ gc-heap(lpt, nx, 0) = ∅;
used for: s, ls;
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)} ;∅);
used for: ls;
gc-heap : ⊦ gc-heap(lpt, nx) = gc-heap(lpt, nx, # lpt);
used for: ls;
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));
log-group-block : ⊦ log-group-block(nx, lpt) ↔ (∀ n. n ∈ nx → n < # lpt ∧ lpt[n].flags = LP_GROUP_NODES);
used for: ls;
lpt-leb-size : ⊦ lpt-leb-size(lpt) ↔ (∀ n. n < # lpt → lpt[n].size ≤ LEB_SIZE);
used for: ls;
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);
used for: ls;
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 = []));
end enrich