lib/alloc/phase/src/capacity/root.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

   1 //! ## Package overview
   2 //!
   3 //! A component can prepare storage before repeated operations, specify a
   4 //! response when demand exceeds that storage, and state which resources its
   5 //! budget covers. The alloc_phase.capacity module supplies type checks and
   6 //! declarations for that purpose. Separate runtime phase allocator guards
   7 //! detect allocator operations routed through their handles. This module checks
   8 //! structures and declarations rather than enforcing actual numerical bounds.
   9 //!
  10 //! ## The two axes of owner shape
  11 //!
  12 //! Storage arrives either through an allocator passed to initialization, called
  13 //! `allocator_backed`, or via aligned bytes supplied by the caller, called
  14 //! `caller_provisioned`. Alongside this storage choice, `OwnerShape` classifies
  15 //! the overload interface as either `exact` or `rejecting`. The four constants
  16 //! are OwnerShape.allocator_exact, OwnerShape.allocator_rejecting,
  17 //! OwnerShape.provisioned_exact, and OwnerShape.provisioned_rejecting. An exact
  18 //! classification indicates only that the validator does not require an
  19 //! Exhaustion declaration, which does not guarantee that workloads will always
  20 //! fit or that all methods will succeed. A rejecting classification requires
  21 //! Owner.Exhaustion to be a finite nonempty error set, and at least one
  22 //! non-lifecycle pointer-receiver owner method must return that set directly or
  23 //! return an error union containing it. These classifications serve as
  24 //! interface checks and do not prove error reachability or validate a sizing
  25 //! equation.
  26 //!
  27 //! Each owner shape requires `Owner.Limits` and `Owner.Capacity` declarations
  28 //! plus runtime phase and capacity fields. The nested `Capacity` type provides
  29 //! `Capacity.derive`, whereas `init`, `activate`, and `deinit` are methods of
  30 //! the owner itself. Provisioned owners additionally require a Storage
  31 //! declaration representing an aligned mutable byte slice, a stored
  32 //! storage:Storage field, a runtime Capacity.storage_bytes field of type usize,
  33 //! work_limits, and claim. For provisioned owners, derive and init signatures
  34 //! return finite nonempty error unions, activate returns void, and deinit
  35 //! returns Storage. Allocator-backed owners may omit claim. These signatures do
  36 //! not establish that activate terminates successfully or that deinit returns
  37 //! the original bytes. The caller retains responsibility for storage lifetime,
  38 //! while actual implementation logic and supporting evidence determine runtime
  39 //! behavior.
  40 //!
  41 //! Shape validation inspects field types and receiver-method signatures to
  42 //! detect visible allocator capabilities. The scanning depth differs across
  43 //! owner variants: the immediate scanner applied to allocator-backed types
  44 //! inspects only shallow struct fields and method signatures, whereas the
  45 //! recursive scanner applied to caller-provisioned owners traverses nested
  46 //! definitions, including fields within `Limits` and `Capacity`. For example, a
  47 //! struct containing a borrowed pointer to an inner struct with an `Allocator`
  48 //! field passes the immediate scanner undetected but is caught by the recursive
  49 //! scanner. These static inspections examine type declarations rather than
  50 //! analyzing function bodies, tracking global state, or inspecting targets
  51 //! behind type-erased pointers.
  52 //!
  53 //! ## Storage ownership and rejection
  54 //!
  55 //! The next example configures the public ProvisionedRejectingFixture with two
  56 //! slots of two bytes inside caller-owned four-byte storage aligned to the
  57 //! requirement of the fixture. The sequence initializes the fixture, activates
  58 //! it, fills both slots, and then attempts a third submission. The test checks
  59 //! for the Full error, verifies that the payload and the used count remain
  60 //! unchanged, and inspects updated diagnostic counters.
  61 //!
  62 //! ```zig
  63 //! const std = @import("std");
  64 //! const capacity = @import("alloc_phase").capacity;
  65 //!
  66 //! test "caller storage ownership and rejection behavior" {
  67 //!     comptime capacity.requireProvisionedRejectingOwnerShape(
  68 //!         capacity.ProvisionedRejectingFixture,
  69 //!     );
  70 //!
  71 //!     const limits = capacity.ProvisionedRejectingFixture.Limits{
  72 //!         .slots = 2,
  73 //!         .slot_bytes = 2,
  74 //!     };
  75 //!
  76 //!     var buffer: [4]u8 align(capacity.ProvisionedRejectingFixture.storage_alignment) = @splat(0);
  77 //!
  78 //!     var owner = try capacity.ProvisionedRejectingFixture.init(&buffer, limits);
  79 //!     owner.activate();
  80 //!     defer _ = owner.deinit();
  81 //!
  82 //!     try owner.submit(0x11);
  83 //!     try owner.submit(0x22);
  84 //!
  85 //!     const snapshot_buffer = buffer;
  86 //!     const snapshot_used = owner.used;
  87 //!     try std.testing.expectEqual(@as(usize, 2), snapshot_used);
  88 //!
  89 //!     try std.testing.expectError(error.Full, owner.submit(0x33));
  90 //!
  91 //!     try std.testing.expectEqualSlices(u8, &snapshot_buffer, &buffer);
  92 //!     try std.testing.expectEqual(snapshot_used, owner.used);
  93 //!     try std.testing.expectEqual(@as(usize, 3), owner.usage.submitted);
  94 //!     try std.testing.expectEqual(@as(usize, 2), owner.usage.accepted);
  95 //!     try std.testing.expectEqual(@as(usize, 1), owner.usage.rejected);
  96 //!
  97 //!     try std.testing.expect(owner.cleanupOne());
  98 //!     try std.testing.expectEqual(@as(usize, 1), owner.used);
  99 //!     try std.testing.expectEqual(@as(u8, 0x11), buffer[0]);
 100 //!     try std.testing.expectEqual(@as(u8, 0x11), buffer[1]);
 101 //!     try std.testing.expectEqual(@as(u8, 0), buffer[2]);
 102 //!     try std.testing.expectEqual(@as(u8, 0), buffer[3]);
 103 //! }
 104 //! ```
 105 //!
 106 //! In this fixture, returning Full updates submitted and rejected counters
 107 //! while preserving the payload and the used count. If AccountingOverflow
 108 //! occurs, it returns before these counter changes take place. The
 109 //! reject_before_mutation claim applies to the protected payload rather than
 110 //! every field on the owner. Calling cleanupOne removes and zeroes one slot
 111 //! without altering the owner.usage field, which has type Usage. The deinit
 112 //! method returns the whole original slice and invalidates the owner without
 113 //! automatically calling cleanupOne. The caller must keep backing storage alive
 114 //! throughout this lifecycle. The declared cleanup call bound does not measure
 115 //! CPU time, because zeroing work depends on slot_bytes.
 116 //!
 117 //! ## Capacity specifications and expression graphs
 118 //!
 119 //! A storage formula is structured as a `Spec` expression graph tied directly
 120 //! to fields declared in an owner's `Limits` type. Within this directed graph,
 121 //! `bindInput` resolves a named field path into a typed ordinal path within the
 122 //! limits structure, while `bindType` registers static sizing facts for
 123 //! associated data types. Every node references only predecessor nodes created
 124 //! earlier in the sequence. For instance, expressing an `n + 1` byte bound
 125 //! requires an input node representing `n`, an integer constant node
 126 //! representing `1`, and an addition node referencing both predecessors. Sizing
 127 //! assertions select a target quantity and declare either an exact match or an
 128 //! upper-bound relation against the expression result. The package has no
 129 //! expression evaluator, and arithmetic helpers are not how the graph is
 130 //! evaluated. Implementations can separately use checked add and mul helpers,
 131 //! which return error.CapacityOverflow when integer arithmetic overflows.
 132 //!
 133 //! A capacity `Declaration` places the sizing formula inside a `SourceEnvelope`
 134 //! that records which resources the budget covers and excludes, the overload
 135 //! strategy, risk classifications, obligation keys with their verification
 136 //! roles, and optional work equations or dependencies. In parallel, a separate
 137 //! `Bindings` record associates the owner type with default limits and
 138 //! lifecycle function selectors. Owners operating under `phase_static`
 139 //! lifecycles require explicit `seal` and `teardown` selectors within their
 140 //! bindings, whereas `startup_static` owners omit these requirements.
 141 //! Work.equation provides descriptive text and WorkLimits contains checked
 142 //! literal bounds. Evidence about the implementation, including analysis or
 143 //! suitable tests, is still needed to support the stated work bound.
 144 //!
 145 //! ```zig
 146 //! const std = @import("std");
 147 //! const capacity = @import("alloc_phase").capacity;
 148 //!
 149 //! test "authoring a claim declaration and verifying checked arithmetic" {
 150 //!     const Owner = struct {
 151 //!         pub const Limits = struct {
 152 //!             message_bytes: usize,
 153 //!         };
 154 //!     };
 155 //!
 156 //!     const claim = comptime capacity.Declaration{
 157 //!         .source = .{
 158 //!             .id = "sample.pedagogic_owner",
 159 //!             .kind = .startup_static,
 160 //!             .limit_source = .caller,
 161 //!             .storage = .{
 162 //!                 .covered = &.{
 163 //!                     .{
 164 //!                         .id = "buffer",
 165 //!                         .lifetime = .steady,
 166 //!                         .detail = "message framing buffer",
 167 //!                     },
 168 //!                 },
 169 //!                 .excluded = &.{
 170 //!                     "operating system process arguments",
 171 //!                     "network socket kernel buffers",
 172 //!                 },
 173 //!             },
 174 //!             .capacity = .{
 175 //!                 .inputs = &.{
 176 //!                     capacity.bindInput(Owner.Limits, "message_bytes", "message_bytes"),
 177 //!                 },
 178 //!                 .type_selectors = &.{},
 179 //!                 .nodes = &.{
 180 //!                     .{ .input = 0 },
 181 //!                     .{ .constant = 1 },
 182 //!                     .{ .add = .{ .left = 0, .right = 1 } },
 183 //!                 },
 184 //!                 .assertions = &.{
 185 //!                     .{
 186 //!                         .scope = .closure_total,
 187 //!                         .measure = .retained,
 188 //!                         .relation = .exact,
 189 //!                         .expression = 2,
 190 //!                     },
 191 //!                 },
 192 //!             },
 193 //!             .overload = .{
 194 //!                 .kind = .reject_before_seal,
 195 //!                 .detail = "rejects limits exceeding addressable memory before activation",
 196 //!             },
 197 //!             .risks = .{
 198 //!                 .transitive = .{
 199 //!                     .status = .open,
 200 //!                     .detail = "callee allocations remain outside this owner claim",
 201 //!                 },
 202 //!                 .foreign = .{
 203 //!                     .status = .open,
 204 //!                     .detail = "external runtime resources remain unmanaged",
 205 //!                 },
 206 //!             },
 207 //!             .obligations = &.{
 208 //!                 .{ .key = "sample_capacity", .role = .capacity_model },
 209 //!                 .{ .key = "sample_overload", .role = .overload },
 210 //!             },
 211 //!         },
 212 //!         .bindings = .{
 213 //!             .owner = Owner,
 214 //!         },
 215 //!     };
 216 //!
 217 //!     try std.testing.expect(
 218 //!         capacity.validateDeclaration(
 219 //!             Owner,
 220 //!             claim,
 221 //!             capacity.OwnerShape.allocator_exact,
 222 //!         ) == null,
 223 //!     );
 224 //!
 225 //!     const computed = try capacity.add(usize, 31, 1);
 226 //!     try std.testing.expectEqual(@as(usize, 32), computed);
 227 //!
 228 //!     try std.testing.expectError(
 229 //!         error.CapacityOverflow,
 230 //!         capacity.add(usize, std.math.maxInt(usize), 1),
 231 //!     );
 232 //! }
 233 //! ```
 234 //!
 235 //! The validateDeclaration function validates this typed declaration rather
 236 //! than complete lifecycle-owner conformance. Furthermore, the arithmetic
 237 //! assertions exercise add independently and never evaluate the graph. An
 238 //! actual owner's derive method still needs domain checks and a capacity
 239 //! implementation.
 240 //!
 241 //! ## Metadata registration and evidence witnessing
 242 //!
 243 //! An obligation key names a property for supporting evidence. The
 244 //! witness(Owner,key) function checks that the key exists and returns an
 245 //! annotation with the claim id, key, and role for `record`, but it does
 246 //! not run or inspect the test. Similarly, the .witnessed risk status checks
 247 //! that a matching role obligation exists, not that evidence passed. Phase
 248 //! premise validation checks class, authority, and reference compatibility
 249 //! rather than the truth of the premise or the existence of external evidence.
 250 //!
 251 //! The ServerStorage type in tools/ask/src/storage.zig derives required sizes
 252 //! from a configured message_bytes limit rather than actual incoming message
 253 //! length, adding one reader byte, configured parse_bytes, and output_bytes.
 254 //! The derivation uses checked addition and requires parse_bytes to be
 255 //! positive, output_bytes to be at least 4096, and the total size to not exceed
 256 //! 16MiB. Its regions() method returns disjoint contiguous prefixes for these
 257 //! three required sizes. ServerStorage retains the whole supplied slice and
 258 //! deinit returns it, even when the slice is larger than required. Its source
 259 //! claim excludes arguments and help text, standard stream descriptors and
 260 //! kernel pipe buffering, and inline question summaries.
 261 //!
 262 //! One test compares derive against independent u128 arithmetic on selected
 263 //! limit tuples. Separate tests check exact caller storage acceptance along
 264 //! with one-byte-short rejection, and another separate test checks region
 265 //! lengths and pointer boundaries.
 266 //!
 267 //! When an owner provides a valid claim, shape validation records typed
 268 //! metadata references through the Stardust observer. The module derives two
 269 //! distinct SHA-256 digests: `capacitySpecDigest` identifies ordered expression
 270 //! metadata while omitting diagnostic field spellings and semantic types or
 271 //! sizes, whereas `declarationEnvelopeDigest` hashes the fields of the
 272 //! `SourceEnvelope` while excluding accompanying `Bindings`. Independent typed
 273 //! references are preserved alongside these hashes within the metadata
 274 //! pipeline. Consequently, these digests establish identity for declared
 275 //! specification content rather than confirming total implementation
 276 //! correctness or certifying evidence acceptance.
 277 
 278 const arithmetic = @import("arithmetic.zig");
 279 const capability = @import("capability.zig");
 280 const declaration = @import("declaration.zig");
 281 const owner = @import("owner.zig");
 282 const phase = @import("phase.zig");
 283 const shape = @import("shape.zig");
 284 const spec = @import("spec.zig");
 285 
 286 /// Declaration couples a SourceEnvelope specification with its corresponding
 287 /// compile-time Bindings. The struct acts as a typed metadata container rather
 288 /// than a runtime resource allocation. Calling validateDeclaration checks the
 289 /// declaration against a specified Owner type, expected OwnerShape, and source
 290 /// constraints, but validating a declaration does not verify the whole owner
 291 /// shape by itself. Constructing or validating a declaration installs no
 292 /// automatic runtime enforcement.
 293 pub const Declaration = declaration.Declaration;
 294 /// Computes the checked sum of two integer values of type `T`. It delegates to
 295 /// the `@addWithOverflow` builtin, returning `error.CapacityOverflow` if
 296 /// arithmetic overflow or carry occurs. The function imposes no domain-specific
 297 /// maximum bounds or byte limit policies, leaving application limits to owner
 298 /// capacity derivation. On success, it returns the sum as a value of type `T`.
 299 pub const add = arithmetic.add;
 300 /// Computes the checked product of two integer values of type `T`. It delegates
 301 /// to the `@mulWithOverflow` builtin, returning `error.CapacityOverflow` if
 302 /// arithmetic overflow occurs. The function enforces no external range policies
 303 /// or domain limits beyond the representation limits of type `T`. On success,
 304 /// it returns the product as a value of type `T`.
 305 pub const mul = arithmetic.mul;
 306 /// Violation enumerates the failure categories returned by the source
 307 /// declaration validator. When validation fails, the validator returns the
 308 /// first detected violation category rather than reporting a runtime allocation
 309 /// error. Malformed user types supplied in bindings may trigger Zig compile
 310 /// errors before validation completes. In root.zig, this type is exported under
 311 /// the public alias DeclarationViolation.
 312 pub const DeclarationViolation = declaration.Violation;
 313 /// SourceEnvelope contains the primary specification metadata of a claim,
 314 /// gathering its id, kind, limit_source, storage, capacity, overload, risks,
 315 /// optional work, dependencies, and obligations. The `id` must be a canonical
 316 /// identifier of 1 to 64 bytes consisting of at least two non-empty dot
 317 /// segments composed of lowercase letters, digits, or underscores, where
 318 /// leading digits and underscores are permitted. The `capacity` field is a
 319 /// typed `Spec` with semantic type fields requiring a compile-time
 320 /// representation rather than expression evaluation. The `dependencies` slice
 321 /// accepts up to 8 canonical identifiers, rejects duplicates or
 322 /// self-references, and performs no registry lookup or cycle analysis. The
 323 /// envelope borrows its referenced slices rather than deep-copying runtime
 324 /// strings.
 325 pub const SourceEnvelope = declaration.SourceEnvelope;
 326 /// EnvelopeView provides a structurally uniform representation of a
 327 /// SourceEnvelope where the typed capacity specification is replaced by a
 328 /// SpecView. The remaining borrowed metadata fields, including id, kind,
 329 /// limit_source, storage, overload, risks, work, dependencies, and obligations,
 330 /// remain identical. This view enables structural serialization and digest
 331 /// computation without depending on semantic type coordinates. Slices
 332 /// referenced by the view remain borrowed and are not owned by the view struct.
 333 pub const EnvelopeView = declaration.EnvelopeView;
 334 /// `Kind` specifies source classification as either `startup_static` or
 335 /// `phase_static`. Validation of `phase_static` requires valid seal and
 336 /// teardown bindings. In contrast, `startup_static` does not require or inspect
 337 /// optional phase bindings in `validateBindings`. The tag describes a claim and
 338 /// does not govern actual allocation behavior or enforce an operational
 339 /// lifetime.
 340 pub const Kind = declaration.Kind;
 341 /// LimitSource indicates whether memory capacity limits originate from the
 342 /// caller or from application defaults. Selecting caller forbids supplying a
 343 /// default_limits selector binding. Selecting application_default requires
 344 /// supplying a selector struct containing a public declaration member. The
 345 /// declaration validator verifies that this selector struct exists, but it
 346 /// checks no signature or value compatibility between that declaration and the
 347 /// owner limits.
 348 pub const LimitSource = declaration.LimitSource;
 349 /// CoveredStorage describes a discrete memory region covered by an owner claim
 350 /// through its id, lifetime, and detail fields. The id string must contain 1 to
 351 /// 64 bytes, starting with a lowercase ASCII letter and followed only by
 352 /// lowercase ASCII letters, digits, or underscores. Each id must be unique
 353 /// within the containing covered list. The lifetime field holds a
 354 /// StorageLifetime tag, and the detail string must contain 1 to 512 single-line
 355 /// bytes without null bytes, carriage returns, or line feeds. The struct
 356 /// borrows these slices without owning allocations or enforcing lifetimes at
 357 /// runtime.
 358 pub const CoveredStorage = declaration.CoveredStorage;
 359 /// Storage specifies the memory coverage boundaries of a claim using covered
 360 /// and excluded slices, rather than holding the backing storage buffer of an
 361 /// owner. The covered list accepts 1 to 16 CoveredStorage records with unique
 362 /// local identifiers. The excluded list accepts 1 to 16 descriptive strings,
 363 /// each bounded to 1 to 512 single-line bytes excluding null bytes, carriage
 364 /// returns, and line feeds. Excluded entries are not checked for uniqueness,
 365 /// and their presence makes no claim that other process memory is absent. The
 366 /// struct holds borrowed slices rather than copying text or managing memory.
 367 pub const Storage = declaration.Storage;
 368 /// StorageLifetime labels the operational stage of a covered storage region
 369 /// using the initialization, steady, or transferred tags. These values provide
 370 /// descriptive metadata about when an owner uses a memory region. The enum
 371 /// performs no runtime lifetime tracking, memory management, or ownership
 372 /// operations.
 373 pub const StorageLifetime = declaration.StorageLifetime;
 374 /// `Overload` describes declared overload behavior through its `kind` and
 375 /// `detail` fields, where `detail` identifies protected state. Full declaration
 376 /// validation checks that `kind` is compatible with `OwnerShape` and verifies
 377 /// that `detail` contains 1 to 512 bytes excluding NUL, LF, and CR characters.
 378 /// Merely constructing the record validates nothing and installs no dynamic
 379 /// policy.
 380 pub const Overload = declaration.Overload;
 381 /// OverloadKind defines the policy an owner follows when an operation exceeds
 382 /// capacity. Compatibility depends on the storage source and shape of the
 383 /// owner. Exact shapes accept reject_before_seal or not_applicable. For
 384 /// rejecting shapes, allocator-backed owners accept reject_before_mutation,
 385 /// replace, drop, or terminal, while caller-provisioned owners accept only
 386 /// reject_before_mutation. The accompanying detail string describes which
 387 /// internal state is protected, such as allowing submitted and rejected
 388 /// counters to increment in a full fixture. Validation checks compatibility
 389 /// between the enum tag and the owner shape without inspecting operation
 390 /// bodies.
 391 pub const OverloadKind = declaration.OverloadKind;
 392 /// Risk pairs a RiskStatus tag with a descriptive detail string explaining an
 393 /// operational boundary hazard. The detail string must contain 1 to 512
 394 /// single-line bytes without null characters, carriage returns, or line feeds.
 395 /// Declaration validation inspects the detail text grammar and verifies that
 396 /// any risk marked witnessed has a corresponding obligation role declared in
 397 /// the source envelope. The struct retains these values as source metadata
 398 /// without executing checks at runtime.
 399 pub const Risk = declaration.Risk;
 400 /// Risks groups the operational hazards of an owner into transitive and foreign
 401 /// Risk records. The transitive field documents risks originating within
 402 /// callees or subsidiary components, while the foreign field documents risks
 403 /// arising from external resources. The descriptive details define the actual
 404 /// scope of each hazard. Declaration validation enforces grammar and witnessed
 405 /// obligations for both fields, but it does not compute or audit a transitive
 406 /// closure across components.
 407 pub const Risks = declaration.Risks;
 408 /// RiskStatus describes whether an identified hazard has evidentiary coverage
 409 /// through the witnessed, excluded, or open tags. Setting status to witnessed
 410 /// requires declaring a matching risk role obligation in the source envelope,
 411 /// but it does not establish that a test passed. Setting status to excluded
 412 /// documents that the hazard falls outside the operational scope of the claim.
 413 /// Setting status to open documents an unresolved claim status without
 414 /// satisfying an obligation requirement.
 415 pub const RiskStatus = declaration.RiskStatus;
 416 /// `Work` defines an `equation` field consisting of descriptive work bound text
 417 /// between 1 and 512 bytes long, excluding NUL, LF, and CR characters. It is
 418 /// required whenever an owner uses a caller-provisioned shape, and its presence
 419 /// requires declaring an obligation with the work_bound role. The equation text
 420 /// provides descriptive documentation that is neither parsed nor evaluated
 421 /// during validation. This record differs from the WorkLimits structure, which
 422 /// supplies concrete numeric limits.
 423 pub const Work = declaration.Work;
 424 /// Bindings gathers compile-time type coordinates and lifecycle phase bindings
 425 /// separate from the source envelope. Fields include owner, default_limits,
 426 /// seal, teardown, and source, which all default to null. Validation requires
 427 /// owner to match the Owner type supplied to validateDeclaration. The
 428 /// default_limits binding is required for application_default limit sources and
 429 /// forbidden for caller limit sources, while seal and teardown bindings are
 430 /// required for phase_static declarations. The optional source type is retained
 431 /// as metadata but is not inspected by the validator. Envelope digests exclude
 432 /// all bindings and premises, and the struct owns no heap memory or reference
 433 /// counts.
 434 pub const Bindings = declaration.Bindings;
 435 /// PhaseBinding associates a lifecycle transition with an implementation seam
 436 /// and an evidentiary premise through its family and premise fields. Both
 437 /// fields default to null, but validating a phase_static declaration requires
 438 /// both to be present. The family field must be a selector struct containing a
 439 /// public declaration member that resolves to a function. Validation does not
 440 /// inspect the function signature or body, nor does it require the function to
 441 /// match Owner.activate or Owner.deinit. The struct stores compile-time type
 442 /// and premise descriptors rather than a runtime callable closure.
 443 pub const PhaseBinding = declaration.PhaseBinding;
 444 /// Premise pairs a PremiseClass category with a PremiseAuthority variant to
 445 /// justify a phase lifecycle binding. The validatePremise function checks that
 446 /// the class and authority are mutually compatible, that selector identifiers
 447 /// follow required canonical or local syntax, and that local theorem keys exist
 448 /// within the source obligations. Validation confirms structural and syntactic
 449 /// compatibility but produces no proof of the underlying fact.
 450 pub const Premise = declaration.Premise;
 451 /// PremiseClass names the form of basis that supports a phase binding. Its tags
 452 /// distinguish between mathematical theorem domains, checked semantic or path
 453 /// facts, certified claim summaries, and trusted user, external, or environment
 454 /// assertions. Selecting a tag identifies the expected authority category
 455 /// during premise validation, but the enum itself does not establish or
 456 /// evaluate the underlying evidence.
 457 pub const PremiseClass = declaration.PremiseClass;
 458 /// PremiseAuthority specifies the justifying source for a premise as a tagged
 459 /// union over checker, theorem, certified_claim, and trusted variants. Each
 460 /// variant carries its respective selector, except checker, which carries no
 461 /// payload. The authority must pair with a compatible PremiseClass during
 462 /// validation: checker requires checked_semantic_fact or checked_path_fact,
 463 /// theorem requires theorem_domain, certified_claim requires certified_summary,
 464 /// and trusted requires trusted_user, trusted_extern, or trusted_environment.
 465 pub const PremiseAuthority = declaration.PremiseAuthority;
 466 /// Obligation pairs a claim-local identifier key with an ObligationRole tag.
 467 /// The key string must contain 1 to 64 bytes, beginning with a lowercase ASCII
 468 /// letter and containing only lowercase letters, digits, or underscores. The
 469 /// source envelope accepts a list of 1 to 24 obligations, and every key must be
 470 /// unique within that list. Validation mandates the capacity_model role in
 471 /// every claim, the overload role unless overload is not applicable,
 472 /// appropriate risk roles for witnessed risks, and the work_bound role when a
 473 /// work equation is declared. Keys remain local to the enclosing claim rather
 474 /// than resolving globally.
 475 pub const Obligation = declaration.Obligation;
 476 /// ObligationRole classifies the evidentiary purpose of a named obligation
 477 /// within a claim. Roles identify evidence requirements including
 478 /// capacity_model, overload, work_bound, transitive_risk, foreign_risk, seal,
 479 /// and teardown. Declaration validation enforces role presence rules for
 480 /// selected source fields, requiring capacity_model for every claim, overload
 481 /// unless overload handling is not applicable, work_bound when a work equation
 482 /// is present, and matching risk roles when transitive or foreign risks are
 483 /// witnessed. Assigning a role classifies the requirement within the
 484 /// declaration but does not establish that evidence exists or that any test
 485 /// passed.
 486 pub const ObligationRole = declaration.ObligationRole;
 487 /// `WitnessAnnotation` holds `claim_id` and `obligation_key` slices alongside a
 488 /// `role` value. The `witness` operation requires `Owner.claim` to have the
 489 /// exact type `Declaration` and verifies that the obligation key exists, but it
 490 /// does not validate the whole claim. Passing the returned annotation to
 491 /// `record` associates it with the enclosing test. Constructing the annotation
 492 /// alone does not record an association with a test or prove that a test
 493 /// passed, and it performs no test execution or assertion inspection.
 494 pub const WitnessAnnotation = declaration.WitnessAnnotation;
 495 /// witness extracts a WitnessAnnotation for a specified Owner type and
 496 /// obligation key at compile time. It requires that Owner declare a public
 497 /// member named claim whose type is exactly Declaration, and that the
 498 /// obligation key exists within the claim obligations list, failing compilation
 499 /// if either condition is not met. It returns a WitnessAnnotation containing
 500 /// the claim id, obligation key, and associated obligation role from the source
 501 /// envelope. The function does not run full declaration validation, inspect
 502 /// test logic, or execute tests.
 503 pub const witness = declaration.witness;
 504 /// `record` enters a witness annotation into the Stardust claim table for the
 505 /// enclosing test. It is `inline`, so the test stays the compiler's analysis
 506 /// owner. Without the Stardust observer, as in a release, it records nothing.
 507 pub const record = declaration.record;
 508 /// ObligationSelector identifies a claim-local obligation that grounds a
 509 /// theorem premise through its key field. Validation checks that the key is a
 510 /// valid local identifier and that it matches an obligation declared in the
 511 /// current source envelope. The check enforces no role restriction on the
 512 /// targeted obligation and performs no evaluation of the theorem.
 513 pub const ObligationSelector = declaration.ObligationSelector;
 514 /// ClaimSelector designates an external claim supporting a certified summary
 515 /// premise through its id field. Validation confirms that the id string
 516 /// satisfies the syntax of a canonical dotted identifier containing at least
 517 /// two segments. The check verifies identifier syntax only and does not look up
 518 /// or confirm the existence of the referenced claim.
 519 pub const ClaimSelector = declaration.ClaimSelector;
 520 /// TrustDeclarationSelector identifies a trust declaration supporting a trusted
 521 /// user, external component, or environment premise through its id field.
 522 /// Validation checks that the id string conforms to canonical dotted identifier
 523 /// syntax. The validator performs no resolution of the external identifier and
 524 /// does not validate the underlying trust declaration.
 525 pub const TrustDeclarationSelector = declaration.TrustDeclarationSelector;
 526 /// Typed capacity specification holding semantic bindings: `Spec` bundles
 527 /// borrowed slices of typed `Input` definitions, ordered `Node` entries,
 528 /// `Assertion` claims, and optional `TypeSelector` bindings. Valid
 529 /// specifications contain up to 48 inputs, up to 16 type selectors, 1 to 64
 530 /// nodes, and 1 to 8 assertions, with inputs and type selectors permitted to be
 531 /// empty. Because `Input` and `TypeSelector` contain compile-time type
 532 /// references, a `Spec` is constructed at compile time and does not validate
 533 /// invariants upon instantiation. The enclosing owner declaration validation
 534 /// routine invokes the internal typed `validate` function to check structural
 535 /// and layout rules.
 536 pub const Spec = spec.Spec;
 537 /// Type-erased view of a capacity specification: `View`, re-exported at the
 538 /// package root as `SpecView`, represents a specification using `InputView` and
 539 /// `TypeSelectorView` slices alongside expression nodes and assertions. All
 540 /// slices are borrowed, and callers can construct or provide a `View` at
 541 /// runtime because it contains no compile-time type fields. The internal
 542 /// compile-time `view` constructor produces view slices with static storage
 543 /// lifetime, but arbitrary runtime instances do not own underlying memory or
 544 /// guarantee static persistence.
 545 pub const SpecView = spec.View;
 546 /// Specification input parameter holding compile-time type information: `Input`
 547 /// defines an external input with an identifier string (`id`), a compile-time
 548 /// limit type (`limits_type`), a navigation path (`field_path`), and an
 549 /// expected category (`leaf_class`). The identifier must contain 1 to 64 bytes
 550 /// beginning with a lowercase ASCII letter followed by lowercase alphanumeric
 551 /// characters or underscores, and must be unique across all inputs. Because
 552 /// `limits_type` stores a compile-time type, constructing an `Input` occurs at
 553 /// compile time, borrowing string slices for the identifier and path
 554 /// diagnostic. Typed validation confirms that `limits_type` matches the
 555 /// expected limits type and that following the ordinal path through that type
 556 /// yields the declared `leaf_class`.
 557 pub const Input = spec.Input;
 558 /// Type-erased description of a specification input: `InputView` retains the
 559 /// identifier string (`id`), ordinal path (`field_path`), and classification
 560 /// tag (`leaf_class`) while omitting the compile-time type binding. It holds
 561 /// borrowed string slices suitable for runtime inspection and digest
 562 /// computation. Structural validation checks identifier syntax and path bounds,
 563 /// but cannot verify whether the path corresponds to a field in any concrete
 564 /// Zig type.
 565 pub const InputView = spec.InputView;
 566 /// Category of data held at the termination of a field path: `LeafClass`
 567 /// classifies inputs as `unsigned_integer`, `signed_integer`, `collection`, or
 568 /// `byte_collection`. When resolving fields in `bindInput`, integers up to 64
 569 /// bits produce integer classes, slices of `u8` yield `byte_collection`, and
 570 /// slices of other element types become `collection`. Expression validation
 571 /// enforces that `Node.input` references only integer classes, collection
 572 /// length projections accept both slice classes, and byte count projections
 573 /// target only `byte_collection`.
 574 pub const LeafClass = spec.LeafClass;
 575 /// Compile-time metadata binding for a referenced memory type: `TypeSelector`
 576 /// pairs an identifier string (`id`) with a compile-time type
 577 /// (`selected_type`), a size in bytes (`byte_size`), and a byte alignment
 578 /// requirement (`byte_alignment`). Identifiers must be unique across all
 579 /// selectors in a specification. Constructing a selector through `bindType`
 580 /// captures the results of `@sizeOf` and `@alignOf` without taking ownership of
 581 /// the underlying type. Typed validation verifies that the stored size and
 582 /// alignment match the type, and that alignment is a non-zero power of two.
 583 pub const TypeSelector = spec.TypeSelector;
 584 /// `TypeSelectorView` exposes only a borrowed identifier while omitting
 585 /// `selected_type`, `byte_size`, and `byte_alignment`. Structural validation
 586 /// verifies identifier grammar and confirms uniqueness across all selectors in
 587 /// the view. The digest incorporates the selector identifier without erased
 588 /// semantic type or layout details. An entire specification digest cannot be
 589 /// assumed independent of host layout because other graph nodes may encode
 590 /// concrete layout values.
 591 pub const TypeSelectorView = spec.TypeSelectorView;
 592 /// Compile-time type binding for input limits and type selectors:
 593 /// `SemanticType` is an alias for the Zig language primitive `type`. It
 594 /// captures compile-time type identity during specification definition rather
 595 /// than serializing a runtime type identifier. This binding allows compile-time
 596 /// validation to inspect memory layout properties directly from the type
 597 /// system.
 598 pub const SemanticType = spec.SemanticType;
 599 /// `BoundedFieldOrdinalPath` represents a static path through nested structs
 600 /// using a fixed array of eight `u16` field ordinals, an active `u8` length,
 601 /// and a borrowed diagnostic string. The ordinals are zero-based field indices
 602 /// in nested structs rather than memory byte offsets. The active length must
 603 /// range from 1 to 8. The diagnostic string must consist of 1 to 256 bytes
 604 /// formed by non-empty dot-separated ASCII segments containing letters, digits,
 605 /// or underscores, with uppercase characters permitted. Typed validation
 606 /// follows the actual field indices and verifies the leaf class. Structural
 607 /// validation checks diagnostic syntax without resolving the diagnostic
 608 /// spelling against field definitions. The computed hash covers the active
 609 /// length and active ordinals while excluding the diagnostic string and unused
 610 /// tail ordinals. The structure does not perform runtime navigation operations.
 611 pub const BoundedFieldOrdinalPath = spec.BoundedFieldOrdinalPath;
 612 /// `FieldPath` is a type alias for `BoundedFieldOrdinalPath`, providing eight
 613 /// fixed field-index slots alongside an active length. The type maintains
 614 /// identical ordinal constraints and shares the lifetime of its borrowed
 615 /// diagnostic string without treating indices as memory offsets.
 616 pub const FieldPath = spec.FieldPath;
 617 /// Failure reason for capacity specification validation: `Violation`,
 618 /// re-exported at the package root as `SpecViolation`, enumerates the first
 619 /// structural or typed rule failure encountered during validation. The
 620 /// specification does not enforce any rule that rejects unused or unreferenced
 621 /// graph nodes. An invalid assertion expression failure specifically denotes a
 622 /// referenced node index that is out of bounds rather than an arithmetic
 623 /// evaluation error.
 624 pub const SpecViolation = spec.Violation;
 625 /// Expression graph node union: `Node` defines the operations of the capacity
 626 /// expression language through tags `constant`, `input`, `add`, `maximum`,
 627 /// `scale`, `product`, `alignment`, `ceiling_division`, `conditional`,
 628 /// `next_power_of_two`, and `collection`. Nodes form an ordered acyclic graph
 629 /// bounded to at most 64 entries in a valid specification. Structural
 630 /// validation requires operand node indices to strictly precede the current
 631 /// node position, while inputs and collection projections must address valid
 632 /// inputs matching their required leaf classes. Validation does not evaluate
 633 /// expressions, check for division by zero, guard against arithmetic overflow,
 634 /// or verify value positivity.
 635 pub const Node = spec.Node;
 636 /// Binary operand reference for node expressions: `Pair` holds two 16-bit
 637 /// unsigned integer indices, `left` and `right`. Both indices address earlier
 638 /// nodes in the ordered expression array rather than input indices. Structural
 639 /// validation enforces this directed acyclic graph ordering by requiring that
 640 /// both indices strictly precede the position of the containing node.
 641 pub const Pair = spec.Pair;
 642 /// Symbolic multiplication of a node by a scaling factor: `Scale` combines a
 643 /// 16-bit expression node index (`node`) with a `Coefficient` multiplier.
 644 /// Validation requires that the referenced node index appears earlier in the
 645 /// expression sequence, and enforces selector bounds if the coefficient
 646 /// references a concrete type. The structure describes a mathematical scaling
 647 /// operation without calculating a product or checking for integer overflow.
 648 pub const Scale = spec.Scale;
 649 /// The `Alignment` union represents an alignment requirement as either a
 650 /// literal `u64` value or a `concrete_type` referencing a `u16` selector index.
 651 /// Validation requires a literal value to be a non-zero power of two, or a
 652 /// concrete index to reside within the valid selector range. Typed validation
 653 /// examines selector size and alignment facts for concrete selections. A view
 654 /// provides only the selector identifier for concrete selection, whereas a
 655 /// literal `Alignment` retains its explicit numeric value. The type provides no
 656 /// runtime allocation guarantee.
 657 pub const Alignment = spec.Alignment;
 658 /// Symbolic rounding descriptor targeting a memory boundary: `Align` pairs a
 659 /// 16-bit expression node index (`node`) with an `Alignment` rule. Structural
 660 /// validation requires the target node index to strictly precede the position
 661 /// of the current node. This struct describes a symbolic rounding calculation
 662 /// for byte capacity expressions, rather than providing guarantees about
 663 /// allocated pointer addresses.
 664 pub const Align = spec.Align;
 665 /// Relational operator tag for conditional expressions: `Comparison` defines
 666 /// the tags `equal`, `not_equal`, `less_than`, `less_or_equal`, `greater_than`,
 667 /// and `greater_or_equal` for use inside a `Predicate`. Constructing a
 668 /// comparison tag specifies the intended condition between two node values.
 669 /// This module does not evaluate predicates or compare actual input values.
 670 pub const Comparison = spec.Comparison;
 671 /// Comparison expression linking two node operands: `Predicate` combines a
 672 /// `Comparison` operator with two 16-bit node indices, `left` and `right`. When
 673 /// validated inside a `Conditional` node, both operand indices must strictly
 674 /// precede the containing node index. The structure defines a declarative
 675 /// relational test without evaluating operands or storing boolean results.
 676 pub const Predicate = spec.Predicate;
 677 /// Branching expression selecting between alternative expressions:
 678 /// `Conditional` holds a `Predicate` condition together with two 16-bit node
 679 /// indices, `when_true` and `when_false`. Validation requires all referenced
 680 /// nodes, including both predicate operands and both branch targets, to appear
 681 /// earlier in the expression sequence than the conditional node itself. The
 682 /// structure represents branch selection declaratively without executing either
 683 /// branch or verifying path reachability.
 684 pub const Conditional = spec.Conditional;
 685 /// Character occurrence counter for a byte slice: `ByteCount` pairs a 16-bit
 686 /// input index (`input`) with an 8-bit byte value (`byte`). When referenced by
 687 /// a collection projection node, validation verifies that the addressed input
 688 /// exists and possesses a `byte_collection` leaf classification. The struct
 689 /// declaratively describes counting occurrences of the specified byte within
 690 /// the input slice without scanning memory or computing sums.
 691 pub const ByteCount = spec.ByteCount;
 692 /// Measurement extraction from collection inputs: `CollectionProjection` is a
 693 /// tagged union supporting either a `length` query taking a 16-bit input index
 694 /// or a `byte_count` query holding a `ByteCount` descriptor. Unlike binary
 695 /// arithmetic operators, these indices address entries in the specification
 696 /// input list rather than expression nodes. Structural validation rejects
 697 /// scalar integer inputs, permitting `length` on both general slices and byte
 698 /// slices while restricting `byte_count` exclusively to byte slices.
 699 pub const CollectionProjection = spec.CollectionProjection;
 700 /// Multiplication factor operand in a scaling expression: `Coefficient` is a
 701 /// tagged union representing either a 64-bit constant (`literal`), an
 702 /// unresolved integer parameter index (`unsigned_comptime_parameter`), a
 703 /// generic type parameter index (`size_of_type_parameter`), or a concrete type
 704 /// selector index (`size_of_concrete_type`). The parameter variants act as
 705 /// declarative placeholders whose concrete values are not resolved by this
 706 /// module. Structural validation checks that `size_of_concrete_type` references
 707 /// an index within the specification type selector list. Construction and
 708 /// validation do not compute products or perform arithmetic multiplication.
 709 pub const Coefficient = spec.Coefficient;
 710 /// Formal capacity claim for a completed expression: `Assertion` binds a
 711 /// `Scope`, a `Measure`, and a `Relation` to a 16-bit node index
 712 /// (`expression`). Structural validation checks that the referenced expression
 713 /// index points to a valid node within the specification node array.
 714 /// Constructing or validating an `Assertion` does not invoke runtime assertion
 715 /// checks, evaluate expression values, or verify agreement with derived
 716 /// allocation bounds.
 717 pub const Assertion = spec.Assertion;
 718 /// The `Scope` enumeration provides the sole tag `closure_total` to label the
 719 /// evaluation scope of an `Assertion`. The module provides no evaluator,
 720 /// automatic traversal of an owner graph, or proof of transitive coverage. A
 721 /// source type alone does not establish a precise dynamic footprint for an
 722 /// operation.
 723 pub const Scope = spec.Scope;
 724 /// The `Measure` enumeration selects a quantity label within an `Assertion`
 725 /// using tags `reserved`, `committed`, `live`, or `retained`. The measurement
 726 /// tag belongs directly to the `Assertion` rather than to an expression node.
 727 /// This module does not measure allocations or evaluate runtime quantities.
 728 /// Scope and supporting evidence are supplied by an enclosing claim and
 729 /// downstream analysis.
 730 pub const Measure = spec.Measure;
 731 /// Comparison intent for an asserted bound: `Relation` distinguishes whether an
 732 /// expression represents an `upper_bound` or an `exact` quantity in an
 733 /// `Assertion`. The tag declares the intended relation between the selected
 734 /// `Measure` and the target expression node. Structural validation verifies
 735 /// that the referenced expression node index falls within the defined node
 736 /// array, but does not check whether the mathematical relationship holds true.
 737 pub const Relation = spec.Relation;
 738 /// This validator limit specifies a maximum of 64 bytes for canonical dotted
 739 /// claim, dependency, or trust identifiers, under the root alias
 740 /// `claim_id_bytes_max`.
 741 pub const claim_id_bytes_max = declaration.id_bytes_max;
 742 /// This constant defines the 32-byte SHA-256 output digest size corresponding
 743 /// to the root alias `declaration_envelope_digest_bytes`. This value reflects
 744 /// the fixed digest output length rather than the input envelope size.
 745 pub const declaration_envelope_digest_bytes = declaration.digest_bytes;
 746 /// Byte length of the specification digest: `digest_bytes` is an integer
 747 /// constant set to 32, exported at the package root as `spec_digest_bytes`. It
 748 /// reflects the fixed 32-byte output length of the underlying SHA-256
 749 /// cryptographic hash rather than the serialized length of the input data.
 750 pub const spec_digest_bytes = spec.digest_bytes;
 751 /// This validator limit specifies a maximum of 16 covered storage records in
 752 /// `SourceEnvelope.storage.covered`, requiring a valid list to be non-empty.
 753 pub const declaration_covered_max = declaration.covered_max;
 754 /// This validator limit defines a maximum of 16 excluded descriptive strings in
 755 /// a valid non-empty list, without enforcing a uniqueness check.
 756 pub const declaration_excluded_max = declaration.excluded_max;
 757 /// This validator limit defines a maximum of 8 canonical dependency
 758 /// identifiers, permitting an empty list.
 759 pub const declaration_dependencies_max = declaration.dependencies_max;
 760 /// This validator limit specifies a maximum of 24 named obligation records,
 761 /// requiring a valid list to be non-empty.
 762 pub const declaration_obligations_max = declaration.obligations_max;
 763 /// identifierValid checks whether a byte slice adheres to canonical dotted
 764 /// identifier grammar, returning true on success. The slice must contain 1 to
 765 /// 64 bytes divided into at least two non-empty segments separated by dots.
 766 /// Segment characters are restricted to lowercase ASCII letters, digits, and
 767 /// underscores, and segments may begin with a digit or underscore. The function
 768 /// validates canonical identifier syntax only, without performing external
 769 /// registry lookups or enforcing claim-local key grammar.
 770 pub const identifierValid = declaration.identifierValid;
 771 /// Upper bound on specification inputs: `inputs_max` is an integer constant set
 772 /// to 48, exported at the package root as `spec_inputs_max`. Specifications may
 773 /// declare anywhere from zero up to 48 inputs inclusive. Validation returns an
 774 /// error violation if an input list exceeds this bound.
 775 pub const spec_inputs_max = spec.inputs_max;
 776 /// Historical limit for specification inputs: `inputs_max_v1` is an integer
 777 /// constant set to 16, exported at the package root as `spec_inputs_max_v1`. It
 778 /// records the earlier input capacity bound from initial specification
 779 /// revisions. Current validation routines enforce `inputs_max` instead of this
 780 /// historical threshold.
 781 pub const spec_inputs_max_v1 = spec.inputs_max_v1;
 782 /// Schema revision constant for specification input limits:
 783 /// `input_bound_version` is a 16-bit integer constant with value 2, exported at
 784 /// the package root as `spec_input_bound_version`. It identifies the
 785 /// specification revision that expanded the maximum input capacity to 48. This
 786 /// value tracks input bound sizing rather than the digest domain version or an
 787 /// automatic schema conversion mechanism.
 788 pub const spec_input_bound_version = spec.input_bound_version;
 789 /// Upper bound on specification type selectors: `type_selectors_max` is an
 790 /// integer constant set to 16, exported at the package root as
 791 /// `spec_type_selectors_max`. A specification may include an empty type
 792 /// selector list or up to 16 selectors. Validation checks this limit during
 793 /// structural inspection.
 794 pub const spec_type_selectors_max = spec.type_selectors_max;
 795 /// Upper bound on expression graph nodes: `nodes_max` is an integer constant
 796 /// set to 64, exported at the package root as `spec_nodes_max`. A valid
 797 /// specification requires at least one node and permits at most 64 nodes in its
 798 /// ordered expression sequence.
 799 pub const spec_nodes_max = spec.nodes_max;
 800 /// Upper bound on specification assertions: `assertions_max` is an integer
 801 /// constant set to 8, exported at the package root as `spec_assertions_max`. A
 802 /// valid specification must contain at least one assertion and at most 8
 803 /// assertions.
 804 pub const spec_assertions_max = spec.assertions_max;
 805 /// Maximum nesting depth for field navigation paths: `field_path_depth_max` is
 806 /// an integer constant set to 8, exported at the package root as
 807 /// `spec_field_path_depth_max`. It defines the maximum number of ordinal field
 808 /// indices stored within a `BoundedFieldOrdinalPath`. Valid paths must contain
 809 /// at least one ordinal and cannot exceed eight traversal steps.
 810 pub const spec_field_path_depth_max = spec.field_path_depth_max;
 811 /// Specifies the structural protocol expected of a memory owner across two
 812 /// independent axes: storage acquisition, defined by `StorageSource`, and
 813 /// exhaustion behavior, defined by `OverloadShape`. Four named constants
 814 /// represent the valid combinations: `allocator_exact`, `allocator_rejecting`,
 815 /// `provisioned_exact`, and `provisioned_rejecting`. This classification
 816 /// constrains required container declarations, field layouts, and lifecycle
 817 /// function signatures during compile-time shape validation. It does not
 818 /// inspect function bodies, verify that resource bounds are maintained at
 819 /// runtime, or prove the dynamic correctness of owner operations. An `exact`
 820 /// classification indicates only that the shape contract requires no
 821 /// steady-state exhaustion error. It does not promise that operational methods
 822 /// are infallible or that runtime failures cannot occur.
 823 pub const OwnerShape = owner.OwnerShape;
 824 /// Enumerates the first structural check failure detected when validating an
 825 /// owner type against an expected `OwnerShape`. Tags cover missing or malformed
 826 /// declarations, incorrect runtime fields, mismatched lifecycle signatures,
 827 /// prohibited allocator capabilities, invalid exhaustion declarations, and
 828 /// missing or invalid claims. When an owner declares an invalid claim,
 829 /// `validateOwnerShape` collapses the underlying `DeclarationViolation` into
 830 /// the single tag `invalid_claim`. In contrast, `requireOwnerShape` validates
 831 /// the claim directly through `declaration.require` before running shape
 832 /// checks, emitting detailed compile errors for specific declaration failures.
 833 /// Because compile-time reflection can encounter malformed syntax or illegal
 834 /// type definitions in user declarations, passing arbitrary malformed types to
 835 /// validation functions may produce compiler errors rather than returning an
 836 /// optional violation cleanly.
 837 pub const OwnerShapeViolation = shape.OwnerShapeViolation;
 838 /// Defines the lifecycle phases shared across allocator guards:
 839 /// `initialization`, `steady`, and `teardown`. Runtime guards use these values
 840 /// to classify incoming raw allocator calls. Under this classification,
 841 /// `initialization` permits every raw operation, `steady` marks all raw
 842 /// operations as violations, and `teardown` permits only deallocations while
 843 /// marking allocations, resizes, and remaps as violations. Depending on the
 844 /// selected guard type, a violation either triggers an immediate panic or
 845 /// increments audit counters before forwarding the call to the backing
 846 /// allocator. The enumeration itself is an unadorned data type that enforces no
 847 /// transition rules or operational policies on other owners.
 848 pub const Phase = phase.Phase;
 849 /// Defines three static bounds for owner lifecycle and maintenance work:
 850 /// `transition_steps_max`, `cleanup_steps_per_call_max`, and
 851 /// `cleanup_calls_at_capacity_max`. Structural validation requires
 852 /// `transition_steps_max` to be greater than zero. The cleanup bounds must be
 853 /// either both zero or both nonzero, and their arithmetic product must fit
 854 /// within `usize` without overflow. These bounds are literal numeric
 855 /// declarations checked solely for structural validity. Validation does not
 856 /// measure CPU instructions, inspect loop constructs, or evaluate wall-clock
 857 /// duration. In implementations providing cleanup routines, the work performed
 858 /// by each cleanup step may depend on the extent of stored data rather than a
 859 /// constant processing cost.
 860 pub const WorkLimits = owner.WorkLimits;
 861 /// declarationEnvelopeDigest computes the digest of a compile-time Declaration
 862 /// by converting its source envelope through sourceView and hashing the
 863 /// resulting EnvelopeView with envelopeDigest. Because the view omits bindings,
 864 /// changes to bindings such as the owner type, seam functions, or premises do
 865 /// not affect the digest. The underlying capacity digest also omits semantic
 866 /// types and sizing facts. The resulting hash establishes a content identity
 867 /// for selected source specification fields rather than an identity for the
 868 /// whole implementation or its evidence.
 869 pub const declarationEnvelopeDigest = declaration.declarationEnvelopeDigest;
 870 /// envelopeDigest hashes the content of an EnvelopeView using SHA-256 under the
 871 /// domain tiny.alloc.claim-declaration/v2, and is exported from root.zig as
 872 /// declarationSourceEnvelopeDigest. The digest builder length-frames every
 873 /// field and ordered list element, incorporating storage details, the capacity
 874 /// specification digest, overload policy, risks, optional work equations,
 875 /// dependencies, and obligations. Because the view contains no bindings, all
 876 /// typed bindings and premises are excluded from the digest. The function
 877 /// performs no validation or formal proof, requiring callers to provide a valid
 878 /// bounded view.
 879 pub const declarationSourceEnvelopeDigest = declaration.envelopeDigest;
 880 /// The `digest` function, corresponding to the root identifier
 881 /// `capacitySpecDigest`, generates a 32-byte SHA-256 digest using the domain
 882 /// string `tiny.alloc.capacity-spec/v3`. Serialization employs length framing
 883 /// for field names and values while encoding numeric values as little-endian
 884 /// `u64` words and preserving input list order. The digest incorporates input
 885 /// identifiers, input classes, active ordinal paths, selector identifiers,
 886 /// nodes, and assertions. It omits diagnostic strings, `Limits` type
 887 /// identities, and selector concrete type identities along with their size and
 888 /// alignment values. The function performs no internal sorting, algebraic
 889 /// normalization, or structural validation, assuming the caller supplies a
 890 /// valid bounded view. The resulting hash distinguishes only the selected
 891 /// serialized fields and does not attest to overall semantic equivalence, full
 892 /// implementation behavior, or supporting evidence.
 893 pub const capacitySpecDigest = spec.digest;
 894 /// The `validateView` function, known under the root name `validateSpecView`,
 895 /// accepts a specification `View` and executes at compile time or runtime to
 896 /// return an optional first `Violation` or null. The validator verifies
 897 /// structural bounds requiring 0 to 48 inputs, 0 to 16 selectors, 1 to 64
 898 /// nodes, and 1 to 8 assertions. Checks include identifier grammar and
 899 /// uniqueness within each input and selector collection, path structure and
 900 /// diagnostic syntax, references to strictly earlier node operands, input leaf
 901 /// and projection compatibility, concrete selector index ranges, literal
 902 /// power-of-two alignments, and in-bounds assertion node indices. The function
 903 /// cannot inspect semantic `Limits` or concrete type facts that are omitted
 904 /// from the view. The implementation does not evaluate arithmetic operations,
 905 /// verify division denominator values, detect numerical overflow, or resolve
 906 /// generic parameter values.
 907 pub const validateSpecView = spec.validateView;
 908 /// Compile-time constructor linking an input identifier to a nested struct
 909 /// field: `bindInput` evaluates at compile time to validate the syntax of an
 910 /// identifier and a dot-separated diagnostic path against a target `Limits`
 911 /// type. It reflects over struct fields to build an ordinal navigation path and
 912 /// deduce the field `LeafClass`. The function emits a compile error if a field
 913 /// name does not exist, an intermediate element is not a struct, traversal
 914 /// depth exceeds eight levels, or the leaf type is unsupported. Supported leaf
 915 /// types include integers up to 64 bits and slices, while fixed-size arrays and
 916 /// wider integers are rejected. Execution raises the compiler evaluation branch
 917 /// quota to 10000 to resolve nested types, and does not inspect runtime values.
 918 pub const bindInput = spec.bindInput;
 919 /// Compile-time constructor capturing layout metrics for a named type:
 920 /// `bindType` validates an identifier string at compile time and queries the
 921 /// size and alignment of type `T` using `@sizeOf` and `@alignOf`. Invalid
 922 /// identifier syntax or types that disallow size and alignment inspection
 923 /// produce a compile error. The function records numeric layout metrics
 924 /// directly without allocating memory, generating runtime type tokens, or
 925 /// validating the enclosing `Spec`.
 926 pub const bindType = spec.bindType;
 927 /// selector takes any compile-time value and returns an anonymous struct type
 928 /// containing a public constant named declaration initialized to that value.
 929 /// This helper allows compile-time type fields to transport typed references
 930 /// and values. The requirement that declaration resolve to a function is not
 931 /// checked by selector itself, but is imposed only when validating a phase
 932 /// binding family. The function neither validates the wrapped value nor creates
 933 /// a callable runtime closure.
 934 pub const selector = declaration.selector;
 935 /// The current implementation of `declareDynamicUnbounded` checks a canonical
 936 /// dotted `id` at compile time and discards `Owner`. It does not inspect
 937 /// whether `Owner` actually allocates, install behavior, record observer
 938 /// metadata, or register a proven bound.
 939 pub const declareDynamicUnbounded = declaration.declareDynamicUnbounded;
 940 /// declareWarmRetained declares a weak capacity owner associated with warm
 941 /// retained memory. It checks at compile time that the provided id satisfies
 942 /// canonical dotted identifier syntax and discards the Owner type parameter.
 943 /// The function records no observer claims and performs no actual
 944 /// retention policy, owner shape, or capacity bound checks.
 945 pub const declareWarmRetained = declaration.declareWarmRetained;
 946 /// This compile-time check validates an allocator_exact owner shape. It
 947 /// inspects Limits and Capacity declarations, runtime phase and capacity
 948 /// declarations, and allocator-backed lifecycle signatures. An immediate
 949 /// capability scanner examines stored fields as well as known parameters and
 950 /// results of non-lifecycle receiver methods, while lifecycle init and deinit
 951 /// intentionally accept an Allocator. An optional claim is validated and
 952 /// recorded through the Stardust observer. Any invalid declaration or shape
 953 /// causes a compile error. The check does not run owner code.
 954 pub const requireAllocatorExactOwnerShape = shape.requireAllocatorExactOwnerShape;
 955 /// This compile-time check validates an allocator_rejecting owner shape. It
 956 /// shares allocator-backed fields and lifecycle signatures with allocator_exact
 957 /// but enforces different overload requirements rather than all exact
 958 /// requirements. The owner must expose a finite nonempty Exhaustion error set
 959 /// on a non-lifecycle pointer-receiver method. Any optional claim is checked
 960 /// for compatibility under the rejecting shape and recorded. The validation
 961 /// performs structural and type checks only.
 962 pub const requireAllocatorRejectingOwnerShape = shape.requireAllocatorRejectingOwnerShape;
 963 /// Enforces at compile time that an owner type conforms to the
 964 /// caller-provisioned exact protocol (`OwnerShape.provisioned_exact`). The
 965 /// owner must declare a positive power-of-two `storage_alignment`, matching
 966 /// aligned slice `Storage`, and typed `work_limits`. Runtime fields must
 967 /// include `phase: Phase`, `capacity: Capacity` (containing a runtime
 968 /// `storage_bytes: usize`), and `storage: Storage`. Lifecycle functions must
 969 /// implement specific signatures: `Capacity.derive` and `init` must return
 970 /// finite nonempty error unions, `activate` must return `void` exactly, and
 971 /// `deinit` must return `Storage` exactly. A typed `claim` declaration is
 972 /// mandatory and validated. Recursive capability checks verify that stored
 973 /// fields, `Limits`, `Capacity`, and non-lifecycle method signatures contain no
 974 /// allocator capabilities. Any violation causes a compile error. Conformance
 975 /// does not execute owner code or verify runtime buffer management.
 976 pub const requireProvisionedExactOwnerShape = shape.requireProvisionedExactOwnerShape;
 977 /// This compile-time check validates a provisioned_rejecting owner shape. It
 978 /// shares provisioned storage, fields, lifecycle, and work rules with
 979 /// provisioned_exact, but enforces distinct overload requirements instead of
 980 /// all exact requirements. The owner must expose a finite nonempty Exhaustion
 981 /// error set on a non-lifecycle pointer-receiver method, and its claim overload
 982 /// kind must be reject_before_mutation. The validator verifies this
 983 /// classification and records a valid claim without inspecting actual protected
 984 /// payload or diagnostic mutation. Callers should read the owner claim detail
 985 /// to identify protected state. Any failed declaration or shape triggers a
 986 /// compile error.
 987 pub const requireProvisionedRejectingOwnerShape = shape.requireProvisionedRejectingOwnerShape;
 988 /// Recursively inspects a compile-time type to detect whether it exposes an
 989 /// allocator capability. The traversal follows typed pointers, arrays, vectors,
 990 /// optionals, error-union payloads, struct and union fields, and container
 991 /// receiver methods whose return types lead to an allocator. It maintains a
 992 /// compile-time tuple of visited containers to prevent infinite loops on
 993 /// recursive data structures, and recognizes `std.mem.Allocator` as an
 994 /// immediate capability. For bare function types, the check examines only the
 995 /// return type, without scanning parameter lists. This public recursive
 996 /// inspector differs from the narrower internal scanner used by
 997 /// allocator-backed shapes, which inspects only immediate field types and
 998 /// container allocator methods. The function does not inspect function bodies,
 999 /// detect global allocator variables, or track capabilities through type-erased
