Conceptual Model

Conceptual Model

ISO 19450 Conformance

This chapter expresses Prism's conceptual model in Object-Process Methodology (OPM) per the normative source:

ISO/PAS 19450:2015 — Automation systems and integration — Object-Process Methodology, First edition, 2015-12-15 (ICS 25.040.40, 35.240.50). Advanced to ISO 19450:2024 (Second edition, 2024-04). Published by the International Organization for Standardization. The 2015 edition (Public Available Specification, ISO/PAS) is the source the wiki's pinned OPL EBNF transcription at tools/iso-19450-opl.ebnf targets; the 2024 edition advances the same content to a full ISO standard with the same Annex A formal-syntax structure.

Supplementary sources corroborating this chapter's OPM transcription:

• Dori, D. (2002). "From Object-Process Diagrams to a Natural Object-Process Language." In: A.B. Pidduck et al. (Eds.): CAiSE 2002, LNCS 2348, pp. 221–238. Springer-Verlag. Establishes the canonical OPL production rules in their original R-numbered form (R1–R20+); predates the ISO standard.
• Dori, D. (2016). Model-Based Systems Engineering with OPM and SysML. Springer New York. ISBN 978-1-4939-3294-8. Chapter 11 ("Object-Process Language: The Text") aligns with Annex A of the standard.
• ISO 19450:2015 free preview (Foreword, Introduction, Clauses 1–3) — confirms term vocabulary and the bimodal-equivalence principle V7 enforces. Available at iso.org's preview viewer.

Per the standard's Foreword, compliance may involve the use of a patent concerning OPM as a modelling system (Clauses 6–14). The patent holder, Prof. Dov Dori (Technion — Israel Institute of Technology), has assured ISO of willingness to license under reasonable and non-discriminatory terms.

OPM specifies a bimodal representation: each conceptual statement appears as both an Object-Process Diagram (OPD) — the visual rendering — and an Object-Process Language (OPL) sentence — the textual rendering. The two modes are semantically equivalent per the standard's bimodality principle; V6 (OPL syntax conformance) and V7 (OPD–OPL coherence) validators enforce equivalence on every OPD-OPL pair in this chapter.

The standard's normative content used here:

• §6 Object-Process Diagram (OPD) — diagram syntax: object rectangles, process ellipses, structural and procedural links, in-zoom and out-zoom refinement.
• §7 Object-Process Language (OPL) — natural-language form: sentence productions R1–R20+ in Annex A's EBNF.
• §8 Generic OPM ontology — essence predicate (physical | informatical), affiliation predicate (environmental | systemic), structural relations (exhibits, consists of, is a), procedural relations (requires, yields, affects, handles, invokes).

The OPDs are organized as a progressive in-zoom hierarchy per §6.5 of the standard: the top-level System Diagram (SD) presents the system at its highest abstraction; subsequent diagrams (SD1, SD2, …) in-zoom into a specific top-level component or process. Each OPD's narrative below names which top-level entity it refines, cites the architectural commitment it upholds, and cross-references the arc42 chapter (sections 3–8) elaborating its content normatively.

Cost-Model Established by the Conceptual Model

The conceptual model is load-bearing for Prism's cost commitments — the architecture (chapters 4, 5, 8, 9) and the implementation must uphold the cost-model the OPM establishes here, not the reverse. Four cost-model commitments are normative at the conceptual layer:

C1 — Operational cost equals declared bandwidth, at equality

For a PrismModel declaring a TypedCommitment carrying K bits of typed-bandwidth admission predicates per ADR-048, the expected number of forward(input) invocations to find a κ-label satisfying the commitment equals α⁻¹ × 2^K at the σ-Projection Hardening Principle's U6 bandwidth-additivity axiom (ADR-047), where α is the admission probability of the base relation σ(x) ≤ target declared via ConstraintRef::Bound per ADR-040. The relation is tight (equality, not upper bound) — the Lean tight-bound theorem Commitment.prf_prob_tight_wellFormed (foundation-side Lean corpus) is the formal proof.

