lib/machine/src/profile/determinism.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2
3 const Sha256 = std.crypto.hash.sha2.Sha256;
4
5 /// The eleven families a divergence source can belong to are categories, so a reader
6 /// sees which part of the machine a source comes from: CPU instructions, CPUID features,
7 /// scheduler choices, interrupts, devices, the clock, entropy, packets, host services,
8 /// the test driver, and external results.
9 /// Each inventory entry records its source's category.
10 pub const Category = enum(u8) {
11 cpu_instruction = 1,
12 cpuid_feature = 2,
13 scheduler_choice = 3,
14 interrupt = 4,
15 device = 5,
16 clock = 6,
17 entropy = 7,
18 packet = 8,
19 host_service = 9,
20 test_driver = 10,
21 external_result = 11,
22 };
23
24 /// The places where two runs of the same program could differ that the package takes
25 /// responsibility for are divergence sources, so a reader checks a source against
26 /// this list to see whether the package has accounted for it.
27 /// The list holds 42 sources, and the inventory carries exactly one entry per source
28 /// in the same order.
29 pub const Source = enum(u16) {
30 backend_selection = 1,
31 backend_availability = 2,
32 executable_bytes = 3,
33 instruction_forms = 4,
34 instruction_flags = 5,
35 initial_cpu_state = 6,
36 backend_instruction_result = 7,
37 cpuid_vendor = 8,
38 cpuid_signature = 9,
39 cpuid_page_size_extension = 10,
40 cpuid_physical_address_extension = 11,
41 cpuid_conditional_move = 12,
42 cpuid_execute_disable = 13,
43 cpuid_long_mode = 14,
44 cpuid_address_widths = 15,
45 cpuid_leaf_range = 16,
46 guest_schedule = 17,
47 host_run_stutter = 18,
48 guest_interrupt = 19,
49 host_signal_interrupt = 20,
50 channel_device = 21,
51 doorbell_exit = 22,
52 unmodeled_device_exit = 23,
53 cpu_clock_instruction = 24,
54 cpu_entropy_instruction = 25,
55 checkpoint_memory = 26,
56 checkpoint_source = 27,
57 terminal_input = 28,
58 virtual_time = 29,
59 entropy_input = 30,
60 packet_payload = 31,
61 packet_delivery = 32,
62 packet_fault = 33,
63 host_service_result = 34,
64 effect_result = 35,
65 fault_choice = 36,
66 capacity_fault = 37,
67 machine_crash = 38,
68 process_crash = 39,
69 activation_fence = 40,
70 turn_selection = 41,
71 replay_source = 42,
72 };
73
74 /// The named, versioned mechanisms that hold a divergence source fixed are witnesses,
75 /// so a reader follows a name to the mechanism.
76 /// Each name carries its own version, so a strengthened mechanism shows up as a
77 /// new value.
78 pub const Witness = enum(u16) {
79 backend_selection_v1 = 1,
80 backend_availability_v1 = 2,
81 execution_manifest_v1 = 3,
82 instruction_policy_v2 = 4,
83 instruction_flags_v2 = 5,
84 initial_cpu_state_v1 = 6,
85 portable_instruction_result_v1 = 7,
86 cpuid_model_v1 = 8,
87 cooperative_schedule_v2 = 9,
88 portable_no_stutter_v1 = 10,
89 guest_interrupt_exclusion_v1 = 11,
90 portable_no_host_signal_v1 = 12,
91 channel_device_v1 = 13,
92 doorbell_completion_v1 = 14,
93 unmodeled_device_rejection_v1 = 15,
94 clock_instruction_rejection_v1 = 16,
95 entropy_instruction_rejection_v1 = 17,
96 checkpoint_memory_v1 = 18,
97 checkpoint_stream_v1 = 19,
98 terminal_admission_v1 = 20,
99 virtual_time_admission_v1 = 21,
100 entropy_admission_v1 = 22,
101 packet_payload_v3 = 23,
102 packet_delivery_v3 = 24,
103 packet_fault_v1 = 25,
104 service_result_v1 = 26,
105 effect_result_v1 = 27,
106 fault_decision_v1 = 28,
107 capacity_fault_v1 = 29,
108 machine_crash_v1 = 30,
109 activation_fence_v1 = 31,
110 world_turn_v1 = 32,
111 transition_replay_v1 = 33,
112 };
113
114 /// Assumptions are the dependencies a control rests on and takes on trust, listed
115 /// so a reader sees what the package trusts without a check.
116 /// Three assumptions exist today: two concern the Linux kernel interface for running
117 /// a virtual machine on host hardware, KVM, covering instruction equivalence under
118 /// it and its stutter budget, and the third is the process-crash provider.
119 pub const Assumption = enum(u16) {
120 kvm_instruction_equivalence_v1 = 1,
121 kvm_stutter_budget_v1 = 2,
122 process_crash_provider_v1 = 3,
123 };
124
125 pub const ControlKind = enum(u8) {
126 enforced = 1,
127 assumed = 2,
128 };
129
130 /// A control determines whether a witness enforces a source or the source stands
131 /// as an assumption, so a reader opens the value to see whether a source is held
132 /// by a mechanism or by trust.
133 pub const Control = union(ControlKind) {
134 enforced: Witness,
135 assumed: Assumption,
136 };
137
138 /// One row of the inventory names a source with its category and its version, giving
139 /// the control that holds under the portable x86-64 interpreter, or reference backend,
140 /// beside the control that holds under KVM so a reader sees how that source is held
141 /// on each backend.
142 /// The two control fields are separate, so a source enforced by the interpreter
143 /// and assumed under KVM records both at once.
144 pub const Entry = struct {
145 source: Source,
146 category: Category,
147 version: u16,
148 reference: Control,
149 kvm: Control,
150 };
151
152 pub const ClaimWitness = enum(u16) {
153 portable_semantics_v1 = 1,
154 portable_world_replay_v1 = 2,
155 };
156
157 pub const ClaimAssumption = enum(u16) {
158 kvm_semantics_v1 = 1,
159 reconstruct_whole_system_v1 = 2,
160 kvm_whole_system_v1 = 3,
161 cross_host_equivalence_v1 = 4,
162 instruction_exact_equivalence_v1 = 5,
163 };
164
165 pub const ClaimKind = enum(u8) {
166 enforced = 1,
167 assumed = 2,
168 };
169
170 pub const Claim = union(ClaimKind) {
171 enforced: ClaimWitness,
172 assumed: ClaimAssumption,
173 };
174
175 /// The four determinism claims one profile makes, one at each of four levels (semantic
176 /// replay, whole-system replay on one backend, equivalence across hosts, and equivalence
177 /// down to the instruction).
178 /// A caller reads them to learn what the profile promises and on what evidence.
179 /// Each claim either carries a claim witness that enforces it or stands as an assumption.
180 pub const Claims = struct {
181 semantic: Claim,
182 same_backend_whole_system: Claim,
183 cross_host: Claim,
184 instruction_exact: Claim,
185 };
186
187 pub const Schema = enum(u16) {
188 whole_system_v1 = 1,
189 };
190
191 /// What identifies one inventory is its schema, how many entries it holds, and its
192 /// digest, so a caller compares this value to know whether two profiles were built
193 /// against the same inventory.
194 /// Every contract embeds this identity, so a change to the inventory changes the
195 /// identity of the shared execution rules, which is the contract fingerprint.
196 /// The digest is taken over every entry in order, covering each source, category,
197 /// version, and both controls.
198 pub const Identity = struct {
199 schema: Schema,
200 entry_count: u16,
201 digest: [Sha256.digest_length]u8,
202 };
203
204 pub const AuditError = error{
205 InventoryIdentityMismatch,
206 SurfaceCountMismatch,
207 SurfaceOrderMismatch,
208 };
209
210 pub const profile_sources = [_]Source{
211 .backend_selection,
212 .backend_availability,
213 };
214
215 /// The complete source inventory in canonical order, provided so a reader walks
216 /// this to audit the whole scope of the determinism promise in one place.
217 /// A compile-time check enforces that the order matches the source enum one for
218 /// one.
219 pub const entries = [_]Entry{
220 same(.backend_selection, .test_driver, 1, .backend_selection_v1),
221 same(.backend_availability, .external_result, 1, .backend_availability_v1),
222 same(.executable_bytes, .cpu_instruction, 1, .execution_manifest_v1),
223 same(.instruction_forms, .cpu_instruction, 2, .instruction_policy_v2),
224 same(.instruction_flags, .cpu_instruction, 2, .instruction_flags_v2),
225 same(.initial_cpu_state, .cpu_instruction, 1, .initial_cpu_state_v1),
226 split(
227 .backend_instruction_result,
228 .cpu_instruction,
229 1,
230 .portable_instruction_result_v1,
231 .kvm_instruction_equivalence_v1,
232 ),
233 same(.cpuid_vendor, .cpuid_feature, 1, .cpuid_model_v1),
234 same(.cpuid_signature, .cpuid_feature, 1, .cpuid_model_v1),
235 same(.cpuid_page_size_extension, .cpuid_feature, 1, .cpuid_model_v1),
236 same(
237 .cpuid_physical_address_extension,
238 .cpuid_feature,
239 1,
240 .cpuid_model_v1,
241 ),
242 same(.cpuid_conditional_move, .cpuid_feature, 1, .cpuid_model_v1),
243 same(.cpuid_execute_disable, .cpuid_feature, 1, .cpuid_model_v1),
244 same(.cpuid_long_mode, .cpuid_feature, 1, .cpuid_model_v1),
245 same(.cpuid_address_widths, .cpuid_feature, 1, .cpuid_model_v1),
246 same(.cpuid_leaf_range, .cpuid_feature, 1, .cpuid_model_v1),
247 same(.guest_schedule, .scheduler_choice, 2, .cooperative_schedule_v2),
248 split(
249 .host_run_stutter,
250 .scheduler_choice,
251 1,
252 .portable_no_stutter_v1,
253 .kvm_stutter_budget_v1,
254 ),
255 same(.guest_interrupt, .interrupt, 1, .guest_interrupt_exclusion_v1),
256 split(
257 .host_signal_interrupt,
258 .interrupt,
259 1,
260 .portable_no_host_signal_v1,
261 .kvm_stutter_budget_v1,
262 ),
263 same(.channel_device, .device, 1, .channel_device_v1),
264 same(.doorbell_exit, .device, 1, .doorbell_completion_v1),
265 same(.unmodeled_device_exit, .device, 1, .unmodeled_device_rejection_v1),
266 same(.cpu_clock_instruction, .clock, 1, .clock_instruction_rejection_v1),
267 same(.cpu_entropy_instruction, .entropy, 1, .entropy_instruction_rejection_v1),
268 same(.checkpoint_memory, .external_result, 1, .checkpoint_memory_v1),
269 same(.checkpoint_source, .external_result, 1, .checkpoint_stream_v1),
270 same(.terminal_input, .test_driver, 1, .terminal_admission_v1),
271 same(.virtual_time, .clock, 1, .virtual_time_admission_v1),
272 same(.entropy_input, .entropy, 1, .entropy_admission_v1),
273 same(.packet_payload, .packet, 3, .packet_payload_v3),
274 same(.packet_delivery, .packet, 3, .packet_delivery_v3),
275 same(.packet_fault, .packet, 1, .packet_fault_v1),
276 same(.host_service_result, .host_service, 1, .service_result_v1),
277 same(.effect_result, .external_result, 1, .effect_result_v1),
278 same(.fault_choice, .test_driver, 1, .fault_decision_v1),
279 same(.capacity_fault, .test_driver, 1, .capacity_fault_v1),
280 same(.machine_crash, .test_driver, 1, .machine_crash_v1),
281 assumed(.process_crash, .host_service, 1, .process_crash_provider_v1),
282 same(.activation_fence, .test_driver, 1, .activation_fence_v1),
283 same(.turn_selection, .test_driver, 1, .world_turn_v1),
284 same(.replay_source, .external_result, 1, .transition_replay_v1),
285 };
286
287 pub const inventory_identity: Identity = .{
288 .schema = .whole_system_v1,
289 .entry_count = @intCast(entries.len),
290 .digest = inventoryDigest(),
291 };
292
293 pub const portable_reconstruct_claims: Claims = .{
294 .semantic = .{ .enforced = .portable_semantics_v1 },
295 .same_backend_whole_system = .{ .assumed = .reconstruct_whole_system_v1 },
296 .cross_host = .{ .assumed = .cross_host_equivalence_v1 },
297 .instruction_exact = .{ .assumed = .instruction_exact_equivalence_v1 },
298 };
299
300 pub const portable_continuation_claims: Claims = .{
301 .semantic = .{ .enforced = .portable_semantics_v1 },
302 .same_backend_whole_system = .{ .enforced = .portable_world_replay_v1 },
303 .cross_host = .{ .assumed = .cross_host_equivalence_v1 },
304 .instruction_exact = .{ .assumed = .instruction_exact_equivalence_v1 },
305 };
306
307 pub const kvm_reconstruct_claims: Claims = .{
308 .semantic = .{ .assumed = .kvm_semantics_v1 },
309 .same_backend_whole_system = .{ .assumed = .reconstruct_whole_system_v1 },
310 .cross_host = .{ .assumed = .cross_host_equivalence_v1 },
311 .instruction_exact = .{ .assumed = .instruction_exact_equivalence_v1 },
312 };
313
314 pub const kvm_continuation_claims: Claims = .{
315 .semantic = .{ .assumed = .kvm_semantics_v1 },
316 .same_backend_whole_system = .{ .assumed = .kvm_whole_system_v1 },
317 .cross_host = .{ .assumed = .cross_host_equivalence_v1 },
318 .instruction_exact = .{ .assumed = .instruction_exact_equivalence_v1 },
319 };
320
321 pub fn entry(source: Source) *const Entry {
322 const index = @backingInt(source) - 1;
323 std.debug.assert(index < entries.len);
324 std.debug.assert(entries[index].source == source);
325 return &entries[index];
326 }
327
328 pub fn audit(identity: Identity, surface: []const Source) AuditError!void {
329 if (!std.meta.eql(identity, inventory_identity)) {
330 return error.InventoryIdentityMismatch;
331 }
332 if (surface.len != entries.len) return error.SurfaceCountMismatch;
333 for (surface, entries) |source, declared| {
334 if (source != declared.source) return error.SurfaceOrderMismatch;
335 }
336 }
337
338 fn same(
339 source: Source,
340 category: Category,
341 version: u16,
342 witness: Witness,
343 ) Entry {
344 return .{
345 .source = source,
346 .category = category,
347 .version = version,
348 .reference = .{ .enforced = witness },
349 .kvm = .{ .enforced = witness },
350 };
351 }
352
353 fn split(
354 source: Source,
355 category: Category,
356 version: u16,
357 reference: Witness,
358 kvm: Assumption,
359 ) Entry {
360 return .{
361 .source = source,
362 .category = category,
363 .version = version,
364 .reference = .{ .enforced = reference },
365 .kvm = .{ .assumed = kvm },
366 };
367 }
368
369 fn assumed(
370 source: Source,
371 category: Category,
372 version: u16,
373 assumption: Assumption,
374 ) Entry {
375 return .{
376 .source = source,
377 .category = category,
378 .version = version,
379 .reference = .{ .assumed = assumption },
380 .kvm = .{ .assumed = assumption },
381 };
382 }
383
384 fn inventoryDigest() [Sha256.digest_length]u8 {
385 @setEvalBranchQuota(100_000);
386 var hasher = Sha256.init(.{});
387 hasher.update("tiny.machine-determinism-inventory/v1");
388 for (entries) |declared| {
389 var encoded: [11]u8 = @splat(0);
390 std.mem.writeInt(u16, encoded[0..2], @backingInt(declared.source), .little);
391 encoded[2] = @backingInt(declared.category);
392 std.mem.writeInt(u16, encoded[3..5], declared.version, .little);
393 encodeControl(declared.reference, encoded[5..8]);
394 encodeControl(declared.kvm, encoded[8..11]);
395 hasher.update(&encoded);
396 }
397 var digest: [Sha256.digest_length]u8 = undefined;
398 hasher.final(&digest);
399 return digest;
400 }
401
402 fn encodeControl(control: Control, output: *[3]u8) void {
403 switch (control) {
404 .enforced => |witness| {
405 output[0] = 1;
406 std.mem.writeInt(u16, output[1..3], @backingInt(witness), .little);
407 },
408 .assumed => |assumption| {
409 output[0] = 2;
410 std.mem.writeInt(u16, output[1..3], @backingInt(assumption), .little);
411 },
412 }
413 }
414
415 comptime {
416 const sources = std.meta.tags(Source);
417 std.debug.assert(entries.len == sources.len);
418 std.debug.assert(entries.len <= std.math.maxInt(u16));
419 for (entries, sources) |declared, source| {
420 std.debug.assert(declared.source == source);
421 std.debug.assert(declared.version > 0);
422 }
423 }