lib/sql/src/properties/store.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const hypothesis = @import("hypothesis");
3 const sql = @import("sql");
4
5 const Store = sql.Store;
6
7 const key_count = 10;
8
9 const SnapshotModel = struct {
10 generation: u64,
11 values: [key_count]?u8,
12 };
13
14 pub fn settings() hypothesis.Settings {
15 return hypothesis.Settings.quick()
16 .withSeed(0x71DB_2026)
17 .withDatabase("zig-out/hypothesis-failures/sql");
18 }
19
20 fn drawUsize(conjecture: *hypothesis.ConjectureData, min: usize, max: usize, shrink_towards: usize) !usize {
21 return @intCast(try conjecture.drawInteger(
22 @intCast(min),
23 @intCast(max),
24 @intCast(shrink_towards),
25 ));
26 }
27
28 fn keyByte(index: usize) u8 {
29 return @intCast(index);
30 }
31
32 fn expectModel(store: *const Store, values: [key_count]?u8) !void {
33 var index: usize = 0;
34 while (index < key_count) : (index += 1) {
35 const key_bytes = [_]u8{keyByte(index)};
36 const actual = store.get(&key_bytes);
37 if (values[index]) |expected| {
38 try std.testing.expect(actual != null);
39 try std.testing.expectEqual(expected, actual.?[0]);
40 } else {
41 try std.testing.expect(actual == null);
42 }
43 }
44
45 var range = try store.range(null, null);
46 var previous: ?u8 = null;
47 while (range.next()) |entry| {
48 try std.testing.expect(entry.key.len == 1);
49 try std.testing.expect(entry.value.len == 1);
50 const key_value = entry.key[0];
51 if (previous) |prev| try std.testing.expect(prev < key_value);
52 previous = key_value;
53 try std.testing.expect(values[key_value] != null);
54 try std.testing.expectEqual(values[key_value].?, entry.value[0]);
55 }
56 }
57
58 fn expectSnapshot(store: *const Store, snapshot: SnapshotModel) !void {
59 var range = try store.rangeAt(null, null, snapshot.generation);
60 var seen = @as([key_count]bool, @splat(false));
61 while (range.next()) |entry| {
62 try std.testing.expect(entry.key.len == 1);
63 const key_value = entry.key[0];
64 seen[key_value] = true;
65 try std.testing.expect(snapshot.values[key_value] != null);
66 try std.testing.expectEqual(snapshot.values[key_value].?, entry.value[0]);
67 }
68
69 var index: usize = 0;
70 while (index < key_count) : (index += 1) {
71 const key_bytes = [_]u8{keyByte(index)};
72 const actual = store.getAt(&key_bytes, snapshot.generation);
73 if (snapshot.values[index]) |expected| {
74 try std.testing.expect(seen[index]);
75 try std.testing.expect(actual != null);
76 try std.testing.expectEqual(expected, actual.?[0]);
77 } else {
78 try std.testing.expect(!seen[index]);
79 try std.testing.expect(actual == null);
80 }
81 }
82 }
83
84 pub const StateProperty = struct {
85 pub fn property(conjecture: *hypothesis.ConjectureData, allocator: std.mem.Allocator) !void {
86 var store = Store.init(allocator);
87 defer store.deinit();
88
89 var model = @as([key_count]?u8, @splat(null));
90 var snapshots: std.ArrayList(SnapshotModel) = .empty;
91 defer snapshots.deinit(allocator);
92
93 const steps = try drawUsize(conjecture, 1, 120, 20);
94 var step: usize = 0;
95 while (step < steps) : (step += 1) {
96 const op = try drawUsize(conjecture, 0, 99, 0);
97 const slot = try drawUsize(conjecture, 0, key_count - 1, 0);
98 const key_bytes = [_]u8{keyByte(slot)};
99 if (op < 50) {
100 const value = [_]u8{@intCast(try drawUsize(conjecture, 0, 255, 0))};
101 var tx = store.beginWrite();
102 defer tx.deinit();
103 try tx.put(&key_bytes, &value);
104 _ = try tx.commit();
105 model[slot] = value[0];
106 } else if (op < 70) {
107 var tx = store.beginWrite();
108 defer tx.deinit();
109 try tx.delete(&key_bytes);
110 _ = try tx.commit();
111 model[slot] = null;
112 } else if (op < 85) {
113 try snapshots.append(allocator, .{
114 .generation = store.currentGeneration(),
115 .values = model,
116 });
117 } else {
118 try expectModel(&store, model);
119 }
120
121 try expectModel(&store, model);
122 for (snapshots.items) |snapshot| try expectSnapshot(&store, snapshot);
123 }
124 }
125 };
126
127 test "property: ordered MVCC store matches the bounded model" {
128 if (!@import("sql_test_options").run_property_tests) return error.SkipZigTest;
129
130 try hypothesis.checkNamed(StateProperty, "sql-state", settings());
131 }