tiny.smt.sat.scratch

1pub const scratch = @import("scratch.zig");

1//! Scratch memory for one conflict analysis at a time: room for the literals of the clause being2//! learned and one mark per variable. The solver analyzes each conflict it meets above decision3//! level zero, and a caller that bounds memory wants that analysis to run in memory set aside4//! before the search starts. The clause learned from one conflict holds at most one literal per5//! variable, and the analysis marks each variable at most once, so the memory one analysis needs6//! grows with the variable count alone. The solver already allocates the list of assigned literals7//! in the order they were assigned (the trail), which holds at most one literal per variable.8//!9//! The scratch (`ConflictScratch`) lives in the trail's allocation, past its first variable-count10//! entries. At the start of each solve, the solver grows that allocation to the variable count plus11//! the entries the scratch needs (`Capacity.trail_capacity`) and hands the tail to the scratch. The12//! scratch takes storage of exactly the byte length it needs, refuses any other length with13//! `error.StorageLengthMismatch`, calls no allocator, and returns the same storage from `deinit`.14//! That storage holds one literal per variable, then one bit per variable rounded up to whole15//! bytes.16//!17//! The analysis works through a handle to the scratch memory for one conflict analysis (a *loan*),18//! and the scratch hands out one loan at a time. A loan records the number of loans taken so far19//! and its own address, so a released loan or a copy of a loan is refused with20//! `error.ConflictScratchStaleLoan`. Every refusal comes before any change, so the scratch and the21//! caller's storage stay as they were. Taking a loan clears the marks, at most one byte per 822//! variables, and a loan holds at most one literal and one resolution step per variable. A23//! compile-time record of this memory (`ConflictScratch.claim`) states the size equation and the24//! refusal behavior, and the shape check at the end of the file validates it.25const std = @import("std");26const alloc_phase = @import("alloc_phase");27const types = @import("types.zig");2829const assert = std.debug.assert;30const Literal = types.Literal;3132/// Scratch memory for one conflict analysis at a time, in storage its caller hands over: a buffer33/// of up to one literal per variable and one mark bit per variable. The solver builds one over the34/// tail of its trail allocation at the start of each solve and takes a loan from it for each35/// conflict it analyzes. `init` takes the storage, `activate` moves the scratch from36/// `.initialization` to `.steady`, and `deinit` moves it to `.teardown` and returns the storage.37/// The scratch calls no allocator. One loan is out at a time, and every loan function refuses a38/// released or copied loan.39pub const ConflictScratch = struct {40    /// The errors that `acquire`, `release` and the loan functions return. The solver's conflict41    /// analysis passes them up with `try`, so they belong to the errors a solve can return. Each42    /// error is returned before any change to the scratch.43    pub const Exhaustion = error{44        /// `acquire` was called while a loan is out.45        ConflictScratchInUse,46        /// `acquire` asked for more variables than the scratch covers, or `Loan.append` or47        /// `Loan.recordResolution` went past the loan's variable count.48        ConflictScratchCapacityExceeded,49        /// `acquire` found the loan counter at the largest `u64`.50        ConflictScratchLoanEpochExhausted,51        /// A loan function or `release` got a loan that is released, a copy at another address,52        /// from a scratch outside `.steady`, or from another scratch.53        ConflictScratchStaleLoan,54    };5556    /// A compile-time record of the scratch's memory: what the storage covers, what stays outside57    /// it, the equation that sizes it from `Limits`, the refusal behavior, the work bound, and the58    /// tests that witness each obligation. The shape check at the end of the file validates the59    /// record and the scratch's shape at compile time. The equation gives the variable count times60    /// the size of a literal, plus the variable count divided by 8 and rounded up, in bytes. The61    /// record states that short storage, oversize use, an exhausted loan counter, copied loans and62    /// overlapping loans are refused before the caller's storage or the scratch changes. The record63    /// states the work bound: taking a loan clears at most one byte per 8 variables, and an64    /// analysis takes at most one resolution step per variable. The learned clauses the solver65    /// keeps, the trail's own entries, the clauses, the watch lists, the search state and the proof66    /// steps stay outside the storage.67    pub const claim: alloc_phase.capacity.Declaration = .{68        .source = .{69            .id = "smt.conflict_scratch",70            .kind = .phase_static,71            .limit_source = .caller,72            .storage = .{73                .covered = &.{74                    .{75                        .id = "conflict_analysis_learned_literal_scratch",76                        .lifetime = .transferred,77                        .detail = "one learned literal per admitted solver variable in the exact trail-tail storage transferred by the caller",78                    },79                    .{80                        .id = "conflict_analysis_seen_variable_scratch",81                        .lifetime = .transferred,82                        .detail = "one dense seen bit per admitted solver variable in the exact trail-tail storage transferred by the caller",83                    },84                },85                .excluded = &.{86                    "retained learned-clause literals copied by addLearnedClause",87                    "the primary trail prefix, rounded tail padding, original clauses, clause headers, watch lists, and search state",88                    "proof trace steps and reverse-unit-propagation assignment state",89                    "old plus new trail backing overlap while variable growth establishes a larger admitted solve workspace",90                },91            },92            .capacity = .{93                .inputs = &.{94                    alloc_phase.capacity.bindInput(Limits, "variables", "variables"),95                },96                .type_selectors = &.{97                    alloc_phase.capacity.bindType(Literal, "literal"),98                },99                .nodes = &.{100                    .{ .input = 0 },101                    .{ .scale = .{ .node = 0, .coefficient = .{ .size_of_concrete_type = 0 } } },102                    .{ .constant = 8 },103                    .{ .ceiling_division = .{ .left = 0, .right = 2 } },104                    .{ .add = .{ .left = 1, .right = 3 } },105                },106                .assertions = &.{.{107                    .scope = .closure_total,108                    .measure = .retained,109                    .relation = .exact,110                    .expression = 4,111                }},112            },113            .overload = .{114                .kind = .reject_before_mutation,115                .detail = "short storage, oversize use, epoch exhaustion, copied tokens, and overlapping address-bound affine loans fail before caller storage or ownership state changes",116            },117            .risks = .{118                .transitive = .{119                    .status = .open,120                    .detail = "learnFromConflict uses one address-bound epoch loan within stable token-storage and owner lifetimes and bounded SAT properties check status, proof, core, and learned-clause semantics; retained learned-clause copies remain a separate owner",121                },122                .foreign = .{123                    .status = .excluded,124                    .detail = "the exact transferred trail tail is process-local memory and conflict analysis crosses no operating-system or foreign-runtime edge",125                },126            },127            .work = .{128                .equation = "initialization <= 1, acquire clearing <= ceil(variables / 8), and resolution steps <= variables",129            },130            .obligations = &.{131                .{ .key = "smt_conflict_scratch_capacity", .role = .capacity_model },132                .{ .key = "smt_conflict_scratch_acquisition", .role = .custom },133                .{ .key = "smt_conflict_scratch_storage_identity", .role = .foreign_risk },134                .{ .key = "smt_conflict_scratch_overload", .role = .overload },135                .{ .key = "smt_conflict_scratch_reuse", .role = .overload },136                .{ .key = "smt_conflict_scratch_work_bound", .role = .work_bound },137                .{ .key = "smt_conflict_scratch_solver_admission", .role = .overload },138                .{ .key = "smt_conflict_scratch_solver_semantics", .role = .transitive_risk },139                .{ .key = "smt_conflict_scratch_foreign_risk", .role = .foreign_risk },140            },141        },142        .bindings = .{143            .owner = @This(),144            .seal = .{145                .family = alloc_phase.capacity.selector(@This().activate),146                .premise = .{147                    .class = .checked_semantic_fact,148                    .authority = .checker,149                },150            },151            .teardown = .{152                .family = alloc_phase.capacity.selector(@This().deinit),153                .premise = .{154                    .class = .checked_semantic_fact,155                    .authority = .checker,156                },157            },158        },159    };160161    /// The alignment the caller's storage needs, equal to the alignment of a literal. A caller162    /// aligns a buffer of its own to this value before it hands the buffer to `init`.163    pub const storage_alignment: usize = @alignOf(Literal);164    /// The byte slice a scratch takes from its caller, aligned for literals. A caller passes one to165    /// `init` and gets the same one back from `deinit`.166    pub const Storage = []align(storage_alignment) u8;167    /// The errors of `init`: `error.CapacityOverflow` from `Capacity.derive`, and168    /// `error.StorageLengthMismatch` when the storage length differs from `Capacity.storage_bytes`.169    /// The solver passes them up from the start of a solve.170    pub const InitError = Capacity.DeriveError || error{StorageLengthMismatch};171    /// Work bounds that the shape check reads: any number of setup steps, and zero cleanup steps172    /// per call. The shape check at the end of the file requires it beside the record in `claim`.173    pub const work_limits: alloc_phase.capacity.WorkLimits = .{174        .transition_steps_max = std.math.maxInt(usize),175        .cleanup_steps_per_call_max = 0,176        .cleanup_calls_at_capacity_max = 0,177    };178179    phase: alloc_phase.capacity.Phase,180    /// The sizes `Capacity.derive` gave for the limits passed to `init`. `admits` and `acquire`181    /// compare with its variable count, and the solver reads it to find the storage again at each182    /// analysis.183    capacity: Capacity,184    /// The storage passed to `init`, which `deinit` returns. The literal buffer starts at its first185    /// byte, and the mark bits start at `Capacity.seen_offset`. The solver checks at each analysis186    /// that it still matches the tail of the trail allocation.187    storage: Storage,188    literals: []Literal,189    seen: []u8,190    loaned: bool = false,191    loan_epoch: u64 = 0,192    loan_identity: usize = 0,193    loan_variables: usize = 0,194    loan_literal_count: usize = 0,195    loan_resolution_steps: usize = 0,196197    /// The input that sizes a scratch: its variable count. The solver builds one from the variable198    /// count a solve needs, counting every variable its assumptions name.199    pub const Limits = struct {200        /// The number of variables the scratch covers.201        variables: usize,202203        /// Returns the limits for `variables`. The solver builds its scratch limits through it.204        pub fn inspect(variables: usize) Limits {205            return .{ .variables = variables };206        }207    };208209    /// The sizes of one scratch and of the trail allocation that holds it, in bytes and in210    /// literals. The solver derives it at the start of each solve to size its trail allocation and211    /// to find the scratch storage inside it.212    pub const Capacity = struct {213        /// The variable count from the limits, which is the most literals and marks a loan uses.214        variables: usize,215        /// Bytes of the literal buffer: the variable count times the size of a literal.216        literal_bytes: usize,217        /// The byte offset of the mark bits in the storage, equal to `literal_bytes`.218        seen_offset: usize,219        /// Bytes of mark bits: the variable count divided by 8, rounded up.220        seen_bytes: usize,221        /// Bytes of storage: `literal_bytes` plus `seen_bytes`. `init` refuses storage of any other222        /// length.223        storage_bytes: usize,224        /// The storage size in literals, rounded up, which is the number of trail entries the225        /// solver sets aside for the scratch.226        backing_literals: usize,227        /// The trail allocation the solver needs, in literals: the variable count plus228        /// `backing_literals`.229        trail_capacity: usize,230231        /// The error of `derive`: `error.CapacityOverflow`. `init` and the solver pass it up before232        /// anything is allocated.233        pub const DeriveError = error{CapacityOverflow};234235        /// Returns the sizes for `limits`. The solver sizes its trail allocation from it before a236        /// solve, and `init` checks the storage length against it. The call returns237        /// `error.CapacityOverflow` when the literal bytes, the storage bytes or the trail238        /// allocation overflows `usize`.239        pub fn derive(limits: Limits) DeriveError!Capacity {240            const literal_bytes = std.math.mul(241                usize,242                limits.variables,243                @sizeOf(Literal),244            ) catch return error.CapacityOverflow;245            const seen_bytes = limits.variables / 8 +246                @intFromBool(limits.variables % 8 != 0);247            const storage_bytes = std.math.add(248                usize,249                literal_bytes,250                seen_bytes,251            ) catch return error.CapacityOverflow;252            const backing_literals = storage_bytes / @sizeOf(Literal) +253                @intFromBool(storage_bytes % @sizeOf(Literal) != 0);254            const trail_capacity = std.math.add(255                usize,256                limits.variables,257                backing_literals,258            ) catch return error.CapacityOverflow;259            assert(literal_bytes % @alignOf(Literal) == 0);260            return .{261                .variables = limits.variables,262                .literal_bytes = literal_bytes,263                .seen_offset = literal_bytes,264                .seen_bytes = seen_bytes,265                .storage_bytes = storage_bytes,266                .backing_literals = backing_literals,267                .trail_capacity = trail_capacity,268            };269        }270    };271272    /// A handle to the scratch memory for one conflict analysis, which reaches the scratch's273    /// literal buffer and marks and holds the scratch's address and the loan's number. The solver's274    /// conflict analysis takes one per conflict with `acquire`, marks the variables it meets,275    /// collects the learned clause's literals, and hands the loan back with `release`. Every loan276    /// function checks the loan first and returns `error.ConflictScratchStaleLoan` when the loan277    /// was released, when a later `acquire` replaced it, when it is a copy at another address, or278    /// when the scratch is outside `.steady`. The loan stays valid only at the address `acquire`279    /// filled, so the caller keeps it in place until `release`.280    pub const Loan = struct {281        const BitPosition = struct {282            byte: usize,283            mask: u8,284        };285286        owner: *ConflictScratch,287        epoch: u64,288289        /// Marks `variable_index` as met and returns true, or returns false when it was already290        /// marked. The analysis calls it on each literal of a clause it resolves on, and a false291        /// result skips a variable it has already counted. The call asserts that `variable_index`292        /// is below the loan's variable count. The call returns `error.ConflictScratchStaleLoan`293        /// for a stale loan.294        pub fn markSeen(self: *const Loan, variable_index: u32) Exhaustion!bool {295            const owner = try self.ownerFor();296            assert(variable_index < owner.loan_variables);297            const bit = bitPosition(variable_index);298            if (owner.seen[bit.byte] & bit.mask != 0) return false;299            owner.seen[bit.byte] |= bit.mask;300            return true;301        }302303        /// Removes the mark from `variable_index`. The analysis unmarks the variable it resolves on304        /// at each step. The call asserts that `variable_index` is below the loan's variable count305        /// and is marked. The call returns `error.ConflictScratchStaleLoan` for a stale loan.306        pub fn clearSeen(self: *const Loan, variable_index: u32) Exhaustion!void {307            const owner = try self.ownerFor();308            assert(variable_index < owner.loan_variables);309            const bit = bitPosition(variable_index);310            assert(owner.seen[bit.byte] & bit.mask != 0);311            owner.seen[bit.byte] &= ~bit.mask;312        }313314        /// Returns true when `variable_index` is marked. The analysis walks the trail backward and315        /// stops at the first marked variable. The call asserts that `variable_index` is below the316        /// loan's variable count. The call returns `error.ConflictScratchStaleLoan` for a stale317        /// loan.318        pub fn isSeen(self: *const Loan, variable_index: u32) Exhaustion!bool {319            const owner = try self.ownerFor();320            assert(variable_index < owner.loan_variables);321            const bit = bitPosition(variable_index);322            return owner.seen[bit.byte] & bit.mask != 0;323        }324325        /// Adds `literal` after the loan's earlier literals. The analysis adds each literal of the326        /// learned clause through it. The call returns `error.ConflictScratchCapacityExceeded` when327        /// the loan already holds its variable count of literals, and328        /// `error.ConflictScratchStaleLoan` for a stale loan, before any change.329        pub fn append(self: *const Loan, literal: Literal) Exhaustion!void {330            const owner = try self.ownerFor();331            if (owner.loan_literal_count == owner.loan_variables) {332                return error.ConflictScratchCapacityExceeded;333            }334            owner.literals[owner.loan_literal_count] = literal;335            owner.loan_literal_count += 1;336        }337338        /// Counts one resolution step. The analysis calls it at the start of each resolution step.339        /// The call returns `error.ConflictScratchCapacityExceeded` when the loan has already340        /// counted its variable count of steps, and `error.ConflictScratchStaleLoan` for a stale341        /// loan, before counting.342        pub fn recordResolution(self: *const Loan) Exhaustion!void {343            const owner = try self.ownerFor();344            if (owner.loan_resolution_steps == owner.loan_variables) {345                return error.ConflictScratchCapacityExceeded;346            }347            owner.loan_resolution_steps += 1;348        }349350        /// Returns the literals added since `acquire`, in order. The analysis reads the learned351        /// clause through it when the resolution ends. The slice points into the scratch storage,352        /// so literals added under a later loan overwrite it. The call returns353        /// `error.ConflictScratchStaleLoan` for a stale loan.354        pub fn literals(self: *const Loan) Exhaustion![]const Literal {355            const owner = try self.ownerFor();356            assert(owner.loan_literal_count <= owner.loan_variables);357            return owner.literals[0..owner.loan_literal_count];358        }359360        fn ownerFor(self: *const Loan) Exhaustion!*ConflictScratch {361            const owner = self.owner;362            if (owner.phase != .steady or363                !owner.loaned or364                owner.loan_epoch != self.epoch or365                owner.loan_identity != @intFromPtr(self))366            {367                return error.ConflictScratchStaleLoan;368            }369            return owner;370        }371372        fn bitPosition(variable_index: u32) BitPosition {373            return .{374                .byte = variable_index / 8,375                .mask = @as(u8, 1) << @intCast(variable_index % 8),376            };377        }378    };379380    /// Returns a scratch in `.initialization` over `storage`, sized for `limits`. The solver builds381    /// one over the tail of its trail allocation at the start of each solve that has at least one382    /// variable. The call returns `error.CapacityOverflow` from `Capacity.derive`, and383    /// `error.StorageLengthMismatch` when `storage` is shorter or longer than384    /// `Capacity.storage_bytes`. On either error, `storage` stays unchanged and stays with the385    /// caller. The scratch holds `storage` until `deinit` returns it.386    pub fn init(storage: Storage, limits: Limits) InitError!ConflictScratch {387        const capacity = try Capacity.derive(limits);388        if (storage.len != capacity.storage_bytes) {389            return error.StorageLengthMismatch;390        }391        const owned = storage;392        const literals = typedSlice(Literal, owned, 0, capacity.variables);393        const seen = owned[capacity.seen_offset..][0..capacity.seen_bytes];394        assert(literals.len * @sizeOf(Literal) == capacity.literal_bytes);395        assert(seen.len == capacity.seen_bytes);396        return .{397            .phase = .initialization,398            .capacity = capacity,399            .storage = owned,400            .literals = literals,401            .seen = seen,402        };403    }404405    /// Moves the scratch from `.initialization` to `.steady`, after which `acquire` can hand out406    /// loans. The solver calls it once, right after `init`. The call asserts that the scratch is as407    /// `init` left it.408    pub fn activate(self: *ConflictScratch) void {409        assert(self.phase == .initialization);410        assert(self.storage.len == self.capacity.storage_bytes);411        assert(!self.loaned);412        assert(self.loan_identity == 0);413        assert(self.loan_variables == 0);414        assert(self.loan_literal_count == 0);415        assert(self.loan_resolution_steps == 0);416        self.phase = .steady;417    }418419    /// Returns true when the scratch covers at least `required.variables` variables. A caller that420    /// holds a scratch checks with it whether the scratch covers a variable count before reusing421    /// the scratch for that count. The solver builds a new scratch at each solve, so the package422    /// itself makes no call to it. The call asserts that the scratch is `.steady`.423    pub fn admits(self: *const ConflictScratch, required: Capacity) bool {424        assert(self.phase == .steady);425        return self.capacity.variables >= required.variables;426    }427428    /// Clears the marks and fills `loan` as the one loan out, covering `variables` variables. The429    /// analysis takes a loan with it at the start of each conflict it analyzes. The call returns430    /// `error.ConflictScratchInUse` while another loan is out,431    /// `error.ConflictScratchCapacityExceeded` when `variables` passes the scratch's variable432    /// count, and `error.ConflictScratchLoanEpochExhausted` when the loan counter is at the largest433    /// `u64`. Each error leaves the scratch and its marks as they were. The call clears every mark434    /// byte, at most one byte per 8 variables of the scratch. The call records the address of435    /// `loan`, so the caller keeps `loan` in place until `release`. The call asserts that the436    /// scratch is `.steady`.437    pub fn acquire(438        self: *ConflictScratch,439        variables: usize,440        loan: *Loan,441    ) Exhaustion!void {442        assert(self.phase == .steady);443        if (self.loaned) return error.ConflictScratchInUse;444        if (variables > self.capacity.variables) {445            return error.ConflictScratchCapacityExceeded;446        }447        const epoch = std.math.add(u64, self.loan_epoch, 1) catch {448            return error.ConflictScratchLoanEpochExhausted;449        };450        @memset(self.seen, 0);451        loan.* = .{452            .owner = self,453            .epoch = epoch,454        };455        self.loaned = true;456        self.loan_epoch = epoch;457        self.loan_identity = @intFromPtr(loan);458        self.loan_variables = variables;459        self.loan_literal_count = 0;460        self.loan_resolution_steps = 0;461    }462463    /// Ends the current loan, so `acquire` can hand out the next one. The analysis releases its464    /// loan when it returns, whether it learned a clause or failed. The call returns465    /// `error.ConflictScratchStaleLoan` when `loan` is stale or comes from another scratch, and466    /// then the current loan stays out. Every loan function refuses `loan` after the call. The call467    /// asserts that the scratch is `.steady`.468    pub fn release(self: *ConflictScratch, loan: *const Loan) Exhaustion!void {469        assert(self.phase == .steady);470        const owner = try loan.ownerFor();471        if (owner != self) return error.ConflictScratchStaleLoan;472        assert(self.loan_literal_count <= self.loan_variables);473        assert(self.loan_resolution_steps <= self.loan_variables);474        self.loaned = false;475        self.loan_identity = 0;476        self.loan_variables = 0;477        self.loan_literal_count = 0;478        self.loan_resolution_steps = 0;479    }480481    /// Moves the scratch to `.teardown`, returns the storage passed to `init`, and leaves the482    /// scratch undefined. The solver calls it when a solve ends and checks that the storage came483    /// back with the same address and length. The call asserts that no loan is out. The call works484    /// from `.initialization` or `.steady`.485    pub fn deinit(self: *ConflictScratch) Storage {486        assert(self.phase != .teardown);487        assert(!self.loaned);488        assert(self.loan_identity == 0);489        assert(self.loan_variables == 0);490        assert(self.loan_literal_count == 0);491        assert(self.loan_resolution_steps == 0);492        assert(self.storage.len == self.capacity.storage_bytes);493        self.phase = .teardown;494        const storage = self.storage;495        self.* = undefined;496        return storage;497    }498};499500fn typedSlice(501    comptime T: type,502    bytes: ConflictScratch.Storage,503    offset: usize,504    count: usize,505) []T {506    const byte_count = count * @sizeOf(T);507    const region: []align(@alignOf(T)) u8 = @alignCast(bytes[offset..][0..byte_count]);508    return std.mem.bytesAsSlice(T, region);509}510511test "conflict scratch capacity matches an independent typed-byte model" {512    comptime {513        @stardustClaim(514            @import("alloc_phase").capacity.witness(ConflictScratch, "smt_conflict_scratch_capacity"),515            null,516            null,517            null,518            null,519            null,520            null,521        );522    }523524    const capacity = try ConflictScratch.Capacity.derive(525        ConflictScratch.Limits.inspect(96),526    );527    try std.testing.expectEqual(@as(usize, 96), capacity.variables);528    try std.testing.expectEqual(@as(usize, 96 * @sizeOf(Literal)), capacity.literal_bytes);529    try std.testing.expectEqual(capacity.literal_bytes, capacity.seen_offset);530    try std.testing.expectEqual(@as(usize, 12), capacity.seen_bytes);531    try std.testing.expectEqual(532        @as(usize, 96 * @sizeOf(Literal) + 12),533        capacity.storage_bytes,534    );535    try std.testing.expectEqual(@as(usize, 99), capacity.backing_literals);536    try std.testing.expectEqual(@as(usize, 195), capacity.trail_capacity);537    try std.testing.expectError(538        error.CapacityOverflow,539        ConflictScratch.Capacity.derive(ConflictScratch.Limits.inspect(std.math.maxInt(usize))),540    );541}542543test "conflict scratch returns exact caller storage and rejects inexact transfers" {544    comptime {545        @stardustClaim(546            @import("alloc_phase").capacity.witness(ConflictScratch, "smt_conflict_scratch_storage_identity"),547            null,548            null,549            null,550            null,551            null,552            null,553        );554    }555556    var bytes: [8 * @sizeOf(Literal) + 1]u8 align(ConflictScratch.storage_alignment) =557        @splat(0xa5);558    const before = bytes;559    try std.testing.expectError(560        error.StorageLengthMismatch,561        ConflictScratch.init(bytes[0 .. bytes.len - 1], .{ .variables = 8 }),562    );563    try std.testing.expectEqualSlices(u8, &before, &bytes);564565    var oversized: [8 * @sizeOf(Literal) + 2]u8 align(ConflictScratch.storage_alignment) =566        @splat(0x5a);567    const oversized_before = oversized;568    const oversized_transfer: ConflictScratch.Storage = oversized[0..];569    const oversized_pointer = @intFromPtr(oversized_transfer.ptr);570    const oversized_length = oversized_transfer.len;571    try std.testing.expectError(572        error.StorageLengthMismatch,573        ConflictScratch.init(oversized_transfer, .{ .variables = 8 }),574    );575    try std.testing.expectEqual(oversized_pointer, @intFromPtr(oversized_transfer.ptr));576    try std.testing.expectEqual(oversized_length, oversized_transfer.len);577    try std.testing.expectEqualSlices(u8, &oversized_before, &oversized);578579    const transferred: ConflictScratch.Storage = bytes[0..];580    var owner = try ConflictScratch.init(transferred, .{ .variables = 8 });581    owner.activate();582    const returned = owner.deinit();583    try std.testing.expectEqual(@intFromPtr(transferred.ptr), @intFromPtr(returned.ptr));584    try std.testing.expectEqual(transferred.len, returned.len);585}586587test "conflict scratch rejects before mutation and exactly returns its affine loan" {588    comptime {589        @stardustClaim(590            @import("alloc_phase").capacity.witness(ConflictScratch, "smt_conflict_scratch_acquisition"),591            null,592            null,593            null,594            null,595            null,596            null,597        );598    }599    comptime {600        @stardustClaim(601            @import("alloc_phase").capacity.witness(ConflictScratch, "smt_conflict_scratch_overload"),602            null,603            null,604            null,605            null,606            null,607            null,608        );609    }610    comptime {611        @stardustClaim(612            @import("alloc_phase").capacity.witness(ConflictScratch, "smt_conflict_scratch_reuse"),613            null,614            null,615            null,616            null,617            null,618            null,619        );620    }621    comptime {622        @stardustClaim(623            @import("alloc_phase").capacity.witness(ConflictScratch, "smt_conflict_scratch_work_bound"),624            null,625            null,626            null,627            null,628            null,629            null,630        );631    }632    comptime {633        @stardustClaim(634            @import("alloc_phase").capacity.witness(ConflictScratch, "smt_conflict_scratch_foreign_risk"),635            null,636            null,637            null,638            null,639            null,640            null,641        );642    }643644    var bytes: [3 * @sizeOf(Literal) + 1]u8 align(ConflictScratch.storage_alignment) = undefined;645    var owner = try ConflictScratch.init(bytes[0..], .{ .variables = 3 });646    defer _ = owner.deinit();647    owner.activate();648649    var loan: ConflictScratch.Loan = undefined;650    try owner.acquire(3, &loan);651    const copied_loan = loan;652    const literal_pointer = owner.literals.ptr;653    const seen_pointer = owner.seen.ptr;654    try std.testing.expectError(655        error.ConflictScratchStaleLoan,656        copied_loan.append(Literal.positive(0)),657    );658    try std.testing.expectEqual(@as(usize, 0), owner.loan_literal_count);659    try std.testing.expectError(660        error.ConflictScratchStaleLoan,661        owner.release(&copied_loan),662    );663    try std.testing.expect(owner.loaned);664    try std.testing.expect(try loan.markSeen(0));665    try std.testing.expect(!try loan.markSeen(0));666    try loan.append(Literal.positive(0));667    try loan.append(Literal.negative(1));668    try loan.append(Literal.positive(2));669    try loan.recordResolution();670    try loan.recordResolution();671    try loan.recordResolution();672    try std.testing.expectError(673        error.ConflictScratchCapacityExceeded,674        loan.append(Literal.negative(2)),675    );676    try std.testing.expectError(error.ConflictScratchCapacityExceeded, loan.recordResolution());677    var overlapping: ConflictScratch.Loan = undefined;678    try std.testing.expectError(error.ConflictScratchInUse, owner.acquire(3, &overlapping));679    try std.testing.expectEqual(@as(usize, 3), (try loan.literals()).len);680    try owner.release(&loan);681    try std.testing.expectError(682        error.ConflictScratchStaleLoan,683        copied_loan.append(Literal.positive(0)),684    );685686    owner.seen[0] = 0x80;687    var oversized: ConflictScratch.Loan = undefined;688    try std.testing.expectError(689        error.ConflictScratchCapacityExceeded,690        owner.acquire(4, &oversized),691    );692    try std.testing.expect(owner.seen[0] != 0);693    try std.testing.expect(!owner.loaned);694695    var reused: ConflictScratch.Loan = undefined;696    try owner.acquire(3, &reused);697    try std.testing.expectEqual(literal_pointer, owner.literals.ptr);698    try std.testing.expectEqual(seen_pointer, owner.seen.ptr);699    try std.testing.expect(!try reused.isSeen(0));700    try std.testing.expectError(701        error.ConflictScratchStaleLoan,702        copied_loan.append(Literal.positive(0)),703    );704    try owner.release(&reused);705706    owner.loan_epoch = std.math.maxInt(u64);707    owner.seen[0] = 0x80;708    var exhausted: ConflictScratch.Loan = undefined;709    try std.testing.expectError(710        error.ConflictScratchLoanEpochExhausted,711        owner.acquire(3, &exhausted),712    );713    try std.testing.expect(owner.seen[0] != 0);714    try std.testing.expect(!owner.loaned);715}716717comptime {718    alloc_phase.capacity.requireProvisionedRejectingOwnerShape(ConflictScratch);719}