| # lpt = # avol, avol[m3] = mapped(buf0), m3 < # avol, n1 < n, ebm-vol-inv(avol), is-aligned(n, EB_PAGE_SIZE), is-aligned(m0, EB_PAGE_SIZE), is-aligned(n1, EB_PAGE_SIZE), n2 + n ≤ # buf, m0 + n ≤ LEB_SIZE, # buf0 ≤ m0, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪avol[m3] := mapped(avol[m3].data + mkempbuf(m0 - # avol[m3].data) + subarray(buf, n2, n1))⟫ (ebm-vol-inv(avol) ∧ # lpt = # avol), err0 = ESUCCESS, n1 = 0 |
Used simplifier rules: ⊦ ⌊err⌋ → err ≠ ESUCCESS; (s)% ⊦ n ≥ m ↔ m ≤ n; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic% ⊦ m < n → n ≠ 0; (s)% ⊦ mapped(buf).data = buf; (s)% ⊦ mapped(buf).mapped?; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat% ⊦ m + n < m + n0 ↔ n < n0; (s)% ⊦ m < n → ¬ n < m; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ aleb.mapped? ↔ (∃ buf. aleb = mapped(buf)); (as)% ⊦ # avol[n, aleb] = # avol; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m < n → (n ≤ m ↔ false); (s)%n < # avol ⊦ ebm-vol-inv(avol) → ( ebm-vol-inv(avol[n, aleb]) ↔ ( avol[n].mapped? → # avol[n].data ≤ LEB_SIZE ∧ is-aligned(# avol[n].data, EB_PAGE_SIZE)) → aleb.mapped? → # aleb.data ≤ LEB_SIZE ∧ is-aligned(# aleb.data, EB_PAGE_SIZE)); (ss)% ⊦ #(buf + buf0) = # buf + # buf0; (s)% ⊦ # mkempbuf(n) = n; (s)% ⊦ # subarray(buf, m, n) = n; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ n ≤ n0 → (m + (n0 - n)) + n = m + n0; (s)% ⊦ EB_PAGE_SIZE ≠ 0; (s)%m ≠ 0, is-aligned(n1, m) ⊦ is-aligned(n0 + n1, m) ↔ is-aligned(n0, m); (s)% ⊦ mapped(buf) = mapped(buf0) ↔ buf = buf0; (s)