lib/machine/src/profile/types.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const os = @import("os");
3 const determinism = @import("determinism.zig");
4
5 const os_abi = os.abi;
6
7 pub const schema_major: u16 = 1;
8 pub const schema_minor: u16 = 1;
9
10 /// 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 root
12 /// serves only as a cache. By contrast, continuation test requires authoritative
13 /// roots and rejects a missing one.
14 pub const ProfileKind = enum(u8) {
15 reconstruct_v1 = 1,
16 continuation_test_v1 = 2,
17 };
18
19 pub const Architecture = enum(u8) {
20 x86_64 = 1,
21 };
22
23 pub const CpuContract = os.boot.kernel.manifest.CpuContract;
24
25 pub const InstructionAdmission = enum(u16) {
26 verified_deterministic_cfg_v2 = 2,
27 };
28
29 pub const BootDialect = enum(u16) {
30 elf64_k0_direct_v1 = 1,
31 };
32
33 pub const RootSemantics = enum(u8) {
34 optional_cache = 1,
35 authoritative = 2,
36 };
37
38 pub const MissingRoot = enum(u8) {
39 reconstruct = 1,
40 reject = 2,
41 };
42
43 pub const DeviceDialect = enum(u16) {
44 k0_channels_v1 = 1,
45 };
46
47 pub const Scheduling = enum(u16) {
48 cooperative_single_vcpu_boundary_v2 = 2,
49 };
50
51 pub const TimeSemantics = enum(u16) {
52 injected_monotonic_v1 = 1,
53 };
54
55 pub const EntropySemantics = enum(u16) {
56 injected_stream_v1 = 1,
57 };
58
59 pub const TransportDialect = enum(u16) {
60 os_machine_v1 = 1,
61 };
62
63 pub const CheckpointFormat = enum(u16) {
64 machine_root_v1 = 1,
65 };
66
67 pub const BackendSemantics = enum(u16) {
68 linux_kvm_single_vcpu_v1 = 1,
69 portable_x86_64_interpreter_v1 = 2,
70 };
71
72 pub const EffectSemantics = enum(u16) {
73 recorded_results_only_v1 = 1,
74 };
75
76 /// 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 memory
78 /// layout before constructing an instance. Every canonical profile fixes one vCPU,
79 /// a RAM base of zero, and 67,108,864 RAM bytes.
80 pub const Geometry = struct {
81 vcpu_count: u16,
82 page_bytes: u32,
83 ram_base: u64,
84 ram_bytes: u64,
85 };
86
87 /// 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 the
90 /// guest. The machine ABI supplies every one of these values.
91 pub 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 };
106
107 /// Holds the rules for executing a guest that every backend of one canonical kind
108 /// obeys, so a caller can compare contracts to know whether two runs obeyed the
109 /// same rules. Enum fields name versioned semantics: the CPU model, the admitted
110 /// instructions, direct K0 boot, root handling, the device dialect, scheduling,
111 /// time, entropy, the checkpoint format, and effect handling. Structured and numeric
112 /// fields fix the geometry, the transport sizes, the determinism identity, and the
113 /// capacity limits. The determinism identity is embedded here, so a change to the
114 /// inventory changes every contract.
115 pub 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 };
138
139 /// One execution contract, the backend chosen to run it, and the determinism claims
140 /// 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.
142 pub const Profile = struct {
143 contract: Contract,
144 backend: BackendSemantics,
145 claims: determinism.Claims,
146 };
147
148 pub const Error = error{
149 BadMagic,
150 UnsupportedVersion,
151 WireBytesMismatch,
152 UnsupportedFlags,
153 UnknownProfileField,
154 ReservedNonzero,
155 IncompatibleProfile,
156 IncompatibleGeometry,
157 CapacityExceeded,
158 };
159
160 /// Produces the canonical reconstruct profile for one backend, so a caller can rebuild
161 /// a missing root and keep going. Stored roots are an optional cache under this
162 /// kind, and a missing one is rebuilt.
163 pub fn reconstructV1(backend: BackendSemantics) Profile {
164 return base(.reconstruct_v1, .optional_cache, .reconstruct, backend);
165 }
166
167 /// Produces the profile that continuation tests run under on a given backend, so
168 /// a caller can treat stored roots as authoritative. Stored roots are authoritative
169 /// under this kind, and a missing one is rejected.
170 pub fn continuationTestV1(backend: BackendSemantics) Profile {
171 return base(.continuation_test_v1, .authoritative, .reject, backend);
172 }
173
174 pub fn kvmReconstructV1() Profile {
175 return reconstructV1(.linux_kvm_single_vcpu_v1);
176 }
177
178 pub fn kvmContinuationTestV1() Profile {
179 return continuationTestV1(.linux_kvm_single_vcpu_v1);
180 }
181
182 pub fn interpretedReconstructV1() Profile {
183 return reconstructV1(.portable_x86_64_interpreter_v1);
184 }
185
186 pub fn interpretedContinuationTestV1() Profile {
187 return continuationTestV1(.portable_x86_64_interpreter_v1);
188 }
189
190 /// Admits a profile when it came from a canonical constructor and carries the inventory
191 /// identity in force, and refuses it otherwise. Every entry point that takes a profile
192 /// calls this function first, so a hand-built value goes no further. A profile whose
193 /// determinism identity differs from the current inventory is rejected before anything
194 /// else. The value is then compared field by field against the constructor output
195 /// for its own kind and backend.
196 pub 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 }
206
207 fn 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 }
260
261 fn 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 }
276
277 comptime {
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 }