tiny.machine.profile.types

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

1const std = @import("std");2const os = @import("os");3const determinism = @import("determinism.zig");45const os_abi = os.abi;67pub const schema_major: u16 = 1;8pub const schema_minor: u16 = 1;910/// The two canonical profile kinds, so a caller says how stored roots are treated.11/// Reconstruct rebuilds a root when the stored value is absent, so a stored root12/// serves only as a cache. By contrast, continuation test requires authoritative13/// roots and rejects a missing one.14pub const ProfileKind = enum(u8) {15    reconstruct_v1 = 1,16    continuation_test_v1 = 2,17};1819pub const Architecture = enum(u8) {20    x86_64 = 1,21};2223pub const CpuContract = os.boot.kernel.manifest.CpuContract;2425pub const InstructionAdmission = enum(u16) {26    verified_deterministic_cfg_v2 = 2,27};2829pub const BootDialect = enum(u16) {30    elf64_k0_direct_v1 = 1,31};3233pub const RootSemantics = enum(u8) {34    optional_cache = 1,35    authoritative = 2,36};3738pub const MissingRoot = enum(u8) {39    reconstruct = 1,40    reject = 2,41};4243pub const DeviceDialect = enum(u16) {44    k0_channels_v1 = 1,45};4647pub const Scheduling = enum(u16) {48    cooperative_single_vcpu_boundary_v2 = 2,49};5051pub const TimeSemantics = enum(u16) {52    injected_monotonic_v1 = 1,53};5455pub const EntropySemantics = enum(u16) {56    injected_stream_v1 = 1,57};5859pub const TransportDialect = enum(u16) {60    os_machine_v1 = 1,61};6263pub const CheckpointFormat = enum(u16) {64    machine_root_v1 = 1,65};6667pub const BackendSemantics = enum(u16) {68    linux_kvm_single_vcpu_v1 = 1,69    portable_x86_64_interpreter_v1 = 2,70};7172pub const EffectSemantics = enum(u16) {73    recorded_results_only_v1 = 1,74};7576/// The memory geometry a contract fixes gives how many vCPUs run, the page size,77/// the base address, and the number of bytes, so a caller can check its own memory78/// layout before constructing an instance. Every canonical profile fixes one vCPU,79/// a RAM base of zero, and 67,108,864 RAM bytes.80pub const Geometry = struct {81    vcpu_count: u16,82    page_bytes: u32,83    ram_base: u64,84    ram_bytes: u64,85};8687/// The transport sizes a contract takes from the machine ABI fix the encoding version,88/// the ABI major and minor numbers, and the bounds on a frame, a ring, a record,89/// and a payload, so a caller can size its message buffers before it talks to the90/// guest. The machine ABI supplies every one of these values.91pub const Transport = struct {92    dialect: TransportDialect,93    abi_major: u16,94    abi_minor: u16,95    boot_frame_bytes: u16,96    message_frame_bytes: u16,97    ring_header_bytes: u16,98    request_records: u16,99    event_records: u16,100    terminal_bytes: u16,101    entropy_bytes: u16,102    semantic_bytes: u16,103    effect_request_bytes: u16,104    effect_result_bytes: u16,105};106107/// Holds the rules for executing a guest that every backend of one canonical kind108/// obeys, so a caller can compare contracts to know whether two runs obeyed the109/// same rules. Enum fields name versioned semantics: the CPU model, the admitted110/// instructions, direct K0 boot, root handling, the device dialect, scheduling,111/// time, entropy, the checkpoint format, and effect handling. Structured and numeric112/// fields fix the geometry, the transport sizes, the determinism identity, and the113/// capacity limits. The determinism identity is embedded here, so a change to the114/// inventory changes every contract.115pub const Contract = struct {116    schema_major: u16,117    schema_minor: u16,118    kind: ProfileKind,119    architecture: Architecture,120    cpu: CpuContract,121    instruction_admission: InstructionAdmission,122    boot: BootDialect,123    root_semantics: RootSemantics,124    missing_root: MissingRoot,125    device: DeviceDialect,126    scheduling: Scheduling,127    time: TimeSemantics,128    entropy: EntropySemantics,129    geometry: Geometry,130    transport: Transport,131    checkpoint: CheckpointFormat,132    effects: EffectSemantics,133    determinism: determinism.Identity,134    instance_limit: u16,135    checkpoint_candidate_limit: u16,136    admission_limit: u32,137};138139/// One execution contract, the backend chosen to run it, and the determinism claims140/// that pairing makes define a profile. A caller hands one of these to an instance,141/// a checkpoint, or a world so that code knows the rules.142pub const Profile = struct {143    contract: Contract,144    backend: BackendSemantics,145    claims: determinism.Claims,146};147148pub const Error = error{149    BadMagic,150    UnsupportedVersion,151    WireBytesMismatch,152    UnsupportedFlags,153    UnknownProfileField,154    ReservedNonzero,155    IncompatibleProfile,156    IncompatibleGeometry,157    CapacityExceeded,158};159160/// Produces the canonical reconstruct profile for one backend, so a caller can rebuild161/// a missing root and keep going. Stored roots are an optional cache under this162/// kind, and a missing one is rebuilt.163pub fn reconstructV1(backend: BackendSemantics) Profile {164    return base(.reconstruct_v1, .optional_cache, .reconstruct, backend);165}166167/// Produces the profile that continuation tests run under on a given backend, so168/// a caller can treat stored roots as authoritative. Stored roots are authoritative169/// under this kind, and a missing one is rejected.170pub fn continuationTestV1(backend: BackendSemantics) Profile {171    return base(.continuation_test_v1, .authoritative, .reject, backend);172}173174pub fn kvmReconstructV1() Profile {175    return reconstructV1(.linux_kvm_single_vcpu_v1);176}177178pub fn kvmContinuationTestV1() Profile {179    return continuationTestV1(.linux_kvm_single_vcpu_v1);180}181182pub fn interpretedReconstructV1() Profile {183    return reconstructV1(.portable_x86_64_interpreter_v1);184}185186pub fn interpretedContinuationTestV1() Profile {187    return continuationTestV1(.portable_x86_64_interpreter_v1);188}189190/// Admits a profile when it came from a canonical constructor and carries the inventory191/// identity in force, and refuses it otherwise. Every entry point that takes a profile192/// calls this function first, so a hand-built value goes no further. A profile whose193/// determinism identity differs from the current inventory is rejected before anything194/// else. The value is then compared field by field against the constructor output195/// for its own kind and backend.196pub fn validate(value: Profile) Error!void {197    if (!std.meta.eql(value.contract.determinism, determinism.inventory_identity)) {198        return error.IncompatibleProfile;199    }200    const expected = switch (value.contract.kind) {201        .reconstruct_v1 => reconstructV1(value.backend),202        .continuation_test_v1 => continuationTestV1(value.backend),203    };204    if (!std.meta.eql(value, expected)) return error.IncompatibleProfile;205}206207fn base(208    kind: ProfileKind,209    root_semantics: RootSemantics,210    missing_root: MissingRoot,211    backend: BackendSemantics,212) Profile {213    return .{214        .contract = .{215            .schema_major = schema_major,216            .schema_minor = schema_minor,217            .kind = kind,218            .architecture = .x86_64,219            .cpu = .x86_64_k0_long_mode_v1,220            .instruction_admission = .verified_deterministic_cfg_v2,221            .boot = .elf64_k0_direct_v1,222            .root_semantics = root_semantics,223            .missing_root = missing_root,224            .device = .k0_channels_v1,225            .scheduling = .cooperative_single_vcpu_boundary_v2,226            .time = .injected_monotonic_v1,227            .entropy = .injected_stream_v1,228            .geometry = .{229                .vcpu_count = 1,230                .page_bytes = os_abi.boot.page_bytes,231                .ram_base = 0,232                .ram_bytes = os_abi.channel.ram_bytes,233            },234            .transport = .{235                .dialect = .os_machine_v1,236                .abi_major = os_abi.major,237                .abi_minor = os_abi.minor,238                .boot_frame_bytes = os_abi.boot.frame_bytes,239                .message_frame_bytes = os_abi.message.frame_bytes,240                .ring_header_bytes = os_abi.ring.header_bytes,241                .request_records = os_abi.ring.capacity,242                .event_records = os_abi.ring.capacity,243                .terminal_bytes = os_abi.message.terminal_bytes_max,244                .entropy_bytes = os_abi.message.entropy_bytes_max,245                .semantic_bytes = os_abi.message.semantic_bytes_max,246                .effect_request_bytes = os_abi.message.effect_request_bytes_max,247                .effect_result_bytes = os_abi.message.effect_result_bytes_max,248            },249            .checkpoint = .machine_root_v1,250            .effects = .recorded_results_only_v1,251            .determinism = determinism.inventory_identity,252            .instance_limit = 4,253            .checkpoint_candidate_limit = 1,254            .admission_limit = 4096,255        },256        .backend = backend,257        .claims = claims(kind, backend),258    };259}260261fn claims(262    kind: ProfileKind,263    backend: BackendSemantics,264) determinism.Claims {265    return switch (backend) {266        .portable_x86_64_interpreter_v1 => switch (kind) {267            .reconstruct_v1 => determinism.portable_reconstruct_claims,268            .continuation_test_v1 => determinism.portable_continuation_claims,269        },270        .linux_kvm_single_vcpu_v1 => switch (kind) {271            .reconstruct_v1 => determinism.kvm_reconstruct_claims,272            .continuation_test_v1 => determinism.kvm_continuation_claims,273        },274    };275}276277comptime {278    std.debug.assert(os_abi.boot.page_bytes == os_abi.ring.page_bytes);279    std.debug.assert(os_abi.boot.ring_capacity == os_abi.ring.capacity);280    std.debug.assert(os_abi.boot.message_bytes == os_abi.message.frame_bytes);281    std.debug.assert(os_abi.message.terminal_bytes_max <= std.math.maxInt(u16));282    std.debug.assert(os_abi.message.entropy_bytes_max <= std.math.maxInt(u16));283    std.debug.assert(os_abi.message.semantic_bytes_max <= std.math.maxInt(u16));284    std.debug.assert(os_abi.message.effect_request_bytes_max <= std.math.maxInt(u16));285    std.debug.assert(os_abi.message.effect_result_bytes_max <= std.math.maxInt(u16));286}