The conceptual commitment: the host's retry loop count is the only externality; everything else is structural. The architecture's role (chapters 5, 9) is to monomorphize the typed commitment so its evaluation adds no per-invocation cost beyond the K inlined predicate evaluations; the implementation's role is to realize this monomorphization through the substrate's TypedCommitment trait surface (ADR-048).

C2 — Zero runtime movement per inference

A forward(input) invocation that produces Ok(Grounded<Output>) performs:

1. One catamorphism traversal of the verb body's Term arena per ADR-029 (stack-only; bounded by the Term arena's depth).
2. Eight resolver-bound ψ-stage emissions per ADR-035 (the canonical k-invariants branch: ψ_1, ψ_7, ψ_8, ψ_9, plus four off-path stages for substitution-axis completeness per ADR-036).
3. K inlined ObservablePredicate::evaluate calls per ADR-049 inside the post-resolver C::evaluate(kappa_label) consultation per ADR-048.

No heap allocation along the principal data path (TC-01 + ADR-019 + #![no_std] posture). No dynamic dispatch (no Vec, no dyn per ADR-048's rejected alternative 2). No runtime-unknown loop bounds (every loop is bounded by a HostBounds associated constant per ADR-037 or a ConstrainedTypeShape::CYCLE_SIZE per ADR-032). Per-invocation cost is O(1) + K · t_eval where t_eval is the per-predicate observable-read cost (O(digest_byte_length), a single pass over the digest bytes).

Structural mechanism — the Fold-Fusion Principle (ADR-054) with universal axis-body enforcement (ADR-055). C2 is realized by fold fusion: every prism transformation — verb-body composition, prism_model! route body, resolver body, and every axis-impl body — is a folding operation, and the catamorphism's universal property (ADR-019) fuses composed fold-rules into a single structure-preserving map. Three fusion layers stack: (i) macro-expansion fusion — verb-call sites lower to Term subtrees at proc-macro expansion (ADR-024); after expansion the verb-call walker is absent at run time. (ii) catamorphism fusion — the per-variant fold-rules (ADR-029) compose universally; the initial-algebra property guarantees there is no choice about how to fuse them. (iii) monomorphization fusion — the resulting per-substitution-axis-selection Rust routine has no dynamic dispatch and no allocation (TC-01); LLVM inlining collapses per-variant dispatch with fold-rule bodies into straight-line code. Per ADR-055's universal substrate-Term verb body discipline, every AxisExtension impl (standard-library AND application-author custom) carries a substrate-Term verb body via the foundation-declared SubstrateTermBody sealed supertrait bound — the catamorphism's Term::AxisInvocation fold-rule recursively folds the axis's body_arena() static Term slice rather than calling an opaque kernel function. Fold-fusion's structural reach extends to the leaf level across every axis surface for every axis impl. There is no carve-out for "novel-domain axes": per ADR-019's initial-algebra commitment, every prism operation is substrate-Term decomposable; operations that cannot be decomposed are not prism operations and must be hosted at the host boundary outside the catamorphism's reach. C2's "one Rust function per forward invocation" claim is structurally guaranteed, not provisional — fold-fusion holds universally for every prism transformation, enforced at compile time through the SubstrateTermBody supertrait bound.

C3 — Structural inference, not search

The conceptual model commits Prism to one structural inference per input at the typed-iso surface. The catamorphism's per-variant fold-rules per ADR-029 traverse the Term arena deterministically; the resolver-internal iterative-resolution discipline per ADR-043 is not a search over the typed-iso surface — it is the substrate's structural-transform realization machinery (the ψ-residuals discipline per ADR-035 + ADR-046 forbids search-shaped emissions in verb bodies; the resolver-internal loop is admissible because resolver bodies are not closure-body expressions per ADR-046).

The conceptual commitment: admission is a structural property of the value's k-invariant signature, not a runtime predicate over byte values. The host-boundary retry mechanism (varying the input outside the iterative-resolution domain) is external to the catamorphism's per-invocation contract.

C4 — σ-projection axis qualification is conceptual, not implementation

The canonical hash axis selection (the third substitution position per ADR-030) must satisfy the σ-Projection Hardening Principle's six axioms (U1–U6 per ADR-047) for the cost-model commitments above to hold. A non-conforming Hasher impl introduces a cheaper-than-σ observable predicting admission, which invalidates C1's equality: the empirical trial count falls below α⁻¹ × 2^K (a structural attack exploits the non-conformance). U1–U6 are conceptual axioms on the projection's structural properties; the empirical witness through axis::cryptanalyze per ADR-049 audits the axioms; foundation's CI enforces conformance on every release.

Reading order

The OPDs below proceed from the most-abstract (SD, system context) to specific in-zooms (principal data path, verification, compile-time enforcement, distribute-and-run). Each OPD's narrative names which cost-model commitment(s) (C1–C4) it upholds and cross-references the arc42 chapter elaborating its content. Read SD first; then read the subsequent SDs in the order they appear; the conceptual layering matches the architectural exposition.

SD

OPD kind: System Diagram (the top-level OPD per ISO 19450 §6.5.1). Names the system, its environmental actors, and the system-level data flows.

Architectural commitment: This OPD declares Prism as the single informatical system (Prism is informatical.) with three environmental actors — the Application Author (physical), the Application User (physical), and the Rust Toolchain (informatical-environmental). The system's three input dependencies (Rust Toolchain, Author Source, Host Bytes) and three output products (Grounded Output, Trace, Certified Output) are the system-level surface elaborated in chapters 3 (Context and Scope) and 5 (Building Block View).

Cost-model commitments upheld: All of C1–C4. The SD declares the system whose cost-model the conceptual model establishes:

• C1 (operational cost = declared bandwidth at equality) is realized at this layer as the relationship between one Host Bytes admission (one forward(input) invocation) and one Grounded Output emission. The host-side retry loop (varying Host Bytes to find an admitting κ-label) is the externality C1 names.
• C2 (zero runtime movement) is realized as the single yields relation from Prism to each of its three outputs — no intermediate state object persists across invocations.
• C3 (structural inference) is realized as the directness of the requires / yields relations — Prism's relationship to its inputs is structural admission, not iterative refinement.
• C4 (axis qualification) is realized at this layer through the opacity of the σ-projection inside Prism — the SD does not reveal the canonical hash axis selection because the axis-qualification commitment is per-axis, not per-system; the in-zoom into SD2 surfaces the axis-mediated pipeline.

ISO 19450 vocabulary used:

• essence predicate (§8.3): physical for human actors; informatical for software and data; the Rust Toolchain is both environmental and informatical since it lives outside Prism but is informatical in essence.
• affiliation predicate (§8.4): all three actors are environmental (outside the system boundary); Prism and its data products are systemic (inside the system boundary, implicit since Prism is named as the system).
• handles relation (§7.3.4): connects environmental physical actors to the system they interact with — both Application Author and Application User handle Prism.
• requires / yields (§7.3.2–§7.3.3): the system's input-output procedural surface.

Arc42 cross-reference: Chapter 3 (Context and Scope) — the SD is the OPM realization of §3.1 (Business Context) and §3.2 (Technical Context); chapter 1 (Introduction and Goals) — the SD's actors are the three external stakeholders named in §1.2.

Application Author is environmental and physical.
Application User is environmental and physical.
Rust Toolchain is environmental and informatical.
Author Source is informatical.
Host Bytes is informatical.
Grounded Output is informatical.
Trace is informatical.
Certified Output is informatical.
Prism is informatical.
Application Author handles Prism.
Application User handles Prism.
Prism requires Rust Toolchain.
Prism requires Author Source.
Prism requires Host Bytes.
Prism yields Grounded Output.
Prism yields Trace.
Prism yields Certified Output.

SD1 Prism Structure

OPD kind: In-zoom of the Prism informatical object from SD (per ISO 19450 §6.5.4). Refines Prism's internal structure by enumerating its consists of constituents — the three architectural containers (Substrate, Runtime, Replay Surface) — and their exhibits attributes.

Architectural commitment: This OPD declares Prism's three-container decomposition per ADR-002 (three-crate architecture: uor-foundation is Substrate; prism is Runtime; prism-verify is Replay Surface). Each container's attribute set is enumerated: Substrate exhibits Type Vocabulary, Mint Primitive, and Wire Format Type; Runtime exhibits Pipeline Runtime and Sealed Type; Replay Surface exhibits Wire Format Type and Sealed Type. The procedural relations declare Pipeline Runtime's dependencies and emissions: it requires Mint Primitive (admission via foundation's sealed-type construction primitives per ADR-016) and yields Trace plus yields Certificate.

