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-nodes-rec | ⊦ abs-nodes(buf, m, a ' + x, lax, weak) ↔ (∃ buf0, buf1. buf = buf0 + buf1 ∧ ( abs-padding(buf0) ∧ abs-nodes(buf1, m + # buf0, a ' + x, lax, weak) ∨ lax ≠ [] ∧ lax.head.off = m ∧ lax.head.size = # buf0 ∧ abs-node(buf0, a) ∧ abs-nodes(buf1, m + # buf0, x, lax.tail, weak))) | An Axiom |
| abs-nodes-base | ⊦ abs-nodes(buf, m, [], lax, weak) ↔ # buf = 0 ∧ lax = [] ∨ (∃ buf0, buf1. buf = buf0 + buf1 ∧ abs-padding(buf0) ∧ abs-nodes(buf1, m + # buf0, [], lax, weak)) ∨ weak ∧ abs-failed(buf) ∧ lax = [] | An Axiom |
| abs-nodes | ⊦ abs-nodes(buf, x, lax, weak) ↔ abs-nodes(buf, 0, x, lax, weak) | An Axiom |
| size-rec | ⊦ (a ' + x).flashsize = a.flashsize + x.flashsize | An Axiom |
| size-base | ⊦ [].flashsize = 0 | An Axiom |
| abs-failed-abs-nodes | ⊦ abs-failed(buf) → (abs-nodes(buf, x, lax, weak) ↔ lax = [] ∧ x = [] ∧ weak) | A User Theorem |
| abs-failed-abs-nodes-h | ⊦ abs-failed(buf) → (abs-nodes(buf, n, x, lax, weak) ↔ lax = [] ∧ x = [] ∧ weak) | A User Theorem |
| abs-nodes-add-crash-aligned | ⊦ abs-nodes(buf0, x, lax, false) ∧ abs-node(buf1, a) → (abs-nodes((buf0 + buf1).align↓, x + a ', lax + @(# buf0, a.flashsize) ', boolvar) ↔ is-aligned(# buf0 + # buf1, EB_PAGE_SIZE)) | A User Theorem |
| abs-nodes-add-crash-aligned-h | ⊦ abs-nodes(buf0, m, x, lax, false) ∧ abs-node(buf1, a) ∧ is-aligned(n, NODE_HEADER_SIZE) ∧ is-aligned(m, NODE_HEADER_SIZE) ∧ n ≤ # buf0 + # buf1 ∧ abs-nodes(subarray(buf0 + buf1, 0, n), m, x + a ', lax + @(m + # buf0, a.flashsize) ', boolvar) → n = # buf0 + # buf1 | A User Theorem |
| abs-nodes-add-crash-aligned-nodes | ⊦ abs-nodes(buf0, x, lax, false) ∧ abs-nodes(buf1, # buf0, x0, lax0, false) ∧ # buf1 = x0.flashsize ∧ x0 ≠ [] → (abs-nodes((buf0 + buf1).align↓, x + x0, lax + lax0, boolvar) ↔ is-aligned(# buf0 + x0.flashsize, EB_PAGE_SIZE)) | A User Theorem |
| abs-nodes-aligned-2headersize | ⊦ abs-nodes(buf, x, lax, false) → is-aligned(# buf, 2 * NODE_HEADER_SIZE) | A User Theorem |
| abs-nodes-aligned-2headersize-h | ⊦ abs-nodes(buf, m, x, lax, false) → is-aligned(# buf, 2 * NODE_HEADER_SIZE) | A User Theorem |
| abs-nodes-aligned-2headersize-mod | ⊦ abs-nodes(buf, x, lax, false) ∧ EB_PAGE_SIZE = n + # buf % EB_PAGE_SIZE → is-aligned(n, 2 * NODE_HEADER_SIZE) | A User Theorem |
| abs-nodes-aligned-headersize | ⊦ abs-nodes(buf, x, lax, weak) → is-aligned(# buf, NODE_HEADER_SIZE) | A User Theorem |
| abs-nodes-aligned-headersize-h | ⊦ abs-nodes(buf, m, x, lax, weak) → is-aligned(# buf, NODE_HEADER_SIZE) | A User Theorem |
| abs-nodes-append | ⊦ abs-nodes(buf0, x0, lax0, false) → (abs-nodes(buf0 + buf1, x0 + x1, lax0 + lax1, weak) ↔ abs-nodes(buf1, # buf0, x1, lax1, weak)) | A User Theorem |
| abs-nodes-append-empty | ⊦ abs-nodes(buf0, x0, lax0, false) → (abs-nodes(buf0 + buf1, x0, lax0, weak) ↔ abs-nodes(buf1, # buf0, [], [], weak)) | A User Theorem |
| abs-nodes-append-empty-h | ⊦ abs-nodes(buf0, m, x0, lax0, false) → (abs-nodes(buf0 + buf1, m, x0, lax0, weak) ↔ abs-nodes(buf1, m + # buf0, [], [], weak)) | A User Theorem |
| abs-nodes-append-h | ⊦ abs-nodes(buf0, m, x0, lax0, false) → (abs-nodes(buf0 + buf1, m, x0 + x1, lax0 + lax1, weak) ↔ abs-nodes(buf1, m + # buf0, x1, lax1, weak)) | A User Theorem |
| abs-nodes-at-least-flashsize | ⊦ abs-nodes(buf, m, x, lax, false) → # buf ≥ x.flashsize | A User Theorem |
| abs-nodes-atend-no-address | ⊦ abs-nodes(buf, x, lax, boolvar) → ¬ @(# buf, m1) ∈ lax | A User Theorem |
| abs-nodes-before-no-address-h | ⊦ abs-nodes(buf, m, x, lax, boolvar) ∧ m0 < m → ¬ @(m0, m1) ∈ lax | A User Theorem |
| abs-nodes-beyond-no-address | ⊦ abs-nodes(buf, x, lax, boolvar) ∧ # buf ≤ m0 → ¬ @(m0, m1) ∈ lax | A User Theorem |
| abs-nodes-beyond-no-address-h | ⊦ abs-nodes(buf, m, x, lax, boolvar) ∧ # buf + m ≤ m0 → ¬ @(m0, m1) ∈ lax | A User Theorem |
| abs-nodes-bothcrash-prefix | ⊦ abs-nodes(buf0.align↓, x0, lax0, boolvar0) ∧ abs-nodes((buf0 + buf1).align↓, x1, lax1, boolvar1) → x0 ⊑ x1 ∧ lax0 ⊑ lax1 | A User Theorem |
| abs-nodes-case-distinction-h | abs-nodes(buf, m, x, lax, true) ⊦ x = [] ∧ # buf = 0 ∨ x = [] ∧ abs-failed(buf) ∨ (∃ buf0, buf1. buf = buf0 + buf1 ∧ ( abs-padding(buf0) ∧ abs-nodes(buf1, m + # buf0, x, lax, true) ∨ x ≠ [] ∧ lax ≠ [] ∧ lax.head = @(m, x.head.flashsize) ∧ abs-node(buf0, x.head) ∧ abs-nodes(buf1, m + # buf0, x.tail, lax.tail, true))) | A User Theorem |
| abs-nodes-crash | ⊦ abs-nodes(buf, x, lax, true) → (∃ x0, lax0. x0 ⊑ x ∧ lax0 ⊑ lax ∧ abs-nodes(buf.align↓, x0, lax0, true)) | A User Theorem |
| abs-nodes-crash-h | ⊦ abs-nodes(buf, m, x, lax, true) ∧ is-aligned(n, NODE_HEADER_SIZE) ∧ n ≤ # buf → (∃ x0, lax0. x0 ⊑ x ∧ lax0 ⊑ lax ∧ abs-nodes(subarray(buf, 0, n), m, x0, lax0, true)) | A User Theorem |
| abs-nodes-crash-prefix | ⊦ abs-nodes(buf.align↓, x0, lax0, boolvar0) ∧ abs-nodes(buf, x1, lax1, boolvar1) → x0 ⊑ x1 ∧ lax0 ⊑ lax1 | A User Theorem |
| abs-nodes-elems-adr-length | ⊦ abs-nodes(buf, x, lax, weak) → # x = # lax | A User Theorem |
| abs-nodes-elems-adr-length-h | ⊦ abs-nodes(buf, m, x, lax, weak) → # x = # lax | A User Theorem |
| abs-nodes-elems-empty-adr-empty | ⊦ abs-nodes(buf, [], lax, weak) → lax = [] | A User Theorem |
| abs-nodes-elems-empty-adr-empty-h | ⊦ abs-nodes(buf, m, [], lax, weak) → lax = [] | A User Theorem |
| abs-nodes-emptyheader-h | ⊦ isempty(buf, 0, NODE_HEADER_SIZE) → (abs-nodes(buf, m, x, lax, weak) ↔ (# buf = 0 ∨ abs-failed(buf) ∧ weak) ∧ x = [] ∧ lax = []) | A User Theorem |
| abs-nodes-first-adr-explicit | ⊦ abs-nodes(buf, m, a ' + x, lax, weak) → (lax.head = ladr ↔ (∃ lax0. lax = ladr + lax0)) | A User Theorem |
| abs-nodes-headerspace | # buf ≠ 0 ⊦ abs-nodes(buf, m, x, lax, weak) → (NODE_HEADER_SIZE ≤ # buf + n ↔ NODE_HEADER_SIZE ≤ # buf) | A User Theorem |
| abs-nodes-mkbuf0-empty | ⊦ abs-nodes(mkbuf(0), x, lax, weak) ↔ x = [] ∧ lax = [] | A User Theorem |
| abs-nodes-mkbuf0-empty-h | ⊦ abs-nodes(mkbuf(0), m, x, lax, weak) ↔ x = [] ∧ lax = [] | A User Theorem |
| abs-nodes-no-padding-last | ⊦ # buf = (x + a ').flashsize → ( abs-nodes(buf, m, x + a ', lax + ladr ', false) ↔ (∃ buf0, buf1. buf = buf0 + buf1 ∧ abs-nodes(buf0, m, x, lax, false) ∧ abs-node(buf1, a) ∧ ladr = @(# buf0 + m, a.flashsize))) | A User Theorem |
| abs-nodes-no-padding-one | ⊦ # buf = a '.flashsize → (abs-nodes(buf, m, a ', lax, false) ↔ lax = @(m, # buf) ' ∧ abs-node(buf, a)) | A User Theorem |
| abs-nodes-no-padding-rec | ⊦ # buf = (a ' + x).flashsize → ( abs-nodes(buf, m, a ' + x, lax, false) ↔ (∃ buf0, buf1. buf = buf0 + buf1 ∧ lax ≠ [] ∧ lax.head.off = m ∧ lax.head.size = # buf0 ∧ abs-node(buf0, a) ∧ abs-nodes(buf1, m + # buf0, x, lax.tail, false))) | A User Theorem |
| abs-nodes-nodups | ⊦ abs-nodes(buf, x, lax, boolvar) → ¬ dups(lax) | A User Theorem |
| abs-nodes-nodups-h | ⊦ abs-nodes(buf, m, x, lax, boolvar) → ¬ dups(lax) | A User Theorem |
| abs-nodes-nospace | # buf < NODE_HEADER_SIZE ⊦ abs-nodes(buf, x, lax, boolvar) ↔ x = [] ∧ lax = [] ∧ buf = mkbuf(0) | A User Theorem |
| abs-nodes-nospace-h | # buf < NODE_HEADER_SIZE ⊦ abs-nodes(buf, m, x, lax, boolvar) ↔ x = [] ∧ lax = [] ∧ buf = mkbuf(0) | A User Theorem |
| abs-nodes-nospace-header-h | NODE_HEADER_SIZE ≤ # buf ⊦ is-encoded(nodeheader(m, boolvar0), subarray(buf, 0, NODE_HEADER_SIZE)) ∧ # buf < 2 * NODE_HEADER_SIZE + align↑(m, 2 * NODE_HEADER_SIZE) → (abs-nodes(buf, n, x, lax, weak) ↔ abs-failed(buf) ∧ x = [] ∧ lax = [] ∧ weak) | A User Theorem |
| abs-nodes-notrailer-h | ⊦ is-encoded(nodeheader(m, boolvar0), subarray(buf, 0, NODE_HEADER_SIZE)) ∧ 2 * NODE_HEADER_SIZE + align↑(m, 2 * NODE_HEADER_SIZE) ≤ # buf ∧ ¬ range=(buf, NODE_HEADER_SIZE + align↑(m, 2 * NODE_HEADER_SIZE), validtrailer, 0, NODE_HEADER_SIZE) → (abs-nodes(buf, n, x, lax, weak) ↔ abs-failed(buf) ∧ x = [] ∧ lax = [] ∧ weak) | A User Theorem |
| abs-nodes-one | ⊦ abs-nodes(buf, a ', lax, weak) ↔ (∃ buf0, buf1. buf = buf0 + buf1 ∧ ( abs-padding(buf0) ∧ abs-nodes(buf1, # buf0, a ', lax, weak) ∨ lax = @(0, a.flashsize) ' ∧ abs-node(buf0, a) ∧ abs-nodes(buf1, # buf0, [], [], weak))) | A User Theorem |
| abs-nodes-one-abs-node | ⊦ abs-node(buf, a) → (abs-nodes(buf, m, a ', ladr ', false) ↔ ladr = @(m, a.flashsize)) | A User Theorem |
| abs-nodes-one-h | ⊦ abs-nodes(buf, m, a ', lax, weak) ↔ (∃ buf0, buf1. buf = buf0 + buf1 ∧ ( abs-padding(buf0) ∧ abs-nodes(buf1, m + # buf0, a ', lax, weak) ∨ lax = @(m, a.flashsize) ' ∧ abs-node(buf0, a) ∧ abs-nodes(buf1, m + # buf0, [], [], weak))) | A User Theorem |
| abs-nodes-padding-prefix | ⊦ abs-padding(buf0) → (abs-nodes(buf0 + buf1, m, x, lax, weak) ↔ abs-nodes(buf1, m + # buf0, x, lax, weak)) | A User Theorem |
| abs-nodes-prefix | ⊦ abs-nodes(buf0, x0, lax0, boolvar0) ∧ abs-nodes(buf0 + buf1, x1, lax1, boolvar1) → x0 ⊑ x1 ∧ lax0 ⊑ lax1 | A User Theorem |
| abs-nodes-prefix-elim | ⊦ abs-nodes(buf0, x0, lax0, false) → (abs-nodes(buf0 + buf1, x1, lax1, boolvar1) ↔ (∃ x2, lax2. x1 = x0 + x2 ∧ lax1 = lax0 + lax2 ∧ abs-nodes(buf1, # buf0, x2, lax2, boolvar1))) | A User Theorem |
| abs-nodes-prefix-h | ⊦ abs-nodes(buf0, m, x0, lax0, boolvar0) ∧ abs-nodes(buf0 + buf1, m, x1, lax1, boolvar1) → x0 ⊑ x1 ∧ lax0 ⊑ lax1 | A User Theorem |
| abs-nodes-split | ⊦ abs-nodes(buf, x0 + x1, lax, weak) → (∃ buf0, buf1, lax0, lax1. lax = lax0 + lax1 ∧ buf = buf0 + buf1 ∧ abs-nodes(buf0, x0, lax0, false) ∧ abs-nodes(buf1, # buf0, x1, lax1, weak)) | A User Theorem |
| abs-nodes-split-h | ⊦ abs-nodes(buf, m, x0 + x1, lax, weak) → (∃ buf0, buf1, lax0, lax1. lax = lax0 + lax1 ∧ buf = buf0 + buf1 ∧ abs-nodes(buf0, m, x0, lax0, false) ∧ abs-nodes(buf1, m + # buf0, x1, lax1, weak)) | A User Theorem |
| abs-nodes-strengthen | ⊦ abs-nodes(buf, x, lax, weak) ∧ ¬ abs-nodes(buf, x, lax, false) → weak | A User Theorem |
| abs-nodes-strong-imp-weak | ⊦ abs-nodes(buf, x, lax, false) → abs-nodes(buf, x, lax, true) | A User Theorem |
| abs-nodes-strong-imp-weak-h | ⊦ abs-nodes(buf, m, x, lax, false) → abs-nodes(buf, m, x, lax, true) | A User Theorem |
| abs-nodes-subarray-failed | n < # buf, n ≠ 0 ⊦ abs-nodes(buf, m, x, lax, false) ∧ is-aligned(n, NODE_HEADER_SIZE) ∧ x ≠ [] ∧ # buf = x.flashsize → (∃ n0. n0 < # x ∧ abs-nodes(subarray(buf, 0, n), m, prefixn(n0, x), prefixn(n0, lax), true)) | A User Theorem |
| abs-nodes-unique-strong | ⊦ abs-nodes(buf, x0, lax0, false) → (abs-nodes(buf, x1, lax1, boolvar1) ↔ x0 = x1 ∧ lax0 = lax1) | A User Theorem |
| abs-nodes-unique-strong-h | ⊦ abs-nodes(buf, m, x0, lax0, false) → (abs-nodes(buf, m, x1, lax1, boolvar1) ↔ x0 = x1 ∧ lax0 = lax1) | A User Theorem |
| abs-nodes-unique-weak | ⊦ abs-nodes(buf, x0, lax0, true) → (abs-nodes(buf, x1, lax1, true) ↔ x0 = x1 ∧ lax0 = lax1) | A User Theorem |
| abs-nodes-unique-weak-h | ⊦ abs-nodes(buf, m, x0, lax0, true) → (abs-nodes(buf, m, x1, lax1, true) ↔ x0 = x1 ∧ lax0 = lax1) | A User Theorem |
| abs-nodes-valid-node | ⊦ is-encoded(nodeheader(m, boolvar0), subarray(buf, 0, NODE_HEADER_SIZE)) ∧ 2 * NODE_HEADER_SIZE + align↑(m, 2 * NODE_HEADER_SIZE) ≤ # buf ∧ range=(buf, NODE_HEADER_SIZE + align↑(m, 2 * NODE_HEADER_SIZE), validtrailer, 0, NODE_HEADER_SIZE) → ( abs-nodes(buf, n, x, lax, weak) ↔ (∃ buf0, buf1. buf = buf0 + buf1 ∧ ( boolvar0 ∧ abs-padding(buf0) ∧ abs-nodes(buf1, n + # buf0, x, lax, weak) ∨ # buf0 = x.head.flashsize ∧ x ≠ [] ∧ lax ≠ [] ∧ lax.head = @(n, # buf0) ∧ ¬ boolvar0 ∧ abs-node(buf0, x.head) ∧ abs-nodes(buf1, n + # buf0, x.tail, lax.tail, weak)))) | A User Theorem |
| abs-padding-abs-nodes-h | ⊦ abs-padding(buf) → (abs-nodes(buf, m, x, lax, weak) ↔ x = [] ∧ lax = []) | A User Theorem |
| abs-split-by-address | ⊦ abs-nodes(buf, x, lax0 + ladr ' + lax1, boolvar0) → (∃ buf0, buf1, buf2, x0, a, x1. x = x0 + a ' + x1 ∧ # x0 = # lax0 ∧ buf = buf0 + buf1 + buf2 ∧ ladr = @(# buf0, a.flashsize) ∧ # buf1 = a.flashsize ∧ abs-node(buf1, a)) | A User Theorem |
| abs-split-by-address-h | ⊦ abs-nodes(buf, m, x, lax0 + ladr ' + lax1, boolvar0) → (∃ buf0, buf1, buf2, x0, a, x1. x = x0 + a ' + x1 ∧ # x0 = # lax0 ∧ buf = buf0 + buf1 + buf2 ∧ ladr = @(m + # buf0, a.flashsize) ∧ # buf1 = a.flashsize ∧ abs-node(buf1, a)) | A User Theorem |
| add-failed-is-aligned | ⊦ abs-nodes(buf, x, lax, boolvar) ∧ is-aligned(# buf + n, EB_PAGE_SIZE) → is-aligned(n, NODE_HEADER_SIZE) | A User Theorem |
| flashsize-eq-0 | ⊦ x.flashsize = 0 ↔ x = [] | A User Theorem |
| flashsize-one | ⊦ a '.flashsize = a.flashsize | A User Theorem |
| inj-adr | ⊦ @(m0, m1) = @(m2, m3) ↔ m0 = m2 ∧ m1 = m3 | A User Theorem |
| ls-abs-node-buf-size | ⊦ abs-node(buf, nd) → # buf = nd.alignedsize + 2 * NODE_HEADER_SIZE | A User Theorem |