lib/smt/src/sat/scratch.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 //! Scratch memory for one conflict analysis at a time: room for the literals of the clause being
2 //! learned and one mark per variable. The solver analyzes each conflict it meets above decision
3 //! level zero, and a caller that bounds memory wants that analysis to run in memory set aside
4 //! before the search starts. The clause learned from one conflict holds at most one literal per
5 //! variable, and the analysis marks each variable at most once, so the memory one analysis needs
6 //! grows with the variable count alone. The solver already allocates the list of assigned literals
7 //! 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-count
10 //! entries. At the start of each solve, the solver grows that allocation to the variable count plus
11 //! the entries the scratch needs (`Capacity.trail_capacity`) and hands the tail to the scratch. The
12 //! scratch takes storage of exactly the byte length it needs, refuses any other length with
13 //! `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 whole
15 //! 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 far
19 //! and its own address, so a released loan or a copy of a loan is refused with
20 //! `error.ConflictScratchStaleLoan`. Every refusal comes before any change, so the scratch and the
21 //! caller's storage stay as they were. Taking a loan clears the marks, at most one byte per 8
22 //! variables, and a loan holds at most one literal and one resolution step per variable. A
23 //! compile-time record of this memory (`ConflictScratch.claim`) states the size equation and the
24 //! refusal behavior, and the shape check at the end of the file validates it.
25 const std = @import("std");
26 const alloc_phase = @import("alloc_phase");
27 const types = @import("types.zig");
28
29 const assert = std.debug.assert;
30 const Literal = types.Literal;
31
32 /// Scratch memory for one conflict analysis at a time, in storage its caller hands over: a buffer
33 /// of up to one literal per variable and one mark bit per variable. The solver builds one over the
34 /// tail of its trail allocation at the start of each solve and takes a loan from it for each
35 /// conflict it analyzes. `init` takes the storage, `activate` moves the scratch from
36 /// `.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 a
38 /// released or copied loan.
39 pub const ConflictScratch = struct {
40 /// The errors that `acquire`, `release` and the loan functions return. The solver's conflict
41 /// analysis passes them up with `try`, so they belong to the errors a solve can return. Each
42 /// 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` or
47 /// `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 };
55
56 /// A compile-time record of the scratch's memory: what the storage covers, what stays outside
57 /// it, the equation that sizes it from `Limits`, the refusal behavior, the work bound, and the
58 /// tests that witness each obligation. The shape check at the end of the file validates the
59 /// record and the scratch's shape at compile time. The equation gives the variable count times
60 /// the size of a literal, plus the variable count divided by 8 and rounded up, in bytes. The
61 /// record states that short storage, oversize use, an exhausted loan counter, copied loans and
62 /// overlapping loans are refused before the caller's storage or the scratch changes. The record
63 /// states the work bound: taking a loan clears at most one byte per 8 variables, and an
64 /// analysis takes at most one resolution step per variable. The learned clauses the solver
65 /// keeps, the trail's own entries, the clauses, the watch lists, the search state and the proof
66 /// 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 };
160
161 /// The alignment the caller's storage needs, equal to the alignment of a literal. A caller
162 /// 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 to
165 /// `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`, and
168 /// `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 steps
172 /// 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 };
178
179 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 each
182 /// analysis.
183 capacity: Capacity,
184 /// The storage passed to `init`, which `deinit` returns. The literal buffer starts at its first
185 /// byte, and the mark bits start at `Capacity.seen_offset`. The solver checks at each analysis
186 /// 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,
196
197 /// The input that sizes a scratch: its variable count. The solver builds one from the variable
198 /// 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,
202
203 /// 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 };
208
209 /// The sizes of one scratch and of the trail allocation that holds it, in bytes and in
210 /// literals. The solver derives it at the start of each solve to size its trail allocation and
211 /// 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 other
222 /// length.
223 storage_bytes: usize,
224 /// The storage size in literals, rounded up, which is the number of trail entries the
225 /// solver sets aside for the scratch.
226 backing_literals: usize,
227 /// The trail allocation the solver needs, in literals: the variable count plus
228 /// `backing_literals`.
229 trail_capacity: usize,
230
231 /// The error of `derive`: `error.CapacityOverflow`. `init` and the solver pass it up before
232 /// anything is allocated.
233 pub const DeriveError = error{CapacityOverflow};
234
235 /// Returns the sizes for `limits`. The solver sizes its trail allocation from it before a
236 /// solve, and `init` checks the storage length against it. The call returns
237 /// `error.CapacityOverflow` when the literal bytes, the storage bytes or the trail
238 /// 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 };
271
272 /// A handle to the scratch memory for one conflict analysis, which reaches the scratch's
273 /// literal buffer and marks and holds the scratch's address and the loan's number. The solver's
274 /// 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 loan
276 /// function checks the loan first and returns `error.ConflictScratchStaleLoan` when the loan
277 /// was released, when a later `acquire` replaced it, when it is a copy at another address, or
278 /// 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 };
285
286 owner: *ConflictScratch,
287 epoch: u64,
288
289 /// Marks `variable_index` as met and returns true, or returns false when it was already
290 /// marked. The analysis calls it on each literal of a clause it resolves on, and a false
291 /// 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 }
302
303 /// Removes the mark from `variable_index`. The analysis unmarks the variable it resolves on
304 /// at each step. The call asserts that `variable_index` is below the loan's variable count
305 /// 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 }
313
314 /// Returns true when `variable_index` is marked. The analysis walks the trail backward and
315 /// stops at the first marked variable. The call asserts that `variable_index` is below the
316 /// loan's variable count. The call returns `error.ConflictScratchStaleLoan` for a stale
317 /// 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 }
324
325 /// Adds `literal` after the loan's earlier literals. The analysis adds each literal of the
326 /// learned clause through it. The call returns `error.ConflictScratchCapacityExceeded` when
327 /// the loan already holds its variable count of literals, and
328 /// `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 }
337
338 /// 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 already
340 /// counted its variable count of steps, and `error.ConflictScratchStaleLoan` for a stale
341 /// 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 }
349
350 /// Returns the literals added since `acquire`, in order. The analysis reads the learned
351 /// 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 returns
353 /// `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 }
359
360 fn ownerFor(self: *const Loan) Exhaustion!*ConflictScratch {
361 const owner = self.owner;
362 if (owner.phase != .steady or
363 !owner.loaned or
364 owner.loan_epoch != self.epoch or
365 owner.loan_identity != @intFromPtr(self))
366 {
367 return error.ConflictScratchStaleLoan;
368 }
369 return owner;
370 }
371
372 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 };
379
380 /// Returns a scratch in `.initialization` over `storage`, sized for `limits`. The solver builds
381 /// one over the tail of its trail allocation at the start of each solve that has at least one
382 /// variable. The call returns `error.CapacityOverflow` from `Capacity.derive`, and
383 /// `error.StorageLengthMismatch` when `storage` is shorter or longer than
384 /// `Capacity.storage_bytes`. On either error, `storage` stays unchanged and stays with the
385 /// 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 }
404
405 /// Moves the scratch from `.initialization` to `.steady`, after which `acquire` can hand out
406 /// loans. The solver calls it once, right after `init`. The call asserts that the scratch is as
407 /// `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 }
418
419 /// Returns true when the scratch covers at least `required.variables` variables. A caller that
420 /// holds a scratch checks with it whether the scratch covers a variable count before reusing
421 /// the scratch for that count. The solver builds a new scratch at each solve, so the package
422 /// 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 }
427
428 /// Clears the marks and fills `loan` as the one loan out, covering `variables` variables. The
429 /// analysis takes a loan with it at the start of each conflict it analyzes. The call returns
430 /// `error.ConflictScratchInUse` while another loan is out,
431 /// `error.ConflictScratchCapacityExceeded` when `variables` passes the scratch's variable
432 /// count, and `error.ConflictScratchLoanEpochExhausted` when the loan counter is at the largest
433 /// `u64`. Each error leaves the scratch and its marks as they were. The call clears every mark
434 /// byte, at most one byte per 8 variables of the scratch. The call records the address of
435 /// `loan`, so the caller keeps `loan` in place until `release`. The call asserts that the
436 /// 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 }
462
463 /// Ends the current loan, so `acquire` can hand out the next one. The analysis releases its
464 /// loan when it returns, whether it learned a clause or failed. The call returns
465 /// `error.ConflictScratchStaleLoan` when `loan` is stale or comes from another scratch, and
466 /// then the current loan stays out. Every loan function refuses `loan` after the call. The call
467 /// 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 }
480
481 /// Moves the scratch to `.teardown`, returns the storage passed to `init`, and leaves the
482 /// scratch undefined. The solver calls it when a solve ends and checks that the storage came
483 /// back with the same address and length. The call asserts that no loan is out. The call works
484 /// 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 };
499
500 fn 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 }
510
511 test "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 }
523
524 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 }
542
543 test "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 }
555
556 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);
564
565 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);
578
579 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 }
586
587 test "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 }
643
644 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();
648
649 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 );
685
686 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);
694
695 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);
705
706 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 }
716
717 comptime {
718 alloc_phase.capacity.requireProvisionedRejectingOwnerShape(ConflictScratch);
719 }