| # buf2 = EB_PAGE_SIZE, LEB_SIZE = n1 + logoff0, LEB_SIZE = n0 + # buf0, avol[m5] = mapped(buf0), m5 < # avol, logoff0 < LEB_SIZE, ebm-vol-inv(avol), is-aligned(logoff0, EB_PAGE_SIZE), is-encoded(log0, buf0), is-encoded(log, subarray(buf0, 0, logoff0)), logoff0 + EB_PAGE_SIZE ≤ LEB_SIZE, logoff0 ≤ # buf0, # buf0 ≤ LEB_SIZE, err = ESUCCESS → is-encoded(rnd, subarray(buf0 + mkempbuf(n0), logoff0, EB_PAGE_SIZE)), err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪logoff := logoff0 + EB_PAGE_SIZE⟫ ( logoff ≤ LEB_SIZE ∧ is-aligned(logoff, EB_PAGE_SIZE) ∧ (err = ESUCCESS ∨ err = ENOENT ∨ ⌊err⌋ ) ∧ avol[m5].mapped? ∧ (err = ESUCCESS → logoff ≤ # avol[m5].data ∧ is-encoded(log, subarray(avol[m5].data, 0, logoff))) ∧ (err = ENOENT → is-encoded(log, avol[m5].data)) ∧ LEB_SIZE < n1 + logoff), copy(buf0 + mkempbuf(n0), logoff0, buf2, 0, EB_PAGE_SIZE) = emptypage, err = ESUCCESS, n1 = 0 |
Used simplifier rules: nat-stuff1: ⊦ n = n0 + n1 → (n0 + n1 + n2 ≤ n ↔ n2 = 0);% ⊦ ⌊err⌋ → err ≠ ESUCCESS; (s)% ⊦ EB_PAGE_SIZE ≠ 0; (s)%n ≠ 0 ⊦ is-aligned(n, n); (s)%m ≠ 0, is-aligned(n1, m) ⊦ is-aligned(n0 + n1, m) ↔ is-aligned(n0, m); (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ mapped(buf).mapped?; (s)% ⊦ mapped(buf).data = buf; (s)% ⊦ is-encoded(nx0, buf) → (is-encoded(nx1, buf) ↔ nx0 = nx1); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic%transitivity: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification oelem[nat-set]% ⊦ EB_PAGE_SIZE + n = 0 ↔ false; (s)% ⊦ m ≤ n → (n ≤ m ↔ m = n); (s)% ⊦ # mkempbuf(n) = n; (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)% ⊦ m < m + n ↔ n ≠ 0; (s)% ⊦ m +1 = m + 1; (s)% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s)% ⊦ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1; (ws)% ⊦ m ≠ n → (m ≤ n ↔ m < n); (s)% ⊦ ¬ ⌊ENOENT⌋ ; (s)%# buf ≤ n, n + m1 ≤ # buf + # buf0 ⊦ copy(buf + buf0, n, buf1, m0, m1) = copy(buf0, n - # buf, buf1, m0, m1); (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]%# buf = n ⊦ subarray(buf, 0, n) = buf; (s)