Cost-model commitments upheld:

• C2 (zero runtime movement) is upheld structurally by the Sealed Type attribute appearing on both Runtime and Replay Surface (the type-system mechanism per ADR-011 + ADR-016 that prevents allocation-forcing intermediate constructions; sealed types descend only from sanctioned construction paths, so the principal data path has no escape into heap-allocated intermediate forms).
• C3 (structural inference) is upheld through the Pipeline Runtime requires Mint Primitive link — admission to the principal data path is structural mint, not search-based intake. The mint primitive surface is constrained per ADR-016 to a single sanctioned caller (prism's pipeline), making the construction path of every sealed value structural.
• C4 (axis qualification) is upheld by the Type Vocabulary attribute on Substrate — the canonical hash axis selection lives in the substrate's vocabulary (per ADR-030 + ADR-031); axis-qualification per the Hardening Principle (ADR-047) applies at the substrate layer where the vocabulary is declared.

ISO 19450 vocabulary used:

• consists of relation (§7.3.1): the structural-aggregation link — Prism consists of Substrate, Runtime, and Replay Surface.
• exhibits relation (§7.3.1): the attribute-on-object link — each container exhibits its declared attribute set.
• In-zoom (§6.5.4): the diagrammatic refinement of an SD-level object into its constituent structure.

Arc42 cross-reference: Chapter 5 (Building Block View) — the SD1 is the OPM realization of §5.1 (Whitebox Overall System); chapter 2 (Architecture Constraints) — the three-container decomposition is constrained by TC-02 (sealed-type construction discipline) elaborated in §2.2. ADR-002 commits the three-crate decomposition; ADR-011 + ADR-016 commit the seal regime the Sealed Type attribute realizes.

Prism is informatical.
Substrate is informatical.
Runtime is informatical.
Replay Surface is informatical.
Type Vocabulary is informatical.
Mint Primitive is informatical.
Wire Format Type is informatical.
Pipeline Runtime is informatical.
Sealed Type is informatical.
Trace is informatical.
Certificate is informatical.
Prism consists of Substrate, Runtime, and Replay Surface.
Substrate exhibits Type Vocabulary.
Substrate exhibits Mint Primitive.
Substrate exhibits Wire Format Type.
Runtime exhibits Pipeline Runtime.
Runtime exhibits Sealed Type.
Replay Surface exhibits Wire Format Type.
Replay Surface exhibits Sealed Type.
Pipeline Runtime requires Mint Primitive.
Pipeline Runtime yields Trace.
Pipeline Runtime yields Certificate.

SD2 Principal Data Path

OPD kind: In-zoom of the principal data path's process surface (per ISO 19450 §6.5.4 — process in-zoom). Refines the SD-level requires Host Bytes → yields Grounded Output + Trace procedural surface into the four-stage pipeline: Grounding, Compile Unit Construction, Validation, and Pipeline Run.

Architectural commitment: This OPD declares Prism's four-stage principal data path per ADR-010 (pipeline staging) + ADR-015 (catamorphism's evaluation environment). Each stage's requires / yields surface is named, with invokes links chaining the stages into a single bidirectional dependency: Grounding invokes Compile Unit Construction; Compile Unit Construction invokes Validation; Validation invokes Pipeline Run. Each stage may yield an Impossibility Witness (the negative-verdict path per ADR-039 + ADR-042) instead of progressing to the next stage; the impossibility witness is the conceptual model's realization of Err(PipelineFailure).

