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: |
|---|---|---|
| inv-block | ⊦ inv(ablock) ↔ # ablock.list = # ablock.ladrlist ∧ inv-flashsize(ablock.list, ablock.ladrlist) ∧ ¬ dups(ablock.ladrlist) | An Axiom |
| size-base | ⊦ [].flashsize = 0 | An Axiom |
| size-rec | ⊦ (a ' + x).flashsize = a.flashsize + x.flashsize | An Axiom |
| inv-store | ⊦ inv(st) ↔ (∀ n. n ∈ st → inv(st[n])) | An Axiom |
| blockstore-prefix | ⊦ st0 ⊑ st ↔ dom st0 ⊆ dom st ∧ (∀ n. n ∈ st0 ∧ n ∈ st → st0[n].list ⊑ st[n].list ∧ st0[n].ladrlist ⊑ st[n].ladrlist ∧ # st0[n].list = # st0[n].ladrlist ∧ # st[n].list = # st[n].ladrlist) | An Axiom |
| at-remove-refsize0 | ⊦ n ∈ st ∧ st[n].ref-size ≠ 0 → remove-refsize0(st)[n] = st[n] | An Axiom |
| in-remove-refsize0 | ⊦ n ∈ remove-refsize0(st) ↔ n ∈ st ∧ st[n].ref-size ≠ 0 | An Axiom |
| adrs-rec | ⊦ (ladr ' + lax).to-adr(n) = @(n, ladr.off, ladr.size) + lax.to-adr(n) | An Axiom |
| adrs-empty | ⊦ ([]).to-adr(n) = [] | An Axiom |
| in | ⊦ adr ∈ st ↔ adr.lnum ∈ st ∧ @(adr.pos, adr.size) ∈ st[adr.lnum].ladrlist | An Axiom |
| at | ⊦ adr ∈ st → st[adr] = st[adr.lnum].list[pos(@(adr.pos, adr.size), st[adr.lnum].ladrlist)] | An Axiom |
| inv-flashsize | ⊦ inv-flashsize(x, lax) ↔ # x = # lax ∧ (∀ n. n < # x → lax[n].size = x[n].flashsize) | An Axiom |
| flashsize-neq-0 | ⊦ a.flashsize ≠ 0 | An Axiom |
| except-refsize-eq | ⊦ st0 =○refsize st1 ↔ (∀ n. (n ∈ st0 ↔ n ∈ st1) ∧ st0[n].list = st1[n].list ∧ st0[n].ladrlist = st1[n].ladrlist) | An Axiom |
| addresslist-in | ⊦ adr ∈ lax.to-adr(n) ↔ adr.lnum = n ∧ @(adr.pos, adr.size) ∈ lax | A User Theorem |
| addresslist-in-lnum-simp | ⊦ @(n0, n1, n2) ∈ lax.to-adr(n) ↔ n0 = n ∧ @(n1, n2) ∈ lax | A User Theorem |
| addresslist-length | ⊦ # lax.to-adr(n) = # lax | A User Theorem |
| at-alloc | ⊦ ¬ n ∈ st ∧ adr ∈ st → st[n, ablock][adr] = st[adr] | A User Theorem |
| at-dealloc | ⊦ n ≠ m ∧ @(m, m0, m1) ∈ st → (st -- n)[@(m, m0, m1)] = st[@(m, m0, m1)] | A User Theorem |
| at-diff | ⊦ @(n, m0, m1) ∈ st ∧ ¬ n ∈ ns → (st \ ns)[@(n, m0, m1)] = st[@(n, m0, m1)] | A User Theorem |
| at-explicit | ⊦ n ∈ st ∧ inv(st) ∧ st[n] = mkblock(x0 + a ' + x1, lax0 + @(m0, m1) ' + lax1, m2) ∧ # x0 = # lax0 → st[@(n, m0, m1)] = a | A User Theorem |
| at-explicit-diff | ⊦ n ∈ st ∧ ¬ n ∈ ns ∧ inv(st \ ns) ∧ st[n] = mkblock(x0 + a ' + x1, lax0 + @(m0, m1) ' + lax1, m2) ∧ # x0 = # lax0 → st[@(n, m0, m1)] = a | A User Theorem |
| at-explicit-other | m ≠ n ⊦ @(m, m0, m1) ∈ st → st[n, ablock][@(m, m0, m1)] = st[@(m, m0, m1)] | A User Theorem |
| at-store-inv | ⊦ inv(st) → (inv(st[n, ablock]) ↔ inv(ablock)) | A User Theorem |
| at-write-app | # x1 = # lax1, # x = # lax, st[n].list = x, st[n].ladrlist = lax ⊦ n ∈ st ∧ adr ∈ st ∧ ¬ dups(lax + lax1) → st[n, mkblock(x + x1, lax + lax1, m)][adr] = st[adr] | A User Theorem |
| at-write-refsize | ⊦ n ∈ st ∧ adr ∈ st → st[n, st[n].ref-size:= m][adr] = st[adr] | A User Theorem |
| at-write-same | st[n].list = x, st[n].ladrlist = lax ⊦ n ∈ st ∧ adr ∈ st → st[n, mkblock(x, lax, m)][adr] = st[adr] | A User Theorem |
| dom-remove-refsize0 | ⊦ dom remove-refsize0(st) ⊆ dom st | A User Theorem |
| except-refsizeeq-comm | ⊦ st0 =○refsize st1 → st1 =○refsize st0 | A User Theorem |
| except-refsizeeq-refl | ⊦ st =○refsize st | A User Theorem |
| except-refsizeeq-trans | ⊦ st0 =○refsize st1 ∧ st1 =○refsize st2 → st0 =○refsize st2 | A User Theorem |
| except-refsizeeq-write-left | ⊦ st0 =○refsize st1 → (st0[n, ablock] =○refsize st1 ↔ n ∈ st0 ∧ ablock.list = st0[n].list ∧ ablock.ladrlist = st0[n].ladrlist) | A User Theorem |
| in-adr-in | ⊦ st[n] = mkblock(x, lax, m0) ∧ @(n, n0, n1) ∈ st → @(n0, n1) ∈ lax | A User Theorem |
| in-alloc | ⊦ ¬ n ∈ st ∧ adr ∈ st → adr ∈ st[n, ablock] | A User Theorem |
| in-dealloc | ⊦ adr ∈ st -- n ↔ adr ∈ st ∧ adr.lnum ≠ n | A User Theorem |
| in-diff | ⊦ adr ∈ st \ ns ↔ adr ∈ st ∧ ¬ adr.lnum ∈ ns | A User Theorem |
| in-diff-explicit | ⊦ ¬ n0 ∈ ns → (@(n0, n1, n2) ∈ st \ ns ↔ @(n0, n1, n2) ∈ st) | A User Theorem |
| in-empty | ⊦ ¬ adr ∈ ∅ | A User Theorem |
| in-in-adr | ⊦ st[n] = mkblock(x, lax, m0) ∧ n ∈ st ∧ @(n0, n1) ∈ lax → @(n, n0, n1) ∈ st | A User Theorem |
| in-store-inv | ⊦ n ∈ st ∧ inv(st) → (inv(st[n]) ↔ true) | A User Theorem |
| in-write-app | # x1 = # lax1, # x = # lax, st[n].list = x, st[n].ladrlist = lax ⊦ n ∈ st → (adr ∈ st[n, mkblock(x + x1, lax + lax1, m)] ↔ adr ∈ st ∨ adr ∈ lax1.to-adr(n)) | A User Theorem |
| in-write-explicit | ⊦ @(n, n0, n1) ∈ st[n, ablock] ↔ @(n0, n1) ∈ ablock.ladrlist | A User Theorem |
| in-write-refsize | ⊦ n ∈ st → (adr ∈ st[n, st[n].ref-size:= m] ↔ adr ∈ st) | A User Theorem |
| in-write-same | st[n].list = x, st[n].ladrlist = lax ⊦ n ∈ st → (adr ∈ st[n, mkblock(x, lax, m)] ↔ adr ∈ st) | A User Theorem |
| inv-add-node | ⊦ inv(mkblock(x, lax, m0)) ∧ ladr.size = a.flashsize ∧ ¬ ladr ∈ lax → inv(mkblock(x + a ', lax + ladr ', m1 + a.flashsize)) | A User Theorem |
| inv-alloc | ⊦ inv(st \ ns) → (inv(st[n, ablock] \ (ns -- n)) ↔ inv(ablock)) | A User Theorem |
| inv-append | ⊦ inv(mkblock(x, lax, m0)) ∧ ladr.size = a.flashsize ∧ ¬ ladr ∈ lax → inv(mkblock(x + a ', lax + ladr ', n1)) | A User Theorem |
| inv-block-empty | ⊦ inv(mkblock([], [], m0)) | A User Theorem |
| inv-diff-n | ⊦ n ∈ st ∧ ¬ n ∈ ns ∧ inv(st \ ns) → inv(st[n]) | A User Theorem |
| inv-eq-list-size | ⊦ inv(mkblock(x, lax, m0)) → (# x = # lax ↔ true) | A User Theorem |
| inv-flashsize-app | ⊦ inv-flashsize(x0, lax0) ∧ inv-flashsize(x1, lax1) → inv-flashsize(x0 + x1, lax0 + lax1) | A User Theorem |
| inv-flashsize-append | ⊦ inv-flashsize(x + a ', lax + ladr ') ↔ inv-flashsize(x, lax) ∧ ladr.size = a.flashsize | A User Theorem |
| inv-flashsize-empty | ⊦ inv-flashsize([], lax) ↔ lax = [] | A User Theorem |
| inv-flashsize-prefix | ⊦ inv-flashsize(x, lax) ∧ n ≤ # x → inv-flashsize(prefixn(n, x), prefixn(n, lax)) | A User Theorem |
| inv-flashsize-prepend | ⊦ inv-flashsize(a ' + x, ladr ' + lax) ↔ a.flashsize = ladr.size ∧ inv-flashsize(x, lax) | A User Theorem |
| inv-flashsize-size | ⊦ inv-flashsize(x, lax) → (# x = # lax ↔ true) | A User Theorem |
| inv-listlen-ls1 | ⊦ inv(mkblock(x, lax, m0)) → ¬ # x < # lax | A User Theorem |
| inv-listlen-ls2 | ⊦ inv(mkblock(x, lax, m0)) → ¬ # lax < # x | A User Theorem |
| inv-nodups | ⊦ inv(mkblock(x, lax, m0)) → ¬ dups(lax) | A User Theorem |
| inv-nodups-app-left | ⊦ inv(mkblock(x, lax0 + lax1, m0)) → ¬ dups(lax0) | A User Theorem |
| inv-prefixn-lax | ⊦ inv(mkblock(x, lax, m0)) → prefixn(# x, lax) = lax | A User Theorem |
| inv-reduce | ⊦ inv(st \ ns) → (inv(st[n, ablock] \ ns) ↔ n ∈ ns ∨ inv(ablock)) | A User Theorem |
| inv-reduce-rem | ⊦ inv(st \ ns) → inv(st \ (ns ++ n)) | A User Theorem |
| inv-remove-refsize0 | ⊦ inv(st) → inv(remove-refsize0(st)) | A User Theorem |
| inv-remove-refsize0-diff | ⊦ inv(st \ ns) ∧ dom remove-refsize0(st) ∩ ns = ∅ → inv(remove-refsize0(st)) | A User Theorem |
| inv-set-refsize | ⊦ inv(ablock.ref-size:= n0) ↔ inv(ablock) | A User Theorem |
| inv-set-sizes | ⊦ inv(mkblock(x, lax, m0)) → inv(mkblock(x, lax, n0)) | A User Theorem |
| inv-store-empty | ⊦ inv(∅) | A User Theorem |
| list-split | ⊦ x ⊑ y + z ∧ # x ≤ # y → (∃ y1. y = x + y1) | A User Theorem |
| notin-notin | ⊦ ¬ n ∈ st → ¬ @(n, n0, n1) ∈ st | A User Theorem |
| prefix-alloc | ⊦ ¬ n ∈ st ∧ inv(st) → st ⊑ st[n, mkblock(x, lax, n0)] | A User Theorem |
| prefix-append-in | ⊦ st0 ⊑ st ∧ n ∈ st ∧ st[n] = mkblock(x, lax, m0) ∧ # lax0 = # y → st0 ⊑ st[n, mkblock(x + y, lax + lax0, n0)] | A User Theorem |
| prefix-append-notin | ⊦ st0 ⊑ st ∧ ¬ n ∈ st → st0 ⊑ st[n, ablock] | A User Theorem |
| prefix-at | ⊦ adr ∈ st0 ∧ st0 ⊑ st1 → st0[adr] = st1[adr] | A User Theorem |
| prefix-del-right | ⊦ st ⊑ st0 -- m ↔ st ⊑ st0 ∧ ¬ m ∈ st | A User Theorem |
| prefix-domsubset | ⊦ st0 ⊑ st1 → dom st0 ⊆ dom st1 | A User Theorem |
| prefix-empty-left | ⊦ ∅ ⊑ st | A User Theorem |
| prefix-empty-right | ⊦ st ⊑ ∅ ↔ st = ∅ | A User Theorem |
| prefix-fwd-in | ⊦ st0 ⊑ st1 ∧ n ∈ st0 → n ∈ st1 | A User Theorem |
| prefix-in | ⊦ adr ∈ st0 ∧ st0 ⊑ st1 → adr ∈ st1 | A User Theorem |
| prefix-just-alloc | ⊦ ¬ n ∈ st1 ∧ st1[n, mkblock([], [], 0)] ⊑ st0 → st1 ⊑ st0 | A User Theorem |
| prefix-notin-fwd | ⊦ ¬ adr ∈ st1 ∧ st0 ⊑ st1 → ¬ adr ∈ st0 | A User Theorem |
| prefix-refl | ⊦ inv(st) → st ⊑ st | A User Theorem |
| prefix-rem | ⊦ st0 \ ns ⊑ st \ ns → (st0 \ ns) -- n ⊑ (st \ ns) -- n | A User Theorem |
| prefix-rem-alloc | ⊦ st0 \ ns ⊑ st \ ns ∧ ¬ n ∈ st → st0 \ (ns ++ n) ⊑ st[n, ablock] \ (ns -- n) | A User Theorem |
| prefix-rem-left | ⊦ st0 \ ns ⊑ st \ ns → (st0 \ ns) -- n ⊑ st \ ns | A User Theorem |
| prefix-remove-refsize0 | ⊦ inv(st) → remove-refsize0(st) ⊑ st | A User Theorem |
| prefix-set-flags | ⊦ st0 ⊑ st ∧ n ∈ st ∧ st[n] = mkblock(x, lax, m) → st0 ⊑ st[n, mkblock(x, lax, n0)] | A User Theorem |
| prefix-trans | ⊦ st0 ⊑ st1 ∧ st1 ⊑ st2 → st0 ⊑ st2 | A User Theorem |
| prefixn-to-adrs | ⊦ prefixn(n, lax.to-adr(m)) = prefixn(n, lax).to-adr(m) | A User Theorem |
| remove-refsize0-empty | ⊦ remove-refsize0(∅) = ∅ | A User Theorem |
| remove-refsize0-eq-nonzero | ⊦ remove-refsize0(st) = st ∧ n ∈ st → (st[n] = mkblock(x, lax, 0) ↔ false) | A User Theorem |
| remove-refsize0-idem | ⊦ remove-refsize0(remove-refsize0(st)) = remove-refsize0(st) | A User Theorem |
| remove-refsize0-one | ⊦ remove-refsize0((∅)[n, mkblock(x, lax, m0)]) = (m0 = 0 ⊃ ∅;(∅)[n, mkblock(x, lax, m0)]) | A User Theorem |
| size-append | ⊦ (x0 + x1).flashsize = x0.flashsize + x1.flashsize | A User Theorem |
| size-one | ⊦ a '.flashsize = a.flashsize | A User Theorem |
| store-inv-rem | ⊦ inv(st) → (inv(st -- n) ↔ true) | A User Theorem |
| to-adrs-append | ⊦ (lax0 + lax1).to-adr(n) = lax0.to-adr(n) + lax1.to-adr(n) | A User Theorem |
| to-adrs-drop | ⊦ dropn(n, lax.to-adr(m)) = dropn(n, lax).to-adr(m) | A User Theorem |
| to-adrs-eq | ⊦ lax0.to-adr(n) = lax1.to-adr(n) ↔ lax0 = lax1 | A User Theorem |
| to-adrs-eq-app | ⊦ lax0.to-adr(n) = lax.to-adr(n) + @(n, m0, m1) ' ↔ lax0 = lax + @(m0, m1) | A User Theorem |
| to-adrs-eq-empty | ⊦ lax.to-adr(n) = [] ↔ lax = [] | A User Theorem |
| to-adrs-eq-one | ⊦ adr ' = lax.to-adr(n) ↔ lax = @(adr.pos, adr.size) ' ∧ adr.lnum = n | A User Theorem |
| to-adrs-in | ⊦ @(m, m0, m1) ∈ lax.to-adr(n) ↔ m = n ∧ @(m0, m1) ∈ lax | A User Theorem |
| to-adrs-one | ⊦ ladr '.to-adr(n) = @(n, ladr.off, ladr.size) ' | A User Theorem |
| to-adrs-sublist | n0 + n1 ≤ # lax ⊦ sublist(n0, n1, lax.to-adr(n)) = sublist(n0, n1, lax).to-adr(n) | A User Theorem |
| to-ards-no-dups | ⊦ dups(lax.to-adr(n)) ↔ dups(lax) | A User Theorem |