diff --git a/dev/bend2/buffer_refcount/LAWS.bend b/dev/bend2/buffer_refcount/LAWS.bend new file mode 100644 index 0000000000..fe86a2f04d --- /dev/null +++ b/dev/bend2/buffer_refcount/LAWS.bend @@ -0,0 +1,388 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. + +# The laws of the buffer reference-counting model. The human states +# them; PROOF.bend must prove them. Each law quotes the Javadoc or +# Preconditions message in arrow-java's memory-core it comes from, or is +# a sanity check that keeps the others from being satisfied vacuously. +# +# Laws are stated over arbitrary allocator states, so the ones that need +# it take the invariant Inv as a hypothesis; inv_start and inv_kept show +# every reachable state satisfies Inv. + +import Base +import ./main.bend as M + +# the truth of a Bool as a type: Unit when True, Empty when False +def T(b: Bool) -> Data: + match b: + case True{}: + Unit + case False{}: + Empty + +# a conjunction of two copyable facts (A & B is Type-kinded, so a proof +# of it could be used only once) +type And<-A: Data, -B: Data> is Data: + Conj{l: A, r: B} + +# Invariant +# --------- + +# an allocation's freed flag agrees with its reference count: +# "If the reference count drops to 0, it implies that ArrowBufs managed +# by this reference manager no longer need access to the underlying +# memory" (ReferenceManager.release), and the chunk is released exactly +# then (AllocationManager.release: release0()) +def AllocOk(a: M.Alloc) -> Data: + M.Alloc{id, size, refs, freed} = a + {freed == Nat.is_eq(refs, 0n) : Bool} + +def Consistent(xs: List<&2, M.Alloc>) -> Data: + match xs: + case Nil{}: + Unit + case Con{a, t}: + And + +# the accountant's counter is the sum of the live allocations' sizes +# (BaseAllocator.verifyAllocator: "bufferTotal + reservedTotal + childTotal +# != getAllocatedMemory()" is the failure it looks for), and every +# allocation is consistent +def Inv(allocs: List<&2, M.Alloc>, allocated: Nat) -> Data: + And<{allocated == M.live_bytes(allocs) : Nat}, Consistent(allocs)> + +def Inv_s(s: M.Allocator) -> Data: + M.Allocator{allocs, allocated, limit, next, closed} = s + Inv(allocs, allocated) + +# LAW (accounting, start): a fresh RootAllocator accounts for nothing +law inv_start: + for limit : Nat + Inv_s(M.start(limit)) + +# LAW (accounting, step): every request keeps the allocated-bytes counter +# equal to the live bytes and every freed flag equal to "refcount is 0". +# This is law 3 (the counter) and law 2 (freed exactly at zero) of the +# spec, as one inductive invariant. +law inv_kept: + for r : M.Req + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + for closed : Bool + for w : Inv(allocs, allocated) + Inv_s(M.state(M.step(r, allocs, allocated, limit, next, closed))) + +# Release +# ------- + +# LAW: "ref count decrement should be greater than or equal to 1" +# (BufferLedger.release: Preconditions.checkState). release(0) is an +# error and changes nothing. +law release_zero_is_error: + for +id : Nat + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + {M.step(M.RRelease{id, 0n}, allocs, allocated, limit, next, False{}) == (M.Allocator{allocs, allocated, limit, next, False{}}, M.RErr{}) : M.Allocator & M.Resp} + +# LAW: "RefCnt has gone negative" (BufferLedger.release: +# Preconditions.checkState(refCnt >= 0)). Releasing more references than +# are held is an error and leaves the state unchanged; an unknown id +# holds 0 references, so this covers it too. +law release_below_zero_is_error: + for +id : Nat + for +n : Nat + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + for lt : T(Nat.is_lt(M.refs_of(id, allocs), n)) + {M.step(M.RRelease{id, n}, allocs, allocated, limit, next, False{}) == (M.Allocator{allocs, allocated, limit, next, False{}}, M.RErr{}) : M.Allocator & M.Resp} + +# LAW: a release on a buffer whose memory is already released, or on an +# unknown buffer, is an error and not a silent no-op: memory is never +# freed twice. Needs the invariant (freed means the count is 0). +law release_dead_is_error: + for +id : Nat + for +n : Nat + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + for w : Inv(allocs, allocated) + for d : T(Bool.not(M.is_live(id, allocs))) + {M.step(M.RRelease{id, n}, allocs, allocated, limit, next, False{}) == (M.Allocator{allocs, allocated, limit, next, False{}}, M.RErr{}) : M.Allocator & M.Resp} + +# LAW: "@return true if ref count has dropped to 0" (ReferenceManager.release), +# and then "oldAllocator.releaseBytes(getSize()); release0()" +# (AllocationManager.release). Releasing exactly the references held +# answers true, marks the memory freed and takes its size off the counter. +law release_to_zero_frees: + for +id : Nat + for +m : Nat + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + for e : {M.refs_of(id, allocs) == 1n+m : Nat} + after = M.state(M.step(M.RRelease{id, 1n+m}, allocs, allocated, limit, next, False{})) + {M.resp(M.step(M.RRelease{id, 1n+m}, allocs, allocated, limit, next, False{})) == M.RFreed{} : M.Resp} + & T(M.is_freed(id, M.allocs_of(after))) + & {M.allocated_of(after) == Nat.sub(allocated, M.size_of(id, allocs)) : Nat} + +# LAW: "@return ... false otherwise" (ReferenceManager.release). Releasing +# fewer references than are held answers false, keeps the buffer live, +# lowers its count by exactly n and leaves the accountant alone. Needs +# the invariant: a positive count means the memory is held. +law release_keeps_live: + for +id : Nat + for +m : Nat + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + for w : Inv(allocs, allocated) + for lt : T(Nat.is_lt(1n+m, M.refs_of(id, allocs))) + after = M.state(M.step(M.RRelease{id, 1n+m}, allocs, allocated, limit, next, False{})) + {M.resp(M.step(M.RRelease{id, 1n+m}, allocs, allocated, limit, next, False{})) == M.ROk{} : M.Resp} + & T(M.is_live(id, M.allocs_of(after))) + & {M.refs_of(id, M.allocs_of(after)) == Nat.sub(M.refs_of(id, allocs), 1n+m) : Nat} + & {M.allocated_of(after) == allocated : Nat} + +# Retain +# ------ + +# LAW: "retain(%s) argument is not positive" (BufferLedger.retain: +# Preconditions.checkArgument(increment > 0)). retain(0) is an error and +# changes nothing. +law retain_zero_is_error: + for +id : Nat + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + {M.step(M.RRetain{id, 0n}, allocs, allocated, limit, next, False{}) == (M.Allocator{allocs, allocated, limit, next, False{}}, M.RErr{}) : M.Allocator & M.Resp} + +# LAW: "Preconditions.checkArgument(originalReferenceCount > 0)" +# (BufferLedger.retain). A retain on a buffer whose memory is released, +# or on an unknown buffer, is an error and does not revive it. +law retain_dead_is_error: + for +id : Nat + for +n : Nat + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + for w : Inv(allocs, allocated) + for d : T(Bool.not(M.is_live(id, allocs))) + {M.step(M.RRetain{id, n}, allocs, allocated, limit, next, False{}) == (M.Allocator{allocs, allocated, limit, next, False{}}, M.RErr{}) : M.Allocator & M.Resp} + +# LAW: "Increment this reference manager's reference count by a given +# amount for the associated underlying memory" (ReferenceManager.retain). +# On a live buffer, retain(n) adds exactly n, keeps the buffer live and +# does not touch the accountant. +law retain_live_adds: + for +id : Nat + for +m : Nat + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + for w : Inv(allocs, allocated) + for l : T(M.is_live(id, allocs)) + after = M.state(M.step(M.RRetain{id, 1n+m}, allocs, allocated, limit, next, False{})) + {M.resp(M.step(M.RRetain{id, 1n+m}, allocs, allocated, limit, next, False{})) == M.ROk{} : M.Resp} + & T(M.is_live(id, M.allocs_of(after))) + & {M.refs_of(id, M.allocs_of(after)) == Nat.add(M.refs_of(id, allocs), 1n+m) : Nat} + & {M.allocated_of(after) == allocated : Nat} + +# Allocation +# ---------- + +# LAW: "Unable to allocate buffer of size %d due to memory limit" +# (BaseAllocator.buffer throws OutOfMemoryException when +# Accountant.allocate finds newLocal > allocationLimit). "Either +# completely succeeds or completely fails. If it fails, no changes are +# made to accounting." (Accountant.allocateBytes) +law alloc_over_limit_rejected: + for +p : Nat + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + for over : T(Nat.is_lt(limit, Nat.add(allocated, 1n+p))) + {M.step(M.RAlloc{1n+p}, allocs, allocated, limit, next, False{}) == (M.Allocator{allocs, allocated, limit, next, False{}}, M.ROom{}) : M.Allocator & M.Resp} + +# LAW (anti-vacuity): a request that fits is served: a new buffer with +# "a ref count of 1" (BufferLedger.retain Javadoc; associate(this) in +# bufferWithoutReservation), and the counter grows by its size. +law alloc_within_limit_served: + for +p : Nat + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + for fits : T(Nat.is_le(Nat.add(allocated, 1n+p), limit)) + after = M.state(M.step(M.RAlloc{1n+p}, allocs, allocated, limit, next, False{})) + {M.resp(M.step(M.RAlloc{1n+p}, allocs, allocated, limit, next, False{})) == M.RBuf{next} : M.Resp} + & {M.refs_of(next, M.allocs_of(after)) == 1n : Nat} + & {M.allocated_of(after) == Nat.add(allocated, 1n+p) : Nat} + +# LAW: "if (initialRequestSize == 0) return getEmpty();" (BaseAllocator.buffer). +# buffer(0) is the shared empty buffer and accounts nothing. +law alloc_zero_is_empty: + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + {M.step(M.RAlloc{0n}, allocs, allocated, limit, next, False{}) == (M.Allocator{allocs, allocated, limit, next, False{}}, M.REmpty{}) : M.Allocator & M.Resp} + +# Close +# ----- + +# LAW: "Allocator[%s] closed with outstanding buffers allocated" / +# "Memory was leaked by query" (BaseAllocator.close). Closing while any +# buffer is live is an error. +law close_with_live_buffer_is_error: + for +id : Nat + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + for l : T(M.is_live(id, allocs)) + {M.resp(M.step(M.RClose{}, allocs, allocated, limit, next, False{})) == M.RErr{} : M.Resp} + +# LAW: with no outstanding buffer, close succeeds and the allocator is closed. +law close_clean_succeeds: + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + for c : {False{} == M.has_live(allocs) : Bool} + {M.step(M.RClose{}, allocs, allocated, limit, next, False{}) == (M.Allocator{allocs, allocated, limit, next, True{}}, M.ROk{}) : M.Allocator & M.Resp} + +# LAW: the two leak checks agree. BaseAllocator.close tests +# getAllocatedMemory() > 0 always and the outstanding-ledger count in +# DEBUG mode; under the invariant, no live buffer means no accounted bytes. +law clean_means_zero_bytes: + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for w : Inv(allocs, allocated) + for c : {False{} == M.has_live(allocs) : Bool} + {allocated == 0n : Nat} + +# LAW: "Attempting operation on allocator when allocator is closed" +# (BaseAllocator.assertOpen). After close, buffer(), retain() and +# release() fail and change nothing. +law closed_rejects: + for r : M.Req + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + for nc : {False{} == M.is_close(r) : Bool} + {M.step(r, allocs, allocated, limit, next, True{}) == (M.Allocator{allocs, allocated, limit, next, True{}}, M.RErr{}) : M.Allocator & M.Resp} + +# LAW: "Some owners may close more than once" (BaseAllocator.close). +# A second close is a no-op. +law close_twice_is_noop: + for +allocs : List<&2, M.Alloc> + for +allocated : Nat + for +limit : Nat + for +next : Nat + {M.step(M.RClose{}, allocs, allocated, limit, next, True{}) == (M.Allocator{allocs, allocated, limit, next, True{}}, M.ROk{}) : M.Allocator & M.Resp} + +# Traces (anti-vacuity) +# --------------------- + +# LAW: buffer(size); release() frees the memory and the allocator closes cleanly +# (TestBaseAllocator.testRootAllocator_createChildAndUse). +law trace_alloc_release_frees: + for +p : Nat + for +limit : Nat + for fits : T(Nat.is_le(1n+p, limit)) + run = M.replay([M.RAlloc{1n+p}, M.RRelease{0n, 1n}, M.RClose{}], limit) + {M.resp(run) == M.ROk{} : M.Resp} & {M.allocated_of(M.state(run)) == 0n : Nat} + +# LAW: buffer(size); retain(); release() keeps the buffer live with one +# reference, and close then reports the leak +# (TestBaseAllocator.testRootAllocator_closeWithOutstanding). +law trace_retain_keeps_live: + for +p : Nat + for +limit : Nat + for fits : T(Nat.is_le(1n+p, limit)) + run = M.replay([M.RAlloc{1n+p}, M.RRetain{0n, 1n}, M.RRelease{0n, 1n}, M.RClose{}], limit) + {M.resp(run) == M.RErr{} : M.Resp} + & {M.refs_of(0n, M.allocs_of(M.state(run))) == 1n : Nat} + & {M.allocated_of(M.state(run)) == 1n+p : Nat} + +# LAW: buffer(size); release(); release() is an error: memory is never freed twice. +law trace_double_release_is_error: + for +p : Nat + for +limit : Nat + for fits : T(Nat.is_le(1n+p, limit)) + {M.resp(M.replay([M.RAlloc{1n+p}, M.RRelease{0n, 1n}, M.RRelease{0n, 1n}], limit)) == M.RErr{} : M.Resp} + +# Not modelled +# ------------ + +# NOT PROVEN: ownership transfer between two allocators. +# "Transfer the memory accounting ownership of this ArrowBuf to another +# allocator ... Transfers will always succeed, even if that puts the +# other allocator into an overlimit situation." (BufferLedger.transferOwnership) +# The law would be: the sum of allocated bytes over both allocators is +# unchanged by a transfer. This model has one allocator and one ledger +# per allocation; a faithful transfer needs the AllocationManager's map +# from allocators to ledgers, an owning ledger per chunk, and +# forceAllocate/releaseBytes on two accountants. That is a second model, +# not a hypothesis on this one, so it is left as follow-up work. +# +# law transfer_preserves_total: +# for src : M.Allocator +# for dst : M.Allocator +# for +id : Nat +# {total(transfer(id, src, dst)) == Nat.add(allocated_of(src), allocated_of(dst)) : Nat} + +# NOT EXPRESSIBLE: thread safety of the reference count. +# "Operations within the context of a single BufferLedger are lockless in +# nature and can be leveraged by multiple threads." (AllocationManager) +# BufferLedger uses AtomicIntegerFieldUpdater and synchronized +# (allocationManager). Bend is pure and its model of a step is a +# function, so there is no interleaving to quantify over; stating +# linearizability would need an explicit scheduler model, which is not +# what LAWS.bend checks. +# +# law release_is_atomic: ... + +# NOT EXPRESSIBLE: 64-bit overflow of the accountant. +# Accountant.allocate detects "overflow = ((oldLocal ^ newLocal) & (size ^ +# newLocal)) < 0" on a long. Bend has Nat, U32 and F32 only; sizes here +# are unbounded Nat, so the overflow branch has no model. +# +# law alloc_overflow_rejected: ... + +# NOT MODELLED: bounds checking of reads and writes. +# "Will throw an exception if the memory is not readable" (ArrowBuf.checkBytes). +# Index arithmetic against capacity is expressible in Bend, but this model +# has no reader/writer indexes or capacity per ArrowBuf (slices), only the +# chunk size; the check belongs to a model of ArrowBuf views. +# +# law read_within_capacity: ... diff --git a/dev/bend2/buffer_refcount/PROOF.bend b/dev/bend2/buffer_refcount/PROOF.bend new file mode 100644 index 0000000000..2e33f6cf19 --- /dev/null +++ b/dev/bend2/buffer_refcount/PROOF.bend @@ -0,0 +1,1001 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. + +# The proofs. Imports the model (as M) and the claims (as Laws) and +# fills every law they state; `bend PROOF.bend` is the whole check. +# +# Conventions. A rewrite `%e : P` with `e : {a == b : T}` turns a goal +# matching P[b] into P[a], so equations are oriented "new == old". A +# computed value cannot be matched, so each case split on one goes +# through a `.fin` helper that takes the value as a parameter together +# with an equation tying it to the computation (the "inspect" idiom). + +import Base +import ./main.bend as M +import ./LAWS.bend as Laws + +# Proof kit +# --------- + +def disc(b: Bool) -> Type: + match b: + case True{}: + Unit + case False{}: + Empty + +# True and False clash +def true_ne_false(e: {True{} == False{} : Bool}) -> Empty: + %e : disc(_) + Unit{} + +def false_ne_true(e: {False{} == True{} : Bool}) -> Empty: + true_ne_false(Equal.sym(Bool, False{}, True{}, e)) + +def zero_ne_succ.motive(n: Nat) -> Type: + match n: + case 0n: + Unit + case 1n+p: + Empty + +# 0 and a successor clash +def zero_ne_succ(-p: Nat, e: {0n == 1n+p : Nat}) -> Empty: + %e : zero_ne_succ.motive(_) + Unit{} + +# T(True{}) from an equation, and back +def true_T(b: Bool, e: {True{} == b : Bool}) -> Laws.T(b): + %e : Laws.T(_) + Unit{} + +def T_true(b: Bool, w: Laws.T(b)) -> {True{} == b : Bool}: + match b: + case True{}: + {==} + case False{}: + Empty.absurd({True{} == False{} : Bool}, w) + +# T(b) refutes b == False +def T_not_false(b: Bool, w: Laws.T(b), e: {b == False{} : Bool}) -> Empty: + match b: + case True{}: + true_ne_false(e) + case False{}: + w + +# Lemmas on Nat +# ------------- + +def add_zero(+a: Nat) -> {a == Nat.add(a, 0n) : Nat}: + match a: + case 0n: + {==} + case 1n+p: + %add_zero(p) : {1n+p == 1n+_ : Nat} + {==} + +def add_succ(+a: Nat, +b: Nat) -> {1n+Nat.add(a, b) == Nat.add(a, 1n+b) : Nat}: + match a: + case 0n: + {==} + case 1n+p: + %add_succ(p, b) : {2n+Nat.add(p, b) == 1n+_ : Nat} + {==} + +def add_comm(+a: Nat, +b: Nat) -> {Nat.add(a, b) == Nat.add(b, a) : Nat}: + match a: + case 0n: + add_zero(b) + case 1n+p: + %add_succ(b, p) : {1n+Nat.add(p, b) == _ : Nat} + %Equal.sym(Nat, Nat.add(p, b), Nat.add(b, p), add_comm(p, b)) : {1n+_ == 1n+Nat.add(b, p) : Nat} + {==} + +# a + (b + c) == (a + b) + c +def add_assoc(+a: Nat, +b: Nat, +c: Nat) -> {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}: + match a: + case 0n: + {==} + case 1n+p: + %add_assoc(p, b, c) : {1n+Nat.add(p, Nat.add(b, c)) == 1n+_ : Nat} + {==} + +def sub_zero(+a: Nat) -> {a == Nat.sub(a, 0n) : Nat}: + match a: + case 0n: + {==} + case 1n+p: + {==} + +# (a + b) - b == a +def sub_add_cancel(+a: Nat, +b: Nat) -> {a == Nat.sub(Nat.add(a, b), b) : Nat}: + match b: + case 0n: + %add_zero(a) : {a == Nat.sub(_, 0n) : Nat} + sub_zero(a) + case 1n+q: + %add_succ(a, q) : {a == Nat.sub(_, 1n+q) : Nat} + sub_add_cancel(a, q) + +def sub_self(+a: Nat) -> {0n == Nat.sub(a, a) : Nat}: + match a: + case 0n: + {==} + case 1n+p: + sub_self(p) + +def pred(n: Nat) -> Nat: + match n: + case 0n: + 0n + case 1n+p: + p + +def succ_inj(+a: Nat, +b: Nat, e: {1n+a == 1n+b : Nat}) -> {a == b : Nat}: + Equal.cong(Nat, Nat, pred, 1n+a, 1n+b, e) + +def add_succ_both(+a: Nat, +b: Nat, +q: Nat, e: {Nat.add(a, 1n+q) == Nat.add(b, 1n+q) : Nat}) -> {1n+Nat.add(a, q) == 1n+Nat.add(b, q) : Nat}: + %Equal.sym(Nat, 1n+Nat.add(a, q), Nat.add(a, 1n+q), add_succ(a, q)) : {_ == 1n+Nat.add(b, q) : Nat} + %Equal.sym(Nat, 1n+Nat.add(b, q), Nat.add(b, 1n+q), add_succ(b, q)) : {Nat.add(a, 1n+q) == _ : Nat} + e + +# a + c == b + c implies a == b +def add_cancel_r(+a: Nat, +b: Nat, +c: Nat, e: {Nat.add(a, c) == Nat.add(b, c) : Nat}) -> {a == b : Nat}: + match c: + case 0n: + %Equal.sym(Nat, a, Nat.add(a, 0n), add_zero(a)) : {_ == b : Nat} + %Equal.sym(Nat, b, Nat.add(b, 0n), add_zero(b)) : {Nat.add(a, 0n) == _ : Nat} + e + case 1n+q: + add_cancel_r(a, b, q, succ_inj(Nat.add(a, q), Nat.add(b, q), add_succ_both(a, b, q, e))) + +def eq_refl(+n: Nat) -> {True{} == Nat.is_eq(n, n) : Bool}: + match n: + case 0n: + {==} + case 1n+p: + eq_refl(p) + +def lt_irrefl(+n: Nat) -> {False{} == Nat.is_lt(n, n) : Bool}: + match n: + case 0n: + {==} + case 1n+p: + lt_irrefl(p) + +# a < b implies not b <= a +def lt_not_le(+a: Nat, +b: Nat, w: Laws.T(Nat.is_lt(a, b))) -> {False{} == Nat.is_le(b, a) : Bool}: + match a b: + case 0n 0n: + Empty.absurd({False{} == Nat.is_le(0n, 0n) : Bool}, w) + case 0n 1n+q: + {==} + case 1n+p 0n: + Empty.absurd({False{} == Nat.is_le(0n, 1n+p) : Bool}, w) + case 1n+p 1n+q: + lt_not_le(p, q, w) + +# a < b implies not b < a +def lt_asym(+a: Nat, +b: Nat, w: Laws.T(Nat.is_lt(a, b))) -> {False{} == Nat.is_lt(b, a) : Bool}: + match a b: + case 0n 0n: + Empty.absurd({False{} == Nat.is_lt(0n, 0n) : Bool}, w) + case 0n 1n+q: + {==} + case 1n+p 0n: + Empty.absurd({False{} == Nat.is_lt(0n, 1n+p) : Bool}, w) + case 1n+p 1n+q: + lt_asym(p, q, w) + +# a < b implies b - a is positive: b - a == 1 + (b - (1 + a)) +def lt_sub_succ(+a: Nat, +b: Nat, w: Laws.T(Nat.is_lt(a, b))) -> {1n+Nat.sub(b, 1n+a) == Nat.sub(b, a) : Nat}: + match a b: + case 0n 0n: + Empty.absurd({1n+Nat.sub(0n, 1n) == Nat.sub(0n, 0n) : Nat}, w) + case 0n 1n+q: + %sub_zero(q) : {1n+_ == 1n+q : Nat} + {==} + case 1n+p 0n: + Empty.absurd({1n+Nat.sub(0n, 2n+p) == Nat.sub(0n, 1n+p) : Nat}, w) + case 1n+p 1n+q: + lt_sub_succ(p, q, w) + +# a - b == 1 + q implies a is positive, so is_eq(a, 0) is False +def sub_pos_pos(+a: Nat, +b: Nat, -q: Nat, e: {1n+q == Nat.sub(a, b) : Nat}) -> {Nat.is_eq(a, 0n) == False{} : Bool}: + match a b: + case 0n 0n: + Empty.absurd({Nat.is_eq(0n, 0n) == False{} : Bool}, zero_ne_succ(q, Equal.sym(Nat, 1n+q, 0n, e))) + case 0n 1n+bp: + Empty.absurd({Nat.is_eq(0n, 0n) == False{} : Bool}, zero_ne_succ(q, Equal.sym(Nat, 1n+q, 0n, e))) + case 1n+ap 0n: + {==} + case 1n+ap 1n+bp: + {==} + +# a true Nat.is_eq(refs, 0n) means refs is 0 +def refs_zero(+refs: Nat, e: {True{} == Nat.is_eq(refs, 0n) : Bool}) -> {0n == refs : Nat}: + match refs: + case 0n: + {==} + case 1n+r: + Empty.absurd({0n == 1n+r : Nat}, true_ne_false(e)) + +# not refs < n with n >= 1 means refs is positive +def ge_succ_pos(+refs: Nat, -m: Nat, e: {False{} == Nat.is_lt(refs, 1n+m) : Bool}) -> {Nat.is_eq(refs, 0n) == False{} : Bool}: + match refs: + case 0n: + Empty.absurd({Nat.is_eq(0n, 0n) == False{} : Bool}, false_ne_true(e)) + case 1n+r: + {==} + +# n < refs means refs is positive +def lt_pos(-m: Nat, +refs: Nat, w: Laws.T(Nat.is_lt(1n+m, refs))) -> {Nat.is_eq(refs, 0n) == False{} : Bool}: + match refs: + case 0n: + Empty.absurd({Nat.is_eq(0n, 0n) == False{} : Bool}, w) + case 1n+r: + {==} + +# transport along an equation +def cast(-A: Type, -P: A -> Type, -a: A, -b: A, e: {a == b : A}, w: P(a)) -> P(b): + %e : P(_) + w + +# Lemmas on the allocation list +# ----------------------------- + +# the consistency of a lookup result +def AllocOkM(m: Maybe<&2, M.Alloc>) -> Data: + match m: + case None{}: + Unit + case Some{a}: + Laws.AllocOk(a) + +# a lookup in a consistent list finds a consistent allocation: the step +# case, over the verdict c of Nat.is_eq(aid, id) +def lookup_ok.fin(+id: Nat, +aid: Nat, +size: Nat, +refs: Nat, +freed: Bool, -t: List<&2, M.Alloc>, + w: Laws.Consistent(M.Alloc{aid, size, refs, freed} <> t), + rec: Laws.Consistent(t) -> AllocOkM(M.lookup(id, t)), c: Bool) + -> AllocOkM(M.lookup.at(M.Alloc{aid, size, refs, freed}, M.lookup(id, t), c)): + Laws.Conj{ok, wt} = w + match c: + case True{}: + ok + case False{}: + rec(wt) + +def lookup_ok(+id: Nat, xs: List<&2, M.Alloc>) -> Laws.Consistent(xs) -> AllocOkM(M.lookup(id, xs)): + match xs: + case Nil{}: + w => Unit{} + case Con{M.Alloc{+aid, +size, +refs, +freed}, +t}: + w => lookup_ok.fin(id, aid, size, refs, freed, t, w, lookup_ok(id, t), Nat.is_eq(aid, id)) + +# replacing an allocation by a consistent one keeps the list consistent +def replace_ok.fin(+id: Nat, +a2: M.Alloc, +aid: Nat, +size: Nat, +refs: Nat, +freed: Bool, +t: List<&2, M.Alloc>, + w: Laws.Consistent(M.Alloc{aid, size, refs, freed} <> t), w2: Laws.AllocOk(a2), + rec: Laws.Consistent(t) -> Laws.AllocOk(a2) -> Laws.Consistent(M.replace(id, a2, t)), c: Bool) + -> Laws.Consistent(M.replace.at(M.Alloc{aid, size, refs, freed}, a2, t, M.replace(id, a2, t), c)): + Laws.Conj{ok, wt} = w + match c: + case True{}: + Laws.Conj{w2, wt} + case False{}: + Laws.Conj{ok, rec(wt, w2)} + +def replace_ok(+id: Nat, +a2: M.Alloc, xs: List<&2, M.Alloc>) -> Laws.Consistent(xs) -> Laws.AllocOk(a2) -> Laws.Consistent(M.replace(id, a2, xs)): + match xs: + case Nil{}: + w => w2 => Unit{} + case Con{M.Alloc{+aid, +size, +refs, +freed}, +t}: + w => w2 => replace_ok.fin(id, a2, aid, size, refs, freed, t, w, w2, replace_ok(id, a2, t), Nat.is_eq(aid, id)) + +# the bytes of a lookup result, and the bytes of its replacement +def mbytes(m: Maybe<&2, M.Alloc>) -> Nat: + match m: + case None{}: + 0n + case Some{a}: + M.bytes(a) + +def pick(m: Maybe<&2, M.Alloc>, a2: M.Alloc) -> Nat: + match m: + case None{}: + 0n + case Some{a}: + M.bytes(a2) + +# (x + y) + z == (z + y) + x +def add_rot(+x: Nat, +y: Nat, +z: Nat) -> {Nat.add(Nat.add(x, y), z) == Nat.add(Nat.add(z, y), x) : Nat}: + %add_assoc(x, y, z) : {_ == Nat.add(Nat.add(z, y), x) : Nat} + %add_comm(x, Nat.add(z, y)) : {Nat.add(x, Nat.add(y, z)) == _ : Nat} + %add_comm(y, z) : {Nat.add(x, Nat.add(y, z)) == Nat.add(x, _) : Nat} + {==} + +# replacing the found allocation moves its bytes out and a2's bytes in: +# live_bytes(xs) + bytes(a2) == live_bytes(replace(id, a2, xs)) + bytes(found) +def replace_bytes.fin(+id: Nat, +a2: M.Alloc, +aid: Nat, +size: Nat, +refs: Nat, +freed: Bool, +t: List<&2, M.Alloc>, + rec: {Nat.add(M.live_bytes(t), pick(M.lookup(id, t), a2)) == Nat.add(M.live_bytes(M.replace(id, a2, t)), mbytes(M.lookup(id, t))) : Nat}, + c: Bool, e: {c == Nat.is_eq(aid, id) : Bool}) + -> {Nat.add(M.live_bytes(M.Alloc{aid, size, refs, freed} <> t), pick(M.lookup.at(M.Alloc{aid, size, refs, freed}, M.lookup(id, t), Nat.is_eq(aid, id)), a2)) + == Nat.add(M.live_bytes(M.replace.at(M.Alloc{aid, size, refs, freed}, a2, t, M.replace(id, a2, t), Nat.is_eq(aid, id))), mbytes(M.lookup.at(M.Alloc{aid, size, refs, freed}, M.lookup(id, t), Nat.is_eq(aid, id)))) : Nat}: + match c: + case True{}: + %e : {Nat.add(M.live_bytes(M.Alloc{aid, size, refs, freed} <> t), pick(M.lookup.at(M.Alloc{aid, size, refs, freed}, M.lookup(id, t), _), a2)) + == Nat.add(M.live_bytes(M.replace.at(M.Alloc{aid, size, refs, freed}, a2, t, M.replace(id, a2, t), _)), mbytes(M.lookup.at(M.Alloc{aid, size, refs, freed}, M.lookup(id, t), _))) : Nat} + add_rot(M.bytes.of(freed, size), M.live_bytes(t), M.bytes(a2)) + case False{}: + %e : {Nat.add(M.live_bytes(M.Alloc{aid, size, refs, freed} <> t), pick(M.lookup.at(M.Alloc{aid, size, refs, freed}, M.lookup(id, t), _), a2)) + == Nat.add(M.live_bytes(M.replace.at(M.Alloc{aid, size, refs, freed}, a2, t, M.replace(id, a2, t), _)), mbytes(M.lookup.at(M.Alloc{aid, size, refs, freed}, M.lookup(id, t), _))) : Nat} + %add_assoc(M.bytes.of(freed, size), M.live_bytes(t), pick(M.lookup(id, t), a2)) : {_ == Nat.add(Nat.add(M.bytes.of(freed, size), M.live_bytes(M.replace(id, a2, t))), mbytes(M.lookup(id, t))) : Nat} + %add_assoc(M.bytes.of(freed, size), M.live_bytes(M.replace(id, a2, t)), mbytes(M.lookup(id, t))) : {Nat.add(M.bytes.of(freed, size), Nat.add(M.live_bytes(t), pick(M.lookup(id, t), a2))) == _ : Nat} + %rec : {Nat.add(M.bytes.of(freed, size), Nat.add(M.live_bytes(t), pick(M.lookup(id, t), a2))) == Nat.add(M.bytes.of(freed, size), _) : Nat} + {==} + +def replace_bytes(+id: Nat, +a2: M.Alloc, xs: List<&2, M.Alloc>) + -> {Nat.add(M.live_bytes(xs), pick(M.lookup(id, xs), a2)) == Nat.add(M.live_bytes(M.replace(id, a2, xs)), mbytes(M.lookup(id, xs))) : Nat}: + match xs: + case Nil{}: + {==} + case Con{M.Alloc{+aid, +size, +refs, +freed}, +t}: + replace_bytes.fin(id, a2, aid, size, refs, freed, t, replace_bytes(id, a2, t), Nat.is_eq(aid, id), {==}) + +# the same, with the lookup result named +def replace_bytes_at(+id: Nat, +a2: M.Alloc, +xs: List<&2, M.Alloc>, -m0: Maybe<&2, M.Alloc>, e: {M.lookup(id, xs) == m0 : Maybe<&2, M.Alloc>}) + -> {Nat.add(M.live_bytes(xs), pick(m0, a2)) == Nat.add(M.live_bytes(M.replace(id, a2, xs)), mbytes(m0)) : Nat}: + %e : {Nat.add(M.live_bytes(xs), pick(_, a2)) == Nat.add(M.live_bytes(M.replace(id, a2, xs)), mbytes(_)) : Nat} + replace_bytes(id, a2, xs) + +def none_ne_some.motive(m: Maybe<&2, M.Alloc>) -> Type: + match m: + case None{}: + Unit + case Some{a}: + Empty + +def none_ne_some(-a: M.Alloc, e: {None{} == Some{a} : Maybe<&2, M.Alloc>}) -> Empty: + %e : none_ne_some.motive(_) + Unit{} + +# after replacing the found allocation by one with the same id, the lookup finds the new one +def lookup_replace.fin(+id: Nat, +size: Nat, +refs: Nat, +freed: Bool, -a: M.Alloc, +aid: Nat, +asize: Nat, +arefs: Nat, +afreed: Bool, +t: List<&2, M.Alloc>, + rec: {M.lookup(id, t) == Some{a} : Maybe<&2, M.Alloc>} -> {M.lookup(id, M.replace(id, M.Alloc{id, size, refs, freed}, t)) == Some{M.Alloc{id, size, refs, freed}} : Maybe<&2, M.Alloc>}, + c: Bool, +e: {c == Nat.is_eq(aid, id) : Bool}, + el: {M.lookup.at(M.Alloc{aid, asize, arefs, afreed}, M.lookup(id, t), c) == Some{a} : Maybe<&2, M.Alloc>}) + -> {M.lookup(id, M.replace.at(M.Alloc{aid, asize, arefs, afreed}, M.Alloc{id, size, refs, freed}, t, M.replace(id, M.Alloc{id, size, refs, freed}, t), Nat.is_eq(aid, id))) == Some{M.Alloc{id, size, refs, freed}} : Maybe<&2, M.Alloc>}: + match c: + case True{}: + %e : {M.lookup(id, M.replace.at(M.Alloc{aid, asize, arefs, afreed}, M.Alloc{id, size, refs, freed}, t, M.replace(id, M.Alloc{id, size, refs, freed}, t), _)) == Some{M.Alloc{id, size, refs, freed}} : Maybe<&2, M.Alloc>} + %eq_refl(id) : {M.lookup.at(M.Alloc{id, size, refs, freed}, M.lookup(id, t), _) == Some{M.Alloc{id, size, refs, freed}} : Maybe<&2, M.Alloc>} + {==} + case False{}: + %e : {M.lookup(id, M.replace.at(M.Alloc{aid, asize, arefs, afreed}, M.Alloc{id, size, refs, freed}, t, M.replace(id, M.Alloc{id, size, refs, freed}, t), _)) == Some{M.Alloc{id, size, refs, freed}} : Maybe<&2, M.Alloc>} + %e : {M.lookup.at(M.Alloc{aid, asize, arefs, afreed}, M.lookup(id, M.replace(id, M.Alloc{id, size, refs, freed}, t)), _) == Some{M.Alloc{id, size, refs, freed}} : Maybe<&2, M.Alloc>} + rec(el) + +def lookup_replace(+id: Nat, +size: Nat, +refs: Nat, +freed: Bool, -a: M.Alloc, xs: List<&2, M.Alloc>) + -> {M.lookup(id, xs) == Some{a} : Maybe<&2, M.Alloc>} -> {M.lookup(id, M.replace(id, M.Alloc{id, size, refs, freed}, xs)) == Some{M.Alloc{id, size, refs, freed}} : Maybe<&2, M.Alloc>}: + match xs: + case Nil{}: + el => Empty.absurd({M.lookup(id, Nil{}) == Some{M.Alloc{id, size, refs, freed}} : Maybe<&2, M.Alloc>}, none_ne_some(a, el)) + case Con{M.Alloc{+aid, +asize, +arefs, +afreed}, +t}: + el => lookup_replace.fin(id, size, refs, freed, a, aid, asize, arefs, afreed, t, lookup_replace(id, size, refs, freed, a, t), Nat.is_eq(aid, id), {==}, el) + +# a live allocation means there is an outstanding buffer +def live_has_live.fin(c: Bool, +id: Nat, +aid: Nat, +size: Nat, +refs: Nat, +freed: Bool, +t: List<&2, M.Alloc>, + rec: Laws.T(M.is_live(id, t)) -> {True{} == M.has_live(t) : Bool}, + l: Laws.T(M.is_live.m(M.lookup.at(M.Alloc{aid, size, refs, freed}, M.lookup(id, t), c)))) + -> {True{} == M.has_live(M.Alloc{aid, size, refs, freed} <> t) : Bool}: + match c: + case True{}: + match freed: + case True{}: + match l: + case False{}: + {==} + case False{}: + match freed: + case True{}: + rec(l) + case False{}: + {==} + +def live_has_live(+id: Nat, xs: List<&2, M.Alloc>) -> Laws.T(M.is_live(id, xs)) -> {True{} == M.has_live(xs) : Bool}: + match xs: + case Nil{}: + l => Empty.absurd({True{} == M.has_live(Nil{}) : Bool}, l) + case Con{M.Alloc{+aid, +size, +refs, +freed}, +t}: + l => live_has_live.fin(Nat.is_eq(aid, id), id, aid, size, refs, freed, t, live_has_live(id, t), l) + +# no outstanding buffer means no accounted bytes +def no_live_no_bytes.fin(+size: Nat, +freed: Bool, +t: List<&2, M.Alloc>, + c: {False{} == (Bool.not(freed) || M.has_live(t)) : Bool}, + rec: {False{} == M.has_live(t) : Bool} -> {M.live_bytes(t) == 0n : Nat}) + -> {Nat.add(M.bytes.of(freed, size), M.live_bytes(t)) == 0n : Nat}: + match freed: + case True{}: + rec(c) + case False{}: + Empty.absurd({Nat.add(size, M.live_bytes(t)) == 0n : Nat}, false_ne_true(c)) + +def no_live_no_bytes(xs: List<&2, M.Alloc>) -> {False{} == M.has_live(xs) : Bool} -> {M.live_bytes(xs) == 0n : Nat}: + match xs: + case Nil{}: + c => {==} + case Con{M.Alloc{+aid, +size, +refs, +freed}, +t}: + c => no_live_no_bytes.fin(size, freed, t, c, no_live_no_bytes(t)) + +# Invariant laws +# -------------- + +def Laws.inv_start(limit): + Laws.Conj{{==}, Unit{}} + +# the consistency of the allocation a lookup finds +def ok_of_lookup(+id: Nat, +allocs: List<&2, M.Alloc>, -allocated: Nat, w: Laws.Inv(allocs, allocated)) -> AllocOkM(M.lookup(id, allocs)): + Laws.Conj{e, c} = w + lookup_ok(id, allocs)(c) + +# the closed allocator answers every request without touching its state +def kept_closed(r: M.Req, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, w: Laws.Inv(allocs, allocated)) + -> Laws.Inv_s(M.state(M.step_closed(r, allocs, allocated, limit, next))): + match r: + case M.RAlloc{size}: + w + case M.RRetain{id, n}: + w + case M.RRelease{id, n}: + w + case M.RClose{}: + w + +# buffer(size): the counter grows by the size of the new live allocation +def alloc_bytes(+size: Nat, -allocs: List<&2, M.Alloc>, +allocated: Nat, e: {allocated == M.live_bytes(allocs) : Nat}) + -> {Nat.add(allocated, size) == Nat.add(size, M.live_bytes(allocs)) : Nat}: + %e : {Nat.add(allocated, size) == Nat.add(size, _) : Nat} + add_comm(allocated, size) + +def kept_alloc.fin(ok: Bool, +size: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, w: Laws.Inv(allocs, allocated)) + -> Laws.Inv_s(M.state(M.alloc.fits(size, allocs, allocated, limit, next, ok))): + match ok: + case True{}: + Laws.Conj{e, c} = w + Laws.Conj{alloc_bytes(size, allocs, allocated, e), Laws.Conj{{==}, c}} + case False{}: + w + +def kept_alloc(size: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, w: Laws.Inv(allocs, allocated)) + -> Laws.Inv_s(M.state(M.alloc(size, allocs, allocated, limit, next))): + match size: + case 0n: + w + case 1n+p: + +size2 = {1n+p : Nat} + kept_alloc.fin(Nat.is_le(Nat.add(allocated, size2), limit), size2, allocs, allocated, limit, next, w) + +# a replacement with the same bytes as the allocation it replaces keeps the counter right +def same_bytes.fix(-L: Nat, -L2: Nat, -B2: Nat, -B1: Nat, -B: Nat, rb: {Nat.add(L, B2) == Nat.add(L2, B1) : Nat}, b2: {B2 == B : Nat}, b1: {B1 == B : Nat}) + -> {Nat.add(L, B) == Nat.add(L2, B) : Nat}: + %b2 : {Nat.add(L, _) == Nat.add(L2, B) : Nat} + %b1 : {Nat.add(L, B2) == Nat.add(L2, _) : Nat} + rb + +def same_bytes(+id: Nat, +a2: M.Alloc, +allocs: List<&2, M.Alloc>, +allocated: Nat, +B: Nat, -a: M.Alloc, + el: {M.lookup(id, allocs) == Some{a} : Maybe<&2, M.Alloc>}, + e: {allocated == M.live_bytes(allocs) : Nat}, + b2: {M.bytes(a2) == B : Nat}, + b1: {M.bytes(a) == B : Nat}) + -> {allocated == M.live_bytes(M.replace(id, a2, allocs)) : Nat}: + rb = replace_bytes_at(id, a2, allocs, Some{a}, el) + %add_cancel_r(M.live_bytes(allocs), M.live_bytes(M.replace(id, a2, allocs)), B, same_bytes.fix(M.live_bytes(allocs), M.live_bytes(M.replace(id, a2, allocs)), M.bytes(a2), M.bytes(a), B, rb, b2, b1)) : {allocated == _ : Nat} + e + +# retain(n) on a live allocation: the count grows, the bytes do not move +def kept_retain.live(+id: Nat, +n: Nat, +aid: Nat, +size: Nat, refs: Nat, +freed: Bool, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + w: Laws.Inv(allocs, allocated), el: {M.lookup(id, allocs) == Some{M.Alloc{aid, size, refs, freed}} : Maybe<&2, M.Alloc>}, + ok: Laws.AllocOk(M.Alloc{aid, size, refs, freed})) + -> Laws.Inv_s(M.state(M.retain.live(id, n, size, refs, freed, allocs, allocated, limit, next))): + match refs: + case 0n: + w + case 1n+q: + Laws.Conj{e, c} = w + +refs2 = {1n+q : Nat} + Laws.Conj{same_bytes(id, M.Alloc{id, size, Nat.add(refs2, n), freed}, allocs, allocated, M.bytes.of(freed, size), M.Alloc{aid, size, refs2, freed}, el, e, {==}, {==}), + replace_ok(id, M.Alloc{id, size, Nat.add(refs2, n), freed}, allocs)(c, ok)} + +def kept_retain.found(+id: Nat, +n: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + w: Laws.Inv(allocs, allocated), m0: Maybe<&2, M.Alloc>, el: {M.lookup(id, allocs) == m0 : Maybe<&2, M.Alloc>}, ok: AllocOkM(m0)) + -> Laws.Inv_s(M.state(M.retain.found(id, n, m0, allocs, allocated, limit, next))): + match m0: + case None{}: + w + case Some{M.Alloc{+aid, +size, refs, freed}}: + kept_retain.live(id, n, aid, size, refs, freed, allocs, allocated, limit, next, w, el, ok) + +def kept_retain(+id: Nat, n: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, +w: Laws.Inv(allocs, allocated)) + -> Laws.Inv_s(M.state(M.retain(id, n, allocs, allocated, limit, next))): + match n: + case 0n: + w + case 1n+m: + kept_retain.found(id, 1n+m, allocs, allocated, limit, next, w, M.lookup(id, allocs), {==}, ok_of_lookup(id, allocs, allocated, w)) + +# release(n) that frees: the counter loses the size of the allocation, +# whose bytes were its size (it was live: refs >= n >= 1) +def freed_bytes(+L: Nat, -L2: Nat, -B: Nat, -size: Nat, rb: {Nat.add(L, 0n) == Nat.add(L2, B) : Nat}, bl: {B == size : Nat}) -> {L == Nat.add(L2, size) : Nat}: + %bl : {L == Nat.add(L2, _) : Nat} + %Equal.sym(Nat, L, Nat.add(L, 0n), add_zero(L)) : {_ == Nat.add(L2, B) : Nat} + rb + +def live_bytes_of(-freed: Bool, -refs: Nat, -size: Nat, ok: {freed == Nat.is_eq(refs, 0n) : Bool}, pos: {Nat.is_eq(refs, 0n) == False{} : Bool}) + -> {M.bytes.of(freed, size) == size : Nat}: + %Equal.sym(Bool, freed, False{}, Equal.trans(Bool, freed, Nat.is_eq(refs, 0n), False{}, ok, pos)) : {M.bytes.of(_, size) == size : Nat} + {==} + +def kept_release.freed(+id: Nat, +size: Nat, -aid: Nat, -refs: Nat, -freed: Bool, +allocs: List<&2, M.Alloc>, +allocated: Nat, + el: {M.lookup(id, allocs) == Some{M.Alloc{aid, size, refs, freed}} : Maybe<&2, M.Alloc>}, + e: {allocated == M.live_bytes(allocs) : Nat}, + bl: {M.bytes.of(freed, size) == size : Nat}) + -> {Nat.sub(allocated, size) == M.live_bytes(M.replace(id, M.Alloc{id, size, 0n, True{}}, allocs)) : Nat}: + fb = freed_bytes(M.live_bytes(allocs), M.live_bytes(M.replace(id, M.Alloc{id, size, 0n, True{}}, allocs)), M.bytes.of(freed, size), size, + replace_bytes_at(id, M.Alloc{id, size, 0n, True{}}, allocs, Some{M.Alloc{aid, size, refs, freed}}, el), bl) + %Equal.sym(Nat, allocated, M.live_bytes(allocs), e) : {Nat.sub(_, size) == M.live_bytes(M.replace(id, M.Alloc{id, size, 0n, True{}}, allocs)) : Nat} + %Equal.sym(Nat, M.live_bytes(allocs), Nat.add(M.live_bytes(M.replace(id, M.Alloc{id, size, 0n, True{}}, allocs)), size), fb) : {Nat.sub(_, size) == M.live_bytes(M.replace(id, M.Alloc{id, size, 0n, True{}}, allocs)) : Nat} + Equal.sym(Nat, M.live_bytes(M.replace(id, M.Alloc{id, size, 0n, True{}}, allocs)), Nat.sub(Nat.add(M.live_bytes(M.replace(id, M.Alloc{id, size, 0n, True{}}, allocs)), size), size), + sub_add_cancel(M.live_bytes(M.replace(id, M.Alloc{id, size, 0n, True{}}, allocs)), size)) + +# release(n) after the decrement, over the new count refs2 = refs - n +def kept_release.new(refs2: Nat, +id: Nat, +n: Nat, +aid: Nat, +size: Nat, +refs: Nat, +freed: Bool, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + w: Laws.Inv(allocs, allocated), el: {M.lookup(id, allocs) == Some{M.Alloc{aid, size, refs, freed}} : Maybe<&2, M.Alloc>}, + ok: Laws.AllocOk(M.Alloc{aid, size, refs, freed}), + e2: {refs2 == Nat.sub(refs, n) : Nat}, pos: {Nat.is_eq(refs, 0n) == False{} : Bool}) + -> Laws.Inv_s(M.state(M.release.new(id, size, refs2, freed, allocs, allocated, limit, next))): + match refs2: + case 0n: + Laws.Conj{e, c} = w + Laws.Conj{kept_release.freed(id, size, aid, refs, freed, allocs, allocated, el, e, live_bytes_of(freed, refs, size, ok, pos)), + replace_ok(id, M.Alloc{id, size, 0n, True{}}, allocs)(c, {==})} + case 1n+q: + Laws.Conj{e, c} = w + +refs3 = {1n+q : Nat} + Laws.Conj{same_bytes(id, M.Alloc{id, size, refs3, freed}, allocs, allocated, M.bytes.of(freed, size), M.Alloc{aid, size, refs, freed}, el, e, {==}, {==}), + replace_ok(id, M.Alloc{id, size, refs3, freed}, allocs)(c, Equal.trans(Bool, freed, Nat.is_eq(refs, 0n), False{}, ok, pos))} + +def kept_release.checked(negative: Bool, +id: Nat, +n: Nat, +aid: Nat, +size: Nat, +refs: Nat, +freed: Bool, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + w: Laws.Inv(allocs, allocated), el: {M.lookup(id, allocs) == Some{M.Alloc{aid, size, refs, freed}} : Maybe<&2, M.Alloc>}, + ok: Laws.AllocOk(M.Alloc{aid, size, refs, freed}), e3: {negative == Nat.is_lt(refs, 1n+n) : Bool}) + -> Laws.Inv_s(M.state(M.release.checked(id, 1n+n, size, refs, freed, allocs, allocated, limit, next, negative))): + match negative: + case True{}: + w + case False{}: + kept_release.new(Nat.sub(refs, 1n+n), id, 1n+n, aid, size, refs, freed, allocs, allocated, limit, next, w, el, ok, {==}, ge_succ_pos(refs, n, e3)) + +def kept_release.found(+id: Nat, +n: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + w: Laws.Inv(allocs, allocated), m0: Maybe<&2, M.Alloc>, el: {M.lookup(id, allocs) == m0 : Maybe<&2, M.Alloc>}, ok: AllocOkM(m0)) + -> Laws.Inv_s(M.state(M.release.found(id, 1n+n, m0, allocs, allocated, limit, next))): + match m0: + case None{}: + w + case Some{M.Alloc{+aid, +size, +refs, +freed}}: + kept_release.checked(Nat.is_lt(refs, 1n+n), id, n, aid, size, refs, freed, allocs, allocated, limit, next, w, el, ok, {==}) + +def kept_release(+id: Nat, n: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, +w: Laws.Inv(allocs, allocated)) + -> Laws.Inv_s(M.state(M.release(id, n, allocs, allocated, limit, next))): + match n: + case 0n: + w + case 1n+m: + kept_release.found(id, m, allocs, allocated, limit, next, w, M.lookup(id, allocs), {==}, ok_of_lookup(id, allocs, allocated, w)) + +def kept_close(leak: Bool, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, w: Laws.Inv(allocs, allocated)) + -> Laws.Inv_s(M.state(M.close(allocs, allocated, limit, next, leak))): + match leak: + case True{}: + w + case False{}: + w + +def kept_step(closed: Bool, r: M.Req, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, w: Laws.Inv(allocs, allocated)) + -> Laws.Inv_s(M.state(M.step(r, allocs, allocated, limit, next, closed))): + match closed: + case True{}: + kept_closed(r, allocs, allocated, limit, next, w) + case False{}: + match r: + case M.RAlloc{size}: + kept_alloc(size, allocs, allocated, limit, next, w) + case M.RRetain{+id, n}: + kept_retain(id, n, allocs, allocated, limit, next, w) + case M.RRelease{+id, n}: + kept_release(id, n, allocs, allocated, limit, next, w) + case M.RClose{}: + kept_close(M.has_live(allocs), allocs, allocated, limit, next, w) + +def Laws.inv_kept(r, allocs, allocated, limit, next, closed, w): + kept_step(closed, r, allocs, allocated, limit, next, w) + +# Response laws +# ------------- + +# the unchanged state beside a response +def Unchanged(+allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, closed: Bool, r: M.Resp) -> M.Allocator & M.Resp: + (M.Allocator{allocs, allocated, limit, next, closed}, r) + +# Release + +def Laws.release_zero_is_error(id, allocs, allocated, limit, next): + {==} + +# over the lookup result m0 +def rel_below.fin(m0: Maybe<&2, M.Alloc>, +id: Nat, +m: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + lt: Laws.T(Nat.is_lt(M.refs_of.m(m0), 1n+m))) + -> {M.release.found(id, 1n+m, m0, allocs, allocated, limit, next) == Unchanged(allocs, allocated, limit, next, False{}, M.RErr{}) : M.Allocator & M.Resp}: + match m0: + case None{}: + {==} + case Some{M.Alloc{aid, +size, +refs, +freed}}: + %T_true(Nat.is_lt(refs, 1n+m), lt) : {M.release.checked(id, 1n+m, size, refs, freed, allocs, allocated, limit, next, _) == Unchanged(allocs, allocated, limit, next, False{}, M.RErr{}) : M.Allocator & M.Resp} + {==} + +def Laws.release_below_zero_is_error(id, n, allocs, allocated, limit, next, lt): + match n: + case 0n: + {==} + case 1n+m: + rel_below.fin(M.lookup(id, allocs), id, m, allocs, allocated, limit, next, lt) + +# a found allocation that is not live has count 0, so any release overdraws +def rel_dead.fix(refs: Nat, freed: Bool, +id: Nat, +m: Nat, +size: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + ok: {freed == Nat.is_eq(refs, 0n) : Bool}, d: Laws.T(Bool.not(Bool.not(freed)))) + -> {M.release.checked(id, 1n+m, size, refs, freed, allocs, allocated, limit, next, Nat.is_lt(refs, 1n+m)) == Unchanged(allocs, allocated, limit, next, False{}, M.RErr{}) : M.Allocator & M.Resp}: + match refs: + case 0n: + {==} + case 1n+r: + match freed: + case True{}: + Empty.absurd({M.release.checked(id, 1n+m, size, 1n+r, True{}, allocs, allocated, limit, next, Nat.is_lt(1n+r, 1n+m)) == Unchanged(allocs, allocated, limit, next, False{}, M.RErr{}) : M.Allocator & M.Resp}, true_ne_false(ok)) + case False{}: + match d: + +def rel_dead.fin(m0: Maybe<&2, M.Alloc>, +id: Nat, +m: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + ok: AllocOkM(m0), d: Laws.T(Bool.not(M.is_live.m(m0)))) + -> {M.release.found(id, 1n+m, m0, allocs, allocated, limit, next) == Unchanged(allocs, allocated, limit, next, False{}, M.RErr{}) : M.Allocator & M.Resp}: + match m0: + case None{}: + {==} + case Some{M.Alloc{aid, +size, refs, freed}}: + rel_dead.fix(refs, freed, id, m, size, allocs, allocated, limit, next, ok, d) + +def Laws.release_dead_is_error(id, n, allocs, allocated, limit, next, w, d): + match n: + case 0n: + {==} + case 1n+m: + rel_dead.fin(M.lookup(id, allocs), id, m, allocs, allocated, limit, next, ok_of_lookup(id, allocs, allocated, w), d) + +# after replacing the found allocation by a freed one, the id is freed +def freed_after(+id: Nat, +size: Nat, +allocs: List<&2, M.Alloc>, -a: M.Alloc, el: {M.lookup(id, allocs) == Some{a} : Maybe<&2, M.Alloc>}) + -> Laws.T(M.is_freed(id, M.replace(id, M.Alloc{id, size, 0n, True{}}, allocs))): + %Equal.sym(Maybe<&2, M.Alloc>, M.lookup(id, M.replace(id, M.Alloc{id, size, 0n, True{}}, allocs)), Some{M.Alloc{id, size, 0n, True{}}}, lookup_replace(id, size, 0n, True{}, a, allocs)(el)) : Laws.T(M.is_freed.m(_)) + Unit{} + +# after replacing the found allocation by a live one, the id is live with that count +def live_after(+id: Nat, +size: Nat, +refs: Nat, +allocs: List<&2, M.Alloc>, -a: M.Alloc, el: {M.lookup(id, allocs) == Some{a} : Maybe<&2, M.Alloc>}) + -> Laws.T(M.is_live(id, M.replace(id, M.Alloc{id, size, refs, False{}}, allocs))): + %Equal.sym(Maybe<&2, M.Alloc>, M.lookup(id, M.replace(id, M.Alloc{id, size, refs, False{}}, allocs)), Some{M.Alloc{id, size, refs, False{}}}, lookup_replace(id, size, refs, False{}, a, allocs)(el)) : Laws.T(M.is_live.m(_)) + Unit{} + +def count_after(+id: Nat, +size: Nat, +refs: Nat, +allocs: List<&2, M.Alloc>, -a: M.Alloc, el: {M.lookup(id, allocs) == Some{a} : Maybe<&2, M.Alloc>}, + -target: Nat, e: {refs == target : Nat}) + -> {M.refs_of(id, M.replace(id, M.Alloc{id, size, refs, False{}}, allocs)) == target : Nat}: + %Equal.sym(Maybe<&2, M.Alloc>, M.lookup(id, M.replace(id, M.Alloc{id, size, refs, False{}}, allocs)), Some{M.Alloc{id, size, refs, False{}}}, lookup_replace(id, size, refs, False{}, a, allocs)(el)) : {M.refs_of.m(_) == target : Nat} + e + +# release to zero: the goal, over the lookup result, the verdict, and the new count +def FreesGoal(m0: Maybe<&2, M.Alloc>, +id: Nat, +m: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Type: + {M.resp(M.release.found(id, 1n+m, m0, allocs, allocated, limit, next)) == M.RFreed{} : M.Resp} + & Laws.T(M.is_freed(id, M.allocs_of(M.state(M.release.found(id, 1n+m, m0, allocs, allocated, limit, next))))) + & {M.allocated_of(M.state(M.release.found(id, 1n+m, m0, allocs, allocated, limit, next))) == Nat.sub(allocated, M.size_of.m(m0)) : Nat} + +def FreesGoal2(neg: Bool, +id: Nat, +m: Nat, +size: Nat, +freed: Bool, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Type: + {M.resp(M.release.checked(id, 1n+m, size, 1n+m, freed, allocs, allocated, limit, next, neg)) == M.RFreed{} : M.Resp} + & Laws.T(M.is_freed(id, M.allocs_of(M.state(M.release.checked(id, 1n+m, size, 1n+m, freed, allocs, allocated, limit, next, neg))))) + & {M.allocated_of(M.state(M.release.checked(id, 1n+m, size, 1n+m, freed, allocs, allocated, limit, next, neg))) == Nat.sub(allocated, size) : Nat} + +def FreesGoal3(refs2: Nat, +id: Nat, +size: Nat, +freed: Bool, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Type: + {M.resp(M.release.new(id, size, refs2, freed, allocs, allocated, limit, next)) == M.RFreed{} : M.Resp} + & Laws.T(M.is_freed(id, M.allocs_of(M.state(M.release.new(id, size, refs2, freed, allocs, allocated, limit, next))))) + & {M.allocated_of(M.state(M.release.new(id, size, refs2, freed, allocs, allocated, limit, next))) == Nat.sub(allocated, size) : Nat} + +def frees.new(refs2: Nat, +id: Nat, +m: Nat, +size: Nat, +freed: Bool, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + -a: M.Alloc, el: {M.lookup(id, allocs) == Some{a} : Maybe<&2, M.Alloc>}, e4: {refs2 == Nat.sub(1n+m, 1n+m) : Nat}) + -> FreesGoal3(refs2, id, size, freed, allocs, allocated, limit, next): + match refs2: + case 0n: + ({==}, (freed_after(id, size, allocs, a, el), {==})) + case 1n+q: + Empty.absurd(FreesGoal3(1n+q, id, size, freed, allocs, allocated, limit, next), + zero_ne_succ(q, Equal.sym(Nat, 1n+q, 0n, Equal.trans(Nat, 1n+q, Nat.sub(1n+m, 1n+m), 0n, e4, Equal.sym(Nat, 0n, Nat.sub(1n+m, 1n+m), sub_self(1n+m)))))) + +def frees.checked(neg: Bool, +id: Nat, +m: Nat, +size: Nat, +freed: Bool, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + -a: M.Alloc, el: {M.lookup(id, allocs) == Some{a} : Maybe<&2, M.Alloc>}, e3: {neg == Nat.is_lt(1n+m, 1n+m) : Bool}) + -> FreesGoal2(neg, id, m, size, freed, allocs, allocated, limit, next): + match neg: + case True{}: + Empty.absurd(FreesGoal2(True{}, id, m, size, freed, allocs, allocated, limit, next), + true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(1n+m, 1n+m), False{}, e3, Equal.sym(Bool, False{}, Nat.is_lt(1n+m, 1n+m), lt_irrefl(1n+m))))) + case False{}: + frees.new(Nat.sub(1n+m, 1n+m), id, m, size, freed, allocs, allocated, limit, next, a, el, {==}) + +def frees.fin(m0: Maybe<&2, M.Alloc>, +id: Nat, +m: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + el: {M.lookup(id, allocs) == m0 : Maybe<&2, M.Alloc>}, e: {M.refs_of.m(m0) == 1n+m : Nat}) + -> FreesGoal(m0, id, m, allocs, allocated, limit, next): + match m0: + case None{}: + Empty.absurd(FreesGoal(None{}, id, m, allocs, allocated, limit, next), zero_ne_succ(m, e)) + case Some{M.Alloc{+aid, +size, +refs, +freed}}: + %Equal.sym(Nat, refs, 1n+m, e) : FreesGoal(Some{M.Alloc{aid, size, _, freed}}, id, m, allocs, allocated, limit, next) + frees.checked(Nat.is_lt(1n+m, 1n+m), id, m, size, freed, allocs, allocated, limit, next, M.Alloc{aid, size, refs, freed}, el, {==}) + +def Laws.release_to_zero_frees(id, m, allocs, allocated, limit, next, e): + frees.fin(M.lookup(id, allocs), id, m, allocs, allocated, limit, next, {==}, e) + +# release that keeps the memory: the goal, over the lookup result, the verdict, and the new count +def KeepsGoal(m0: Maybe<&2, M.Alloc>, +id: Nat, +m: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Type: + {M.resp(M.release.found(id, 1n+m, m0, allocs, allocated, limit, next)) == M.ROk{} : M.Resp} + & Laws.T(M.is_live(id, M.allocs_of(M.state(M.release.found(id, 1n+m, m0, allocs, allocated, limit, next))))) + & {M.refs_of(id, M.allocs_of(M.state(M.release.found(id, 1n+m, m0, allocs, allocated, limit, next)))) == Nat.sub(M.refs_of.m(m0), 1n+m) : Nat} + & {M.allocated_of(M.state(M.release.found(id, 1n+m, m0, allocs, allocated, limit, next))) == allocated : Nat} + +def KeepsGoal2(neg: Bool, +id: Nat, +m: Nat, +size: Nat, +refs: Nat, +freed: Bool, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Type: + {M.resp(M.release.checked(id, 1n+m, size, refs, freed, allocs, allocated, limit, next, neg)) == M.ROk{} : M.Resp} + & Laws.T(M.is_live(id, M.allocs_of(M.state(M.release.checked(id, 1n+m, size, refs, freed, allocs, allocated, limit, next, neg))))) + & {M.refs_of(id, M.allocs_of(M.state(M.release.checked(id, 1n+m, size, refs, freed, allocs, allocated, limit, next, neg)))) == Nat.sub(refs, 1n+m) : Nat} + & {M.allocated_of(M.state(M.release.checked(id, 1n+m, size, refs, freed, allocs, allocated, limit, next, neg))) == allocated : Nat} + +def KeepsGoal3(refs2: Nat, +id: Nat, +m: Nat, +size: Nat, +refs: Nat, +freed: Bool, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Type: + {M.resp(M.release.new(id, size, refs2, freed, allocs, allocated, limit, next)) == M.ROk{} : M.Resp} + & Laws.T(M.is_live(id, M.allocs_of(M.state(M.release.new(id, size, refs2, freed, allocs, allocated, limit, next))))) + & {M.refs_of(id, M.allocs_of(M.state(M.release.new(id, size, refs2, freed, allocs, allocated, limit, next)))) == Nat.sub(refs, 1n+m) : Nat} + & {M.allocated_of(M.state(M.release.new(id, size, refs2, freed, allocs, allocated, limit, next))) == allocated : Nat} + +def keeps.new(refs2: Nat, +id: Nat, +m: Nat, +size: Nat, +refs: Nat, +freed: Bool, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + -a: M.Alloc, +el: {M.lookup(id, allocs) == Some{a} : Maybe<&2, M.Alloc>}, fl: {freed == False{} : Bool}, + lt: Laws.T(Nat.is_lt(1n+m, refs)), e4: {refs2 == Nat.sub(refs, 1n+m) : Nat}) + -> KeepsGoal3(refs2, id, m, size, refs, freed, allocs, allocated, limit, next): + match refs2: + case 0n: + Empty.absurd(KeepsGoal3(0n, id, m, size, refs, freed, allocs, allocated, limit, next), + zero_ne_succ(Nat.sub(refs, 2n+m), Equal.trans(Nat, 0n, Nat.sub(refs, 1n+m), 1n+Nat.sub(refs, 2n+m), e4, Equal.sym(Nat, 1n+Nat.sub(refs, 2n+m), Nat.sub(refs, 1n+m), lt_sub_succ(1n+m, refs, lt))))) + case 1n+q: + +refs3 = {1n+q : Nat} + %Equal.sym(Bool, freed, False{}, fl) : KeepsGoal3(refs3, id, m, size, refs, _, allocs, allocated, limit, next) + ({==}, (live_after(id, size, refs3, allocs, a, el), (count_after(id, size, refs3, allocs, a, el, Nat.sub(refs, 1n+m), e4), {==}))) + +def keeps.checked(neg: Bool, +id: Nat, +m: Nat, +size: Nat, +refs: Nat, +freed: Bool, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + -a: M.Alloc, el: {M.lookup(id, allocs) == Some{a} : Maybe<&2, M.Alloc>}, fl: {freed == False{} : Bool}, + +lt: Laws.T(Nat.is_lt(1n+m, refs)), e3: {neg == Nat.is_lt(refs, 1n+m) : Bool}) + -> KeepsGoal2(neg, id, m, size, refs, freed, allocs, allocated, limit, next): + match neg: + case True{}: + Empty.absurd(KeepsGoal2(True{}, id, m, size, refs, freed, allocs, allocated, limit, next), + true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(refs, 1n+m), False{}, e3, Equal.sym(Bool, False{}, Nat.is_lt(refs, 1n+m), lt_asym(1n+m, refs, lt))))) + case False{}: + keeps.new(Nat.sub(refs, 1n+m), id, m, size, refs, freed, allocs, allocated, limit, next, a, el, fl, lt, {==}) + +def keeps.fin(m0: Maybe<&2, M.Alloc>, +id: Nat, +m: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + el: {M.lookup(id, allocs) == m0 : Maybe<&2, M.Alloc>}, ok: AllocOkM(m0), +lt: Laws.T(Nat.is_lt(1n+m, M.refs_of.m(m0)))) + -> KeepsGoal(m0, id, m, allocs, allocated, limit, next): + match m0: + case None{}: + match lt: + case Some{M.Alloc{+aid, +size, +refs, +freed}}: + keeps.checked(Nat.is_lt(refs, 1n+m), id, m, size, refs, freed, allocs, allocated, limit, next, M.Alloc{aid, size, refs, freed}, el, + Equal.trans(Bool, freed, Nat.is_eq(refs, 0n), False{}, ok, lt_pos(m, refs, lt)), lt, {==}) + +def Laws.release_keeps_live(id, m, allocs, allocated, limit, next, w, lt): + keeps.fin(M.lookup(id, allocs), id, m, allocs, allocated, limit, next, {==}, ok_of_lookup(id, allocs, allocated, w), lt) + +# Retain + +def Laws.retain_zero_is_error(id, allocs, allocated, limit, next): + {==} + +def ret_dead.fix(refs: Nat, freed: Bool, +id: Nat, +m: Nat, +size: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + ok: {freed == Nat.is_eq(refs, 0n) : Bool}, d: Laws.T(Bool.not(Bool.not(freed)))) + -> {M.retain.live(id, 1n+m, size, refs, freed, allocs, allocated, limit, next) == Unchanged(allocs, allocated, limit, next, False{}, M.RErr{}) : M.Allocator & M.Resp}: + match refs: + case 0n: + {==} + case 1n+r: + match freed: + case True{}: + Empty.absurd({M.retain.live(id, 1n+m, size, 1n+r, True{}, allocs, allocated, limit, next) == Unchanged(allocs, allocated, limit, next, False{}, M.RErr{}) : M.Allocator & M.Resp}, true_ne_false(ok)) + case False{}: + match d: + +def ret_dead.fin(m0: Maybe<&2, M.Alloc>, +id: Nat, +m: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + ok: AllocOkM(m0), d: Laws.T(Bool.not(M.is_live.m(m0)))) + -> {M.retain.found(id, 1n+m, m0, allocs, allocated, limit, next) == Unchanged(allocs, allocated, limit, next, False{}, M.RErr{}) : M.Allocator & M.Resp}: + match m0: + case None{}: + {==} + case Some{M.Alloc{aid, +size, refs, freed}}: + ret_dead.fix(refs, freed, id, m, size, allocs, allocated, limit, next, ok, d) + +def Laws.retain_dead_is_error(id, n, allocs, allocated, limit, next, w, d): + match n: + case 0n: + {==} + case 1n+m: + ret_dead.fin(M.lookup(id, allocs), id, m, allocs, allocated, limit, next, ok_of_lookup(id, allocs, allocated, w), d) + +def AddsGoal(m0: Maybe<&2, M.Alloc>, +id: Nat, +m: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Type: + {M.resp(M.retain.found(id, 1n+m, m0, allocs, allocated, limit, next)) == M.ROk{} : M.Resp} + & Laws.T(M.is_live(id, M.allocs_of(M.state(M.retain.found(id, 1n+m, m0, allocs, allocated, limit, next))))) + & {M.refs_of(id, M.allocs_of(M.state(M.retain.found(id, 1n+m, m0, allocs, allocated, limit, next)))) == Nat.add(M.refs_of.m(m0), 1n+m) : Nat} + & {M.allocated_of(M.state(M.retain.found(id, 1n+m, m0, allocs, allocated, limit, next))) == allocated : Nat} + +def AddsGoal2(refs: Nat, freed: Bool, +id: Nat, +m: Nat, +size: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Type: + {M.resp(M.retain.live(id, 1n+m, size, refs, freed, allocs, allocated, limit, next)) == M.ROk{} : M.Resp} + & Laws.T(M.is_live(id, M.allocs_of(M.state(M.retain.live(id, 1n+m, size, refs, freed, allocs, allocated, limit, next))))) + & {M.refs_of(id, M.allocs_of(M.state(M.retain.live(id, 1n+m, size, refs, freed, allocs, allocated, limit, next)))) == Nat.add(refs, 1n+m) : Nat} + & {M.allocated_of(M.state(M.retain.live(id, 1n+m, size, refs, freed, allocs, allocated, limit, next))) == allocated : Nat} + +def adds.fix(refs: Nat, freed: Bool, +id: Nat, +m: Nat, +aid: Nat, +size: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + +el: {M.lookup(id, allocs) == Some{M.Alloc{aid, size, refs, freed}} : Maybe<&2, M.Alloc>}, + ok: {freed == Nat.is_eq(refs, 0n) : Bool}, l: Laws.T(Bool.not(freed))) + -> AddsGoal2(refs, freed, id, m, size, allocs, allocated, limit, next): + match refs: + case 0n: + match freed: + case True{}: + match l: + case False{}: + Empty.absurd(AddsGoal2(0n, False{}, id, m, size, allocs, allocated, limit, next), false_ne_true(ok)) + case 1n+q: + match freed: + case True{}: + match l: + case False{}: + +refs3 = {1n+q : Nat} + ({==}, (live_after(id, size, Nat.add(refs3, 1n+m), allocs, M.Alloc{aid, size, refs3, False{}}, el), + (count_after(id, size, Nat.add(refs3, 1n+m), allocs, M.Alloc{aid, size, refs3, False{}}, el, Nat.add(refs3, 1n+m), {==}), {==}))) + +def adds.fin(m0: Maybe<&2, M.Alloc>, +id: Nat, +m: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, + el: {M.lookup(id, allocs) == m0 : Maybe<&2, M.Alloc>}, ok: AllocOkM(m0), l: Laws.T(M.is_live.m(m0))) + -> AddsGoal(m0, id, m, allocs, allocated, limit, next): + match m0: + case None{}: + match l: + case Some{M.Alloc{+aid, +size, refs, freed}}: + adds.fix(refs, freed, id, m, aid, size, allocs, allocated, limit, next, el, ok, l) + +def Laws.retain_live_adds(id, m, allocs, allocated, limit, next, w, l): + adds.fin(M.lookup(id, allocs), id, m, allocs, allocated, limit, next, {==}, ok_of_lookup(id, allocs, allocated, w), l) + +# Allocation + +def Laws.alloc_over_limit_rejected(p, allocs, allocated, limit, next, over): + %lt_not_le(limit, Nat.add(allocated, 1n+p), over) : {M.alloc.fits(1n+p, allocs, allocated, limit, next, _) == Unchanged(allocs, allocated, limit, next, False{}, M.ROom{}) : M.Allocator & M.Resp} + {==} + +def ServedGoal(ok: Bool, +p: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Type: + {M.resp(M.alloc.fits(1n+p, allocs, allocated, limit, next, ok)) == M.RBuf{next} : M.Resp} + & {M.refs_of(next, M.allocs_of(M.state(M.alloc.fits(1n+p, allocs, allocated, limit, next, ok)))) == 1n : Nat} + & {M.allocated_of(M.state(M.alloc.fits(1n+p, allocs, allocated, limit, next, ok))) == Nat.add(allocated, 1n+p) : Nat} + +# the new buffer is found first, with a count of 1 +def served_refs(+p: Nat, +allocs: List<&2, M.Alloc>, +next: Nat) -> {M.refs_of(next, M.Alloc{next, 1n+p, 1n, False{}} <> allocs) == 1n : Nat}: + %eq_refl(next) : {M.refs_of.m(M.lookup.at(M.Alloc{next, 1n+p, 1n, False{}}, M.lookup(next, allocs), _)) == 1n : Nat} + {==} + +def served.fin(ok: Bool, +p: Nat, +allocs: List<&2, M.Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, fits: Laws.T(ok)) + -> ServedGoal(ok, p, allocs, allocated, limit, next): + match ok: + case True{}: + ({==}, (served_refs(p, allocs, next), {==})) + case False{}: + match fits: + +def Laws.alloc_within_limit_served(p, allocs, allocated, limit, next, fits): + served.fin(Nat.is_le(Nat.add(allocated, 1n+p), limit), p, allocs, allocated, limit, next, fits) + +def Laws.alloc_zero_is_empty(allocs, allocated, limit, next): + {==} + +# Close + +def Laws.close_with_live_buffer_is_error(id, allocs, allocated, limit, next, l): + %live_has_live(id, allocs)(l) : {M.resp(M.close(allocs, allocated, limit, next, _)) == M.RErr{} : M.Resp} + {==} + +def Laws.close_clean_succeeds(allocs, allocated, limit, next, c): + %c : {M.close(allocs, allocated, limit, next, _) == Unchanged(allocs, allocated, limit, next, True{}, M.ROk{}) : M.Allocator & M.Resp} + {==} + +def Laws.clean_means_zero_bytes(allocs, allocated, w, c): + Laws.Conj{e, cons} = w + %Equal.sym(Nat, allocated, M.live_bytes(allocs), e) : {_ == 0n : Nat} + no_live_no_bytes(allocs)(c) + +def Laws.closed_rejects(r, allocs, allocated, limit, next, nc): + match r: + case M.RAlloc{size}: + {==} + case M.RRetain{id, n}: + {==} + case M.RRelease{id, n}: + {==} + case M.RClose{}: + Empty.absurd({M.step(M.RClose{}, allocs, allocated, limit, next, True{}) == Unchanged(allocs, allocated, limit, next, True{}, M.RErr{}) : M.Allocator & M.Resp}, false_ne_true(nc)) + +def Laws.close_twice_is_noop(allocs, allocated, limit, next): + {==} + +# Traces +# ------ + +# each trace starts with buffer(1 + p) on a fresh allocator; the verdict +# of the limit check is the only non-literal computation in it + +def Trace1(ok: Bool, +p: Nat, +limit: Nat) -> Type: + {M.resp(M.run([M.RRelease{0n, 1n}, M.RClose{}], M.alloc.fits(1n+p, Nil{}, 0n, limit, 0n, ok))) == M.ROk{} : M.Resp} + & {M.allocated_of(M.state(M.run([M.RRelease{0n, 1n}, M.RClose{}], M.alloc.fits(1n+p, Nil{}, 0n, limit, 0n, ok)))) == 0n : Nat} + +def trace1.fin(ok: Bool, +p: Nat, +limit: Nat, fits: Laws.T(ok)) -> Trace1(ok, p, limit): + match ok: + case True{}: + ({==}, Equal.sym(Nat, 0n, Nat.sub(p, p), sub_self(p))) + case False{}: + match fits: + +def Laws.trace_alloc_release_frees(p, limit, fits): + trace1.fin(Nat.is_le(Nat.add(0n, 1n+p), limit), p, limit, fits) + +def Trace2(ok: Bool, +p: Nat, +limit: Nat) -> Type: + {M.resp(M.run([M.RRetain{0n, 1n}, M.RRelease{0n, 1n}, M.RClose{}], M.alloc.fits(1n+p, Nil{}, 0n, limit, 0n, ok))) == M.RErr{} : M.Resp} + & {M.refs_of(0n, M.allocs_of(M.state(M.run([M.RRetain{0n, 1n}, M.RRelease{0n, 1n}, M.RClose{}], M.alloc.fits(1n+p, Nil{}, 0n, limit, 0n, ok))))) == 1n : Nat} + & {M.allocated_of(M.state(M.run([M.RRetain{0n, 1n}, M.RRelease{0n, 1n}, M.RClose{}], M.alloc.fits(1n+p, Nil{}, 0n, limit, 0n, ok)))) == 1n+p : Nat} + +def trace2.fin(ok: Bool, +p: Nat, +limit: Nat, fits: Laws.T(ok)) -> Trace2(ok, p, limit): + match ok: + case True{}: + ({==}, ({==}, {==})) + case False{}: + match fits: + +def Laws.trace_retain_keeps_live(p, limit, fits): + trace2.fin(Nat.is_le(Nat.add(0n, 1n+p), limit), p, limit, fits) + +def Trace3(ok: Bool, +p: Nat, +limit: Nat) -> Type: + {M.resp(M.run([M.RRelease{0n, 1n}, M.RRelease{0n, 1n}], M.alloc.fits(1n+p, Nil{}, 0n, limit, 0n, ok))) == M.RErr{} : M.Resp} + +def trace3.fin(ok: Bool, +p: Nat, +limit: Nat, fits: Laws.T(ok)) -> Trace3(ok, p, limit): + match ok: + case True{}: + {==} + case False{}: + match fits: + +def Laws.trace_double_release_is_error(p, limit, fits): + trace3.fin(Nat.is_le(Nat.add(0n, 1n+p), limit), p, limit, fits) diff --git a/dev/bend2/buffer_refcount/README.md b/dev/bend2/buffer_refcount/README.md new file mode 100644 index 0000000000..af83ebf9f9 --- /dev/null +++ b/dev/bend2/buffer_refcount/README.md @@ -0,0 +1,265 @@ + + +# Bend 2 model of ArrowBuf reference counting and allocator accounting + +A proof of concept that uses the Bend 2 language to state and enforce +the reference-counting and ownership protocol of buffers in the +`memory-core` module: `ArrowBuf`, `ReferenceManager` / `BufferLedger`, +`AllocationManager` and `BufferAllocator` / `BaseAllocator` / +`Accountant`. The protocol is written as a small executable model in +Bend, the rules the Javadoc and `Preconditions` messages state are +written as laws, and `bend PROOF.bend` refuses to pass until every law +is proven against the model. + +Written against Bend 2.0.21, commit `6018e28` of +[bendlang/bend](https://github.com/bendlang/bend), on 2026-09-20. The +research notes on Bend 2 itself, and a first model of the Flight SQL +prepared-statement lifecycle, are on the `claude/bend2-arrow-integration-pgexut` +branch under `dev/bend2/`; this directory reuses its proof-kit idioms. + +| File | Lines | Contents | +| --- | ---: | --- | +| `main.bend` | 419 | the model and a runnable trace (`main`) | +| `LAWS.bend` | 388 | 21 laws, plus 4 commented-out laws that are not proven or not expressible | +| `PROOF.bend` | 1001 | the proofs and the lemma library they need | + +## 1. What is modelled + +One `BaseAllocator` and the allocations it owns. Each allocation is one +`AllocationManager` together with its owning `BufferLedger`: + +```python +type Alloc is Data: + Alloc{id: Nat, size: Nat, refs: Nat, freed: Bool} + +type Allocator is Data: + Allocator{allocs: List<&2, Alloc>, allocated: Nat, limit: Nat, next: Nat, closed: Bool} +``` + +- `id` is the handle the `ArrowBuf` carries; `buffer(size)` issues them + from the counter `next`. +- `size` is `AllocationManager.getSize()`, `refs` is + `BufferLedger.getRefCount()`, and `freed` records that + `AllocationManager.release0()` has run for the chunk. +- `allocated` is `Accountant.getAllocatedMemory()` (`locallyHeldMemory`), + `limit` is `Accountant.getLimit()` (`allocationLimit`), and `closed` is + `BaseAllocator.isClosed`. + +Four requests are modelled, each with the checks the Java code makes, +in the order it makes them: + +| Request | Java | Model | +| --- | --- | --- | +| `RAlloc{size}` | `BufferAllocator.buffer(size)` | `size == 0` answers the shared empty buffer (`REmpty`), else `allocated + size <= limit` or `OutOfMemoryException` (`ROom`); on success a new allocation with `refs = 1`, `allocated += size` | +| `RRetain{id, n}` | `buf.getReferenceManager().retain(n)` | `n >= 1` (`checkArgument(increment > 0)`), the ledger exists and `refs > 0` (`checkArgument(originalReferenceCount > 0)`), then `refs += n` | +| `RRelease{id, n}` | `buf.getReferenceManager().release(n)`; `ArrowBuf.close()` is `n = 1` | `n >= 1` (`checkState(decrement >= 1)`), the ledger exists and `refs >= n` (`checkState(refCnt >= 0, "RefCnt has gone negative")`), then `refs -= n`; at 0, `releaseBytes(getSize())` and `release0()` (`RFreed`), else `ROk` | +| `RClose{}` | `BufferAllocator.close()` | `isClosed = true` first; an outstanding buffer is the "Memory was leaked" `IllegalStateException` (`RErr`); a second `close()` is a no-op | + +Every request against a closed allocator except `close()` fails, as +`assertOpen()` does with assertions enabled. + +Sizes and counts are `Nat`, so Java's `long` and `int` are unbounded +here (see section 5). Not modelled: child allocators and reservations +(the `Accountant` parent chain), the rounding policy, slices and +reader/writer indexes, the multi-ledger side of `AllocationManager` +(`retain(ArrowBuf, BufferAllocator)`, `transferOwnership`), and the +`BufferManager` hook. + +`main.bend` runs a trace on a 1024-byte root allocator and prints: + +``` + buffer(512) -> buf0 + buf0.retain(1) -> ok + buf0.release(1) -> ok + buf0.release(1) -> true (memory released) + buf0.release(1) -> IllegalStateException + buffer(768) -> buf1 + buffer(256) -> buf2 + buffer(768) -> OutOfMemoryException + buf1.release(2) -> IllegalStateException + close() -> IllegalStateException + buf1.release(1) -> IllegalStateException + allocated=1024/1024 live_bytes=1024 closed=True +``` + +## 2. The laws + +`LAWS.bend` states 21 laws. Laws hold for arbitrary allocator states; +the ones that need it take the invariant `Inv` as a hypothesis, and the +two invariant laws show every reachable state satisfies it. Each law +below quotes the sentence in `memory-core` it comes from. + +### The invariant (laws 2 and 3 of the brief) + +```python +def Inv(allocs, allocated) -> Data: + And<{allocated == live_bytes(allocs) : Nat}, Consistent(allocs)> +``` + +`live_bytes` sums the sizes of the allocations whose `freed` flag is +false, and `Consistent` says that for every allocation +`freed == (refs == 0)`. + +| Law | Source sentence | +| --- | --- | +| `inv_start` | a fresh `RootAllocator` accounts for nothing | +| `inv_kept` | `BaseAllocator.verifyAllocator`: it fails when `bufferTotal + reservedTotal + childTotal != getAllocatedMemory()`. `ReferenceManager.release`: "If the reference count drops to 0, it implies that ArrowBufs managed by this reference manager no longer need access to the underlying memory"; `AllocationManager.release` then calls `releaseBytes(getSize())` and `release0()`. Every request keeps the counter equal to the live bytes and the freed flag equal to "count is 0". | + +### Release (law 1 and law 2) + +| Law | Source sentence | +| --- | --- | +| `release_zero_is_error` | "ref count decrement should be greater than or equal to 1" (`BufferLedger.release`) | +| `release_below_zero_is_error` | "RefCnt has gone negative" (`BufferLedger.release`): releasing more than is held is an error and changes nothing; an unknown id holds 0 | +| `release_dead_is_error` | a release on a freed or unknown buffer is an error, not a silent no-op: memory is never freed twice (needs `Inv`) | +| `release_to_zero_frees` | "@return true if ref count has dropped to 0" (`ReferenceManager.release`), then `releaseBytes(getSize()); release0()`: the response is `true`, the id is freed afterwards, and the counter drops by the buffer's size | +| `release_keeps_live` | "@return ... false otherwise": the buffer stays live, its count drops by exactly `n`, the counter is untouched (needs `Inv`) | + +### Retain + +| Law | Source sentence | +| --- | --- | +| `retain_zero_is_error` | "retain(%s) argument is not positive" (`BufferLedger.retain`) | +| `retain_dead_is_error` | `Preconditions.checkArgument(originalReferenceCount > 0)` (`BufferLedger.retain`): a retain on a freed or unknown buffer is an error and does not revive it (needs `Inv`) | +| `retain_live_adds` | "Increment this reference manager's reference count by a given amount" (`ReferenceManager.retain`): exactly `n` is added, the buffer stays live, the counter is untouched (needs `Inv`) | + +### Allocation (law 4 and law 6) + +| Law | Source sentence | +| --- | --- | +| `alloc_over_limit_rejected` | "Unable to allocate buffer of size %d due to memory limit" (`BaseAllocator.buffer`); "Either completely succeeds or completely fails. If it fails, no changes are made to accounting." (`Accountant.allocateBytes`) | +| `alloc_within_limit_served` | anti-vacuity: a request that fits answers a new buffer with "a ref count of 1" (`BufferLedger` Javadoc, `associate(this)` in `bufferWithoutReservation`) and the counter grows by its size | +| `alloc_zero_is_empty` | `if (initialRequestSize == 0) return getEmpty();` (`BaseAllocator.buffer`) | + +### Close (law 5) + +| Law | Source sentence | +| --- | --- | +| `close_with_live_buffer_is_error` | "Allocator[%s] closed with outstanding buffers allocated" / "Memory was leaked by query" (`BaseAllocator.close`) | +| `close_clean_succeeds` | with no outstanding buffer, `close()` succeeds and the allocator is closed | +| `clean_means_zero_bytes` | the two leak checks in `BaseAllocator.close` (ledger count in DEBUG mode, `getAllocatedMemory() > 0` always) agree under `Inv` | +| `closed_rejects` | "Attempting operation on allocator when allocator is closed" (`BaseAllocator.assertOpen`): after close, `buffer`, `retain` and `release` fail and change nothing | +| `close_twice_is_noop` | "Some owners may close more than once" (`BaseAllocator.close`) | + +### Traces (law 6, anti-vacuity) + +| Law | Trace | +| --- | --- | +| `trace_alloc_release_frees` | `buffer(1+p); release(); close()` answers `ok` with 0 bytes accounted (`TestBaseAllocator.testRootAllocator_createChildAndUse`) | +| `trace_retain_keeps_live` | `buffer(1+p); retain(); release(); close()` leaves one reference and `1+p` bytes, and `close()` reports the leak (`testRootAllocator_closeWithOutstanding`) | +| `trace_double_release_is_error` | `buffer(1+p); release(); release()` is an error | + +### Not proven or not expressible (kept as comments in `LAWS.bend`) + +| Law | Status | Why | +| --- | --- | --- | +| `transfer_preserves_total` (law 7) | `NOT PROVEN` | `BufferLedger.transferOwnership`: "Transfers will always succeed, even if that puts the other allocator into an overlimit situation." The model has one allocator and one ledger per chunk. A faithful transfer needs `AllocationManager`'s map from allocators to ledgers, an owning ledger per chunk, and `forceAllocate`/`releaseBytes` on two accountants; that is a second model, not a hypothesis on this one. | +| `release_is_atomic` | `NOT EXPRESSIBLE` | `BufferLedger` uses `AtomicIntegerFieldUpdater` and `synchronized (allocationManager)`. Bend is pure; a step is a function, so there is no interleaving to quantify over without an explicit scheduler model. | +| `alloc_overflow_rejected` | `NOT EXPRESSIBLE` | `Accountant.allocate` detects `long` overflow with `((oldLocal ^ newLocal) & (size ^ newLocal)) < 0`. Bend has `Nat`, `U32` and `F32` only; sizes here are unbounded. | +| `read_within_capacity` | `NOT MODELLED` | `ArrowBuf.checkBytes` bounds checking is expressible, but this model has no per-buffer capacity or indexes (slices), only the chunk size. | + +## 3. How to run + +The installer host (`bend-lang.com`) and the docs sites were not +reachable from the sandbox, so the checker is run from a clone with +`bun`, which is what the installed binary wraps: + +```sh +git clone --depth 1 https://github.com/bendlang/bend.git /tmp/bend +BEND="bun /tmp/bend/bend2/main.ts" +cd dev/bend2/buffer_refcount +$BEND PROOF.bend # checks LAWS.bend against main.bend; prints "All terms check." +$BEND main.bend # checks the model and runs the trace above +$BEND main.bend -o out.js # JavaScript target; node out.js +$BEND main.bend -o out # native binary via clang; ./out +``` + +## 4. Results + +`bend PROOF.bend` prints `All terms check.` in 0.30 s wall time. The +JavaScript build is 26 KB and the native binary 1.1 MB; both run the +trace and print the output in section 1. + +### Mutation tests + +Six bugs were introduced into `main.bend` one at a time, the checker was +run, and the file restored (it is byte-identical to the committed +version). Every mutation is rejected. The table gives the first error +the checker reports; where that is a proof whose shape broke rather +than the law that became false, the false law is named too. + +| # | Bug injected | First failure reported | Law that is false | +| --- | --- | --- | --- | +| M1 | release past zero answers `ok` instead of throwing (`release.checked`) | `rel_below.fin`: expected `ROk`, observed `RErr` | `release_below_zero_is_error` (and `release_dead_is_error`) | +| M2 | freeing forgets `releaseBytes` (counter not decremented) | `kept_release.new`: `allocated` vs `Nat.sub(allocated, size)` | `inv_kept` (accounting) and `release_to_zero_frees` | +| M3 | `retain` on a freed buffer revives it (no `originalReferenceCount > 0` check) | `kept_retain.live`: the new state is not `Inv` | `inv_kept` (bytes appear without the counter moving) and `retain_dead_is_error` | +| M4 | freeing does not mark the chunk released (`release0` forgotten) | `kept_release.new`: replacement shape differs | `inv_kept` (consistency: `False == is_eq(0n, 0n)`) and `release_to_zero_frees` | +| M5 | `buffer(size)` ignores the limit | `kept_alloc`: the proof passes the limit verdict the model no longer computes | `alloc_over_limit_rejected`; confirmed by adapting `kept_alloc` under the mutation, after which the checker stops at exactly that law (expected `RBuf`, observed `ROom`) | +| M6 | `close()` never reports a leak | `LAWS.close_with_live_buffer_is_error`: expected `ROk`, observed `RErr` | `close_with_live_buffer_is_error` | + +M4 and M5 show the brittleness noted in the research notes: a mutation +that changes the shape of a state breaks the proofs that spell out that +shape before the checker reaches the law that is false. Both readings +block the build, which is what `LAWS.bend` promises; telling them apart +is left to the reader of the error. + +### What the model says about the Java + +Writing the laws against the code surfaced three details of +`BufferLedger` worth knowing. None is a bug in normal use, and the Java +was not changed. + +1. `BufferLedger.retain(int)` does not call `allocator.assertOpen()`; + `release` and `newArrowBuf` do. The model's `closed_rejects` law is + therefore stricter than the code for `retain`: after a failed + `close()` (which sets `isClosed` before throwing), Java still accepts + `retain` on the leaked buffers, and rejects `release`. +2. `retain(int)` does `getAndAdd(increment)` and then + `checkArgument(originalReferenceCount > 0)`, so a retain on a ledger + whose count is 0 bumps the count and then throws. `release(int)` + likewise does `addAndGet(-decrement)` and then + `checkState(refCnt >= 0)`. The model states the intended contract, + that a failed call leaves the state unchanged; the Java mutates and + throws. The affected ledger is already dissociated from its + `AllocationManager` (count 0 means `release(this)` ran), so the + difference is not observable through a live buffer. +3. `BaseAllocator.close()` sets `isClosed = true` before it checks for + leaks, so a leaked buffer can never be released once its allocator's + `close()` has thrown (with assertions on). The model reproduces this + (`close` marks the allocator closed either way), and the sample trace + in `main` shows it. + +## 5. Limitations + +- Sizes and counts are `Nat`. The `long` overflow branch of + `Accountant.allocate` and any `int` wraparound of `bufRefCnt` are + outside the model. +- One allocator, one ledger per chunk. Ownership transfer, shared + ownership through `retain(ArrowBuf, BufferAllocator)`, the owning-ledger + hand-off in `AllocationManager.release`, child allocators and + reservations are follow-up models. +- Proofs are hand-written: about 2.4 lines of proof per line of model, + most of it a lemma library that Base does not ship (`Nat.add` + commutativity and associativity, `(a + b) - b == a`, cancellation, + `<`/`<=` facts, and the lookup/replace lemmas over the allocation + list). +- The checker is `bend.ts`, not the Lean formalisation, and Bend 2 is + days old; treat the result as specification work, not as a + verification of `memory-core`. diff --git a/dev/bend2/buffer_refcount/main.bend b/dev/bend2/buffer_refcount/main.bend new file mode 100644 index 0000000000..060951811e --- /dev/null +++ b/dev/bend2/buffer_refcount/main.bend @@ -0,0 +1,419 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. + +# A model of reference counting and allocator accounting in the +# arrow-java memory module (ArrowBuf, ReferenceManager / BufferLedger, +# AllocationManager, BufferAllocator / BaseAllocator / Accountant), +# written in Bend 2 so that its laws can be stated and proven. +# +# One allocator owns a list of allocations. An allocation is one +# AllocationManager with its owning BufferLedger: an id (the ArrowBuf +# handle), the chunk size, the ledger's reference count and whether the +# chunk has been released (release0 was called). The allocator keeps the +# Accountant's counters: allocated bytes, the limit, and whether it has +# been closed. Sizes and counts are Nat; Java's long/int are unbounded +# here. +# +# bend main.bend # checks the model and runs the sample trace in main +# bend PROOF.bend # checks LAWS.bend against this model + +import Base + +# Requests and responses +# ---------------------- + +# one call against the allocator or one of its buffers +type Req is Data: + RAlloc{size: Nat} # BufferAllocator.buffer(size) + RRetain{id: Nat, n: Nat} # buf.getReferenceManager().retain(n) + RRelease{id: Nat, n: Nat} # buf.getReferenceManager().release(n); release() is n = 1 + RClose{} # BufferAllocator.close() + +# the outcome of a call +type Resp is Data: + RBuf{id: Nat} # buffer(size): a new ArrowBuf, named by its allocation id + REmpty{} # buffer(0): the shared empty buffer, not accounted + ROk{} # retain(n), release(n) that keeps the memory (false), close() + RFreed{} # release(n) that dropped the count to 0 (true): memory released + ROom{} # OutOfMemoryException: the request exceeds the limit + RErr{} # IllegalStateException / IllegalArgumentException + +# State +# ----- + +# one AllocationManager and its owning BufferLedger +type Alloc is Data: + Alloc{id: Nat, size: Nat, refs: Nat, freed: Bool} + +# one BaseAllocator: its allocations and its Accountant +type Allocator is Data: + Allocator{allocs: List<&2, Alloc>, allocated: Nat, limit: Nat, next: Nat, closed: Bool} + +def Alloc.id(a: Alloc) -> Nat: + Alloc{id, size, refs, freed} = a + id + +def Alloc.size(a: Alloc) -> Nat: + Alloc{id, size, refs, freed} = a + size + +def Alloc.refs(a: Alloc) -> Nat: + Alloc{id, size, refs, freed} = a + refs + +def Alloc.freed(a: Alloc) -> Bool: + Alloc{id, size, refs, freed} = a + freed + +# the bytes an allocation accounts for: its size while live, 0 once freed +def bytes.of(freed: Bool, size: Nat) -> Nat: + match freed: + case True{}: + 0n + case False{}: + size + +def bytes(a: Alloc) -> Nat: + Alloc{id, size, refs, freed} = a + bytes.of(freed, size) + +# the bytes the allocator should be accounting for +def live_bytes(xs: List<&2, Alloc>) -> Nat: + match xs: + case Nil{}: + 0n + case Con{a, t}: + Nat.add(bytes(a), live_bytes(t)) + +# whether any allocation is still live (an outstanding buffer) +def has_live(xs: List<&2, Alloc>) -> Bool: + match xs: + case Nil{}: + False{} + case Con{a, t}: + Bool.not(Alloc.freed(a)) || has_live(t) + +# List helpers +# ------------ + +# the first allocation with the given id +def lookup.at(a: Alloc, rec: Maybe<&2, Alloc>, hit: Bool) -> Maybe<&2, Alloc>: + match hit: + case True{}: + Some{a} + case False{}: + rec + +def lookup(+id: Nat, xs: List<&2, Alloc>) -> Maybe<&2, Alloc>: + match xs: + case Nil{}: + None{} + case Con{+a, t}: + lookup.at(a, lookup(id, t), Nat.is_eq(Alloc.id(a), id)) + +# xs with the first allocation of the given id replaced by a2 +def replace.at(a: Alloc, a2: Alloc, t: List<&2, Alloc>, rec: List<&2, Alloc>, hit: Bool) -> List<&2, Alloc>: + match hit: + case True{}: + a2 <> t + case False{}: + a <> rec + +def replace(+id: Nat, +a2: Alloc, xs: List<&2, Alloc>) -> List<&2, Alloc>: + match xs: + case Nil{}: + Nil{} + case Con{+a, +t}: + replace.at(a, a2, t, replace(id, a2, t), Nat.is_eq(Alloc.id(a), id)) + +# Observations of a lookup +# ------------------------ + +def refs_of.m(m: Maybe<&2, Alloc>) -> Nat: + match m: + case None{}: + 0n + case Some{a}: + Alloc.refs(a) + +def size_of.m(m: Maybe<&2, Alloc>) -> Nat: + match m: + case None{}: + 0n + case Some{a}: + Alloc.size(a) + +def is_live.m(m: Maybe<&2, Alloc>) -> Bool: + match m: + case None{}: + False{} + case Some{a}: + Bool.not(Alloc.freed(a)) + +def is_freed.m(m: Maybe<&2, Alloc>) -> Bool: + match m: + case None{}: + False{} + case Some{a}: + Alloc.freed(a) + +# the reference count of the buffer with the given id (0 if unknown) +def refs_of(+id: Nat, xs: List<&2, Alloc>) -> Nat: + refs_of.m(lookup(id, xs)) + +# the size of the buffer with the given id (0 if unknown) +def size_of(+id: Nat, xs: List<&2, Alloc>) -> Nat: + size_of.m(lookup(id, xs)) + +# whether the id names an allocation whose memory is still held +def is_live(+id: Nat, xs: List<&2, Alloc>) -> Bool: + is_live.m(lookup(id, xs)) + +# whether the id names an allocation whose memory was released +def is_freed(+id: Nat, xs: List<&2, Alloc>) -> Bool: + is_freed.m(lookup(id, xs)) + +# Transitions +# ----------- + +# the state with nothing changed +def same(+allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, closed: Bool) -> Allocator: + Allocator{allocs, allocated, limit, next, closed} + +# buffer(size), once the request is known to fit (Accountant.allocate: +# newLocal > allocationLimit fails): a new AllocationManager, its ledger +# associated with a count of 1, and the bytes added to the accountant +def alloc.fits(+size: Nat, +allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, ok: Bool) -> Allocator & Resp: + match ok: + case True{}: + (Allocator{Alloc{next, size, 1n, False{}} <> allocs, Nat.add(allocated, size), limit, 1n+next, False{}}, RBuf{next}) + case False{}: + (same(allocs, allocated, limit, next, False{}), ROom{}) + +# buffer(size): size 0 answers the shared empty buffer and accounts nothing +def alloc(size: Nat, +allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Allocator & Resp: + match size: + case 0n: + (same(allocs, allocated, limit, next, False{}), REmpty{}) + case 1n+p: + +size2 = {1n+p : Nat} + alloc.fits(size2, allocs, allocated, limit, next, Nat.is_le(Nat.add(allocated, size2), limit)) + +# retain(n) on a found ledger: checkArgument(originalReferenceCount > 0) +def retain.live(+id: Nat, +n: Nat, +size: Nat, refs: Nat, freed: Bool, +allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Allocator & Resp: + match refs: + case 0n: + (same(allocs, allocated, limit, next, False{}), RErr{}) + case 1n+q: + (Allocator{replace(id, Alloc{id, size, Nat.add(1n+q, n), freed}, allocs), allocated, limit, next, False{}}, ROk{}) + +def retain.found(+id: Nat, +n: Nat, m: Maybe<&2, Alloc>, +allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Allocator & Resp: + match m: + case None{}: + (same(allocs, allocated, limit, next, False{}), RErr{}) + case Some{Alloc{aid, +size, refs, freed}}: + retain.live(id, n, size, refs, freed, allocs, allocated, limit, next) + +# retain(n): checkArgument(increment > 0), then bump the ledger's count +def retain(+id: Nat, n: Nat, +allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Allocator & Resp: + match n: + case 0n: + (same(allocs, allocated, limit, next, False{}), RErr{}) + case 1n+m: + retain.found(id, 1n+m, lookup(id, allocs), allocs, allocated, limit, next) + +# release(n) after the decrement: a count of 0 releases the chunk +# (AllocationManager.release: releaseBytes(getSize()); release0()), +# any other count keeps it +def release.new(+id: Nat, +size: Nat, refs2: Nat, freed: Bool, +allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Allocator & Resp: + match refs2: + case 0n: + (Allocator{replace(id, Alloc{id, size, 0n, True{}}, allocs), Nat.sub(allocated, size), limit, next, False{}}, RFreed{}) + case 1n+q: + (Allocator{replace(id, Alloc{id, size, 1n+q, freed}, allocs), allocated, limit, next, False{}}, ROk{}) + +# release(n) on a found ledger: checkState(refCnt >= 0, "RefCnt has gone negative") +def release.checked(+id: Nat, +n: Nat, +size: Nat, +refs: Nat, freed: Bool, +allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, negative: Bool) -> Allocator & Resp: + match negative: + case True{}: + (same(allocs, allocated, limit, next, False{}), RErr{}) + case False{}: + release.new(id, size, Nat.sub(refs, n), freed, allocs, allocated, limit, next) + +def release.found(+id: Nat, +n: Nat, m: Maybe<&2, Alloc>, +allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Allocator & Resp: + match m: + case None{}: + (same(allocs, allocated, limit, next, False{}), RErr{}) + case Some{Alloc{aid, +size, +refs, freed}}: + release.checked(id, n, size, refs, freed, allocs, allocated, limit, next, Nat.is_lt(refs, n)) + +# release(n): checkState(decrement >= 1), then decrement the ledger's count +def release(+id: Nat, n: Nat, +allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Allocator & Resp: + match n: + case 0n: + (same(allocs, allocated, limit, next, False{}), RErr{}) + case 1n+m: + release.found(id, 1n+m, lookup(id, allocs), allocs, allocated, limit, next) + +# close(): the allocator is closed either way (isClosed = true comes +# first), and outstanding buffers make it an error ("Memory was leaked") +def close(+allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, leak: Bool) -> Allocator & Resp: + match leak: + case True{}: + (same(allocs, allocated, limit, next, True{}), RErr{}) + case False{}: + (same(allocs, allocated, limit, next, True{}), ROk{}) + +# a request against an open allocator +def step_open(r: Req, +allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Allocator & Resp: + match r: + case RAlloc{size}: + alloc(size, allocs, allocated, limit, next) + case RRetain{+id, n}: + retain(id, n, allocs, allocated, limit, next) + case RRelease{+id, n}: + release(id, n, allocs, allocated, limit, next) + case RClose{}: + close(allocs, allocated, limit, next, has_live(allocs)) + +# a request against a closed allocator: assertOpen() throws, except +# that a second close() is a no-op +def step_closed(r: Req, +allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat) -> Allocator & Resp: + match r: + case RAlloc{size}: + (same(allocs, allocated, limit, next, True{}), RErr{}) + case RRetain{id, n}: + (same(allocs, allocated, limit, next, True{}), RErr{}) + case RRelease{id, n}: + (same(allocs, allocated, limit, next, True{}), RErr{}) + case RClose{}: + (same(allocs, allocated, limit, next, True{}), ROk{}) + +# whether a request is close() +def is_close(r: Req) -> Bool: + match r: + case RAlloc{size}: + False{} + case RRetain{id, n}: + False{} + case RRelease{id, n}: + False{} + case RClose{}: + True{} + +# one request against one state +def step(r: Req, +allocs: List<&2, Alloc>, +allocated: Nat, +limit: Nat, +next: Nat, closed: Bool) -> Allocator & Resp: + match closed: + case True{}: + step_closed(r, allocs, allocated, limit, next) + case False{}: + step_open(r, allocs, allocated, limit, next) + +# projections of a step +def state(sr: Allocator & Resp) -> Allocator: + (s, r) = sr + s + +def resp(sr: Allocator & Resp) -> Resp: + (s, r) = sr + r + +def allocs_of(s: Allocator) -> List<&2, Alloc>: + Allocator{allocs, allocated, limit, next, closed} = s + allocs + +def allocated_of(s: Allocator) -> Nat: + Allocator{allocs, allocated, limit, next, closed} = s + allocated + +def closed_of(s: Allocator) -> Bool: + Allocator{allocs, allocated, limit, next, closed} = s + closed + +# a request against a whole allocator +def step_s(r: Req, s: Allocator) -> Allocator & Resp: + Allocator{allocs, allocated, limit, next, closed} = s + step(r, allocs, allocated, limit, next, closed) + +# new RootAllocator(limit) +def start(limit: Nat) -> Allocator: + Allocator{Nil{}, 0n, limit, 0n, False{}} + +# a whole trace, threading the state and the last response +def run(reqs: List, sr: Allocator & Resp) -> Allocator & Resp: + match reqs: + case Nil{}: + sr + case Con{r, rest}: + (s, last) = sr + run(rest, step_s(r, s)) + +def replay(reqs: List, limit: Nat) -> Allocator & Resp: + run(reqs, (start(limit), ROk{})) + +# Show +# ---- + +def Req.show(r: Req) -> String: + match r: + case RAlloc{size}: + "buffer(" ++ Nat.show(size) ++ ")" + case RRetain{id, n}: + "buf" ++ Nat.show(id) ++ ".retain(" ++ Nat.show(n) ++ ")" + case RRelease{id, n}: + "buf" ++ Nat.show(id) ++ ".release(" ++ Nat.show(n) ++ ")" + case RClose{}: + "close()" + +def Resp.show(r: Resp) -> String: + match r: + case RBuf{id}: + "buf" ++ Nat.show(id) + case REmpty{}: + "empty buffer" + case ROk{}: + "ok" + case RFreed{}: + "true (memory released)" + case ROom{}: + "OutOfMemoryException" + case RErr{}: + "IllegalStateException" + +def Allocator.show(s: Allocator) -> String: + Allocator{allocs, allocated, limit, next, closed} = s + "allocated=" ++ Nat.show(allocated) ++ "/" ++ Nat.show(limit) ++ " live_bytes=" ++ Nat.show(live_bytes(allocs)) ++ " closed=" ++ Bool.show(closed) + +# one line per request, then the final state +def trace.fin(r: Req, sr: Allocator & Resp, rec: Allocator -> String) -> String: + (s, answer) = sr + " " ++ Req.show(r) ++ " -> " ++ Resp.show(answer) ++ "\n" ++ rec(s) + +def trace(reqs: List) -> Allocator -> String: + match reqs: + case Nil{}: + s => " " ++ Allocator.show(s) + case Con{+r, rest}: + s => trace.fin(r, step_s(r, s), trace(rest)) + +# a RootAllocator of 1024 bytes: allocate, share, release twice, over-release, +# allocate past the limit, leak on close, then close cleanly +def main() -> IO(Unit): + IO.print(trace([ + RAlloc{512n}, RRetain{0n, 1n}, RRelease{0n, 1n}, RRelease{0n, 1n}, RRelease{0n, 1n}, + RAlloc{768n}, RAlloc{256n}, RAlloc{768n}, RRelease{1n, 2n}, RClose{}, RRelease{1n, 1n} + ])(start(1024n)))