Cost-model commitments upheld:

• C1 (operational cost = declared bandwidth at equality) is upheld at the Pipeline Run stage, which requires Validated Compile Unit and yields Grounded Output plus Trace. The κ-label emission inside the Pipeline Run stage carries the typed-bandwidth commitment evaluated per ADR-048 (the CommitmentEvaluated trace event records the K-predicate conjunction's result inside the Trace yielded here).
• C2 (zero runtime movement) is upheld by the linearity of the invocation chain — each invokes link is a single stage transition with no fan-out, no rollback, no intermediate persistence. The catamorphism's per-variant fold-rules (per ADR-029) run inside Pipeline Run; there are no inter-stage allocations. The Fold-Fusion Principle (ADR-054) with universal axis-body enforcement (ADR-055) is the structural mechanism: every transformation reachable from Pipeline Run — verb-body composition, ψ-stage emissions, post-resolver C::evaluate consultation, every axis-impl body (standard-library AND application-author custom per ADR-055's SubstrateTermBody supertrait bound) — is a folding operation, and the catamorphism's initial-algebra universal property fuses composed fold-rules into one Rust routine per substitution-axis selection. The fusion stacks three layers: macro-expansion (verb calls dissolve at proc-macro time), catamorphism (per-variant fold-rules compose universally per ADR-019; Term::AxisInvocation recursively folds the axis impl's body_arena() static Term slice rather than calling an opaque kernel function), and monomorphization (LLVM inlining collapses to straight-line code per TC-01). C2's guarantee is type-system-enforced — axis impls without a substrate-Term body clause fail to compile.
• C3 (structural inference) is upheld by the Impossibility Witness emission path — admission failures surface as structural witnesses (proof:InhabitanceImpossibilityWitness per ADR-039), not as retry signals; the host-boundary retry loop is external to this OPD (it operates at the SD level, varying Host Bytes between invocations of this entire pipeline).
• C4 (axis qualification) is upheld through the Validation stage's structural check — the validation phase per ADR-022 D4 confirms the Term arena is closure-conformant before Pipeline Run consumes it; the σ-projection axis selection per ADR-030 is consulted inside Pipeline Run's resolver-bound ψ-stages per ADR-035 + ADR-036.

