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: |
|---|---|---|
| valid-journal-head | ⊦ valid-journal-head(nx, gstore, ginval) ↔ nx ≠ [] ∧ nx.last ∈ gstore ∧ ¬ nx.last ∈ ginval ∧ (gstore[nx.last].gndlist = [] ∨ gstore[nx.last].gndlist.last.end) | An Axiom |
| keys-base | ⊦ ∅.keys = ∅ | An Axiom |
| keys-rec | ⊦ ¬ n ∈ ns → (ns ++ n).keys = ns.keys ++ inodekey(n) | An Axiom |
| inos-node-store-def | ⊦ n ∈ ri.inos ↔ inodekey(n) ∈ ri | An Axiom |
| lebs-rec | ⊦ (adr ' + ax).lebs = ax.lebs ++ adr.lnum | An Axiom |
| lebs-base | ⊦ [].lebs = ∅ | An Axiom |
| lebs-index | ⊦ n ∈ ri.lebs ↔ (∃ adr. adr.lnum = n ∧ adr ∈ ri) | An Axiom |
| lebs-set | ⊦ n ∈ as.lebs ↔ (∃ adr. adr.lnum = n ∧ adr ∈ as) | An Axiom |
| transaction | ⊦ transaction(ndx, gndx) ↔ # gndx = # ndx ∧ (gndx = [] ∨ gndx.head.start ∧ gndx.last.end ∧ (∀ n. (0 < n ∧ n < # gndx → ¬ gndx[n].start) ∧ (n + 1 < # gndx → ¬ gndx[n].end))) ∧ (∀ n. n < # gndx → gndx[n].nd = ndx[n]) | An Axiom |
| transaction-prefix | ⊦ transaction-prefix(ndx, gndx) ↔ # gndx < # ndx ∧ (gndx = [] ∨ gndx.head.start ∧ (∀ n. (0 < n ∧ n < # gndx → ¬ gndx[n].start) ∧ (n < # gndx → ¬ gndx[n].end))) ∧ (∀ n. n < # gndx → gndx[n].nd = ndx[n]) | An Axiom |
| flashsize-node | ⊦ gnd.flashsize = GROUP_NODE_HEADER_SIZE + nd.flashsize | An Axiom |
| flashsize-nodes-rec | ⊦ (nd ' + ndx).flashsize = nd.flashsize + ndx.flashsize | An Axiom |
| flashsize-nodes-base | ⊦ [].flashsize = 0 | An Axiom |
| keys-rec-01 | ⊦ (nd ' + ndx).keys = nd.key + ndx.keys | An Axiom |
| keys-base-01 | ⊦ [].keys = [] | An Axiom |
| key-cons | ⊦ key-cons(kx, ax, gstore, ginval) ↔ # kx = # ax ∧ (∀ n. n < # kx → ax[n] ∈ gstore ∧ ¬ ax[n].lnum ∈ ginval ∧ key-cons(kx[n], gstore[ax[n]].nd)) | An Axiom |
| nodes-cons | ⊦ nodes-cons(ax, ndx, gstore, ginval) ↔ # ax = # ndx ∧ (∀ n. n < # ax → ax[n] ∈ gstore ∧ ¬ ax[n].lnum ∈ ginval ∧ gstore[ax[n]].nd = ndx[n]) | An Axiom |
| key-cons-rec | ⊦ key-cons(nd ' + ndx) ↔ ¬ ¬(key-cons(nd.key, nd) ∧ key-cons(ndx)) | An Axiom |
| key-cons-base | ⊦ key-cons([]) | An Axiom |
| referenced-adrs-rec | ⊦ referenced-adrs(adr ' + ax, ri) = (adr ∈ ri ⊃ adr ';[]) + referenced-adrs(ax, ri) | An Axiom |
| referenced-adrs-base | ⊦ referenced-adrs([], ri) = [] | An Axiom |
| nds-rec | ⊦ (gnd ' + gndx).nds = gnd.nd + gndx.nds | An Axiom |
| nds-base | ⊦ [].nds = [] | An Axiom |
| at-write-at | ⊦ # ax = # ndx ∧ adr ∈ ax ∧ ¬ dups(ax) → fs[ax, ndx][adr] = ndx[pos(adr, ax)] | A User Theorem |
| at-write-other | ⊦ # ax = # ndx ∧ ¬ adr ∈ ax → fs[ax, ndx][adr] = fs[adr] | A User Theorem |
| except-refsizeeq-valid-head | ⊦ valid-journal-head(nx, gstore0, ginval) ∧ gstore0 =○refsize gstore1 → valid-journal-head(nx, gstore1, ginval) | A User Theorem |
| flashsize-app | ⊦ (ndx0 + ndx1).flashsize = ndx0.flashsize + ndx1.flashsize | A User Theorem |
| flashsize-one | ⊦ nd '.flashsize = nd.flashsize | A User Theorem |
| in-data-explicit | ⊦ key ∈ ri ∧ ri[key] = adr → adr ∈ ri | A User Theorem |
| in-index-in-range | ⊦ key ∈ ri ∧ ri[key] = adr → adr ∈ range ri | A User Theorem |
| in-rem-keys-in-data | ⊦ adr ∈ ri \ ks → adr ∈ ri | A User Theorem |
| in-write | # ax = # ndx ⊦ adr ∈ fs[ax, ndx] ↔ adr ∈ fs ∨ adr ∈ ax | A User Theorem |
| index-update-dom | # kx = # ax ⊦ dom ri[kx, ax] = dom ri ∪ kx.toSet | A User Theorem |
| index-update-range | # kx = # ax ⊦ ri-inj(ri) ∧ kx.toSet ⊆ dom ri ∧ ax.toSet ∩ range ri = ∅ ∧ ¬ dups(kx) ∧ ¬ dups(ax) → range ri[kx, ax] = (range ri \ ri[kx].toSet) ∪ ax.toSet | A User Theorem |
| inos-dom | ⊦ dom ri0 = dom ri1 → ri0.inos = ri1.inos | A User Theorem |
| inos-empty | ⊦ ∅.inos = ∅ | A User Theorem |
| inos-greater-del | ⊦ ri.inos < maxino → (ri -- key).inos < maxino | A User Theorem |
| inos-greater-notin | ⊦ ri.inos < maxino → ¬ inodekey(maxino) ∈ ri | A User Theorem |
| inos-greater-rem | ⊦ ri.inos < maxino → (ri \ ks).inos < maxino | A User Theorem |
| inos-write | ⊦ ri[key, adr].inos = ri.inos ∪ (key.inode? ⊃ ∅ ++ key.ino;∅) | A User Theorem |
| key-cons-app | ⊦ key-cons(ndx0 + ndx1) ↔ key-cons(ndx0) ∧ key-cons(ndx1) | A User Theorem |
| key-cons-ext | ⊦ key-cons(ndx) ↔ (∀ n. n < # ndx → key-cons(ndx[n].key, ndx[n])) | A User Theorem |
| key-cons-one | ⊦ key-cons(nd ') ↔ key-cons(nd.key, nd) | A User Theorem |
| keys-app | ⊦ (ndx0 + ndx1).keys = ndx0.keys + ndx1.keys | A User Theorem |
| keys-empty | ⊦ ns.keys = ∅ ↔ ns = ∅ | A User Theorem |
| keys-eq-one | ⊦ ndx.keys = key ' ↔ (∃ nd. ndx = nd ' ∧ nd.key = key) | A User Theorem |
| keys-in | ⊦ key ∈ ns.keys ↔ (∃ n. key = inodekey(n) ∧ n ∈ ns) | A User Theorem |
| keys-inodekey-in | ⊦ inodekey(n) ∈ ns.keys ↔ n ∈ ns | A User Theorem |
| keys-inodekeys | ⊦ ns.keys.inodes? | A User Theorem |
| keys-len | ⊦ # ndx.keys = # ndx | A User Theorem |
| keys-one | ⊦ nd '.keys = nd.key ' | A User Theorem |
| keys-rec-full | ⊦ (ns ++ n).keys = ns.keys ++ inodekey(n) | A User Theorem |
| keys-rem | ⊦ (ns -- n).keys = ns.keys -- inodekey(n) | A User Theorem |
| keys-split | ⊦ ndx.keys = kx0 + kx1 ↔ (∃ ndx0, ndx1. ndx = ndx0 + ndx1 ∧ ndx0.keys = kx0 ∧ ndx1.keys = kx1) | A User Theorem |
| ladrlist-to-adr-split | n < # lax ⊦ lax.to-adr(m)[n] = adr ↔ (∃ lax0, lax1. lax = lax0 + @(adr.pos, adr.size) ' + lax1 ∧ adr.lnum = m ∧ # lax0 = n) | A User Theorem |
| lebs-del-subseteq | ⊦ ri.lebs ⊆ ns → (ri -- key).lebs ⊆ ns | A User Theorem |
| lebs-del-subseteq-set | ⊦ as.lebs ⊆ ns → (as -- adr).lebs ⊆ ns | A User Theorem |
| lebs-empty | ⊦ ∅.lebs = ∅ | A User Theorem |
| lebs-in-ri-in-gstore | ⊦ adr ∈ ri ∧ ri.lebs ⊆ dom gstore → adr.lnum ∈ gstore | A User Theorem |
| lebs-in-ri-in-gstore-explicit | ⊦ key ∈ ri ∧ ri[key] = adr ∧ ri.lebs ⊆ dom gstore → adr.lnum ∈ gstore | A User Theorem |
| lebs-lookup-subseteq | ⊦ ri.lebs ⊆ ns → ri[ks].lebs ⊆ ns | A User Theorem |
| lebs-range | ⊦ (range ri).lebs = ri.lebs | A User Theorem |
| lebs-rem-subseteq | ⊦ ri.lebs ⊆ ns → (ri \ ks).lebs ⊆ ns | A User Theorem |
| lebs-write | ⊦ ¬ key ∈ ri → ri[key, adr].lebs = ri.lebs ++ adr.lnum | A User Theorem |
| lebs-write-subseteq | ⊦ ri.lebs ⊆ dom gstore → ri[key, @(m, m1, m2)].lebs ⊆ dom gstore ++ m | A User Theorem |
| lebs-write-subseteq0 | ⊦ ri.lebs ⊆ dom gstore ∧ m ∈ gstore → ri[key, @(m, m1, m2)].lebs ⊆ dom gstore | A User Theorem |
| natset-ls-add-max-ls | ⊦ ns < n → ns ++ m < max(m + 1, n) | A User Theorem |
| natset-ls-max-ls | ⊦ ns < n → ns < max(m + 1, n) | A User Theorem |
| nds-app | ⊦ (gndx0 + gndx1).nds = gndx0.nds + gndx1.nds | A User Theorem |
| nds-eq-empty | ⊦ gndx.nds = [] ↔ gndx = [] | A User Theorem |
| nds-eq-one | ⊦ gndx.nds = nd ' ↔ (∃ gnd. gndx = gnd ' ∧ gnd.nd = nd) | A User Theorem |
| nds-length | ⊦ # gndx.nds = # gndx | A User Theorem |
| nds-one | ⊦ gnd '.nds = gnd.nd ' | A User Theorem |
| new-inter-empty | ⊦ as ⊆ dom fs ∧ new(ax, fs) → ax.toSet ∩ as = ∅ | A User Theorem |
| nodes-cons-rec | ⊦ nodes-cons(adr ' + ax, nd ' + ndx, gstore, ginval) ↔ adr ∈ gstore ∧ ¬ adr.lnum ∈ ginval ∧ gstore[adr].nd = nd ∧ nodes-cons(ax, ndx, gstore, ginval) | A User Theorem |
| nodes-cons-write-app | ⊦ n ∈ gstore ∧ ¬ n ∈ ginval ∧ gstore[n].gndlist = gndx0 ∧ gstore[n].ladrlist = lax0 ∧ # gndx0 = # lax0 ∧ # gndx1 = # lax1 ∧ ¬ dups(lax0 + lax1) ∧ transaction(ndx, gndx1) → nodes-cons(lax1.to-adr(n), ndx, gstore[n, groupblock(gndx0 + gndx1, lax0 + lax1, m)], ginval) | A User Theorem |
| nodes-cons-write-other | gblock.gndlist = gstore[n].gndlist, gblock.ladrlist = gstore[n].ladrlist ⊦ nodes-cons(ax, ndx, gstore, ginval) → nodes-cons(ax, ndx, gstore[n, gblock], ginval) | A User Theorem |
| range-add-explicit | ⊦ key ∈ ri ∧ ri[key] = adr → range ri = range ri ++ adr | A User Theorem |
| range-del-in | ⊦ key ∈ ri ∧ ri[key] = adr ∧ ri-inj(ri) → range(ri -- key) = range ri -- adr | A User Theorem |
| range-empty | ⊦ range ∅ = ∅ | A User Theorem |
| range-write-in | ⊦ key ∈ ri ∧ ri-inj(ri) → range ri[key, adr] = (range ri -- ri[key]) ++ adr | A User Theorem |
| range-write-notin | ⊦ ¬ key ∈ ri → range ri[key, adr] = range ri ++ adr | A User Theorem |
| referenced-adrs-app | ⊦ referenced-adrs(ax0 + ax1, ri) = referenced-adrs(ax0, ri) + referenced-adrs(ax1, ri) | A User Theorem |
| referenced-adrs-eq-one-lookup | ⊦ referenced-adrs(ax, ri) = adr ' → fs[referenced-adrs(ax, ri)] = fs[adr] ' | A User Theorem |
| referenced-adrs-in | ⊦ adr ∈ referenced-adrs(ax, ri) ↔ adr ∈ ax ∧ adr ∈ ri | A User Theorem |
| referenced-adrs-inter-empty | ⊦ ax.toSet ∩ as = ∅ → referenced-adrs(ax, ri).toSet ∩ as = ∅ | A User Theorem |
| referenced-adrs-lookup-key-cons | ⊦ ri-cons(ri, fs) → key-cons(fs[referenced-adrs(ax, ri)]) | A User Theorem |
| referenced-adrs-lookup-keys-in-dom | ⊦ ri-cons(ri, fs) → fs[referenced-adrs(ax, ri)].keys.toSet ⊆ dom ri | A User Theorem |
| referenced-adrs-lookup-keys-lookup | ⊦ ri-cons(ri, fs) → ri[fs[referenced-adrs(ax, ri)].keys] = referenced-adrs(ax, ri) | A User Theorem |
| referenced-adrs-lookup-keys-nodups | ⊦ ri-cons(ri, fs) ∧ ¬ dups(ax) → ¬ dups(fs[referenced-adrs(ax, ri)].keys) | A User Theorem |
| referenced-adrs-nodups | ⊦ ¬ dups(ax) → ¬ dups(referenced-adrs(ax, ri)) | A User Theorem |
| referenced-adrs-one | ⊦ referenced-adrs(adr ', ri) = (adr ∈ ri ⊃ adr ';[]) | A User Theorem |
| referenced-adrs-split | ⊦ referenced-adrs(ax, ri) = ax0 + ax1 ↔ (∃ ax2, ax3. ax = ax2 + ax3 ∧ referenced-adrs(ax2, ri) = ax0 ∧ referenced-adrs(ax3, ri) = ax1) | A User Theorem |
| referenced-adrs-split-one | ⊦ referenced-adrs(ax, ri) = adr ' ↔ (∃ ax0, ax1. ax = ax0 + adr ' + ax1 ∧ referenced-adrs(ax0, ri) = [] ∧ referenced-adrs(ax1, ri) = [] ∧ adr ∈ ri) | A User Theorem |
| referenced-adrs-subseteq-range | ⊦ referenced-adrs(ax, ri).toSet ⊆ range ri | A User Theorem |
| refsize-cons-crash | ⊦ refsize-cons(gstore0, range fi) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ fi.lebs ⊆ dom gstore0 → refsize-cons(crash(gstore, gstore0, ginval, nx), range fi) | A User Theorem |
| refsize-cons-in-ri-0 | ⊦ refsize-cons(gstore, range ri) ∧ gstore[adr.lnum].ref-size = 0 ∧ ri.lebs ⊆ dom gstore ∧ adr.size ≠ 0 → ¬ adr ∈ ri | A User Theorem |
| restrict-in-empty | ⊦ range ri | n = ∅ → ¬ @(n, m0, m1) ∈ ri | A User Theorem |
| restrict-range-notin-lebs | ⊦ ¬ n ∈ gstore ∧ fi.lebs ⊆ dom gstore → range fi | n = ∅ | A User Theorem |
| ri-inj-index-update | # ax = # kx ⊦ ri-inj(ri) ∧ ¬ dups(ax) ∧ ax.toSet ∩ range ri = ∅ → ri-inj(ri[kx, ax]) | A User Theorem |
| transaction-empty | ⊦ transaction([], gndx) ↔ gndx = [] | A User Theorem |
| transaction-empty-right | ⊦ transaction(ndx, []) ↔ ndx = [] | A User Theorem |
| transaction-last-nend | ⊦ ¬ transaction(ndx, gndx + mkgnode(nd, n, boolvar, false) ') | A User Theorem |
| transaction-length | ⊦ transaction(ndx, gndx) → (# ndx = # gndx ↔ true) | A User Theorem |
| transaction-length0 | ⊦ # gndx = n ∧ transaction(ndx, gndx) → (# ndx = n ↔ true) | A User Theorem |
| transaction-prefix-app | ⊦ transaction-prefix(ndx, gndx0 + gndx1) → transaction-prefix(ndx, gndx0) | A User Theorem |
| transaction-prefix-app-last | # ndx = # gndx ⊦ transaction-prefix(ndx + nd ', gndx) → transaction(ndx + nd ', gndx + mkgnode(nd, n, ndx = [], true) ') | A User Theorem |
| transaction-prefix-app-nonlast | ndx1 ≠ [], # ndx = # gndx ⊦ transaction-prefix(ndx + nd ' + ndx1, gndx) → transaction-prefix(ndx + nd ' + ndx1, gndx + mkgnode(nd, n, ndx = [], false) ') | A User Theorem |
| transaction-prefix-empty | ⊦ transaction-prefix(ndx, []) ↔ ndx ≠ [] | A User Theorem |
| transaction-prefix-is-transaction-prefix | n < # gndx ⊦ transaction(ndx, gndx) → transaction-prefix(ndx, prefixn(n, gndx)) | A User Theorem |
| transaction-prefix-last-nonend | ⊦ ¬ transaction-prefix(ndx, gndx + mkgnode(nd, n, boolvar, true) ') | A User Theorem |
| valid-journal-head-emptylog | ⊦ ¬ valid-journal-head([], gstore, ginval) | A User Theorem |