| # buf3 = EB_PAGE_SIZE, # buf = # buf1, LEB_SIZE = n1 + logoff0, avol[m5] = mapped(buf0), buf1 = buf3, buf2 = buf, err = err0, m0 = EB_PAGE_SIZE, n = EB_PAGE_SIZE, n0 = 0, 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)), range=(buf1, n0 + n, buf, n0 + n, # buf1 - n0 + n), range=(buf1, 0, buf, 0, n0), logoff0 + EB_PAGE_SIZE ≤ LEB_SIZE, logoff0 ≤ # buf0, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪logoff := logoff0 + m0⟫ ( logoff ≤ LEB_SIZE ∧ # buf2 = m0 ∧ is-aligned(logoff, # buf2) ∧ (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), err = ESUCCESS, n1 = 0 |
Used simplifier rules: nat-stuff1: ⊦ n = n0 + n1 → (n0 + n1 + n2 ≤ n ↔ n2 = 0);% ⊦ n + 0 = n; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ range=(buf, n0, buf0, n1, 0) ↔ n0 ≤ # buf ∧ n1 ≤ # buf0; (s)% ⊦ 0 ≤ m; (s)% ⊦ ⌊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)% ⊦ m - m = 0; (s)% ⊦ 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%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]%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat% ⊦ EB_PAGE_SIZE + n = 0 ↔ false; (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 → (n ≤ m ↔ m = n); (s)% ⊦ m ≤ m; (s)% ⊦ ¬ ⌊ENOENT⌋ ; (s)