ISO 19450 vocabulary used:

• invokes relation (§7.3.5): the chained-process link — each stage triggers the next stage's invocation. The chain Grounding → Compile Unit Construction → Validation → Pipeline Run is the canonical principal data path.
• requires / yields (§7.3.2–§7.3.3): per-stage input-output surface.
• handles (§7.3.4): the Application User initiates the data path by handling Grounding.

Arc42 cross-reference: Chapter 6 (Runtime View) — SD2 is the OPM realization of §6.1 Scenario 1 (Principal Data Path Execution); chapter 5 §5.3 (Level 3 Whitebox: pipeline component); ADRs ADR-010 (pipeline staging), ADR-015 (catamorphism's evaluation environment), ADR-029 (per-variant fold-rules), ADR-035 (canonical ψ-pipeline), ADR-036 (ResolverTuple dispatch), ADR-043 (iterative-resolution discipline), ADR-048 (TypedCommitment post-resolver consultation).

Application User is environmental and physical.
Host Bytes is informatical.
Datum is informatical.
Compile Unit is informatical.
Validated Compile Unit is informatical.
Grounded Output is informatical.
Trace is informatical.
Impossibility Witness is informatical.
Grounding is informatical.
Compile Unit Construction is informatical.
Validation is informatical.
Pipeline Run is informatical.
Application User handles Grounding.
Grounding requires Host Bytes.
Grounding yields Datum.
Grounding yields Impossibility Witness.
Grounding invokes Compile Unit Construction.
Compile Unit Construction requires Datum.
Compile Unit Construction yields Compile Unit.
Compile Unit Construction invokes Validation.
Validation requires Compile Unit.
Validation yields Validated Compile Unit.
Validation yields Impossibility Witness.
Validation invokes Pipeline Run.
Pipeline Run requires Validated Compile Unit.
Pipeline Run yields Grounded Output.
Pipeline Run yields Trace.

SD3 Verification

OPD kind: In-zoom of the Application User's verification activity (per ISO 19450 §6.5.4). Refines the SD-level yields Trace + Certified Output procedural surface into the four-stage replay path: Trace Reception, Structural Validation, Certificate Reconstruction, and Sealing.

Architectural commitment: This OPD declares the anamorphism dual to SD2's catamorphism per ADR-019 (categorical structure: catamorphism + anamorphism = hylomorphism with verifiable round-trip). The Application User receives a Trace (from any source — typically alongside a Grounded<Output> from a prior forward(input)) plus the Hasher Identifier (out-of-band per ADR-008's wire-format discipline), runs Trace Reception which yields the Hasher Selection, invokes Structural Validation, which invokes Certificate Reconstruction, which invokes Sealing, producing the Certified Output. The Replay Error path is the negative-verdict surface — Structural Validation can short-circuit with a Replay Error on wire-format malformation, version mismatch, or Hasher identifier mismatch.

