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: |
|---|---|---|
| btree | ⊦ ((btree(rp, r0, adr, height, dirty0, ri, iast, as, alladrs, nstat) * P))(zh0) ↔ (∃ r, zh, zbrar, dirty, nused. (r0 = null ⊃ ¬ dirty ∧ P(zh0);r = r0 ∧ zh = zh0) ∧ (dirty → dirty0) ∧ (adr ∈ as ↔ ¬ dirty) ∧ adr ∈ alladrs ∧ nsize(nused, nstat) ∧ unmodified(adr, mkznode(rp, zbrar, height = 0, dirty, nused), iast) ∧ (( r => mkznode(rp, zbrar, height = 0, dirty, nused) * bnode(r, zbrar, 0, nused, nused, height, dirty, ri, iast, as -- adr, alladrs -- adr) * P) )(zh)) | An Axiom |
| bleaf | ⊦ bnode(rp, zbrar, m, len, nused, 0, dirty, ri, iast, as, alladrs) = ( ⌜m + len ≤ nused ∧ nused ≤ # zbrar ∧ # zbrar = BRANCH_SIZE⌝ ∧ ⌜sorted(zbrar, 0, nused)⌝ ∧ ⌜ri = payload(zbrar, m, len)⌝ ∧ ⌜as = ∅⌝ ∧ ⌜alladrs = ∅⌝ ∧ emp) | An Axiom |
| bnode | ⊦ bnode(rp, zbrar, m, len, nused, height + 1, dirty, ri, iast, as, alladrs) = ( ⌜m + len ≤ nused ∧ nused ≤ # zbrar ∧ # zbrar = BRANCH_SIZE⌝ ∧ ⌜nused ≠ 0 ∧ sorted(zbrar, 0, nused - 1)⌝ ∧ _∃ (λ asar. _∃ (λ asar0. ⌜ # asar = nused ∧ disj(asar, 0, nused) ∧ union(asar, m, len) = as ∧ # asar0 = nused ∧ disj(asar0, 0, nused) ∧ union(asar0, m, len) = alladrs ⌝ ∧ (λ n. ⌜zbrar[n].branch?⌝ ∧ btree(rp, zbrar[n].child, zbrar[n].adr, height, dirty, key-range(zbrar, n, nused, ri), iast, asar[n], asar0[n], ok) )⊗_ (m, len )))) | An Axiom |
| infinite-memory | ⊦ ∃ r. r ≠ null ∧ ¬ r ∈ zh | An Axiom |
| btree-inv | ⊦ btree-inv(r, adr, istore, istore0, zh, ri, fi) ↔ (∃ height, dirty, as, alladrs. ((btree(null, r, adr, height, dirty, ri, nodes(istore), as, alladrs, ok) * true))(zh) ∧ refsize-cons(istore, as) ∧ adr ∈ istore ∧ alladrs ⊆ dom nodes(istore)) ∧ (∃ height, dirty, as, alladrs. ((btree(null, null, adr, height, false, fi, nodes(istore0), as, alladrs, ok) * true))(zh) ∧ refsize-cons(istore0, as) ∧ alladrs ⊆ dom nodes(istore)) | An Axiom |
| btree-sub-clean | ⊦ btree-sub-clean(r, n, zh) ↔ r ∈ zh ∧ ( ¬ zh[r].leaf → (∀ n0. n0 < zh[r].usedsize ∧ n0 < n ∧ zh[r].zbranches[n0].branch? ∧ zh[r].zbranches[n0].child ∈ zh → ¬ zh[zh[r].zbranches[n0].child].dirty)) | An Axiom |
| commit-inv | ⊦ commit-inv(n, pstate, istore1, istore0, nx, gstore, gstore0, ginval, bv, err, rp, r, adr, height, dirty, ri, istore, as, as0, alladrs, P, zh) ↔ (∃ as1. refsize-cons(istore, as0 ∪ as1) ∧ as1 ∩ dom nodes(istore1) ⊆ as ∧ as1 ∩ as0 = ∅ ∧ ((btree(rp, r, adr, height, dirty, ri, nodes(istore) | as1, as1, alladrs, ok) * P))(zh)) ∧ istore1 ⊑ istore ∧ r ∈ zh ∧ n ≤ zh[r].usedsize ∧ zh[r].dirty ∧ ¬ zh[r].leaf ∧ inv-journal(nx, gstore, gstore0, ginval) ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, bv) ∧ (err = ESUCCESS → pstate.index? ∧ btree-sub-clean(r, n, zh)) | An Axiom |
| congruent | ⊦ P0 ≡ P1 ↔ P0 = P1 | An Axiom |
| add-rem-same | ⊦ (as ++ adr) \ as = (adr ∈ as ⊃ ∅;∅ ++ adr) | A User Theorem |
| btree-adrs | ⊦ ((btree(rp, rp0, adr0, height, dirty, fi, iast, as, alladrs, nstat) * P))(zh) → as ⊆ dom iast | A User Theorem |
| btree-as-empty | ⊦ ((btree(rp, r0, adr, height, dirty0, ri, ∅, ∅, alladrs, nstat) * P))(zh0) → ((btree(rp, r0, adr, height, dirty0, ri, iast, ∅, alladrs, nstat) * P))(zh0) | A User Theorem |
| btree-as-empty-rev | ⊦ ((btree(rp, r0, adr, height, dirty0, ri, iast, ∅, alladrs, nstat) * P))(zh0) → ((btree(rp, r0, adr, height, dirty0, ri, ∅, ∅, alladrs, nstat) * P))(zh0) | A User Theorem |
| btree-clean-adr-in | ⊦ r ∈ zh ∧ zh[r] = mkznode(rp0, zbrar, boolvar, false, height0) ∧ ((btree(rp, r, adr, height, dirty, ri, iast, as, alladrs, nstat) * P))(zh) → adr ∈ as ∧ (height = 0 → as = ∅ ++ adr) | A User Theorem |
| btree-clean-alladrs | ⊦ ((btree(rp, r, adr, height, false, ri, iast, as, alladrs, nstat) * P))(zh) → as = alladrs | A User Theorem |
| btree-clean-fwd | ⊦ ((btree(rp0, r0, adr, height0, false, ri0, iast, as0, alladrs0, nstat) * P0))(zh0) ∧ ((btree(rp1, r1, adr, height1, false, ri1, iast, as1, alladrs1, nstat) * P1))(zh1) → height0 = height1 ∧ as0 = as1 ∧ ri0 = ri1 ∧ alladrs0 = alladrs1 | A User Theorem |
| btree-clean-fwd-strong | ⊦ iast0 ⊆ iast1 ∧ ((btree(rp0, r0, adr, height0, false, ri0, iast0, as0, alladrs0, nstat) * P0))(zh0) ∧ ((btree(rp1, r1, adr, height1, false, ri1, iast1, as1, alladrs1, nstat) * P1))(zh1) → height0 = height1 ∧ as0 = as1 ∧ ri0 = ri1 ∧ alladrs0 = alladrs1 | A User Theorem |
| btree-crash | ⊦ ((btree(null, null, adr, height, false, fi, iast0, as, alladrs, ok) * true))(zh0) → ((btree(null, null, adr, height, false, fi, iast0, as, alladrs, ok) * true))(zh1) | A User Theorem |
| btree-dirty-adr-notin | ⊦ r ∈ zh ∧ zh[r] = mkznode(rp0, zbrar, boolvar, true, height0) ∧ ((btree(rp, r, adr, height, dirty, ri, iast, as, alladrs, nstat) * P))(zh) → ¬ adr ∈ as ∧ (height = 0 → as = ∅) | A User Theorem |
| btree-imp-dirty | ⊦ ((btree(rp, r, adr, height, dirty, fi, iast, as, alladrs, nstat) * P))(zh) → ((btree(rp, r, adr, height, true, fi, iast, as, alladrs, nstat) * P))(zh) | A User Theorem |
| btree-inv-adr-lnum-in | ⊦ btree-inv(rp, @(m0, m1, m2), istore, istore0, zh, fi, fi0) → m0 ∈ istore | A User Theorem |
| btree-inv-alloc | ⊦ ¬ n ∈ istore ∧ inv(istore) ∧ btree-inv(rp, adr, istore, istore0, zh0, ri, fi) → btree-inv(rp, adr, istore[n, indexblock(indx, lax, 0)], istore0, zh0, ri, fi) | A User Theorem |
| btree-inv-clean-commit | ⊦ (rp = null ∨ ¬ zh[rp].dirty) ∧ istore0 ⊑ istore ∧ btree-inv(rp, adr, istore, istore0, zh, ri, fi) → btree-inv(rp, adr, istore, istore, zh, ri, ri) | A User Theorem |
| btree-inv-crash | ⊦ istore0 ⊑ istore ∧ remove-refsize0(istore0) = istore0 ∧ btree-inv(rp, adr, istore, istore0, zh0, ri, fi) ∧ inv(istore) → btree-inv(null, adr, remove-refsize0(crash(istore, istore0)), istore0, zh1, fi, fi) | A User Theorem |
| btree-inv-format | ⊦ btree-inv (null, @(n, m0, m1), (∅)[n, indexblock(indexnode(mkbrarray(BRANCH_SIZE), true, 0) ', @(m0, m1) ', m1)], (∅)[n, indexblock(indexnode(mkbrarray(BRANCH_SIZE), true, 0) ', @(m0, m1) ', m1)], zh, ∅, ∅) | A User Theorem |
| btree-inv-remove-refsize0 | ¬ dirty ∨ rp = null ⊦ inv(istore) ∧ inv(istore0) ∧ zh[rp] = mkznode(rp0, zbrar, boolvar, dirty, nused) ∧ btree-inv(rp, adr, istore, istore0, zh, ri, fi) ∧ istore0 ⊑ istore → btree-inv(rp, adr, remove-refsize0(istore), remove-refsize0(istore), zh, ri, fi) | A User Theorem |
| btree-inv-root-neq-null-fwd | ⊦ rp ≠ null ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) → rp ∈ zh | A User Theorem |
| btree-inv-root-null | ⊦ istore0 ⊑ istore ∧ btree-inv(null, adr, istore, istore0, zh, ri, fi) → ri = fi | A User Theorem |
| btree-inv-root-null-or-clean | r = null ∨ ¬ zh[r].dirty ⊦ istore0 ⊑ istore ∧ btree-inv(r, adr, istore, istore0, zh, ri, fi) → ri = fi | A User Theorem |
| btree-istore-reduce | ⊦ iast0 ⊆ iast1 ∧ ((btree(rp, r0, adr, height, dirty0, ri, iast0, as, alladrs, nstat) * P))(zh0) → ((btree(rp, r0, adr, height, dirty0, ri, iast1, as, alladrs, nstat) * P))(zh0) | A User Theorem |
| btree-istore-reduce-refed | ⊦ iast0 | as ⊆ iast1 ∧ ((btree(rp, rp0, adr, height, dirty, ri, iast0, as, alladrs, nstat) * P))(zh) → ((btree(rp, rp0, adr, height, dirty, ri, iast1, as, alladrs, nstat) * P))(zh) | A User Theorem |
| btree-istore-restrict | ⊦ ((btree(rp, r0, adr, height, dirty0, ri, iast | as0, as, alladrs, nstat) * P))(zh0) → ((btree(rp, r0, adr, height, dirty0, ri, iast, as, alladrs, nstat) * P))(zh0) | A User Theorem |
| btree-istore-restrict-to-as | ⊦ ((btree(rp, r0, adr, height, dirty0, ri, iast, as, alladrs, nstat) * P))(zh0) → ((btree(rp, r0, adr, height, dirty0, ri, iast | as, as, alladrs, nstat) * P))(zh0) | A User Theorem |
| btree-leaf-adr | ⊦ ((btree(rp, r, adr, 0, dirty, ri, iast, as, alladrs, nstat) * P))(zh) → alladrs = {adr} | A User Theorem |
| btree-leaf-fwd | ⊦ r ∈ zh ∧ zh[r] = mkznode(rp0, zbrar0, true, dirty0, nused) ∧ ((btree(rp, r, adr, height, dirty, fi, iast, as, alladrs, nstat) * P))(zh) → height = 0 | A User Theorem |
| btree-mark-dirty | ⊦ r ∈ zh ∧ zh[r] = mkznode(rp0, zbrar, boolvar, false, height0) ∧ ((btree(rp, r, adr, height, false, ri, iast, as, alladrs, nstat) * P))(zh) → ((btree(rp, r, adr, height, true, ri, iast, as -- adr, alladrs, nstat) * P))(zh[r, mkznode(rp0, zbrar, boolvar, true, height0)]) | A User Theorem |
| btree-null | ⊦ ((btree(rp, null, adr, height, dirty0, ri, iast, as, alladrs, nstat) * true))(zh0) → ((btree(rp, null, adr, height, dirty0, ri, iast, as, alladrs, nstat) * true))(zh1) | A User Theorem |
| btree-null-or-clean-below | ⊦ r = null ∨ ¬ zh0[r].dirty → ( ((btree(rp, r, adr, height, dirty, ri, iast, as, alladrs, nstat) * P))(zh0) ↔ ((btree(rp, r, adr, height, false, ri, iast, as, alladrs, nstat) * P))(zh0)) | A User Theorem |
| btree-refed-subseteq-alladrs | ⊦ ((btree(rp, r, adr, height, dirty, fi, iast, as, alladrs, nstat) * P))(zh) → as ⊆ alladrs | A User Theorem |
| btree-remove-context | ⊦ ((btree(rp, r, adr, height, dirty, ri, iast, as, alladrs, ok) * P))(zh) ↔ (∃ P0. P0 ≡ P ∧ ((btree(rp, r, adr, height, dirty, ri, iast, as, alladrs, ok) * P0))(zh)) | A User Theorem |
| btree-repl-dirty-address | ⊦ ¬ adr1 ∈ alladrs ∧ r ∈ zh ∧ zh[r].dirty ∧ ((btree(rp, r, adr0, height, true, ri, iast, as, alladrs, nstat) * P))(zh) → ((btree(rp, r, adr1, height, true, ri, iast, as, (alladrs -- adr0) ++ adr1, nstat) * P))(zh) | A User Theorem |
| btree-reset-root | ⊦ ((btree(rp, r, adr, height, false, ri, iast, as, alladrs, ok) * true))(zh) → ((btree(rp, null, adr, height, false, ri, iast, as, alladrs, ok) * true))(zh) | A User Theorem |
| btree-reset-root-frame | ⊦ ((btree(rp, r, adr, height, false, ri, iast, as, alladrs, ok) * P))(zh) → ((btree(rp, null, adr, height, false, ri, iast, as, alladrs, ok) * true * P))(zh) | A User Theorem |
| btree-restrict-union-proper | n < # asar ⊦ ((btree(rp, r, adr, height, dirty, ri, iast | union(asar, 0, # asar), asar[n], alladrs, nstat) * P))(zh) ↔ ((btree(rp, r, adr, height, dirty, ri, iast | asar[n], asar[n], alladrs, nstat) * P))(zh) | A User Theorem |
| btree-ri-unique | ⊦ ((btree(rp, rp0, adr, height, dirty, ri0, iast, as0, alladrs0, ok) * P0))(zh) ∧ ((btree(rp, rp0, adr, height, dirty, ri1, iast, as1, alladrs1, ok) * P1))(zh) → ri0 = ri1 | A User Theorem |
| btree-root-in-heap | ⊦ r ≠ null ∧ ((btree(rp, r, adr, height, dirty, fi, iast, as, alladrs, nstat) * P))(zh) → r ∈ zh | A User Theorem |
| btree-sub-clean-0 | ⊦ btree-sub-clean(r, 0, zh) ↔ r ∈ zh | A User Theorem |
| btree-sub-clean-leaf | ⊦ r ∈ zh ∧ zh[r] = mkznode(rp, zbrar, true, dirty, height) → btree-sub-clean(r, n, zh) | A User Theorem |
| btree-sub-clean-next | ⊦ btree-sub-clean(r, n, zh) → ( btree-sub-clean(r, n + 1, zh) ↔ ¬ zh[r].leaf ∧ n < zh[r].usedsize ∧ zh[r].zbranches[n].branch? ∧ zh[r].zbranches[n].child ∈ zh → ¬ zh[zh[r].zbranches[n].child].dirty) | A User Theorem |
| btree-sub-clean-write-branches | n < # zbrar ⊦ zh[r].zbranches = zbrar ∧ zbrar[n].child = r1 ∧ ¬ zh[r1].dirty ∧ btree-sub-clean(r, n, zh) → btree-sub-clean(r, n + 1, zh[r, zh[r].zbranches:= zbrar[n, mkzbranch(key, adr, r1)]]) | A User Theorem |
| btree-truify-context | ⊦ ((btree(rp, r, adr, height, dirty, ri, iast, as, alladrs, ok) * P))(zh) → ((btree(rp, r, adr, height, dirty, ri, iast, as, alladrs, ok) * true))(zh) | A User Theorem |
| btree-write-node | ⊦ ¬ adr1 ∈ iast ∧ ¬ adr1 ∈ alladrs ∧ r ∈ zh ∧ zh[r] = mkznode(r0, zbrar, boolvar, true, m0) ∧ ((btree(rp, r, adr0, height, dirty, ri, iast, as, alladrs, nstat) * P))(zh) ∧ btree-sub-clean(r, m0, zh) → ((btree(rp, r, adr1, height, false, ri, iast[adr1, save(mkznode(r0, zbrar, boolvar, true, m0))], as ++ adr1, (alladrs -- adr0) ++ adr1, nstat) * P) )(zh[r, mkznode(r0, zbrar, boolvar, false, m0)]) | A User Theorem |
| btree-write-other | ⊦ ¬ adr ∈ as → ( ((btree(rp, r, adr0, height, dirty, ri, iast[adr, ind], as, alladrs, nstat) * P))(zh) ↔ ((btree(rp, r, adr0, height, dirty, ri, iast, as, alladrs, nstat) * P))(zh)) | A User Theorem |
| diff-add-same | ⊦ (as0 \ as1) ++ adr = (as0 ++ adr) \ as1 ↔ ¬ adr ∈ as1 | A User Theorem |
| diff-empty-subseteq | ⊦ as0 \ as1 = ∅ ↔ as0 ⊆ as1 | A User Theorem |
| diff-eq-diff-eq-union | ⊦ as2 \ as1 = as3 ∧ as1 \ as0 = as4 ∧ as1 ⊆ as2 ∧ as0 ⊆ as1 → as2 \ as0 = as3 ∪ as4 | A User Theorem |
| diff-subseteq-subseteq | ⊦ as1 ⊆ as2 → (as0 \ as1 ⊆ as2 ↔ as0 ⊆ as2) | A User Theorem |
| eq-union-disj | ⊦ zh0 ⊥ zh ∧ zh1 ⊥ zh → (zh0 ∪ zh = zh1 ∪ zh ↔ zh0 = zh1) | A User Theorem |
| inter-empty-inter-diff-empty | ⊦ as0 ∩ as1 = ∅ → as0 ∩ (as1 \ as) = ∅ | A User Theorem |
| inter-subseteq-simp | ⊦ as0 ∩ as ⊆ as1 ∩ as ↔ as0 ∩ as ⊆ as1 | A User Theorem |
| inter-subseteq-weaken | ⊦ as ⊆ as2 ∧ as0 ∩ as2 ⊆ as1 → as0 ∩ as ⊆ as1 | A User Theorem |
| inter-union-diff | ⊦ (as0 ∪ (as1 \ as)) ∩ as = as0 ∩ as | A User Theorem |
| inter-union-diff-subseteq | ⊦ as1 ∩ as3 ⊆ as → ((as0 ∪ (as1 \ as2)) ∩ as3 ⊆ as ↔ as0 ∩ as3 ⊆ as) | A User Theorem |
| maplet-null | ⊦ ((r => znd * P))(zh) → r ≠ null | A User Theorem |
| nat-le-eq | ⊦ n = n0 + n1 → (n ≤ n0 ↔ n1 = 0 ∧ n = n0) | A User Theorem |
| restrict-2 | ⊦ (iast | as0) | as1 = iast | (as0 ∩ as1) | A User Theorem |
| restrict-add-at | ⊦ iast0 | as ⊆ iast1 ∧ adr ∈ as ∧ adr ∈ iast0 ∧ iast0[adr] = ind → iast1[adr] = iast0[adr] | A User Theorem |
| restrict-add-in | ⊦ iast0 | as ⊆ iast1 ∧ adr ∈ as ∧ adr ∈ iast0 → adr ∈ iast1 | A User Theorem |
| restrict-add-subseteq-at | ⊦ iast0 | (as ++ adr) ⊆ iast1 ∧ adr ∈ iast0 ∧ iast0[adr] = ind → iast1[adr] = iast0[adr] | A User Theorem |
| restrict-add-subseteq-in | ⊦ iast0 | (as ++ adr) ⊆ iast1 ∧ adr ∈ iast0 → adr ∈ iast1 | A User Theorem |
| restrict-dom | ⊦ dom(iast | as) = dom iast ∩ as | A User Theorem |
| restrict-further | ⊦ iast0 | as0 ⊆ iast1 ∧ as1 ⊆ as0 → iast0 | as1 ⊆ iast1 | A User Theorem |
| restrict-idem | ⊦ (iast | as) | as = iast | as | A User Theorem |
| ri-range-ext | nused < # zbrar, sorted(zbrar, 0, nused) ⊦ ri0 = ri1 ↔ (∀ n. n ≤ nused → key-range(zbrar, n, nused + 1, ri0) = key-range(zbrar, n, nused + 1, ri1)) | A User Theorem |
| sep-forall-reduce | ⊦ (∀ n0, P. n0 < m ∧ ((nP(n + n0) * P))(zh) → ((nP2(n + n0) * P))(zh)) ∧ ((nP ⊗_(n, m) * P0))(zh) → ((nP2 ⊗_(n, m) * P0))(zh) | A User Theorem |
| sep-forall-reduce-true | ⊦ (∀ n0, P. n0 < m ∧ ((nP(n + n0) * P))(zh) → ((nP2(n + n0) * true * P))(zh)) ∧ ((nP ⊗_(n, m) * P0))(zh) → ((nP2 ⊗_(n, m) * true * P0))(zh) | A User Theorem |
| subseteq-inter-same | ⊦ as ⊆ as0 ∩ as ↔ as ⊆ as0 | A User Theorem |
| subseteq-restrict | ⊦ iast0 ⊆ iast1 → iast0 | as ⊆ iast1 | A User Theorem |
| subseteq-union-simp | ⊦ as = as0 ∪ as1 → (as ⊆ as0 ∪ as2 ↔ as1 ⊆ as0 ∪ as2) | A User Theorem |
| union-diff-same | ⊦ as0 ∪ (as1 \ as0) = as0 ∪ as1 | A User Theorem |
| union-diff-subseteq-union | ⊦ as0 \ as1 ⊆ as0 ∪ as2 | A User Theorem |
| union-eq-empty | ⊦ zh0 ⊥ zh1 → (∅ = zh0 ∪ zh1 ↔ zh0 = ∅ ∧ zh1 = ∅) | A User Theorem |