tiny.smt.sat.trace

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

1//! Fixed memory for the proof steps of one solve, used when the solve has a conflict limit. A2//! solver records a proof step for each clause it learns, and a caller that bounds a search by a3//! 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 per6//! variable, so a conflict limit bounds the steps and their literals, with room left for the final7//! empty clause. The steps of a solve are dropped all at once when the solver clears them, and the8//! 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 (a11//! slab), with room for the conflict limit plus 2 steps, each at most as wide as the variable12//! count. Adding a step copies its literals after the last one, clearing resets two counters, and13//! taking back a step drops the last one, so no operation after setup calls an allocator. Adding a14//! 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 the16//! extra solves of core minimization. A compile-time record of this memory (`Trace.claim`) states17//! the size equation and the overload behavior, and the shape check at the end of the file18//! validates it.19const std = @import("std");20const alloc_phase = @import("alloc_phase");21const types = @import("types.zig");2223const assert = std.debug.assert;24const Allocator = std.mem.Allocator;25const Literal = types.Literal;2627/// Fixed memory for the literals of one solve's proof steps, packed end to end in one slab, with28/// 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` moves30/// the trace from `.initialization` to `.steady`, and `deinit` moves it to `.teardown` and frees31/// the slab. In `.steady`, adding, taking back and clearing steps call no allocator, and adding a32/// 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.34pub 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 witness37    /// each obligation. The shape check at the end of the file validates the record and the trace's38    /// shape at compile time. The equation gives the conflict limit plus 2, times the variable39    /// 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's41    /// list of steps, the proof assumptions, the steps of solves whose conflict limit is null and42    /// 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` and133    /// the solver's reservation of its step list read them.134    capacity: Capacity,135    slab: []Literal,136    step_count: usize,137    literal_count: usize,138139    /// 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 each141    /// 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,147148        /// Returns the limits for `conflicts` and `variables`. The solver builds its trace limits149        /// through it.150        pub fn inspect(conflicts: usize, variables: usize) Limits {151            return .{152                .conflicts = conflicts,153                .variables = variables,154            };155        }156    };157158    /// The sizes of one trace: its step count, its step width in literals and its total literal159    /// count. The solver derives the sizes a solve needs and asks its current trace whether it160    /// `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 every163        /// 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,169170        /// Returns the sizes a trace needs for `limits`. The solver and `init` size a trace from it171        /// before anything is allocated. The call returns `error.CapacityOverflow` when the step172        /// 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) catch175                return error.CapacityOverflow;176            const literal_count = std.math.mul(usize, steps, limits.variables) catch177                return error.CapacityOverflow;178            _ = std.math.mul(usize, literal_count, @sizeOf(Literal)) catch179                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    };189190    /// Returns a trace in `.initialization` whose slab comes from `allocator`, with every step191    /// free. The solver builds its trace with it at the start of a solve whose conflict limit or192    /// variable count needs more room than its current trace has. The call returns193    /// `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    }206207    /// Moves the trace from `.initialization` to `.steady`, after which the trace calls no208    /// allocator until `deinit`. The solver calls it once, right after `init`. The call asserts209    /// 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    }217218    /// Returns true when the trace's step count, step width and literal count are each at least219    /// those of `required`. The solver keeps its trace across solves while the trace admits what220    /// 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    }227228    /// Returns the number of steps still free since the last `clear`. A caller checks how many229    /// 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    }235236    /// Returns true when `literals` starts inside the slab. The solver checks, before it clears its237    /// proof trace, that every nonempty step it holds lives in the slab. The call works in any238    /// 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    }246247    /// Copies `literals` after the last step, counts one step, and returns the copy. The solver248    /// 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 a250    /// 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    }264265    /// Counts one empty step and returns an empty slice at the end of the packed literals. The266    /// solver records the final empty clause of a refutation through it. The call asserts that the267    /// 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    }274275    /// Takes back the most recent step, which has to be `literals` and has to hold at least one276    /// literal. The solver takes back the step of a learned clause that it then fails to store. The277    /// call asserts that the trace is `.steady` and that `literals` ends where the packed literals278    /// 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    }290291    /// Drops every step, so the next step starts at the beginning of the slab. The solver clears it292    /// whenever it clears its proof trace: at the start of each solve and at each change that makes293    /// the trace stale. Slices handed out before the call are overwritten by later steps. The call294    /// 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    }301302    /// Frees the slab with `allocator` and leaves the trace undefined. The solver calls it when it303    /// replaces its trace, when it drops the trace after the conflict limit is removed, and when it304    /// is freed itself. `allocator` has to be the one given to `init`. Every slice the trace handed305    /// 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};313314comptime {315    alloc_phase.capacity.requireAllocatorExactOwnerShape(Trace);316}317318test "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    }341342    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);347348    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);351352    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}365366fn 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}371372test "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    }384385    const limits = Trace.Limits.inspect(4, 6);386    try std.testing.checkAllAllocationFailures(387        std.testing.allocator,388        checkTraceInitFailures,389        .{limits},390    );391392    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}397398test "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    }421422    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());427428    failing.fail_index = failing.alloc_index;429    failing.resize_fail_index = failing.resize_index;430431    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);444445    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);450451    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}