06 Runtime View

Runtime View

This chapter specifies Prism’s behavior at runtime through four scenarios. The scenarios are normative: a conforming Prism implementation MUST exhibit the behavior each scenario describes. The scenarios collectively cover every cross-boundary interaction enumerated in section 3 (Context and Scope) and every component interaction relevant to constraints TC-01 through TC-06 (section 2).

The scenarios are:

• Principal Data Path Execution — what happens at runtime when the application author’s compiled executable processes input through pipeline::run.

• Trace-Replay Verification — what happens when the application user invokes certify_from_trace against a Trace they received.

• Compile-Time UORassembly Enforcement — what happens when the Rust toolchain compiles the application author’s source against prism; not a runtime scenario in the conventional sense, but a deterministic interaction whose specification is necessary for the wiki’s normative completeness.

• Distribute and Run — what happens between the application author finishing compilation and the user obtaining the final output of the executable.

Scenario 1: Principal Data Path Execution

This scenario specifies the runtime behavior of the application author’s compiled executable when it invokes pipeline::run. The interaction is internal to the executable; no external system is contacted, no service is reached, no I/O occurs beyond what the application author’s domain code performs.

Sequence

1. The application’s domain code obtains host bytes from its input source (a file, a stream, a memory buffer — the source is not Prism’s concern).

2. The application invokes the author’s Grounding impl on the host bytes. The Grounding impl is the author’s specification of how host bytes are interpreted as a candidate for admission to the principal data path.

3. The Grounding impl returns either a Datum (the input is admitted) or a typed impossibility witness (the input is rejected at the admission stage). If a witness is returned, this scenario terminates here; the application receives the witness and processes it according to its domain logic.

4. Given a Datum, the application invokes CompileUnitBuilder with the author’s ConstrainedTypeShape impl. The builder accumulates the constraints declared by the shape impl and produces a Validated<CompileUnit, Phase> at intermediate phases.

5. The builder transitions through the validation phases. Each phase confirms a subset of the ConstrainedTypeShape constraints. Failure at any phase produces a typed ShapeViolation and this scenario terminates; the application receives the violation.

6. When all phases succeed, the builder produces Validated<CompileUnit, FinalPhase>.

7. The application invokes prism's pipeline::run (or higher-level pipeline::run_route) with the Validated<CompileUnit, FinalPhase> and the substrate parameters per ADR-030 + ADR-036: H: HostTypes, B: HostBounds, A: AxisTuple + Hasher (the substitution-axis tuple with the canonical hash axis bound — for the canonical first axis, HashAxis from prism-crypto per ADR-031), and R: ResolverTuple (defaulting to NullResolverTuple for verb bodies that emit no resolver-bound ψ-Term variants; otherwise carrying application-provided per-value content). H/B/A flow as type parameters only (axis methods are type-associated and invoked through <A as Hasher>::initial()); R flows as a value reference (resolvers: &R). The Datum admission in step 3 was produced by uor-foundation's mint_datum primitive (called from inside the Grounding impl); subsequent UOR-domain admissions (Triad, Derivation, FreeRank) are produced by uor-foundation's mint primitives, called from inside pipeline::run at the corresponding stages.

