tiny.reducer.bytes.storage

1/// Module holding the workspace, allocated up front and double-buffered, and2/// the phase-checked lifecycle around it.3pub const storage = @import("storage.zig");

1//! `Storage` holds the backing memory a byte reduction run needs, allocated2//! once up front and reused for every run: the *workspace*. The `alloc_phase`3//! checker tracks the phase and establishes that the owner makes no further4//! backing allocation once the workspace is activated into steady state.5//!6//! ## Workspace Lifecycle7//!8//! | Operation | Effect / Transition |9//! | :--- | :--- |10//! | `storage.activate()` | Moves `initialization` to `steady (idle)` |11//! | `storage.acquire(bytes)` | Leases `steady (idle)` to `steady (acquired)` |12//! | `result.deinit()` / `storage.release()` | Releases `steady (acquired)` back to `steady (idle)` |13//! | `storage.deinit(allocator)` (unactivated) | Frees unactivated `initialization` to `teardown` |14//! | `storage.deinit(allocator)` (idle) | Frees idle `steady` to `teardown` (invalid while acquired) |15//!16//! 1. **Initialization (`Phase.initialization`)**: `Storage.init()` derives the17//!    layout, which comes to $N + \max(N - 1, 0)$ bytes (its *capacity*), and18//!    allocates the backing buffer once. The instance starts out with19//!    `phase = .initialization`. A workspace that is never activated can be20//!    freed straight away by `storage.deinit(allocator)`, using the allocator21//!    `init()` received. Filling in `Storage` fields by hand is unsafe, so22//!    callers reach a valid workspace through `init()`.23//! 2. **Activation (`Phase.steady`)**: the caller calls `storage.activate()`,24//!    which seals the initialization phase and moves the workspace to steady25//!    and idle. In steady state the workspace owner allocates nothing further.26//! 3. **Acquisition (`in_use = true`)**: inside `reduce()`,27//!    `storage.acquire(input_bytes)` checks that the workspace is in steady28//!    phase, checks that no lease is out, and checks that `input_bytes` is29//!    within `max_input_bytes`. It sets `in_use = true` and returns the two30//!    byte lanes as `Regions`, returning slices, copying nothing into the31//!    witness lane and initializing nothing. An oversized input returns32//!    `error.InputCapacityExceeded`, and a request made while a lease is out33//!    returns `error.ReductionStorageInUse`, both before any workspace byte34//!    changes.35//! 4. **Release and reuse (`in_use = false`)**: when a run finishes,36//!    `Result.deinit()`, or `storage.release()`, clears `in_use`. The workspace37//!    returns to steady and idle, and a later run can acquire it with no38//!    further allocation.39//! 5. **Teardown (`Phase.teardown`)**: `storage.deinit(allocator)` checks that40//!    no lease is out, sets `phase = .teardown`, and frees the backing buffer41//!    with the same allocator `init()` received.42//!43//! ## Ownership and Concurrency Constraints44//! - `Storage` offers no thread safety. `in_use` is a plain boolean that turns45//!   away a second use on one thread, so reaching one workspace from multiple46//!   threads at once is the caller's to synchronize.47//! - Zig checks no linear or affine type at compile time, and a runtime check48//!   catches no shallow copy of a `Storage` or a `Result`, so one owner holds49//!   each of them, makes no shallow duplicate, and leaves the bookkeeping50//!   fields alone.51//! - The capacity claim `reducer.byte_storage` covers the two internal byte52//!   lanes. It leaves out the caller's own initial input bytes, the predicate's53//!   context, and every allocation and foreign side effect the callback54//!   performs.5556const std = @import("std");57const alloc_phase = @import("alloc_phase");58const capacity_mod = @import("capacity.zig");59const model = @import("model.zig");6061/// Pair of memory lane slices `Storage.acquire()` returns. `acquire()` copies62/// nothing into these slices and initializes nothing in them: they are63/// sub-slices of the backing allocation.64pub const Regions = struct {65    /// Slice of the witness lane sized to this run's `input_bytes`.66    current: []u8,6768    /// Scratch lane, whose length is `candidate_bytes`, which is69    /// $\max(N - 1, 0)$.70    candidate: []u8,71};7273/// Snapshot of one workspace's state, taken by value at the moment of the call.74pub const Status = struct {75    /// Workspace current phase, one of `.initialization`, `.steady`, or76    /// `.teardown`.77    phase: alloc_phase.capacity.Phase,7879    /// Flag recording whether a running reduction or a `Result` whose80    /// `deinit()` has yet to be called currently holds the workspace.81    in_use: bool,8283    /// Derived capacity the workspace was configured for, which is84    /// $N + \max(N - 1, 0)$ bytes. The figure is a record of the configured85    /// size, and it stays recorded after teardown.86    storage_bytes: usize,8788    /// Longest input in bytes this workspace serves, which is $N$.89    max_input_bytes: usize,90};9192/// Workspace, allocated up front and double-buffered, that carries reduction in93/// steady state. It holds the backing allocation and tracks the phase it is in94/// and whether a lease is out.95pub const Storage = struct {96    /// Lifecycle phase that `alloc_phase` enforces.97    phase: alloc_phase.capacity.Phase,9899    /// Layout derived while initializing.100    capacity: capacity_mod.Capacity,101102    /// Entire contiguous backing byte allocation.103    bytes: []u8,104105    /// Fixed sub-slice reserved for the witness lane, spanning $0 \dots N$.106    current: []u8,107108    /// Fixed sub-slice reserved for the scratch lane, spanning109    /// $N \dots N + \max(N - 1, 0)$.110    candidate: []u8,111112    /// Flag recording that a lease is out, turning away a reentrant acquisition113    /// and one made while an earlier result is still live.114    in_use: bool = false,115116    /// Re-export of the capacity limits type.117    pub const Limits: type = capacity_mod.Limits;118119    /// Re-export of the derived capacity type.120    pub const Capacity: type = capacity_mod.Capacity;121122    /// Re-export of the exhaustion error set.123    pub const Exhaustion: type = model.Exhaustion;124125    /// Errors `Storage.init()` may return.126    pub const InitError = std.mem.Allocator.Error || capacity_mod.DeriveError;127128    /// Stardust capacity declaration that phase-directed allocation129    /// verification reads. It records that the workspace owner makes no further130    /// backing allocation once sealed into steady state. It bounds the storage131    /// by $2 \times \text{max\_input\_bytes}$. It leaves out the memory and the132    /// effects the caller's predicate owns.133    pub const claim: alloc_phase.capacity.Declaration = .{134        .source = .{135            .id = "reducer.byte_storage",136            .kind = .phase_static,137            .limit_source = .caller,138            .storage = .{139                .covered = &.{140                    .{141                        .id = "accepted_input_and_borrowed_result_bytes",142                        .lifetime = .steady,143                        .detail = "accepted input and borrowed result bytes",144                    },145                    .{146                        .id = "deletion_candidate_scratch_bytes",147                        .lifetime = .steady,148                        .detail = "deletion candidate scratch bytes",149                    },150                },151                .excluded = &.{152                    "caller-owned initial input bytes",153                    "caller-owned predicate context, allocation, and effects",154                },155            },156            .capacity = .{157                .inputs = &.{158                    alloc_phase.capacity.bindInput(Limits, "max_input_bytes", "max_input_bytes"),159                },160                .type_selectors = &.{},161                .nodes = &.{162                    .{ .input = 0 },163                    .{ .scale = .{ .node = 0, .coefficient = .{ .literal = 2 } } },164                },165                .assertions = &.{.{166                    .scope = .closure_total,167                    .measure = .retained,168                    .relation = .upper_bound,169                    .expression = 1,170                }},171            },172            .overload = .{173                .kind = .reject_before_mutation,174                .detail = "oversize and concurrent requests fail before workspace bytes change",175            },176            .risks = .{177                .transitive = .{178                    .status = .witnessed,179                    .detail = "reduction uses byte lanes; predicate effects remain caller-owned",180                },181                .foreign = .{182                    .status = .excluded,183                    .detail = "predicate and operating-system effects are caller-owned",184                },185            },186            .obligations = &.{187                .{ .key = "reducer_byte_capacity", .role = .capacity_model },188                .{ .key = "reducer_byte_acquisition", .role = .custom },189                .{ .key = "reducer_byte_oom", .role = .custom },190                .{ .key = "reducer_byte_boundaries", .role = .overload },191                .{ .key = "reducer_byte_reuse", .role = .overload },192                .{ .key = "reducer_byte_sealed", .role = .transitive_risk },193                .{ .key = "reducer_byte_callback", .role = .foreign_risk },194                .{ .key = "reducer_byte_root", .role = .custom },195            },196        },197        .bindings = .{198            .owner = @This(),199            .seal = .{200                .family = alloc_phase.capacity.selector(@This().activate),201                .premise = .{202                    .class = .checked_semantic_fact,203                    .authority = .checker,204                },205            },206            .teardown = .{207                .family = alloc_phase.capacity.selector(@This().deinit),208                .premise = .{209                    .class = .checked_semantic_fact,210                    .authority = .checker,211                },212            },213        },214    };215216    /// Allocates a reduction workspace and divides it into the two lanes, sized217    /// for inputs up to `limits.max_input_bytes`. The new workspace is in218    /// `.initialization`, and the caller calls `storage.activate()` on it219    /// before passing it to `reduce()`. A workspace that is never activated can220    /// be freed directly by `storage.deinit()`.221    ///222    /// ## Errors223    /// - `error.CapacityOverflow` when $N + \max(N - 1, 0)$ overflows `usize`.224    /// - `error.OutOfMemory` when the allocator declines the request.225    pub fn init(allocator: std.mem.Allocator, limits: Limits) InitError!Storage {226        const capacity = try Capacity.derive(limits);227        const bytes = try allocator.alloc(u8, capacity.storage_bytes);228        const owner = Storage{229            .phase = .initialization,230            .capacity = capacity,231            .bytes = bytes,232            .current = bytes[0..limits.max_input_bytes],233            .candidate = bytes[capacity.candidate_offset..][0..capacity.candidate_bytes],234        };235        std.debug.assert(owner.current.len == limits.max_input_bytes);236        std.debug.assert(owner.candidate.len == capacity.candidate_bytes);237        std.debug.assert(owner.current.len + owner.candidate.len == owner.bytes.len);238        return owner;239    }240241    /// Moves the workspace from `.initialization` to `.steady`. Once it242    /// returns, the workspace owner makes no further heap allocation.243    ///244    /// ## Preconditions245    /// - `self.phase` is `.initialization`.246    /// - The backing allocation's length equals `self.capacity.storage_bytes`.247    pub fn activate(self: *Storage) void {248        std.debug.assert(self.phase == .initialization);249        std.debug.assert(self.bytes.len == self.capacity.storage_bytes);250        self.phase = .steady;251    }252253    /// Takes exclusive use of the workspace for a run over `input_bytes` bytes.254    /// It returns `Regions` holding sub-slices of the backing buffer. It copies255    /// nothing into `Regions.current`.256    ///257    /// ## Preconditions258    /// - `self.phase` is `.steady`.259    ///260    /// ## Errors261    /// - `error.ReductionStorageInUse` when `self.in_use` is already true. A262    ///   reentrant call, and a call made while an earlier result is still live,263    ///   are both turned away without disturbing the hold that is already out.264    /// - `error.InputCapacityExceeded` when `input_bytes` exceeds265    ///   `max_input_bytes`.266    pub fn acquire(self: *Storage, input_bytes: usize) Exhaustion!Regions {267        std.debug.assert(self.phase == .steady);268        if (self.in_use) return error.ReductionStorageInUse;269        if (input_bytes > self.capacity.limits.max_input_bytes) {270            return error.InputCapacityExceeded;271        }272        std.debug.assert(self.current.len == self.capacity.limits.max_input_bytes);273        std.debug.assert(self.candidate.len == self.capacity.candidate_bytes);274        self.in_use = true;275        return .{276            .current = self.current[0..input_bytes],277            .candidate = self.candidate,278        };279    }280281    /// Gives up this run's lease, returning the workspace to steady and idle so282    /// it can serve another run. `Result.deinit()` calls it, and it moves the283    /// workspace no closer to teardown.284    ///285    /// ## Preconditions286    /// - `self.phase` is `.steady`.287    /// - `self.in_use` is true.288    pub fn release(self: *Storage) void {289        std.debug.assert(self.phase == .steady);290        std.debug.assert(self.in_use);291        self.in_use = false;292        std.debug.assert(!self.in_use);293    }294295    /// Returns a snapshot of this workspace, taken by value at the moment of296    /// the call.297    pub fn status(self: *const Storage) Status {298        return .{299            .phase = self.phase,300            .in_use = self.in_use,301            .storage_bytes = self.capacity.storage_bytes,302            .max_input_bytes = self.capacity.limits.max_input_bytes,303        };304    }305306    /// Frees the backing allocation and moves the workspace to `.teardown`. It307    /// works on an idle steady workspace and on one still in `.initialization`308    /// that was never activated. It needs the same allocator `Storage.init()`309    /// received.310    ///311    /// ## Preconditions312    /// - `self.phase` is anything other than `.teardown`.313    /// - `self.in_use` is false, so every result has had its `deinit()` called.314    pub fn deinit(self: *Storage, allocator: std.mem.Allocator) void {315        std.debug.assert(self.phase != .teardown);316        std.debug.assert(!self.in_use);317        std.debug.assert(self.bytes.len == self.capacity.storage_bytes);318        self.phase = .teardown;319        allocator.free(self.bytes);320        self.bytes = &.{};321        self.current = &.{};322        self.candidate = &.{};323    }324};325326fn checkInitFailures(allocator: std.mem.Allocator) !void {327    var storage = try Storage.init(allocator, .{ .max_input_bytes = 9 });328    storage.deinit(allocator);329}330331test "byte reduction storage acquires one exact region" {332    comptime {333        @stardustClaim(334            @import("alloc_phase").capacity.witness(Storage, "reducer_byte_acquisition"),335            null,336            null,337            null,338            null,339            null,340            null,341        );342    }343344    var counting = std.testing.FailingAllocator.init(std.testing.allocator, .{});345    const limits = capacity_mod.Limits{ .max_input_bytes = 9 };346    const capacity = try capacity_mod.Capacity.derive(limits);347    var storage = try Storage.init(counting.allocator(), limits);348    defer storage.deinit(counting.allocator());349350    try std.testing.expectEqual(@as(usize, 1), counting.alloc_index);351    try std.testing.expectEqual(capacity.storage_bytes, counting.allocated_bytes);352    try std.testing.expectEqual(alloc_phase.capacity.Phase.initialization, storage.status().phase);353    storage.activate();354    const regions = try storage.acquire(9);355    defer storage.release();356    try std.testing.expectEqual(@intFromPtr(storage.bytes.ptr), @intFromPtr(regions.current.ptr));357    try std.testing.expectEqual(358        @intFromPtr(storage.bytes.ptr) + capacity.candidate_offset,359        @intFromPtr(regions.candidate.ptr),360    );361}362363test "byte reduction storage retries after every allocation failure" {364    comptime {365        @stardustClaim(366            @import("alloc_phase").capacity.witness(Storage, "reducer_byte_oom"),367            null,368            null,369            null,370            null,371            null,372            null,373        );374    }375376    try std.testing.checkAllAllocationFailures(std.testing.allocator, checkInitFailures, .{});377}378379comptime {380    alloc_phase.capacity.requireAllocatorRejectingOwnerShape(Storage);381}