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: |
|---|---|---|
| initialization | jmaxino = LEB_SIZE, jvalid0 ↔ jvalid1 ⊦ ⟪gjournal_format# (jmaxino0, jmaxino, jvalid0; jmaxino1, fi0, fi1, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid2; jvalid3, jmaxino2, jro0, jvalid1, err)⟫ ( ( err = ESUCCESS → ⟨aubifs_core_format#(jmaxino0, jmaxino, jvalid1; ; ri0, fi2, ro0, fo0, fs0, log0, jvalid4, err0)⟩ ( ( jro0.keys = ro0 ∧ p_os.keys = fo0 ∧ fi0 = ri0 ∧ fi1 = fi2 ∧ log0 = abs-log(nx, gstore ↓) ∧ fs0 = nodes(gstore ↓, jro) ∧ (jvalid4 → jvalid2)) ∧ err = err0)) ∧ ( err ≠ ESUCCESS → (∀ ri, fi, ro, fo, fs, log, jvalid. ⟨aubifs_core_format#(jmaxino0, jmaxino, jvalid1; ; ri0, fi2, ro0, fo0, fs0, log0, jvalid4, err0)⟩ (ri = ri0 ∧ fi = fi2 ∧ ro = ro0 ∧ fo = fo0 ∧ fs = fs0 ∧ log = log0 ∧ (jvalid ↔ jvalid4) ∧ err = err0)))) | A Proof Obligation |
| refine-newino | jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), key = key0 ⊦ ⟪gjournal_index_newino#(; key, jmaxino)⟫ ⟨aubifs_core_index_newino#(ri, fi1, ro, fo, fs, log, jvalid; key0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ key = key0) | A Proof Obligation |
| refine-contains | jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), jvalid2 ↔ jvalid3 ⊦ ⟪gjournal_index_contains#(key, fi, fi0, jro0, gstore, gstore0, nx, pmaxino, p_os, jvalid0; jvalid2; err)⟫ ⟨aubifs_core_index_contains#(key, ri, fi1, ro, fo, fs, log, jvalid; jvalid3; err0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ (jvalid2 ↔ jvalid3) ∧ err = err0) | A Proof Obligation |
| refine-lookup | ri-cons(ri, fs), jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), jvalid2 ↔ jvalid3, nd = nd0 ⊦ ⟪gjournal_index_lookup#(key, fi, fi0, jro0, gstore, gstore0, nx, pmaxino, p_os, jvalid0; jvalid2, nd; err)⟫ ⟨aubifs_core_index_lookup#(key, ri, fi1, ro, fo, fs, log, jvalid; jvalid3, nd0; err0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ (jvalid2 ↔ jvalid3) ∧ nd = nd0 ∧ err = err0) | A Proof Obligation |
| refine-store | ¬ adr ∈ ri, adr ∈ fs, key-cons(key, fs[adr]), jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_index_store#(key, adr, fi0, jro0, gstore0, nx, pmaxino, p_os, jvalid0; jmaxino, fi, gstore)⟫ ⟨aubifs_core_index_store#(key, adr, fi1, ro, fo, fs, log, jvalid; ri)⟩ (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) | A Proof Obligation |
| refine-remove | jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_index_remove#(key, fi0, jro0, gstore0, nx, pmaxino, p_os, jvalid0; fi, gstore)⟫ ⟨aubifs_core_index_remove#(key, fi1, ro, fo, fs, log, jvalid; ri)⟩ (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) | A Proof Obligation |
| refine-truncate | jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_index_truncate#(key, n, jvalid1, fi0, jro0, gstore0, nx, pmaxino, p_os, jvalid0; fi, gstore)⟫ ⟨aubifs_core_index_truncate#(key, n, fi1, ro, fo, fs, log, jvalid; ri)⟩ (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) | A Proof Obligation |
| refine-entries | jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), strings = strings0 ⊦ ⟪gjournal_index_entries#(key, fi, fi0, jro0, gstore, gstore0, nx, pmaxino, p_os, jvalid0; strings; err)⟫ ⟨aubifs_core_index_entries#(key, ri, fi1, ro, fo, fs, log, jvalid; strings0; err0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ strings = strings0 ∧ err = err0) | A Proof Obligation |
| refine-get | adr ∈ fs, jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), nd = nd0 ⊦ ⟪gjournal_journal_get#(adr, fi, fi0, jro0, gstore, gstore0, nx, pmaxino, p_os, jvalid0; nd; err)⟫ ⟨aubifs_core_journal_get#(adr, ri, fi1, ro, fo, fs, log, jvalid; nd0; err0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ nd = nd0 ∧ err = err0) | A Proof Obligation |
| refine-add1 | ri-cons(ri, fs), node-cons(nd.key, nd), jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), adr = adr0 ⊦ ⟪gjournal_journal_add1#(nd, jvalid2, fi, fi0, gstore0, pmaxino, p_os; adr, jvalid1, jmaxino0, jro0, gstore, nx, jvalid0; err)⟫ ⟨aubifs_core_journal_add1#(nd, ri, fi1, ro, fo; adr0, fs, log; jvalid, err0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ adr = adr0 ∧ err = err0) | A Proof Obligation |
| refine-add2 | ri-cons(ri, fs), node-cons(nd.key, nd), node-cons(nd0.key, nd0), jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), adr = adr0, adr1 = adr2 ⊦ ⟪gjournal_journal_add2#(nd, nd0, jvalid2, fi, fi0, gstore0, pmaxino, p_os; adr, adr1, jvalid1, jmaxino0, jro0, gstore, nx, jvalid0; err)⟫ ⟨aubifs_core_journal_add2#(nd, nd0, ri, fi1, ro, fo; adr0, adr2, fs, log; jvalid, err0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ adr = adr0 ∧ adr1 = adr2 ∧ err = err0) | A Proof Obligation |
| refine-add3 | ri-cons(ri, fs), node-cons(nd.key, nd), node-cons(nd0.key, nd0), node-cons(nd1.key, nd1), jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), adr = adr0, adr1 = adr2, adr3 = adr4 ⊦ ⟪gjournal_journal_add3# (nd, nd0, nd1, jvalid2, fi, fi0, gstore0, pmaxino, p_os; adr, adr1, adr3, jvalid1, jmaxino0, jro0, gstore, nx, jvalid0; err)⟫ ⟨aubifs_core_journal_add3#(nd, nd0, nd1, ri, fi1, ro, fo; adr0, adr2, adr4, fs, log; jvalid, err0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ adr = adr0 ∧ adr1 = adr2 ∧ adr3 = adr4 ∧ err = err0) | A Proof Obligation |
| refine-add4 | ri-cons(ri, fs), node-cons(nd.key, nd), node-cons(nd0.key, nd0), node-cons(nd1.key, nd1), node-cons(nd2.key, nd2), jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), adr = adr0, adr1 = adr2, adr3 = adr4, adr5 = adr6 ⊦ ⟪gjournal_journal_add4# (nd, nd0, nd1, nd2, jvalid2, fi, fi0, gstore0, pmaxino, p_os; adr, adr1, adr3, adr5, jvalid1, jmaxino0, jro0, gstore, nx, jvalid0; err)⟫ ⟨aubifs_core_journal_add4#(nd, nd0, nd1, nd2, ri, fi1, ro, fo; adr0, adr2, adr4, adr6, fs, log; jvalid, err0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ adr = adr0 ∧ adr1 = adr2 ∧ adr3 = adr4 ∧ adr5 = adr6 ∧ err = err0) | A Proof Obligation |
| refine-gc | ri-cons(ri, fs), jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_journal_gc#(jvalid2, fi0, gstore0, pmaxino, p_os; jvalid1, jmaxino0, jmaxino, fi, jro0, gstore, nx, jvalid0)⟫ ⟨aubifs_core_journal_gc#(fi1, ro, fo; ri, fs, log; jvalid)⟩ (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) | A Proof Obligation |
| refine-check-commit | ri-cons(ri, fs), jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_check_commit#(jmaxino, jro, fi; fi0, jro0, gstore, gstore0, nx, pmaxino, p_os, jvalid0; err)⟫ ⟨aubifs_core_check_commit#(ri, ro; fi1, fo, fs, log, jvalid; err0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ err = err0) | A Proof Obligation |
| refine-commit | ri-cons(ri, fs), jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_commit#(jmaxino, jro, fi; fi0, jro0, gstore, gstore0, nx, pmaxino, p_os, jvalid0; err)⟫ ⟨aubifs_core_commit#(ri, ro; fs, fi1, fo, log; jvalid, err0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ err = err0) | A Proof Obligation |
| refine-orphans-contains | key.inode?, jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), jvalid2 ↔ jvalid3 ⊦ ⟪gjournal_orphans_contains#(key, jro; jvalid2)⟫ ⟨aubifs_core_orphans_contains#(key, ri, fi1, ro, fo, fs, log, jvalid; jvalid3)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ (jvalid2 ↔ jvalid3)) | A Proof Obligation |
| refine-orphans-insert | key.inode?, jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_orphans_insert#(key; jmaxino, jro)⟫ ⟨aubifs_core_orphans_insert#(key, ri, fi1, fo, fs, log, jvalid; ro)⟩ (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) | A Proof Obligation |
| refine-orphans-remove | key.inode?, jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_orphans_remove#(key; jro)⟫ ⟨aubifs_core_orphans_remove#(key, ri, fi1, fo, fs, log, jvalid; ro)⟩ (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) | A Proof Obligation |
| recovery | jro = jro0, gstore = crash(gstore0, gstore1, jro0, nx), gstore2 = gstore1, nx0 = nx, pmaxino = jmaxino, p_os = jro1, fi0 = fi1, jro2.keys = ro0, jro1.keys = fo0, fi2 = ri0, fi1 = fi3, log0 = abs-log(nx, gstore0 ↓), fs0 = nodes(gstore0 ↓, jro0), jvalid0 → jvalid1, jvalid1, ri-inj(ri0), ri-inj(fi3), log-cons(log0, fs0), ro0.inodes?, fo0.inodes?, jro2 < jmaxino0, jro1 < jmaxino, jmaxino ≤ jmaxino0, fi2.inos < jmaxino0, fi1.inos < jmaxino, jmaxino0 ≠ 0, jmaxino ≠ 0, jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore0, jro0), fi2.lebs ⊆ dom gstore0, fi1.lebs ⊆ dom gstore1, refsize-cons(gstore0, range fi2), refsize-cons(gstore1, range fi1), inv-journal(nx, gstore0, gstore1, jro0), ri-inj(fi2), ri-inj(fi1), log1 = ax, ks = ks0, jvalid3 ↔ jvalid4 ⊦ ⟪gjournal_recover# (jvalid3; log1, ks, jmaxino1, jro3, fi4, fi0, jro, gstore, gstore2, nx0, pmaxino, p_os, jvalid5; jvalid6, jmaxino2, jvalid4, err)⟫ ( ( err = ESUCCESS → (∃ ri, fi, ro, fo, fs, log, jvalid. (fi = fi3 ∧ fo = fo0 ∧ fs = fs0 ∧ log = log0) ∧ ⟨aubifs_core_recover#(jvalid4; ax, ks0, fi, ro, fo, log, fs; ri, jvalid, err0)⟩ ( ( jro3.keys = ro ∧ p_os.keys = fo ∧ fi4 = ri ∧ fi0 = fi ∧ log = abs-log(nx0, gstore ↓) ∧ fs = nodes(gstore ↓, jro) ∧ (jvalid → jvalid5)) ∧ log1 = ax ∧ ks = ks0 ∧ err = err0))) ∧ ( err ≠ ESUCCESS → (∀ ri, fi, ro, fo, fs, log, jvalid. ⟨aubifs_core_recover#(jvalid4; ax, ks0, fi5, ro1, fo1, log1, fs1; ri1, jvalid7, err0)⟩ (ri = ri1 ∧ fi = fi5 ∧ ro = ro1 ∧ fo = fo1 ∧ fs = fs1 ∧ log = log1 ∧ (jvalid ↔ jvalid7) ∧ log1 = ax ∧ ks = ks0 ∧ err = err0)))) | A Proof Obligation |
| synced | jvalid, jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0) ⊦ jvalid0 | A Proof Obligation |
| refine-sync | jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_journal_sync#(fi, fi0, jro0, gstore, gstore0, nx, pmaxino, p_os; jvalid0; err)⟫ ⟨aubifs_core_journal_sync#(ri, fi1, ro, fo, fs, log; ; jvalid, err0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ err = err0) | A Proof Obligation |
| refine-add5 | ri-cons(ri, fs), node-cons(nd.key, nd), node-cons(nd0.key, nd0), node-cons(nd1.key, nd1), node-cons(nd2.key, nd2), node-cons(nd3.key, nd3), jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), adr = adr0, adr1 = adr2, adr3 = adr4, adr5 = adr6, adr7 = adr8 ⊦ ⟪gjournal_journal_add5# (nd, nd0, nd1, nd2, nd3, jvalid2, fi, fi0, gstore0, pmaxino, p_os; adr, adr1, adr3, adr5, adr7, jvalid1, jmaxino0, jro0, gstore, nx, jvalid0; err)⟫ ⟨aubifs_core_journal_add5#(nd, nd0, nd1, nd2, nd3, ri, fi1, ro, fo; adr0, adr2, adr4, adr6, adr8, fs, log; jvalid, err0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ adr = adr0 ∧ adr1 = adr2 ∧ adr3 = adr4 ∧ adr5 = adr6 ∧ adr7 = adr8 ∧ err = err0) | A Proof Obligation |
| prepost-remove-nonend-blocks | n ∈ gstore, ¬ n ∈ ginval, ax = ax0, inv(gstore \ ginval) ⊦ ⟪gjournal_remove_nonend_blocks#(n, ri, fi, ginval, gstore, gstore0, nx0, maxino, ns, boolvar0; ax; err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → ax = ax0 + prefixn(valid-group-nodes(gstore[n].gndlist), gstore[n].ladrlist.to-adr(n)))) | A User Theorem |
| prepost-restore-log | elems nx ⊆ dom gstore, elems nx ∩ ginval = ∅, inv(gstore \ ginval) ⊦ ⟪gjournal_restore_log#(nx, ri, fi, ginval, gstore, gstore0, nx0, maxino, ns, boolvar0; ax; err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → ax = abs-log(nx, gstore ↓))) | A User Theorem |