| # avol0 = # avol1, # buf = (n2 + n4) * LEB_SIZE, # avol1 = n3 + n5 + n2 + n4, avol = avol0[n5 + n4, mapped(mkbuf(0))], err = err0, lebs(avol0, n5, n4) = subarray(buf, 0, n4 * LEB_SIZE), m = 0, m0 = n5 + n4, n = 0, n0 = LEB_SIZE, n1 = n4 * LEB_SIZE, n < n0, n5 + n4 < # avol1, n5 + n4 < # avol0, ebm-vol-inv(avol), ebm-vol-inv(avol0[n5 + n4, mapped(mkbuf(0))]), ebm-vol-inv(avol1), ebm-vol-inv(avol0), is-aligned(n, EB_PAGE_SIZE), is-aligned(LEB_SIZE, EB_PAGE_SIZE), mapped-full?(avol0, n5, n4), range=(avol0, n5 + n2 + n4, avol1, n5 + n2 + n4, n3), range=(avol0, 0, avol1, 0, n5), n4 * LEB_SIZE + LEB_SIZE ≤ # buf, n5 + n2 + n4 ≤ # avol1, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪n6 := n4 + 1⟫ ( n6 ≤ n2 + n4 ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ # avol = # avol1 ∧ range=(avol, 0, avol1, 0, n5) ∧ range=(avol, n5 + n2 + n4, avol1, n5 + n2 + n4, n3) ∧ (err = ESUCCESS → lebs(avol, n5, n6) = subarray(buf, 0, n6 * LEB_SIZE) ∧ mapped-full?(avol, n5, n6)) ∧ n4 < n6), n3 + n2 = 0, err = ESUCCESS, n2 = 0 |
Used simplifier rules: ⊦ EB_PAGE_SIZE ≠ 0; (s)%n ≠ 0 ⊦ is-aligned(0, n); (s)% ⊦ 0 < m ↔ m ≠ 0; (s)% ⊦ LEB_SIZE ≠ 0; (s)% ⊦ ⌊err⌋ → err ≠ ESUCCESS; (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ # avol[n, aleb] = # avol; (s)% ⊦ n + 0 = n; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ ¬ m + n < m; (s)%m0 + m ≤ n ⊦ range=(avol[n, aleb], m0, avol0, m1, m) ↔ range=(avol, m0, avol0, m1, m); (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m + m0 ≤ m ↔ m0 = 0; (s)%n < m0 ⊦ range=(avol[n, aleb], m0, avol0, m1, m) ↔ range=(avol, m0, avol0, m1, m); (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)% ⊦ ¬ n < n; (s)% ⊦ m < 1 ↔ m = 0; (s)%# buf = n ⊦ subarray(buf, 0, n) = buf; (s)