lib/machine/src/profile/root.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

  1 //! Comparing two runs requires writing down the rules both ran under and what exactly
  2 //! is being claimed about them, and this namespace holds both as one execution contract,
  3 //! the backend chosen to run it, and the determinism claims that pairing makes (a
  4 //! *profile*), with the evidence for each claim named.
  5 //!
  6 //! The execution rules one profile kind shares across backends (its *contract*)
  7 //! name the CPU model and the admitted instruction forms, directly boot K0, the
  8 //! restricted kernel from `lib/os` that exchanges request and event messages with
  9 //! the host through fixed rings in guest RAM, schedule the single vCPU cooperatively,
 10 //! inject time and entropy, feed back recorded effect results, and settle the RAM
 11 //! geometry, transport sizes, inventory identity, and capacity limits. The two canonical
 12 //! profile kinds govern root handling: reconstruct rebuilds a root when the stored
 13 //! value is absent, and continuation test requires authoritative roots and rejects
 14 //! a missing one. Semantic choices are versioned enum values, and geometry, transport,
 15 //! and capacity fields are fixed numbers. The `validate` function accepts only canonical
 16 //! constructor outputs carrying the current inventory identity.
 17 //!
 18 //! A promise can be checked only once its scope is written down, so the namespace
 19 //! carries the canonical list naming all 42 places where two runs could differ across
 20 //! eleven categories (the *inventory*). Each inventory entry records its control
 21 //! twice, once for the reference backend and once for KVM: enforced by a named witness,
 22 //! or resting on a named assumption. Each profile states four *determinism claims*
 23 //! about itself in the same plain terms, covering semantic replay, whole-system
 24 //! replay on one backend, equivalence across hosts, and equivalence down to the
 25 //! instruction. A portable profile enforces semantic replay, the portable continuation-test
 26 //! profile enforces whole-system replay as well, and three subjects stay assumptions:
 27 //! KVM semantics, equivalence across hosts, and equivalence down to the instruction.
 28 //!
 29 //! From earlier work in the [Linux KVM API](https://docs.kernel.org/virt/kvm/api.html)
 30 //! and the
 31 //! [Intel Software Developer Manuals](https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html),
 32 //! the namespace took the x86-64 CPU model with the long-mode contract it admits,
 33 //! one virtual CPU, and KVM named as one execution semantics among the backends
 34 //! of the profile.
 35 //!
 36 //! The backend is one field of the profile, so the same contract carries a second,
 37 //! portable implementation, and the inventory records what that implementation enforces
 38 //! while KVM rests on assumptions. A profile carries two fingerprints. The first
 39 //! covers the execution rules a kind shares, computed over the encoded profile with
 40 //! the backend field and the claim fields zeroed as the *contract fingerprint*,
 41 //! so a KVM profile and its portable counterpart hold the same value and can be
 42 //! run against each other. The second covers the whole profile as the *profile fingerprint*,
 43 //! with the contract, the backend, and the claims all contributing, so every pairing
 44 //! of a canonical kind with a backend gets a value of its own.
 45 
 46 pub const capacity = @import("capacity.zig");
 47 pub const determinism = @import("determinism.zig");
 48 pub const types = @import("types.zig");
 49 pub const wire = @import("wire.zig");
 50 
 51 pub const Architecture = types.Architecture;
 52 pub const BackendSemantics = types.BackendSemantics;
 53 pub const BootDialect = types.BootDialect;
 54 pub const Capacity = capacity.Capacity;
 55 pub const CheckpointFormat = types.CheckpointFormat;
 56 pub const Contract = types.Contract;
 57 pub const ContractFingerprint = wire.ContractFingerprint;
 58 pub const CpuContract = types.CpuContract;
 59 pub const DeterminismAssumption = determinism.Assumption;
 60 pub const DeterminismAuditError = determinism.AuditError;
 61 pub const DeterminismCategory = determinism.Category;
 62 pub const DeterminismClaim = determinism.Claim;
 63 pub const DeterminismClaimAssumption = determinism.ClaimAssumption;
 64 pub const DeterminismClaimKind = determinism.ClaimKind;
 65 pub const DeterminismClaims = determinism.Claims;
 66 pub const DeterminismClaimWitness = determinism.ClaimWitness;
 67 pub const DeterminismControl = determinism.Control;
 68 pub const DeterminismControlKind = determinism.ControlKind;
 69 pub const DeterminismEntry = determinism.Entry;
 70 pub const DeterminismIdentity = determinism.Identity;
 71 pub const DeterminismSchema = determinism.Schema;
 72 pub const DeterminismSource = determinism.Source;
 73 pub const DeterminismWitness = determinism.Witness;
 74 pub const DeviceDialect = types.DeviceDialect;
 75 pub const EffectSemantics = types.EffectSemantics;
 76 pub const EntropySemantics = types.EntropySemantics;
 77 pub const Error = types.Error;
 78 pub const Geometry = types.Geometry;
 79 pub const InstructionAdmission = types.InstructionAdmission;
 80 pub const MissingRoot = types.MissingRoot;
 81 pub const Profile = types.Profile;
 82 pub const ProfileFingerprint = wire.ProfileFingerprint;
 83 pub const ProfileKind = types.ProfileKind;
 84 pub const RootSemantics = types.RootSemantics;
 85 pub const Scheduling = types.Scheduling;
 86 pub const TimeSemantics = types.TimeSemantics;
 87 pub const Transport = types.Transport;
 88 pub const TransportDialect = types.TransportDialect;
 89 pub const Usage = capacity.Usage;
 90 
 91 pub const auditDeterminism = determinism.audit;
 92 pub const contractFingerprint = wire.contractFingerprint;
 93 pub const continuationTestV1 = types.continuationTestV1;
 94 pub const decode = wire.decode;
 95 pub const encode = wire.encode;
 96 pub const interpretedContinuationTestV1 = types.interpretedContinuationTestV1;
 97 pub const interpretedReconstructV1 = types.interpretedReconstructV1;
 98 pub const kvmContinuationTestV1 = types.kvmContinuationTestV1;
 99 pub const kvmReconstructV1 = types.kvmReconstructV1;
100 pub const profileFingerprint = wire.profileFingerprint;
101 pub const reconstructV1 = types.reconstructV1;
102 pub const schema_major = types.schema_major;
103 pub const schema_minor = types.schema_minor;
104 pub const validate = types.validate;
105 pub const wire_bytes = wire.bytes;
106 pub const determinism_entries = determinism.entries;
107 pub const determinism_sources = determinism.profile_sources;