Cost-model commitments upheld:

• C2 (zero runtime movement) is upheld through the replay path's complete non-evaluation of the application author's deciders. Per ADR-019 + ADR-021, replay walks the trace's typed derivation steps without re-invoking the catamorphism's fold-rules; the verifier's per-event cost is bounded by the trace's event-count ceiling per ADR-018 (<B as HostBounds>::TRACE_MAX_EVENTS). No allocation along the verification path; the Certificate Reconstruction stage builds the certificate from the trace's ContentFingerprint plus the Hasher Selection without re-evaluating the original inference.
• C3 (structural inference) is upheld by the Structural Validation stage — the validation is purely structural (each TraceEvent's payload is checked against the foundation's known catalogs per ADR-008's verifier-check discipline plus ADR-038/ADR-049's Observable IRI catalog for CommitmentEvaluated events); no admission decision is re-derived. The replay surface confirms the original inference was well-typed; it does not re-perform the inference.
• C4 (axis qualification) is upheld by the Hasher Selection step — Trace Reception requires the Hasher Identifier (carried inside the trace per §8 wire format) plus the matching Hasher Selection (which the verifier resolves out-of-band per TC-05); mismatch fails closed with ReplayError::HasherMismatch. The verifier's σ-projection axis MUST match the original inference's axis selection for the certificate's content-fingerprint to round-trip; this is the structural dependence of C4 on identical-axis-conformance at both endpoints.

ISO 19450 vocabulary used:

• exhibits (§7.3.1): structural attributes on Trace (Trace Event, Content Fingerprint, Hasher Identifier) and on Certificate (Content Address); these are the wire-format structural elements per ADR-008.
• invokes (§7.3.5): the chained-stage link in the replay sequence.
• requires / yields (§7.3.2–§7.3.3): per-stage input-output surface, paralleling SD2's principal data path but in the verification direction.

Arc42 cross-reference: Chapter 6 (Runtime View) — SD3 is the OPM realization of §6.2 Scenario 2 (Trace Replay and Verification); chapter 8 (Concepts) — the wire-format details of Trace and Certificate live in §8 (Trace Wire Format, Certificate Format); ADRs ADR-008 (trace wire format), ADR-019 (categorical structure: catamorphism + anamorphism), ADR-021 (V&V framework), TC-05 (replay equivalence constraint).

Application User is environmental and physical.
Trace is informatical.
Hasher Identifier is informatical.
Hasher Selection is informatical.
Trace Event is informatical.
Content Address is informatical.
Content Fingerprint is informatical.
Certificate is informatical.
Certified Output is informatical.
Replay Error is informatical.
Trace Reception is informatical.
Structural Validation is informatical.
Certificate Reconstruction is informatical.
Sealing is informatical.
Trace exhibits Trace Event.
Trace exhibits Content Fingerprint.
Trace exhibits Hasher Identifier.
Certificate exhibits Content Address.
Application User handles Trace Reception.
Trace Reception requires Trace.
Trace Reception requires Hasher Identifier.
Trace Reception yields Hasher Selection.
Trace Reception invokes Structural Validation.
Structural Validation requires Trace.
Structural Validation invokes Certificate Reconstruction.
Structural Validation yields Replay Error.
Certificate Reconstruction requires Trace.
Certificate Reconstruction requires Hasher Selection.
Certificate Reconstruction yields Certificate.
Certificate Reconstruction invokes Sealing.
Sealing requires Certificate.
Sealing yields Certified Output.

SD4 UORassembly Enforcement

OPD kind: In-zoom of the compile-time bilateral-enforcement process (per ISO 19450 §6.5.4). Refines the SD-level requires Rust Toolchain + Author Source surface into the compilation flow: Compilation (handled by the Application Author) requires the Rust Toolchain + Author Source + Substrate + Runtime, invokes Bound Checking against the UORassembly Contract, and yields the Compiled Executable.