8. pipeline::run executes the principal data path’s PipelineRun stage. It evaluates the route’s Term tree as a structural fold (the catamorphism per ADR-029), applying the per-variant fold-rules across all twenty-one Term variants: Term::Literal emits a constant byte sequence at its declared Witt level; Term::Variable looks up the binding identified by name_index (name_index = 0 resolves to the route input value serialized via IntoBindingValue per ADR-023; other indices resolve to let-introduced bindings); Term::Application applies a PrimitiveOp to the recursively-folded args (per the canonical catalog at the snapshot per ADR-013/TR-08, including byte-level comparison and concatenation per the foundation 0.3.5+ catalog); Term::Lift/Project perform Witt-level transitions; Term::Match dispatches on the scrutinee against the arm patterns; Term::Recurse performs well-founded recursion guarded by the descent measure with the iteration counter bound through the foundation-fixed RECURSE_IDX_NAME_INDEX per ADR-034; Term::Unfold performs the coalgebraic step; Term::Try propagates failures through the outer Result or routes them through a handler; Term::AxisInvocation (the substitution-axis-realized verb form per ADR-026 G19, generalized per ADR-030) routes through the application’s AxisTuple selection to the right axis impl; per ADR-055’s universal substrate-Term verb body discipline, the fold-rule then recursively folds the axis impl’s SubstrateTermBody::body_arena() static Term slice rather than calling an opaque kernel function, extending fold-fusion’s structural reach to the leaf level across every axis surface for every axis impl (standard-library AND application-author custom); Term::ProjectField (per ADR-033) slices a byte range from a recursively-folded source value to extract a product-shape field; Term::FirstAdmit (per ADR-034) iterates idx ascending across [0, <domain>::CYCLE_SIZE) with the candidate bound through the foundation-fixed FIRST_ADMIT_IDX_NAME_INDEX, structurally short-circuiting at the first admitting candidate and emitting a coproduct-shaped TermValue ((0x01, idx_bytes) for found, (0x00, padding) for not-found); the nine ψ-chain Term variants per ADR-035 (Nerve, ChainComplex, HomologyGroups, Betti, CochainComplex, CohomologyGroups, PostnikovTower, HomotopyGroups, KInvariants) lower from closure-body grammar forms G21-G29 and parallel the ontology-defined ψ-maps (ψ_1..ψ_9) — eight of the variants are resolver-bound, dispatching through the Has<Category>Resolver<A> marker-trait accessors on the model’s R: ResolverTuple per ADR-036 at evaluation time (per ADR-060 each resolver returns a TermValue directly — fn resolve(&self, input: TermValue<'a, {carrier_inline_bytes::<B>()}>) → Result<TermValue<'a, {carrier_inline_bytes::<B>()}>, ShapeViolation> — constructing whichever carrier variant Inline / Borrowed / Stream its ψ-stage output requires, rather than the pre-0.5.0 writer-style form that wrote into a caller-supplied &mut [u8] and returned a byte count; per-ψ-stage carrier widths derive from foundation const fn and no per-stage allocation occurs for Inline/Borrowed outputs; per ADR-057, the ψ_1 NerveResolver additionally resolves ConstraintRef::Recurse references encountered while walking the typed-feature-hierarchy’s CONSTRAINTS array, consulting foundation’s shape_iri_registry via lookup_shape(shape_iri) and unrolling the referenced shape’s CONSTRAINTS up to the descent budget — the simplicial complex N© emerges from the dynamically-unrolled constraint set with the descent decrement bottoming out at the typed feature hierarchy’s irreducible leaves), and the resolver-free variant Betti extracts the Betti-number array directly from the HomologyGroups byte serialization; resolver shape-violations (RESOLVER_ABSENT for NullResolverTuple's Null* impls, CAPACITY_EXCEEDED for oversized outputs) propagate through Term::Try per ADR-022 D3 G9. The ψ-residuals discipline per ADR-035 + ADR-056 forbids direct syntactic emissions of Term::FirstAdmit, Term::AxisInvocation, and byte-comparison/concat PrimitiveOps from the route body’s syntactic surface (the prism_model!-declared route closure body); compound verbs per ADR-024, axis impl bodies per ADR-055, and resolver bodies per ADR-046 may compose the full substrate vocabulary internally — fold-fusion per ADR-054 inlines them through the catamorphism at evaluation time without exposing residual forms at the route surface. The canonical compiled form is the k-invariants branch ψ_1 → ψ_7 → ψ_8 → ψ_9 producing a constant-width κ-label that classifies the value’s homotopy type up to weak equivalence. The catamorphism produces output bytes, populated into the Grounded's value payload (per ADR-028, accessible via output_bytes()). The stage produces a Grounded<Output> (carrying both the metadata fingerprint and the value payload) and a Trace simultaneously, constructed from the same data so that replayability (constraint TC-05) holds by construction. Validated, Grounded, and Certified are constructed by prism's seal regime.

9. The canonical hash axis (HashAxis from prism-crypto per ADR-031, consumed type-associatedly through the A: AxisTuple + Hasher substrate parameter per ADR-030 + ADR-036 via <A as Hasher>::initial()) is invoked exactly once during pipeline execution — at the certificate emission stage, to compute the ContentFingerprint carried by the GroundingCertificate. The route body’s syntactic surface contains no axis-method invocations (the ψ-residuals discipline per ADR-035 + ADR-056 forbids direct Term::AxisInvocation emissions from the route closure body); compound verbs declared via verb! per ADR-024 and axis impl bodies per ADR-055 may invoke axis methods internally through the substrate-Term verb body discipline (fold-fusion per ADR-054 inlines them at the catamorphism without exposing residual forms at the route surface), and resolver impls invoked by resolver-bound ψ-Term fold-rules may internally call the canonical hash axis as part of producing per-value structural witnesses; those calls are resolver- or fold-fusion-internal and conceptually distinct from the certificate-emission invocation.

10. The application receives (Grounded<Output>, Trace) and proceeds with its domain logic. The output value is read from the Grounded via output_bytes() (ADR-028); the metadata fingerprint and unit_address remain accessible for path attestation and content addressing. For typed feature hierarchies whose admission relations are inhabitance questions, the application consumes Grounded<Output> as the cert:InhabitanceCertificate envelope per ADR-039 + ADR-042 via the foundation-provided typed view Grounded::as_inhabitance_certificate(&self) -> InhabitanceCertificate<'_, Output>. The view’s accessors expose the κ-label via kappa_label() (the Term::KInvariants emission at ψ_9 per ADR-035, returned as KInvariantsBytes<'_> per ADR-041), the concrete cert:witness ValueTuple via witness() (derivable from Term::Nerve's 0-simplices at ψ_1), the cert:searchTrace via search_trace() (the recoverable Trace per ADR-019’s anamorphism dual), and the cert:certifiedType IRI via certified_type(). A catamorphism failure Err(PipelineFailure) whose structural cause is "the constraint nerve has empty Kan completion" yields a cert:InhabitanceImpossibilityCertificate envelope via PipelineFailure::as_inhabitance_impossibility_certificate(&self) → Option<…>, with contradiction_proof() exposing the canonical-form failure trace (the proof:InhabitanceImpossibilityWitness payload).

Properties

This scenario satisfies the following normative properties:

• No code outside uor-foundation and prism is invoked during steps 4 through 9. The interaction is contained within the application’s compiled executable plus both crates' compiled code. (The pipeline runtime is in prism; the four UOR-domain mint primitives are in uor-foundation; the three Prism-mechanism sealed-type constructors are in prism's seal regime.)

• No allocation occurs in the default-feature build (the #![no_std] posture, section 8). With the alloc feature enabled, allocation is bounded by the HostBounds selection.

• No runtime dispatch occurs (constraint TC-01). All trait method calls are resolved by the Rust toolchain at the application author’s compile time.

• The canonical hash axis (HashAxis from prism-crypto per ADR-031, consumed type-associatedly through the A: AxisTuple + Hasher substrate parameter) is invoked exactly once at the certificate-emission stage to compute the ContentFingerprint carried by the GroundingCertificate. Verb bodies emit no Term::AxisInvocation (forbidden per ADR-035’s ψ-residuals discipline); resolver impls invoked by resolver-bound ψ-Term fold-rules may invoke the canonical hash axis internally as part of producing per-value structural witnesses, but those are resolver-internal calls distinct from the certificate-emission invocation. The certificate-emission invocation remains exactly once.

• The Trace is constructed from the same intermediate values that produced the Grounded<T>. The trace is not a separate computation; it is a record of the principal data path’s traversal.

Scenario 2: Trace-Replay Verification

This scenario specifies the runtime behavior when the application user invokes certify_from_trace against a Trace they received from the application author. The interaction is internal to the user’s verification executable; no external system is contacted, the application author is not reached, no decider is invoked.

Sequence

1. The application user (or a third party they trust) obtains a Trace value through whatever channel they share with the application author. The trace is a byte sequence; the user deserializes it through the wire format specified in section 8.

2. The user instantiates a Hasher whose identifier matches the hasher_identifier carried in the trace. If no matching Hasher is available, this scenario terminates: the verifier cannot proceed without the matching hasher.

3. The user invokes certify_from_trace(trace, hasher_instance) through prism-verify's re-export. Control transfers from the user’s code to prism-verify's re-exported certify_from_trace, whose implementation lives in prism's replay component. The function reads wire-format type definitions (Trace, TraceEvent, Certificate, Hasher) from uor-foundation's bridge component.

4. certify_from_trace validates the trace’s format_version against TRACE_REPLAY_FORMAT_VERSION. Mismatch produces ReplayError::FormatVersion and this scenario terminates.

5. certify_from_trace validates the trace’s hasher_identifier against the supplied hasher_instance's identifier. Mismatch produces ReplayError::HasherMismatch and this scenario terminates.

6. certify_from_trace walks the trace’s event sequence in order. For each TraceEvent, it applies the variant-specific structural validation specified in section 8.

7. certify_from_trace does not invoke the hasher_instance. The hasher is provided so that its identifier can be confirmed; the function never calls its hashing method.

8. certify_from_trace does not invoke any decider from the application author’s code. Specifically, the function does not invoke Grounding, ConstrainedTypeShape, pipeline::run, or any PrimitiveOp. It walks the trace structurally.

9. Upon successful walk completion, certify_from_trace constructs Certified<GroundingCertificate> from the trace’s ContentFingerprint (carried unchanged from the trace) and the certificate-emission event’s recorded data.

10. The user receives Certified<GroundingCertificate> and treats it as the verification’s positive outcome. If any step in the walk failed, the user receives a structured ReplayError instead and treats it as the negative outcome.

Properties

This scenario satisfies the following normative properties:

• No invocation of the application author’s deciders occurs (constraint TC-05). The verifier walks the trace’s recorded data; it does not re-run the operations the trace records.

• No invocation of any cryptographic hash function occurs (constraint TC-05). The ContentFingerprint is data carried by the trace.

• No external system is contacted. The verification is entirely local.

• The verification time scales with the trace size, not with the original input size. A trace’s event count is bounded by the trace event-count ceiling carried by the application’s selected HostBounds, so verification has a bounded upper time complexity.

• The round-trip property holds: for every Grounded<T> value produced through Scenario 1 with hasher H, applying Scenario 2 to the trace using a Hasher instance with H's identifier returns a Certified<GroundingCertificate> whose Certificate is bit-identical to the certificate the original Grounded<T> carried.

Scenario 3: Compile-Time UORassembly Enforcement

This scenario specifies the deterministic interaction that occurs when the Rust toolchain compiles the application author’s source. The interaction is not "runtime" in the sense of the application’s execution; however, constraint TC-04 makes UORassembly enforcement a normative compile-time event whose specification is part of Prism’s architecture.

Sequence

1. The application author invokes cargo build (or equivalent) on their crate. The Rust toolchain begins resolving the crate’s dependency graph.

2. The toolchain compiles uor-foundation (or retrieves it pre-compiled from cache). The foundation’s compilation succeeds; the foundation’s published surface includes the trait surfaces, sealed types, and constants prism references.

3. The toolchain compiles prism against uor-foundation. prism's source declares trait bounds against the foundation’s surface (e.g., where T: ConstrainedTypeShape<H>, where H: HostTypes + HostBounds + Hasher). The toolchain checks each bound. If uor-foundation does not satisfy any bound, the prism compilation fails; the application author’s compilation halts with a type error pointing at the foundation’s missing or non-conforming surface.

4. With prism compiled successfully, the toolchain compiles the application author’s crate. The crate imports prism; expansions of product_shape!, coproduct_shape!, and cartesian_product_shape! macros (which live in uor-foundation's internal proc-macro sub-crate, reached through prism's vocabulary re-exports) emit absolute-path references into uor-foundation's surface.

5. The toolchain checks the author’s ConstrainedTypeShape impls, Grounding impls, and substitution-axis selections against prism's bounds. Each bound check is mechanical: the type system either confirms the bound is satisfied or rejects the source with a typed error.

6. If any bound check fails, compilation halts. The author receives a rustc error pointing at the specific clause of the UORassembly contract (section 8) that was violated. The error is a typed bound failure, not a panic, not a warning.

7. If all bound checks succeed, the toolchain emits the compiled executable. The executable contains prism's pipeline runtime as compiled code; the executable contains no UORassembly enforcement code (the contract has been fully discharged at this scenario’s time).

Properties

This scenario satisfies the following normative properties:

• The enforcement is bilateral. Step 3 enforces UORassembly against uor-foundation; step 5 enforces it against the application author’s crate. Both must satisfy prism's bounds (constraint TC-04, ADR-006).

• The enforcement is exclusively at compile time. No runtime check is performed; the produced executable contains no UORassembly assertions, no type-tag inspections, no validation calls (constraint TC-01).

• The enforcement is exclusively through the Rust type system. No external linter, no code-generation step beyond proc-macro expansion, no separate validation tool participates (ADR-006, rejected alternative 3).

• Compilation is deterministic. The same source against the same toolchain version produces the same compiled executable, modulo timestamps the toolchain itself injects.

Scenario 4: Distribute and Run

This scenario specifies the interaction between the application author and the application user that brings the executable from the author’s compilation environment to the user’s hardware. The interaction is mediated by a distribution channel of the author’s choosing; Prism is silent on the channel mechanism (ADR-004).

Sequence

1. The application author completes Scenario 3 successfully and obtains a compiled executable.

2. The application author publishes the executable to a distribution channel of their choosing. Possibilities include: a release page, a package registry, a peer-to-peer network, a signed Git repository, removable media. Prism does not participate in this step.

3. The application user obtains the executable from the distribution channel. The mechanism is the same one the author used; the user’s role is to retrieve, not to negotiate. Prism does not participate in this step.

4. The application user runs the executable on local hardware. The executable processes input the user provides through whatever interface the application’s domain logic exposes (CLI, GUI, batch input, embedded sensor — the domain logic is the author’s, not Prism’s).

5. The executable performs Scenario 1 internally. It produces sealed outputs (Grounded<T>, Trace, Certified<GroundingCertificate>) and surfaces whichever of these the application’s domain logic exposes to the user.

6. The user, optionally, invokes Scenario 2 against any Trace the application produced, using a verification executable they obtained through the same distribution channel (or a different one — Prism does not participate).

Properties

This scenario satisfies the following normative properties:

• No infrastructure operated by the application author is required for steps 3 through 6 (constraint TC-06). The author’s role ends at step 2; the author is not contacted thereafter.

• The user’s verification (step 6) requires only the trace and a verification executable. The author’s source code, the author’s deciders, and the author’s hasher implementation are not required.

• The distribution channel does not participate in the application’s correctness. A compromised channel can deliver a different executable, but the user can detect this by computing the executable’s content address against an out-of-band reference (e.g., a signed release manifest the author publishes alongside the executable). The wiki is silent on this mechanism; it is the application author’s choice of supply-chain integrity.

• The user’s verification of an output is independent of the executable’s authenticity. Verification confirms the output’s claims given the trace; it does not confirm that the executable producing the trace was the one the author published. These are orthogonal properties; Prism specifies the former, leaves the latter to whatever distribution-channel integrity mechanism the application author selects.

Cross-Scenario Properties

The four scenarios above compose to satisfy the system-level properties enumerated in section 1 (Quality Goals) and section 2 (Architecture Constraints). The composition properties:

• Sealed types never leave their owning crate’s construction discipline. Across all four scenarios, the three Prism-mechanism types (Validated, Grounded, Certified) are produced by prism's crate-internal constructors (in Scenario 1 by pipeline::run, in Scenario 2 by certify_from_trace). The four UOR-domain types (Triad, Derivation, FreeRank, Datum) are produced by uor-foundation's crate-internal constructors via the public mint_* primitives that prism's pipeline calls. The application author’s code and the user’s code receive these values but cannot construct them (constraint TC-02).

• The principal data path is exercised exactly once per produced output. Scenario 1 invokes the path; Scenario 2 walks the trace produced by Scenario 1 without re-invoking the path. There is no second path through which a Grounded<T> can arise (constraint TC-03).

• No cryptographic hashing occurs at verification time. Scenario 1 invokes the Hasher exactly once at certificate emission. Scenario 2 confirms the Hasher identifier matches but never invokes the hasher’s hashing method (constraint TC-05).

• No author infrastructure mediates any scenario. Scenarios 1 and 2 are local to the user’s hardware. Scenario 3 is local to the author’s compilation environment. Scenario 4 transits a distribution channel that Prism does not participate in (constraint TC-06).

<Runtime Scenario 1>

Resolved by Scenario 1 above: Principal Data Path Execution — what happens at runtime when the application author’s compiled executable processes input through pipeline::run.

<Runtime Scenario 2>

Resolved by Scenario 2 above: Trace-Replay Verification — what happens when the application user invokes certify_from_trace against a Trace they received.

…​

Resolved by Scenario 3 above: Compile-Time UORassembly Enforcement — the deterministic toolchain interaction during the application author’s cargo build that enforces the UORassembly contract bilaterally at compile time.

<Runtime Scenario n>

Resolved by Scenario 4 above: Distribute and Run — what happens between the application author finishing compilation and the user obtaining the final output. The four numbered scenarios above are exhaustive; the chapter specifies no further runtime scenarios.