tiny.machine.profile.determinism

1const std = @import("std");23const Sha256 = std.crypto.hash.sha2.Sha256;45/// The eleven families a divergence source can belong to are categories, so a reader6/// 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.10pub 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};2324/// The places where two runs of the same program could differ that the package takes25/// responsibility for are divergence sources, so a reader checks a source against26/// 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 source28/// in the same order.29pub 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};7374/// 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 a77/// new value.78pub 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};113114/// Assumptions are the dependencies a control rests on and takes on trust, listed115/// so a reader sees what the package trusts without a check.116/// Three assumptions exist today: two concern the Linux kernel interface for running117/// a virtual machine on host hardware, KVM, covering instruction equivalence under118/// it and its stutter budget, and the third is the process-crash provider.119pub const Assumption = enum(u16) {120    kvm_instruction_equivalence_v1 = 1,121    kvm_stutter_budget_v1 = 2,122    process_crash_provider_v1 = 3,123};124125pub const ControlKind = enum(u8) {126    enforced = 1,127    assumed = 2,128};129130/// A control determines whether a witness enforces a source or the source stands131/// as an assumption, so a reader opens the value to see whether a source is held132/// by a mechanism or by trust.133pub const Control = union(ControlKind) {134    enforced: Witness,135    assumed: Assumption,136};137138/// One row of the inventory names a source with its category and its version, giving139/// 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 held141/// on each backend.142/// The two control fields are separate, so a source enforced by the interpreter143/// and assumed under KVM records both at once.144pub const Entry = struct {145    source: Source,146    category: Category,147    version: u16,148    reference: Control,149    kvm: Control,150};151152pub const ClaimWitness = enum(u16) {153    portable_semantics_v1 = 1,154    portable_world_replay_v1 = 2,155};156157pub 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};164165pub const ClaimKind = enum(u8) {166    enforced = 1,167    assumed = 2,168};169170pub const Claim = union(ClaimKind) {171    enforced: ClaimWitness,172    assumed: ClaimAssumption,173};174175/// The four determinism claims one profile makes, one at each of four levels (semantic176/// replay, whole-system replay on one backend, equivalence across hosts, and equivalence177/// 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.180pub const Claims = struct {181    semantic: Claim,182    same_backend_whole_system: Claim,183    cross_host: Claim,184    instruction_exact: Claim,185};186187pub const Schema = enum(u16) {188    whole_system_v1 = 1,189};190191/// What identifies one inventory is its schema, how many entries it holds, and its192/// digest, so a caller compares this value to know whether two profiles were built193/// against the same inventory.194/// Every contract embeds this identity, so a change to the inventory changes the195/// 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.198pub const Identity = struct {199    schema: Schema,200    entry_count: u16,201    digest: [Sha256.digest_length]u8,202};203204pub const AuditError = error{205    InventoryIdentityMismatch,206    SurfaceCountMismatch,207    SurfaceOrderMismatch,208};209210pub const profile_sources = [_]Source{211    .backend_selection,212    .backend_availability,213};214215/// The complete source inventory in canonical order, provided so a reader walks216/// 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 for218/// one.219pub 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};286287pub const inventory_identity: Identity = .{288    .schema = .whole_system_v1,289    .entry_count = @intCast(entries.len),290    .digest = inventoryDigest(),291};292293pub 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};299300pub 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};306307pub 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};313314pub 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};320321pub 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}327328pub 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}337338fn 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}352353fn 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}368369fn 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}383384fn 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}401402fn 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}414415comptime {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}

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