Architectural commitment: This OPD declares Prism's compile-time enforcement per ADR-006 (bilateral compile-time UORassembly contract) — the closure check is performed by the type system, not by a separate verifier. The UORassembly Contract is the union of architectural constraints that the type system enforces at the Application Author's compile time: ψ-residuals discipline per ADR-035 (verb body grammar), FoundationClosed impl emission per ADR-020 (every Term node must be foundation-vocabulary), ConstrainedTypeShape closure per ADR-013 (TC-01: primitive set closed at foundation layer), seal regime per ADR-011 (TC-02: sealed types unconstructable outside their owning crate), single-path discipline per ADR-016 (TC-03), bilateral compile-time enforcement per ADR-006 (TC-04). The contract is bilateral — both prism and the Application Author's crate satisfy the contract through type-system bounds.

Cost-model commitments upheld:

• C2 (zero runtime movement) is upheld causally by SD4 — the compile-time bilateral check is what makes runtime zero-cost achievable. Closure under foundation vocabulary (per ADR-013) means every primitive operation is known at compile time; monomorphization per TC-01 turns the typed-iso surface into inlinable code; the TypedCommitment chain per ADR-048 + the resolver impls per ADR-036 monomorphize into the Compiled Executable's static text. SD4's Bound Checking is the architectural guarantee that the runtime zero-cost commitment is structurally upheld for every Compiled Executable.
• C3 (structural inference) is upheld through the ψ-residuals discipline per ADR-035 + ADR-046, which is part of the UORassembly Contract — the proc-macro's verb-body parse rejects Term::FirstAdmit, Term::AxisInvocation, and byte-comparison/concat PrimitiveOp emissions in verb bodies. A verb body that compiles successfully through SD4 is structurally guaranteed to be search-free at the typed-iso surface.
• C4 (axis qualification) is upheld through the canonical hash axis selection landing in the Substrate before SD4 runs — the Application Author selects a Hasher impl whose Hardening Principle conformance (U1–U6 per ADR-047) is witnessed by axis::cryptanalyze per ADR-049; SD4's Bound Checking does not re-validate the axis's structural properties (those are foundation-CI's responsibility), but it does enforce that the selected axis is foundation-vetted (the Hasher trait is sealed via __sdk_seal::Sealed per ADR-022 D1, so external impls are non-conforming).

ISO 19450 vocabulary used:

• requires (§7.3.2): Compilation requires four objects — the Rust Toolchain (environmental), the Author Source (the application crate's code), the Substrate, and the Runtime. The four-way requires declares the bilateral nature of the check.
• invokes (§7.3.5): Compilation invokes Bound Checking — the type system's trait-resolver evaluates the UORassembly Contract bounds.
• yields (§7.3.3): Compilation yields the Compiled Executable — the sole positive outcome; compilation failure yields no executable.
• handles (§7.3.4): the Application Author initiates Compilation.

Arc42 cross-reference: Chapter 6 (Runtime View) — SD4 is the OPM realization of §6.3 Scenario 3 (Compile-Time UORassembly Enforcement); chapter 2 (Architecture Constraints) — the UORassembly Contract is the union of TC-01..TC-05 elaborated in §2.1 + §2.2; ADRs ADR-006 (bilateral compile-time UORassembly), ADR-011 (seal regime), ADR-013 (closure under foundation), ADR-016 (mint primitive single-caller), ADR-022 D1 (sealed-trait pattern), ADR-035 (ψ-residuals discipline), ADR-046 (resolver-body discipline scope).

Application Author is environmental and physical.
Rust Toolchain is environmental and informatical.
Author Source is informatical.
Substrate is informatical.
Runtime is informatical.
UORassembly Contract is informatical.
Compiled Executable is informatical.
Compilation is informatical.
Bound Checking is informatical.
Application Author handles Compilation.
Compilation requires Rust Toolchain.
Compilation requires Author Source.
Compilation requires Substrate.
Compilation requires Runtime.
Compilation invokes Bound Checking.
Bound Checking requires UORassembly Contract.
Compilation yields Compiled Executable.

SD5 Distribute And Run

OPD kind: In-zoom of the author-to-user handoff process (per ISO 19450 §6.5.4). Refines the cross-actor procedural surface between SD's two environmental physical actors (Application Author and Application User) into the four-stage handoff path: Publication, Retrieval, Execution, and Verification.

Architectural commitment: This OPD declares Prism's distribution semantics per ADR-008 (trace wire format) + ADR-017 (canonical UOR-address mapping) — the Application Author publishes the Compiled Executable through a Distribution Channel (environmental-informatical, outside Prism's substrate); the Application User retrieves it, executes it (producing a Trace), and verifies the Trace independently (producing a Certified Output). The architectural commitment is that the verification path's correctness depends on no out-of-band channel — the Trace itself (per §8 wire format) carries everything the verifier needs to re-derive the Certified Output, modulo the out-of-band Hasher Selection per ADR-008's hasher_identifier field per TC-05.

Cost-model commitments upheld:

• C1 (operational cost = declared bandwidth at equality) is upheld at the system boundary — the Application User's Execution invocation produces a Trace whose CommitmentEvaluated events (per ADR-048's wire-format extension) record the typed-bandwidth admission's per-κ-label cost. The host-side retry loop (Application User varying Host Bytes between Execution invocations) is the externality named in C1; the per-Execution cost itself is bounded by the catamorphism's per-invocation structural cost.
• C2 (zero runtime movement) is upheld through the Compiled Executable's self-containment — Execution requires only the Compiled Executable plus the runtime input bytes; no shared library, no dynamic plugin, no out-of-band configuration affects the per-invocation cost. The Compiled Executable's text is the monomorphized output of SD4's Compilation; per-invocation cost is static across all Execution invocations of a given executable.
• C3 (structural inference) is upheld by the yields Trace link on Execution — every Execution produces exactly one Trace per forward(input) invocation; the Trace's structural events (per ADR-008) record the structural inference without any search trace.
• C4 (axis qualification) is upheld through Verification's reliance on the matching Hasher Selection — if the canonical hash axis at the Author endpoint and the User endpoint mismatch (different Hasher impl), the trace's hasher_identifier mismatches the verifier's configuration and Verification fails closed. The Hardening Principle's U1–U6 conformance per ADR-047 applies at both endpoints; if the axis at the author endpoint passes the battery but the axis at the verifier endpoint does not (because the user configured a non-conforming impl), the certificate's content-fingerprint will not round-trip — Verification yields a Replay Error, not a Certified Output.

