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: |
|---|---|---|
| refine-contains | ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0), syn1 ↔ syn2 ⊦ ⟪btree_index_contains#(key, adr0, adr, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; syn1, rp, zh, istore; err)⟫ ⟨index_index_contains#(key, fi, fi0, ginval, gstore, gstore1, nx, maxino, ginval1, syn; syn2; err0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ (syn1 ↔ syn2) ∧ err = err0) | A Proof Obligation |
| refine-lookup | ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0), syn1 ↔ syn2, adr0 = adr1 ⊦ ⟪btree_index_lookup#(key, adr2, adr, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; syn1, adr0, rp, zh, istore; err)⟫ ⟨index_index_lookup#(key, fi, fi0, ginval, gstore, gstore1, nx, maxino, ginval1, syn; syn2, adr1; err0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ (syn1 ↔ syn2) ∧ adr0 = adr1 ∧ err = err0) | A Proof Obligation |
| refine-store | ¬ adr ∈ fi, adr ∈ gstore, key-cons(key, gstore[adr].nd), ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr0, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr0, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0), adr1 = adr2, syn1 ↔ syn2 ⊦ ⟪btree_index_store#(key, adr, adr3, adr0, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; adr1, syn1, rp, zh, istore)⟫ ⟨index_index_store#(key, adr, fi0, ginval, gstore, gstore1, nx, maxino, ginval1, syn; adr2, syn2, fi)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr0, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ adr1 = adr2 ∧ (syn1 ↔ syn2)) | A Proof Obligation |
| refine-remove | ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0), adr0 = adr1, syn1 ↔ syn2 ⊦ ⟪btree_index_remove#(key, adr2, adr, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; adr0, syn1, rp, zh, istore)⟫ ⟨index_index_remove#(key, fi0, ginval, gstore, gstore1, nx, maxino, ginval1, syn; adr1, syn2, fi)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ adr0 = adr1 ∧ (syn1 ↔ syn2)) | A Proof Obligation |
| refine-truncate | ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0), as = as0 ⊦ ⟪btree_index_truncate#(key, n, adr0, adr, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; as, rp, zh, istore)⟫ ⟨index_index_truncate#(key, n, fi0, ginval, gstore, gstore1, nx, maxino, ginval1, syn; as0, fi)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ as = as0) | A Proof Obligation |
| refine-entries | ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0), strings = strings0 ⊦ ⟪btree_index_entries#(key, adr0, adr, istore, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; strings, rp, zh; err)⟫ ⟨index_index_entries#(key, fi, fi0, ginval, gstore, gstore1, nx, maxino, ginval1, syn; strings0; err0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ strings = strings0 ∧ err = err0) | A Proof Obligation |
| refine-read-gnd | adr ∈ gstore, ¬ adr.lnum ∈ ginval, ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr0, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr0, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0), gnd = gnd0 ⊦ ⟪btree_read_gnd#(adr, adr0, istore, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; gnd; err)⟫ ⟨index_read_gnd#(adr, fi, fi0, ginval, gstore, gstore1, nx, maxino, ginval1, syn; gnd0; err0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr0, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ gnd = gnd0 ∧ err = err0) | A Proof Obligation |
| refine-read-gblock | maxino ∈ gstore, ¬ maxino ∈ ginval, ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino0 = maxino1, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0), ax = ax0, gndx = gndx0 ⊦ ⟪btree_read_gblock_nodes#(maxino, adr, istore, istore0, ginval0, gstore0, gstore2, nx0, maxino1, ginval2, pstate, syn0; ax, gndx; err)⟫ ⟨index_read_gblock_nodes#(maxino, fi, fi0, ginval, gstore, gstore1, nx, maxino0, ginval1, syn; ax0, gndx0; err0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino0 = maxino1 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ ax = ax0 ∧ gndx = gndx0 ∧ err = err0) | A Proof Obligation |
| refine-get-gc-block | ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0), n = n0 ⊦ ⟪btree_get_gc_block#(adr, istore, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; n; err)⟫ ⟨index_get_gc_block#(fi, fi0, ginval, gstore, gstore1, nx, maxino, ginval1, syn; n0; err0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ n = n0 ∧ err = err0) | A Proof Obligation |
| refine-add-gnds | nx ≠ [], ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0), ax = ax0 ⊦ ⟪btree_add_gnds#(gndx, adr, istore, istore0, ginval0, gstore2, nx0, maxino0, ginval2; ax, gstore0, pstate, syn0; err)⟫ ⟨index_add_gnds#(gndx, fi, fi0, ginval, gstore1, nx, maxino, ginval1; ax0, gstore; syn, err0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ ax = ax0 ∧ err = err0) | A Proof Obligation |
| refine-set-gblock-refsize | maxino ∈ gstore, ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino0 = maxino1, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0) ⊦ ⟪btree_set_gblock_refsize#(maxino, n, adr, istore, istore0, ginval0, gstore2, nx0, maxino1, ginval2, pstate, syn0; gstore0)⟫ ⟨index_set_gblock_refsize#(maxino, n, fi, fi0, ginval, gstore1, nx, maxino0, ginval1, syn; gstore)⟩ ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino0 = maxino1 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) | A Proof Obligation |
| refine-get-gblock-refsize | maxino ∈ gstore, ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino0 = maxino1, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0) ⊦ ⟪btree_get_gblock_refsize#(maxino, adr, istore, istore0, ginval0, gstore0, gstore2, nx0, maxino1, ginval2, pstate, syn0; ; n)⟫ ⟨index_get_gblock_refsize#(maxino, fi, fi0, ginval, gstore, gstore1, nx, maxino0, ginval1, syn; ; n0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino0 = maxino1 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ n = n0) | A Proof Obligation |
| refine-allocate-gnd | syn, ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0) ⊦ ⟪btree_allocate_gnd#(adr, istore, istore0, gstore2, maxino0, ginval2, syn0; ginval0, gstore0, nx0, pstate; err)⟫ ⟨index_allocate_gnd#(fi, fi0, gstore1, maxino, ginval1, syn; ginval, gstore, nx; err0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ err = err0) | A Proof Obligation |
| refine-deallocate-gnd | syn, n ∈ gstore, ¬ n ∈ nx, ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0) ⊦ ⟪btree_deallocate_gnd#(n, adr, istore, istore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; ginval0, gstore0; err)⟫ ⟨index_deallocate_gnd#(n, fi, fi0, gstore1, nx, maxino, ginval1, syn; ginval, gstore; err0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ err = err0) | A Proof Obligation |
| refine-commit | syn, dom remove-refsize0(gstore) ∩ ginval = ∅, ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0), ginval3 = ginval4, maxino1 = maxino2 ⊦ ⟪btree_commit#(maxino1, rp; ginval3, adr0, zh, adr, istore, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; err)⟫ ⟨index_commit#(maxino2, fi, syn; ginval4, ginval, gstore, fi0, gstore1, nx, maxino, ginval1; err0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ ginval3 = ginval4 ∧ err = err0) | A Proof Obligation |
| refine-requires-commit | ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0) ⊦ ⟪btree_requires_commit#(adr, istore, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; ; syn1)⟫ ⟨index_requires_commit#(fi, fi0, ginval, gstore, gstore1, nx, maxino, ginval1, syn; ; syn2)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ (syn1 ↔ syn2)) | A Proof Obligation |
| initialization | maxino0 = LEB_SIZE, maxino1 = maxino2 ⊦ ⟪btree_format#(maxino3, maxino0, maxino1; adr, adr0, istore, istore0, ginval1, gstore1, gstore2, nx0, maxino4, ginval2, pstate, syn0; rp, err)⟫ ( ( err = ESUCCESS → ⟨index_format#(maxino3, maxino0, maxino2; ; fi1, fi2, ginval3, gstore3, gstore4, nx1, maxino5, ginval4, syn1, err0)⟩ ( ( ginval3 = ginval1 ∧ gstore3 = gstore1 ∧ gstore4 = gstore2 ∧ nx1 = nx0 ∧ maxino5 = maxino4 ∧ ginval4 = ginval2 ∧ btree-inv(rp, adr0, istore, istore0, zh, fi1, fi2) ∧ ri = fi1 ∧ fi3 = fi2 ∧ (syn1 ↔ syn0)) ∧ err = err0)) ∧ ( err ≠ ESUCCESS → (∀ fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn. ⟨index_format#(maxino3, maxino0, maxino2; ; fi1, fi2, ginval3, gstore3, gstore4, nx1, maxino5, ginval4, syn1, err0)⟩ ( fi = fi1 ∧ fi0 = fi2 ∧ ginval = ginval3 ∧ gstore = gstore3 ∧ gstore0 = gstore4 ∧ nx = nx1 ∧ maxino = maxino5 ∧ ginval0 = ginval4 ∧ (syn ↔ syn1) ∧ err = err0)))) | A Proof Obligation |
| recovery | adr = adr0, istore = remove-refsize0(crash(istore0, istore1)), istore2 = istore1, ginval1 = ginval2, gstore1 = crash(gstore2, gstore3, ginval2, nx0), gstore4 = gstore3, nx1 = nx0, maxino0 = maxino1, ginval3 = ginval4, ginval5 = ginval2, gstore5 = gstore2, gstore6 = gstore3, nx2 = nx0, maxino2 = maxino1, ginval6 = ginval4, btree-inv(rp, adr0, istore0, istore1, zh, fi1, fi2), ri = fi1, fi3 = fi2, syn0 ↔ syn1, syn1, inv-journal(nx2, gstore5, gstore6, ginval5), ri-inj(fi1), ri-inj(fi2), btree-inv(rp, adr0, istore0, istore1, zh, ri, fi3), inv-journal(nx0, gstore2, gstore3, ginval2), inv-index(istore0, istore1), inv-state(pstate, nx0, gstore2, istore0, syn1), maxino3 = maxino4, nx3 = nx4, ginval7 = ginval8 ⊦ ⟪btree_recover#(; maxino3, nx3, ginval7, adr1, adr, istore, istore2, ginval1, gstore1, gstore4, nx1, maxino0, ginval3, pstate0, syn2; rp0, err)⟫ ( ( err = ESUCCESS → (∃ fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn. ( ginval = ginval5 ∧ gstore = crash(gstore5, gstore6, ginval5, nx2) ∧ gstore0 = gstore6 ∧ nx = nx2 ∧ maxino = maxino2 ∧ ginval0 = ginval6 ∧ fi0 = fi2) ∧ ⟨index_recover#(; maxino4, nx4, ginval8, fi0, nx, maxino, ginval0, ginval, gstore, gstore0; fi, syn, err0)⟩ ( ( ginval = ginval1 ∧ gstore = gstore1 ∧ gstore0 = gstore4 ∧ nx = nx1 ∧ maxino = maxino0 ∧ ginval0 = ginval3 ∧ btree-inv(rp0, adr, istore, istore2, zh0, fi, fi0) ∧ ri0 = fi ∧ fi4 = fi0 ∧ (syn ↔ syn2)) ∧ maxino3 = maxino4 ∧ nx3 = nx4 ∧ ginval7 = ginval8 ∧ err = err0))) ∧ ( err ≠ ESUCCESS → (∀ fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn. ⟨index_recover#(; maxino4, nx4, ginval8, fi5, nx5, maxino5, ginval9, ginval10, gstore7, gstore8; fi6, syn3, err0)⟩ ( fi = fi6 ∧ fi0 = fi5 ∧ ginval = ginval10 ∧ gstore = gstore7 ∧ gstore0 = gstore8 ∧ nx = nx5 ∧ maxino = maxino5 ∧ ginval0 = ginval9 ∧ (syn ↔ syn3) ∧ maxino3 = maxino4 ∧ nx3 = nx4 ∧ ginval7 = ginval8 ∧ err = err0)))) | A Proof Obligation |
| refine-sync | ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0) ⊦ ⟪btree_sync#(adr, istore, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2; pstate, syn0; err)⟫ ⟨index_sync#(fi, fi0, ginval, gstore, gstore1, nx, maxino, ginval1; ; syn, err0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ err = err0) | A Proof Obligation |
| synced | syn, ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1) ⊦ syn0 | A Proof Obligation |
| refine-get-block-free-size | ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0) ⊦ ⟪btree_get_block_free_size#(adr, istore, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; ; n)⟫ ⟨index_get_block_free_size#(fi, fi0, ginval, gstore, gstore1, nx, maxino, ginval1, syn; ; n0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ n = n0) | A Proof Obligation |
| refine-is-log-empty | ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0) ⊦ ⟪btree_is_log_empty#(adr, istore, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; ; syn1)⟫ ⟨index_is_log_empty#(fi, fi0, ginval, gstore, gstore1, nx, maxino, ginval1, syn; ; syn2)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ (syn1 ↔ syn2)) | A Proof Obligation |
| refine-get-leb-size | ginval = ginval0, gstore = gstore0, gstore1 = gstore2, nx = nx0, maxino = maxino0, ginval1 = ginval2, btree-inv(rp, adr, istore, istore0, zh, fi, fi0), ri = fi, fi1 = fi0, syn ↔ syn0, inv-journal(nx, gstore, gstore1, ginval), ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, istore, istore0, zh, ri, fi1), inv-journal(nx0, gstore0, gstore2, ginval0), inv-index(istore, istore0), inv-state(pstate, nx0, gstore0, istore, syn0) ⊦ ⟪btree_get_leb_size(adr, istore, istore0, ginval0, gstore0, gstore2, nx0, maxino0, ginval2, pstate, syn0; ; n)⟫ ⟨index_get_leb_size(fi, fi0, ginval, gstore, gstore1, nx, maxino, ginval1, syn; ; n0)⟩ ( ( ginval = ginval0 ∧ gstore = gstore0 ∧ gstore1 = gstore2 ∧ nx = nx0 ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ btree-inv(rp, adr, istore, istore0, zh, fi, fi0) ∧ ri = fi ∧ fi1 = fi0 ∧ (syn ↔ syn0)) ∧ n = n0) | A Proof Obligation |