tiny.reducer.Storage

1/// Workspace, allocated up front and double-buffered, that carries reduction in2/// steady state. It holds the backing allocation and tracks the phase it is in3/// and whether a lease is out.4pub const Storage = struct {5    /// Lifecycle phase that `alloc_phase` enforces.6    phase: alloc_phase.capacity.Phase,78    /// Layout derived while initializing.9    capacity: capacity_mod.Capacity,1011    /// Entire contiguous backing byte allocation.12    bytes: []u8,1314    /// Fixed sub-slice reserved for the witness lane, spanning $0 \dots N$.15    current: []u8,1617    /// Fixed sub-slice reserved for the scratch lane, spanning18    /// $N \dots N + \max(N - 1, 0)$.19    candidate: []u8,2021    /// Flag recording that a lease is out, turning away a reentrant acquisition22    /// and one made while an earlier result is still live.23    in_use: bool = false,2425    /// Re-export of the capacity limits type.26    pub const Limits: type = capacity_mod.Limits;2728    /// Re-export of the derived capacity type.29    pub const Capacity: type = capacity_mod.Capacity;3031    /// Re-export of the exhaustion error set.32    pub const Exhaustion: type = model.Exhaustion;3334    /// Errors `Storage.init()` may return.35    pub const InitError = std.mem.Allocator.Error || capacity_mod.DeriveError;3637    /// Stardust capacity declaration that phase-directed allocation38    /// verification reads. It records that the workspace owner makes no further39    /// backing allocation once sealed into steady state. It bounds the storage40    /// by $2 \times \text{max\_input\_bytes}$. It leaves out the memory and the41    /// effects the caller's predicate owns.42    pub const claim: alloc_phase.capacity.Declaration = .{43        .source = .{44            .id = "reducer.byte_storage",45            .kind = .phase_static,46            .limit_source = .caller,47            .storage = .{48                .covered = &.{49                    .{50                        .id = "accepted_input_and_borrowed_result_bytes",51                        .lifetime = .steady,52                        .detail = "accepted input and borrowed result bytes",53                    },54                    .{55                        .id = "deletion_candidate_scratch_bytes",56                        .lifetime = .steady,57                        .detail = "deletion candidate scratch bytes",58                    },59                },60                .excluded = &.{61                    "caller-owned initial input bytes",62                    "caller-owned predicate context, allocation, and effects",63                },64            },65            .capacity = .{66                .inputs = &.{67                    alloc_phase.capacity.bindInput(Limits, "max_input_bytes", "max_input_bytes"),68                },69                .type_selectors = &.{},70                .nodes = &.{71                    .{ .input = 0 },72                    .{ .scale = .{ .node = 0, .coefficient = .{ .literal = 2 } } },73                },74                .assertions = &.{.{75                    .scope = .closure_total,76                    .measure = .retained,77                    .relation = .upper_bound,78                    .expression = 1,79                }},80            },81            .overload = .{82                .kind = .reject_before_mutation,83                .detail = "oversize and concurrent requests fail before workspace bytes change",84            },85            .risks = .{86                .transitive = .{87                    .status = .witnessed,88                    .detail = "reduction uses byte lanes; predicate effects remain caller-owned",89                },90                .foreign = .{91                    .status = .excluded,92                    .detail = "predicate and operating-system effects are caller-owned",93                },94            },95            .obligations = &.{96                .{ .key = "reducer_byte_capacity", .role = .capacity_model },97                .{ .key = "reducer_byte_acquisition", .role = .custom },98                .{ .key = "reducer_byte_oom", .role = .custom },99                .{ .key = "reducer_byte_boundaries", .role = .overload },100                .{ .key = "reducer_byte_reuse", .role = .overload },101                .{ .key = "reducer_byte_sealed", .role = .transitive_risk },102                .{ .key = "reducer_byte_callback", .role = .foreign_risk },103                .{ .key = "reducer_byte_root", .role = .custom },104            },105        },106        .bindings = .{107            .owner = @This(),108            .seal = .{109                .family = alloc_phase.capacity.selector(@This().activate),110                .premise = .{111                    .class = .checked_semantic_fact,112                    .authority = .checker,113                },114            },115            .teardown = .{116                .family = alloc_phase.capacity.selector(@This().deinit),117                .premise = .{118                    .class = .checked_semantic_fact,119                    .authority = .checker,120                },121            },122        },123    };124125    /// Allocates a reduction workspace and divides it into the two lanes, sized126    /// for inputs up to `limits.max_input_bytes`. The new workspace is in127    /// `.initialization`, and the caller calls `storage.activate()` on it128    /// before passing it to `reduce()`. A workspace that is never activated can129    /// be freed directly by `storage.deinit()`.130    ///131    /// ## Errors132    /// - `error.CapacityOverflow` when $N + \max(N - 1, 0)$ overflows `usize`.133    /// - `error.OutOfMemory` when the allocator declines the request.134    pub fn init(allocator: std.mem.Allocator, limits: Limits) InitError!Storage {135        const capacity = try Capacity.derive(limits);136        const bytes = try allocator.alloc(u8, capacity.storage_bytes);137        const owner = Storage{138            .phase = .initialization,139            .capacity = capacity,140            .bytes = bytes,141            .current = bytes[0..limits.max_input_bytes],142            .candidate = bytes[capacity.candidate_offset..][0..capacity.candidate_bytes],143        };144        std.debug.assert(owner.current.len == limits.max_input_bytes);145        std.debug.assert(owner.candidate.len == capacity.candidate_bytes);146        std.debug.assert(owner.current.len + owner.candidate.len == owner.bytes.len);147        return owner;148    }149150    /// Moves the workspace from `.initialization` to `.steady`. Once it151    /// returns, the workspace owner makes no further heap allocation.152    ///153    /// ## Preconditions154    /// - `self.phase` is `.initialization`.155    /// - The backing allocation's length equals `self.capacity.storage_bytes`.156    pub fn activate(self: *Storage) void {157        std.debug.assert(self.phase == .initialization);158        std.debug.assert(self.bytes.len == self.capacity.storage_bytes);159        self.phase = .steady;160    }161162    /// Takes exclusive use of the workspace for a run over `input_bytes` bytes.163    /// It returns `Regions` holding sub-slices of the backing buffer. It copies164    /// nothing into `Regions.current`.165    ///166    /// ## Preconditions167    /// - `self.phase` is `.steady`.168    ///169    /// ## Errors170    /// - `error.ReductionStorageInUse` when `self.in_use` is already true. A171    ///   reentrant call, and a call made while an earlier result is still live,172    ///   are both turned away without disturbing the hold that is already out.173    /// - `error.InputCapacityExceeded` when `input_bytes` exceeds174    ///   `max_input_bytes`.175    pub fn acquire(self: *Storage, input_bytes: usize) Exhaustion!Regions {176        std.debug.assert(self.phase == .steady);177        if (self.in_use) return error.ReductionStorageInUse;178        if (input_bytes > self.capacity.limits.max_input_bytes) {179            return error.InputCapacityExceeded;180        }181        std.debug.assert(self.current.len == self.capacity.limits.max_input_bytes);182        std.debug.assert(self.candidate.len == self.capacity.candidate_bytes);183        self.in_use = true;184        return .{185            .current = self.current[0..input_bytes],186            .candidate = self.candidate,187        };188    }189190    /// Gives up this run's lease, returning the workspace to steady and idle so191    /// it can serve another run. `Result.deinit()` calls it, and it moves the192    /// workspace no closer to teardown.193    ///194    /// ## Preconditions195    /// - `self.phase` is `.steady`.196    /// - `self.in_use` is true.197    pub fn release(self: *Storage) void {198        std.debug.assert(self.phase == .steady);199        std.debug.assert(self.in_use);200        self.in_use = false;201        std.debug.assert(!self.in_use);202    }203204    /// Returns a snapshot of this workspace, taken by value at the moment of205    /// the call.206    pub fn status(self: *const Storage) Status {207        return .{208            .phase = self.phase,209            .in_use = self.in_use,210            .storage_bytes = self.capacity.storage_bytes,211            .max_input_bytes = self.capacity.limits.max_input_bytes,212        };213    }214215    /// Frees the backing allocation and moves the workspace to `.teardown`. It216    /// works on an idle steady workspace and on one still in `.initialization`217    /// that was never activated. It needs the same allocator `Storage.init()`218    /// received.219    ///220    /// ## Preconditions221    /// - `self.phase` is anything other than `.teardown`.222    /// - `self.in_use` is false, so every result has had its `deinit()` called.223    pub fn deinit(self: *Storage, allocator: std.mem.Allocator) void {224        std.debug.assert(self.phase != .teardown);225        std.debug.assert(!self.in_use);226        std.debug.assert(self.bytes.len == self.capacity.storage_bytes);227        self.phase = .teardown;228        allocator.free(self.bytes);229        self.bytes = &.{};230        self.current = &.{};231        self.candidate = &.{};232    }233};

1/// Workspace, allocated up front and double-buffered, that carries reduction in2/// steady state.3pub const Storage = bytes.Storage;