ISO 19450 vocabulary used:

• handles (§7.3.4): each environmental physical actor handles one process — Application Author handles Publication; Application User handles Retrieval + Execution + Verification.
• affects relation (§7.3.6): Publication affects the Distribution Channel — the channel's state is mutated by Publication (a new Compiled Executable is added).
• requires / yields (§7.3.2–§7.3.3): per-stage input-output surface across the actor boundary.

Arc42 cross-reference: Chapter 6 (Runtime View) — SD5 is the OPM realization of §6.4 Scenario 4 (Author-to-User Distribution and Independent Verification); chapter 7 (Deployment View) — the Distribution Channel + actor topology elaborated in §7; ADRs ADR-008 (trace wire format — load-bearing for the verifier's structural validation), ADR-017 (canonical UOR-address mapping — the content-addressing surface the verifier walks), TC-05 (replay equivalence — the round-trip property SD5 realizes end-to-end).

Application Author is environmental and physical.
Application User is environmental and physical.
Distribution Channel is environmental and informatical.
Compiled Executable is informatical.
Trace is informatical.
Certified Output is informatical.
Publication is informatical.
Retrieval is informatical.
Execution is informatical.
Verification is informatical.
Application Author handles Publication.
Publication requires Compiled Executable.
Publication affects Distribution Channel.
Application User handles Retrieval.
Retrieval requires Distribution Channel.
Retrieval yields Compiled Executable.
Application User handles Execution.
Execution requires Compiled Executable.
Execution yields Trace.
Application User handles Verification.
Verification requires Trace.
Verification yields Certified Output.