1000 /// pointers such as `*anyopaque`. It does not prove that runtime execution is
1001 /// free from allocation side effects.
1002 pub const typeHasAllocatorCapability = capability.typeHasAllocatorCapability;
1003 /// Validates that an owner type conforms to `OwnerShape.allocator_exact`,
1004 /// returning an optional `OwnerShapeViolation`. It uses an immediate shallow
1005 /// capability scanner that inspects stored fields and method signatures for
1006 /// direct references to `std.mem.Allocator` or container allocator factories.
1007 /// If a valid typed `claim` is declared, the function records claim metadata at
1008 /// compile time. A return value of `null` confirms that all structural checks
1009 /// passed. It does not prove that owner methods avoid runtime heap allocation
1010 /// or that dynamic memory behavior is infallible.
1011 pub const validateAllocatorExactOwnerShape = shape.validateAllocatorExactOwnerShape;
1012 /// This function validates an allocator_rejecting owner shape, returning the
1013 /// first OwnerShapeViolation or null. It shares allocator-backed lifecycle and
1014 /// field rules with the exact shape but does not require all exact claim
1015 /// policies. It instead adds an Exhaustion surface requirement and verifies
1016 /// claim compatibility for the rejecting shape when a claim is present. The
1017 /// function executes a shallow capability scan, records any valid present
1018 /// claim, and does not prove error reachability.
1019 pub const validateAllocatorRejectingOwnerShape = shape.validateAllocatorRejectingOwnerShape;
1020 /// validate evaluates a compile-time Declaration against an Owner type and an
1021 /// OwnerShape, returning the first detected Violation or null if validation
1022 /// passes, and is exported from root.zig as validateDeclaration. It checks
1023 /// identifier syntax, storage limits, the typed capacity specification against
1024 /// Owner.Limits, overload compatibility and detail text, risks, work equations,
1025 /// dependencies, obligations, and bindings. The function does not run the owner
1026 /// shape validator or record observer claims. Returning null
1027 /// indicates only that the declaration metadata is valid. The Owner type must
1028 /// define a Limits type compatible with the capacity specification, and the
1029 /// function makes no promise of universal safety for arbitrary type
1030 /// introspection.
1031 pub const validateDeclaration = declaration.validate;
1032 /// `validatePremise` accepts a compile-time `SourceEnvelope` and premise pair
1033 /// and returns the first optional `Violation` or null. It checks classification
1034 /// and authority compatibility between the supplied entities. For `theorem`,
1035 /// the function validates the local key and its existence in source obligations
1036 /// without applying role restrictions. Both `certified_claim` and `trusted`
1037 /// validate canonical `id` syntax without performing a registry lookup. The
1038 /// function does not validate the whole `SourceEnvelope` or inspect underlying
1039 /// evidence.
1040 pub const validatePremise = declaration.validatePremise;
1041 /// Inspects a type at compile time against an expected `OwnerShape`, returning
1042 /// `null` if the type satisfies the protocol or the first `OwnerShapeViolation`
1043 /// if a check fails. If the owner provides a valid typed `claim`, the function
1044 /// records claim metadata through the Stardust observer, linking the claim to
1045 /// `init`, default limits, and lifecycle family declarations. Allocator-backed
1046 /// owners may omit a claim, in which case validation succeeds without recording
1047 /// claim metadata. Provisioned owners require a valid claim. Validation
1048 /// examines types, declarations, and signatures without executing owner
1049 /// functions, allocating resources, or verifying that declared formal
1050 /// obligations are mathematically discharged.
1051 pub const validateOwnerShape = shape.validateOwnerShape;
1052 /// This function validates a provisioned_exact owner shape, returning the first
1053 /// violation or null. It verifies runtime phase, capacity, and storage
1054 /// declarations, ensuring an aligned Storage type and a Capacity.storage_bytes
1055 /// field. It also verifies a typed claim and a work_limits declaration, noting
1056 /// that work_limits is a compile-time declaration rather than a runtime field.
1057 /// A recursive capability scan inspects the owner including Limits and
1058 /// Capacity, and any valid claim is recorded. The function does not execute
1059 /// lifecycle methods.
1060 pub const validateProvisionedExactOwnerShape = shape.validateProvisionedExactOwnerShape;
1061 /// This function validates a provisioned_rejecting owner shape, returning the
1062 /// first violation or null. It applies shared provisioned storage, lifecycle,
1063 /// and work rules while enforcing a different overload classification. The
1064 /// owner must expose a finite nonempty Exhaustion error set on a
1065 /// pointer-receiver method and declare a reject_before_mutation claim overload.
1066 /// A recursive capability scan is performed, and any valid claim is recorded.
1067 /// The function does not itself check payload preservation.
1068 pub const validateProvisionedRejectingOwnerShape = shape.validateProvisionedRejectingOwnerShape;
1069 
1070 /// Demonstrates an implementation of the caller-provisioned exact owner
1071 /// protocol, re-exported from the package root as `ProvisionedExactFixture`.
1072 /// The owner accepts requested capacities from 1 to 64 bytes and requires
1073 /// caller-provided storage at least as long as the requested count. It retains
1074 /// the entire caller slice across its active lifecycle and returns that exact
1075 /// slice upon deinitialization, even when the provided buffer exceeds the
1076 /// requested capacity. Lifecycle transitions are guarded by debug assertions
1077 /// across `initialization`, `steady`, and `teardown` phases without allocating
1078 /// memory or holding an internal allocator. The instance remains caller-backed
1079 /// throughout its existence. It represents a concrete demonstration fixture, so
1080 /// its specific buffer retention and assertion choices should not be taken as
1081 /// universal requirements for all provisioned owners.
1082 pub const ProvisionedExactFixture = @import("fixture.zig").ExactOwner;
1083 /// Demonstrates an implementation of the caller-provisioned rejecting owner
1084 /// protocol, re-exported from the package root as
1085 /// `ProvisionedRejectingFixture`. The owner manages a bounded number of slots,
1086 /// up to 8, with each slot having a positive byte width, backed by
1087 /// caller-supplied 16-byte aligned memory. Calling submit when full returns
1088 /// Full after incrementing both submitted and rejected counts if both
1089 /// increments fit, or returns AccountingOverflow before mutation if an
1090 /// increment would overflow usize. The payload is preserved along either
1091 /// rejection path. Calling cleanupOne pops and zeroes a single slot, while
1092 /// deinit returns the entire original slice without executing a cleanup loop,
1093 /// requiring the caller to keep borrowed bytes alive.
1094 pub const ProvisionedRejectingFixture = @import("fixture.zig").RejectingOwner;