lib/machine/src/explore/model.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const fabric = @import("../fabric/root.zig");
2 const fault = @import("../fault/root.zig");
3 const profile = @import("../profile/root.zig");
4 const std = @import("std");
5
6 const Sha256 = std.crypto.hash.sha2.Sha256;
7 const ChoiceError = error{
8 ChoiceOutOfRange,
9 InvalidPlan,
10 StaleChoiceSite,
11 };
12
13 pub const GeneratorError: type = profile.Error || ChoiceError;
14
15 pub const Stream = enum(u8) {
16 input = 1,
17 schedule = 2,
18 topology = 3,
19 fault = 4,
20 };
21
22 pub const SeedDialect = enum(u8) {
23 sha256_v1 = 1,
24 };
25
26 pub const Seed = struct {
27 dialect: SeedDialect = .sha256_v1,
28 bytes: [32]u8,
29
30 pub fn fromU64(value: u64) Seed {
31 var bytes: [32]u8 = @splat(0);
32 std.mem.writeInt(u64, bytes[0..8], value, .little);
33 return .{ .bytes = bytes };
34 }
35
36 pub fn digest(
37 self: Seed,
38 stream: Stream,
39 sequence: u16,
40 lane: u8,
41 ) [Sha256.digest_length]u8 {
42 var hasher = Sha256.init(.{});
43 hasher.update("tiny.machine.explore.seed/v1");
44 hasher.update(&.{@backingInt(self.dialect)});
45 hasher.update(&self.bytes);
46 hasher.update(&.{@backingInt(stream)});
47 var encoded: [3]u8 = undefined;
48 std.mem.writeInt(u16, encoded[0..2], sequence, .little);
49 encoded[2] = lane;
50 hasher.update(&encoded);
51 var result: [Sha256.digest_length]u8 = undefined;
52 hasher.final(&result);
53 return result;
54 }
55
56 pub fn word(
57 self: Seed,
58 stream: Stream,
59 sequence: u16,
60 lane: u8,
61 ) u64 {
62 const bytes = self.digest(stream, sequence, lane);
63 return std.mem.readInt(u64, bytes[0..8], .little);
64 }
65
66 pub fn suggest(
67 self: Seed,
68 stream: Stream,
69 sequence: u16,
70 alternative_count: u8,
71 ) u8 {
72 std.debug.assert(alternative_count > 0);
73 const count: u64 = alternative_count;
74 const selected = self.word(stream, sequence, 0) % count;
75 std.debug.assert(selected < alternative_count);
76 return @intCast(selected);
77 }
78 };
79
80 pub const SiteId = struct {
81 stream: Stream,
82 sequence: u16,
83 virtual_time_tick: u64,
84 };
85
86 pub const Origin = struct {
87 source: profile.DeterminismSource,
88 version: u16,
89 };
90
91 pub fn origin(source: profile.DeterminismSource) Origin {
92 const declared = profile.determinism.entry(source);
93 std.debug.assert(declared.source == source);
94 std.debug.assert(declared.version > 0);
95 return .{ .source = source, .version = declared.version };
96 }
97
98 pub const IncompleteReason = enum(u8) {
99 step_capacity = 1,
100 alternative_capacity = 2,
101 node_capacity = 3,
102 kind_capacity = 4,
103 event_capacity = 5,
104 virtual_time_bound = 6,
105 };
106
107 pub fn Generation(comptime T: type) type {
108 return union(enum) {
109 item: T,
110 exhausted,
111 incomplete: IncompleteReason,
112 };
113 }
114
115 pub fn ChoiceSite(
116 comptime Alternative: type,
117 comptime alternative_capacity: u8,
118 ) type {
119 return struct {
120 id: SiteId,
121 alternatives: [alternative_capacity]Alternative,
122 count: u8,
123 suggested: u8,
124
125 pub fn values(self: *const @This()) []const Alternative {
126 std.debug.assert(self.count <= self.alternatives.len);
127 return self.alternatives[0..self.count];
128 }
129 };
130 }
131
132 pub const TemporalPlan = struct {
133 steps: u16,
134 start_tick: u64,
135 end_tick: u64,
136 };
137
138 pub const InputCapacity = struct {
139 steps: u16,
140 alternatives: u8,
141 };
142
143 pub const ScheduleCapacity = struct {
144 steps: u16,
145 nodes: u8,
146 alternatives: u8,
147 };
148
149 pub const SchedulePlan = struct {
150 temporal: TemporalPlan,
151 nodes: u8,
152 };
153
154 pub const TopologyCapacity = struct {
155 steps: u16,
156 nodes: u8,
157 alternatives: u8,
158 };
159
160 pub const TopologyPlan = struct {
161 temporal: TemporalPlan,
162 nodes: u8,
163 };
164
165 pub const FaultCapacity = struct {
166 steps: u16,
167 kinds: u8,
168 alternatives: u8,
169 };
170
171 pub const FaultPlan = struct {
172 temporal: TemporalPlan,
173 kinds: []const fault.Kind,
174 };
175
176 pub const EventCapacity = struct {
177 events: u16,
178 };
179
180 pub const OperationOutcome = enum(u8) {
181 succeeded = 1,
182 failed = 2,
183 uncertain = 3,
184 };
185
186 pub const InputPhase = enum(u8) {
187 quiet = 1,
188 burst = 2,
189 };
190
191 pub const InputKind = enum(u8) {
192 wait = 1,
193 terminal = 2,
194 entropy = 3,
195 packet = 4,
196 service_result = 5,
197 effect_result = 6,
198 };
199
200 pub const InputValue = union(InputKind) {
201 wait: u64,
202 terminal: u64,
203 entropy: u64,
204 packet: u64,
205 service_result: OperationOutcome,
206 effect_result: OperationOutcome,
207 };
208
209 pub const InputAlternative = struct {
210 origin: Origin,
211 virtual_time_tick: u64,
212 value: InputValue,
213 };
214
215 pub const GeneratedInput = InputAlternative;
216
217 pub const ScheduleKind = enum(u8) {
218 turn = 1,
219 idle = 2,
220 };
221
222 pub const ScheduleValue = union(ScheduleKind) {
223 turn: u8,
224 idle,
225 };
226
227 pub const ScheduleAlternative = struct {
228 origin: Origin,
229 virtual_time_tick: u64,
230 value: ScheduleValue,
231 };
232
233 pub const GeneratedSchedule = ScheduleAlternative;
234
235 pub const TopologyKind = enum(u8) {
236 node = 1,
237 complete = 2,
238 };
239
240 pub const TopologyNode = struct {
241 id: fabric.NodeId,
242 included: bool,
243 };
244
245 pub const TopologyValue = union(TopologyKind) {
246 node: TopologyNode,
247 complete,
248 };
249
250 pub const TopologyAlternative = struct {
251 origin: Origin,
252 virtual_time_tick: u64,
253 value: TopologyValue,
254 };
255
256 pub const GeneratedTopology = TopologyAlternative;
257
258 pub const FaultAction = union(enum) {
259 healthy,
260 inject: fault.Kind,
261 persist: fault.Kind,
262 recover: fault.Kind,
263 };
264
265 pub const FaultAlternative = struct {
266 choice_origin: Origin,
267 effect_origin: ?Origin,
268 virtual_time_tick: u64,
269 action: FaultAction,
270 };
271
272 pub const GeneratedFault = FaultAlternative;
273
274 pub fn faultOrigin(kind: fault.Kind) Origin {
275 return origin(switch (kind) {
276 .machine_crash => .machine_crash,
277 .process_crash => .process_crash,
278 .io_error => .effect_result,
279 .packet_loss, .packet_delay, .packet_reorder, .partition => .packet_fault,
280 .clock_jump => .virtual_time,
281 .entropy_choice => .entropy_input,
282 .capacity_exhaustion => .capacity_fault,
283 .host_service_failure => .host_service_result,
284 });
285 }
286
287 pub const SemanticId = u64;
288
289 pub const PropertyKind = enum(u8) {
290 safety = 1,
291 bounded_liveness = 2,
292 };
293
294 pub const Bound = union(enum) {
295 steps: u16,
296 virtual_time: u64,
297 };
298
299 pub const Verdict = enum(u8) {
300 holds = 1,
301 violated = 2,
302 unreached = 3,
303 incomplete = 4,
304 };
305
306 pub const EvaluationReason = enum(u8) {
307 satisfied = 1,
308 forbidden_event = 2,
309 response_missing = 3,
310 bound_exceeded = 4,
311 trigger_not_seen = 5,
312 trace_incomplete = 6,
313 declaration_missing = 7,
314 declaration_mismatch = 8,
315 };
316
317 pub const PropertyDeclaration = struct {
318 id: SemanticId,
319 kind: PropertyKind,
320 bound: ?Bound,
321 };
322
323 pub const PropertyEvaluation = struct {
324 id: SemanticId,
325 verdict: Verdict,
326 reason: EvaluationReason,
327 witness: ?u16,
328 };
329
330 pub const Observation = struct {
331 id: SemanticId,
332 value: u64,
333 };
334
335 pub const Operation = struct {
336 id: SemanticId,
337 outcome: OperationOutcome,
338 };
339
340 pub const Diagnostic = struct {
341 id: SemanticId,
342 code: u32,
343 };
344
345 pub const ExternalAdmission = struct {
346 id: SemanticId,
347 origin: Origin,
348 };
349
350 pub const EventValue = union(enum) {
351 controlled_input: GeneratedInput,
352 schedule_choice: GeneratedSchedule,
353 topology_choice: GeneratedTopology,
354 observation: Observation,
355 property_declaration: PropertyDeclaration,
356 property_evaluation: PropertyEvaluation,
357 injected_fault: GeneratedFault,
358 diagnostic: Diagnostic,
359 external_admission: ExternalAdmission,
360 operation: Operation,
361 };
362
363 pub const Event = struct {
364 sequence: u16,
365 virtual_time_tick: u64,
366 value: EventValue,
367 };
368
369 pub const EventClass = enum(u8) {
370 controlled_input = 1,
371 schedule_choice = 2,
372 topology_choice = 3,
373 observation = 4,
374 property_declaration = 5,
375 property_evaluation = 6,
376 injected_fault = 7,
377 diagnostic = 8,
378 external_admission = 9,
379 operation = 10,
380 };
381
382 pub const OperationPattern = struct {
383 id: SemanticId,
384 outcome: ?OperationOutcome = null,
385 };
386
387 pub const EvaluationPattern = struct {
388 id: SemanticId,
389 verdict: ?Verdict = null,
390 };
391
392 pub const Pattern = union(enum) {
393 event_class: EventClass,
394 input: InputKind,
395 schedule: ScheduleKind,
396 topology: TopologyKind,
397 observation: SemanticId,
398 property_declaration: SemanticId,
399 property_evaluation: EvaluationPattern,
400 fault: fault.Kind,
401 diagnostic: SemanticId,
402 external_admission: profile.DeterminismSource,
403 operation: OperationPattern,
404 };
405
406 pub const Safety = struct {
407 property: SemanticId,
408 forbidden: Pattern,
409 };
410
411 pub const BoundedLiveness = struct {
412 property: SemanticId,
413 trigger: Pattern,
414 response: Pattern,
415 bound: Bound,
416 };
417
418 pub const TraceState = enum(u8) {
419 open = 1,
420 exhausted = 2,
421 incomplete = 3,
422 };
423
424 pub const TraceCompletion = enum(u8) {
425 exhausted = 1,
426 incomplete = 2,
427 };