lib/smt/src/sat/trace.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 //! Fixed memory for the proof steps of one solve, used when the solve has a conflict limit. A
2 //! solver records a proof step for each clause it learns, and a caller that bounds a search by a
3 //! conflict limit wants the memory for those steps known before the search starts.
4 //!
5 //! A solve learns at most one clause per conflict, and each clause holds at most one literal per
6 //! variable, so a conflict limit bounds the steps and their literals, with room left for the final
7 //! empty clause. The steps of a solve are dropped all at once when the solver clears them, and the
8 //! solver takes back only the step it added last, when that step's clause fails to be stored.
9 //!
10 //! The trace storage (`Trace`) packs the step literals end to end in one block of literals (a
11 //! slab), with room for the conflict limit plus 2 steps, each at most as wide as the variable
12 //! count. Adding a step copies its literals after the last one, clearing resets two counters, and
13 //! taking back a step drops the last one, so no operation after setup calls an allocator. Adding a
14 //! step to a full trace trips an assertion, because the step count is meant to rule that case out.
15 //! When the conflict limit is null, the solver keeps its steps in its heap memory, and so do the
16 //! extra solves of core minimization. A compile-time record of this memory (`Trace.claim`) states
17 //! the size equation and the overload behavior, and the shape check at the end of the file
18 //! validates it.
19 const std = @import("std");
20 const alloc_phase = @import("alloc_phase");
21 const types = @import("types.zig");
22
23 const assert = std.debug.assert;
24 const Allocator = std.mem.Allocator;
25 const Literal = types.Literal;
26
27 /// Fixed memory for the literals of one solve's proof steps, packed end to end in one slab, with
28 /// counts of the steps and literals handed out. The solver keeps one while `Solver.conflict_budget`
29 /// is set and records each proof step of a solve in it. `init` allocates the slab, `activate` moves
30 /// the trace from `.initialization` to `.steady`, and `deinit` moves it to `.teardown` and frees
31 /// the slab. In `.steady`, adding, taking back and clearing steps call no allocator, and adding a
32 /// step costs the copy of its literals. The solver clears it whenever it clears its proof trace,
33 /// and keeps it across solves while it admits what the next solve needs.
34 pub const Trace = struct {
35 /// A compile-time record of the trace's memory: what the slab covers, what stays outside it,
36 /// the equation that sizes it from `Limits`, the overload behavior, and the tests that witness
37 /// each obligation. The shape check at the end of the file validates the record and the trace's
38 /// shape at compile time. The equation gives the conflict limit plus 2, times the variable
39 /// count, in literals. The record states that an overflow is refused before any storage exists,
40 /// and that adding a step to a full trace is a sizing bug that trips an assertion. The solver's
41 /// list of steps, the proof assumptions, the steps of solves whose conflict limit is null and
42 /// of core minimization, and exported proof artifacts stay outside the slab.
43 pub const claim: alloc_phase.capacity.Declaration = .{
44 .source = .{
45 .id = "smt.proof_trace",
46 .kind = .phase_static,
47 .limit_source = .caller,
48 .storage = .{
49 .covered = &.{
50 .{
51 .id = "proof_step_literal_slab_of_steps_x_variablecount_li_d1a74d0532c5",
52 .lifetime = .steady,
53 .detail = "proof step literal slab of steps x variableCount literals on budgeted solves",
54 },
55 },
56 .excluded = &.{
57 "proof step headers in the solver-owned proof_steps list, whose capacity is reserved during trace initialization",
58 "proof assumptions, which track caller assumption counts",
59 "steps on solvers without conflict_budget and on probe scratch solvers (proof_trace_slab = false), which keep heap dupe semantics",
60 "ProofArtifact exports, which copy into caller-owned storage",
61 },
62 },
63 .capacity = .{
64 .inputs = &.{
65 alloc_phase.capacity.bindInput(Limits, "conflicts", "conflicts"),
66 alloc_phase.capacity.bindInput(Limits, "variables", "variables"),
67 },
68 .type_selectors = &.{
69 alloc_phase.capacity.bindType(Literal, "literal"),
70 },
71 .nodes = &.{
72 .{ .input = 0 },
73 .{ .constant = 2 },
74 .{ .add = .{ .left = 0, .right = 1 } },
75 .{ .input = 1 },
76 .{ .product = .{ .left = 2, .right = 3 } },
77 .{ .constant = 1 },
78 .{ .scale = .{ .node = 5, .coefficient = .{ .size_of_concrete_type = 0 } } },
79 .{ .product = .{ .left = 4, .right = 6 } },
80 },
81 .assertions = &.{.{
82 .scope = .closure_total,
83 .measure = .retained,
84 .relation = .exact,
85 .expression = 7,
86 }},
87 },
88 .overload = .{
89 .kind = .reject_before_seal,
90 .detail = "Capacity.derive rejects arithmetic overflow before any storage is acquired, so oversized budgets fail the solve loudly; steady acquire asserts a free step and slab room because the step equation covers every learn plus the final step, so steady exhaustion is a capacity-model bug and crashes",
91 },
92 .risks = .{
93 .transitive = .{
94 .status = .open,
95 .detail = "step headers referencing slab literals live in the solver-owned proof_steps list with capacity reserved at trace initialization, slab versus heap freeing is routed by trace presence with all-or-nothing storage per clear cycle, and the bounded differential and store-exercise properties independently check artifact acceptance, exact-scope unsatisfiability, and retained-clause entailment through the smt-pbt lane",
96 },
97 .foreign = .{
98 .status = .excluded,
99 .detail = "the slab is process-local memory from the caller allocator with no operating-system or foreign-runtime edge",
100 },
101 },
102 .obligations = &.{
103 .{ .key = "smt_trace_capacity_capacity_model", .role = .capacity_model },
104 .{ .key = "smt_trace_capacity_overload", .role = .overload },
105 .{ .key = "smt_trace_oom_retry", .role = .foreign_risk },
106 .{ .key = "smt_trace_sealed_fill_overload", .role = .overload },
107 .{ .key = "smt_trace_sealed_fill_foreign_risk", .role = .foreign_risk },
108 .{ .key = "smt_trace_slab_solve", .role = .transitive_risk },
109 .{ .key = "smt_trace_lifecycle", .role = .transitive_risk },
110 .{ .key = "smt_trace_bounded_solve", .role = .transitive_risk },
111 },
112 },
113 .bindings = .{
114 .owner = @This(),
115 .seal = .{
116 .family = alloc_phase.capacity.selector(@This().activate),
117 .premise = .{
118 .class = .checked_semantic_fact,
119 .authority = .checker,
120 },
121 },
122 .teardown = .{
123 .family = alloc_phase.capacity.selector(@This().deinit),
124 .premise = .{
125 .class = .checked_semantic_fact,
126 .authority = .checker,
127 },
128 },
129 },
130 };
131 phase: alloc_phase.capacity.Phase,
132 /// The sizes that `Capacity.derive` gave when the trace was built. `admits`, `freeSteps` and
133 /// the solver's reservation of its step list read them.
134 capacity: Capacity,
135 slab: []Literal,
136 step_count: usize,
137 literal_count: usize,
138
139 /// The inputs that size a trace: the solve's conflict limit and the solver's variable count.
140 /// The solver builds one from `conflict_budget` and its variable count at the start of each
141 /// solve with a conflict limit.
142 pub const Limits = struct {
143 /// The conflict limit of the solve, taken from `Solver.conflict_budget`.
144 conflicts: usize,
145 /// The solver's variable count, which is the most literals one step holds.
146 variables: usize,
147
148 /// Returns the limits for `conflicts` and `variables`. The solver builds its trace limits
149 /// through it.
150 pub fn inspect(conflicts: usize, variables: usize) Limits {
151 return .{
152 .conflicts = conflicts,
153 .variables = variables,
154 };
155 }
156 };
157
158 /// The sizes of one trace: its step count, its step width in literals and its total literal
159 /// count. The solver derives the sizes a solve needs and asks its current trace whether it
160 /// `admits` them before it builds a new one.
161 pub const Capacity = struct {
162 /// Steps the trace holds: the conflict limit plus 2. The count covers a step for every
163 /// clause learned within the limit and the final empty step.
164 steps: usize,
165 /// The most literals in one step, equal to the variable count.
166 step_width: usize,
167 /// Literals in the slab: the step count times the step width.
168 literal_count: usize,
169
170 /// Returns the sizes a trace needs for `limits`. The solver and `init` size a trace from it
171 /// before anything is allocated. The call returns `error.CapacityOverflow` when the step
172 /// count, the literal count or the slab's byte size overflows `usize`.
173 pub fn derive(limits: Limits) error{CapacityOverflow}!Capacity {
174 const steps = std.math.add(usize, limits.conflicts, 2) catch
175 return error.CapacityOverflow;
176 const literal_count = std.math.mul(usize, steps, limits.variables) catch
177 return error.CapacityOverflow;
178 _ = std.math.mul(usize, literal_count, @sizeOf(Literal)) catch
179 return error.CapacityOverflow;
180 assert(steps > limits.conflicts);
181 assert(literal_count == steps * limits.variables);
182 return .{
183 .steps = steps,
184 .step_width = limits.variables,
185 .literal_count = literal_count,
186 };
187 }
188 };
189
190 /// Returns a trace in `.initialization` whose slab comes from `allocator`, with every step
191 /// free. The solver builds its trace with it at the start of a solve whose conflict limit or
192 /// variable count needs more room than its current trace has. The call returns
193 /// `error.CapacityOverflow` from `Capacity.derive` and `error.OutOfMemory` from the allocator.
194 /// The caller passes the same allocator to `deinit`.
195 pub fn init(allocator: Allocator, limits: Limits) !Trace {
196 const capacity = try Capacity.derive(limits);
197 const slab = try allocator.alloc(Literal, capacity.literal_count);
198 return .{
199 .phase = .initialization,
200 .capacity = capacity,
201 .slab = slab,
202 .step_count = 0,
203 .literal_count = 0,
204 };
205 }
206
207 /// Moves the trace from `.initialization` to `.steady`, after which the trace calls no
208 /// allocator until `deinit`. The solver calls it once, right after `init`. The call asserts
209 /// that the trace is as `init` left it.
210 pub fn activate(self: *Trace) void {
211 assert(self.phase == .initialization);
212 assert(self.slab.len == self.capacity.literal_count);
213 assert(self.step_count == 0);
214 assert(self.literal_count == 0);
215 self.phase = .steady;
216 }
217
218 /// Returns true when the trace's step count, step width and literal count are each at least
219 /// those of `required`. The solver keeps its trace across solves while the trace admits what
220 /// the next solve needs. The call asserts that the trace is `.steady`.
221 pub fn admits(self: *const Trace, required: Capacity) bool {
222 assert(self.phase == .steady);
223 if (self.capacity.steps < required.steps) return false;
224 if (self.capacity.step_width < required.step_width) return false;
225 return self.capacity.literal_count >= required.literal_count;
226 }
227
228 /// Returns the number of steps still free since the last `clear`. A caller checks how many
229 /// steps remain before the trace is full.
230 pub fn freeSteps(self: *const Trace) usize {
231 assert(self.phase == .steady);
232 assert(self.step_count <= self.capacity.steps);
233 return self.capacity.steps - self.step_count;
234 }
235
236 /// Returns true when `literals` starts inside the slab. The solver checks, before it clears its
237 /// proof trace, that every nonempty step it holds lives in the slab. The call works in any
238 /// phase before `.teardown`.
239 pub fn owns(self: *const Trace, literals: []const Literal) bool {
240 assert(self.phase != .teardown);
241 const base = @intFromPtr(self.slab.ptr);
242 const address = @intFromPtr(literals.ptr);
243 if (address < base) return false;
244 return address < base + self.slab.len * @sizeOf(Literal);
245 }
246
247 /// Copies `literals` after the last step, counts one step, and returns the copy. The solver
248 /// records each nonempty proof step through it. The call asserts that the trace is `.steady`,
249 /// that `literals` holds from 1 to `step_width` literals and lies outside the slab, and that a
250 /// step and enough slab room are free, because a full trace is a sizing bug.
251 pub fn acquire(self: *Trace, literals: []const Literal) []Literal {
252 assert(self.phase == .steady);
253 assert(literals.len >= 1);
254 assert(literals.len <= self.capacity.step_width);
255 assert(self.step_count < self.capacity.steps);
256 assert(self.literal_count + literals.len <= self.capacity.literal_count);
257 assert(!self.owns(literals));
258 const target = self.slab[self.literal_count .. self.literal_count + literals.len];
259 @memcpy(target, literals);
260 self.step_count += 1;
261 self.literal_count += literals.len;
262 return target;
263 }
264
265 /// Counts one empty step and returns an empty slice at the end of the packed literals. The
266 /// solver records the final empty clause of a refutation through it. The call asserts that the
267 /// trace is `.steady` and that a step is free.
268 pub fn acquireEmpty(self: *Trace) []Literal {
269 assert(self.phase == .steady);
270 assert(self.step_count < self.capacity.steps);
271 self.step_count += 1;
272 return self.slab[self.literal_count..self.literal_count];
273 }
274
275 /// Takes back the most recent step, which has to be `literals` and has to hold at least one
276 /// literal. The solver takes back the step of a learned clause that it then fails to store. The
277 /// call asserts that the trace is `.steady` and that `literals` ends where the packed literals
278 /// end.
279 pub fn releaseLast(self: *Trace, literals: []Literal) void {
280 assert(self.phase == .steady);
281 assert(literals.len >= 1);
282 assert(self.step_count > 0);
283 assert(self.literal_count >= literals.len);
284 assert(self.owns(literals));
285 const cursor = @intFromPtr(self.slab.ptr) + self.literal_count * @sizeOf(Literal);
286 assert(@intFromPtr(literals.ptr) + literals.len * @sizeOf(Literal) == cursor);
287 self.step_count -= 1;
288 self.literal_count -= literals.len;
289 }
290
291 /// Drops every step, so the next step starts at the beginning of the slab. The solver clears it
292 /// whenever it clears its proof trace: at the start of each solve and at each change that makes
293 /// the trace stale. Slices handed out before the call are overwritten by later steps. The call
294 /// asserts that the trace is `.steady`.
295 pub fn clear(self: *Trace) void {
296 assert(self.phase == .steady);
297 assert(self.literal_count <= self.capacity.literal_count);
298 self.step_count = 0;
299 self.literal_count = 0;
300 }
301
302 /// Frees the slab with `allocator` and leaves the trace undefined. The solver calls it when it
303 /// replaces its trace, when it drops the trace after the conflict limit is removed, and when it
304 /// is freed itself. `allocator` has to be the one given to `init`. Every slice the trace handed
305 /// out becomes invalid.
306 pub fn deinit(self: *Trace, allocator: Allocator) void {
307 assert(self.phase != .teardown);
308 self.phase = .teardown;
309 allocator.free(self.slab);
310 self.* = undefined;
311 }
312 };
313
314 comptime {
315 alloc_phase.capacity.requireAllocatorExactOwnerShape(Trace);
316 }
317
318 test "proof trace capacity matches an independent typed-byte model" {
319 comptime {
320 @stardustClaim(
321 @import("alloc_phase").capacity.witness(Trace, "smt_trace_capacity_capacity_model"),
322 null,
323 null,
324 null,
325 null,
326 null,
327 null,
328 );
329 }
330 comptime {
331 @stardustClaim(
332 @import("alloc_phase").capacity.witness(Trace, "smt_trace_capacity_overload"),
333 null,
334 null,
335 null,
336 null,
337 null,
338 null,
339 );
340 }
341
342 const limits = Trace.Limits.inspect(2_000, 96);
343 const capacity = try Trace.Capacity.derive(limits);
344 try std.testing.expectEqual(@as(usize, 2_002), capacity.steps);
345 try std.testing.expectEqual(@as(usize, 96), capacity.step_width);
346 try std.testing.expectEqual(@as(usize, 2_002 * 96), capacity.literal_count);
347
348 const zero_budget = try Trace.Capacity.derive(Trace.Limits.inspect(0, 8));
349 try std.testing.expectEqual(@as(usize, 2), zero_budget.steps);
350 try std.testing.expectEqual(@as(usize, 16), zero_budget.literal_count);
351
352 try std.testing.expectError(
353 error.CapacityOverflow,
354 Trace.Capacity.derive(Trace.Limits.inspect(std.math.maxInt(usize) - 1, 8)),
355 );
356 try std.testing.expectError(
357 error.CapacityOverflow,
358 Trace.Capacity.derive(Trace.Limits.inspect(8, std.math.maxInt(usize) - 1)),
359 );
360 try std.testing.expectError(
361 error.CapacityOverflow,
362 Trace.Capacity.derive(Trace.Limits.inspect(std.math.maxInt(u64) / 2, 4)),
363 );
364 }
365
366 fn checkTraceInitFailures(allocator: Allocator, limits: Trace.Limits) !void {
367 var owner = try Trace.init(allocator, limits);
368 defer owner.deinit(allocator);
369 try std.testing.expectEqual(alloc_phase.capacity.Phase.initialization, owner.phase);
370 }
371
372 test "proof trace init cleans every allocation failure and retries" {
373 comptime {
374 @stardustClaim(
375 @import("alloc_phase").capacity.witness(Trace, "smt_trace_oom_retry"),
376 null,
377 null,
378 null,
379 null,
380 null,
381 null,
382 );
383 }
384
385 const limits = Trace.Limits.inspect(4, 6);
386 try std.testing.checkAllAllocationFailures(
387 std.testing.allocator,
388 checkTraceInitFailures,
389 .{limits},
390 );
391
392 var owner = try Trace.init(std.testing.allocator, limits);
393 defer owner.deinit(std.testing.allocator);
394 owner.activate();
395 try std.testing.expectEqual(@as(usize, 6), owner.freeSteps());
396 }
397
398 test "proof trace fills to capacity with stable pointers and zero steady operations" {
399 comptime {
400 @stardustClaim(
401 @import("alloc_phase").capacity.witness(Trace, "smt_trace_sealed_fill_overload"),
402 null,
403 null,
404 null,
405 null,
406 null,
407 null,
408 );
409 }
410 comptime {
411 @stardustClaim(
412 @import("alloc_phase").capacity.witness(Trace, "smt_trace_sealed_fill_foreign_risk"),
413 null,
414 null,
415 null,
416 null,
417 null,
418 null,
419 );
420 }
421
422 var failing = std.testing.FailingAllocator.init(std.testing.allocator, .{});
423 var owner = try Trace.init(failing.allocator(), Trace.Limits.inspect(2, 3));
424 defer owner.deinit(failing.allocator());
425 owner.activate();
426 try std.testing.expectEqual(@as(usize, 4), owner.freeSteps());
427
428 failing.fail_index = failing.alloc_index;
429 failing.resize_fail_index = failing.resize_index;
430
431 const pattern = [_]Literal{ Literal.positive(0), Literal.negative(1), Literal.positive(2) };
432 const first = owner.acquire(pattern[0..3]);
433 const second = owner.acquire(pattern[0..2]);
434 const third = owner.acquire(pattern[0..1]);
435 const final = owner.acquireEmpty();
436 try std.testing.expectEqual(@as(usize, 0), owner.freeSteps());
437 try std.testing.expectEqual(@as(usize, 6), owner.literal_count);
438 try std.testing.expect(owner.owns(first));
439 try std.testing.expect(owner.owns(second));
440 try std.testing.expect(owner.owns(third));
441 try std.testing.expectEqual(@as(usize, 0), final.len);
442 try std.testing.expectEqual(first.ptr + 3, second.ptr);
443 try std.testing.expectEqual(@as(u32, Literal.positive(0).raw), second[0].raw);
444
445 owner.clear();
446 try std.testing.expectEqual(@as(usize, 4), owner.freeSteps());
447 const refilled = owner.acquire(pattern[0..2]);
448 try std.testing.expectEqual(first.ptr, refilled.ptr);
449 try std.testing.expectEqual(@as(usize, 2), owner.literal_count);
450
451 owner.releaseLast(refilled);
452 try std.testing.expectEqual(@as(usize, 4), owner.freeSteps());
453 try std.testing.expectEqual(@as(usize, 0), owner.literal_count);
454 try std.testing.expect(!failing.has_induced_failure);
455 }