| jvalid6 ↔ jvalid3, jvalid5 ↔ jvalid, jvalid2 ↔ jvalid4, err = err0, err = ESUCCESS, err1 = ESUCCESS, fi1 = fi2, gstore1 = gstore2, jmaxino2 = jmaxino, jmaxino4 = jmaxino, jro1 = jro0, jro3 = jro0, ndx2 = ndx4, ndx3 = ndx, ndx5 = ndx, nx0 = nx1, remove-refsize0(gstore0) = gstore0, elems nx1 ∩ jro0 = ∅, (nx.toSet \ nx1.toSet) ∩ dom gstore2 = ∅, dom gstore0 ∪ elems nx1 = dom gstore2 ∪ jro0, jro2 < jmaxino, p_os < pmaxino, fi2.inos < jmaxino, fi0.inos < pmaxino, fi.inos < jmaxino0, inv(gstore2 \ jro0), inv(gstore0), inv-journal(nx, gstore, gstore0, jro), key-cons(ndx), refsize-cons(gstore2, range fi2), refsize-cons(gstore0, range fi0), refsize-cons(gstore, range fi), ri-inj(fi2), ri-inj(fi0), ri-inj(fi), pmaxino ≤ jmaxino, jmaxino0 ≥ jmaxino4, fi2.lebs ⊆ dom gstore2, fi0.lebs ⊆ dom gstore0, ndx.keys.toSet ⊆ dom fi2, range fi2 ⊆ dom nodes(gstore2 ↓, jro0), fi.lebs ⊆ dom gstore, ndx2.keys.toSet ⊆ dom fi, range fi ⊆ dom nodes(gstore ↓, jro), dom gstore2 ⊆ dom gstore, jvalid ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro0), jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), ∃ ndx0. ndx5 = ndx0 + ndx2, ∃ ax, ndx0, ndx1. ndx5 = ndx0 + ndx1 ∧ (err = ESUCCESS → ndx1 = ndx2) ∧ new(ax, nodes(gstore2 ↓, jro3)) ∧ ¬ dups(ax) ∧ # ax = # ndx0 ∧ fi = fi2[ndx0.keys, ax] ∧ nodes(gstore ↓, jro) = nodes(gstore2 ↓, jro3)[ax, ndx0] ∧ abs-log(nx, gstore ↓) = abs-log(nx1, gstore2 ↓) + ax, err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪let jmaxino = 0, jvalid = ? in {index_is_log_empty#(fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; ; jvalid); if ¬ jvalid then {index_get_block_free_size#(fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; ; jmaxino); if jmaxino < ndx2.head.flashsize then jmaxino := 0}; let ndx = [], ax0 = [], n = ? in {index_get_leb_size(fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; ; n); gjournal_split_nodes#(n - jmaxino; ndx2, ndx); if ndx = [] then err := EINVAL else {gjournal_journal_addn#(ndx, jvalid2, fi, fi0, gstore0, pmaxino, p_os; ax0, jvalid1, jmaxino1, jro, gstore, nx, jvalid0; err); if err = ESUCCESS then gjournal_gc_update_index#(jvalid1, fi0, jro, gstore0, nx, pmaxino, p_os, jvalid0; ax0, ndx, jmaxino0, fi, gstore)}}}⟫ ( ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (∃ ndx0. ndx5 = ndx0 + ndx2) ∧ jmaxino0 ≥ jmaxino4 ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi.inos < jmaxino0 ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro) ∧ ri-inj(fi) ∧ ndx2.keys.toSet ⊆ dom fi ∧ range fi ⊆ dom nodes(gstore ↓, jro) ∧ dom gstore2 ⊆ dom gstore ∧ (nx.toSet \ nx1.toSet) ∩ dom gstore2 = ∅ ∧ (∃ ax, ndx0, ndx1. ndx5 = ndx0 + ndx1 ∧ (err = ESUCCESS → ndx1 = ndx2) ∧ new(ax, nodes(gstore2 ↓, jro3)) ∧ ¬ dups(ax) ∧ # ax = # ndx0 ∧ fi = fi2[ndx0.keys, ax] ∧ nodes(gstore ↓, jro) = nodes(gstore2 ↓, jro3)[ax, ndx0] ∧ abs-log(nx, gstore ↓) = abs-log(nx1, gstore2 ↓) + ax)) ∧ (err = ESUCCESS ⊃ # ndx2;0) < (err0 = ESUCCESS ⊃ # ndx4;0)), jmaxino = 0, ndx2 = [], pmaxino = 0, dups(nx1), dups(ndx.keys) |
jvalid2 ↔ jvalid4, jvalid5 ↔ jvalid7, jvalid6 ↔ jvalid3, err = ESUCCESS, err = err0, err1 = ESUCCESS, fi1 = fi2, gstore1 = gstore2, jmaxino = 0, jmaxino2 = jmaxino3, jmaxino4 = jmaxino3, jro1 = jro0, jro3 = jro0, ndx2 = ndx4, ndx3 = ndx, ndx5 = ndx, nx0 = nx1, remove-refsize0(gstore0) = gstore0, (nx.toSet \ nx1.toSet) ∩ dom gstore2 = ∅, elems nx1 ∩ jro0 = ∅, dom gstore0 ∪ elems nx1 = dom gstore2 ∪ jro0, fi.inos < jmaxino0, fi0.inos < pmaxino, fi2.inos < jmaxino3, p_os < pmaxino, jro2 < jmaxino3, inv(gstore0), inv(gstore2 \ jro0), inv-journal(nx, gstore, gstore0, jro), key-cons(ndx), refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), refsize-cons(gstore2, range fi2), ri-inj(fi), ri-inj(fi0), ri-inj(fi2), pmaxino ≤ jmaxino3, jmaxino0 ≥ jmaxino4, dom gstore2 ⊆ dom gstore, range fi ⊆ dom nodes(gstore ↓, jro), ndx2.keys.toSet ⊆ dom fi, fi.lebs ⊆ dom gstore, range fi2 ⊆ dom nodes(gstore2 ↓, jro0), ndx.keys.toSet ⊆ dom fi2, fi0.lebs ⊆ dom gstore0, fi2.lebs ⊆ dom gstore2, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), jvalid7 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro0), ∃ ax, ndx0, ndx1. ndx5 = ndx0 + ndx1 ∧ (err = ESUCCESS → ndx1 = ndx2) ∧ new(ax, nodes(gstore2 ↓, jro3)) ∧ ¬ dups(ax) ∧ # ax = # ndx0 ∧ fi = fi2[ndx0.keys, ax] ∧ nodes(gstore ↓, jro) = nodes(gstore2 ↓, jro3)[ax, ndx0] ∧ abs-log(nx, gstore ↓) = abs-log(nx1, gstore2 ↓) + ax, ∃ ndx0. ndx5 = ndx0 + ndx2, err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪index_is_log_empty#(fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; ; jvalid); if ¬ jvalid then {index_get_block_free_size#(fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; ; jmaxino); if jmaxino < ndx2.head.flashsize then jmaxino := 0}; let ndx = [], ax0 = [], n = ? in {index_get_leb_size(fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; ; n); gjournal_split_nodes#(n - jmaxino; ndx2, ndx); if ndx = [] then err := EINVAL else {gjournal_journal_addn#(ndx, jvalid2, fi, fi0, gstore0, pmaxino, p_os; ax0, jvalid1, jmaxino1, jro, gstore, nx, jvalid0; err); if err = ESUCCESS then gjournal_gc_update_index#(jvalid1, fi0, jro, gstore0, nx, pmaxino, p_os, jvalid0; ax0, ndx, jmaxino0, fi, gstore)}}⟫ ( ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (∃ ndx0. ndx5 = ndx0 + ndx2) ∧ jmaxino0 ≥ jmaxino4 ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi.inos < jmaxino0 ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro) ∧ ri-inj(fi) ∧ ndx2.keys.toSet ⊆ dom fi ∧ range fi ⊆ dom nodes(gstore ↓, jro) ∧ dom gstore2 ⊆ dom gstore ∧ (nx.toSet \ nx1.toSet) ∩ dom gstore2 = ∅ ∧ (∃ ax, ndx0, ndx1. ndx5 = ndx0 + ndx1 ∧ (err = ESUCCESS → ndx1 = ndx2) ∧ new(ax, nodes(gstore2 ↓, jro3)) ∧ ¬ dups(ax) ∧ # ax = # ndx0 ∧ fi = fi2[ndx0.keys, ax] ∧ nodes(gstore ↓, jro) = nodes(gstore2 ↓, jro3)[ax, ndx0] ∧ abs-log(nx, gstore ↓) = abs-log(nx1, gstore2 ↓) + ax)) ∧ (err = ESUCCESS ⊃ # ndx2;0) < (err0 = ESUCCESS ⊃ # ndx4;0)), jmaxino3 = 0, ndx2 = [], pmaxino = 0, dups(ndx.keys), dups(nx1)