lib/quic/src/properties/sim.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const hypothesis = @import("hypothesis");
3 const quic = @import("quic");
4
5 const sim = quic.sim;
6 const property_seed: u64 = 0x7175_6963_7369_6d03;
7
8 fn settings() hypothesis.Settings {
9 return hypothesis.Settings.quick()
10 .withSeed(property_seed)
11 .withDatabase("zig-out/hypothesis-failures/quic-sim");
12 }
13
14 fn Harness(comptime limits: sim.Limits) type {
15 const capacity = comptime sim.Capacity.derive(limits) catch unreachable;
16 return struct {
17 bytes: [capacity.storage_bytes]u8 align(sim.Memory.storage_alignment),
18 memory: sim.Memory,
19 link: sim.Link,
20
21 const Self = @This();
22
23 fn init(self: *Self, seed: u64, a_to_b: sim.Policy, b_to_a: sim.Policy) !void {
24 self.memory = try sim.Memory.init(&self.bytes, limits);
25 self.link = try sim.Link.init(limits, &self.memory, seed, a_to_b, b_to_a);
26 }
27
28 fn deinit(self: *Self) void {
29 _ = self.memory.deinit();
30 }
31 };
32 }
33
34 fn drawPolicy(data: *hypothesis.ConjectureData) !sim.Policy {
35 const delay_min = try data.drawInteger(0, 20, 0);
36 const delay_width = try data.drawInteger(0, 20, 0);
37 return .{
38 .loss_permille = @intCast(try data.drawInteger(0, 1000, 0)),
39 .duplicate_permille = @intCast(try data.drawInteger(0, 1000, 0)),
40 .reorder_permille = @intCast(try data.drawInteger(0, 1000, 0)),
41 .delay_min_ns = delay_min,
42 .delay_max_ns = delay_min + delay_width,
43 .mtu = 1,
44 };
45 }
46
47 fn sendSequence(link: *sim.Link, from: sim.End, count: usize) !void {
48 for (0..16) |index| {
49 if (index >= count) break;
50 const byte = [1]u8{@intCast(index)};
51 try link.send(from, &byte, index);
52 }
53 }
54
55 fn drain(link: *sim.Link, at: sim.End, output: []u8) usize {
56 var count: usize = 0;
57 var byte: [1]u8 = undefined;
58 for (0..32) |_| {
59 const delivery_at = link.nextDeliveryAt(at) orelse break;
60 _ = link.receive(at, delivery_at, &byte).?;
61 output[count] = byte[0];
62 count += 1;
63 }
64 return count;
65 }
66
67 const ZeroSequence = struct {
68 pub fn property(data: *hypothesis.ConjectureData, _: std.mem.Allocator) !void {
69 const limits = sim.Limits{ .queue_capacity = 16, .datagram_capacity = 1 };
70 const count: usize = @intCast(try data.drawInteger(0, 16, 0));
71 var harness: Harness(limits) = undefined;
72 try harness.init(1, .{}, .{});
73 defer harness.deinit();
74 try sendSequence(&harness.link, .a, count);
75 var delivered: [16]u8 = undefined;
76 const delivered_count = drain(&harness.link, .b, &delivered);
77 try std.testing.expectEqual(count, delivered_count);
78 for (0..16) |index| {
79 if (index >= count) break;
80 try std.testing.expectEqual(@as(u8, @intCast(index)), delivered[index]);
81 }
82 }
83 };
84
85 test "property: zero simulator policy preserves the sent sequence" {
86 try hypothesis.checkNamed(ZeroSequence, "quic-sim-zero-sequence", settings());
87 }
88
89 const DeliveryMultiset = struct {
90 pub fn property(data: *hypothesis.ConjectureData, _: std.mem.Allocator) !void {
91 const limits = sim.Limits{ .queue_capacity = 32, .datagram_capacity = 1 };
92 const count: usize = @intCast(try data.drawInteger(0, 16, 0));
93 const policy = try drawPolicy(data);
94 var harness: Harness(limits) = undefined;
95 try harness.init(try data.drawInteger(0, std.math.maxInt(u64), 0), policy, .{});
96 defer harness.deinit();
97 try sendSequence(&harness.link, .a, count);
98 var delivered: [32]u8 = undefined;
99 const delivered_count = drain(&harness.link, .b, &delivered);
100 var occurrences: [16]u2 = @splat(0);
101 for (delivered[0..delivered_count]) |value| {
102 try std.testing.expect(value < count);
103 try std.testing.expect(occurrences[value] < 2);
104 occurrences[value] += 1;
105 }
106 const stats = harness.link.stats(.a);
107 try std.testing.expectEqual(stats.sent - stats.lost + stats.duplicated, delivered_count);
108 }
109 };
110
111 test "property: impaired delivery is a duplicated sub-multiset of sent datagrams" {
112 try hypothesis.checkNamed(DeliveryMultiset, "quic-sim-multiset", settings());
113 }
114
115 const PayloadIntegrity = struct {
116 pub fn property(data: *hypothesis.ConjectureData, _: std.mem.Allocator) !void {
117 const limits = sim.Limits{ .queue_capacity = 4, .datagram_capacity = 64 };
118 const length: usize = @intCast(try data.drawInteger(1, 64, 1));
119 const lengths = [2]usize{ length, limits.datagram_capacity - length + 1 };
120 var payloads: [2][limits.datagram_capacity]u8 = undefined;
121 for (0..2) |payload_index| {
122 for (0..limits.datagram_capacity) |byte_index| {
123 if (byte_index >= lengths[payload_index]) break;
124 payloads[payload_index][byte_index] = @intCast(
125 try data.drawInteger(0, 255, 0),
126 );
127 }
128 payloads[payload_index][0] = @intCast(0xa1 + payload_index);
129 }
130 const policy = try drawPayloadPolicy(data, limits.datagram_capacity);
131 var harness: Harness(limits) = undefined;
132 try harness.init(try data.drawInteger(0, std.math.maxInt(u64), 0), policy, .{});
133 defer harness.deinit();
134 for (0..2) |index| try harness.link.send(.a, payloads[index][0..lengths[index]], index);
135 var out: [limits.datagram_capacity]u8 = undefined;
136 var occurrences: [2]u2 = @splat(0);
137 for (0..4) |_| {
138 const delivery_at = harness.link.nextDeliveryAt(.b) orelse break;
139 const received = harness.link.receive(.b, delivery_at, &out).?;
140 const payload_index: usize = out[0] - 0xa1;
141 try std.testing.expect(payload_index < payloads.len);
142 try std.testing.expectEqual(lengths[payload_index], received);
143 try std.testing.expectEqualSlices(
144 u8,
145 payloads[payload_index][0..received],
146 out[0..received],
147 );
148 occurrences[payload_index] += 1;
149 try std.testing.expect(occurrences[payload_index] <= 2);
150 }
151 try std.testing.expectEqual(@as(?u64, null), harness.link.nextDeliveryAt(.b));
152 }
153 };
154
155 fn drawPayloadPolicy(data: *hypothesis.ConjectureData, mtu: u16) !sim.Policy {
156 var policy = try drawPolicy(data);
157 policy.mtu = mtu;
158 return policy;
159 }
160
161 test "property: impaired delivery preserves every payload byte" {
162 try hypothesis.checkNamed(PayloadIntegrity, "quic-sim-payload-integrity", settings());
163 }
164
165 fn compareDirection(first: *sim.Link, second: *sim.Link, at: sim.End) !void {
166 var first_out: [1]u8 = undefined;
167 var second_out: [1]u8 = undefined;
168 for (0..32) |_| {
169 const first_at = first.nextDeliveryAt(at);
170 const second_at = second.nextDeliveryAt(at);
171 try std.testing.expectEqual(first_at, second_at);
172 const delivery_at = first_at orelse break;
173 const first_len = first.receive(at, delivery_at, &first_out).?;
174 const second_len = second.receive(at, delivery_at, &second_out).?;
175 try std.testing.expectEqual(first_len, second_len);
176 try std.testing.expectEqualSlices(u8, first_out[0..first_len], second_out[0..second_len]);
177 }
178 }
179
180 const DeterministicSchedule = struct {
181 pub fn property(data: *hypothesis.ConjectureData, _: std.mem.Allocator) !void {
182 const limits = sim.Limits{ .queue_capacity = 32, .datagram_capacity = 1 };
183 const count: usize = @intCast(try data.drawInteger(0, 16, 0));
184 const seed = try data.drawInteger(0, std.math.maxInt(u64), 0);
185 const a_to_b = try drawPolicy(data);
186 const b_to_a = try drawPolicy(data);
187 var first: Harness(limits) = undefined;
188 var second: Harness(limits) = undefined;
189 try first.init(seed, a_to_b, b_to_a);
190 defer first.deinit();
191 try second.init(seed, a_to_b, b_to_a);
192 defer second.deinit();
193 for (0..16) |index| {
194 if (index >= count) break;
195 const byte = [1]u8{@intCast(index)};
196 const from: sim.End = if (index % 2 == 0) .a else .b;
197 try first.link.send(from, &byte, index);
198 try second.link.send(from, &byte, index);
199 }
200 try compareDirection(&first.link, &second.link, .a);
201 try compareDirection(&first.link, &second.link, .b);
202 try std.testing.expectEqual(first.link.stats(.a), second.link.stats(.a));
203 try std.testing.expectEqual(first.link.stats(.b), second.link.stats(.b));
204 }
205 };
206
207 test "property: equal seeds policies and inputs produce equal schedules" {
208 try hypothesis.checkNamed(DeterministicSchedule, "quic-sim-determinism", settings());
209 }
210
211 const NextDelivery = struct {
212 pub fn property(data: *hypothesis.ConjectureData, _: std.mem.Allocator) !void {
213 const limits = sim.Limits{ .queue_capacity = 32, .datagram_capacity = 1 };
214 const count: usize = @intCast(try data.drawInteger(1, 16, 1));
215 var policy = try drawPolicy(data);
216 policy.loss_permille = 0;
217 var harness: Harness(limits) = undefined;
218 try harness.init(try data.drawInteger(0, std.math.maxInt(u64), 0), policy, .{});
219 defer harness.deinit();
220 try sendSequence(&harness.link, .a, count);
221 var out: [1]u8 = undefined;
222 for (0..32) |_| {
223 const delivery_at = harness.link.nextDeliveryAt(.b) orelse break;
224 if (delivery_at > 0) {
225 try std.testing.expectEqual(
226 @as(?usize, null),
227 harness.link.receive(.b, delivery_at - 1, &out),
228 );
229 }
230 try std.testing.expect(harness.link.receive(.b, delivery_at, &out) != null);
231 }
232 try std.testing.expectEqual(@as(?u64, null), harness.link.nextDeliveryAt(.b));
233 }
234 };
235
236 test "property: next delivery time is the next datagram deadline" {
237 try hypothesis.checkNamed(NextDelivery, "quic-sim-next-delivery", settings());
238 }
239
240 const MonotonicClock = struct {
241 pub fn property(data: *hypothesis.ConjectureData, _: std.mem.Allocator) !void {
242 var clock = sim.Clock{ .now_ns = try data.drawInteger(0, std.math.maxInt(u64), 0) };
243 for (0..16) |_| {
244 const previous = clock.now_ns;
245 clock.advance(try data.drawInteger(0, std.math.maxInt(u64), 0));
246 try std.testing.expect(clock.now_ns >= previous);
247 }
248 }
249 };
250
251 test "property: manual clock never moves backward" {
252 try hypothesis.checkNamed(MonotonicClock, "quic-sim-clock", settings());
253 }
254
255 const DropPattern = struct {
256 pub fn property(data: *hypothesis.ConjectureData, _: std.mem.Allocator) !void {
257 const limits = sim.Limits{ .queue_capacity = 32, .datagram_capacity = 1 };
258 const count: usize = @intCast(try data.drawInteger(0, 16, 0));
259 const pattern = try data.drawInteger(0, std.math.maxInt(u64), 0);
260 const seed = try data.drawInteger(0, std.math.maxInt(u64), 0);
261 const policy = try drawPolicy(data);
262 var dropped: Harness(limits) = undefined;
263 try dropped.init(seed, policy, .{});
264 defer dropped.deinit();
265 var reference: Harness(limits) = undefined;
266 try reference.init(seed, policy, .{});
267 defer reference.deinit();
268 dropped.link.dropNext(.a, pattern);
269 for (0..16) |index| {
270 if (index >= count) break;
271 const byte = [1]u8{@intCast(index)};
272 try dropped.link.send(.a, &byte, index);
273 if ((pattern >> @intCast(index)) & 1 == 0) {
274 try reference.link.send(.a, &byte, index);
275 }
276 }
277 try compareDirection(&dropped.link, &reference.link, .b);
278 const window = (@as(u64, 1) << @intCast(count)) - 1;
279 const masked: u64 = @popCount(pattern & window);
280 const dropped_stats = dropped.link.stats(.a);
281 const reference_stats = reference.link.stats(.a);
282 try std.testing.expectEqual(reference_stats.sent + masked, dropped_stats.sent);
283 try std.testing.expectEqual(reference_stats.lost + masked, dropped_stats.lost);
284 }
285 };
286
287 test "property: a drop pattern removes its datagrams and leaves the seeded schedule intact" {
288 try hypothesis.checkNamed(DropPattern, "quic-sim-drop-pattern", settings());
289 }